awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : Fintype ι
i j : ↥b.support
⊢ ω b * (f i * e j) - ω b * (e j * f i) = -ω b * ⁅e j, f i⁆
have rw : ω b * (f i * e j) - ω b * (e j * f i) = -(ω b * (e j * f i)) + ω b * (f i * e j)
Tactic: rw [Ring.lie_def, mul_sub, neg_mul, neg_mul, sub_neg_eq_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : Fintype ι
i j : ↥b.support
⊢ ⁅e i, f j⁆ * ω b = -ω b * ⁅e j, f i⁆
have calc : ⁅e i, f j⁆ * ω b = e i * f j * ω b - f j * e i * ω b
Tactic: classical
  calc ⁅e i, f j⁆ * ω b = e i * f j * ω b - f j * e i * ω b := by rw [Ring.lie_def, sub_mul]
                      _ = e i * (f j * ω b) - f j * (e i * ω b) := by rw [mul_assoc, mul_assoc]
                      _ = e i * (ω b * e j) - f j * (ω b * f i) := by rw [← ω_mul_e, ← ω_mul_f]
                      _ = (e i * ω b) * e j - (f j * ω b) * f i := by rw [← mul_assoc, ← mul_assoc]
                      _ = (ω b * f i) * e j - (ω b * e j) * f i := by rw [← ω_mul_e, ← ω_mul_f]
                      _ = ω b * (f i * e j) - ω b * (e j * f i) := by rw [mul_assoc, mul_assoc]
                      _ = -ω b * ⁅e j, f i⁆ := ?_
  rw [Ring.lie_def, mul_sub, neg_mul, neg_mul, sub_neg_eq_add]
  abel
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : Fintype ι
i j : ↥b.support
calc : ⁅e i, f j⁆ * ω b = e i * f j * ω b - f j * e i * ω b
⊢ ⁅e i, f j⁆ * ω b = -ω b * ⁅e j, f i⁆
have calc₁ : e i * f j * ω b - f j * e i * ω b = e i * (f j * ω b) - f j * (e i * ω b)
Tactic: classical
  calc ⁅e i, f j⁆ * ω b = e i * f j * ω b - f j * e i * ω b := by rw [Ring.lie_def, sub_mul]
                      _ = e i * (f j * ω b) - f j * (e i * ω b) := by rw [mul_assoc, mul_assoc]
                      _ = e i * (ω b * e j) - f j * (ω b * f i) := by rw [← ω_mul_e, ← ω_mul_f]
                      _ = (e i * ω b) * e j - (f j * ω b) * f i := by rw [← mul_assoc, ← mul_assoc]
                      _ = (ω b * f i) * e j - (ω b * e j) * f i := by rw [← ω_mul_e, ← ω_mul_f]
                      _ = ω b * (f i * e j) - ω b * (e j * f i) := by rw [mul_assoc, mul_assoc]
                      _ = -ω b * ⁅e j, f i⁆ := ?_
  rw [Ring.lie_def, mul_sub, neg_mul, neg_mul, sub_neg_eq_add]
  abel
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : Fintype ι
i j : ↥b.support
calc : ⁅e i, f j⁆ * ω b = e i * f j * ω b - f j * e i * ω b
calc₁ : e i * f j * ω b - f j * e i * ω b = e i * (f j * ω b) - f j * (e i * ω b)
⊢ ⁅e i, f j⁆ * ω b = -ω b * ⁅e j, f i⁆
have calc₂ : e i * (f j * ω b) - f j * (e i * ω b) = e i * (ω b * e j) - f j * (ω b * f i)
Tactic: classical
  calc ⁅e i, f j⁆ * ω b = e i * f j * ω b - f j * e i * ω b := by rw [Ring.lie_def, sub_mul]
                      _ = e i * (f j * ω b) - f j * (e i * ω b) := by rw [mul_assoc, mul_assoc]
                      _ = e i * (ω b * e j) - f j * (ω b * f i) := by rw [← ω_mul_e, ← ω_mul_f]
                      _ = (e i * ω b) * e j - (f j * ω b) * f i := by rw [← mul_assoc, ← mul_assoc]
                      _ = (ω b * f i) * e j - (ω b * e j) * f i := by rw [← ω_mul_e, ← ω_mul_f]
                      _ = ω b * (f i * e j) - ω b * (e j * f i) := by rw [mul_assoc, mul_assoc]
                      _ = -ω b * ⁅e j, f i⁆ := ?_
  rw [Ring.lie_def, mul_sub, neg_mul, neg_mul, sub_neg_eq_add]
  abel
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : Fintype ι
i j : ↥b.support
calc : ⁅e i, f j⁆ * ω b = e i * f j * ω b - f j * e i * ω b
calc₁ : e i * f j * ω b - f j * e i * ω b = e i * (f j * ω b) - f j * (e i * ω b)
calc₂ : e i * (f j * ω b) - f j * (e i * ω b) = e i * (ω b * e j) - f j * (ω b * f i)
⊢ ⁅e i, f j⁆ * ω b = -ω b * ⁅e j, f i⁆
have calc₃ : e i * (ω b * e j) - f j * (ω b * f i) = e i * ω b * e j - f j * ω b * f i
Tactic: classical
  calc ⁅e i, f j⁆ * ω b = e i * f j * ω b - f j * e i * ω b := by rw [Ring.lie_def, sub_mul]
                      _ = e i * (f j * ω b) - f j * (e i * ω b) := by rw [mul_assoc, mul_assoc]
                      _ = e i * (ω b * e j) - f j * (ω b * f i) := by rw [← ω_mul_e, ← ω_mul_f]
                      _ = (e i * ω b) * e j - (f j * ω b) * f i := by rw [← mul_assoc, ← mul_assoc]
                      _ = (ω b * f i) * e j - (ω b * e j) * f i := by rw [← ω_mul_e, ← ω_mul_f]
                      _ = ω b * (f i * e j) - ω b * (e j * f i) := by rw [mul_assoc, mul_assoc]
                      _ = -ω b * ⁅e j, f i⁆ := ?_
  rw [Ring.lie_def, mul_sub, neg_mul, neg_mul, sub_neg_eq_add]
  abel
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : Fintype ι
i j : ↥b.support
calc : ⁅e i, f j⁆ * ω b = e i * f j * ω b - f j * e i * ω b
calc₁ : e i * f j * ω b - f j * e i * ω b = e i * (f j * ω b) - f j * (e i * ω b)
calc₂ : e i * (f j * ω b) - f j * (e i * ω b) = e i * (ω b * e j) - f j * (ω b * f i)
calc₃ : e i * (ω b * e j) - f j * (ω b * f i) = e i * ω b * e j - f j * ω b * f i
⊢ ⁅e i, f j⁆ * ω b = -ω b * ⁅e j, f i⁆
have calc₄ : e i * ω b * e j - f j * ω b * f i = ω b * f i * e j - ω b * e j * f i
Tactic: classical
  calc ⁅e i, f j⁆ * ω b = e i * f j * ω b - f j * e i * ω b := by rw [Ring.lie_def, sub_mul]
                      _ = e i * (f j * ω b) - f j * (e i * ω b) := by rw [mul_assoc, mul_assoc]
                      _ = e i * (ω b * e j) - f j * (ω b * f i) := by rw [← ω_mul_e, ← ω_mul_f]
                      _ = (e i * ω b) * e j - (f j * ω b) * f i := by rw [← mul_assoc, ← mul_assoc]
                      _ = (ω b * f i) * e j - (ω b * e j) * f i := by rw [← ω_mul_e, ← ω_mul_f]
                      _ = ω b * (f i * e j) - ω b * (e j * f i) := by rw [mul_assoc, mul_assoc]
                      _ = -ω b * ⁅e j, f i⁆ := ?_
  rw [Ring.lie_def, mul_sub, neg_mul, neg_mul, sub_neg_eq_add]
  abel
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : Fintype ι
i j : ↥b.support
calc : ⁅e i, f j⁆ * ω b = e i * f j * ω b - f j * e i * ω b
calc₁ : e i * f j * ω b - f j * e i * ω b = e i * (f j * ω b) - f j * (e i * ω b)
calc₂ : e i * (f j * ω b) - f j * (e i * ω b) = e i * (ω b * e j) - f j * (ω b * f i)
calc₃ : e i * (ω b * e j) - f j * (ω b * f i) = e i * ω b * e j - f j * ω b * f i
calc₄ : e i * ω b * e j - f j * ω b * f i = ω b * f i * e j - ω b * e j * f i
⊢ ⁅e i, f j⁆ * ω b = -ω b * ⁅e j, f i⁆
have calc₅ : ω b * f i * e j - ω b * e j * f i = ω b * (f i * e j) - ω b * (e j * f i)
Tactic: classical
  calc ⁅e i, f j⁆ * ω b = e i * f j * ω b - f j * e i * ω b := by rw [Ring.lie_def, sub_mul]
                      _ = e i * (f j * ω b) - f j * (e i * ω b) := by rw [mul_assoc, mul_assoc]
                      _ = e i * (ω b * e j) - f j * (ω b * f i) := by rw [← ω_mul_e, ← ω_mul_f]
                      _ = (e i * ω b) * e j - (f j * ω b) * f i := by rw [← mul_assoc, ← mul_assoc]
                      _ = (ω b * f i) * e j - (ω b * e j) * f i := by rw [← ω_mul_e, ← ω_mul_f]
                      _ = ω b * (f i * e j) - ω b * (e j * f i) := by rw [mul_assoc, mul_assoc]
                      _ = -ω b * ⁅e j, f i⁆ := ?_
  rw [Ring.lie_def, mul_sub, neg_mul, neg_mul, sub_neg_eq_add]
  abel
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : Fintype ι
i j : ↥b.support
calc : ⁅e i, f j⁆ * ω b = e i * f j * ω b - f j * e i * ω b
calc₁ : e i * f j * ω b - f j * e i * ω b = e i * (f j * ω b) - f j * (e i * ω b)
calc₂ : e i * (f j * ω b) - f j * (e i * ω b) = e i * (ω b * e j) - f j * (ω b * f i)
calc₃ : e i * (ω b * e j) - f j * (ω b * f i) = e i * ω b * e j - f j * ω b * f i
calc₄ : e i * ω b * e j - f j * ω b * f i = ω b * f i * e j - ω b * e j * f i
calc₅ : ω b * f i * e j - ω b * e j * f i = ω b * (f i * e j) - ω b * (e j * f i)
⊢ ⁅e i, f j⁆ * ω b = -ω b * ⁅e j, f i⁆
have calc₆ : ω b * (f i * e j) - ω b * (e j * f i) = -ω b * ⁅e j, f i⁆
Tactic: classical
  calc ⁅e i, f j⁆ * ω b = e i * f j * ω b - f j * e i * ω b := by rw [Ring.lie_def, sub_mul]
                      _ = e i * (f j * ω b) - f j * (e i * ω b) := by rw [mul_assoc, mul_assoc]
                      _ = e i * (ω b * e j) - f j * (ω b * f i) := by rw [← ω_mul_e, ← ω_mul_f]
                      _ = (e i * ω b) * e j - (f j * ω b) * f i := by rw [← mul_assoc, ← mul_assoc]
                      _ = (ω b * f i) * e j - (ω b * e j) * f i := by rw [← ω_mul_e, ← ω_mul_f]
                      _ = ω b * (f i * e j) - ω b * (e j * f i) := by rw [mul_assoc, mul_assoc]
                      _ = -ω b * ⁅e j, f i⁆ := ?_
  rw [Ring.lie_def, mul_sub, neg_mul, neg_mul, sub_neg_eq_add]
  abel
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : Fintype ι
i j : ↥b.support
calc : ⁅e i, f j⁆ * ω b = e i * f j * ω b - f j * e i * ω b
calc₁ : e i * f j * ω b - f j * e i * ω b = e i * (f j * ω b) - f j * (e i * ω b)
calc₂ : e i * (f j * ω b) - f j * (e i * ω b) = e i * (ω b * e j) - f j * (ω b * f i)
calc₃ : e i * (ω b * e j) - f j * (ω b * f i) = e i * ω b * e j - f j * ω b * f i
calc₄ : e i * ω b * e j - f j * ω b * f i = ω b * f i * e j - ω b * e j * f i
calc₅ : ω b * f i * e j - ω b * e j * f i = ω b * (f i * e j) - ω b * (e j * f i)
calc₆ : ω b * (f i * e j) - ω b * (e j * f i) = -ω b * ⁅e j, f i⁆
⊢ ⁅e i, f j⁆ * ω b = -ω b * ⁅e j, f i⁆
have calc₇ : ω b * (f i * e j) - ω b * (e j * f i) = -(ω b * (e j * f i)) + ω b * (f i * e j)
Tactic: classical
  calc ⁅e i, f j⁆ * ω b = e i * f j * ω b - f j * e i * ω b := by rw [Ring.lie_def, sub_mul]
                      _ = e i * (f j * ω b) - f j * (e i * ω b) := by rw [mul_assoc, mul_assoc]
                      _ = e i * (ω b * e j) - f j * (ω b * f i) := by rw [← ω_mul_e, ← ω_mul_f]
                      _ = (e i * ω b) * e j - (f j * ω b) * f i := by rw [← mul_assoc, ← mul_assoc]
                      _ = (ω b * f i) * e j - (ω b * e j) * f i := by rw [← ω_mul_e, ← ω_mul_f]
                      _ = ω b * (f i * e j) - ω b * (e j * f i) := by rw [mul_assoc, mul_assoc]
                      _ = -ω b * ⁅e j, f i⁆ := ?_
  rw [Ring.lie_def, mul_sub, neg_mul, neg_mul, sub_neg_eq_add]
  abel
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : DecidableEq ι
j : ι
x_1 x : ↥b.support ⊕ ι → R
h : Membership.mem (γ := Set (↥b.support ⊕ ι → R)) (range u) x
⊢ x (Sum.inr j) = 0
have mem : ∀ (i : ↥b.support), u i (Sum.inr j) = 0
Tactic: obtain ⟨i, rfl⟩ := h
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : DecidableEq ι
j : ι
x : ↥b.support ⊕ ι → R
hx : Membership.mem (γ := Submodule R (↥b.support ⊕ ι → R)) (span R (range u)) x
⊢ x (Sum.inr j) = 0
have mem : ∀ (x : ↥b.support ⊕ ι → R) (h : Membership.mem (γ := Set (↥b.support ⊕ ι → R)) (range u) x), x (Sum.inr j) = 0
Tactic: 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]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : DecidableEq ι
j : ι
x : ↥b.support ⊕ ι → R
hx : Membership.mem (γ := Submodule R (↥b.support ⊕ ι → R)) (span R (range u)) x
mem : ∀ (x : ↥b.support ⊕ ι → R) (h : Membership.mem (γ := Set (↥b.support ⊕ ι → R)) (range u) x), x (Sum.inr j) = 0
⊢ x (Sum.inr j) = 0
have zero : Eq.{u_2 + 1} (α := R) (0 (Sum.inr j)) 0
Tactic: 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]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : DecidableEq ι
j : ι
x : ↥b.support ⊕ ι → R
hx : Membership.mem (γ := Submodule R (↥b.support ⊕ ι → R)) (span R (range u)) x
mem : ∀ (x : ↥b.support ⊕ ι → R) (h : Membership.mem (γ := Set (↥b.support ⊕ ι → R)) (range u) x), x (Sum.inr j) = 0
zero : Eq.{u_2 + 1} (α := R) (0 (Sum.inr j)) 0
⊢ x (Sum.inr j) = 0
have add : ∀ (u v : ↥b.support ⊕ ι → R),
  Membership.mem (γ := Submodule R (↥b.support ⊕ ι → R)) (span R (range GeckConstruction.u)) u →
    Membership.mem (γ := Submodule R (↥b.support ⊕ ι → R)) (span R (range GeckConstruction.u)) v →
      ∀ (hu : u (Sum.inr j) = 0) (hv : v (Sum.inr j) = 0), (u + v) (Sum.inr j) = 0
Tactic: 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]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
b : P.Base
inst_5 : DecidableEq ι
j : ι
x : ↥b.support ⊕ ι → R
hx : Membership.mem (γ := Submodule R (↥b.support ⊕ ι → R)) (span R (range u)) x
mem : ∀ (x : ↥b.support ⊕ ι → R) (h : Membership.mem (γ := Set (↥b.support ⊕ ι → R)) (range u) x), x (Sum.inr j) = 0
zero : Eq.{u_2 + 1} (α := R) (0 (Sum.inr j)) 0
add :
  ∀ (u v : ↥b.support ⊕ ι → R),
    Membership.mem (γ := Submodule R (↥b.support ⊕ ι → R)) (span R (range GeckConstruction.u)) u →
      Membership.mem (γ := Submodule R (↥b.support ⊕ ι → R)) (span R (range GeckConstruction.u)) v →
        ∀ (hu : u (Sum.inr j) = 0) (hv : v (Sum.inr j) = 0), (u + v) (Sum.inr j) = 0
⊢ x (Sum.inr j) = 0
have smul : ∀ (t : R) (u : ↥b.support ⊕ ι → R),
  Membership.mem (γ := Submodule R (↥b.support ⊕ ι → R)) (span R (range GeckConstruction.u)) u →
    ∀ (hu : u (Sum.inr j) = 0), (t • u) (Sum.inr j) = 0
Tactic: 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]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : DecidableEq ι
inst_10 : Fintype ι
i j : ↥b.support
⊢ ⁅e i, ⁅f i, u j⁆⁆ = |b.cartanMatrix i j| • u i
have h : ∀ (k : ↥b.support), ⁅e i, ⁅f i, u j⁆⁆ (Sum.inl k) = (|b.cartanMatrix i j| • u i) (Sum.inl k)
Tactic: ext (k | k)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : DecidableEq ι
inst_10 : Fintype ι
i j : ↥b.support
h : ∀ (k : ↥b.support), ⁅e i, ⁅f i, u j⁆⁆ (Sum.inl k) = (|b.cartanMatrix i j| • u i) (Sum.inl k)
⊢ ⁅e i, ⁅f i, u j⁆⁆ = |b.cartanMatrix i j| • u i
have h₁ : ∀ (k : ι), ⁅e i, ⁅f i, u j⁆⁆ (Sum.inr k) = (|b.cartanMatrix i j| • u i) (Sum.inr k)
Tactic: ext (k | k)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : DecidableEq ι
inst_10 : Fintype ι
⊢ IsLieAbelian ↥(cartanSubalgebra b)
have rw : ∀ (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R),
  Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range h) x →
    ∀ (y : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R),
      Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range h) y → ⁅x, y⁆ = 0
Tactic: rw [cartanSubalgebra_eq_lieSpan, LieSubalgebra.isLieAbelian_lieSpan_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : DecidableEq ι
inst_10 : Fintype ι
⊢ IsLieAbelian ↥(cartanSubalgebra' b)
have refine : ∀ (x x : ↥(cartanSubalgebra' b)) (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
  (hx :
    Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b) x)
  (hx' :
    Membership.mem (γ := LieSubalgebra R ↥(lieAlgebra b)) (cartanSubalgebra' b)
      (Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) ↦
        Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
          (lieAlgebra b) x)
        x hx))
  (y : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
  (hy :
    Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b) y)
  (hy' :
    Membership.mem (γ := LieSubalgebra R ↥(lieAlgebra b)) (cartanSubalgebra' b)
      (Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) ↦
        Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
          (lieAlgebra b) x)
        y hy)),
  ⁅Subtype.mk (p := fun (x : ↥(lieAlgebra b)) ↦
        Membership.mem (γ := LieSubalgebra R ↥(lieAlgebra b)) (cartanSubalgebra' b) x)
        (Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) ↦
          Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
            (lieAlgebra b) x)
          x hx)
        hx',
      Subtype.mk (p := fun (x : ↥(lieAlgebra b)) ↦
        Membership.mem (γ := LieSubalgebra R ↥(lieAlgebra b)) (cartanSubalgebra' b) x)
        (Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) ↦
          Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
            (lieAlgebra b) x)
          y hy)
        hy'⁆ =
    0
Tactic: refine ⟨fun ⟨⟨x, hx⟩, hx'⟩ ⟨⟨y, hy⟩, hy'⟩ ↦ ?_⟩