case h0
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.247072
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S 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 : Ideal R
S : Type ?u.247072
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S 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 : Ideal R
S : Type ?u.247072
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S 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
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.247072
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S 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
induction' g using PolynomialModule.induction_linear with p q hp hq
no goals
case h0
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.247072
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
r : R
n : ℕ
⊢ ↑(↑(monomial i) r • 0) n = if i ≤ n then r • ↑0 (n - i) else 0
simp only [smul_zero, zero_apply, ite_self]
case hadd
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.247072
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S 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
case hadd
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.247072
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S 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
simp only [smul_add, add_apply, hp, hq]
case hadd.inl
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.247072
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S 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 hadd.inr
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.247072
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S 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
case hadd
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.247072
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S 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
split_ifs
no goals
case hadd.inl
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.247072
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S 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 hadd.inr
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.247072
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S 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
exacts [rfl, zero_add 0]
case hsingle
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.247072
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S 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
case hsingle
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.247072
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S 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
rw [monomial_smul_single, single_apply, single_apply, smul_ite, smul_zero, ← ite_and]
case hsingle.e_c
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.247072
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
r : R
n a✝ : ℕ
b✝ : M
⊢ (i + a✝ = n) = (i ≤ n ∧ a✝ = n - i)
case hsingle
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.247072
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S 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
congr
case hsingle.e_c
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.247072
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
r : R
n a✝ : ℕ
b✝ : M
⊢ i + a✝ = n ↔ i ≤ n ∧ a✝ = n - i
case hsingle.e_c
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.247072
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
r : R
n a✝ : ℕ
b✝ : M
⊢ (i + a✝ = n) = (i ≤ n ∧ a✝ = n - i)
rw [eq_iff_iff]
case hsingle.e_c.mp
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.247072
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S 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 : Ideal R
S : Type ?u.247072
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
r : R
n a✝ : ℕ
b✝ : M
⊢ i ≤ n ∧ a✝ = n - i → i + a✝ = n
case hsingle.e_c
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.247072
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
r : R
n a✝ : ℕ
b✝ : M
⊢ i + a✝ = n ↔ i ≤ n ∧ a✝ = n - i
constructor
case hsingle.e_c.mp
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.247072
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
r : R
a✝ : ℕ
b✝ : M
⊢ i ≤ i + a✝ ∧ a✝ = i + a✝ - i
case hsingle.e_c.mp
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.247072
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
r : R
n a✝ : ℕ
b✝ : M
⊢ i + a✝ = n → i ≤ n ∧ a✝ = n - i
rintro rfl
no goals
case hsingle.e_c.mp
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.247072
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
r : R
a✝ : ℕ
b✝ : M
⊢ i ≤ i + a✝ ∧ a✝ = i + a✝ - i
simp
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 : Ideal R
S : Type ?u.247072
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
r : R
n : ℕ
b✝ : M
e : i ≤ n
⊢ i + (n - i) = n
case hsingle.e_c.mpr
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type ?u.247072
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
r : R
n a✝ : ℕ
b✝ : M
⊢ i ≤ n ∧ a✝ = n - i → i + a✝ = n
rintro ⟨e, rfl⟩
no goals
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 : Ideal R
S : Type ?u.247072
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
r : R
n : ℕ
b✝ : M
e : i ≤ n
⊢ i + (n - i) = n
rw [add_comm, tsub_add_cancel_of_le e]