awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
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 : ↥b.support
have have₁ have₂ :
  ∀
    (this :
      Eq (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
        ((fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) ↦ x * ω b)
          ((fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) ↦ ω b * x) (ω b * e i)))
        ((fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) ↦ x * ω b)
          ((fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) ↦ ω b * x) (f i * ω b)))),
    ω b * f i = e i * ω b
have₃ : ∀ (this : 1 * e i * ω b = ω b * f i * ω b * ω b), ω b * f i = e i * ω b
⊢ ω b * f i = e i * ω b

Tactic:
classical
  have := congr_arg (· * ω b) (congr_arg (ω b * ·) (ω_mul_e i))
  simp only [← mul_assoc, ω_mul_ω] at this
  simpa [mul_assoc, ω_mul_ω] using this.symm

Premises used: mul_assoc, RootPairing.GeckConstruction.ω_mul_ω
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
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
rw : (e i * f j - f j * e i) * ω b = e i * f j * ω b - f j * e i * ω b
rw₁ rw₂ : 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 = e i * f j * ω b - f j * e i * ω b

Tactic:
rw [Ring.lie_def, sub_mul]

Premises used: sub_mul, Ring.lie_def
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
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
rw : e i * (f j * ω b) - f j * e i * ω b = e i * (f j * ω b) - f j * (e i * ω b)
rw₁ rw₂ : 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 - f j * e i * ω b = e i * (f j * ω b) - f j * (e i * ω b)

Tactic:
rw [mul_assoc, mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
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
rw : e i * (ω b * e j) - f j * (e i * ω b) = e i * (ω b * e j) - f j * (ω b * f i)
rw₁ rw₂ : 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) - f j * (e i * ω b) = e i * (ω b * e j) - f j * (ω b * f i)

Tactic:
rw [← ω_mul_e, ← ω_mul_f]

Premises used: RootPairing.GeckConstruction.ω_mul_e, RootPairing.GeckConstruction.ω_mul_f
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
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
rw : e i * ω b * e j - f j * (ω b * f i) = e i * ω b * e j - f j * ω b * f i
rw₁ rw₂ : e i * ω b * e j - f j * ω b * f i = e i * ω b * e j - f j * ω b * f i
⊢ e i * (ω b * e j) - f j * (ω b * f i) = e i * ω b * e j - f j * ω b * f i

Tactic:
rw [← mul_assoc, ← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
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
rw : e i * ω b * e j - ω b * e j * f i = ω b * f i * e j - ω b * e j * f i
rw₁ rw₂ : ω b * f i * e j - ω b * e j * f i = ω b * f i * e j - ω b * e j * f i
⊢ e i * ω b * e j - f j * ω b * f i = ω b * f i * e j - ω b * e j * f i

Tactic:
rw [← ω_mul_e, ← ω_mul_f]

Premises used: RootPairing.GeckConstruction.ω_mul_e, RootPairing.GeckConstruction.ω_mul_f
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
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
rw : ω b * (f i * e j) - ω b * e j * f i = ω b * (f i * e j) - ω b * (e j * f i)
rw₁ rw₂ : ω b * (f i * e j) - ω b * (e j * f i) = ω b * (f i * e j) - ω b * (e j * f i)
⊢ ω b * f i * e j - ω b * e j * f i = ω b * (f i * e j) - ω b * (e j * f i)

Tactic:
rw [mul_assoc, mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
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⁆

Tactic:
?_
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
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 : ω 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⁆

Tactic:
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⁆ := ?_

Premises used: RootPairing.GeckConstruction.f, HMul.hMul, RootPairing.GeckConstruction.ω, RootPairing.GeckConstruction.e
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
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
rw : ω b * (f i * e j) - ω b * (e j * f i) = -(ω b * (e j * f i)) + ω b * (f i * e j)
⊢ ω b * (f i * e j) - ω b * (e j * f i) = -ω b * ⁅e j, f i⁆

Tactic:
rw [Ring.lie_def, mul_sub, neg_mul, neg_mul, sub_neg_eq_add]

Premises used: mul_sub, Ring.lie_def, neg_mul, sub_neg_eq_add
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
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)) + ω b * (f i * e j)

Tactic:
abel
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
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⁆
calc₇ : ω b * (f i * e j) - ω b * (e j * f i) = -(ω b * (e j * f i)) + ω b * (f i * e j)
⊢ ⁅e i, f j⁆ * ω b = -ω 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

Premises used: RootPairing.GeckConstruction.f, HMul.hMul, mul_sub, RootPairing.GeckConstruction.ω, Ring.lie_def, neg_mul, RootPairing.GeckConstruction.e, sub_neg_eq_add
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
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
mem : ∀ (i : ↥b.support), u i (Sum.inr j) = 0
⊢ x (Sum.inr j) = 0

Tactic:
obtain ⟨i, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
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
i : ↥b.support
⊢ u i (Sum.inr j) = 0

Tactic:
simp [u]

Premises used: RootPairing.GeckConstruction.u
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
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
⊢ Eq.{u_2 + 1} (α := R) (0 (Sum.inr j)) 0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
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 u v : ↥b.support ⊕ ι → R
hx : Membership.mem (γ := Submodule R (↥b.support ⊕ ι → R)) (span R (range GeckConstruction.u)) u
hy : 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:
simp [hu, hv]
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
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
t : R
u : ↥b.support ⊕ ι → R
hx : 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:
simp [hu]
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
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
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
⊢ 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]

Premises used: RootPairing.GeckConstruction.h, RootPairing.GeckConstruction.u, RootPairing.GeckConstruction.v, Submodule.smul, Submodule.zero, Submodule.add, rfl
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
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)
h₁ : ∀ (k : ι), ⁅e i, ⁅f i, u j⁆⁆ (Sum.inr k) = (|b.cartanMatrix i j| • u i) (Sum.inr k)
⊢ ⁅e i, ⁅f i, u j⁆⁆ = |b.cartanMatrix i j| • u i

Tactic:
ext (k | k)
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
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
k : ι
⊢ ⁅e i, ⁅f i, u j⁆⁆ (Sum.inr k) = (|b.cartanMatrix i j| • u i) (Sum.inr k)

Tactic:
simp [e, f, Matrix.mulVec, dotProduct, P.ne_zero]

Premises used: RootPairing.GeckConstruction.f, RootPairing.ne_zero, dotProduct, Matrix.mulVec, RootPairing.GeckConstruction.e
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
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 ι
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
⊢ IsLieAbelian ↥(cartanSubalgebra b)

Tactic:
rw [cartanSubalgebra_eq_lieSpan, LieSubalgebra.isLieAbelian_lieSpan_iff]

Premises used: LieSubalgebra.isLieAbelian_lieSpan_iff, RootPairing.GeckConstruction.cartanSubalgebra_eq_lieSpan
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
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 i, h j⁆ = 0

Tactic:
lie_h_h i j

Premises used: RootPairing.GeckConstruction.lie_h_h
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
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 i, h j⁆ = 0

Tactic:
exact lie_h_h i j

Premises used: RootPairing.GeckConstruction.lie_h_h
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
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)

Tactic:
⟨fun ⟨⟨x, hx⟩, hx'⟩ ⟨⟨y, hy⟩, hy'⟩ ↦ ?_⟩

Premises used: Bracket.bracket, Subtype.mk, LieModule.IsTrivial.mk, _private.0.RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra'.match_1, OfNat.ofNat, Eq
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
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 ι
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
⊢ IsLieAbelian ↥(cartanSubalgebra' b)

Tactic:
refine ⟨fun ⟨⟨x, hx⟩, hx'⟩ ⟨⟨y, hy⟩, hy'⟩ ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
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 ι
x_1 x_2 : ↥(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)
x' : ↥(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))
      (cartanSubalgebra b) x)
    x hx'
y' : ↥(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))
      (cartanSubalgebra b) x)
    y hy'
this : ⁅x', y'⁆ = 0
⊢ ⁅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:
simpa [x', y', Subtype.ext_iff] using this

Premises used: Subtype.ext_iff