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
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₂ : invFun = invFun_1
h₁ : toLieModuleHom = toLieModuleHom_1
⊢ { 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:
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
e : M ≃ₗ⁅R,L⁆ N
⊢ Eq (α := (a : M) → N) (⇑e.toLieModuleHom : (a : M) → N) (⇑e : (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
e : M ≃ₗ⁅R,L⁆ N
⊢ Injective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑e : (a : M) → N)

Tactic:
e.toEquiv.injective

Premises used: LieModuleEquiv.toEquiv, Equiv.injective
-- 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
e : M ≃ₗ⁅R,L⁆ N
⊢ Surjective.{w + 1, w₁ + 1} (α := M) (β := N) (⇑e : (a : M) → N)

Tactic:
e.toEquiv.surjective

Premises used: LieModuleEquiv.toEquiv, Equiv.surjective
-- 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
g : N → M
h₁ : LeftInverse g (↑f : M →ₗ[R] N).toFun
h₂ : RightInverse g (↑f : M →ₗ[R] N).toFun
⊢ { toLieModuleHom := f, invFun := g, left_inv := h₁, right_inv := h₂ : M ≃ₗ⁅R,L⁆ N }.toEquiv =
    { toFun := (⇑f : (a : M) → N), invFun := g, left_inv := h₁, right_inv := h₂ }

Tactic:
rfl

Premises used: LieModuleEquiv.toEquiv, 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
invFun : N → M
h₁ : LeftInverse invFun (↑f : M →ₗ[R] N).toFun
h₂ : RightInverse invFun (↑f : M →ₗ[R] N).toFun
⊢ Eq (α := (a : M) → N)
    (⇑{ toLieModuleHom := f, invFun := invFun, left_inv := h₁, right_inv := h₂ : M ≃ₗ⁅R,L⁆ 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₁
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
e : M ≃ₗ⁅R,L⁆ N
⊢ Eq (α := (a : M) → N) (⇑e.toLinearEquiv : (a : M) → N) (⇑e : (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_inv : N → M
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⁆
left_inv :
  LeftInverse f_inv
    (↑{ toFun := f, map_add' := map_add', map_smul' := map_smul', map_lie' := @map_lie' : M →ₗ⁅R,L⁆ N } :
        M →ₗ[R] N).toFun
right_inv :
  RightInverse f_inv
    (↑{ toFun := f, map_add' := map_add', map_smul' := map_smul', map_lie' := @map_lie' : M →ₗ⁅R,L⁆ N } :
        M →ₗ[R] N).toFun
g_inv : N → 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⁆
left_inv_1 :
  LeftInverse g_inv
    (↑{ toFun := g, map_add' := map_add'_1, map_smul' := map_smul'_1, map_lie' := @map_lie'_1 : M →ₗ⁅R,L⁆ N } :
        M →ₗ[R] N).toFun
right_inv_1 :
  RightInverse g_inv
    (↑{ toFun := g, map_add' := map_add'_1, map_smul' := map_smul'_1, map_lie' := @map_lie'_1 : M →ₗ⁅R,L⁆ N } :
        M →ₗ[R] N).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 : M ≃ₗ⁅R,L⁆ N }.toEquiv =
      { 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 : M ≃ₗ⁅R,L⁆ N }.toEquiv →
    { 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 : M ≃ₗ⁅R,L⁆ N } =
      { 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
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
e₁ e₂ : M ≃ₗ⁅R,L⁆ N
h : ∀ (m : M), Eq.{w₁ + 1} (α := N) ((e₁ : (a : M) → N) m : N) ((e₂ : (a : M) → N) m : N)
⊢ e₁ = e₂

Tactic:
toEquiv_injective (Equiv.ext h)

Premises used: Equiv.ext, LieModuleEquiv.toEquiv_injective
-- 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.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)
rw₁ 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)
⊢ (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_toLinearEquiv, map_add]

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

Premises used: RingHom.id_apply, LieModuleEquiv.coe_toLinearEquiv, map_smul
-- 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
m : M
⊢ (1 : (a : M) → M) m = m

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
m : M
⊢ (refl : (a : M) → M) m = m

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
e : M ≃ₗ⁅R,L⁆ N
⊢ ∀ (x : N), (e : (a : M) → N) ((e.symm : (a : N) → M) x : M) = x

Tactic:
e.toLinearEquiv.apply_symm_apply

Premises used: LinearEquiv.apply_symm_apply, LieModuleEquiv.toLinearEquiv
-- 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
e : M ≃ₗ⁅R,L⁆ N
⊢ ∀ (x : M), (e.symm : (a : N) → M) ((e : (a : M) → N) x : N) = x

Tactic:
e.toLinearEquiv.symm_apply_apply

Premises used: LinearEquiv.symm_apply_apply, LieModuleEquiv.toLinearEquiv
-- 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
n : N
e : M ≃ₗ⁅R,L⁆ N
⊢ (e : (a : M) → N) m = n ↔ m = (e.symm : (a : N) → M) n

Tactic:
(e : M ≃ N).apply_eq_iff_eq_symm_apply

Premises used: EquivLike.toEquiv, Equiv.apply_eq_iff_eq_symm_apply
-- 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
e : M ≃ₗ⁅R,L⁆ N
⊢ e.symm.symm = e

Tactic:
rfl

Premises used: LieModuleHom.inverse, LieModuleEquiv.symm, LinearMap.inverse, 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
⊢ Bijective (α := M ≃ₗ⁅R,L⁆ N) symm

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

Premises used: Iff.mpr, LieModuleEquiv.symm_symm, Function.bijective_iff_has_inverse, And.intro, Exists.intro
-- 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
e₁ : M ≃ₗ⁅R,L⁆ N
e₂ : N ≃ₗ⁅R,L⁆ P
m : M
⊢ Eq.{w₂ + 1} (α := P) ((e₁.trans e₂ : (a : M) → P) m : P) ((e₂ : (a : N) → P) ((e₁ : (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
e₁ : M ≃ₗ⁅R,L⁆ N
e₂ : N ≃ₗ⁅R,L⁆ P
⊢ (e₁.trans e₂).symm = e₂.symm.trans e₁.symm

Tactic:
rfl

Premises used: LieModuleHom.inverse, LieModuleEquiv.symm, LieModuleEquiv.trans, LinearMap.inverse, LieModuleHom.comp, 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
e : M ≃ₗ⁅R,L⁆ N
⊢ e.trans e.symm = refl

Tactic:
ext _ _ e.symm_apply_apply

Premises used: LieModuleEquiv.ext, LieModuleEquiv.symm_apply_apply
-- 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
e : M ≃ₗ⁅R,L⁆ N
⊢ e.symm.trans e = refl

Tactic:
ext _ _ e.apply_symm_apply

Premises used: LieModuleEquiv.ext, LieModuleEquiv.apply_symm_apply
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : IsAddTorsionFree L
i : ι
⊢ NoZeroSMulDivisors ℤ L

Tactic:
have : NoZeroSMulDivisors ℤ L := IsAddTorsionFree.to_noZeroSMulDivisors_int
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : IsAddTorsionFree L
i : ι
this : NoZeroSMulDivisors ℤ L
rw : b.A i i • b.e i - b.A i i • b.e i = 0
⊢ (b.A i i - 2) • b.e i = 0

Tactic:
rw [sub_smul, ofNat_smul_eq_nsmul, ← (b.sl2 i).lie_h_e_nsmul, b.lie_h_e i i]

Premises used: ofNat_smul_eq_nsmul, sub_smul, LieAlgebra.Basis.lie_h_e, IsSl2Triple.lie_h_e_nsmul, LieAlgebra.Basis.sl2
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : IsAddTorsionFree L
i : ι
this : NoZeroSMulDivisors ℤ L
⊢ b.A i i • b.e i - b.A i i • b.e i = 0

Tactic:
abel
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : IsAddTorsionFree L
i : ι
this : NoZeroSMulDivisors ℤ L
⊢ (b.A i i - 2) • b.e i = 0

Tactic:
have aux : (b.A i i - 2) • b.e i = 0 := by
    rw [sub_smul, ofNat_smul_eq_nsmul, ← (b.sl2 i).lie_h_e_nsmul, b.lie_h_e i i]; abel
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
inst_4 : IsAddTorsionFree L
i : ι
this : NoZeroSMulDivisors ℤ L
aux : (b.A i i - 2) • b.e i = 0
rwa : ∀ (aux : b.A i i - 2 = 0), b.A i i = 2
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (aux : b.A i i = 2), b.A i i = 2
⊢ b.A i i = 2

Tactic:
rwa [IsAddTorsionFree.zsmul_eq_zero_iff_left (b.sl2 i).e_ne_zero, sub_eq_zero] at aux

Premises used: sub_eq_zero, IsSl2Triple.e_ne_zero, IsAddTorsionFree.zsmul_eq_zero_iff_left, LieAlgebra.Basis.sl2
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
rw : Eq (α := Submodule R L) (toSubmodule (lieSpan R L (range b.h))) (Submodule.span R (range b.h))
⊢ b.cartan.toSubmodule = Submodule.span R (range b.h)

Tactic:
rw [b.cartan_eq_lieSpan]

Premises used: LieAlgebra.Basis.cartan_eq_lieSpan
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
hs : ∀ x ∈ range b.h, ∀ y ∈ range b.h, ⁅x, y⁆ = 0
⊢ Eq (α := Submodule R L) (toSubmodule (lieSpan R L (range b.h))) (Submodule.span R (range b.h))

Tactic:
apply coe_lieSpan_eq_span_of_forall_lie_eq_zero

Premises used: LieSubalgebra.coe_lieSpan_eq_span_of_forall_lie_eq_zero
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
i j : ι
⊢ ⁅b.h i, b.h j⁆ = 0

Tactic:
b.lie_h_h i j

Premises used: LieAlgebra.Basis.lie_h_h
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
i j : ι
⊢ ⁅b.h i, b.h j⁆ = 0

Tactic:
exact b.lie_h_h i j

Premises used: LieAlgebra.Basis.lie_h_h
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
rw : ∀ x ∈ range b.h, ∀ y ∈ range b.h, ⁅x, y⁆ = 0
⊢ IsLieAbelian.{u_3} ↥b.cartan

Tactic:
rw [cartan_eq_lieSpan, isLieAbelian_lieSpan_iff]

Premises used: LieSubalgebra.isLieAbelian_lieSpan_iff, LieAlgebra.Basis.cartan_eq_lieSpan
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
rw : b.cartan = lieSpan R L (range b.h)
⊢ b.cartan = lieSpan R L (range (-b.h))

Tactic:
rw [← neg_range', lieSpan_neg]

Premises used: LieSubalgebra.lieSpan_neg, Set.neg_range'
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
⊢ b.cartan = lieSpan R L (range b.h)

Tactic:
b.cartan_eq_lieSpan

Premises used: LieAlgebra.Basis.cartan_eq_lieSpan
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
⊢ b.cartan = lieSpan R L (range b.h)

Tactic:
exact b.cartan_eq_lieSpan

Premises used: LieAlgebra.Basis.cartan_eq_lieSpan
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
rw : Eq (α := LieSubalgebra R L) (lieSpan R L (range b.e ∪ range b.f)) ⊤
rw₁ rw₂ : Eq.{u_3 + 1} (α := LieSubalgebra R L) ⊤ ⊤
⊢ Eq (α := LieSubalgebra R L) (lieSpan R L (range b.f ∪ range b.e)) ⊤

Tactic:
rw [union_comm, b.span_ef]

Premises used: Set.union_comm, LieAlgebra.Basis.span_ef
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
i j : ι
rw : ⁅-b.h i, (-b.h) j⁆ = 0
rw₁ : ⁅-b.h i, -b.h j⁆ = 0
rw₂ : -⁅b.h i, -b.h j⁆ = 0
rw₃ : - -⁅b.h i, b.h j⁆ = 0
rw₄ : Eq.{u_3 + 1} (α := L) (- -0) 0
rw₅ rw₆ : Eq.{u_3 + 1} (α := L) 0 0
⊢ ⁅(-b.h) i, (-b.h) j⁆ = 0

Tactic:
rw [Pi.neg_apply, Pi.neg_apply, neg_lie, lie_neg, b.lie_h_h i j, neg_neg]

Premises used: lie_neg, neg_neg, neg_lie, LieAlgebra.Basis.lie_h_h, Pi.neg_apply
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
i j : ι
rw : ⁅-b.h j, b.f i⁆ = b.A i j • b.f i
rw₁ : -⁅b.h j, b.f i⁆ = b.A i j • b.f i
rw₂ : -(-b.A i j • b.f i) = b.A i j • b.f i
rw₃ : - -(b.A i j • b.f i) = b.A i j • b.f i
rw₄ rw₅ : b.A i j • b.f i = b.A i j • b.f i
⊢ ⁅(-b.h) j, b.f i⁆ = b.A i j • b.f i

Tactic:
rw [Pi.neg_apply, neg_lie, b.lie_h_f i j, neg_smul, neg_neg]

Premises used: neg_smul, LieAlgebra.Basis.lie_h_f, neg_neg, neg_lie, Pi.neg_apply
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
i j : ι
rw : ⁅-b.h j, b.e i⁆ = -b.A i j • b.e i
rw₁ : -⁅b.h j, b.e i⁆ = -b.A i j • b.e i
rw₂ : -(b.A i j • b.e i) = -b.A i j • b.e i
rw₃ rw₄ : -(b.A i j • b.e i) = -(b.A i j • b.e i)
⊢ ⁅(-b.h) j, b.e i⁆ = -b.A i j • b.e i

Tactic:
rw [Pi.neg_apply, neg_lie, b.lie_h_e, neg_smul]

Premises used: neg_smul, neg_lie, LieAlgebra.Basis.lie_h_e, Pi.neg_apply
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
i j : ι
h : i ≠ j
rw : -⁅b.e j, b.f i⁆ = 0
rw₁ : ⁅b.e j, b.f i⁆ = 0
rw₂ rw₃ : Eq.{u_3 + 1} (α := L) 0 0
⊢ ⁅b.f i, b.e j⁆ = 0

Tactic:
rw [← lie_skew, neg_eq_zero, b.lie_e_f_ne j i h.symm]

Premises used: neg_eq_zero, Ne.symm, lie_skew, LieAlgebra.Basis.lie_e_f_ne
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
⊢ b.symm.symm = b

Tactic:
aesop
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
i : ι
⊢ b.symm.h' i = -b.h' i

Tactic:
rfl

Premises used: Set.Mem, LieAlgebra.Basis.h', rfl
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x y : L
hx : x ∈ b.cartan
u : L
hu : u ∈ range b.e
mem : ∀ (i : ι), Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, b.e i⁆
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, u⁆

Tactic:
obtain ⟨i, rfl⟩ := hu

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x y : L
hx : x ∈ b.cartan
i : ι
mem :
  ∀ (hx : Membership.mem (γ := Submodule R L) (Submodule.span R (range b.h)) x) (i : ι),
    Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, b.e i⁆
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅x, b.e i⁆

Tactic:
rw [← mem_toSubmodule, coe_cartan_eq_span] at hx

Premises used: LieSubalgebra.mem_toSubmodule, LieAlgebra.Basis.coe_cartan_eq_span
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x y : L
i : ι
v : L
hv : v ∈ range b.h
mem : ∀ (j : ι), Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅b.h j, b.e i⁆
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅v, b.e i⁆

Tactic:
obtain ⟨j, rfl⟩ := hv

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x y : L
i j : ι
mem : Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) (b.A i j • b.e i)
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) ⁅b.h j, b.e i⁆

Tactic:
rw [b.lie_h_e]

Premises used: LieAlgebra.Basis.lie_h_e
-- Module: Mathlib.Algebra.Lie.Basis
Goal:
ι : Type u_1
R : Type u_2
L : Type u_3
inst : Finite ι
inst_1 : CommRing R
inst_2 : LieRing L
inst_3 : LieAlgebra R L
b : Basis ι R L
x y : L
i j : ι
⊢ Membership.mem (γ := LieSubalgebra R L) (lieSpan R L (range b.e)) (b.A i j • b.e i)

Tactic:
apply zsmul_mem <| subset_lieSpan <| mem_range_self i

Premises used: Set.mem_range_self, zsmul_mem, LieSubalgebra.subset_lieSpan