awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Basic
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
simp_rw : Eq.{w + 1} (α := M) (∑ i ∈ s, ⁅f i, ∑ j ∈ t, g j⁆) (∑ i ∈ s, ∑ j ∈ t, ⁅f i, g j⁆)
⊢ 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⁆)

Tactic:
simp_rw [sum_lie, lie_sum]

Premises used: lie_sum, sum_lie
-- Module: Mathlib.Algebra.Lie.Basic
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)
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
⊢ x = y

Tactic:
cases x
-- Module: Mathlib.Algebra.Lie.Basic
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)
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 }
⊢ { toLinearMap := toLinearMap, map_lie' := @map_lie' : L₁ →ₗ⁅R⁆ L₂ } = y

Tactic:
cases y
-- Module: Mathlib.Algebra.Lie.Basic
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_1

Tactic:
simp at h
-- Module: Mathlib.Algebra.Lie.Basic
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 : toLinearMap = toLinearMap_1
⊢ { toLinearMap := toLinearMap, map_lie' := @map_lie' : L₁ →ₗ⁅R⁆ L₂ } =
    { toLinearMap := toLinearMap_1, map_lie' := @map_lie'_1 }

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Lie.Basic
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₂
⊢ Eq (α := (a : L₁) → L₂) (⇑(↑f : L₁ →ₗ[R] L₂) : (a : L₁) → L₂) (⇑f : (a : L₁) → L₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Basic
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₂
⊢ (↑f : L₁ →ₗ[R] L₂).toFun = (⇑f : (a : L₁) → L₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Basic
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₂)
rw₁ 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₂)
⊢ (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₂)

Tactic:
rw [← coe_toLinearMap, map_add]

Premises used: map_add, LieHom.coe_toLinearMap
-- Module: Mathlib.Algebra.Lie.Basic
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₂)
rw₁ 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₂)
⊢ (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₂)

Tactic:
rw [← coe_toLinearMap, map_smulₛₗ]

Premises used: MulActionSemiHomClass.map_smulₛₗ, LieHom.coe_toLinearMap
-- Module: Mathlib.Algebra.Lie.Basic
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₂
x y : L₁
⊢ Eq.{w + 1} (α := L₂) ((f : (a : L₁) → L₂) ⁅x, y⁆ : L₂)
    (Bracket.bracket (L := L₂) ((f : (a : L₁) → L₂) x : L₂) ((f : (a : L₁) → L₂) y) : L₂)

Tactic:
LieHom.map_lie' f

Premises used: LieHom.map_lie'
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L₁ : Type v
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieAlgebra R L₁
⊢ Eq.{v + 1} (α := (a : L₁) → L₁) (⇑id : (a : L₁) → L₁) _root_.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L₁ : Type v
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieAlgebra R L₁
x : L₁
⊢ (id : (a : L₁) → L₁) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Basic
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₁},
    Eq.{w + 1} (α := L₂) (AddHom.toFun (LinearMap.toAddHom.{u, u, v, w} (R := R) (S := R) (σ := RingHom.id R) 0) ⁅x, y⁆)
      (Bracket.bracket (L := L₂)
        (AddHom.toFun (LinearMap.toAddHom.{u, u, v, w} (R := R) (S := R) (σ := RingHom.id R) 0) x)
        (AddHom.toFun (LinearMap.toAddHom.{u, u, v, w} (R := R) (S := R) (σ := RingHom.id R) 0) y))

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Basic
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₂
⊢ Eq (α := (a : L₁) → L₂) (⇑0 : (a : L₁) → L₂) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Basic
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₂
x : L₁
⊢ Eq.{w + 1} (α := L₂) ((0 : (a : L₁) → L₂) x : L₂) (0 : L₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L₁ : Type v
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieAlgebra R L₁
⊢ Eq.{v + 1} (α := (a : L₁) → L₁) (⇑1 : (a : L₁) → L₁) _root_.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L₁ : Type v
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieAlgebra R L₁
x : L₁
⊢ (1 : (a : L₁) → L₁) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Basic
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₁ → L₂
map_add' : ∀ (x y : L₁), f (x + y) = f x + f y
map_smul' :
  ∀ (m : R) (x : L₁),
    { toFun := f, map_add' := map_add' : L₁ →ₙ+ L₂ }.toFun (m • x) =
      HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R)
        ({ toFun := f, map_add' := map_add' : L₁ →ₙ+ L₂ }.toFun x)
map_lie' :
  ∀ {x y : L₁},
    { toFun := f, map_add' := map_add', map_smul' := map_smul' : L₁ →ₗ[R] L₂ }.toFun ⁅x, y⁆ =
      ⁅{ toFun := f, map_add' := map_add', map_smul' := map_smul' : L₁ →ₗ[R] L₂ }.toFun x,
        { toFun := f, map_add' := map_add', map_smul' := map_smul' : L₁ →ₗ[R] L₂ }.toFun y⁆
g : L₁ → L₂
map_add'_1 : ∀ (x y : L₁), g (x + y) = g x + g y
map_smul'_1 :
  ∀ (m : R) (x : L₁),
    { toFun := g, map_add' := map_add'_1 : L₁ →ₙ+ L₂ }.toFun (m • x) =
      HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R)
        ({ toFun := g, map_add' := map_add'_1 : L₁ →ₙ+ L₂ }.toFun x)
map_lie'_1 :
  ∀ {x y : L₁},
    { toFun := g, map_add' := map_add'_1, map_smul' := map_smul'_1 : L₁ →ₗ[R] L₂ }.toFun ⁅x, y⁆ =
      ⁅{ toFun := g, map_add' := map_add'_1, map_smul' := map_smul'_1 : L₁ →ₗ[R] L₂ }.toFun x,
        { toFun := g, map_add' := map_add'_1, map_smul' := map_smul'_1 : L₁ →ₗ[R] L₂ }.toFun y⁆
h :
  Eq (α := L₁ → L₂)
    (⇑{ toFun := f, map_add' := map_add', map_smul' := map_smul', map_lie' := @map_lie' : L₁ →ₗ⁅R⁆ L₂ } : (a : L₁) → L₂)
    (⇑{ toFun := g, map_add' := map_add'_1, map_smul' := map_smul'_1, map_lie' := @map_lie'_1 : L₁ →ₗ⁅R⁆ L₂ } :
      (a : L₁) → L₂)
⊢ { toFun := f, map_add' := map_add', map_smul' := map_smul', map_lie' := @map_lie' : L₁ →ₗ⁅R⁆ L₂ } =
    { toFun := g, map_add' := map_add'_1, map_smul' := map_smul'_1, map_lie' := @map_lie'_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Lie.Basic
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 g : L₁ →ₗ⁅R⁆ L₂
h : ∀ (x : L₁), Eq.{w + 1} (α := L₂) ((f : (a : L₁) → L₂) x : L₂) ((g : (a : L₁) → L₂) x : L₂)
⊢ f = g

Tactic:
coe_injective <| funext h

Premises used: funext, LieHom.coe_injective
-- Module: Mathlib.Algebra.Lie.Basic
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 g : L₁ →ₗ⁅R⁆ L₂
h : f = g
x : L₁
⊢ Eq.{w + 1} (α := L₂) ((f : (a : L₁) → L₂) x : L₂) ((g : (a : L₁) → L₂) x : L₂)

Tactic:
h ▸ rfl

Premises used: Eq.rec, rfl
-- Module: Mathlib.Algebra.Lie.Basic
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⁆
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₂)
⊢ { toFun := (⇑f : (a : L₁) → L₂), map_add' := h₁, map_smul' := h₂, map_lie' := @h₃ : L₁ →ₗ⁅R⁆ L₂ } = f

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Basic
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⁆
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:
rfl
-- Module: Mathlib.Algebra.Lie.Basic
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₁ → L₂
h₁ : ∀ (x y : L₁), f (x + y) = f x + f y
h₂ :
  ∀ (m : R) (x : L₁),
    { toFun := f, map_add' := h₁ : L₁ →ₙ+ L₂ }.toFun (m • x) =
      HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R) ({ toFun := f, map_add' := h₁ : L₁ →ₙ+ L₂ }.toFun x)
h₃ :
  ∀ {x y : L₁},
    { toFun := f, map_add' := h₁, map_smul' := h₂ : L₁ →ₗ[R] L₂ }.toFun ⁅x, y⁆ =
      ⁅{ toFun := f, map_add' := h₁, map_smul' := h₂ : L₁ →ₗ[R] L₂ }.toFun x,
        { toFun := f, map_add' := h₁, map_smul' := h₂ : L₁ →ₗ[R] L₂ }.toFun y⁆
⊢ (⇑{ toFun := f, map_add' := h₁, map_smul' := h₂, map_lie' := @h₃ : L₁ →ₗ⁅R⁆ L₂ } : (a : L₁) → L₂) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Basic
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₁ →ₗ⁅R⁆ L₂
⊢ ∀ {x y : L₁},
    ((↑f : L₂ →ₗ[R] L₃) ∘ₗ (↑g : L₁ →ₗ[R] L₂)).toFun ⁅x, y⁆ =
      ⁅((↑f : L₂ →ₗ[R] L₃) ∘ₗ (↑g : L₁ →ₗ[R] L₂)).toFun x, ((↑f : L₂ →ₗ[R] L₃) ∘ₗ (↑g : L₁ →ₗ[R] L₂)).toFun y⁆

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Basic
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₁ →ₗ⁅R⁆ L₂
x : L₁
⊢ Eq.{w₁ + 1} (α := L₃) ((f.comp g : (a : L₁) → L₃) x : L₃) ((f : (a : L₂) → L₃) ((g : (a : L₁) → L₂) x : L₂) : L₃)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Basic
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₁ →ₗ⁅R⁆ L₂
⊢ Eq (α := (a : L₁) → L₃) (⇑(f.comp g) : (a : L₁) → L₃)
    (Function.comp.{v + 1, w + 1, w₁ + 1} (β := L₂) (⇑f : (a : L₂) → L₃) (⇑g : (a : L₁) → L₂))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Basic
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₁ →ₗ⁅R⁆ L₂
⊢ (↑(f.comp g) : L₁ →ₗ[R] L₃) = (↑f : L₂ →ₗ[R] L₃) ∘ₗ (↑g : L₁ →ₗ[R] L₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Basic
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₂
⊢ f.comp id = f

Tactic:
rfl

Premises used: LieHom.comp, rfl
-- Module: Mathlib.Algebra.Lie.Basic
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₂
⊢ comp id f = f

Tactic:
rfl

Premises used: LieHom.comp, rfl
-- Module: Mathlib.Algebra.Lie.Basic
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₂
rw : g (Bracket.bracket (L := L₂) ((f : (a : L₁) → L₂) (g x) : L₂) ((f : (a : L₁) → L₂) (g y)))
| g ⁅x, y⁆

Tactic:
rw [← h₂ x, ← h₂ y]
-- Module: Mathlib.Algebra.Lie.Basic
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)))
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)))
⊢ 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]
-- Module: Mathlib.Algebra.Lie.Basic
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₂
rw 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)))
⊢ 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:
rw [map_lie]

Premises used: LieHom.map_lie
-- Module: Mathlib.Algebra.Lie.Basic
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 ((f : (a : L₁) → L₂) ⁅g x, g y⁆) = ⁅g x, g y⁆

Tactic:
h₁ _
-- Module: Mathlib.Algebra.Lie.Basic
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)))
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⁆)
⊢ ((↑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⁆

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₁ _

Premises used: Bracket.bracket, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L₁ : Type v
L₂ : Type w
M : 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 : AddCommGroup M
inst_6 : LieRingModule L₂ M
f : L₁ →ₗ⁅R⁆ L₂
x y : L₁
m : M
⊢ Bracket.bracket.{w, w₁} (L := L₂) ((f : (a : L₁) → L₂) (x + y) : L₂) m =
    Bracket.bracket.{w, w₁} (L := L₂) ((f : (a : L₁) → L₂) x : L₂) m +
      Bracket.bracket.{w, w₁} (L := L₂) ((f : (a : L₁) → L₂) y : L₂) m

Tactic:
simp only [map_add, add_lie]

Premises used: map_add, add_lie
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L₁ : Type v
L₂ : Type w
M : 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 : AddCommGroup M
inst_6 : LieRingModule L₂ M
f : L₁ →ₗ⁅R⁆ L₂
x y : L₁
m : M
⊢ Bracket.bracket.{w, w₁} (L := L₂) ((f : (a : L₁) → L₂) x : L₂)
      (Bracket.bracket.{w, w₁} (L := L₂) ((f : (a : L₁) → L₂) y : L₂) m) =
    Bracket.bracket.{w, w₁} (L := L₂) ((f : (a : L₁) → L₂) ⁅x, y⁆ : L₂) m +
      Bracket.bracket.{w, w₁} (L := L₂) ((f : (a : L₁) → L₂) y : L₂)
        (Bracket.bracket.{w, w₁} (L := L₂) ((f : (a : L₁) → L₂) x : L₂) m)

Tactic:
simp only [lie_lie, sub_add_cancel, LieHom.map_lie]

Premises used: LieHom.map_lie, sub_add_cancel, lie_lie
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L₁ : Type v
L₂ : Type w
M : 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 : AddCommGroup M
inst_6 : LieRingModule L₂ M
f : L₁ →ₗ⁅R⁆ L₂
x : L₁
m : M
⊢ ⁅x, m⁆ = Bracket.bracket.{w, w₁} (L := L₂) ((f : (a : L₁) → L₂) x : L₂) m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L₁ : Type v
L₂ : Type w
M : 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 : AddCommGroup M
inst_6 : LieRingModule L₂ M
f : L₁ →ₗ⁅R⁆ L₂
inst_7 : Module R M
inst_8 : LieModule R L₂ M
t : R
x : L₁
m : M
⊢ ⁅t • x, m⁆ = t • ⁅x, m⁆

Tactic:
simp only [LieRingModule.compLieHom_apply, smul_lie, map_smul]

Premises used: LieRingModule.compLieHom_apply, smul_lie, map_smul
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L₁ : Type v
L₂ : Type w
M : 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 : AddCommGroup M
inst_6 : LieRingModule L₂ M
f : L₁ →ₗ⁅R⁆ L₂
inst_7 : Module R M
inst_8 : LieModule R L₂ M
t : R
x : L₁
m : M
⊢ ⁅x, t • m⁆ = t • ⁅x, m⁆

Tactic:
simp only [LieRingModule.compLieHom_apply, lie_smul]

Premises used: lie_smul, LieRingModule.compLieHom_apply
-- Module: Mathlib.Algebra.Lie.Basic
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
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
⊢ f = g

Tactic:
cases f