[GOAL]
b : Bool
h : Decidable (b = true)
⊢ decide (b = true) = b
[PROOFSTEP]
cases b
[GOAL]
case false
h : Decidable (false = true)
⊢ decide (false = true) = false
[PROOFSTEP]
exact decide_eq_false $ λ j => by cases j
[GOAL]
h : Decidable (false = true)
j : false = true
⊢ False
[PROOFSTEP]
cases j
[GOAL]
case true
h : Decidable (true = true)
⊢ decide (true = true) = true
[PROOFSTEP]
exact decide_eq_true $ rfl
[GOAL]
p : Prop
inst✝ : Decidable p
⊢ (decide ¬p) = !decide p
[PROOFSTEP]
by_cases p
[GOAL]
p : Prop
inst✝ : Decidable p
⊢ (decide ¬p) = !decide p
[PROOFSTEP]
by_cases p
[GOAL]
case pos
p : Prop
inst✝ : Decidable p
h : p
⊢ (decide ¬p) = !decide p
[PROOFSTEP]
simp [*]
[GOAL]
case neg
p : Prop
inst✝ : Decidable p
h : ¬p
⊢ (decide ¬p) = !decide p
[PROOFSTEP]
simp [*]
[GOAL]
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
⊢ decide (p ∧ q) = (decide p && decide q)
[PROOFSTEP]
by_cases p
[GOAL]
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
⊢ decide (p ∧ q) = (decide p && decide q)
[PROOFSTEP]
by_cases p
[GOAL]
case pos
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h : p
⊢ decide (p ∧ q) = (decide p && decide q)
[PROOFSTEP]
by_cases q
[GOAL]
case pos
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h : p
⊢ decide (p ∧ q) = (decide p && decide q)
[PROOFSTEP]
by_cases q
[GOAL]
case neg
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h : ¬p
⊢ decide (p ∧ q) = (decide p && decide q)
[PROOFSTEP]
by_cases q
[GOAL]
case neg
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h : ¬p
⊢ decide (p ∧ q) = (decide p && decide q)
[PROOFSTEP]
by_cases q
[GOAL]
case pos
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h✝ : p
h : q
⊢ decide (p ∧ q) = (decide p && decide q)
[PROOFSTEP]
simp [*]
[GOAL]
case neg
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h✝ : p
h : ¬q
⊢ decide (p ∧ q) = (decide p && decide q)
[PROOFSTEP]
simp [*]
[GOAL]
case pos
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h✝ : ¬p
h : q
⊢ decide (p ∧ q) = (decide p && decide q)
[PROOFSTEP]
simp [*]
[GOAL]
case neg
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h✝ : ¬p
h : ¬q
⊢ decide (p ∧ q) = (decide p && decide q)
[PROOFSTEP]
simp [*]
[GOAL]
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
⊢ decide (p ∨ q) = (decide p || decide q)
[PROOFSTEP]
by_cases p
[GOAL]
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
⊢ decide (p ∨ q) = (decide p || decide q)
[PROOFSTEP]
by_cases p
[GOAL]
case pos
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h : p
⊢ decide (p ∨ q) = (decide p || decide q)
[PROOFSTEP]
by_cases q
[GOAL]
case pos
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h : p
⊢ decide (p ∨ q) = (decide p || decide q)
[PROOFSTEP]
by_cases q
[GOAL]
case neg
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h : ¬p
⊢ decide (p ∨ q) = (decide p || decide q)
[PROOFSTEP]
by_cases q
[GOAL]
case neg
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h : ¬p
⊢ decide (p ∨ q) = (decide p || decide q)
[PROOFSTEP]
by_cases q
[GOAL]
case pos
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h✝ : p
h : q
⊢ decide (p ∨ q) = (decide p || decide q)
[PROOFSTEP]
simp [*]
[GOAL]
case neg
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h✝ : p
h : ¬q
⊢ decide (p ∨ q) = (decide p || decide q)
[PROOFSTEP]
simp [*]
[GOAL]
case pos
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h✝ : ¬p
h : q
⊢ decide (p ∨ q) = (decide p || decide q)
[PROOFSTEP]
simp [*]
[GOAL]
case neg
p q : Prop
inst✝¹ : Decidable p
inst✝ : Decidable q
h✝ : ¬p
h : ¬q
⊢ decide (p ∨ q) = (decide p || decide q)
[PROOFSTEP]
simp [*]
[GOAL]
a b : Bool
⊢ a = b ↔ (a = true ↔ b = true)
[PROOFSTEP]
cases a
[GOAL]
case false
b : Bool
⊢ false = b ↔ (false = true ↔ b = true)
[PROOFSTEP]
cases b
[GOAL]
case true
b : Bool
⊢ true = b ↔ (true = true ↔ b = true)
[PROOFSTEP]
cases b
[GOAL]
case false.false
⊢ false = false ↔ (false = true ↔ false = true)
[PROOFSTEP]
simp
  -- Porting note: new theorem
[GOAL]
case false.true
⊢ false = true ↔ (false = true ↔ true = true)
[PROOFSTEP]
simp
  -- Porting note: new theorem
[GOAL]
case true.false
⊢ true = false ↔ (true = true ↔ false = true)
[PROOFSTEP]
simp
  -- Porting note: new theorem
[GOAL]
case true.true
⊢ true = true ↔ (true = true ↔ true = true)
[PROOFSTEP]
simp
  -- Porting note: new theorem
[GOAL]
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
⊢ (a == b) = true ↔ (b == a) = true
[PROOFSTEP]
simp [@eq_comm α]
[GOAL]
b : Bool
⊢ b = false ∨ b = true
[PROOFSTEP]
cases b
[GOAL]
case false
⊢ false = false ∨ false = true
[PROOFSTEP]
simp
[GOAL]
case true
⊢ true = false ∨ true = true
[PROOFSTEP]
simp
[GOAL]
p : Bool → Prop
h : ∀ (b : Bool), p b
⊢ p false ∧ p true
[PROOFSTEP]
simp [h]
[GOAL]
p : Bool → Prop
x✝ : p false ∧ p true
b : Bool
h₁ : p false
h₂ : p true
⊢ p b
[PROOFSTEP]
cases b
[GOAL]
case false
p : Bool → Prop
x✝ : p false ∧ p true
h₁ : p false
h₂ : p true
⊢ p false
[PROOFSTEP]
assumption
[GOAL]
case true
p : Bool → Prop
x✝ : p false ∧ p true
h₁ : p false
h₂ : p true
⊢ p true
[PROOFSTEP]
assumption
[GOAL]
p : Bool → Prop
x✝ : ∃ b, p b
b : Bool
h : p b
⊢ p false ∨ p true
[PROOFSTEP]
cases b
[GOAL]
case false
p : Bool → Prop
x✝ : ∃ b, p b
h : p false
⊢ p false ∨ p true
case true p : Bool → Prop x✝ : ∃ b, p b h : p true ⊢ p false ∨ p true
[PROOFSTEP]
exact Or.inl h
[GOAL]
case true
p : Bool → Prop
x✝ : ∃ b, p b
h : p true
⊢ p false ∨ p true
[PROOFSTEP]
exact Or.inr h
[GOAL]
α : Type u_1
b : Bool
t e : α
⊢ (bif b then t else e) = if b = true then t else e
[PROOFSTEP]
cases b
[GOAL]
case false
α : Type u_1
t e : α
⊢ (bif false then t else e) = if false = true then t else e
[PROOFSTEP]
simp
[GOAL]
case true
α : Type u_1
t e : α
⊢ (bif true then t else e) = if true = true then t else e
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
p : Prop
inst✝ : Decidable p
t e : α
⊢ (bif decide p then t else e) = if p then t else e
[PROOFSTEP]
by_cases p
[GOAL]
α : Type u_1
p : Prop
inst✝ : Decidable p
t e : α
⊢ (bif decide p then t else e) = if p then t else e
[PROOFSTEP]
by_cases p
[GOAL]
case pos
α : Type u_1
p : Prop
inst✝ : Decidable p
t e : α
h : p
⊢ (bif decide p then t else e) = if p then t else e
[PROOFSTEP]
simp [*]
[GOAL]
case neg
α : Type u_1
p : Prop
inst✝ : Decidable p
t e : α
h : ¬p
⊢ (bif decide p then t else e) = if p then t else e
[PROOFSTEP]
simp [*]
[GOAL]
α : Type u_1
b : Bool
t e : α
⊢ (bif !b then t else e) = bif b then e else t
[PROOFSTEP]
cases b
[GOAL]
case false
α : Type u_1
t e : α
⊢ (bif !false then t else e) = bif false then e else t
[PROOFSTEP]
rfl
[GOAL]
case true
α : Type u_1
t e : α
⊢ (bif !true then t else e) = bif true then e else t
[PROOFSTEP]
rfl
[GOAL]
⊢ ∀ {a b : Bool}, (a = true ↔ b = true) ↔ a = b
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ {a : Bool}, a ≠ false → a = true
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ {a : Bool}, a ≠ true → a = false
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a b : Bool), (a || b) = (b || a)
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a b c : Bool), (a || (b || c)) = (b || (a || c))
[PROOFSTEP]
decide
[GOAL]
a b : Bool
H : a = true
⊢ (a || b) = true
[PROOFSTEP]
simp [H]
[GOAL]
a b : Bool
H : b = true
⊢ (a || b) = true
[PROOFSTEP]
cases a
[GOAL]
case false
b : Bool
H : b = true
⊢ (false || b) = true
[PROOFSTEP]
simp [H]
[GOAL]
case true
b : Bool
H : b = true
⊢ (true || b) = true
[PROOFSTEP]
simp [H]
[GOAL]
⊢ ∀ (a b : Bool), (a && b) = (b && a)
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a b c : Bool), (a && (b && c)) = (b && (a && c))
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ {a b : Bool}, (a && b) = true → a = true
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ {a b : Bool}, a = true → b = true → (a && b) = true
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ {a b : Bool}, (a && b) = true → b = true
[PROOFSTEP]
decide
[GOAL]
a b c : Bool
⊢ (a && (b || c)) = (a && b || a && c)
[PROOFSTEP]
cases a
[GOAL]
case false
b c : Bool
⊢ (false && (b || c)) = (false && b || false && c)
[PROOFSTEP]
simp
[GOAL]
case true
b c : Bool
⊢ (true && (b || c)) = (true && b || true && c)
[PROOFSTEP]
simp
[GOAL]
a b c : Bool
⊢ ((a || b) && c) = (a && c || b && c)
[PROOFSTEP]
cases a
[GOAL]
case false
b c : Bool
⊢ ((false || b) && c) = (false && c || b && c)
[PROOFSTEP]
cases b
[GOAL]
case true
b c : Bool
⊢ ((true || b) && c) = (true && c || b && c)
[PROOFSTEP]
cases b
[GOAL]
case false.false
c : Bool
⊢ ((false || false) && c) = (false && c || false && c)
[PROOFSTEP]
cases c
[GOAL]
case false.true
c : Bool
⊢ ((false || true) && c) = (false && c || true && c)
[PROOFSTEP]
cases c
[GOAL]
case true.false
c : Bool
⊢ ((true || false) && c) = (true && c || false && c)
[PROOFSTEP]
cases c
[GOAL]
case true.true
c : Bool
⊢ ((true || true) && c) = (true && c || true && c)
[PROOFSTEP]
cases c
[GOAL]
case false.false.false
⊢ ((false || false) && false) = (false && false || false && false)
[PROOFSTEP]
simp
[GOAL]
case false.false.true
⊢ ((false || false) && true) = (false && true || false && true)
[PROOFSTEP]
simp
[GOAL]
case false.true.false
⊢ ((false || true) && false) = (false && false || true && false)
[PROOFSTEP]
simp
[GOAL]
case false.true.true
⊢ ((false || true) && true) = (false && true || true && true)
[PROOFSTEP]
simp
[GOAL]
case true.false.false
⊢ ((true || false) && false) = (true && false || false && false)
[PROOFSTEP]
simp
[GOAL]
case true.false.true
⊢ ((true || false) && true) = (true && true || false && true)
[PROOFSTEP]
simp
[GOAL]
case true.true.false
⊢ ((true || true) && false) = (true && false || true && false)
[PROOFSTEP]
simp
[GOAL]
case true.true.true
⊢ ((true || true) && true) = (true && true || true && true)
[PROOFSTEP]
simp
[GOAL]
a b c : Bool
⊢ (a || b && c) = ((a || b) && (a || c))
[PROOFSTEP]
cases a
[GOAL]
case false
b c : Bool
⊢ (false || b && c) = ((false || b) && (false || c))
[PROOFSTEP]
simp
[GOAL]
case true
b c : Bool
⊢ (true || b && c) = ((true || b) && (true || c))
[PROOFSTEP]
simp
[GOAL]
a b c : Bool
⊢ (a && b || c) = ((a || c) && (b || c))
[PROOFSTEP]
cases a
[GOAL]
case false
b c : Bool
⊢ (false && b || c) = ((false || c) && (b || c))
[PROOFSTEP]
cases b
[GOAL]
case true
b c : Bool
⊢ (true && b || c) = ((true || c) && (b || c))
[PROOFSTEP]
cases b
[GOAL]
case false.false
c : Bool
⊢ (false && false || c) = ((false || c) && (false || c))
[PROOFSTEP]
cases c
[GOAL]
case false.true
c : Bool
⊢ (false && true || c) = ((false || c) && (true || c))
[PROOFSTEP]
cases c
[GOAL]
case true.false
c : Bool
⊢ (true && false || c) = ((true || c) && (false || c))
[PROOFSTEP]
cases c
[GOAL]
case true.true
c : Bool
⊢ (true && true || c) = ((true || c) && (true || c))
[PROOFSTEP]
cases c
[GOAL]
case false.false.false
⊢ (false && false || false) = ((false || false) && (false || false))
[PROOFSTEP]
simp
[GOAL]
case false.false.true
⊢ (false && false || true) = ((false || true) && (false || true))
[PROOFSTEP]
simp
[GOAL]
case false.true.false
⊢ (false && true || false) = ((false || false) && (true || false))
[PROOFSTEP]
simp
[GOAL]
case false.true.true
⊢ (false && true || true) = ((false || true) && (true || true))
[PROOFSTEP]
simp
[GOAL]
case true.false.false
⊢ (true && false || false) = ((true || false) && (false || false))
[PROOFSTEP]
simp
[GOAL]
case true.false.true
⊢ (true && false || true) = ((true || true) && (false || true))
[PROOFSTEP]
simp
[GOAL]
case true.true.false
⊢ (true && true || false) = ((true || false) && (true || false))
[PROOFSTEP]
simp
[GOAL]
case true.true.true
⊢ (true && true || true) = ((true || true) && (true || true))
[PROOFSTEP]
simp
[GOAL]
⊢ ∀ {a b : Bool}, a = !b ↔ a ≠ b
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ {a b : Bool}, (!decide (a = b)) = true ↔ a ≠ b
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ {a b : Bool}, ¬a = !b ↔ a = b
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ {a b : Bool}, ¬(!a) = b ↔ a = b
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (b : Bool), (!b) ≠ b
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (b : Bool), b ≠ !b
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a b : Bool), a = b ∨ a = !b
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ {b : Bool}, (!b) = true ↔ ¬b = true
[PROOFSTEP]
simp
[GOAL]
a : Bool
⊢ (!decide (a = false)) = true → a = true
[PROOFSTEP]
cases a
[GOAL]
case false
⊢ (!decide (false = false)) = true → false = true
[PROOFSTEP]
decide
[GOAL]
case true
⊢ (!decide (true = false)) = true → true = true
[PROOFSTEP]
decide
[GOAL]
a : Bool
⊢ (!decide (a = true)) = true → a = false
[PROOFSTEP]
cases a
[GOAL]
case false
⊢ (!decide (false = true)) = true → false = false
[PROOFSTEP]
decide
[GOAL]
case true
⊢ (!decide (true = true)) = true → true = false
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (x : Bool), (x && !x) = false
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (x : Bool), (!x && x) = false
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (x : Bool), (x || !x) = true
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (x : Bool), (!x || x) = true
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a b : Bool), xor a b = xor b a
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a b c : Bool), xor (xor a b) c = xor a (xor b c)
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a b c : Bool), xor a (xor b c) = xor b (xor a c)
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a : Bool), xor (!a) a = true
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a : Bool), (xor a !a) = true
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a b : Bool), (xor (!a) !b) = xor a b
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a : Bool), xor false a = a
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a : Bool), xor a false = a
[PROOFSTEP]
decide
[GOAL]
a b c : Bool
⊢ (a && xor b c) = xor (a && b) (a && c)
[PROOFSTEP]
cases a
[GOAL]
case false
b c : Bool
⊢ (false && xor b c) = xor (false && b) (false && c)
[PROOFSTEP]
simp
[GOAL]
case true
b c : Bool
⊢ (true && xor b c) = xor (true && b) (true && c)
[PROOFSTEP]
simp
[GOAL]
a b c : Bool
⊢ (xor a b && c) = xor (a && c) (b && c)
[PROOFSTEP]
cases a
[GOAL]
case false
b c : Bool
⊢ (xor false b && c) = xor (false && c) (b && c)
[PROOFSTEP]
cases b
[GOAL]
case true
b c : Bool
⊢ (xor true b && c) = xor (true && c) (b && c)
[PROOFSTEP]
cases b
[GOAL]
case false.false
c : Bool
⊢ (xor false false && c) = xor (false && c) (false && c)
[PROOFSTEP]
cases c
[GOAL]
case false.true
c : Bool
⊢ (xor false true && c) = xor (false && c) (true && c)
[PROOFSTEP]
cases c
[GOAL]
case true.false
c : Bool
⊢ (xor true false && c) = xor (true && c) (false && c)
[PROOFSTEP]
cases c
[GOAL]
case true.true
c : Bool
⊢ (xor true true && c) = xor (true && c) (true && c)
[PROOFSTEP]
cases c
[GOAL]
case false.false.false
⊢ (xor false false && false) = xor (false && false) (false && false)
[PROOFSTEP]
simp
[GOAL]
case false.false.true
⊢ (xor false false && true) = xor (false && true) (false && true)
[PROOFSTEP]
simp
[GOAL]
case false.true.false
⊢ (xor false true && false) = xor (false && false) (true && false)
[PROOFSTEP]
simp
[GOAL]
case false.true.true
⊢ (xor false true && true) = xor (false && true) (true && true)
[PROOFSTEP]
simp
[GOAL]
case true.false.false
⊢ (xor true false && false) = xor (true && false) (false && false)
[PROOFSTEP]
simp
[GOAL]
case true.false.true
⊢ (xor true false && true) = xor (true && true) (false && true)
[PROOFSTEP]
simp
[GOAL]
case true.true.false
⊢ (xor true true && false) = xor (true && false) (true && false)
[PROOFSTEP]
simp
[GOAL]
case true.true.true
⊢ (xor true true && true) = xor (true && true) (true && true)
[PROOFSTEP]
simp
[GOAL]
⊢ ∀ {x y : Bool}, xor x y = true ↔ x ≠ y
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a b : Bool), (!(a && b)) = (!a || !b)
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a b : Bool), (!(a || b)) = (!a && !b)
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ {a b : Bool}, (!a) = !b → a = b
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a : Bool), a ≤ a
[PROOFSTEP]
unfold LE.le
[GOAL]
⊢ ∀ (a : Bool), { le := fun a b => a = false ∨ b = true }.1 a a
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a b c : Bool), a ≤ b → b ≤ c → a ≤ c
[PROOFSTEP]
unfold LE.le
[GOAL]
⊢ ∀ (a b c : Bool),
    { le := fun a b => a = false ∨ b = true }.1 a b →
      { le := fun a b => a = false ∨ b = true }.1 b c → { le := fun a b => a = false ∨ b = true }.1 a c
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a b : Bool), a ≤ b → b ≤ a → a = b
[PROOFSTEP]
unfold LE.le Preorder.toLE
[GOAL]
⊢ ∀ (a b : Bool),
    (Preorder.mk (_ : ∀ (a : Bool), { le := fun a b => a = false ∨ b = true }.1 a a)
              (_ :
                ∀ (a b c : Bool),
                  { le := fun a b => a = false ∨ b = true }.1 a b →
                    { le := fun a b => a = false ∨ b = true }.1 b c →
                      { le := fun a b => a = false ∨ b = true }.1 a c)).1.1
        a b →
      (Preorder.mk (_ : ∀ (a : Bool), { le := fun a b => a = false ∨ b = true }.1 a a)
                (_ :
                  ∀ (a b c : Bool),
                    { le := fun a b => a = false ∨ b = true }.1 a b →
                      { le := fun a b => a = false ∨ b = true }.1 b c →
                        { le := fun a b => a = false ∨ b = true }.1 a c)).1.1
          b a →
        a = b
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (a b : Bool), a ≤ b ∨ b ≤ a
[PROOFSTEP]
unfold LE.le Preorder.toLE PartialOrder.toPreorder
[GOAL]
⊢ ∀ (a b : Bool),
    (PartialOrder.mk
                (_ :
                  ∀ (a b : Bool),
                    (Preorder.mk (_ : ∀ (a : Bool), { le := fun a b => a = false ∨ b = true }.1 a a)
                              (_ :
                                ∀ (a b c : Bool),
                                  { le := fun a b => a = false ∨ b = true }.1 a b →
                                    { le := fun a b => a = false ∨ b = true }.1 b c →
                                      { le := fun a b => a = false ∨ b = true }.1 a c)).1.1
                        a b →
                      (Preorder.mk (_ : ∀ (a : Bool), { le := fun a b => a = false ∨ b = true }.1 a a)
                                (_ :
                                  ∀ (a b c : Bool),
                                    { le := fun a b => a = false ∨ b = true }.1 a b →
                                      { le := fun a b => a = false ∨ b = true }.1 b c →
                                        { le := fun a b => a = false ∨ b = true }.1 a c)).1.1
                          b a →
                        a = b)).1.1.1
        a b ∨
      (PartialOrder.mk
                (_ :
                  ∀ (a b : Bool),
                    (Preorder.mk (_ : ∀ (a : Bool), { le := fun a b => a = false ∨ b = true }.1 a a)
                              (_ :
                                ∀ (a b c : Bool),
                                  { le := fun a b => a = false ∨ b = true }.1 a b →
                                    { le := fun a b => a = false ∨ b = true }.1 b c →
                                      { le := fun a b => a = false ∨ b = true }.1 a c)).1.1
                        a b →
                      (Preorder.mk (_ : ∀ (a : Bool), { le := fun a b => a = false ∨ b = true }.1 a a)
                                (_ :
                                  ∀ (a b c : Bool),
                                    { le := fun a b => a = false ∨ b = true }.1 a b →
                                      { le := fun a b => a = false ∨ b = true }.1 b c →
                                        { le := fun a b => a = false ∨ b = true }.1 a c)).1.1
                          b a →
                        a = b)).1.1.1
        b a
[PROOFSTEP]
decide
[GOAL]
⊢ DecidableRel fun x x_1 => x ≤ x_1
[PROOFSTEP]
unfold LE.le Preorder.toLE PartialOrder.toPreorder
[GOAL]
⊢ DecidableRel fun x x_1 =>
    (PartialOrder.mk
              (_ :
                ∀ (a b : Bool),
                  (Preorder.mk (_ : ∀ (a : Bool), { le := fun a b => a = false ∨ b = true }.1 a a)
                            (_ :
                              ∀ (a b c : Bool),
                                { le := fun a b => a = false ∨ b = true }.1 a b →
                                  { le := fun a b => a = false ∨ b = true }.1 b c →
                                    { le := fun a b => a = false ∨ b = true }.1 a c)).1.1
                      a b →
                    (Preorder.mk (_ : ∀ (a : Bool), { le := fun a b => a = false ∨ b = true }.1 a a)
                              (_ :
                                ∀ (a b c : Bool),
                                  { le := fun a b => a = false ∨ b = true }.1 a b →
                                    { le := fun a b => a = false ∨ b = true }.1 b c →
                                      { le := fun a b => a = false ∨ b = true }.1 a c)).1.1
                        b a →
                      a = b)).1.1.1
      x x_1
[PROOFSTEP]
exact inferInstance
[GOAL]
a b : Bool
⊢ min a b = if a ≤ b then a else b
[PROOFSTEP]
cases a
[GOAL]
case false
b : Bool
⊢ min false b = if false ≤ b then false else b
[PROOFSTEP]
cases b
[GOAL]
case true
b : Bool
⊢ min true b = if true ≤ b then true else b
[PROOFSTEP]
cases b
[GOAL]
case false.false
⊢ min false false = if false ≤ false then false else false
[PROOFSTEP]
decide
[GOAL]
case false.true
⊢ min false true = if false ≤ true then false else true
[PROOFSTEP]
decide
[GOAL]
case true.false
⊢ min true false = if true ≤ false then true else false
[PROOFSTEP]
decide
[GOAL]
case true.true
⊢ min true true = if true ≤ true then true else true
[PROOFSTEP]
decide
[GOAL]
a b : Bool
⊢ max a b = if a ≤ b then b else a
[PROOFSTEP]
cases a
[GOAL]
case false
b : Bool
⊢ max false b = if false ≤ b then b else false
[PROOFSTEP]
cases b
[GOAL]
case true
b : Bool
⊢ max true b = if true ≤ b then b else true
[PROOFSTEP]
cases b
[GOAL]
case false.false
⊢ max false false = if false ≤ false then false else false
[PROOFSTEP]
decide
[GOAL]
case false.true
⊢ max false true = if false ≤ true then true else false
[PROOFSTEP]
decide
[GOAL]
case true.false
⊢ max true false = if true ≤ false then false else true
[PROOFSTEP]
decide
[GOAL]
case true.true
⊢ max true true = if true ≤ true then true else true
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ {x y : Bool}, x < y ↔ x = false ∧ y = true
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ {x y : Bool}, x ≤ y ↔ x = true → y = true
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (x y : Bool), (x && y) ≤ x
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (x y : Bool), (x && y) ≤ y
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ {x y z : Bool}, x ≤ y → x ≤ z → x ≤ (y && z)
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (x y : Bool), x ≤ (x || y)
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ (x y : Bool), y ≤ (x || y)
[PROOFSTEP]
decide
[GOAL]
⊢ ∀ {x y z : Bool}, x ≤ z → y ≤ z → (x || y) ≤ z
[PROOFSTEP]
decide
[GOAL]
n m : ℕ
h : n ≤ m
⊢ ofNat n ≤ ofNat m
[PROOFSTEP]
simp only [ofNat, ne_eq, _root_.decide_not]
[GOAL]
n m : ℕ
h : n ≤ m
⊢ (!decide (n = 0)) ≤ !decide (m = 0)
[PROOFSTEP]
cases Nat.decEq n 0 with
| isTrue hn => rw [decide_eq_true hn]; exact false_le
| isFalse hn =>
  cases Nat.decEq m 0 with
  | isFalse hm => rw [decide_eq_false hm]; exact le_true
  | isTrue hm => subst hm; have h := le_antisymm h (Nat.zero_le n); contradiction
[GOAL]
n m : ℕ
h : n ≤ m
x✝ : Decidable (n = 0)
⊢ (!decide (n = 0)) ≤ !decide (m = 0)
[PROOFSTEP]
cases Nat.decEq n 0 with
| isTrue hn => rw [decide_eq_true hn]; exact false_le
| isFalse hn =>
  cases Nat.decEq m 0 with
  | isFalse hm => rw [decide_eq_false hm]; exact le_true
  | isTrue hm => subst hm; have h := le_antisymm h (Nat.zero_le n); contradiction
[GOAL]
case isTrue
n m : ℕ
h : n ≤ m
hn : n = 0
⊢ (!decide (n = 0)) ≤ !decide (m = 0)
[PROOFSTEP]

| isTrue hn => rw [decide_eq_true hn]; exact false_le
[GOAL]
case isTrue
n m : ℕ
h : n ≤ m
hn : n = 0
⊢ (!decide (n = 0)) ≤ !decide (m = 0)
[PROOFSTEP]
rw [decide_eq_true hn]
[GOAL]
case isTrue
n m : ℕ
h : n ≤ m
hn : n = 0
⊢ (!true) ≤ !decide (m = 0)
[PROOFSTEP]
exact false_le
[GOAL]
case isFalse
n m : ℕ
h : n ≤ m
hn : ¬n = 0
⊢ (!decide (n = 0)) ≤ !decide (m = 0)
[PROOFSTEP]

| isFalse hn =>
  cases Nat.decEq m 0 with
  | isFalse hm => rw [decide_eq_false hm]; exact le_true
  | isTrue hm => subst hm; have h := le_antisymm h (Nat.zero_le n); contradiction
[GOAL]
case isFalse
n m : ℕ
h : n ≤ m
hn : ¬n = 0
⊢ (!decide (n = 0)) ≤ !decide (m = 0)
[PROOFSTEP]
cases Nat.decEq m 0 with
| isFalse hm => rw [decide_eq_false hm]; exact le_true
| isTrue hm => subst hm; have h := le_antisymm h (Nat.zero_le n); contradiction
[GOAL]
case isFalse
n m : ℕ
h : n ≤ m
hn : ¬n = 0
x✝ : Decidable (m = 0)
⊢ (!decide (n = 0)) ≤ !decide (m = 0)
[PROOFSTEP]
cases Nat.decEq m 0 with
| isFalse hm => rw [decide_eq_false hm]; exact le_true
| isTrue hm => subst hm; have h := le_antisymm h (Nat.zero_le n); contradiction
[GOAL]
case isFalse.isFalse
n m : ℕ
h : n ≤ m
hn : ¬n = 0
hm : ¬m = 0
⊢ (!decide (n = 0)) ≤ !decide (m = 0)
[PROOFSTEP]

| isFalse hm => rw [decide_eq_false hm]; exact le_true
[GOAL]
case isFalse.isFalse
n m : ℕ
h : n ≤ m
hn : ¬n = 0
hm : ¬m = 0
⊢ (!decide (n = 0)) ≤ !decide (m = 0)
[PROOFSTEP]
rw [decide_eq_false hm]
[GOAL]
case isFalse.isFalse
n m : ℕ
h : n ≤ m
hn : ¬n = 0
hm : ¬m = 0
⊢ (!decide (n = 0)) ≤ !false
[PROOFSTEP]
exact le_true
[GOAL]
case isFalse.isTrue
n m : ℕ
h : n ≤ m
hn : ¬n = 0
hm : m = 0
⊢ (!decide (n = 0)) ≤ !decide (m = 0)
[PROOFSTEP]

| isTrue hm => subst hm; have h := le_antisymm h (Nat.zero_le n); contradiction
[GOAL]
case isFalse.isTrue
n m : ℕ
h : n ≤ m
hn : ¬n = 0
hm : m = 0
⊢ (!decide (n = 0)) ≤ !decide (m = 0)
[PROOFSTEP]
subst hm
[GOAL]
case isFalse.isTrue
n : ℕ
hn : ¬n = 0
h : n ≤ 0
⊢ (!decide (n = 0)) ≤ !decide (0 = 0)
[PROOFSTEP]
have h := le_antisymm h (Nat.zero_le n)
[GOAL]
case isFalse.isTrue
n : ℕ
hn : ¬n = 0
h✝ : n ≤ 0
h : n = 0
⊢ (!decide (n = 0)) ≤ !decide (0 = 0)
[PROOFSTEP]
contradiction
[GOAL]
b₀ b₁ : Bool
h : b₀ ≤ b₁
⊢ toNat b₀ ≤ toNat b₁
[PROOFSTEP]
cases h with
| inl h => subst h; exact Nat.zero_le _
| inr h => subst h; cases b₀ <;> simp
[GOAL]
b₀ b₁ : Bool
h : b₀ ≤ b₁
⊢ toNat b₀ ≤ toNat b₁
[PROOFSTEP]
cases h with
| inl h => subst h; exact Nat.zero_le _
| inr h => subst h; cases b₀ <;> simp
[GOAL]
case inl
b₀ b₁ : Bool
h : b₀ = false
⊢ toNat b₀ ≤ toNat b₁
[PROOFSTEP]

| inl h => subst h; exact Nat.zero_le _
[GOAL]
case inl
b₀ b₁ : Bool
h : b₀ = false
⊢ toNat b₀ ≤ toNat b₁
[PROOFSTEP]
subst h
[GOAL]
case inl
b₁ : Bool
⊢ toNat false ≤ toNat b₁
[PROOFSTEP]
exact Nat.zero_le _
[GOAL]
case inr
b₀ b₁ : Bool
h : b₁ = true
⊢ toNat b₀ ≤ toNat b₁
[PROOFSTEP]

| inr h => subst h; cases b₀ <;> simp
[GOAL]
case inr
b₀ b₁ : Bool
h : b₁ = true
⊢ toNat b₀ ≤ toNat b₁
[PROOFSTEP]
subst h
[GOAL]
case inr
b₀ : Bool
⊢ toNat b₀ ≤ toNat true
[PROOFSTEP]
cases b₀
[GOAL]
case inr.false
⊢ toNat false ≤ toNat true
[PROOFSTEP]
simp
[GOAL]
case inr.true
⊢ toNat true ≤ toNat true
[PROOFSTEP]
simp
[GOAL]
b : Bool
⊢ ofNat (toNat b) = b
[PROOFSTEP]
cases b
[GOAL]
case false
⊢ ofNat (toNat false) = false
[PROOFSTEP]
rfl
[GOAL]
case true
⊢ ofNat (toNat true) = true
[PROOFSTEP]
rfl
[GOAL]
α : Sort u_1
f : Bool → α
H : f false ≠ f true
x y : Bool
hxy : f x = f y
⊢ x = y
[PROOFSTEP]
cases x
[GOAL]
case false
α : Sort u_1
f : Bool → α
H : f false ≠ f true
y : Bool
hxy : f false = f y
⊢ false = y
[PROOFSTEP]
cases y
[GOAL]
case true
α : Sort u_1
f : Bool → α
H : f false ≠ f true
y : Bool
hxy : f true = f y
⊢ true = y
[PROOFSTEP]
cases y
[GOAL]
case false.false
α : Sort u_1
f : Bool → α
H : f false ≠ f true
hxy : f false = f false
⊢ false = false
case false.true
α : Sort u_1
f : Bool → α
H : f false ≠ f true
hxy : f false = f true
⊢ false = true
case true.false
α : Sort u_1
f : Bool → α
H : f false ≠ f true
hxy : f true = f false
⊢ true = false
case true.true α : Sort u_1 f : Bool → α H : f false ≠ f true hxy : f true = f true ⊢ true = true
[PROOFSTEP]
exacts [rfl, (H hxy).elim, (H hxy.symm).elim, rfl]
[GOAL]
f : Bool → Bool
x : Bool
⊢ f (f (f x)) = f x
[PROOFSTEP]
cases x
[GOAL]
case false
f : Bool → Bool
⊢ f (f (f false)) = f false
[PROOFSTEP]
cases h₁ : f true
[GOAL]
case true
f : Bool → Bool
⊢ f (f (f true)) = f true
[PROOFSTEP]
cases h₁ : f true
[GOAL]
case false.false
f : Bool → Bool
h₁ : f true = false
⊢ f (f (f false)) = f false
[PROOFSTEP]
cases h₂ : f false
[GOAL]
case false.true
f : Bool → Bool
h₁ : f true = true
⊢ f (f (f false)) = f false
[PROOFSTEP]
cases h₂ : f false
[GOAL]
case true.false
f : Bool → Bool
h₁ : f true = false
⊢ f (f false) = false
[PROOFSTEP]
cases h₂ : f false
[GOAL]
case true.true
f : Bool → Bool
h₁ : f true = true
⊢ f (f true) = true
[PROOFSTEP]
cases h₂ : f false
[GOAL]
case false.false.false
f : Bool → Bool
h₁ : f true = false
h₂ : f false = false
⊢ f (f false) = false
[PROOFSTEP]
simp only [h₁, h₂]
[GOAL]
case false.false.true
f : Bool → Bool
h₁ : f true = false
h₂ : f false = true
⊢ f (f true) = true
[PROOFSTEP]
simp only [h₁, h₂]
[GOAL]
case false.true.false
f : Bool → Bool
h₁ : f true = true
h₂ : f false = false
⊢ f (f false) = false
[PROOFSTEP]
simp only [h₁, h₂]
[GOAL]
case false.true.true
f : Bool → Bool
h₁ : f true = true
h₂ : f false = true
⊢ f (f true) = true
[PROOFSTEP]
simp only [h₁, h₂]
[GOAL]
case true.false.false
f : Bool → Bool
h₁ : f true = false
h₂ : f false = false
⊢ f false = false
[PROOFSTEP]
simp only [h₁, h₂]
[GOAL]
case true.false.true
f : Bool → Bool
h₁ : f true = false
h₂ : f false = true
⊢ f true = false
[PROOFSTEP]
simp only [h₁, h₂]
[GOAL]
case true.true.false
f : Bool → Bool
h₁ : f true = true
h₂ : f false = false
⊢ f (f true) = true
[PROOFSTEP]
simp only [h₁, h₂]
[GOAL]
case true.true.true
f : Bool → Bool
h₁ : f true = true
h₂ : f false = true
⊢ f (f true) = true
[PROOFSTEP]
simp only [h₁, h₂]


[GOAL]
R : Type u_1
M✝ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M✝
inst✝⁸ : Module R M✝
I : Ideal R
S : Type u_3
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra S R
inst✝⁵ : Module S M✝
inst✝⁴ : IsScalarTower S R M✝
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
⊢ IsScalarTower S R[X] (PolynomialModule R M)
[PROOFSTEP]
haveI : IsScalarTower R R[X] (PolynomialModule R M) := modulePolynomialOfEndo.isScalarTower _
[GOAL]
R : Type u_1
M✝ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M✝
inst✝⁸ : Module R M✝
I : Ideal R
S : Type u_3
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra S R
inst✝⁵ : Module S M✝
inst✝⁴ : IsScalarTower S R M✝
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
this : IsScalarTower R R[X] (PolynomialModule R M)
⊢ IsScalarTower S R[X] (PolynomialModule R M)
[PROOFSTEP]
constructor
[GOAL]
case smul_assoc
R : Type u_1
M✝ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M✝
inst✝⁸ : Module R M✝
I : Ideal R
S : Type u_3
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra S R
inst✝⁵ : Module S M✝
inst✝⁴ : IsScalarTower S R M✝
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
this : IsScalarTower R R[X] (PolynomialModule R M)
⊢ ∀ (x : S) (y : R[X]) (z : PolynomialModule R M), (x • y) • z = x • y • z
[PROOFSTEP]
intro x y z
[GOAL]
case smul_assoc
R : Type u_1
M✝ : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M✝
inst✝⁸ : Module R M✝
I : Ideal R
S : Type u_3
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra S R
inst✝⁵ : Module S M✝
inst✝⁴ : IsScalarTower S R M✝
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
this : IsScalarTower R R[X] (PolynomialModule R M)
x : S
y : R[X]
z : PolynomialModule R M
⊢ (x • y) • z = x • y • z
[PROOFSTEP]
rw [← @IsScalarTower.algebraMap_smul S R, ← @IsScalarTower.algebraMap_smul S R, smul_assoc]
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
r : R
j : ℕ
m : M
⊢ ↑(monomial i) r • ↑(single R j) m = ↑(single R (i + j)) (r • m)
[PROOFSTEP]
simp only [LinearMap.mul_apply, Polynomial.aeval_monomial, LinearMap.pow_apply, Module.algebraMap_end_apply,
  modulePolynomialOfEndo_smul_def]
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
r : R
j : ℕ
m : M
⊢ r • (↑(Finsupp.lmapDomain M R Nat.succ))^[i] (↑(single R j) m) = ↑(single R (i + j)) (r • m)
[PROOFSTEP]
induction i generalizing r j m with
| zero =>
  rw [Nat.zero_eq, Function.iterate_zero, zero_add]
  exact Finsupp.smul_single r j m
| succ n hn =>
  rw [Function.iterate_succ, Function.comp_apply, Nat.succ_eq_add_one, add_assoc, ← hn]
  congr 2
  rw [← Nat.succ_eq_one_add]
  exact Finsupp.mapDomain_single
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
r : R
j : ℕ
m : M
⊢ r • (↑(Finsupp.lmapDomain M R Nat.succ))^[i] (↑(single R j) m) = ↑(single R (i + j)) (r • m)
[PROOFSTEP]
induction i generalizing r j m with
| zero =>
  rw [Nat.zero_eq, Function.iterate_zero, zero_add]
  exact Finsupp.smul_single r j m
| succ n hn =>
  rw [Function.iterate_succ, Function.comp_apply, Nat.succ_eq_add_one, add_assoc, ← hn]
  congr 2
  rw [← Nat.succ_eq_one_add]
  exact Finsupp.mapDomain_single
[GOAL]
case zero
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
r : R
j : ℕ
m : M
⊢ r • (↑(Finsupp.lmapDomain M R Nat.succ))^[Nat.zero] (↑(single R j) m) = ↑(single R (Nat.zero + j)) (r • m)
[PROOFSTEP]

| zero =>
  rw [Nat.zero_eq, Function.iterate_zero, zero_add]
  exact Finsupp.smul_single r j m
[GOAL]
case zero
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
r : R
j : ℕ
m : M
⊢ r • (↑(Finsupp.lmapDomain M R Nat.succ))^[Nat.zero] (↑(single R j) m) = ↑(single R (Nat.zero + j)) (r • m)
[PROOFSTEP]
rw [Nat.zero_eq, Function.iterate_zero, zero_add]
[GOAL]
case zero
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
r : R
j : ℕ
m : M
⊢ r • id (↑(single R j) m) = ↑(single R j) (r • m)
[PROOFSTEP]
exact Finsupp.smul_single r j m
[GOAL]
case succ
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
n : ℕ
hn :
  ∀ (r : R) (j : ℕ) (m : M),
    r • (↑(Finsupp.lmapDomain M R Nat.succ))^[n] (↑(single R j) m) = ↑(single R (n + j)) (r • m)
r : R
j : ℕ
m : M
⊢ r • (↑(Finsupp.lmapDomain M R Nat.succ))^[Nat.succ n] (↑(single R j) m) = ↑(single R (Nat.succ n + j)) (r • m)
[PROOFSTEP]

| succ n hn =>
  rw [Function.iterate_succ, Function.comp_apply, Nat.succ_eq_add_one, add_assoc, ← hn]
  congr 2
  rw [← Nat.succ_eq_one_add]
  exact Finsupp.mapDomain_single
[GOAL]
case succ
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
n : ℕ
hn :
  ∀ (r : R) (j : ℕ) (m : M),
    r • (↑(Finsupp.lmapDomain M R Nat.succ))^[n] (↑(single R j) m) = ↑(single R (n + j)) (r • m)
r : R
j : ℕ
m : M
⊢ r • (↑(Finsupp.lmapDomain M R Nat.succ))^[Nat.succ n] (↑(single R j) m) = ↑(single R (Nat.succ n + j)) (r • m)
[PROOFSTEP]
rw [Function.iterate_succ, Function.comp_apply, Nat.succ_eq_add_one, add_assoc, ← hn]
[GOAL]
case succ
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
n : ℕ
hn :
  ∀ (r : R) (j : ℕ) (m : M),
    r • (↑(Finsupp.lmapDomain M R Nat.succ))^[n] (↑(single R j) m) = ↑(single R (n + j)) (r • m)
r : R
j : ℕ
m : M
⊢ r • (↑(Finsupp.lmapDomain M R Nat.succ))^[n] (↑(Finsupp.lmapDomain M R Nat.succ) (↑(single R j) m)) =
    r • (↑(Finsupp.lmapDomain M R Nat.succ))^[n] (↑(single R (1 + j)) m)
[PROOFSTEP]
congr 2
[GOAL]
case succ.e_a.e_a
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
n : ℕ
hn :
  ∀ (r : R) (j : ℕ) (m : M),
    r • (↑(Finsupp.lmapDomain M R Nat.succ))^[n] (↑(single R j) m) = ↑(single R (n + j)) (r • m)
r : R
j : ℕ
m : M
⊢ ↑(Finsupp.lmapDomain M R Nat.succ) (↑(single R j) m) = ↑(single R (1 + j)) m
[PROOFSTEP]
rw [← Nat.succ_eq_one_add]
[GOAL]
case succ.e_a.e_a
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
n : ℕ
hn :
  ∀ (r : R) (j : ℕ) (m : M),
    r • (↑(Finsupp.lmapDomain M R Nat.succ))^[n] (↑(single R j) m) = ↑(single R (n + j)) (r • m)
r : R
j : ℕ
m : M
⊢ ↑(Finsupp.lmapDomain M R Nat.succ) (↑(single R j) m) = ↑(single R (Nat.succ j)) m
[PROOFSTEP]
exact Finsupp.mapDomain_single
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
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
[PROOFSTEP]
induction' g using PolynomialModule.induction_linear with p q hp hq
[GOAL]
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_3
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
[PROOFSTEP]
simp only [smul_zero, zero_apply, ite_self]
[GOAL]
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_3
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
[PROOFSTEP]
simp only [smul_add, add_apply, hp, hq]
[GOAL]
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_3
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
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
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 neg
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
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
[PROOFSTEP]
exacts [rfl, zero_add 0]
[GOAL]
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_3
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
[PROOFSTEP]
rw [monomial_smul_single, single_apply, single_apply, smul_ite, smul_zero, ← ite_and]
[GOAL]
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_3
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
[PROOFSTEP]
congr
[GOAL]
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_3
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)
[PROOFSTEP]
rw [eq_iff_iff]
[GOAL]
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_3
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
[PROOFSTEP]
constructor
[GOAL]
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_3
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
[PROOFSTEP]
rintro rfl
[GOAL]
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_3
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
[PROOFSTEP]
simp
[GOAL]
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_3
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
[PROOFSTEP]
rintro ⟨e, rfl⟩
[GOAL]
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_3
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
[PROOFSTEP]
rw [add_comm, tsub_add_cancel_of_le e]
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
f : R[X]
m : M
n : ℕ
⊢ ↑(f • ↑(single R i) m) n = if i ≤ n then coeff f (n - i) • m else 0
[PROOFSTEP]
induction' f using Polynomial.induction_on' with p q hp hq
[GOAL]
case h_add
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
m : M
n : ℕ
p q : R[X]
hp : ↑(p • ↑(single R i) m) n = if i ≤ n then coeff p (n - i) • m else 0
hq : ↑(q • ↑(single R i) m) n = if i ≤ n then coeff q (n - i) • m else 0
⊢ ↑((p + q) • ↑(single R i) m) n = if i ≤ n then coeff (p + q) (n - i) • m else 0
[PROOFSTEP]
rw [add_smul, Finsupp.add_apply, hp, hq, coeff_add, add_smul]
[GOAL]
case h_add
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
m : M
n : ℕ
p q : R[X]
hp : ↑(p • ↑(single R i) m) n = if i ≤ n then coeff p (n - i) • m else 0
hq : ↑(q • ↑(single R i) m) n = if i ≤ n then coeff q (n - i) • m else 0
⊢ ((if i ≤ n then coeff p (n - i) • m else 0) + if i ≤ n then coeff q (n - i) • m else 0) =
    if i ≤ n then coeff p (n - i) • m + coeff q (n - i) • m else 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
m : M
n : ℕ
p q : R[X]
hp : ↑(p • ↑(single R i) m) n = if i ≤ n then coeff p (n - i) • m else 0
hq : ↑(q • ↑(single R i) m) n = if i ≤ n then coeff q (n - i) • m else 0
h✝ : i ≤ n
⊢ coeff p (n - i) • m + coeff q (n - i) • m = coeff p (n - i) • m + coeff q (n - i) • m
case neg
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
m : M
n : ℕ
p q : R[X]
hp : ↑(p • ↑(single R i) m) n = if i ≤ n then coeff p (n - i) • m else 0
hq : ↑(q • ↑(single R i) m) n = if i ≤ n then coeff q (n - i) • m else 0
h✝ : ¬i ≤ n
⊢ 0 + 0 = 0
[PROOFSTEP]
exacts [rfl, zero_add 0]
[GOAL]
case h_monomial
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
m : M
n n✝ : ℕ
a✝ : R
⊢ ↑(↑(monomial n✝) a✝ • ↑(single R i) m) n = if i ≤ n then coeff (↑(monomial n✝) a✝) (n - i) • m else 0
[PROOFSTEP]
rw [monomial_smul_single, single_apply, coeff_monomial, ite_smul, zero_smul]
[GOAL]
case h_monomial
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
m : M
n n✝ : ℕ
a✝ : R
⊢ (if n✝ + i = n then a✝ • m else 0) = if i ≤ n then if n✝ = n - i then a✝ • m else 0 else 0
[PROOFSTEP]
by_cases h : i ≤ n
[GOAL]
case pos
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
m : M
n n✝ : ℕ
a✝ : R
h : i ≤ n
⊢ (if n✝ + i = n then a✝ • m else 0) = if i ≤ n then if n✝ = n - i then a✝ • m else 0 else 0
[PROOFSTEP]
simp_rw [eq_tsub_iff_add_eq_of_le h, if_pos h]
[GOAL]
case neg
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
m : M
n n✝ : ℕ
a✝ : R
h : ¬i ≤ n
⊢ (if n✝ + i = n then a✝ • m else 0) = if i ≤ n then if n✝ = n - i then a✝ • m else 0 else 0
[PROOFSTEP]
rw [if_neg h, ite_eq_right_iff]
[GOAL]
case neg
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
m : M
n n✝ : ℕ
a✝ : R
h : ¬i ≤ n
⊢ n✝ + i = n → a✝ • m = 0
[PROOFSTEP]
intro e
[GOAL]
case neg
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
m : M
n n✝ : ℕ
a✝ : R
h : ¬i ≤ n
e : n✝ + i = n
⊢ a✝ • m = 0
[PROOFSTEP]
exfalso
[GOAL]
case neg.h
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
i : ℕ
m : M
n n✝ : ℕ
a✝ : R
h : ¬i ≤ n
e : n✝ + i = n
⊢ False
[PROOFSTEP]
linarith
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
f : R[X]
g : PolynomialModule R M
n : ℕ
⊢ ↑(f • g) n = ∑ x in Finset.Nat.antidiagonal n, coeff f x.fst • ↑g x.snd
[PROOFSTEP]
induction' f using Polynomial.induction_on' with p q hp hq f_n f_a
[GOAL]
case h_add
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
g : PolynomialModule R M
n : ℕ
p q : R[X]
hp : ↑(p • g) n = ∑ x in Finset.Nat.antidiagonal n, coeff p x.fst • ↑g x.snd
hq : ↑(q • g) n = ∑ x in Finset.Nat.antidiagonal n, coeff q x.fst • ↑g x.snd
⊢ ↑((p + q) • g) n = ∑ x in Finset.Nat.antidiagonal n, coeff (p + q) x.fst • ↑g x.snd
[PROOFSTEP]
rw [add_smul, Finsupp.add_apply, hp, hq, ← Finset.sum_add_distrib]
[GOAL]
case h_add
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
g : PolynomialModule R M
n : ℕ
p q : R[X]
hp : ↑(p • g) n = ∑ x in Finset.Nat.antidiagonal n, coeff p x.fst • ↑g x.snd
hq : ↑(q • g) n = ∑ x in Finset.Nat.antidiagonal n, coeff q x.fst • ↑g x.snd
⊢ ∑ x in Finset.Nat.antidiagonal n, (coeff p x.fst • ↑g x.snd + coeff q x.fst • ↑g x.snd) =
    ∑ x in Finset.Nat.antidiagonal n, coeff (p + q) x.fst • ↑g x.snd
[PROOFSTEP]
congr
[GOAL]
case h_add.e_f
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
g : PolynomialModule R M
n : ℕ
p q : R[X]
hp : ↑(p • g) n = ∑ x in Finset.Nat.antidiagonal n, coeff p x.fst • ↑g x.snd
hq : ↑(q • g) n = ∑ x in Finset.Nat.antidiagonal n, coeff q x.fst • ↑g x.snd
⊢ (fun x => coeff p x.fst • ↑g x.snd + coeff q x.fst • ↑g x.snd) = fun x => coeff (p + q) x.fst • ↑g x.snd
[PROOFSTEP]
ext
[GOAL]
case h_add.e_f.h
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
g : PolynomialModule R M
n : ℕ
p q : R[X]
hp : ↑(p • g) n = ∑ x in Finset.Nat.antidiagonal n, coeff p x.fst • ↑g x.snd
hq : ↑(q • g) n = ∑ x in Finset.Nat.antidiagonal n, coeff q x.fst • ↑g x.snd
x✝ : ℕ × ℕ
⊢ coeff p x✝.fst • ↑g x✝.snd + coeff q x✝.fst • ↑g x✝.snd = coeff (p + q) x✝.fst • ↑g x✝.snd
[PROOFSTEP]
rw [coeff_add, add_smul]
[GOAL]
case h_monomial
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
⊢ ↑(↑(monomial f_n) f_a • g) n = ∑ x in Finset.Nat.antidiagonal n, coeff (↑(monomial f_n) f_a) x.fst • ↑g x.snd
[PROOFSTEP]
rw [Finset.Nat.sum_antidiagonal_eq_sum_range_succ fun i j => (monomial f_n f_a).coeff i • g j, monomial_smul_apply]
[GOAL]
case h_monomial
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
⊢ (if f_n ≤ n then f_a • ↑g (n - f_n) else 0) =
    ∑ k in Finset.range (Nat.succ n), coeff (↑(monomial f_n) f_a) k • ↑g (n - k)
[PROOFSTEP]
simp_rw [Polynomial.coeff_monomial, ← Finset.mem_range_succ_iff]
[GOAL]
case h_monomial
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
⊢ (if f_n ∈ Finset.range (Nat.succ n) then f_a • ↑g (n - f_n) else 0) =
    ∑ x in Finset.range (Nat.succ n), (if f_n = x then f_a else 0) • ↑g (n - x)
[PROOFSTEP]
rw [← Finset.sum_ite_eq (Finset.range (Nat.succ n)) f_n (fun x => f_a • g (n - x))]
[GOAL]
case h_monomial
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
⊢ (∑ x in Finset.range (Nat.succ n), if f_n = x then f_a • ↑g (n - x) else 0) =
    ∑ x in Finset.range (Nat.succ n), (if f_n = x then f_a else 0) • ↑g (n - x)
[PROOFSTEP]
congr
[GOAL]
case h_monomial.e_f
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
⊢ (fun x => if f_n = x then f_a • ↑g (n - x) else 0) = fun x => (if f_n = x then f_a else 0) • ↑g (n - x)
[PROOFSTEP]
ext x
[GOAL]
case h_monomial.e_f.h
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
x : ℕ
⊢ (if f_n = x then f_a • ↑g (n - x) else 0) = (if f_n = x then f_a else 0) • ↑g (n - x)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
x : ℕ
h✝ : f_n = x
⊢ f_a • ↑g (n - x) = f_a • ↑g (n - x)
case neg
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
g : PolynomialModule R M
n f_n : ℕ
f_a : R
x : ℕ
h✝ : ¬f_n = x
⊢ 0 = 0 • ↑g (n - x)
[PROOFSTEP]
exacts [rfl, (zero_smul R _).symm]
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
x : PolynomialModule R R
⊢ AddHom.toFun
      { toFun := src✝.toFun,
        map_add' :=
          (_ :
            ∀ (x y : AddMonoidAlgebra R ℕ),
              Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
      (r • x) =
    ↑(RingHom.id R[X]) r •
      AddHom.toFun
        { toFun := src✝.toFun,
          map_add' :=
            (_ :
              ∀ (x y : AddMonoidAlgebra R ℕ),
                Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
        x
[PROOFSTEP]
dsimp
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
x : PolynomialModule R R
⊢ ↑(↑(toFinsuppIso R)).symm (r • x) = r * ↑(↑(toFinsuppIso R)).symm x
[PROOFSTEP]
rw [← RingEquiv.coe_toEquiv_symm, RingEquiv.coe_toEquiv]
[GOAL]
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
x : PolynomialModule R R
⊢ ↑(RingEquiv.symm (toFinsuppIso R)) (r • x) = r * ↑(RingEquiv.symm (toFinsuppIso R)) x
[PROOFSTEP]
induction' x using induction_linear with _ _ hp hq n a
[GOAL]
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_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
⊢ ↑(RingEquiv.symm (toFinsuppIso R)) (r • 0) = r * ↑(RingEquiv.symm (toFinsuppIso R)) 0
[PROOFSTEP]
rw [smul_zero, map_zero, mul_zero]
[GOAL]
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_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
f✝ g✝ : PolynomialModule R R
hp : ↑(RingEquiv.symm (toFinsuppIso R)) (r • f✝) = r * ↑(RingEquiv.symm (toFinsuppIso R)) f✝
hq : ↑(RingEquiv.symm (toFinsuppIso R)) (r • g✝) = r * ↑(RingEquiv.symm (toFinsuppIso R)) g✝
⊢ ↑(RingEquiv.symm (toFinsuppIso R)) (r • (f✝ + g✝)) = r * ↑(RingEquiv.symm (toFinsuppIso R)) (f✝ + g✝)
[PROOFSTEP]
rw [smul_add, map_add, map_add, mul_add, hp, hq]
[GOAL]
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_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
⊢ ↑(RingEquiv.symm (toFinsuppIso R)) (r • ↑(single R n) a) = r * ↑(RingEquiv.symm (toFinsuppIso R)) (↑(single R n) a)
[PROOFSTEP]
ext i
[GOAL]
case hsingle.a
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
⊢ coeff (↑(RingEquiv.symm (toFinsuppIso R)) (r • ↑(single R n) a)) i =
    coeff (r * ↑(RingEquiv.symm (toFinsuppIso R)) (↑(single R n) a)) i
[PROOFSTEP]
simp only [coeff_ofFinsupp, smul_single_apply, toFinsuppIso_symm_apply, coeff_ofFinsupp, single_apply, ge_iff_le,
  smul_eq_mul, Polynomial.coeff_mul, mul_ite, mul_zero]
[GOAL]
case hsingle.a
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
⊢ (if n ≤ i then coeff r (i - n) * a else 0) =
    ∑ x in Finset.Nat.antidiagonal i, if n = x.snd then coeff r x.fst * a else 0
[PROOFSTEP]
split_ifs with hn
[GOAL]
case pos
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
⊢ coeff r (i - n) * a = ∑ x in Finset.Nat.antidiagonal i, if n = x.snd then coeff r x.fst * a else 0
[PROOFSTEP]
rw [Finset.sum_eq_single (i - n, n)]
[GOAL]
case pos
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
⊢ coeff r (i - n) * a = if n = (i - n, n).snd then coeff r (i - n, n).fst * a else 0
case pos.h₀
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
⊢ ∀ (b : ℕ × ℕ), b ∈ Finset.Nat.antidiagonal i → b ≠ (i - n, n) → (if n = b.snd then coeff r b.fst * a else 0) = 0
case pos.h₁
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
⊢ ¬(i - n, n) ∈ Finset.Nat.antidiagonal i → (if n = (i - n, n).snd then coeff r (i - n, n).fst * a else 0) = 0
[PROOFSTEP]
simp only [ite_true]
[GOAL]
case pos.h₀
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
⊢ ∀ (b : ℕ × ℕ), b ∈ Finset.Nat.antidiagonal i → b ≠ (i - n, n) → (if n = b.snd then coeff r b.fst * a else 0) = 0
[PROOFSTEP]
rintro ⟨p, q⟩ hpq1 hpq2
[GOAL]
case pos.h₀.mk
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
p q : ℕ
hpq1 : (p, q) ∈ Finset.Nat.antidiagonal i
hpq2 : (p, q) ≠ (i - n, n)
⊢ (if n = (p, q).snd then coeff r (p, q).fst * a else 0) = 0
[PROOFSTEP]
rw [Finset.Nat.mem_antidiagonal] at hpq1
[GOAL]
case pos.h₀.mk
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
p q : ℕ
hpq1 : (p, q).fst + (p, q).snd = i
hpq2 : (p, q) ≠ (i - n, n)
⊢ (if n = (p, q).snd then coeff r (p, q).fst * a else 0) = 0
[PROOFSTEP]
split_ifs with H
[GOAL]
case pos
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
p q : ℕ
hpq1 : (p, q).fst + (p, q).snd = i
hpq2 : (p, q) ≠ (i - n, n)
H : n = (p, q).snd
⊢ coeff r (p, q).fst * a = 0
[PROOFSTEP]
dsimp at H
[GOAL]
case pos
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
p q : ℕ
hpq1 : (p, q).fst + (p, q).snd = i
hpq2 : (p, q) ≠ (i - n, n)
H : n = q
⊢ coeff r (p, q).fst * a = 0
[PROOFSTEP]
exfalso
[GOAL]
case pos.h
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
p q : ℕ
hpq1 : (p, q).fst + (p, q).snd = i
hpq2 : (p, q) ≠ (i - n, n)
H : n = q
⊢ False
[PROOFSTEP]
apply hpq2
[GOAL]
case pos.h
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
p q : ℕ
hpq1 : (p, q).fst + (p, q).snd = i
hpq2 : (p, q) ≠ (i - n, n)
H : n = q
⊢ (p, q) = (i - n, n)
[PROOFSTEP]
rw [← hpq1, H]
[GOAL]
case pos.h
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
p q : ℕ
hpq1 : (p, q).fst + (p, q).snd = i
hpq2 : (p, q) ≠ (i - n, n)
H : n = q
⊢ (p, q) = ((p, q).fst + (p, q).snd - q, q)
[PROOFSTEP]
simp only [add_le_iff_nonpos_left, nonpos_iff_eq_zero, add_tsub_cancel_right]
[GOAL]
case neg
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
p q : ℕ
hpq1 : (p, q).fst + (p, q).snd = i
hpq2 : (p, q) ≠ (i - n, n)
H : ¬n = (p, q).snd
⊢ 0 = 0
[PROOFSTEP]
rfl
[GOAL]
case pos.h₁
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
⊢ ¬(i - n, n) ∈ Finset.Nat.antidiagonal i → (if n = (i - n, n).snd then coeff r (i - n, n).fst * a else 0) = 0
[PROOFSTEP]
intro H
[GOAL]
case pos.h₁
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
H : ¬(i - n, n) ∈ Finset.Nat.antidiagonal i
⊢ (if n = (i - n, n).snd then coeff r (i - n, n).fst * a else 0) = 0
[PROOFSTEP]
exfalso
[GOAL]
case pos.h₁.h
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
H : ¬(i - n, n) ∈ Finset.Nat.antidiagonal i
⊢ False
[PROOFSTEP]
apply H
[GOAL]
case pos.h₁.h
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : n ≤ i
H : ¬(i - n, n) ∈ Finset.Nat.antidiagonal i
⊢ (i - n, n) ∈ Finset.Nat.antidiagonal i
[PROOFSTEP]
rw [Finset.Nat.mem_antidiagonal, tsub_add_cancel_of_le hn]
[GOAL]
case neg
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : ¬n ≤ i
⊢ 0 = ∑ x in Finset.Nat.antidiagonal i, if n = x.snd then coeff r x.fst * a else 0
[PROOFSTEP]
symm
[GOAL]
case neg
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : ¬n ≤ i
⊢ (∑ x in Finset.Nat.antidiagonal i, if n = x.snd then coeff r x.fst * a else 0) = 0
[PROOFSTEP]
rw [Finset.sum_ite_of_false, Finset.sum_const_zero]
[GOAL]
case neg.h
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : ¬n ≤ i
⊢ ∀ (x : ℕ × ℕ), x ∈ Finset.Nat.antidiagonal i → ¬n = x.snd
[PROOFSTEP]
simp_rw [Finset.Nat.mem_antidiagonal]
[GOAL]
case neg.h
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : ¬n ≤ i
⊢ ∀ (x : ℕ × ℕ), x.fst + x.snd = i → ¬n = x.snd
[PROOFSTEP]
intro x hx
[GOAL]
case neg.h
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
hn : ¬n ≤ i
x : ℕ × ℕ
hx : x.fst + x.snd = i
⊢ ¬n = x.snd
[PROOFSTEP]
contrapose! hn
[GOAL]
case neg.h
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
x : ℕ × ℕ
hx : x.fst + x.snd = i
hn : n = x.snd
⊢ n ≤ i
[PROOFSTEP]
rw [add_comm, ← hn] at hx
[GOAL]
case neg.h
R : Type u_1
M : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
I : Ideal R
S : Type u_3
inst✝³ : CommSemiring S
inst✝² : Algebra S R
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
src✝ : AddMonoidAlgebra R ℕ ≃+* R[X] := RingEquiv.symm (toFinsuppIso R)
r : R[X]
n : ℕ
a : R
i : ℕ
x : ℕ × ℕ
hx : n + x.fst = i
hn : n = x.snd
⊢ n ≤ i
[PROOFSTEP]
exact Nat.le.intro hx
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
p : R[X]
q : PolynomialModule R M
⊢ ↑(map R' f) (p • q) = Polynomial.map (algebraMap R R') p • ↑(map R' f) q
[PROOFSTEP]
apply induction_linear q
[GOAL]
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_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
p : R[X]
q : PolynomialModule R M
⊢ ↑(map R' f) (p • 0) = Polynomial.map (algebraMap R R') p • ↑(map R' f) 0
[PROOFSTEP]
rw [smul_zero, map_zero, smul_zero]
[GOAL]
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_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
p : R[X]
q : PolynomialModule R M
⊢ ∀ (f_1 g : PolynomialModule R M),
    ↑(map R' f) (p • f_1) = Polynomial.map (algebraMap R R') p • ↑(map R' f) f_1 →
      ↑(map R' f) (p • g) = Polynomial.map (algebraMap R R') p • ↑(map R' f) g →
        ↑(map R' f) (p • (f_1 + g)) = Polynomial.map (algebraMap R R') p • ↑(map R' f) (f_1 + g)
[PROOFSTEP]
intro f g e₁ e₂
[GOAL]
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_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f✝ : M →ₗ[R] M'
p : R[X]
q f g : PolynomialModule R M
e₁ : ↑(map R' f✝) (p • f) = Polynomial.map (algebraMap R R') p • ↑(map R' f✝) f
e₂ : ↑(map R' f✝) (p • g) = Polynomial.map (algebraMap R R') p • ↑(map R' f✝) g
⊢ ↑(map R' f✝) (p • (f + g)) = Polynomial.map (algebraMap R R') p • ↑(map R' f✝) (f + g)
[PROOFSTEP]
rw [smul_add, map_add, e₁, e₂, map_add, smul_add]
[GOAL]
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_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
p : R[X]
q : PolynomialModule R M
⊢ ∀ (a : ℕ) (b : M),
    ↑(map R' f) (p • ↑(single R a) b) = Polynomial.map (algebraMap R R') p • ↑(map R' f) (↑(single R a) b)
[PROOFSTEP]
intro i m
[GOAL]
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_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
p : R[X]
q : PolynomialModule R M
i : ℕ
m : M
⊢ ↑(map R' f) (p • ↑(single R i) m) = Polynomial.map (algebraMap R R') p • ↑(map R' f) (↑(single R i) m)
[PROOFSTEP]
induction' p using Polynomial.induction_on' with _ _ e₁ e₂
[GOAL]
case hsingle.h_add
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
q : PolynomialModule R M
i : ℕ
m : M
p✝ q✝ : R[X]
e₁ : ↑(map R' f) (p✝ • ↑(single R i) m) = Polynomial.map (algebraMap R R') p✝ • ↑(map R' f) (↑(single R i) m)
e₂ : ↑(map R' f) (q✝ • ↑(single R i) m) = Polynomial.map (algebraMap R R') q✝ • ↑(map R' f) (↑(single R i) m)
⊢ ↑(map R' f) ((p✝ + q✝) • ↑(single R i) m) = Polynomial.map (algebraMap R R') (p✝ + q✝) • ↑(map R' f) (↑(single R i) m)
[PROOFSTEP]
rw [add_smul, map_add, e₁, e₂, Polynomial.map_add, add_smul]
[GOAL]
case hsingle.h_monomial
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
q : PolynomialModule R M
i : ℕ
m : M
n✝ : ℕ
a✝ : R
⊢ ↑(map R' f) (↑(monomial n✝) a✝ • ↑(single R i) m) =
    Polynomial.map (algebraMap R R') (↑(monomial n✝) a✝) • ↑(map R' f) (↑(single R i) m)
[PROOFSTEP]
rw [monomial_smul_single, map_single, Polynomial.map_monomial, map_single, monomial_smul_single, f.map_smul,
  algebraMap_smul]
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
r s : R
m : PolynomialModule R M
⊢ AddHom.toFun
      { toFun := fun p => Finsupp.sum p fun i m => r ^ i • m,
        map_add' :=
          (_ :
            ∀ (x y : PolynomialModule R M),
              (Finsupp.sum (x + y) fun i m => r ^ i • m) =
                (Finsupp.sum x fun i m => r ^ i • m) + Finsupp.sum y fun i m => r ^ i • m) }
      (s • m) =
    ↑(RingHom.id R) s •
      AddHom.toFun
        { toFun := fun p => Finsupp.sum p fun i m => r ^ i • m,
          map_add' :=
            (_ :
              ∀ (x y : PolynomialModule R M),
                (Finsupp.sum (x + y) fun i m => r ^ i • m) =
                  (Finsupp.sum x fun i m => r ^ i • m) + Finsupp.sum y fun i m => r ^ i • m) }
        m
[PROOFSTEP]
refine' (Finsupp.sum_smul_index' _).trans _
[GOAL]
case refine'_1
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
r s : R
m : PolynomialModule R M
⊢ ∀ (i : ℕ), r ^ i • 0 = 0
[PROOFSTEP]
exact fun i => smul_zero _
[GOAL]
case refine'_2
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
r s : R
m : PolynomialModule R M
⊢ (Finsupp.sum m fun i c => r ^ i • s • c) =
    ↑(RingHom.id R) s •
      AddHom.toFun
        { toFun := fun p => Finsupp.sum p fun i m => r ^ i • m,
          map_add' :=
            (_ :
              ∀ (x y : PolynomialModule R M),
                (Finsupp.sum (x + y) fun i m => r ^ i • m) =
                  (Finsupp.sum x fun i m => r ^ i • m) + Finsupp.sum y fun i m => r ^ i • m) }
        m
[PROOFSTEP]
simp_rw [RingHom.id_apply, Finsupp.smul_sum]
[GOAL]
case refine'_2
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
r s : R
m : PolynomialModule R M
⊢ (Finsupp.sum m fun i c => r ^ i • s • c) = Finsupp.sum m fun a b => s • r ^ a • b
[PROOFSTEP]
congr
[GOAL]
case refine'_2.e_g
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
r s : R
m : PolynomialModule R M
⊢ (fun i c => r ^ i • s • c) = fun a b => s • r ^ a • b
[PROOFSTEP]
ext i c
[GOAL]
case refine'_2.e_g.h.h
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
r s : R
m : PolynomialModule R M
i : ℕ
c : M
⊢ r ^ i • s • c = s • r ^ i • c
[PROOFSTEP]
rw [smul_comm]
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
p : R[X]
q : PolynomialModule R M
r : R
⊢ ↑(eval r) (p • q) = Polynomial.eval r p • ↑(eval r) q
[PROOFSTEP]
apply induction_linear q
[GOAL]
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_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
p : R[X]
q : PolynomialModule R M
r : R
⊢ ↑(eval r) (p • 0) = Polynomial.eval r p • ↑(eval r) 0
[PROOFSTEP]
rw [smul_zero, map_zero, smul_zero]
[GOAL]
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_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
p : R[X]
q : PolynomialModule R M
r : R
⊢ ∀ (f g : PolynomialModule R M),
    ↑(eval r) (p • f) = Polynomial.eval r p • ↑(eval r) f →
      ↑(eval r) (p • g) = Polynomial.eval r p • ↑(eval r) g →
        ↑(eval r) (p • (f + g)) = Polynomial.eval r p • ↑(eval r) (f + g)
[PROOFSTEP]
intro f g e₁ e₂
[GOAL]
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_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
p : R[X]
q : PolynomialModule R M
r : R
f g : PolynomialModule R M
e₁ : ↑(eval r) (p • f) = Polynomial.eval r p • ↑(eval r) f
e₂ : ↑(eval r) (p • g) = Polynomial.eval r p • ↑(eval r) g
⊢ ↑(eval r) (p • (f + g)) = Polynomial.eval r p • ↑(eval r) (f + g)
[PROOFSTEP]
rw [smul_add, map_add, e₁, e₂, map_add, smul_add]
[GOAL]
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_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
p : R[X]
q : PolynomialModule R M
r : R
⊢ ∀ (a : ℕ) (b : M), ↑(eval r) (p • ↑(single R a) b) = Polynomial.eval r p • ↑(eval r) (↑(single R a) b)
[PROOFSTEP]
intro i m
[GOAL]
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_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
p : R[X]
q : PolynomialModule R M
r : R
i : ℕ
m : M
⊢ ↑(eval r) (p • ↑(single R i) m) = Polynomial.eval r p • ↑(eval r) (↑(single R i) m)
[PROOFSTEP]
induction' p using Polynomial.induction_on' with _ _ e₁ e₂
[GOAL]
case hsingle.h_add
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
q : PolynomialModule R M
r : R
i : ℕ
m : M
p✝ q✝ : R[X]
e₁ : ↑(eval r) (p✝ • ↑(single R i) m) = Polynomial.eval r p✝ • ↑(eval r) (↑(single R i) m)
e₂ : ↑(eval r) (q✝ • ↑(single R i) m) = Polynomial.eval r q✝ • ↑(eval r) (↑(single R i) m)
⊢ ↑(eval r) ((p✝ + q✝) • ↑(single R i) m) = Polynomial.eval r (p✝ + q✝) • ↑(eval r) (↑(single R i) m)
[PROOFSTEP]
rw [add_smul, map_add, Polynomial.eval_add, e₁, e₂, add_smul]
[GOAL]
case hsingle.h_monomial
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
q : PolynomialModule R M
r : R
i : ℕ
m : M
n✝ : ℕ
a✝ : R
⊢ ↑(eval r) (↑(monomial n✝) a✝ • ↑(single R i) m) = Polynomial.eval r (↑(monomial n✝) a✝) • ↑(eval r) (↑(single R i) m)
[PROOFSTEP]
rw [monomial_smul_single, eval_single, Polynomial.eval_monomial, eval_single, smul_comm, ← smul_smul, pow_add, mul_smul]
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
q : PolynomialModule R M
r : R
⊢ ↑(eval (↑(algebraMap R R') r)) (↑(map R' f) q) = ↑f (↑(eval r) q)
[PROOFSTEP]
apply induction_linear q
[GOAL]
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_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
q : PolynomialModule R M
r : R
⊢ ↑(eval (↑(algebraMap R R') r)) (↑(map R' f) 0) = ↑f (↑(eval r) 0)
[PROOFSTEP]
simp_rw [map_zero]
[GOAL]
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_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
q : PolynomialModule R M
r : R
⊢ ∀ (f_1 g : PolynomialModule R M),
    ↑(eval (↑(algebraMap R R') r)) (↑(map R' f) f_1) = ↑f (↑(eval r) f_1) →
      ↑(eval (↑(algebraMap R R') r)) (↑(map R' f) g) = ↑f (↑(eval r) g) →
        ↑(eval (↑(algebraMap R R') r)) (↑(map R' f) (f_1 + g)) = ↑f (↑(eval r) (f_1 + g))
[PROOFSTEP]
intro f g e₁ e₂
[GOAL]
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_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f✝ : M →ₗ[R] M'
q : PolynomialModule R M
r : R
f g : PolynomialModule R M
e₁ : ↑(eval (↑(algebraMap R R') r)) (↑(map R' f✝) f) = ↑f✝ (↑(eval r) f)
e₂ : ↑(eval (↑(algebraMap R R') r)) (↑(map R' f✝) g) = ↑f✝ (↑(eval r) g)
⊢ ↑(eval (↑(algebraMap R R') r)) (↑(map R' f✝) (f + g)) = ↑f✝ (↑(eval r) (f + g))
[PROOFSTEP]
simp_rw [map_add, e₁, e₂]
[GOAL]
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_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
q : PolynomialModule R M
r : R
⊢ ∀ (a : ℕ) (b : M), ↑(eval (↑(algebraMap R R') r)) (↑(map R' f) (↑(single R a) b)) = ↑f (↑(eval r) (↑(single R a) b))
[PROOFSTEP]
intro i m
[GOAL]
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_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
q : PolynomialModule R M
r : R
i : ℕ
m : M
⊢ ↑(eval (↑(algebraMap R R') r)) (↑(map R' f) (↑(single R i) m)) = ↑f (↑(eval r) (↑(single R i) m))
[PROOFSTEP]
rw [map_single, eval_single, eval_single, f.map_smul, ← map_pow, algebraMap_smul]
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
p : R[X]
i : ℕ
m : M
⊢ ↑(comp p) (↑(single R i) m) = p ^ i • ↑(single R 0) m
[PROOFSTEP]
rw [comp_apply]
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
p : R[X]
i : ℕ
m : M
⊢ ↑(eval p) (↑(map R[X] (lsingle R 0)) (↑(single R i) m)) = p ^ i • ↑(single R 0) m
[PROOFSTEP]
erw [map_single, eval_single]
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
p : R[X]
i : ℕ
m : M
⊢ p ^ i • ↑(lsingle R 0) m = p ^ i • ↑(single R 0) m
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
p : R[X]
q : PolynomialModule R M
r : R
⊢ ↑(eval r) (↑(comp p) q) = ↑(eval (Polynomial.eval r p)) q
[PROOFSTEP]
rw [← LinearMap.comp_apply]
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
p : R[X]
q : PolynomialModule R M
r : R
⊢ ↑(LinearMap.comp (eval r) (comp p)) q = ↑(eval (Polynomial.eval r p)) q
[PROOFSTEP]
apply induction_linear q
[GOAL]
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_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
p : R[X]
q : PolynomialModule R M
r : R
⊢ ↑(LinearMap.comp (eval r) (comp p)) 0 = ↑(eval (Polynomial.eval r p)) 0
[PROOFSTEP]
simp_rw [map_zero]
[GOAL]
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_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
p : R[X]
q : PolynomialModule R M
r : R
⊢ ∀ (f g : PolynomialModule R M),
    ↑(LinearMap.comp (eval r) (comp p)) f = ↑(eval (Polynomial.eval r p)) f →
      ↑(LinearMap.comp (eval r) (comp p)) g = ↑(eval (Polynomial.eval r p)) g →
        ↑(LinearMap.comp (eval r) (comp p)) (f + g) = ↑(eval (Polynomial.eval r p)) (f + g)
[PROOFSTEP]
intro _ _ e₁ e₂
[GOAL]
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_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
p : R[X]
q : PolynomialModule R M
r : R
f✝ g✝ : PolynomialModule R M
e₁ : ↑(LinearMap.comp (eval r) (comp p)) f✝ = ↑(eval (Polynomial.eval r p)) f✝
e₂ : ↑(LinearMap.comp (eval r) (comp p)) g✝ = ↑(eval (Polynomial.eval r p)) g✝
⊢ ↑(LinearMap.comp (eval r) (comp p)) (f✝ + g✝) = ↑(eval (Polynomial.eval r p)) (f✝ + g✝)
[PROOFSTEP]
simp_rw [map_add, e₁, e₂]
[GOAL]
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_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
p : R[X]
q : PolynomialModule R M
r : R
⊢ ∀ (a : ℕ) (b : M),
    ↑(LinearMap.comp (eval r) (comp p)) (↑(single R a) b) = ↑(eval (Polynomial.eval r p)) (↑(single R a) b)
[PROOFSTEP]
intro i m
[GOAL]
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_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
p : R[X]
q : PolynomialModule R M
r : R
i : ℕ
m : M
⊢ ↑(LinearMap.comp (eval r) (comp p)) (↑(single R i) m) = ↑(eval (Polynomial.eval r p)) (↑(single R i) m)
[PROOFSTEP]
rw [LinearMap.comp_apply, comp_single, eval_single, eval_smul, eval_single, pow_zero, one_smul, Polynomial.eval_pow]
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
p p' : R[X]
q : PolynomialModule R M
⊢ ↑(comp p) (p' • q) = Polynomial.comp p' p • ↑(comp p) q
[PROOFSTEP]
rw [comp_apply, map_smul, eval_smul, Polynomial.comp, Polynomial.eval_map, comp_apply]
[GOAL]
R : Type u_1
M : Type u_2
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
I : Ideal R
S : Type u_3
inst✝⁹ : CommSemiring S
inst✝⁸ : Algebra S R
inst✝⁷ : Module S M
inst✝⁶ : IsScalarTower S R M
R' : Type u_4
M' : Type u_5
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Algebra R R'
inst✝¹ : Module R M'
inst✝ : IsScalarTower R R' M'
p p' : R[X]
q : PolynomialModule R M
⊢ eval₂ (algebraMap R R[X]) p p' • ↑(eval p) (↑(map R[X] (lsingle R 0)) q) =
    eval₂ C p p' • ↑(eval p) (↑(map R[X] (lsingle R 0)) q)
[PROOFSTEP]
rfl