fixes

Monlib/LinearAlgebra/Coalgebra/FiniteDimensional.lean

@@ -275,7 +275,7 @@ noncomputable def FiniteDimensionalCoAlgebra_isFrobeniusAlgebra_of
 open CoalgebraStruct
 structure LinearMap.IsCoalgHom {R A B : Type*}
   [CommSemiring R] [AddCommMonoid A] [Module R A] [AddCommMonoid B] [Module R B]
-  [CoalgebraStruct R A] [CoalgebraStruct R B] (x : A →ₗ[R] B) : Prop :=
+  [CoalgebraStruct R A] [CoalgebraStruct R B] (x : A →ₗ[R] B) : Prop where
     counit_comp : counit ∘ₗ x = counit
     map_comp_comul : TensorProduct.map x x ∘ₗ comul = comul ∘ₗ x
 lemma LinearMap.isCoalgHom_iff {R A B : Type*}
@@ -285,7 +285,7 @@ lemma LinearMap.isCoalgHom_iff {R A B : Type*}
 ⟨λ h => ⟨h.1, h.2⟩, λ h => ⟨h.1, h.2⟩⟩
 
 structure LinearMap.IsAlgHom {R A B : Type*} [CommSemiring R] [Semiring A] [Semiring B]
-  [Algebra R A] [Algebra R B] (x : A →ₗ[R] B) : Prop :=
+  [Algebra R A] [Algebra R B] (x : A →ₗ[R] B) : Prop where
     comp_unit : x ∘ₗ Algebra.linearMap R A = Algebra.linearMap R B
     mul'_comp_map : (mul' R B) ∘ₗ (TensorProduct.map x x) = x ∘ₗ (mul' R A)
 lemma LinearMap.isAlgHom_iff {R A B : Type*} [CommSemiring R] [Semiring A] [Semiring B]

Monlib/LinearAlgebra/InnerAut.lean

@@ -483,7 +483,7 @@ theorem _root_.StarAlgEquiv.of_matrix_is_inner
   have this9 := (PosSemidef.invertible_iff_posDef this8).mp this7
   have this12 : (1 : n → 𝕜) ≠ 0 :=
     by
-    simp_rw [ne_eq, Function.funext_iff, Pi.one_apply, Pi.zero_apply, one_ne_zero]
+    simp_rw [ne_eq, funext_iff, Pi.one_apply, Pi.zero_apply, one_ne_zero]
     simp only [Classical.not_forall, not_false_iff, exists_const]
   have this10 : α = RCLike.re α :=
     by
@@ -573,9 +573,9 @@ theorem diagonal.spectrum {𝕜 n : Type _} [Field 𝕜] [Fintype n] [DecidableE
     spectrum 𝕜 (toLin' (diagonal A : Matrix n n 𝕜)) = {x : 𝕜 | ∃ i : n, A i = x} :=
   by
   simp_rw [Set.ext_iff, ← Module.End.hasEigenvalue_iff_mem_spectrum, ←
-    Module.End.has_eigenvector_iff_hasEigenvalue, toLin'_apply, Function.funext_iff, mulVec,
+    Module.End.has_eigenvector_iff_hasEigenvalue, toLin'_apply, funext_iff, mulVec,
     diagonal_dotProduct, Pi.smul_apply, Algebra.id.smul_eq_mul, mul_eq_mul_right_iff, ne_eq,
-    Set.mem_setOf_eq, Function.funext_iff, Pi.zero_apply, Classical.not_forall]
+    Set.mem_setOf_eq, funext_iff, Pi.zero_apply, Classical.not_forall]
   intro x
   constructor
   · rintro ⟨v, ⟨h, ⟨j, hj⟩⟩⟩

Monlib/LinearAlgebra/Ips/Functional.lean

@@ -236,7 +236,7 @@ lemma PiMat.nonneg_iff {k : Type _} [Fintype k]
   0 ≤ x ↔ ∃ y : PiMat ℂ k s, x = star y * y :=
 by
   simp_rw [Pi.le_def, Pi.zero_apply, Pi.mul_def, Pi.star_apply, Matrix.nonneg_iff,
-    Function.funext_iff]
+    funext_iff]
   exact ⟨λ h => ⟨(λ i => (h i).choose), λ _ => (h _).choose_spec⟩,
     λ h a => ⟨h.choose a, h.choose_spec _⟩⟩
 
@@ -277,7 +277,7 @@ def Module.Dual.IsUnital {A : Type _} [AddCommMonoid A] [Module R A] [One A] (φ
 
 /-- A linear functional is called a state if it is positive and unital -/
 class Module.Dual.IsState {A : Type _} [Semiring A] [StarRing A] [Module 𝕜 A] (φ : Module.Dual 𝕜 A) :
-    Prop :=
+    Prop where
 toIsPosMap : φ.IsPosMap
 toIsUnital : φ.IsUnital
 
@@ -301,7 +301,7 @@ lemma Matrix.includeBlock_eq_zero {k : Type _} [Fintype k] [DecidableEq k] {s :
   {x : Matrix (s i) (s i) R} :
   includeBlock x = 0 ↔ x = 0 :=
 by
-  simp_rw [Function.funext_iff, Pi.zero_apply, includeBlock_apply,
+  simp_rw [funext_iff, Pi.zero_apply, includeBlock_apply,
     dite_eq_right_iff, eq_mp_eq_cast]
   exact ⟨λ h => (h i rfl), by rintro rfl a rfl; rfl⟩
 
@@ -404,7 +404,7 @@ theorem Module.Dual.IsPosMap.isFaithful_iff_of_matrix {φ : Module.Dual ℂ (Mat
 --     (φ : Module.Dual 𝕜 A) : Prop :=
 --   φ.IsPosMap ∧ φ.IsFaithful
 @[class]
-structure Module.Dual.IsFaithfulPosMap {A : Type _} [NonUnitalSemiring A] [StarRing A] [Module 𝕜 A] (φ : Module.Dual 𝕜 A) : Prop :=
+structure Module.Dual.IsFaithfulPosMap {A : Type _} [NonUnitalSemiring A] [StarRing A] [Module 𝕜 A] (φ : Module.Dual 𝕜 A) : Prop where
 toIsPosMap : φ.IsPosMap
 toIsFaithful : φ.IsFaithful
 
@@ -762,10 +762,8 @@ theorem Module.Dual.isFaithfulPosMap_of_matrix_tfae (φ : Module.Dual ℂ (Matri
       [φ.IsFaithfulPosMap, φ.matrix.PosDef,
         IsInner fun xy : Matrix n n ℂ × Matrix n n ℂ => φ (xy.1ᴴ * xy.2)] :=
   by
-  tfae_have 1 ↔ 2
-  · exact φ.isFaithfulPosMap_iff_of_matrix
-  tfae_have 1 ↔ 3
-  · exact φ.isFaithfulPosMap_iff_isInner_of_matrix
+  tfae_have 1 ↔ 2 := φ.isFaithfulPosMap_iff_of_matrix
+  tfae_have 1 ↔ 3 := φ.isFaithfulPosMap_iff_isInner_of_matrix
   tfae_finish
 
 end

Monlib/LinearAlgebra/Ips/MatIps.lean

@@ -331,8 +331,8 @@ theorem starAlgEquiv_is_isometry_tFAE [hφ : φ.IsFaithfulPosMap] [Nontrivial n]
         φ ∘ₗ f.toLinearMap = φ, ∀ x y, ⟪f x, f y⟫_ℂ = ⟪x, y⟫_ℂ,
         ∀ x : Matrix n n ℂ, ‖f x‖ = ‖x‖, Commute φ.matrix f.of_matrix_unitary] :=
   by
-  tfae_have 5 ↔ 2
-  · simp_rw [InnerProductSpace.Core.norm_eq_sqrt_inner,
+  tfae_have 5 ↔ 2 := by
+    simp_rw [InnerProductSpace.Core.norm_eq_sqrt_inner,
       Real.sqrt_inj inner_self_nonneg inner_self_nonneg,
       ← Complex.ofReal_inj]
     have : ∀ x : Matrix n n ℂ, (RCLike.re ⟪x, x⟫_ℂ : ℂ) = ⟪x, x⟫_ℂ := fun x => inner_self_ofReal_re x
@@ -349,8 +349,8 @@ theorem starAlgEquiv_is_isometry_tFAE [hφ : φ.IsFaithfulPosMap] [Nontrivial n]
     simp_rw [this, inner_map_self_eq_zero, sub_eq_zero, StarAlgEquiv.comp_eq_iff,
       LinearMap.one_comp]
   rw [tfae_5_iff_2]
-  tfae_have 4 ↔ 3
-  · simp_rw [inner_eq, ← star_eq_conjTranspose, ← map_star f, ← _root_.map_mul f,
+  tfae_have 4 ↔ 3 := by
+    simp_rw [inner_eq, ← star_eq_conjTranspose, ← map_star f, ← _root_.map_mul f,
       LinearMap.ext_iff, LinearMap.comp_apply, StarAlgEquiv.toLinearMap_apply]
     refine' ⟨fun h x => _, fun h x y => h _⟩
     rw [← Matrix.one_mul x, ← star_one]
@@ -361,14 +361,13 @@ theorem starAlgEquiv_is_isometry_tFAE [hφ : φ.IsFaithfulPosMap] [Nontrivial n]
     StarAlgEquiv.toLinearMap_apply, mul_inv_eq_iff_eq_mul_of_invertible,
     φ.apply, StarAlgEquiv.symm_apply_eq, _root_.map_mul,
     StarAlgEquiv.apply_symm_apply, ← forall_left_hMul φ.matrix, @eq_comm _ φ.matrix]
-  tfae_have 1 ↔ 2
-  · rw [iff_self]; trivial
-  tfae_have 1 → 3
-  · intro i x
+  tfae_have 1 ↔ 2 := by rw [iff_self]; trivial
+  tfae_have 1 → 3 := by
+    intro i x
     nth_rw 1 [← i]
     rw [← _root_.map_mul, f.trace_preserving]
-  tfae_have 3 → 1
-  · intro i
+  tfae_have 3 → 1 := by
+    intro i
     simp_rw [← f.symm.trace_preserving (φ.matrix * f _), _root_.map_mul,
       StarAlgEquiv.symm_apply_apply, ← φ.apply, @eq_comm _ _ (φ _)] at i
     -- obtain ⟨Q, hQ, h⟩ := Module.Dual.eq_trace_unique φ
@@ -607,7 +606,7 @@ theorem inner_eq [∀ i, (ψ i).IsFaithfulPosMap] (x y : PiMat ℂ k s) :
   rfl
 
 omit [DecidableEq k] in
-theorem inner_eq' [hψ : ∀ i, (ψ i).IsFaithfulPosMap] (x y : PiMat ℂ k s) :
+theorem inner_eq' [∀ i, (ψ i).IsFaithfulPosMap] (x y : PiMat ℂ k s) :
     ⟪x, y⟫_ℂ = ∑ i, ((ψ i).matrix * (x i)ᴴ * y i).trace := by
   simp only [inner_eq, Module.Dual.pi.apply, Pi.mul_apply,
     Matrix.star_eq_conjTranspose, Pi.star_apply, Matrix.mul_assoc]
@@ -1315,7 +1314,7 @@ theorem LinearMap.pi_mul'_comp_mul'_adjoint_eq_smul_id_iff [hψ : ∀ i, (ψ i).
     LinearMap.mul' ℂ (PiMat ℂ k s) ∘ₗ (LinearMap.adjoint (LinearMap.mul' ℂ (PiMat ℂ k s))) = α • 1 ↔ ∀ i, Matrix.trace ((ψ i).matrix⁻¹) = α :=
   by
   simp_rw [LinearMap.ext_iff, LinearMap.comp_apply, LinearMap.pi_mul'_comp_mul'_adjoint,
-    Function.funext_iff, Finset.sum_apply, ← LinearMap.map_smul,
+    funext_iff, Finset.sum_apply, ← LinearMap.map_smul,
     includeBlock_apply, Finset.sum_dite_eq', Finset.mem_univ, if_true,
     LinearMap.smul_apply, LinearMap.one_apply, Pi.smul_apply]
   simp only [eq_mp_eq_cast, cast_eq, ← Pi.smul_apply]

Monlib/LinearAlgebra/Ips/MinimalProj.lean

@@ -154,7 +154,7 @@ theorem orthogonalProjection.isIdempotentElem [InnerProductSpace 𝕜 E] (U : Su
     orthogonalProjection_mem_subspace_eq_self]
 
 class ContinuousLinearMap.IsOrthogonalProjection [InnerProductSpace 𝕜 E]
-  (T : E →L[𝕜] E) : Prop :=
+  (T : E →L[𝕜] E) : Prop where
   isIdempotent : IsIdempotentElem T
   kerEqRangeOrtho : LinearMap.ker T = (LinearMap.range T)ᗮ
 
@@ -383,14 +383,13 @@ theorem IsIdempotentElem.self_adjoint_is_positive_isOrthogonalProjection_tFAE {E
     [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {p : E →L[ℂ] E}
     (hp : IsIdempotentElem p) : List.TFAE [IsSelfAdjoint p, p.IsOrthogonalProjection, 0 ≤ p] :=
   by
-  tfae_have 3 ↔ 1
-  · exact hp.is_positive_iff_self_adjoint
-  tfae_have 2 → 1
-  · intro h
+  tfae_have 3 ↔ 1 := hp.is_positive_iff_self_adjoint
+  tfae_have 2 → 1 := by
+    intro h
     rw [IsIdempotentElem.isSelfAdjoint_iff_ker_isOrtho_to_range _ hp]
     exact h.2
-  tfae_have 1 → 2
-  · intro h
+  tfae_have 1 → 2 := by
+    intro h
     rw [IsIdempotentElem.isSelfAdjoint_iff_ker_isOrtho_to_range _ hp] at h
     exact ⟨hp, h⟩
   tfae_finish

Monlib/LinearAlgebra/Matrix/IncludeBlock.lean

@@ -377,7 +377,7 @@ theorem includeBlock_inj {k : Type _} [Fintype k] [DecidableEq k] {s : k → Typ
   by
   simp only [includeBlock_apply]
   refine' ⟨fun h => _, fun h => by rw [h]⟩
-  simp_rw [Function.funext_iff, ← Matrix.ext_iff, eq_mp_eq_cast] at h
+  simp_rw [funext_iff, ← Matrix.ext_iff, eq_mp_eq_cast] at h
   ext j k
   specialize h i j k
   aesop

Monlib/LinearAlgebra/Matrix/StarOrderedRing.lean

@@ -180,7 +180,7 @@ theorem diagonal_posDef_iff {𝕜 n : Type _}
       mul_zero, Finset.sum_ite_eq', Finset.mem_univ, if_true, norm_one,
       RCLike.ofReal_one, one_pow, mul_one] at h2
     apply h2
-    simp_rw [ne_eq, Function.funext_iff, not_forall]
+    simp_rw [ne_eq, funext_iff, not_forall]
     use i
     simp only [↓reduceIte, Pi.zero_apply, one_ne_zero, not_false_eq_true]
   . intro h
@@ -191,7 +191,7 @@ theorem diagonal_posDef_iff {𝕜 n : Type _}
     simp_rw [RCLike.conj_eq_iff_re] at h
     rw [← (h i).2, ← RCLike.ofReal_pow, ← RCLike.ofReal_mul, RCLike.zero_le_real]
     apply mul_nonneg (le_of_lt (h i).1) (sq_nonneg _)
-    simp_rw [ne_eq, Function.funext_iff, not_forall, Pi.zero_apply] at hx
+    simp_rw [ne_eq, funext_iff, not_forall, Pi.zero_apply] at hx
     obtain ⟨i, hi⟩ := hx
     use i
     simp only [Finset.mem_univ, true_and, ← RCLike.ofReal_pow]
@@ -394,7 +394,7 @@ theorem Pi.le_iff_sub_nonneg {ι : Type _} [Fintype ι] [DecidableEq ι] {n : ι
     [∀ i, Fintype (n i)] [∀ i, DecidableEq (n i)] (x y : PiMat ℂ ι n) :
     x ≤ y ↔ ∃ z : PiMat ℂ ι n, y = x + star z * z :=
   by
-  simp_rw [Function.funext_iff, Pi.add_apply, Pi.mul_apply, Pi.star_apply,
+  simp_rw [funext_iff, Pi.add_apply, Pi.mul_apply, Pi.star_apply,
     Pi.le_def, Matrix.le_iff, Matrix.posSemidef_iff, sub_eq_iff_eq_add',
     Matrix.star_eq_conjTranspose]
   exact

Monlib/LinearAlgebra/PiDirectSum.lean

@@ -239,7 +239,7 @@ theorem Pi.tensor_ext_iff {R : Type _} [CommRing R] {ι₁ : Type _} {ι₂ : Ty
     (y w : ∀ i, M₂ i) : x ⊗ₜ[R] y = z ⊗ₜ[R] w ↔ ∀ i j, x i ⊗ₜ[R] y j = z i ⊗ₜ[R] w j :=
   by
   rw [← Function.Injective.eq_iff directSumTensor.injective]
-  simp_rw [Function.funext_iff, directSumTensor_apply, directSumTensorToFun_apply, Prod.forall]
+  simp_rw [funext_iff, directSumTensor_apply, directSumTensorToFun_apply, Prod.forall]
 
 theorem Pi.tensor_ext {R : Type _} [CommRing R] {ι₁ : Type _} {ι₂ : Type _} [DecidableEq ι₁]
     [DecidableEq ι₂] [Fintype ι₁] [Fintype ι₂] {M₁ : ι₁ → Type _} {M₂ : ι₂ → Type _}

Monlib/LinearAlgebra/PiStarOrderedRing.lean

@@ -95,7 +95,7 @@ theorem Pi.StarOrderedRing.nonneg_def {ι : Type _} {α : ι → Type _} [∀ i,
     (h : ∀ (i : ι) (x : α i), 0 ≤ x ↔ ∃ y, star y * y = x) (x : ∀ i, α i) :
     0 ≤ x ↔ ∃ y, star y * y = x :=
   by
-  simp_rw [Pi.le_def, Pi.zero_apply, Function.funext_iff, Pi.mul_apply, Pi.star_apply, h]
+  simp_rw [Pi.le_def, Pi.zero_apply, funext_iff, Pi.mul_apply, Pi.star_apply, h]
   exact
     ⟨fun hx => ⟨fun i => (hx i).choose, fun i => (hx i).choose_spec⟩,
     fun ⟨y, hy⟩ i => ⟨y i, hy i⟩⟩

Monlib/LinearAlgebra/PosMap_isReal.lean

@@ -428,7 +428,7 @@ theorem PiMat.IsSelfAdjoint.posSemidefDecomposition {k : Type*} {n : k → Type*
 by
   have : ∀ i, (x i).IsHermitian := λ i =>
   by
-    rw [IsSelfAdjoint, Function.funext_iff] at hx
+    rw [IsSelfAdjoint, funext_iff] at hx
     simp_rw [Pi.star_apply, Matrix.star_eq_conjTranspose] at hx
     exact hx i
   have := λ i => Matrix.IsHermitian.posSemidefDecomposition' (this i)
@@ -468,7 +468,7 @@ by
   . rw [hab, ← toLinearMapAlgEquiv_symm_apply, map_sub, map_mul]
     rfl
 
-structure isEquivToPiMat (A : Type*) [Add A] [Mul A] [Star A] [SMul ℂ A] :=
+structure isEquivToPiMat (A : Type*) [Add A] [Mul A] [Star A] [SMul ℂ A] where
   k : Type*
   -- hn₁ : Fintype n
   -- hn₂ : DecidableEq n
@@ -544,7 +544,7 @@ theorem StarNonUnitalAlgHom.toLinearMap_apply
   {R A B : Type*} [Semiring R] [NonUnitalNonAssocSemiring A]
   [Module R A] [NonUnitalNonAssocSemiring B] [Module R B]
   [Star A] [Star B]
-  (f : A →⋆ₙₐ[R] B) (x : A) : (f.toLinearMap : A →ₗ[R] B) x = f x := rfl
+  (f : A →⋆ₙₐ[R] B) (x : A) : (f : A →ₗ[R] B) x = f x := rfl
 
 theorem LinearMap.isPosMap_iff_star_mul_self_nonneg {A K : Type*}
   [NonUnitalSemiring A] [PartialOrder A] [StarRing A] [StarOrderedRing A]
@@ -666,7 +666,7 @@ theorem NonUnitalAlgHom.isPosMap_iff_isReal_of_nonUnitalStarAlgEquiv_piMat
   {f : A →ₙₐ[ℂ] K} :
   LinearMap.IsPosMap f ↔ LinearMap.IsReal f :=
 by
-  have : LinearMap.IsPosMap f ↔ LinearMap.IsPosMap f.toLinearMap := by rfl
+  have : LinearMap.IsPosMap f ↔ LinearMap.IsPosMap (f : A →ₗ[ℂ] K) := by rfl
   refine ⟨λ h => isReal_of_isPosMap_of_starAlgEquiv_piMat hφ (this.mp h), λ h => ?_⟩
   let f' : A →⋆ₙₐ[ℂ] K := NonUnitalStarAlgHom.mk f h
   exact starMulHom_isPosMap hA f'

Monlib/LinearAlgebra/QuantumSet/Basic.lean

@@ -997,8 +997,8 @@ theorem _root_.QuantumSet.starAlgEquiv_is_isometry_tfae
         ∀ x, ‖f x‖ = ‖x‖,
         Isometry f] :=
 by
-  tfae_have 3 ↔ 1
-  · simp_rw [@norm_eq_sqrt_inner ℂ, Real.sqrt_inj inner_self_nonneg inner_self_nonneg,
+  tfae_have 3 ↔ 1 := by
+    simp_rw [@norm_eq_sqrt_inner ℂ, Real.sqrt_inj inner_self_nonneg inner_self_nonneg,
       ← @RCLike.ofReal_inj ℂ, @inner_self_re ℂ, ← @sub_eq_zero _ _ _ ⟪_, _⟫_ℂ]
     have :
       ∀ x y,

Monlib/LinearAlgebra/QuantumSet/Instances.lean

@@ -240,7 +240,7 @@ by
       simp only [hQQ, or_false]
       refine' ⟨λ ⟨h, h2⟩ => _, _⟩
       . rw [← Matrix.IsHermitian.eigenvalues_eq_zero_iff hQ.1] at hQQ
-        simp only [Function.funext_iff, Function.comp_apply, Pi.zero_apply,
+        simp only [funext_iff, Function.comp_apply, Pi.zero_apply,
           algebraMap.lift_map_eq_zero_iff, not_forall] at hQQ
         obtain ⟨i, hi⟩ := hQQ
         specialize h2 (hQ.1.eigenvectorMatrixᵀ i)

Monlib/LinearAlgebra/QuantumSet/Symm.lean

@@ -257,16 +257,16 @@ theorem symmMap_eq_conj_modAut_tfae (f : B →ₗ[ℂ] B) :
       f.real = (modAut (k B)).toLinearMap ∘ₗ LinearMap.adjoint f ∘ₗ (modAut (-k B)).toLinearMap,
       ∀ x y, counit (f x * y) = (counit (x * f y) : ℂ)] :=
 by
-  tfae_have 1 ↔ 2
-  . simp_rw [symmMap_apply, LinearMap.adjoint_eq_iff, LinearMap.adjoint_comp,
+  tfae_have 1 ↔ 2 := by
+    simp_rw [symmMap_apply, LinearMap.adjoint_eq_iff, LinearMap.adjoint_comp,
       QuantumSet.modAut_adjoint, LinearMap.comp_assoc]
-  tfae_have 1 → 3
-  . intro h x y
+  tfae_have 1 → 3 := by
+    intro h x y
     simp_rw [counit_map_mul_eq_counit_mul_modAut_conj_symmMap]
     simp_rw [h, LinearMap.comp_apply, AlgEquiv.toLinearMap_apply, QuantumSet.modAut_apply_modAut,
       add_neg_cancel, starAlgebra.modAut_zero, AlgEquiv.one_apply]
-  tfae_have 3 → 2
-  . intro h
+  tfae_have 3 → 2 := by
+    intro h
     rw [LinearMap.ext_iff_inner_map]
     intro u
     rw [hB.inner_eq_counit, LinearMap.real_apply, star_star, h]
@@ -283,10 +283,8 @@ theorem symmMap_eq_self_tfae (f : B →ₗ[ℂ] B) (gns : hB.k = 0) :
         f.real = LinearMap.adjoint f,
         ∀ x y : B, counit (f x * y) = (counit (x * f y) : ℂ)] :=
 by
-  tfae_have 1 ↔ 2
-  · rw [← LinearEquiv.eq_symm_apply, eq_comm]
-  tfae_have 1 ↔ 3
-  · rw [symmMap_apply, LinearMap.adjoint_eq_iff]
+  tfae_have 1 ↔ 2 := by rw [← LinearEquiv.eq_symm_apply, eq_comm]
+  tfae_have 1 ↔ 3 := by rw [symmMap_apply, LinearMap.adjoint_eq_iff]
   have := List.TFAE.out (symmMap_eq_conj_modAut_tfae f) 1 2
   simp only [gns, neg_zero, starAlgebra.modAut_zero, AlgEquiv.one_toLinearMap,
     LinearMap.one_comp, LinearMap.comp_one] at this

Monlib/Preq/Complex.lean

@@ -173,7 +173,7 @@ theorem abs_of_sum_sq_eq_sum_abs_sq_iff'' {n : Type _} [Fintype n] (α : n → 
       intros
       use 0
       simp_rw [H, Pi.zero_apply, MulZeroClass.zero_mul]
-    · have : ∃ i : n, α i ≠ 0 := by simp_rw [ne_eq, ← not_forall, ← Function.funext_iff]; exact H
+    · have : ∃ i : n, α i ≠ 0 := by simp_rw [ne_eq, ← not_forall, ← funext_iff]; exact H
       have := this
       cases' this with i hi
       cases' this with j hj

Monlib/QuantumGraph/Basic.lean

@@ -253,7 +253,7 @@ by
   simp_rw [← AlgEquiv.TensorProduct.map_toLinearMap, AlgEquiv.toLinearMap_apply,
     AlgEquiv.TensorProduct.map_map_toLinearMap, AlgEquiv.op_trans,
     QuantumSet.modAut_trans]
-  simp only [add_right_neg, QuantumSet.modAut_zero, sub_add_sub_cancel, sub_self,
+  simp only [add_neg_cancel, QuantumSet.modAut_zero, sub_add_sub_cancel, sub_self,
     AlgEquiv.op_one, AlgEquiv.TensorProduct.map_one, AlgEquiv.one_apply]
   simp only [← LinearEquiv.coe_toLinearMap, ← AlgEquiv.toLinearMap_apply,
     ← LinearMap.comp_apply, AlgEquiv.TensorProduct.map_toLinearMap, modAut_map_comp_Psi,
@@ -279,7 +279,7 @@ by
 
 
 class schurProjection (f : A →ₗ[ℂ] B) :
-    Prop :=
+    Prop where
   isIdempotentElem : f •ₛ f = f
   isReal : LinearMap.IsReal f
 
@@ -326,11 +326,11 @@ theorem schurIdempotent.isSchurProjection_iff_isPosMap
  λ h => ⟨hf, isReal_of_isPosMap_of_starAlgEquiv_piMat hh h⟩⟩
 
 class QuantumGraph (A : Type*) [starAlgebra A] [hA : QuantumSet A]
-    (f : A →ₗ[ℂ] A) : Prop :=
+    (f : A →ₗ[ℂ] A) : Prop where
   isIdempotentElem : f •ₛ f = f
 
 class QuantumGraph.IsReal {A : Type*} [starAlgebra A] [hA : QuantumSet A]
-    {f : A →ₗ[ℂ] A} (h : QuantumGraph A f) : Prop :=
+    {f : A →ₗ[ℂ] A} (h : QuantumGraph A f) : Prop where
   isReal : LinearMap.IsReal f
 
 class QuantumGraph.Real (A : Type*) [starAlgebra A] [hA : QuantumSet A]

Monlib/QuantumGraph/Example.lean

@@ -306,15 +306,15 @@ by
   · simp_rw [if_true, sub_eq_zero, eq_comm]
   · simp_rw [if_false, sub_eq_self]
 
-class QamReflexive (x : l(A)) : Prop :=
+class QamReflexive (x : l(A)) : Prop where
 toQam : x •ₛ x = x
 toRefl : x •ₛ 1 = 1
 
 lemma QamReflexive_iff (x : l(A)) :
     QamReflexive x ↔ x •ₛ x = x ∧ x •ₛ 1 = 1 :=
 ⟨λ h => ⟨h.toQam, h.toRefl⟩, λ h => ⟨h.1, h.2⟩⟩
 
-class QamIrreflexive (x : l(A)) : Prop :=
+class QamIrreflexive (x : l(A)) : Prop where
 toQam : x •ₛ x = x
 toIrrefl : x •ₛ 1 = 0
 

Monlib/RepTheory/AutMat.lean

@@ -348,7 +348,7 @@ theorem AlgEquiv.prod_isInner_iff_prod_map {K R₁ R₂ : Type*} [CommSemiring K
   [Semiring R₁] [Semiring R₂]
   [Algebra K R₁] [Algebra K R₂] (f : (R₁ × R₂) ≃ₐ[K] (R₁ × R₂)) :
   AlgEquiv.IsInner f
-    ↔ ∃ (a : R₁) (ha : Invertible a) (b : R₂) (hb : Invertible b),
+    ↔ ∃ (a : R₁) (_ha : Invertible a) (b : R₂) (_hb : Invertible b),
       f = AlgEquiv.prod_map (Algebra.autInner a) (Algebra.autInner b) :=
 by
   constructor
@@ -363,7 +363,7 @@ theorem AlgEquiv.pi_isInner_iff_pi_map {K ι : Type*} {R : ι → Type*} [CommSe
   [Π i, Semiring (R i)] [Π i, Algebra K (R i)]
   (f : (Π i, R i) ≃ₐ[K] (Π i, R i)) :
   AlgEquiv.IsInner f
-    ↔ ∃ (a : Π i, R i) (ha : Π i, Invertible (a i)),
+    ↔ ∃ (a : Π i, R i) (_ha : Π i, Invertible (a i)),
       f = AlgEquiv.Pi (λ i => Algebra.autInner (a i)) :=
 by constructor <;> exact λ ⟨a, ha, h⟩ => ⟨(λ i => a i), by infer_instance, by rw [h]; rfl⟩