awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₃
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
⊢ { toLieHom := toLieHom, invFun := invFun, left_inv := left_inv, right_inv := right_inv : L₁ ≃ₗ⁅R⁆ L₂ } = g
have 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 }
Tactic: cases g
Cleared hypotheses: g, h₁, 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 : 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, 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 }
have h₃ : toLieHom = toLieHom_1
Tactic: simp at h₁ 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 : 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₁
⊢ (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.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₂)
Tactic: rw [← coe_toLinearEquiv, 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 : 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₂)
⊢ (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.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₂)
Tactic: rw [← coe_toLinearEquiv, 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 : 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₁
⊢ (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.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₂)
Tactic: rw [← coe_toLinearEquiv, map_smul, RingHom.id_apply]
-- 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₃
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₂)
⊢ (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 (β := 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₂)
Tactic: rw [← coe_toLinearEquiv, map_smul, RingHom.id_apply]
-- 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₃
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₂)
⊢ (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 (β := L₂) x_1 ((x.toLinearEquiv : (a : L₁) → L₂) x_2 : L₂) =
  HSMul.hSMul (β := L₂) x_1 ((x.toLinearEquiv : (a : L₁) → L₂) x_2 : L₂)
Tactic: rw [← coe_toLinearEquiv, map_smul, RingHom.id_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
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)
⊢ x = y
have 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
Tactic: cases x
Cleared hypotheses: x, h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
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)
⊢ { toLinearMap := toLinearMap, map_lie' := @map_lie' : M →ₗ⁅R,L⁆ N } = y
have 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 }
Tactic: cases y
Cleared hypotheses: y, h
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (hypothesis)
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, map_lie' := @map_lie' : M →ₗ⁅R,L⁆ N } =
    { 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
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
⊢ (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)
have 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)
Tactic: rw [← coe_toLinearMap, map_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
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)
⊢ (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)
have 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)
Tactic: rw [← coe_toLinearMap, map_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
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
⊢ (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)
have 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)
Tactic: rw [← coe_toLinearMap, map_smulₛₗ]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
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)
⊢ (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)
have 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)
Tactic: rw [← coe_toLinearMap, map_smulₛₗ]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
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 ⁅x, n⁆ = g ⁅x, (f : (a : M) → N) (g n)⁆
have rw : g ⁅x, n⁆ = g ⁅x, n⁆
Tactic: rw [h₂]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
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 ⁅x, (f : (a : M) → N) (g n)⁆ = g ((f : (a : M) → N) ⁅x, g n⁆)
have rw : g ⁅x, (f : (a : M) → N) (g n)⁆ = g ⁅x, (f : (a : M) → N) (g n)⁆
Tactic: rw [map_lie]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
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
⊢ ((↑f : M →ₗ[R] N).inverse g h₁ h₂).toFun ⁅x, n⁆ = ⁅x, ((↑f : M →ₗ[R] N).inverse g h₁ h₂).toFun n⁆
have g₁ : g ⁅x, n⁆ = g ⁅x, (f : (a : M) → N) (g 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₁ _
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
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)⁆
⊢ ((↑f : M →ₗ[R] N).inverse g h₁ h₂).toFun ⁅x, n⁆ = ⁅x, ((↑f : M →ₗ[R] N).inverse g h₁ h₂).toFun n⁆
have g₂ : g ⁅x, (f : (a : M) → N) (g n)⁆ = g ((f : (a : M) → N) ⁅x, g 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₁ _
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
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
⊢ f = g
have 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
Tactic: cases f
Cleared hypotheses: f, h₁, h₂
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
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
⊢ { toLieModuleHom := toLieModuleHom, invFun := invFun, left_inv := left_inv, right_inv := right_inv : M ≃ₗ⁅R,L⁆ N } = g
have 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 }
Tactic: cases g
Cleared hypotheses: g, h₁, h₂
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (hypothesis)
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, 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 }
have h₃ : toLieModuleHom = toLieModuleHom_1
Tactic: simp at h₁ h₂
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
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
⊢ (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)
have rw : (x.toLinearEquiv : (a : M) → N) (x_1 + x_2) =
  HAdd.hAdd (α := N) (β := N) ((x.toLinearEquiv : (a : M) → N) x_1 : N) ((x.toLinearEquiv : (a : M) → N) x_2 : N)
Tactic: rw [← coe_toLinearEquiv, map_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Basic (goal)
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.toLinearEquiv : (a : M) → N) (x_1 + x_2) =
    HAdd.hAdd (α := N) (β := N) ((x.toLinearEquiv : (a : M) → N) x_1 : N) ((x.toLinearEquiv : (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)
have rw₁ : HAdd.hAdd (α := N) (β := N) ((x.toLinearEquiv : (a : M) → N) x_1 : N) ((x.toLinearEquiv : (a : M) → N) x_2 : N) =
  HAdd.hAdd (α := N) (β := N) ((x.toLinearEquiv : (a : M) → N) x_1 : N) ((x.toLinearEquiv : (a : M) → N) x_2 : N)
Tactic: rw [← coe_toLinearEquiv, map_add]