mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField

Goal state before:
pp: case inr
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
⊢ -(M ^ Fintype.card K).charpoly.coeff (Fintype.card n - 1) = (-M.charpoly.coeff (Fintype.card n - 1)) ^ Fintype.card K

Tactic:
FiniteField.Matrix.charpoly_pow_card,

Goal state after:
case inr
n : Type u_1
inst✝³ : DecidableEq n
inst✝² : Fintype n
K : Type u_2
inst✝¹ : Field K
inst✝ : Fintype K
M : Matrix n n K
h✝ : Nonempty n
⊢ -M.charpoly.coeff (Fintype.card n - 1) = (-M.charpoly.coeff (Fintype.card n - 1)) ^ Fintype.card K
Module: Mathlib.LinearAlgebra.Matrix.Circulant

Goal state before:
pp: α : Type u_5
inst✝¹ : Zero α
inst✝ : One α
n : ℕ
⊢ (circulant fun i ↦ if ↑i = 0 then 1 else 0) = 1

Tactic:
by
    rw [← circulant_single_one]
    congr with j
    simp [Pi.single_apply]

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

Goal state before:
pp: m : Type u_1
n : Type u_3
R : Type u_5
inst✝ : CommRing R
A : Matrix m n R
⊢ A.IsTotallyUnimodular ↔
    ∀ (ι : Type w) [inst : Fintype ι] [inst_1 : DecidableEq ι] (f : ι → m) (g : ι → n),
      (A.submatrix f g).det ∈ Set.range SignType.cast

Tactic:
rw [isTotallyUnimodular_iff]
  constructor
  · intro hA ι _ _ f g
    specialize hA (Fintype.card ι) (f ∘ (Fintype.equivFin ι).symm) (g ∘ (Fintype.equivFin ι).symm)
    rwa [← submatrix_submatrix, det_submatrix_equiv_self] at hA
  · intro hA k f g
    specialize hA (ULift (Fin k)) (f ∘ Equiv.ulift) (g ∘ Equiv.ulift)
    rwa [← submatrix_submatrix, det_submatrix_equiv_self] at hA

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (j : Fin (n + 1)), j ≠ j₀ → ∑ i, M i j = 0
| fun i ↦ ((-1) ^ (↑i₀ + ↑↑i) * ∑ c, M c ↑i) * (M.submatrix i₀.succAbove (↑i).succAbove).det

Tactic:
i

Goal state after:
R : Type u_1
inst✝ : CommRing R
n : ℕ
M : Matrix (Fin (n + 1)) (Fin (n + 1)) R
i₀ j₀ : Fin (n + 1)
hv : ∀ (j : Fin (n + 1)), j ≠ j₀ → ∑ i, M i j = 0
i : { i // i ≠ j₀ }
| ((-1) ^ (↑i₀ + ↑↑i) * ∑ c, M c ↑i) * (M.submatrix i₀.succAbove (↑i).succAbove).det
Module: Mathlib.LinearAlgebra.Matrix.Echelon.Decomposition

Goal state before:
pp: m : Type u_1
inst✝⁵ : Fintype m
inst✝⁴ : LinearOrder m
n : Type u_2
inst✝³ : Fintype n
inst✝² : LinearOrder n
R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDomain R
A : Matrix m n R
cert : Decomposition A
⊢ A.rank = #{i | cert.pivot i ≠ ⊤}

Tactic:
rw [← cert.isPivotedBy.rank_eq,
    cert.L.rank_mul_eq_right_of_isLowerTriangular _ cert.L_lowerTriangular cert.L_diag_ne_zero]

Goal state after:
m : Type u_1
inst✝⁵ : Fintype m
inst✝⁴ : LinearOrder m
n : Type u_2
inst✝³ : Fintype n
inst✝² : LinearOrder n
R : Type u_3
inst✝¹ : CommRing R
inst✝ : IsDomain R
A : Matrix m n R
cert : Decomposition A
⊢ A.rank = (A.submatrix (⇑cert.σ) id).rank
Module: Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.MvPolynomial

Goal state before:
pp: case neg
m : Type u_1
k : Type u_2
inst✝³ : Fintype m
inst✝² : DecidableEq m
inst✝¹ : Field k
inst✝ : Infinite k
p q : MvPolynomial (m × m) k
h : ∀ (g : GL m k), (eval fun ij ↦ ↑g ij.1 ij.2) p = (eval fun ij ↦ ↑g ij.1 ij.2) q
s : m × m → k
hs_det : ¬(Matrix.of fun i j ↦ s (i, j)).det = 0
⊢ ((eval s) p - (eval s) q) * (Matrix.of fun i j ↦ s (i, j)).det = 0

Tactic:
· have hh : (eval s) p = (eval s) q :=
        h (Matrix.GeneralLinearGroup.mkOfDetNeZero
          (Matrix.of fun i j : m => s (i, j)) hs_det)
      rw [hh, sub_self, zero_mul]

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

Goal state before:
pp: case «1».«1»
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
h10 : ↑A 1 0 = 0
h00 : 0 < ↑A 0 0
h01 : 0 ≤ ↑A 0 1
h11 : |↑A 0 1| < |↑A 1 1|
h1 : 0 < |↑A 1 1|
h2 : 0 < |↑A 0 0|
⊢ |↑A ((fun i ↦ i) ⟨1, ⋯⟩) ((fun i ↦ i) ⟨1, ⋯⟩)| ≤ |m|

Tactic:
· simpa only [← abs_mul, A_c_eq_zero h10] using! (le_mul_iff_one_le_left h1).mpr h2

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Irreducible.Defs

Goal state before:
pp: case mp
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
h_irr : A.IsIrreducible
⊢ ∀ (i j : n), ∃ k > 0, 0 < (A ^ k) i j

Tactic:
i

Goal state after:
case mp
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
h_irr : A.IsIrreducible
i : n
⊢ ∀ (j : n), ∃ k > 0, 0 < (A ^ k) i j
Module: Mathlib.LinearAlgebra.Matrix.IsDiag

Goal state before:
pp: case mp.refine_4
α : Type u_1
n : Type u_4
m : Type u_5
inst✝ : Zero α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
h : (fromBlocks A B C D).IsDiag
i j : n
hij : i ≠ j
⊢ (fun i j ↦ D i j = 0) i j

Tactic:
· exact h (Sum.inr_injective.ne hij)

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

Goal state before:
pp: case of
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
A : Set (ℙ K V)
B : Subspace K V
h : A ⊆ ↑B
x x✝ : ℙ K V
hx✝ : x✝ ∈ A
⊢ x✝ ∈ B

Tactic:
apply h; assumption

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:
rw [Subgroup.map_iSup]

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

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

Tactic:
exact Subgroup.map_top_of_surjective _ (QuotientGroup.mk'_surjective _)

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

Goal state before:
pp: F : Type u_1
inst✝² : Field F
ι : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
v : ι → F
hv : v ≠ 0
A B : SpecialLinearGroup ι F
hA : A ∈ lineStab (F ∙ v)
hB : B ∈ lineStab (F ∙ v)
⊢ A * B = B * A

Tactic:
by
  refine Subtype.ext <| ext_iff_smul.2 fun w ↦ ?_
  obtain ⟨α, hα⟩ := Submodule.mem_span_singleton.mp (hA w)
  obtain ⟨β, hβ⟩ := Submodule.mem_span_singleton.mp (hB w)
  simp only [coe_mul, mul_smul, ← Matrix.SpecialLinearGroup.smul_def]
  rw [← sub_add_cancel (A • w) w, ← hα, ← sub_add_cancel (B • w) w,
    ← hβ, smul_add, smul_add, ← sub_left_inj (a := w), ← add_sub, ← hα, ← add_sub, ← hβ,
    smul_comm, lineStab_fix_of_span v hv A hA, smul_comm, lineStab_fix_of_span v hv B hB, add_comm]

Goal state after:
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 := ⋯.extend ⋯
b : Module.Basis (↑s) K V := Module.Basis.extend this
hD_mem : D.rep ∈ s
hD'_mem : D'.rep ∈ s
⊢ D'.rep = D'.rep + (b.repr D'.rep) ⟨D.rep, hD_mem⟩ • (↑a - 1) • b ⟨D.rep, hD_mem⟩

Tactic:
suffices (b.repr D'.rep) ⟨D.rep, hD_mem⟩ = 0 by
        rw [Module.Basis.extend_apply_self]
        simp [this]

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
⊢ (b.repr D'.rep) ⟨D.rep, hD_mem⟩ = 0
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: 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 : SpecialLinearGroup R V
hg : g ∈ Subgroup.center (SpecialLinearGroup R V)
x : V
⊢ ↑↑g x = ⋯.choose • x

Tactic:
by
  let H := (mem_center_iff.mp hg).choose_spec.2
  rw [LinearMap.ext_iff] at H
  simp [H]

Goal state after:
Module: Mathlib.LinearAlgebra.QuadraticForm.Basis

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : LinearOrder ι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticMap R M N
bm : Basis ι R M
i j : ι
⊢ ((Q.toBilin bm) (bm i)) (bm j) = if i = j then Q (bm i) else if i < j then polar (⇑Q) (bm i) (bm j) else 0

Tactic:
by
  simp [toBilin]

Goal state after:
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case pos
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 : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : Subsingleton R
⊢ ↑↑1 • LinearMap.id = ↑↑↑g

pp: case pos
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 : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV : Subsingleton V
⊢ ↑↑1 • LinearMap.id = ↑↑↑g

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 : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV : ¬Subsingleton V
⊢ ↑↑⟨⋯.unit, ⋯⟩ • LinearMap.id = ↑↑↑g

Tactic:
· simp [Subsingleton.eq_one g]

Goal state after:
case pos
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 : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV : Subsingleton V
⊢ ↑↑1 • LinearMap.id = ↑↑↑g

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 : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV : ¬Subsingleton V
⊢ ↑↑⟨⋯.unit, ⋯⟩ • LinearMap.id = ↑↑↑g
Module: Mathlib.LinearAlgebra.SpecialLinearGroup

Goal state before:
pp: case pos
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 : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV : Subsingleton V
⊢ ↑↑1 • LinearMap.id = ↑↑↑g

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 : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV : ¬Subsingleton V
⊢ ↑↑⟨⋯.unit, ⋯⟩ • LinearMap.id = ↑↑↑g

Tactic:
· simp [Subsingleton.eq_one g]

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 : ↥(Subgroup.center (SpecialLinearGroup R V))
hR : ¬Subsingleton R
hV : ¬Subsingleton V
⊢ ↑↑⟨⋯.unit, ⋯⟩ • LinearMap.id = ↑↑↑g
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

Goal state before:
pp: case inr.inr
ι : 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✝¹ : CharZero R
inst✝ : Fintype ι
i : ↥b.support
k l : ι
⊢ (ω b * h i) (Sum.inr k) (Sum.inr l) = (-h i * ω b) (Sum.inr k) (Sum.inr l)

Tactic:
simp only [ω, h, Matrix.mul_apply, Fintype.sum_sum_type, Matrix.fromBlocks_apply₂₂]
    aesop

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ : P.root k + P.root i = P.root l
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra✝ : P.IsG2
n : ι
h₃ : P.root n = P.root k + P.root i - P.root j
x y : ℤ
h₀ : x • P.root i + y • P.root j = P.root k
s : Set ℤ := {-3, -1, 0, 1, 3}
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
hli' : P.root l ≠ -P.root i
contra : P.root m = P.root i
h₂ : P.root k = P.root i + P.root j
⊢ P.root n = 2 • P.root i

Tactic:
rw [h₃, h₂]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ : P.root k + P.root i = P.root l
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra✝ : P.IsG2
n : ι
h₃ : P.root n = P.root k + P.root i - P.root j
x y : ℤ
h₀ : x • P.root i + y • P.root j = P.root k
s : Set ℤ := {-3, -1, 0, 1, 3}
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
hli' : P.root l ≠ -P.root i
contra : P.root m = P.root i
h₂ : P.root k = P.root i + P.root j
⊢ P.root i + P.root j + P.root i - P.root j = 2 • P.root i
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Lemmas

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ : P.root k + P.root i = P.root l
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra✝ : P.IsG2
n : ι
h₃ : P.root n = P.root k + P.root i - P.root j
x y : ℤ
h₀ : x • P.root i + y • P.root j = P.root k
s : Set ℤ := {-3, -1, 0, 1, 3}
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
hli' : P.root l ≠ -P.root i
hmi : P.root m ≠ P.root i
contra : P.root m = -P.root i
h₂ : P.root k = -P.root i + P.root j
⊢ P.root n = 0

Tactic:
rw [h₃, h₂]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CharZero R
inst✝⁸ : IsDomain R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : RootPairing ι R M N
inst✝³ : Finite ι
inst✝² : P.IsCrystallographic
b : P.Base
i j k l m : ι
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
hi : i ∈ b.support
hj : j ∈ b.support
hij : i ≠ j
h₁ : P.root k + P.root i = P.root l
this✝ : Module.IsReflexive R M
this : IsAddTorsionFree M
contra✝ : P.IsG2
n : ι
h₃ : P.root n = P.root k + P.root i - P.root j
x y : ℤ
h₀ : x • P.root i + y • P.root j = P.root k
s : Set ℤ := {-3, -1, 0, 1, 3}
A : ℤ := P.pairingIn ℤ j i
hki : P.root k ≠ P.root i
hki' : P.root k ≠ -P.root i
hli : P.root l ≠ P.root i
hli' : P.root l ≠ -P.root i
hmi : P.root m ≠ P.root i
contra : P.root m = -P.root i
h₂ : P.root k = -P.root i + P.root j
⊢ -P.root i + P.root j + P.root i - P.root j = 0
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 : ι
⊢ ⁅h j, e i⁆ (Sum.inr k) (Sum.inr l) = (b.cartanMatrix i j • e i) (Sum.inr k) (Sum.inr l)

Tactic:
· simp only [h, e, indexNeg_neg, Ring.lie_def, Matrix.sub_apply, Matrix.mul_apply,
      Fintype.sum_sum_type, Matrix.fromBlocks_apply₂₁, Matrix.zero_apply, Matrix.fromBlocks_apply₁₂,
      Matrix.of_apply, mul_ite, mul_one, mul_zero, ite_self, Finset.sum_const_zero,
      Matrix.fromBlocks_apply₂₂, zero_add, ite_mul, zero_mul, Matrix.smul_apply, smul_ite, smul_add,
      zsmul_eq_mul, smul_zero]
    rw [← Finset.sum_sub_distrib, ← Finset.sum_subset (Finset.subset_univ {k, l}) (by aesop)]
    rcases eq_or_ne k l with rfl | hkl; · simp [P.ne_zero i]
    simp only [Matrix.diagonal_apply, ite_mul, zero_mul, mul_ite, mul_zero, Finset.sum_sub_distrib,
      Finset.mem_singleton, Finset.sum_singleton, Finset.sum_insert, hkl, not_false_eq_true,
      reduceIte, right_eq_add, ite_self, add_zero, zero_add, ite_sub_ite, sub_self,
      Base.cartanMatrix, Base.cartanMatrixIn_def]
    refine ite_congr rfl (fun hkil ↦ ?_) (fun _ ↦ rfl)
    simp only [pairingIn_eq_add_of_root_eq_add hkil, Int.cast_add]
    ring

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

Goal state before:
pp: case h.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
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
case_inl : ∀ (j : ↥b.support), (e i ^ 2).col (Sum.inl j) = 0
j : ι
hij : ¬j = -↑i
k : ι
x : ℕ
hk₁ : P.root j + (chainTopCoeff (↑i) j + 1) • P.root ↑i ∈ range ⇑P.root
hij' : LinearIndependent R ![P.root ↑i, P.root j]
⊢ False

Tactic:
root_add_nsmul_mem_range_iff_le_chainTopCoeff hij'

Goal state after:
case h.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
this✝¹ : Module.IsReflexive R M
this✝ : IsAddTorsionFree M
this : InvolutiveNeg ι := P.indexNeg
case_inl : ∀ (j : ↥b.support), (e i ^ 2).col (Sum.inl j) = 0
j : ι
hij : ¬j = -↑i
k : ι
x : ℕ
hk₁ : chainTopCoeff (↑i) j + 1 ≤ chainTopCoeff (↑i) j
hij' : LinearIndependent R ![P.root ↑i, P.root j]
⊢ False
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis

Goal state before:
pp: case hx
ι : 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) := ⋯
e₀ : ↥b.support → ↥(lieAlgebra b) := ⋯
f₀ : ↥b.support → ↥(lieAlgebra b) := ⋯
i : ↥b.support
hef : h₀ i = ⁅e₀ i, f₀ i⁆
⊢ e₀ i ∈ LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀)

Tactic:
exact LieSubalgebra.subset_lieSpan <| by simp

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

Goal state before:
pp: case hy
ι : 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) := ⋯
e₀ : ↥b.support → ↥(lieAlgebra b) := ⋯
f₀ : ↥b.support → ↥(lieAlgebra b) := ⋯
i : ↥b.support
hef : h₀ i = ⁅e₀ i, f₀ i⁆
⊢ f₀ i ∈ LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀)

Tactic:
exact LieSubalgebra.subset_lieSpan <| by simp

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

Goal state before:
pp: case h₂
ι : 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.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
_i : InvolutiveNeg ι := ⋯
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
j : ι
⊢ ∀ (i j k : ι),
    P.root k = P.root i + P.root j →
      (∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, (∀ (k : ↥b.support), u k ∈ U) → v b i ∈ U) →
        j ∈ b.support →
          ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, (∀ (k : ↥b.support), u k ∈ U) → v b k ∈ U

Tactic:
intro k l m hm hk hl U aux

Goal state after:
case h₂
ι : 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.IsCrystallographic
b : P.Base
inst✝¹ : P.IsReduced
inst✝ : P.IsIrreducible
_i : InvolutiveNeg ι := P.indexNeg
hωu : ∀ (i : ↥b.support), ω b *ᵥ u i = u i
hωv : ∀ (i : ι), ω b *ᵥ v b i = v b (-i)
j k l m : ι
hm : P.root m = P.root k + P.root l
hk : ∀ {U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)}, (∀ (k : ↥b.support), u k ∈ U) → v b k ∈ U
hl : l ∈ b.support
U : LieSubmodule K (↥(lieAlgebra b)) (↥b.support ⊕ ι → K)
aux : ∀ (k : ↥b.support), u k ∈ U
⊢ v b m ∈ U
Module: Mathlib.LinearAlgebra.RootSystem.OfBilinear

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReflexive R M
B : M →ₗ[R] M →ₗ[R] R
hNB : B.Nondegenerate
hSB : B.IsSymm
h2 : IsRegular 2
x y : ↑{x | B.IsReflective x}
z : M
⊢ 2 * (B ↑y) z - 2 * (B ↑y) ↑x * (IsReflective.coroot B ⋯) z = (B ↑y) ↑y * (IsReflective.coroot B ⋯) z

Tactic:
rw [← isOrthogonal_reflection B x.2 hSB y y, apply_self_mul_coroot_apply, ← hSB.eq z,
      ← hSB.eq z, RingHom.id_apply, RingHom.id_apply, Module.reflection_apply, map_sub,
      mul_sub, sub_eq_sub_iff_comm, sub_left_inj]

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReflexive R M
B : M →ₗ[R] M →ₗ[R] R
hNB : B.Nondegenerate
hSB : B.IsSymm
h2 : IsRegular 2
x y : ↑{x | B.IsReflective x}
z : M
⊢ 2 * (B ↑y) ↑x * (IsReflective.coroot B ⋯) z = 2 * (B z) ((IsReflective.coroot B ⋯) ↑y • ↑x)
Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Semisimple

Goal state before:
pp: case refine_2
ι : 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.IsCrystallographic
b : P.Base
i : ↥b.support
⊢ ∀ (x : ↥H), ∃ k, (((toEnd K (↥H) (↥b.support ⊕ ι → K)) x - 0 x • 1) ^ k) (u i) = 0

Tactic:
rintro ⟨⟨x, -⟩, hx⟩

Goal state after:
case refine_2
ι : 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.IsCrystallographic
b : P.Base
i : ↥b.support
x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) K
property✝ : x ∈ lieAlgebra b
hx : ⟨x, property✝⟩ ∈ H
⊢ ∃ k, (((toEnd K (↥H) (↥b.support ⊕ ι → K)) ⟨⟨x, property✝⟩, hx⟩ - 0 ⟨⟨x, property✝⟩, hx⟩ • 1) ^ k) (u i) = 0