awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
h :
  ∀ (m : L ⧸ H.toLieSubmodule),
    Membership.mem (γ := LieSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
        (LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)) m →
      m = 0
x : L
hx : x ∈ H.normalizer
y : L ⧸ H.toLieSubmodule := (LieSubmodule.Quotient.mk' H.toLieSubmodule : (a : L) → L ⧸ H.toLieSubmodule) x
⊢ Membership.mem (γ := LieSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
    (LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)) y

Tactic:
have hy : y ∈ LieModule.maxTrivSubmodule R H (L ⧸ H.toLieSubmodule) := by
      rintro ⟨z, hz⟩
      rw [← LieModuleHom.map_lie, LieSubmodule.Quotient.mk_eq_zero, coe_bracket_of_module,
        Submodule.coe_mk, mem_toLieSubmodule]
      exact (H.mem_normalizer_iff' x).mp hx z hz
-- Module: Mathlib.Algebra.Lie.Normalizer
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
h :
  ∀ (m : L ⧸ H.toLieSubmodule),
    Membership.mem (γ := LieSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
        (LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)) m →
      m = 0
x : L
hx : x ∈ H.normalizer
y : L ⧸ H.toLieSubmodule := (LieSubmodule.Quotient.mk' H.toLieSubmodule : (a : L) → L ⧸ H.toLieSubmodule) x
hy :
  Membership.mem (γ := LieSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
    (LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)) y
⊢ x ∈ H

Tactic:
simpa [y] using h y hy
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
A : Type v
inst : Ring A
x x_1 x_2 : A
simp : x * x_2 + x_1 * x_2 - (x_2 * x + x_2 * x_1) = x * x_2 - x_2 * x + (x_1 * x_2 - x_2 * x_1)
⊢ ⁅x + x_1, x_2⁆ = ⁅x, x_2⁆ + ⁅x_1, x_2⁆

Tactic:
simp only [Ring.lie_def, right_distrib, left_distrib]

Premises used: Ring.lie_def, right_distrib, left_distrib
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
A : Type v
inst : Ring A
x x_1 x_2 : A
⊢ x * x_2 + x_1 * x_2 - (x_2 * x + x_2 * x_1) = x * x_2 - x_2 * x + (x_1 * x_2 - x_2 * x_1)

Tactic:
abel
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
A : Type v
inst : Ring A
x x_1 x_2 : A
simp : x * x_1 + x * x_2 - (x_1 * x + x_2 * x) = x * x_1 - x_1 * x + (x * x_2 - x_2 * x)
⊢ ⁅x, x_1 + x_2⁆ = ⁅x, x_1⁆ + ⁅x, x_2⁆

Tactic:
simp only [Ring.lie_def, right_distrib, left_distrib]

Premises used: Ring.lie_def, right_distrib, left_distrib
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
A : Type v
inst : Ring A
x x_1 x_2 : A
⊢ x * x_1 + x * x_2 - (x_1 * x + x_2 * x) = x * x_1 - x_1 * x + (x * x_2 - x_2 * x)

Tactic:
abel
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
A : Type v
inst : Ring A
⊢ ∀ (x : A), ⁅x, x⁆ = 0

Tactic:
simp only [Ring.lie_def, forall_const, sub_self]

Premises used: sub_self, Ring.lie_def, forall_const
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
A : Type v
inst : Ring A
x x_1 x_2 : A
simp :
  x * (x_1 * x_2) - x * (x_2 * x_1) - (x_1 * (x_2 * x) - x_2 * (x_1 * x)) =
    x * (x_1 * x_2) - x_1 * (x * x_2) - (x_2 * (x * x_1) - x_2 * (x_1 * x)) +
      (x_1 * (x * x_2) - x_1 * (x_2 * x) - (x * (x_2 * x_1) - x_2 * (x * x_1)))
⊢ ⁅x, ⁅x_1, x_2⁆⁆ = ⁅⁅x, x_1⁆, x_2⁆ + ⁅x_1, ⁅x, x_2⁆⁆

Tactic:
simp only [Ring.lie_def, mul_sub_left_distrib, mul_sub_right_distrib, mul_assoc]

Premises used: mul_assoc, mul_sub_left_distrib, mul_sub_right_distrib, Ring.lie_def
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
A : Type v
inst : Ring A
x x_1 x_2 : A
⊢ x * (x_1 * x_2) - x * (x_2 * x_1) - (x_1 * (x_2 * x) - x_2 * (x_1 * x)) =
    x * (x_1 * x_2) - x_1 * (x * x_2) - (x_2 * (x * x_1) - x_2 * (x_1 * x)) +
      (x_1 * (x * x_2) - x_1 * (x_2 * x) - (x * (x_2 * x_1) - x_2 * (x * x_1)))

Tactic:
abel
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
A : Type v
inst : Ring A
x y : A
⊢ ⁅x, y⁆ = x * y - y * x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
A : Type v
inst : Ring A
α : Type u_1
f g : α → A
a : α
⊢ ⁅f, g⁆ a = ⁅f a, g a⁆

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
A : Type v
inst : Ring A
M : Type w
inst_1 : AddCommGroup M
inst_2 : Module A M
⊢ ∀ (x y : A) (m : M), x • y • m = ⁅x, y⁆ • m + y • x • m

Tactic:
simp [LieRing.of_associative_ring_bracket, sub_smul, mul_smul, sub_add_cancel]

Premises used: sub_smul, LieRing.of_associative_ring_bracket, sub_add_cancel, SemigroupAction.mul_smul
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
A : Type v
inst : Ring A
M : Type w
inst_1 : AddCommGroup M
inst_2 : Module A M
a : A
m : M
⊢ ⁅a, m⁆ = a • m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
A : Type v
inst : Ring A
R : Type u
inst_1 : CommRing R
inst_2 : Algebra R A
t : R
x y : A
rw : x * t • y - t • y * x = t • ⁅x, y⁆
rw₁ : x * t • y - t • y * x = t • (x * y - y * x)
rw₂ : t • (x * y) - t • y * x = t • (x * y - y * x)
rw₃ : t • (x * y) - t • (y * x) = t • (x * y - y * x)
rw₄ rw₅ : t • (x * y) - t • (y * x) = t • (x * y) - t • (y * x)
⊢ ⁅x, t • y⁆ = t • ⁅x, y⁆

Tactic:
rw [LieRing.of_associative_ring_bracket, LieRing.of_associative_ring_bracket,
      Algebra.mul_smul_comm, Algebra.smul_mul_assoc, smul_sub]

Premises used: Algebra.mul_smul_comm, LieRing.of_associative_ring_bracket, smul_sub, Algebra.smul_mul_assoc
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
A : Type v
inst : Ring A
R : Type u
inst_1 : CommRing R
inst_2 : Algebra R A
M : Type w
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
⊢ LieModule R (End R M) M

Tactic:
LieModule.ofAssociativeModule

Premises used: LieModule.ofAssociativeModule
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
inst : CommRing R
M : Type w
inst_1 : AddCommGroup M
inst_2 : Module R M
f : End R M
m : M
⊢ ⁅f, m⁆ = (f : (a : M) → M) m

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
inst : CommRing R
M : Type w
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Eq.{w + 1} (α := LieRingModule (End R M) (M →ₗ[R] M)) LinearMap.instLieRingModule lieRingSelfModule

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
A : Type v
inst : Ring A
R : Type u
inst_1 : CommRing R
inst_2 : Algebra R A
B : Type w
C : Type w₁
inst_3 : Ring B
inst_4 : Ring C
inst_5 : Algebra R B
inst_6 : Algebra R C
f : A →ₐ[R] B
g : B →ₐ[R] C
x x_1 : A
⊢ f.toLinearMap.toFun ⁅x, x_1⁆ = ⁅f.toLinearMap.toFun x, f.toLinearMap.toFun x_1⁆

Tactic:
simp [LieRing.of_associative_ring_bracket]

Premises used: LieRing.of_associative_ring_bracket
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
A : Type v
inst : Ring A
R : Type u
inst_1 : CommRing R
inst_2 : Algebra R A
B : Type w
inst_3 : Ring B
inst_4 : Algebra R B
f : A →ₐ[R] B
⊢ Eq (α := (a : A) → B) (⇑f.toLieHom : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
A : Type v
inst : Ring A
R : Type u
inst_1 : CommRing R
inst_2 : Algebra R A
B : Type w
inst_3 : Ring B
inst_4 : Algebra R B
f : A →ₐ[R] B
x : A
⊢ Eq.{w + 1} (α := B) ((f.toLieHom : (a : A) → B) x : B) ((f : (a : A) → B) x : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
A : Type v
inst : Ring A
R : Type u
inst_1 : CommRing R
inst_2 : Algebra R A
⊢ Eq (α := A →ₗ⁅R⁆ A) (toLieHom (AlgHom.id R A)) LieHom.id

Tactic:
rfl

Premises used: AlgHom.toLinearMap, LieHom.id, rfl
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
A : Type v
inst : Ring A
R : Type u
inst_1 : CommRing R
inst_2 : Algebra R A
B : Type w
C : Type w₁
inst_3 : Ring B
inst_4 : Ring C
inst_5 : Algebra R B
inst_6 : Algebra R C
f : A →ₐ[R] B
g : B →ₐ[R] C
⊢ (g.comp f).toLieHom = g.toLieHom.comp f.toLieHom

Tactic:
rfl

Premises used: AlgHom.toLieHom, LieHom.comp, rfl
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
A : Type v
inst : Ring A
R : Type u
inst_1 : CommRing R
inst_2 : Algebra R A
B : Type w
inst_3 : Ring B
inst_4 : Algebra R B
f g : A →ₐ[R] B
h : f.toLieHom = g.toLieHom
H : ∀ (a : A), Eq.{w + 1} (α := B) ((f : (a : A) → B) a : B) ((g : (a : A) → B) a : B)
⊢ f = g

Tactic:
ext a
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
A : Type v
inst : Ring A
R : Type u
inst_1 : CommRing R
inst_2 : Algebra R A
B : Type w
inst_3 : Ring B
inst_4 : Algebra R B
f g : A →ₐ[R] B
h : f.toLieHom = g.toLieHom
a : A
⊢ Eq.{w + 1} (α := B) ((f : (a : A) → B) a : B) ((g : (a : A) → B) a : B)

Tactic:
LieHom.congr_fun h a

Premises used: LieHom.congr_fun
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
A : Type v
inst : Ring A
R : Type u
inst_1 : CommRing R
inst_2 : Algebra R A
B : Type w
inst_3 : Ring B
inst_4 : Algebra R B
f g : A →ₐ[R] B
h : f.toLieHom = g.toLieHom
a : A
⊢ Eq.{w + 1} (α := B) ((f : (a : A) → B) a : B) ((g : (a : A) → B) a : B)

Tactic:
exact LieHom.congr_fun h a

Premises used: LieHom.congr_fun
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y : L
h :
  ∀ (m : M),
    Eq (α := M) (({ toFun := fun (m : M) ↦ ⁅x + y, m⁆, map_add' := ⋯, map_smul' := ⋯ } : (a : M) → M) m : M)
      ((HAdd.hAdd (α := Module.End R M) { toFun := fun (m : M) ↦ ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] M }
              { toFun := fun (m : M) ↦ ⁅y, m⁆, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] M } :
            (a : M) → M)
          m :
        M)
⊢ { toFun := fun (m : M) ↦ ⁅x + y, m⁆, map_add' := ⋯, map_smul' := ⋯ } =
    HAdd.hAdd (α := Module.End R M) { toFun := fun (m : M) ↦ ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] M }
      { toFun := fun (m : M) ↦ ⁅y, m⁆, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] M }

Tactic:
ext m
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y : L
m : M
⊢ Eq (α := M) (({ toFun := fun (m : M) ↦ ⁅x + y, m⁆, map_add' := ⋯, map_smul' := ⋯ } : (a : M) → M) m : M)
    ((HAdd.hAdd (α := Module.End R M) { toFun := fun (m : M) ↦ ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] M }
            { toFun := fun (m : M) ↦ ⁅y, m⁆, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] M } :
          (a : M) → M)
        m :
      M)

Tactic:
apply add_lie

Premises used: add_lie
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
t : R
x : L
h :
  ∀ (m : M),
    Eq (α := M) (({ toFun := fun (m : M) ↦ ⁅t • x, m⁆, map_add' := ⋯, map_smul' := ⋯ } : (a : M) → M) m : M)
      ((HSMul.hSMul (α := R) (β := Module.End R M) ((RingHom.id R : (a : R) → R) t : R)
              { toFun := fun (m : M) ↦ ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] M } :
            (a : M) → M)
          m :
        M)
⊢ { toFun := fun (m : M) ↦ ⁅t • x, m⁆, map_add' := ⋯, map_smul' := ⋯ } =
    HSMul.hSMul (α := R) (β := Module.End R M) ((RingHom.id R : (a : R) → R) t : R)
      { toFun := fun (m : M) ↦ ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] M }

Tactic:
ext m
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
t : R
x : L
m : M
⊢ Eq (α := M) (({ toFun := fun (m : M) ↦ ⁅t • x, m⁆, map_add' := ⋯, map_smul' := ⋯ } : (a : M) → M) m : M)
    ((HSMul.hSMul (α := R) (β := Module.End R M) ((RingHom.id R : (a : R) → R) t : R)
            { toFun := fun (m : M) ↦ ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ : M →ₗ[R] M } :
          (a : M) → M)
        m :
      M)

Tactic:
apply smul_lie

Premises used: smul_lie
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y : L
h :
  ∀ (m : M),
    Eq (α := M) (({ toFun := fun (m : M) ↦ ⁅⁅x, y⁆, m⁆, map_add' := ⋯, map_smul' := ⋯ } : (a : M) → M) m : M)
      ((Bracket.bracket (L := Module.End R M) { toFun := fun (m : M) ↦ ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ }
              { toFun := fun (m : M) ↦ ⁅y, m⁆, map_add' := ⋯, map_smul' := ⋯ } :
            (a : M) → M)
          m :
        M)
⊢ Eq.{w + 1} (α := Module.End R M) { toFun := fun (m : M) ↦ ⁅⁅x, y⁆, m⁆, map_add' := ⋯, map_smul' := ⋯ }
    (Bracket.bracket (L := Module.End R M) { toFun := fun (m : M) ↦ ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ }
      { toFun := fun (m : M) ↦ ⁅y, m⁆, map_add' := ⋯, map_smul' := ⋯ })

Tactic:
ext m
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y : L
m : M
⊢ Eq (α := M) (({ toFun := fun (m : M) ↦ ⁅⁅x, y⁆, m⁆, map_add' := ⋯, map_smul' := ⋯ } : (a : M) → M) m : M)
    ((Bracket.bracket (L := Module.End R M) { toFun := fun (m : M) ↦ ⁅x, m⁆, map_add' := ⋯, map_smul' := ⋯ }
            { toFun := fun (m : M) ↦ ⁅y, m⁆, map_add' := ⋯, map_smul' := ⋯ } :
          (a : M) → M)
        m :
      M)

Tactic:
apply lie_lie

Premises used: lie_lie
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x y : L
⊢ (((ad R L : (a : L) → Module.End R L) x : Module.End R L) : (a : L) → L) y = ⁅x, y⁆

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
h :
  ∀ (g : Module.End R M) (m : M),
    Eq (α := M)
      ((((toEnd R (Module.End R M) M : (a : Module.End R M) → Module.End R M) g : Module.End R M) : (a : M) → M) m : M)
      ((((LieHom.id : (a : Module.End R M) → Module.End R M) g : Module.End R M) : (a : M) → M) m : M)
⊢ Eq (α := Module.End R M →ₗ⁅R⁆ Module.End R M) (toEnd R (Module.End R M) M) LieHom.id

Tactic:
ext g m
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
g : Module.End R M
m : M
⊢ Eq (α := M)
    ((((toEnd R (Module.End R M) M : (a : Module.End R M) → Module.End R M) g : Module.End R M) : (a : M) → M) m : M)
    ((((LieHom.id : (a : Module.End R M) → Module.End R M) g : Module.End R M) : (a : M) → M) m : M)

Tactic:
simp [lie_eq_smul]

Premises used: lie_eq_smul
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
K : LieSubalgebra R L
x : ↥K
⊢ Eq.{w + 1} (α := Module.End R M) ((LieModule.toEnd R (↥K) M : (a : ↥K) → Module.End R M) x : Module.End R M)
    (((LieModule.toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) (↑x : L) :
      Module.End R M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
K : LieSubalgebra R L
x : L
hx : x ∈ K
⊢ Eq.{w + 1} (α := Module.End R M)
    ((LieModule.toEnd R (↥K) M : (a : ↥K) → Module.End R M) (Subtype.mk (p := fun (x : L) ↦ x ∈ K) x hx) :
      Module.End R M)
    (((LieModule.toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : IsFaithful R L M
x y : L
⊢ Eq.{w + 1} (α := Module.End R M)
      (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
      (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M) ↔
    x = y

Tactic:
IsFaithful.injective_toEnd.eq_iff

Premises used: Function.Injective.eq_iff, LieModule.IsFaithful.injective_toEnd
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : IsFaithful R L M
x y : L
h : ∀ (m : M), ⁅x, m⁆ = ⁅y, m⁆
⊢ x = y

Tactic:
(toEnd_eq_iff R L M).mp <| LinearMap.ext h

Premises used: LinearMap.ext, LieModule.toEnd_eq_iff, Iff.mp
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : IsFaithful R L M
x : L
rw :
  Eq.{w + 1} (α := Module.End R M)
      (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
      ((((↑(toEnd R L M) : LinearMap.{u, u, v, w} (RingHom.id R) L (Module.End R M)) :
              LinearMap.{u, u, v, w} (RingHom.id R) L (Module.End R M)) :
            (a : L) → Module.End R M)
          0 :
        Module.End R M) ↔
    x = 0
⊢ Eq.{w + 1} (α := Module.End R M)
      (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
      (0 : Module.End R M) ↔
    x = 0

Tactic:
rw [← (toEnd R L M).toLinearMap.map_zero]

Premises used: LinearMap.map_zero, LieModule.toEnd, LieHom.toLinearMap
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : IsFaithful R L M
x : L
⊢ Eq.{w + 1} (α := Module.End R M)
      (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
      ((((↑(toEnd R L M) : LinearMap.{u, u, v, w} (RingHom.id R) L (Module.End R M)) :
              LinearMap.{u, u, v, w} (RingHom.id R) L (Module.End R M)) :
            (a : L) → Module.End R M)
          0 :
        Module.End R M) ↔
    x = 0

Tactic:
toEnd_eq_iff R L M

Premises used: LieModule.toEnd_eq_iff
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : IsFaithful R L M
x : L
⊢ Eq.{w + 1} (α := Module.End R M)
      (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
      ((((↑(toEnd R L M) : LinearMap.{u, u, v, w} (RingHom.id R) L (Module.End R M)) :
              LinearMap.{u, u, v, w} (RingHom.id R) L (Module.End R M)) :
            (a : L) → Module.End R M)
          0 :
        Module.End R M) ↔
    x = 0

Tactic:
exact toEnd_eq_iff R L M

Premises used: LieModule.toEnd_eq_iff
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
⊢ IsFaithful R L M ↔ ∀ (x : L), (∀ (m : M), ⁅x, m⁆ = 0) → x = 0

Tactic:
⟨fun h x hx ↦ ?_, fun h ↦ ⟨fun x y hxy ↦ ?_⟩⟩

Premises used: LieModule.IsFaithful.mk, Iff.intro
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
refine_1 : ∀ (h : IsFaithful R L M) (x : L) (hx : ∀ (m : M), ⁅x, m⁆ = 0), x = 0
refine_2 :
  ∀ (h : ∀ (x : L), (∀ (m : M), ⁅x, m⁆ = 0) → x = 0) (x y : L)
    (hxy :
      Eq.{w + 1} (α := Module.End R M)
        (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
        (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M)),
    x = y
⊢ IsFaithful R L M ↔ ∀ (x : L), (∀ (m : M), ⁅x, m⁆ = 0) → x = 0

Tactic:
refine ⟨fun h x hx ↦ ?_, fun h ↦ ⟨fun x y hxy ↦ ?_⟩⟩
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h : IsFaithful R L M
x : L
hx : ∀ (m : M), ⁅x, m⁆ = 0
h₁ :
  ∀ (m : M),
    Eq (α := M)
      (((((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) :
            (a : M) → M)
          m :
        M)
      ((0 : (a : M) → M) m : M)
⊢ Eq.{w + 1} (α := Module.End R M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
    (0 : Module.End R M)

Tactic:
ext m
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h : IsFaithful R L M
x : L
hx : ∀ (m : M), ⁅x, m⁆ = 0
m : M
⊢ Eq (α := M)
    (((((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M) :
          (a : M) → M)
        m :
      M)
    ((0 : (a : M) → M) m : M)

Tactic:
simpa using hx m
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h : IsFaithful R L M
x : L
hx : ∀ (m : M), ⁅x, m⁆ = 0
⊢ Eq.{w + 1} (α := Module.End R M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
    (0 : Module.End R M)

Tactic:
replace hx : toEnd R L M x = 0 := by ext m; simpa using hx m
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h : IsFaithful R L M
x : L
hx :
  Eq.{w + 1} (α := Module.End R M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
    (0 : Module.End R M)
⊢ x = 0

Tactic:
simpa using hx
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h : ∀ (x : L), (∀ (m : M), ⁅x, m⁆ = 0) → x = 0
x y : L
hxy :
  Eq.{w + 1} (α := Module.End R M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M)
refine_2 : x - y = 0
⊢ x = y

Tactic:
rw [← sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
h : ∀ (x : L), (∀ (m : M), ⁅x, m⁆ = 0) → x = 0
x y : L
hxy :
  Eq.{w + 1} (α := Module.End R M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
    (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) y : Module.End R M)
⊢ x - y = 0

Tactic:
h _ fun m ↦ ?_