internlm/Lean-Github huggingface dataset:
Theorem: DividedPowers.isExponential_dpowExp
Proof state before:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hI : DividedPowers I
a : R
ha : a ∈ I
⊢ (constantCoeff R) (hI.dpowExp a) = 1 ∧
    ∀ (p q : ℕ),
      ↑((p + q).choose p) * (coeff R (p + q)) (hI.dpowExp a) = (coeff R p) (hI.dpowExp a) * (coeff R q) (hI.dpowExp a)
Tactic:
constructor
Proof state after:
case left
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hI : DividedPowers I
a : R
ha : a ∈ I
⊢ (constantCoeff R) (hI.dpowExp a) = 1

case right
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hI : DividedPowers I
a : R
ha : a ∈ I
⊢ ∀ (p q : ℕ),
    ↑((p + q).choose p) * (coeff R (p + q)) (hI.dpowExp a) = (coeff R p) (hI.dpowExp a) * (coeff R q) (hI.dpowExp a)
Theorem: DividedPowers.isExponential_dpowExp
Proof state before:
case left
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hI : DividedPowers I
a : R
ha : a ∈ I
⊢ (constantCoeff R) (hI.dpowExp a) = 1
Tactic:
simp only [dpowExp, ← coeff_zero_eq_constantCoeff_apply, coeff_mk, dpow_zero _ ha]
Proof state after:
no goals
Theorem: DividedPowers.isExponential_dpowExp
Proof state before:
case right
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hI : DividedPowers I
a : R
ha : a ∈ I
⊢ ∀ (p q : ℕ),
    ↑((p + q).choose p) * (coeff R (p + q)) (hI.dpowExp a) = (coeff R p) (hI.dpowExp a) * (coeff R q) (hI.dpowExp a)
Tactic:
intro p q
Proof state after:
case right
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hI : DividedPowers I
a : R
ha : a ∈ I
p q : ℕ
⊢ ↑((p + q).choose p) * (coeff R (p + q)) (hI.dpowExp a) = (coeff R p) (hI.dpowExp a) * (coeff R q) (hI.dpowExp a)
Theorem: DividedPowers.isExponential_dpowExp
Proof state before:
case right
R : Type u_1
inst✝ : CommRing R
I : Ideal R
hI : DividedPowers I
a : R
ha : a ∈ I
p q : ℕ
⊢ ↑((p + q).choose p) * (coeff R (p + q)) (hI.dpowExp a) = (coeff R p) (hI.dpowExp a) * (coeff R q) (hI.dpowExp a)
Tactic:
simp only [dpowExp, coeff_mk, hI.dpow_mul p q ha]
Proof state after:
no goals
Theorem: Ideal.sub_mem_ofRel_of_rel
Proof state before:
R✝ : Type u_1
M : Type u_2
inst✝³ : CommSemiring R✝
inst✝² : AddCommMonoid M
inst✝¹ : Module R✝ M
R : Type u_3
inst✝ : Ring R
r : R → R → Prop
a b : R
hr : r a b
⊢ a - b + b = a
Tactic:
rw [sub_add_cancel]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.mk_surjective
Proof state before:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ Function.Surjective ⇑mk
Tactic:
apply RingQuot.mkAlgHom_surjective
Proof state after:
no goals
Theorem: DividedPowerAlgebra.mk_C
Proof state before:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
⊢ mk (C a) = (algebraMap R (DividedPowerAlgebra R M)) a
Tactic:
rw [← MvPolynomial.algebraMap_eq, AlgHom.commutes]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dp_eq_mkRingHom
Proof state before:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
m : M
⊢ dp R n m = (mkRingHom (Rel R M)) (X (n, m))
Tactic:
rw [dp_def, ← mkAlgHom_coe R]
Proof state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
m : M
⊢ (mkAlgHom R (Rel R M)) (X (n, m)) = ↑(mkAlgHom R (Rel R M)) (X (n, m))
Theorem: DividedPowerAlgebra.dp_eq_mkRingHom
Proof state before:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
m : M
⊢ (mkAlgHom R (Rel R M)) (X (n, m)) = ↑(mkAlgHom R (Rel R M)) (X (n, m))
Tactic:
rfl
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dp_zero
Proof state before:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ dp R 0 m = 1
Tactic:
rw [dp_def, ← map_one (mkAlgHom R (Rel R M))]
Proof state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ (mkAlgHom R (Rel R M)) (X (0, m)) = (mkAlgHom R (Rel R M)) 1
Theorem: DividedPowerAlgebra.dp_zero
Proof state before:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ (mkAlgHom R (Rel R M)) (X (0, m)) = (mkAlgHom R (Rel R M)) 1
Tactic:
exact RingQuot.mkAlgHom_rel R Rel.zero
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dp_smul
Proof state before:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
n : ℕ
m : M
⊢ dp R n (r • m) = r ^ n • dp R n m
Tactic:
rw [dp_def, dp_def, ← map_smul]
Proof state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
n : ℕ
m : M
⊢ (mkAlgHom R (Rel R M)) (X (n, r • m)) = (mkAlgHom R (Rel R M)) (r ^ n • X (n, m))
Theorem: DividedPowerAlgebra.dp_smul
Proof state before:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
n : ℕ
m : M
⊢ (mkAlgHom R (Rel R M)) (X (n, r • m)) = (mkAlgHom R (Rel R M)) (r ^ n • X (n, m))
Tactic:
exact mkAlgHom_rel R Rel.smul
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dp_null
Proof state before:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
⊢ dp R n 0 = if n = 0 then 1 else 0
Tactic:
cases' Nat.eq_zero_or_pos n with hn hn
Proof state after:
case inl
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n = 0
⊢ dp R n 0 = if n = 0 then 1 else 0

case inr
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n > 0
⊢ dp R n 0 = if n = 0 then 1 else 0
Theorem: DividedPowerAlgebra.dp_null
Proof state before:
case inl
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n = 0
⊢ dp R n 0 = if n = 0 then 1 else 0
Tactic:
rw [if_pos hn, hn, dp_zero]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dp_null
Proof state before:
case inr
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n > 0
⊢ dp R n 0 = if n = 0 then 1 else 0
Tactic:
rw [if_neg (ne_of_gt hn), ← zero_smul R (0 : M), dp_smul]
Proof state after:
case inr
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n > 0
⊢ 0 ^ n • dp R n 0 = 0
Theorem: DividedPowerAlgebra.dp_null
Proof state before:
case inr
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
hn : n > 0
⊢ 0 ^ n • dp R n 0 = 0
Tactic:
rw [zero_pow (Nat.pos_iff_ne_zero.mp hn), zero_smul]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dp_mul
Proof state before:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n p : ℕ
m : M
⊢ dp R n m * dp R p m = (n + p).choose n • dp R (n + p) m
Tactic:
simp only [dp_def, ← _root_.map_mul, ← map_nsmul]
Proof state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n p : ℕ
m : M
⊢ (mkAlgHom R (Rel R M)) (X (n, m) * X (p, m)) = (mkAlgHom R (Rel R M)) ((n + p).choose n • X (n + p, m))
Theorem: DividedPowerAlgebra.dp_mul
Proof state before:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n p : ℕ
m : M
⊢ (mkAlgHom R (Rel R M)) (X (n, m) * X (p, m)) = (mkAlgHom R (Rel R M)) ((n + p).choose n • X (n + p, m))
Tactic:
exact mkAlgHom_rel R Rel.mul
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dp_add
Proof state before:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x y : M
⊢ dp R n (x + y) = ∑ k ∈ antidiagonal n, dp R k.1 x * dp R k.2 y
Tactic:
simp only [dp_def]
Proof state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x y : M
⊢ (mkAlgHom R (Rel R M)) (X (n, x + y)) =
    ∑ x_1 ∈ antidiagonal n, (mkAlgHom R (Rel R M)) (X (x_1.1, x)) * (mkAlgHom R (Rel R M)) (X (x_1.2, y))
Theorem: DividedPowerAlgebra.dp_add
Proof state before:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x y : M
⊢ (mkAlgHom R (Rel R M)) (X (n, x + y)) =
    ∑ x_1 ∈ antidiagonal n, (mkAlgHom R (Rel R M)) (X (x_1.1, x)) * (mkAlgHom R (Rel R M)) (X (x_1.2, y))
Tactic:
rw [mkAlgHom_rel (A := MvPolynomial (ℕ × M) R) R Rel.add]
Proof state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x y : M
⊢ (mkAlgHom R (Rel R M)) (∑ k ∈ antidiagonal n, X (k.1, x) * X (k.2, y)) =
    ∑ x_1 ∈ antidiagonal n, (mkAlgHom R (Rel R M)) (X (x_1.1, x)) * (mkAlgHom R (Rel R M)) (X (x_1.2, y))
Theorem: DividedPowerAlgebra.dp_add
Proof state before:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x y : M
⊢ (mkAlgHom R (Rel R M)) (∑ k ∈ antidiagonal n, X (k.1, x) * X (k.2, y)) =
    ∑ x_1 ∈ antidiagonal n, (mkAlgHom R (Rel R M)) (X (x_1.1, x)) * (mkAlgHom R (Rel R M)) (X (x_1.2, y))
Tactic:
rw [AlgHom.map_sum]
Proof state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x y : M
⊢ ∑ x_1 ∈ antidiagonal n, (mkAlgHom R (Rel R M)) (X (x_1.1, x) * X (x_1.2, y)) =
    ∑ x_1 ∈ antidiagonal n, (mkAlgHom R (Rel R M)) (X (x_1.1, x)) * (mkAlgHom R (Rel R M)) (X (x_1.2, y))
Theorem: DividedPowerAlgebra.dp_add
Proof state before:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x y : M
⊢ ∑ x_1 ∈ antidiagonal n, (mkAlgHom R (Rel R M)) (X (x_1.1, x) * X (x_1.2, y)) =
    ∑ x_1 ∈ antidiagonal n, (mkAlgHom R (Rel R M)) (X (x_1.1, x)) * (mkAlgHom R (Rel R M)) (X (x_1.2, y))
Tactic:
apply Finset.sum_congr rfl
Proof state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x y : M
⊢ ∀ x_1 ∈ antidiagonal n,
    (mkAlgHom R (Rel R M)) (X (x_1.1, x) * X (x_1.2, y)) =
      (mkAlgHom R (Rel R M)) (X (x_1.1, x)) * (mkAlgHom R (Rel R M)) (X (x_1.2, y))
Theorem: DividedPowerAlgebra.dp_add
Proof state before:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x y : M
⊢ ∀ x_1 ∈ antidiagonal n,
    (mkAlgHom R (Rel R M)) (X (x_1.1, x) * X (x_1.2, y)) =
      (mkAlgHom R (Rel R M)) (X (x_1.1, x)) * (mkAlgHom R (Rel R M)) (X (x_1.2, y))
Tactic:
intro k _
Proof state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x y : M
k : ℕ × ℕ
a✝ : k ∈ antidiagonal n
⊢ (mkAlgHom R (Rel R M)) (X (k.1, x) * X (k.2, y)) =
    (mkAlgHom R (Rel R M)) (X (k.1, x)) * (mkAlgHom R (Rel R M)) (X (k.2, y))
Theorem: DividedPowerAlgebra.dp_add
Proof state before:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x y : M
k : ℕ × ℕ
a✝ : k ∈ antidiagonal n
⊢ (mkAlgHom R (Rel R M)) (X (k.1, x) * X (k.2, y)) =
    (mkAlgHom R (Rel R M)) (X (k.1, x)) * (mkAlgHom R (Rel R M)) (X (k.2, y))
Tactic:
rw [AlgHom.map_mul]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dp_sum
Proof state before:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
s : Finset ι
q : ℕ
x : ι → M
⊢ dp R q (s.sum x) = ∑ k ∈ s.sym q, ∏ i ∈ s, dp R (Multiset.count i ↑k) (x i)
Tactic:
apply DividedPowers.dpow_sum_aux'
Proof state after:
case dpow_zero
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
s : Finset ι
q : ℕ
x : ι → M
⊢ ∀ (x : M), dp R 0 x = 1

case dpow_add
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
s : Finset ι
q : ℕ
x : ι → M
⊢ ∀ (n : ℕ) (x y : M),
    dp R n (x + y) =
      ∑ x_1 ∈ antidiagonal n,
        match x_1 with
        | (k, l) => dp R k x * dp R l y

case dpow_eval_zero
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
s : Finset ι
q : ℕ
x : ι → M
⊢ ∀ {n : ℕ}, n ≠ 0 → dp R n 0 = 0
Theorem: DividedPowerAlgebra.dp_sum
Proof state before:
case dpow_zero
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
s : Finset ι
q : ℕ
x : ι → M
⊢ ∀ (x : M), dp R 0 x = 1
Tactic:
intro x
Proof state after:
case dpow_zero
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
s : Finset ι
q : ℕ
x✝ : ι → M
x : M
⊢ dp R 0 x = 1
Theorem: DividedPowerAlgebra.dp_sum
Proof state before:
case dpow_zero
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
s : Finset ι
q : ℕ
x✝ : ι → M
x : M
⊢ dp R 0 x = 1
Tactic:
rw [dp_zero]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dp_sum
Proof state before:
case dpow_add
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
s : Finset ι
q : ℕ
x : ι → M
⊢ ∀ (n : ℕ) (x y : M),
    dp R n (x + y) =
      ∑ x_1 ∈ antidiagonal n,
        match x_1 with
        | (k, l) => dp R k x * dp R l y
Tactic:
intro n x y
Proof state after:
case dpow_add
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
s : Finset ι
q : ℕ
x✝ : ι → M
n : ℕ
x y : M
⊢ dp R n (x + y) =
    ∑ x_1 ∈ antidiagonal n,
      match x_1 with
      | (k, l) => dp R k x * dp R l y
Theorem: DividedPowerAlgebra.dp_sum
Proof state before:
case dpow_add
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
s : Finset ι
q : ℕ
x✝ : ι → M
n : ℕ
x y : M
⊢ dp R n (x + y) =
    ∑ x_1 ∈ antidiagonal n,
      match x_1 with
      | (k, l) => dp R k x * dp R l y
Tactic:
rw [dp_add]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dp_sum
Proof state before:
case dpow_eval_zero
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
s : Finset ι
q : ℕ
x : ι → M
⊢ ∀ {n : ℕ}, n ≠ 0 → dp R n 0 = 0
Tactic:
intro n hn
Proof state after:
case dpow_eval_zero
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
s : Finset ι
q : ℕ
x : ι → M
n : ℕ
hn : n ≠ 0
⊢ dp R n 0 = 0
Theorem: DividedPowerAlgebra.dp_sum
Proof state before:
case dpow_eval_zero
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
s : Finset ι
q : ℕ
x : ι → M
n : ℕ
hn : n ≠ 0
⊢ dp R n 0 = 0
Tactic:
rw [dp_null R n, if_neg hn]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.dp_sum_smul
Proof state before:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
s : Finset ι
q : ℕ
a : ι → R
x : ι → M
⊢ dp R q (∑ i ∈ s, a i • x i) =
    ∑ k ∈ s.sym q, (∏ i ∈ s, a i ^ Multiset.count i ↑k) • ∏ i ∈ s, dp R (Multiset.count i ↑k) (x i)
Tactic:
simp_rw [dp_sum, dp_smul, Algebra.smul_def, map_prod, ← Finset.prod_mul_distrib]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.ext_iff
Proof state before:
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
⊢ f = g ↔ ∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)
Tactic:
constructor
Proof state after:
case mp
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
⊢ f = g → ∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)

case mpr
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
⊢ (∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)) → f = g
Theorem: DividedPowerAlgebra.ext_iff
Proof state before:
case mp
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
⊢ f = g → ∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)

case mpr
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
⊢ (∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)) → f = g
Tactic:
. intro h n m
  rw [h]
Proof state after:
case mpr
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
⊢ (∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)) → f = g
Theorem: DividedPowerAlgebra.ext_iff
Proof state before:
case mpr
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
⊢ (∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)) → f = g
Tactic:
. intro h
  rw [DFunLike.ext'_iff]
  apply Function.Surjective.injective_comp_right (mkAlgHom_surjective R (Rel R M))
  dsimp only
  rw [← AlgHom.coe_comp, ← AlgHom.coe_comp, ← DFunLike.ext'_iff]
  exact MvPolynomial.algHom_ext fun ⟨n, m⟩ => h n m
Proof state after:
no goals
Theorem: DividedPowerAlgebra.ext_iff
Proof state before:
case mp
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
⊢ f = g → ∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)
Tactic:
intro h n m
Proof state after:
case mp
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
h : f = g
n : ℕ
m : M
⊢ f (dp R n m) = g (dp R n m)
Theorem: DividedPowerAlgebra.ext_iff
Proof state before:
case mp
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
h : f = g
n : ℕ
m : M
⊢ f (dp R n m) = g (dp R n m)
Tactic:
rw [h]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.ext_iff
Proof state before:
case mpr
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
⊢ (∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)) → f = g
Tactic:
intro h
Proof state after:
case mpr
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
h : ∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)
⊢ f = g
Theorem: DividedPowerAlgebra.ext_iff
Proof state before:
case mpr
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
h : ∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)
⊢ f = g
Tactic:
rw [DFunLike.ext'_iff]
Proof state after:
case mpr
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
h : ∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)
⊢ ⇑f = ⇑g
Theorem: DividedPowerAlgebra.ext_iff
Proof state before:
case mpr
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
h : ∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)
⊢ ⇑f = ⇑g
Tactic:
apply Function.Surjective.injective_comp_right (mkAlgHom_surjective R (Rel R M))
Proof state after:
case mpr.a
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
h : ∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)
⊢ (fun g => g ∘ ⇑(mkAlgHom R (Rel R M))) ⇑f = (fun g => g ∘ ⇑(mkAlgHom R (Rel R M))) ⇑g
Theorem: DividedPowerAlgebra.ext_iff
Proof state before:
case mpr.a
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
h : ∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)
⊢ (fun g => g ∘ ⇑(mkAlgHom R (Rel R M))) ⇑f = (fun g => g ∘ ⇑(mkAlgHom R (Rel R M))) ⇑g
Tactic:
dsimp only
Proof state after:
case mpr.a
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
h : ∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)
⊢ ⇑f ∘ ⇑(mkAlgHom R (Rel R M)) = ⇑g ∘ ⇑(mkAlgHom R (Rel R M))
Theorem: DividedPowerAlgebra.ext_iff
Proof state before:
case mpr.a
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
h : ∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)
⊢ ⇑f ∘ ⇑(mkAlgHom R (Rel R M)) = ⇑g ∘ ⇑(mkAlgHom R (Rel R M))
Tactic:
rw [← AlgHom.coe_comp, ← AlgHom.coe_comp, ← DFunLike.ext'_iff]
Proof state after:
case mpr.a
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
h : ∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)
⊢ f.comp (mkAlgHom R (Rel R M)) = g.comp (mkAlgHom R (Rel R M))
Theorem: DividedPowerAlgebra.ext_iff
Proof state before:
case mpr.a
R : Type u_1
M : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
f g : DividedPowerAlgebra R M →ₐ[R] A
h : ∀ (n : ℕ) (m : M), f (dp R n m) = g (dp R n m)
⊢ f.comp (mkAlgHom R (Rel R M)) = g.comp (mkAlgHom R (Rel R M))
Tactic:
exact MvPolynomial.algHom_ext fun ⟨n, m⟩ => h n m
Proof state after:
no goals
Theorem: DividedPowerAlgebra.induction_on
Proof state before:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : DividedPowerAlgebra R M → Prop
f : DividedPowerAlgebra R M
h_C : ∀ (a : R), P (mk (C 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
Tactic:
obtain ⟨F, hf⟩ :=  RingQuot.mkRingHom_surjective (DividedPowerAlgebra.Rel R M) f
Proof state after:
case intro
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : DividedPowerAlgebra R M → Prop
f : DividedPowerAlgebra R M
h_C : ∀ (a : R), P (mk (C 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 (ℕ × M) R
hf : (mkRingHom (Rel R M)) F = f
⊢ P f
Theorem: DividedPowerAlgebra.induction_on
Proof state before:
case intro
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : DividedPowerAlgebra R M → Prop
f : DividedPowerAlgebra R M
h_C : ∀ (a : R), P (mk (C 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 (ℕ × M) R
hf : (mkRingHom (Rel R M)) F = f
⊢ P f
Tactic:
rw [← hf]
Proof state after:
case intro
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : DividedPowerAlgebra R M → Prop
f : DividedPowerAlgebra R M
h_C : ∀ (a : R), P (mk (C 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 (ℕ × M) R
hf : (mkRingHom (Rel R M)) F = f
⊢ P ((mkRingHom (Rel R M)) F)