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 : DecidableEq ι
inst_10 : Fintype ι
x u : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hu :
  Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range h ∪ range e ∪ range f) u
mem :
  ∀ (i : ↥b.support)
    (hu :
      Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
        (range h ∪ range e ∪ range f) (h i)),
    Membership.mem (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (γ :=
      LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b)
      ((ωConj b : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (h i) :
        Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
mem₁ :
  ∀ (i : ↥b.support)
    (hu :
      Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
        (range h ∪ range e ∪ range f) (e i)),
    Membership.mem (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (γ :=
      LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b)
      ((ωConj b : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (e i) :
        Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
⊢ Membership.mem (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (γ :=
    LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b)
    ((ωConj b : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) u :
      Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
have mem₂ : ∀ (i : ↥b.support)
  (hu :
    Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range h ∪ range e ∪ range f)
      (f i)),
  Membership.mem (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (γ :=
    LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b)
    ((ωConj b : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (f i) :
      Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
Tactic: obtain (⟨i, rfl⟩ | ⟨i, rfl⟩ | ⟨i, rfl⟩) : (∃ j, h j = u) ∨ (∃ j, e j = u) ∨ (∃ j, f j = u) := by
      simpa only [mem_union, mem_range, or_assoc] using hu
Cleared hypotheses: u, hu
-- 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 ι
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
i : ↥b.support
hu :
  Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range h ∪ range e ∪ range f)
    (h i)
⊢ Membership.mem (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (γ :=
    LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b)
    ((ωConj b : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (h i) :
      Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
have mem : Membership.mem (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (γ :=
  LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b)
  (-(ωConj b : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (h i) :
    Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
Tactic: rw [← neg_mem_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 ι
x u v : 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))
    (LieSubalgebra.lieSpan R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (range h ∪ range e ∪ range f))
    u
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 ∪ range e ∪ range f))
    v
hu :
  Membership.mem (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (γ :=
    LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b)
    ((ωConj b : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) u :
      Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
hv :
  Membership.mem (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (γ :=
    LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b)
    ((ωConj b : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) v :
      Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
⊢ Membership.mem (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (γ :=
    LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b)
    ((ωConj b : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) ⁅u, v⁆ :
      Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
have lie : Membership.mem (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (γ :=
  LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b)
  (Bracket.bracket (L := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
      ((ωConj b : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) u :
        Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
      ((ωConj b : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) v) :
    Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
Tactic: rw [LieEquiv.map_lie]
-- 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 ι
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
⊢ Membership.mem (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (γ :=
    LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b)
    ((ωConj b : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) x :
      Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
have mem : ∀ (u : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
  (hu :
    Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range h ∪ range e ∪ range f)
      u),
  Membership.mem (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (γ :=
    LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b)
    ((ωConj b : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) u :
      Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
Tactic: induction hx using LieSubalgebra.lieSpan_induction with
  | mem u hu =>
    obtain (⟨i, rfl⟩ | ⟨i, rfl⟩ | ⟨i, rfl⟩) : (∃ j, h j = u) ∨ (∃ j, e j = u) ∨ (∃ j, f j = u) := by
      simpa only [mem_union, mem_range, or_assoc] using hu
    · rw [← neg_mem_iff]
      exact LieSubalgebra.subset_lieSpan <| by simp [ω_mul_h, mul_assoc]
    · exact LieSubalgebra.subset_lieSpan <| by simp [ω_mul_e, mul_assoc]
    · exact LieSubalgebra.subset_lieSpan <| by simp [ω_mul_f, mul_assoc]
  | zero => simp
  | add u v _ _ hu hv => simpa [mul_add, add_mul] using add_mem hu hv
  | smul t u _ hu => simpa using SMulMemClass.smul_mem _ hu
  | lie u v _ _ hu hv =>
    rw [LieEquiv.map_lie]
    exact (lieAlgebra b).lie_mem hu hv
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 ι
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
mem :
  ∀ (u : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
    (hu :
      Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
        (range h ∪ range e ∪ range f) u),
    Membership.mem (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (γ :=
      LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b)
      ((ωConj b : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) u :
        Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
⊢ Membership.mem (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (γ :=
    LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b)
    ((ωConj b : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) x :
      Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
have zero : Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (lieAlgebra b)
  ((ωConj b : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) 0)
Tactic: induction hx using LieSubalgebra.lieSpan_induction with
  | mem u hu =>
    obtain (⟨i, rfl⟩ | ⟨i, rfl⟩ | ⟨i, rfl⟩) : (∃ j, h j = u) ∨ (∃ j, e j = u) ∨ (∃ j, f j = u) := by
      simpa only [mem_union, mem_range, or_assoc] using hu
    · rw [← neg_mem_iff]
      exact LieSubalgebra.subset_lieSpan <| by simp [ω_mul_h, mul_assoc]
    · exact LieSubalgebra.subset_lieSpan <| by simp [ω_mul_e, mul_assoc]
    · exact LieSubalgebra.subset_lieSpan <| by simp [ω_mul_f, mul_assoc]
  | zero => simp
  | add u v _ _ hu hv => simpa [mul_add, add_mul] using add_mem hu hv
  | smul t u _ hu => simpa using SMulMemClass.smul_mem _ hu
  | lie u v _ _ hu hv =>
    rw [LieEquiv.map_lie]
    exact (lieAlgebra b).lie_mem hu hv
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_1 : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N_1
inst_4 : Module R N_1
P : RootPairing ι R M N_1
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : DecidableEq ι
inst_10 : Fintype ι
N : LieSubmodule R (↥(lieAlgebra b)) (↥b.support ⊕ ι → R)
A : ↥(lieAlgebra b)
x : ↥b.support ⊕ ι → R
hx :
  Membership.mem (γ := Set (↥b.support ⊕ ι → R))
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (toAddSubmonoid (R := R)
          (comap (σ₁₂ := RingHom.id R)
            ((Matrix.toLin' :
                (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → (↥b.support ⊕ ι → R) →ₗ[R] ↥b.support ⊕ ι → R)
              (ω b))
            (↑N : Submodule R (↥b.support ⊕ ι → R))))))
    x
A' : ↥(lieAlgebra 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)
    ((ωConj b : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
      (↑A : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
    ⋯
⊢ Membership.mem (γ := Set (↥b.support ⊕ ι → R))
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (toAddSubmonoid (R := R)
          (comap (σ₁₂ := RingHom.id R)
            ((Matrix.toLin' :
                (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → (↥b.support ⊕ ι → R) →ₗ[R] ↥b.support ⊕ ι → R)
              (ω b))
            (↑N : Submodule R (↥b.support ⊕ ι → R))))))
    ⁅A, x⁆
have suffices : ⁅A', ω b *ᵥ x⁆ ∈ N
Tactic: suffices ⁅A', ω b *ᵥ x⁆ ∈ N by simpa [A', mul_assoc] using this
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N_1 : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N_1
inst_4 : Module R N_1
P : RootPairing ι R M N_1
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : DecidableEq ι
inst_10 : Fintype ι
N : LieSubmodule R (↥(lieAlgebra b)) (↥b.support ⊕ ι → R)
⊢ ωConjLieSubmodule N = ⊤ ↔ N = ⊤
have rw : (↑(ωConjLieSubmodule N) : Submodule R (↥b.support ⊕ ι → R)) = ⊤ ↔ N = ⊤
Tactic: rw [← LieSubmodule.toSubmodule_eq_top]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N_1 : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N_1
inst_4 : Module R N_1
P : RootPairing ι R M N_1
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : DecidableEq ι
inst_10 : Fintype ι
N : LieSubmodule R (↥(lieAlgebra b)) (↥b.support ⊕ ι → R)
e : Submodule R (↥b.support ⊕ ι → R) ≃o Submodule R (↥b.support ⊕ ι → R) :=
  orderIsoMapComapOfBijective (σ₁₂ := RingHom.id R)
    ((Matrix.toLin' : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → (↥b.support ⊕ ι → R) →ₗ[R] ↥b.support ⊕ ι → R)
      (ω b))
    ⋯
⊢ (↑(ωConjLieSubmodule N) : Submodule R (↥b.support ⊕ ι → R)) = ⊤ ↔ N = ⊤
have change : Eq (α := Submodule R (↥b.support ⊕ ι → R))
    ((e.symm : (a : Submodule R (↥b.support ⊕ ι → R)) → Submodule R (↥b.support ⊕ ι → R))
        (↑N : Submodule R (↥b.support ⊕ ι → R)) :
      Submodule R (↥b.support ⊕ ι → R))
    (⊤ : Submodule R (↥b.support ⊕ ι → R)) ↔
  N = ⊤
Tactic: change e.symm N = ⊤ ↔ _
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis (goal)
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
⊢ Eq (α := LieSubalgebra K ↥(lieAlgebra b)) (cartanSubalgebra' 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)
          (h i) ⋯))
have rw : Eq (α := LieSubalgebra K ↥(lieAlgebra b))
  (LieSubalgebra.comap (LieSubalgebra.incl (lieAlgebra b))
    (LieSubalgebra.lieSpan K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K) (range h)))
  (LieSubalgebra.comap (LieSubalgebra.incl (lieAlgebra b))
    (LieSubalgebra.lieSpan K (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) K)
      (range (ι := ↥b.support)
        (Function.comp (β := ↥(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))
          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) sorry))))
Tactic: rw [cartanSubalgebra', cartanSubalgebra_eq_lieSpan, ← LieSubalgebra.comap_lieSpan_range_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis (hypothesis)
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₀))
⊢ Eq (α := LieSubalgebra K ↥(lieAlgebra b)) (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀)) ⊤
have 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)
Tactic: have hr : range h₀ ∪ range e₀ ∪ range f₀ = Subtype.val ⁻¹' (range h ∪ range e ∪ range f) := by
        aesop
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis (goal)
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)) (range e₀ ∪ range f₀)) ⊤
have 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)))
  ⊤
Tactic: rw [this, hr]
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis (goal)
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) ⋯
⊢ Eq (α := LieSubalgebra K ↥(lieAlgebra b)) (LieSubalgebra.lieSpan K (↥(lieAlgebra b)) (range e₀ ∪ range f₀)) ⊤
have 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₀))
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