awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₃
g : L₁ ≃ₗ⁅R⁆ L₂
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
mk :
  ∀ (toLieHom_1 : L₁ →ₗ⁅R⁆ L₂) (invFun_1 : L₂ → L₁)
    (left_inv_1 : LeftInverse invFun_1 (↑toLieHom_1 : L₁ →ₗ[R] L₂).toFun)
    (right_inv_1 : RightInverse invFun_1 (↑toLieHom_1 : 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 =
        (↑{ toLieHom := toLieHom_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 :
                  L₁ ≃ₗ⁅R⁆ L₂ }.toLieHom :
            L₁ →ₗ[R] L₂).toFun)
    (h₂ :
      { toLieHom := toLieHom, invFun := invFun, left_inv := left_inv, right_inv := right_inv : L₁ ≃ₗ⁅R⁆ L₂ }.invFun =
        { toLieHom := toLieHom_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 :
            L₁ ≃ₗ⁅R⁆ L₂ }.invFun),
    { toLieHom := toLieHom, invFun := invFun, left_inv := left_inv, right_inv := right_inv : L₁ ≃ₗ⁅R⁆ L₂ } =
      { toLieHom := toLieHom_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 }
⊢ { toLieHom := toLieHom, invFun := invFun, left_inv := left_inv, right_inv := right_inv : L₁ ≃ₗ⁅R⁆ L₂ } = g

Tactic:
cases g
-- 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₃
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
toLieHom_1 : L₁ →ₗ⁅R⁆ L₂
invFun_1 : L₂ → L₁
left_inv_1 : LeftInverse invFun_1 (↑toLieHom_1 : L₁ →ₗ[R] L₂).toFun
right_inv_1 : RightInverse invFun_1 (↑toLieHom_1 : 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 =
    (↑{ toLieHom := toLieHom_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 :
              L₁ ≃ₗ⁅R⁆ L₂ }.toLieHom :
        L₁ →ₗ[R] L₂).toFun
h₂ :
  { toLieHom := toLieHom, invFun := invFun, left_inv := left_inv, right_inv := right_inv : L₁ ≃ₗ⁅R⁆ L₂ }.invFun =
    { toLieHom := toLieHom_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 :
        L₁ ≃ₗ⁅R⁆ L₂ }.invFun
⊢ toLieHom = toLieHom_1

Tactic:
simp at h₁ 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 : LieRing L₂
inst_3 : LieRing L₃
inst_4 : LieAlgebra R L₁
inst_5 : LieAlgebra R L₂
inst_6 : LieAlgebra R L₃
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
toLieHom_1 : L₁ →ₗ⁅R⁆ L₂
invFun_1 : L₂ → L₁
left_inv_1 : LeftInverse invFun_1 (↑toLieHom_1 : L₁ →ₗ[R] L₂).toFun
right_inv_1 : RightInverse invFun_1 (↑toLieHom_1 : L₁ →ₗ[R] L₂).toFun
h₂ : invFun = invFun_1
h₁ : toLieHom = toLieHom_1
⊢ { toLieHom := toLieHom, invFun := invFun, left_inv := left_inv, right_inv := right_inv : L₁ ≃ₗ⁅R⁆ L₂ } =
    { toLieHom := toLieHom_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 }

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 : LieRing L₂
inst_3 : LieAlgebra R L₁
inst_4 : LieAlgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
⊢ Eq (α := (a : L₁) → L₂) (⇑e.toLieHom : (a : L₁) → L₂) (⇑e : (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 : LieRing L₂
inst_3 : LieAlgebra R L₁
inst_4 : LieAlgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
⊢ Eq (α := (a : L₁) → L₂) (⇑e.toLinearEquiv : (a : L₁) → L₂) (⇑e : (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 : LieRing L₂
inst_3 : LieAlgebra R L₁
inst_4 : LieAlgebra R L₂
f : L₁ →ₗ⁅R⁆ L₂
g : L₂ → L₁
h₁ : LeftInverse g (↑f : L₁ →ₗ[R] L₂).toFun
h₂ : RightInverse g (↑f : L₁ →ₗ[R] L₂).toFun
⊢ { toLieHom := f, invFun := g, left_inv := h₁, right_inv := h₂ : L₁ ≃ₗ⁅R⁆ L₂ }.toLinearEquiv =
    { toLinearMap := (↑f : L₁ →ₗ[R] L₂), invFun := g, left_inv := h₁, right_inv := h₂ }

Tactic:
rfl

Premises used: LieEquiv.toLinearEquiv, 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 : LieRing L₂
inst_3 : LieAlgebra R L₁
inst_4 : LieAlgebra R L₂
f_inv : L₂ → 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⁆
left_inv :
  LeftInverse f_inv
    (↑{ toFun := f, map_add' := map_add', map_smul' := map_smul', map_lie' := @map_lie' : L₁ →ₗ⁅R⁆ L₂ } :
        L₁ →ₗ[R] L₂).toFun
right_inv :
  RightInverse f_inv
    (↑{ toFun := f, map_add' := map_add', map_smul' := map_smul', map_lie' := @map_lie' : L₁ →ₗ⁅R⁆ L₂ } :
        L₁ →ₗ[R] L₂).toFun
g_inv : L₂ → L₁
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⁆
left_inv_1 :
  LeftInverse g_inv
    (↑{ toFun := g, map_add' := map_add'_1, map_smul' := map_smul'_1, map_lie' := @map_lie'_1 : L₁ →ₗ⁅R⁆ L₂ } :
        L₁ →ₗ[R] L₂).toFun
right_inv_1 :
  RightInverse g_inv
    (↑{ toFun := g, map_add' := map_add'_1, map_smul' := map_smul'_1, map_lie' := @map_lie'_1 : L₁ →ₗ⁅R⁆ L₂ } :
        L₁ →ₗ[R] L₂).toFun
⊢ { toFun := f, map_add' := map_add', map_smul' := map_smul', map_lie' := @map_lie', invFun := f_inv,
          left_inv := left_inv, right_inv := right_inv : L₁ ≃ₗ⁅R⁆ L₂ }.toLinearEquiv =
      { toFun := g, map_add' := map_add'_1, map_smul' := map_smul'_1, map_lie' := @map_lie'_1, invFun := g_inv,
          left_inv := left_inv_1, right_inv := right_inv_1 }.toLinearEquiv →
    { toFun := f, map_add' := map_add', map_smul' := map_smul', map_lie' := @map_lie', invFun := f_inv,
        left_inv := left_inv, right_inv := right_inv : L₁ ≃ₗ⁅R⁆ L₂ } =
      { toFun := g, map_add' := map_add'_1, map_smul' := map_smul'_1, map_lie' := @map_lie'_1, invFun := g_inv,
        left_inv := left_inv_1, right_inv := right_inv_1 }

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 : LieRing L₂
inst_3 : LieAlgebra R L₁
inst_4 : LieAlgebra R L₂
⊢ Injective (α := L₁ ≃ₗ⁅R⁆ L₂) (β := L₁ → L₂) (DFunLike.coe (β := fun (x : L₁) ↦ L₂))

Tactic:
LinearEquiv.coe_injective.comp toLinearEquiv_injective

Premises used: Function.Injective.comp, LieEquiv.toLinearEquiv_injective, LinearEquiv.coe_injective
-- 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₃
x : L₁ ≃ₗ⁅R⁆ L₂
x_1 x_2 : L₁
rw :
  (x.toLinearEquiv : (a : L₁) → L₂) (x_1 + x_2) =
    HAdd.hAdd (α := L₂) (β := L₂) ((x.toLinearEquiv : (a : L₁) → L₂) x_1 : L₂)
      ((x.toLinearEquiv : (a : L₁) → L₂) x_2 : L₂)
rw₁ rw₂ :
  HAdd.hAdd (α := L₂) (β := L₂) ((x.toLinearEquiv : (a : L₁) → L₂) x_1 : L₂)
      ((x.toLinearEquiv : (a : L₁) → L₂) x_2 : L₂) =
    HAdd.hAdd (α := L₂) (β := L₂) ((x.toLinearEquiv : (a : L₁) → L₂) x_1 : L₂)
      ((x.toLinearEquiv : (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_toLinearEquiv, map_add]

Premises used: map_add, LieEquiv.coe_toLinearEquiv
-- 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₃
x : L₁ ≃ₗ⁅R⁆ L₂
x_1 : R
x_2 : L₁
rw :
  (x.toLinearEquiv : (a : L₁) → L₂) (x_1 • x_2) =
    HSMul.hSMul (α := R) (β := L₂) ((RingHom.id R : (a : R) → R) x_1 : R) ((x.toLinearEquiv : (a : L₁) → L₂) x_2 : L₂)
rw₁ :
  HSMul.hSMul (β := L₂) x_1 ((x.toLinearEquiv : (a : L₁) → L₂) x_2 : L₂) =
    HSMul.hSMul (α := R) (β := L₂) ((RingHom.id R : (a : R) → R) x_1 : R) ((x.toLinearEquiv : (a : L₁) → L₂) x_2 : L₂)
rw₂ rw₃ :
  HSMul.hSMul (β := L₂) x_1 ((x.toLinearEquiv : (a : L₁) → L₂) x_2 : L₂) =
    HSMul.hSMul (β := L₂) x_1 ((x.toLinearEquiv : (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_toLinearEquiv, map_smul, RingHom.id_apply]

Premises used: RingHom.id_apply, map_smul, LieEquiv.coe_toLinearEquiv
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L₁ : Type v
L₂ : Type w
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieRing L₂
inst_3 : LieAlgebra R 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: LieEquiv.coe_injective, funext
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L₁ : Type v
L₂ : Type w
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieRing L₂
inst_3 : LieAlgebra R L₁
inst_4 : LieAlgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
x y : L₁
⊢ Eq.{w + 1} (α := L₂) ((e : (a : L₁) → L₂) ⁅x, y⁆ : L₂)
    (Bracket.bracket (L := L₂) ((e : (a : L₁) → L₂) x : L₂) ((e : (a : L₁) → L₂) y) : L₂)

Tactic:
LieHom.map_lie e.toLieHom x y

Premises used: LieEquiv.toLieHom, 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₁
x : L₁
⊢ (refl : (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 : LieRing L₂
inst_3 : LieAlgebra R L₁
inst_4 : LieAlgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
⊢ e.symm.symm = e

Tactic:
rfl

Premises used: LieHom.inverse, LinearMap.inverse, LieEquiv.symm, 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 : LieRing L₂
inst_3 : LieAlgebra R L₁
inst_4 : LieAlgebra R L₂
⊢ Bijective (α := L₁ ≃ₗ⁅R⁆ L₂) symm

Tactic:
Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Premises used: Iff.mpr, Function.bijective_iff_has_inverse, And.intro, Exists.intro, LieEquiv.symm_symm
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L₁ : Type v
L₂ : Type w
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieRing L₂
inst_3 : LieAlgebra R L₁
inst_4 : LieAlgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
⊢ ∀ (x : L₂), (e : (a : L₁) → L₂) ((e.symm : (a : L₂) → L₁) x : L₁) = x

Tactic:
e.toLinearEquiv.apply_symm_apply

Premises used: LinearEquiv.apply_symm_apply, LieEquiv.toLinearEquiv
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L₁ : Type v
L₂ : Type w
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieRing L₂
inst_3 : LieAlgebra R L₁
inst_4 : LieAlgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
⊢ ∀ (x : L₁), (e.symm : (a : L₂) → L₁) ((e : (a : L₁) → L₂) x : L₂) = x

Tactic:
e.toLinearEquiv.symm_apply_apply

Premises used: LinearEquiv.symm_apply_apply, LieEquiv.toLinearEquiv
-- 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} (α := L₁ ≃ₗ⁅R⁆ L₁) (symm refl) refl

Tactic:
rfl

Premises used: LieHom.inverse, LinearMap.inverse, LieEquiv.symm, rfl, LieEquiv.refl
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L₁ : Type v
L₂ : Type w
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieRing L₂
inst_3 : LieAlgebra R L₁
inst_4 : LieAlgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
⊢ e.trans e.symm = refl

Tactic:
ext e.symm_apply_apply

Premises used: LieEquiv.symm_apply_apply, LieEquiv.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 : LieRing L₂
inst_3 : LieAlgebra R L₁
inst_4 : LieAlgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
⊢ e.symm.trans e = refl

Tactic:
e.symm.self_trans_symm

Premises used: LieHom.inverse, LinearMap.inverse, LieEquiv.self_trans_symm, LieEquiv.symm
-- 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₃
e₁ : L₁ ≃ₗ⁅R⁆ L₂
e₂ : L₂ ≃ₗ⁅R⁆ L₃
x : L₁
⊢ Eq.{w₁ + 1} (α := L₃) ((e₁.trans e₂ : (a : L₁) → L₃) x : L₃) ((e₂ : (a : L₂) → L₃) ((e₁ : (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 : LieRing L₂
inst_3 : LieRing L₃
inst_4 : LieAlgebra R L₁
inst_5 : LieAlgebra R L₂
inst_6 : LieAlgebra R L₃
e₁ : L₁ ≃ₗ⁅R⁆ L₂
e₂ : L₂ ≃ₗ⁅R⁆ L₃
⊢ (e₁.trans e₂).symm = e₂.symm.trans e₁.symm

Tactic:
rfl

Premises used: LieHom.inverse, LinearMap.inverse, LieEquiv.trans, LieEquiv.symm, 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 : LieRing L₂
inst_3 : LieAlgebra R L₁
inst_4 : LieAlgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
⊢ Bijective.{v + 1, w + 1} (α := L₁) (β := L₂) (⇑e.toLieHom : (a : L₁) → L₂)

Tactic:
e.toLinearEquiv.bijective

Premises used: LinearEquiv.bijective, LieEquiv.toLinearEquiv
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L₁ : Type v
L₂ : Type w
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieRing L₂
inst_3 : LieAlgebra R L₁
inst_4 : LieAlgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
⊢ Injective.{v + 1, w + 1} (α := L₁) (β := L₂) (⇑e.toLieHom : (a : L₁) → L₂)

Tactic:
e.toLinearEquiv.injective

Premises used: LinearEquiv.injective, LieEquiv.toLinearEquiv
-- Module: Mathlib.Algebra.Lie.Basic
Goal:
R : Type u
L₁ : Type v
L₂ : Type w
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieRing L₂
inst_3 : LieAlgebra R L₁
inst_4 : LieAlgebra R L₂
e : L₁ ≃ₗ⁅R⁆ L₂
⊢ Surjective.{v + 1, w + 1} (α := L₁) (β := L₂) (⇑e.toLieHom : (a : L₁) → L₂)

Tactic:
e.toLinearEquiv.surjective

Premises used: LinearEquiv.surjective, LieEquiv.toLinearEquiv
-- 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 : L₁ →ₗ⁅R⁆ L₂
h : Bijective.{v + 1, w + 1} (α := L₁) (β := L₂) (⇑f : (a : L₁) → 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:
f.map_lie x y

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 : LieRing L₂
inst_3 : LieRing L₃
inst_4 : LieAlgebra R L₁
inst_5 : LieAlgebra R L₂
inst_6 : LieAlgebra R L₃
f : L₁ →ₗ⁅R⁆ L₂
h : Bijective.{v + 1, w + 1} (α := L₁) (β := L₂) (⇑f : (a : L₁) → 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:
exact f.map_lie x y

Premises used: LieHom.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
x y : M →ₗ⁅R,L⁆ N
h :
  Eq (α := (a : M) → N) ((fun (f : M →ₗ⁅R,L⁆ N) ↦ (↑f : M →ₗ[R] N).toFun) x)
    ((fun (f : M →ₗ⁅R,L⁆ N) ↦ (↑f : M →ₗ[R] N).toFun) y)
mk :
  ∀ (toLinearMap : M →ₗ[R] N) (map_lie' : ∀ {x : L} {m : M}, toLinearMap.toFun ⁅x, m⁆ = ⁅x, toLinearMap.toFun m⁆)
    (h :
      Eq (α := (a : M) → N)
        ((fun (f : M →ₗ⁅R,L⁆ N) ↦ (↑f : M →ₗ[R] N).toFun) { toLinearMap := toLinearMap, map_lie' := @map_lie' })
        ((fun (f : M →ₗ⁅R,L⁆ N) ↦ (↑f : M →ₗ[R] N).toFun) y)),
    { toLinearMap := toLinearMap, map_lie' := @map_lie' : M →ₗ⁅R,L⁆ N } = y
⊢ x = y

Tactic:
cases x
-- 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
y : M →ₗ⁅R,L⁆ N
toLinearMap : M →ₗ[R] N
map_lie' : ∀ {x : L} {m : M}, toLinearMap.toFun ⁅x, m⁆ = ⁅x, toLinearMap.toFun m⁆
h :
  Eq (α := (a : M) → N)
    ((fun (f : M →ₗ⁅R,L⁆ N) ↦ (↑f : M →ₗ[R] N).toFun) { toLinearMap := toLinearMap, map_lie' := @map_lie' })
    ((fun (f : M →ₗ⁅R,L⁆ N) ↦ (↑f : M →ₗ[R] N).toFun) y)
mk :
  ∀ (toLinearMap_1 : M →ₗ[R] N)
    (map_lie'_1 : ∀ {x : L} {m : M}, toLinearMap_1.toFun ⁅x, m⁆ = ⁅x, toLinearMap_1.toFun m⁆)
    (h :
      Eq (α := (a : M) → N)
        ((fun (f : M →ₗ⁅R,L⁆ N) ↦ (↑f : M →ₗ[R] N).toFun) { toLinearMap := toLinearMap, map_lie' := @map_lie' })
        ((fun (f : M →ₗ⁅R,L⁆ N) ↦ (↑f : M →ₗ[R] N).toFun) { toLinearMap := toLinearMap_1, map_lie' := @map_lie'_1 })),
    { toLinearMap := toLinearMap, map_lie' := @map_lie' : M →ₗ⁅R,L⁆ N } =
      { toLinearMap := toLinearMap_1, map_lie' := @map_lie'_1 }
⊢ { toLinearMap := toLinearMap, map_lie' := @map_lie' : M →ₗ⁅R,L⁆ N } = y

Tactic:
cases y
-- 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
toLinearMap : M →ₗ[R] N
map_lie' : ∀ {x : L} {m : M}, toLinearMap.toFun ⁅x, m⁆ = ⁅x, toLinearMap.toFun m⁆
toLinearMap_1 : M →ₗ[R] N
map_lie'_1 : ∀ {x : L} {m : M}, toLinearMap_1.toFun ⁅x, m⁆ = ⁅x, toLinearMap_1.toFun m⁆
h :
  Eq (α := (a : M) → N)
    ((fun (f : M →ₗ⁅R,L⁆ N) ↦ (↑f : M →ₗ[R] N).toFun) { toLinearMap := toLinearMap, map_lie' := @map_lie' })
    ((fun (f : M →ₗ⁅R,L⁆ N) ↦ (↑f : M →ₗ[R] N).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
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
toLinearMap : M →ₗ[R] N
map_lie' : ∀ {x : L} {m : M}, toLinearMap.toFun ⁅x, m⁆ = ⁅x, toLinearMap.toFun m⁆
toLinearMap_1 : M →ₗ[R] N
map_lie'_1 : ∀ {x : L} {m : M}, toLinearMap_1.toFun ⁅x, m⁆ = ⁅x, toLinearMap_1.toFun m⁆
h : toLinearMap = toLinearMap_1
⊢ { toLinearMap := toLinearMap, map_lie' := @map_lie' : M →ₗ⁅R,L⁆ N } =
    { toLinearMap := toLinearMap_1, map_lie' := @map_lie'_1 }

Tactic:
simp [h]
-- 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 : M →ₗ[R] N) : (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₁
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 : M →ₗ⁅R,L⁆ N
x_1 x_2 : M
rw :
  ((↑x : M →ₗ[R] N) : (a : M) → N) (x_1 + x_2) =
    HAdd.hAdd (α := N) (β := N) (((↑x : M →ₗ[R] N) : (a : M) → N) x_1 : N) (((↑x : M →ₗ[R] N) : (a : M) → N) x_2 : N)
rw₁ rw₂ :
  HAdd.hAdd (α := N) (β := N) (((↑x : M →ₗ[R] N) : (a : M) → N) x_1 : N) (((↑x : M →ₗ[R] N) : (a : M) → N) x_2 : N) =
    HAdd.hAdd (α := N) (β := N) (((↑x : M →ₗ[R] N) : (a : M) → N) x_1 : N) (((↑x : M →ₗ[R] N) : (a : M) → N) x_2 : N)
⊢ (x : (a : M) → N) (x_1 + x_2) = HAdd.hAdd (α := N) (β := N) ((x : (a : M) → N) x_1 : N) ((x : (a : M) → N) x_2 : N)

Tactic:
rw [← coe_toLinearMap, map_add]

Premises used: LieModuleHom.coe_toLinearMap, map_add
-- 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 : M →ₗ⁅R,L⁆ N
x_1 : R
x_2 : M
rw :
  ((↑x : M →ₗ[R] N) : (a : M) → N) (x_1 • x_2) =
    HSMul.hSMul (α := R) (β := N) ((RingHom.id R : (a : R) → R) x_1 : R) (((↑x : M →ₗ[R] N) : (a : M) → N) x_2 : N)
rw₁ rw₂ :
  HSMul.hSMul (α := R) (β := N) ((RingHom.id R : (a : R) → R) x_1 : R) (((↑x : M →ₗ[R] N) : (a : M) → N) x_2 : N) =
    HSMul.hSMul (α := R) (β := N) ((RingHom.id R : (a : R) → R) x_1 : R) (((↑x : M →ₗ[R] N) : (a : M) → N) x_2 : N)
⊢ (x : (a : M) → N) (x_1 • x_2) =
    HSMul.hSMul (α := R) (β := N) ((RingHom.id R : (a : R) → R) x_1 : R) ((x : (a : M) → N) x_2 : N)

Tactic:
rw [← coe_toLinearMap, map_smulₛₗ]

Premises used: LieModuleHom.coe_toLinearMap, MulActionSemiHomClass.map_smulₛₗ
-- 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
x : L
m : M
⊢ Eq.{w₁ + 1} (α := N) ((f : (a : M) → N) ⁅x, m⁆ : N) (⁅x, (f : (a : M) → N) m⁆ : N)

Tactic:
LieModuleHom.map_lie' f

Premises used: LieModuleHom.map_lie'