awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_3
M : Type u_4
ι : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
hv : Eq (α := Submodule R M) (Submodule.span R (Set.range v)) ⊤
p : DividedPowerAlgebra R M
C :
  ∀ (r : R),
    Membership.mem (α := DividedPowerAlgebra R M) (γ := Submodule R (DividedPowerAlgebra R M))
      (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i)))
      ((algebraMap R (DividedPowerAlgebra R M) : (a : R) → DividedPowerAlgebra R M) r : DividedPowerAlgebra R M)
⊢ Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
    (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i))) p
have add : ∀ (x y : DividedPowerAlgebra R M)
  (hx :
    Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
      (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i))) x)
  (hy :
    Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
      (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i))) y),
  Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
    (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i))) (x + y)
Tactic: induction p using DividedPowerAlgebra.induction_on with
  | C r =>
    simp only [Algebra.algebraMap_eq_smul_one]
    exact smul_mem _ _ (subset_span ⟨0, by simp⟩)
  | add x y hx hy => exact Submodule.add_mem _ hx hy
  | dp x k m hx =>
    have hm : m ∈ span R (Set.range v) := by simp [hv, mem_top]
    induction hm using span_induction generalizing x k with
    | zero => rw [dp_null]; split_ifs <;> simp [hx]
    | smul r m hm h => simp [dp_smul, smul_mem _ _ (h x k hx)]
    | mem y hy =>
      obtain ⟨i, rfl⟩ := hy
      induction hx using span_induction with
      | zero => simp
      | mem x hx =>
        obtain ⟨n, rfl⟩ := hx
        simp only
        rw [← n.mul_prod_erase' i _ (fun i ↦ dp_zero (m := v i)), mul_comm,
          ← mul_assoc, dp_mul, nsmul_eq_mul, mul_assoc, ← nsmul_eq_mul]
        refine smul_of_tower_mem _ _ (mem_span_of_mem ⟨Finsupp.single i k + n, ?_⟩)
        simp only
        rw [← (Finsupp.single i k + n).mul_prod_erase' i _ (fun i ↦ dp_zero (m := v i))]
        simp
      | add x y hxmem hymem hx hy =>
        rw [add_mul]
        exact Submodule.add_mem _ hx hy
      | smul r x hxmem hx =>
        rw [smul_mul_assoc]
        exact smul_mem _ _ hx
    | add m n hm_mem hn_mem hm hn =>
      rw [dp_add, mul_sum]
      apply sum_mem (fun c hc ↦ ?_)
      rw [← mul_assoc]
      exact hn (x * dp R c.1 m) c.2 (hm x c.1 hx)
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_3
M : Type u_4
ι : Type u_5
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
v : ι → M
hv : Eq (α := Submodule R M) (Submodule.span R (Set.range v)) ⊤
p : DividedPowerAlgebra R M
C :
  ∀ (r : R),
    Membership.mem (α := DividedPowerAlgebra R M) (γ := Submodule R (DividedPowerAlgebra R M))
      (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i)))
      ((algebraMap R (DividedPowerAlgebra R M) : (a : R) → DividedPowerAlgebra R M) r : DividedPowerAlgebra R M)
add :
  ∀ (x y : DividedPowerAlgebra R M)
    (hx :
      Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
        (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i))) x)
    (hy :
      Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
        (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i))) y),
    Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
      (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i))) (x + y)
⊢ Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
    (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i))) p
have dp : ∀ (x : DividedPowerAlgebra R M) (k : ℕ) (m : M)
  (hx :
    Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
      (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i))) x),
  Membership.mem (γ := Submodule R (DividedPowerAlgebra R M))
    (Submodule.span R (Set.range fun (n : ι →₀ ℕ) ↦ n.prod fun (i : ι) (k : ℕ) ↦ dp R k (v i))) (x * dp R k m)
Tactic: induction p using DividedPowerAlgebra.induction_on with
  | C r =>
    simp only [Algebra.algebraMap_eq_smul_one]
    exact smul_mem _ _ (subset_span ⟨0, by simp⟩)
  | add x y hx hy => exact Submodule.add_mem _ hx hy
  | dp x k m hx =>
    have hm : m ∈ span R (Set.range v) := by simp [hv, mem_top]
    induction hm using span_induction generalizing x k with
    | zero => rw [dp_null]; split_ifs <;> simp [hx]
    | smul r m hm h => simp [dp_smul, smul_mem _ _ (h x k hx)]
    | mem y hy =>
      obtain ⟨i, rfl⟩ := hy
      induction hx using span_induction with
      | zero => simp
      | mem x hx =>
        obtain ⟨n, rfl⟩ := hx
        simp only
        rw [← n.mul_prod_erase' i _ (fun i ↦ dp_zero (m := v i)), mul_comm,
          ← mul_assoc, dp_mul, nsmul_eq_mul, mul_assoc, ← nsmul_eq_mul]
        refine smul_of_tower_mem _ _ (mem_span_of_mem ⟨Finsupp.single i k + n, ?_⟩)
        simp only
        rw [← (Finsupp.single i k + n).mul_prod_erase' i _ (fun i ↦ dp_zero (m := v i))]
        simp
      | add x y hxmem hymem hx hy =>
        rw [add_mul]
        exact Submodule.add_mem _ hx hy
      | smul r x hxmem hx =>
        rw [smul_mul_assoc]
        exact smul_mem _ _ hx
    | add m n hm_mem hn_mem hm hn =>
      rw [dp_add, mul_sum]
      apply sum_mem (fun c hc ↦ ?_)
      rw [← mul_assoc]
      exact hn (x * dp R c.1 m) c.2 (hm x c.1 hx)
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.RingTheory.DividedPowerAlgebra.Init (goal)
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
n : ℕ
m : M
k : ℕ
⊢ HPow.hPow (α := DividedPowerAlgebra R M) (dp R n m) k =
    HMul.hMul (α := DividedPowerAlgebra R M)
      (↑(HSMul.hSMul (β := Multiset ℕ) k {n}).multinomial : DividedPowerAlgebra R M) (dp R (k * n) m)
have rw : HMul.hMul (α := DividedPowerAlgebra R M) (↑(Nat.multinomial univ fun (_i : Fin k) ↦ n) : DividedPowerAlgebra R M)
    (dp R (∑ _i : Fin k, n) m) =
  HMul.hMul (α := DividedPowerAlgebra R M) (↑(Nat.multinomial (range k) fun (x : ℕ) ↦ n) : DividedPowerAlgebra R M)
    (dp R (k * n) m)
Tactic: rw [Multiset.multinomial_nsmul_singleton, ← Fin.prod_const, prod_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
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        match (motive := ℕ × ℕ → A) x with
        | (k, l) => f (k, u) * f (l, v)
p q : MvPolynomial.{u_2, u_1} (ℕ × M) R
h : Rel R M p q
⊢ Eq.{u_3 + 1} (α := A) ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) p : A)
    ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) q : A)
have rfl_zero : Eq.{u_3 + 1} (α := A) ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) 0 : A)
  ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) 0 : A)
Tactic: rcases h
Cleared hypotheses: p, q, h
-- 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
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        match (motive := ℕ × ℕ → A) x with
        | (k, l) => f (k, u) * f (l, v)
p q : MvPolynomial.{u_2, u_1} (ℕ × M) R
h : Rel R M p q
rfl_zero :
  Eq.{u_3 + 1} (α := A) ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) 0 : A)
    ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) 0 : A)
⊢ Eq.{u_3 + 1} (α := A) ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) p : A)
    ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) q : A)
have zero : ∀ {a : M},
  Eq.{u_3 + 1} (α := A) ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) (X (0, a)) : A)
    ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) 1 : A)
Tactic: rcases h
Cleared hypotheses: p, q, h
-- 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
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        match (motive := ℕ × ℕ → A) x with
        | (k, l) => f (k, u) * f (l, v)
p q : MvPolynomial.{u_2, u_1} (ℕ × M) R
h : Rel R M p q
rfl_zero :
  Eq.{u_3 + 1} (α := A) ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) 0 : A)
    ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) 0 : A)
zero :
  ∀ {a : M},
    Eq.{u_3 + 1} (α := A) ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) (X (0, a)) : A)
      ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) 1 : A)
⊢ Eq.{u_3 + 1} (α := A) ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) p : A)
    ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) q : A)
have smul : ∀ {r : R} {n : ℕ} {a : M},
  Eq.{u_3 + 1} (α := A) ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) (X (n, r • a)) : A)
    ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A)
        (HSMul.hSMul (β := MvPolynomial.{u_2, u_1} (ℕ × M) R) (r ^ n) (X (n, a))) :
      A)
Tactic: rcases h
Cleared hypotheses: p, q, h
-- 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
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        match (motive := ℕ × ℕ → A) x with
        | (k, l) => f (k, u) * f (l, v)
p q : MvPolynomial.{u_2, u_1} (ℕ × M) R
h : Rel R M p q
rfl_zero :
  Eq.{u_3 + 1} (α := A) ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) 0 : A)
    ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) 0 : A)
zero :
  ∀ {a : M},
    Eq.{u_3 + 1} (α := A) ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) (X (0, a)) : A)
      ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) 1 : A)
smul :
  ∀ {r : R} {n : ℕ} {a : M},
    Eq.{u_3 + 1} (α := A) ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) (X (n, r • a)) : A)
      ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A)
          (HSMul.hSMul (β := MvPolynomial.{u_2, u_1} (ℕ × M) R) (r ^ n) (X (n, a))) :
        A)
⊢ Eq.{u_3 + 1} (α := A) ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) p : A)
    ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) q : A)
have mul : ∀ {m n : ℕ} {a : M},
  Eq.{u_3 + 1} (α := A)
    ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A)
        (HMul.hMul (α := MvPolynomial.{u_2, u_1} (ℕ × M) R) (X (m, a)) (X (n, a))) :
      A)
    ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A)
        (HSMul.hSMul (β := MvPolynomial.{u_2, u_1} (ℕ × M) R) ((m + n).choose m) (X (m + n, a))) :
      A)
Tactic: rcases h
Cleared hypotheses: p, q, h
-- 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
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        match (motive := ℕ × ℕ → A) x with
        | (k, l) => f (k, u) * f (l, v)
p q : MvPolynomial.{u_2, u_1} (ℕ × M) R
h : Rel R M p q
rfl_zero :
  Eq.{u_3 + 1} (α := A) ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) 0 : A)
    ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) 0 : A)
zero :
  ∀ {a : M},
    Eq.{u_3 + 1} (α := A) ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) (X (0, a)) : A)
      ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) 1 : A)
smul :
  ∀ {r : R} {n : ℕ} {a : M},
    Eq.{u_3 + 1} (α := A) ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) (X (n, r • a)) : A)
      ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A)
          (HSMul.hSMul (β := MvPolynomial.{u_2, u_1} (ℕ × M) R) (r ^ n) (X (n, a))) :
        A)
mul :
  ∀ {m n : ℕ} {a : M},
    Eq.{u_3 + 1} (α := A)
      ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A)
          (HMul.hMul (α := MvPolynomial.{u_2, u_1} (ℕ × M) R) (X (m, a)) (X (n, a))) :
        A)
      ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A)
          (HSMul.hSMul (β := MvPolynomial.{u_2, u_1} (ℕ × M) R) ((m + n).choose m) (X (m + n, a))) :
        A)
⊢ Eq.{u_3 + 1} (α := A) ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) p : A)
    ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) q : A)
have add : ∀ {n : ℕ} {a b : M},
  Eq.{u_3 + 1} (α := A) ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A) (X (n, a + b)) : A)
    ((eval₂AlgHom R f : (a : MvPolynomial (ℕ × M) R) → A)
        (∑ k ∈ @antidiagonal _ Nat.instAddMonoid _ n,
          HMul.hMul (α := MvPolynomial.{u_2, u_1} (ℕ × M) R) (X (k.1, a)) (X (k.2, b))) :
      A)
Tactic: rcases h
Cleared hypotheses: p, q, h
-- 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
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        match (motive := ℕ × ℕ → A) x with
        | (k, l) => f (k, u) * f (l, v)
n : ℕ
m : M
⊢ (lift' hf_zero hf_smul hf_mul hf_add : (a : DividedPowerAlgebra R M) → A) (dp R n m) = f (n, m)
have rw : (lift' hf_zero hf_smul hf_mul hf_add : (a : DividedPowerAlgebra R M) → A)
    ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X (n, m)) :
      RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M)) =
  f (n, m)
Tactic: rw [dp_def, lift'_apply hf_zero hf_smul hf_mul hf_add, aeval_X]
-- 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
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        match (motive := ℕ × ℕ → A) x with
        | (k, l) => f (k, u) * f (l, v)
n : ℕ
m : M
rw :
  (lift' hf_zero hf_smul hf_mul hf_add : (a : DividedPowerAlgebra R M) → A)
      ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X (n, m)) :
        RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M)) =
    f (n, m)
⊢ (lift' hf_zero hf_smul hf_mul hf_add : (a : DividedPowerAlgebra R M) → A) (dp R n m) = f (n, m)
have rw₁ : (aeval f : (a : MvPolynomial (ℕ × M) R) → A) (X (n, m)) = f (n, m)
Tactic: rw [dp_def, lift'_apply hf_zero hf_smul hf_mul hf_add, aeval_X]
-- 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
f : ℕ × M → A
hf_zero : ∀ (m : M), f (0, m) = 1
hf_smul : ∀ (n : ℕ) (r : R) (m : M), f (n, r • m) = r ^ n • f (n, m)
hf_mul : ∀ (n p : ℕ) (m : M), f (n, m) * f (p, m) = (n + p).choose n • f (n + p, m)
hf_add :
  ∀ (n : ℕ) (u v : M),
    f (n, u + v) =
      ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
        match (motive := ℕ × ℕ → A) x with
        | (k, l) => f (k, u) * f (l, v)
n : ℕ
m : M
rw :
  (lift' hf_zero hf_smul hf_mul hf_add : (a : DividedPowerAlgebra R M) → A)
      ((mkAlgHom R (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (X (n, m)) :
        RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M)) =
    f (n, m)
rw₁ : (aeval f : (a : MvPolynomial (ℕ × M) R) → A) (X (n, m)) = f (n, m)
⊢ (lift' hf_zero hf_smul hf_mul hf_add : (a : DividedPowerAlgebra R M) → A) (dp R n m) = f (n, m)
have rw₂ : f (n, m) = f (n, m)
Tactic: rw [dp_def, lift'_apply hf_zero hf_smul hf_mul hf_add, aeval_X]
-- 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
⊢ (fun (nm : ℕ × M) ↦ hI.dpow nm.1 ((g : (a : M) → A) nm.2)) (n, r • m) =
    HSMul.hSMul (β := A) (r ^ n) ((fun (nm : ℕ × M) ↦ hI.dpow nm.1 ((g : (a : M) → A) nm.2)) (n, m))
have dsimp : hI.dpow n ((g : (a : M) → A) (r • m)) = r ^ n • hI.dpow n ((g : (a : M) → A) m)
Tactic: dsimp only
-- 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
⊢ hI.dpow n ((g : (a : M) → A) (r • m)) = r ^ n • hI.dpow n ((g : (a : M) → A) m)
have 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)
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)
⊢ hI.dpow n ((g : (a : M) → A) (r • m)) = r ^ n • hI.dpow n ((g : (a : M) → A) m)
have rw₁ : hI.dpow n (HSMul.hSMul (β := A) r ((g : (a : M) → A) m : A)) = 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)
⊢ hI.dpow n ((g : (a : M) → A) (r • m)) = r ^ n • hI.dpow n ((g : (a : M) → A) m)
have 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)
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)
⊢ hI.dpow n ((g : (a : M) → A) (r • m)) = r ^ n • hI.dpow n ((g : (a : M) → A) m)
have 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)
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)
⊢ 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]