Theorem: DividedPowerAlgebra.induction_on (DividedPowers/DPAlgebra/Init.lean)

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
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

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]
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)

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)
State after:
no goals

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
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)

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]
State after:
no goals

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]
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)

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)
State after:
no goals

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]
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))

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']
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)

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)
State after:
no goals

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]
State after:
no goals