awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
Goal:
A : Type u
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : Fintype ι
b b' : Basis ι ℤ A
h :
  Eq (α := ι → A) (⇑b : (a : ι) → A)
    ((⇑b' : (a : ι) → A) ᵥ* Matrix.map (b'.toMatrix (⇑b : (a : ι) → A)) (⇑(algebraMap ℤ A) : (a : ℤ) → A))
⊢ discr.{0, u, w} (ι := ι) ℤ (B := A) (⇑b : (a : ι) → A) = discr.{0, u, w} (ι := ι) ℤ (B := A) (⇑b' : (a : ι) → A)
have h₁ : discr.{0, u, w} (ι := ι) ℤ (B := A) (⇑b' : (a : ι) → A) =
  HPow.hPow (β := ℕ) (det (b'.toMatrix (⇑b : (a : ι) → A))) 2 * discr.{0, u, w} (ι := ι) ℤ (B := A) (⇑b' : (a : ι) → A)
Tactic: convert! Algebra.discr_of_matrix_vecMul b' (b'.toMatrix b)
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
Goal:
A : Type u
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : Fintype ι
b b' : Basis ι ℤ A
⊢ Eq (α := ι → A) (⇑b : (a : ι) → A)
    ((⇑b' : (a : ι) → A) ᵥ* Matrix.map (b'.toMatrix (⇑b : (a : ι) → A)) (⇑(algebraMap ℤ A) : (a : ℤ) → A))
have h : Eq (α := ι → A) (⇑b : (a : ι) → A) (⇑b : (a : ι) → A)
Tactic: rw [Basis.toMatrix_map_vecMul]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (hypothesis)
Goal:
A : Type u
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : Fintype ι
b b' : Basis ι ℤ A
this : IsUnit (det (b'.toMatrix (⇑b : (a : ι) → A)))
⊢ discr.{0, u, w} (ι := ι) ℤ (B := A) (⇑b' : (a : ι) → A) =
    HPow.hPow (β := ℕ) (det (b'.toMatrix (⇑b : (a : ι) → A))) 2 *
      discr.{0, u, w} (ι := ι) ℤ (B := A) (⇑b' : (a : ι) → A)
have this₁ : HPow.hPow (β := ℕ) (det (b'.toMatrix (⇑b : (a : ι) → A))) 2 = 1
Tactic: rw [Int.isUnit_iff, ← sq_eq_one_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
Goal:
A : Type u
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : Fintype ι
b b' : Basis ι ℤ A
this : HPow.hPow (β := ℕ) (det (b'.toMatrix (⇑b : (a : ι) → A))) 2 = 1
⊢ discr.{0, u, w} (ι := ι) ℤ (B := A) (⇑b' : (a : ι) → A) =
    HPow.hPow (β := ℕ) (det (b'.toMatrix (⇑b : (a : ι) → A))) 2 *
      discr.{0, u, w} (ι := ι) ℤ (B := A) (⇑b' : (a : ι) → A)
have rw : discr.{0, u, w} (ι := ι) ℤ (B := A) (⇑b' : (a : ι) → A) = 1 * discr.{0, u, w} (ι := ι) ℤ (B := A) (⇑b' : (a : ι) → A)
Tactic: rw [this, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
Goal:
A : Type u
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : Fintype ι
b b' : Basis ι ℤ A
this : HPow.hPow (β := ℕ) (det (b'.toMatrix (⇑b : (a : ι) → A))) 2 = 1
rw :
  discr.{0, u, w} (ι := ι) ℤ (B := A) (⇑b' : (a : ι) → A) = 1 * discr.{0, u, w} (ι := ι) ℤ (B := A) (⇑b' : (a : ι) → A)
⊢ discr.{0, u, w} (ι := ι) ℤ (B := A) (⇑b' : (a : ι) → A) =
    HPow.hPow (β := ℕ) (det (b'.toMatrix (⇑b : (a : ι) → A))) 2 *
      discr.{0, u, w} (ι := ι) ℤ (B := A) (⇑b' : (a : ι) → A)
have rw₁ : discr.{0, u, w} (ι := ι) ℤ (B := A) (⇑b' : (a : ι) → A) = discr.{0, u, w} (ι := ι) ℤ (B := A) (⇑b' : (a : ι) → A)
Tactic: rw [this, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
Goal:
A : Type u
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : Fintype ι
b b' : Basis ι ℤ A
⊢ discr.{0, u, w} (ι := ι) ℤ (B := A) (⇑b' : (a : ι) → A) =
    HPow.hPow (β := ℕ) (det (b'.toMatrix (⇑b : (a : ι) → A))) 2 *
      discr.{0, u, w} (ι := ι) ℤ (B := A) (⇑b' : (a : ι) → A)
have h : IsUnit (det (b'.toMatrix (⇑b : (a : ι) → A)))
Tactic: suffices IsUnit (b'.toMatrix b).det by
      rw [Int.isUnit_iff, ← sq_eq_one_iff] at this
      rw [this, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Discriminant (goal)
Goal:
A : Type u
ι : Type w
inst : DecidableEq ι
inst_1 : CommRing A
inst_2 : Fintype ι
b b' : Basis ι ℤ A
⊢ IsUnit (det (b'.toMatrix (⇑b : (a : ι) → A)))
have h : IsUnit (M := ℤ) (det.{0, w} (n := ι) ((LinearMap.toMatrix b b' : (a : A →ₗ[ℤ] A) → Matrix ι ι ℤ) LinearMap.id))
Tactic: rw [← LinearMap.toMatrix_id_eq_basis_toMatrix b b']
-- 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 : R
⊢ Eq (α := 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))
    ((algebraMap R (DividedPowerAlgebra R M) : (a : R) → DividedPowerAlgebra R M) a : DividedPowerAlgebra R M)
have rw : Eq (α := 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))
      ((algebraMap R (MvPolynomial.{u_2, u_1} (ℕ × M) R) : (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 [← MvPolynomial.algebraMap_eq, AlgHom.commutes]
-- 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 : R
rw :
  Eq (α := 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))
        ((algebraMap R (MvPolynomial.{u_2, u_1} (ℕ × M) R) : (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)
⊢ Eq (α := 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))
    ((algebraMap R (DividedPowerAlgebra R M) : (a : R) → DividedPowerAlgebra R M) a : DividedPowerAlgebra R M)
have rw₁ : Eq (α := RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M))
  ((algebraMap R (RingQuot (R := MvPolynomial.{u_2, u_1} (ℕ × M) R) (Rel R M)) : (a : R) → RingQuot (Rel R M)) 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 [← MvPolynomial.algebraMap_eq, AlgHom.commutes]
-- 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 : R
⊢ 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)
have 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))
Tactic: rw [← mkAlgHom_C, mkAlgHom, AlgHom.coe_mk]
-- 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 : 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))
⊢ 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)
have 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' := sorry } :
        (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_C, mkAlgHom, AlgHom.coe_mk]
-- 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 : 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))
⊢ 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)
have 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))
Tactic: rw [← mkAlgHom_C, mkAlgHom, AlgHom.coe_mk]
-- 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
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)
⊢ P f
have 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
Tactic: obtain ⟨F, hf⟩ := RingQuot.mkRingHom_surjective (DividedPowerAlgebra.Rel R M) f
-- 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
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
⊢ P f
have rw : P ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) F)
Tactic: rw [← 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
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
    ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M))
      ((C : (a : R) → MvPolynomial (ℕ × M) R) a))
have 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))
Tactic: convert! h_C a using 1
-- 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
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
⊢ 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))
have 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' := sorry } :
        (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]
-- 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
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))
⊢ 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))
have 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))
Tactic: rw [mkAlgHom, AlgHom.coe_mk]
-- 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
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 ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (g1 + g2))
have 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)))
Tactic: rw [map_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
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
⊢ P ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (g * X nm))
have 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))
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]
-- 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
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 ((mkRingHom (Rel R M) : (a : MvPolynomial (ℕ × M) R) → RingQuot (Rel R M)) (g * X nm))
have 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))
Tactic: rw [_root_.map_mul, h']