awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : Field K
inst_3 : CharZero K
inst_4 : AddCommGroup M
inst_5 : Module K M
inst_6 : AddCommGroup N
inst_7 : Module K N
P : RootPairing ι K M N
inst_8 : P.IsReduced
inst_9 : P.IsCrystallographic
inst_10 : P.IsIrreducible
inst_11 : P.IsRootSystem
b : P.Base
h₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x)
      (h i) ⋯
e₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x)
      (e i) ⋯
f₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x)
      (f i) ⋯
change : Eq (α := LieSubalgebra K ↥(lieAlgebra b)) (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀)) ⊤
⊢ Eq (α := LieSubalgebra K ↥(lieAlgebra b))
    (LieSubalgebra.lieSpan K (↥(lieAlgebra b))
      ((range fun (i : ↥b.support) ↦
          Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
            Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K))
              (lieAlgebra b) x)
            (e i) ⋯) ∪
        range fun (i : ↥b.support) ↦
          Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
            Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K))
              (lieAlgebra b) x)
            (f i) ⋯))
    ⊤

Tactic:
change LieSubalgebra.lieSpan K (lieAlgebra b) (range e₀ ∪ range f₀) = ⊤

Premises used: Membership.mem, RootPairing.GeckConstruction.lieAlgebra, Subtype, LieSubalgebra.lieSpan, Set.range, Union.union
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : Field K
inst_3 : CharZero K
inst_4 : AddCommGroup M
inst_5 : Module K M
inst_6 : AddCommGroup N
inst_7 : Module K N
P : RootPairing ι K M N
inst_8 : P.IsReduced
inst_9 : P.IsCrystallographic
inst_10 : P.IsIrreducible
inst_11 : P.IsRootSystem
b : P.Base
h₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x)
      (h i) ⋯
e₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x)
      (e i) ⋯
f₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x)
      (f i) ⋯
this :
  Eq (α := LieSubalgebra K ↥(lieAlgebra b)) (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀))
    (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range h₀ ∪ range e₀ ∪ range f₀))
⊢ range h₀ ∪ range e₀ ∪ range f₀ =
    Subtype.val (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
        Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K))
          (lieAlgebra b) x) ⁻¹'
      (range h ∪ range e ∪ range f)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : Field K
inst_3 : CharZero K
inst_4 : AddCommGroup M
inst_5 : Module K M
inst_6 : AddCommGroup N
inst_7 : Module K N
P : RootPairing ι K M N
inst_8 : P.IsReduced
inst_9 : P.IsCrystallographic
inst_10 : P.IsIrreducible
inst_11 : P.IsRootSystem
b : P.Base
h₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x)
      (h i) ⋯
e₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x)
      (e i) ⋯
f₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x)
      (f i) ⋯
this :
  Eq (α := LieSubalgebra K ↥(lieAlgebra b)) (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀))
    (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range h₀ ∪ range e₀ ∪ range f₀))
⊢ range h₀ ∪ range e₀ ∪ range f₀ =
    Subtype.val (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
        Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K))
          (lieAlgebra b) x) ⁻¹'
      (range h ∪ range e ∪ range f)

Tactic:
have hr : range h₀ ∪ range e₀ ∪ range f₀ = Subtype.val ⁻¹' (range h ∪ range e ∪ range f) := by
        aesop
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : Field K
inst_3 : CharZero K
inst_4 : AddCommGroup M
inst_5 : Module K M
inst_6 : AddCommGroup N
inst_7 : Module K N
P : RootPairing ι K M N
inst_8 : P.IsReduced
inst_9 : P.IsCrystallographic
inst_10 : P.IsIrreducible
inst_11 : P.IsRootSystem
b : P.Base
h₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x)
      (h i) ⋯
e₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x)
      (e i) ⋯
f₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x)
      (f i) ⋯
this :
  Eq (α := LieSubalgebra K ↥(lieAlgebra b)) (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀))
    (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range h₀ ∪ range e₀ ∪ range f₀))
hr :
  range h₀ ∪ range e₀ ∪ range f₀ =
    Subtype.val (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
        Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K))
          (lieAlgebra b) x) ⁻¹'
      (range h ∪ range e ∪ range f)
rw :
  Eq (α := LieSubalgebra K ↥(lieAlgebra b))
    (LieSubalgebra.lieSpan K (↥(lieAlgebra b))
      (Subtype.val (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
          Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K))
            (lieAlgebra b) x) ⁻¹'
        (range h ∪ range e ∪ range f)))
    ⊤
⊢ Eq (α := LieSubalgebra K ↥(lieAlgebra b)) (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀)) ⊤

Tactic:
rw [this, hr]
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : Field K
inst_3 : CharZero K
inst_4 : AddCommGroup M
inst_5 : Module K M
inst_6 : AddCommGroup N
inst_7 : Module K N
P : RootPairing ι K M N
inst_8 : P.IsReduced
inst_9 : P.IsCrystallographic
inst_10 : P.IsIrreducible
inst_11 : P.IsRootSystem
b : P.Base
h₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x)
      (h i) ⋯
e₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x)
      (e i) ⋯
f₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x)
      (f i) ⋯
this :
  Eq (α := LieSubalgebra K ↥(lieAlgebra b)) (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀))
    (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range h₀ ∪ range e₀ ∪ range f₀))
hr :
  range h₀ ∪ range e₀ ∪ range f₀ =
    Subtype.val (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
        Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K))
          (lieAlgebra b) x) ⁻¹'
      (range h ∪ range e ∪ range f)
⊢ Eq (α := LieSubalgebra K ↥(lieAlgebra b))
    (LieSubalgebra.lieSpan K (↥(lieAlgebra b))
      (Subtype.val (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
          Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K))
            (lieAlgebra b) x) ⁻¹'
        (range h ∪ range e ∪ range f)))
    ⊤

Tactic:
LieSubalgebra.lieSpan_lieSpan_coe_preimage

Premises used: Set.Mem, RootPairing.GeckConstruction.lieAlgebra, LieSubalgebra.lieSpan_lieSpan_coe_preimage
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : Field K
inst_3 : CharZero K
inst_4 : AddCommGroup M
inst_5 : Module K M
inst_6 : AddCommGroup N
inst_7 : Module K N
P : RootPairing ι K M N
inst_8 : P.IsReduced
inst_9 : P.IsCrystallographic
inst_10 : P.IsIrreducible
inst_11 : P.IsRootSystem
b : P.Base
h₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x)
      (h i) ⋯
e₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x)
      (e i) ⋯
f₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x)
      (f i) ⋯
this :
  Eq (α := LieSubalgebra K ↥(lieAlgebra b)) (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀))
    (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range h₀ ∪ range e₀ ∪ range f₀))
hr :
  range h₀ ∪ range e₀ ∪ range f₀ =
    Subtype.val (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
        Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K))
          (lieAlgebra b) x) ⁻¹'
      (range h ∪ range e ∪ range f)
⊢ Eq (α := LieSubalgebra K ↥(lieAlgebra b))
    (LieSubalgebra.lieSpan K (↥(lieAlgebra b))
      (Subtype.val (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
          Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K))
            (lieAlgebra b) x) ⁻¹'
        (range h ∪ range e ∪ range f)))
    ⊤

Tactic:
exact LieSubalgebra.lieSpan_lieSpan_coe_preimage

Premises used: LieSubalgebra.lieSpan_lieSpan_coe_preimage
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : Field K
inst_3 : CharZero K
inst_4 : AddCommGroup M
inst_5 : Module K M
inst_6 : AddCommGroup N
inst_7 : Module K N
P : RootPairing ι K M N
inst_8 : P.IsReduced
inst_9 : P.IsCrystallographic
inst_10 : P.IsIrreducible
inst_11 : P.IsRootSystem
b : P.Base
h₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x)
      (h i) ⋯
e₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x)
      (e i) ⋯
f₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x)
      (f i) ⋯
suffices :
  Eq (α := LieSubalgebra K ↥(lieAlgebra b)) (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀))
    (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range h₀ ∪ range e₀ ∪ range f₀))
⊢ Eq (α := LieSubalgebra K ↥(lieAlgebra b)) (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀)) ⊤

Tactic:
suffices LieSubalgebra.lieSpan K (lieAlgebra b) (range e₀ ∪ range f₀) =
        LieSubalgebra.lieSpan K (lieAlgebra b) (range h₀ ∪ range e₀ ∪ range f₀) by
      have hr : range h₀ ∪ range e₀ ∪ range f₀ = Subtype.val ⁻¹' (range h ∪ range e ∪ range f) := by
        aesop
      rw [this, hr]
      exact LieSubalgebra.lieSpan_lieSpan_coe_preimage
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : Field K
inst_3 : CharZero K
inst_4 : AddCommGroup M
inst_5 : Module K M
inst_6 : AddCommGroup N
inst_7 : Module K N
P : RootPairing ι K M N
inst_8 : P.IsReduced
inst_9 : P.IsCrystallographic
inst_10 : P.IsIrreducible
inst_11 : P.IsRootSystem
b : P.Base
h₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x)
      (h i) ⋯
e₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x)
      (e i) ⋯
f₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x)
      (f i) ⋯
simp :
  Eq (α := LieSubalgebra K ↥(lieAlgebra b)) (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀))
    (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range h₀ ∪ (range e₀ ∪ range f₀)))
⊢ Eq (α := LieSubalgebra K ↥(lieAlgebra b)) (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀))
    (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range h₀ ∪ range e₀ ∪ range f₀))

Tactic:
simp only [union_assoc]

Premises used: Set.union_assoc
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : Field K
inst_3 : CharZero K
inst_4 : AddCommGroup M
inst_5 : Module K M
inst_6 : AddCommGroup N
inst_7 : Module K N
P : RootPairing ι K M N
inst_8 : P.IsReduced
inst_9 : P.IsCrystallographic
inst_10 : P.IsIrreducible
inst_11 : P.IsRootSystem
b : P.Base
h₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x)
      (h i) ⋯
e₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x)
      (e i) ⋯
f₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x)
      (f i) ⋯
⊢ range e₀ ∪ range f₀ ⊆ range h₀ ∪ (range e₀ ∪ range f₀)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : Field K
inst_3 : CharZero K
inst_4 : AddCommGroup M
inst_5 : Module K M
inst_6 : AddCommGroup N
inst_7 : Module K N
P : RootPairing ι K M N
inst_8 : P.IsReduced
inst_9 : P.IsCrystallographic
inst_10 : P.IsIrreducible
inst_11 : P.IsRootSystem
b : P.Base
h₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x)
      (h i) ⋯
e₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x)
      (e i) ⋯
f₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x)
      (f i) ⋯
refine :
  LE.le (α := LieSubalgebra K ↥(lieAlgebra b))
    (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range h₀ ∪ (range e₀ ∪ range f₀)))
    (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀))
⊢ Eq (α := LieSubalgebra K ↥(lieAlgebra b)) (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀))
    (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range h₀ ∪ (range e₀ ∪ range f₀)))

Tactic:
refine le_antisymm (LieSubalgebra.lieSpan_mono <| by simp) ?_

Premises used: LieSubalgebra.lieSpan_mono, le_antisymm
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : Field K
inst_3 : CharZero K
inst_4 : AddCommGroup M
inst_5 : Module K M
inst_6 : AddCommGroup N
inst_7 : Module K N
P : RootPairing ι K M N
inst_8 : P.IsReduced
inst_9 : P.IsCrystallographic
inst_10 : P.IsIrreducible
inst_11 : P.IsRootSystem
b : P.Base
h₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x)
      (h i) ⋯
e₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x)
      (e i) ⋯
f₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x)
      (f i) ⋯
rw :
  range h₀ ∪ (range e₀ ∪ range f₀) ⊆
    (↑(LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀)) : Set ↥(lieAlgebra b))
⊢ LE.le (α := LieSubalgebra K ↥(lieAlgebra b))
    (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range h₀ ∪ (range e₀ ∪ range f₀)))
    (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀))

Tactic:
rw [LieSubalgebra.lieSpan_le]

Premises used: LieSubalgebra.lieSpan_le
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis
Goal:
ι : Type u_1
K : Type u_2
M : Type u_3
N : Type u_4
inst : Fintype ι
inst_1 : DecidableEq ι
inst_2 : Field K
inst_3 : CharZero K
inst_4 : AddCommGroup M
inst_5 : Module K M
inst_6 : AddCommGroup N
inst_7 : Module K N
P : RootPairing ι K M N
inst_8 : P.IsReduced
inst_9 : P.IsCrystallographic
inst_10 : P.IsIrreducible
inst_11 : P.IsRootSystem
b : P.Base
h₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x)
      (h i) ⋯
e₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x)
      (e i) ⋯
f₀ : (i : ↥b.support) → ↥(lieAlgebra b) :=
  fun (i : ↥b.support) ↦
    Subtype.mk (p := fun (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) ↦
      Membership.mem (γ := LieSubalgebra K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)) (lieAlgebra b)
        x)
      (f i) ⋯
⊢ range h₀ ∪ (range e₀ ∪ range f₀) ⊆
    (↑(LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀)) : Set ↥(lieAlgebra b))

Tactic:
union_subset ?_ LieSubalgebra.subset_lieSpan

Premises used: LieSubalgebra.subset_lieSpan, Set.union_subset