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 : Fintype ι
i j : ↥b.support
⊢ ⁅h i, h j⁆ = 0

Tactic:
simpa only [h_eq_diagonal, ← commute_iff_lie_eq] using Matrix.commute_diagonal _ _

Premises used: Matrix.commute_diagonal, RootPairing.GeckConstruction.h_eq_diagonal, commute_iff_lie_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 : Fintype ι
i j : ↥b.support
⊢ ⁅h i, h j⁆ = 0

Tactic:
classical
  simpa only [h_eq_diagonal, ← commute_iff_lie_eq] using Matrix.commute_diagonal _ _

Premises used: Matrix.commute_diagonal, RootPairing.GeckConstruction.h_eq_diagonal, commute_iff_lie_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 : Fintype ι
inst_10 : DecidableEq ι
x y : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx :
  Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (toAddSubmonoid (span R (range h))))) x
hy :
  Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (toAddSubmonoid (span R (range h))))) y
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 : Fintype ι
inst_10 : DecidableEq ι
x y : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx :
  Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (toAddSubmonoid (span R (range h))))) x
hy :
  Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (toAddSubmonoid (span R (range h))))) y
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 : Fintype ι
inst_10 : DecidableEq ι
x y : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx :
  Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (toAddSubmonoid (span R (range h))))) x
hy :
  Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (toAddSubmonoid (span R (range h))))) y
⊢ ∀ (u : 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) u →
      ∀ (v : 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) v → ⁅u, v⁆ = 0

Tactic:
have aux : (∀ u ∈ range (h (b := b)), ∀ v ∈ range (h (b := b)), ⁅u, v⁆ = 0) := by
      rintro - ⟨i, rfl⟩ - ⟨j, rfl⟩; exact lie_h_h i j
-- 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 ι
inst_10 : DecidableEq ι
x y : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx :
  Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (toAddSubmonoid (span R (range h))))) x
hy :
  Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (toAddSubmonoid (span R (range h))))) y
aux :
  ∀ (u : 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) u →
      ∀ (v : 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) v → ⁅u, v⁆ = 0
simp :
  ∀
    (hx :
      Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
        (LieSubalgebra.lieSpan R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (range h)) x)
    (hy :
      Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
        (LieSubalgebra.lieSpan R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (range h)) y),
    Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
      (LieSubalgebra.lieSpan R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (range h)) ⁅x, y⁆
⊢ Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (toAddSubmonoid (span R (range h))))) ⁅x, y⁆

Tactic:
simp only [Submodule.carrier_eq_coe, SetLike.mem_coe, LieSubalgebra.mem_toSubmodule,
      ← LieSubalgebra.coe_lieSpan_eq_span_of_forall_lie_eq_zero (R := R) aux] at hx hy ⊢

Premises used: LieSubalgebra.mem_toSubmodule, LieSubalgebra.coe_lieSpan_eq_span_of_forall_lie_eq_zero, SetLike.mem_coe, Submodule.carrier_eq_coe
-- 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 ι
inst_10 : DecidableEq ι
x y : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
aux :
  ∀ (u : 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) u →
      ∀ (v : 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) v → ⁅u, v⁆ = 0
hx :
  Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
    (LieSubalgebra.lieSpan R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (range h)) x
hy :
  Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
    (LieSubalgebra.lieSpan R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (range h)) y
⊢ Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
    (LieSubalgebra.lieSpan R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (range h)) ⁅x, y⁆

Tactic:
LieSubalgebra.lie_mem _ hx hy

Premises used: LieSubalgebra.lie_mem
-- 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 ι
inst_10 : DecidableEq ι
x y : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
aux :
  ∀ (u : 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) u →
      ∀ (v : 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) v → ⁅u, v⁆ = 0
hx :
  Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
    (LieSubalgebra.lieSpan R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (range h)) x
hy :
  Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
    (LieSubalgebra.lieSpan R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (range h)) y
⊢ Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
    (LieSubalgebra.lieSpan R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (range h)) ⁅x, y⁆

Tactic:
exact LieSubalgebra.lie_mem _ hx hy

Premises used: LieSubalgebra.lie_mem
-- 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 : Fintype ι
inst_7 : DecidableEq ι
⊢ Eq (α := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (cartanSubalgebra b)
    (LieSubalgebra.lieSpan R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (range h))

Tactic:
le_antisymm LieSubalgebra.submodule_span_le_lieSpan ?_

Premises used: LieSubalgebra.submodule_span_le_lieSpan, le_antisymm
-- 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 : Fintype ι
inst_7 : DecidableEq ι
refine :
  LE.le (α := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
    (LieSubalgebra.lieSpan R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (range h))
    (cartanSubalgebra b)
⊢ Eq (α := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (cartanSubalgebra b)
    (LieSubalgebra.lieSpan R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (range h))

Tactic:
refine le_antisymm LieSubalgebra.submodule_span_le_lieSpan ?_

Premises used: LieSubalgebra.submodule_span_le_lieSpan, le_antisymm
-- 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 : Fintype ι
inst_7 : DecidableEq ι
rw :
  range h ⊆
    (↑{ toSubmodule := span R (range h), lie_mem' := ⋯ :
          LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) } :
      Set (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
⊢ LE.le (α := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
    (LieSubalgebra.lieSpan R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (range h))
    (cartanSubalgebra b)

Tactic:
rw [LieSubalgebra.lieSpan_le, cartanSubalgebra]

Premises used: RootPairing.GeckConstruction.cartanSubalgebra, LieSubalgebra.lieSpan_le
-- 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 : Fintype ι
inst_7 : DecidableEq ι
⊢ range h ⊆
    (↑{ toSubmodule := span R (range h), lie_mem' := ⋯ :
          LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) } :
      Set (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))

Tactic:
Submodule.subset_span

Premises used: Set.Mem, setOf, Submodule.subset_span
-- 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 : Fintype ι
inst_7 : DecidableEq ι
⊢ range h ⊆
    (↑{ toSubmodule := span R (range h), lie_mem' := ⋯ :
          LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) } :
      Set (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))

Tactic:
exact Submodule.subset_span

Premises used: Submodule.subset_span
-- 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 : Fintype ι
inst_7 : DecidableEq ι
i : ↥b.support
⊢ Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
    (cartanSubalgebra b) (h i)

Tactic:
Submodule.subset_span <| mem_range_self i

Premises used: Set.mem_range_self, Set.Mem, setOf, Submodule.subset_span
-- 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 ι
inst_10 : DecidableEq ι
i : ↥b.support
hi :
  Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b)
    (h i)
⊢ 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)
      (h i) hi)

Tactic:
simp [cartanSubalgebra']

Premises used: RootPairing.GeckConstruction.cartanSubalgebra'
-- 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 ι
inst_10 : DecidableEq ι
i : ↥b.support
⊢ Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range h ∪ range e ∪ range f)
    (h i)

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
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
⊢ Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range h ∪ range e ∪ range f)
    (e i)

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
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : Fintype ι
inst_10 : DecidableEq ι
i : ↥b.support
⊢ Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range h ∪ range e ∪ range f)
    (f i)

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
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : Fintype ι
inst_10 : DecidableEq ι
rw : LE.le (α := Submodule R ↥(cartanSubalgebra' b)) ⊤ (span R (range h'))
⊢ Eq (α := Submodule R ↥(cartanSubalgebra' b)) (span R (range h')) ⊤

Tactic:
rw [eq_top_iff]

Premises used: eq_top_iff
-- 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 ι
inst_10 : DecidableEq ι
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
property :
  Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b) x
hx : Membership.mem (γ := Submodule R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (span R (range h)) x
g : ↥(cartanSubalgebra' b) →ₗ[R] Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R :=
  Submodule.subtype (LieSubalgebra.toSubmodule (lieAlgebra b)) ∘ₗ
    Submodule.subtype (LieSubalgebra.toSubmodule (cartanSubalgebra' b))
suffices : x ∈ map g (span R (range h'))
⊢ Membership.mem (γ := Submodule R ↥(cartanSubalgebra' b)) (span R (range h'))
    (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 property)
      hx)

Tactic:
suffices x ∈ (span R (range h')).map g by
    rwa [← SetLike.mem_coe, ← (injective_subtype _).mem_set_image,
        ← (injective_subtype _).mem_set_image, ← image_comp]
-- 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 ι
inst_10 : DecidableEq ι
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
property :
  Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b) x
hx : Membership.mem (γ := Submodule R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (span R (range h)) x
g : ↥(cartanSubalgebra' b) →ₗ[R] Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R :=
  Submodule.subtype (LieSubalgebra.toSubmodule (lieAlgebra b)) ∘ₗ
    Submodule.subtype (LieSubalgebra.toSubmodule (cartanSubalgebra' b))
rwa :
  Membership.mem (γ := Submodule R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
    (span R
      (image (α := ↥(cartanSubalgebra' b))
        (⇑g : (a : ↥(cartanSubalgebra' b)) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (range h')))
    x
rwa₁ rwa₂ rwa₃ rwa₄ :
  Membership.mem (γ := Submodule R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
    (span R
      (range (ι := ↥b.support)
        (comp (β := ↥(cartanSubalgebra' b))
          (⇑g : (a : ↥(cartanSubalgebra' b)) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) h')))
    x
⊢ x ∈ map g (span R (range h'))

Tactic:
rwa [map_span, ← range_comp]

Premises used: Set.range_comp, Submodule.map_span
-- 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 ι
inst_6 : Fintype ι
a : ∀ (k l : ↥b.support), (ω b * ω b) (Sum.inl k) (Sum.inl l) = 1 (Sum.inl k) (Sum.inl l)
a₁ : ∀ (k : ↥b.support) (l : ι), (ω b * ω b) (Sum.inl k) (Sum.inr l) = 1 (Sum.inl k) (Sum.inr l)
a₂ : ∀ (k : ι) (l : ↥b.support), (ω b * ω b) (Sum.inr k) (Sum.inl l) = 1 (Sum.inr k) (Sum.inl l)
a₃ : ∀ (k l : ι), (ω b * ω b) (Sum.inr k) (Sum.inr l) = 1 (Sum.inr k) (Sum.inr l)
⊢ ω b * ω b = 1

Tactic:
ext (k | k) (l | l)
-- 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 ι
inst_6 : Fintype ι
k l : ↥b.support
⊢ (ω b * ω b) (Sum.inl k) (Sum.inl l) = 1 (Sum.inl k) (Sum.inl l)

Tactic:
simp [ω, -indexNeg_neg]

Premises used: RootPairing.GeckConstruction.ω, RootPairing.indexNeg_neg
-- 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 ι
inst_6 : Fintype ι
k : ↥b.support
l : ι
⊢ (ω b * ω b) (Sum.inl k) (Sum.inr l) = 1 (Sum.inl k) (Sum.inr l)

Tactic:
simp [ω, -indexNeg_neg]

Premises used: RootPairing.GeckConstruction.ω, RootPairing.indexNeg_neg
-- 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 ι
inst_6 : Fintype ι
k : ι
l : ↥b.support
⊢ (ω b * ω b) (Sum.inr k) (Sum.inl l) = 1 (Sum.inr k) (Sum.inl l)

Tactic:
simp [ω, -indexNeg_neg]

Premises used: RootPairing.GeckConstruction.ω, RootPairing.indexNeg_neg
-- 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 ι
inst_6 : Fintype ι
k l : ι
⊢ (ω b * ω b) (Sum.inr k) (Sum.inr l) = 1 (Sum.inr k) (Sum.inr l)

Tactic:
simp [ω, -indexNeg_neg]

Premises used: RootPairing.GeckConstruction.ω, RootPairing.indexNeg_neg
-- 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 : CharZero R
inst_7 : Fintype ι
i : ↥b.support
a : ∀ (k l : ↥b.support), (ω b * h i) (Sum.inl k) (Sum.inl l) = (-h i * ω b) (Sum.inl k) (Sum.inl l)
a₁ : ∀ (k : ↥b.support) (l : ι), (ω b * h i) (Sum.inl k) (Sum.inr l) = (-h i * ω b) (Sum.inl k) (Sum.inr l)
a₂ : ∀ (k : ι) (l : ↥b.support), (ω b * h i) (Sum.inr k) (Sum.inl l) = (-h i * ω b) (Sum.inr k) (Sum.inl l)
a₃ : ∀ (k l : ι), (ω b * h i) (Sum.inr k) (Sum.inr l) = (-h i * ω b) (Sum.inr k) (Sum.inr l)
⊢ ω b * h i = -h i * ω b

Tactic:
ext (k | k) (l | l)