awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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
x : L
hx : x ∈ H.normalizer
v : L
hv : v ∈ H
w : L
hw : w ∈ H
t : R
hu₁ : Membership.mem (γ := Submodule R L) (R ∙ x) (t • x)
s : R
hu₂ : Membership.mem (γ := Submodule R L) (R ∙ x) (s • x)
a : ⁅v, x⁆ ∈ H
⊢ s • ⁅v, x⁆ + (t • ⁅x, w⁆ + ⁅v, w⁆) ∈ H
have a₁ : ⁅x, w⁆ ∈ H
Tactic: refine H.add_mem (H.smul_mem s ?_) (H.add_mem (H.smul_mem t ?_) (H.lie_mem hv hw))
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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
x y : L
hx : x ∈ H.normalizer
hy : y ∈ H
⊢ ⁅x, y⁆ ∈ H
have rw : ⁅y, x⁆ ∈ H
Tactic: rw [← lie_skew, neg_mem_iff (G := L)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H K : LieSubalgebra R L
h₁ : H ≤ K
h₂ : K ≤ H.normalizer
⊢ ∃ (I : LieIdeal R ↥K), LieIdeal.toLieSubalgebra R (↥K) I = ofLe h₁
have rw : ∀ (x y : L), x ∈ K → y ∈ H → ⁅x, y⁆ ∈ H
Tactic: rw [exists_nested_lieIdeal_coe_eq_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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.normalizer = H ↔
    Eq.{u_2 + 1} (α := LieSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
      (LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)) ⊥
have rw : H.normalizer = H ↔
  ∀ (m : L ⧸ H.toLieSubmodule),
    Membership.mem (γ := LieSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
        (LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)) m →
      m = 0
Tactic: rw [LieSubmodule.eq_bot_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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.normalizer = H ↔
    ∀ (m : L ⧸ H.toLieSubmodule),
      Membership.mem (γ := LieSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
          (LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)) m →
        m = 0
have refine_1 : ∀ (h : H.normalizer = H) (m : L ⧸ H.toLieSubmodule),
  Membership.mem (γ := LieSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
      (LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)) m →
    m = 0
Tactic: refine ⟨fun h => ?_, fun h => le_antisymm ?_ H.le_normalizer⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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
refine_1 :
  ∀ (h : H.normalizer = H) (m : L ⧸ H.toLieSubmodule),
    Membership.mem (γ := LieSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
        (LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)) m →
      m = 0
⊢ H.normalizer = H ↔
    ∀ (m : L ⧸ H.toLieSubmodule),
      Membership.mem (γ := LieSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
          (LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)) m →
        m = 0
have refine_2 : ∀
  (h :
    ∀ (m : L ⧸ H.toLieSubmodule),
      Membership.mem (γ := LieSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
          (LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule)) m →
        m = 0),
  H.normalizer ≤ H
Tactic: refine ⟨fun h => ?_, fun h => le_antisymm ?_ H.le_normalizer⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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 : H.normalizer = H
m : L ⧸ H.toLieSubmodule
x : L
hx :
  Membership.mem (γ := LieSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
    (LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
    (Quot.mk (⇑(↑H.toLieSubmodule : Submodule R L).quotientRel : L → L → Prop) x)
this : x ∈ H
⊢ Eq (α := L ⧸ H.toLieSubmodule) (Quot.mk (⇑(↑H.toLieSubmodule : Submodule R L).quotientRel : L → L → Prop) x) 0
have rwa : Eq (α := L ⧸ H.toLieSubmodule) (Submodule.Quotient.mk x) 0
Tactic: rwa [Submodule.Quotient.quot_mk_eq_mk, Submodule.Quotient.mk_eq_zero,
      coe_toLieSubmodule, mem_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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 : H.normalizer = H
m : L ⧸ H.toLieSubmodule
x : L
hx :
  Membership.mem (γ := LieSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
    (LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
    (Quot.mk (⇑(↑H.toLieSubmodule : Submodule R L).quotientRel : L → L → Prop) x)
this : x ∈ H
rwa : Eq (α := L ⧸ H.toLieSubmodule) (Submodule.Quotient.mk x) 0
⊢ Eq (α := L ⧸ H.toLieSubmodule) (Quot.mk (⇑(↑H.toLieSubmodule : Submodule R L).quotientRel : L → L → Prop) x) 0
have rwa₁ : x ∈ (↑H.toLieSubmodule : Submodule R L)
Tactic: rwa [Submodule.Quotient.quot_mk_eq_mk, Submodule.Quotient.mk_eq_zero,
      coe_toLieSubmodule, mem_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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 : H.normalizer = H
m : L ⧸ H.toLieSubmodule
x : L
hx :
  Membership.mem (γ := LieSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
    (LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
    (Quot.mk (⇑(↑H.toLieSubmodule : Submodule R L).quotientRel : L → L → Prop) x)
this : x ∈ H
rwa : Eq (α := L ⧸ H.toLieSubmodule) (Submodule.Quotient.mk x) 0
rwa₁ : x ∈ (↑H.toLieSubmodule : Submodule R L)
⊢ Eq (α := L ⧸ H.toLieSubmodule) (Quot.mk (⇑(↑H.toLieSubmodule : Submodule R L).quotientRel : L → L → Prop) x) 0
have rwa₂ : x ∈ H.toSubmodule
Tactic: rwa [Submodule.Quotient.quot_mk_eq_mk, Submodule.Quotient.mk_eq_zero,
      coe_toLieSubmodule, mem_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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 : H.normalizer = H
m : L ⧸ H.toLieSubmodule
x : L
hx :
  Membership.mem (γ := LieSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
    (LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
    (Quot.mk (⇑(↑H.toLieSubmodule : Submodule R L).quotientRel : L → L → Prop) x)
⊢ Eq (α := L ⧸ H.toLieSubmodule) (Quot.mk (⇑(↑H.toLieSubmodule : Submodule R L).quotientRel : L → L → Prop) x) 0
have refine_1 : x ∈ H
Tactic: suffices x ∈ H by rwa [Submodule.Quotient.quot_mk_eq_mk, Submodule.Quotient.mk_eq_zero,
      coe_toLieSubmodule, mem_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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 : H.normalizer = H
m : L ⧸ H.toLieSubmodule
x : L
hx :
  Membership.mem (γ := LieSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
    (LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
    (Quot.mk (⇑(↑H.toLieSubmodule : Submodule R L).quotientRel : L → L → Prop) x)
⊢ x ∈ H
have refine_1 : ∀ y ∈ H, ⁅y, x⁆ ∈ H
Tactic: rw [← h, H.mem_normalizer_iff']
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (hypothesis)
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 : H.normalizer = H
m : L ⧸ H.toLieSubmodule
x : L
hx :
  Membership.mem (γ := LieSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
    (LieModule.maxTrivSubmodule R (↥H) (L ⧸ H.toLieSubmodule))
    (Quot.mk (⇑(↑H.toLieSubmodule : Submodule R L).quotientRel : L → L → Prop) x)
y : L
hy : y ∈ H
⊢ ⁅y, x⁆ ∈ H
have hx₁ : Eq (α := L ⧸ H.toLieSubmodule)
  (⁅Subtype.mk (p := fun (x : L) ↦ x ∈ H) y hy,
      (LieSubmodule.Quotient.mk' H.toLieSubmodule : (a : L) → L ⧸ H.toLieSubmodule) x⁆ :
    L ⧸ H.toLieSubmodule)
  (0 : L ⧸ H.toLieSubmodule)
Tactic: replace hx : ⁅_, LieSubmodule.Quotient.mk' _ x⁆ = 0 := hx ⟨y, hy⟩
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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 : H.normalizer = H
m : L ⧸ H.toLieSubmodule
x y : L
hy : y ∈ H
hx :
  Eq (α := L ⧸ H.toLieSubmodule)
    (⁅Subtype.mk (p := fun (x : L) ↦ x ∈ H) y hy,
        (LieSubmodule.Quotient.mk' H.toLieSubmodule : (a : L) → L ⧸ H.toLieSubmodule) x⁆ :
      L ⧸ H.toLieSubmodule)
    (0 : L ⧸ H.toLieSubmodule)
⊢ ⁅y, x⁆ ∈ H
have refine_1 : ∀
  (hx :
    Eq (α := L ⧸ H.toLieSubmodule)
      ((LieSubmodule.Quotient.mk' H.toLieSubmodule : (a : L) → L ⧸ H.toLieSubmodule)
          ⁅Subtype.mk (p := fun (x : L) ↦ x ∈ H) y hy, x⁆ :
        L ⧸ H.toLieSubmodule)
      (0 : L ⧸ H.toLieSubmodule)),
  ⁅y, x⁆ ∈ H
Tactic: rwa [← LieModuleHom.map_lie, LieSubmodule.Quotient.mk_eq_zero] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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 : H.normalizer = H
m : L ⧸ H.toLieSubmodule
x y : L
hy : y ∈ H
hx :
  Eq (α := L ⧸ H.toLieSubmodule)
    (⁅Subtype.mk (p := fun (x : L) ↦ x ∈ H) y hy,
        (LieSubmodule.Quotient.mk' H.toLieSubmodule : (a : L) → L ⧸ H.toLieSubmodule) x⁆ :
      L ⧸ H.toLieSubmodule)
    (0 : L ⧸ H.toLieSubmodule)
refine_1 :
  ∀
    (hx :
      Eq (α := L ⧸ H.toLieSubmodule)
        ((LieSubmodule.Quotient.mk' H.toLieSubmodule : (a : L) → L ⧸ H.toLieSubmodule)
            ⁅Subtype.mk (p := fun (x : L) ↦ x ∈ H) y hy, x⁆ :
          L ⧸ H.toLieSubmodule)
        (0 : L ⧸ H.toLieSubmodule)),
    ⁅y, x⁆ ∈ H
⊢ ⁅y, x⁆ ∈ H
have refine_1₁ : ∀ (hx : ⁅Subtype.mk (p := fun (x : L) ↦ x ∈ H) y hy, x⁆ ∈ H.toLieSubmodule), ⁅y, x⁆ ∈ H
Tactic: rwa [← LieModuleHom.map_lie, LieSubmodule.Quotient.mk_eq_zero] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (goal)
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
z : L
hz : z ∈ H
⊢ ⁅Subtype.mk (p := fun (x : L) ↦ x ∈ H) z hz, y⁆ = 0
have rw : ⁅z, x⁆ ∈ H
Tactic: rw [← LieModuleHom.map_lie, LieSubmodule.Quotient.mk_eq_zero, coe_bracket_of_module,
        Submodule.coe_mk, mem_toLieSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Normalizer (hypothesis)
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
⊢ x ∈ H
have hy : 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
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
Goal:
A : Type v
inst : Ring A
x x_1 x_2 : A
⊢ ⁅x + x_1, x_2⁆ = ⁅x, x_2⁆ + ⁅x_1, x_2⁆
have 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)
Tactic: simp only [Ring.lie_def, right_distrib, left_distrib]
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
Goal:
A : Type v
inst : Ring A
x x_1 x_2 : A
⊢ ⁅x, x_1 + x_2⁆ = ⁅x, x_1⁆ + ⁅x, x_2⁆
have 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)
Tactic: simp only [Ring.lie_def, right_distrib, left_distrib]
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
Goal:
A : Type v
inst : Ring A
x x_1 x_2 : A
⊢ ⁅x, ⁅x_1, x_2⁆⁆ = ⁅⁅x, x_1⁆, x_2⁆ + ⁅x_1, ⁅x, x_2⁆⁆
have 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)))
Tactic: simp only [Ring.lie_def, mul_sub_left_distrib, mul_sub_right_distrib, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
Goal:
A : Type v
inst : Ring A
R : Type u
inst_1 : CommRing R
inst_2 : Algebra R A
t : R
x y : A
⊢ ⁅x, t • y⁆ = t • ⁅x, y⁆
have rw : x * t • y - t • y * x = 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]
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
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⁆
⊢ ⁅x, t • y⁆ = t • ⁅x, y⁆
have rw₁ : x * t • y - t • y * x = t • (x * y - y * x)
Tactic: rw [LieRing.of_associative_ring_bracket, LieRing.of_associative_ring_bracket,
      Algebra.mul_smul_comm, Algebra.smul_mul_assoc, smul_sub]
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
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)
⊢ ⁅x, t • y⁆ = t • ⁅x, y⁆
have rw₂ : t • (x * y) - t • y * x = t • (x * y - y * x)
Tactic: rw [LieRing.of_associative_ring_bracket, LieRing.of_associative_ring_bracket,
      Algebra.mul_smul_comm, Algebra.smul_mul_assoc, smul_sub]
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
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)
⊢ ⁅x, t • y⁆ = t • ⁅x, y⁆
have rw₃ : t • (x * y) - t • (y * x) = t • (x * y - y * x)
Tactic: rw [LieRing.of_associative_ring_bracket, LieRing.of_associative_ring_bracket,
      Algebra.mul_smul_comm, Algebra.smul_mul_assoc, smul_sub]
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
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)
⊢ ⁅x, t • y⁆ = t • ⁅x, y⁆
have rw₄ : t • (x * y) - t • (y * x) = t • (x * y) - t • (y * x)
Tactic: rw [LieRing.of_associative_ring_bracket, LieRing.of_associative_ring_bracket,
      Algebra.mul_smul_comm, Algebra.smul_mul_assoc, smul_sub]
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
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
⊢ f = g
have H : ∀ (a : A), Eq.{w + 1} (α := B) ((f : (a : A) → B) a : B) ((g : (a : A) → B) a : B)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
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
⊢ { 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 }
have h : ∀ (m : M),
  Eq (α := M) (({ toFun := fun (m : M) ↦ ⁅x + y, m⁆, map_add' := sorry, map_smul' := sorry } : (a : M) → M) m : M)
    ((HAdd.hAdd (α := Module.End R M) { toFun := fun (m : M) ↦ ⁅x, m⁆, map_add' := sorry, map_smul' := sorry : M →ₗ[R] M }
            { toFun := fun (m : M) ↦ ⁅y, m⁆, map_add' := sorry, map_smul' := sorry : M →ₗ[R] M } :
          (a : M) → M)
        m :
      M)
Tactic: ext m
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
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
⊢ { 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 }
have h : ∀ (m : M),
  Eq (α := M) (({ toFun := fun (m : M) ↦ ⁅t • x, m⁆, map_add' := sorry, map_smul' := sorry } : (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' := sorry, map_smul' := sorry : M →ₗ[R] M } :
          (a : M) → M)
        m :
      M)
Tactic: ext m
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
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
⊢ 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' := ⋯ })
have h : ∀ (m : M),
  Eq (α := M) (({ toFun := fun (m : M) ↦ ⁅⁅x, y⁆, m⁆, map_add' := sorry, map_smul' := sorry } : (a : M) → M) m : M)
    ((Bracket.bracket (L := Module.End R M) { toFun := fun (m : M) ↦ ⁅x, m⁆, map_add' := sorry, map_smul' := sorry }
            { toFun := fun (m : M) ↦ ⁅y, m⁆, map_add' := sorry, map_smul' := sorry } :
          (a : M) → M)
        m :
      M)
Tactic: ext m
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
Goal:
R : Type u
M : Type w
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Eq (α := Module.End R M →ₗ⁅R⁆ Module.End R M) (toEnd R (Module.End R M) M) LieHom.id
have 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)
Tactic: ext g m
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
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)
      (0 : Module.End R M) ↔
    x = 0
have 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
Tactic: rw [← (toEnd R L M).toLinearMap.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
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
have refine_1 : ∀ (h : IsFaithful R L M) (x : L) (hx : ∀ (m : M), ⁅x, m⁆ = 0), x = 0
Tactic: refine ⟨fun h x hx ↦ ?_, fun h ↦ ⟨fun x y hxy ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
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
⊢ IsFaithful R L M ↔ ∀ (x : L), (∀ (m : M), ⁅x, m⁆ = 0) → x = 0
have 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
Tactic: refine ⟨fun h x hx ↦ ?_, fun h ↦ ⟨fun x y hxy ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
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)
have 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)
Tactic: ext m
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (hypothesis)
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
⊢ x = 0
have 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)
Tactic: replace hx : toEnd R L M x = 0 := by ext m; simpa using hx m
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
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
have refine_2 : x - y = 0
Tactic: rw [← sub_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
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
have refine_2 : ∀ (m : M), ⁅x - y, m⁆ = 0
Tactic: refine h _ fun m ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (goal)
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)
m : M
⊢ ⁅x - y, m⁆ = 0
have refine_2 : ⁅x, m⁆ - ⁅y, m⁆ = 0
Tactic: rw [sub_lie, sub_eq_zero, ← toEnd_apply_apply R, ← toEnd_apply_apply R, hxy]