awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.DifferentialRing (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Differential A
R : Type u_2
R₂ : Type u_3
inst_2 : CommRing R
inst_3 : CommRing R₂
inst_4 : Differential R₂
inst_5 : Algebra A R
inst_6 : Algebra A R₂
inst_7 : DifferentialAlgebra A R₂
h : R ≃ₐ[A] R₂
this : Differential R := Differential.equiv h.toRingEquiv
a : A
⊢ Eq (α := R)
    ((h.toRingEquiv.symm.toAddMonoidHom.toIntLinearMap ∘ₗ
            (↑Differential.deriv : R₂ →ₗ[ℤ] R₂) ∘ₗ h.toRingEquiv.toAddMonoidHom.toIntLinearMap :
          (a : R) → R)
        ((algebraMap A R : (a : A) → R) a : R) :
      R)
    ((algebraMap A R : (a : A) → R) (a′ : A) : R)
have simp : Eq.{u_2 + 1} (α := R) ((h.toRingEquiv.symm : (a : R₂) → R) ((algebraMap A R₂ : (a : A) → R₂) (a′ : A) : R₂) : R)
  ((algebraMap A R : (a : A) → R) (a′ : A) : R)
Tactic: simp only [RingHom.toAddMonoidHom_eq_coe,
      RingEquiv.toRingHom_eq_coe, AlgEquiv.toRingEquiv_toRingHom, LinearMap.coe_comp,
      AddMonoidHom.coe_toIntLinearMap, AddMonoidHom.coe_coe, RingHom.coe_coe, Derivation.coeFn_coe,
      Function.comp_apply, AlgEquiv.commutes, deriv_algebraMap]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Lie (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1_1 D2_1 : Derivation R A A
a_1 : A
D1 D2 : Derivation R A A
a b : A
⊢ (⁅(↑D1 : A →ₗ[R] A), (↑D2 : A →ₗ[R] A)⁆ : (a : A) → A) (a * b) =
    HSMul.hSMul (β := A) a ((⁅(↑D1 : A →ₗ[R] A), (↑D2 : A →ₗ[R] A)⁆ : (a : A) → A) b : A) +
      HSMul.hSMul (β := A) b ((⁅(↑D1 : A →ₗ[R] A), (↑D2 : A →ₗ[R] A)⁆ : (a : A) → A) a : A)
have simp : HMul.hMul (β := A) a ((D1 : (a : A) → A) ((D2 : (a : A) → A) b : A) : A) +
        HMul.hMul (α := A) (β := A) ((D2 : (a : A) → A) b : A) ((D1 : (a : A) → A) a : A) +
      (HMul.hMul (β := A) b ((D1 : (a : A) → A) ((D2 : (a : A) → A) a : A) : A) +
        HMul.hMul (α := A) (β := A) ((D2 : (a : A) → A) a : A) ((D1 : (a : A) → A) b : A)) -
    (HMul.hMul (β := A) a ((D2 : (a : A) → A) ((D1 : (a : A) → A) b : A) : A) +
        HMul.hMul (α := A) (β := A) ((D1 : (a : A) → A) b : A) ((D2 : (a : A) → A) a : A) +
      (HMul.hMul (β := A) b ((D2 : (a : A) → A) ((D1 : (a : A) → A) a : A) : A) +
        HMul.hMul (α := A) (β := A) ((D1 : (a : A) → A) a : A) ((D2 : (a : A) → A) b : A))) =
  a *
      HSub.hSub (α := A) (β := A) ((D1 : (a : A) → A) ((D2 : (a : A) → A) b : A) : A)
        ((D2 : (a : A) → A) ((D1 : (a : A) → A) b : A) : A) +
    b *
      HSub.hSub (α := A) (β := A) ((D1 : (a : A) → A) ((D2 : (a : A) → A) a : A) : A)
        ((D2 : (a : A) → A) ((D1 : (a : A) → A) a : A) : A)
Tactic: simp only [Ring.lie_def, map_add, smul_eq_mul, Module.End.mul_apply, leibniz,
        coeFn_coe, LinearMap.sub_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Lie (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
a : A
d e f : Derivation R A A
⊢ ⁅d + e, f⁆ = ⁅d, f⁆ + ⁅e, f⁆
have H : ∀ (a : A), Eq (α := A) ((⁅d + e, f⁆ : (a : A) → A) a : A) ((⁅d, f⁆ + ⁅e, f⁆ : (a : A) → A) a : A)
Tactic: ext a
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Lie (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
a_1 : A
d e f : Derivation R A A
a : A
⊢ Eq (α := A) ((⁅d + e, f⁆ : (a : A) → A) a : A) ((⁅d, f⁆ + ⁅e, f⁆ : (a : A) → A) a : A)
have H : HAdd.hAdd (α := A) (β := A) ((d : (a : A) → A) ((f : (a : A) → A) a : A) : A)
      ((e : (a : A) → A) ((f : (a : A) → A) a : A) : A) -
    HAdd.hAdd (α := A) (β := A) ((f : (a : A) → A) ((d : (a : A) → A) a : A) : A)
      ((f : (a : A) → A) ((e : (a : A) → A) a : A) : A) =
  HSub.hSub (α := A) (β := A) ((d : (a : A) → A) ((f : (a : A) → A) a : A) : A)
      ((f : (a : A) → A) ((d : (a : A) → A) a : A) : A) +
    HSub.hSub (α := A) (β := A) ((e : (a : A) → A) ((f : (a : A) → A) a : A) : A)
      ((f : (a : A) → A) ((e : (a : A) → A) a : A) : A)
Tactic: simp only [commutator_apply, add_apply, map_add]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Lie (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
a : A
d e f : Derivation R A A
⊢ ⁅d, e + f⁆ = ⁅d, e⁆ + ⁅d, f⁆
have H : ∀ (a : A), Eq (α := A) ((⁅d, e + f⁆ : (a : A) → A) a : A) ((⁅d, e⁆ + ⁅d, f⁆ : (a : A) → A) a : A)
Tactic: ext a
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Lie (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
a_1 : A
d e f : Derivation R A A
a : A
⊢ Eq (α := A) ((⁅d, e + f⁆ : (a : A) → A) a : A) ((⁅d, e⁆ + ⁅d, f⁆ : (a : A) → A) a : A)
have H : HAdd.hAdd (α := A) (β := A) ((d : (a : A) → A) ((e : (a : A) → A) a : A) : A)
      ((d : (a : A) → A) ((f : (a : A) → A) a : A) : A) -
    HAdd.hAdd (α := A) (β := A) ((e : (a : A) → A) ((d : (a : A) → A) a : A) : A)
      ((f : (a : A) → A) ((d : (a : A) → A) a : A) : A) =
  HSub.hSub (α := A) (β := A) ((d : (a : A) → A) ((e : (a : A) → A) a : A) : A)
      ((e : (a : A) → A) ((d : (a : A) → A) a : A) : A) +
    HSub.hSub (α := A) (β := A) ((d : (a : A) → A) ((f : (a : A) → A) a : A) : A)
      ((f : (a : A) → A) ((d : (a : A) → A) a : A) : A)
Tactic: simp only [commutator_apply, add_apply, map_add]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Lie (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
a : A
d : Derivation R A A
⊢ ⁅d, d⁆ = 0
have H : ∀ (a : A), Eq (α := A) ((⁅d, d⁆ : (a : A) → A) a : A) ((0 : (a : A) → A) a : A)
Tactic: ext a
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Lie (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
a_1 : A
d : Derivation R A A
a : A
⊢ Eq (α := A) ((⁅d, d⁆ : (a : A) → A) a : A) ((0 : (a : A) → A) a : A)
have H : HSub.hSub (α := A) (β := A) ((d : (a : A) → A) ((d : (a : A) → A) a : A) : A)
    ((d : (a : A) → A) ((d : (a : A) → A) a : A) : A) =
  (0 : (a : A) → A) a
Tactic: simp only [commutator_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Lie (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
a_1 : A
d : Derivation R A A
a : A
⊢ HSub.hSub (α := A) (β := A) ((d : (a : A) → A) ((d : (a : A) → A) a : A) : A)
      ((d : (a : A) → A) ((d : (a : A) → A) a : A) : A) =
    (0 : (a : A) → A) a
have H : Eq (α := A) (0 : A) ((0 : (a : A) → A) a : A)
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Lie (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
a : A
d e f : Derivation R A A
⊢ ⁅d, ⁅e, f⁆⁆ = ⁅⁅d, e⁆, f⁆ + ⁅e, ⁅d, f⁆⁆
have H : ∀ (a : A), Eq (α := A) ((⁅d, ⁅e, f⁆⁆ : (a : A) → A) a : A) ((⁅⁅d, e⁆, f⁆ + ⁅e, ⁅d, f⁆⁆ : (a : A) → A) a : A)
Tactic: ext a
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Lie (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
a_1 : A
d e f : Derivation R A A
a : A
⊢ Eq (α := A) ((⁅d, ⁅e, f⁆⁆ : (a : A) → A) a : A) ((⁅⁅d, e⁆, f⁆ + ⁅e, ⁅d, f⁆⁆ : (a : A) → A) a : A)
have H : HSub.hSub (α := A) (β := A) ((d : (a : A) → A) ((e : (a : A) → A) ((f : (a : A) → A) a : A) : A) : A)
      ((d : (a : A) → A) ((f : (a : A) → A) ((e : (a : A) → A) a : A) : A) : A) -
    HSub.hSub (α := A) (β := A) ((e : (a : A) → A) ((f : (a : A) → A) ((d : (a : A) → A) a : A) : A) : A)
      ((f : (a : A) → A) ((e : (a : A) → A) ((d : (a : A) → A) a : A) : A) : A) =
  HSub.hSub (α := A) (β := A) ((d : (a : A) → A) ((e : (a : A) → A) ((f : (a : A) → A) a : A) : A) : A)
        ((e : (a : A) → A) ((d : (a : A) → A) ((f : (a : A) → A) a : A) : A) : A) -
      HSub.hSub (α := A) (β := A) ((f : (a : A) → A) ((d : (a : A) → A) ((e : (a : A) → A) a : A) : A) : A)
        ((f : (a : A) → A) ((e : (a : A) → A) ((d : (a : A) → A) a : A) : A) : A) +
    (HSub.hSub (α := A) (β := A) ((e : (a : A) → A) ((d : (a : A) → A) ((f : (a : A) → A) a : A) : A) : A)
        ((e : (a : A) → A) ((f : (a : A) → A) ((d : (a : A) → A) a : A) : A) : A) -
      HSub.hSub (α := A) (β := A) ((d : (a : A) → A) ((f : (a : A) → A) ((e : (a : A) → A) a : A) : A) : A)
        ((f : (a : A) → A) ((d : (a : A) → A) ((e : (a : A) → A) a : A) : A) : A))
Tactic: simp only [commutator_apply, add_apply, map_sub]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Lie (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
a : A
r : R
d e : Derivation R A A
⊢ ⁅d, r • e⁆ = r • ⁅d, e⁆
have H : ∀ (a : A), Eq (α := A) ((⁅d, r • e⁆ : (a : A) → A) a : A) ((r • ⁅d, e⁆ : (a : A) → A) a : A)
Tactic: ext a
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Lie (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
a : A
x x_1 : Derivation R A A
x_2 : A
⊢ (x : (a : A) → A) ((x_1 : (a : A) → A) x_2 : A) =
    HAdd.hAdd (α := A) (β := A) ((⁅x, x_1⁆ : (a : A) → A) x_2 : A) ((x_1 : (a : A) → A) ((x : (a : A) → A) x_2 : A) : A)
have rw : (x : (a : A) → A) ((x_1 : (a : A) → A) x_2 : A) =
  HAdd.hAdd (β := A)
    (HSub.hSub (α := A) (β := A) ((x : (a : A) → A) ((x_1 : (a : A) → A) x_2 : A) : A)
      ((x_1 : (a : A) → A) ((x : (a : A) → A) x_2 : A) : A))
    ((x_1 : (a : A) → A) ((x : (a : A) → A) x_2 : A) : A)
Tactic: rw [commutator_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Lie (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
D1 D2 : Derivation R A A
a : A
A' : Type u_3
inst_3 : CommRing A'
inst_4 : Algebra R A'
inst_5 : Algebra A A'
inst_6 : IsScalarTower R A A'
x y : Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A)
hx :
  Membership.mem (γ := Set (Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A)))
    {x : Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A) |
      Eq (α := Derivation R A A')
        (((compAlgebraMapL R A A' A' : Derivation R A' A' →ₗ[A'] Derivation R A A') :
              (a : Derivation R A' A') → Derivation R A A')
            x.1 :
          Derivation R A A')
        (((LinearMap.compDer (AlgHom.toLinearMap (Algebra.ofId A A')) : Derivation R A A →ₗ[A] Derivation R A A') :
              (a : Derivation R A A) → Derivation R A A')
            x.2 :
          Derivation R A A')}
    x
hy :
  Membership.mem (γ := Set (Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A)))
    {x : Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A) |
      Eq (α := Derivation R A A')
        (((compAlgebraMapL R A A' A' : Derivation R A' A' →ₗ[A'] Derivation R A A') :
              (a : Derivation R A' A') → Derivation R A A')
            x.1 :
          Derivation R A A')
        (((LinearMap.compDer (AlgHom.toLinearMap (Algebra.ofId A A')) : Derivation R A A →ₗ[A] Derivation R A A') :
              (a : Derivation R A A) → Derivation R A A')
            x.2 :
          Derivation R A A')}
    y
⊢ Membership.mem (γ := Set (Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A)))
    {x : Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A) |
      Eq (α := Derivation R A A')
        (((compAlgebraMapL R A A' A' : Derivation R A' A' →ₗ[A'] Derivation R A A') :
              (a : Derivation R A' A') → Derivation R A A')
            x.1 :
          Derivation R A A')
        (((LinearMap.compDer (AlgHom.toLinearMap (Algebra.ofId A A')) : Derivation R A A →ₗ[A] Derivation R A A') :
              (a : Derivation R A A) → Derivation R A A')
            x.2 :
          Derivation R A A')}
    ⁅x, y⁆
have hxx : ∀ (a : A),
  Eq.{u_3 + 1} (α := A')
    ((fun (f : Derivation R A A') ↦ ((f : (a : A) → A') a : A'))
      (((compAlgebraMapL R A A' A' : Derivation R A' A' →ₗ[A'] Derivation R A A') :
          (a : Derivation R A' A') → Derivation R A A')
        x.1))
    ((fun (f : Derivation R A A') ↦ ((f : (a : A) → A') a : A'))
      (((LinearMap.compDer (AlgHom.toLinearMap (Algebra.ofId A A')) : Derivation R A A →ₗ[A] Derivation R A A') :
          (a : Derivation R A A) → Derivation R A A')
        x.2))
Tactic: have hxx (a : A) := congrArg (fun f => f a) hx
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Lie (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
A' : Type u_3
inst_3 : CommRing A'
inst_4 : Algebra R A'
inst_5 : Algebra A A'
inst_6 : IsScalarTower R A A'
x : Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A)
⊢ Membership.mem (γ := LieSubalgebra R (Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A))) (couple R A A') x ↔
    Eq (α := A → A') (Function.comp (β := A') (⇑x.1 : (a : A') → A') (⇑(Algebra.ofId A A') : (a : A) → A'))
      (Function.comp (β := A) (⇑(Algebra.ofId A A') : (a : A) → A') (⇑x.2 : (a : A) → A))
have mp : Membership.mem (γ := LieSubalgebra R (Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A))) (couple R A A') x →
  Eq (α := A → A') (Function.comp (β := A') (⇑x.1 : (a : A') → A') (⇑(Algebra.ofId A A') : (a : A) → A'))
    (Function.comp (β := A) (⇑(Algebra.ofId A A') : (a : A) → A') (⇑x.2 : (a : A) → A))
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Lie (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
A' : Type u_3
inst_3 : CommRing A'
inst_4 : Algebra R A'
inst_5 : Algebra A A'
inst_6 : IsScalarTower R A A'
x : Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A)
mp :
  Membership.mem (γ := LieSubalgebra R (Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A))) (couple R A A') x →
    Eq (α := A → A') (Function.comp (β := A') (⇑x.1 : (a : A') → A') (⇑(Algebra.ofId A A') : (a : A) → A'))
      (Function.comp (β := A) (⇑(Algebra.ofId A A') : (a : A) → A') (⇑x.2 : (a : A) → A))
⊢ Membership.mem (γ := LieSubalgebra R (Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A))) (couple R A A') x ↔
    Eq (α := A → A') (Function.comp (β := A') (⇑x.1 : (a : A') → A') (⇑(Algebra.ofId A A') : (a : A) → A'))
      (Function.comp (β := A) (⇑(Algebra.ofId A A') : (a : A) → A') (⇑x.2 : (a : A) → A))
have mpr : Eq (α := A → A') (Function.comp (β := A') (⇑x.1 : (a : A') → A') (⇑(Algebra.ofId A A') : (a : A) → A'))
    (Function.comp (β := A) (⇑(Algebra.ofId A A') : (a : A) → A') (⇑x.2 : (a : A) → A)) →
  Membership.mem (γ := LieSubalgebra R (Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A))) (couple R A A') x
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Lie (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
A' : Type u_3
inst_3 : CommRing A'
inst_4 : Algebra R A'
inst_5 : Algebra A A'
inst_6 : IsScalarTower R A A'
x : Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A)
hx : Membership.mem (γ := LieSubalgebra R (Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A))) (couple R A A') x
⊢ Eq (α := A → A') (Function.comp (β := A') (⇑x.1 : (a : A') → A') (⇑(Algebra.ofId A A') : (a : A) → A'))
    (Function.comp (β := A) (⇑(Algebra.ofId A A') : (a : A) → A') (⇑x.2 : (a : A) → A))
have mp : ∀ (a : A),
  Eq (α := A') (Function.comp (β := A') (⇑x.1 : (a : A') → A') (⇑(Algebra.ofId A A') : (a : A) → A') a)
    (Function.comp (β := A) (⇑(Algebra.ofId A A') : (a : A) → A') (⇑x.2 : (a : A) → A) a)
Tactic: ext a
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.Lie (goal)
Goal:
R : Type u_1
inst : CommRing R
A : Type u_2
inst_1 : CommRing A
inst_2 : Algebra R A
A' : Type u_3
inst_3 : CommRing A'
inst_4 : Algebra R A'
inst_5 : Algebra A A'
inst_6 : IsScalarTower R A A'
x : Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A)
hx :
  Eq (α := A → A') (Function.comp (β := A') (⇑x.1 : (a : A') → A') (⇑(Algebra.ofId A A') : (a : A) → A'))
    (Function.comp (β := A) (⇑(Algebra.ofId A A') : (a : A) → A') (⇑x.2 : (a : A) → A))
⊢ Membership.mem (γ := LieSubalgebra R (Prod.{u_3, u_2} (Derivation R A' A') (Derivation R A A))) (couple R A A') x
have mpr : ∀ (a : A),
  Eq.{u_3 + 1} (α := A')
    (((((compAlgebraMapL R A A' A' : Derivation R A' A' →ₗ[A'] Derivation R A A') :
                (a : Derivation R A' A') → Derivation R A A')
              x.1 :
            Derivation R A A') :
          (a : A) → A')
        a :
      A')
    (((((LinearMap.compDer (AlgHom.toLinearMap (Algebra.ofId A A')) : Derivation R A A →ₗ[A] Derivation R A A') :
                (a : Derivation R A A) → Derivation R A A')
              x.2 :
            Derivation R A A') :
          (a : A) → A')
        a :
      A')
Tactic: ext a
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.MapCoeffs (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : AddCommGroup M
inst_4 : Module A M
inst_5 : Module R M
d : Derivation R A M
p q : A[X]
⊢ (PolynomialModule.map A (↑d : A →ₗ[R] M) ∘ₗ
          (↑(LinearEquiv.symm PolynomialModule.equivPolynomial) : A[X] →ₗ[R] PolynomialModule R A) :
        (a : A[X]) → PolynomialModule A M)
      (p * q) =
    HSMul.hSMul (β := PolynomialModule A M) p
        ((PolynomialModule.map A (↑d : A →ₗ[R] M) ∘ₗ
                (↑(LinearEquiv.symm PolynomialModule.equivPolynomial) : A[X] →ₗ[R] PolynomialModule R A) :
              (a : A[X]) → PolynomialModule A M)
            q :
          PolynomialModule A M) +
      HSMul.hSMul (β := PolynomialModule A M) q
        ((PolynomialModule.map A (↑d : A →ₗ[R] M) ∘ₗ
                (↑(LinearEquiv.symm PolynomialModule.equivPolynomial) : A[X] →ₗ[R] PolynomialModule R A) :
              (a : A[X]) → PolynomialModule A M)
            p :
          PolynomialModule A M)
have dsimp : (PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
    ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A) (p * q)) =
  HSMul.hSMul (β := PolynomialModule A M) p
      ((PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
          ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A) q) :
        PolynomialModule A M) +
    HSMul.hSMul (β := PolynomialModule A M) q
      ((PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
          ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A) p) :
        PolynomialModule A M)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.MapCoeffs (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : AddCommGroup M
inst_4 : Module A M
inst_5 : Module R M
d : Derivation R A M
n : ℕ
a : A
m : ℕ
b : A
⊢ (PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
      ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A)
        (HMul.hMul (α := A[X]) (β := A[X]) ((monomial n : (a : A) → A[X]) a : A[X])
          ((monomial m : (a : A) → A[X]) b : A[X]))) =
    HSMul.hSMul (α := A[X]) (β := PolynomialModule A M) ((monomial n : (a : A) → A[X]) a : A[X])
        ((PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
            ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A)
              ((monomial m : (a : A) → A[X]) b)) :
          PolynomialModule A M) +
      HSMul.hSMul (α := A[X]) (β := PolynomialModule A M) ((monomial m : (a : A) → A[X]) b : A[X])
        ((PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
            ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A)
              ((monomial n : (a : A) → A[X]) a)) :
          PolynomialModule A M)
have monomial : ∀ (i : ℕ),
  Eq (α := M)
    ((((PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
              ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A)
                (HMul.hMul (α := A[X]) (β := A[X]) ((monomial n : (a : A) → A[X]) a : A[X])
                  ((monomial m : (a : A) → A[X]) b : A[X]))) :
            PolynomialModule A M) :
          (a : ℕ) → M)
        i :
      M)
    ((HSMul.hSMul (α := A[X]) (β := PolynomialModule A M) ((monomial n : (a : A) → A[X]) a : A[X])
              ((PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
                  ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A)
                    ((monomial m : (a : A) → A[X]) b)) :
                PolynomialModule A M) +
            HSMul.hSMul (α := A[X]) (β := PolynomialModule A M) ((monomial m : (a : A) → A[X]) b : A[X])
              ((PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
                  ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A)
                    ((monomial n : (a : A) → A[X]) a)) :
                PolynomialModule A M) :
          (a : ℕ) → M)
        i :
      M)
Tactic: refine Finsupp.ext fun i ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.Derivation.MapCoeffs (goal)
Goal:
R : Type u_1
A : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
inst_3 : AddCommGroup M
inst_4 : Module A M
inst_5 : Module R M
d : Derivation R A M
n : ℕ
a : A
m : ℕ
b : A
i : ℕ
⊢ Eq (α := M)
    ((((PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
              ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A)
                (HMul.hMul (α := A[X]) (β := A[X]) ((monomial n : (a : A) → A[X]) a : A[X])
                  ((monomial m : (a : A) → A[X]) b : A[X]))) :
            PolynomialModule A M) :
          (a : ℕ) → M)
        i :
      M)
    ((HSMul.hSMul (α := A[X]) (β := PolynomialModule A M) ((monomial n : (a : A) → A[X]) a : A[X])
              ((PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
                  ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A)
                    ((monomial m : (a : A) → A[X]) b)) :
                PolynomialModule A M) +
            HSMul.hSMul (α := A[X]) (β := PolynomialModule A M) ((monomial m : (a : A) → A[X]) b : A[X])
              ((PolynomialModule.map A (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
                  ((LinearEquiv.symm PolynomialModule.equivPolynomial : (a : A[X]) → PolynomialModule R A)
                    ((monomial n : (a : A) → A[X]) a)) :
                PolynomialModule A M) :
          (a : ℕ) → M)
        i :
      M)
have monomial : Eq (α := M)
  ((((Finsupp.mapRange.linearMap (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
            (HMul.hMul (α := A[X]) (β := A[X]) ((monomial n : (a : A) → A[X]) a : A[X])
                ((monomial m : (a : A) → A[X]) b : A[X])).toFinsupp :
          PolynomialModule A M) :
        (a : ℕ) → M)
      i :
    M)
  ((HSMul.hSMul (α := A[X]) (β := PolynomialModule A M) ((monomial n : (a : A) → A[X]) a : A[X])
            ((Finsupp.mapRange.linearMap (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
                (toFinsupp ((monomial m : (a : A) → A[X]) b)) :
              PolynomialModule A M) +
          HSMul.hSMul (α := A[X]) (β := PolynomialModule A M) ((monomial m : (a : A) → A[X]) b : A[X])
            ((Finsupp.mapRange.linearMap (↑d : A →ₗ[R] M) : (a : PolynomialModule R A) → PolynomialModule A M)
                (toFinsupp ((monomial n : (a : A) → A[X]) a)) :
              PolynomialModule A M) :
        (a : ℕ) → M)
      i :
    M)
Tactic: dsimp [PolynomialModule.equivPolynomial, PolynomialModule.map]