awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : LieRingModule L M
inst_9 : LieRingModule L N
inst_10 : LieRingModule L P
inst_11 : LieAlgebra R L
inst_12 : LieModule R L N
inst_13 : LieModule R L P
f : M →ₗ⁅R,L⁆ N →ₗ[R] P
x : L
m : M
n : N
⊢ ⁅x, (((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) n⁆ =
    HAdd.hAdd (α := P) (β := P) ((((f : (a : M) → N →ₗ[R] P) ⁅x, m⁆ : N →ₗ[R] P) : (a : N) → P) n : P)
      ((((f : (a : M) → N →ₗ[R] P) m : N →ₗ[R] P) : (a : N) → P) ⁅x, n⁆ : P)

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

Premises used: LieHom.lie_apply, LieModuleHom.map_lie, sub_add_cancel
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
⊢ Eq.{w + 1} (α := (a : M) → M) (⇑id : (a : M) → M) _root_.id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
x : M
⊢ (id : (a : M) → M) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : LieRingModule L M
inst_9 : LieRingModule L N
inst_10 : LieRingModule L P
⊢ ∀ {x : L} {m : M},
    Eq.{w₁ + 1} (α := N)
      (AddHom.toFun (LinearMap.toAddHom.{u, u, w, w₁} (R := R) (S := R) (σ := RingHom.id R) 0) ⁅x, m⁆)
      ⁅x, AddHom.toFun (LinearMap.toAddHom.{u, u, w, w₁} (R := R) (S := R) (σ := RingHom.id R) 0) m⁆

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : LieRingModule L M
inst_7 : LieRingModule L N
⊢ Eq (α := (a : M) → N) (⇑0 : (a : M) → N) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : LieRingModule L M
inst_7 : LieRingModule L N
m : M
⊢ Eq.{w₁ + 1} (α := N) ((0 : (a : M) → N) m : N) (0 : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : LieRingModule L M
inst_7 : LieRingModule L N
f : M → N
map_add' : ∀ (x y : M), f (x + y) = f x + f y
map_smul' :
  ∀ (m : R) (x : M),
    { toFun := f, map_add' := map_add' : M →ₙ+ N }.toFun (m • x) =
      HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R) ({ toFun := f, map_add' := map_add' : M →ₙ+ N }.toFun x)
map_lie' :
  ∀ {x : L} {m : M},
    { toFun := f, map_add' := map_add', map_smul' := map_smul' : M →ₗ[R] N }.toFun ⁅x, m⁆ =
      ⁅x, { toFun := f, map_add' := map_add', map_smul' := map_smul' : M →ₗ[R] N }.toFun m⁆
g : M → N
map_add'_1 : ∀ (x y : M), g (x + y) = g x + g y
map_smul'_1 :
  ∀ (m : R) (x : M),
    { toFun := g, map_add' := map_add'_1 : M →ₙ+ N }.toFun (m • x) =
      HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m : R)
        ({ toFun := g, map_add' := map_add'_1 : M →ₙ+ N }.toFun x)
map_lie'_1 :
  ∀ {x : L} {m : M},
    { toFun := g, map_add' := map_add'_1, map_smul' := map_smul'_1 : M →ₗ[R] N }.toFun ⁅x, m⁆ =
      ⁅x, { toFun := g, map_add' := map_add'_1, map_smul' := map_smul'_1 : M →ₗ[R] N }.toFun m⁆
h :
  Eq (α := M → N)
    (⇑{ toFun := f, map_add' := map_add', map_smul' := map_smul', map_lie' := @map_lie' : M →ₗ⁅R,L⁆ N } : (a : M) → N)
    (⇑{ toFun := g, map_add' := map_add'_1, map_smul' := map_smul'_1, map_lie' := @map_lie'_1 : M →ₗ⁅R,L⁆ N } :
      (a : M) → N)
⊢ { toFun := f, map_add' := map_add', map_smul' := map_smul', map_lie' := @map_lie' : M →ₗ⁅R,L⁆ N } =
    { 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
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : LieRingModule L M
inst_7 : LieRingModule L N
f g : M →ₗ⁅R,L⁆ N
h : ∀ (m : M), Eq.{w₁ + 1} (α := N) ((f : (a : M) → N) m : N) ((g : (a : M) → N) m : N)
⊢ f = g

Tactic:
coe_injective <| funext h

Premises used: LieModuleHom.coe_injective, funext
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : LieRingModule L M
inst_7 : LieRingModule L N
f g : M →ₗ⁅R,L⁆ N
h : f = g
x : M
⊢ Eq.{w₁ + 1} (α := N) ((f : (a : M) → N) x : N) ((g : (a : M) → N) x : N)

Tactic:
h ▸ rfl

Premises used: Eq.rec, rfl
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : LieRingModule L M
inst_7 : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
h : ∀ {x : L} {m : M}, (↑f : M →ₗ[R] N).toFun ⁅x, m⁆ = ⁅x, (↑f : M →ₗ[R] N).toFun m⁆
⊢ { toLinearMap := (↑f : M →ₗ[R] N), map_lie' := @h : M →ₗ⁅R,L⁆ N } = f

Tactic:
rfl
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : LieRingModule L M
inst_7 : LieRingModule L N
f : M →ₗ[R] N
h : ∀ {x : L} {m : M}, f.toFun ⁅x, m⁆ = ⁅x, f.toFun m⁆
⊢ Eq (α := (a : M) → N) (⇑{ toLinearMap := f, map_lie' := @h : M →ₗ⁅R,L⁆ N } : (a : M) → N) (⇑f : (a : M) → N)

Tactic:
rfl
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : LieRingModule L M
inst_7 : LieRingModule L N
f : M →ₗ[R] N
h : ∀ {x : L} {m : M}, f.toFun ⁅x, m⁆ = ⁅x, f.toFun m⁆
⊢ (↑{ toLinearMap := f, map_lie' := @h : M →ₗ⁅R,L⁆ N } : M →ₗ[R] N) = f

Tactic:
rfl
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : LieRingModule L M
inst_9 : LieRingModule L N
inst_10 : LieRingModule L P
f : N →ₗ⁅R,L⁆ P
g : M →ₗ⁅R,L⁆ N
⊢ ∀ {x : L} {m : M},
    ((↑f : N →ₗ[R] P) ∘ₗ (↑g : M →ₗ[R] N)).toFun ⁅x, m⁆ = ⁅x, ((↑f : N →ₗ[R] P) ∘ₗ (↑g : M →ₗ[R] N)).toFun m⁆

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : LieRingModule L M
inst_9 : LieRingModule L N
inst_10 : LieRingModule L P
f : N →ₗ⁅R,L⁆ P
g : M →ₗ⁅R,L⁆ N
m : M
⊢ Eq.{w₂ + 1} (α := P) ((f.comp g : (a : M) → P) m : P) ((f : (a : N) → P) ((g : (a : M) → N) m : N) : P)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : LieRingModule L M
inst_9 : LieRingModule L N
inst_10 : LieRingModule L P
f : N →ₗ⁅R,L⁆ P
g : M →ₗ⁅R,L⁆ N
⊢ Eq (α := (a : M) → P) (⇑(f.comp g) : (a : M) → P)
    (Function.comp.{w + 1, w₁ + 1, w₂ + 1} (β := N) (⇑f : (a : N) → P) (⇑g : (a : M) → N))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : LieRingModule L M
inst_9 : LieRingModule L N
inst_10 : LieRingModule L P
f : N →ₗ⁅R,L⁆ P
g : M →ₗ⁅R,L⁆ N
⊢ (↑(f.comp g) : M →ₗ[R] P) = (↑f : N →ₗ[R] P) ∘ₗ (↑g : M →ₗ[R] N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : LieRingModule L M
inst_9 : LieRingModule L N
inst_10 : LieRingModule L P
f : M →ₗ⁅R,L⁆ N
g : N → M
h₁ : LeftInverse g (⇑f : (a : M) → N)
h₂ : RightInverse g (⇑f : (a : M) → N)
x : L
n : N
rw rw₁ : g ⁅x, n⁆ = g ⁅x, n⁆
⊢ g ⁅x, n⁆ = g ⁅x, (f : (a : M) → N) (g n)⁆

Tactic:
rw [h₂]
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : LieRingModule L M
inst_9 : LieRingModule L N
inst_10 : LieRingModule L P
f : M →ₗ⁅R,L⁆ N
g : N → M
h₁ : LeftInverse g (⇑f : (a : M) → N)
h₂ : RightInverse g (⇑f : (a : M) → N)
x : L
n : N
rw rw₁ : g ⁅x, (f : (a : M) → N) (g n)⁆ = g ⁅x, (f : (a : M) → N) (g n)⁆
⊢ g ⁅x, (f : (a : M) → N) (g n)⁆ = g ((f : (a : M) → N) ⁅x, g n⁆)

Tactic:
rw [map_lie]

Premises used: LieModuleHom.map_lie
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : LieRingModule L M
inst_9 : LieRingModule L N
inst_10 : LieRingModule L P
f : M →ₗ⁅R,L⁆ N
g : N → M
h₁ : LeftInverse g (⇑f : (a : M) → N)
h₂ : RightInverse g (⇑f : (a : M) → N)
x : L
n : N
⊢ g ((f : (a : M) → N) ⁅x, g n⁆) = ⁅x, g n⁆

Tactic:
h₁ _
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : LieRingModule L M
inst_9 : LieRingModule L N
inst_10 : LieRingModule L P
f : M →ₗ⁅R,L⁆ N
g : N → M
h₁ : LeftInverse g (⇑f : (a : M) → N)
h₂ : RightInverse g (⇑f : (a : M) → N)
x : L
n : N
g₁ : g ⁅x, n⁆ = g ⁅x, (f : (a : M) → N) (g n)⁆
g₂ : g ⁅x, (f : (a : M) → N) (g n)⁆ = g ((f : (a : M) → N) ⁅x, g n⁆)
⊢ ((↑f : M →ₗ[R] N).inverse g h₁ h₂).toFun ⁅x, n⁆ = ⁅x, ((↑f : M →ₗ[R] N).inverse g h₁ h₂).toFun n⁆

Tactic:
calc
        g ⁅x, n⁆ = g ⁅x, f (g n)⁆ := by rw [h₂]
        _ = g (f ⁅x, g n⁆) := by rw [map_lie]
        _ = ⁅x, g n⁆ := h₁ _

Premises used: Bracket.bracket, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : LieRingModule L M
inst_9 : LieRingModule L N
inst_10 : LieRingModule L P
f g : M →ₗ⁅R,L⁆ N
⊢ ∀ {x : L} {m : M},
    ((↑f : M →ₗ[R] N) + (↑g : M →ₗ[R] N)).toFun ⁅x, m⁆ = ⁅x, ((↑f : M →ₗ[R] N) + (↑g : M →ₗ[R] N)).toFun m⁆

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : LieRingModule L M
inst_9 : LieRingModule L N
inst_10 : LieRingModule L P
f g : M →ₗ⁅R,L⁆ N
⊢ ∀ {x : L} {m : M},
    ((↑f : M →ₗ[R] N) - (↑g : M →ₗ[R] N)).toFun ⁅x, m⁆ = ⁅x, ((↑f : M →ₗ[R] N) - (↑g : M →ₗ[R] N)).toFun m⁆

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : LieRingModule L M
inst_9 : LieRingModule L N
inst_10 : LieRingModule L P
f : M →ₗ⁅R,L⁆ N
⊢ ∀ {x : L} {m : M}, (-(↑f : M →ₗ[R] N)).toFun ⁅x, m⁆ = ⁅x, (-(↑f : M →ₗ[R] N)).toFun m⁆

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : LieRingModule L M
inst_7 : LieRingModule L N
f g : M →ₗ⁅R,L⁆ N
⊢ (⇑(f + g) : (a : M) → N) = HAdd.hAdd (α := (a : M) → N) (⇑f : (a : M) → N) (⇑g : (a : M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : LieRingModule L M
inst_7 : LieRingModule L N
f g : M →ₗ⁅R,L⁆ N
m : M
⊢ (f + g : (a : M) → N) m = HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) m : N) ((g : (a : M) → N) m : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : LieRingModule L M
inst_7 : LieRingModule L N
f g : M →ₗ⁅R,L⁆ N
⊢ (⇑(f - g) : (a : M) → N) = HSub.hSub (α := (a : M) → N) (⇑f : (a : M) → N) (⇑g : (a : M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : LieRingModule L M
inst_7 : LieRingModule L N
f g : M →ₗ⁅R,L⁆ N
m : M
⊢ (f - g : (a : M) → N) m = HSub.hSub (α := N) (β := N) ((f : (a : M) → N) m : N) ((g : (a : M) → N) m : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : LieRingModule L M
inst_7 : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
⊢ Eq (α := (a : M) → N) (⇑(-f) : (a : M) → N) (-(⇑f : (a : M) → N))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : LieRingModule L M
inst_7 : LieRingModule L N
f : M →ₗ⁅R,L⁆ N
m : M
⊢ Eq.{w₁ + 1} (α := N) ((-f : (a : M) → N) m : N) (-(f : (a : M) → N) m : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : LieRingModule L M
inst_9 : LieRingModule L N
inst_10 : LieRingModule L P
n : ℕ
f : M →ₗ⁅R,L⁆ N
⊢ ∀ {x : L} {m : M}, (n • (↑f : M →ₗ[R] N)).toFun ⁅x, m⁆ = ⁅x, (n • (↑f : M →ₗ[R] N)).toFun m⁆

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : LieRingModule L M
inst_7 : LieRingModule L N
n : ℕ
f : M →ₗ⁅R,L⁆ N
⊢ (⇑(n • f) : (a : M) → N) = HSMul.hSMul (β := (a : M) → N) n (⇑f : (a : M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : LieRingModule L M
inst_7 : LieRingModule L N
n : ℕ
f : M →ₗ⁅R,L⁆ N
m : M
⊢ (n • f : (a : M) → N) m = HSMul.hSMul (β := N) n ((f : (a : M) → N) m : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : LieRingModule L M
inst_9 : LieRingModule L N
inst_10 : LieRingModule L P
z : ℤ
f : M →ₗ⁅R,L⁆ N
⊢ ∀ {x : L} {m : M}, (z • (↑f : M →ₗ[R] N)).toFun ⁅x, m⁆ = ⁅x, (z • (↑f : M →ₗ[R] N)).toFun m⁆

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : LieRingModule L M
inst_7 : LieRingModule L N
z : ℤ
f : M →ₗ⁅R,L⁆ N
⊢ (⇑(z • f) : (a : M) → N) = HSMul.hSMul (β := (a : M) → N) z (⇑f : (a : M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : LieRingModule L M
inst_7 : LieRingModule L N
z : ℤ
f : M →ₗ⁅R,L⁆ N
m : M
⊢ (z • f : (a : M) → N) m = HSMul.hSMul (β := N) z ((f : (a : M) → N) m : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : LieRingModule L M
inst_9 : LieRingModule L N
inst_10 : LieRingModule L P
inst_11 : LieAlgebra R L
inst_12 : LieModule R L N
t : R
f : M →ₗ⁅R,L⁆ N
⊢ ∀ {x : L} {m : M}, (t • (↑f : M →ₗ[R] N)).toFun ⁅x, m⁆ = ⁅x, (t • (↑f : M →ₗ[R] N)).toFun m⁆

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : LieRingModule L M
inst_7 : LieRingModule L N
inst_8 : LieAlgebra R L
inst_9 : LieModule R L N
t : R
f : M →ₗ⁅R,L⁆ N
⊢ (⇑(t • f) : (a : M) → N) = HSMul.hSMul (β := (a : M) → N) t (⇑f : (a : M) → N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : Module R M
inst_5 : Module R N
inst_6 : LieRingModule L M
inst_7 : LieRingModule L N
inst_8 : LieAlgebra R L
inst_9 : LieModule R L N
t : R
f : M →ₗ⁅R,L⁆ N
m : M
⊢ (t • f : (a : M) → N) m = HSMul.hSMul (β := N) t ((f : (a : M) → N) m : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : LieRingModule L M
inst_9 : LieRingModule L N
inst_10 : LieRingModule L P
f g : M ≃ₗ⁅R,L⁆ N
h₁ : (↑f.toLieModuleHom : M →ₗ[R] N).toFun = (↑g.toLieModuleHom : M →ₗ[R] N).toFun
h₂ : f.invFun = g.invFun
mk :
  ∀ (toLieModuleHom : M →ₗ⁅R,L⁆ N) (invFun : N → M) (left_inv : LeftInverse invFun (↑toLieModuleHom : M →ₗ[R] N).toFun)
    (right_inv : RightInverse invFun (↑toLieModuleHom : M →ₗ[R] N).toFun)
    (h₁ :
      (↑{ toLieModuleHom := toLieModuleHom, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
                  M ≃ₗ⁅R,L⁆ N }.toLieModuleHom :
            M →ₗ[R] N).toFun =
        (↑g.toLieModuleHom : M →ₗ[R] N).toFun)
    (h₂ :
      { toLieModuleHom := toLieModuleHom, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
            M ≃ₗ⁅R,L⁆ N }.invFun =
        g.invFun),
    { toLieModuleHom := toLieModuleHom, invFun := invFun, left_inv := left_inv, right_inv := right_inv : M ≃ₗ⁅R,L⁆ N } =
      g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : LieRingModule L M
inst_9 : LieRingModule L N
inst_10 : LieRingModule L P
g : M ≃ₗ⁅R,L⁆ N
toLieModuleHom : M →ₗ⁅R,L⁆ N
invFun : N → M
left_inv : LeftInverse invFun (↑toLieModuleHom : M →ₗ[R] N).toFun
right_inv : RightInverse invFun (↑toLieModuleHom : M →ₗ[R] N).toFun
h₁ :
  (↑{ toLieModuleHom := toLieModuleHom, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
              M ≃ₗ⁅R,L⁆ N }.toLieModuleHom :
        M →ₗ[R] N).toFun =
    (↑g.toLieModuleHom : M →ₗ[R] N).toFun
h₂ :
  { toLieModuleHom := toLieModuleHom, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
        M ≃ₗ⁅R,L⁆ N }.invFun =
    g.invFun
mk :
  ∀ (toLieModuleHom_1 : M →ₗ⁅R,L⁆ N) (invFun_1 : N → M)
    (left_inv_1 : LeftInverse invFun_1 (↑toLieModuleHom_1 : M →ₗ[R] N).toFun)
    (right_inv_1 : RightInverse invFun_1 (↑toLieModuleHom_1 : M →ₗ[R] N).toFun)
    (h₁ :
      (↑{ toLieModuleHom := toLieModuleHom, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
                  M ≃ₗ⁅R,L⁆ N }.toLieModuleHom :
            M →ₗ[R] N).toFun =
        (↑{ toLieModuleHom := toLieModuleHom_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 :
                  M ≃ₗ⁅R,L⁆ N }.toLieModuleHom :
            M →ₗ[R] N).toFun)
    (h₂ :
      { toLieModuleHom := toLieModuleHom, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
            M ≃ₗ⁅R,L⁆ N }.invFun =
        { toLieModuleHom := toLieModuleHom_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 :
            M ≃ₗ⁅R,L⁆ N }.invFun),
    { toLieModuleHom := toLieModuleHom, invFun := invFun, left_inv := left_inv, right_inv := right_inv : M ≃ₗ⁅R,L⁆ N } =
      { toLieModuleHom := toLieModuleHom_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 }
⊢ { toLieModuleHom := toLieModuleHom, invFun := invFun, left_inv := left_inv, right_inv := right_inv : M ≃ₗ⁅R,L⁆ N } = g

Tactic:
cases g
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L : Type v
M : Type w
N : Type w₁
P : Type w₂
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : AddCommGroup N
inst_4 : AddCommGroup P
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : LieRingModule L M
inst_9 : LieRingModule L N
inst_10 : LieRingModule L P
toLieModuleHom : M →ₗ⁅R,L⁆ N
invFun : N → M
left_inv : LeftInverse invFun (↑toLieModuleHom : M →ₗ[R] N).toFun
right_inv : RightInverse invFun (↑toLieModuleHom : M →ₗ[R] N).toFun
toLieModuleHom_1 : M →ₗ⁅R,L⁆ N
invFun_1 : N → M
left_inv_1 : LeftInverse invFun_1 (↑toLieModuleHom_1 : M →ₗ[R] N).toFun
right_inv_1 : RightInverse invFun_1 (↑toLieModuleHom_1 : M →ₗ[R] N).toFun
h₁ :
  (↑{ toLieModuleHom := toLieModuleHom, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
              M ≃ₗ⁅R,L⁆ N }.toLieModuleHom :
        M →ₗ[R] N).toFun =
    (↑{ toLieModuleHom := toLieModuleHom_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 :
              M ≃ₗ⁅R,L⁆ N }.toLieModuleHom :
        M →ₗ[R] N).toFun
h₂ :
  { toLieModuleHom := toLieModuleHom, invFun := invFun, left_inv := left_inv, right_inv := right_inv :
        M ≃ₗ⁅R,L⁆ N }.invFun =
    { toLieModuleHom := toLieModuleHom_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 :
        M ≃ₗ⁅R,L⁆ N }.invFun
⊢ toLieModuleHom = toLieModuleHom_1

Tactic:
simp at h₁ h₂