awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Quotient (goal)
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
N N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
I J : LieIdeal R L
x y z : L
⊢ ⁅HAdd.hAdd (α := L ⧸ I) (Quotient.mk'' x) (Quotient.mk'' y), Quotient.mk'' z⁆ =
    HAdd.hAdd (α := L ⧸ I) (Bracket.bracket (L := L ⧸ I) (Quotient.mk'' x) (Quotient.mk'' z))
      (Bracket.bracket (L := L ⧸ I) (Quotient.mk'' y) (Quotient.mk'' z))
have h : Eq (α := L ⧸ I) (mk ⁅x + y, z⁆) (Submodule.Quotient.mk (⁅x, z⁆ + ⁅y, z⁆))
Tactic: repeat'
      first
      | rw [is_quotient_mk]
      | rw [← mk_bracket]
      | rw [← Submodule.Quotient.mk_add (R := R) (M := L)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Quotient (goal)
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
N N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
I J : LieIdeal R L
x y z : L
⊢ Eq (α := L ⧸ I) (mk ⁅x + y, z⁆) (Submodule.Quotient.mk (⁅x, z⁆ + ⁅y, z⁆))
have h : ⁅x + y, z⁆ = ⁅x, z⁆ + ⁅y, z⁆
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.Algebra.Lie.Quotient (goal)
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
N N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
I J : LieIdeal R L
x' y' z' : L ⧸ I
⊢ ⁅x', y' + z'⁆ = ⁅x', y'⁆ + ⁅x', z'⁆
have h : ∀ (x y z : L),
  Bracket.bracket (L := L ⧸ I) (Quotient.mk'' x) (HAdd.hAdd (α := L ⧸ I) (Quotient.mk'' y) (Quotient.mk'' z)) =
    HAdd.hAdd (α := L ⧸ I) (Bracket.bracket (L := L ⧸ I) (Quotient.mk'' x) (Quotient.mk'' y))
      (Bracket.bracket (L := L ⧸ I) (Quotient.mk'' x) (Quotient.mk'' z))
Tactic: induction x', y', z' using Quotient.inductionOn₃' with | _ x y z
Cleared hypotheses: x', y', z'
-- Lean 4 proof step from Mathlib.Algebra.Lie.Quotient (goal)
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
N N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
I J : LieIdeal R L
x y z : L
⊢ Bracket.bracket (L := L ⧸ I) (mk x) (HAdd.hAdd (α := L ⧸ I) (mk y) (mk z)) =
    HAdd.hAdd (α := L ⧸ I) (mk ⁅x, y⁆) (mk ⁅x, z⁆)
have h : Bracket.bracket (L := L ⧸ I) (mk x) (Submodule.Quotient.mk (y + z)) = HAdd.hAdd (α := L ⧸ I) (mk ⁅x, y⁆) (mk ⁅x, z⁆)
Tactic: rw [← Submodule.Quotient.mk_add (R := R) (M := L)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Quotient (goal)
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
N N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
I J : LieIdeal R L
x y z : L
⊢ Bracket.bracket (L := L ⧸ I) (mk x) (HAdd.hAdd (α := L ⧸ I) (mk y) (mk z)) =
    HAdd.hAdd (α := L ⧸ I) (mk ⁅x, y⁆) (mk ⁅x, z⁆)
have h : Bracket.bracket (L := L ⧸ I) (mk x) (Submodule.Quotient.mk (y + z)) = HAdd.hAdd (α := L ⧸ I) (mk ⁅x, y⁆) (mk ⁅x, z⁆)
Tactic: first
      | rw [is_quotient_mk]
      | rw [← mk_bracket]
      | rw [← Submodule.Quotient.mk_add (R := R) (M := L)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Quotient (goal)
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
N N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
I J : LieIdeal R L
x y z : L
⊢ mk ⁅x, y + z⁆ = HAdd.hAdd (α := L ⧸ I) (mk ⁅x, y⁆) (mk ⁅x, z⁆)
have h : Eq (α := L ⧸ I) (mk ⁅x, y + z⁆) (Submodule.Quotient.mk (⁅x, y⁆ + ⁅x, z⁆))
Tactic: rw [← Submodule.Quotient.mk_add (R := R) (M := L)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Quotient (goal)
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
N N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
I J : LieIdeal R L
x y z : L
⊢ mk ⁅x, y + z⁆ = HAdd.hAdd (α := L ⧸ I) (mk ⁅x, y⁆) (mk ⁅x, z⁆)
have h : Eq (α := L ⧸ I) (mk ⁅x, y + z⁆) (Submodule.Quotient.mk (⁅x, y⁆ + ⁅x, z⁆))
Tactic: first
      | rw [is_quotient_mk]
      | rw [← mk_bracket]
      | rw [← Submodule.Quotient.mk_add (R := R) (M := L)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Quotient (goal)
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
N N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
I J : LieIdeal R L
x y z : L
⊢ Bracket.bracket (L := L ⧸ I) (Quotient.mk'' x) (HAdd.hAdd (α := L ⧸ I) (Quotient.mk'' y) (Quotient.mk'' z)) =
    HAdd.hAdd (α := L ⧸ I) (Bracket.bracket (L := L ⧸ I) (Quotient.mk'' x) (Quotient.mk'' y))
      (Bracket.bracket (L := L ⧸ I) (Quotient.mk'' x) (Quotient.mk'' z))
have h : Eq (α := L ⧸ I) (mk ⁅x, y + z⁆) (Submodule.Quotient.mk (⁅x, y⁆ + ⁅x, z⁆))
Tactic: repeat'
      first
      | rw [is_quotient_mk]
      | rw [← mk_bracket]
      | rw [← Submodule.Quotient.mk_add (R := R) (M := L)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Quotient (goal)
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
N N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
I J : LieIdeal R L
x y z : L
⊢ Eq (α := L ⧸ I) (mk ⁅x, y + z⁆) (Submodule.Quotient.mk (⁅x, y⁆ + ⁅x, z⁆))
have h : ⁅x, y + z⁆ = ⁅x, y⁆ + ⁅x, z⁆
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.Algebra.Lie.Quotient (goal)
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
N N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
I J : LieIdeal R L
x' : L ⧸ I
⊢ ⁅x', x'⁆ = 0
have h : ∀ (x : L), Eq (α := L ⧸ I) (Bracket.bracket (L := L ⧸ I) (Quotient.mk'' x) (Quotient.mk'' x)) 0
Tactic: induction x' using Quotient.inductionOn' with | _ x
Cleared hypotheses: x'
-- Lean 4 proof step from Mathlib.Algebra.Lie.Quotient (goal)
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
N N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
I J : LieIdeal R L
x : L
⊢ Eq (α := L ⧸ I) (mk ⁅x, x⁆) 0
have h : ⁅x, x⁆ = 0
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.Algebra.Lie.Quotient (goal)
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
N N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
I J : LieIdeal R L
x' y' z' : L ⧸ I
⊢ ⁅x', ⁅y', z'⁆⁆ = ⁅⁅x', y'⁆, z'⁆ + ⁅y', ⁅x', z'⁆⁆
have h : ∀ (x y z : L),
  Bracket.bracket (L := L ⧸ I) (Quotient.mk'' x) (Bracket.bracket (L := L ⧸ I) (Quotient.mk'' y) (Quotient.mk'' z)) =
    HAdd.hAdd (α := L ⧸ I)
      (Bracket.bracket (L := L ⧸ I) (Bracket.bracket (L := L ⧸ I) (Quotient.mk'' x) (Quotient.mk'' y))
        (Quotient.mk'' z))
      (Bracket.bracket (L := L ⧸ I) (Quotient.mk'' y)
        (Bracket.bracket (L := L ⧸ I) (Quotient.mk'' x) (Quotient.mk'' z)))
Tactic: induction x', y', z' using Quotient.inductionOn₃' with | _ x y z
Cleared hypotheses: x', y', z'
-- Lean 4 proof step from Mathlib.Algebra.Lie.Quotient (goal)
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
N N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
I J : LieIdeal R L
x y z : L
⊢ mk ⁅x, ⁅y, z⁆⁆ = HAdd.hAdd (α := L ⧸ I) (mk ⁅⁅x, y⁆, z⁆) (mk ⁅y, ⁅x, z⁆⁆)
have h : Eq (α := L ⧸ I) (mk ⁅x, ⁅y, z⁆⁆) (Submodule.Quotient.mk (⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆))
Tactic: rw [← Submodule.Quotient.mk_add (R := R) (M := L)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Quotient (goal)
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
N N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
I J : LieIdeal R L
x y z : L
⊢ mk ⁅x, ⁅y, z⁆⁆ = HAdd.hAdd (α := L ⧸ I) (mk ⁅⁅x, y⁆, z⁆) (mk ⁅y, ⁅x, z⁆⁆)
have h : Eq (α := L ⧸ I) (mk ⁅x, ⁅y, z⁆⁆) (Submodule.Quotient.mk (⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆))
Tactic: first
      | rw [is_quotient_mk]
      | rw [← mk_bracket]
      | rw [← Submodule.Quotient.mk_add (R := R) (M := L)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Quotient (goal)
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
N N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
I J : LieIdeal R L
x y z : L
⊢ Bracket.bracket (L := L ⧸ I) (Quotient.mk'' x) (Bracket.bracket (L := L ⧸ I) (Quotient.mk'' y) (Quotient.mk'' z)) =
    HAdd.hAdd (α := L ⧸ I)
      (Bracket.bracket (L := L ⧸ I) (Bracket.bracket (L := L ⧸ I) (Quotient.mk'' x) (Quotient.mk'' y))
        (Quotient.mk'' z))
      (Bracket.bracket (L := L ⧸ I) (Quotient.mk'' y)
        (Bracket.bracket (L := L ⧸ I) (Quotient.mk'' x) (Quotient.mk'' z)))
have h : Eq (α := L ⧸ I) (mk ⁅x, ⁅y, z⁆⁆) (Submodule.Quotient.mk (⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆))
Tactic: repeat'
      first
      | rw [is_quotient_mk]
      | rw [← mk_bracket]
      | rw [← Submodule.Quotient.mk_add (R := R) (M := L)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Quotient (goal)
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
N N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
I J : LieIdeal R L
x y z : L
⊢ Eq (α := L ⧸ I) (mk ⁅x, ⁅y, z⁆⁆) (Submodule.Quotient.mk (⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆))
have h : ⁅x, ⁅y, z⁆⁆ = ⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.Algebra.Lie.Quotient (goal)
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
N N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
I J : LieIdeal R L
t : R
x' y' : L ⧸ I
⊢ ⁅x', t • y'⁆ = t • ⁅x', y'⁆
have h : ∀ (x y : L),
  Bracket.bracket (L := L ⧸ I) (Quotient.mk'' x) (HSMul.hSMul (β := L ⧸ I) t (Quotient.mk'' y)) =
    HSMul.hSMul (β := L ⧸ I) t (Bracket.bracket (L := L ⧸ I) (Quotient.mk'' x) (Quotient.mk'' y))
Tactic: induction x', y' using Quotient.inductionOn₂' with | _ x y
Cleared hypotheses: x', y'
-- Lean 4 proof step from Mathlib.Algebra.Lie.Quotient (goal)
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
N N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
I J : LieIdeal R L
t : R
x y : L
⊢ Bracket.bracket (L := L ⧸ I) (Quotient.mk'' x) (HSMul.hSMul (β := L ⧸ I) t (Quotient.mk'' y)) =
    HSMul.hSMul (β := L ⧸ I) t (Bracket.bracket (L := L ⧸ I) (Quotient.mk'' x) (Quotient.mk'' y))
have h : Eq (α := L ⧸ I) (mk ⁅x, t • y⁆) (Submodule.Quotient.mk (t • ⁅x, y⁆))
Tactic: repeat'
      first
      | rw [is_quotient_mk]
      | rw [← mk_bracket]
      | rw [← Submodule.Quotient.mk_smul (R := R) (M := L)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Quotient (goal)
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
N N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
I J : LieIdeal R L
t : R
x y : L
⊢ Eq (α := L ⧸ I) (mk ⁅x, t • y⁆) (Submodule.Quotient.mk (t • ⁅x, y⁆))
have h : ⁅x, t • y⁆ = t • ⁅x, y⁆
Tactic: apply congr_arg
-- Lean 4 proof step from Mathlib.Algebra.Lie.Quotient (goal)
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
N : LieSubmodule R L M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
⊢ LieModuleHom.ker (mk' N) = N
have h : ∀ (m : M), m ∈ LieModuleHom.ker (mk' N) ↔ m ∈ N
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.Quotient (goal)
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
N N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
⊢ Eq (α := LieSubmodule R L (M ⧸ N)) (map (mk' N) N') ⊥ ↔ N' ≤ N
have rw : N' ≤ LieModuleHom.ker (mk' N) ↔ N' ≤ N
Tactic: rw [← LieModuleHom.le_ker_iff_map, mk'_ker]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Quotient (goal)
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
N N' : LieSubmodule R L M
inst_5 : LieAlgebra R L
inst_6 : LieModule R L M
rw : N' ≤ LieModuleHom.ker (mk' N) ↔ N' ≤ N
⊢ Eq (α := LieSubmodule R L (M ⧸ N)) (map (mk' N) N') ⊥ ↔ N' ≤ N
have rw₁ : N' ≤ N ↔ N' ≤ N
Tactic: rw [← LieModuleHom.le_ker_iff_map, mk'_ker]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Quotient (goal)
Goal:
R : Type u_1
L : Type u_2
L' : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
x y : L ⧸ f.ker
⊢ Eq.{u_3 + 1} (α := ↥f.range)
    (((↑f : L →ₗ[R] L').quotKerEquivRange : (a : L ⧸ (↑f : L →ₗ[R] L').ker) → ↥(↑f : L →ₗ[R] L').range) ⁅x, y⁆ :
      ↥(↑f : L →ₗ[R] L').range)
    (Bracket.bracket (L := ↥f.range)
        (((↑f : L →ₗ[R] L').quotKerEquivRange : (a : L ⧸ (↑f : L →ₗ[R] L').ker) → ↥(↑f : L →ₗ[R] L').range) x :
          ↥(↑f : L →ₗ[R] L').range)
        (((↑f : L →ₗ[R] L').quotKerEquivRange : (a : L ⧸ (↑f : L →ₗ[R] L').ker) → ↥(↑f : L →ₗ[R] L').range) y) :
      ↥f.range)
have H : ∀ (z : L),
  Eq.{u_3 + 1} (α := ↥f.range)
    (((↑f : L →ₗ[R] L').quotKerEquivRange : (a : L ⧸ (↑f : L →ₗ[R] L').ker) → ↥(↑f : L →ₗ[R] L').range)
        (Bracket.bracket (L := L ⧸ f.ker) (Submodule.Quotient.mk z) y) :
      ↥(↑f : L →ₗ[R] L').range)
    (Bracket.bracket (L := ↥f.range)
        (((↑f : L →ₗ[R] L').quotKerEquivRange : (a : L ⧸ (↑f : L →ₗ[R] L').ker) → ↥(↑f : L →ₗ[R] L').range)
            (Submodule.Quotient.mk z) :
          ↥(↑f : L →ₗ[R] L').range)
        (((↑f : L →ₗ[R] L').quotKerEquivRange : (a : L ⧸ (↑f : L →ₗ[R] L').ker) → ↥(↑f : L →ₗ[R] L').range) y) :
      ↥f.range)
Tactic: induction x using Submodule.Quotient.induction_on
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Lie.Quotient (goal)
Goal:
R : Type u_1
L : Type u_2
L' : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
y : L ⧸ f.ker
z : L
⊢ Eq.{u_3 + 1} (α := ↥f.range)
    (((↑f : L →ₗ[R] L').quotKerEquivRange : (a : L ⧸ (↑f : L →ₗ[R] L').ker) → ↥(↑f : L →ₗ[R] L').range)
        (Bracket.bracket (L := L ⧸ f.ker) (Submodule.Quotient.mk z) y) :
      ↥(↑f : L →ₗ[R] L').range)
    (Bracket.bracket (L := ↥f.range)
        (((↑f : L →ₗ[R] L').quotKerEquivRange : (a : L ⧸ (↑f : L →ₗ[R] L').ker) → ↥(↑f : L →ₗ[R] L').range)
            (Submodule.Quotient.mk z) :
          ↥(↑f : L →ₗ[R] L').range)
        (((↑f : L →ₗ[R] L').quotKerEquivRange : (a : L ⧸ (↑f : L →ₗ[R] L').ker) → ↥(↑f : L →ₗ[R] L').range) y) :
      ↥f.range)
have H : ∀ (z_1 : L),
  Eq.{u_3 + 1} (α := ↥f.range)
    (((↑f : L →ₗ[R] L').quotKerEquivRange : (a : L ⧸ (↑f : L →ₗ[R] L').ker) → ↥(↑f : L →ₗ[R] L').range)
        (Bracket.bracket (L := L ⧸ f.ker) (Submodule.Quotient.mk z) (Submodule.Quotient.mk z_1)) :
      ↥(↑f : L →ₗ[R] L').range)
    (Bracket.bracket (L := ↥f.range)
        (((↑f : L →ₗ[R] L').quotKerEquivRange : (a : L ⧸ (↑f : L →ₗ[R] L').ker) → ↥(↑f : L →ₗ[R] L').range)
            (Submodule.Quotient.mk z) :
          ↥(↑f : L →ₗ[R] L').range)
        (((↑f : L →ₗ[R] L').quotKerEquivRange : (a : L ⧸ (↑f : L →ₗ[R] L').ker) → ↥(↑f : L →ₗ[R] L').range)
          (Submodule.Quotient.mk z_1)) :
      ↥f.range)
Tactic: induction y using Submodule.Quotient.induction_on
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Lie.Quotient (goal)
Goal:
R : Type u_1
L : Type u_2
L' : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : LieRing L'
inst_4 : LieAlgebra R L'
f : L →ₗ⁅R⁆ L'
z z_1 : L
⊢ Eq.{u_3 + 1} (α := ↥f.range)
    (((↑f : L →ₗ[R] L').quotKerEquivRange : (a : L ⧸ (↑f : L →ₗ[R] L').ker) → ↥(↑f : L →ₗ[R] L').range)
        (Bracket.bracket (L := L ⧸ f.ker) (Submodule.Quotient.mk z) (Submodule.Quotient.mk z_1)) :
      ↥(↑f : L →ₗ[R] L').range)
    (Bracket.bracket (L := ↥f.range)
        (((↑f : L →ₗ[R] L').quotKerEquivRange : (a : L ⧸ (↑f : L →ₗ[R] L').ker) → ↥(↑f : L →ₗ[R] L').range)
            (Submodule.Quotient.mk z) :
          ↥(↑f : L →ₗ[R] L').range)
        (((↑f : L →ₗ[R] L').quotKerEquivRange : (a : L ⧸ (↑f : L →ₗ[R] L').ker) → ↥(↑f : L →ₗ[R] L').range)
          (Submodule.Quotient.mk z_1)) :
      ↥f.range)
have H : Eq.{u_3 + 1} (α := L')
  (↑(((↑f : L →ₗ[R] L').quotKerEquivRange : (a : L ⧸ (↑f : L →ₗ[R] L').ker) → ↥(↑f : L →ₗ[R] L').range)
        (Bracket.bracket (L := L ⧸ f.ker) (Submodule.Quotient.mk z) (Submodule.Quotient.mk z_1))) :
    L')
  (Bracket.bracket (L := L')
    (↑(((↑f : L →ₗ[R] L').quotKerEquivRange : (a : L ⧸ (↑f : L →ₗ[R] L').ker) → ↥(↑f : L →ₗ[R] L').range)
          (Submodule.Quotient.mk z)) :
      L')
    (↑(((↑f : L →ₗ[R] L').quotKerEquivRange : (a : L ⧸ (↑f : L →ₗ[R] L').ker) → ↥(↑f : L →ₗ[R] L').range)
          (Submodule.Quotient.mk z_1)) :
      L'))
Tactic: rw [← SetLike.coe_eq_coe, LieSubalgebra.coe_bracket f.range]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Rank (goal)
Goal:
K : Type u_7
L : Type u_8
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
x : L
⊢ IsRegular K x ↔ finrank.{u_7, u_8} K ↥(engel K x) = rank K L
have rw : Polynomial.natTrailingDegree.{u_7} (R := K) (LinearMap.charpoly.{u_7, u_8} (M := L) ((ad K L : (a : L) → End K L) x)) =
    rank K L ↔
  finrank.{u_7, u_8} K ↥(engel K x) = rank K L
Tactic: rw [isRegular_iff_natTrailingDegree_charpoly_eq_rank, finrank_engel]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Rank (goal)
Goal:
K : Type u_7
L : Type u_8
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
x : L
rw :
  Polynomial.natTrailingDegree.{u_7} (R := K)
        (LinearMap.charpoly.{u_7, u_8} (M := L) ((ad K L : (a : L) → End K L) x)) =
      rank K L ↔
    finrank.{u_7, u_8} K ↥(engel K x) = rank K L
⊢ IsRegular K x ↔ finrank.{u_7, u_8} K ↥(engel K x) = rank K L
have rw₁ : Polynomial.natTrailingDegree.{u_7} (R := K) (LinearMap.charpoly.{u_7, u_8} (M := L) ((ad K L : (a : L) → End K L) x)) =
    rank K L ↔
  Polynomial.natTrailingDegree.{u_7} (R := K)
      (LinearMap.charpoly.{u_7, u_8} (M := L) ((ad K L : (a : L) → End K L) x)) =
    rank K L
Tactic: rw [isRegular_iff_natTrailingDegree_charpoly_eq_rank, finrank_engel]
-- Lean 4 proof step from Mathlib.Algebra.Lie.SemiDirect (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
x x_1 x_2 : K ⋊⁅ψ⁆ L
⊢ ⁅x + x_1, x_2⁆ = ⁅x, x_2⁆ + ⁅x_1, x_2⁆
have simp : ⁅x.left, x_2.left⁆ + ⁅x_1.left, x_2.left⁆ +
      HAdd.hAdd (α := K) (β := K)
        ((((ψ : (a : L) → LieDerivation R K K) x.right : LieDerivation R K K) : (a : K) → K) x_2.left : K)
        ((((ψ : (a : L) → LieDerivation R K K) x_1.right : LieDerivation R K K) : (a : K) → K) x_2.left : K) -
    HAdd.hAdd (α := K) (β := K)
      ((((ψ : (a : L) → LieDerivation R K K) x_2.right : LieDerivation R K K) : (a : K) → K) x.left : K)
      ((((ψ : (a : L) → LieDerivation R K K) x_2.right : LieDerivation R K K) : (a : K) → K) x_1.left : K) =
  HSub.hSub (β := K)
      (HAdd.hAdd (β := K) ⁅x.left, x_2.left⁆
        ((((ψ : (a : L) → LieDerivation R K K) x.right : LieDerivation R K K) : (a : K) → K) x_2.left : K))
      ((((ψ : (a : L) → LieDerivation R K K) x_2.right : LieDerivation R K K) : (a : K) → K) x.left : K) +
    HSub.hSub (β := K)
      (HAdd.hAdd (β := K) ⁅x_1.left, x_2.left⁆
        ((((ψ : (a : L) → LieDerivation R K K) x_1.right : LieDerivation R K K) : (a : K) → K) x_2.left : K))
      ((((ψ : (a : L) → LieDerivation R K K) x_2.right : LieDerivation R K K) : (a : K) → K) x_1.left : K)
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Lie.SemiDirect (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
x x_1 x_2 : K ⋊⁅ψ⁆ L
⊢ ⁅x, x_1 + x_2⁆ = ⁅x, x_1⁆ + ⁅x, x_2⁆
have simp : ⁅x.left, x_1.left⁆ + ⁅x.left, x_2.left⁆ +
      HAdd.hAdd (α := K) (β := K)
        ((((ψ : (a : L) → LieDerivation R K K) x.right : LieDerivation R K K) : (a : K) → K) x_1.left : K)
        ((((ψ : (a : L) → LieDerivation R K K) x.right : LieDerivation R K K) : (a : K) → K) x_2.left : K) -
    HAdd.hAdd (α := K) (β := K)
      ((((ψ : (a : L) → LieDerivation R K K) x_1.right : LieDerivation R K K) : (a : K) → K) x.left : K)
      ((((ψ : (a : L) → LieDerivation R K K) x_2.right : LieDerivation R K K) : (a : K) → K) x.left : K) =
  HSub.hSub (β := K)
      (HAdd.hAdd (β := K) ⁅x.left, x_1.left⁆
        ((((ψ : (a : L) → LieDerivation R K K) x.right : LieDerivation R K K) : (a : K) → K) x_1.left : K))
      ((((ψ : (a : L) → LieDerivation R K K) x_1.right : LieDerivation R K K) : (a : K) → K) x.left : K) +
    HSub.hSub (β := K)
      (HAdd.hAdd (β := K) ⁅x.left, x_2.left⁆
        ((((ψ : (a : L) → LieDerivation R K K) x.right : LieDerivation R K K) : (a : K) → K) x_2.left : K))
      ((((ψ : (a : L) → LieDerivation R K K) x_2.right : LieDerivation R K K) : (a : K) → K) x.left : K)
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.Lie.SemiDirect (goal)
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
⊢ (inl ψ).range = LieIdeal.toLieSubalgebra R (K ⋊⁅ψ⁆ L) (projr ψ).ker
have h : ∀ (x : K) (y : L),
  { left := x, right := y } ∈ (inl ψ).range ↔
    { left := x, right := y } ∈ LieIdeal.toLieSubalgebra R (K ⋊⁅ψ⁆ L) (projr ψ).ker
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.Algebra.Lie.Semisimple.Lemmas (hypothesis)
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
⊢ HasCentralRadical k L ∧
    ∀ (x : L),
      Membership.mem (γ := LieIdeal k L) (center k L) x ↔
        Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
          (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)
have _i : Nontrivial M
Tactic: have _i := nontrivial_of_isIrreducible k L M