-- Mathlib/Algebra/Polynomial/Module/Basic.lean
theorem monomial_smul_apply (i : ℕ) (r : R) (g : PolynomialModule R M) (n : ℕ) :
    (monomial i r • g) n = ite (i ≤ n) (r • g (n - i)) 0

Proof state:
case pos
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
r : R
n : ℕ
p q : PolynomialModule R M
hp : ((monomial i) r • p) n = if i ≤ n then r • p (n - i) else 0
hq : ((monomial i) r • q) n = if i ≤ n then r • q (n - i) else 0
h✝ : i ≤ n
⊢ r • p (n - i) + r • q (n - i) = r • p (n - i) + r • q (n - i)

case neg
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
r : R
n : ℕ
p q : PolynomialModule R M
hp : ((monomial i) r • p) n = if i ≤ n then r • p (n - i) else 0
hq : ((monomial i) r • q) n = if i ≤ n then r • q (n - i) else 0
h✝ : ¬i ≤ n
⊢ 0 + 0 = 0

Tactic:
exacts [rfl, zero_add 0]

Result:
no goals

Proof state:
case hsingle
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
r : R
n a✝ : ℕ
b✝ : M
⊢ (if i + a✝ = n then r • b✝ else 0) = if i ≤ n ∧ a✝ = n - i then r • b✝ else 0

Tactic:
congr

Result:
case hsingle.e_c
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
r : R
n a✝ : ℕ
b✝ : M
⊢ (i + a✝ = n) = (i ≤ n ∧ a✝ = n - i)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
r : R
g : PolynomialModule R M
n : ℕ
⊢ ((monomial i) r • g) n = if i ≤ n then r • g (n - i) else 0

Tactic:
induction' g using PolynomialModule.induction_linear with p q hp hq

Result:
case h0
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
r : R
n : ℕ
⊢ ((monomial i) r • 0) n = if i ≤ n then r • 0 (n - i) else 0

case hadd
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
r : R
n : ℕ
p q : PolynomialModule R M
hp : ((monomial i) r • p) n = if i ≤ n then r • p (n - i) else 0
hq : ((monomial i) r • q) n = if i ≤ n then r • q (n - i) else 0
⊢ ((monomial i) r • (p + q)) n = if i ≤ n then r • (p + q) (n - i) else 0

case hsingle
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
r : R
n a✝ : ℕ
b✝ : M
⊢ ((monomial i) r • (single R a✝) b✝) n = if i ≤ n then r • ((single R a✝) b✝) (n - i) else 0

Proof state:
case hsingle.e_c.mpr.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
r : R
n : ℕ
b✝ : M
e : i ≤ n
⊢ i + (n - i) = n

Tactic:
rw [add_comm, tsub_add_cancel_of_le e]

Result:
no goals

Proof state:
case hadd
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
r : R
n : ℕ
p q : PolynomialModule R M
hp : ((monomial i) r • p) n = if i ≤ n then r • p (n - i) else 0
hq : ((monomial i) r • q) n = if i ≤ n then r • q (n - i) else 0
⊢ ((if i ≤ n then r • p (n - i) else 0) + if i ≤ n then r • q (n - i) else 0) =
    if i ≤ n then r • p (n - i) + r • q (n - i) else 0

Tactic:
split_ifs

Result:
case pos
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
r : R
n : ℕ
p q : PolynomialModule R M
hp : ((monomial i) r • p) n = if i ≤ n then r • p (n - i) else 0
hq : ((monomial i) r • q) n = if i ≤ n then r • q (n - i) else 0
h✝ : i ≤ n
⊢ r • p (n - i) + r • q (n - i) = r • p (n - i) + r • q (n - i)

case neg
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
r : R
n : ℕ
p q : PolynomialModule R M
hp : ((monomial i) r • p) n = if i ≤ n then r • p (n - i) else 0
hq : ((monomial i) r • q) n = if i ≤ n then r • q (n - i) else 0
h✝ : ¬i ≤ n
⊢ 0 + 0 = 0

Proof state:
case hadd
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
r : R
n : ℕ
p q : PolynomialModule R M
hp : ((monomial i) r • p) n = if i ≤ n then r • p (n - i) else 0
hq : ((monomial i) r • q) n = if i ≤ n then r • q (n - i) else 0
⊢ ((monomial i) r • (p + q)) n = if i ≤ n then r • (p + q) (n - i) else 0

Tactic:
simp only [smul_add, add_apply, hp, hq]

Result:
case hadd
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
r : R
n : ℕ
p q : PolynomialModule R M
hp : ((monomial i) r • p) n = if i ≤ n then r • p (n - i) else 0
hq : ((monomial i) r • q) n = if i ≤ n then r • q (n - i) else 0
⊢ ((if i ≤ n then r • p (n - i) else 0) + if i ≤ n then r • q (n - i) else 0) =
    if i ≤ n then r • p (n - i) + r • q (n - i) else 0

Proof state:
case hsingle.e_c.mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
r : R
n a✝ : ℕ
b✝ : M
⊢ i + a✝ = n → i ≤ n ∧ a✝ = n - i

Tactic:
rintro rfl

Result:
case hsingle.e_c.mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
r : R
a✝ : ℕ
b✝ : M
⊢ i ≤ i + a✝ ∧ a✝ = i + a✝ - i

Proof state:
case hsingle
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
r : R
n a✝ : ℕ
b✝ : M
⊢ ((monomial i) r • (single R a✝) b✝) n = if i ≤ n then r • ((single R a✝) b✝) (n - i) else 0

Tactic:
rw [monomial_smul_single, single_apply, single_apply, smul_ite, smul_zero, ← ite_and]

Result:
case hsingle
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
r : R
n a✝ : ℕ
b✝ : M
⊢ (if i + a✝ = n then r • b✝ else 0) = if i ≤ n ∧ a✝ = n - i then r • b✝ else 0

Proof state:
case hsingle.e_c.mpr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
r : R
n a✝ : ℕ
b✝ : M
⊢ i ≤ n ∧ a✝ = n - i → i + a✝ = n

Tactic:
rintro ⟨e, rfl⟩

Result:
case hsingle.e_c.mpr.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
r : R
n : ℕ
b✝ : M
e : i ≤ n
⊢ i + (n - i) = n

Proof state:
case hsingle.e_c.mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
r : R
a✝ : ℕ
b✝ : M
⊢ i ≤ i + a✝ ∧ a✝ = i + a✝ - i

Tactic:
simp

Result:
no goals

Proof state:
case hsingle.e_c
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
r : R
n a✝ : ℕ
b✝ : M
⊢ (i + a✝ = n) = (i ≤ n ∧ a✝ = n - i)

Tactic:
rw [eq_iff_iff]

Result:
case hsingle.e_c
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
r : R
n a✝ : ℕ
b✝ : M
⊢ i + a✝ = n ↔ i ≤ n ∧ a✝ = n - i

Proof state:
case h0
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
r : R
n : ℕ
⊢ ((monomial i) r • 0) n = if i ≤ n then r • 0 (n - i) else 0

Tactic:
simp only [smul_zero, zero_apply, ite_self]

Result:
no goals

Proof state:
case hsingle.e_c
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
r : R
n a✝ : ℕ
b✝ : M
⊢ i + a✝ = n ↔ i ≤ n ∧ a✝ = n - i

Tactic:
constructor

Result:
case hsingle.e_c.mp
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
r : R
n a✝ : ℕ
b✝ : M
⊢ i + a✝ = n → i ≤ n ∧ a✝ = n - i

case hsingle.e_c.mpr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
r : R
n a✝ : ℕ
b✝ : M
⊢ i ≤ n ∧ a✝ = n - i → i + a✝ = n