awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Basic (hypothesis)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieAlgebra ℚ L
D : LieDerivation R L L
h : IsNilpotent (↑D : L →ₗ[R] L)
_i : NonUnitalNonAssocRing L := LieRing.toNonUnitalNonAssocRing L
this : SMulCommClass R L L
⊢ ∀ {x y : L},
    (IsNilpotent.exp (↑D : L →ₗ[R] L)).toFun ⁅x, y⁆ =
      ⁅(IsNilpotent.exp (↑D : L →ₗ[R] L)).toFun x, (IsNilpotent.exp (↑D : L →ₗ[R] L)).toFun y⁆
have this₁ : IsScalarTower R L L
Tactic: have : IsScalarTower R L L := LieAlgebra.isScalarTower R L
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Killing (goal)
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
⊢ Eq (α := LinearMap.BilinForm.{u_1, u_2} R ↥(LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    (LinearMap.BilinForm.restrict (killingForm R (LieDerivation R L L))
      (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    (killingForm R ↥(LieHom.range (ad R L)))
have rw : Eq (α :=
  LinearMap.BilinForm.{u_1, u_2} R
    ↥(LieSubalgebra.toSubmodule (LieIdeal.toLieSubalgebra R (LieDerivation R L L) (LieHom.idealRange (ad R L)))))
  (killingForm R ↥(LieHom.idealRange (ad R L)) : LinearMap.BilinForm.{u_1, u_2} R ↥(LieHom.idealRange (ad R L)))
  (killingForm R ↥(LieIdeal.toLieSubalgebra R (LieDerivation R L L) (LieHom.idealRange (ad R L))))
Tactic: rw [← (ad_isIdealMorphism R L).eq, ← LieIdeal.killingForm_eq]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Killing (hypothesis)
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x : L
D : LieDerivation R L L
hD :
  Membership.mem (γ := Set (LieDerivation R L L))
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid
          (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
            (LieSubalgebra.toSubmodule (LieHom.range (ad R L)))))))
    D
⊢ Membership.mem (γ := Set (LieDerivation R L L))
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid
          (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
            (LieSubalgebra.toSubmodule (LieHom.range (ad R L)))))))
    ⁅x, D⁆
have this : Eq (α := Submodule R (LieDerivation R L L))
  (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
    (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
  (LieSubalgebra.toSubmodule
    (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
      (LieIdeal.killingCompl R (LieDerivation R L L) (LieHom.idealRange (ad R L)))))
Tactic: have : 𝕀ᗮ = (ad R L).idealRange.killingCompl := by simp [← (ad_isIdealMorphism R L).eq]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Killing (hypothesis)
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x : L
D : LieDerivation R L L
hD :
  Membership.mem (γ := Set (LieDerivation R L L))
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid
          (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
            (LieSubalgebra.toSubmodule (LieHom.range (ad R L)))))))
    D
this :
  Eq (α := Submodule R (LieDerivation R L L))
    (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
      (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    (LieSubalgebra.toSubmodule
      (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
        (LieIdeal.killingCompl R (LieDerivation R L L) (LieHom.idealRange (ad R L)))))
⊢ Membership.mem (γ := Set (LieDerivation R L L))
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid
          (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
            (LieSubalgebra.toSubmodule (LieHom.range (ad R L)))))))
    ⁅x, D⁆
have hD₁ : Membership.mem (γ := Submodule R (LieDerivation R L L))
  (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
    (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
  D
Tactic: change D ∈ 𝕀ᗮ at hD
Cleared hypotheses: hD
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Killing (goal)
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x : L
D : LieDerivation R L L
this :
  Eq (α := Submodule R (LieDerivation R L L))
    (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
      (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    (LieSubalgebra.toSubmodule
      (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
        (LieIdeal.killingCompl R (LieDerivation R L L) (LieHom.idealRange (ad R L)))))
hD :
  Membership.mem (γ := Submodule R (LieDerivation R L L))
    (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
      (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    D
⊢ Membership.mem (γ := Submodule R (LieDerivation R L L))
    (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
      (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    ⁅x, D⁆
have rw : ∀
  (hD :
    Membership.mem (γ := Submodule R (LieDerivation R L L))
      (LieSubalgebra.toSubmodule
        (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
          (LieIdeal.killingCompl R (LieDerivation R L L) (LieHom.idealRange (ad R L)))))
      D),
  Membership.mem (γ := Submodule R (LieDerivation R L L))
    (LieSubalgebra.toSubmodule
      (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
        (LieIdeal.killingCompl R (LieDerivation R L L) (LieHom.idealRange (ad R L)))))
    ⁅x, D⁆
Tactic: rw [this] at hD ⊢
Cleared hypotheses: hD
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Killing (goal)
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x : L
D : LieDerivation R L L
this :
  Eq (α := Submodule R (LieDerivation R L L))
    (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
      (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    (LieSubalgebra.toSubmodule
      (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
        (LieIdeal.killingCompl R (LieDerivation R L L) (LieHom.idealRange (ad R L)))))
hD :
  Membership.mem (γ := Submodule R (LieDerivation R L L))
    (LieSubalgebra.toSubmodule
      (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
        (LieIdeal.killingCompl R (LieDerivation R L L) (LieHom.idealRange (ad R L)))))
    D
⊢ Membership.mem (γ := Submodule R (LieDerivation R L L))
    (LieSubalgebra.toSubmodule
      (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
        (LieIdeal.killingCompl R (LieDerivation R L L) (LieHom.idealRange (ad R L)))))
    ⁅x, D⁆
have rw : Membership.mem (γ := Submodule R (LieDerivation R L L))
  (LieSubalgebra.toSubmodule
    (LieIdeal.toLieSubalgebra R (LieDerivation R L L)
      (LieIdeal.killingCompl R (LieDerivation R L L) (LieHom.idealRange (ad R L)))))
  (Bracket.bracket (L := LieDerivation R L L) ((ad R L : (a : L) → LieDerivation R L L) x : LieDerivation R L L) D)
Tactic: rw [← lie_ad]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Killing (goal)
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
D : LieDerivation R L L
hD :
  Membership.mem (γ := Submodule R (LieDerivation R L L))
    (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
      (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    D
x : L
⊢ Membership.mem (α := LieDerivation R L L) (γ := Submodule R (LieDerivation R L L))
    (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
      (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    ((ad R L : (a : L) → LieDerivation R L L) ((D : (a : L) → L) x : L) : LieDerivation R L L)
have simp : Membership.mem (γ := Submodule R (LieDerivation R L L))
  (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
    (LinearMap.range (↑(ad R L) : L →ₗ[R] LieDerivation R L L)))
  ⁅x, D⁆
Tactic: simp only [ad_apply_lieDerivation, LieHom.range_toSubmodule, neg_mem_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Killing (goal)
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
D : LieDerivation R L L
hD :
  Membership.mem (γ := Submodule R (LieDerivation R L L))
    (LinearMap.BilinForm.orthogonal (killingForm R (LieDerivation R L L))
      (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    D
x : L
⊢ Membership.mem (α := LieDerivation R L L) (γ := Submodule R (LieDerivation R L L))
    (Submodule.map (M := ↥(LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
      (Submodule.subtype (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
      (LinearMap.ker (killingForm R ↥(LieHom.range (ad R L)))))
    ((ad R L : (a : L) → LieDerivation R L L) ((D : (a : L) → L) x : L) : LieDerivation R L L)
have rw : Membership.mem (α := LieDerivation R L L) (γ := Submodule R (LieDerivation R L L))
  (Submodule.map (M := ↥(LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    (Submodule.subtype (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    (LinearMap.ker
      (LinearMap.BilinForm.restrict (killingForm R (LieDerivation R L L))
        (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))))
  ((ad R L : (a : L) → LieDerivation R L L) ((D : (a : L) → L) x : L) : LieDerivation R L L)
Tactic: rw [← killingForm_restrict_range_ad]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Killing (goal)
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : LieAlgebra.IsKilling R L
x : L
⊢ Eq (α := LieDerivation R L L) ((ad R L : (a : L) → LieDerivation R L L) x : LieDerivation R L L)
      (0 : LieDerivation R L L) ↔
    x = 0
have refine : ∀
  (h :
    Eq (α := LieDerivation R L L) ((ad R L : (a : L) → LieDerivation R L L) x : LieDerivation R L L)
      (0 : LieDerivation R L L)),
  x = 0
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Killing (goal)
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : LieAlgebra.IsKilling R L
x : L
h :
  Eq (α := LieDerivation R L L) ((ad R L : (a : L) → LieDerivation R L L) x : LieDerivation R L L)
    (0 : LieDerivation R L L)
⊢ x = 0
have rwa : ∀ (h : Membership.mem (γ := LieIdeal R L) (LieHom.ker (ad R L)) x), x = 0
Tactic: rwa [← LieHom.mem_ker, ad_ker_eq_center, LieAlgebra.center_eq_bot, LieSubmodule.mem_bot] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Killing (goal)
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : LieAlgebra.IsKilling R L
x : L
h :
  Eq (α := LieDerivation R L L) ((ad R L : (a : L) → LieDerivation R L L) x : LieDerivation R L L)
    (0 : LieDerivation R L L)
rwa : ∀ (h : Membership.mem (γ := LieIdeal R L) (LieHom.ker (ad R L)) x), x = 0
⊢ x = 0
have rwa₁ : ∀ (h : Membership.mem (γ := LieIdeal R L) (LieAlgebra.center R L) x), x = 0
Tactic: rwa [← LieHom.mem_ker, ad_ker_eq_center, LieAlgebra.center_eq_bot, LieSubmodule.mem_bot] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Killing (goal)
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : LieAlgebra.IsKilling R L
x : L
h :
  Eq (α := LieDerivation R L L) ((ad R L : (a : L) → LieDerivation R L L) x : LieDerivation R L L)
    (0 : LieDerivation R L L)
rwa : ∀ (h : Membership.mem (γ := LieIdeal R L) (LieHom.ker (ad R L)) x), x = 0
rwa₁ : ∀ (h : Membership.mem (γ := LieIdeal R L) (LieAlgebra.center R L) x), x = 0
⊢ x = 0
have rwa₂ : ∀ (h : Membership.mem (γ := LieIdeal R L) ⊥ x), x = 0
Tactic: rwa [← LieHom.mem_ker, ad_ker_eq_center, LieAlgebra.center_eq_bot, LieSubmodule.mem_bot] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Killing (goal)
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : LieAlgebra.IsKilling R L
x : L
h :
  Eq (α := LieDerivation R L L) ((ad R L : (a : L) → LieDerivation R L L) x : LieDerivation R L L)
    (0 : LieDerivation R L L)
rwa : ∀ (h : Membership.mem (γ := LieIdeal R L) (LieHom.ker (ad R L)) x), x = 0
rwa₁ : ∀ (h : Membership.mem (γ := LieIdeal R L) (LieAlgebra.center R L) x), x = 0
rwa₂ : ∀ (h : Membership.mem (γ := LieIdeal R L) ⊥ x), x = 0
⊢ x = 0
have rwa₃ : ∀ (h : x = 0), x = 0
Tactic: rwa [← LieHom.mem_ker, ad_ker_eq_center, LieAlgebra.center_eq_bot, LieSubmodule.mem_bot] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Killing (goal)
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : LieAlgebra.IsKilling R L
⊢ LinearMap.BilinForm.Nondegenerate (M := ↥(LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    (LinearMap.BilinForm.restrict (killingForm R (LieDerivation R L L))
      (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
have h : ↥(LieSubalgebra.toSubmodule (LieHom.range (ad R L))) = ↥(LieHom.range (ad R L)) →
  HEq (α := AddCommMonoid ↥(LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
      (Submodule.addCommMonoid (LieSubalgebra.toSubmodule (LieHom.range (ad R L)))) (β :=
      AddCommMonoid ↥(LieHom.range (ad R L))) AddCommGroup.toAddCommMonoid →
    HEq (α := Module.{u_1, u_2} R ↥(LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
        (Submodule.module (LieSubalgebra.toSubmodule (LieHom.range (ad R L)))) (β :=
        Module.{u_1, u_2} R ↥(LieHom.range (ad R L))) LieAlgebra.toModule →
      Eq (α := LinearMap.BilinForm.{u_1, u_2} R ↥(LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
        (LinearMap.BilinForm.restrict (killingForm R (LieDerivation R L L))
          (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
        (killingForm R ↥(LieHom.range (ad R L)))
Tactic: convert! LieAlgebra.IsKilling.killingForm_nondegenerate R 𝕀
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Killing (goal)
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : LieAlgebra.IsKilling R L
⊢ Eq (α := LieSubalgebra R (LieDerivation R L L)) (LieHom.range (ad R L)) ⊤
have rw : Eq (α := Submodule R (LieDerivation R L L)) (LieSubalgebra.toSubmodule (LieHom.range (ad R L)))
  (LieSubalgebra.toSubmodule ⊤)
Tactic: rw [← LieSubalgebra.toSubmodule_inj]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Killing (goal)
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : LieAlgebra.IsKilling R L
⊢ Eq (α := Submodule R (LieDerivation R L L)) (LieSubalgebra.toSubmodule (LieHom.range (ad R L)))
    (LieSubalgebra.toSubmodule ⊤)
have apply : Eq (α := Submodule R (LieDerivation R L L))
  (LinearMap.BilinForm.orthogonal (LieModule.traceForm R (LieDerivation R L L) (LieDerivation R L L))
    (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
  ⊥
Tactic: apply LinearMap.BilinForm.eq_top_of_restrict_nondegenerate_of_orthogonal_eq_bot
    (LieModule.traceForm_isSymm R 𝔻 𝔻).isRefl (killingForm_restrict_range_ad_nondegenerate R L)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Killing (goal)
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : LieAlgebra.IsKilling R L
⊢ Eq (α := Submodule R (LieDerivation R L L))
    (LinearMap.BilinForm.orthogonal (LieModule.traceForm R (LieDerivation R L L) (LieDerivation R L L))
      (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
    ⊥
have refine : ∀ (D : LieDerivation R L L)
  (hD :
    Membership.mem (γ := Submodule R (LieDerivation R L L))
      (LinearMap.BilinForm.orthogonal (LieModule.traceForm R (LieDerivation R L L) (LieDerivation R L L))
        (LieSubalgebra.toSubmodule (LieHom.range (ad R L))))
      D)
  (x : L), Eq (α := L) ((D : (a : L) → L) x : L) ((0 : (a : L) → L) x : L)
Tactic: refine (Submodule.eq_bot_iff _).mpr fun D hD ↦ ext fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.Derivation.Killing (goal)
Goal:
R : Type u_1
L : Type u_2
inst : Field R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Module.Finite R L
inst_4 : LieAlgebra.IsKilling R L
D : LieDerivation R L L
⊢ Membership.mem (γ := LieSubalgebra R (LieDerivation R L L)) (LieHom.range (ad R L)) D
have rw : Membership.mem (γ := LieSubalgebra R (LieDerivation R L L)) ⊤ D
Tactic: rw [range_ad_eq_top R L]
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : Type w₁
M : ι → Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : (i : ι) → AddCommGroup (M i)
inst_4 : (i : ι) → Module.{u, w} R (M i)
inst_5 : (i : ι) → LieRingModule.{w₁, w} L (M i)
inst_6 : ∀ (i : ι), LieModule.{u, w₁, w} R L (M i)
x y : L
m : ⨁ (i : ι), M i
⊢ mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅x + y, m'⁆) ⋯ m =
    HAdd.hAdd (α := ⨁ (i : ι), M i)
      (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅x, m'⁆) ⋯ m)
      (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x : ι) (m' : M x) ↦ ⁅y, m'⁆) ⋯ m)
have w : ∀ (i : ι),
  (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅x + y, m'⁆) sorry m : (a : ι) → M a) i =
    (HAdd.hAdd (α := ⨁ (i : ι), M i)
          (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅x, m'⁆) sorry m)
          (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x : ι) (m' : M x) ↦ ⁅y, m'⁆) sorry m) :
        (a : ι) → M a)
      i
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : Type w₁
M : ι → Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : (i : ι) → AddCommGroup (M i)
inst_4 : (i : ι) → Module.{u, w} R (M i)
inst_5 : (i : ι) → LieRingModule.{w₁, w} L (M i)
inst_6 : ∀ (i : ι), LieModule.{u, w₁, w} R L (M i)
x : L
m n : ⨁ (i : ι), M i
⊢ mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅x, m'⁆) ⋯ (m + n) =
    HAdd.hAdd (α := ⨁ (i : ι), M i)
      (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅x, m'⁆) ⋯ m)
      (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅x, m'⁆) ⋯ n)
have w : ∀ (i : ι),
  (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅x, m'⁆) sorry (m + n) : (a : ι) → M a) i =
    (HAdd.hAdd (α := ⨁ (i : ι), M i)
          (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅x, m'⁆) sorry m)
          (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅x, m'⁆) sorry n) :
        (a : ι) → M a)
      i
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : Type w₁
M : ι → Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : (i : ι) → AddCommGroup (M i)
inst_4 : (i : ι) → Module.{u, w} R (M i)
inst_5 : (i : ι) → LieRingModule.{w₁, w} L (M i)
inst_6 : ∀ (i : ι), LieModule.{u, w₁, w} R L (M i)
x y : L
m : ⨁ (i : ι), M i
⊢ mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅x, m'⁆) ⋯
      (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x : ι) (m' : M x) ↦ ⁅y, m'⁆) ⋯ m) =
    HAdd.hAdd (α := ⨁ (i : ι), M i)
      (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅⁅x, y⁆, m'⁆) ⋯ m)
      (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x : ι) (m' : M x) ↦ ⁅y, m'⁆) ⋯
        (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅x, m'⁆) ⋯ m))
have w : ∀ (i : ι),
  (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅x, m'⁆) sorry
          (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x : ι) (m' : M x) ↦ ⁅y, m'⁆) sorry m) :
        (a : ι) → M a)
      i =
    (HAdd.hAdd (α := ⨁ (i : ι), M i)
          (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅⁅x, y⁆, m'⁆) sorry m)
          (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x : ι) (m' : M x) ↦ ⁅y, m'⁆) sorry
            (mapRange (β₁ := M) (β₂ := fun (i : ι) ↦ M i) (fun (x_1 : ι) (m' : M x_1) ↦ ⁅x, m'⁆) sorry m)) :
        (a : ι) → M a)
      i
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : Type w₁
M : ι → Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : (i : ι) → AddCommGroup (M i)
inst_4 : (i : ι) → Module.{u, w} R (M i)
inst_5 : (i : ι) → LieRingModule.{w₁, w} L (M i)
inst_6 : ∀ (i : ι), LieModule.{u, w₁, w} R L (M i)
t : R
x : L
m : ⨁ (i : ι), M i
⊢ ⁅t • x, m⁆ = t • ⁅x, m⁆
have w : ∀ (i : ι), (⁅t • x, m⁆ : (a : ι) → M a) i = (t • ⁅x, m⁆ : (a : ι) → M a) i
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : Type w₁
M : ι → Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : (i : ι) → AddCommGroup (M i)
inst_4 : (i : ι) → Module.{u, w} R (M i)
inst_5 : (i : ι) → LieRingModule.{w₁, w} L (M i)
inst_6 : ∀ (i : ι), LieModule.{u, w₁, w} R L (M i)
t : R
x : L
m : ⨁ (i : ι), M i
⊢ ⁅x, t • m⁆ = t • ⁅x, m⁆
have w : ∀ (i : ι), (⁅x, t • m⁆ : (a : ι) → M a) i = (t • ⁅x, m⁆ : (a : ι) → M a) i
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : Type w₁
M : ι → Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : (i : ι) → AddCommGroup (M i)
inst_4 : (i : ι) → Module.{u, w} R (M i)
inst_5 : (i : ι) → LieRingModule.{w₁, w} L (M i)
inst_6 : ∀ (i : ι), LieModule.{u, w₁, w} R L (M i)
inst_7 : DecidableEq ι
j : ι
x : L
m : M j
⊢ Eq (α := ⨁ (i : ι), M i) (AddHom.toFun (LinearMap.toAddHom (lof R ι M j)) ⁅x, m⁆)
    ⁅x, AddHom.toFun (LinearMap.toAddHom (lof R ι M j)) m⁆
have w : ∀ (i : ι),
  (AddHom.toFun (LinearMap.toAddHom (lof R ι M j)) ⁅x, m⁆ : (a : ι) → M a) i =
    (⁅x, AddHom.toFun (LinearMap.toAddHom (lof R ι M j)) m⁆ : (a : ι) → M a) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : Type w₁
M : ι → Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : (i : ι) → AddCommGroup (M i)
inst_4 : (i : ι) → Module.{u, w} R (M i)
inst_5 : (i : ι) → LieRingModule.{w₁, w} L (M i)
inst_6 : ∀ (i : ι), LieModule.{u, w₁, w} R L (M i)
inst_7 : DecidableEq ι
j : ι
x : L
m : M j
i : ι
⊢ (AddHom.toFun (LinearMap.toAddHom (lof R ι M j)) ⁅x, m⁆ : (a : ι) → M a) i =
    (⁅x, AddHom.toFun (LinearMap.toAddHom (lof R ι M j)) m⁆ : (a : ι) → M a) i
have pos : ∀ (h : j = i),
  (AddHom.toFun (LinearMap.toAddHom (lof R ι M j)) ⁅x, m⁆ : (a : ι) → M a) i =
    (⁅x, AddHom.toFun (LinearMap.toAddHom (lof R ι M j)) m⁆ : (a : ι) → M a) i
Tactic: by_cases h : j = i
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : Type w₁
M : ι → Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : (i : ι) → AddCommGroup (M i)
inst_4 : (i : ι) → Module.{u, w} R (M i)
inst_5 : (i : ι) → LieRingModule.{w₁, w} L (M i)
inst_6 : ∀ (i : ι), LieModule.{u, w₁, w} R L (M i)
inst_7 : DecidableEq ι
j : ι
x : L
m : M j
i : ι
pos :
  ∀ (h : j = i),
    (AddHom.toFun (LinearMap.toAddHom (lof R ι M j)) ⁅x, m⁆ : (a : ι) → M a) i =
      (⁅x, AddHom.toFun (LinearMap.toAddHom (lof R ι M j)) m⁆ : (a : ι) → M a) i
⊢ (AddHom.toFun (LinearMap.toAddHom (lof R ι M j)) ⁅x, m⁆ : (a : ι) → M a) i =
    (⁅x, AddHom.toFun (LinearMap.toAddHom (lof R ι M j)) m⁆ : (a : ι) → M a) i
have neg : ∀ (h : ¬j = i),
  (AddHom.toFun (LinearMap.toAddHom (lof R ι M j)) ⁅x, m⁆ : (a : ι) → M a) i =
    (⁅x, AddHom.toFun (LinearMap.toAddHom (lof R ι M j)) m⁆ : (a : ι) → M a) i
Tactic: by_cases h : j = i