awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
Goal:
R : Type u
L : Type v
M : Type w
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
h : ∀ (x : L), (∀ (m : M), ⁅x, m⁆ = 0) → x = 0
x y : L
hxy :
  Eq.{w + 1} (α := Module.End R M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M)
m : M
refine_2 : ⁅x, m⁆ - ⁅y, m⁆ = 0
⊢ ⁅x - y, m⁆ = 0
have refine_2₁ : ⁅x, m⁆ = ⁅y, m⁆
Tactic: rw [sub_lie, sub_eq_zero, ← toEnd_apply_apply R, ← toEnd_apply_apply R, hxy]
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
Goal:
R : Type u
L : Type v
M : Type w
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
h : ∀ (x : L), (∀ (m : M), ⁅x, m⁆ = 0) → x = 0
x y : L
hxy :
  Eq.{w + 1} (α := Module.End R M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M)
m : M
refine_2 : ⁅x, m⁆ - ⁅y, m⁆ = 0
refine_2₁ : ⁅x, m⁆ = ⁅y, m⁆
⊢ ⁅x - y, m⁆ = 0
have refine_2₂ : ((((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) : (a : M) → M)
    m =
  ⁅y, m⁆
Tactic: rw [sub_lie, sub_eq_zero, ← toEnd_apply_apply R, ← toEnd_apply_apply R, hxy]
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
Goal:
R : Type u
L : Type v
M : Type w
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
h : ∀ (x : L), (∀ (m : M), ⁅x, m⁆ = 0) → x = 0
x y : L
hxy :
  Eq.{w + 1} (α := Module.End R M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M)
m : M
refine_2 : ⁅x, m⁆ - ⁅y, m⁆ = 0
refine_2₁ : ⁅x, m⁆ = ⁅y, m⁆
refine_2₂ :
  ((((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) :
        (a : M) → M)
      m =
    ⁅y, m⁆
⊢ ⁅x - y, m⁆ = 0
have refine_2₃ : Eq (α := M)
  (((((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) :
        (a : M) → M)
      m :
    M)
  (((((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M) :
        (a : M) → M)
      m :
    M)
Tactic: rw [sub_lie, sub_eq_zero, ← toEnd_apply_apply R, ← toEnd_apply_apply R, hxy]
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
Goal:
R : Type u
L : Type v
M : Type w
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
h : ∀ (x : L), (∀ (m : M), ⁅x, m⁆ = 0) → x = 0
x y : L
hxy :
  Eq.{w + 1} (α := Module.End R M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M)
m : M
refine_2 : ⁅x, m⁆ - ⁅y, m⁆ = 0
refine_2₁ : ⁅x, m⁆ = ⁅y, m⁆
refine_2₂ :
  ((((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) :
        (a : M) → M)
      m =
    ⁅y, m⁆
refine_2₃ :
  Eq (α := M)
    (((((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) :
          (a : M) → M)
        m :
      M)
    (((((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M) :
          (a : M) → M)
        m :
      M)
⊢ ⁅x - y, m⁆ = 0
have refine_2₄ : Eq (α := M)
  (((((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M) :
        (a : M) → M)
      m :
    M)
  (((((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M) :
        (a : M) → M)
      m :
    M)
Tactic: rw [sub_lie, sub_eq_zero, ← toEnd_apply_apply R, ← toEnd_apply_apply R, hxy]
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
Goal:
R : Type u
L : Type v
M : Type w
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
inst_7 : IsFaithful R L M
L' : LieSubalgebra R L
⊢ IsFaithful.{u, v, w} R (↥L') M
have refine : Injective.{v + 1, w + 1} (α := ↥L') (β := Module.End R M)
  ((⇑(toEnd R L M) : (a : L) → Module.End R M) ∘ Subtype.val (p := fun (x : L) ↦ x ∈ L'))
Tactic: refine ⟨(?_ : Injective (toEnd R L M ∘ ((↑) : L' → L)))⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
Goal:
R : Type u
L : Type v
M : Type w
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
N : LieSubmodule R L M
x : L
y : ↥N
n : ℕ
⊢ Eq (α := M)
    ((↑((HPow.hPow (α := Module.End R ↥N)
                (((toEnd.{u, v, w} R L ↥N : LieHom.{u, v, w} R L (Module.End R ↥N)) : (a : L) → Module.End R ↥N) x :
                  Module.End R ↥N)
                n :
              (a : ↥N) → ↥N)
            y) :
        M) :
      M)
    ((HPow.hPow (α := Module.End R M)
            (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) n :
          (a : M) → M)
        (↑y : M) :
      M)
have zero : ∀ (y : ↥N),
  Eq (α := M)
    ((↑((HPow.hPow (α := Module.End R ↥N) (β := ℕ)
                (((toEnd.{u, v, w} R L ↥N : LieHom.{u, v, w} R L (Module.End R ↥N)) : (a : L) → Module.End R ↥N) x :
                  Module.End R ↥N)
                0 :
              (a : ↥N) → ↥N)
            y) :
        M) :
      M)
    ((HPow.hPow (α := Module.End R M) (β := ℕ)
            (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) 0 :
          (a : M) → M)
        (↑y : M) :
      M)
Tactic: induction n generalizing y with
  | zero => rfl
  | succ n ih => simp only [pow_succ', Module.End.mul_apply, ih, LieSubmodule.coe_toEnd]
Cleared hypotheses: y, n
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
Goal:
R : Type u
L : Type v
M : Type w
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
N : LieSubmodule R L M
x : L
y : ↥N
n : ℕ
zero :
  ∀ (y : ↥N),
    Eq (α := M)
      ((↑((HPow.hPow (α := Module.End R ↥N) (β := ℕ)
                  (((toEnd.{u, v, w} R L ↥N : LieHom.{u, v, w} R L (Module.End R ↥N)) : (a : L) → Module.End R ↥N) x :
                    Module.End R ↥N)
                  0 :
                (a : ↥N) → ↥N)
              y) :
          M) :
        M)
      ((HPow.hPow (α := Module.End R M) (β := ℕ)
              (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
              0 :
            (a : M) → M)
          (↑y : M) :
        M)
⊢ Eq (α := M)
    ((↑((HPow.hPow (α := Module.End R ↥N)
                (((toEnd.{u, v, w} R L ↥N : LieHom.{u, v, w} R L (Module.End R ↥N)) : (a : L) → Module.End R ↥N) x :
                  Module.End R ↥N)
                n :
              (a : ↥N) → ↥N)
            y) :
        M) :
      M)
    ((HPow.hPow (α := Module.End R M)
            (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) n :
          (a : M) → M)
        (↑y : M) :
      M)
have succ : ∀ (n : ℕ)
  (ih :
    ∀ (y : ↥N),
      Eq (α := M)
        ((↑((HPow.hPow (α := Module.End R ↥N)
                    (((toEnd.{u, v, w} R L ↥N : LieHom.{u, v, w} R L (Module.End R ↥N)) : (a : L) → Module.End R ↥N) x :
                      Module.End R ↥N)
                    n :
                  (a : ↥N) → ↥N)
                y) :
            M) :
          M)
        ((HPow.hPow (α := Module.End R M)
                (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
                n :
              (a : M) → M)
            (↑y : M) :
          M))
  (y : ↥N),
  Eq (α := M)
    ((↑((HPow.hPow (α := Module.End R ↥N)
                (((toEnd.{u, v, w} R L ↥N : LieHom.{u, v, w} R L (Module.End R ↥N)) : (a : L) → Module.End R ↥N) x :
                  Module.End R ↥N)
                (n + 1) :
              (a : ↥N) → ↥N)
            y) :
        M) :
      M)
    ((HPow.hPow (α := Module.End R M)
            (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
            (n + 1) :
          (a : M) → M)
        (↑y : M) :
      M)
Tactic: induction n generalizing y with
  | zero => rfl
  | succ n ih => simp only [pow_succ', Module.End.mul_apply, ih, LieSubmodule.coe_toEnd]
Cleared hypotheses: y, n
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (hypothesis)
Goal:
R : Type u
L : Type v
M : Type w
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
x y : L
z : M
n : ℕ
ih :
  Eq (α := M)
    ((HPow.hPow (α := Module.End R M)
            (((φ : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) n :
          (a : M) → M)
        ⁅y, z⁆ :
      M)
    (∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        HSMul.hSMul (β := M) (n.choose ij.1)
          (Bracket.bracket (L := L)
              ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) ij.1 :
                    (a : L) → L)
                  y :
                L)
              ((HPow.hPow (α := Module.End R M)
                    (((φ : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) ij.2 :
                  (a : M) → M)
                z) :
            M) :
      M)
i j : ℕ
hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
⊢ HSMul.hSMul (β := M) (n.choose (i, j).1)
      (Bracket.bracket (L := L)
          ((((ad R L : (a : L) → Module.End R L) x : Module.End R L) : (a : L) → L)
              ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) (i, j).1 :
                    (a : L) → L)
                  y :
                L) :
            L)
          ((HPow.hPow (α := Module.End R M)
                (((φ : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) (i, j).2 :
              (a : M) → M)
            z) :
        M) =
    HSMul.hSMul (β := M) (n.choose (i, j).2)
      (Bracket.bracket (L := L)
          ((((ad R L : (a : L) → Module.End R L) x : Module.End R L) : (a : L) → L)
              ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) (i, j).1 :
                    (a : L) → L)
                  y :
                L) :
            L)
          ((HPow.hPow (α := Module.End R M)
                (((φ : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) (i, j).2 :
              (a : M) → M)
            z) :
        M)
have hij₁ : (i, j).1 + (i, j).2 = n
Tactic: rw [mem_antidiagonal] at hij
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
Goal:
R : Type u
L : Type v
M : Type w
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
x y : L
z : M
n : ℕ
⊢ Eq (α := M)
    ((HPow.hPow (α := Module.End R M)
            (((φ : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) n :
          (a : M) → M)
        ⁅y, z⁆ :
      M)
    (∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        HSMul.hSMul (β := M) (n.choose ij.1)
          (Bracket.bracket (L := L)
              ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) ij.1 :
                    (a : L) → L)
                  y :
                L)
              ((HPow.hPow (α := Module.End R M)
                    (((φ : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) ij.2 :
                  (a : M) → M)
                z) :
            M) :
      M)
have zero : Eq (α := M)
  ((HPow.hPow (α := Module.End R M) (β := ℕ)
          (((φ : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) 0 :
        (a : M) → M)
      ⁅y, z⁆ :
    M)
  (∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ 0,
      HSMul.hSMul (β := M) (Nat.choose 0 ij.1)
        (Bracket.bracket (L := L)
            ((HPow.hPow (α := Module.End R L) ((ad R L : (a : L) → Module.End R L) x : Module.End R L) ij.1 :
                  (a : L) → L)
                y :
              L)
            ((HPow.hPow (α := Module.End R M)
                  (((φ : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) ij.2 :
                (a : M) → M)
              z) :
          M) :
    M)
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    rw [Finset.sum_antidiagonal_choose_succ_nsmul
      (fun i j ↦ ⁅((ad R L x) ^ i) y, ((φ x) ^ j) z⁆) n]
    simp only [pow_succ', Module.End.mul_apply, ih, map_sum, map_nsmul,
      toEnd_lie, nsmul_add, sum_add_distrib]
    rw [add_comm, add_left_cancel_iff, sum_congr rfl]
    rintro ⟨i, j⟩ hij
    rw [mem_antidiagonal] at hij
    rw [Nat.choose_symm_of_eq_add hij.symm]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
Goal:
R : Type u
L : Type v
M : Type w
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
M₂ : Type w₁
inst_7 : AddCommGroup M₂
inst_8 : Module R M₂
inst_9 : LieRingModule L M₂
inst_10 : LieModule R L M₂
f : M →ₗ⁅R,L⁆ M₂
k : ℕ
x : L
⊢ HPow.hPow (α := Module.End R M₂)
        (((toEnd R L M₂ : LieHom.{u, v, w₁} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x : Module.End R M₂)
        k ∘ₗ
      (↑f : M →ₗ[R] M₂) =
    (↑f : M →ₗ[R] M₂) ∘ₗ
      HPow.hPow (α := Module.End R M)
        (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) k
have h : ((toEnd R L M₂ : LieHom.{u, v, w₁} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x ∘ₗ (↑f : M →ₗ[R] M₂) =
  (↑f : M →ₗ[R] M₂) ∘ₗ ((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x
Tactic: apply Module.End.commute_pow_left_of_commute
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
Goal:
R : Type u
L : Type v
M : Type w
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
M₂ : Type w₁
inst_7 : AddCommGroup M₂
inst_8 : Module R M₂
inst_9 : LieRingModule L M₂
inst_10 : LieModule R L M₂
f : M →ₗ⁅R,L⁆ M₂
k : ℕ
x : L
⊢ ((toEnd R L M₂ : LieHom.{u, v, w₁} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x ∘ₗ (↑f : M →ₗ[R] M₂) =
    (↑f : M →ₗ[R] M₂) ∘ₗ ((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x
have h : ∀ (x_1 : M),
  Eq.{w₁ + 1} (α := M₂)
    ((((toEnd R L M₂ : LieHom.{u, v, w₁} R L (Module.End R M₂)) : (a : L) → Module.End R M₂) x ∘ₗ (↑f : M →ₗ[R] M₂) :
          (a : M) → M₂)
        x_1 :
      M₂)
    (((↑f : M →ₗ[R] M₂) ∘ₗ ((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x :
          (a : M) → M₂)
        x_1 :
      M₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
Goal:
R : Type u
L : Type v
M : Type w
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
N : LieSubmodule R L M
φ : R
k : ℕ
x : L
⊢ MapsTo
    (⇑(HSub.hSub (α := Module.End R M) (β := Module.End R M)
            (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
            ((algebraMap R (Module.End R M) : (a : R) → Module.End R M) φ : Module.End R M) ^
          k) :
      (a : M) → M)
    (↑N : Set M) (↑N : Set M)
have rw : MapsTo
  (⇑(HSub.hSub (α := Module.End R M) (β := Module.End R M)
          (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
          ((algebraMap R (Module.End R M) : (a : R) → Module.End R M) φ : Module.End R M)) :
      (a : M) → M)^[k]
  (↑N : Set M) (↑N : Set M)
Tactic: rw [Module.End.coe_pow]
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : Ring A
inst_2 : Algebra R A
⊢ (⇑(ad R A) : (a : A) → Module.End R A) =
    HSub.hSub (α := (a : A) → A →ₗ[R] A) (LinearMap.mulLeft R) (LinearMap.mulRight R)
have h : ∀ (a b : A),
  Eq (α := A) ((((ad R A : (a : A) → Module.End R A) a : Module.End R A) : (a : A) → A) b : A)
    ((HSub.hSub (α := (a : A) → A →ₗ[R] A) (β := (b : A) → A →ₗ[R] A) (LinearMap.mulLeft R) (LinearMap.mulRight R) a :
          (a : A) → A)
        b :
      A)
Tactic: ext a b
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
x : ↥K
⊢ (ad R L : (a : L) → Module.End R L) (↑x : L) ∘ₗ (↑K.incl : ↥K →ₗ[R] L) =
    (↑K.incl : ↥K →ₗ[R] L) ∘ₗ (ad R ↥K : (a : ↥K) → Module.End R ↥K) x
have h : ∀ (y : ↥K),
  Eq (α := L) (((ad R L : (a : L) → Module.End R L) (↑x : L) ∘ₗ (↑K.incl : ↥K →ₗ[R] L) : (a : ↥K) → L) y : L)
    (((↑K.incl : ↥K →ₗ[R] L) ∘ₗ (ad R ↥K : (a : ↥K) → Module.End R ↥K) x : (a : ↥K) → L) y : L)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (hypothesis)
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : Ring A
inst_2 : Algebra R A
A' : Subalgebra R A
x y : A
hx :
  Membership.mem (γ := Set A)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u, v} (R := R)
          ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) A'))))
    x
hy :
  Membership.mem (γ := Set A)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u, v} (R := R)
          ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) A'))))
    y
⊢ ⁅x, y⁆ ∈ A'
have hx₁ : x ∈ A'
Tactic: change x ∈ A' at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (hypothesis)
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : Ring A
inst_2 : Algebra R A
A' : Subalgebra R A
x y : A
hy :
  Membership.mem (γ := Set A)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u, v} (R := R)
          ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) A'))))
    y
hx : x ∈ A'
⊢ ⁅x, y⁆ ∈ A'
have hy₁ : y ∈ A'
Tactic: change y ∈ A' at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : Ring A
inst_2 : Algebra R A
A' : Subalgebra R A
x y : A
hx : x ∈ A'
hy : y ∈ A'
⊢ ⁅x, y⁆ ∈ A'
have rw : x * y - y * x ∈ A'
Tactic: rw [LieRing.of_associative_ring_bracket]
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (hypothesis)
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : Ring A
inst_2 : Algebra R A
A' : Subalgebra R A
x y : A
hx : x ∈ A'
hy : y ∈ A'
⊢ x * y - y * x ∈ A'
have hxy : x * y ∈ A'
Tactic: have hxy := A'.mul_mem hx hy
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (hypothesis)
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : Ring A
inst_2 : Algebra R A
A' : Subalgebra R A
x y : A
hx : x ∈ A'
hy : y ∈ A'
hxy : x * y ∈ A'
⊢ x * y - y * x ∈ A'
have hyx : y * x ∈ A'
Tactic: have hyx := A'.mul_mem hy hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (hypothesis)
Goal:
R : Type u
A₁ : Type v
A₂ : Type w
inst : CommRing R
inst_1 : Ring A₁
inst_2 : Ring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
x y : A₁
⊢ e.toFun ⁅x, y⁆ = ⁅e.toFun x, e.toFun y⁆
have this : e.toFun = (⇑e : (a : A₁) → A₂)
Tactic: have : e.toEquiv.toFun = e := rfl
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
Goal:
R : Type u
A₁ : Type v
A₂ : Type w
inst : CommRing R
inst_1 : Ring A₁
inst_2 : Ring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
x y : A₁
this : e.toFun = (⇑e : (a : A₁) → A₂)
⊢ e.toFun ⁅x, y⁆ = ⁅e.toFun x, e.toFun y⁆
have simp_rw : e.toFun (x * y - y * x) = e.toFun x * e.toFun y - e.toFun y * e.toFun x
Tactic: simp_rw [LieRing.of_associative_ring_bracket, this, map_sub, map_mul]
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
Goal:
R : Type u
A₁ : Type v
A₂ : Type w
inst : CommRing R
inst_1 : Ring A₁
inst_2 : Ring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
x y : A₁
this : e.toFun = (⇑e : (a : A₁) → A₂)
simp_rw : e.toFun (x * y - y * x) = e.toFun x * e.toFun y - e.toFun y * e.toFun x
⊢ e.toFun ⁅x, y⁆ = ⁅e.toFun x, e.toFun y⁆
have simp_rw₁ : (e : (a : A₁) → A₂) (x * y - y * x) =
  HMul.hMul (α := A₂) (β := A₂) ((e : (a : A₁) → A₂) x : A₂) ((e : (a : A₁) → A₂) y : A₂) -
    HMul.hMul (α := A₂) (β := A₂) ((e : (a : A₁) → A₂) y : A₂) ((e : (a : A₁) → A₂) x : A₂)
Tactic: simp_rw [LieRing.of_associative_ring_bracket, this, map_sub, map_mul]
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
Goal:
R : Type u
A₁ : Type v
A₂ : Type w
inst : CommRing R
inst_1 : Ring A₁
inst_2 : Ring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
x y : A₁
this : e.toFun = (⇑e : (a : A₁) → A₂)
simp_rw : e.toFun (x * y - y * x) = e.toFun x * e.toFun y - e.toFun y * e.toFun x
simp_rw₁ :
  (e : (a : A₁) → A₂) (x * y - y * x) =
    HMul.hMul (α := A₂) (β := A₂) ((e : (a : A₁) → A₂) x : A₂) ((e : (a : A₁) → A₂) y : A₂) -
      HMul.hMul (α := A₂) (β := A₂) ((e : (a : A₁) → A₂) y : A₂) ((e : (a : A₁) → A₂) x : A₂)
⊢ e.toFun ⁅x, y⁆ = ⁅e.toFun x, e.toFun y⁆
have simp_rw₂ : HSub.hSub (α := A₂) (β := A₂) ((e : (a : A₁) → A₂) (x * y) : A₂) ((e : (a : A₁) → A₂) (y * x) : A₂) =
  HMul.hMul (α := A₂) (β := A₂) ((e : (a : A₁) → A₂) x : A₂) ((e : (a : A₁) → A₂) y : A₂) -
    HMul.hMul (α := A₂) (β := A₂) ((e : (a : A₁) → A₂) y : A₂) ((e : (a : A₁) → A₂) x : A₂)
Tactic: simp_rw [LieRing.of_associative_ring_bracket, this, map_sub, map_mul]
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
Goal:
R : Type u_1
L : Type u_2
L' : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
e : L ≃ₗ⁅R⁆ L'
x : L
⊢ Eq.{u_3 + 1} (α := Module.End R L')
    ((e.toLinearEquiv.conj : (a : Module.End R L) → Module.End R L') ((ad R L : (a : L) → Module.End R L) x) :
      Module.End R L')
    ((ad R L' : (a : L') → Module.End R L') ((e : (a : L) → L') x : L') : Module.End R L')
have h : ∀ (y' : L'),
  Eq (α := L')
    ((((e.toLinearEquiv.conj : (a : Module.End R L) → Module.End R L') ((ad R L : (a : L) → Module.End R L) x) :
            Module.End R L') :
          (a : L') → L')
        y' :
      L')
    ((((ad R L' : (a : L') → Module.End R L') ((e : (a : L) → L') x : L') : Module.End R L') : (a : L') → L') y' : L')
Tactic: ext y'