-- Mathlib/Algebra/MvPolynomial/Basic.lean
theorem induction_on_monomial {M : MvPolynomial σ R → Prop} (h_C : ∀ a, M (C a))
    (h_X : ∀ p n, M p → M (p * X n)) : ∀ s a, M (monomial s a)

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
M : MvPolynomial σ R → Prop
h_C : ∀ (a : R), M (C a)
h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)
⊢ ∀ (s : σ →₀ ℕ) (a : R), M ((monomial s) a)

Tactic:
intro s a

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
M : MvPolynomial σ R → Prop
h_C : ∀ (a : R), M (C a)
h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)
s : σ →₀ ℕ
a : R
⊢ M ((monomial s) a)

Proof state:
case zero
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
M : MvPolynomial σ R → Prop
h_C : ∀ (a : R), M (C a)
h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)
s : σ →₀ ℕ
a : R
n : σ
e : ℕ
p : σ →₀ ℕ
_hpn : n ∉ p.support
_he : e ≠ 0
ih : M ((monomial p) a)
⊢ M ((monomial p) a * X n ^ 0)

Tactic:
simp [ih]

Result:
no goals

Proof state:
case ha
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
M : MvPolynomial σ R → Prop
h_C : ∀ (a : R), M (C a)
h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)
s : σ →₀ ℕ
a : R
n : σ
e : ℕ
p : σ →₀ ℕ
_hpn : n ∉ p.support
_he : e ≠ 0
ih : M ((monomial p) a)
⊢ M ((monomial (Finsupp.single n e + p)) a)

Tactic:
have : ∀ e : ℕ, M (monomial p a * X n ^ e) := by
  intro e
  induction e with
  | zero => simp [ih]
  | succ e e_ih => simp [ih, pow_succ, (mul_assoc _ _ _).symm, h_X, e_ih]

Result:
case ha
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
M : MvPolynomial σ R → Prop
h_C : ∀ (a : R), M (C a)
h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)
s : σ →₀ ℕ
a : R
n : σ
e : ℕ
p : σ →₀ ℕ
_hpn : n ∉ p.support
_he : e ≠ 0
ih : M ((monomial p) a)
this : ∀ (e : ℕ), M ((monomial p) a * X n ^ e)
⊢ M ((monomial (Finsupp.single n e + p)) a)

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
M : MvPolynomial σ R → Prop
h_C : ∀ (a : R), M (C a)
h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)
s : σ →₀ ℕ
a : R
n : σ
e✝ : ℕ
p : σ →₀ ℕ
_hpn : n ∉ p.support
_he : e✝ ≠ 0
ih : M ((monomial p) a)
e : ℕ
⊢ M ((monomial p) a * X n ^ e)

Tactic:
induction e with
| zero => simp [ih]
| succ e e_ih => simp [ih, pow_succ, (mul_assoc _ _ _).symm, h_X, e_ih]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
M : MvPolynomial σ R → Prop
h_C : ∀ (a : R), M (C a)
h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)
s : σ →₀ ℕ
a : R
n : σ
e : ℕ
p : σ →₀ ℕ
_hpn : n ∉ p.support
_he : e ≠ 0
ih : M ((monomial p) a)
⊢ ∀ (e : ℕ), M ((monomial p) a * X n ^ e)

Tactic:
intro e

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
M : MvPolynomial σ R → Prop
h_C : ∀ (a : R), M (C a)
h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)
s : σ →₀ ℕ
a : R
n : σ
e✝ : ℕ
p : σ →₀ ℕ
_hpn : n ∉ p.support
_he : e✝ ≠ 0
ih : M ((monomial p) a)
e : ℕ
⊢ M ((monomial p) a * X n ^ e)

Proof state:
case ha
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
M : MvPolynomial σ R → Prop
h_C : ∀ (a : R), M (C a)
h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)
s : σ →₀ ℕ
a : R
n : σ
e : ℕ
p : σ →₀ ℕ
_hpn : n ∉ p.support
_he : e ≠ 0
ih : M ((monomial p) a)
this : ∀ (e : ℕ), M ((monomial p) a * X n ^ e)
⊢ M ((monomial (Finsupp.single n e + p)) a)

Tactic:
simp [add_comm, monomial_add_single, this]

Result:
no goals

Proof state:
case ha
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
M : MvPolynomial σ R → Prop
h_C : ∀ (a : R), M (C a)
h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)
s : σ →₀ ℕ
a : R
⊢ ∀ (a_1 : σ) (b : ℕ) (f : σ →₀ ℕ),
    a_1 ∉ f.support → b ≠ 0 → M ((monomial f) a) → M ((monomial (Finsupp.single a_1 b + f)) a)

Tactic:
intro n e p _hpn _he ih

Result:
case ha
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
M : MvPolynomial σ R → Prop
h_C : ∀ (a : R), M (C a)
h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)
s : σ →₀ ℕ
a : R
n : σ
e : ℕ
p : σ →₀ ℕ
_hpn : n ∉ p.support
_he : e ≠ 0
ih : M ((monomial p) a)
⊢ M ((monomial (Finsupp.single n e + p)) a)

Proof state:
case h0
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
M : MvPolynomial σ R → Prop
h_C : ∀ (a : R), M (C a)
h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)
s : σ →₀ ℕ
a : R
⊢ M ((monomial 0) a)

Tactic:
exact h_C a

Result:
no goals

Proof state:
case succ
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
M : MvPolynomial σ R → Prop
h_C : ∀ (a : R), M (C a)
h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)
s : σ →₀ ℕ
a : R
n : σ
e✝ : ℕ
p : σ →₀ ℕ
_hpn : n ∉ p.support
_he : e✝ ≠ 0
ih : M ((monomial p) a)
e : ℕ
e_ih : M ((monomial p) a * X n ^ e)
⊢ M ((monomial p) a * X n ^ (e + 1))

Tactic:
simp [ih, pow_succ, (mul_assoc _ _ _).symm, h_X, e_ih]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
M : MvPolynomial σ R → Prop
h_C : ∀ (a : R), M (C a)
h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)
s : σ →₀ ℕ
a : R
⊢ M ((monomial s) a)

Tactic:
apply @Finsupp.induction σ ℕ _ _ s

Result:
case h0
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
M : MvPolynomial σ R → Prop
h_C : ∀ (a : R), M (C a)
h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)
s : σ →₀ ℕ
a : R
⊢ M ((monomial 0) a)

case ha
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
M : MvPolynomial σ R → Prop
h_C : ∀ (a : R), M (C a)
h_X : ∀ (p : MvPolynomial σ R) (n : σ), M p → M (p * X n)
s : σ →₀ ℕ
a : R
⊢ ∀ (a_1 : σ) (b : ℕ) (f : σ →₀ ℕ),
    a_1 ∉ f.support → b ≠ 0 → M ((monomial f) a) → M ((monomial (Finsupp.single a_1 b + f)) a)