awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (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'
e : L ≃ₗ⁅R⁆ L'
x : L
y' : L'
⊢ Eq (α := L')
    ((((e.toLinearEquiv.conj : (a : Module.End R L) → Module.End R L') ((ad R L : (a : L) → Module.End R L) x) :
            Module.End R L') :
          (a : L') → L')
        y' :
      L')
    ((((ad R L' : (a : L') → Module.End R L') ((e : (a : L) → L') x : L') : Module.End R L') : (a : L') → L') y' : L')
have h : Eq.{u_3 + 1} (α := L')
  ((e.toLinearEquiv : (a : L) → L')
      ((((ad R L : (a : L) → Module.End R L) x : Module.End R L) : (a : L) → L)
          ((e.toLinearEquiv.symm : (a : L') → L) y' : L) :
        L) :
    L')
  ((((ad R L' : (a : L') → Module.End R L') ((e : (a : L) → L') x : L') : Module.End R L') : (a : L') → L') y' : L')
Tactic: rw [LinearEquiv.conj_apply_apply, ad_apply, ad_apply, coe_toLinearEquiv, map_lie,
    ← coe_toLinearEquiv, LinearEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (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'
e : L ≃ₗ⁅R⁆ L'
x : L
y' : L'
h :
  Eq.{u_3 + 1} (α := L')
    ((e.toLinearEquiv : (a : L) → L')
        ((((ad R L : (a : L) → Module.End R L) x : Module.End R L) : (a : L) → L)
            ((e.toLinearEquiv.symm : (a : L') → L) y' : L) :
          L) :
      L')
    ((((ad R L' : (a : L') → Module.End R L') ((e : (a : L) → L') x : L') : Module.End R L') : (a : L') → L') y' : L')
⊢ Eq (α := L')
    ((((e.toLinearEquiv.conj : (a : Module.End R L) → Module.End R L') ((ad R L : (a : L) → Module.End R L) x) :
            Module.End R L') :
          (a : L') → L')
        y' :
      L')
    ((((ad R L' : (a : L') → Module.End R L') ((e : (a : L) → L') x : L') : Module.End R L') : (a : L') → L') y' : L')
have h₁ : Eq.{u_3 + 1} (α := L') ((e.toLinearEquiv : (a : L) → L') (⁅x, (e.toLinearEquiv.symm : (a : L') → L) y'⁆ : L) : L')
  ((((ad R L' : (a : L') → Module.End R L') ((e : (a : L) → L') x : L') : Module.End R L') : (a : L') → L') y' : L')
Tactic: rw [LinearEquiv.conj_apply_apply, ad_apply, ad_apply, coe_toLinearEquiv, map_lie,
    ← coe_toLinearEquiv, LinearEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (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'
e : L ≃ₗ⁅R⁆ L'
x : L
y' : L'
h :
  Eq.{u_3 + 1} (α := L')
    ((e.toLinearEquiv : (a : L) → L')
        ((((ad R L : (a : L) → Module.End R L) x : Module.End R L) : (a : L) → L)
            ((e.toLinearEquiv.symm : (a : L') → L) y' : L) :
          L) :
      L')
    ((((ad R L' : (a : L') → Module.End R L') ((e : (a : L) → L') x : L') : Module.End R L') : (a : L') → L') y' : L')
h₁ :
  Eq.{u_3 + 1} (α := L') ((e.toLinearEquiv : (a : L) → L') (⁅x, (e.toLinearEquiv.symm : (a : L') → L) y'⁆ : L) : L')
    ((((ad R L' : (a : L') → Module.End R L') ((e : (a : L) → L') x : L') : Module.End R L') : (a : L') → L') y' : L')
⊢ Eq (α := L')
    ((((e.toLinearEquiv.conj : (a : Module.End R L) → Module.End R L') ((ad R L : (a : L) → Module.End R L) x) :
            Module.End R L') :
          (a : L') → L')
        y' :
      L')
    ((((ad R L' : (a : L') → Module.End R L') ((e : (a : L) → L') x : L') : Module.End R L') : (a : L') → L') y' : L')
have h₂ : (e.toLinearEquiv : (a : L) → L') (⁅x, (e.toLinearEquiv.symm : (a : L') → L) y'⁆ : L) =
  Bracket.bracket (L := L') ((e : (a : L) → L') x : L') y'
Tactic: rw [LinearEquiv.conj_apply_apply, ad_apply, ad_apply, coe_toLinearEquiv, map_lie,
    ← coe_toLinearEquiv, LinearEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (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'
e : L ≃ₗ⁅R⁆ L'
x : L
y' : L'
h :
  Eq.{u_3 + 1} (α := L')
    ((e.toLinearEquiv : (a : L) → L')
        ((((ad R L : (a : L) → Module.End R L) x : Module.End R L) : (a : L) → L)
            ((e.toLinearEquiv.symm : (a : L') → L) y' : L) :
          L) :
      L')
    ((((ad R L' : (a : L') → Module.End R L') ((e : (a : L) → L') x : L') : Module.End R L') : (a : L') → L') y' : L')
h₁ :
  Eq.{u_3 + 1} (α := L') ((e.toLinearEquiv : (a : L) → L') (⁅x, (e.toLinearEquiv.symm : (a : L') → L) y'⁆ : L) : L')
    ((((ad R L' : (a : L') → Module.End R L') ((e : (a : L) → L') x : L') : Module.End R L') : (a : L') → L') y' : L')
h₂ :
  (e.toLinearEquiv : (a : L) → L') (⁅x, (e.toLinearEquiv.symm : (a : L') → L) y'⁆ : L) =
    Bracket.bracket (L := L') ((e : (a : L) → L') x : L') y'
⊢ Eq (α := L')
    ((((e.toLinearEquiv.conj : (a : Module.End R L) → Module.End R L') ((ad R L : (a : L) → Module.End R L) x) :
            Module.End R L') :
          (a : L') → L')
        y' :
      L')
    ((((ad R L' : (a : L') → Module.End R L') ((e : (a : L) → L') x : L') : Module.End R L') : (a : L') → L') y' : L')
have h₃ : (e : (a : L) → L') (⁅x, (e.toLinearEquiv.symm : (a : L') → L) y'⁆ : L) =
  Bracket.bracket (L := L') ((e : (a : L) → L') x : L') y'
Tactic: rw [LinearEquiv.conj_apply_apply, ad_apply, ad_apply, coe_toLinearEquiv, map_lie,
    ← coe_toLinearEquiv, LinearEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (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'
e : L ≃ₗ⁅R⁆ L'
x : L
y' : L'
h :
  Eq.{u_3 + 1} (α := L')
    ((e.toLinearEquiv : (a : L) → L')
        ((((ad R L : (a : L) → Module.End R L) x : Module.End R L) : (a : L) → L)
            ((e.toLinearEquiv.symm : (a : L') → L) y' : L) :
          L) :
      L')
    ((((ad R L' : (a : L') → Module.End R L') ((e : (a : L) → L') x : L') : Module.End R L') : (a : L') → L') y' : L')
h₁ :
  Eq.{u_3 + 1} (α := L') ((e.toLinearEquiv : (a : L) → L') (⁅x, (e.toLinearEquiv.symm : (a : L') → L) y'⁆ : L) : L')
    ((((ad R L' : (a : L') → Module.End R L') ((e : (a : L) → L') x : L') : Module.End R L') : (a : L') → L') y' : L')
h₂ :
  (e.toLinearEquiv : (a : L) → L') (⁅x, (e.toLinearEquiv.symm : (a : L') → L) y'⁆ : L) =
    Bracket.bracket (L := L') ((e : (a : L) → L') x : L') y'
h₃ :
  (e : (a : L) → L') (⁅x, (e.toLinearEquiv.symm : (a : L') → L) y'⁆ : L) =
    Bracket.bracket (L := L') ((e : (a : L) → L') x : L') y'
⊢ Eq (α := L')
    ((((e.toLinearEquiv.conj : (a : Module.End R L) → Module.End R L') ((ad R L : (a : L) → Module.End R L) x) :
            Module.End R L') :
          (a : L') → L')
        y' :
      L')
    ((((ad R L' : (a : L') → Module.End R L') ((e : (a : L) → L') x : L') : Module.End R L') : (a : L') → L') y' : L')
have h₄ : Bracket.bracket (L := L') ((e : (a : L) → L') x : L')
    ((e : (a : L) → L') ((e.toLinearEquiv.symm : (a : L') → L) y' : L)) =
  Bracket.bracket (L := L') ((e : (a : L) → L') x : L') y'
Tactic: rw [LinearEquiv.conj_apply_apply, ad_apply, ad_apply, coe_toLinearEquiv, map_lie,
    ← coe_toLinearEquiv, LinearEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (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'
e : L ≃ₗ⁅R⁆ L'
x : L
y' : L'
h :
  Eq.{u_3 + 1} (α := L')
    ((e.toLinearEquiv : (a : L) → L')
        ((((ad R L : (a : L) → Module.End R L) x : Module.End R L) : (a : L) → L)
            ((e.toLinearEquiv.symm : (a : L') → L) y' : L) :
          L) :
      L')
    ((((ad R L' : (a : L') → Module.End R L') ((e : (a : L) → L') x : L') : Module.End R L') : (a : L') → L') y' : L')
h₁ :
  Eq.{u_3 + 1} (α := L') ((e.toLinearEquiv : (a : L) → L') (⁅x, (e.toLinearEquiv.symm : (a : L') → L) y'⁆ : L) : L')
    ((((ad R L' : (a : L') → Module.End R L') ((e : (a : L) → L') x : L') : Module.End R L') : (a : L') → L') y' : L')
h₂ :
  (e.toLinearEquiv : (a : L) → L') (⁅x, (e.toLinearEquiv.symm : (a : L') → L) y'⁆ : L) =
    Bracket.bracket (L := L') ((e : (a : L) → L') x : L') y'
h₃ :
  (e : (a : L) → L') (⁅x, (e.toLinearEquiv.symm : (a : L') → L) y'⁆ : L) =
    Bracket.bracket (L := L') ((e : (a : L) → L') x : L') y'
h₄ :
  Bracket.bracket (L := L') ((e : (a : L) → L') x : L')
      ((e : (a : L) → L') ((e.toLinearEquiv.symm : (a : L') → L) y' : L)) =
    Bracket.bracket (L := L') ((e : (a : L) → L') x : L') y'
⊢ Eq (α := L')
    ((((e.toLinearEquiv.conj : (a : Module.End R L) → Module.End R L') ((ad R L : (a : L) → Module.End R L) x) :
            Module.End R L') :
          (a : L') → L')
        y' :
      L')
    ((((ad R L' : (a : L') → Module.End R L') ((e : (a : L) → L') x : L') : Module.End R L') : (a : L') → L') y' : L')
have h₅ : Bracket.bracket (L := L') ((e.toLinearEquiv : (a : L) → L') x : L')
    ((e.toLinearEquiv : (a : L) → L') ((e.toLinearEquiv.symm : (a : L') → L) y' : L)) =
  Bracket.bracket (L := L') ((e.toLinearEquiv : (a : L) → L') x : L') y'
Tactic: rw [LinearEquiv.conj_apply_apply, ad_apply, ad_apply, coe_toLinearEquiv, map_lie,
    ← coe_toLinearEquiv, LinearEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.OfAssociative (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'
e : L ≃ₗ⁅R⁆ L'
x : L
y' : L'
h :
  Eq.{u_3 + 1} (α := L')
    ((e.toLinearEquiv : (a : L) → L')
        ((((ad R L : (a : L) → Module.End R L) x : Module.End R L) : (a : L) → L)
            ((e.toLinearEquiv.symm : (a : L') → L) y' : L) :
          L) :
      L')
    ((((ad R L' : (a : L') → Module.End R L') ((e : (a : L) → L') x : L') : Module.End R L') : (a : L') → L') y' : L')
h₁ :
  Eq.{u_3 + 1} (α := L') ((e.toLinearEquiv : (a : L) → L') (⁅x, (e.toLinearEquiv.symm : (a : L') → L) y'⁆ : L) : L')
    ((((ad R L' : (a : L') → Module.End R L') ((e : (a : L) → L') x : L') : Module.End R L') : (a : L') → L') y' : L')
h₂ :
  (e.toLinearEquiv : (a : L) → L') (⁅x, (e.toLinearEquiv.symm : (a : L') → L) y'⁆ : L) =
    Bracket.bracket (L := L') ((e : (a : L) → L') x : L') y'
h₃ :
  (e : (a : L) → L') (⁅x, (e.toLinearEquiv.symm : (a : L') → L) y'⁆ : L) =
    Bracket.bracket (L := L') ((e : (a : L) → L') x : L') y'
h₄ :
  Bracket.bracket (L := L') ((e : (a : L) → L') x : L')
      ((e : (a : L) → L') ((e.toLinearEquiv.symm : (a : L') → L) y' : L)) =
    Bracket.bracket (L := L') ((e : (a : L) → L') x : L') y'
h₅ :
  Bracket.bracket (L := L') ((e.toLinearEquiv : (a : L) → L') x : L')
      ((e.toLinearEquiv : (a : L) → L') ((e.toLinearEquiv.symm : (a : L') → L) y' : L)) =
    Bracket.bracket (L := L') ((e.toLinearEquiv : (a : L) → L') x : L') y'
⊢ Eq (α := L')
    ((((e.toLinearEquiv.conj : (a : Module.End R L) → Module.End R L') ((ad R L : (a : L) → Module.End R L) x) :
            Module.End R L') :
          (a : L') → L')
        y' :
      L')
    ((((ad R L' : (a : L') → Module.End R L') ((e : (a : L) → L') x : L') : Module.End R L') : (a : L') → L') y' : L')
have h₆ : Bracket.bracket (L := L') ((e.toLinearEquiv : (a : L) → L') x : L') y' =
  Bracket.bracket (L := L') ((e.toLinearEquiv : (a : L) → L') x : L') y'
Tactic: rw [LinearEquiv.conj_apply_apply, ad_apply, ad_apply, coe_toLinearEquiv, map_lie,
    ← coe_toLinearEquiv, LinearEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Prod (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₂
⊢ Eq (α := LieSubalgebra R (L₁ × L₂)) (range (inl R L₁ L₂)) (LieIdeal.toLieSubalgebra R (L₁ × L₂) (ker (snd R L₁ L₂)))
have rw : Eq (α := Submodule R (L₁ × L₂)) (LinearMap.range (↑(inl R L₁ L₂) : L₁ →ₗ[R] L₁ × L₂))
  (LinearMap.ker (↑(snd R L₁ L₂) : L₁ × L₂ →ₗ[R] L₂))
Tactic: rw [← LieSubalgebra.toSubmodule_inj, range_toSubmodule, LieIdeal.toLieSubalgebra_toSubmodule,
   ker_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Prod (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₂
⊢ Eq (α := LieSubalgebra R (L₁ × L₂)) (range (inr R L₁ L₂)) (LieIdeal.toLieSubalgebra R (L₁ × L₂) (ker (fst R L₁ L₂)))
have rw : Eq (α := Submodule R (L₁ × L₂)) (LinearMap.range (↑(inr R L₁ L₂) : L₂ →ₗ[R] L₁ × L₂))
  (LinearMap.ker (↑(fst R L₁ L₂) : L₁ × L₂ →ₗ[R] L₁))
Tactic: rw [← LieSubalgebra.toSubmodule_inj, range_toSubmodule, LieIdeal.toLieSubalgebra_toSubmodule,
   ker_toSubmodule]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Prod (goal)
Goal:
R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieAlgebra R L₁
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
inst_5 : LieRing L
inst_6 : LieAlgebra R L
f g : L₁ × L₂ →ₗ⁅R⁆ L
⊢ f = g ↔ f.comp (inl R L₁ L₂) = g.comp (inl R L₁ L₂) ∧ f.comp (inr R L₁ L₂) = g.comp (inr R L₁ L₂)
have simp_rw : (∀ (x : L₁ × L₂), Eq.{u_4 + 1} (α := L) ((f : (a : L₁ × L₂) → L) x : L) ((g : (a : L₁ × L₂) → L) x : L)) ↔
  (∀ (x : L₁),
      Eq.{u_4 + 1} (α := L) ((f.comp (inl R L₁ L₂) : (a : L₁) → L) x : L)
        ((g.comp (inl R L₁ L₂) : (a : L₁) → L) x : L)) ∧
    ∀ (x : L₂),
      Eq.{u_4 + 1} (α := L) ((f.comp (inr R L₁ L₂) : (a : L₂) → L) x : L) ((g.comp (inr R L₁ L₂) : (a : L₂) → L) x : L)
Tactic: simp_rw [LieHom.ext_iff]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Prod (hypothesis)
Goal:
R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieAlgebra R L₁
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
inst_5 : LieRing L
inst_6 : LieAlgebra R L
f g : L₁ × L₂ →ₗ⁅R⁆ L
⊢ (∀ (x : L₁ × L₂), Eq.{u_4 + 1} (α := L) ((f : (a : L₁ × L₂) → L) x : L) ((g : (a : L₁ × L₂) → L) x : L)) ↔
    (∀ (x : L₁),
        Eq.{u_4 + 1} (α := L) ((f.comp (inl R L₁ L₂) : (a : L₁) → L) x : L)
          ((g.comp (inl R L₁ L₂) : (a : L₁) → L) x : L)) ∧
      ∀ (x : L₂),
        Eq.{u_4 + 1} (α := L) ((f.comp (inr R L₁ L₂) : (a : L₂) → L) x : L)
          ((g.comp (inr R L₁ L₂) : (a : L₂) → L) x : L)
have h : (↑f : L₁ × L₂ →ₗ[R] L) = (↑g : L₁ × L₂ →ₗ[R] L) ↔
  Eq (α := L₁ →ₗ[R] L) ((↑f : L₁ × L₂ →ₗ[R] L) ∘ₗ LinearMap.inl R L₁ L₂)
      ((↑g : L₁ × L₂ →ₗ[R] L) ∘ₗ LinearMap.inl R L₁ L₂) ∧
    Eq (α := L₂ →ₗ[R] L) ((↑f : L₁ × L₂ →ₗ[R] L) ∘ₗ LinearMap.inr R L₁ L₂)
      ((↑g : L₁ × L₂ →ₗ[R] L) ∘ₗ LinearMap.inr R L₁ L₂)
Tactic: have h := LinearMap.prod_ext_iff (f := f.toLinearMap) (g := g.toLinearMap)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Prod (hypothesis)
Goal:
R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
inst : CommRing R
inst_1 : LieRing L₁
inst_2 : LieAlgebra R L₁
inst_3 : LieRing L₂
inst_4 : LieAlgebra R L₂
inst_5 : LieRing L
inst_6 : LieAlgebra R L
f g : L₁ × L₂ →ₗ⁅R⁆ L
h :
  (↑f : L₁ × L₂ →ₗ[R] L) = (↑g : L₁ × L₂ →ₗ[R] L) ↔
    Eq (α := L₁ →ₗ[R] L) ((↑f : L₁ × L₂ →ₗ[R] L) ∘ₗ LinearMap.inl R L₁ L₂)
        ((↑g : L₁ × L₂ →ₗ[R] L) ∘ₗ LinearMap.inl R L₁ L₂) ∧
      Eq (α := L₂ →ₗ[R] L) ((↑f : L₁ × L₂ →ₗ[R] L) ∘ₗ LinearMap.inr R L₁ L₂)
        ((↑g : L₁ × L₂ →ₗ[R] L) ∘ₗ LinearMap.inr R L₁ L₂)
⊢ (∀ (x : L₁ × L₂), Eq.{u_4 + 1} (α := L) ((f : (a : L₁ × L₂) → L) x : L) ((g : (a : L₁ × L₂) → L) x : L)) ↔
    (∀ (x : L₁),
        Eq.{u_4 + 1} (α := L) ((f.comp (inl R L₁ L₂) : (a : L₁) → L) x : L)
          ((g.comp (inl R L₁ L₂) : (a : L₁) → L) x : L)) ∧
      ∀ (x : L₂),
        Eq.{u_4 + 1} (α := L) ((f.comp (inr R L₁ L₂) : (a : L₂) → L) x : L)
          ((g.comp (inr R L₁ L₂) : (a : L₂) → L) x : L)
have h₁ : (∀ (x : L₁ × L₂),
    Eq.{u_4 + 1} (α := L) (((↑f : L₁ × L₂ →ₗ[R] L) : (a : L₁ × L₂) → L) x : L)
      (((↑g : L₁ × L₂ →ₗ[R] L) : (a : L₁ × L₂) → L) x : L)) ↔
  (∀ (x : L₁),
      Eq.{u_4 + 1} (α := L) (((↑f : L₁ × L₂ →ₗ[R] L) ∘ₗ LinearMap.inl R L₁ L₂ : (a : L₁) → L) x : L)
        (((↑g : L₁ × L₂ →ₗ[R] L) ∘ₗ LinearMap.inl R L₁ L₂ : (a : L₁) → L) x : L)) ∧
    ∀ (x : L₂),
      Eq.{u_4 + 1} (α := L) (((↑f : L₁ × L₂ →ₗ[R] L) ∘ₗ LinearMap.inr R L₁ L₂ : (a : L₂) → L) x : L)
        (((↑g : L₁ × L₂ →ₗ[R] L) ∘ₗ LinearMap.inr R L₁ L₂ : (a : L₂) → L) x : L)
Tactic: simp_rw [LinearMap.ext_iff] at h
Cleared hypotheses: h
-- 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 : L ⧸ I
⊢ L ⧸ I
have apply : ∀ (a₁ a₂ b₁ b₂ : L),
  ((↑I : Submodule R L).quotientRel : L → L → Prop) a₁ b₁ →
    ((↑I : Submodule R L).quotientRel : L → L → Prop) a₂ b₂ → Eq (α := L ⧸ I) (mk ⁅a₁, a₂⁆) (mk ⁅b₁, b₂⁆)
Tactic: apply Quotient.liftOn₂' x y fun x' y' => mk ⁅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
x y : L ⧸ I
x₁ x₂ y₁ y₂ : L
h₁ : ((↑I : Submodule R L).quotientRel : L → L → Prop) x₁ y₁
h₂ : ((↑I : Submodule R L).quotientRel : L → L → Prop) x₂ y₂
⊢ Eq (α := L ⧸ I) (mk ⁅x₁, x₂⁆) (mk ⁅y₁, y₂⁆)
have apply : ⁅x₁, x₂⁆ - ⁅y₁, y₂⁆ ∈ (↑I : Submodule R L)
Tactic: apply (Submodule.Quotient.eq I.toSubmodule).2
-- Lean 4 proof step from Mathlib.Algebra.Lie.Quotient (hypothesis)
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₁ : ((↑I : Submodule R L).quotientRel : L → L → Prop) x₁ y₁
h₂ : ((↑I : Submodule R L).quotientRel : L → L → Prop) x₂ y₂
⊢ ⁅x₁, x₂⁆ - ⁅y₁, y₂⁆ ∈ (↑I : Submodule R L)
have h₃ : x₁ - y₁ ∈ (↑I : Submodule R L)
Tactic: rw [Submodule.quotientRel_def] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Algebra.Lie.Quotient (hypothesis)
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₁ : ((↑I : Submodule R L).quotientRel : L → L → Prop) x₁ y₁
h₂ : ((↑I : Submodule R L).quotientRel : L → L → Prop) x₂ y₂
h₃ : x₁ - y₁ ∈ (↑I : Submodule R L)
⊢ ⁅x₁, x₂⁆ - ⁅y₁, y₂⁆ ∈ (↑I : Submodule R L)
have h₄ : x₂ - y₂ ∈ (↑I : Submodule R L)
Tactic: rw [Submodule.quotientRel_def] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Algebra.Lie.Quotient (hypothesis)
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)
⊢ ⁅x₁, x₂⁆ - ⁅y₁, y₂⁆ ∈ (↑I : Submodule R L)
have h : ⁅x₁, x₂⁆ - ⁅y₁, y₂⁆ = ⁅x₁, x₂ - y₂⁆ + ⁅x₁ - y₁, y₂⁆
Tactic: have h : ⁅x₁, x₂⁆ - ⁅y₁, y₂⁆ = ⁅x₁, x₂ - y₂⁆ + ⁅x₁ - y₁, y₂⁆ := by
      simp [-lie_skew, sub_eq_add_neg, add_assoc]
-- 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 : 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₁, y₂⁆ ∈ (↑I : Submodule R L)
have rw : ⁅x₁, x₂ - y₂⁆ + ⁅x₁ - y₁, y₂⁆ ∈ (↑I : Submodule R L)
Tactic: rw [h]
-- 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 : 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₂⁆ + ⁅x₁ - y₁, y₂⁆ ∈ (↑I : Submodule R L)
have h₃ : ⁅x₁, x₂ - y₂⁆ ∈ (↑I : Submodule R L)
Tactic: apply Submodule.add_mem
-- 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 : 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₂⁆
h₃ : ⁅x₁, x₂ - y₂⁆ ∈ (↑I : Submodule R L)
⊢ ⁅x₁, x₂ - y₂⁆ + ⁅x₁ - y₁, y₂⁆ ∈ (↑I : Submodule R L)
have h₄ : ⁅x₁ - y₁, y₂⁆ ∈ (↑I : Submodule R L)
Tactic: apply Submodule.add_mem
-- 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', z'⁆ + ⁅y', z'⁆
have 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))
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
⊢ ⁅HAdd.hAdd (α := L ⧸ I) (mk x) (mk y), mk z⁆ = HAdd.hAdd (α := L ⧸ I) (mk ⁅x, z⁆) (mk ⁅y, z⁆)
have h : Bracket.bracket (L := L ⧸ I) (Submodule.Quotient.mk (x + y)) (mk z) = HAdd.hAdd (α := L ⧸ I) (mk ⁅x, z⁆) (mk ⁅y, 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
⊢ ⁅HAdd.hAdd (α := L ⧸ I) (mk x) (mk y), mk z⁆ = HAdd.hAdd (α := L ⧸ I) (mk ⁅x, z⁆) (mk ⁅y, z⁆)
have h : Bracket.bracket (L := L ⧸ I) (Submodule.Quotient.mk (x + 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)]
-- 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, z⁆) (mk ⁅y, z⁆)
have h : Eq (α := L ⧸ I) (mk ⁅x + y, z⁆) (Submodule.Quotient.mk (⁅x, z⁆ + ⁅y, 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, z⁆) (mk ⁅y, z⁆)
have h : Eq (α := L ⧸ I) (mk ⁅x + y, z⁆) (Submodule.Quotient.mk (⁅x, z⁆ + ⁅y, z⁆))
Tactic: first
      | rw [is_quotient_mk]
      | rw [← mk_bracket]
      | rw [← Submodule.Quotient.mk_add (R := R) (M := L)]