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 : DecidableEq ι
d_1 : ι → R
g : Matrix ι ι R →ₗ[R] Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R :=
  { toFun := fromBlocks 0 0 0, map_add' := ⋯, map_smul' := ⋯ }
h₀ :
  Injective (α := ι → R) (β := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
    (Function.comp (β := Matrix ι ι R) (⇑g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
      (⇑(diagonalLinearMap ι R R) : (a : ι → R) → Matrix ι ι R))
d : ι → R
a :
  ∀ (i j : ↥b.support),
    Matrix.diagonal (Sum.elim 0 d) (Sum.inl i) (Sum.inl j) =
      (g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
        ((diagonalLinearMap ι R R : (a : ι → R) → Matrix ι ι R) d) (Sum.inl i) (Sum.inl j)
a₁ :
  ∀ (i : ↥b.support) (j : ι),
    Matrix.diagonal (Sum.elim 0 d) (Sum.inl i) (Sum.inr j) =
      (g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
        ((diagonalLinearMap ι R R : (a : ι → R) → Matrix ι ι R) d) (Sum.inl i) (Sum.inr j)
⊢ Eq (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (Matrix.diagonal (Sum.elim 0 d))
    ((g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
      ((diagonalLinearMap ι R R : (a : ι → R) → Matrix ι ι R) d))
have a₂ : ∀ (i : ι) (j : ↥b.support),
  Matrix.diagonal (Sum.elim 0 d) (Sum.inr i) (Sum.inl j) =
    (g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
      ((diagonalLinearMap ι R R : (a : ι → R) → Matrix ι ι R) d) (Sum.inr i) (Sum.inl j)
Tactic: ext (i | i) (j | j)
-- 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 : DecidableEq ι
d_1 : ι → R
g : Matrix ι ι R →ₗ[R] Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R :=
  { toFun := fromBlocks 0 0 0, map_add' := ⋯, map_smul' := ⋯ }
h₀ :
  Injective (α := ι → R) (β := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
    (Function.comp (β := Matrix ι ι R) (⇑g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
      (⇑(diagonalLinearMap ι R R) : (a : ι → R) → Matrix ι ι R))
d : ι → R
a :
  ∀ (i j : ↥b.support),
    Matrix.diagonal (Sum.elim 0 d) (Sum.inl i) (Sum.inl j) =
      (g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
        ((diagonalLinearMap ι R R : (a : ι → R) → Matrix ι ι R) d) (Sum.inl i) (Sum.inl j)
a₁ :
  ∀ (i : ↥b.support) (j : ι),
    Matrix.diagonal (Sum.elim 0 d) (Sum.inl i) (Sum.inr j) =
      (g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
        ((diagonalLinearMap ι R R : (a : ι → R) → Matrix ι ι R) d) (Sum.inl i) (Sum.inr j)
a₂ :
  ∀ (i : ι) (j : ↥b.support),
    Matrix.diagonal (Sum.elim 0 d) (Sum.inr i) (Sum.inl j) =
      (g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
        ((diagonalLinearMap ι R R : (a : ι → R) → Matrix ι ι R) d) (Sum.inr i) (Sum.inl j)
⊢ Eq (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (Matrix.diagonal (Sum.elim 0 d))
    ((g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
      ((diagonalLinearMap ι R R : (a : ι → R) → Matrix ι ι R) d))
have a₃ : ∀ (i j : ι),
  Matrix.diagonal (n := ↥b.support ⊕ ι) (Sum.elim 0 d) (Sum.inr i) (Sum.inr j) =
    (g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
      ((diagonalLinearMap ι R R : (a : ι → R) → Matrix ι ι R) d) (Sum.inr i) (Sum.inr j)
Tactic: ext (i | i) (j | j)
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (hypothesis)
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 : DecidableEq ι
d : ι → R
g : Matrix ι ι R →ₗ[R] Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R :=
  { toFun := fromBlocks 0 0 0, map_add' := ⋯, map_smul' := ⋯ }
h₀ :
  Injective (α := ι → R) (β := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
    (Function.comp (β := Matrix ι ι R) (⇑g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
      (⇑(diagonalLinearMap ι R R) : (a : ι → R) → Matrix ι ι R))
⊢ Membership.mem (γ := Submodule R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (span R (range h))
      (Matrix.diagonal (Sum.elim 0 d)) ↔
    Membership.mem (γ := Submodule R ((j : ι) → R))
      (span R (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : R))) d
have h₁ : ∀ {d : ι → R},
  Eq (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (Matrix.diagonal (Sum.elim 0 d))
    ((g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
      ((diagonalLinearMap ι R R : (a : ι → R) → Matrix ι ι R) d))
Tactic: have h₁ {d : ι → R} : diagonal (Sum.elim 0 d) = g (diagonalLinearMap ι R R d) := by
    ext (i | i) (j | j) <;> simp [g]
-- 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 : DecidableEq ι
d : ι → R
g : Matrix ι ι R →ₗ[R] Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R :=
  { toFun := fromBlocks 0 0 0, map_add' := ⋯, map_smul' := ⋯ }
h₀ :
  Injective (α := ι → R) (β := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
    (Function.comp (β := Matrix ι ι R) (⇑g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
      (⇑(diagonalLinearMap ι R R) : (a : ι → R) → Matrix ι ι R))
h₁ :
  ∀ {d : ι → R},
    Eq (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (Matrix.diagonal (Sum.elim 0 d))
      ((g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
        ((diagonalLinearMap ι R R : (a : ι → R) → Matrix ι ι R) d))
⊢ Eq (α := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range h)
    (image (α := Matrix ι ι R) (⇑g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
      (image (α := ι → R) (⇑(diagonalLinearMap ι R R) : (a : ι → R) → Matrix ι ι R)
        (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : R))))
have h : ∀ (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R),
  Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range h) x ↔
    Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
      (image (α := Matrix ι ι R) (⇑g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
        (image (α := ι → R) (⇑(diagonalLinearMap ι R R) : (a : ι → R) → Matrix ι ι R)
          (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : R))))
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (hypothesis)
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 : DecidableEq ι
d : ι → R
g : Matrix ι ι R →ₗ[R] Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R :=
  { toFun := fromBlocks 0 0 0, map_add' := ⋯, map_smul' := ⋯ }
h₀ :
  Injective (α := ι → R) (β := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
    (Function.comp (β := Matrix ι ι R) (⇑g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
      (⇑(diagonalLinearMap ι R R) : (a : ι → R) → Matrix ι ι R))
h₁ :
  ∀ {d : ι → R},
    Eq (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (Matrix.diagonal (Sum.elim 0 d))
      ((g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
        ((diagonalLinearMap ι R R : (a : ι → R) → Matrix ι ι R) d))
⊢ Membership.mem (γ := Submodule R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (span R (range h))
      (Matrix.diagonal (Sum.elim 0 d)) ↔
    Membership.mem (γ := Submodule R ((j : ι) → R))
      (span R (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : R))) d
have h₂ : Eq (α := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range h)
  (image (α := Matrix ι ι R) (⇑g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
    (image (α := ι → R) (⇑(diagonalLinearMap ι R R) : (a : ι → R) → Matrix ι ι R)
      (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : R))))
Tactic: have h₂ : range h = g '' (diagonalLinearMap ι R R ''
    (range <| fun (i : b.support) j ↦ (P.pairingIn ℤ j i : R))) := by ext; simp [g, h_def]
-- 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 : DecidableEq ι
d : ι → R
g : Matrix ι ι R →ₗ[R] Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R :=
  { toFun := fromBlocks 0 0 0, map_add' := ⋯, map_smul' := ⋯ }
h₀ :
  Injective (α := ι → R) (β := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
    (Function.comp (β := Matrix ι ι R) (⇑g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
      (⇑(diagonalLinearMap ι R R) : (a : ι → R) → Matrix ι ι R))
h₁ :
  ∀ {d : ι → R},
    Eq (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (Matrix.diagonal (Sum.elim 0 d))
      ((g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
        ((diagonalLinearMap ι R R : (a : ι → R) → Matrix ι ι R) d))
h₂ :
  Eq (α := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range h)
    (image (α := Matrix ι ι R) (⇑g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
      (image (α := ι → R) (⇑(diagonalLinearMap ι R R) : (a : ι → R) → Matrix ι ι R)
        (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : R))))
⊢ Membership.mem (γ := Submodule R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (span R (range h))
      (Matrix.diagonal (Sum.elim 0 d)) ↔
    Membership.mem (γ := Submodule R ((j : ι) → R))
      (span R (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : R))) d
have simp_rw : Membership.mem (α := Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (γ :=
    Submodule R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (span R (range h))
    ((g : (a : Matrix ι ι R) → Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
        ((diagonalLinearMap ι R R : (a : ι → R) → Matrix ι ι R) d) :
      Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) ↔
  Membership.mem (γ := Submodule R ((j : ι) → R))
    (span R (range fun (i : ↥b.support) (j : ι) ↦ (↑(P.pairingIn ℤ j (↑i : ι)) : R))) d
Tactic: simp_rw [h₁, h₂, span_image, ← map_comp, ← comp_apply (f := g), mem_map, LinearMap.coe_comp,
    h₀.eq_iff, exists_eq_right]
-- 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
i : ↥b.support
j : ↥b.support ⊕ ι
x_1 x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
h : Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range GeckConstruction.h) x
⊢ x j (Sum.inl i) = 0
have mem : ∀ (i_1 : ↥b.support), GeckConstruction.h i_1 j (Sum.inl i) = 0
Tactic: obtain ⟨i, rfl⟩ := h
Cleared hypotheses: x, h
-- 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
i_1 : ↥b.support
j : ↥b.support ⊕ ι
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
i : ↥b.support
⊢ h i j (Sum.inl i_1) = 0
have mem : ∀ (val : ↥b.support), h i (Sum.inl val) (Sum.inl i_1) = 0
Tactic: cases j
Cleared hypotheses: j
-- 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
i_1 : ↥b.support
j : ↥b.support ⊕ ι
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
i : ↥b.support
mem : ∀ (val : ↥b.support), h i (Sum.inl val) (Sum.inl i_1) = 0
⊢ h i j (Sum.inl i_1) = 0
have mem₁ : ∀ (val : ι), h i (Sum.inr val) (Sum.inl i_1) = 0
Tactic: cases j
Cleared hypotheses: j
-- 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
i : ↥b.support
j : ↥b.support ⊕ ι
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx : Membership.mem (γ := Submodule R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (span R (range h)) x
⊢ x j (Sum.inl i) = 0
have mem : ∀ (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
  (h : Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range h) x),
  x j (Sum.inl i) = 0
Tactic: induction hx using span_induction with
  | mem x h => obtain ⟨i, rfl⟩ := h; cases j <;> simp [h]
  | zero => simp
  | add u v _ _ hu hv => simp [hu, hv]
  | smul t u _ hu => simp [hu]
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
i : ↥b.support
j : ↥b.support ⊕ ι
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx : Membership.mem (γ := Submodule R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (span R (range h)) x
mem :
  ∀ (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
    (h : Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range h) x),
    x j (Sum.inl i) = 0
⊢ x j (Sum.inl i) = 0
have zero : Eq.{u_2 + 1} (α := R) (0 j (Sum.inl i)) 0
Tactic: induction hx using span_induction with
  | mem x h => obtain ⟨i, rfl⟩ := h; cases j <;> simp [h]
  | zero => simp
  | add u v _ _ hu hv => simp [hu, hv]
  | smul t u _ hu => simp [hu]
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
i : ↥b.support
j : ↥b.support ⊕ ι
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx : Membership.mem (γ := Submodule R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (span R (range h)) x
mem :
  ∀ (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
    (h : Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range h) x),
    x j (Sum.inl i) = 0
zero : Eq.{u_2 + 1} (α := R) (0 j (Sum.inl i)) 0
⊢ x j (Sum.inl i) = 0
have add : ∀ (u v : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R),
  Membership.mem (γ := Submodule R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (span R (range h)) u →
    Membership.mem (γ := Submodule R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (span R (range h))
        v →
      ∀ (hu : u j (Sum.inl i) = 0) (hv : v j (Sum.inl i) = 0), (u + v) j (Sum.inl i) = 0
Tactic: induction hx using span_induction with
  | mem x h => obtain ⟨i, rfl⟩ := h; cases j <;> simp [h]
  | zero => simp
  | add u v _ _ hu hv => simp [hu, hv]
  | smul t u _ hu => simp [hu]
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
i : ↥b.support
j : ↥b.support ⊕ ι
x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx : Membership.mem (γ := Submodule R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (span R (range h)) x
mem :
  ∀ (x : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)
    (h : Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range h) x),
    x j (Sum.inl i) = 0
zero : Eq.{u_2 + 1} (α := R) (0 j (Sum.inl i)) 0
add :
  ∀ (u v : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R),
    Membership.mem (γ := Submodule R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (span R (range h))
        u →
      Membership.mem (γ := Submodule R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (span R (range h))
          v →
        ∀ (hu : u j (Sum.inl i) = 0) (hv : v j (Sum.inl i) = 0), (u + v) j (Sum.inl i) = 0
⊢ x j (Sum.inl i) = 0
have smul : ∀ (t : R) (u : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R),
  Membership.mem (γ := Submodule R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (span R (range h)) u →
    ∀ (hu : u j (Sum.inl i) = 0), (t • u) j (Sum.inl i) = 0
Tactic: induction hx using span_induction with
  | mem x h => obtain ⟨i, rfl⟩ := h; cases j <;> simp [h]
  | zero => simp
  | add u v _ _ hu hv => simp [hu, hv]
  | smul t u _ hu => simp [hu]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
P : RootPairing ι R M N
inst_5 : P.IsCrystallographic
b : P.Base
inst_6 : Finite ι
inst_7 : IsDomain R
inst_8 : CharZero R
inst_9 : Fintype ι
inst_10 : DecidableEq ι
x y : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx :
  Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (toAddSubmonoid (span R (range h))))) x
hy :
  Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (toAddSubmonoid (span R (range h))))) y
⊢ Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (toAddSubmonoid (span R (range h))))) ⁅x, y⁆
have aux : ∀ (u : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R),
  Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range h) u →
    ∀ (v : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R),
      Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range h) v → ⁅u, v⁆ = 0
Tactic: have aux : (∀ u ∈ range (h (b := b)), ∀ v ∈ range (h (b := b)), ⁅u, v⁆ = 0) := by
      rintro - ⟨i, rfl⟩ - ⟨j, rfl⟩; exact lie_h_h i j
-- 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 y : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R
hx :
  Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (toAddSubmonoid (span R (range h))))) x
hy :
  Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (toAddSubmonoid (span R (range h))))) y
aux :
  ∀ (u : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R),
    Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range h) u →
      ∀ (v : Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R),
        Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (range h) v → ⁅u, v⁆ = 0
⊢ Membership.mem (γ := Set (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
    (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (toAddSubmonoid (span R (range h))))) ⁅x, y⁆
have simp : ∀
  (hx :
    Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
      (LieSubalgebra.lieSpan R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (range h)) x)
  (hy :
    Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
      (LieSubalgebra.lieSpan R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (range h)) y),
  Membership.mem (γ := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
    (LieSubalgebra.lieSpan R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (range h)) ⁅x, y⁆
Tactic: simp only [Submodule.carrier_eq_coe, SetLike.mem_coe, LieSubalgebra.mem_toSubmodule,
      ← LieSubalgebra.coe_lieSpan_eq_span_of_forall_lie_eq_zero (R := R) aux] at hx hy ⊢
Cleared hypotheses: hx, hy
-- 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 : Fintype ι
inst_7 : DecidableEq ι
⊢ Eq (α := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R)) (cartanSubalgebra b)
    (LieSubalgebra.lieSpan R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (range h))
have refine : LE.le (α := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
  (LieSubalgebra.lieSpan R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (range h)) (cartanSubalgebra b)
Tactic: refine le_antisymm LieSubalgebra.submodule_span_le_lieSpan ?_
-- 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 : Fintype ι
inst_7 : DecidableEq ι
⊢ LE.le (α := LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
    (LieSubalgebra.lieSpan R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (range h))
    (cartanSubalgebra b)
have rw : range h ⊆
  (↑{ toSubmodule := span R (range h), lie_mem' := sorry :
        LieSubalgebra R (Matrix.{u_1, u_1, u_2} (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) } :
    Set (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R))
Tactic: rw [LieSubalgebra.lieSpan_le, cartanSubalgebra]