awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Quotient
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 : L ⧸ I
x₁ x₂ y₁ y₂ : L
h₁ : x₁ - y₁ ∈ (↑I : Submodule R L)
h₂ : x₂ - y₂ ∈ (↑I : Submodule R L)
h : ⁅x₁, x₂⁆ - ⁅y₁, y₂⁆ = ⁅x₁, x₂ - y₂⁆ + ⁅x₁ - y₁, y₂⁆
⊢ ⁅x₁, x₂ - y₂⁆ ∈ (↑I : Submodule R L)

Tactic:
apply lie_mem_right R L I x₁ (x₂ - y₂) h₂

Premises used: HSub.hSub, lie_mem_right
-- Module: Mathlib.Algebra.Lie.Quotient
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 : L ⧸ I
x₁ x₂ y₁ y₂ : L
h₁ : x₁ - y₁ ∈ (↑I : Submodule R L)
h₂ : x₂ - y₂ ∈ (↑I : Submodule R L)
h : ⁅x₁, x₂⁆ - ⁅y₁, y₂⁆ = ⁅x₁, x₂ - y₂⁆ + ⁅x₁ - y₁, y₂⁆
⊢ ⁅x₁ - y₁, y₂⁆ ∈ (↑I : Submodule R L)

Tactic:
apply lie_mem_left R L I (x₁ - y₁) y₂ h₁

Premises used: HSub.hSub, lie_mem_left
-- Module: Mathlib.Algebra.Lie.Quotient
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
I : LieIdeal R L
x y : L
⊢ Eq (α := L ⧸ I) (mk ⁅x, y⁆) (Bracket.bracket (L := L ⧸ I) (mk x) (mk y))

Tactic:
rfl

Premises used: Submodule.Quotient.mk, rfl, Quotient.liftOn₂'
-- Module: Mathlib.Algebra.Lie.Quotient
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
h :
  ∀ (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))
⊢ ⁅x' + y', z'⁆ = ⁅x', z'⁆ + ⁅y', z'⁆

Tactic:
induction x', y', z' using Quotient.inductionOn₃' with | _ x y z
-- Module: Mathlib.Algebra.Lie.Quotient
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
h : Bracket.bracket (L := L ⧸ I) (Submodule.Quotient.mk (x + y)) (mk z) = HAdd.hAdd (α := L ⧸ I) (mk ⁅x, z⁆) (mk ⁅y, z⁆)
⊢ ⁅HAdd.hAdd (α := L ⧸ I) (mk x) (mk y), mk z⁆ = HAdd.hAdd (α := L ⧸ I) (mk ⁅x, z⁆) (mk ⁅y, z⁆)

Tactic:
rw [← Submodule.Quotient.mk_add (R := R) (M := L)]

Premises used: Submodule.Quotient.mk_add
-- Module: Mathlib.Algebra.Lie.Quotient
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
h : Bracket.bracket (L := L ⧸ I) (Submodule.Quotient.mk (x + y)) (mk z) = HAdd.hAdd (α := L ⧸ I) (mk ⁅x, z⁆) (mk ⁅y, z⁆)
⊢ ⁅HAdd.hAdd (α := L ⧸ I) (mk x) (mk y), mk z⁆ = HAdd.hAdd (α := L ⧸ I) (mk ⁅x, z⁆) (mk ⁅y, z⁆)

Tactic:
first
      | rw [is_quotient_mk]
      | rw [← mk_bracket]
      | rw [← Submodule.Quotient.mk_add (R := R) (M := L)]

Premises used: Submodule.Quotient.mk_add, LieSubmodule.Quotient.mk_bracket, LieSubmodule.Quotient.is_quotient_mk
-- Module: Mathlib.Algebra.Lie.Quotient
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
h : Eq (α := L ⧸ I) (mk ⁅x + y, z⁆) (Submodule.Quotient.mk (⁅x, z⁆ + ⁅y, z⁆))
⊢ mk ⁅x + y, z⁆ = HAdd.hAdd (α := L ⧸ I) (mk ⁅x, z⁆) (mk ⁅y, z⁆)

Tactic:
rw [← Submodule.Quotient.mk_add (R := R) (M := L)]

Premises used: Submodule.Quotient.mk_add
-- Module: Mathlib.Algebra.Lie.Quotient
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
h : Eq (α := L ⧸ I) (mk ⁅x + y, z⁆) (Submodule.Quotient.mk (⁅x, z⁆ + ⁅y, z⁆))
⊢ mk ⁅x + y, z⁆ = HAdd.hAdd (α := L ⧸ I) (mk ⁅x, z⁆) (mk ⁅y, z⁆)

Tactic:
first
      | rw [is_quotient_mk]
      | rw [← mk_bracket]
      | rw [← Submodule.Quotient.mk_add (R := R) (M := L)]

Premises used: Submodule.Quotient.mk_add, LieSubmodule.Quotient.mk_bracket, LieSubmodule.Quotient.is_quotient_mk
-- Module: Mathlib.Algebra.Lie.Quotient
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
h : Eq (α := L ⧸ I) (mk ⁅x + y, z⁆) (Submodule.Quotient.mk (⁅x, z⁆ + ⁅y, z⁆))
⊢ ⁅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))

Tactic:
repeat'
      first
      | rw [is_quotient_mk]
      | rw [← mk_bracket]
      | rw [← Submodule.Quotient.mk_add (R := R) (M := L)]

Premises used: Submodule.Quotient.mk_add, LieSubmodule.Quotient.mk_bracket, LieSubmodule.Quotient.is_quotient_mk
-- Module: Mathlib.Algebra.Lie.Quotient
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
h : ⁅x + y, z⁆ = ⁅x, z⁆ + ⁅y, z⁆
⊢ Eq (α := L ⧸ I) (mk ⁅x + y, z⁆) (Submodule.Quotient.mk (⁅x, z⁆ + ⁅y, z⁆))

Tactic:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.Algebra.Lie.Quotient
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
⊢ ⁅x + y, z⁆ = ⁅x, z⁆ + ⁅y, z⁆

Tactic:
apply add_lie

Premises used: add_lie
-- Module: Mathlib.Algebra.Lie.Quotient
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
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))
⊢ ⁅x', y' + z'⁆ = ⁅x', y'⁆ + ⁅x', z'⁆

Tactic:
induction x', y', z' using Quotient.inductionOn₃' with | _ x y z
-- Module: Mathlib.Algebra.Lie.Quotient
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
h : Bracket.bracket (L := L ⧸ I) (mk x) (Submodule.Quotient.mk (y + z)) = HAdd.hAdd (α := L ⧸ I) (mk ⁅x, y⁆) (mk ⁅x, z⁆)
⊢ 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⁆)

Tactic:
rw [← Submodule.Quotient.mk_add (R := R) (M := L)]

Premises used: Submodule.Quotient.mk_add
-- Module: Mathlib.Algebra.Lie.Quotient
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
h : Bracket.bracket (L := L ⧸ I) (mk x) (Submodule.Quotient.mk (y + z)) = HAdd.hAdd (α := L ⧸ I) (mk ⁅x, y⁆) (mk ⁅x, z⁆)
⊢ 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⁆)

Tactic:
first
      | rw [is_quotient_mk]
      | rw [← mk_bracket]
      | rw [← Submodule.Quotient.mk_add (R := R) (M := L)]

Premises used: Submodule.Quotient.mk_add, LieSubmodule.Quotient.mk_bracket, LieSubmodule.Quotient.is_quotient_mk
-- Module: Mathlib.Algebra.Lie.Quotient
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
h : Eq (α := L ⧸ I) (mk ⁅x, y + z⁆) (Submodule.Quotient.mk (⁅x, y⁆ + ⁅x, z⁆))
⊢ mk ⁅x, y + z⁆ = HAdd.hAdd (α := L ⧸ I) (mk ⁅x, y⁆) (mk ⁅x, z⁆)

Tactic:
rw [← Submodule.Quotient.mk_add (R := R) (M := L)]

Premises used: Submodule.Quotient.mk_add
-- Module: Mathlib.Algebra.Lie.Quotient
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
h : Eq (α := L ⧸ I) (mk ⁅x, y + z⁆) (Submodule.Quotient.mk (⁅x, y⁆ + ⁅x, z⁆))
⊢ mk ⁅x, 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)]

Premises used: Submodule.Quotient.mk_add, LieSubmodule.Quotient.mk_bracket, LieSubmodule.Quotient.is_quotient_mk
-- Module: Mathlib.Algebra.Lie.Quotient
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
h : Eq (α := L ⧸ I) (mk ⁅x, y + z⁆) (Submodule.Quotient.mk (⁅x, y⁆ + ⁅x, z⁆))
⊢ 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:
repeat'
      first
      | rw [is_quotient_mk]
      | rw [← mk_bracket]
      | rw [← Submodule.Quotient.mk_add (R := R) (M := L)]

Premises used: Submodule.Quotient.mk_add, LieSubmodule.Quotient.mk_bracket, LieSubmodule.Quotient.is_quotient_mk
-- Module: Mathlib.Algebra.Lie.Quotient
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
h : ⁅x, y + z⁆ = ⁅x, y⁆ + ⁅x, z⁆
⊢ Eq (α := L ⧸ I) (mk ⁅x, y + z⁆) (Submodule.Quotient.mk (⁅x, y⁆ + ⁅x, z⁆))

Tactic:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.Algebra.Lie.Quotient
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
⊢ ⁅x, y + z⁆ = ⁅x, y⁆ + ⁅x, z⁆

Tactic:
apply lie_add

Premises used: lie_add
-- Module: Mathlib.Algebra.Lie.Quotient
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
h : ∀ (x : L), Eq (α := L ⧸ I) (Bracket.bracket (L := L ⧸ I) (Quotient.mk'' x) (Quotient.mk'' x)) 0
⊢ ⁅x', x'⁆ = 0

Tactic:
induction x' using Quotient.inductionOn' with | _ x
-- Module: Mathlib.Algebra.Lie.Quotient
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
h : ⁅x, x⁆ = 0
⊢ Eq (α := L ⧸ I) (mk ⁅x, x⁆) 0

Tactic:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.Algebra.Lie.Quotient
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
⊢ ⁅x, x⁆ = 0

Tactic:
apply lie_self

Premises used: lie_self
-- Module: Mathlib.Algebra.Lie.Quotient
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
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)))
⊢ ⁅x', ⁅y', z'⁆⁆ = ⁅⁅x', y'⁆, z'⁆ + ⁅y', ⁅x', z'⁆⁆

Tactic:
induction x', y', z' using Quotient.inductionOn₃' with | _ x y z
-- Module: Mathlib.Algebra.Lie.Quotient
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
h : Eq (α := L ⧸ I) (mk ⁅x, ⁅y, z⁆⁆) (Submodule.Quotient.mk (⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆))
⊢ mk ⁅x, ⁅y, z⁆⁆ = HAdd.hAdd (α := L ⧸ I) (mk ⁅⁅x, y⁆, z⁆) (mk ⁅y, ⁅x, z⁆⁆)

Tactic:
rw [← Submodule.Quotient.mk_add (R := R) (M := L)]

Premises used: Submodule.Quotient.mk_add
-- Module: Mathlib.Algebra.Lie.Quotient
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
h : Eq (α := L ⧸ I) (mk ⁅x, ⁅y, z⁆⁆) (Submodule.Quotient.mk (⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆))
⊢ mk ⁅x, ⁅y, z⁆⁆ = HAdd.hAdd (α := L ⧸ I) (mk ⁅⁅x, y⁆, z⁆) (mk ⁅y, ⁅x, z⁆⁆)

Tactic:
first
      | rw [is_quotient_mk]
      | rw [← mk_bracket]
      | rw [← Submodule.Quotient.mk_add (R := R) (M := L)]

Premises used: Submodule.Quotient.mk_add, LieSubmodule.Quotient.mk_bracket, LieSubmodule.Quotient.is_quotient_mk
-- Module: Mathlib.Algebra.Lie.Quotient
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
h : Eq (α := L ⧸ I) (mk ⁅x, ⁅y, z⁆⁆) (Submodule.Quotient.mk (⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆))
⊢ 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:
repeat'
      first
      | rw [is_quotient_mk]
      | rw [← mk_bracket]
      | rw [← Submodule.Quotient.mk_add (R := R) (M := L)]

Premises used: Submodule.Quotient.mk_add, LieSubmodule.Quotient.mk_bracket, LieSubmodule.Quotient.is_quotient_mk
-- Module: Mathlib.Algebra.Lie.Quotient
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
h : ⁅x, ⁅y, z⁆⁆ = ⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆
⊢ Eq (α := L ⧸ I) (mk ⁅x, ⁅y, z⁆⁆) (Submodule.Quotient.mk (⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆))

Tactic:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.Algebra.Lie.Quotient
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
⊢ ⁅x, ⁅y, z⁆⁆ = ⁅⁅x, y⁆, z⁆ + ⁅y, ⁅x, z⁆⁆

Tactic:
apply leibniz_lie

Premises used: leibniz_lie
-- Module: Mathlib.Algebra.Lie.Quotient
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
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))
⊢ ⁅x', t • y'⁆ = t • ⁅x', y'⁆

Tactic:
induction x', y' using Quotient.inductionOn₂' with | _ x y
-- Module: Mathlib.Algebra.Lie.Quotient
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
h : Eq (α := L ⧸ I) (mk ⁅x, t • y⁆) (Submodule.Quotient.mk (t • ⁅x, y⁆))
⊢ 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:
repeat'
      first
      | rw [is_quotient_mk]
      | rw [← mk_bracket]
      | rw [← Submodule.Quotient.mk_smul (R := R) (M := L)]

Premises used: Submodule.Quotient.mk_smul, LieSubmodule.Quotient.mk_bracket, LieSubmodule.Quotient.is_quotient_mk
-- Module: Mathlib.Algebra.Lie.Quotient
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
h : ⁅x, t • y⁆ = t • ⁅x, y⁆
⊢ Eq (α := L ⧸ I) (mk ⁅x, t • y⁆) (Submodule.Quotient.mk (t • ⁅x, y⁆))

Tactic:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.Algebra.Lie.Quotient
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
⊢ ⁅x, t • y⁆ = t • ⁅x, y⁆

Tactic:
apply lie_smul

Premises used: lie_smul
-- Module: Mathlib.Algebra.Lie.Quotient
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
⊢ Function.Surjective (α := M) (β := M ⧸ N) (⇑(mk' N) : (a : M) → M ⧸ N)

Tactic:
Quot.mk_surjective

Premises used: Submodule.Quotient.mk, Quotient, Quot.mk_surjective
-- Module: Mathlib.Algebra.Lie.Quotient
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
⊢ Eq (α := LieSubmodule R L (M ⧸ N)) (LieModuleHom.range (mk' N)) ⊤

Tactic:
simp [LieModuleHom.range_eq_top]

Premises used: LieModuleHom.range_eq_top
-- Module: Mathlib.Algebra.Lie.Quotient
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
inst_7 : IsNoetherian R M
⊢ IsNoetherian.{u, w} R (M ⧸ N)

Tactic:
inferInstanceAs (IsNoetherian R (M ⧸ (N : Submodule R M)))

Premises used: _private.0.LieSubmodule.Quotient.isNoetherian._proof_1
-- Module: Mathlib.Algebra.Lie.Quotient
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
m : M
⊢ Eq (α := M ⧸ N) ((mk' N : (a : M) → M ⧸ N) m : M ⧸ N) (0 : M ⧸ N) ↔ m ∈ N

Tactic:
Submodule.Quotient.mk_eq_zero N.toSubmodule

Premises used: Set.Mem, Submodule.Quotient.mk, LieSubmodule.toSubmodule, Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.Algebra.Lie.Quotient
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
h : ∀ (m : M), m ∈ LieModuleHom.ker (mk' N) ↔ m ∈ N
⊢ LieModuleHom.ker (mk' N) = N

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Quotient
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
m : M
⊢ m ∈ LieModuleHom.ker (mk' N) ↔ m ∈ N

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Quotient
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
rw₁ rw₂ : N' ≤ N ↔ N' ≤ N
⊢ Eq (α := LieSubmodule R L (M ⧸ N)) (map (mk' N) N') ⊥ ↔ N' ≤ N

Tactic:
rw [← LieModuleHom.le_ker_iff_map, mk'_ker]

Premises used: LieSubmodule.Quotient.mk'_ker, LieModuleHom.le_ker_iff_map
-- Module: Mathlib.Algebra.Lie.Quotient
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
f g : M ⧸ N →ₗ⁅R,L⁆ M
h : f.comp (mk' N) = g.comp (mk' N)
⊢ f = g

Tactic:
LieModuleHom.ext fun x => Quotient.inductionOn' x <| LieModuleHom.congr_fun h

Premises used: LieModuleHom.ext, Quotient.inductionOn'
-- Module: Mathlib.Algebra.Lie.Quotient
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
x : L
⊢ (LieModule.toEnd R L (M ⧸ N) : (a : L) → Module.End R (M ⧸ N)) x ∘ₗ (↑(mk' N) : M →ₗ[R] M ⧸ N) =
    (↑(mk' N) : M →ₗ[R] M ⧸ N) ∘ₗ
      ((LieModule.toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, Quotient, rfl
-- Module: Mathlib.Algebra.Lie.Quotient
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
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)
⊢ 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)

Tactic:
induction x using Submodule.Quotient.induction_on