awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : 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 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
t : R
x_1 y z : L
m n : M
x : L
f g : M →ₗ[R] N
⊢ {
      toFun := fun (m : M) ↦
        HSub.hSub (α := N) (β := N) (⁅x, (f + g : (a : M) → N) m⁆ : N) ((f + g : (a : M) → N) ⁅x, m⁆ : N),
      map_add' := ⋯, map_smul' := ⋯ } =
    HAdd.hAdd (α := M →ₗ[R] N)
      {
        toFun := fun (m : M) ↦
          HSub.hSub (α := N) (β := N) (⁅x, (f : (a : M) → N) m⁆ : N) ((f : (a : M) → N) ⁅x, m⁆ : N),
        map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] N }
      {
        toFun := fun (m : M) ↦
          HSub.hSub (α := N) (β := N) (⁅x, (g : (a : M) → N) m⁆ : N) ((g : (a : M) → N) ⁅x, m⁆ : N),
        map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] N }
have h : ∀ (n : M),
  Eq.{w₁ + 1} (α := N)
    (({
            toFun := fun (m : M) ↦
              HSub.hSub (α := N) (β := N) (⁅x, (f + g : (a : M) → N) m⁆ : N) ((f + g : (a : M) → N) ⁅x, m⁆ : N),
            map_add' := sorry, map_smul' := sorry } :
          (a : M) → N)
        n :
      N)
    ((HAdd.hAdd (α := M →ₗ[R] N)
            {
              toFun := fun (m : M) ↦
                HSub.hSub (α := N) (β := N) (⁅x, (f : (a : M) → N) m⁆ : N) ((f : (a : M) → N) ⁅x, m⁆ : N),
              map_add' := sorry, map_smul' := sorry : M →ₗ[R] N }
            {
              toFun := fun (m : M) ↦
                HSub.hSub (α := N) (β := N) (⁅x, (g : (a : M) → N) m⁆ : N) ((g : (a : M) → N) ⁅x, m⁆ : N),
              map_add' := sorry, map_smul' := sorry : M →ₗ[R] N } :
          (a : M) → N)
        n :
      N)
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : 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 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
t : R
x_1 y z : L
m n_1 : M
x : L
f g : M →ₗ[R] N
n : M
⊢ Eq.{w₁ + 1} (α := N)
    (({
            toFun := fun (m : M) ↦
              HSub.hSub (α := N) (β := N) (⁅x, (f + g : (a : M) → N) m⁆ : N) ((f + g : (a : M) → N) ⁅x, m⁆ : N),
            map_add' := ⋯, map_smul' := ⋯ } :
          (a : M) → N)
        n :
      N)
    ((HAdd.hAdd (α := M →ₗ[R] N)
            {
              toFun := fun (m : M) ↦
                HSub.hSub (α := N) (β := N) (⁅x, (f : (a : M) → N) m⁆ : N) ((f : (a : M) → N) ⁅x, m⁆ : N),
              map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] N }
            {
              toFun := fun (m : M) ↦
                HSub.hSub (α := N) (β := N) (⁅x, (g : (a : M) → N) m⁆ : N) ((g : (a : M) → N) ⁅x, m⁆ : N),
              map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] N } :
          (a : M) → N)
        n :
      N)
have h : HAdd.hAdd (α := N) (β := N) (⁅x, (f : (a : M) → N) n⁆ : N) (⁅x, (g : (a : M) → N) n⁆ : N) -
    HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) ⁅x, n⁆ : N) ((g : (a : M) → N) ⁅x, n⁆ : N) =
  HSub.hSub (α := N) (β := N) (⁅x, (f : (a : M) → N) n⁆ : N) ((f : (a : M) → N) ⁅x, n⁆ : N) +
    HSub.hSub (α := N) (β := N) (⁅x, (g : (a : M) → N) n⁆ : N) ((g : (a : M) → N) ⁅x, n⁆ : N)
Tactic: simp only [coe_mk, AddHom.coe_mk, lie_add, add_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : 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 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
t_1 : R
x_1 y z : L
m n : M
t : R
x : L
f : M →ₗ[R] N
⊢ ⁅t • x, f⁆ = t • ⁅x, f⁆
have h : ∀ (n : M), Eq.{w₁ + 1} (α := N) ((⁅t • x, f⁆ : (a : M) → N) n : N) ((t • ⁅x, f⁆ : (a : M) → N) n : N)
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : 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 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
t_1 : R
x_1 y z : L
m n : M
t : R
x : L
f : M →ₗ[R] N
⊢ ⁅x, t • f⁆ = t • ⁅x, f⁆
have h : ∀ (n : M), Eq.{w₁ + 1} (α := N) ((⁅x, t • f⁆ : (a : M) → N) n : N) ((t • ⁅x, f⁆ : (a : M) → N) n : N)
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : 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 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
t : R
x_1 y_1 z : L
m_1 n : M
x y : L
m : M →ₗ[R] R
⊢ { toFun := fun (m_2 : M) ↦ -(m : (a : M) → R) ⁅x + y, m_2⁆, map_add' := ⋯, map_smul' := ⋯ } =
    HAdd.hAdd (α := M →ₗ[R] R)
      { toFun := fun (m_2 : M) ↦ -(m : (a : M) → R) ⁅x, m_2⁆, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] R }
      { toFun := fun (m_2 : M) ↦ -(m : (a : M) → R) ⁅y, m_2⁆, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] R }
have h : ∀ (n : M),
  Eq.{u + 1} (α := R)
    (({ toFun := fun (m_2 : M) ↦ -(m : (a : M) → R) ⁅x + y, m_2⁆, map_add' := sorry, map_smul' := sorry } : (a : M) → R) n : R)
    ((HAdd.hAdd (α := M →ₗ[R] R)
            { toFun := fun (m_2 : M) ↦ -(m : (a : M) → R) ⁅x, m_2⁆, map_add' := sorry, map_smul' := sorry : M →ₗ[R] R }
            { toFun := fun (m_2 : M) ↦ -(m : (a : M) → R) ⁅y, m_2⁆, map_add' := sorry, map_smul' := sorry : M →ₗ[R] R } :
          (a : M) → R)
        n :
      R)
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : 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 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
t : R
x_1 y z : L
m_1 n_1 : M
x : L
m n : M →ₗ[R] R
⊢ { toFun := fun (m_2 : M) ↦ -(m + n : (a : M) → R) ⁅x, m_2⁆, map_add' := ⋯, map_smul' := ⋯ } =
    HAdd.hAdd (α := M →ₗ[R] R)
      { toFun := fun (m_2 : M) ↦ -(m : (a : M) → R) ⁅x, m_2⁆, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] R }
      { toFun := fun (m : M) ↦ -(n : (a : M) → R) ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] R }
have h : ∀ (p : M),
  Eq.{u + 1} (α := R)
    (({ toFun := fun (m_2 : M) ↦ -(m + n : (a : M) → R) ⁅x, m_2⁆, map_add' := sorry, map_smul' := sorry } : (a : M) → R) p : R)
    ((HAdd.hAdd (α := M →ₗ[R] R)
            { toFun := fun (m_2 : M) ↦ -(m : (a : M) → R) ⁅x, m_2⁆, map_add' := sorry, map_smul' := sorry : M →ₗ[R] R }
            { toFun := fun (m : M) ↦ -(n : (a : M) → R) ⁅x, m⁆, map_add' := sorry, map_smul' := sorry : M →ₗ[R] R } :
          (a : M) → R)
        p :
      R)
Tactic: ext p
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : 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 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
t : R
x_1 y z : L
m_1 n_1 : M
x m : L
n : M →ₗ[R] R
⊢ {
      toFun := fun (m_2 : M) ↦
        -({ toFun := fun (m_3 : M) ↦ -(n : (a : M) → R) ⁅m, m_3⁆, map_add' := ⋯, map_smul' := ⋯ } : (a : M) → R)
            ⁅x, m_2⁆,
      map_add' := ⋯, map_smul' := ⋯ } =
    HAdd.hAdd (α := M →ₗ[R] R)
      { toFun := fun (m_2 : M) ↦ -(n : (a : M) → R) ⁅⁅x, m⁆, m_2⁆, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] R }
      {
        toFun := fun (m_2 : M) ↦
          -({ toFun := fun (m : M) ↦ -(n : (a : M) → R) ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] R } :
                (a : M) → R)
              ⁅m, m_2⁆,
        map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] R }
have h : ∀ (p : M),
  Eq.{u + 1} (α := R)
    (({
            toFun := fun (m_2 : M) ↦
              -({ toFun := fun (m_3 : M) ↦ -(n : (a : M) → R) ⁅m, m_3⁆, map_add' := sorry, map_smul' := sorry } : (a : M) → R)
                  ⁅x, m_2⁆,
            map_add' := sorry, map_smul' := sorry } :
          (a : M) → R)
        p :
      R)
    ((HAdd.hAdd (α := M →ₗ[R] R)
            { toFun := fun (m_2 : M) ↦ -(n : (a : M) → R) ⁅⁅x, m⁆, m_2⁆, map_add' := sorry, map_smul' := sorry : M →ₗ[R] R }
            {
              toFun := fun (m_2 : M) ↦
                -({ toFun := fun (m : M) ↦ -(n : (a : M) → R) ⁅x, m⁆, map_add' := sorry, map_smul' := sorry : M →ₗ[R] R } :
                      (a : M) → R)
                    ⁅m, m_2⁆,
              map_add' := sorry, map_smul' := sorry : M →ₗ[R] R } :
          (a : M) → R)
        p :
      R)
Tactic: ext p
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : 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 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
t_1 : R
x_1 y z : L
m_1 n : M
t : R
x : L
m : M →ₗ[R] R
⊢ ⁅t • x, m⁆ = t • ⁅x, m⁆
have h : ∀ (n : M), Eq.{u + 1} (α := R) ((⁅t • x, m⁆ : (a : M) → R) n : R) ((t • ⁅x, m⁆ : (a : M) → R) n : R)
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
R : Type u
L : Type v
M : Type w
N : 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 : AddCommGroup N
inst_8 : Module R N
inst_9 : LieRingModule L N
inst_10 : LieModule R L N
t_1 : R
x_1 y z : L
m_1 n : M
t : R
x : L
m : M →ₗ[R] R
⊢ ⁅x, t • m⁆ = t • ⁅x, m⁆
have h : ∀ (n : M), Eq.{u + 1} (α := R) ((⁅x, t • m⁆ : (a : M) → R) n : R) ((t • ⁅x, m⁆ : (a : M) → R) n : R)
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
L : Type v
M : Type w
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
ι : Type u_1
κ : Type u_3
s : Finset ι
t : Finset κ
f : ι → L
g : κ → M
⊢ Eq.{w + 1} (α := M) (Bracket.bracket.{v, w} (L := L) (∑ i ∈ s, f i) (∑ j ∈ t, g j)) (∑ i ∈ s, ∑ j ∈ t, ⁅f i, g j⁆)
have simp_rw : Eq.{w + 1} (α := M) (∑ i ∈ s, ⁅f i, ∑ j ∈ t, g j⁆) (∑ i ∈ s, ∑ j ∈ t, ⁅f i, g j⁆)
Tactic: simp_rw [sum_lie, lie_sum]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieAlgebra R L₁
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
inst_5 : LieRing L₃
inst_6 : LieAlgebra R L₃
x y : L₁ →ₗ⁅R⁆ L₂
h :
  Eq (α := (a : L₁) → L₂) ((fun (f : L₁ →ₗ⁅R⁆ L₂) ↦ (↑f : L₁ →ₗ[R] L₂).toFun) x)
    ((fun (f : L₁ →ₗ⁅R⁆ L₂) ↦ (↑f : L₁ →ₗ[R] L₂).toFun) y)
⊢ x = y
have mk : ∀ (toLinearMap : L₁ →ₗ[R] L₂)
  (map_lie' : ∀ {x y : L₁}, toLinearMap.toFun ⁅x, y⁆ = ⁅toLinearMap.toFun x, toLinearMap.toFun y⁆)
  (h :
    Eq (α := (a : L₁) → L₂)
      ((fun (f : L₁ →ₗ⁅R⁆ L₂) ↦ (↑f : L₁ →ₗ[R] L₂).toFun) { toLinearMap := toLinearMap, map_lie' := @map_lie' })
      ((fun (f : L₁ →ₗ⁅R⁆ L₂) ↦ (↑f : L₁ →ₗ[R] L₂).toFun) y)),
  { toLinearMap := toLinearMap, map_lie' := @map_lie' : L₁ →ₗ⁅R⁆ L₂ } = y
Tactic: cases x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieAlgebra R L₁
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
inst_5 : LieRing L₃
inst_6 : LieAlgebra R L₃
y : L₁ →ₗ⁅R⁆ L₂
toLinearMap : L₁ →ₗ[R] L₂
map_lie' : ∀ {x y : L₁}, toLinearMap.toFun ⁅x, y⁆ = ⁅toLinearMap.toFun x, toLinearMap.toFun y⁆
h :
  Eq (α := (a : L₁) → L₂)
    ((fun (f : L₁ →ₗ⁅R⁆ L₂) ↦ (↑f : L₁ →ₗ[R] L₂).toFun) { toLinearMap := toLinearMap, map_lie' := @map_lie' })
    ((fun (f : L₁ →ₗ⁅R⁆ L₂) ↦ (↑f : L₁ →ₗ[R] L₂).toFun) y)
⊢ { toLinearMap := toLinearMap, map_lie' := @map_lie' : L₁ →ₗ⁅R⁆ L₂ } = y
have mk : ∀ (toLinearMap_1 : L₁ →ₗ[R] L₂)
  (map_lie'_1 : ∀ {x y : L₁}, toLinearMap_1.toFun ⁅x, y⁆ = ⁅toLinearMap_1.toFun x, toLinearMap_1.toFun y⁆)
  (h :
    Eq (α := (a : L₁) → L₂)
      ((fun (f : L₁ →ₗ⁅R⁆ L₂) ↦ (↑f : L₁ →ₗ[R] L₂).toFun) { toLinearMap := toLinearMap, map_lie' := @map_lie' })
      ((fun (f : L₁ →ₗ⁅R⁆ L₂) ↦ (↑f : L₁ →ₗ[R] L₂).toFun) { toLinearMap := toLinearMap_1, map_lie' := @map_lie'_1 })),
  { toLinearMap := toLinearMap, map_lie' := @map_lie' : L₁ →ₗ⁅R⁆ L₂ } =
    { toLinearMap := toLinearMap_1, map_lie' := @map_lie'_1 }
Tactic: cases y
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (hypothesis)
Goal:
R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieAlgebra R L₁
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
inst_5 : LieRing L₃
inst_6 : LieAlgebra R L₃
toLinearMap : L₁ →ₗ[R] L₂
map_lie' : ∀ {x y : L₁}, toLinearMap.toFun ⁅x, y⁆ = ⁅toLinearMap.toFun x, toLinearMap.toFun y⁆
toLinearMap_1 : L₁ →ₗ[R] L₂
map_lie'_1 : ∀ {x y : L₁}, toLinearMap_1.toFun ⁅x, y⁆ = ⁅toLinearMap_1.toFun x, toLinearMap_1.toFun y⁆
h :
  Eq (α := (a : L₁) → L₂)
    ((fun (f : L₁ →ₗ⁅R⁆ L₂) ↦ (↑f : L₁ →ₗ[R] L₂).toFun) { toLinearMap := toLinearMap, map_lie' := @map_lie' })
    ((fun (f : L₁ →ₗ⁅R⁆ L₂) ↦ (↑f : L₁ →ₗ[R] L₂).toFun) { toLinearMap := toLinearMap_1, map_lie' := @map_lie'_1 })
⊢ { toLinearMap := toLinearMap, map_lie' := @map_lie' : L₁ →ₗ⁅R⁆ L₂ } =
    { toLinearMap := toLinearMap_1, map_lie' := @map_lie'_1 }
have h₁ : toLinearMap = toLinearMap_1
Tactic: simp at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieAlgebra R L₁
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
inst_5 : LieRing L₃
inst_6 : LieAlgebra R L₃
x : L₁ →ₗ⁅R⁆ L₂
x_1 x_2 : L₁
⊢ (x : (a : L₁) → L₂) (x_1 + x_2) =
    HAdd.hAdd (α := L₂) (β := L₂) ((x : (a : L₁) → L₂) x_1 : L₂) ((x : (a : L₁) → L₂) x_2 : L₂)
have rw : ((↑x : L₁ →ₗ[R] L₂) : (a : L₁) → L₂) (x_1 + x_2) =
  HAdd.hAdd (α := L₂) (β := L₂) (((↑x : L₁ →ₗ[R] L₂) : (a : L₁) → L₂) x_1 : L₂)
    (((↑x : L₁ →ₗ[R] L₂) : (a : L₁) → L₂) x_2 : L₂)
Tactic: rw [← coe_toLinearMap, map_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieAlgebra R L₁
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
inst_5 : LieRing L₃
inst_6 : LieAlgebra R L₃
x : L₁ →ₗ⁅R⁆ L₂
x_1 x_2 : L₁
rw :
  ((↑x : L₁ →ₗ[R] L₂) : (a : L₁) → L₂) (x_1 + x_2) =
    HAdd.hAdd (α := L₂) (β := L₂) (((↑x : L₁ →ₗ[R] L₂) : (a : L₁) → L₂) x_1 : L₂)
      (((↑x : L₁ →ₗ[R] L₂) : (a : L₁) → L₂) x_2 : L₂)
⊢ (x : (a : L₁) → L₂) (x_1 + x_2) =
    HAdd.hAdd (α := L₂) (β := L₂) ((x : (a : L₁) → L₂) x_1 : L₂) ((x : (a : L₁) → L₂) x_2 : L₂)
have rw₁ : HAdd.hAdd (α := L₂) (β := L₂) (((↑x : L₁ →ₗ[R] L₂) : (a : L₁) → L₂) x_1 : L₂)
    (((↑x : L₁ →ₗ[R] L₂) : (a : L₁) → L₂) x_2 : L₂) =
  HAdd.hAdd (α := L₂) (β := L₂) (((↑x : L₁ →ₗ[R] L₂) : (a : L₁) → L₂) x_1 : L₂)
    (((↑x : L₁ →ₗ[R] L₂) : (a : L₁) → L₂) x_2 : L₂)
Tactic: rw [← coe_toLinearMap, map_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieAlgebra R L₁
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
inst_5 : LieRing L₃
inst_6 : LieAlgebra R L₃
x : L₁ →ₗ⁅R⁆ L₂
x_1 : R
x_2 : L₁
⊢ (x : (a : L₁) → L₂) (x_1 • x_2) =
    HSMul.hSMul (α := R) (β := L₂) ((RingHom.id R : (a : R) → R) x_1 : R) ((x : (a : L₁) → L₂) x_2 : L₂)
have rw : ((↑x : L₁ →ₗ[R] L₂) : (a : L₁) → L₂) (x_1 • x_2) =
  HSMul.hSMul (α := R) (β := L₂) ((RingHom.id R : (a : R) → R) x_1 : R) (((↑x : L₁ →ₗ[R] L₂) : (a : L₁) → L₂) x_2 : L₂)
Tactic: rw [← coe_toLinearMap, map_smulₛₗ]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieAlgebra R L₁
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
inst_5 : LieRing L₃
inst_6 : LieAlgebra R L₃
x : L₁ →ₗ⁅R⁆ L₂
x_1 : R
x_2 : L₁
rw :
  ((↑x : L₁ →ₗ[R] L₂) : (a : L₁) → L₂) (x_1 • x_2) =
    HSMul.hSMul (α := R) (β := L₂) ((RingHom.id R : (a : R) → R) x_1 : R)
      (((↑x : L₁ →ₗ[R] L₂) : (a : L₁) → L₂) x_2 : L₂)
⊢ (x : (a : L₁) → L₂) (x_1 • x_2) =
    HSMul.hSMul (α := R) (β := L₂) ((RingHom.id R : (a : R) → R) x_1 : R) ((x : (a : L₁) → L₂) x_2 : L₂)
have rw₁ : HSMul.hSMul (α := R) (β := L₂) ((RingHom.id R : (a : R) → R) x_1 : R) (((↑x : L₁ →ₗ[R] L₂) : (a : L₁) → L₂) x_2 : L₂) =
  HSMul.hSMul (α := R) (β := L₂) ((RingHom.id R : (a : R) → R) x_1 : R) (((↑x : L₁ →ₗ[R] L₂) : (a : L₁) → L₂) x_2 : L₂)
Tactic: rw [← coe_toLinearMap, map_smulₛₗ]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
R : Type u
L₁ : Type v
L₂ : Type w
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieAlgebra R L₁
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
f : L₁ →ₗ⁅R⁆ L₂
h₁ :
  ∀ (x y : L₁),
    (f : (a : L₁) → L₂) (x + y) =
      HAdd.hAdd (α := L₂) (β := L₂) ((f : (a : L₁) → L₂) x : L₂) ((f : (a : L₁) → L₂) y : L₂)
h₂ :
  ∀ (m : R) (x : L₁),
    { toFun := (⇑f : (a : L₁) → L₂), map_add' := h₁ : L₁ →ₙ+ L₂ }.toFun (m • x) =
      HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R)
        ({ toFun := (⇑f : (a : L₁) → L₂), map_add' := h₁ : L₁ →ₙ+ L₂ }.toFun x)
h₃ :
  ∀ {x y : L₁},
    { toFun := (⇑f : (a : L₁) → L₂), map_add' := h₁, map_smul' := h₂ : L₁ →ₗ[R] L₂ }.toFun ⁅x, y⁆ =
      ⁅{ toFun := (⇑f : (a : L₁) → L₂), map_add' := h₁, map_smul' := h₂ : L₁ →ₗ[R] L₂ }.toFun x,
        { toFun := (⇑f : (a : L₁) → L₂), map_add' := h₁, map_smul' := h₂ : L₁ →ₗ[R] L₂ }.toFun y⁆
⊢ { toFun := (⇑f : (a : L₁) → L₂), map_add' := h₁, map_smul' := h₂, map_lie' := @h₃ : L₁ →ₗ⁅R⁆ L₂ } = f
have h : ∀ (x : L₁),
  Eq.{w + 1} (α := L₂)
    (({ toFun := (⇑f : (a : L₁) → L₂), map_add' := h₁, map_smul' := h₂, map_lie' := @h₃ : L₁ →ₗ⁅R⁆ L₂ } : (a : L₁) → L₂)
        x :
      L₂)
    ((f : (a : L₁) → L₂) x : L₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieAlgebra R L₁
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
inst_5 : LieRing L₃
inst_6 : LieAlgebra R L₃
f : L₁ →ₗ⁅R⁆ L₂
g : L₂ → L₁
h₁ : LeftInverse g (⇑f : (a : L₁) → L₂)
h₂ : RightInverse g (⇑f : (a : L₁) → L₂)
x y : L₂
| g ⁅x, y⁆
have rw : g (Bracket.bracket (L := L₂) ((f : (a : L₁) → L₂) (g x) : L₂) ((f : (a : L₁) → L₂) (g y)))
Tactic: rw [← h₂ x, ← h₂ y]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieAlgebra R L₁
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
inst_5 : LieRing L₃
inst_6 : LieAlgebra R L₃
f : L₁ →ₗ⁅R⁆ L₂
g : L₂ → L₁
h₁ : LeftInverse g (⇑f : (a : L₁) → L₂)
h₂ : RightInverse g (⇑f : (a : L₁) → L₂)
x y : L₂
⊢ g ⁅x, y⁆ = g (Bracket.bracket (L := L₂) ((f : (a : L₁) → L₂) (g x) : L₂) ((f : (a : L₁) → L₂) (g y)))
have conv_lhs : g ⁅x, y⁆ = g (Bracket.bracket (L := L₂) ((f : (a : L₁) → L₂) (g x) : L₂) ((f : (a : L₁) → L₂) (g y)))
Tactic: conv_lhs => rw [← h₂ x, ← h₂ y]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieAlgebra R L₁
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
inst_5 : LieRing L₃
inst_6 : LieAlgebra R L₃
f : L₁ →ₗ⁅R⁆ L₂
g : L₂ → L₁
h₁ : LeftInverse g (⇑f : (a : L₁) → L₂)
h₂ : RightInverse g (⇑f : (a : L₁) → L₂)
x y : L₂
conv_lhs : g ⁅x, y⁆ = g (Bracket.bracket (L := L₂) ((f : (a : L₁) → L₂) (g x) : L₂) ((f : (a : L₁) → L₂) (g y)))
⊢ g ⁅x, y⁆ = g (Bracket.bracket (L := L₂) ((f : (a : L₁) → L₂) (g x) : L₂) ((f : (a : L₁) → L₂) (g y)))
have conv_lhs₁ : g (Bracket.bracket (L := L₂) ((f : (a : L₁) → L₂) (g x) : L₂) ((f : (a : L₁) → L₂) (g y))) =
  g (Bracket.bracket (L := L₂) ((f : (a : L₁) → L₂) (g x) : L₂) ((f : (a : L₁) → L₂) (g y)))
Tactic: conv_lhs => rw [← h₂ x, ← h₂ y]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieAlgebra R L₁
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
inst_5 : LieRing L₃
inst_6 : LieAlgebra R L₃
f : L₁ →ₗ⁅R⁆ L₂
g : L₂ → L₁
h₁ : LeftInverse g (⇑f : (a : L₁) → L₂)
h₂ : RightInverse g (⇑f : (a : L₁) → L₂)
x y : L₂
⊢ g (Bracket.bracket (L := L₂) ((f : (a : L₁) → L₂) (g x) : L₂) ((f : (a : L₁) → L₂) (g y))) =
    g ((f : (a : L₁) → L₂) ⁅g x, g y⁆)
have rw : g (Bracket.bracket (L := L₂) ((f : (a : L₁) → L₂) (g x) : L₂) ((f : (a : L₁) → L₂) (g y))) =
  g (Bracket.bracket (L := L₂) ((f : (a : L₁) → L₂) (g x) : L₂) ((f : (a : L₁) → L₂) (g y)))
Tactic: rw [map_lie]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieAlgebra R L₁
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
inst_5 : LieRing L₃
inst_6 : LieAlgebra R L₃
f : L₁ →ₗ⁅R⁆ L₂
g : L₂ → L₁
h₁ : LeftInverse g (⇑f : (a : L₁) → L₂)
h₂ : RightInverse g (⇑f : (a : L₁) → L₂)
x y : L₂
⊢ ((↑f : L₁ →ₗ[R] L₂).inverse g h₁ h₂).toFun ⁅x, y⁆ =
    ⁅((↑f : L₁ →ₗ[R] L₂).inverse g h₁ h₂).toFun x, ((↑f : L₁ →ₗ[R] L₂).inverse g h₁ h₂).toFun y⁆
have g₁ : g ⁅x, y⁆ = g (Bracket.bracket (L := L₂) ((f : (a : L₁) → L₂) (g x) : L₂) ((f : (a : L₁) → L₂) (g y)))
Tactic: calc
        g ⁅x, y⁆ = g ⁅f (g x), f (g y)⁆ := by conv_lhs => rw [← h₂ x, ← h₂ y]
        _ = g (f ⁅g x, g y⁆) := by rw [map_lie]
        _ = ⁅g x, g y⁆ := h₁ _
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieAlgebra R L₁
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
inst_5 : LieRing L₃
inst_6 : LieAlgebra R L₃
f : L₁ →ₗ⁅R⁆ L₂
g : L₂ → L₁
h₁ : LeftInverse g (⇑f : (a : L₁) → L₂)
h₂ : RightInverse g (⇑f : (a : L₁) → L₂)
x y : L₂
g₁ : g ⁅x, y⁆ = g (Bracket.bracket (L := L₂) ((f : (a : L₁) → L₂) (g x) : L₂) ((f : (a : L₁) → L₂) (g y)))
⊢ ((↑f : L₁ →ₗ[R] L₂).inverse g h₁ h₂).toFun ⁅x, y⁆ =
    ⁅((↑f : L₁ →ₗ[R] L₂).inverse g h₁ h₂).toFun x, ((↑f : L₁ →ₗ[R] L₂).inverse g h₁ h₂).toFun y⁆
have g₂ : g (Bracket.bracket (L := L₂) ((f : (a : L₁) → L₂) (g x) : L₂) ((f : (a : L₁) → L₂) (g y))) =
  g ((f : (a : L₁) → L₂) ⁅g x, g y⁆)
Tactic: calc
        g ⁅x, y⁆ = g ⁅f (g x), f (g y)⁆ := by conv_lhs => rw [← h₂ x, ← h₂ y]
        _ = g (f ⁅g x, g y⁆) := by rw [map_lie]
        _ = ⁅g x, g y⁆ := h₁ _
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
Goal:
R : Type u
L₁ : Type v
L₂ : Type w
L₃ : Type w₁
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieRing L₂
inst_3 : LieRing L₃
inst_4 : LieAlgebra R L₁
inst_5 : LieAlgebra R L₂
inst_6 : LieAlgebra R L₃
f g : L₁ ≃ₗ⁅R⁆ L₂
h₁ : (↑f.toLieHom : L₁ →ₗ[R] L₂).toFun = (↑g.toLieHom : L₁ →ₗ[R] L₂).toFun
h₂ : f.invFun = g.invFun
⊢ f = g
have mk : ∀ (toLieHom : L₁ →ₗ⁅R⁆ L₂) (invFun : L₂ → L₁) (left_inv : LeftInverse invFun (↑toLieHom : L₁ →ₗ[R] L₂).toFun)
  (right_inv : RightInverse invFun (↑toLieHom : L₁ →ₗ[R] L₂).toFun)
  (h₁ :
    (↑{ toLieHom := toLieHom, invFun := invFun, left_inv := left_inv, right_inv := right_inv : L₁ ≃ₗ⁅R⁆ L₂ }.toLieHom :
          L₁ →ₗ[R] L₂).toFun =
      (↑g.toLieHom : L₁ →ₗ[R] L₂).toFun)
  (h₂ :
    { toLieHom := toLieHom, invFun := invFun, left_inv := left_inv, right_inv := right_inv : L₁ ≃ₗ⁅R⁆ L₂ }.invFun =
      g.invFun),
  { toLieHom := toLieHom, invFun := invFun, left_inv := left_inv, right_inv := right_inv : L₁ ≃ₗ⁅R⁆ L₂ } = g
Tactic: cases f
Cleared hypotheses: f, h₁, h₂