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 : Fintype ι
inst_10 : DecidableEq ι
⊢ Eq (α := Submodule R ↥(cartanSubalgebra' b)) (span R (range h')) ⊤
have rw : LE.le (α := Submodule R ↥(cartanSubalgebra' b)) ⊤ (span R (range h'))
Tactic: rw [eq_top_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 : 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))
this : 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)
have rwa : 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 ∈
  (↑(span R (range h')) : Set ↥(cartanSubalgebra' b))
Tactic: rwa [← SetLike.mem_coe, ← (injective_subtype _).mem_set_image,
        ← (injective_subtype _).mem_set_image, ← image_comp]
-- 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 : 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))
this : x ∈ map g (span R (range h'))
rwa :
  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 ∈
    (↑(span R (range h')) : Set ↥(cartanSubalgebra' b))
⊢ 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)
have rwa₁ : Membership.mem (α := ↥(lieAlgebra b)) (γ := Set ↥(lieAlgebra b))
  ((⇑(Submodule.subtype (LieSubalgebra.toSubmodule (cartanSubalgebra' b))) :
      (a : ↥(cartanSubalgebra' b).toSubmodule) → ↥(lieAlgebra b)) ''
    (↑(span R (range h')) : Set ↥(cartanSubalgebra' b)))
  ((Submodule.subtype (LieSubalgebra.toSubmodule (cartanSubalgebra' b)) :
        (a : ↥(cartanSubalgebra' b).toSubmodule) → ↥(lieAlgebra b))
      (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) :
    ↥(lieAlgebra b))
Tactic: rwa [← SetLike.mem_coe, ← (injective_subtype _).mem_set_image,
        ← (injective_subtype _).mem_set_image, ← image_comp]
-- 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 : 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))
⊢ 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)
have suffices : x ∈ map g (span R (range h'))
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]
-- 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 : 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))
⊢ x ∈ map g (span R (range h'))
have 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
Tactic: rwa [map_span, ← range_comp]
-- 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 : 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
⊢ x ∈ map g (span R (range h'))
have 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
Tactic: rwa [map_span, ← range_comp]
-- 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
b : P.Base
inst_5 : DecidableEq ι
inst_6 : Fintype ι
⊢ ω b * ω b = 1
have a : ∀ (k l : ↥b.support), (ω b * ω b) (Sum.inl k) (Sum.inl l) = 1 (Sum.inl k) (Sum.inl l)
Tactic: ext (k | k) (l | l)
-- 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
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)
⊢ ω b * ω b = 1
have a₁ : ∀ (k : ↥b.support) (l : ι), (ω b * ω b) (Sum.inl k) (Sum.inr l) = 1 (Sum.inl k) (Sum.inr l)
Tactic: ext (k | k) (l | l)
-- 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
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)
⊢ ω b * ω b = 1
have a₂ : ∀ (k : ι) (l : ↥b.support), (ω b * ω b) (Sum.inr k) (Sum.inl l) = 1 (Sum.inr k) (Sum.inl l)
Tactic: ext (k | k) (l | l)
-- 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
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)
⊢ ω b * ω b = 1
have a₃ : ∀ (k l : ι), (ω b * ω b) (Sum.inr k) (Sum.inr l) = 1 (Sum.inr k) (Sum.inr l)
Tactic: ext (k | k) (l | l)
-- 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 : CharZero R
inst_7 : Fintype ι
i : ↥b.support
⊢ ω b * h i = -h i * ω b
have a : ∀ (k l : ↥b.support), (ω b * h i) (Sum.inl k) (Sum.inl l) = (-h i * ω b) (Sum.inl k) (Sum.inl l)
Tactic: ext (k | k) (l | l)
-- 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 : 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)
⊢ ω b * h i = -h i * ω b
have a₁ : ∀ (k : ↥b.support) (l : ι), (ω b * h i) (Sum.inl k) (Sum.inr l) = (-h i * ω b) (Sum.inl k) (Sum.inr l)
Tactic: ext (k | k) (l | l)
-- 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 : 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)
⊢ ω b * h i = -h i * ω b
have a₂ : ∀ (k : ι) (l : ↥b.support), (ω b * h i) (Sum.inr k) (Sum.inl l) = (-h i * ω b) (Sum.inr k) (Sum.inl l)
Tactic: ext (k | k) (l | l)
-- 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 : 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)
⊢ ω b * h i = -h i * ω b
have a₃ : ∀ (k l : ι), (ω b * h i) (Sum.inr k) (Sum.inr l) = (-h i * ω b) (Sum.inr k) (Sum.inr l)
Tactic: ext (k | k) (l | l)
-- 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 : CharZero R
inst_7 : Fintype ι
i : ↥b.support
k l : ι
⊢ (ω b * h i) (Sum.inr k) (Sum.inr l) = (-h i * ω b) (Sum.inr k) (Sum.inr l)
have a : HAdd.hAdd (α := R)
    (∑ a₁ : ↥b.support,
      HMul.hMul (α := R)
        (Matrix.fromBlocks (m := ι) (n := ↥b.support) 1 0 0
          ((Matrix.of : (a : ι → ι → R) → Matrix ι ι R) fun (i j : ι) ↦ if i = -j then 1 else 0) (Sum.inr k)
          (Sum.inl a₁))
        (Matrix.fromBlocks (l := ↥b.support) 0 0 0 (Matrix.diagonal fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R))
          (Sum.inl a₁) (Sum.inr l)))
    (∑ x : ι,
      HMul.hMul (α := R) (β := R)
        ((Matrix.of : (a : ι → ι → R) → Matrix ι ι R) (fun (i j : ι) ↦ if i = -j then 1 else 0) k x : R)
        (Matrix.diagonal (fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R)) x l : R)) =
  HAdd.hAdd (α := R)
    (∑ a₁ : ↥b.support,
      HMul.hMul (α := R) (β := R)
        ((-Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R))) (Sum.inr k)
            (Sum.inl a₁) :
          R)
        (Matrix.fromBlocks (l := ↥b.support) (o := ι) 1 0 0
            ((Matrix.of : (a : ι → ι → R) → Matrix ι ι R) fun (i j : ι) ↦ if i = -j then 1 else 0) (Sum.inl a₁)
            (Sum.inr l) :
          R))
    (∑ x : ι,
      HMul.hMul (α := R) (β := R)
        ((-Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun (x : ι) ↦ (↑(P.pairingIn ℤ x (↑i : ι)) : R))) (Sum.inr k)
            (Sum.inr x) :
          R)
        ((Matrix.of : (a : ι → ι → R) → Matrix ι ι R) (fun (i j : ι) ↦ if i = -j then 1 else 0) x l : R))
Tactic: simp only [ω, h, Matrix.mul_apply, Fintype.sum_sum_type, Matrix.fromBlocks_apply₂₂]
-- 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 : CharZero R
inst_7 : Fintype ι
i : ↥b.support
⊢ ω b * h i = -h i * ω b
have a : ∀ (k l : ↥b.support), (ω b * h i) (Sum.inl k) (Sum.inl l) = (-h i * ω b) (Sum.inl k) (Sum.inl l)
Tactic: classical
  ext (k | k) (l | l)
  · simp [ω, h]
  · simp [ω, h]
  · simp [ω, h]
  · simp only [ω, h, Matrix.mul_apply, Fintype.sum_sum_type, Matrix.fromBlocks_apply₂₂]
    aesop
-- 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 : 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)
⊢ ω b * h i = -h i * ω b
have a₁ : ∀ (k : ↥b.support) (l : ι), (ω b * h i) (Sum.inl k) (Sum.inr l) = (-h i * ω b) (Sum.inl k) (Sum.inr l)
Tactic: classical
  ext (k | k) (l | l)
  · simp [ω, h]
  · simp [ω, h]
  · simp [ω, h]
  · simp only [ω, h, Matrix.mul_apply, Fintype.sum_sum_type, Matrix.fromBlocks_apply₂₂]
    aesop
-- 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 : 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)
⊢ ω b * h i = -h i * ω b
have a₂ : ∀ (k : ι) (l : ↥b.support), (ω b * h i) (Sum.inr k) (Sum.inl l) = (-h i * ω b) (Sum.inr k) (Sum.inl l)
Tactic: classical
  ext (k | k) (l | l)
  · simp [ω, h]
  · simp [ω, h]
  · simp [ω, h]
  · simp only [ω, h, Matrix.mul_apply, Fintype.sum_sum_type, Matrix.fromBlocks_apply₂₂]
    aesop
-- 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 : 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)
⊢ ω b * h i = -h i * ω b
have a₃ : ∀ (k l : ι), (ω b * h i) (Sum.inr k) (Sum.inr l) = (-h i * ω b) (Sum.inr k) (Sum.inr l)
Tactic: classical
  ext (k | k) (l | l)
  · simp [ω, h]
  · simp [ω, h]
  · simp [ω, h]
  · simp only [ω, h, Matrix.mul_apply, Fintype.sum_sum_type, Matrix.fromBlocks_apply₂₂]
    aesop
-- 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 : Fintype ι
i : ↥b.support
this : InvolutiveNeg ι := P.indexNeg
⊢ ω b * e i = f i * ω b
have a : ∀ (k l : ↥b.support), (ω b * e i) (Sum.inl k) (Sum.inl l) = (f i * ω b) (Sum.inl k) (Sum.inl l)
Tactic: ext (k | k) (l | l)
-- 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 : Fintype ι
i : ↥b.support
this : InvolutiveNeg ι := P.indexNeg
a : ∀ (k l : ↥b.support), (ω b * e i) (Sum.inl k) (Sum.inl l) = (f i * ω b) (Sum.inl k) (Sum.inl l)
⊢ ω b * e i = f i * ω b
have a₁ : ∀ (k : ↥b.support) (l : ι), (ω b * e i) (Sum.inl k) (Sum.inr l) = (f i * ω b) (Sum.inl k) (Sum.inr l)
Tactic: ext (k | k) (l | l)
-- 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 : Fintype ι
i : ↥b.support
this : InvolutiveNeg ι := P.indexNeg
a : ∀ (k l : ↥b.support), (ω b * e i) (Sum.inl k) (Sum.inl l) = (f i * ω b) (Sum.inl k) (Sum.inl l)
a₁ : ∀ (k : ↥b.support) (l : ι), (ω b * e i) (Sum.inl k) (Sum.inr l) = (f i * ω b) (Sum.inl k) (Sum.inr l)
⊢ ω b * e i = f i * ω b
have a₂ : ∀ (k : ι) (l : ↥b.support), (ω b * e i) (Sum.inr k) (Sum.inl l) = (f i * ω b) (Sum.inr k) (Sum.inl l)
Tactic: ext (k | k) (l | l)
-- 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 : Fintype ι
i : ↥b.support
this : InvolutiveNeg ι := P.indexNeg
a : ∀ (k l : ↥b.support), (ω b * e i) (Sum.inl k) (Sum.inl l) = (f i * ω b) (Sum.inl k) (Sum.inl l)
a₁ : ∀ (k : ↥b.support) (l : ι), (ω b * e i) (Sum.inl k) (Sum.inr l) = (f i * ω b) (Sum.inl k) (Sum.inr l)
a₂ : ∀ (k : ι) (l : ↥b.support), (ω b * e i) (Sum.inr k) (Sum.inl l) = (f i * ω b) (Sum.inr k) (Sum.inl l)
⊢ ω b * e i = f i * ω b
have a₃ : ∀ (k l : ι), (ω b * e i) (Sum.inr k) (Sum.inr l) = (f i * ω b) (Sum.inr k) (Sum.inr l)
Tactic: ext (k | k) (l | l)