From b9479c904d22ac0b81214a5f079029848f410460 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 20 Aug 2024 15:27:45 -0400
Subject: [PATCH] refactor: more multiple-goals

---
 .../PureU1/Odd/BasisLinear.lean               | 235 +++++++++---------
 .../PureU1/Odd/Parameterization.lean          |  14 +-
 .../SM/NoGrav/One/LinearParameterization.lean |  78 +++---
 .../IndexNotation/WithUniqueDual.lean         |  19 +-
 4 files changed, 166 insertions(+), 180 deletions(-)

diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean b/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean
index 40b3b65..d92a015 100644
--- a/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Odd/BasisLinear.lean
@@ -179,36 +179,36 @@ lemma basis_on_δ₁_other {k j : Fin n} (h : k ≠ j) :
   simp [basisAsCharges]
   simp [δ₁, δ₂]
   split
-  rename_i h1
-  rw [Fin.ext_iff] at h1
-  simp_all
-  rw [Fin.ext_iff] at h
-  simp_all
-  split
-  rename_i h1 h2
-  simp_all
-  rw [Fin.ext_iff] at h2
-  simp at h2
-  omega
-  rfl
+  · rename_i h1
+    rw [Fin.ext_iff] at h1
+    simp_all
+    rw [Fin.ext_iff] at h
+    simp_all
+  · split
+    · rename_i h1 h2
+      simp_all
+      rw [Fin.ext_iff] at h2
+      simp at h2
+      omega
+    · rfl
 
 lemma basis!_on_δ!₁_other {k j : Fin n} (h : k ≠ j) :
     basis!AsCharges k (δ!₁ j) = 0 := by
   simp [basis!AsCharges]
   simp [δ!₁, δ!₂]
   split
-  rename_i h1
-  rw [Fin.ext_iff] at h1
-  simp_all
-  rw [Fin.ext_iff] at h
-  simp_all
-  split
-  rename_i h1 h2
-  simp_all
-  rw [Fin.ext_iff] at h2
-  simp at h2
-  omega
-  rfl
+  · rename_i h1
+    rw [Fin.ext_iff] at h1
+    simp_all
+    rw [Fin.ext_iff] at h
+    simp_all
+  · split
+    · rename_i h1 h2
+      simp_all
+      rw [Fin.ext_iff] at h2
+      simp at h2
+      omega
+    rfl
 
 lemma basis_on_other {k : Fin n} {j : Fin (2 * n + 1)} (h1 : j ≠ δ₁ k) (h2 : j ≠ δ₂ k) :
     basisAsCharges k j = 0 := by
@@ -245,8 +245,8 @@ lemma basis!_δ!₂_eq_minus_δ!₁ (j i : Fin n) :
   all_goals rename_i h1 h2
   all_goals rw [Fin.ext_iff] at h1 h2
   all_goals simp_all
-  subst h1
-  exact Fin.elim0 i
+  · subst h1
+    exact Fin.elim0 i
   all_goals rename_i h3
   all_goals rw [Fin.ext_iff] at h3
   all_goals simp_all
@@ -269,26 +269,26 @@ lemma basis!_on_δ!₂_other {k j : Fin n} (h : k ≠ j) : basis!AsCharges k (δ
 lemma basis_on_δ₃ (j : Fin n) : basisAsCharges j δ₃ = 0 := by
   simp [basisAsCharges]
   split <;> rename_i h
-  rw [Fin.ext_iff] at h
-  simp [δ₃, δ₁] at h
-  omega
-  split <;> rename_i h2
-  rw [Fin.ext_iff] at h2
-  simp [δ₃, δ₂] at h2
-  omega
-  rfl
+  · rw [Fin.ext_iff] at h
+    simp [δ₃, δ₁] at h
+    omega
+  · split <;> rename_i h2
+    · rw [Fin.ext_iff] at h2
+      simp [δ₃, δ₂] at h2
+      omega
+    · rfl
 
 lemma basis!_on_δ!₃ (j : Fin n) : basis!AsCharges j δ!₃ = 0 := by
   simp [basis!AsCharges]
   split <;> rename_i h
-  rw [Fin.ext_iff] at h
-  simp [δ!₃, δ!₁] at h
-  omega
-  split <;> rename_i h2
-  rw [Fin.ext_iff] at h2
-  simp [δ!₃, δ!₂] at h2
-  omega
-  rfl
+  · rw [Fin.ext_iff] at h
+    simp [δ!₃, δ!₁] at h
+    omega
+  · split <;> rename_i h2
+    · rw [Fin.ext_iff] at h2
+      simp [δ!₃, δ!₂] at h2
+      omega
+    · rfl
 
 lemma basis_linearACC (j : Fin n) : (accGrav (2 * n + 1)) (basisAsCharges j) = 0 := by
   rw [accGrav]
@@ -338,16 +338,16 @@ lemma swap!_as_add {S S' : (PureU1 (2 * n + 1)).LinSols} (j : Fin n)
   funext i
   rw [← hS, FamilyPermutations_anomalyFreeLinear_apply]
   by_cases hi : i = δ!₁ j
-  subst hi
-  simp [HSMul.hSMul, basis!_on_δ!₁_self, pairSwap_inv_fst]
-  by_cases hi2 : i = δ!₂ j
-  subst hi2
-  simp [HSMul.hSMul,basis!_on_δ!₂_self, pairSwap_inv_snd]
-  simp [HSMul.hSMul]
-  rw [basis!_on_other hi hi2]
-  change S.val ((pairSwap (δ!₁ j) (δ!₂ j)).invFun i) =_
-  erw [pairSwap_inv_other (Ne.symm hi) (Ne.symm hi2)]
-  simp
+  · subst hi
+    simp [HSMul.hSMul, basis!_on_δ!₁_self, pairSwap_inv_fst]
+  · by_cases hi2 : i = δ!₂ j
+    · subst hi2
+      simp [HSMul.hSMul,basis!_on_δ!₂_self, pairSwap_inv_snd]
+    · simp [HSMul.hSMul]
+      rw [basis!_on_other hi hi2]
+      change S.val ((pairSwap (δ!₁ j) (δ!₂ j)).invFun i) =_
+      erw [pairSwap_inv_other (Ne.symm hi) (Ne.symm hi2)]
+      simp
 
 /-- A point in the span of the first part of the basis as a charge. -/
 def P (f : Fin n → ℚ) : (PureU1 (2 * n + 1)).Charges := ∑ i, f i • basisAsCharges i
@@ -362,45 +362,45 @@ lemma P_δ₁ (f : Fin n → ℚ) (j : Fin n) : P f (δ₁ j) = f j := by
   rw [P, sum_of_charges]
   simp [HSMul.hSMul, SMul.smul]
   rw [Finset.sum_eq_single j]
-  rw [basis_on_δ₁_self]
-  simp only [mul_one]
-  intro k _ hkj
-  rw [basis_on_δ₁_other hkj]
-  simp only [mul_zero]
-  simp only [mem_univ, not_true_eq_false, _root_.mul_eq_zero, IsEmpty.forall_iff]
+  · rw [basis_on_δ₁_self]
+    simp only [mul_one]
+  · intro k _ hkj
+    rw [basis_on_δ₁_other hkj]
+    simp only [mul_zero]
+  · simp only [mem_univ, not_true_eq_false, _root_.mul_eq_zero, IsEmpty.forall_iff]
 
 lemma P!_δ!₁ (f : Fin n → ℚ) (j : Fin n) : P! f (δ!₁ j) = f j := by
   rw [P!, sum_of_charges]
   simp [HSMul.hSMul, SMul.smul]
   rw [Finset.sum_eq_single j]
-  rw [basis!_on_δ!₁_self]
-  simp only [mul_one]
-  intro k _ hkj
-  rw [basis!_on_δ!₁_other hkj]
-  simp only [mul_zero]
-  simp only [mem_univ, not_true_eq_false, _root_.mul_eq_zero, IsEmpty.forall_iff]
+  · rw [basis!_on_δ!₁_self]
+    simp only [mul_one]
+  · intro k _ hkj
+    rw [basis!_on_δ!₁_other hkj]
+    simp only [mul_zero]
+  · simp only [mem_univ, not_true_eq_false, _root_.mul_eq_zero, IsEmpty.forall_iff]
 
 lemma P_δ₂ (f : Fin n → ℚ) (j : Fin n) : P f (δ₂ j) = - f j := by
   rw [P, sum_of_charges]
   simp [HSMul.hSMul, SMul.smul]
   rw [Finset.sum_eq_single j]
-  rw [basis_on_δ₂_self]
-  simp only [mul_neg, mul_one]
-  intro k _ hkj
-  rw [basis_on_δ₂_other hkj]
-  simp only [mul_zero]
-  simp
+  · rw [basis_on_δ₂_self]
+    simp only [mul_neg, mul_one]
+  · intro k _ hkj
+    rw [basis_on_δ₂_other hkj]
+    simp only [mul_zero]
+  · simp
 
 lemma P!_δ!₂ (f : Fin n → ℚ) (j : Fin n) : P! f (δ!₂ j) = - f j := by
   rw [P!, sum_of_charges]
   simp [HSMul.hSMul, SMul.smul]
   rw [Finset.sum_eq_single j]
-  rw [basis!_on_δ!₂_self]
-  simp only [mul_neg, mul_one]
-  intro k _ hkj
-  rw [basis!_on_δ!₂_other hkj]
-  simp only [mul_zero]
-  simp
+  · rw [basis!_on_δ!₂_self]
+    simp only [mul_neg, mul_one]
+  · intro k _ hkj
+    rw [basis!_on_δ!₂_other hkj]
+    simp only [mul_zero]
+  · simp
 
 lemma P_δ₃ (f : Fin n → ℚ) : P f (δ₃) = 0 := by
   rw [P, sum_of_charges]
@@ -476,12 +476,12 @@ lemma P_P_P!_accCube (g : Fin n → ℚ) (j : Fin n) :
   rw [sum_δ!, basis!_on_δ!₃]
   simp only [mul_zero, Function.comp_apply, zero_add]
   rw [Finset.sum_eq_single j, basis!_on_δ!₁_self, basis!_on_δ!₂_self]
-  rw [← δ₂_δ!₂, P_δ₂]
-  ring
-  intro k _ hkj
-  erw [basis!_on_δ!₁_other hkj.symm, basis!_on_δ!₂_other hkj.symm]
-  simp only [mul_zero, add_zero]
-  simp
+  · rw [← δ₂_δ!₂, P_δ₂]
+    ring
+  · intro k _ hkj
+    erw [basis!_on_δ!₁_other hkj.symm, basis!_on_δ!₂_other hkj.symm]
+    simp only [mul_zero, add_zero]
+  · simp
 
 lemma P_zero (f : Fin n → ℚ) (h : P f = 0) : ∀ i, f i = 0 := by
   intro i
@@ -584,29 +584,27 @@ theorem basisa_linear_independent : LinearIndependent ℚ (@basisa n.succ) := by
   have hf := Pa_zero (f ∘ Sum.inl) (f ∘ Sum.inr) h1
   have hg := Pa_zero! (f ∘ Sum.inl) (f ∘ Sum.inr) h1
   intro i
-  simp_all
+  simp_all only [succ_eq_add_one, Function.comp_apply]
   cases i
-  simp_all
-  simp_all
+  · simp_all
+  · simp_all
 
 lemma Pa'_eq (f f' : (Fin n.succ) ⊕ (Fin n.succ) → ℚ) : Pa' f = Pa' f' ↔ f = f' := by
-  apply Iff.intro
-  intro h
-  funext i
-  rw [Pa', Pa'] at h
-  have h1 : ∑ i : Fin n.succ ⊕ Fin n.succ, (f i + (- f' i)) • basisa i = 0 := by
-    simp only [add_smul, neg_smul]
-    rw [Finset.sum_add_distrib]
-    rw [h]
-    rw [← Finset.sum_add_distrib]
-    simp
-  have h2 : ∀ i, (f i + (- f' i)) = 0 := by
-    exact Fintype.linearIndependent_iff.mp (@basisa_linear_independent n)
-      (fun i => f i + -f' i) h1
-  have h2i := h2 i
-  linarith
-  intro h
-  rw [h]
+  refine Iff.intro (fun h => ?_) (fun h => ?_)
+  · funext i
+    rw [Pa', Pa'] at h
+    have h1 : ∑ i : Fin n.succ ⊕ Fin n.succ, (f i + (- f' i)) • basisa i = 0 := by
+      simp only [add_smul, neg_smul]
+      rw [Finset.sum_add_distrib]
+      rw [h]
+      rw [← Finset.sum_add_distrib]
+      simp
+    have h2 : ∀ i, (f i + (- f' i)) = 0 := by
+      exact Fintype.linearIndependent_iff.mp (@basisa_linear_independent n)
+        (fun i => f i + -f' i) h1
+    have h2i := h2 i
+    linarith
+  · rw [h]
 
 /-! TODO: Replace the definition of `join` with a Mathlib definition, most likely `Sum.elim`. -/
 /-- A helper function for what follows. -/
@@ -617,28 +615,23 @@ def join (g f : Fin n → ℚ) : Fin n ⊕ Fin n → ℚ := fun i =>
 
 lemma join_ext (g g' : Fin n → ℚ) (f f' : Fin n → ℚ) :
     join g f = join g' f' ↔ g = g' ∧ f = f' := by
-  apply Iff.intro
-  intro h
-  apply And.intro
-  funext i
-  exact congr_fun h (Sum.inl i)
-  funext i
-  exact congr_fun h (Sum.inr i)
-  intro h
-  rw [h.left, h.right]
+  refine Iff.intro (fun h => ?_) (fun h => ?_)
+  · apply And.intro
+    · funext i
+      exact congr_fun h (Sum.inl i)
+    · funext i
+      exact congr_fun h (Sum.inr i)
+  · rw [h.left, h.right]
 
 lemma join_Pa (g g' : Fin n.succ → ℚ) (f f' : Fin n.succ → ℚ) :
     Pa' (join g f) = Pa' (join g' f') ↔ Pa g f = Pa g' f' := by
-  apply Iff.intro
-  intro h
-  rw [Pa'_eq] at h
-  rw [join_ext] at h
-  rw [h.left, h.right]
-  intro h
-  apply ACCSystemLinear.LinSols.ext
-  rw [Pa'_P'_P!', Pa'_P'_P!']
-  simp [P'_val, P!'_val]
-  exact h
+  refine Iff.intro (fun h => ?_) (fun h => ?_)
+  · rw [Pa'_eq, join_ext] at h
+    rw [h.left, h.right]
+  · apply ACCSystemLinear.LinSols.ext
+    rw [Pa'_P'_P!', Pa'_P'_P!']
+    simp only [succ_eq_add_one, ACCSystemLinear.linSolsAddCommMonoid_add_val, P'_val, P!'_val]
+    exact h
 
 lemma Pa_eq (g g' : Fin n.succ → ℚ) (f f' : Fin n.succ → ℚ) :
     Pa g f = Pa g' f' ↔ g = g' ∧ f = f' := by
diff --git a/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean b/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean
index 38b78a5..6f6e065 100644
--- a/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean
+++ b/HepLean/AnomalyCancellation/PureU1/Odd/Parameterization.lean
@@ -114,8 +114,8 @@ lemma generic_or_special (S : (PureU1 (2 * n.succ + 1)).Sols) :
       accCubeTriLinSymm (P g) (P g) (P! f) = 0 := by
     exact ne_or_eq _ _
   cases h1 <;> rename_i h1
-  exact Or.inl (genericCase_exists S ⟨g, f, h, h1⟩)
-  exact Or.inr (specialCase_exists S ⟨g, f, h, h1⟩)
+  · exact Or.inl (genericCase_exists S ⟨g, f, h, h1⟩)
+  · exact Or.inr (specialCase_exists S ⟨g, f, h, h1⟩)
 
 theorem generic_case {S : (PureU1 (2 * n.succ + 1)).Sols} (h : GenericCase S) :
     ∃ g f a, S = parameterization g f a := by
@@ -127,11 +127,11 @@ theorem generic_case {S : (PureU1 (2 * n.succ + 1)).Sols} (h : GenericCase S) :
   change S.val = _ • (_ • P g + _• P! f)
   rw [anomalyFree_param _ _ hS]
   rw [neg_neg, ← smul_add, smul_smul, inv_mul_cancel, one_smul]
-  exact hS
-  have h := h g f hS
-  rw [anomalyFree_param _ _ hS] at h
-  simp at h
-  exact h
+  · exact hS
+  · have h := h g f hS
+    rw [anomalyFree_param _ _ hS] at h
+    simp at h
+    exact h
 
 lemma special_case_lineInCubic {S : (PureU1 (2 * n.succ + 1)).Sols}
     (h : SpecialCase S) :
diff --git a/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean b/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
index 617ea11..0b7a094 100644
--- a/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
+++ b/HepLean/AnomalyCancellation/SM/NoGrav/One/LinearParameterization.lean
@@ -107,10 +107,10 @@ lemma cubic_zero_E'_zero (S : linearParameters) (hc : accCube (S.asCharges) = 0)
   rw [h1] at hc
   simp at hc
   cases' hc with hc hc
-  have h2 := (add_eq_zero_iff' (by nlinarith) (sq_nonneg S.Y)).mp hc
-  simp at h2
-  exact h2.1
-  exact hc
+  · have h2 := (add_eq_zero_iff' (by nlinarith) (sq_nonneg S.Y)).mp hc
+    simp at h2
+    exact h2.1
+  · exact hc
 
 /-- The bijection between the type of linear parameters and `(SMNoGrav 1).LinSols`. -/
 def bijection : linearParameters ≃ (SMNoGrav 1).LinSols where
@@ -120,13 +120,13 @@ def bijection : linearParameters ≃ (SMNoGrav 1).LinSols where
       SMCharges.E S.val (0 : Fin 1)⟩
   left_inv S := by
     apply linearParameters.ext
-    rfl
-    simp only [Fin.isValue]
-    repeat erw [speciesVal]
-    simp only [asCharges, neg_add_rev]
-    ring
-    simp only [toSpecies_apply]
-    rfl
+    · rfl
+    · simp only [Fin.isValue]
+      repeat erw [speciesVal]
+      simp only [asCharges, neg_add_rev]
+      ring
+    · simp only [toSpecies_apply]
+      rfl
   right_inv S := by
     simp only [Fin.isValue, toSpecies_apply]
     apply ACCSystemLinear.LinSols.ext
@@ -239,25 +239,25 @@ def bijectionLinearParameters :
     have hvw := S.hvw
     have hQ := S.hx
     apply linearParametersQENeqZero.ext
-    rfl
-    field_simp
-    ring
-    simp only [tolinearParametersQNeqZero_w, toLinearParameters_coe_Y, toLinearParameters_coe_Q',
-      toLinearParameters_coe_E']
-    field_simp
-    ring
+    · rfl
+    · field_simp
+      ring
+    · simp only [tolinearParametersQNeqZero_w, toLinearParameters_coe_Y, toLinearParameters_coe_Q',
+        toLinearParameters_coe_E']
+      field_simp
+      ring
   right_inv S := by
     apply Subtype.ext
     have hQ := S.2.1
     have hE := S.2.2
     apply linearParameters.ext
-    rfl
-    field_simp
-    ring_nf
-    field_simp [hQ, hE]
-    field_simp
-    ring_nf
-    field_simp [hQ, hE]
+    · rfl
+    · field_simp
+      ring_nf
+      field_simp [hQ, hE]
+    · field_simp
+      ring_nf
+      field_simp [hQ, hE]
 
 /-- The bijection between `linearParametersQENeqZero` and `LinSols` with `Q` and `E` non-zero. -/
 def bijection : linearParametersQENeqZero ≃
@@ -332,23 +332,21 @@ lemma cube_w_v (S : linearParametersQENeqZero) (h : accCube (bijection S).1.val
     (S.v = -1 ∧ S.w = 0) ∨ (S.v = 0 ∧ S.w = -1) := by
   have h' := cubic_v_or_w_zero S h FLTThree
   cases' h' with hx hx
-  simp [hx]
-  exact cubic_v_zero S h hx
-  simp [hx]
-  exact cube_w_zero S h hx
+  · simp [hx]
+    exact cubic_v_zero S h hx
+  · simp [hx]
+    exact cube_w_zero S h hx
 
 lemma grav (S : linearParametersQENeqZero) : accGrav (bijection S).1.val = 0 ↔ S.v + S.w = -1 := by
   erw [linearParameters.grav]
   have hvw := S.hvw
   have hQ := S.hx
   field_simp
-  apply Iff.intro
-  intro h
-  apply (mul_right_inj' hQ).mp
-  linear_combination -1 * h / 6
-  intro h
-  rw [h]
-  exact Eq.symm (mul_neg_one (6 * S.x))
+  refine Iff.intro (fun h => ?_) (fun h => ?_)
+  · apply (mul_right_inj' hQ).mp
+    linear_combination -1 * h / 6
+  · rw [h]
+    exact Eq.symm (mul_neg_one (6 * S.x))
 
 lemma grav_of_cubic (S : linearParametersQENeqZero) (h : accCube (bijection S).1.val = 0)
     (FLTThree : FermatLastTheoremWith ℚ 3) :
@@ -356,10 +354,10 @@ lemma grav_of_cubic (S : linearParametersQENeqZero) (h : accCube (bijection S).1
   rw [grav]
   have h' := cube_w_v S h FLTThree
   cases' h' with h h
-  rw [h.1, h.2]
-  exact Rat.add_zero (-1)
-  rw [h.1, h.2]
-  exact Rat.zero_add (-1)
+  · rw [h.1, h.2]
+    exact Rat.add_zero (-1)
+  · rw [h.1, h.2]
+    exact Rat.zero_add (-1)
 
 end linearParametersQENeqZero
 
diff --git a/HepLean/SpaceTime/LorentzTensor/IndexNotation/WithUniqueDual.lean b/HepLean/SpaceTime/LorentzTensor/IndexNotation/WithUniqueDual.lean
index be0c053..257e449 100644
--- a/HepLean/SpaceTime/LorentzTensor/IndexNotation/WithUniqueDual.lean
+++ b/HepLean/SpaceTime/LorentzTensor/IndexNotation/WithUniqueDual.lean
@@ -115,9 +115,7 @@ lemma all_dual_eq_getDual?_of_mem_withUniqueDual (i : Fin l.length) (h : i ∈ l
 
 lemma some_eq_getDual?_of_withUniqueDual_iff (i j : Fin l.length) (h : i ∈ l.withUniqueDual) :
     l.AreDualInSelf i j ↔ some j = l.getDual? i := by
-  apply Iff.intro
-  exact fun h' => all_dual_eq_getDual?_of_mem_withUniqueDual l i h j h'
-  intro h'
+  refine Iff.intro (fun h' => all_dual_eq_getDual?_of_mem_withUniqueDual l i h j h') (fun h' => ?_)
   have hj : j = (l.getDual? i).get (mem_withUniqueDual_isSome l i h) :=
     Eq.symm (Option.get_of_mem (mem_withUniqueDual_isSome l i h) (id (Eq.symm h')))
   subst hj
@@ -128,8 +126,8 @@ lemma eq_getDual?_get_of_withUniqueDual_iff (i j : Fin l.length) (h : i ∈ l.wi
     l.AreDualInSelf i j ↔ j = (l.getDual? i).get (mem_withUniqueDual_isSome l i h) := by
   rw [l.some_eq_getDual?_of_withUniqueDual_iff i j h]
   refine Iff.intro (fun h' => ?_) (fun h' => ?_)
-  exact Eq.symm (Option.get_of_mem (mem_withUniqueDual_isSome l i h) (id (Eq.symm h')))
-  simp [h']
+  · exact Eq.symm (Option.get_of_mem (mem_withUniqueDual_isSome l i h) (id (Eq.symm h')))
+  · simp [h']
 
 lemma eq_of_areDualInSelf_withUniqueDual {j k : Fin l.length} (i : l.withUniqueDual)
     (hj : l.AreDualInSelf i j) (hk : l.AreDualInSelf i k) : j = k := by
@@ -198,9 +196,7 @@ lemma all_dual_eq_of_withUniqueDualInOther (i : Fin l.length)
 lemma some_eq_getDualInOther?_of_withUniqueDualInOther_iff (i : Fin l.length) (j : Fin l2.length)
     (h : i ∈ l.withUniqueDualInOther l2) :
     l.AreDualInOther l2 i j ↔ some j = l.getDualInOther? l2 i := by
-  apply Iff.intro
-  exact fun h' => l.all_dual_eq_of_withUniqueDualInOther l2 i h j h'
-  intro h'
+  refine Iff.intro (fun h' => l.all_dual_eq_of_withUniqueDualInOther l2 i h j h') (fun h' => ?_)
   have hj : j = (l.getDualInOther? l2 i).get (mem_withUniqueDualInOther_isSome l l2 i h) :=
     Eq.symm (Option.get_of_mem (mem_withUniqueDualInOther_isSome l l2 i h) (id (Eq.symm h')))
   subst hj
@@ -213,8 +209,8 @@ lemma eq_getDualInOther?_get_of_withUniqueDualInOther_iff (i : Fin l.length) (j
       (mem_withUniqueDualInOther_isSome l l2 i h) := by
   rw [l.some_eq_getDualInOther?_of_withUniqueDualInOther_iff l2 i j h]
   refine Iff.intro (fun h' => ?_) (fun h' => ?_)
-  exact Eq.symm (Option.get_of_mem (mem_withUniqueDualInOther_isSome l l2 i h) (id (Eq.symm h')))
-  simp [h']
+  · exact (Option.get_of_mem (mem_withUniqueDualInOther_isSome l l2 i h) (id (Eq.symm h'))).symm
+  · simp [h']
 
 @[simp, nolint simpNF]
 lemma getDualInOther?_get_getDualInOther?_get_of_withUniqueDualInOther
@@ -284,8 +280,7 @@ lemma getDualInOther?_get_of_mem_withUniqueInOther_mem (i : Fin l.length)
   simp only [withUniqueDualInOther, mem_withDual_iff_isSome, Bool.not_eq_true, Option.not_isSome,
     Option.isNone_iff_eq_none, mem_withInDualOther_iff_isSome, Finset.mem_filter, Finset.mem_univ,
     getDualInOther?_getDualInOther?_get_isSome, true_and]
-  apply And.intro
-  exact getDual?_of_getDualInOther?_of_mem_withUniqueInOther_eq_none l l2 i h
+  apply And.intro (getDual?_of_getDualInOther?_of_mem_withUniqueInOther_eq_none l l2 i h)
   intro j hj
   simp only [h, getDualInOther?_getDualInOther?_get_of_withUniqueDualInOther, Option.some.injEq]
   by_contra hn