awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
a : R
rw :
  Eq (α := RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
    ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
        ((C : (a : R) → MvPolynomial (ℕ × M) R) a) :
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
    ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
        ((C : (a : R) → MvPolynomial (ℕ × M) R) a) :
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
rw₁ :
  Eq (α := RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
    ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
        ((C : (a : R) → MvPolynomial (ℕ × M) R) a) :
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
    ((let __src : MvPolynomial.{u_2, u_1} (ℕ × M) R →+* RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M) :=
            mkRingHom (Rel R M);
          { toRingHom := __src, commutes' := ⋯ } :
          (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
        ((C : (a : R) → MvPolynomial (ℕ × M) R) a) :
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
rw₂ rw₃ :
  Eq (α := RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
    ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
        ((C : (a : R) → MvPolynomial (ℕ × M) R) a) :
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
    ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
        ((C : (a : R) → MvPolynomial (ℕ × M) R) a) :
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
⊢ Eq (α := RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
    ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
        ((C : (a : R) → MvPolynomial (ℕ × M) R) a) :
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
    ((algebraMap R (DividedPowerAlgebra R M) : (a : R) → DividedPowerAlgebra R M) a : DividedPowerAlgebra R M)

Tactic:
rw [← mkAlgHom_C, mkAlgHom, AlgHom.coe_mk]

Premises used: AlgHom.coe_mk, RingQuot.mkAlgHom, DividedPowerAlgebra.mkAlgHom_C
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
n : ℕ
m : M
⊢ Eq (α := DividedPowerAlgebra R M) (dp R n m)
    ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X (n, m)))

Tactic:
rfl

Premises used: DividedPowerAlgebra.dp, rfl
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
P : DividedPowerAlgebra R M → Prop
f : DividedPowerAlgebra R M
h_C :
  ∀ (a : R),
    P
      ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
        ((C : (a : R) → MvPolynomial (ℕ × M) R) a))
h_add : ∀ (f g : DividedPowerAlgebra R M), P f → P g → P (f + g)
h_dp : ∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * dp R n m)
obtain :
  ∀ (F : MvPolynomial.{u_2, u_1} (ℕ × M) R)
    (hf : (mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) F = f), P f
⊢ P f

Tactic:
obtain ⟨F, hf⟩ := RingQuot.mkRingHom_surjective (DividedPowerAlgebra.Rel R M) f

Premises used: DividedPowerAlgebra.Rel, RingQuot.mkRingHom_surjective
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
P : DividedPowerAlgebra R M → Prop
f : DividedPowerAlgebra R M
h_C :
  ∀ (a : R),
    P
      ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
        ((C : (a : R) → MvPolynomial (ℕ × M) R) a))
h_add : ∀ (f g : DividedPowerAlgebra R M), P f → P g → P (f + g)
h_dp : ∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * dp R n m)
F : MvPolynomial.{u_2, u_1} (ℕ × M) R
hf : (mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) F = f
rw : P ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) F)
⊢ P f

Tactic:
rw [← hf]
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
P : DividedPowerAlgebra R M → Prop
h_C :
  ∀ (a : R),
    P
      ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
        ((C : (a : R) → MvPolynomial (ℕ × M) R) a))
h_add : ∀ (f g : DividedPowerAlgebra R M), P f → P g → P (f + g)
h_dp : ∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * dp R n m)
a : R
f : DividedPowerAlgebra R M
hf :
  (mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) ((C : (a : R) → MvPolynomial (ℕ × M) R) a) =
    f
⊢ P
    ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
      ((C : (a : R) → MvPolynomial (ℕ × M) R) a))

Tactic:
h_C a
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
P : DividedPowerAlgebra R M → Prop
h_C :
  ∀ (a : R),
    P
      ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
        ((C : (a : R) → MvPolynomial (ℕ × M) R) a))
h_add : ∀ (f g : DividedPowerAlgebra R M), P f → P g → P (f + g)
h_dp : ∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * dp R n m)
a : R
f : DividedPowerAlgebra R M
hf :
  (mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) ((C : (a : R) → MvPolynomial (ℕ × M) R) a) =
    f
h :
  Eq (α := DividedPowerAlgebra R M)
    ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
        ((C : (a : R) → MvPolynomial (ℕ × M) R) a) :
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
    ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
        ((C : (a : R) → MvPolynomial (ℕ × M) R) a) :
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
⊢ P
    ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
      ((C : (a : R) → MvPolynomial (ℕ × M) R) a))

Tactic:
convert! h_C a using 1
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
P : DividedPowerAlgebra R M → Prop
h_C :
  ∀ (a : R),
    P
      ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
        ((C : (a : R) → MvPolynomial (ℕ × M) R) a))
h_add : ∀ (f g : DividedPowerAlgebra R M), P f → P g → P (f + g)
h_dp : ∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * dp R n m)
a : R
f : DividedPowerAlgebra R M
hf :
  (mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) ((C : (a : R) → MvPolynomial (ℕ × M) R) a) =
    f
h :
  Eq (α := DividedPowerAlgebra R M)
    ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
        ((C : (a : R) → MvPolynomial (ℕ × M) R) a) :
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
    ((let __src : MvPolynomial.{u_2, u_1} (ℕ × M) R →+* RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M) :=
            mkRingHom (Rel R M);
          { toRingHom := __src, commutes' := ⋯ } :
          (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
        ((C : (a : R) → MvPolynomial (ℕ × M) R) a) :
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
h₁ h₂ :
  Eq (α := DividedPowerAlgebra R M)
    ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
        ((C : (a : R) → MvPolynomial (ℕ × M) R) a) :
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
    ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
        ((C : (a : R) → MvPolynomial (ℕ × M) R) a) :
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
⊢ Eq (α := DividedPowerAlgebra R M)
    ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
        ((C : (a : R) → MvPolynomial (ℕ × M) R) a) :
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
    ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
        ((C : (a : R) → MvPolynomial (ℕ × M) R) a) :
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))

Tactic:
rw [mkAlgHom, AlgHom.coe_mk]

Premises used: AlgHom.coe_mk, RingQuot.mkAlgHom
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
P : DividedPowerAlgebra R M → Prop
h_C :
  ∀ (a : R),
    P
      ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
        ((C : (a : R) → MvPolynomial (ℕ × M) R) a))
h_add : ∀ (f g : DividedPowerAlgebra R M), P f → P g → P (f + g)
h_dp : ∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * dp R n m)
g1 g2 : MvPolynomial.{u_2, u_1} (ℕ × M) R
hg1 :
  ∀ (f : DividedPowerAlgebra R M)
    (hf : (mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) g1 = f),
    P ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) g1)
hg2 :
  ∀ (f : DividedPowerAlgebra R M)
    (hf : (mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) g2 = f),
    P ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) g2)
f : DividedPowerAlgebra R M
hf : (mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (g1 + g2) = f
add :
  P
    (HAdd.hAdd (α := RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M)) (β :=
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
      ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) g1 :
        RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
      ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) g2 :
        RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M)))
⊢ P ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (g1 + g2))

Tactic:
rw [map_add]

Premises used: map_add
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
P : DividedPowerAlgebra R M → Prop
h_C :
  ∀ (a : R),
    P
      ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
        ((C : (a : R) → MvPolynomial (ℕ × M) R) a))
h_add : ∀ (f g : DividedPowerAlgebra R M), P f → P g → P (f + g)
h_dp : ∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * dp R n m)
g1 g2 : MvPolynomial.{u_2, u_1} (ℕ × M) R
hg1 :
  ∀ (f : DividedPowerAlgebra R M)
    (hf : (mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) g1 = f),
    P ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) g1)
hg2 :
  ∀ (f : DividedPowerAlgebra R M)
    (hf : (mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) g2 = f),
    P ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) g2)
f : DividedPowerAlgebra R M
hf : (mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (g1 + g2) = f
⊢ P
    (HAdd.hAdd (α := RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M)) (β :=
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
      ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) g1 :
        RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
      ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) g2 :
        RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M)))

Tactic:
h_add _ _ (hg1 ((mkRingHom (Rel R M)) g1) rfl) (hg2 ((mkRingHom (Rel R M)) g2) rfl)

Premises used: DividedPowerAlgebra.Rel, RingQuot.mkRingHom, DFunLike.coe, rfl
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
P : DividedPowerAlgebra R M → Prop
h_C :
  ∀ (a : R),
    P
      ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
        ((C : (a : R) → MvPolynomial (ℕ × M) R) a))
h_add : ∀ (f g : DividedPowerAlgebra R M), P f → P g → P (f + g)
h_dp : ∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * dp R n m)
g1 g2 : MvPolynomial.{u_2, u_1} (ℕ × M) R
hg1 :
  ∀ (f : DividedPowerAlgebra R M)
    (hf : (mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) g1 = f),
    P ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) g1)
hg2 :
  ∀ (f : DividedPowerAlgebra R M)
    (hf : (mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) g2 = f),
    P ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) g2)
f : DividedPowerAlgebra R M
hf : (mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (g1 + g2) = f
⊢ P
    (HAdd.hAdd (α := RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M)) (β :=
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
      ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) g1 :
        RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
      ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) g2 :
        RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M)))

Tactic:
exact h_add _ _ (hg1 ((mkRingHom (Rel R M)) g1) rfl) (hg2 ((mkRingHom (Rel R M)) g2) rfl)

Premises used: DividedPowerAlgebra.Rel, RingQuot.mkRingHom, DFunLike.coe, rfl
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
P : DividedPowerAlgebra R M → Prop
h_C :
  ∀ (a : R),
    P
      ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
        ((C : (a : R) → MvPolynomial (ℕ × M) R) a))
h_add : ∀ (f g : DividedPowerAlgebra R M), P f → P g → P (f + g)
h_dp : ∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * dp R n m)
g : MvPolynomial.{u_2, u_1} (ℕ × M) R
nm : ℕ × M
h :
  ∀ (f : DividedPowerAlgebra R M)
    (hf : (mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) g = f),
    P ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) g)
f : DividedPowerAlgebra R M
hf : (mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (g * X nm) = f
⊢ Eq (α := RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
    ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X nm) :
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
    (dp R nm.1 nm.2 : DividedPowerAlgebra R M)

Tactic:
simp only [dp_def, Prod.mk.eta, mkAlgHom, AlgHom.coe_mk]

Premises used: AlgHom.coe_mk, RingQuot.mkAlgHom, DividedPowerAlgebra.dp_def, Prod.mk.eta
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
P : DividedPowerAlgebra R M → Prop
h_C :
  ∀ (a : R),
    P
      ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
        ((C : (a : R) → MvPolynomial (ℕ × M) R) a))
h_add : ∀ (f g : DividedPowerAlgebra R M), P f → P g → P (f + g)
h_dp : ∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * dp R n m)
g : MvPolynomial.{u_2, u_1} (ℕ × M) R
nm : ℕ × M
h :
  ∀ (f : DividedPowerAlgebra R M)
    (hf : (mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) g = f),
    P ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) g)
f : DividedPowerAlgebra R M
hf : (mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (g * X nm) = f
mul_X :
  ∀
    (h' :
      Eq (α := RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
        ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X nm) :
          RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
        (dp R nm.1 nm.2 : DividedPowerAlgebra R M)),
    P ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (g * X nm))
⊢ P ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (g * X nm))

Tactic:
have h' : (mkRingHom (Rel R M)) (X nm) = dp R nm.1 nm.2 := by
        simp only [dp_def, Prod.mk.eta, mkAlgHom, AlgHom.coe_mk]
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
P : DividedPowerAlgebra R M → Prop
h_C :
  ∀ (a : R),
    P
      ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
        ((C : (a : R) → MvPolynomial (ℕ × M) R) a))
h_add : ∀ (f g : DividedPowerAlgebra R M), P f → P g → P (f + g)
h_dp : ∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * dp R n m)
g : MvPolynomial.{u_2, u_1} (ℕ × M) R
nm : ℕ × M
h :
  ∀ (f : DividedPowerAlgebra R M)
    (hf : (mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) g = f),
    P ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) g)
f : DividedPowerAlgebra R M
hf : (mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (g * X nm) = f
h' :
  Eq (α := RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
    ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X nm) :
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
    (dp R nm.1 nm.2 : DividedPowerAlgebra R M)
mul_X :
  P
    (HMul.hMul (α := RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M)) (β :=
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
      ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) g :
        RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
      (dp R nm.1 nm.2))
⊢ P ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (g * X nm))

Tactic:
rw [_root_.map_mul, h']

Premises used: map_mul
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
P : DividedPowerAlgebra R M → Prop
h_C :
  ∀ (a : R),
    P
      ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
        ((C : (a : R) → MvPolynomial (ℕ × M) R) a))
h_add : ∀ (f g : DividedPowerAlgebra R M), P f → P g → P (f + g)
h_dp : ∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * dp R n m)
g : MvPolynomial.{u_2, u_1} (ℕ × M) R
nm : ℕ × M
h :
  ∀ (f : DividedPowerAlgebra R M)
    (hf : (mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) g = f),
    P ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) g)
f : DividedPowerAlgebra R M
hf : (mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (g * X nm) = f
h' :
  Eq (α := RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
    ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X nm) :
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
    (dp R nm.1 nm.2 : DividedPowerAlgebra R M)
⊢ P
    (HMul.hMul (α := RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M)) (β :=
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
      ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) g :
        RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
      (dp R nm.1 nm.2))

Tactic:
h_dp _ _ _ (h (mkRingHom (Rel R M) g) rfl)

Premises used: DividedPowerAlgebra.Rel, RingQuot.mkRingHom, DFunLike.coe, rfl
-- Module: Mathlib.RingTheory.DividedPowerAlgebra.Init
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
P : DividedPowerAlgebra R M → Prop
h_C :
  ∀ (a : R),
    P
      ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
        ((C : (a : R) → MvPolynomial (ℕ × M) R) a))
h_add : ∀ (f g : DividedPowerAlgebra R M), P f → P g → P (f + g)
h_dp : ∀ (f : DividedPowerAlgebra R M) (n : ℕ) (m : M), P f → P (f * dp R n m)
g : MvPolynomial.{u_2, u_1} (ℕ × M) R
nm : ℕ × M
h :
  ∀ (f : DividedPowerAlgebra R M)
    (hf : (mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) g = f),
    P ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) g)
f : DividedPowerAlgebra R M
hf : (mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (g * X nm) = f
h' :
  Eq (α := RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
    ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X nm) :
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
    (dp R nm.1 nm.2 : DividedPowerAlgebra R M)
⊢ P
    (HMul.hMul (α := RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M)) (β :=
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
      ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) g :
        RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
      (dp R nm.1 nm.2))

Tactic:
exact h_dp _ _ _ (h (mkRingHom (Rel R M) g) rfl)

Premises used: DividedPowerAlgebra.Rel, RingQuot.mkRingHom, DFunLike.coe, rfl