awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : ι → Type w
inst_1 : (i : ι) → LieRing (L i)
inst_2 : (i : ι) → LieAlgebra.{u, w} R (L i)
inst_3 : DecidableEq ι
L' : Type w₁
inst_4 : LieRing L'
inst_5 : LieAlgebra R L'
f : (i : ι) → LieHom.{u, w, w₁} R (L i) L'
hf :
  Pairwise fun (i j : ι) ↦
    ∀ (x : L i) (y : L j),
      Eq.{w₁ + 1} (α := L') (Bracket.bracket (L := L') ((f i : (a : L i) → L') x : L') ((f j : (a : L j) → L') y) : L')
        (0 : L')
x_1 y_1 : ⨁ (i : ι), L i
f' : (i : ι) → LinearMap.{u, u, w, w₁} (RingHom.id R) (L i) L' := fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L')
i j : ι
y : L i
x : L j
⊢ Eq.{w₁ + 1} (α := L')
    ((toAddMonoid (β := L) fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : ⨁ (i : ι), L i) → L')
        (Bracket.bracket (L := ⨁ (i : ι), L i) ((of L j : (a : L j) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i)
            ((of L i : (a : L i) → ⨁ (i : ι), L i) y) :
          ⨁ (i : ι), L i) :
      L')
    (Bracket.bracket (L := L') (((↑(f j) : L j →ₗ[R] L').toAddMonoidHom : (a : L j) → L') x : L')
        (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') y) :
      L')
have inl : ∀ (x : L i),
  Eq.{w₁ + 1} (α := L')
    ((toAddMonoid (β := L) fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : ⨁ (i : ι), L i) → L')
        (Bracket.bracket (L := ⨁ (i : ι), L i) ((of L i : (a : L i) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i)
            ((of L i : (a : L i) → ⨁ (i : ι), L i) y) :
          ⨁ (i : ι), L i) :
      L')
    (Bracket.bracket (L := L') (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') x : L')
        (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') y) :
      L')
Tactic: obtain rfl | hij := Decidable.eq_or_ne i j
Cleared hypotheses: j, x
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : ι → Type w
inst_1 : (i : ι) → LieRing (L i)
inst_2 : (i : ι) → LieAlgebra.{u, w} R (L i)
inst_3 : DecidableEq ι
L' : Type w₁
inst_4 : LieRing L'
inst_5 : LieAlgebra R L'
f : (i : ι) → LieHom.{u, w, w₁} R (L i) L'
hf :
  Pairwise fun (i j : ι) ↦
    ∀ (x : L i) (y : L j),
      Eq.{w₁ + 1} (α := L') (Bracket.bracket (L := L') ((f i : (a : L i) → L') x : L') ((f j : (a : L j) → L') y) : L')
        (0 : L')
x_1 y_1 : ⨁ (i : ι), L i
f' : (i : ι) → LinearMap.{u, u, w, w₁} (RingHom.id R) (L i) L' := fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L')
i j : ι
y : L i
x : L j
inl :
  ∀ (x : L i),
    Eq.{w₁ + 1} (α := L')
      ((toAddMonoid (β := L) fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : ⨁ (i : ι), L i) → L')
          (Bracket.bracket (L := ⨁ (i : ι), L i) ((of L i : (a : L i) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i)
              ((of L i : (a : L i) → ⨁ (i : ι), L i) y) :
            ⨁ (i : ι), L i) :
        L')
      (Bracket.bracket (L := L') (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') x : L')
          (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') y) :
        L')
⊢ Eq.{w₁ + 1} (α := L')
    ((toAddMonoid (β := L) fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : ⨁ (i : ι), L i) → L')
        (Bracket.bracket (L := ⨁ (i : ι), L i) ((of L j : (a : L j) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i)
            ((of L i : (a : L i) → ⨁ (i : ι), L i) y) :
          ⨁ (i : ι), L i) :
      L')
    (Bracket.bracket (L := L') (((↑(f j) : L j →ₗ[R] L').toAddMonoidHom : (a : L j) → L') x : L')
        (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') y) :
      L')
have inr : ∀ (hij : i ≠ j),
  Eq.{w₁ + 1} (α := L')
    ((toAddMonoid (β := L) fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : ⨁ (i : ι), L i) → L')
        (Bracket.bracket (L := ⨁ (i : ι), L i) ((of L j : (a : L j) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i)
            ((of L i : (a : L i) → ⨁ (i : ι), L i) y) :
          ⨁ (i : ι), L i) :
      L')
    (Bracket.bracket (L := L') (((↑(f j) : L j →ₗ[R] L').toAddMonoidHom : (a : L j) → L') x : L')
        (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') y) :
      L')
Tactic: obtain rfl | hij := Decidable.eq_or_ne i j
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : ι → Type w
inst_1 : (i : ι) → LieRing (L i)
inst_2 : (i : ι) → LieAlgebra.{u, w} R (L i)
inst_3 : DecidableEq ι
L' : Type w₁
inst_4 : LieRing L'
inst_5 : LieAlgebra R L'
f : (i : ι) → LieHom.{u, w, w₁} R (L i) L'
hf :
  Pairwise fun (i j : ι) ↦
    ∀ (x : L i) (y : L j),
      Eq.{w₁ + 1} (α := L') (Bracket.bracket (L := L') ((f i : (a : L i) → L') x : L') ((f j : (a : L j) → L') y) : L')
        (0 : L')
x_1 y_1 : ⨁ (i : ι), L i
f' : (i : ι) → LinearMap.{u, u, w, w₁} (RingHom.id R) (L i) L' := fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L')
i : ι
y x : L i
⊢ Eq.{w₁ + 1} (α := L')
    ((toAddMonoid (β := L) fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : ⨁ (i : ι), L i) → L')
        (Bracket.bracket (L := ⨁ (i : ι), L i) ((of L i : (a : L i) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i)
            ((of L i : (a : L i) → ⨁ (i : ι), L i) y) :
          ⨁ (i : ι), L i) :
      L')
    (Bracket.bracket (L := L') (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') x : L')
        (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') y) :
      L')
have inl : Eq.{w₁ + 1} (α := L')
  ((toAddMonoid (β := L) fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : ⨁ (i : ι), L i) → L')
      ((of L i : (a : L i) → ⨁ (i : ι), L i) ⁅x, y⁆ : ⨁ (i : ι), L i) :
    L')
  (Bracket.bracket (L := L') (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') x : L')
      (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') y) :
    L')
Tactic: simp_rw [lie_of_same, toAddMonoid_of, LinearMap.toAddMonoidHom_coe, LieHom.coe_toLinearMap,
          LieHom.map_lie]
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : ι → Type w
inst_1 : (i : ι) → LieRing (L i)
inst_2 : (i : ι) → LieAlgebra.{u, w} R (L i)
inst_3 : DecidableEq ι
L' : Type w₁
inst_4 : LieRing L'
inst_5 : LieAlgebra R L'
f : (i : ι) → LieHom.{u, w, w₁} R (L i) L'
hf :
  Pairwise fun (i j : ι) ↦
    ∀ (x : L i) (y : L j),
      Eq.{w₁ + 1} (α := L') (Bracket.bracket (L := L') ((f i : (a : L i) → L') x : L') ((f j : (a : L j) → L') y) : L')
        (0 : L')
x_1 y_1 : ⨁ (i : ι), L i
f' : (i : ι) → LinearMap.{u, u, w, w₁} (RingHom.id R) (L i) L' := fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L')
i : ι
y x : L i
inl :
  Eq.{w₁ + 1} (α := L')
    ((toAddMonoid (β := L) fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : ⨁ (i : ι), L i) → L')
        ((of L i : (a : L i) → ⨁ (i : ι), L i) ⁅x, y⁆ : ⨁ (i : ι), L i) :
      L')
    (Bracket.bracket (L := L') (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') x : L')
        (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') y) :
      L')
⊢ Eq.{w₁ + 1} (α := L')
    ((toAddMonoid (β := L) fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : ⨁ (i : ι), L i) → L')
        (Bracket.bracket (L := ⨁ (i : ι), L i) ((of L i : (a : L i) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i)
            ((of L i : (a : L i) → ⨁ (i : ι), L i) y) :
          ⨁ (i : ι), L i) :
      L')
    (Bracket.bracket (L := L') (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') x : L')
        (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') y) :
      L')
have inl₁ : Eq.{w₁ + 1} (α := L') (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') ⁅x, y⁆ : L')
  (Bracket.bracket (L := L') (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') x : L')
      (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') y) :
    L')
Tactic: simp_rw [lie_of_same, toAddMonoid_of, LinearMap.toAddMonoidHom_coe, LieHom.coe_toLinearMap,
          LieHom.map_lie]
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : ι → Type w
inst_1 : (i : ι) → LieRing (L i)
inst_2 : (i : ι) → LieAlgebra.{u, w} R (L i)
inst_3 : DecidableEq ι
L' : Type w₁
inst_4 : LieRing L'
inst_5 : LieAlgebra R L'
f : (i : ι) → LieHom.{u, w, w₁} R (L i) L'
hf :
  Pairwise fun (i j : ι) ↦
    ∀ (x : L i) (y : L j),
      Eq.{w₁ + 1} (α := L') (Bracket.bracket (L := L') ((f i : (a : L i) → L') x : L') ((f j : (a : L j) → L') y) : L')
        (0 : L')
x_1 y_1 : ⨁ (i : ι), L i
f' : (i : ι) → LinearMap.{u, u, w, w₁} (RingHom.id R) (L i) L' := fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L')
i : ι
y x : L i
inl :
  Eq.{w₁ + 1} (α := L')
    ((toAddMonoid (β := L) fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : ⨁ (i : ι), L i) → L')
        ((of L i : (a : L i) → ⨁ (i : ι), L i) ⁅x, y⁆ : ⨁ (i : ι), L i) :
      L')
    (Bracket.bracket (L := L') (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') x : L')
        (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') y) :
      L')
inl₁ :
  Eq.{w₁ + 1} (α := L') (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') ⁅x, y⁆ : L')
    (Bracket.bracket (L := L') (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') x : L')
        (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') y) :
      L')
⊢ Eq.{w₁ + 1} (α := L')
    ((toAddMonoid (β := L) fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : ⨁ (i : ι), L i) → L')
        (Bracket.bracket (L := ⨁ (i : ι), L i) ((of L i : (a : L i) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i)
            ((of L i : (a : L i) → ⨁ (i : ι), L i) y) :
          ⨁ (i : ι), L i) :
      L')
    (Bracket.bracket (L := L') (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') x : L')
        (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') y) :
      L')
have inl₂ : Eq.{w₁ + 1} (α := L') (((↑(f i) : L i →ₗ[R] L') : (a : L i) → L') ⁅x, y⁆ : L')
  (Bracket.bracket (L := L') (((↑(f i) : L i →ₗ[R] L') : (a : L i) → L') x : L')
      (((↑(f i) : L i →ₗ[R] L') : (a : L i) → L') y) :
    L')
Tactic: simp_rw [lie_of_same, toAddMonoid_of, LinearMap.toAddMonoidHom_coe, LieHom.coe_toLinearMap,
          LieHom.map_lie]
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : ι → Type w
inst_1 : (i : ι) → LieRing (L i)
inst_2 : (i : ι) → LieAlgebra.{u, w} R (L i)
inst_3 : DecidableEq ι
L' : Type w₁
inst_4 : LieRing L'
inst_5 : LieAlgebra R L'
f : (i : ι) → LieHom.{u, w, w₁} R (L i) L'
hf :
  Pairwise fun (i j : ι) ↦
    ∀ (x : L i) (y : L j),
      Eq.{w₁ + 1} (α := L') (Bracket.bracket (L := L') ((f i : (a : L i) → L') x : L') ((f j : (a : L j) → L') y) : L')
        (0 : L')
x_1 y_1 : ⨁ (i : ι), L i
f' : (i : ι) → LinearMap.{u, u, w, w₁} (RingHom.id R) (L i) L' := fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L')
i : ι
y x : L i
inl :
  Eq.{w₁ + 1} (α := L')
    ((toAddMonoid (β := L) fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : ⨁ (i : ι), L i) → L')
        ((of L i : (a : L i) → ⨁ (i : ι), L i) ⁅x, y⁆ : ⨁ (i : ι), L i) :
      L')
    (Bracket.bracket (L := L') (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') x : L')
        (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') y) :
      L')
inl₁ :
  Eq.{w₁ + 1} (α := L') (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') ⁅x, y⁆ : L')
    (Bracket.bracket (L := L') (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') x : L')
        (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') y) :
      L')
inl₂ :
  Eq.{w₁ + 1} (α := L') (((↑(f i) : L i →ₗ[R] L') : (a : L i) → L') ⁅x, y⁆ : L')
    (Bracket.bracket (L := L') (((↑(f i) : L i →ₗ[R] L') : (a : L i) → L') x : L')
        (((↑(f i) : L i →ₗ[R] L') : (a : L i) → L') y) :
      L')
⊢ Eq.{w₁ + 1} (α := L')
    ((toAddMonoid (β := L) fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : ⨁ (i : ι), L i) → L')
        (Bracket.bracket (L := ⨁ (i : ι), L i) ((of L i : (a : L i) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i)
            ((of L i : (a : L i) → ⨁ (i : ι), L i) y) :
          ⨁ (i : ι), L i) :
      L')
    (Bracket.bracket (L := L') (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') x : L')
        (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') y) :
      L')
have inl₃ : Eq.{w₁ + 1} (α := L') ((f i : (a : L i) → L') ⁅x, y⁆ : L')
  (Bracket.bracket (L := L') ((f i : (a : L i) → L') x : L') ((f i : (a : L i) → L') y) : L')
Tactic: simp_rw [lie_of_same, toAddMonoid_of, LinearMap.toAddMonoidHom_coe, LieHom.coe_toLinearMap,
          LieHom.map_lie]
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : ι → Type w
inst_1 : (i : ι) → LieRing (L i)
inst_2 : (i : ι) → LieAlgebra.{u, w} R (L i)
inst_3 : DecidableEq ι
L' : Type w₁
inst_4 : LieRing L'
inst_5 : LieAlgebra R L'
f : (i : ι) → LieHom.{u, w, w₁} R (L i) L'
hf :
  Pairwise fun (i j : ι) ↦
    ∀ (x : L i) (y : L j),
      Eq.{w₁ + 1} (α := L') (Bracket.bracket (L := L') ((f i : (a : L i) → L') x : L') ((f j : (a : L j) → L') y) : L')
        (0 : L')
x_1 y_1 : ⨁ (i : ι), L i
f' : (i : ι) → LinearMap.{u, u, w, w₁} (RingHom.id R) (L i) L' := fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L')
i j : ι
y : L i
x : L j
hij : i ≠ j
⊢ Eq.{w₁ + 1} (α := L')
    ((toAddMonoid (β := L) fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : ⨁ (i : ι), L i) → L')
        (Bracket.bracket (L := ⨁ (i : ι), L i) ((of L j : (a : L j) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i)
            ((of L i : (a : L i) → ⨁ (i : ι), L i) y) :
          ⨁ (i : ι), L i) :
      L')
    (Bracket.bracket (L := L') (((↑(f j) : L j →ₗ[R] L').toAddMonoidHom : (a : L j) → L') x : L')
        (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') y) :
      L')
have inr : Eq.{w₁ + 1} (α := L')
  ((toAddMonoid (β := L) fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : ⨁ (i : ι), L i) → L') 0 : L')
  (Bracket.bracket (L := L') (((↑(f j) : L j →ₗ[R] L').toAddMonoidHom : (a : L j) → L') x : L')
      (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') y) :
    L')
Tactic: simp_rw [lie_of_of_ne _ hij.symm, map_zero, LinearMap.toAddMonoidHom_coe,
          LieHom.coe_toLinearMap, hf hij.symm x y]
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : ι → Type w
inst_1 : (i : ι) → LieRing (L i)
inst_2 : (i : ι) → LieAlgebra.{u, w} R (L i)
inst_3 : DecidableEq ι
L' : Type w₁
inst_4 : LieRing L'
inst_5 : LieAlgebra R L'
f : (i : ι) → LieHom.{u, w, w₁} R (L i) L'
hf :
  Pairwise fun (i j : ι) ↦
    ∀ (x : L i) (y : L j),
      Eq.{w₁ + 1} (α := L') (Bracket.bracket (L := L') ((f i : (a : L i) → L') x : L') ((f j : (a : L j) → L') y) : L')
        (0 : L')
x_1 y_1 : ⨁ (i : ι), L i
f' : (i : ι) → LinearMap.{u, u, w, w₁} (RingHom.id R) (L i) L' := fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L')
i j : ι
y : L i
x : L j
hij : i ≠ j
inr :
  Eq.{w₁ + 1} (α := L')
    ((toAddMonoid (β := L) fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : ⨁ (i : ι), L i) → L') 0 : L')
    (Bracket.bracket (L := L') (((↑(f j) : L j →ₗ[R] L').toAddMonoidHom : (a : L j) → L') x : L')
        (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') y) :
      L')
⊢ Eq.{w₁ + 1} (α := L')
    ((toAddMonoid (β := L) fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : ⨁ (i : ι), L i) → L')
        (Bracket.bracket (L := ⨁ (i : ι), L i) ((of L j : (a : L j) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i)
            ((of L i : (a : L i) → ⨁ (i : ι), L i) y) :
          ⨁ (i : ι), L i) :
      L')
    (Bracket.bracket (L := L') (((↑(f j) : L j →ₗ[R] L').toAddMonoidHom : (a : L j) → L') x : L')
        (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') y) :
      L')
have inr₁ : Eq.{w₁ + 1} (α := L') (0 : L')
  (Bracket.bracket (L := L') (((↑(f j) : L j →ₗ[R] L').toAddMonoidHom : (a : L j) → L') x : L')
      (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') y) :
    L')
Tactic: simp_rw [lie_of_of_ne _ hij.symm, map_zero, LinearMap.toAddMonoidHom_coe,
          LieHom.coe_toLinearMap, hf hij.symm x y]
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : ι → Type w
inst_1 : (i : ι) → LieRing (L i)
inst_2 : (i : ι) → LieAlgebra.{u, w} R (L i)
inst_3 : DecidableEq ι
L' : Type w₁
inst_4 : LieRing L'
inst_5 : LieAlgebra R L'
f : (i : ι) → LieHom.{u, w, w₁} R (L i) L'
hf :
  Pairwise fun (i j : ι) ↦
    ∀ (x : L i) (y : L j),
      Eq.{w₁ + 1} (α := L') (Bracket.bracket (L := L') ((f i : (a : L i) → L') x : L') ((f j : (a : L j) → L') y) : L')
        (0 : L')
x_1 y_1 : ⨁ (i : ι), L i
f' : (i : ι) → LinearMap.{u, u, w, w₁} (RingHom.id R) (L i) L' := fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L')
i j : ι
y : L i
x : L j
hij : i ≠ j
inr :
  Eq.{w₁ + 1} (α := L')
    ((toAddMonoid (β := L) fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : ⨁ (i : ι), L i) → L') 0 : L')
    (Bracket.bracket (L := L') (((↑(f j) : L j →ₗ[R] L').toAddMonoidHom : (a : L j) → L') x : L')
        (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') y) :
      L')
inr₁ :
  Eq.{w₁ + 1} (α := L') (0 : L')
    (Bracket.bracket (L := L') (((↑(f j) : L j →ₗ[R] L').toAddMonoidHom : (a : L j) → L') x : L')
        (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') y) :
      L')
⊢ Eq.{w₁ + 1} (α := L')
    ((toAddMonoid (β := L) fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : ⨁ (i : ι), L i) → L')
        (Bracket.bracket (L := ⨁ (i : ι), L i) ((of L j : (a : L j) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i)
            ((of L i : (a : L i) → ⨁ (i : ι), L i) y) :
          ⨁ (i : ι), L i) :
      L')
    (Bracket.bracket (L := L') (((↑(f j) : L j →ₗ[R] L').toAddMonoidHom : (a : L j) → L') x : L')
        (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') y) :
      L')
have inr₂ : Eq.{w₁ + 1} (α := L') (0 : L')
  (Bracket.bracket (L := L') (((↑(f j) : L j →ₗ[R] L') : (a : L j) → L') x : L')
      (((↑(f i) : L i →ₗ[R] L') : (a : L i) → L') y) :
    L')
Tactic: simp_rw [lie_of_of_ne _ hij.symm, map_zero, LinearMap.toAddMonoidHom_coe,
          LieHom.coe_toLinearMap, hf hij.symm x y]
-- Lean 4 proof step from Mathlib.Algebra.Lie.DirectSum (goal)
Goal:
R : Type u
ι : Type v
inst : CommRing R
L : ι → Type w
inst_1 : (i : ι) → LieRing (L i)
inst_2 : (i : ι) → LieAlgebra.{u, w} R (L i)
inst_3 : DecidableEq ι
L' : Type w₁
inst_4 : LieRing L'
inst_5 : LieAlgebra R L'
f : (i : ι) → LieHom.{u, w, w₁} R (L i) L'
hf :
  Pairwise fun (i j : ι) ↦
    ∀ (x : L i) (y : L j),
      Eq.{w₁ + 1} (α := L') (Bracket.bracket (L := L') ((f i : (a : L i) → L') x : L') ((f j : (a : L j) → L') y) : L')
        (0 : L')
x_1 y_1 : ⨁ (i : ι), L i
f' : (i : ι) → LinearMap.{u, u, w, w₁} (RingHom.id R) (L i) L' := fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L')
i j : ι
y : L i
x : L j
hij : i ≠ j
inr :
  Eq.{w₁ + 1} (α := L')
    ((toAddMonoid (β := L) fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : ⨁ (i : ι), L i) → L') 0 : L')
    (Bracket.bracket (L := L') (((↑(f j) : L j →ₗ[R] L').toAddMonoidHom : (a : L j) → L') x : L')
        (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') y) :
      L')
inr₁ :
  Eq.{w₁ + 1} (α := L') (0 : L')
    (Bracket.bracket (L := L') (((↑(f j) : L j →ₗ[R] L').toAddMonoidHom : (a : L j) → L') x : L')
        (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') y) :
      L')
inr₂ :
  Eq.{w₁ + 1} (α := L') (0 : L')
    (Bracket.bracket (L := L') (((↑(f j) : L j →ₗ[R] L') : (a : L j) → L') x : L')
        (((↑(f i) : L i →ₗ[R] L') : (a : L i) → L') y) :
      L')
⊢ Eq.{w₁ + 1} (α := L')
    ((toAddMonoid (β := L) fun (i : ι) ↦ (↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : ⨁ (i : ι), L i) → L')
        (Bracket.bracket (L := ⨁ (i : ι), L i) ((of L j : (a : L j) → ⨁ (i : ι), L i) x : ⨁ (i : ι), L i)
            ((of L i : (a : L i) → ⨁ (i : ι), L i) y) :
          ⨁ (i : ι), L i) :
      L')
    (Bracket.bracket (L := L') (((↑(f j) : L j →ₗ[R] L').toAddMonoidHom : (a : L j) → L') x : L')
        (((↑(f i) : L i →ₗ[R] L').toAddMonoidHom : (a : L i) → L') y) :
      L')
have inr₃ : Eq.{w₁ + 1} (α := L') (0 : L')
  (Bracket.bracket (L := L') ((f j : (a : L j) → L') x : L') ((f i : (a : L i) → L') y) : L')
Tactic: simp_rw [lie_of_of_ne _ hij.symm, map_zero, LinearMap.toAddMonoidHom_coe,
          LieHom.coe_toLinearMap, hf hij.symm x y]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (hypothesis)
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
y : L
⊢ ∃ (t : R), ∃ z ∈ I, y = t • x + z
have hy : Membership.mem (γ := Submodule R L) ⊤ y
Tactic: have hy : y ∈ (⊤ : Submodule R L) := Submodule.mem_top
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (hypothesis)
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
y : L
hy : Membership.mem (γ := Submodule R L) ⊤ y
⊢ ∃ (t : R), ∃ z ∈ I, y = t • x + z
have hy₁ : ∃ (y_1 : L), (∃ (a : R), a • x = y_1) ∧ ∃ z ∈ (LieIdeal.toLieSubalgebra R L I).toSubmodule, y_1 + z = y
Tactic: simp only [← hxI, Submodule.mem_sup, Submodule.mem_span_singleton] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (goal)
Goal:
R : Type u₁
L : Type u₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
y : L
hy : ∃ (y_1 : L), (∃ (a : R), a • x = y_1) ∧ ∃ z ∈ (LieIdeal.toLieSubalgebra R L I).toSubmodule, y_1 + z = y
⊢ ∃ (t : R), ∃ z ∈ I, y = t • x + z
have obtain : ∀ (t : R) (z : L) (hz : z ∈ (LieIdeal.toLieSubalgebra R L I).toSubmodule),
  ∃ (t_1 : R), ∃ z_1 ∈ I, t • x + z = t_1 • x + z_1
Tactic: obtain ⟨-, ⟨t, rfl⟩, z, hz, rfl⟩ := hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (goal)
Goal:
R : Type u₁
L : Type u₂
M : Type u₄
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
N : LieSubmodule R L M
⊢ (↑(Bracket.bracket.{u₂, u₄} (L := LieIdeal R L) ⊤ N) : Submodule R M) =
    Submodule.map (σ₁₂ := RingHom.id R)
        (((toEnd R L M : LieHom.{u₁, u₂, u₄} R L (Module.End R M)) : (a : L) → Module.End R M) x) (↑N : Submodule R M) ⊔
      (↑⁅I, N⁆ : Submodule R M)
have simp : Eq (α := Submodule R M) (Submodule.span R {x : M | ∃ (x_1 : L), ∃ n ∈ N, ⁅x_1, n⁆ = x})
  (Submodule.span R
    ((fun (a : M) ↦ ⁅x, a⁆) '' (↑(↑N : Submodule R M) : Set M) ∪ {x : M | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x}))
Tactic: simp only [lieIdeal_oper_eq_linear_span', Submodule.sup_span, mem_top, true_and,
    Submodule.map_coe, toEnd_apply_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Engel (goal)
Goal:
R : Type u₁
L : Type u₂
M : Type u₄
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
I : LieIdeal R L
x : L
hxI : R ∙ x ⊔ (LieIdeal.toLieSubalgebra R L I).toSubmodule = ⊤
N : LieSubmodule R L M
⊢ Eq (α := Submodule R M) (Submodule.span R {x : M | ∃ (x_1 : L), ∃ n ∈ N, ⁅x_1, n⁆ = x})
    (Submodule.span R
      ((fun (a : M) ↦ ⁅x, a⁆) '' (↑(↑N : Submodule R M) : Set M) ∪ {x : M | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x}))
have refine_1 : {x : M | ∃ (x_1 : L), ∃ n ∈ N, ⁅x_1, n⁆ = x} ⊆
  (↑(Submodule.span R
        ((fun (a : M) ↦ ⁅x, a⁆) '' (↑(↑N : Submodule R M) : Set M) ∪ {x : M | ∃ x_1 ∈ I, ∃ n ∈ N, ⁅x_1, n⁆ = x})) :
    Set M)
Tactic: refine le_antisymm (Submodule.span_le.mpr ?_) (Submodule.span_mono fun z hz => ?_)