internlm/Lean-Github huggingface dataset:
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 ((mkRingHom (Rel R M)) F)
Tactic:
induction F using MvPolynomial.induction_on generalizing f with
| h_C a =>
    convert h_C a using 1;
    rw [mk, mkAlgHom, AlgHom.coe_mk]
| h_add g1 g2 hg1 hg2 =>
    rw [map_add]
    exact h_add _ _ (hg1 ((mkRingHom (Rel R M)) g1) rfl) (hg2 ((mkRingHom (Rel R M)) g2) rfl)
| h_X g nm h =>
    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]
    rw [_root_.map_mul, h']
    exact h_dp _ _ _ (h (mkRingHom (Rel R M) g) rfl)
Proof state after:
no goals
Theorem: DividedPowerAlgebra.induction_on
Proof state before:
case intro.h_C
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : DividedPowerAlgebra R M → Prop
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)
a : R
f : DividedPowerAlgebra R M
hf : (mkRingHom (Rel R M)) (C a) = f
⊢ P ((mkRingHom (Rel R M)) (C a))
Tactic:
convert h_C a using 1
Proof state after:
case h.e'_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : DividedPowerAlgebra R M → Prop
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)
a : R
f : DividedPowerAlgebra R M
hf : (mkRingHom (Rel R M)) (C a) = f
⊢ (mkRingHom (Rel R M)) (C a) = mk (C a)
Theorem: DividedPowerAlgebra.induction_on
Proof state before:
case h.e'_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : DividedPowerAlgebra R M → Prop
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)
a : R
f : DividedPowerAlgebra R M
hf : (mkRingHom (Rel R M)) (C a) = f
⊢ (mkRingHom (Rel R M)) (C a) = mk (C a)
Tactic:
rw [mk, mkAlgHom, AlgHom.coe_mk]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.induction_on
Proof state before:
case intro.h_add
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : DividedPowerAlgebra R M → Prop
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)
g1 g2 : MvPolynomial (ℕ × M) R
hg1 : ∀ (f : DividedPowerAlgebra R M), (mkRingHom (Rel R M)) g1 = f → P ((mkRingHom (Rel R M)) g1)
hg2 : ∀ (f : DividedPowerAlgebra R M), (mkRingHom (Rel R M)) g2 = f → P ((mkRingHom (Rel R M)) g2)
f : DividedPowerAlgebra R M
hf : (mkRingHom (Rel R M)) (g1 + g2) = f
⊢ P ((mkRingHom (Rel R M)) (g1 + g2))
Tactic:
rw [map_add]
Proof state after:
case intro.h_add
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : DividedPowerAlgebra R M → Prop
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)
g1 g2 : MvPolynomial (ℕ × M) R
hg1 : ∀ (f : DividedPowerAlgebra R M), (mkRingHom (Rel R M)) g1 = f → P ((mkRingHom (Rel R M)) g1)
hg2 : ∀ (f : DividedPowerAlgebra R M), (mkRingHom (Rel R M)) g2 = f → P ((mkRingHom (Rel R M)) g2)
f : DividedPowerAlgebra R M
hf : (mkRingHom (Rel R M)) (g1 + g2) = f
⊢ P ((mkRingHom (Rel R M)) g1 + (mkRingHom (Rel R M)) g2)
Theorem: DividedPowerAlgebra.induction_on
Proof state before:
case intro.h_add
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : DividedPowerAlgebra R M → Prop
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)
g1 g2 : MvPolynomial (ℕ × M) R
hg1 : ∀ (f : DividedPowerAlgebra R M), (mkRingHom (Rel R M)) g1 = f → P ((mkRingHom (Rel R M)) g1)
hg2 : ∀ (f : DividedPowerAlgebra R M), (mkRingHom (Rel R M)) g2 = f → P ((mkRingHom (Rel R M)) g2)
f : DividedPowerAlgebra R M
hf : (mkRingHom (Rel R M)) (g1 + g2) = f
⊢ P ((mkRingHom (Rel R M)) g1 + (mkRingHom (Rel R M)) g2)
Tactic:
exact h_add _ _ (hg1 ((mkRingHom (Rel R M)) g1) rfl) (hg2 ((mkRingHom (Rel R M)) g2) rfl)
Proof state after:
no goals
Theorem: DividedPowerAlgebra.induction_on
Proof state before:
case intro.h_X
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : DividedPowerAlgebra R M → Prop
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)
g : MvPolynomial (ℕ × M) R
nm : ℕ × M
h : ∀ (f : DividedPowerAlgebra R M), (mkRingHom (Rel R M)) g = f → P ((mkRingHom (Rel R M)) g)
f : DividedPowerAlgebra R M
hf : (mkRingHom (Rel R M)) (g * X nm) = f
⊢ P ((mkRingHom (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]
Proof state after:
case intro.h_X
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : DividedPowerAlgebra R M → Prop
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)
g : MvPolynomial (ℕ × M) R
nm : ℕ × M
h : ∀ (f : DividedPowerAlgebra R M), (mkRingHom (Rel R M)) g = f → P ((mkRingHom (Rel R M)) g)
f : DividedPowerAlgebra R M
hf : (mkRingHom (Rel R M)) (g * X nm) = f
h' : (mkRingHom (Rel R M)) (X nm) = dp R nm.1 nm.2
⊢ P ((mkRingHom (Rel R M)) (g * X nm))
Theorem: DividedPowerAlgebra.induction_on
Proof state before:
case intro.h_X
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : DividedPowerAlgebra R M → Prop
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)
g : MvPolynomial (ℕ × M) R
nm : ℕ × M
h : ∀ (f : DividedPowerAlgebra R M), (mkRingHom (Rel R M)) g = f → P ((mkRingHom (Rel R M)) g)
f : DividedPowerAlgebra R M
hf : (mkRingHom (Rel R M)) (g * X nm) = f
h' : (mkRingHom (Rel R M)) (X nm) = dp R nm.1 nm.2
⊢ P ((mkRingHom (Rel R M)) (g * X nm))
Tactic:
rw [_root_.map_mul, h']
Proof state after:
case intro.h_X
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : DividedPowerAlgebra R M → Prop
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)
g : MvPolynomial (ℕ × M) R
nm : ℕ × M
h : ∀ (f : DividedPowerAlgebra R M), (mkRingHom (Rel R M)) g = f → P ((mkRingHom (Rel R M)) g)
f : DividedPowerAlgebra R M
hf : (mkRingHom (Rel R M)) (g * X nm) = f
h' : (mkRingHom (Rel R M)) (X nm) = dp R nm.1 nm.2
⊢ P ((mkRingHom (Rel R M)) g * dp R nm.1 nm.2)
Theorem: DividedPowerAlgebra.induction_on
Proof state before:
case intro.h_X
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
P : DividedPowerAlgebra R M → Prop
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)
g : MvPolynomial (ℕ × M) R
nm : ℕ × M
h : ∀ (f : DividedPowerAlgebra R M), (mkRingHom (Rel R M)) g = f → P ((mkRingHom (Rel R M)) g)
f : DividedPowerAlgebra R M
hf : (mkRingHom (Rel R M)) (g * X nm) = f
h' : (mkRingHom (Rel R M)) (X nm) = dp R nm.1 nm.2
⊢ P ((mkRingHom (Rel R M)) g * dp R nm.1 nm.2)
Tactic:
exact h_dp _ _ _ (h (mkRingHom (Rel R M) g) rfl)
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
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)
g : MvPolynomial (ℕ × M) R
nm : ℕ × M
h : ∀ (f : DividedPowerAlgebra R M), (mkRingHom (Rel R M)) g = f → P ((mkRingHom (Rel R M)) g)
f : DividedPowerAlgebra R M
hf : (mkRingHom (Rel R M)) (g * X nm) = f
⊢ (mkRingHom (Rel R M)) (X nm) = dp R nm.1 nm.2
Tactic:
simp only [dp_def, Prod.mk.eta, mkAlgHom, AlgHom.coe_mk]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.lift'_imp
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 : ℕ × 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 n,
        match x with
        | (k, l) => f (k, u) * f (l, v)
p q : MvPolynomial (ℕ × M) R
h : Rel R M p q
⊢ (eval₂AlgHom R f) p = (eval₂AlgHom R f) q
Tactic:
cases' h with a r n a m n a n a b <;>
  simp only [eval₂AlgHom_X', map_one, map_zero, map_smul, AlgHom.map_mul, map_nsmul, AlgHom.map_sum]
Proof state after:
case zero
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 : ℕ × 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 n,
        match x with
        | (k, l) => f (k, u) * f (l, v)
a : M
⊢ f (0, a) = 1

case smul
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 : ℕ × 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 n,
        match x with
        | (k, l) => f (k, u) * f (l, v)
r : R
n : ℕ
a : M
⊢ f (n, r • a) = r ^ n • f (n, a)

case mul
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 : ℕ × 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 n,
        match x with
        | (k, l) => f (k, u) * f (l, v)
m n : ℕ
a : M
⊢ f (m, a) * f (n, a) = (m + n).choose m • f (m + n, a)

case add
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 : ℕ × 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 n,
        match x with
        | (k, l) => f (k, u) * f (l, v)
n : ℕ
a b : M
⊢ f (n, a + b) = ∑ x ∈ antidiagonal n, f (x.1, a) * f (x.2, b)
Theorem: DividedPowerAlgebra.lift'_imp
Proof state before:
case smul
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 : ℕ × 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 n,
        match x with
        | (k, l) => f (k, u) * f (l, v)
r : R
n : ℕ
a : M
⊢ f (n, r • a) = r ^ n • f (n, a)

case mul
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 : ℕ × 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 n,
        match x with
        | (k, l) => f (k, u) * f (l, v)
m n : ℕ
a : M
⊢ f (m, a) * f (n, a) = (m + n).choose m • f (m + n, a)

case add
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 : ℕ × 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 n,
        match x with
        | (k, l) => f (k, u) * f (l, v)
n : ℕ
a b : M
⊢ f (n, a + b) = ∑ x ∈ antidiagonal n, f (x.1, a) * f (x.2, b)
Tactic:
. apply hf_smul
Proof state after:
case mul
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 : ℕ × 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 n,
        match x with
        | (k, l) => f (k, u) * f (l, v)
m n : ℕ
a : M
⊢ f (m, a) * f (n, a) = (m + n).choose m • f (m + n, a)

case add
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 : ℕ × 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 n,
        match x with
        | (k, l) => f (k, u) * f (l, v)
n : ℕ
a b : M
⊢ f (n, a + b) = ∑ x ∈ antidiagonal n, f (x.1, a) * f (x.2, b)
Theorem: DividedPowerAlgebra.lift'_imp
Proof state before:
case mul
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 : ℕ × 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 n,
        match x with
        | (k, l) => f (k, u) * f (l, v)
m n : ℕ
a : M
⊢ f (m, a) * f (n, a) = (m + n).choose m • f (m + n, a)

case add
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 : ℕ × 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 n,
        match x with
        | (k, l) => f (k, u) * f (l, v)
n : ℕ
a b : M
⊢ f (n, a + b) = ∑ x ∈ antidiagonal n, f (x.1, a) * f (x.2, b)
Tactic:
. apply hf_mul
Proof state after:
case add
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 : ℕ × 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 n,
        match x with
        | (k, l) => f (k, u) * f (l, v)
n : ℕ
a b : M
⊢ f (n, a + b) = ∑ x ∈ antidiagonal n, f (x.1, a) * f (x.2, b)
Theorem: DividedPowerAlgebra.lift'_imp
Proof state before:
case add
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 : ℕ × 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 n,
        match x with
        | (k, l) => f (k, u) * f (l, v)
n : ℕ
a b : M
⊢ f (n, a + b) = ∑ x ∈ antidiagonal n, f (x.1, a) * f (x.2, b)
Tactic:
. apply hf_add
Proof state after:
no goals
Theorem: DividedPowerAlgebra.lift'_imp
Proof state before:
case zero
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 : ℕ × 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 n,
        match x with
        | (k, l) => f (k, u) * f (l, v)
a : M
⊢ f (0, a) = 1
Tactic:
apply hf_zero
Proof state after:
no goals
Theorem: DividedPowerAlgebra.lift'_imp
Proof state before:
case smul
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 : ℕ × 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 n,
        match x with
        | (k, l) => f (k, u) * f (l, v)
r : R
n : ℕ
a : M
⊢ f (n, r • a) = r ^ n • f (n, a)
Tactic:
apply hf_smul
Proof state after:
no goals
Theorem: DividedPowerAlgebra.lift'_imp
Proof state before:
case mul
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 : ℕ × 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 n,
        match x with
        | (k, l) => f (k, u) * f (l, v)
m n : ℕ
a : M
⊢ f (m, a) * f (n, a) = (m + n).choose m • f (m + n, a)
Tactic:
apply hf_mul
Proof state after:
no goals
Theorem: DividedPowerAlgebra.lift'_imp
Proof state before:
case add
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 : ℕ × 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 n,
        match x with
        | (k, l) => f (k, u) * f (l, v)
n : ℕ
a b : M
⊢ f (n, a + b) = ∑ x ∈ antidiagonal n, f (x.1, a) * f (x.2, b)
Tactic:
apply hf_add
Proof state after:
no goals
Theorem: DividedPowerAlgebra.lift'AlgHom_apply
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 : ℕ × 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 n,
        match x with
        | (k, l) => f (k, u) * f (l, v)
p : MvPolynomial (ℕ × M) R
⊢ (lift' f hf_zero hf_smul hf_mul hf_add) (mk p) = (aeval f) p
Tactic:
rw [mk, lift', RingQuot.liftAlgHom_mkAlgHom_apply, coe_eval₂AlgHom]
Proof state after:
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 : ℕ × 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 n,
        match x with
        | (k, l) => f (k, u) * f (l, v)
p : MvPolynomial (ℕ × M) R
⊢ eval₂ (algebraMap R A) f p = (aeval f) p
Theorem: DividedPowerAlgebra.lift'AlgHom_apply
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 : ℕ × 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 n,
        match x with
        | (k, l) => f (k, u) * f (l, v)
p : MvPolynomial (ℕ × M) R
⊢ eval₂ (algebraMap R A) f p = (aeval f) p
Tactic:
rfl
Proof state after:
no goals
Theorem: DividedPowerAlgebra.lift'AlgHom_apply_dp
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 : ℕ × 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 n,
        match x with
        | (k, l) => f (k, u) * f (l, v)
n : ℕ
m : M
⊢ (lift' f hf_zero hf_smul hf_mul hf_add) (dp R n m) = f (n, m)
Tactic:
rw [dp_def, ← mk, lift'AlgHom_apply f hf_zero hf_smul hf_mul hf_add, aeval_X]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.liftAlgHom_apply
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
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
p : MvPolynomial (ℕ × M) R
⊢ (lift hI φ hφ) (mk p) = (aeval fun nm => hI.dpow nm.1 (φ nm.2)) p
Tactic:
rw [lift, lift'AlgHom_apply]
Proof state after:
no goals
Theorem: DividedPowerAlgebra.liftAlgHom_apply_dp
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
I : Ideal A
hI : DividedPowers I
φ : M →ₗ[R] A
hφ : ∀ (m : M), φ m ∈ I
n : ℕ
m : M
⊢ (lift hI φ hφ) (dp R n m) = hI.dpow n (φ m)
Tactic:
rw [lift, lift'AlgHom_apply_dp]
Proof state after:
no goals