awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), Membership.mem (α := A) I ((g : (a : M) → A) m : A)
n : ℕ
r : R
m : M
rw :
  hI.dpow n (HSMul.hSMul (α := R) (β := A) ((RingHom.id R : (a : R) → R) r : R) ((g : (a : M) → A) m : A)) =
    r ^ n • hI.dpow n ((g : (a : M) → A) m)
rw₁ : hI.dpow n (HSMul.hSMul (β := A) r ((g : (a : M) → A) m : A)) = r ^ n • hI.dpow n ((g : (a : M) → A) m)
rw₂ :
  hI.dpow n (HSMul.hSMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) ((g : (a : M) → A) m : A)) =
    r ^ n • hI.dpow n ((g : (a : M) → A) m)
rw₃ :
  hI.dpow n (HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) ((g : (a : M) → A) m : A)) =
    r ^ n • hI.dpow n ((g : (a : M) → A) m)
rw₄ :
  HPow.hPow (α := A) ((algebraMap R A : (a : R) → A) r : A) n * hI.dpow n ((g : (a : M) → A) m) =
    r ^ n • hI.dpow n ((g : (a : M) → A) m)
⊢ hI.dpow n ((g : (a : M) → A) (r • m)) = r ^ n • hI.dpow n ((g : (a : M) → A) m)
have rw₅ : HPow.hPow (α := A) ((algebraMap R A : (a : R) → A) r : A) n • hI.dpow n ((g : (a : M) → A) m) =
  r ^ n • hI.dpow n ((g : (a : M) → A) m)
Tactic: rw [LinearMap.map_smulₛₗ, RingHom.id_apply, ← algebraMap_smul A r (g m), smul_eq_mul,
        hI.dpow_mul (hg m), ← smul_eq_mul, ← map_pow, algebraMap_smul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), Membership.mem (α := A) I ((g : (a : M) → A) m : A)
n : ℕ
r : R
m : M
rw :
  hI.dpow n (HSMul.hSMul (α := R) (β := A) ((RingHom.id R : (a : R) → R) r : R) ((g : (a : M) → A) m : A)) =
    r ^ n • hI.dpow n ((g : (a : M) → A) m)
rw₁ : hI.dpow n (HSMul.hSMul (β := A) r ((g : (a : M) → A) m : A)) = r ^ n • hI.dpow n ((g : (a : M) → A) m)
rw₂ :
  hI.dpow n (HSMul.hSMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) ((g : (a : M) → A) m : A)) =
    r ^ n • hI.dpow n ((g : (a : M) → A) m)
rw₃ :
  hI.dpow n (HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) ((g : (a : M) → A) m : A)) =
    r ^ n • hI.dpow n ((g : (a : M) → A) m)
rw₄ :
  HPow.hPow (α := A) ((algebraMap R A : (a : R) → A) r : A) n * hI.dpow n ((g : (a : M) → A) m) =
    r ^ n • hI.dpow n ((g : (a : M) → A) m)
rw₅ :
  HPow.hPow (α := A) ((algebraMap R A : (a : R) → A) r : A) n • hI.dpow n ((g : (a : M) → A) m) =
    r ^ n • hI.dpow n ((g : (a : M) → A) m)
⊢ hI.dpow n ((g : (a : M) → A) (r • m)) = r ^ n • hI.dpow n ((g : (a : M) → A) m)
have rw₆ : HSMul.hSMul (α := A) ((algebraMap R A : (a : R) → A) (r ^ n) : A) (hI.dpow n ((g : (a : M) → A) m)) =
  r ^ n • hI.dpow n ((g : (a : M) → A) m)
Tactic: rw [LinearMap.map_smulₛₗ, RingHom.id_apply, ← algebraMap_smul A r (g m), smul_eq_mul,
        hI.dpow_mul (hg m), ← smul_eq_mul, ← map_pow, algebraMap_smul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), Membership.mem (α := A) I ((g : (a : M) → A) m : A)
n : ℕ
r : R
m : M
rw :
  hI.dpow n (HSMul.hSMul (α := R) (β := A) ((RingHom.id R : (a : R) → R) r : R) ((g : (a : M) → A) m : A)) =
    r ^ n • hI.dpow n ((g : (a : M) → A) m)
rw₁ : hI.dpow n (HSMul.hSMul (β := A) r ((g : (a : M) → A) m : A)) = r ^ n • hI.dpow n ((g : (a : M) → A) m)
rw₂ :
  hI.dpow n (HSMul.hSMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) ((g : (a : M) → A) m : A)) =
    r ^ n • hI.dpow n ((g : (a : M) → A) m)
rw₃ :
  hI.dpow n (HMul.hMul (α := A) (β := A) ((algebraMap R A : (a : R) → A) r : A) ((g : (a : M) → A) m : A)) =
    r ^ n • hI.dpow n ((g : (a : M) → A) m)
rw₄ :
  HPow.hPow (α := A) ((algebraMap R A : (a : R) → A) r : A) n * hI.dpow n ((g : (a : M) → A) m) =
    r ^ n • hI.dpow n ((g : (a : M) → A) m)
rw₅ :
  HPow.hPow (α := A) ((algebraMap R A : (a : R) → A) r : A) n • hI.dpow n ((g : (a : M) → A) m) =
    r ^ n • hI.dpow n ((g : (a : M) → A) m)
rw₆ :
  HSMul.hSMul (α := A) ((algebraMap R A : (a : R) → A) (r ^ n) : A) (hI.dpow n ((g : (a : M) → A) m)) =
    r ^ n • hI.dpow n ((g : (a : M) → A) m)
⊢ hI.dpow n ((g : (a : M) → A) (r • m)) = r ^ n • hI.dpow n ((g : (a : M) → A) m)
have rw₇ : r ^ n • hI.dpow n ((g : (a : M) → A) m) = r ^ n • hI.dpow n ((g : (a : M) → A) m)
Tactic: rw [LinearMap.map_smulₛₗ, RingHom.id_apply, ← algebraMap_smul A r (g m), smul_eq_mul,
        hI.dpow_mul (hg m), ← smul_eq_mul, ← map_pow, algebraMap_smul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), Membership.mem (α := A) I ((g : (a : M) → A) m : A)
n p : ℕ
m : M
⊢ HMul.hMul (α := A) ((fun (nm : ℕ × M) ↦ hI.dpow nm.1 ((g : (a : M) → A) nm.2)) (n, m))
      ((fun (nm : ℕ × M) ↦ hI.dpow nm.1 ((g : (a : M) → A) nm.2)) (p, m)) =
    HSMul.hSMul (β := A) ((n + p).choose n) ((fun (nm : ℕ × M) ↦ hI.dpow nm.1 ((g : (a : M) → A) nm.2)) (n + p, m))
have rw : (↑(((n, m).1 + (p, m).1).choose (n, m).1) : A) * hI.dpow ((n, m).1 + (p, m).1) ((g : (a : M) → A) m) =
  HSMul.hSMul (β := A) ((n + p).choose n) ((fun (nm : ℕ × M) ↦ hI.dpow nm.1 ((g : (a : M) → A) nm.2)) (n + p, m))
Tactic: rw [hI.mul_dpow (hg m), ← nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), Membership.mem (α := A) I ((g : (a : M) → A) m : A)
n p : ℕ
m : M
rw :
  (↑(((n, m).1 + (p, m).1).choose (n, m).1) : A) * hI.dpow ((n, m).1 + (p, m).1) ((g : (a : M) → A) m) =
    HSMul.hSMul (β := A) ((n + p).choose n) ((fun (nm : ℕ × M) ↦ hI.dpow nm.1 ((g : (a : M) → A) nm.2)) (n + p, m))
⊢ HMul.hMul (α := A) ((fun (nm : ℕ × M) ↦ hI.dpow nm.1 ((g : (a : M) → A) nm.2)) (n, m))
      ((fun (nm : ℕ × M) ↦ hI.dpow nm.1 ((g : (a : M) → A) nm.2)) (p, m)) =
    HSMul.hSMul (β := A) ((n + p).choose n) ((fun (nm : ℕ × M) ↦ hI.dpow nm.1 ((g : (a : M) → A) nm.2)) (n + p, m))
have rw₁ : ((n, m).1 + (p, m).1).choose (n, m).1 • hI.dpow ((n, m).1 + (p, m).1) ((g : (a : M) → A) m) =
  HSMul.hSMul (β := A) ((n + p).choose n) ((fun (nm : ℕ × M) ↦ hI.dpow nm.1 ((g : (a : M) → A) nm.2)) (n + p, m))
Tactic: rw [hI.mul_dpow (hg m), ← nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), Membership.mem (α := A) I ((g : (a : M) → A) m : A)
p : MvPolynomial.{u_2, u_1} (ℕ × M) R
⊢ Eq.{u_3 + 1} (α := A)
    ((lift hI g hg : (a : DividedPowerAlgebra R M) → A)
        ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) p :
          RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M)) :
      A)
    ((aeval fun (nm : ℕ × M) ↦ hI.dpow nm.1 ((g : (a : M) → A) nm.2) : (a : MvPolynomial (ℕ × M) R) → A) p : A)
have rw : Eq.{u_3 + 1} (α := A)
  ((lift' (f := fun (nm : ℕ × M) ↦ hI.dpow nm.1 ((g : (a : M) → A) nm.2)) sorry sorry sorry sorry : (a : DividedPowerAlgebra R M) → A)
      ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) p :
        RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M)) :
    A)
  ((aeval fun (nm : ℕ × M) ↦ hI.dpow nm.1 ((g : (a : M) → A) nm.2) : (a : MvPolynomial (ℕ × M) R) → A) p : A)
Tactic: rw [lift, lift'_apply]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), Membership.mem (α := A) I ((g : (a : M) → A) m : A)
p : MvPolynomial.{u_2, u_1} (ℕ × M) R
rw :
  Eq.{u_3 + 1} (α := A)
    ((lift' (f := fun (nm : ℕ × M) ↦ hI.dpow nm.1 ((g : (a : M) → A) nm.2)) ⋯ ⋯ ⋯ ⋯ : (a : DividedPowerAlgebra R M) → A)
        ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) p :
          RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M)) :
      A)
    ((aeval fun (nm : ℕ × M) ↦ hI.dpow nm.1 ((g : (a : M) → A) nm.2) : (a : MvPolynomial (ℕ × M) R) → A) p : A)
⊢ Eq.{u_3 + 1} (α := A)
    ((lift hI g hg : (a : DividedPowerAlgebra R M) → A)
        ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) p :
          RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M)) :
      A)
    ((aeval fun (nm : ℕ × M) ↦ hI.dpow nm.1 ((g : (a : M) → A) nm.2) : (a : MvPolynomial (ℕ × M) R) → A) p : A)
have rw₁ : Eq.{u_3 + 1} (α := A)
  ((aeval fun (nm : ℕ × M) ↦ hI.dpow nm.1 ((g : (a : M) → A) nm.2) : (a : MvPolynomial (ℕ × M) R) → A) p : A)
  ((aeval fun (nm : ℕ × M) ↦ hI.dpow nm.1 ((g : (a : M) → A) nm.2) : (a : MvPolynomial (ℕ × M) R) → A) p : A)
Tactic: rw [lift, lift'_apply]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), Membership.mem (α := A) I ((g : (a : M) → A) m : A)
n : ℕ
m : M
⊢ (lift hI g hg : (a : DividedPowerAlgebra R M) → A) (dp R n m) = hI.dpow n ((g : (a : M) → A) m)
have rw : (lift' (f := fun (nm : ℕ × M) ↦ hI.dpow nm.1 ((g : (a : M) → A) nm.2)) sorry sorry sorry sorry : (a : DividedPowerAlgebra R M) → A)
    (dp R n m) =
  hI.dpow n ((g : (a : M) → A) m)
Tactic: rw [lift, lift'_apply_dp]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), Membership.mem (α := A) I ((g : (a : M) → A) m : A)
n : ℕ
m : M
rw :
  (lift' (f := fun (nm : ℕ × M) ↦ hI.dpow nm.1 ((g : (a : M) → A) nm.2)) ⋯ ⋯ ⋯ ⋯ : (a : DividedPowerAlgebra R M) → A)
      (dp R n m) =
    hI.dpow n ((g : (a : M) → A) m)
⊢ (lift hI g hg : (a : DividedPowerAlgebra R M) → A) (dp R n m) = hI.dpow n ((g : (a : M) → A) m)
have rw₁ : hI.dpow (n, m).1 ((g : (a : M) → A) (n, m).2) = hI.dpow n ((g : (a : M) → A) m)
Tactic: rw [lift, lift'_apply_dp]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), Membership.mem (α := A) I ((g : (a : M) → A) m : A)
f : DividedPowerAlgebra R M →ₐ[R] A
hf : ∀ (n : ℕ) (m : M), (f : (a : DividedPowerAlgebra R M) → A) (dp R n m) = hI.dpow n ((g : (a : M) → A) m)
x : ℕ
x_1 : M
⊢ Eq.{u_3 + 1} (α := A) ((f : (a : DividedPowerAlgebra R M) → A) (dp R x x_1) : A)
    ((lift hI g hg : (a : DividedPowerAlgebra R M) → A) (dp R x x_1) : A)
have rw : (f : (a : DividedPowerAlgebra R M) → A) (dp R x x_1) = hI.dpow x ((g : (a : M) → A) x_1)
Tactic: rw [lift_apply_dp, hf]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), Membership.mem (α := A) I ((g : (a : M) → A) m : A)
f : DividedPowerAlgebra R M →ₐ[R] A
hf : ∀ (n : ℕ) (m : M), (f : (a : DividedPowerAlgebra R M) → A) (dp R n m) = hI.dpow n ((g : (a : M) → A) m)
x : ℕ
x_1 : M
rw : (f : (a : DividedPowerAlgebra R M) → A) (dp R x x_1) = hI.dpow x ((g : (a : M) → A) x_1)
⊢ Eq.{u_3 + 1} (α := A) ((f : (a : DividedPowerAlgebra R M) → A) (dp R x x_1) : A)
    ((lift hI g hg : (a : DividedPowerAlgebra R M) → A) (dp R x x_1) : A)
have rw₁ : hI.dpow x ((g : (a : M) → A) x_1) = hI.dpow x ((g : (a : M) → A) x_1)
Tactic: rw [lift_apply_dp, hf]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : CommSemiring A
inst_4 : Algebra R A
I : Ideal A
hI : DividedPowers I
g : M →ₗ[R] A
hg : ∀ (m : M), Membership.mem (α := A) I ((g : (a : M) → A) m : A)
⊢ (lift hI g hg).toLinearMap ∘ₗ embed R M = g
have h : ∀ (x : M),
  Eq.{u_3 + 1} (α := A) (((lift hI g hg).toLinearMap ∘ₗ embed R M : (a : M) → A) x : A) ((g : (a : M) → A) x : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
inst_3 : CommSemiring S
N : Type u_4
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
f : M →ₗ[R] N
n : ℕ
a b : M
⊢ Eq (α := DividedPowerAlgebra S N) (dp S n ((f : (a : M) → N) (a + b)) : DividedPowerAlgebra S N)
    (∑ k ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        HMul.hMul (α := DividedPowerAlgebra S N) (β := DividedPowerAlgebra S N)
          (dp S k.1 ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
          (dp S k.2 ((f : (a : M) → N) b) : DividedPowerAlgebra S N) :
      DividedPowerAlgebra S N)
have rw : Eq (α := DividedPowerAlgebra S N)
  (dp S n (HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N)))
  (∑ k ∈ @antidiagonal _ Nat.instAddMonoid _ n,
    HMul.hMul (α := DividedPowerAlgebra S N) (β := DividedPowerAlgebra S N)
      (dp S k.1 ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
      (dp S k.2 ((f : (a : M) → N) b) : DividedPowerAlgebra S N))
Tactic: rw [map_add, DividedPowerAlgebra.dp_add]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
inst_3 : CommSemiring S
N : Type u_4
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
f : M →ₗ[R] N
n : ℕ
a b : M
rw :
  Eq (α := DividedPowerAlgebra S N)
    (dp S n (HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) a : N) ((f : (a : M) → N) b : N)))
    (∑ k ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      HMul.hMul (α := DividedPowerAlgebra S N) (β := DividedPowerAlgebra S N)
        (dp S k.1 ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
        (dp S k.2 ((f : (a : M) → N) b) : DividedPowerAlgebra S N))
⊢ Eq (α := DividedPowerAlgebra S N) (dp S n ((f : (a : M) → N) (a + b)) : DividedPowerAlgebra S N)
    (∑ k ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        HMul.hMul (α := DividedPowerAlgebra S N) (β := DividedPowerAlgebra S N)
          (dp S k.1 ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
          (dp S k.2 ((f : (a : M) → N) b) : DividedPowerAlgebra S N) :
      DividedPowerAlgebra S N)
have rw₁ : Eq (α := DividedPowerAlgebra S N)
  (∑ k ∈ @antidiagonal _ Nat.instAddMonoid _ n,
    HMul.hMul (α := DividedPowerAlgebra S N) (β := DividedPowerAlgebra S N)
      (dp S k.1 ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
      (dp S k.2 ((f : (a : M) → N) b) : DividedPowerAlgebra S N))
  (∑ k ∈ @antidiagonal _ Nat.instAddMonoid _ n,
    HMul.hMul (α := DividedPowerAlgebra S N) (β := DividedPowerAlgebra S N)
      (dp S k.1 ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
      (dp S k.2 ((f : (a : M) → N) b) : DividedPowerAlgebra S N))
Tactic: rw [map_add, DividedPowerAlgebra.dp_add]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
inst_3 : CommSemiring S
N : Type u_4
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
f : M →ₗ[R] N
inst_7 : Algebra R S
inst_8 : IsScalarTower R S N
n : ℕ
r : R
a : M
⊢ dp S n ((f : (a : M) → N) (r • a)) =
    HSMul.hSMul (β := DividedPowerAlgebra S N) (r ^ n) (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
have rw : dp S n (HSMul.hSMul (β := N) r ((f : (a : M) → N) a : N)) =
  HSMul.hSMul (β := DividedPowerAlgebra S N) (r ^ n) (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
Tactic: rw [f.map_smul, algebra_compatible_smul S r (f a),
    DividedPowerAlgebra.dp_smul, ← map_pow, algebraMap_smul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
inst_3 : CommSemiring S
N : Type u_4
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
f : M →ₗ[R] N
inst_7 : Algebra R S
inst_8 : IsScalarTower R S N
n : ℕ
r : R
a : M
rw :
  dp S n (HSMul.hSMul (β := N) r ((f : (a : M) → N) a : N)) =
    HSMul.hSMul (β := DividedPowerAlgebra S N) (r ^ n) (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
⊢ dp S n ((f : (a : M) → N) (r • a)) =
    HSMul.hSMul (β := DividedPowerAlgebra S N) (r ^ n) (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
have rw₁ : dp S n
    (HSMul.hSMul.{u_3, u_4, u_4} (α := S) (β := N) ((algebraMap R S : (a : R) → S) r : S) ((f : (a : M) → N) a : N)) =
  HSMul.hSMul (β := DividedPowerAlgebra S N) (r ^ n) (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
Tactic: rw [f.map_smul, algebra_compatible_smul S r (f a),
    DividedPowerAlgebra.dp_smul, ← map_pow, algebraMap_smul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
inst_3 : CommSemiring S
N : Type u_4
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
f : M →ₗ[R] N
inst_7 : Algebra R S
inst_8 : IsScalarTower R S N
n : ℕ
r : R
a : M
rw :
  dp S n (HSMul.hSMul (β := N) r ((f : (a : M) → N) a : N)) =
    HSMul.hSMul (β := DividedPowerAlgebra S N) (r ^ n) (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
rw₁ :
  dp S n
      (HSMul.hSMul.{u_3, u_4, u_4} (α := S) (β := N) ((algebraMap R S : (a : R) → S) r : S) ((f : (a : M) → N) a : N)) =
    HSMul.hSMul (β := DividedPowerAlgebra S N) (r ^ n) (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
⊢ dp S n ((f : (a : M) → N) (r • a)) =
    HSMul.hSMul (β := DividedPowerAlgebra S N) (r ^ n) (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
have rw₂ : HSMul.hSMul (β := DividedPowerAlgebra S N) (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n)
    (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N) =
  HSMul.hSMul (β := DividedPowerAlgebra S N) (r ^ n) (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
Tactic: rw [f.map_smul, algebra_compatible_smul S r (f a),
    DividedPowerAlgebra.dp_smul, ← map_pow, algebraMap_smul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
inst_3 : CommSemiring S
N : Type u_4
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
f : M →ₗ[R] N
inst_7 : Algebra R S
inst_8 : IsScalarTower R S N
n : ℕ
r : R
a : M
rw :
  dp S n (HSMul.hSMul (β := N) r ((f : (a : M) → N) a : N)) =
    HSMul.hSMul (β := DividedPowerAlgebra S N) (r ^ n) (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
rw₁ :
  dp S n
      (HSMul.hSMul.{u_3, u_4, u_4} (α := S) (β := N) ((algebraMap R S : (a : R) → S) r : S) ((f : (a : M) → N) a : N)) =
    HSMul.hSMul (β := DividedPowerAlgebra S N) (r ^ n) (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
rw₂ :
  HSMul.hSMul (β := DividedPowerAlgebra S N) (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n)
      (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N) =
    HSMul.hSMul (β := DividedPowerAlgebra S N) (r ^ n) (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
⊢ dp S n ((f : (a : M) → N) (r • a)) =
    HSMul.hSMul (β := DividedPowerAlgebra S N) (r ^ n) (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
have rw₃ : HSMul.hSMul (α := S) (β := DividedPowerAlgebra S N) ((algebraMap R S : (a : R) → S) (r ^ n) : S)
    (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N) =
  HSMul.hSMul (β := DividedPowerAlgebra S N) (r ^ n) (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
Tactic: rw [f.map_smul, algebra_compatible_smul S r (f a),
    DividedPowerAlgebra.dp_smul, ← map_pow, algebraMap_smul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
inst_3 : CommSemiring S
N : Type u_4
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
f : M →ₗ[R] N
inst_7 : Algebra R S
inst_8 : IsScalarTower R S N
n : ℕ
r : R
a : M
rw :
  dp S n (HSMul.hSMul (β := N) r ((f : (a : M) → N) a : N)) =
    HSMul.hSMul (β := DividedPowerAlgebra S N) (r ^ n) (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
rw₁ :
  dp S n
      (HSMul.hSMul.{u_3, u_4, u_4} (α := S) (β := N) ((algebraMap R S : (a : R) → S) r : S) ((f : (a : M) → N) a : N)) =
    HSMul.hSMul (β := DividedPowerAlgebra S N) (r ^ n) (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
rw₂ :
  HSMul.hSMul (β := DividedPowerAlgebra S N) (HPow.hPow (α := S) ((algebraMap R S : (a : R) → S) r : S) n)
      (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N) =
    HSMul.hSMul (β := DividedPowerAlgebra S N) (r ^ n) (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
rw₃ :
  HSMul.hSMul (α := S) (β := DividedPowerAlgebra S N) ((algebraMap R S : (a : R) → S) (r ^ n) : S)
      (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N) =
    HSMul.hSMul (β := DividedPowerAlgebra S N) (r ^ n) (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
⊢ dp S n ((f : (a : M) → N) (r • a)) =
    HSMul.hSMul (β := DividedPowerAlgebra S N) (r ^ n) (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
have rw₄ : HSMul.hSMul (β := DividedPowerAlgebra S N) (r ^ n) (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N) =
  HSMul.hSMul (β := DividedPowerAlgebra S N) (r ^ n) (dp S n ((f : (a : M) → N) a) : DividedPowerAlgebra S N)
Tactic: rw [f.map_smul, algebra_compatible_smul S r (f a),
    DividedPowerAlgebra.dp_smul, ← map_pow, algebraMap_smul]
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_3
inst_3 : CommSemiring S
N : Type u_4
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
f : M →ₗ[R] N
inst_7 : Algebra R S
inst_8 : IsScalarTower R S N
p : MvPolynomial.{u_2, u_1} (ℕ × M) R
⊢ Eq (α := DividedPowerAlgebra S N)
    ((map S f : (a : DividedPowerAlgebra R M) → DividedPowerAlgebra S N)
        ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) p) :
      DividedPowerAlgebra S N)
    ((aeval fun (nm : ℕ × M) ↦ dp S nm.1 ((f : (a : M) → N) nm.2) :
          (a : MvPolynomial (ℕ × M) R) → DividedPowerAlgebra S N)
        p :
      DividedPowerAlgebra S N)
have rw : Eq (α := DividedPowerAlgebra S N)
  ((lift' (f := fun (nm : ℕ × M) ↦ dp S nm.1 ((f : (a : M) → N) nm.2)) sorry sorry sorry sorry :
        (a : DividedPowerAlgebra R M) → DividedPowerAlgebra S N)
      ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) p) :
    DividedPowerAlgebra S N)
  ((aeval fun (nm : ℕ × M) ↦ dp S nm.1 ((f : (a : M) → N) nm.2) :
        (a : MvPolynomial (ℕ × M) R) → DividedPowerAlgebra S N)
      p :
    DividedPowerAlgebra S N)
Tactic: rw [map, lift'_apply]