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 : DecidableEq ι
inst_10 : Fintype ι
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
t : R
u : 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
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)
⊢ 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) (t • u) :
      Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)

Tactic:
simpa using SMulMemClass.smul_mem _ hu

Premises used: SMulMemClass.smul_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 : 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)
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)
⊢ 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)

Tactic:
rw [LieEquiv.map_lie]

Premises used: LieEquiv.map_lie
-- 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 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)
    (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:
(lieAlgebra b).lie_mem hu hv

Premises used: Set.Mem, RootPairing.GeckConstruction.lieAlgebra, 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 : 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)
    (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:
exact (lieAlgebra b).lie_mem hu hv

Premises used: RootPairing.GeckConstruction.lieAlgebra, LieSubalgebra.lie_mem
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
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))
    ⋯
suffices : ⁅A', ω b *ᵥ x⁆ ∈ N
⊢ 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⁆

Tactic:
suffices ⁅A', ω b *ᵥ x⁆ ∈ N by simpa [A', mul_assoc] using this
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
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))
    ⋯
⊢ ⁅A', ω b *ᵥ x⁆ ∈ N

Tactic:
LieSubmodule.lie_mem _ hx

Premises used: Set.Mem, LieSubmodule.lie_mem
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
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))
    ⋯
⊢ ⁅A', ω b *ᵥ x⁆ ∈ N

Tactic:
exact LieSubmodule.lie_mem _ hx

Premises used: LieSubmodule.lie_mem
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
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)
x : ↥b.support ⊕ ι → R
⊢ x ∈ ωConjLieSubmodule N ↔ ω b *ᵥ x ∈ N

Tactic:
Iff.rfl

Premises used: Multiset.sum, Multiset.foldr, dotProduct, Set.Mem, Iff.rfl, setOf, Set.preimage, Matrix.mulVec, Finset.sum
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
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)
rw : (↑(ωConjLieSubmodule N) : Submodule R (↥b.support ⊕ ι → R)) = ⊤ ↔ N = ⊤
⊢ ωConjLieSubmodule N = ⊤ ↔ N = ⊤

Tactic:
rw [← LieSubmodule.toSubmodule_eq_top]

Premises used: LieSubmodule.toSubmodule_eq_top
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
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)
x : ↥b.support ⊕ ι → R
⊢ (((Matrix.toLin' : (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → (↥b.support ⊕ ι → R) →ₗ[R] ↥b.support ⊕ ι → R)
            (ω b) :
          (↥b.support ⊕ ι → R) →ₗ[R] ↥b.support ⊕ ι → R) :
        (a : ↥b.support ⊕ ι → R) → ↥b.support ⊕ ι → R)
      ((((Matrix.toLin' :
                  (a : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) → (↥b.support ⊕ ι → R) →ₗ[R] ↥b.support ⊕ ι → R)
                (ω b) :
              (↥b.support ⊕ ι → R) →ₗ[R] ↥b.support ⊕ ι → R) :
            (a : ↥b.support ⊕ ι → R) → ↥b.support ⊕ ι → R)
          x :
        ↥b.support ⊕ ι → R) =
    x

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
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))
    ⋯
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 = ⊤
⊢ (↑(ωConjLieSubmodule N) : Submodule R (↥b.support ⊕ ι → R)) = ⊤ ↔ N = ⊤

Tactic:
change e.symm N = ⊤ ↔ _

Premises used: LieSubmodule.toSubmodule, OrderIso.symm, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
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))
    ⋯
⊢ 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:
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
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) ⋯))))
⊢ 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) ⋯))

Tactic:
rw [cartanSubalgebra', cartanSubalgebra_eq_lieSpan, ← LieSubalgebra.comap_lieSpan_range_eq]

Premises used: RootPairing.GeckConstruction.cartanSubalgebra_eq_lieSpan, RootPairing.GeckConstruction.cartanSubalgebra', LieSubalgebra.comap_lieSpan_range_eq
-- 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
⊢ 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) ⋯))))

Tactic:
rfl