awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
N : LieSubmodule R L M
φ : R
k : ℕ
x : L
⊢ MapsTo
    (⇑(HSub.hSub (α := Module.End R M) (β := Module.End R M)
            (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
            ((algebraMap R (Module.End R M) : (a : R) → Module.End R M) φ : Module.End R M)) :
        (a : M) → M)^[k]
    (↑N : Set M) (↑N : Set M)

Tactic:
MapsTo.iterate (fun m hm ↦ N.sub_mem (N.lie_mem hm) (N.smul_mem _ hm)) k

Premises used: LieSubmodule.toSubmodule, Set.MapsTo.iterate, LieSubmodule.lie_mem, Submodule.sub_mem, Submodule.smul_mem
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
L : Type v
M : Type w
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
N : LieSubmodule R L M
φ : R
k : ℕ
x : L
⊢ MapsTo
    (⇑(HSub.hSub (α := Module.End R M) (β := Module.End R M)
            (((toEnd R L M : LieHom.{u, v, w} R L (Module.End R M)) : (a : L) → Module.End R M) x : Module.End R M)
            ((algebraMap R (Module.End R M) : (a : R) → Module.End R M) φ : Module.End R M)) :
        (a : M) → M)^[k]
    (↑N : Set M) (↑N : Set M)

Tactic:
exact MapsTo.iterate (fun m hm ↦ N.sub_mem (N.lie_mem hm) (N.smul_mem _ hm)) k

Premises used: LieSubmodule.toSubmodule, Set.MapsTo.iterate, LieSubmodule.lie_mem, Submodule.sub_mem, Submodule.smul_mem
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : Ring A
inst_2 : Algebra R A
h :
  ∀ (a b : A),
    Eq (α := A) ((((ad R A : (a : A) → Module.End R A) a : Module.End R A) : (a : A) → A) b : A)
      ((HSub.hSub (α := (a : A) → A →ₗ[R] A) (β := (b : A) → A →ₗ[R] A) (LinearMap.mulLeft R) (LinearMap.mulRight R) a :
            (a : A) → A)
          b :
        A)
⊢ (⇑(ad R A) : (a : A) → Module.End R A) =
    HSub.hSub (α := (a : A) → A →ₗ[R] A) (LinearMap.mulLeft R) (LinearMap.mulRight R)

Tactic:
ext a b
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : Ring A
inst_2 : Algebra R A
a b : A
⊢ Eq (α := A) ((((ad R A : (a : A) → Module.End R A) a : Module.End R A) : (a : A) → A) b : A)
    ((HSub.hSub (α := (a : A) → A →ₗ[R] A) (β := (b : A) → A →ₗ[R] A) (LinearMap.mulLeft R) (LinearMap.mulRight R) a :
          (a : A) → A)
        b :
      A)

Tactic:
simp [LieRing.of_associative_ring_bracket]

Premises used: LieRing.of_associative_ring_bracket
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
x : ↥K
h :
  ∀ (y : ↥K),
    Eq (α := L) (((ad R L : (a : L) → Module.End R L) (↑x : L) ∘ₗ (↑K.incl : ↥K →ₗ[R] L) : (a : ↥K) → L) y : L)
      (((↑K.incl : ↥K →ₗ[R] L) ∘ₗ (ad R ↥K : (a : ↥K) → Module.End R ↥K) x : (a : ↥K) → L) y : L)
⊢ (ad R L : (a : L) → Module.End R L) (↑x : L) ∘ₗ (↑K.incl : ↥K →ₗ[R] L) =
    (↑K.incl : ↥K →ₗ[R] L) ∘ₗ (ad R ↥K : (a : ↥K) → Module.End R ↥K) x

Tactic:
ext y
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
K : LieSubalgebra R L
x y : ↥K
⊢ Eq (α := L) (((ad R L : (a : L) → Module.End R L) (↑x : L) ∘ₗ (↑K.incl : ↥K →ₗ[R] L) : (a : ↥K) → L) y : L)
    (((↑K.incl : ↥K →ₗ[R] L) ∘ₗ (ad R ↥K : (a : ↥K) → Module.End R ↥K) x : (a : ↥K) → L) y : L)

Tactic:
simp only [ad_apply, LieHom.coe_toLinearMap, LieSubalgebra.coe_incl, LinearMap.coe_comp,
    LieSubalgebra.coe_bracket, Function.comp_apply]

Premises used: LieSubalgebra.coe_bracket, LieAlgebra.ad_apply, LieHom.coe_toLinearMap, LinearMap.coe_comp, LieSubalgebra.coe_incl, Function.comp_apply
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : Ring A
inst_2 : Algebra R A
A' : Subalgebra R A
x y : A
hx :
  Membership.mem (γ := Set A)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u, v} (R := R)
          ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) A'))))
    x
hy :
  Membership.mem (γ := Set A)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u, v} (R := R)
          ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) A'))))
    y
⊢ x ∈ A'

Tactic:
change x ∈ A' at hx
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : Ring A
inst_2 : Algebra R A
A' : Subalgebra R A
x y : A
hy :
  Membership.mem (γ := Set A)
    (AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup
        (Submodule.toAddSubmonoid.{u, v} (R := R)
          ((Subalgebra.toSubmodule : (a : Subalgebra R A) → Submodule R A) A'))))
    y
hx : x ∈ A'
⊢ y ∈ A'

Tactic:
change y ∈ A' at hy
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : Ring A
inst_2 : Algebra R A
A' : Subalgebra R A
x y : A
hx : x ∈ A'
hy : y ∈ A'
rw : x * y - y * x ∈ A'
⊢ ⁅x, y⁆ ∈ A'

Tactic:
rw [LieRing.of_associative_ring_bracket]

Premises used: LieRing.of_associative_ring_bracket
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : Ring A
inst_2 : Algebra R A
A' : Subalgebra R A
x y : A
hx : x ∈ A'
hy : y ∈ A'
⊢ x * y ∈ A'

Tactic:
have hxy := A'.mul_mem hx hy
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : Ring A
inst_2 : Algebra R A
A' : Subalgebra R A
x y : A
hx : x ∈ A'
hy : y ∈ A'
hxy : x * y ∈ A'
⊢ y * x ∈ A'

Tactic:
have hyx := A'.mul_mem hy hx
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : Ring A
inst_2 : Algebra R A
A' : Subalgebra R A
x y : A
hx : x ∈ A'
hy : y ∈ A'
hxy : x * y ∈ A'
hyx : y * x ∈ A'
⊢ x * y - y * x ∈ A'

Tactic:
Submodule.sub_mem (Subalgebra.toSubmodule A') hxy hyx

Premises used: Set.Mem, Subalgebra.toSubmodule, DFunLike.coe, Submodule.sub_mem
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
inst : CommRing R
A : Type v
inst_1 : Ring A
inst_2 : Algebra R A
A' : Subalgebra R A
x y : A
hx : x ∈ A'
hy : y ∈ A'
hxy : x * y ∈ A'
hyx : y * x ∈ A'
⊢ x * y - y * x ∈ A'

Tactic:
exact Submodule.sub_mem (Subalgebra.toSubmodule A') hxy hyx

Premises used: Subalgebra.toSubmodule, DFunLike.coe, Submodule.sub_mem
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
M₁ : Type v
M₂ : Type w
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
e : M₁ ≃ₗ[R] M₂
f g : Module.End R M₁
⊢ Eq.{w + 1} (α := Module.End R M₂) ((e.conj : (a : Module.End R M₁) → Module.End R M₂) ⁅f, g⁆ : Module.End R M₂)
    (Bracket.bracket (L := Module.End R M₂) ((e.conj : (a : Module.End R M₁) → Module.End R M₂) f : Module.End R M₂)
        ((e.conj : (a : Module.End R M₁) → Module.End R M₂) g) :
      Module.End R M₂)

Tactic:
simp only [LieRing.of_associative_ring_bracket, Module.End.mul_eq_comp, e.conj_comp,
          map_sub]

Premises used: map_sub, Module.End.mul_eq_comp, LinearEquiv.conj_comp, LieRing.of_associative_ring_bracket
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
M₁ : Type v
M₂ : Type w
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
e : M₁ ≃ₗ[R] M₂
f : Module.End R M₁
⊢ Eq.{w + 1} (α := Module.End R M₂) ((e.lieConj : (a : Module.End R M₁) → Module.End R M₂) f : Module.End R M₂)
    ((e.conj : (a : Module.End R M₁) → Module.End R M₂) f : Module.End R M₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
M₁ : Type v
M₂ : Type w
inst : CommRing R
inst_1 : AddCommGroup M₁
inst_2 : Module R M₁
inst_3 : AddCommGroup M₂
inst_4 : Module R M₂
e : M₁ ≃ₗ[R] M₂
⊢ e.lieConj.symm = e.symm.lieConj

Tactic:
rfl

Premises used: LieHom.inverse, LinearEquiv.lieConj, LinearMap.inverse, LieEquiv.symm, rfl
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
A₁ : Type v
A₂ : Type w
inst : CommRing R
inst_1 : Ring A₁
inst_2 : Ring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
x y : A₁
⊢ e.toFun = (⇑e : (a : A₁) → A₂)

Tactic:
have : e.toEquiv.toFun = e := rfl
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
A₁ : Type v
A₂ : Type w
inst : CommRing R
inst_1 : Ring A₁
inst_2 : Ring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
x y : A₁
this : e.toFun = (⇑e : (a : A₁) → A₂)
simp_rw : e.toFun (x * y - y * x) = e.toFun x * e.toFun y - e.toFun y * e.toFun x
simp_rw₁ :
  (e : (a : A₁) → A₂) (x * y - y * x) =
    HMul.hMul (α := A₂) (β := A₂) ((e : (a : A₁) → A₂) x : A₂) ((e : (a : A₁) → A₂) y : A₂) -
      HMul.hMul (α := A₂) (β := A₂) ((e : (a : A₁) → A₂) y : A₂) ((e : (a : A₁) → A₂) x : A₂)
simp_rw₂ :
  HSub.hSub (α := A₂) (β := A₂) ((e : (a : A₁) → A₂) (x * y) : A₂) ((e : (a : A₁) → A₂) (y * x) : A₂) =
    HMul.hMul (α := A₂) (β := A₂) ((e : (a : A₁) → A₂) x : A₂) ((e : (a : A₁) → A₂) y : A₂) -
      HMul.hMul (α := A₂) (β := A₂) ((e : (a : A₁) → A₂) y : A₂) ((e : (a : A₁) → A₂) x : A₂)
⊢ e.toFun ⁅x, y⁆ = ⁅e.toFun x, e.toFun y⁆

Tactic:
simp_rw [LieRing.of_associative_ring_bracket, this, map_sub, map_mul]

Premises used: map_sub, LieRing.of_associative_ring_bracket, map_mul
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
A₁ : Type v
A₂ : Type w
inst : CommRing R
inst_1 : Ring A₁
inst_2 : Ring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
x : A₁
⊢ Eq.{w + 1} (α := A₂) ((e.toLieEquiv : (a : A₁) → A₂) x : A₂) ((e : (a : A₁) → A₂) x : A₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.OfAssociative
Goal:
R : Type u
A₁ : Type v
A₂ : Type w
inst : CommRing R
inst_1 : Ring A₁
inst_2 : Ring A₂
inst_3 : Algebra R A₁
inst_4 : Algebra R A₂
e : A₁ ≃ₐ[R] A₂
x : A₂
⊢ Eq.{v + 1} (α := A₁) ((e.toLieEquiv.symm : (a : A₂) → A₁) x : A₁) ((e.symm : (a : A₂) → A₁) x : A₁)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.OfAssociative
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
h :
  ∀ (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')
⊢ Eq.{u_3 + 1} (α := Module.End R 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')
    ((ad R L' : (a : L') → Module.End R L') ((e : (a : L) → L') x : L') : Module.End R L')

Tactic:
ext y'
-- Module: Mathlib.Algebra.Lie.OfAssociative
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'
h₆ 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'
⊢ 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')

Tactic:
rw [LinearEquiv.conj_apply_apply, ad_apply, ad_apply, coe_toLinearEquiv, map_lie,
    ← coe_toLinearEquiv, LinearEquiv.apply_symm_apply]

Premises used: LieEquiv.map_lie, LinearEquiv.conj_apply_apply, LieAlgebra.ad_apply, LinearEquiv.apply_symm_apply, LieEquiv.coe_toLinearEquiv
-- Module: Mathlib.Algebra.Lie.Prod
Goal:
R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
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₅
inst_13 : LieRing L₆
inst_14 : LieAlgebra R L₆
⊢ ∀ (x y z : L₁ × L₂), (⁅(x + y).1, z.1⁆, ⁅(x + y).2, z.2⁆) = (⁅x.1, z.1⁆, ⁅x.2, z.2⁆) + (⁅y.1, z.1⁆, ⁅y.2, z.2⁆)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Prod
Goal:
R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
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₅
inst_13 : LieRing L₆
inst_14 : LieAlgebra R L₆
⊢ ∀ (x y z : L₁ × L₂), (⁅x.1, (y + z).1⁆, ⁅x.2, (y + z).2⁆) = (⁅x.1, y.1⁆, ⁅x.2, y.2⁆) + (⁅x.1, z.1⁆, ⁅x.2, z.2⁆)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Prod
Goal:
R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
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₅
inst_13 : LieRing L₆
inst_14 : LieAlgebra R L₆
⊢ ∀ (x : L₁ × L₂), (⁅x.1, x.1⁆, ⁅x.2, x.2⁆) = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Prod
Goal:
R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
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₅
inst_13 : LieRing L₆
inst_14 : LieAlgebra R L₆
⊢ ∀ (x y z : L₁ × L₂),
    (⁅x.1, (⁅y.1, z.1⁆, ⁅y.2, z.2⁆).1⁆, ⁅x.2, (⁅y.1, z.1⁆, ⁅y.2, z.2⁆).2⁆) =
      (⁅(⁅x.1, y.1⁆, ⁅x.2, y.2⁆).1, z.1⁆, ⁅(⁅x.1, y.1⁆, ⁅x.2, y.2⁆).2, z.2⁆) +
        (⁅y.1, (⁅x.1, z.1⁆, ⁅x.2, z.2⁆).1⁆, ⁅y.2, (⁅x.1, z.1⁆, ⁅x.2, z.2⁆).2⁆)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Prod
Goal:
L₁ : Type u_2
L₂ : Type u_3
inst : LieRing L₁
inst_1 : LieRing L₂
x y : L₁ × L₂
⊢ ⁅x, y⁆ = (⁅x.1, y.1⁆, ⁅x.2, y.2⁆)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.Prod
Goal:
R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
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₅
inst_13 : LieRing L₆
inst_14 : LieAlgebra R L₆
x : R
x_1 x_2 : L₁ × L₂
⊢ ⁅x_1, x • x_2⁆ = x • ⁅x_1, x_2⁆

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Prod
Goal:
R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
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₅
inst_13 : LieRing L₆
inst_14 : LieAlgebra R L₆
⊢ ∀ {x y : L₁ × L₂},
    AddHom.toFun (LinearMap.toAddHom (R := R) (S := R) (σ := RingHom.id R) (LinearMap.fst R L₁ L₂) : L₁ × L₂ →ₙ+ L₁)
        ⁅x, y⁆ =
      ⁅AddHom.toFun (LinearMap.toAddHom (R := R) (S := R) (σ := RingHom.id R) (LinearMap.fst R L₁ L₂) : L₁ × L₂ →ₙ+ L₁)
          x,
        AddHom.toFun (LinearMap.toAddHom (R := R) (S := R) (σ := RingHom.id R) (LinearMap.fst R L₁ L₂) : L₁ × L₂ →ₙ+ L₁)
          y⁆

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Prod
Goal:
R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
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₅
inst_13 : LieRing L₆
inst_14 : LieAlgebra R L₆
⊢ ∀ {x y : L₁ × L₂},
    AddHom.toFun (LinearMap.toAddHom (R := R) (S := R) (σ := RingHom.id R) (LinearMap.snd R L₁ L₂) : L₁ × L₂ →ₙ+ L₂)
        ⁅x, y⁆ =
      ⁅AddHom.toFun (LinearMap.toAddHom (R := R) (S := R) (σ := RingHom.id R) (LinearMap.snd R L₁ L₂) : L₁ × L₂ →ₙ+ L₂)
          x,
        AddHom.toFun (LinearMap.toAddHom (R := R) (S := R) (σ := RingHom.id R) (LinearMap.snd R L₁ L₂) : L₁ × L₂ →ₙ+ L₂)
          y⁆

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Prod
Goal:
R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
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₅
inst_13 : LieRing L₆
inst_14 : LieAlgebra R L₆
⊢ ∀ {x y : L₁},
    AddHom.toFun (LinearMap.toAddHom (R := R) (S := R) (σ := RingHom.id R) (LinearMap.inl R L₁ L₂) : L₁ →ₙ+ L₁ × L₂)
        ⁅x, y⁆ =
      ⁅AddHom.toFun (LinearMap.toAddHom (R := R) (S := R) (σ := RingHom.id R) (LinearMap.inl R L₁ L₂) : L₁ →ₙ+ L₁ × L₂)
          x,
        AddHom.toFun (LinearMap.toAddHom (R := R) (S := R) (σ := RingHom.id R) (LinearMap.inl R L₁ L₂) : L₁ →ₙ+ L₁ × L₂)
          y⁆

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Prod
Goal:
R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
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₅
inst_13 : LieRing L₆
inst_14 : LieAlgebra R L₆
⊢ ∀ {x y : L₂},
    AddHom.toFun (LinearMap.toAddHom (R := R) (S := R) (σ := RingHom.id R) (LinearMap.inr R L₁ L₂) : L₂ →ₙ+ L₁ × L₂)
        ⁅x, y⁆ =
      ⁅AddHom.toFun (LinearMap.toAddHom (R := R) (S := R) (σ := RingHom.id R) (LinearMap.inr R L₁ L₂) : L₂ →ₙ+ L₁ × L₂)
          x,
        AddHom.toFun (LinearMap.toAddHom (R := R) (S := R) (σ := RingHom.id R) (LinearMap.inr R L₁ L₂) : L₂ →ₙ+ L₁ × L₂)
          y⁆

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₁ × L₂
⊢ (fst R L₁ L₂ : (a : L₁ × L₂) → L₁) x = x.1

Tactic:
rfl

Premises used: 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₁ × L₂
⊢ (snd R L₁ L₂ : (a : L₁ × L₂) → L₂) x = x.2

Tactic:
rfl

Premises used: 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₁) (⇑(fst R L₁ L₂) : (a : L₁ × L₂) → L₁) Prod.fst

Tactic:
rfl

Premises used: 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₂) (⇑(snd R L₁ L₂) : (a : L₁ × L₂) → L₂) Prod.snd

Tactic:
rfl

Premises used: 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₂
⊢ Function.Surjective (α := L₁ × L₂) (β := L₁) (⇑(fst R L₁ L₂) : (a : L₁ × L₂) → L₁)

Tactic:
fun x => ⟨(x, 0), rfl⟩

Premises used: Prod.mk, Exists.intro, OfNat.ofNat, Function.Surjective, 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₂
⊢ Function.Surjective (α := L₁ × L₂) (β := L₂) (⇑(snd R L₁ L₂) : (a : L₁ × L₂) → L₂)

Tactic:
fun x => ⟨(0, x), rfl⟩

Premises used: Prod.mk, Exists.intro, OfNat.ofNat, Function.Surjective, rfl
-- Module: Mathlib.Algebra.Lie.Prod
Goal:
R : Type u_1
L₁ : Type u_2
L₂ : Type u_3
L : Type u_4
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₅
inst_13 : LieRing L₆
inst_14 : LieAlgebra R L₆
f : L →ₗ⁅R⁆ L₁
g : L →ₗ⁅R⁆ L₂
⊢ ∀ {x y : L},
    ((↑f : L →ₗ[R] L₁).prod (↑g : L →ₗ[R] L₂)).toFun ⁅x, y⁆ =
      ⁅((↑f : L →ₗ[R] L₁).prod (↑g : L →ₗ[R] L₂)).toFun x, ((↑f : L →ₗ[R] L₁).prod (↑g : L →ₗ[R] L₂)).toFun y⁆

Tactic:
simp
-- 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₂
⊢ Eq (α := (a : L) → L₁ × L₂) (⇑(f.prod g) : (a : L) → L₁ × L₂)
    (Function.prod (α := fun (a : L) ↦ L₁) (β := fun (a : L) ↦ L₂) (⇑f : (a : L) → L₁) (⇑g : (a : 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
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₂
⊢ comp (fst R L₁ L₂) (f.prod g) = f

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
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₂
⊢ comp (snd R L₁ L₂) (f.prod g) = g

Tactic:
rfl

Premises used: LieHom.comp, rfl