awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α_1 β_1 α : Weight K (↥H) L
hα : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) α
β : Weight K (↥H) L
hβ : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) β
u : K
hu : u • Weight.toLinear K (↥H) L α = Weight.toLinear K (↥H) L β
h : β = -α
inl :
  ∀ (x : ↥H),
    Eq.{u_1 + 1} (α := K)
      ((((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
                (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
                  Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) α
                  hα) :
              Dual.{u_1, u_2} K ↥H) :
            (a : ↥H) → K)
          x :
        K)
      (((-(RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
                  (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
                    Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) β
                    hβ) :
              Dual.{u_1, u_2} K ↥H) :
            (a : ↥H) → K)
          x :
        K)
⊢ Eq (α := Dual.{u_1, u_2} K ↥H)
    ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
        (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
          Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) α hα) :
      Dual.{u_1, u_2} K ↥H)
    (-(RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
          (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
            Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) β hβ) :
      Dual.{u_1, u_2} K ↥H)

Tactic:
ext x
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α_1 β_1 α : Weight K (↥H) L
hα : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) α
β : Weight K (↥H) L
hβ : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) β
u : K
hu : u • Weight.toLinear K (↥H) L α = Weight.toLinear K (↥H) L β
h : β = -α
x : ↥H
⊢ Eq.{u_1 + 1} (α := K)
    ((((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
              (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
                Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) α
                hα) :
            Dual.{u_1, u_2} K ↥H) :
          (a : ↥H) → K)
        x :
      K)
    (((-(RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
                (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
                  Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) β
                  hβ) :
            Dual.{u_1, u_2} K ↥H) :
          (a : ↥H) → K)
        x :
      K)

Tactic:
simpa [neg_eq_iff_eq_neg] using DFunLike.congr_fun h.symm x

Premises used: DFunLike.congr_fun, neg_eq_iff_eq_neg, Eq.symm
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α_1 β_1 α : Weight K (↥H) L
hα : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) α
β : Weight K (↥H) L
hβ : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) β
u : K
hu : u • Weight.toLinear K (↥H) L α = Weight.toLinear K (↥H) L β
h : β = α
inr :
  Eq (α := Dual.{u_1, u_2} K ↥H)
    ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
        (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
          Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) α hα) :
      Dual.{u_1, u_2} K ↥H)
    ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
        (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
          Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) β hβ) :
      Dual.{u_1, u_2} K ↥H)
⊢ Eq (α := Dual.{u_1, u_2} K ↥H)
      ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
          (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
            Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) α hα) :
        Dual.{u_1, u_2} K ↥H)
      ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
          (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
            Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) β hβ) :
        Dual.{u_1, u_2} K ↥H) ∨
    Eq (α := Dual.{u_1, u_2} K ↥H)
      ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
          (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
            Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) α hα) :
        Dual.{u_1, u_2} K ↥H)
      (-(RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
            (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
              Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) β hβ) :
        Dual.{u_1, u_2} K ↥H)

Tactic:
left
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α_1 β_1 α : Weight K (↥H) L
hα : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) α
β : Weight K (↥H) L
hβ : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) β
u : K
hu : u • Weight.toLinear K (↥H) L α = Weight.toLinear K (↥H) L β
h : β = α
inr :
  ∀ (x : ↥H),
    Eq.{u_1 + 1} (α := K)
      ((((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
                (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
                  Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) α
                  hα) :
              Dual.{u_1, u_2} K ↥H) :
            (a : ↥H) → K)
          x :
        K)
      ((((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
                (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
                  Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) β
                  hβ) :
              Dual.{u_1, u_2} K ↥H) :
            (a : ↥H) → K)
          x :
        K)
⊢ Eq (α := Dual.{u_1, u_2} K ↥H)
    ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
        (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
          Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) α hα) :
      Dual.{u_1, u_2} K ↥H)
    ((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
        (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
          Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) β hβ) :
      Dual.{u_1, u_2} K ↥H)

Tactic:
ext x
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α_1 β_1 α : Weight K (↥H) L
hα : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) α
β : Weight K (↥H) L
hβ : Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) β
u : K
hu : u • Weight.toLinear K (↥H) L α = Weight.toLinear K (↥H) L β
h : β = α
x : ↥H
⊢ Eq.{u_1 + 1} (α := K)
    ((((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
              (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
                Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) α
                hα) :
            Dual.{u_1, u_2} K ↥H) :
          (a : ↥H) → K)
        x :
      K)
    ((((RootPairing.root (rootSystem H) : (a : ↥LieSubalgebra.root) → Dual K ↥H)
              (Subtype.mk (p := fun (x : Weight K (↥H) L) ↦
                Membership.mem (γ := Finset (Weight K (↥H) L)) (LieSubalgebra.root : Finset (Weight K (↥H) L)) x) β
                hβ) :
            Dual.{u_1, u_2} K ↥H) :
          (a : ↥H) → K)
        x :
      K)

Tactic:
simpa using DFunLike.congr_fun h.symm x

Premises used: DFunLike.congr_fun, Eq.symm
-- Module: Mathlib.Algebra.LieRinehartAlgebra.Defs
Goal:
A₁ : Type u_2
L₁ : Type u_3
inst : CommRing A₁
inst_1 : LieRing L₁
inst_2 : Module A₁ L₁
inst_3 : LieRingModule L₁ A₁
inst_4 : LieRinehartRing A₁ L₁
a b : A₁
x : L₁
⊢ ⁅a • x, b⁆ = a * ⁅x, b⁆

Tactic:
LieRinehartRing.lie_smul_eq_mul' a b x

Premises used: LieRinehartRing.lie_smul_eq_mul'
-- Module: Mathlib.Algebra.LieRinehartAlgebra.Defs
Goal:
A₁ : Type u_2
L₁ : Type u_3
inst : CommRing A₁
inst_1 : LieRing L₁
inst_2 : Module A₁ L₁
inst_3 : LieRingModule L₁ A₁
inst_4 : LieRinehartRing A₁ L₁
x : L₁
a b : A₁
⊢ ⁅x, a * b⁆ = a • ⁅x, b⁆ + ⁅x, a⁆ * b

Tactic:
LieRinehartRing.leibniz_mul_right' x a b

Premises used: LieRinehartRing.leibniz_mul_right'
-- Module: Mathlib.Algebra.LieRinehartAlgebra.Defs
Goal:
A₁ : Type u_2
L₁ : Type u_3
inst : CommRing A₁
inst_1 : LieRing L₁
inst_2 : Module A₁ L₁
inst_3 : LieRingModule L₁ A₁
inst_4 : LieRinehartRing A₁ L₁
x y : L₁
a : A₁
⊢ ⁅x, a • y⁆ = a • ⁅x, y⁆ + ⁅x, a⁆ • y

Tactic:
LieRinehartRing.leibniz_smul_right' x y a

Premises used: LieRinehartRing.leibniz_smul_right'
-- Module: Mathlib.Algebra.LieRinehartAlgebra.Defs
Goal:
R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst : CommRing R
inst_1 : CommRing A₁
inst_2 : LieRing L₁
inst_3 : Module A₁ L₁
inst_4 : LieRingModule L₁ A₁
inst_5 : CommRing A₂
inst_6 : LieRing L₂
inst_7 : Module A₂ L₂
inst_8 : LieRingModule L₂ A₂
inst_9 : CommRing A₃
inst_10 : LieRing L₃
inst_11 : Module A₃ L₃
inst_12 : LieRingModule L₃ A₃
inst_13 : Algebra R A₁
inst_14 : LieAlgebra R L₁
inst_15 : Algebra R A₂
inst_16 : LieAlgebra R L₂
inst_17 : Algebra R A₃
inst_18 : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
x : Derivation R A₁ A₁
x_1 x_2 : A₁
simp : HMul.hMul (β := A₁) x_2 ((x : (a : A₁) → A₁) x_1 : A₁) = HMul.hMul (α := A₁) ((x : (a : A₁) → A₁) x_1 : A₁) x_2
⊢ ⁅x, x_1 * x_2⁆ = x_1 • ⁅x, x_2⁆ + ⁅x, x_1⁆ * x_2

Tactic:
simp
-- Module: Mathlib.Algebra.LieRinehartAlgebra.Defs
Goal:
R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst : CommRing R
inst_1 : CommRing A₁
inst_2 : LieRing L₁
inst_3 : Module A₁ L₁
inst_4 : LieRingModule L₁ A₁
inst_5 : CommRing A₂
inst_6 : LieRing L₂
inst_7 : Module A₂ L₂
inst_8 : LieRingModule L₂ A₂
inst_9 : CommRing A₃
inst_10 : LieRing L₃
inst_11 : Module A₃ L₃
inst_12 : LieRingModule L₃ A₃
inst_13 : Algebra R A₁
inst_14 : LieAlgebra R L₁
inst_15 : Algebra R A₂
inst_16 : LieAlgebra R L₂
inst_17 : Algebra R A₃
inst_18 : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
x : Derivation R A₁ A₁
x_1 x_2 : A₁
⊢ HMul.hMul (β := A₁) x_2 ((x : (a : A₁) → A₁) x_1 : A₁) = HMul.hMul (α := A₁) ((x : (a : A₁) → A₁) x_1 : A₁) x_2

Tactic:
ring
-- Module: Mathlib.Algebra.LieRinehartAlgebra.Defs
Goal:
R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst : CommRing R
inst_1 : CommRing A₁
inst_2 : LieRing L₁
inst_3 : Module A₁ L₁
inst_4 : LieRingModule L₁ A₁
inst_5 : CommRing A₂
inst_6 : LieRing L₂
inst_7 : Module A₂ L₂
inst_8 : LieRingModule L₂ A₂
inst_9 : CommRing A₃
inst_10 : LieRing L₃
inst_11 : Module A₃ L₃
inst_12 : LieRingModule L₃ A₃
inst_13 : Algebra R A₁
inst_14 : LieAlgebra R L₁
inst_15 : Algebra R A₂
inst_16 : LieAlgebra R L₂
inst_17 : Algebra R A₃
inst_18 : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
x x_1 : Derivation R A₁ A₁
x_2 : A₁
H :
  ∀ (a : A₁),
    Eq (α := A₁) ((⁅x, x_2 • x_1⁆ : (a : A₁) → A₁) a : A₁) ((x_2 • ⁅x, x_1⁆ + ⁅x, x_2⁆ • x_1 : (a : A₁) → A₁) a : A₁)
⊢ ⁅x, x_2 • x_1⁆ = x_2 • ⁅x, x_1⁆ + ⁅x, x_2⁆ • x_1

Tactic:
ext
-- Module: Mathlib.Algebra.LieRinehartAlgebra.Defs
Goal:
R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst : CommRing R
inst_1 : CommRing A₁
inst_2 : LieRing L₁
inst_3 : Module A₁ L₁
inst_4 : LieRingModule L₁ A₁
inst_5 : CommRing A₂
inst_6 : LieRing L₂
inst_7 : Module A₂ L₂
inst_8 : LieRingModule L₂ A₂
inst_9 : CommRing A₃
inst_10 : LieRing L₃
inst_11 : Module A₃ L₃
inst_12 : LieRingModule L₃ A₃
inst_13 : Algebra R A₁
inst_14 : LieAlgebra R L₁
inst_15 : Algebra R A₂
inst_16 : LieAlgebra R L₂
inst_17 : Algebra R A₃
inst_18 : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
x x_1 : Derivation R A₁ A₁
x_2 a : A₁
H :
  HMul.hMul (β := A₁) x_2 ((x : (a : A₁) → A₁) ((x_1 : (a : A₁) → A₁) a : A₁) : A₁) +
        HMul.hMul (α := A₁) (β := A₁) ((x_1 : (a : A₁) → A₁) a : A₁) ((x : (a : A₁) → A₁) x_2 : A₁) -
      HMul.hMul (β := A₁) x_2 ((x_1 : (a : A₁) → A₁) ((x : (a : A₁) → A₁) a : A₁) : A₁) =
    x_2 *
        HSub.hSub (α := A₁) (β := A₁) ((x : (a : A₁) → A₁) ((x_1 : (a : A₁) → A₁) a : A₁) : A₁)
          ((x_1 : (a : A₁) → A₁) ((x : (a : A₁) → A₁) a : A₁) : A₁) +
      HMul.hMul (α := A₁) (β := A₁) ((x : (a : A₁) → A₁) x_2 : A₁) ((x_1 : (a : A₁) → A₁) a : A₁)
⊢ Eq (α := A₁) ((⁅x, x_2 • x_1⁆ : (a : A₁) → A₁) a : A₁) ((x_2 • ⁅x, x_1⁆ + ⁅x, x_2⁆ • x_1 : (a : A₁) → A₁) a : A₁)

Tactic:
simp [Derivation.commutator_apply]

Premises used: Derivation.commutator_apply
-- Module: Mathlib.Algebra.LieRinehartAlgebra.Defs
Goal:
R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst : CommRing R
inst_1 : CommRing A₁
inst_2 : LieRing L₁
inst_3 : Module A₁ L₁
inst_4 : LieRingModule L₁ A₁
inst_5 : CommRing A₂
inst_6 : LieRing L₂
inst_7 : Module A₂ L₂
inst_8 : LieRingModule L₂ A₂
inst_9 : CommRing A₃
inst_10 : LieRing L₃
inst_11 : Module A₃ L₃
inst_12 : LieRingModule L₃ A₃
inst_13 : Algebra R A₁
inst_14 : LieAlgebra R L₁
inst_15 : Algebra R A₂
inst_16 : LieAlgebra R L₂
inst_17 : Algebra R A₃
inst_18 : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
x x_1 : Derivation R A₁ A₁
x_2 a : A₁
⊢ HMul.hMul (β := A₁) x_2 ((x : (a : A₁) → A₁) ((x_1 : (a : A₁) → A₁) a : A₁) : A₁) +
        HMul.hMul (α := A₁) (β := A₁) ((x_1 : (a : A₁) → A₁) a : A₁) ((x : (a : A₁) → A₁) x_2 : A₁) -
      HMul.hMul (β := A₁) x_2 ((x_1 : (a : A₁) → A₁) ((x : (a : A₁) → A₁) a : A₁) : A₁) =
    x_2 *
        HSub.hSub (α := A₁) (β := A₁) ((x : (a : A₁) → A₁) ((x_1 : (a : A₁) → A₁) a : A₁) : A₁)
          ((x_1 : (a : A₁) → A₁) ((x : (a : A₁) → A₁) a : A₁) : A₁) +
      HMul.hMul (α := A₁) (β := A₁) ((x : (a : A₁) → A₁) x_2 : A₁) ((x_1 : (a : A₁) → A₁) a : A₁)

Tactic:
ring
-- Module: Mathlib.Algebra.LieRinehartAlgebra.Defs
Goal:
R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
inst : CommRing R
inst_1 : CommRing A₁
inst_2 : LieRing L₁
inst_3 : Module A₁ L₁
inst_4 : LieRingModule L₁ A₁
inst_5 : CommRing A₂
inst_6 : LieRing L₂
inst_7 : Module A₂ L₂
inst_8 : LieRingModule L₂ A₂
inst_9 : Algebra R A₁
inst_10 : LieAlgebra R L₁
inst_11 : Algebra R A₂
inst_12 : LieAlgebra R L₂
σ₁₂ : A₁ →ₐ[R] A₂
f : L₁ →ₗ⁅σ₁₂⁆ L₂
a : A₁
x : L₁
⊢ (f.toLieHom : (a : L₁) → L₂) (a • x) =
    HSMul.hSMul.{u_4, u_5, u_5} (α := A₂) (β := L₂) ((σ₁₂ : (a : A₁) → A₂) a : A₂) ((f.toLieHom : (a : L₁) → L₂) x : L₂)

Tactic:
f.map_smul_apply' a x

Premises used: LieRinehartAlgebra.Hom.map_smul_apply'
-- Module: Mathlib.Algebra.LieRinehartAlgebra.Defs
Goal:
R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
inst : CommRing R
inst_1 : CommRing A₁
inst_2 : LieRing L₁
inst_3 : Module A₁ L₁
inst_4 : LieRingModule L₁ A₁
inst_5 : CommRing A₂
inst_6 : LieRing L₂
inst_7 : Module A₂ L₂
inst_8 : LieRingModule L₂ A₂
inst_9 : Algebra R A₁
inst_10 : LieAlgebra R L₁
inst_11 : Algebra R A₂
inst_12 : LieAlgebra R L₂
σ₁₂ : A₁ →ₐ[R] A₂
f : L₁ →ₗ⁅σ₁₂⁆ L₂
a : A₁
x : L₁
⊢ Eq.{u_4 + 1} (α := A₂) ((σ₁₂ : (a : A₁) → A₂) ⁅x, a⁆ : A₂)
    (Bracket.bracket.{u_5, u_4} (L := L₂) ((f.toLieHom : (a : L₁) → L₂) x : L₂) ((σ₁₂ : (a : A₁) → A₂) a) : A₂)

Tactic:
f.apply_lie' a x

Premises used: LieRinehartAlgebra.Hom.apply_lie'
-- Module: Mathlib.Algebra.LieRinehartAlgebra.Defs
Goal:
R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
inst : CommRing R
inst_1 : CommRing A₁
inst_2 : LieRing L₁
inst_3 : Module A₁ L₁
inst_4 : LieRingModule L₁ A₁
inst_5 : CommRing A₂
inst_6 : LieRing L₂
inst_7 : Module A₂ L₂
inst_8 : LieRingModule L₂ A₂
inst_9 : Algebra R A₁
inst_10 : LieAlgebra R L₁
inst_11 : Algebra R A₂
inst_12 : LieAlgebra R L₂
σ₁₂ : A₁ →ₐ[R] A₂
f : L₁ →ₗ⁅σ₁₂⁆ L₂
x : L₁
⊢ Eq.{u_5 + 1} (α := L₂) ((f.toLinearMap' : (a : L₁) → L₂) x : L₂) ((f.toLieHom : (a : L₁) → L₂) x : L₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.LieRinehartAlgebra.Defs
Goal:
R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst : CommRing R
inst_1 : CommRing A₁
inst_2 : LieRing L₁
inst_3 : Module A₁ L₁
inst_4 : LieRingModule L₁ A₁
inst_5 : CommRing A₂
inst_6 : LieRing L₂
inst_7 : Module A₂ L₂
inst_8 : LieRingModule L₂ A₂
inst_9 : CommRing A₃
inst_10 : LieRing L₃
inst_11 : Module A₃ L₃
inst_12 : LieRingModule L₃ A₃
inst_13 : Algebra R A₁
inst_14 : LieAlgebra R L₁
inst_15 : Algebra R A₂
inst_16 : LieAlgebra R L₂
inst_17 : Algebra R A₃
inst_18 : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
f : L₁ →ₗ⁅σ₁₂⁆ L₂
g : L₂ →ₗ⁅σ₂₃⁆ L₃
x : A₁
x_1 : L₁
⊢ (g.comp f.toLieHom : (a : L₁) → L₃) (x • x_1) =
    HSMul.hSMul.{u_6, u_7, u_7} (α := A₃) (β := L₃) ((σ₂₃.comp σ₁₂ : (a : A₁) → A₃) x : A₃)
      ((g.comp f.toLieHom : (a : L₁) → L₃) x_1 : L₃)

Tactic:
simp [Hom.map_smul_apply]

Premises used: LieRinehartAlgebra.Hom.map_smul_apply
-- Module: Mathlib.Algebra.LieRinehartAlgebra.Defs
Goal:
R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst : CommRing R
inst_1 : CommRing A₁
inst_2 : LieRing L₁
inst_3 : Module A₁ L₁
inst_4 : LieRingModule L₁ A₁
inst_5 : CommRing A₂
inst_6 : LieRing L₂
inst_7 : Module A₂ L₂
inst_8 : LieRingModule L₂ A₂
inst_9 : CommRing A₃
inst_10 : LieRing L₃
inst_11 : Module A₃ L₃
inst_12 : LieRingModule L₃ A₃
inst_13 : Algebra R A₁
inst_14 : LieAlgebra R L₁
inst_15 : Algebra R A₂
inst_16 : LieAlgebra R L₂
inst_17 : Algebra R A₃
inst_18 : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
f : L₁ →ₗ⁅σ₁₂⁆ L₂
g : L₂ →ₗ⁅σ₂₃⁆ L₃
x : A₁
x_1 : L₁
⊢ Eq.{u_6 + 1} (α := A₃) ((σ₂₃.comp σ₁₂ : (a : A₁) → A₃) ⁅x_1, x⁆ : A₃)
    (Bracket.bracket.{u_7, u_6} (L := L₃) ((g.comp f.toLieHom : (a : L₁) → L₃) x_1 : L₃)
        ((σ₂₃.comp σ₁₂ : (a : A₁) → A₃) x) :
      A₃)

Tactic:
simp [f.apply_lie, g.apply_lie]

Premises used: LieRinehartAlgebra.Hom.apply_lie
-- Module: Mathlib.Algebra.LieRinehartAlgebra.Defs
Goal:
R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst : CommRing R
inst_1 : CommRing A₁
inst_2 : LieRing L₁
inst_3 : Module A₁ L₁
inst_4 : LieRingModule L₁ A₁
inst_5 : CommRing A₂
inst_6 : LieRing L₂
inst_7 : Module A₂ L₂
inst_8 : LieRingModule L₂ A₂
inst_9 : CommRing A₃
inst_10 : LieRing L₃
inst_11 : Module A₃ L₃
inst_12 : LieRingModule L₃ A₃
inst_13 : Algebra R A₁
inst_14 : LieAlgebra R L₁
inst_15 : Algebra R A₂
inst_16 : LieAlgebra R L₂
inst_17 : Algebra R A₃
inst_18 : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
x : A₁
x_1 : L₁
⊢ (LieHom.id : (a : L₁) → L₁) (x • x_1) =
    HSMul.hSMul (α := A₁) (β := L₁) ((AlgHom.id R A₁ : (a : A₁) → A₁) x : A₁) ((LieHom.id : (a : L₁) → L₁) x_1 : L₁)

Tactic:
simp
-- Module: Mathlib.Algebra.LieRinehartAlgebra.Defs
Goal:
R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst : CommRing R
inst_1 : CommRing A₁
inst_2 : LieRing L₁
inst_3 : Module A₁ L₁
inst_4 : LieRingModule L₁ A₁
inst_5 : CommRing A₂
inst_6 : LieRing L₂
inst_7 : Module A₂ L₂
inst_8 : LieRingModule L₂ A₂
inst_9 : CommRing A₃
inst_10 : LieRing L₃
inst_11 : Module A₃ L₃
inst_12 : LieRingModule L₃ A₃
inst_13 : Algebra R A₁
inst_14 : LieAlgebra R L₁
inst_15 : Algebra R A₂
inst_16 : LieAlgebra R L₂
inst_17 : Algebra R A₃
inst_18 : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
x : A₁
x_1 : L₁
⊢ Eq (α := A₁) ((AlgHom.id R A₁ : (a : A₁) → A₁) ⁅x_1, x⁆ : A₁)
    (Bracket.bracket (L := L₁) ((LieHom.id : (a : L₁) → L₁) x_1 : L₁) ((AlgHom.id R A₁ : (a : A₁) → A₁) x) : A₁)

Tactic:
simp
-- Module: Mathlib.Algebra.LieRinehartAlgebra.Defs
Goal:
R : Type u_1
A₁ : Type u_2
L₁ : Type u_3
A₂ : Type u_4
L₂ : Type u_5
A₃ : Type u_6
L₃ : Type u_7
inst : CommRing R
inst_1 : CommRing A₁
inst_2 : LieRing L₁
inst_3 : Module A₁ L₁
inst_4 : LieRingModule L₁ A₁
inst_5 : CommRing A₂
inst_6 : LieRing L₂
inst_7 : Module A₂ L₂
inst_8 : LieRingModule L₂ A₂
inst_9 : CommRing A₃
inst_10 : LieRing L₃
inst_11 : Module A₃ L₃
inst_12 : LieRingModule L₃ A₃
inst_13 : Algebra R A₁
inst_14 : LieAlgebra R L₁
inst_15 : Algebra R A₂
inst_16 : LieAlgebra R L₂
inst_17 : Algebra R A₃
inst_18 : LieAlgebra R L₃
σ₁₂ : A₁ →ₐ[R] A₂
σ₂₃ : A₂ →ₐ[R] A₃
inst_19 : LieRinehartRing A₁ L₁
inst_20 : LieRinehartAlgebra R A₁ L₁
x : L₁
a b : A₁
⊢ ((((LieModule.toEnd R L₁ A₁ : LieHom.{u_1, u_3, u_2} R L₁ (Module.End R A₁)) : (a : L₁) → Module.End R A₁) x :
          Module.End R A₁) :
        (a : A₁) → A₁)
      (a * b) =
    HSMul.hSMul (β := A₁) a
        (((((LieModule.toEnd R L₁ A₁ : LieHom.{u_1, u_3, u_2} R L₁ (Module.End R A₁)) : (a : L₁) → Module.End R A₁) x :
                Module.End R A₁) :
              (a : A₁) → A₁)
            b :
          A₁) +
      HSMul.hSMul (β := A₁) b
        (((((LieModule.toEnd R L₁ A₁ : LieHom.{u_1, u_3, u_2} R L₁ (Module.End R A₁)) : (a : L₁) → Module.End R A₁) x :
                Module.End R A₁) :
              (a : A₁) → A₁)
            a :
          A₁)

Tactic:
simp [mul_comm b]

Premises used: mul_comm