From 8e2e31c0663e976373a6519ef493d438095bd63c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pol=27tta=20/=20Miyahara=20K=C5=8D?= Date: Tue, 4 Jun 2024 18:12:25 +0000 Subject: [PATCH] style: remove mathport output (#13198) --- Mathlib/Algebra/Category/Ring/Limits.lean | 4 --- .../Computation/TerminatesIffRat.lean | 1 - Mathlib/Algebra/MvPolynomial/Degrees.lean | 1 - Mathlib/Algebra/Ring/Subring/Basic.lean | 2 -- Mathlib/Analysis/Matrix.lean | 1 - .../CategoryTheory/Functor/FullyFaithful.lean | 2 -- Mathlib/CategoryTheory/Monoidal/Mod_.lean | 1 - .../Enumerative/Composition.lean | 4 --- Mathlib/Data/FinEnum.lean | 3 -- Mathlib/Data/Int/Bitwise.lean | 1 - Mathlib/Data/Multiset/Basic.lean | 2 -- Mathlib/Data/Nat/Pairing.lean | 2 -- Mathlib/Data/Ordmap/Ordnode.lean | 2 -- Mathlib/Data/PFunctor/Multivariate/Basic.lean | 1 - Mathlib/Data/Semiquot.lean | 6 ---- Mathlib/Data/Seq/Computation.lean | 1 - Mathlib/Data/Set/Lattice.lean | 28 ------------------- Mathlib/GroupTheory/CoprodI.lean | 2 -- Mathlib/Logic/Equiv/Fin.lean | 2 -- Mathlib/SetTheory/ZFC/Basic.lean | 2 -- Mathlib/Topology/Algebra/Semigroup.lean | 4 --- Mathlib/Topology/Instances/AddCircle.lean | 1 - 22 files changed, 73 deletions(-) diff --git a/Mathlib/Algebra/Category/Ring/Limits.lean b/Mathlib/Algebra/Category/Ring/Limits.lean index 4fd8a7952fb137..d94dd52a715a27 100644 --- a/Mathlib/Algebra/Category/Ring/Limits.lean +++ b/Mathlib/Algebra/Category/Ring/Limits.lean @@ -134,7 +134,6 @@ instance hasLimit : HasLimit F := ⟨limitCone.{v, u} F, limitConeIsLimit.{v, u} /-- If `J` is `u`-small, `SemiRingCat.{u}` has limits of shape `J`. -/ instance hasLimitsOfShape [Small.{u} J] : HasLimitsOfShape J SemiRingCat.{u} where -/- ./././Mathport/Syntax/Translate/Command.lean:322:38: unsupported irreducible non-definition -/ /-- The category of rings has all limits. -/ instance hasLimitsOfSize [UnivLE.{v, u}] : HasLimitsOfSize.{w, v} SemiRingCat.{u} where has_limits_of_shape _ _ := { } @@ -299,7 +298,6 @@ instance hasLimit : HasLimit F := ⟨limitCone.{v, u} F, limitConeIsLimit.{v, u} /-- If `J` is `u`-small, `CommSemiRingCat.{u}` has limits of shape `J`. -/ instance hasLimitsOfShape [Small.{u} J] : HasLimitsOfShape J CommSemiRingCat.{u} where -/- ./././Mathport/Syntax/Translate/Command.lean:322:38: unsupported irreducible non-definition -/ /-- The category of rings has all limits. -/ instance hasLimitsOfSize [UnivLE.{v, u}] : HasLimitsOfSize.{w, v} CommSemiRingCat.{u} where set_option linter.uppercaseLean3 false in @@ -431,7 +429,6 @@ instance hasLimit : HasLimit F := /-- If `J` is `u`-small, `RingCat.{u}` has limits of shape `J`. -/ instance hasLimitsOfShape [Small.{u} J] : HasLimitsOfShape J RingCat.{u} where -/- ./././Mathport/Syntax/Translate/Command.lean:322:38: unsupported irreducible non-definition -/ /-- The category of rings has all limits. -/ instance hasLimitsOfSize [UnivLE.{v, u}] : HasLimitsOfSize.{w, v} RingCat.{u} where set_option linter.uppercaseLean3 false in @@ -597,7 +594,6 @@ instance hasLimit : HasLimit F := /-- If `J` is `u`-small, `CommRingCat.{u}` has limits of shape `J`. -/ instance hasLimitsOfShape [Small.{u} J] : HasLimitsOfShape J CommRingCat.{u} where -/- ./././Mathport/Syntax/Translate/Command.lean:322:38: unsupported irreducible non-definition -/ /-- The category of commutative rings has all limits. -/ instance hasLimitsOfSize [UnivLE.{v, u}] : HasLimitsOfSize.{w, v} CommRingCat.{u} where set_option linter.uppercaseLean3 false in diff --git a/Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean b/Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean index f4869f7ecf21cf..4c47dc483814e1 100644 --- a/Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean +++ b/Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean @@ -33,7 +33,6 @@ rational, continued fraction, termination namespace GeneralizedContinuedFraction -/- ./././Mathport/Syntax/Translate/Command.lean:230:11: unsupported: unusual advanced open style -/ open GeneralizedContinuedFraction (of) variable {K : Type*} [LinearOrderedField K] [FloorRing K] diff --git a/Mathlib/Algebra/MvPolynomial/Degrees.lean b/Mathlib/Algebra/MvPolynomial/Degrees.lean index 653a25c04bcd68..e502891da378c4 100644 --- a/Mathlib/Algebra/MvPolynomial/Degrees.lean +++ b/Mathlib/Algebra/MvPolynomial/Degrees.lean @@ -471,7 +471,6 @@ theorem totalDegree_X_pow [Nontrivial R] (s : σ) (n : ℕ) : set_option linter.uppercaseLean3 false in #align mv_polynomial.total_degree_X_pow MvPolynomial.totalDegree_X_pow -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ theorem totalDegree_list_prod : ∀ s : List (MvPolynomial σ R), s.prod.totalDegree ≤ (s.map MvPolynomial.totalDegree).sum | [] => by rw [@List.prod_nil (MvPolynomial σ R) _, totalDegree_one]; rfl diff --git a/Mathlib/Algebra/Ring/Subring/Basic.lean b/Mathlib/Algebra/Ring/Subring/Basic.lean index 62aea80fb3cc1f..0433841134ec92 100644 --- a/Mathlib/Algebra/Ring/Subring/Basic.lean +++ b/Mathlib/Algebra/Ring/Subring/Basic.lean @@ -1322,8 +1322,6 @@ variable {s : Set R} -- attribute [local reducible] closure -- Porting note: not available in Lean4 -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ @[elab_as_elim] protected theorem InClosure.recOn {C : R → Prop} {x : R} (hx : x ∈ closure s) (h1 : C 1) (hneg1 : C (-1)) (hs : ∀ z ∈ s, ∀ n, C n → C (z * n)) (ha : ∀ {x y}, C x → C y → C (x + y)) : diff --git a/Mathlib/Analysis/Matrix.lean b/Mathlib/Analysis/Matrix.lean index 9cf9dd8d94fc23..341e2d0bb4f00f 100644 --- a/Mathlib/Analysis/Matrix.lean +++ b/Mathlib/Analysis/Matrix.lean @@ -333,7 +333,6 @@ section NonUnitalSeminormedRing variable [NonUnitalSeminormedRing α] -/- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (k j) -/ theorem linfty_opNNNorm_mul (A : Matrix l m α) (B : Matrix m n α) : ‖A * B‖₊ ≤ ‖A‖₊ * ‖B‖₊ := by simp_rw [linfty_opNNNorm_def, Matrix.mul_apply] calc diff --git a/Mathlib/CategoryTheory/Functor/FullyFaithful.lean b/Mathlib/CategoryTheory/Functor/FullyFaithful.lean index 000fb47bdd5891..f49c902ad882b1 100644 --- a/Mathlib/CategoryTheory/Functor/FullyFaithful.lean +++ b/Mathlib/CategoryTheory/Functor/FullyFaithful.lean @@ -46,8 +46,6 @@ class Full (F : C ⥤ D) : Prop where map_surjective {X Y : C} : Function.Surjective (F.map (X := X) (Y := Y)) #align category_theory.full CategoryTheory.Functor.Full -/- ./././Mathport/Syntax/Translate/Command.lean:379:30: infer kinds are unsupported in Lean 4: -#[`map_injective'] [] -/ /-- A functor `F : C ⥤ D` is faithful if for each `X Y : C`, `F.map` is injective. See . diff --git a/Mathlib/CategoryTheory/Monoidal/Mod_.lean b/Mathlib/CategoryTheory/Monoidal/Mod_.lean index ad42552943df7b..38d700eddce715 100644 --- a/Mathlib/CategoryTheory/Monoidal/Mod_.lean +++ b/Mathlib/CategoryTheory/Monoidal/Mod_.lean @@ -39,7 +39,6 @@ theorem assoc_flip : set_option linter.uppercaseLean3 false in #align Mod_.assoc_flip Mod_.assoc_flip -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ /-- A morphism of module objects. -/ @[ext] structure Hom (M N : Mod_ A) where diff --git a/Mathlib/Combinatorics/Enumerative/Composition.lean b/Mathlib/Combinatorics/Enumerative/Composition.lean index e59943c0e18dff..e2c1da7651622a 100644 --- a/Mathlib/Combinatorics/Enumerative/Composition.lean +++ b/Mathlib/Combinatorics/Enumerative/Composition.lean @@ -625,8 +625,6 @@ namespace List variable {α : Type*} -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ /-- Auxiliary for `List.splitWrtComposition`. -/ def splitWrtCompositionAux : List α → List ℕ → List (List α) | _, [] => [] @@ -645,8 +643,6 @@ def splitWrtComposition (l : List α) (c : Composition n) : List (List α) := -- Porting note: can't refer to subeqn in Lean 4 this way, and seems to definitionally simp --attribute [local simp] splitWrtCompositionAux.equations._eqn_1 -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ @[local simp] theorem splitWrtCompositionAux_cons (l : List α) (n ns) : l.splitWrtCompositionAux (n::ns) = take n l::(drop n l).splitWrtCompositionAux ns := by diff --git a/Mathlib/Data/FinEnum.lean b/Mathlib/Data/FinEnum.lean index 1bb43d0cdaf4f6..fa2b0fbaa660fa 100644 --- a/Mathlib/Data/FinEnum.lean +++ b/Mathlib/Data/FinEnum.lean @@ -20,8 +20,6 @@ universe u v open Finset -/- ./././Mathport/Syntax/Translate/Command.lean:379:30: - infer kinds are unsupported in Lean 4: #[`Equiv] [] -/ /-- `FinEnum α` means that `α` is finite and can be enumerated in some order, i.e. `α` has an explicit bijection with `Fin n` for some n. -/ class FinEnum (α : Sort*) where @@ -105,7 +103,6 @@ instance punit : FinEnum PUnit := ofList [PUnit.unit] fun x => by cases x; simp #align fin_enum.punit FinEnum.punit -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ instance prod {β} [FinEnum α] [FinEnum β] : FinEnum (α × β) := ofList (toList α ×ˢ toList β) fun x => by cases x; simp #align fin_enum.prod FinEnum.prod diff --git a/Mathlib/Data/Int/Bitwise.lean b/Mathlib/Data/Int/Bitwise.lean index 03fccceab66ef0..f01aa8185d0b72 100644 --- a/Mathlib/Data/Int/Bitwise.lean +++ b/Mathlib/Data/Int/Bitwise.lean @@ -310,7 +310,6 @@ theorem testBit_bit_succ (m b) : ∀ n, testBit (bit b n) (Nat.succ m) = testBit #align int.test_bit_succ Int.testBit_bit_succ -- Porting note (#11215): TODO --- /- ./././Mathport/Syntax/Translate/Expr.lean:333:4: warning: unsupported (TODO): `[tacs] -/ -- private unsafe def bitwise_tac : tactic Unit := -- sorry -- #align int.bitwise_tac int.bitwise_tac diff --git a/Mathlib/Data/Multiset/Basic.lean b/Mathlib/Data/Multiset/Basic.lean index de156456b406d2..2ea5887258bccb 100644 --- a/Mathlib/Data/Multiset/Basic.lean +++ b/Mathlib/Data/Multiset/Basic.lean @@ -2627,8 +2627,6 @@ theorem count_map {α β : Type*} (f : α → β) (s : Multiset α) [DecidableEq simp [Bool.beq_eq_decide_eq, eq_comm, count, countP_map] #align multiset.count_map Multiset.count_map -/- ./././Mathport/Syntax/Translate/Basic.lean:632:2: warning: - expanding binder collection (x «expr ∈ » s) -/ /-- `Multiset.map f` preserves `count` if `f` is injective on the set of elements contained in the multiset -/ theorem count_map_eq_count [DecidableEq β] (f : α → β) (s : Multiset α) diff --git a/Mathlib/Data/Nat/Pairing.lean b/Mathlib/Data/Nat/Pairing.lean index 2152b876778ab2..ad633cd6078da1 100644 --- a/Mathlib/Data/Nat/Pairing.lean +++ b/Mathlib/Data/Nat/Pairing.lean @@ -196,8 +196,6 @@ end CompleteLattice namespace Set -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ theorem iUnion_unpair_prod {α β} {s : ℕ → Set α} {t : ℕ → Set β} : ⋃ n : ℕ, s n.unpair.fst ×ˢ t n.unpair.snd = (⋃ n, s n) ×ˢ ⋃ n, t n := by rw [← Set.iUnion_prod] diff --git a/Mathlib/Data/Ordmap/Ordnode.lean b/Mathlib/Data/Ordmap/Ordnode.lean index 2e3c9592360893..095d6b99958b34 100644 --- a/Mathlib/Data/Ordmap/Ordnode.lean +++ b/Mathlib/Data/Ordmap/Ordnode.lean @@ -65,8 +65,6 @@ ordered map, ordered set, data structure universe u -/- ./././Mathport/Syntax/Translate/Command.lean:355:30: infer kinds are unsupported in Lean 4: - nil {} -/ /-- An `Ordnode α` is a finite set of values, represented as a tree. The operations on this type maintain that the tree is balanced and correctly stores subtree sizes at each level. -/ diff --git a/Mathlib/Data/PFunctor/Multivariate/Basic.lean b/Mathlib/Data/PFunctor/Multivariate/Basic.lean index 52e7534fc60521..b96c22c532474f 100644 --- a/Mathlib/Data/PFunctor/Multivariate/Basic.lean +++ b/Mathlib/Data/PFunctor/Multivariate/Basic.lean @@ -242,7 +242,6 @@ def last : PFunctor where B a := (P.B a).last #align mvpfunctor.last MvPFunctor.last -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ /-- append arrows of a polynomial functor application -/ abbrev appendContents {α : TypeVec n} {β : Type*} {a : P.A} (f' : P.drop.B a ⟹ α) (f : P.last.B a → β) : P.B a ⟹ (α ::: β) := diff --git a/Mathlib/Data/Semiquot.lean b/Mathlib/Data/Semiquot.lean index 9519f80eaa34d9..5983def896eccd 100644 --- a/Mathlib/Data/Semiquot.lean +++ b/Mathlib/Data/Semiquot.lean @@ -106,16 +106,12 @@ def toTrunc (q : Semiquot α) : Trunc α := q.2.map Subtype.val #align semiquot.to_trunc Semiquot.toTrunc -/- ./././Mathport/Syntax/Translate/Basic.lean:632:2: -warning: expanding binder collection (a b «expr ∈ » q) -/ /-- If `f` is a constant on `q.s`, then `q.liftOn f` is the value of `f` at any point of `q`. -/ def liftOn (q : Semiquot α) (f : α → β) (h : ∀ a ∈ q, ∀ b ∈ q, f a = f b) : β := Trunc.liftOn q.2 (fun x => f x.1) fun x y => h _ x.2 _ y.2 #align semiquot.lift_on Semiquot.liftOn -/- ./././Mathport/Syntax/Translate/Basic.lean:632:2: -warning: expanding binder collection (a b «expr ∈ » q) -/ theorem liftOn_ofMem (q : Semiquot α) (f : α → β) (h : ∀ a ∈ q, ∀ b ∈ q, f a = f b) (a : α) (aq : a ∈ q) : liftOn q f h = f a := by revert h; rw [eq_mk_of_mem aq]; intro; rfl @@ -201,8 +197,6 @@ theorem pure_le {a : α} {s : Semiquot α} : pure a ≤ s ↔ a ∈ s := Set.singleton_subset_iff #align semiquot.pure_le Semiquot.pure_le -/- ./././Mathport/Syntax/Translate/Basic.lean:632:2: -warning: expanding binder collection (a b «expr ∈ » q) -/ /-- Assert that a `Semiquot` contains only one possible value. -/ def IsPure (q : Semiquot α) : Prop := ∀ a ∈ q, ∀ b ∈ q, a = b diff --git a/Mathlib/Data/Seq/Computation.lean b/Mathlib/Data/Seq/Computation.lean index ee8c37fb2c6081..5441536e1c7899 100644 --- a/Mathlib/Data/Seq/Computation.lean +++ b/Mathlib/Data/Seq/Computation.lean @@ -47,7 +47,6 @@ def pure (a : α) : Computation α := instance : CoeTC α (Computation α) := ⟨pure⟩ -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ -- note [use has_coe_t] /-- `think c` is the computation that delays for one "tick" and then performs computation `c`. -/ diff --git a/Mathlib/Data/Set/Lattice.lean b/Mathlib/Data/Set/Lattice.lean index a57cceecb9d076..6a3a630671a2f6 100644 --- a/Mathlib/Data/Set/Lattice.lean +++ b/Mathlib/Data/Set/Lattice.lean @@ -1335,13 +1335,11 @@ theorem inter_eq_iInter {s₁ s₂ : Set α} : s₁ ∩ s₂ = ⋂ b : Bool, con inf_eq_iInf s₁ s₂ #align set.inter_eq_Inter Set.inter_eq_iInter -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ theorem sInter_union_sInter {S T : Set (Set α)} : ⋂₀ S ∪ ⋂₀ T = ⋂ p ∈ S ×ˢ T, (p : Set α × Set α).1 ∪ p.2 := sInf_sup_sInf #align set.sInter_union_sInter Set.sInter_union_sInter -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ theorem sUnion_inter_sUnion {s t : Set (Set α)} : ⋃₀s ∩ ⋃₀t = ⋃ p ∈ s ×ˢ t, (p : Set α × Set α).1 ∩ p.2 := sSup_inf_sSup @@ -1764,51 +1762,37 @@ end Preimage section Prod -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ theorem prod_iUnion {s : Set α} {t : ι → Set β} : (s ×ˢ ⋃ i, t i) = ⋃ i, s ×ˢ t i := by ext simp #align set.prod_Union Set.prod_iUnion -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ /- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/ /- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/ -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ theorem prod_iUnion₂ {s : Set α} {t : ∀ i, κ i → Set β} : (s ×ˢ ⋃ (i) (j), t i j) = ⋃ (i) (j), s ×ˢ t i j := by simp_rw [prod_iUnion] #align set.prod_Union₂ Set.prod_iUnion₂ -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ theorem prod_sUnion {s : Set α} {C : Set (Set β)} : s ×ˢ ⋃₀C = ⋃₀((fun t => s ×ˢ t) '' C) := by simp_rw [sUnion_eq_biUnion, biUnion_image, prod_iUnion₂] #align set.prod_sUnion Set.prod_sUnion -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ theorem iUnion_prod_const {s : ι → Set α} {t : Set β} : (⋃ i, s i) ×ˢ t = ⋃ i, s i ×ˢ t := by ext simp #align set.Union_prod_const Set.iUnion_prod_const -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ /- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/ /- ./././Mathport/Syntax/Translate/Expr.lean:107:6: warning: expanding binder group (i j) -/ -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ theorem iUnion₂_prod_const {s : ∀ i, κ i → Set α} {t : Set β} : (⋃ (i) (j), s i j) ×ˢ t = ⋃ (i) (j), s i j ×ˢ t := by simp_rw [iUnion_prod_const] #align set.Union₂_prod_const Set.iUnion₂_prod_const -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ theorem sUnion_prod_const {C : Set (Set α)} {t : Set β} : ⋃₀C ×ˢ t = ⋃₀((fun s : Set α => s ×ˢ t) '' C) := by simp only [sUnion_eq_biUnion, iUnion₂_prod_const, biUnion_image] #align set.sUnion_prod_const Set.sUnion_prod_const -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ theorem iUnion_prod {ι ι' α β} (s : ι → Set α) (t : ι' → Set β) : ⋃ x : ι × ι', s x.1 ×ˢ t x.2 = (⋃ i : ι, s i) ×ˢ ⋃ i : ι', t i := by ext @@ -1819,8 +1803,6 @@ theorem iUnion_prod {ι ι' α β} (s : ι → Set α) (t : ι' → Set β) : lemma iUnion_prod' (f : β × γ → Set α) : ⋃ x : β × γ, f x = ⋃ (i : β) (j : γ), f (i, j) := iSup_prod -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ theorem iUnion_prod_of_monotone [SemilatticeSup α] {s : α → Set β} {t : α → Set γ} (hs : Monotone s) (ht : Monotone t) : ⋃ x, s x ×ˢ t x = (⋃ x, s x) ×ˢ ⋃ x, t x := by ext ⟨z, w⟩; simp only [mem_prod, mem_iUnion, exists_imp, and_imp, iff_def]; constructor @@ -1830,17 +1812,11 @@ theorem iUnion_prod_of_monotone [SemilatticeSup α] {s : α → Set β} {t : α exact ⟨x ⊔ x', hs le_sup_left hz, ht le_sup_right hw⟩ #align set.Union_prod_of_monotone Set.iUnion_prod_of_monotone -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ theorem sInter_prod_sInter_subset (S : Set (Set α)) (T : Set (Set β)) : ⋂₀ S ×ˢ ⋂₀ T ⊆ ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2 := subset_iInter₂ fun x hx _ hy => ⟨hy.1 x.1 hx.1, hy.2 x.2 hx.2⟩ #align set.sInter_prod_sInter_subset Set.sInter_prod_sInter_subset -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ theorem sInter_prod_sInter {S : Set (Set α)} {T : Set (Set β)} (hS : S.Nonempty) (hT : T.Nonempty) : ⋂₀ S ×ˢ ⋂₀ T = ⋂ r ∈ S ×ˢ T, r.1 ×ˢ r.2 := by obtain ⟨s₁, h₁⟩ := hS @@ -1850,16 +1826,12 @@ theorem sInter_prod_sInter {S : Set (Set α)} {T : Set (Set β)} (hS : S.Nonempt exact ⟨fun s₀ h₀ => (hx (s₀, s₂) ⟨h₀, h₂⟩).1, fun s₀ h₀ => (hx (s₁, s₀) ⟨h₁, h₀⟩).2⟩ #align set.sInter_prod_sInter Set.sInter_prod_sInter -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ theorem sInter_prod {S : Set (Set α)} (hS : S.Nonempty) (t : Set β) : ⋂₀ S ×ˢ t = ⋂ s ∈ S, s ×ˢ t := by rw [← sInter_singleton t, sInter_prod_sInter hS (singleton_nonempty t), sInter_singleton] simp_rw [prod_singleton, mem_image, iInter_exists, biInter_and', iInter_iInter_eq_right] #align set.sInter_prod Set.sInter_prod -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ theorem prod_sInter {T : Set (Set β)} (hT : T.Nonempty) (s : Set α) : s ×ˢ ⋂₀ T = ⋂ t ∈ T, s ×ˢ t := by rw [← sInter_singleton s, sInter_prod_sInter (singleton_nonempty s) hT, sInter_singleton] diff --git a/Mathlib/GroupTheory/CoprodI.lean b/Mathlib/GroupTheory/CoprodI.lean index b64207426f935f..f1cac9b3632072 100644 --- a/Mathlib/GroupTheory/CoprodI.lean +++ b/Mathlib/GroupTheory/CoprodI.lean @@ -354,7 +354,6 @@ def cons {i} (m : M i) (w : Word M) (hmw : w.fstIdx ≠ some i) (h1 : m ≠ 1) : · exact w.ne_one l hl chain_ne := w.chain_ne.cons' (fstIdx_ne_iff.mp hmw) } -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ /-- Given a pair `(head, tail)`, we can form a word by prepending `head` to `tail`, except if `head` is `1 : M i` then we have to just return `Word` since we need the result to be reduced. -/ def rcons {i} (p : Pair M i) : Word M := @@ -444,7 +443,6 @@ theorem consRecOn_cons {motive : Word M → Sort*} (i) (m : M i) (w : Word M) h1 variable [DecidableEq ι] -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ -- This definition is computable but not very nice to look at. Thankfully we don't have to inspect -- it, since `rcons` is known to be injective. /-- Given `i : ι`, any reduced word can be decomposed into a pair `p` such that `w = rcons p`. -/ diff --git a/Mathlib/Logic/Equiv/Fin.lean b/Mathlib/Logic/Equiv/Fin.lean index acedd7ee508bec..95ed8241d42304 100644 --- a/Mathlib/Logic/Equiv/Fin.lean +++ b/Mathlib/Logic/Equiv/Fin.lean @@ -53,7 +53,6 @@ def piFinTwoEquiv (α : Fin 2 → Type u) : (∀ i, α i) ≃ α 0 × α 1 where #align pi_fin_two_equiv_symm_apply piFinTwoEquiv_symm_apply #align pi_fin_two_equiv_apply piFinTwoEquiv_apply -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ theorem Fin.preimage_apply_01_prod {α : Fin 2 → Type u} (s : Set (α 0)) (t : Set (α 1)) : (fun f : ∀ i, α i => (f 0, f 1)) ⁻¹' s ×ˢ t = Set.pi Set.univ (Fin.cons s <| Fin.cons t finZeroElim) := by @@ -61,7 +60,6 @@ theorem Fin.preimage_apply_01_prod {α : Fin 2 → Type u} (s : Set (α 0)) (t : simp [Fin.forall_fin_two] #align fin.preimage_apply_01_prod Fin.preimage_apply_01_prod -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ theorem Fin.preimage_apply_01_prod' {α : Type u} (s t : Set α) : (fun f : Fin 2 → α => (f 0, f 1)) ⁻¹' s ×ˢ t = Set.pi Set.univ ![s, t] := @Fin.preimage_apply_01_prod (fun _ => α) s t diff --git a/Mathlib/SetTheory/ZFC/Basic.lean b/Mathlib/SetTheory/ZFC/Basic.lean index 1f90c7baef4a11..9f0ac43fa9f08e 100644 --- a/Mathlib/SetTheory/ZFC/Basic.lean +++ b/Mathlib/SetTheory/ZFC/Basic.lean @@ -1707,7 +1707,6 @@ theorem eq_univ_of_powerset_subset {A : Class} (hA : powerset A ⊆ A) : A = uni WellFounded.not_lt_min ZFSet.mem_wf _ hnA hB <| coe_apply.1 hx)) #align Class.eq_univ_of_powerset_subset Class.eq_univ_of_powerset_subset -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ /-- The definite description operator, which is `{x}` if `{y | A y} = {x}` and `∅` otherwise. -/ def iota (A : Class) : Class := ⋃₀ { x | ∀ y, A y ↔ y = x } @@ -1771,7 +1770,6 @@ theorem choice_mem_aux (y : ZFSet.{u}) (yx : y ∈ x) : by_contradiction fun n => h <| by rwa [← (eq_empty y).2 fun z zx => n ⟨z, zx⟩] #align Set.choice_mem_aux ZFSet.choice_mem_aux -/- ./././Mathport/Syntax/Translate/Expr.lean:177:8: unsupported: ambiguous notation -/ theorem choice_isFunc : IsFunc x (⋃₀ x) (choice x) := (@map_isFunc _ (Classical.allDefinable _) _ _).2 fun y yx => mem_sUnion.2 ⟨y, yx, choice_mem_aux x h y yx⟩ diff --git a/Mathlib/Topology/Algebra/Semigroup.lean b/Mathlib/Topology/Algebra/Semigroup.lean index 347a580154c56e..b254fccb199fc7 100644 --- a/Mathlib/Topology/Algebra/Semigroup.lean +++ b/Mathlib/Topology/Algebra/Semigroup.lean @@ -19,8 +19,6 @@ We also state a corresponding lemma guaranteeing that a subset of `M` contains a -/ -/- ./././Mathport/Syntax/Translate/Basic.lean:628:2: warning: expanding binder - collection (m m' «expr ∈ » N) -/ /-- Any nonempty compact Hausdorff semigroup where right-multiplication is continuous contains an idempotent, i.e. an `m` such that `m * m = m`. -/ @[to_additive @@ -75,8 +73,6 @@ theorem exists_idempotent_of_compact_t2_of_continuous_mul_left {M} [Nonempty M] #align exists_idempotent_of_compact_t2_of_continuous_mul_left exists_idempotent_of_compact_t2_of_continuous_mul_left #align exists_idempotent_of_compact_t2_of_continuous_add_left exists_idempotent_of_compact_t2_of_continuous_add_left -/- ./././Mathport/Syntax/Translate/Basic.lean:628:2: warning: - expanding binder collection (x y «expr ∈ » s) -/ /-- A version of `exists_idempotent_of_compact_t2_of_continuous_mul_left` where the idempotent lies in some specified nonempty compact subsemigroup. -/ @[to_additive exists_idempotent_in_compact_add_subsemigroup diff --git a/Mathlib/Topology/Instances/AddCircle.lean b/Mathlib/Topology/Instances/AddCircle.lean index d27ec5f433221c..347cb0a1e6ebe0 100644 --- a/Mathlib/Topology/Instances/AddCircle.lean +++ b/Mathlib/Topology/Instances/AddCircle.lean @@ -559,7 +559,6 @@ section UnitAddCircle instance instZeroLTOne [StrictOrderedSemiring 𝕜] : Fact ((0 : 𝕜) < 1) := ⟨zero_lt_one⟩ -/- ./././Mathport/Syntax/Translate/Command.lean:328:31: unsupported: @[derive] abbrev -/ /-- The unit circle `ℝ ⧸ ℤ`. -/ abbrev UnitAddCircle := AddCircle (1 : ℝ)