diff --git a/Archive/Wiedijk100Theorems/Partition.lean b/Archive/Wiedijk100Theorems/Partition.lean index 1045104e58395..689d098bcd228 100644 --- a/Archive/Wiedijk100Theorems/Partition.lean +++ b/Archive/Wiedijk100Theorems/Partition.lean @@ -216,7 +216,7 @@ theorem partialGF_prop (α : Type*) [CommSemiring α] (n : ℕ) (s : Finset ℕ) intro a; exact Nat.lt_irrefl 0 (hs 0 (hp₂.2 0 a)) intro a; exact Nat.lt_irrefl 0 (hs 0 (hp₁.2 0 a)) · rw [← mul_left_inj' hi] - rw [Function.funext_iff] at h + rw [funext_iff] at h exact h.2 i · simp only [φ, mem_filter, mem_finsuppAntidiag, mem_univ, exists_prop, true_and, and_assoc] rintro f ⟨hf, hf₃, hf₄⟩ diff --git a/Mathlib/Algebra/BigOperators/Ring.lean b/Mathlib/Algebra/BigOperators/Ring.lean index 8ffa27de019be..ffe59a97cc2ff 100644 --- a/Mathlib/Algebra/BigOperators/Ring.lean +++ b/Mathlib/Algebra/BigOperators/Ring.lean @@ -168,7 +168,7 @@ theorem prod_add (f g : ι → α) (s : Finset ι) : (fun t _ a _ => a ∈ t) (by simp) (by simp [Classical.em]) - (by simp_rw [mem_filter, Function.funext_iff, eq_iff_iff, mem_pi, mem_insert]; tauto) + (by simp_rw [mem_filter, funext_iff, eq_iff_iff, mem_pi, mem_insert]; tauto) (by simp_rw [Finset.ext_iff, @mem_filter _ _ (id _), mem_powerset]; tauto) (fun a _ ↦ by simp only [prod_ite, filter_attach', prod_map, Function.Embedding.coeFn_mk, diff --git a/Mathlib/Algebra/Divisibility/Prod.lean b/Mathlib/Algebra/Divisibility/Prod.lean index 5eda6b629ea04..355b2cfd6033d 100644 --- a/Mathlib/Algebra/Divisibility/Prod.lean +++ b/Mathlib/Algebra/Divisibility/Prod.lean @@ -33,7 +33,7 @@ instance [DecompositionMonoid G₁] [DecompositionMonoid G₂] : DecompositionMo exact ⟨(a₁, a₂), (a₁', a₂'), ⟨h₁, h₂⟩, ⟨h₁', h₂'⟩, Prod.ext eq₁ eq₂⟩ theorem pi_dvd_iff {x y : ∀ i, G i} : x ∣ y ↔ ∀ i, x i ∣ y i := by - simp_rw [dvd_def, Function.funext_iff, Classical.skolem]; rfl + simp_rw [dvd_def, funext_iff, Classical.skolem]; rfl instance [∀ i, DecompositionMonoid (G i)] : DecompositionMonoid (∀ i, G i) where primal a b c h := by diff --git a/Mathlib/Algebra/Group/Pi/Lemmas.lean b/Mathlib/Algebra/Group/Pi/Lemmas.lean index a344930fb34fa..1dee66ec01d1b 100644 --- a/Mathlib/Algebra/Group/Pi/Lemmas.lean +++ b/Mathlib/Algebra/Group/Pi/Lemmas.lean @@ -70,7 +70,7 @@ def Pi.mulHom {γ : Type w} [∀ i, Mul (f i)] [Mul γ] (g : ∀ i, γ →ₙ* f theorem Pi.mulHom_injective {γ : Type w} [Nonempty I] [∀ i, Mul (f i)] [Mul γ] (g : ∀ i, γ →ₙ* f i) (hg : ∀ i, Function.Injective (g i)) : Function.Injective (Pi.mulHom g) := fun _ _ h => let ⟨i⟩ := ‹Nonempty I› - hg i ((Function.funext_iff.mp h : _) i) + hg i ((funext_iff.mp h : _) i) /-- A family of monoid homomorphisms `f a : γ →* β a` defines a monoid homomorphism `Pi.monoidHom f : γ →* Π a, β a` given by `Pi.monoidHom f x b = f b x`. -/ @@ -337,7 +337,7 @@ theorem SemiconjBy.pi {x y z : ∀ i, f i} (h : ∀ i, SemiconjBy (x i) (y i) (z @[to_additive] theorem Pi.semiconjBy_iff {x y z : ∀ i, f i} : - SemiconjBy x y z ↔ ∀ i, SemiconjBy (x i) (y i) (z i) := Function.funext_iff + SemiconjBy x y z ↔ ∀ i, SemiconjBy (x i) (y i) (z i) := funext_iff @[to_additive] theorem Commute.pi {x y : ∀ i, f i} (h : ∀ i, Commute (x i) (y i)) : Commute x y := .pi h diff --git a/Mathlib/Algebra/Homology/Functor.lean b/Mathlib/Algebra/Homology/Functor.lean index 59cf2538f199c..7560ad47ae5ed 100644 --- a/Mathlib/Algebra/Homology/Functor.lean +++ b/Mathlib/Algebra/Homology/Functor.lean @@ -37,11 +37,11 @@ def asFunctor {T : Type*} [Category T] (C : HomologicalComplex (T ⥤ V) c) : d := fun i j => (C.d i j).app t d_comp_d' := fun i j k _ _ => by have := C.d_comp_d i j k - rw [NatTrans.ext_iff, Function.funext_iff] at this + rw [NatTrans.ext_iff, funext_iff] at this exact this t shape := fun i j h => by have := C.shape _ _ h - rw [NatTrans.ext_iff, Function.funext_iff] at this + rw [NatTrans.ext_iff, funext_iff] at this exact this t } map h := { f := fun i => (C.X i).map h diff --git a/Mathlib/Algebra/LinearRecurrence.lean b/Mathlib/Algebra/LinearRecurrence.lean index b3b5648ee9db0..182a96ce2cf20 100644 --- a/Mathlib/Algebra/LinearRecurrence.lean +++ b/Mathlib/Algebra/LinearRecurrence.lean @@ -138,7 +138,7 @@ def toInit : E.solSpace ≃ₗ[α] Fin E.order → α where simp invFun u := ⟨E.mkSol u, E.is_sol_mkSol u⟩ left_inv u := by ext n; symm; apply E.eq_mk_of_is_sol_of_eq_init u.2; intro k; rfl - right_inv u := Function.funext_iff.mpr fun n ↦ E.mkSol_eq_init u n + right_inv u := funext_iff.mpr fun n ↦ E.mkSol_eq_init u n /-- Two solutions are equal iff they are equal on `range E.order`. -/ theorem sol_eq_of_eq_init (u v : ℕ → α) (hu : E.IsSolution u) (hv : E.IsSolution v) : diff --git a/Mathlib/Algebra/Module/ZLattice/Basic.lean b/Mathlib/Algebra/Module/ZLattice/Basic.lean index a436852b2ab88..f5d850e0a404e 100644 --- a/Mathlib/Algebra/Module/ZLattice/Basic.lean +++ b/Mathlib/Algebra/Module/ZLattice/Basic.lean @@ -276,7 +276,7 @@ theorem discreteTopology_pi_basisFun [Finite ι] : refine discreteTopology_iff_isOpen_singleton_zero.mpr ⟨Metric.ball 0 1, Metric.isOpen_ball, ?_⟩ ext x rw [Set.mem_preimage, mem_ball_zero_iff, pi_norm_lt_iff zero_lt_one, Set.mem_singleton_iff] - simp_rw [← coe_eq_zero, Function.funext_iff, Pi.zero_apply, Real.norm_eq_abs] + simp_rw [← coe_eq_zero, funext_iff, Pi.zero_apply, Real.norm_eq_abs] refine forall_congr' (fun i => ?_) rsuffices ⟨y, hy⟩ : ∃ (y : ℤ), (y : ℝ) = (x : ι → ℝ) i · rw [← hy, ← Int.cast_abs, ← Int.cast_one, Int.cast_lt, Int.abs_lt_one_iff, Int.cast_eq_zero] diff --git a/Mathlib/Algebra/Order/BigOperators/Group/Finset.lean b/Mathlib/Algebra/Order/BigOperators/Group/Finset.lean index d5cdc6b8f86e7..8593406fe5e67 100644 --- a/Mathlib/Algebra/Order/BigOperators/Group/Finset.lean +++ b/Mathlib/Algebra/Order/BigOperators/Group/Finset.lean @@ -519,11 +519,11 @@ lemma one_le_prod (hf : 1 ≤ f) : 1 ≤ ∏ i, f i := Finset.one_le_prod' fun _ @[to_additive] lemma prod_eq_one_iff_of_one_le (hf : 1 ≤ f) : ∏ i, f i = 1 ↔ f = 1 := - (Finset.prod_eq_one_iff_of_one_le' fun i _ ↦ hf i).trans <| by simp [Function.funext_iff] + (Finset.prod_eq_one_iff_of_one_le' fun i _ ↦ hf i).trans <| by simp [funext_iff] @[to_additive] lemma prod_eq_one_iff_of_le_one (hf : f ≤ 1) : ∏ i, f i = 1 ↔ f = 1 := - (Finset.prod_eq_one_iff_of_le_one' fun i _ ↦ hf i).trans <| by simp [Function.funext_iff] + (Finset.prod_eq_one_iff_of_le_one' fun i _ ↦ hf i).trans <| by simp [funext_iff] end OrderedCommMonoid diff --git a/Mathlib/Algebra/Polynomial/Smeval.lean b/Mathlib/Algebra/Polynomial/Smeval.lean index d24a7089bfc93..91d57a909fcc3 100644 --- a/Mathlib/Algebra/Polynomial/Smeval.lean +++ b/Mathlib/Algebra/Polynomial/Smeval.lean @@ -133,7 +133,7 @@ theorem smeval.linearMap_apply : smeval.linearMap R x p = p.smeval x := rfl theorem leval_coe_eq_smeval {R : Type*} [Semiring R] (r : R) : ⇑(leval r) = fun p => p.smeval r := by - rw [Function.funext_iff] + rw [funext_iff] intro rw [leval_apply, smeval_def, eval_eq_sum] rfl diff --git a/Mathlib/Analysis/Calculus/LagrangeMultipliers.lean b/Mathlib/Analysis/Calculus/LagrangeMultipliers.lean index faa6e1df7770b..64e2efb39c875 100644 --- a/Mathlib/Analysis/Calculus/LagrangeMultipliers.lean +++ b/Mathlib/Analysis/Calculus/LagrangeMultipliers.lean @@ -106,7 +106,7 @@ theorem IsLocalExtrOn.exists_multipliers_of_hasStrictFDerivAt {ι : Type*} [Fint ∃ (Λ : ι → ℝ) (Λ₀ : ℝ), (Λ, Λ₀) ≠ 0 ∧ (∑ i, Λ i • f' i) + Λ₀ • φ' = 0 := by letI := Classical.decEq ι replace hextr : IsLocalExtrOn φ {x | (fun i => f i x) = fun i => f i x₀} x₀ := by - simpa only [Function.funext_iff] using hextr + simpa only [funext_iff] using hextr rcases hextr.exists_linear_map_of_hasStrictFDerivAt (hasStrictFDerivAt_pi.2 fun i => hf' i) hφ' with ⟨Λ, Λ₀, h0, hsum⟩ @@ -132,5 +132,5 @@ theorem IsLocalExtrOn.linear_dependent_of_hasStrictFDerivAt {ι : Type*} [Finite rcases hextr.exists_multipliers_of_hasStrictFDerivAt hf' hφ' with ⟨Λ, Λ₀, hΛ, hΛf⟩ refine ⟨Option.elim' Λ₀ Λ, ?_, ?_⟩ · simpa [add_comm] using hΛf - · simpa only [Function.funext_iff, not_and_or, or_comm, Option.exists, Prod.mk_eq_zero, Ne, + · simpa only [funext_iff, not_and_or, or_comm, Option.exists, Prod.mk_eq_zero, Ne, not_forall] using hΛ diff --git a/Mathlib/Analysis/InnerProductSpace/OfNorm.lean b/Mathlib/Analysis/InnerProductSpace/OfNorm.lean index e2e23c0b46a9d..b62522a0e45d6 100644 --- a/Mathlib/Analysis/InnerProductSpace/OfNorm.lean +++ b/Mathlib/Analysis/InnerProductSpace/OfNorm.lean @@ -194,7 +194,7 @@ private theorem rat_prop (r : ℚ) : innerProp' E (r : 𝕜) := by private theorem real_prop (r : ℝ) : innerProp' E (r : 𝕜) := by intro x y revert r - rw [← Function.funext_iff] + rw [← funext_iff] refine Rat.isDenseEmbedding_coe_real.dense.equalizer ?_ ?_ (funext fun X => ?_) · exact (continuous_ofReal.smul continuous_const).inner_ continuous_const · exact (continuous_conj.comp continuous_ofReal).mul continuous_const diff --git a/Mathlib/Analysis/Normed/Operator/WeakOperatorTopology.lean b/Mathlib/Analysis/Normed/Operator/WeakOperatorTopology.lean index 45dfa1892cbcc..202618cf94cd6 100644 --- a/Mathlib/Analysis/Normed/Operator/WeakOperatorTopology.lean +++ b/Mathlib/Analysis/Normed/Operator/WeakOperatorTopology.lean @@ -175,7 +175,7 @@ lemma continuous_of_dual_apply_continuous {α : Type*} [TopologicalSpace α] {g lemma embedding_inducingFn : Embedding (inducingFn 𝕜 E F) := by refine Function.Injective.embedding_induced fun A B hAB => ?_ rw [ContinuousLinearMapWOT.ext_dual_iff] - simpa [Function.funext_iff] using hAB + simpa [funext_iff] using hAB open Filter in /-- The defining property of the weak operator topology: a function `f` tends to diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean b/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean index b7b5fa601494d..0086e643a19b8 100644 --- a/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean +++ b/Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean @@ -597,7 +597,7 @@ theorem continuousAt_arg_coe_angle (h : x ≠ 0) : ContinuousAt ((↑) ∘ arg : by_cases hs : x ∈ slitPlane · exact Real.Angle.continuous_coe.continuousAt.comp (continuousAt_arg hs) · rw [← Function.comp_id (((↑) : ℝ → Real.Angle) ∘ arg), - (Function.funext_iff.2 fun _ => (neg_neg _).symm : (id : ℂ → ℂ) = Neg.neg ∘ Neg.neg), ← + (funext_iff.2 fun _ => (neg_neg _).symm : (id : ℂ → ℂ) = Neg.neg ∘ Neg.neg), ← Function.comp_assoc] refine ContinuousAt.comp ?_ continuous_neg.continuousAt suffices ContinuousAt (Function.update (((↑) ∘ arg) ∘ Neg.neg : ℂ → Real.Angle) 0 π) (-x) by diff --git a/Mathlib/CategoryTheory/GradedObject.lean b/Mathlib/CategoryTheory/GradedObject.lean index c3fd1e2c4e0aa..b5344653826c9 100644 --- a/Mathlib/CategoryTheory/GradedObject.lean +++ b/Mathlib/CategoryTheory/GradedObject.lean @@ -158,7 +158,7 @@ abbrev comap {I J : Type*} (h : J → I) : GradedObject I C ⥤ GradedObject J C -- Porting note: added to ease the port, this is a special case of `Functor.eqToHom_proj` @[simp] theorem eqToHom_proj {I : Type*} {x x' : GradedObject I C} (h : x = x') (i : I) : - (eqToHom h : x ⟶ x') i = eqToHom (Function.funext_iff.mp h i) := by + (eqToHom h : x ⟶ x') i = eqToHom (funext_iff.mp h i) := by subst h rfl diff --git a/Mathlib/CategoryTheory/Pi/Basic.lean b/Mathlib/CategoryTheory/Pi/Basic.lean index beeb60fcf3da4..8515247f7d5ba 100644 --- a/Mathlib/CategoryTheory/Pi/Basic.lean +++ b/Mathlib/CategoryTheory/Pi/Basic.lean @@ -206,7 +206,7 @@ section EqToHom @[simp] theorem eqToHom_proj {x x' : ∀ i, C i} (h : x = x') (i : I) : - (eqToHom h : x ⟶ x') i = eqToHom (Function.funext_iff.mp h i) := by + (eqToHom h : x ⟶ x') i = eqToHom (funext_iff.mp h i) := by subst h rfl diff --git a/Mathlib/CategoryTheory/Sites/LocallySurjective.lean b/Mathlib/CategoryTheory/Sites/LocallySurjective.lean index 06a7da7304b54..289d2db4e05a6 100644 --- a/Mathlib/CategoryTheory/Sites/LocallySurjective.lean +++ b/Mathlib/CategoryTheory/Sites/LocallySurjective.lean @@ -93,7 +93,7 @@ instance {F G : Cᵒᵖ ⥤ A} (f : F ⟶ G) [IsLocallySurjective J f] : theorem isLocallySurjective_iff_imagePresheaf_sheafify_eq_top {F G : Cᵒᵖ ⥤ A} (f : F ⟶ G) : IsLocallySurjective J f ↔ (imagePresheaf (whiskerRight f (forget A))).sheafify J = ⊤ := by - simp only [Subpresheaf.ext_iff, Function.funext_iff, Set.ext_iff, top_subpresheaf_obj, + simp only [Subpresheaf.ext_iff, funext_iff, Set.ext_iff, top_subpresheaf_obj, Set.top_eq_univ, Set.mem_univ, iff_true] exact ⟨fun H _ => H.imageSieve_mem, fun H => ⟨H _⟩⟩ diff --git a/Mathlib/CategoryTheory/Sites/Types.lean b/Mathlib/CategoryTheory/Sites/Types.lean index b1ba30f51c8e2..ecbb98c1d2d6f 100644 --- a/Mathlib/CategoryTheory/Sites/Types.lean +++ b/Mathlib/CategoryTheory/Sites/Types.lean @@ -172,6 +172,6 @@ theorem typesGrothendieckTopology_eq_canonical : have : (fun _ => ULift.up true) = fun _ => ULift.up false := (hs PUnit fun _ => x).isSeparatedFor.ext fun β f hf => funext fun y => hsx.elim <| S.2 hf fun _ => y - simp [Function.funext_iff] at this + simp [funext_iff] at this end CategoryTheory diff --git a/Mathlib/CategoryTheory/Types.lean b/Mathlib/CategoryTheory/Types.lean index a084aa296a6af..01484dc45c6dc 100644 --- a/Mathlib/CategoryTheory/Types.lean +++ b/Mathlib/CategoryTheory/Types.lean @@ -117,7 +117,7 @@ lemma sections_property {F : J ⥤ Type w} (s : (F.sections : Type _)) s.property f lemma sections_ext_iff {F : J ⥤ Type w} {x y : F.sections} : x = y ↔ ∀ j, x.val j = y.val j := - Subtype.ext_iff.trans Function.funext_iff + Subtype.ext_iff.trans funext_iff variable (J) diff --git a/Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean b/Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean index 076f7c450bcde..14728c20ba579 100644 --- a/Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean +++ b/Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean @@ -102,7 +102,7 @@ quadrant. -/ def sphere (n d k : ℕ) : Finset (Fin n → ℕ) := (box n d).filter fun x => ∑ i, x i ^ 2 = k -theorem sphere_zero_subset : sphere n d 0 ⊆ 0 := fun x => by simp [sphere, Function.funext_iff] +theorem sphere_zero_subset : sphere n d 0 ⊆ 0 := fun x => by simp [sphere, funext_iff] @[simp] theorem sphere_zero_right (n k : ℕ) : sphere (n + 1) 0 k = ∅ := by simp [sphere] diff --git a/Mathlib/Combinatorics/HalesJewett.lean b/Mathlib/Combinatorics/HalesJewett.lean index 04d6ee1658e63..76bb5d7812114 100644 --- a/Mathlib/Combinatorics/HalesJewett.lean +++ b/Mathlib/Combinatorics/HalesJewett.lean @@ -138,7 +138,7 @@ variable {η' α' ι' : Type*} def reindex (l : Subspace η α ι) (eη : η ≃ η') (eα : α ≃ α') (eι : ι ≃ ι') : Subspace η' α' ι' where idxFun i := (l.idxFun <| eι.symm i).map eα eη proper e := (eι.exists_congr fun i ↦ by cases h : idxFun l i <;> - simp [*, Function.funext_iff, Equiv.eq_symm_apply]).1 <| l.proper <| eη.symm e + simp [*, funext_iff, Equiv.eq_symm_apply]).1 <| l.proper <| eη.symm e @[simp] lemma reindex_apply (l : Subspace η α ι) (eη : η ≃ η') (eα : α ≃ α') (eι : ι ≃ ι') (x i) : l.reindex eη eα eι x i = eα (l (eα.symm ∘ x ∘ eη) <| eι.symm i) := by diff --git a/Mathlib/Combinatorics/Hall/Basic.lean b/Mathlib/Combinatorics/Hall/Basic.lean index 70a89a8ee9790..0d0b9a82657a9 100644 --- a/Mathlib/Combinatorics/Hall/Basic.lean +++ b/Mathlib/Combinatorics/Hall/Basic.lean @@ -100,7 +100,7 @@ instance hallMatchingsOn.finite {ι : Type u} {α : Type v} (t : ι → Finset apply Finite.of_injective g intro f f' h ext a - rw [Function.funext_iff] at h + rw [funext_iff] at h simpa [g] using h a /-- This is the version of **Hall's Marriage Theorem** in terms of indexed diff --git a/Mathlib/Combinatorics/SimpleGraph/Basic.lean b/Mathlib/Combinatorics/SimpleGraph/Basic.lean index 008ba18f37ef6..69de374b0e114 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Basic.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Basic.lean @@ -355,7 +355,7 @@ instance [Subsingleton V] : Unique (SimpleGraph V) where uniq G := by ext a b; have := Subsingleton.elim a b; simp [this] instance [Nontrivial V] : Nontrivial (SimpleGraph V) := - ⟨⟨⊥, ⊤, fun h ↦ not_subsingleton V ⟨by simpa only [← adj_inj, Function.funext_iff, bot_adj, + ⟨⟨⊥, ⊤, fun h ↦ not_subsingleton V ⟨by simpa only [← adj_inj, funext_iff, bot_adj, top_adj, ne_eq, eq_iff_iff, false_iff, not_not] using h⟩⟩⟩ section Decidable diff --git a/Mathlib/Combinatorics/SimpleGraph/Circulant.lean b/Mathlib/Combinatorics/SimpleGraph/Circulant.lean index 121f720ec7a12..99106b3256d7b 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Circulant.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Circulant.lean @@ -72,11 +72,11 @@ theorem cycleGraph_zero_eq_top : cycleGraph 0 = ⊤ := Subsingleton.elim _ _ theorem cycleGraph_one_eq_top : cycleGraph 1 = ⊤ := Subsingleton.elim _ _ theorem cycleGraph_two_eq_top : cycleGraph 2 = ⊤ := by - simp only [SimpleGraph.ext_iff, Function.funext_iff] + simp only [SimpleGraph.ext_iff, funext_iff] decide theorem cycleGraph_three_eq_top : cycleGraph 3 = ⊤ := by - simp only [SimpleGraph.ext_iff, Function.funext_iff] + simp only [SimpleGraph.ext_iff, funext_iff] decide theorem cycleGraph_one_adj {u v : Fin 1} : ¬(cycleGraph 1).Adj u v := by diff --git a/Mathlib/Combinatorics/SimpleGraph/Turan.lean b/Mathlib/Combinatorics/SimpleGraph/Turan.lean index 45760dc0bd670..08ab8e530a2c0 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Turan.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Turan.lean @@ -72,7 +72,7 @@ lemma turanGraph_zero : turanGraph n 0 = ⊤ := by @[simp] theorem turanGraph_eq_top : turanGraph n r = ⊤ ↔ r = 0 ∨ n ≤ r := by - simp_rw [SimpleGraph.ext_iff, Function.funext_iff, turanGraph, top_adj, eq_iff_iff, not_iff_not] + simp_rw [SimpleGraph.ext_iff, funext_iff, turanGraph, top_adj, eq_iff_iff, not_iff_not] refine ⟨fun h ↦ ?_, ?_⟩ · contrapose! h use ⟨0, (Nat.pos_of_ne_zero h.1).trans h.2⟩, ⟨r, h.2⟩ diff --git a/Mathlib/Computability/TMToPartrec.lean b/Mathlib/Computability/TMToPartrec.lean index a19ae0a5453fd..440884be0810c 100644 --- a/Mathlib/Computability/TMToPartrec.lean +++ b/Mathlib/Computability/TMToPartrec.lean @@ -883,7 +883,7 @@ instance Λ'.instInhabited : Inhabited Λ' := instance Λ'.instDecidableEq : DecidableEq Λ' := fun a b => by induction a generalizing b <;> cases b <;> first | apply Decidable.isFalse; rintro ⟨⟨⟩⟩; done - | exact decidable_of_iff' _ (by simp [Function.funext_iff]; rfl) + | exact decidable_of_iff' _ (by simp [funext_iff]; rfl) /-- The type of TM2 statements used by this machine. -/ def Stmt' := diff --git a/Mathlib/Data/Fin/Basic.lean b/Mathlib/Data/Fin/Basic.lean index 7b7b730d2913b..715342aa56963 100644 --- a/Mathlib/Data/Fin/Basic.lean +++ b/Mathlib/Data/Fin/Basic.lean @@ -171,7 +171,7 @@ then they coincide (in the heq sense). -/ protected theorem heq_fun_iff {α : Sort*} {k l : ℕ} (h : k = l) {f : Fin k → α} {g : Fin l → α} : HEq f g ↔ ∀ i : Fin k, f i = g ⟨(i : ℕ), h ▸ i.2⟩ := by subst h - simp [Function.funext_iff] + simp [funext_iff] /-- Assume `k = l` and `k' = l'`. If two functions `Fin k → Fin k' → α` and `Fin l → Fin l' → α` are equal on each pair, @@ -181,7 +181,7 @@ protected theorem heq_fun₂_iff {α : Sort*} {k l k' l' : ℕ} (h : k = l) (h' HEq f g ↔ ∀ (i : Fin k) (j : Fin k'), f i j = g ⟨(i : ℕ), h ▸ i.2⟩ ⟨(j : ℕ), h' ▸ j.2⟩ := by subst h subst h' - simp [Function.funext_iff] + simp [funext_iff] /-- Two elements of `Fin k` and `Fin l` are heq iff their values in `ℕ` coincide. This requires `k = l`. For the left implication without this assumption, see `val_eq_val_of_heq`. -/ diff --git a/Mathlib/Data/Finset/NAry.lean b/Mathlib/Data/Finset/NAry.lean index 97c9c4284cbd7..db73633e28a15 100644 --- a/Mathlib/Data/Finset/NAry.lean +++ b/Mathlib/Data/Finset/NAry.lean @@ -582,7 +582,7 @@ variable {ι : Type*} {α β γ : ι → Type*} [DecidableEq ι] [Fintype ι] [ lemma piFinset_image₂ (f : ∀ i, α i → β i → γ i) (s : ∀ i, Finset (α i)) (t : ∀ i, Finset (β i)) : piFinset (fun i ↦ image₂ (f i) (s i) (t i)) = image₂ (fun a b i ↦ f _ (a i) (b i)) (piFinset s) (piFinset t) := by - ext; simp only [mem_piFinset, mem_image₂, Classical.skolem, forall_and, Function.funext_iff] + ext; simp only [mem_piFinset, mem_image₂, Classical.skolem, forall_and, funext_iff] end Fintype diff --git a/Mathlib/Data/Finset/Sort.lean b/Mathlib/Data/Finset/Sort.lean index 361e4f3721a7f..923e35810f214 100644 --- a/Mathlib/Data/Finset/Sort.lean +++ b/Mathlib/Data/Finset/Sort.lean @@ -219,7 +219,7 @@ theorem orderEmbOfFin_unique {s : Finset α} {k : ℕ} (h : s.card = k) {f : Fin the increasing bijection `orderEmbOfFin s h`. -/ theorem orderEmbOfFin_unique' {s : Finset α} {k : ℕ} (h : s.card = k) {f : Fin k ↪o α} (hfs : ∀ x, f x ∈ s) : f = s.orderEmbOfFin h := - RelEmbedding.ext <| Function.funext_iff.1 <| orderEmbOfFin_unique h hfs f.strictMono + RelEmbedding.ext <| funext_iff.1 <| orderEmbOfFin_unique h hfs f.strictMono /-- Two parametrizations `orderEmbOfFin` of the same set take the same value on `i` and `j` if and only if `i = j`. Since they can be defined on a priori not defeq types `Fin k` and `Fin l` diff --git a/Mathlib/Data/Fintype/Basic.lean b/Mathlib/Data/Fintype/Basic.lean index 0ff3b973f0141..997a6dd16aeb4 100644 --- a/Mathlib/Data/Fintype/Basic.lean +++ b/Mathlib/Data/Fintype/Basic.lean @@ -376,7 +376,7 @@ namespace Fintype instance decidablePiFintype {α} {β : α → Type*} [∀ a, DecidableEq (β a)] [Fintype α] : DecidableEq (∀ a, β a) := fun f g => decidable_of_iff (∀ a ∈ @Fintype.elems α _, f a = g a) - (by simp [Function.funext_iff, Fintype.complete]) + (by simp [funext_iff, Fintype.complete]) instance decidableForallFintype {p : α → Prop} [DecidablePred p] [Fintype α] : Decidable (∀ a, p a) := diff --git a/Mathlib/Data/Fintype/Pi.lean b/Mathlib/Data/Fintype/Pi.lean index 99a88bda7004a..c32f9bbfd62b6 100644 --- a/Mathlib/Data/Fintype/Pi.lean +++ b/Mathlib/Data/Fintype/Pi.lean @@ -25,7 +25,7 @@ analogue of `Finset.pi` where the base finset is `univ` (but formally they are n there is an additional condition `i ∈ Finset.univ` in the `Finset.pi` definition). -/ def piFinset (t : ∀ a, Finset (δ a)) : Finset (∀ a, δ a) := (Finset.univ.pi t).map ⟨fun f a => f a (mem_univ a), fun _ _ => - by simp (config := {contextual := true}) [Function.funext_iff]⟩ + by simp (config := {contextual := true}) [funext_iff]⟩ @[simp] theorem mem_piFinset {t : ∀ a, Finset (δ a)} {f : ∀ a, δ a} : f ∈ piFinset t ↔ ∀ a, f a ∈ t a := by @@ -69,7 +69,7 @@ lemma piFinset_of_isEmpty [IsEmpty α] (s : ∀ a, Finset (γ a)) : piFinset s = @[simp] theorem piFinset_singleton (f : ∀ i, δ i) : piFinset (fun i => {f i} : ∀ i, Finset (δ i)) = {f} := - ext fun _ => by simp only [Function.funext_iff, Fintype.mem_piFinset, mem_singleton] + ext fun _ => by simp only [funext_iff, Fintype.mem_piFinset, mem_singleton] theorem piFinset_subsingleton {f : ∀ i, Finset (δ i)} (hf : ∀ i, (f i : Set (δ i)).Subsingleton) : (Fintype.piFinset f : Set (∀ i, δ i)).Subsingleton := fun _ ha _ hb => @@ -83,7 +83,7 @@ theorem piFinset_disjoint_of_disjoint (t₁ t₂ : ∀ a, Finset (δ a)) {a : α lemma piFinset_image [∀ a, DecidableEq (δ a)] (f : ∀ a, γ a → δ a) (s : ∀ a, Finset (γ a)) : piFinset (fun a ↦ (s a).image (f a)) = (piFinset s).image fun b a ↦ f _ (b a) := by - ext; simp only [mem_piFinset, mem_image, Classical.skolem, forall_and, Function.funext_iff] + ext; simp only [mem_piFinset, mem_image, Classical.skolem, forall_and, funext_iff] lemma eval_image_piFinset_subset (t : ∀ a, Finset (δ a)) (a : α) [DecidableEq (δ a)] : ((piFinset t).image fun f ↦ f a) ⊆ t a := image_subset_iff.2 fun _x hx ↦ mem_piFinset.1 hx _ diff --git a/Mathlib/Data/FunLike/Basic.lean b/Mathlib/Data/FunLike/Basic.lean index 3a04435a85ca6..afcc1b7e13a25 100644 --- a/Mathlib/Data/FunLike/Basic.lean +++ b/Mathlib/Data/FunLike/Basic.lean @@ -194,7 +194,7 @@ theorem ext (f g : F) (h : ∀ x : α, f x = g x) : f = g := DFunLike.coe_injective' (funext h) theorem ext_iff {f g : F} : f = g ↔ ∀ x, f x = g x := - coe_fn_eq.symm.trans Function.funext_iff + coe_fn_eq.symm.trans funext_iff protected theorem congr_fun {f g : F} (h₁ : f = g) (x : α) : f x = g x := congr_fun (congr_arg _ h₁) x diff --git a/Mathlib/Data/Matrix/ColumnRowPartitioned.lean b/Mathlib/Data/Matrix/ColumnRowPartitioned.lean index 1fef44043ba64..67906c2b869f0 100644 --- a/Mathlib/Data/Matrix/ColumnRowPartitioned.lean +++ b/Mathlib/Data/Matrix/ColumnRowPartitioned.lean @@ -108,12 +108,12 @@ lemma fromRows_toRows (A : Matrix (m₁ ⊕ m₂) n R) : fromRows A.toRows₁ A. lemma fromRows_inj : Function.Injective2 (@fromRows R m₁ m₂ n) := by intros x1 x2 y1 y2 - simp only [Function.funext_iff, ← Matrix.ext_iff] + simp only [funext_iff, ← Matrix.ext_iff] aesop lemma fromColumns_inj : Function.Injective2 (@fromColumns R m n₁ n₂) := by intros x1 x2 y1 y2 - simp only [Function.funext_iff, ← Matrix.ext_iff] + simp only [funext_iff, ← Matrix.ext_iff] aesop lemma fromColumns_ext_iff (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (B₁ : Matrix m n₁ R) diff --git a/Mathlib/Data/Multiset/Basic.lean b/Mathlib/Data/Multiset/Basic.lean index 7dc4316f0e993..8f15a338625d1 100644 --- a/Mathlib/Data/Multiset/Basic.lean +++ b/Mathlib/Data/Multiset/Basic.lean @@ -1421,7 +1421,7 @@ instance decidableDforallMultiset {p : ∀ a ∈ m, Prop} [_hp : ∀ (a) (h : a /-- decidable equality for functions whose domain is bounded by multisets -/ instance decidableEqPiMultiset {β : α → Type*} [∀ a, DecidableEq (β a)] : DecidableEq (∀ a ∈ m, β a) := fun f g => - decidable_of_iff (∀ (a) (h : a ∈ m), f a h = g a h) (by simp [Function.funext_iff]) + decidable_of_iff (∀ (a) (h : a ∈ m), f a h = g a h) (by simp [funext_iff]) /-- If `p` is a decidable predicate, so is the existence of an element in a multiset satisfying `p`. -/ diff --git a/Mathlib/Data/Real/GoldenRatio.lean b/Mathlib/Data/Real/GoldenRatio.lean index 42e9c2559ca88..2518fadf3188a 100644 --- a/Mathlib/Data/Real/GoldenRatio.lean +++ b/Mathlib/Data/Real/GoldenRatio.lean @@ -201,7 +201,7 @@ theorem Real.coe_fib_eq' : /-- Binet's formula as a dependent equality. -/ theorem Real.coe_fib_eq : ∀ n, (Nat.fib n : ℝ) = (φ ^ n - ψ ^ n) / √5 := by - rw [← Function.funext_iff, Real.coe_fib_eq'] + rw [← funext_iff, Real.coe_fib_eq'] /-- Relationship between the Fibonacci Sequence, Golden Ratio and its conjugate's exponents --/ theorem fib_golden_conj_exp (n : ℕ) : Nat.fib (n + 1) - φ * Nat.fib n = ψ ^ n := by diff --git a/Mathlib/Data/Set/Image.lean b/Mathlib/Data/Set/Image.lean index b0d95b24f9381..071d9c15c3f6c 100644 --- a/Mathlib/Data/Set/Image.lean +++ b/Mathlib/Data/Set/Image.lean @@ -634,7 +634,7 @@ theorem range_subset_iff : range f ⊆ s ↔ ∀ y, f y ∈ s := theorem range_subset_range_iff_exists_comp {f : α → γ} {g : β → γ} : range f ⊆ range g ↔ ∃ h : α → β, f = g ∘ h := by - simp only [range_subset_iff, mem_range, Classical.skolem, Function.funext_iff, (· ∘ ·), eq_comm] + simp only [range_subset_iff, mem_range, Classical.skolem, funext_iff, (· ∘ ·), eq_comm] theorem range_eq_iff (f : α → β) (s : Set β) : range f = s ↔ (∀ a, f a ∈ s) ∧ ∀ b ∈ s, ∃ a, f a = b := by diff --git a/Mathlib/Data/W/Basic.lean b/Mathlib/Data/W/Basic.lean index a2b73e07e8871..7c1f339cc49d0 100644 --- a/Mathlib/Data/W/Basic.lean +++ b/Mathlib/Data/W/Basic.lean @@ -103,7 +103,7 @@ theorem infinite_of_nonempty_of_isEmpty (a b : α) [ha : Nonempty (β a)] [he : · cases' m with m · simp_all · refine congr_arg Nat.succ (ih ?_) - simp_all [Function.funext_iff]⟩ + simp_all [funext_iff]⟩ variable [∀ a : α, Fintype (β a)] diff --git a/Mathlib/FieldTheory/Finite/Polynomial.lean b/Mathlib/FieldTheory/Finite/Polynomial.lean index a5a76e1726feb..36dd816621f74 100644 --- a/Mathlib/FieldTheory/Finite/Polynomial.lean +++ b/Mathlib/FieldTheory/Finite/Polynomial.lean @@ -99,7 +99,7 @@ end CommRing variable [Field K] theorem eval_indicator_apply_eq_zero (a b : σ → K) (h : a ≠ b) : eval a (indicator b) = 0 := by - obtain ⟨i, hi⟩ : ∃ i, a i ≠ b i := by rwa [Ne, Function.funext_iff, not_forall] at h + obtain ⟨i, hi⟩ : ∃ i, a i ≠ b i := by rwa [Ne, funext_iff, not_forall] at h simp only [indicator, map_prod, map_sub, map_one, map_pow, eval_X, eval_C, sub_self, Finset.prod_eq_zero_iff] refine ⟨i, Finset.mem_univ _, ?_⟩ diff --git a/Mathlib/GroupTheory/CommutingProbability.lean b/Mathlib/GroupTheory/CommutingProbability.lean index 3f168c3c28305..df8f7702b7fdd 100644 --- a/Mathlib/GroupTheory/CommutingProbability.lean +++ b/Mathlib/GroupTheory/CommutingProbability.lean @@ -47,7 +47,7 @@ theorem commProb_prod (M' : Type*) [Mul M'] : commProb (M × M') = commProb M * theorem commProb_pi {α : Type*} (i : α → Type*) [Fintype α] [∀ a, Mul (i a)] : commProb (∀ a, i a) = ∏ a, commProb (i a) := by simp_rw [commProb_def, Finset.prod_div_distrib, Finset.prod_pow, ← Nat.cast_prod, - ← Nat.card_pi, Commute, SemiconjBy, Function.funext_iff] + ← Nat.card_pi, Commute, SemiconjBy, funext_iff] congr 2 exact Nat.card_congr ⟨fun x a => ⟨⟨x.1.1 a, x.1.2 a⟩, x.2 a⟩, fun x => ⟨⟨fun a => (x a).1.1, fun a => (x a).1.2⟩, fun a => (x a).2⟩, fun x => rfl, fun x => rfl⟩ diff --git a/Mathlib/GroupTheory/FreeGroup/IsFreeGroup.lean b/Mathlib/GroupTheory/FreeGroup/IsFreeGroup.lean index 5999f4a20b721..e3a6f25954b2b 100644 --- a/Mathlib/GroupTheory/FreeGroup/IsFreeGroup.lean +++ b/Mathlib/GroupTheory/FreeGroup/IsFreeGroup.lean @@ -214,7 +214,7 @@ group extends in a unique way to a homomorphism from `G`. Note that since `IsFreeGroup.lift` is expressed as a bijection, it already expresses the universal property. -/ theorem unique_lift (f : Generators G → H) : ∃! F : G →* H, ∀ a, F (of a) = f a := by - simpa only [Function.funext_iff] using lift.symm.bijective.existsUnique f + simpa only [funext_iff] using lift.symm.bijective.existsUnique f /-- If a group satisfies the universal property of a free group with respect to a given type, then it is free. Here, the universal property is expressed as in `IsFreeGroup.lift` and its diff --git a/Mathlib/GroupTheory/GroupAction/FixedPoints.lean b/Mathlib/GroupTheory/GroupAction/FixedPoints.lean index 070b3e8dd30e2..a8a5bc7b71b55 100644 --- a/Mathlib/GroupTheory/GroupAction/FixedPoints.lean +++ b/Mathlib/GroupTheory/GroupAction/FixedPoints.lean @@ -237,7 +237,7 @@ then `fixedBy α m = Set.univ` implies that `m = 1`. -/ then `fixedBy α m = Set.univ` implies that `m = 1`."] theorem fixedBy_eq_univ_iff_eq_one {m : M} : fixedBy α m = Set.univ ↔ m = 1 := by rw [← (smul_left_injective' (M := M) (α := α)).eq_iff, Set.eq_univ_iff_forall] - simp_rw [Function.funext_iff, one_smul, mem_fixedBy] + simp_rw [funext_iff, one_smul, mem_fixedBy] /-- If the image of the `(fixedBy α g)ᶜ` set by the pointwise action of `h: G` diff --git a/Mathlib/GroupTheory/HNNExtension.lean b/Mathlib/GroupTheory/HNNExtension.lean index 551403b5170c4..a4d0b7d277511 100644 --- a/Mathlib/GroupTheory/HNNExtension.lean +++ b/Mathlib/GroupTheory/HNNExtension.lean @@ -595,7 +595,7 @@ theorem of_injective : Function.Injective (of : G → HNNExtension G A B φ) := (f := ((· • ·) : HNNExtension G A B φ → NormalWord d → NormalWord d)) ?_ intros _ _ h exact eq_of_smul_eq_smul (fun w : NormalWord d => - by simp_all [Function.funext_iff, of_smul_eq_smul]) + by simp_all [funext_iff, of_smul_eq_smul]) namespace ReducedWord diff --git a/Mathlib/GroupTheory/Perm/DomMulAct.lean b/Mathlib/GroupTheory/Perm/DomMulAct.lean index 5d730372bcddf..4db961f223713 100644 --- a/Mathlib/GroupTheory/Perm/DomMulAct.lean +++ b/Mathlib/GroupTheory/Perm/DomMulAct.lean @@ -139,7 +139,7 @@ theorem stabilizer_card': rw [refl_apply, ← Subtype.coe_inj] simp only [φ, Set.val_codRestrict_apply] · intro g - simp only [Function.funext_iff] + simp only [funext_iff] apply forall_congr' intro a simp only [Function.comp_apply, φ, ← Subtype.coe_inj, Set.val_codRestrict_apply] diff --git a/Mathlib/GroupTheory/PushoutI.lean b/Mathlib/GroupTheory/PushoutI.lean index 47fa6da660134..0f672f3da1e25 100644 --- a/Mathlib/GroupTheory/PushoutI.lean +++ b/Mathlib/GroupTheory/PushoutI.lean @@ -152,7 +152,7 @@ def homEquiv : invFun := fun f => lift f.1.1 f.1.2 f.2, left_inv := fun _ => hom_ext (by simp [DFunLike.ext_iff]) (by simp [DFunLike.ext_iff]) - right_inv := fun ⟨⟨_, _⟩, _⟩ => by simp [DFunLike.ext_iff, Function.funext_iff] } + right_inv := fun ⟨⟨_, _⟩, _⟩ => by simp [DFunLike.ext_iff, funext_iff] } /-- The map from the coproduct into the pushout -/ def ofCoprodI : CoprodI G →* PushoutI φ := @@ -596,7 +596,7 @@ theorem of_injective (hφ : ∀ i, Function.Injective (φ i)) (i : ι) : (f := ((· • ·) : PushoutI φ → NormalWord d → NormalWord d)) ?_ intros _ _ h exact eq_of_smul_eq_smul (fun w : NormalWord d => - by simp_all [Function.funext_iff, of_smul_eq_smul]) + by simp_all [funext_iff, of_smul_eq_smul]) theorem base_injective (hφ : ∀ i, Function.Injective (φ i)) : Function.Injective (base φ) := by @@ -607,7 +607,7 @@ theorem base_injective (hφ : ∀ i, Function.Injective (φ i)) : (f := ((· • ·) : PushoutI φ → NormalWord d → NormalWord d)) ?_ intros _ _ h exact eq_of_smul_eq_smul (fun w : NormalWord d => - by simp_all [Function.funext_iff, base_smul_eq_smul]) + by simp_all [funext_iff, base_smul_eq_smul]) section Reduced diff --git a/Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean b/Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean index ef82d9e40a82c..edeab9e15af30 100644 --- a/Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean +++ b/Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean @@ -703,7 +703,7 @@ theorem pi_comp (g : P3 →ᵃ[k] P1) : (pi fp).comp g = pi (fun i => (fp i).com rfl theorem pi_eq_zero : pi fv = 0 ↔ ∀ i, fv i = 0 := by - simp only [AffineMap.ext_iff, Function.funext_iff, pi_apply] + simp only [AffineMap.ext_iff, funext_iff, pi_apply] exact forall_comm theorem pi_zero : pi (fun _ ↦ 0 : (i : ι) → P1 →ᵃ[k] φv i) = 0 := by diff --git a/Mathlib/LinearAlgebra/AffineSpace/Independent.lean b/Mathlib/LinearAlgebra/AffineSpace/Independent.lean index 24d2fdd76c35b..0fe67bc39f3f9 100644 --- a/Mathlib/LinearAlgebra/AffineSpace/Independent.lean +++ b/Mathlib/LinearAlgebra/AffineSpace/Independent.lean @@ -908,7 +908,7 @@ theorem centroid_eq_iff [CharZero k] {n : ℕ} (s : Simplex k P n) {fs₁ fs₂ (affineIndependent_iff_indicator_eq_of_affineCombination_eq k s.points).1 s.independent _ _ _ _ (fs₁.sum_centroidWeightsIndicator_eq_one_of_card_eq_add_one k h₁) (fs₂.sum_centroidWeightsIndicator_eq_one_of_card_eq_add_one k h₂) h - simp_rw [Finset.coe_univ, Set.indicator_univ, Function.funext_iff, + simp_rw [Finset.coe_univ, Set.indicator_univ, funext_iff, Finset.centroidWeightsIndicator_def, Finset.centroidWeights, h₁, h₂] at ha ext i specialize ha i diff --git a/Mathlib/LinearAlgebra/Dual.lean b/Mathlib/LinearAlgebra/Dual.lean index 5d556906e958a..0dfa5a4d643f0 100644 --- a/Mathlib/LinearAlgebra/Dual.lean +++ b/Mathlib/LinearAlgebra/Dual.lean @@ -1228,7 +1228,7 @@ instance (W : Submodule R M) : FunLike (W.dualAnnihilator) M R where coe φ := φ.val coe_injective' φ ψ h := by ext - simp only [Function.funext_iff] at h + simp only [funext_iff] at h exact h _ @[simp] diff --git a/Mathlib/LinearAlgebra/Matrix/DotProduct.lean b/Mathlib/LinearAlgebra/Matrix/DotProduct.lean index 3a313af6368d5..bb06aeea3eee8 100644 --- a/Mathlib/LinearAlgebra/Matrix/DotProduct.lean +++ b/Mathlib/LinearAlgebra/Matrix/DotProduct.lean @@ -88,7 +88,7 @@ variable [Fintype m] [Fintype n] [Fintype p] @[simp] theorem dotProduct_self_eq_zero [LinearOrderedRing R] {v : n → R} : dotProduct v v = 0 ↔ v = 0 := (Finset.sum_eq_zero_iff_of_nonneg fun i _ => mul_self_nonneg (v i)).trans <| by - simp [Function.funext_iff] + simp [funext_iff] section StarOrderedRing @@ -110,13 +110,13 @@ variable [NoZeroDivisors R] @[simp] theorem dotProduct_star_self_eq_zero {v : n → R} : dotProduct (star v) v = 0 ↔ v = 0 := (Fintype.sum_eq_zero_iff_of_nonneg fun _ => star_mul_self_nonneg _).trans <| - by simp [Function.funext_iff, mul_eq_zero] + by simp [funext_iff, mul_eq_zero] /-- Note that this applies to `ℂ` via `RCLike.toStarOrderedRing`. -/ @[simp] theorem dotProduct_self_star_eq_zero {v : n → R} : dotProduct v (star v) = 0 ↔ v = 0 := (Fintype.sum_eq_zero_iff_of_nonneg fun _ => mul_star_self_nonneg _).trans <| - by simp [Function.funext_iff, mul_eq_zero] + by simp [funext_iff, mul_eq_zero] @[simp] lemma conjTranspose_mul_self_eq_zero {n} {A : Matrix m n R} : Aᴴ * A = 0 ↔ A = 0 := diff --git a/Mathlib/LinearAlgebra/Pi.lean b/Mathlib/LinearAlgebra/Pi.lean index 89740b2d0a89e..079b058aab3d1 100644 --- a/Mathlib/LinearAlgebra/Pi.lean +++ b/Mathlib/LinearAlgebra/Pi.lean @@ -462,8 +462,8 @@ def piOptionEquivProd {ι : Type*} {M : Option ι → Type*} [(i : Option ι) [(i : Option ι) → Module R (M i)] : ((i : Option ι) → M i) ≃ₗ[R] M none × ((i : ι) → M (some i)) := { Equiv.piOptionEquivProd with - map_add' := by simp [Function.funext_iff] - map_smul' := by simp [Function.funext_iff] } + map_add' := by simp [funext_iff] + map_smul' := by simp [funext_iff] } variable (ι M) (S : Type*) [Fintype ι] [DecidableEq ι] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] [SMulCommClass R S M] diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Prod.lean b/Mathlib/LinearAlgebra/QuadraticForm/Prod.lean index 891097a9ae0b6..20c4468b0c051 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Prod.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Prod.lean @@ -303,7 +303,7 @@ theorem Equivalent.pi [Fintype ι] {Q : ∀ i, QuadraticMap R (Mᵢ i) P} /-- If a family is anisotropic then its components must be. The converse is not true. -/ theorem anisotropic_of_pi [Fintype ι] {Q : ∀ i, QuadraticMap R (Mᵢ i) P} (h : (pi Q).Anisotropic) : ∀ i, (Q i).Anisotropic := by - simp_rw [Anisotropic, pi_apply, Function.funext_iff, Pi.zero_apply] at h + simp_rw [Anisotropic, pi_apply, funext_iff, Pi.zero_apply] at h intro i x hx classical have := h (Pi.single i x) ?_ i diff --git a/Mathlib/Logic/Function/Basic.lean b/Mathlib/Logic/Function/Basic.lean index 131ecb1c0731d..a7cb654f6a4e7 100644 --- a/Mathlib/Logic/Function/Basic.lean +++ b/Mathlib/Logic/Function/Basic.lean @@ -893,7 +893,7 @@ lemma forall_existsUnique_iff {r : α → β → Prop} : if and only if it is `(f · = ·)` for some function `f`. -/ lemma forall_existsUnique_iff' {r : α → β → Prop} : (∀ a, ∃! b, r a b) ↔ ∃ f : α → β, r = (f · = ·) := by - simp [forall_existsUnique_iff, Function.funext_iff] + simp [forall_existsUnique_iff, funext_iff] /-- A symmetric relation `r : α → α → Prop` is "function-like" (for each `a` there exists a unique `b` such that `r a b`) diff --git a/Mathlib/MeasureTheory/Measure/VectorMeasure.lean b/Mathlib/MeasureTheory/Measure/VectorMeasure.lean index d6bc3aa0248e0..06d029fc3a63b 100644 --- a/Mathlib/MeasureTheory/Measure/VectorMeasure.lean +++ b/Mathlib/MeasureTheory/Measure/VectorMeasure.lean @@ -96,7 +96,7 @@ theorem coe_injective : @Function.Injective (VectorMeasure α M) (Set α → M) congr theorem ext_iff' (v w : VectorMeasure α M) : v = w ↔ ∀ i : Set α, v i = w i := by - rw [← coe_injective.eq_iff, Function.funext_iff] + rw [← coe_injective.eq_iff, funext_iff] theorem ext_iff (v w : VectorMeasure α M) : v = w ↔ ∀ i : Set α, MeasurableSet i → v i = w i := by constructor diff --git a/Mathlib/ModelTheory/Basic.lean b/Mathlib/ModelTheory/Basic.lean index baa0ada8d4271..6846aee6eb65c 100644 --- a/Mathlib/ModelTheory/Basic.lean +++ b/Mathlib/ModelTheory/Basic.lean @@ -379,7 +379,7 @@ instance funLike : FunLike (M ↪[L] N) M N where cases g congr ext x - exact Function.funext_iff.1 h x + exact funext_iff.1 h x instance embeddingLike : EmbeddingLike (M ↪[L] N) M N where injective' f := f.toEmbedding.injective @@ -416,7 +416,7 @@ theorem coe_injective : @Function.Injective (M ↪[L] N) (M → N) (↑) cases g congr ext x - exact Function.funext_iff.1 h x + exact funext_iff.1 h x @[ext] theorem ext ⦃f g : M ↪[L] N⦄ (h : ∀ x, f x = g x) : f = g := @@ -537,7 +537,7 @@ instance : EquivLike (M ≃[L] N) M N where cases g simp only [mk.injEq] ext x - exact Function.funext_iff.1 h₁ x + exact funext_iff.1 h₁ x instance : StrongHomClass L (M ≃[L] N) M N where map_fun := map_fun' diff --git a/Mathlib/ModelTheory/ElementaryMaps.lean b/Mathlib/ModelTheory/ElementaryMaps.lean index 54428842a22a5..f774228f18d50 100644 --- a/Mathlib/ModelTheory/ElementaryMaps.lean +++ b/Mathlib/ModelTheory/ElementaryMaps.lean @@ -65,7 +65,7 @@ instance instFunLike : FunLike (M ↪ₑ[L] N) M N where cases g simp only [ElementaryEmbedding.mk.injEq] ext x - exact Function.funext_iff.1 h x + exact funext_iff.1 h x instance : CoeFun (M ↪ₑ[L] N) fun _ => M → N := DFunLike.hasCoeToFun diff --git a/Mathlib/ModelTheory/Syntax.lean b/Mathlib/ModelTheory/Syntax.lean index 24c9794e5cfbd..a70ace4f16815 100644 --- a/Mathlib/ModelTheory/Syntax.lean +++ b/Mathlib/ModelTheory/Syntax.lean @@ -85,7 +85,7 @@ instance instDecidableEq [DecidableEq α] [∀ n, DecidableEq (L.Functions n)] : letI : DecidableEq (L.Term α) := instDecidableEq decidable_of_iff (f = h ▸ g ∧ ∀ i : Fin m, xs i = ys (Fin.cast h i)) <| by subst h - simp [Function.funext_iff] + simp [funext_iff] else .isFalse <| by simp [h] | .var _, .func _ _ | .func _ _, .var _ => .isFalse <| by simp diff --git a/Mathlib/NumberTheory/NumberField/House.lean b/Mathlib/NumberTheory/NumberField/House.lean index d56eb4d18c668..18b9930964456 100644 --- a/Mathlib/NumberTheory/NumberField/House.lean +++ b/Mathlib/NumberTheory/NumberField/House.lean @@ -132,7 +132,7 @@ include ha in private theorem asiegel_ne_0 : asiegel K a ≠ 0 := by simp (config := { unfoldPartialApp := true }) only [asiegel, a'] simp only [ne_eq] - rw [Function.funext_iff]; intros hs + rw [funext_iff]; intros hs simp only [Prod.forall] at hs; apply ha rw [← Matrix.ext_iff]; intros k' l @@ -141,7 +141,7 @@ private theorem asiegel_ne_0 : asiegel K a ≠ 0 := by have := ((newBasis K).repr.map_eq_zero_iff (x := (a k' l * (newBasis K) b))).1 <| by ext b' specialize hs b' - rw [Function.funext_iff] at hs + rw [funext_iff] at hs simp only [Prod.forall] at hs apply hs simp only [mul_eq_zero] at this @@ -157,7 +157,7 @@ private theorem ξ_ne_0 : ξ K x ≠ 0 := by intro H apply hxl ext ⟨l, r⟩ - rw [Function.funext_iff] at H + rw [funext_iff] at H have hblin := Basis.linearIndependent (newBasis K) simp only [zsmul_eq_mul, Fintype.linearIndependent_iff] at hblin exact hblin (fun r ↦ x (l,r)) (H _) r @@ -175,9 +175,9 @@ private theorem ξ_mulVec_eq_0 : a *ᵥ ξ K x = 0 := by have lin_0 : ∀ u, ∑ r, ∑ l, (a' K a k l r u * x (l, r) : 𝓞 K) = 0 := by intros u have hξ := ξ_ne_0 K x hxl - rw [Ne, Function.funext_iff, not_forall] at hξ + rw [Ne, funext_iff, not_forall] at hξ rcases hξ with ⟨l, hξ⟩ - rw [Function.funext_iff] at hmulvec0 + rw [funext_iff] at hmulvec0 specialize hmulvec0 ⟨k, u⟩ simp only [Fintype.sum_prod_type, mulVec, dotProduct, asiegel] at hmulvec0 rw [sum_comm] at hmulvec0 diff --git a/Mathlib/Order/RelSeries.lean b/Mathlib/Order/RelSeries.lean index d01a0e54fc8ee..b2c41395b294b 100644 --- a/Mathlib/Order/RelSeries.lean +++ b/Mathlib/Order/RelSeries.lean @@ -704,7 +704,7 @@ def injStrictMono (n : ℕ) : simp_rw [Subtype.mk_eq_mk, Sigma.mk.inj_iff, heq_eq_eq, true_and] have feq := fun i ↦ congr($(e).toFun i) simp_rw [mk_toFun lf f mf, mk_toFun lf g mg, mk_length lf f mf] at feq - rwa [Function.funext_iff] + rwa [funext_iff] /-- For two preorders `α, β`, if `f : α → β` is strictly monotonic, then a strict chain of `α` diff --git a/Mathlib/Probability/ProbabilityMassFunction/Basic.lean b/Mathlib/Probability/ProbabilityMassFunction/Basic.lean index a28a889e12f1a..14593d136558b 100644 --- a/Mathlib/Probability/ProbabilityMassFunction/Basic.lean +++ b/Mathlib/Probability/ProbabilityMassFunction/Basic.lean @@ -165,7 +165,7 @@ theorem toOuterMeasure_inj {p q : PMF α} : p.toOuterMeasure = q.toOuterMeasure theorem toOuterMeasure_apply_eq_zero_iff : p.toOuterMeasure s = 0 ↔ Disjoint p.support s := by rw [toOuterMeasure_apply, ENNReal.tsum_eq_zero] - exact Function.funext_iff.symm.trans Set.indicator_eq_zero' + exact funext_iff.symm.trans Set.indicator_eq_zero' theorem toOuterMeasure_apply_eq_one_iff : p.toOuterMeasure s = 1 ↔ p.support ⊆ s := by refine (p.toOuterMeasure_apply s).symm ▸ ⟨fun h a hap => ?_, fun h => ?_⟩ diff --git a/Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean b/Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean index c2cc073aa0dca..e5fead4c21a6d 100644 --- a/Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean +++ b/Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean @@ -98,7 +98,7 @@ def dZero : A →ₗ[k] G → A where theorem dZero_ker_eq_invariants : LinearMap.ker (dZero A) = invariants A.ρ := by ext x - simp only [LinearMap.mem_ker, mem_invariants, ← @sub_eq_zero _ _ _ x, Function.funext_iff] + simp only [LinearMap.mem_ker, mem_invariants, ← @sub_eq_zero _ _ _ x, funext_iff] rfl @[simp] theorem dZero_eq_zero [A.IsTrivial] : dZero A = 0 := by @@ -226,7 +226,7 @@ variable {A} theorem mem_oneCocycles_def (f : G → A) : f ∈ oneCocycles A ↔ ∀ g h : G, A.ρ g (f h) - f (g * h) + f g = 0 := LinearMap.mem_ker.trans <| by - rw [Function.funext_iff] + rw [funext_iff] simp only [dOne_apply, Pi.zero_apply, Prod.forall] theorem mem_oneCocycles_iff (f : G → A) : @@ -277,7 +277,7 @@ theorem mem_twoCocycles_def (f : G × G → A) : f ∈ twoCocycles A ↔ ∀ g h j : G, A.ρ g (f (h, j)) - f (g * h, j) + f (g, h * j) - f (g, h) = 0 := LinearMap.mem_ker.trans <| by - rw [Function.funext_iff] + rw [funext_iff] simp only [dTwo_apply, Prod.mk.eta, Pi.zero_apply, Prod.forall] theorem mem_twoCocycles_iff (f : G × G → A) : @@ -491,7 +491,7 @@ def twoCoboundariesOfIsTwoCoboundary {f : G × G → A} (hf : IsTwoCoboundary f) theorem isTwoCoboundary_of_twoCoboundaries (f : twoCoboundaries (Rep.ofDistribMulAction k G A)) : IsTwoCoboundary (A := A) f.1.1 := by rcases mem_range_of_mem_twoCoboundaries f.2 with ⟨x, hx⟩ - exact ⟨x, fun g h => Function.funext_iff.1 hx (g, h)⟩ + exact ⟨x, fun g h => funext_iff.1 hx (g, h)⟩ end ofDistribMulAction @@ -616,7 +616,7 @@ theorem isMulTwoCoboundary_of_twoCoboundaries (f : twoCoboundaries (Rep.ofMulDistribMulAction G M)) : IsMulTwoCoboundary (M := M) (Additive.toMul ∘ f.1.1) := by rcases mem_range_of_mem_twoCoboundaries f.2 with ⟨x, hx⟩ - exact ⟨x, fun g h => Function.funext_iff.1 hx (g, h)⟩ + exact ⟨x, fun g h => funext_iff.1 hx (g, h)⟩ end ofMulDistribMulAction diff --git a/Mathlib/RingTheory/HahnSeries/Addition.lean b/Mathlib/RingTheory/HahnSeries/Addition.lean index 61a63a5fceb4a..3daeb21892dce 100644 --- a/Mathlib/RingTheory/HahnSeries/Addition.lean +++ b/Mathlib/RingTheory/HahnSeries/Addition.lean @@ -102,7 +102,7 @@ lemma addOppositeEquiv_orderTop (x : HahnSeries Γ (Rᵃᵒᵖ)) : simp only [orderTop, AddOpposite.unop_op, mk_eq_zero, AddEquivClass.map_eq_zero_iff, addOppositeEquiv_support, ne_eq] simp only [addOppositeEquiv_apply, AddOpposite.unop_op, mk_eq_zero, zero_coeff] - simp_rw [HahnSeries.ext_iff, Function.funext_iff] + simp_rw [HahnSeries.ext_iff, funext_iff] simp only [Pi.zero_apply, AddOpposite.unop_eq_zero_iff, zero_coeff] @[simp] @@ -116,7 +116,7 @@ lemma addOppositeEquiv_leadingCoeff (x : HahnSeries Γ (Rᵃᵒᵖ)) : simp only [leadingCoeff, AddOpposite.unop_op, mk_eq_zero, AddEquivClass.map_eq_zero_iff, addOppositeEquiv_support, ne_eq] simp only [addOppositeEquiv_apply, AddOpposite.unop_op, mk_eq_zero, zero_coeff] - simp_rw [HahnSeries.ext_iff, Function.funext_iff] + simp_rw [HahnSeries.ext_iff, funext_iff] simp only [Pi.zero_apply, AddOpposite.unop_eq_zero_iff, zero_coeff] split <;> rfl diff --git a/Mathlib/RingTheory/HahnSeries/Basic.lean b/Mathlib/RingTheory/HahnSeries/Basic.lean index b063204680d7f..29586b2758fad 100644 --- a/Mathlib/RingTheory/HahnSeries/Basic.lean +++ b/Mathlib/RingTheory/HahnSeries/Basic.lean @@ -427,7 +427,7 @@ theorem embDomain_single {f : Γ ↪o Γ'} {g : Γ} {r : R} : theorem embDomain_injective {f : Γ ↪o Γ'} : Function.Injective (embDomain f : HahnSeries Γ R → HahnSeries Γ' R) := fun x y xy => by ext g - rw [HahnSeries.ext_iff, Function.funext_iff] at xy + rw [HahnSeries.ext_iff, funext_iff] at xy have xyg := xy (f g) rwa [embDomain_coeff, embDomain_coeff] at xyg diff --git a/Mathlib/RingTheory/HahnSeries/Multiplication.lean b/Mathlib/RingTheory/HahnSeries/Multiplication.lean index 153ac24993c5d..11ac4db05c9d9 100644 --- a/Mathlib/RingTheory/HahnSeries/Multiplication.lean +++ b/Mathlib/RingTheory/HahnSeries/Multiplication.lean @@ -535,7 +535,7 @@ instance instNoZeroSMulDivisors {Γ} [LinearOrderedCancelAddCommMonoid Γ] [Zero eq_zero_or_eq_zero_of_smul_eq_zero {x y} hxy := by contrapose! hxy simp only [ne_eq] - rw [HahnModule.ext_iff, Function.funext_iff, not_forall] + rw [HahnModule.ext_iff, funext_iff, not_forall] refine ⟨x.order + ((of R).symm y).order, ?_⟩ rw [smul_coeff_order_add_order x y, of_symm_zero, HahnSeries.zero_coeff, smul_eq_zero, not_or] constructor @@ -644,7 +644,7 @@ theorem C_one : C (1 : R) = (1 : HahnSeries Γ R) := theorem C_injective : Function.Injective (C : R → HahnSeries Γ R) := by intro r s rs - rw [HahnSeries.ext_iff, Function.funext_iff] at rs + rw [HahnSeries.ext_iff, funext_iff] at rs have h := rs 0 rwa [C_apply, single_coeff_same, C_apply, single_coeff_same] at h @@ -756,7 +756,7 @@ instance [Nontrivial Γ] [Nontrivial R] : Nontrivial (Subalgebra R (HahnSeries refine ⟨single a 1, ?_⟩ simp only [Algebra.mem_bot, not_exists, Set.mem_range, iff_true, Algebra.mem_top] intro x - rw [HahnSeries.ext_iff, Function.funext_iff, not_forall] + rw [HahnSeries.ext_iff, funext_iff, not_forall] refine ⟨a, ?_⟩ rw [single_coeff_same, algebraMap_apply, C_apply, single_coeff_of_ne ha] exact zero_ne_one⟩⟩ diff --git a/Mathlib/RingTheory/Ideal/Maps.lean b/Mathlib/RingTheory/Ideal/Maps.lean index 687a565ce36b9..faa5fc206c934 100644 --- a/Mathlib/RingTheory/Ideal/Maps.lean +++ b/Mathlib/RingTheory/Ideal/Maps.lean @@ -570,7 +570,7 @@ theorem ker_ne_top [Nontrivial S] (f : F) : ker f ≠ ⊤ := lemma _root_.Pi.ker_ringHom {ι : Type*} {R : ι → Type*} [∀ i, Semiring (R i)] (φ : ∀ i, S →+* R i) : ker (Pi.ringHom φ) = ⨅ i, ker (φ i) := by ext x - simp [mem_ker, Ideal.mem_iInf, Function.funext_iff] + simp [mem_ker, Ideal.mem_iInf, funext_iff] @[simp] theorem ker_rangeSRestrict (f : R →+* S) : ker f.rangeSRestrict = ker f := diff --git a/Mathlib/RingTheory/Idempotents.lean b/Mathlib/RingTheory/Idempotents.lean index c2dd1724dad6f..958157f3ad00b 100644 --- a/Mathlib/RingTheory/Idempotents.lean +++ b/Mathlib/RingTheory/Idempotents.lean @@ -402,7 +402,7 @@ lemma CompleteOrthogonalIdempotents.bijective_pi (he : CompleteOrthogonalIdempot refine ⟨?_, he.1.surjective_pi⟩ rw [injective_iff_map_eq_zero] intro x hx - simp [Function.funext_iff, Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton] at hx + simp [funext_iff, Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton] at hx suffices ∀ s : Finset I, (∏ i in s, (1 - e i)) * x = x by rw [← this Finset.univ, he.prod_one_sub, zero_mul] refine fun s ↦ Finset.induction_on s (by simp) ?_ diff --git a/Mathlib/RingTheory/WittVector/Defs.lean b/Mathlib/RingTheory/WittVector/Defs.lean index 53b4f06f4f2d8..5003404660142 100644 --- a/Mathlib/RingTheory/WittVector/Defs.lean +++ b/Mathlib/RingTheory/WittVector/Defs.lean @@ -72,7 +72,7 @@ theorem ext {x y : 𝕎 R} (h : ∀ n, x.coeff n = y.coeff n) : x = y := by cases x cases y simp only at h - simp [Function.funext_iff, h] + simp [funext_iff, h] variable (p) diff --git a/Mathlib/RingTheory/WittVector/IsPoly.lean b/Mathlib/RingTheory/WittVector/IsPoly.lean index da0cac3cda942..69617badd6694 100644 --- a/Mathlib/RingTheory/WittVector/IsPoly.lean +++ b/Mathlib/RingTheory/WittVector/IsPoly.lean @@ -113,7 +113,7 @@ theorem poly_eq_of_wittPolynomial_bind_eq' [Fact p.Prime] (f g : ℕ → MvPolyn (h : ∀ n, bind₁ f (wittPolynomial p _ n) = bind₁ g (wittPolynomial p _ n)) : f = g := by ext1 n apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective - rw [← Function.funext_iff] at h + rw [← funext_iff] at h replace h := congr_arg (fun fam => bind₁ (MvPolynomial.map (Int.castRingHom ℚ) ∘ fam) (xInTermsOfW p ℚ n)) h simpa only [Function.comp_def, map_bind₁, map_wittPolynomial, ← bind₁_bind₁, @@ -123,7 +123,7 @@ theorem poly_eq_of_wittPolynomial_bind_eq [Fact p.Prime] (f g : ℕ → MvPolyno (h : ∀ n, bind₁ f (wittPolynomial p _ n) = bind₁ g (wittPolynomial p _ n)) : f = g := by ext1 n apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective - rw [← Function.funext_iff] at h + rw [← funext_iff] at h replace h := congr_arg (fun fam => bind₁ (MvPolynomial.map (Int.castRingHom ℚ) ∘ fam) (xInTermsOfW p ℚ n)) h simpa only [Function.comp_def, map_bind₁, map_wittPolynomial, ← bind₁_bind₁, diff --git a/Mathlib/Topology/Algebra/Module/Basic.lean b/Mathlib/Topology/Algebra/Module/Basic.lean index 1ed9c07b215fe..3a3b76145aaeb 100644 --- a/Mathlib/Topology/Algebra/Module/Basic.lean +++ b/Mathlib/Topology/Algebra/Module/Basic.lean @@ -1134,7 +1134,7 @@ theorem pi_apply (f : ∀ i, M →L[R] φ i) (c : M) (i : ι) : pi f c i = f i c rfl theorem pi_eq_zero (f : ∀ i, M →L[R] φ i) : pi f = 0 ↔ ∀ i, f i = 0 := by - simp only [ContinuousLinearMap.ext_iff, pi_apply, Function.funext_iff] + simp only [ContinuousLinearMap.ext_iff, pi_apply, funext_iff] exact forall_swap theorem pi_zero : pi (fun _ => 0 : ∀ i, M →L[R] φ i) = 0 := diff --git a/Mathlib/Topology/Homotopy/Product.lean b/Mathlib/Topology/Homotopy/Product.lean index a898bde525861..cc848a691b504 100644 --- a/Mathlib/Topology/Homotopy/Product.lean +++ b/Mathlib/Topology/Homotopy/Product.lean @@ -72,7 +72,7 @@ def HomotopyRel.pi (homotopies : ∀ i : I, HomotopyRel (f i) (g i) S) : prop' := by intro t x hx dsimp only [coe_mk, pi_eval, toFun_eq_coe, HomotopyWith.coe_toContinuousMap] - simp only [Function.funext_iff, ← forall_and] + simp only [funext_iff, ← forall_and] intro i exact (homotopies i).prop' t x hx } diff --git a/Mathlib/Topology/LocallyConstant/Basic.lean b/Mathlib/Topology/LocallyConstant/Basic.lean index 401cf78da5d19..916e783447b5b 100644 --- a/Mathlib/Topology/LocallyConstant/Basic.lean +++ b/Mathlib/Topology/LocallyConstant/Basic.lean @@ -358,7 +358,7 @@ def unflip {X α β : Type*} [Finite α] [TopologicalSpace X] (f : α → Locall toFun x a := f a x isLocallyConstant := IsLocallyConstant.iff_isOpen_fiber.2 fun g => by have : (fun (x : X) (a : α) => f a x) ⁻¹' {g} = ⋂ a : α, f a ⁻¹' {g a} := by - ext; simp [Function.funext_iff] + ext; simp [funext_iff] rw [this] exact isOpen_iInter_of_finite fun a => (f a).isLocallyConstant _ diff --git a/Mathlib/Topology/TietzeExtension.lean b/Mathlib/Topology/TietzeExtension.lean index c707446315731..9a2271b7f1202 100644 --- a/Mathlib/Topology/TietzeExtension.lean +++ b/Mathlib/Topology/TietzeExtension.lean @@ -321,7 +321,7 @@ theorem exists_extension_forall_exists_le_ge_of_closedEmbedding [Nonempty X] (f rcases hle.eq_or_lt with (rfl | hlt) · have : ∀ x, f x = a := by simpa using hmem use const Y a - simp [this, Function.funext_iff] + simp [this, funext_iff] -- Put `c = (a + b) / 2`. Then `a < c < b` and `c - a = b - c`. set c := (a + b) / 2 have hac : a < c := left_lt_add_div_two.2 hlt diff --git a/test/instance_diamonds.lean b/test/instance_diamonds.lean index f26a6b719c7ff..8ced918dadd0d 100644 --- a/test/instance_diamonds.lean +++ b/test/instance_diamonds.lean @@ -153,7 +153,7 @@ example {k : Type _} [Semiring k] [Nontrivial k] : (Finsupp.comapSMul : SMul k (k →₀ k)) ≠ Finsupp.smulZeroClass.toSMul := by obtain ⟨u : k, hu⟩ := exists_ne (1 : k) intro h - simp only [SMul.ext_iff, @SMul.smul_eq_hSMul _ _ (_), Function.funext_iff, DFunLike.ext_iff] at h + simp only [SMul.ext_iff, @SMul.smul_eq_hSMul _ _ (_), funext_iff, DFunLike.ext_iff] at h replace h := h u (Finsupp.single 1 1) u classical rw [comapSMul_single, smul_apply, smul_eq_mul, mul_one, single_eq_same, smul_eq_mul, @@ -167,7 +167,7 @@ example {k : Type _} [Semiring k] [Nontrivial kˣ] : obtain ⟨u : kˣ, hu⟩ := exists_ne (1 : kˣ) haveI : Nontrivial k := ⟨⟨u, 1, Units.ext.ne hu⟩⟩ intro h - simp only [SMul.ext_iff, @SMul.smul_eq_hSMul _ _ (_), Function.funext_iff, DFunLike.ext_iff] at h + simp only [SMul.ext_iff, @SMul.smul_eq_hSMul _ _ (_), funext_iff, DFunLike.ext_iff] at h replace h := h u (Finsupp.single 1 1) u classical rw [comapSMul_single, smul_apply, Units.smul_def, smul_eq_mul, mul_one, single_eq_same, @@ -191,14 +191,14 @@ open Polynomial example [Semiring R] [Nontrivial R] : Polynomial.hasSMulPi _ _ ≠ (Pi.instSMul : SMul R[X] (R → R[X])) := by intro h - simp_rw [SMul.ext_iff, @SMul.smul_eq_hSMul _ _ (_), Function.funext_iff, Polynomial.ext_iff] at h + simp_rw [SMul.ext_iff, @SMul.smul_eq_hSMul _ _ (_), funext_iff, Polynomial.ext_iff] at h simpa using h X 1 1 0 /-- `Polynomial.hasSMulPi'` forms a diamond with `Pi.instSMul`. -/ example [CommSemiring R] [Nontrivial R] : Polynomial.hasSMulPi' _ _ _ ≠ (Pi.instSMul : SMul R[X] (R → R[X])) := by intro h - simp_rw [SMul.ext_iff, @SMul.smul_eq_hSMul _ _ (_), Function.funext_iff, Polynomial.ext_iff] at h + simp_rw [SMul.ext_iff, @SMul.smul_eq_hSMul _ _ (_), funext_iff, Polynomial.ext_iff] at h simpa using h X 1 1 0 -- fails `with_reducible_and_instances` #10906