mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: case zero.refine_2
n : Type u_1
R : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : LinearOrder R
A : Matrix n n R
inst✝⁴ : Fintype n
inst✝³ : IsOrderedRing R
inst✝² : PosMulStrictMono R
inst✝¹ : Nontrivial R
inst✝ : DecidableEq n
hA : ∀ (i j : n), 0 ≤ A i j
this : Quiver n := A.toQuiver
i j : n
x✝ : Nonempty { p // p.length = 0 }
p : Path i j
hp : p.length = 0
⊢ 0 < (A ^ 0) i j

Tactic:
simp [Quiver.Path.eq_of_length_zero p hp]

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

Goal state before:
pp: case pred
m✝ : ℤ
C : FixedDetMatrix (Fin 2) ℤ m✝ → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m✝), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m✝), C B → C (T • B)
B : FixedDetMatrix (Fin 2) ℤ m✝
m : ℕ
hm : C (T ^ (-↑m) • B) ↔ C B
⊢ C (T • T⁻¹ • T ^ (-↑m) • B) ↔ C B

Tactic:
smul_inv_smul

Goal state after:
case pred
m✝ : ℤ
C : FixedDetMatrix (Fin 2) ℤ m✝ → Prop
hS : ∀ (B : FixedDetMatrix (Fin 2) ℤ m✝), C B → C (S • B)
hT : ∀ (B : FixedDetMatrix (Fin 2) ℤ m✝), C B → C (T • B)
B : FixedDetMatrix (Fin 2) ℤ m✝
m : ℕ
hm : C (T ^ (-↑m) • B) ↔ C B
⊢ C (T ^ (-↑m) • B) ↔ C B
Module: Mathlib.LinearAlgebra.Matrix.HadamardMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring R
inst✝ : StarRing R
A : Matrix m m R
B : Matrix n n R
hA : A.IsHadamard
hB : B.IsHadamard
⊢ (kroneckerMap (fun x1 x2 ↦ x1 * x2) A B).IsHadamard

Tactic:
by
  refine ⟨fun _ _ ↦ mul_mem (hA.apply_mem _ _) (hB.apply_mem _ _), ?_, ?_⟩ <;> ext ⟨i, i'⟩ ⟨j, j'⟩
  · calc
      _ = ∑ x₁, ∑ x₂, A i x₁ * (B i' x₂ * Bᴴ x₂ j') * Aᴴ x₁ j := by
        simp [conjTranspose_kronecker', mul_apply, mul_assoc, ← Finset.sum_product']
      _ = if i' = j' then ∑ x, A i x * (Fintype.card n • Aᴴ) x j else 0 := by
        simp [← Finset.sum_mul, ← Finset.mul_sum, ← mul_apply, hB.mul_conjTranspose,
          one_apply, mul_assoc _ (Fintype.card n : R), -conjTranspose_apply]
      _ = _ := by
        simp only [← mul_apply, mul_smul_comm, hA.mul_conjTranspose]
        simp [one_apply, ← Nat.cast_mul, mul_comm, ← ite_and, and_comm]
  · calc
      _ = ∑ x₁, ∑ x₂, Bᴴ i' x₂ * (Aᴴ i x₁ * A x₁ j) * B x₂ j' := by
        simp [conjTranspose_kronecker', mul_apply, mul_assoc, ← Finset.sum_product']
      _ = if i = j then ∑ x, Bᴴ i' x * (Fintype.card m • B) x j' else 0 := by
        rw [Finset.sum_comm]
        simp [← Finset.sum_mul, ← Finset.mul_sum, ← mul_apply, hA.conjTranspose_mul,
          one_apply, mul_assoc _ (Fintype.card m : R), -conjTranspose_apply]
      _ = _ := by
        simp only [← mul_apply, mul_smul_comm, hB.conjTranspose_mul]
        simp [one_apply, ← Nat.cast_mul, ← ite_and]

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

Goal state before:
pp: R : Type u_1
n : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n R
ind : LinearIndependent R A.col
a b : R
bal : A.IsDetpBalanced a b
P : ℕ → Prop := fun r ↦ ∀ (f g : Fin r → n), (A.submatrix f g).IsDetpBalanced a b
r : ℕ
x✝¹ : r < Fintype.card n
x✝ : 0 ≤ r
ih : P (r + 1)
f g : Fin r → n
hg : ¬Function.Surjective g
j₀ : n
h₀ : ∀ (x : Fin r), ¬g x = j₀
D : Matrix (Fin r) (Fin r) R := A.submatrix f g
Aj : Fin r → Matrix (Fin r) (Fin r) R := fun j ↦ A.submatrix f (Function.update g j j₀)
v : R → R → n →₀ R :=
  fun a b ↦
    ∑ j, Finsupp.single (g j) (a * detp (-1) (Aj j) + b * detp 1 (Aj j)) +
      Finsupp.single j₀ (a * detp 1 D + b * detp (-1) D)
h : v a b = v b a
⊢ (A.submatrix f g).IsDetpBalanced a b

Tactic:
by simpa [IsDetpBalanced, v, h₀] using congr($h j₀)

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.PSL.PSL2

Goal state before:
pp: F : Type u_2
inst✝ : Field F
⊢ iSup iwasawaT = Subgroup.map (QuotientGroup.mk' (Subgroup.center SL(2, F))) (⨆ p, lineStab p.submodule)

Tactic:
Subgroup.map_iSup

Goal state after:
F : Type u_2
inst✝ : Field F
⊢ iSup iwasawaT = ⨆ i, Subgroup.map (QuotientGroup.mk' (Subgroup.center SL(2, F))) (lineStab i.submodule)
Module: Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
L : Submodule F (ι → F)
A : SpecialLinearGroup ι F
hA : A ∈ {A | ∀ (w : ι → F), A • w - w ∈ L}
w : ι → F
⊢ A⁻¹ • w - w = -(1 • w - A⁻¹ • w)

Tactic:
one_smul,

Goal state after:
F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
L : Submodule F (ι → F)
A : SpecialLinearGroup ι F
hA : A ∈ {A | ∀ (w : ι → F), A • w - w ∈ L}
w : ι → F
⊢ A⁻¹ • w - w = -(w - A⁻¹ • w)
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case neg
R : Type u_1
V : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : Module.Free R V
d1 : Module.finrank R V = 1
u v : SpecialLinearGroup R V
a✝ : Nontrivial R
x : V
hx : ¬x = 0
⊢ ∀ (u : SpecialLinearGroup R V), ↑↑u = LinearMap.id

Tactic:
intro u

Goal state after:
case neg
R : Type u_1
V : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : Module.Free R V
d1 : Module.finrank R V = 1
u✝ v : SpecialLinearGroup R V
a✝ : Nontrivial R
x : V
hx : ¬x = 0
u : SpecialLinearGroup R V
⊢ ↑↑u = LinearMap.id
Module: Mathlib.LinearAlgebra.Projectivization.Action

Goal state before:
pp: case h
K : Type u_1
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Field K
inst✝ : Module K V
this✝ : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
a : Kˣ
this : LinearIndepOn K id {D.rep, D'.rep}
s : Set V := ⋯
b : Module.Basis (↑s) K V := ⋯
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
⊢ 1 • D'.rep = (dilatransvection ⋯) D'.rep

Tactic:
one_smul,

Goal state after:
case h
K : Type u_1
V : Type u_2
inst✝² : AddCommGroup V
inst✝¹ : Field K
inst✝ : Module K V
this✝ : ∀ {a b c d : ℙ K V}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
D D' E E' : ℙ K V
hD : LinearIndependent K ![D.rep, D'.rep]
hE : E ≠ E'
g : V ≃ₗ[K] V
gD : g • D = E
gE : g • D' = E'
hV : FiniteDimensional K V
a : Kˣ
this : LinearIndepOn K id {D.rep, D'.rep}
s : Set V := ⋯.extend ⋯
b : Module.Basis (↑s) K V := Module.Basis.extend this
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
⊢ D'.rep = (dilatransvection ⋯) D'.rep
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case neg
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g h : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV✝ : ¬Subsingleton V
hV : Nontrivial V
this : FaithfulSMul R V
Hg : ∃ r, r ^ Module.finrank R V = 1 ∧ ↑↑↑g = r • LinearMap.id := mem_center_iff.mp (Subtype.prop g)
Hh : ∃ r, r ^ Module.finrank R V = 1 ∧ ↑↑↑h = r • LinearMap.id := mem_center_iff.mp (Subtype.prop h)
Hgh : ∃ r, r ^ Module.finrank R V = 1 ∧ ↑↑↑(g * h) = r • LinearMap.id := mem_center_iff.mp (Subtype.prop (g * h))
⊢ ⋯.choose = Hg.choose * Hh.choose

Tactic:
change Hgh.choose = Hg.choose * Hh.choose

Goal state after:
case neg
R : Type u_1
V : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : Module.Free R V
inst✝ : Module.Finite R V
g h : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV✝ : ¬Subsingleton V
hV : Nontrivial V
this : FaithfulSMul R V
Hg : ∃ r, r ^ Module.finrank R V = 1 ∧ ↑↑↑g = r • LinearMap.id := mem_center_iff.mp (Subtype.prop g)
Hh : ∃ r, r ^ Module.finrank R V = 1 ∧ ↑↑↑h = r • LinearMap.id := mem_center_iff.mp (Subtype.prop h)
Hgh : ∃ r, r ^ Module.finrank R V = 1 ∧ ↑↑↑(g * h) = r • LinearMap.id := mem_center_iff.mp (Subtype.prop (g * h))
⊢ Hgh.choose = Hg.choose * Hh.choose
Module: Mathlib.LinearAlgebra.QuadraticForm.Real

Goal state before:
pp: case pos
ι : Type u_1
inst✝ : Fintype ι
w : ι → ℝ
u : ι → ℝˣ := fun i ↦ if h : w i = 0 then 1 else Units.mk0 (w i) h
hu : ∀ (i : ι), 1 / √|↑(u i)| ≠ 0
i : ι
hi : w i = 0
⊢ w i / |↑(u i)| = ↑(sign (w i))

Tactic:
simp [hi]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries

Goal state before:
pp: R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
M₃ : Type uM₃
M₄ : Type uM₄
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : AddCommGroup M₄
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Invertible 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
Q₄ : QuadraticForm R M₄
f : Q₁ →qᵢ Q₂
g : Q₃ →qᵢ Q₄
h₁ : Q₁ = comp Q₂ f.toLinearMap
h₃ : Q₃ = comp Q₄ g.toLinearMap
⊢ (associatedHom R) (comp (Q₂.tmul Q₄) (TensorProduct.map f.toLinearMap g.toLinearMap)) = (associatedHom R) (Q₁.tmul Q₃)

Tactic:
ext m₁ m₃ m₁' m₃'

Goal state after:
R : Type uR
M₁ : Type uM₁
M₂ : Type uM₂
M₃ : Type uM₃
M₄ : Type uM₄
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : AddCommGroup M₃
inst✝⁵ : AddCommGroup M₄
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M₄
inst✝ : Invertible 2
Q₁ : QuadraticForm R M₁
Q₂ : QuadraticForm R M₂
Q₃ : QuadraticForm R M₃
Q₄ : QuadraticForm R M₄
f : Q₁ →qᵢ Q₂
g : Q₃ →qᵢ Q₄
h₁ : Q₁ = comp Q₂ f.toLinearMap
h₃ : Q₃ = comp Q₄ g.toLinearMap
m₁ : M₁
m₃ : M₃
m₁' : M₁
m₃' : M₃
⊢ ((TensorProduct.AlgebraTensorModule.curry
          (((TensorProduct.AlgebraTensorModule.curry
                ((associatedHom R) (comp (Q₂.tmul Q₄) (TensorProduct.map f.toLinearMap g.toLinearMap))))
              m₁)
            m₃))
        m₁')
      m₃' =
    ((TensorProduct.AlgebraTensorModule.curry
          (((TensorProduct.AlgebraTensorModule.curry ((associatedHom R) (Q₁.tmul Q₃))) m₁) m₃))
        m₁')
      m₃'
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: 𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
p : Set ι := {i | 0 < w i}
m : Set ι := {i | w i ≤ 0}
⊢ sigPos (weightedSumSquares 𝕜 w) = {i | 0 < w i}.ncard

Tactic:
convert_to sigPos _ = p.ncard

Goal state after:
case convert_8
𝕜 : Type u_4
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
p : Set ι := {i | 0 < w i}
m : Set ι := {i | w i ≤ 0}
⊢ sigPos (weightedSumSquares 𝕜 w) = p.ncard
Module: Mathlib.LinearAlgebra.QuadraticForm.Signature

Goal state before:
pp: M : Type u_2
inst✝⁵ : AddCommGroup M
𝕜 : Type u_4
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : Module 𝕜 M
Q : QuadraticForm 𝕜 M
ι : Type u_5
inst✝¹ : Fintype ι
w : ι → 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hQ : Equivalent Q (weightedSumSquares 𝕜 w)
⊢ sigPos Q = {i | 0 < w i}.ncard

Tactic:
rw [hQ.sigPos_eq]
  exact sigPos_weightedSumSquares

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

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
b : P.Base
inst✝ : DecidableEq ι
j : ι
x : ↥b.support ⊕ ι → R
hx : x ∈ span R (range u)
⊢ x (Sum.inr j) = 0

Tactic:
by
  induction hx using span_induction with
  | mem x h => obtain ⟨i, rfl⟩ := h; simp [u]
  | zero => simp
  | add u v _ _ hu hv => simp [hu, hv]
  | smul t u _ hu => simp [hu]

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

Goal state before:
pp: case inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
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
inst✝² : P.IsReduced
b : P.Base
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
j : ι
h : j ≠ -↑i
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
aux : ∀ (n : ℕ), (e i ^ (n + 1)).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)
x : ℕ
hk₂ : (e i ^ 0).col (Sum.inr j) = x • Pi.single (Sum.inr (-↑i)) 1
hk₁ : P.root (-j) = 1 • P.root ↑i
⊢ j = -↑i

Tactic:
one_smul,

Goal state after:
case inl
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
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
inst✝² : P.IsReduced
b : P.Base
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
j : ι
h : j ≠ -↑i
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
aux : ∀ (n : ℕ), (e i ^ (n + 1)).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)
x : ℕ
hk₂ : (e i ^ 0).col (Sum.inr j) = x • Pi.single (Sum.inr (-↑i)) 1
hk₁ : P.root (-j) = P.root ↑i
⊢ j = -↑i
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

Goal state before:
pp: case mem.inl
ι : 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.IsCrystallographic
b : P.Base
inst✝⁴ : Finite ι
inst✝³ : IsDomain R
inst✝² : CharZero R
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
i : ↥b.support
hu : h i ∈ range h ∪ range e ∪ range f
⊢ (ωConj b) (h i) ∈ lieAlgebra b

Tactic:
rw [← neg_mem_iff]
      exact LieSubalgebra.subset_lieSpan <| by simp [ω_mul_h, mul_assoc]

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

Goal state before:
pp: case neg.inr
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
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
inst✝² : P.IsReduced
b : P.Base
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ↥b.support
j : ι
h : j ≠ -↑i
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
aux : ∀ (n : ℕ), (e i ^ (n + 1)).col (Sum.inr j) = e i *ᵥ (e i ^ n).col (Sum.inr j)
n : ℕ
k : ι
x : ℕ
hk₁ : P.root k = P.root j + n • P.root ↑i
hk₂ : (e i ^ n).col (Sum.inr j) = x • Pi.single (Sum.inr k) 1
hki : k ≠ -↑i
hij : P.root j + (n + 1) • P.root ↑i ∉ range ⇑P.root
l : ι
⊢ (x • e i *ᵥ Pi.single (Sum.inr k) 1) (Sum.inr l) = 0 (Sum.inr l)

Tactic:
replace hij : P.root l ≠ P.root i + P.root k :=
          fun contra ↦ hij ⟨l, by rw [contra, hk₁]; module⟩
        simp [e, -indexNeg_neg, hij]

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

Goal state before:
pp: case inr.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 j : ↥b.support
k l : ι
⊢ ∑ x,
      ((if P.root x = P.root ↑i + P.root l then
          Matrix.diagonal (fun x ↦ ↑(P.pairingIn ℤ x ↑j)) k x * (↑(chainBotCoeff (↑i) l) + 1)
        else 0) -
        if P.root k = P.root ↑i + P.root x then
          (↑(chainBotCoeff (↑i) x) + 1) * Matrix.diagonal (fun x ↦ ↑(P.pairingIn ℤ x ↑j)) x l
        else 0) =
    if P.root k = P.root ↑i + P.root l then ↑(b.cartanMatrix i j) * ↑(chainBotCoeff (↑i) l) + ↑(b.cartanMatrix i j)
    else 0

Tactic:
← Finset.sum_subset (Finset.subset_univ {k, l}) (by aesop)

Goal state after:
case inr.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 j : ↥b.support
k l : ι
⊢ ∑ x ∈ {k, l},
      ((if P.root x = P.root ↑i + P.root l then
          Matrix.diagonal (fun x ↦ ↑(P.pairingIn ℤ x ↑j)) k x * (↑(chainBotCoeff (↑i) l) + 1)
        else 0) -
        if P.root k = P.root ↑i + P.root x then
          (↑(chainBotCoeff (↑i) x) + 1) * Matrix.diagonal (fun x ↦ ↑(P.pairingIn ℤ x ↑j)) x l
        else 0) =
    if P.root k = P.root ↑i + P.root l then ↑(b.cartanMatrix i j) * ↑(chainBotCoeff (↑i) l) + ↑(b.cartanMatrix i j)
    else 0
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 : ι
hi : P.root i ∉ allRoots P
this : P.pairingIn ℤ i (short P) = 0 ∧ P.pairingIn ℤ i (long P) = 0
⊢ P.IsOrthogonal i (short P) ∧ P.IsOrthogonal i (long P)

Tactic:
by
    have : Module.IsReflexive R M := .of_isPerfPair P.toLinearMap
    simpa [isOrthogonal_iff_pairing_eq_zero, ← P.algebraMap_pairingIn ℤ]

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

Goal state before:
pp: ι : 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
h₂ : ∀ (a : ι), ¬P.root k = P.root a - P.root ↑i
this : chainBotCoeff (↑i) k = 0 ∧ chainTopCoeff (↑i) k = 0
⊢ ((∑ x, if P.root k = P.root ↑i + P.root x then (↑(chainBotCoeff (↑i) x) + 1) * (↑(chainTopCoeff (↑i) k) + 1) else 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:
by simp [h₁, h₂, this]

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

Goal state before:
pp: case inr.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
⊢ ((w (Sum.inr i))⁻¹ • w) (Sum.inr i) = v b i (Sum.inr i)

Tactic:
simp [hi]

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

Goal state before:
pp: ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Fintype ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module K M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module K N
P : RootPairing ι K M N
inst✝³ : P.IsReduced
inst✝² : P.IsCrystallographic
inst✝¹ : P.IsIrreducible
inst✝ : P.IsRootSystem
b : P.Base
h₀ : ↥b.support → ↥(lieAlgebra b) := fun i ↦ ⟨h i, ⋯⟩
e₀ : ↥b.support → ↥(lieAlgebra b) := fun i ↦ ⟨e i, ⋯⟩
f₀ : ↥b.support → ↥(lieAlgebra b) := fun i ↦ ⟨f i, ⋯⟩
⊢ range h₀ ∪ (range e₀ ∪ range f₀) ⊆ ↑(LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀))

Tactic:
refine union_subset ?_ LieSubalgebra.subset_lieSpan

Goal state after:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : Fintype ι
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : Field K
inst✝⁸ : CharZero K
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module K M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module K N
P : RootPairing ι K M N
inst✝³ : P.IsReduced
inst✝² : P.IsCrystallographic
inst✝¹ : P.IsIrreducible
inst✝ : P.IsRootSystem
b : P.Base
h₀ : ↥b.support → ↥(lieAlgebra b) := fun i ↦ ⟨h i, ⋯⟩
e₀ : ↥b.support → ↥(lieAlgebra b) := fun i ↦ ⟨e i, ⋯⟩
f₀ : ↥b.support → ↥(lieAlgebra b) := fun i ↦ ⟨f i, ⋯⟩
⊢ range h₀ ⊆ ↑(LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀))
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Relations

Goal state before:
pp: ι : 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 j : ↥b.support
hij : i ≠ j
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hij' : ↑i ≠ ↑j
this✝ : InvolutiveNeg ι := P.indexNeg
k l : ι
h₃ : l ≠ ↑j
h₄ : l ≠ -↑i
this :
  (∑ x,
      if P.root x = P.root l - P.root ↑j ∧ P.root k = P.root ↑i + P.root x then
        (↑(chainBotCoeff (↑i) x) + 1) * (↑(chainTopCoeff (↑j) l) + 1)
      else 0) =
    ∑ x,
      if P.root x = P.root ↑i + P.root l ∧ P.root k = P.root x - P.root ↑j then
        (↑(chainTopCoeff (↑j) x) + 1) * (↑(chainBotCoeff (↑i) l) + 1)
      else 0
h₁ : ∀ x ∈ Finset.univ, ¬((x = i ∧ l = -↑i) ∧ k = -↑j)
⊢ ⁅e i, f j⁆ (Sum.inr k) (Sum.inr l) = 0 (Sum.inr k) (Sum.inr l)

Tactic:
have h₂ : ∀ x ∈ Finset.univ, ¬ ((x = j ∧ l = j) ∧ k = i) := by
        rintro - - ⟨⟨-, contra⟩, -⟩; contradiction

Goal state after:
ι : 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 j : ↥b.support
hij : i ≠ j
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hij' : ↑i ≠ ↑j
this✝ : InvolutiveNeg ι := P.indexNeg
k l : ι
h₃ : l ≠ ↑j
h₄ : l ≠ -↑i
this :
  (∑ x,
      if P.root x = P.root l - P.root ↑j ∧ P.root k = P.root ↑i + P.root x then
        (↑(chainBotCoeff (↑i) x) + 1) * (↑(chainTopCoeff (↑j) l) + 1)
      else 0) =
    ∑ x,
      if P.root x = P.root ↑i + P.root l ∧ P.root k = P.root x - P.root ↑j then
        (↑(chainTopCoeff (↑j) x) + 1) * (↑(chainBotCoeff (↑i) l) + 1)
      else 0
h₁ : ∀ x ∈ Finset.univ, ¬((x = i ∧ l = -↑i) ∧ k = -↑j)
h₂ : ∀ x ∈ Finset.univ, ¬((x = j ∧ l = ↑j) ∧ k = ↑i)
⊢ ⁅e i, f j⁆ (Sum.inr k) (Sum.inr l) = 0 (Sum.inr k) (Sum.inr l)