mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Transvection.Basic

Goal state before:
pp: K : Type u_3
V : Type u_4
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : Dual K V
v : V
⊢ LinearMap.det (transvection f v) = 1 + f v

Tactic:
by
  classical
  by_cases hfv : f v = 0
  · by_cases hv : v = 0
    · simp [hv]
    by_cases hf : f = 0
    · simp [hf]
    obtain ⟨ι, b, i, j, hi, hj⟩ := exists_basis_of_pairing_eq_zero hfv hf hv
    have : Fintype ι := FiniteDimensional.fintypeBasisIndex b
    rw [← det_toMatrix b]
    suffices toMatrix b b (LinearMap.transvection f v) = Matrix.transvection i j 1 by
      rw [this, Matrix.det_transvection_of_ne i j hi 1, hfv, add_zero]
    ext x y
    rw [toMatrix_apply, transvection.apply, Matrix.transvection]
    simp only [hj.2, Basis.coord_apply, Basis.repr_self, hj.1, map_add, map_smul,
      Finsupp.smul_single, smul_eq_mul, mul_one, Finsupp.coe_add, Pi.add_apply, Matrix.add_apply]
    apply congr_arg₂
    · by_cases h : x = y
      · rw [h]; simp
      · rw [Finsupp.single_eq_of_ne h, Matrix.one_apply_ne h]
    · by_cases h : i = x ∧ j = y
      · rw [h.1, h.2]; simp
      · rcases not_and_or.mp h with h' | h' <;>
          simp [Finsupp.single_eq_of_ne' h',
            Finsupp.single_eq_of_ne h',
            Matrix.single_apply_of_ne (h := h)]
  · obtain ⟨ι, b, i, hv, hf⟩ := exists_basis_of_pairing_ne_zero hfv
    have : Fintype ι := FiniteDimensional.fintypeBasisIndex b
    rw [← det_toMatrix b]
    suffices toMatrix b b (transvection f v) =
      Matrix.diagonal (Function.update 1 i (1 + f v)) by
      rw [this]
      simp only [Matrix.det_diagonal]
      rw [Finset.prod_eq_single i]
      · simp
      · intro j _ hj
        simp [Function.update_of_ne hj]
      · simp
    ext x y
    rw [toMatrix_apply, transvection.apply, Matrix.diagonal]
    simp only [map_add, Basis.repr_self, map_smul, Finsupp.coe_add, Finsupp.coe_smul,
      Pi.add_apply, Pi.smul_apply, smul_eq_mul, Matrix.of_apply]
    rw [hv, Function.update_apply, Basis.repr_self, Pi.one_apply, hf]
    simp only [smul_apply, Basis.coord_apply, Basis.repr_self, smul_eq_mul,
      Finsupp.single_eq_same, mul_one]
    split_ifs with hxy hxi
    · simp [← hxy, hxi]
    · rw [Finsupp.single_eq_of_ne hxi]; simp [hxy]
    · rw [Finsupp.single_eq_of_ne hxy, zero_add, mul_assoc]
      convert! mul_zero _
      by_cases hxi : x = i
      · simp [← hxi, Finsupp.single_eq_of_ne hxy]
      · simp [Finsupp.single_eq_of_ne hxi]

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m₁✝ m₂✝ : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
⊢ (v Q) m₁ * (v Q) m₂ + r₁ • e0 Q * (v Q) m₂ + (v Q) m₁ * r₂ • e0 Q + r₁ • e0 Q * r₂ • e0 Q =
    (v Q) m₁ * (v Q) m₂ + r₁ • e0 Q * (v Q) m₂ + ((v Q) m₁ * r₂ • e0 Q + r₁ • e0 Q * r₂ • e0 Q)

Tactic:
add_assoc

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m₁✝ m₂✝ : M × R
m₁ : M
r₁ : R
m₂ : M
r₂ : R
⊢ (v Q) m₁ * (v Q) m₂ + r₁ • e0 Q * (v Q) m₂ + ((v Q) m₁ * r₂ • e0 Q + r₁ • e0 Q * r₂ • e0 Q) =
    (v Q) m₁ * (v Q) m₂ + r₁ • e0 Q * (v Q) m₂ + ((v Q) m₁ * r₂ • e0 Q + r₁ • e0 Q * r₂ • e0 Q)
Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

Goal state before:
pp: case mul
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
x : (CliffordAlgebra Q)ˣ
inst✝ : Invertible 2
y z : (CliffordAlgebra Q)ˣ
hx✝ : y ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy✝ : z ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy : ∀ (m : M), ↑y * (ι Q) m * ↑y⁻¹ ∈ (ι Q).range
hz : ∀ (m : M), ↑z * (ι Q) m * ↑z⁻¹ ∈ (ι Q).range
m : M
⊢ ↑(y * z) * (ι Q) m * ↑(y * z)⁻¹ ∈ (ι Q).range

Tactic:
| mul y z _ _ hy hz =>

Goal state after:
Module: Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup

Goal state before:
pp: case mul
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
Q : QuadraticForm R M
inst✝ : Invertible 2
x y z : (CliffordAlgebra Q)ˣ
hx✝ : y ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy✝ : z ∈ Subgroup.closure (Units.val ⁻¹' Set.range ⇑(ι Q))
hy : ∀ (b : M), involute ↑y * (ι Q) b * ↑y⁻¹ ∈ (ι Q).range
hz : ∀ (b : M), involute ↑z * (ι Q) b * ↑z⁻¹ ∈ (ι Q).range
b : M
⊢ involute ↑(y * z) * (ι Q) b * ↑(y * z)⁻¹ ∈ (ι Q).range

Tactic:
| mul y z _ _ hy hz =>

Goal state after:
Module: Mathlib.LinearAlgebra.Goursat

Goal state before:
pp: case h.mpr
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
L : Submodule R (M × N)
M' : Submodule R M := ⋯
N' : Submodule R N := ⋯
P : ↥L →ₗ[R] ↥M' := ⋯
Q : ↥L →ₗ[R] ↥N' := ⋯
L' : Submodule R (↥M' × ↥N') := ⋯
hL₁' : Surjective (Prod.fst ∘ ⇑L'.subtype)
hL₂' : Surjective (Prod.snd ∘ ⇑L'.subtype)
e : (↥M' ⧸ L'.goursatFst) ≃ₗ[R] ↥N' ⧸ L'.goursatSnd
he : (L'.goursatFst.mkQ.prodMap L'.goursatSnd.mkQ ∘ₗ L'.subtype).range = (↑e).graph
m : M
n : N
⊢ (m, n) ∈
      map ((map (LinearMap.fst R M N) L).subtype.prodMap (map (LinearMap.snd R M N) L).subtype)
        (((LinearMap.fst R M N).submoduleMap L).prod ((LinearMap.snd R M N).submoduleMap L)).range →
    (m, n) ∈ L

Tactic:
simp only [mem_map, LinearMap.mem_range, LinearMap.prod_apply, Function.prod_apply,
      Subtype.exists, Prod.exists, LinearMap.prodMap_apply, subtype_apply, Prod.mk.injEq,
      snd_apply, fst_apply, Subtype.ext_iff, submoduleMap_coe_apply]
      grind

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Circulant

Goal state before:
pp: α : Type u_1
n : Type u_3
inst✝ : SubtractionMonoid n
v w : n → α
h : circulant v = circulant w
⊢ v = w

Tactic:
ext k

Goal state after:
α : Type u_1
n : Type u_3
inst✝ : SubtractionMonoid n
v w : n → α
h : circulant v = circulant w
k : n
⊢ v k = w k
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Pivot

Goal state before:
pp: case top
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : LT m
inst✝ : LT n
i : m
hA : A.IsPivotedBy l
hc : l i = ⊤
⊢ ⊤ = ⊤ ↔ A i = 0

Tactic:
| top =>

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Determinant.Misc

Goal state before:
pp: case pos
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin n) R
hv : ∑ j, M j = 0
j₁ j₂ : Fin (n + 1)
i : Fin n
h_ind : (M.submatrix i.castSucc.succAbove id).det = (↑↑i.castSucc).negOnePow • (M.submatrix (Fin.succAbove 0) id).det
a b : Fin n
h : a = i
⊢ -∑ x, M (i.succ.succAbove x) b = M (i.castSucc.succAbove a) b

Tactic:
replace hv := congr_fun hv b
        rw [Fin.sum_univ_succAbove _ i.succ, Pi.add_apply, Finset.sum_apply] at hv
        rwa [h, Fin.succAbove_castSucc_self, neg_eq_iff_add_eq_zero, add_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Pivot

Goal state before:
pp: case top
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : LinearOrder n
inst✝ : LT m
l' : m → WithTop n
hl : A.IsPivotedBy l
hl' : A.IsPivotedBy l'
i : m
hc' : l' i = ⊤
⊢ l i = ⊤

Tactic:
| top =>

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Pivot

Goal state before:
pp: case coe.top
m : Type u_1
n : Type u_2
R : Type u_3
inst✝² : Zero R
A : Matrix m n R
l : m → WithTop n
inst✝¹ : LinearOrder n
inst✝ : LT m
l' : m → WithTop n
hl : A.IsPivotedBy l
hl' : A.IsPivotedBy l'
i : m
c' : n
hc' : l' i = ↑c'
hc : l i = ⊤
⊢ ⊤ = ↑c'

Tactic:
| top =>

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Integer

Goal state before:
pp: m : Type u_1
n : Type u_2
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n ℚ
x✝ : ℕ
⊢ Aᵀ.den ∣ x✝ ↔ A.den ∣ x✝

Tactic:
simpa [den_dvd_iff] using forall_comm

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.FixedDetMatrices

Goal state before:
pp: case neg
m : ℤ
hm : m ≠ 0
A : FixedDetMatrix (Fin 2) ℤ m
h : ↑A 1 0 = 0
hd : ↑A 1 1 ≠ 0
h1 : ¬0 < ↑A 0 0
⊢ reduce A ∈ reps m

Tactic:
simp only [reps, Fin.isValue, reduce_of_not_pos h h1, Int.ediv_neg, neg_neg, smul_def, ←
        mul_assoc, S_mul_S_eq, neg_mul, one_mul, coe_T_zpow, mul_neg, cons_mul, Nat.succ_eq_add_one,
        Nat.reduceAdd, empty_mul, Equiv.symm_apply_apply, neg_of, neg_cons, neg_empty,
        Set.mem_ofPred_eq, of_apply, cons_val', Pi.neg_apply, vecMul, cons_dotProduct, vecHead,
        vecTail, Function.comp_apply, Fin.succ_zero_eq_one, h, mul_zero, dotProduct_of_isEmpty,
        add_zero, zero_mul, neg_zero, empty_val', cons_val_fin_one, cons_val_one, cons_val_zero,
        lt_neg, neg_add_rev, zero_add, le_add_neg_iff_add_le, ← le_neg, abs_neg, true_and]
      refine ⟨?_, Int.ediv_mul_le _ hd, ?_⟩
      · simp only [Int.lt_iff_le_and_ne]
        exact ⟨not_lt.mp h1, A_a_ne_zero h hm⟩
      · rw [mul_comm, add_comm, ← Int.sub_eq_add_neg, ← Int.emod_def,
         abs_eq_self.mpr <| Int.emod_nonneg _ hd]
        exact Int.emod_lt_abs _ hd

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Swap

Goal state before:
pp: R : Type u_1
n : Type u_2
inst✝² : Zero R
inst✝¹ : One R
inst✝ : DecidableEq n
i j : n
⊢ swap R i j = swap R j i

Tactic:
by
  simp only [swap, Equiv.swap_comm]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.WithConv

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝² : Semiring α
inst✝¹ : IsLeftCancelMulZero α
inst✝ : StarRing α
f : WithConv (Matrix m n α)
hf : IsIdempotentElem f
⊢ IsSelfAdjoint f

Tactic:
IsIdempotentElem,

Goal state after:
m : Type u_1
n : Type u_2
α : Type u_3
inst✝² : Semiring α
inst✝¹ : IsLeftCancelMulZero α
inst✝ : StarRing α
f : WithConv (Matrix m n α)
hf : f * f = f
⊢ IsSelfAdjoint f
Module: Mathlib.LinearAlgebra.Projectivization.Cardinality

Goal state before:
pp: case inl.inl
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
a✝ : Nontrivial V
h✝ : Finite k
h : Finite V
this : Fintype V
⊢ Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1)

Tactic:
have : Fintype (ℙ k V) := Fintype.ofFinite (ℙ k V)

Goal state after:
case inl.inl
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
a✝ : Nontrivial V
h✝ : Finite k
h : Finite V
this✝ : Fintype V
this : Fintype (ℙ k V)
⊢ Nat.card V - 1 = Nat.card (ℙ k V) * (Nat.card k - 1)
Module: Mathlib.LinearAlgebra.Projectivization.Independence

Goal state before:
pp: case refine_1
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh : LinearIndependent K ff
⊢ LinearIndependent K (Projectivization.rep ∘ fun i ↦ mk K (ff i) ⋯)

Tactic:
choose a ha using fun i : ι => exists_smul_eq_mk_rep K (ff i) (hff i)

Goal state after:
case refine_1
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh : LinearIndependent K ff
a : ι → Kˣ
ha : ∀ (i : ι), a i • ff i = (mk K (ff i) ⋯).rep
⊢ LinearIndependent K (Projectivization.rep ∘ fun i ↦ mk K (ff i) ⋯)
Module: Mathlib.LinearAlgebra.Projectivization.Independence

Goal state before:
pp: case refine_1
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh1 : LinearIndependent K (Projectivization.rep ∘ fun i ↦ mk K (ff i) ⋯)
⊢ LinearIndependent K ff

Tactic:
choose a ha using fun i : ι => exists_smul_eq_mk_rep K (ff i) (hff i)

Goal state after:
case refine_1
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh1 : LinearIndependent K (Projectivization.rep ∘ fun i ↦ mk K (ff i) ⋯)
a : ι → Kˣ
ha : ∀ (i : ι), a i • ff i = (mk K (ff i) ⋯).rep
⊢ LinearIndependent K ff
Module: Mathlib.LinearAlgebra.Projectivization.Independence

Goal state before:
pp: K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : V
hu : u ≠ 0
hv : v ≠ 0
⊢ Independent ![mk K u hu, mk K v hv] ↔ LinearIndependent K ![u, v]

Tactic:
rw [independent_pair_iff_ne, ne_eq, mk_eq_mk_iff' K u v hu hv, linearIndependent_fin2]

Goal state after:
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : V
hu : u ≠ 0
hv : v ≠ 0
⊢ (¬∃ a, a • v = u) ↔ ![u, v] 1 ≠ 0 ∧ ∀ (a : K), a • ![u, v] 1 ≠ ![u, v] 0
Module: Mathlib.LinearAlgebra.QuadraticForm.AlgClosed

Goal state before:
pp: ι : Type u_1
inst✝³ : Fintype ι
K : Type u_2
inst✝² : Field K
inst✝¹ : IsAlgClosed K
inst✝ : DecidableEq K
w : ι → K
i : ι
⊢ (if w i = 0 then 0 else 1) * ↑(if h : w i = 0 then 1 else Units.mk0 ⋯.choose ⋯) ^ 2 = w i

Tactic:
split_ifs with h <;>
    simp [h, pow_two, ← (IsAlgClosed.exists_eq_mul_self (w i : K)).choose_spec]

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: case refine_2.h
K : Type u_1
inst✝² : Field K
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
m : Matrix.SpecialLinearGroup ι K
x✝ : ∃ r, r ^ Fintype.card ι = 1 ∧ (Matrix.scalar ι) r = ↑m
r : K
hr1 : r ^ Fintype.card ι = 1
hr2 : (Matrix.scalar ι) r = ↑m
v : ι → K
hv : v ≠ 0
⊢ m • mk K v hv = mk K v hv

Tactic:
simp only [smul_mk, mk_eq_mk_iff']
    use r
    change _ = m.1 • v
    simp [← hr2]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : Invertible 2
X : QuadraticModuleCat R
⊢ ModuleCat.ofHom (Hom.toIsometry (λ_ X).hom).toLinearMap =
    𝟙 ((𝟙_ (QuadraticModuleCat R)).toModuleCat ⊗ X.toModuleCat) ≫
      𝟙 (𝟙_ (ModuleCat R)) ▷ X.toModuleCat ≫ (λ_ X.toModuleCat).hom

Tactic:
MonoidalCategory.id_whiskerRight

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : Invertible 2
X : QuadraticModuleCat R
⊢ ModuleCat.ofHom (Hom.toIsometry (λ_ X).hom).toLinearMap =
    𝟙 ((𝟙_ (QuadraticModuleCat R)).toModuleCat ⊗ X.toModuleCat) ≫
      𝟙 ((𝟙_ (QuadraticModuleCat R)).toModuleCat ⊗ X.toModuleCat) ≫ (λ_ X.toModuleCat).hom
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : Module R M
Q : QuadraticForm R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
⊢ sigPos Q ∈ upperBounds {r | ∃ V, Module.finrank R ↥V = r ∧ (QuadraticMap.restrict Q V).PosDef}

Tactic:
rintro _ ⟨V, rfl, hV⟩

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : Module R M
Q : QuadraticForm R M
inst✝¹ : Module.Finite R M
inst✝ : StrongRankCondition R
V : Submodule R M
hV : (QuadraticMap.restrict Q V).PosDef
⊢ Module.finrank R ↥V ≤ sigPos Q
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
i j : ι
inst✝ : P.IsNotG2
⊢ chainBotCoeff i j + chainTopCoeff i j ≤ 2

Tactic:
by_cases h : LinearIndependent R ![P.root i, P.root j]

Goal state after:
case pos
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
i j : ι
inst✝ : P.IsNotG2
h : LinearIndependent R ![P.root i, P.root j]
⊢ chainBotCoeff i j + chainTopCoeff i j ≤ 2

case neg
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : CharZero R
inst✝¹ : IsDomain R
i j : ι
inst✝ : P.IsNotG2
h : ¬LinearIndependent R ![P.root i, P.root j]
⊢ chainBotCoeff i j + chainTopCoeff i j ≤ 2
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: case inl.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Finite ι
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : CharZero R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : Fintype ι
i : ↥b.support
inst✝ : P.IsReduced
k : ι
hki : k ≠ ↑i
hki' : k ≠ (P.reflectionPerm ↑i) ↑i
h_lin_ind : LinearIndependent R ![P.root ↑i, P.root k]
x : ι
hx : P.root k = P.root ↑i + P.root x
h₂ : ∀ (a : ι), ¬P.root k = P.root a - P.root ↑i
⊢ (∑ x, if P.root k = P.root ↑i + P.root x then (↑(chainBotCoeff (↑i) x) + 1) * (↑(chainTopCoeff (↑i) k) + 1) else 0) -
      ∑ x, 0 =
    ↑(chainBotCoeff (↑i) k) - ↑(chainTopCoeff (↑i) k)

Tactic:
Finset.sum_const_zero,

Goal state after:
case inl.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Finite ι
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : CharZero R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : Fintype ι
i : ↥b.support
inst✝ : P.IsReduced
k : ι
hki : k ≠ ↑i
hki' : k ≠ (P.reflectionPerm ↑i) ↑i
h_lin_ind : LinearIndependent R ![P.root ↑i, P.root k]
x : ι
hx : P.root k = P.root ↑i + P.root x
h₂ : ∀ (a : ι), ¬P.root k = P.root a - P.root ↑i
⊢ (∑ x, if P.root k = P.root ↑i + P.root x then (↑(chainBotCoeff (↑i) x) + 1) * (↑(chainTopCoeff (↑i) k) + 1) else 0) -
      0 =
    ↑(chainBotCoeff (↑i) k) - ↑(chainTopCoeff (↑i) k)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: case inr.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Finite ι
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : CharZero R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : Fintype ι
i : ↥b.support
inst✝ : P.IsReduced
k : ι
hki : k ≠ ↑i
hki' : k ≠ (P.reflectionPerm ↑i) ↑i
h_lin_ind : LinearIndependent R ![P.root ↑i, P.root k]
h₁ : ∀ (a : ι), ¬P.root k = P.root ↑i + P.root a
y : ι
hy : P.root k = P.root y - P.root ↑i
⊢ (∑ x, 0 -
      ∑ x,
        if P.root k = P.root x - P.root ↑i then (↑(chainTopCoeff (↑i) x) + 1) * (↑(chainBotCoeff (↑i) k) + 1) else 0) =
    ↑(chainBotCoeff (↑i) k) - ↑(chainTopCoeff (↑i) k)

Tactic:
Finset.sum_const_zero,

Goal state after:
case inr.inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : Finite ι
inst✝⁹ : CommRing R
inst✝⁸ : IsDomain R
inst✝⁷ : CharZero R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
P : RootPairing ι R M N
inst✝² : P.IsCrystallographic
b : P.Base
inst✝¹ : Fintype ι
i : ↥b.support
inst✝ : P.IsReduced
k : ι
hki : k ≠ ↑i
hki' : k ≠ (P.reflectionPerm ↑i) ↑i
h_lin_ind : LinearIndependent R ![P.root ↑i, P.root k]
h₁ : ∀ (a : ι), ¬P.root k = P.root ↑i + P.root a
y : ι
hy : P.root k = P.root y - P.root ↑i
⊢ (0 -
      ∑ x,
        if P.root k = P.root x - P.root ↑i then (↑(chainTopCoeff (↑i) x) + 1) * (↑(chainBotCoeff (↑i) k) + 1) else 0) =
    ↑(chainBotCoeff (↑i) k) - ↑(chainTopCoeff (↑i) k)
Module: Mathlib.LinearAlgebra.RootSystem.Finite.G2

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
h₁ : ¬P.root i = longRoot P
h₂ : ¬P.root i = -longRoot P
h₃ : ¬P.root i = shortRoot P
h₄ : ¬P.root i = -shortRoot P
h₅ : ¬P.root i = shortAddLongRoot P
h₆ : ¬P.root i = -shortAddLongRoot P
h₇ : ¬P.root i = twoShortAddLongRoot P
h₈ : ¬P.root i = -twoShortAddLongRoot P
h₉ : ¬P.root i = threeShortAddLongRoot P
h₁₀ : ¬P.root i = -threeShortAddLongRoot P
h₁₁ : ¬P.root i = threeShortAddTwoLongRoot P
h₁₂ : ¬P.root i = -threeShortAddTwoLongRoot P
ha :
  (P.pairingIn ℤ i (short P), P.pairingIn ℤ (short P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
⊢ P.pairingIn ℤ i (short P) = 0 ∧ P.pairingIn ℤ i (long P) = 0

Tactic:
have hb := P.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed' i (long P) ‹_› ‹_›

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : P.EmbeddedG2
inst✝² : Finite ι
inst✝¹ : CharZero R
inst✝ : IsDomain R
i : ι
h₁ : ¬P.root i = longRoot P
h₂ : ¬P.root i = -longRoot P
h₃ : ¬P.root i = shortRoot P
h₄ : ¬P.root i = -shortRoot P
h₅ : ¬P.root i = shortAddLongRoot P
h₆ : ¬P.root i = -shortAddLongRoot P
h₇ : ¬P.root i = twoShortAddLongRoot P
h₈ : ¬P.root i = -twoShortAddLongRoot P
h₉ : ¬P.root i = threeShortAddLongRoot P
h₁₀ : ¬P.root i = -threeShortAddLongRoot P
h₁₁ : ¬P.root i = threeShortAddTwoLongRoot P
h₁₂ : ¬P.root i = -threeShortAddTwoLongRoot P
ha :
  (P.pairingIn ℤ i (short P), P.pairingIn ℤ (short P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
hb :
  (P.pairingIn ℤ i (long P), P.pairingIn ℤ (long P) i) ∈
    {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)}
⊢ P.pairingIn ℤ i (short P) = 0 ∧ P.pairingIn ℤ i (long P) = 0
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: case inl
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : DecidableEq ι
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module K M
inst✝³ : AddCommGroup N
inst✝² : Module K N
P : RootPairing ι K M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
hw₀ : w ≠ 0
aux :
  ∀ (d : ↥b.support ⊕ ι → K) (x : ↥H),
    ↑↑x = diagonal d → (w ∈ genWeightSpaceOf (↥b.support ⊕ ι → K) (χ x) x ↔ ∃ k, diagonal ((d - χ x • 1) ^ k) *ᵥ w = 0)
i : ι
hi : w (Sum.inr i) ≠ 0
d : ι → K
hd₀ : ∀ (i : ι), d i ≠ 0
hd₁ : Pairwise ((fun x1 x2 ↦ x1 ≠ x2) on d)
hd₂ : diagonal (0 ⊕ᵥ d) ∈ cartanSubalgebra b
x : ↥H := ⟨⟨diagonal (0 ⊕ᵥ d), ⋯⟩, hd₂⟩
k : ℕ
hk : diagonal ((0 ⊕ᵥ d - χ x • 1) ^ k) *ᵥ w = 0
hχx : d i = χ x
hk₀ : k ≠ 0
j : ↥b.support
this : χ x ≠ 0
⊢ ((w (Sum.inr i))⁻¹ • w) (Sum.inl j) = v b i (Sum.inl j)

Tactic:
simpa [hi, mulVec_eq_sum, diagonal_apply, hk₀, this] using! congr_fun hk (Sum.inl j)

Goal state after:
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: case inr
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : DecidableEq ι
inst✝⁶ : Fintype ι
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module K M
inst✝³ : AddCommGroup N
inst✝² : Module K N
P : RootPairing ι K M N
inst✝¹ : P.IsRootSystem
inst✝ : P.IsCrystallographic
b : P.Base
χ : ↥H → K
hχ : χ ≠ 0
w : ↥b.support ⊕ ι → K
hw₀ : w ≠ 0
aux :
  ∀ (d : ↥b.support ⊕ ι → K) (x : ↥H),
    ↑↑x = diagonal d → (w ∈ genWeightSpaceOf (↥b.support ⊕ ι → K) (χ x) x ↔ ∃ k, diagonal ((d - χ x • 1) ^ k) *ᵥ w = 0)
i : ι
hi : w (Sum.inr i) ≠ 0
d : ι → K
hd₀ : ∀ (i : ι), d i ≠ 0
hd₁ : Pairwise ((fun x1 x2 ↦ x1 ≠ x2) on d)
hd₂ : diagonal (0 ⊕ᵥ d) ∈ cartanSubalgebra b
x : ↥H := ⟨⟨diagonal (0 ⊕ᵥ d), ⋯⟩, hd₂⟩
k : ℕ
hk : diagonal ((0 ⊕ᵥ d - χ x • 1) ^ k) *ᵥ w = 0
hχx : d i = χ x
hk₀ : k ≠ 0
j : ι
⊢ ((w (Sum.inr i))⁻¹ • w) (Sum.inr j) = v b i (Sum.inr j)

Tactic:
rcases eq_or_ne i j with rfl | hij
      · simp [hi]
      · suffices d j ≠ χ x by
          simpa [mulVec_eq_sum, diagonal_apply, sub_eq_zero, this, hij, hi] using!
            congr_fun hk (Sum.inr j)
        rw [← hχx]
        exact hd₁ <| by simp [hij.symm]

Goal state after: