awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Prod
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 (α := L₁ × L₂ →ₗ⁅R⁆ L₁ × L₂) (prod (fst R L₁ L₂) (snd R L₁ L₂)) id

Tactic:
rfl

Premises used: Function.prod, LinearMap.prod, LieHom.prod, LieHom.id, rfl
-- Module: Mathlib.Algebra.Lie.Prod
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 : L₁ →ₗ⁅R⁆ L₂
g : L₁ →ₗ⁅R⁆ L
h : L →ₗ⁅R⁆ L₁
⊢ (f.prod g).comp h = (f.comp h).prod (g.comp h)

Tactic:
rfl

Premises used: Function.prod, LinearMap.prod, LieHom.comp, LieHom.prod, rfl
-- Module: Mathlib.Algebra.Lie.Prod
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₂
x : L₁
⊢ Eq (α := L₁ × L₂) ((inl R L₁ L₂ : (a : L₁) → L₁ × L₂) x : L₁ × L₂) ((x, 0) : L₁ × L₂)

Tactic:
rfl

Premises used: Function.prod, rfl
-- Module: Mathlib.Algebra.Lie.Prod
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₂
x : L₂
⊢ Eq (α := L₁ × L₂) ((inr R L₁ L₂ : (a : L₂) → L₁ × L₂) x : L₁ × L₂) ((0, x) : L₁ × L₂)

Tactic:
rfl

Premises used: Function.prod, rfl
-- Module: Mathlib.Algebra.Lie.Prod
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 (α := (a : L₁) → L₁ × L₂) (⇑(inl R L₁ L₂) : (a : L₁) → L₁ × L₂) fun (x : L₁) ↦ (x, 0)

Tactic:
rfl

Premises used: Function.prod, rfl
-- Module: Mathlib.Algebra.Lie.Prod
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 (α := (a : L₂) → L₁ × L₂) (⇑(inr R L₁ L₂) : (a : L₂) → L₁ × L₂) (Prod.mk 0)

Tactic:
rfl

Premises used: Function.prod, rfl
-- Module: Mathlib.Algebra.Lie.Prod
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₂
x : L₁
⊢ ∀ ⦃a₂ : L₁⦄,
    Eq (α := L₁ × L₂) ((inl R L₁ L₂ : (a : L₁) → L₁ × L₂) x : L₁ × L₂)
        ((inl R L₁ L₂ : (a : L₁) → L₁ × L₂) a₂ : L₁ × L₂) →
      x = a₂

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Prod
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₂
x : L₂
⊢ ∀ ⦃a₂ : L₂⦄,
    Eq (α := L₁ × L₂) ((inr R L₁ L₂ : (a : L₂) → L₁ × L₂) x : L₁ × L₂)
        ((inr R L₁ L₂ : (a : L₂) → L₁ × L₂) a₂ : L₁ × L₂) →
      x = a₂

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Prod
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₂
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₂))
⊢ Eq (α := LieSubalgebra R (L₁ × L₂)) (range (inl R L₁ L₂)) (LieIdeal.toLieSubalgebra R (L₁ × L₂) (ker (snd R L₁ L₂)))

Tactic:
rw [← LieSubalgebra.toSubmodule_inj, range_toSubmodule, LieIdeal.toLieSubalgebra_toSubmodule,
   ker_toSubmodule]

Premises used: LieIdeal.toLieSubalgebra_toSubmodule, LieSubalgebra.toSubmodule_inj, LieHom.range_toSubmodule, LieHom.ker_toSubmodule
-- Module: Mathlib.Algebra.Lie.Prod
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 (α := 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:
LinearMap.range_inl R L₁ L₂

Premises used: LinearMap.inl, LinearMap.snd, LinearMap.range_inl, LinearMap.prod
-- Module: Mathlib.Algebra.Lie.Prod
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 (α := 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:
exact LinearMap.range_inl R L₁ L₂

Premises used: LinearMap.range_inl
-- Module: Mathlib.Algebra.Lie.Prod
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₂)) (LieIdeal.toLieSubalgebra R (L₁ × L₂) (ker (snd R L₁ L₂))) (range (inl R L₁ L₂))

Tactic:
Eq.symm <| range_inl R L₁ L₂

Premises used: LieHom.range_inl, Eq.symm
-- Module: Mathlib.Algebra.Lie.Prod
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₂
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₁))
⊢ Eq (α := LieSubalgebra R (L₁ × L₂)) (range (inr R L₁ L₂)) (LieIdeal.toLieSubalgebra R (L₁ × L₂) (ker (fst R L₁ L₂)))

Tactic:
rw [← LieSubalgebra.toSubmodule_inj, range_toSubmodule, LieIdeal.toLieSubalgebra_toSubmodule,
   ker_toSubmodule]

Premises used: LieIdeal.toLieSubalgebra_toSubmodule, LieSubalgebra.toSubmodule_inj, LieHom.range_toSubmodule, LieHom.ker_toSubmodule
-- Module: Mathlib.Algebra.Lie.Prod
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 (α := 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:
LinearMap.range_inr R L₁ L₂

Premises used: LinearMap.fst, LinearMap.range_inr, LinearMap.prod, LinearMap.inr
-- Module: Mathlib.Algebra.Lie.Prod
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 (α := 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:
exact LinearMap.range_inr R L₁ L₂

Premises used: LinearMap.range_inr
-- Module: Mathlib.Algebra.Lie.Prod
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₂)) (LieIdeal.toLieSubalgebra R (L₁ × L₂) (ker (fst R L₁ L₂))) (range (inr R L₁ L₂))

Tactic:
Eq.symm <| range_inr R L₁ L₂

Premises used: LieHom.range_inr, Eq.symm
-- Module: Mathlib.Algebra.Lie.Prod
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 (α := L₁ →ₗ⁅R⁆ L₁) (comp (fst R L₁ L₂) (inl R L₁ L₂)) id

Tactic:
rfl

Premises used: LieHom.comp, LieHom.id, rfl
-- Module: Mathlib.Algebra.Lie.Prod
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 (α := L₁ →ₗ⁅R⁆ L₂) (comp (snd R L₁ L₂) (inl R L₁ L₂)) 0

Tactic:
rfl

Premises used: LieHom.comp, rfl
-- Module: Mathlib.Algebra.Lie.Prod
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 (α := L₂ →ₗ⁅R⁆ L₁) (comp (fst R L₁ L₂) (inr R L₁ L₂)) 0

Tactic:
rfl

Premises used: LieHom.comp, rfl
-- Module: Mathlib.Algebra.Lie.Prod
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 (α := L₂ →ₗ⁅R⁆ L₂) (comp (snd R L₁ L₂) (inr R L₁ L₂)) id

Tactic:
rfl

Premises used: LieHom.comp, LieHom.id, rfl
-- Module: Mathlib.Algebra.Lie.Prod
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 (α := L₁ →ₗ⁅R⁆ L₁ × L₂) (inl R L₁ L₂) (prod id 0)

Tactic:
rfl

Premises used: LinearMap.inl, LieHom.prod, rfl
-- Module: Mathlib.Algebra.Lie.Prod
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 (α := L₂ →ₗ⁅R⁆ L₁ × L₂) (inr R L₁ L₂) (prod 0 id)

Tactic:
rfl

Premises used: LieHom.prod, LinearMap.inr, rfl
-- Module: Mathlib.Algebra.Lie.Prod
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
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)
⊢ 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₂)

Tactic:
simp_rw [LieHom.ext_iff]

Premises used: LieHom.ext_iff
-- Module: Mathlib.Algebra.Lie.Prod
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 : 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)
-- Module: Mathlib.Algebra.Lie.Prod
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 : 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

Premises used: LinearMap.ext_iff
-- Module: Mathlib.Algebra.Lie.Prod
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 :
  (∀ (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)
⊢ (∀ (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:
h
-- Module: Mathlib.Algebra.Lie.Prod
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 :
  (∀ (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)
⊢ (∀ (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:
exact h
-- Module: Mathlib.Algebra.Lie.Prod
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
hl : f.comp (inl R L₁ L₂) = g.comp (inl R L₁ L₂)
hr : f.comp (inr R L₁ L₂) = g.comp (inr R L₁ L₂)
⊢ f = g

Tactic:
(prod_ext_iff R L₁ L₂).mpr ⟨hl,hr⟩

Premises used: Iff.mpr, LieHom.prod_ext_iff, And.intro
-- Module: Mathlib.Algebra.Lie.Prod
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
hl : f.comp (inl R L₁ L₂) = g.comp (inl R L₁ L₂)
hr : f.comp (inr R L₁ L₂) = g.comp (inr R L₁ L₂)
⊢ f = g

Tactic:
refine (prod_ext_iff R L₁ L₂).mpr ⟨hl,hr⟩

Premises used: Iff.mpr, LieHom.prod_ext_iff, And.intro
-- Module: Mathlib.Algebra.Lie.Prod
Goal:
R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L₃ : Type u_5
L₄ : Type u_6
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₃
inst_7 : LieRing L₄
inst_8 : LieAlgebra R L₄
f : L₁ →ₗ⁅R⁆ L₃
g : L₂ →ₗ⁅R⁆ L₄
⊢ Eq (α := (a : L₁ × L₂) → L₃ × L₄) (⇑(f.prodMap g) : (a : L₁ × L₂) → L₃ × L₄)
    (Prod.map (⇑f : (a : L₁) → L₃) (⇑g : (a : L₂) → L₄))

Tactic:
rfl

Premises used: Prod.map, Function.prod, rfl
-- Module: Mathlib.Algebra.Lie.Prod
Goal:
R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L₃ : Type u_5
L₄ : Type u_6
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₃
inst_7 : LieRing L₄
inst_8 : LieAlgebra R L₄
f : L₁ →ₗ⁅R⁆ L₃
g : L₂ →ₗ⁅R⁆ L₄
x : L₁ × L₂
⊢ Eq (α := L₃ × L₄) ((f.prodMap g : (a : L₁ × L₂) → L₃ × L₄) x : L₃ × L₄)
    (((f : (a : L₁) → L₃) x.1, (g : (a : L₂) → L₄) x.2) : L₃ × L₄)

Tactic:
rfl

Premises used: Function.prod, rfl
-- Module: Mathlib.Algebra.Lie.Prod
Goal:
R : Type u_1
L₁ : Type u_2
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
⊢ Eq (α := L × L₁ →ₗ⁅R⁆ L × L₁) (prodMap id id) id

Tactic:
rfl

Premises used: LieHom.prodMap, Function.prod, LinearMap.prod, LieHom.prod, LieHom.id, rfl
-- Module: Mathlib.Algebra.Lie.Prod
Goal:
R : Type u_1
L₁ : Type u_2
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
⊢ Eq (α := L × L₁ →ₗ⁅R⁆ L × L₁) (prodMap 1 1) 1

Tactic:
rfl

Premises used: LieHom.prodMap, Function.prod, LinearMap.prod, LieHom.prod, LieHom.id, rfl
-- Module: Mathlib.Algebra.Lie.Prod
Goal:
R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L₃ : Type u_5
L₄ : Type u_6
L₅ : Type u_7
L₆ : Type u_8
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₃
inst_7 : LieRing L₄
inst_8 : LieAlgebra R L₄
inst_9 : LieRing L₅
inst_10 : LieAlgebra R L₅
inst_11 : LieRing L₆
inst_12 : LieAlgebra R L₆
f₁₂ : L₁ →ₗ⁅R⁆ L₂
f₂₃ : L₂ →ₗ⁅R⁆ L₃
g₁₂ : L₄ →ₗ⁅R⁆ L₅
g₂₃ : L₅ →ₗ⁅R⁆ L₆
⊢ (f₂₃.prodMap g₂₃).comp (f₁₂.prodMap g₁₂) = (f₂₃.comp f₁₂).prodMap (g₂₃.comp g₁₂)

Tactic:
rfl

Premises used: LieHom.prodMap, Function.prod, LinearMap.prod, LieHom.comp, LieHom.prod, rfl
-- Module: Mathlib.Algebra.Lie.Prod
Goal:
R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L₃ : Type u_5
L₄ : Type u_6
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₃
inst_7 : LieRing L₄
inst_8 : LieAlgebra R L₄
⊢ Eq (α := L₁ × L₂ →ₗ⁅R⁆ L₃ × L₄) (prodMap 0 0) 0

Tactic:
rfl

Premises used: LieHom.prodMap, Function.prod, LinearMap.prod, LieHom.prod, rfl
-- 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
S : Type u_1
inst_5 : Semiring S
inst_6 : SMul S R
inst_7 : Module S M
inst_8 : IsScalarTower S R M
inst_9 : SMul.{u_1, u} Sᵐᵒᵖ R
inst_10 : Module.{u_1, w} Sᵐᵒᵖ M
inst_11 : IsScalarTower.{u_1, u, w} Sᵐᵒᵖ R M
inst_12 : IsCentralScalar S M
⊢ IsCentralScalar.{u_1, w} S (M ⧸ N)

Tactic:
Submodule.Quotient.isCentralScalar _

Premises used: Submodule.Quotient.isCentralScalar
-- 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
m : M
⊢ Eq (α := M ⧸ N) (mk m) 0 ↔ m ∈ N

Tactic:
Submodule.Quotient.mk_eq_zero N.toSubmodule

Premises used: Set.Mem, 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
m : M
⊢ Eq (α := Quotient (↑N : Submodule R M).quotientRel) (Quotient.mk'' m) (mk m)

Tactic:
rfl

Premises used: Submodule.Quotient.mk, rfl
-- 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
⊢ LieModule.{u, v, w} R L (M ⧸ N)

Tactic:
LieModule.compLieHom _ (actionAsEndoMap N)

Premises used: LieSubmodule.Quotient.actionAsEndoMap, LieModule.compLieHom
-- 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
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₂⁆)
⊢ L ⧸ I

Tactic:
apply Quotient.liftOn₂' x y fun x' y' => mk ⁅x', y'⁆

Premises used: LieSubmodule.Quotient.mk, Bracket.bracket, 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 : 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₂
apply : ⁅x₁, x₂⁆ - ⁅y₁, y₂⁆ ∈ (↑I : Submodule R L)
⊢ Eq (α := L ⧸ I) (mk ⁅x₁, x₂⁆) (mk ⁅y₁, y₂⁆)

Tactic:
apply (Submodule.Quotient.eq I.toSubmodule).2

Premises used: Submodule.Quotient.eq, Iff.mpr, LieSubmodule.toSubmodule
-- 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₁ : ((↑I : Submodule R L).quotientRel : L → L → Prop) x₁ y₁
h₂ : ((↑I : Submodule R L).quotientRel : L → L → Prop) x₂ y₂
⊢ x₁ - y₁ ∈ (↑I : Submodule R L)

Tactic:
rw [Submodule.quotientRel_def] at h₁ h₂

Premises used: Submodule.quotientRel_def
-- 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₁ : ((↑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₂ - y₂ ∈ (↑I : Submodule R L)

Tactic:
rw [Submodule.quotientRel_def] at h₁ h₂

Premises used: Submodule.quotientRel_def
-- 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)
⊢ ⁅x₁, x₂⁆ - ⁅y₁, y₂⁆ = ⁅x₁, x₂ - y₂⁆ + ⁅x₁ - y₁, y₂⁆

Tactic:
simp [-lie_skew, sub_eq_add_neg, add_assoc]

Premises used: add_assoc, sub_eq_add_neg, lie_skew
-- 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)
⊢ ⁅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]
-- 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₂⁆
rw : ⁅x₁, x₂ - y₂⁆ + ⁅x₁ - y₁, y₂⁆ ∈ (↑I : Submodule R L)
⊢ ⁅x₁, x₂⁆ - ⁅y₁, y₂⁆ ∈ (↑I : Submodule R L)

Tactic:
rw [h]
-- 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₂⁆
h₃ : ⁅x₁, x₂ - y₂⁆ ∈ (↑I : Submodule R L)
h₄ : ⁅x₁ - y₁, y₂⁆ ∈ (↑I : Submodule R L)
⊢ ⁅x₁, x₂ - y₂⁆ + ⁅x₁ - y₁, y₂⁆ ∈ (↑I : Submodule R L)

Tactic:
apply Submodule.add_mem

Premises used: Submodule.add_mem