[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
⊢ ∫ (x : ℝ) in x₀..x₀ + ↑a, f x ≤ ∑ i in Finset.range a, f (x₀ + ↑i)
[PROOFSTEP]
have hint : ∀ k : ℕ, k < a → IntervalIntegrable f volume (x₀ + k) (x₀ + (k + 1 : ℕ)) :=
  by
  intro k hk
  refine' (hf.mono _).intervalIntegrable
  rw [uIcc_of_le]
  · apply Icc_subset_Icc
    · simp only [le_add_iff_nonneg_right, Nat.cast_nonneg]
    · simp only [add_le_add_iff_left, Nat.cast_le, Nat.succ_le_of_lt hk]
  · simp only [add_le_add_iff_left, Nat.cast_le, Nat.le_succ]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
⊢ ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
[PROOFSTEP]
intro k hk
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k < a
⊢ IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
[PROOFSTEP]
refine' (hf.mono _).intervalIntegrable
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k < a
⊢ uIcc (x₀ + ↑k) (x₀ + ↑(k + 1)) ⊆ Icc x₀ (x₀ + ↑a)
[PROOFSTEP]
rw [uIcc_of_le]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k < a
⊢ Icc (x₀ + ↑k) (x₀ + ↑(k + 1)) ⊆ Icc x₀ (x₀ + ↑a)
[PROOFSTEP]
apply Icc_subset_Icc
[GOAL]
case h₁
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k < a
⊢ x₀ ≤ x₀ + ↑k
[PROOFSTEP]
simp only [le_add_iff_nonneg_right, Nat.cast_nonneg]
[GOAL]
case h₂
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k < a
⊢ x₀ + ↑(k + 1) ≤ x₀ + ↑a
[PROOFSTEP]
simp only [add_le_add_iff_left, Nat.cast_le, Nat.succ_le_of_lt hk]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k < a
⊢ x₀ + ↑k ≤ x₀ + ↑(k + 1)
[PROOFSTEP]
simp only [add_le_add_iff_left, Nat.cast_le, Nat.le_succ]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
⊢ ∫ (x : ℝ) in x₀..x₀ + ↑a, f x ≤ ∑ i in Finset.range a, f (x₀ + ↑i)
[PROOFSTEP]
calc
  ∫ x in x₀..x₀ + a, f x = ∑ i in Finset.range a, ∫ x in x₀ + i..x₀ + (i + 1 : ℕ), f x :=
    by
    convert (intervalIntegral.sum_integral_adjacent_intervals hint).symm
    simp only [Nat.cast_zero, add_zero]
  _ ≤ ∑ i in Finset.range a, ∫ _ in x₀ + i..x₀ + (i + 1 : ℕ), f (x₀ + i) :=
    by
    apply Finset.sum_le_sum fun i hi => ?_
    have ia : i < a := Finset.mem_range.1 hi
    refine' intervalIntegral.integral_mono_on (by simp) (hint _ ia) (by simp) fun x hx => _
    apply hf _ _ hx.1
    ·
      simp only [ia.le, mem_Icc, le_add_iff_nonneg_right, Nat.cast_nonneg, add_le_add_iff_left, Nat.cast_le,
        and_self_iff]
    · refine' mem_Icc.2 ⟨le_trans (by simp) hx.1, le_trans hx.2 _⟩
      simp only [add_le_add_iff_left, Nat.cast_le, Nat.succ_le_of_lt ia]
  _ = ∑ i in Finset.range a, f (x₀ + i) := by simp
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
⊢ ∫ (x : ℝ) in x₀..x₀ + ↑a, f x = ∑ i in Finset.range a, ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f x
[PROOFSTEP]
convert (intervalIntegral.sum_integral_adjacent_intervals hint).symm
[GOAL]
case h.e'_2.h.e'_5
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
⊢ x₀ = x₀ + ↑0
[PROOFSTEP]
simp only [Nat.cast_zero, add_zero]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
⊢ ∑ i in Finset.range a, ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f x ≤
    ∑ i in Finset.range a, ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f (x₀ + ↑i)
[PROOFSTEP]
apply Finset.sum_le_sum fun i hi => ?_
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
i : ℕ
hi : i ∈ Finset.range a
⊢ ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f x ≤ ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f (x₀ + ↑i)
[PROOFSTEP]
have ia : i < a := Finset.mem_range.1 hi
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
i : ℕ
hi : i ∈ Finset.range a
ia : i < a
⊢ ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f x ≤ ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f (x₀ + ↑i)
[PROOFSTEP]
refine' intervalIntegral.integral_mono_on (by simp) (hint _ ia) (by simp) fun x hx => _
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
i : ℕ
hi : i ∈ Finset.range a
ia : i < a
⊢ x₀ + ↑i ≤ x₀ + ↑(i + 1)
[PROOFSTEP]
simp
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
i : ℕ
hi : i ∈ Finset.range a
ia : i < a
⊢ IntervalIntegrable (fun x => f (x₀ + ↑i)) volume (x₀ + ↑i) (x₀ + ↑(i + 1))
[PROOFSTEP]
simp
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
i : ℕ
hi : i ∈ Finset.range a
ia : i < a
x : ℝ
hx : x ∈ Icc (x₀ + ↑i) (x₀ + ↑(i + 1))
⊢ f x ≤ f (x₀ + ↑i)
[PROOFSTEP]
apply hf _ _ hx.1
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
i : ℕ
hi : i ∈ Finset.range a
ia : i < a
x : ℝ
hx : x ∈ Icc (x₀ + ↑i) (x₀ + ↑(i + 1))
⊢ x₀ + ↑i ∈ Icc x₀ (x₀ + ↑a)
[PROOFSTEP]
simp only [ia.le, mem_Icc, le_add_iff_nonneg_right, Nat.cast_nonneg, add_le_add_iff_left, Nat.cast_le, and_self_iff]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
i : ℕ
hi : i ∈ Finset.range a
ia : i < a
x : ℝ
hx : x ∈ Icc (x₀ + ↑i) (x₀ + ↑(i + 1))
⊢ x ∈ Icc x₀ (x₀ + ↑a)
[PROOFSTEP]
refine' mem_Icc.2 ⟨le_trans (by simp) hx.1, le_trans hx.2 _⟩
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
i : ℕ
hi : i ∈ Finset.range a
ia : i < a
x : ℝ
hx : x ∈ Icc (x₀ + ↑i) (x₀ + ↑(i + 1))
⊢ x₀ ≤ x₀ + ↑i
[PROOFSTEP]
simp
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
i : ℕ
hi : i ∈ Finset.range a
ia : i < a
x : ℝ
hx : x ∈ Icc (x₀ + ↑i) (x₀ + ↑(i + 1))
⊢ x₀ + ↑(i + 1) ≤ x₀ + ↑a
[PROOFSTEP]
simp only [add_le_add_iff_left, Nat.cast_le, Nat.succ_le_of_lt ia]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
⊢ ∑ i in Finset.range a, ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f (x₀ + ↑i) = ∑ i in Finset.range a, f (x₀ + ↑i)
[PROOFSTEP]
simp
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∫ (x : ℝ) in ↑a..↑b, f x ≤ ∑ x in Finset.Ico a b, f ↑x
[PROOFSTEP]
rw [(Nat.sub_add_cancel hab).symm, Nat.cast_add]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∫ (x : ℝ) in ↑a..↑(b - a) + ↑a, f x ≤ ∑ x in Finset.Ico a (b - a + a), f ↑x
[PROOFSTEP]
conv =>
  congr
  congr
  ·skip
  ·skip
  rw [add_comm]
  ·skip
  ·skip
  congr
  congr
  rw [← zero_add a]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ∫ (x : ℝ) in ↑a..↑(b - a) + ↑a, f x ≤ ∑ x in Finset.Ico a (b - a + a), f ↑x
[PROOFSTEP]
  congr
  congr
  ·skip
  ·skip
  rw [add_comm]
  ·skip
  ·skip
  congr
  congr
  rw [← zero_add a]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ∫ (x : ℝ) in ↑a..↑(b - a) + ↑a, f x ≤ ∑ x in Finset.Ico a (b - a + a), f ↑x
[PROOFSTEP]
  congr
  congr
  ·skip
  ·skip
  rw [add_comm]
  ·skip
  ·skip
  congr
  congr
  rw [← zero_add a]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ∫ (x : ℝ) in ↑a..↑(b - a) + ↑a, f x ≤ ∑ x in Finset.Ico a (b - a + a), f ↑x
[PROOFSTEP]
congr
[GOAL]
case a
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ∫ (x : ℝ) in ↑a..↑(b - a) + ↑a, f x
case a x₀ : ℝ a b : ℕ f : ℝ → ℝ hab : a ≤ b hf : AntitoneOn f (Icc ↑a ↑b) | ∑ x in Finset.Ico a (b - a + a), f ↑x
[PROOFSTEP]
congr
[GOAL]
case a.f
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| fun x => f x
case a.a
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ↑a
case a.b
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ↑(b - a) + ↑a
case a.μ
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| volume
case a x₀ : ℝ a b : ℕ f : ℝ → ℝ hab : a ≤ b hf : AntitoneOn f (Icc ↑a ↑b) | ∑ x in Finset.Ico a (b - a + a), f ↑x
[PROOFSTEP]
·skip
[GOAL]
case a.f
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| fun x => f x
[PROOFSTEP]
skip
[GOAL]
case a.f
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| fun x => f x
[PROOFSTEP]
skip
[GOAL]
case a.f
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| fun x => f x
[PROOFSTEP]
skip
[GOAL]
case a.a
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ↑a
case a.b
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ↑(b - a) + ↑a
case a.μ
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| volume
case a x₀ : ℝ a b : ℕ f : ℝ → ℝ hab : a ≤ b hf : AntitoneOn f (Icc ↑a ↑b) | ∑ x in Finset.Ico a (b - a + a), f ↑x
[PROOFSTEP]
·skip
[GOAL]
case a.a
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ↑a
[PROOFSTEP]
skip
[GOAL]
case a.a
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ↑a
[PROOFSTEP]
skip
[GOAL]
case a.a
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ↑a
[PROOFSTEP]
skip
[GOAL]
case a.b
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ↑(b - a) + ↑a
case a.μ
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| volume
case a x₀ : ℝ a b : ℕ f : ℝ → ℝ hab : a ≤ b hf : AntitoneOn f (Icc ↑a ↑b) | ∑ x in Finset.Ico a (b - a + a), f ↑x
[PROOFSTEP]
rw [add_comm]
[GOAL]
case a.b
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ↑a + ↑(b - a)
case a.μ
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| volume
case a x₀ : ℝ a b : ℕ f : ℝ → ℝ hab : a ≤ b hf : AntitoneOn f (Icc ↑a ↑b) | ∑ x in Finset.Ico a (b - a + a), f ↑x
[PROOFSTEP]
·skip
[GOAL]
case a.b
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ↑a + ↑(b - a)
[PROOFSTEP]
skip
[GOAL]
case a.b
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ↑a + ↑(b - a)
[PROOFSTEP]
skip
[GOAL]
case a.b
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ↑a + ↑(b - a)
[PROOFSTEP]
skip
[GOAL]
case a.μ
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| volume
case a x₀ : ℝ a b : ℕ f : ℝ → ℝ hab : a ≤ b hf : AntitoneOn f (Icc ↑a ↑b) | ∑ x in Finset.Ico a (b - a + a), f ↑x
[PROOFSTEP]
·skip
[GOAL]
case a.μ
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| volume
[PROOFSTEP]
skip
[GOAL]
case a.μ
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| volume
[PROOFSTEP]
skip
[GOAL]
case a.μ
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| volume
[PROOFSTEP]
skip
[GOAL]
case a
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ∑ x in Finset.Ico a (b - a + a), f ↑x
[PROOFSTEP]
congr
[GOAL]
case a.s
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| Finset.Ico a (b - a + a)
case a.f x₀ : ℝ a b : ℕ f : ℝ → ℝ hab : a ≤ b hf : AntitoneOn f (Icc ↑a ↑b) | fun x => f ↑x
[PROOFSTEP]
congr
[GOAL]
case a.s.a
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| a
case a.s.b
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| b - a + a
case a.f x₀ : ℝ a b : ℕ f : ℝ → ℝ hab : a ≤ b hf : AntitoneOn f (Icc ↑a ↑b) | fun x => f ↑x
[PROOFSTEP]
rw [← zero_add a]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x ≤ ∑ x in Finset.Ico (0 + a) (b - a + a), f ↑x
[PROOFSTEP]
rw [← Finset.sum_Ico_add, Nat.Ico_zero_eq_range]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x ≤ ∑ x in Finset.range (b - a), f ↑(a + x)
[PROOFSTEP]
conv =>
  rhs
  congr
  ·skip
  ext
  rw [Nat.cast_add]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x ≤ ∑ x in Finset.range (b - a), f ↑(a + x)
[PROOFSTEP]
  rhs
  congr
  ·skip
  ext
  rw [Nat.cast_add]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x ≤ ∑ x in Finset.range (b - a), f ↑(a + x)
[PROOFSTEP]
  rhs
  congr
  ·skip
  ext
  rw [Nat.cast_add]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x ≤ ∑ x in Finset.range (b - a), f ↑(a + x)
[PROOFSTEP]
rhs
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ∑ x in Finset.range (b - a), f ↑(a + x)
[PROOFSTEP]
congr
[GOAL]
case s
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| Finset.range (b - a)
case f x₀ : ℝ a b : ℕ f : ℝ → ℝ hab : a ≤ b hf : AntitoneOn f (Icc ↑a ↑b) | fun x => f ↑(a + x)
[PROOFSTEP]
·skip
[GOAL]
case s
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| Finset.range (b - a)
[PROOFSTEP]
skip
[GOAL]
case s
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| Finset.range (b - a)
[PROOFSTEP]
skip
[GOAL]
case s
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| Finset.range (b - a)
[PROOFSTEP]
skip
[GOAL]
case f
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| fun x => f ↑(a + x)
[PROOFSTEP]
ext
[GOAL]
case f.h
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
x✝ : ℕ
| f ↑(a + x✝)
[PROOFSTEP]
rw [Nat.cast_add]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x ≤ ∑ x in Finset.range (b - a), f (↑a + ↑x)
[PROOFSTEP]
apply AntitoneOn.integral_le_sum
[GOAL]
case hf
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ AntitoneOn (fun x => f x) (Icc (↑a) (↑a + ↑(b - a)))
[PROOFSTEP]
simp only [hf, hab, Nat.cast_sub, add_sub_cancel'_right]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
⊢ ∑ i in Finset.range a, f (x₀ + ↑(i + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + ↑a, f x
[PROOFSTEP]
have hint : ∀ k : ℕ, k < a → IntervalIntegrable f volume (x₀ + k) (x₀ + (k + 1 : ℕ)) :=
  by
  intro k hk
  refine' (hf.mono _).intervalIntegrable
  rw [uIcc_of_le]
  · apply Icc_subset_Icc
    · simp only [le_add_iff_nonneg_right, Nat.cast_nonneg]
    · simp only [add_le_add_iff_left, Nat.cast_le, Nat.succ_le_of_lt hk]
  · simp only [add_le_add_iff_left, Nat.cast_le, Nat.le_succ]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
⊢ ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
[PROOFSTEP]
intro k hk
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k < a
⊢ IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
[PROOFSTEP]
refine' (hf.mono _).intervalIntegrable
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k < a
⊢ uIcc (x₀ + ↑k) (x₀ + ↑(k + 1)) ⊆ Icc x₀ (x₀ + ↑a)
[PROOFSTEP]
rw [uIcc_of_le]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k < a
⊢ Icc (x₀ + ↑k) (x₀ + ↑(k + 1)) ⊆ Icc x₀ (x₀ + ↑a)
[PROOFSTEP]
apply Icc_subset_Icc
[GOAL]
case h₁
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k < a
⊢ x₀ ≤ x₀ + ↑k
[PROOFSTEP]
simp only [le_add_iff_nonneg_right, Nat.cast_nonneg]
[GOAL]
case h₂
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k < a
⊢ x₀ + ↑(k + 1) ≤ x₀ + ↑a
[PROOFSTEP]
simp only [add_le_add_iff_left, Nat.cast_le, Nat.succ_le_of_lt hk]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
k : ℕ
hk : k < a
⊢ x₀ + ↑k ≤ x₀ + ↑(k + 1)
[PROOFSTEP]
simp only [add_le_add_iff_left, Nat.cast_le, Nat.le_succ]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
⊢ ∑ i in Finset.range a, f (x₀ + ↑(i + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + ↑a, f x
[PROOFSTEP]
calc
  (∑ i in Finset.range a, f (x₀ + (i + 1 : ℕ))) =
      ∑ i in Finset.range a, ∫ _ in x₀ + i..x₀ + (i + 1 : ℕ), f (x₀ + (i + 1 : ℕ)) :=
    by simp
  _ ≤ ∑ i in Finset.range a, ∫ x in x₀ + i..x₀ + (i + 1 : ℕ), f x :=
    by
    apply Finset.sum_le_sum fun i hi => ?_
    have ia : i + 1 ≤ a := Finset.mem_range.1 hi
    refine' intervalIntegral.integral_mono_on (by simp) (by simp) (hint _ ia) fun x hx => _
    apply hf _ _ hx.2
    · refine' mem_Icc.2 ⟨le_trans ((le_add_iff_nonneg_right _).2 (Nat.cast_nonneg _)) hx.1, le_trans hx.2 _⟩
      simp only [Nat.cast_le, add_le_add_iff_left, ia]
    · refine' mem_Icc.2 ⟨(le_add_iff_nonneg_right _).2 (Nat.cast_nonneg _), _⟩
      simp only [add_le_add_iff_left, Nat.cast_le, ia]
  _ = ∫ x in x₀..x₀ + a, f x :=
    by
    convert intervalIntegral.sum_integral_adjacent_intervals hint
    simp only [Nat.cast_zero, add_zero]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
⊢ ∑ i in Finset.range a, f (x₀ + ↑(i + 1)) =
    ∑ i in Finset.range a, ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f (x₀ + ↑(i + 1))
[PROOFSTEP]
simp
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
⊢ ∑ i in Finset.range a, ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f (x₀ + ↑(i + 1)) ≤
    ∑ i in Finset.range a, ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f x
[PROOFSTEP]
apply Finset.sum_le_sum fun i hi => ?_
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
i : ℕ
hi : i ∈ Finset.range a
⊢ ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f (x₀ + ↑(i + 1)) ≤ ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f x
[PROOFSTEP]
have ia : i + 1 ≤ a := Finset.mem_range.1 hi
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
i : ℕ
hi : i ∈ Finset.range a
ia : i + 1 ≤ a
⊢ ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f (x₀ + ↑(i + 1)) ≤ ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f x
[PROOFSTEP]
refine' intervalIntegral.integral_mono_on (by simp) (by simp) (hint _ ia) fun x hx => _
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
i : ℕ
hi : i ∈ Finset.range a
ia : i + 1 ≤ a
⊢ x₀ + ↑i ≤ x₀ + ↑(i + 1)
[PROOFSTEP]
simp
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
i : ℕ
hi : i ∈ Finset.range a
ia : i + 1 ≤ a
⊢ IntervalIntegrable (fun x => f (x₀ + ↑(i + 1))) volume (x₀ + ↑i) (x₀ + ↑(i + 1))
[PROOFSTEP]
simp
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
i : ℕ
hi : i ∈ Finset.range a
ia : i + 1 ≤ a
x : ℝ
hx : x ∈ Icc (x₀ + ↑i) (x₀ + ↑(i + 1))
⊢ f (x₀ + ↑(i + 1)) ≤ f x
[PROOFSTEP]
apply hf _ _ hx.2
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
i : ℕ
hi : i ∈ Finset.range a
ia : i + 1 ≤ a
x : ℝ
hx : x ∈ Icc (x₀ + ↑i) (x₀ + ↑(i + 1))
⊢ x ∈ Icc x₀ (x₀ + ↑a)
[PROOFSTEP]
refine' mem_Icc.2 ⟨le_trans ((le_add_iff_nonneg_right _).2 (Nat.cast_nonneg _)) hx.1, le_trans hx.2 _⟩
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
i : ℕ
hi : i ∈ Finset.range a
ia : i + 1 ≤ a
x : ℝ
hx : x ∈ Icc (x₀ + ↑i) (x₀ + ↑(i + 1))
⊢ x₀ + ↑(i + 1) ≤ x₀ + ↑a
[PROOFSTEP]
simp only [Nat.cast_le, add_le_add_iff_left, ia]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
i : ℕ
hi : i ∈ Finset.range a
ia : i + 1 ≤ a
x : ℝ
hx : x ∈ Icc (x₀ + ↑i) (x₀ + ↑(i + 1))
⊢ x₀ + ↑(i + 1) ∈ Icc x₀ (x₀ + ↑a)
[PROOFSTEP]
refine' mem_Icc.2 ⟨(le_add_iff_nonneg_right _).2 (Nat.cast_nonneg _), _⟩
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
i : ℕ
hi : i ∈ Finset.range a
ia : i + 1 ≤ a
x : ℝ
hx : x ∈ Icc (x₀ + ↑i) (x₀ + ↑(i + 1))
⊢ x₀ + ↑(i + 1) ≤ x₀ + ↑a
[PROOFSTEP]
simp only [add_le_add_iff_left, Nat.cast_le, ia]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
⊢ ∑ i in Finset.range a, ∫ (x : ℝ) in x₀ + ↑i..x₀ + ↑(i + 1), f x = ∫ (x : ℝ) in x₀..x₀ + ↑a, f x
[PROOFSTEP]
convert intervalIntegral.sum_integral_adjacent_intervals hint
[GOAL]
case h.e'_3.h.e'_5
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : AntitoneOn f (Icc x₀ (x₀ + ↑a))
hint : ∀ (k : ℕ), k < a → IntervalIntegrable f volume (x₀ + ↑k) (x₀ + ↑(k + 1))
⊢ x₀ = x₀ + ↑0
[PROOFSTEP]
simp only [Nat.cast_zero, add_zero]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∑ i in Finset.Ico a b, f ↑(i + 1) ≤ ∫ (x : ℝ) in ↑a..↑b, f x
[PROOFSTEP]
rw [(Nat.sub_add_cancel hab).symm, Nat.cast_add]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∑ i in Finset.Ico a (b - a + a), f ↑(i + 1) ≤ ∫ (x : ℝ) in ↑a..↑(b - a) + ↑a, f x
[PROOFSTEP]
conv =>
  congr
  congr
  congr
  rw [← zero_add a]
  ·skip
  ·skip
  ·skip
  rw [add_comm]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ∑ i in Finset.Ico a (b - a + a), f ↑(i + 1) ≤ ∫ (x : ℝ) in ↑a..↑(b - a) + ↑a, f x
[PROOFSTEP]
  congr
  congr
  congr
  rw [← zero_add a]
  ·skip
  ·skip
  ·skip
  rw [add_comm]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ∑ i in Finset.Ico a (b - a + a), f ↑(i + 1) ≤ ∫ (x : ℝ) in ↑a..↑(b - a) + ↑a, f x
[PROOFSTEP]
  congr
  congr
  congr
  rw [← zero_add a]
  ·skip
  ·skip
  ·skip
  rw [add_comm]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ∑ i in Finset.Ico a (b - a + a), f ↑(i + 1) ≤ ∫ (x : ℝ) in ↑a..↑(b - a) + ↑a, f x
[PROOFSTEP]
congr
[GOAL]
case a
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ∑ i in Finset.Ico a (b - a + a), f ↑(i + 1)
case a x₀ : ℝ a b : ℕ f : ℝ → ℝ hab : a ≤ b hf : AntitoneOn f (Icc ↑a ↑b) | ∫ (x : ℝ) in ↑a..↑(b - a) + ↑a, f x
[PROOFSTEP]
congr
[GOAL]
case a.s
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| Finset.Ico a (b - a + a)
case a.f
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| fun i => f ↑(i + 1)
case a x₀ : ℝ a b : ℕ f : ℝ → ℝ hab : a ≤ b hf : AntitoneOn f (Icc ↑a ↑b) | ∫ (x : ℝ) in ↑a..↑(b - a) + ↑a, f x
[PROOFSTEP]
congr
[GOAL]
case a.s.a
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| a
case a.s.b
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| b - a + a
case a.f
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| fun i => f ↑(i + 1)
case a x₀ : ℝ a b : ℕ f : ℝ → ℝ hab : a ≤ b hf : AntitoneOn f (Icc ↑a ↑b) | ∫ (x : ℝ) in ↑a..↑(b - a) + ↑a, f x
[PROOFSTEP]
rw [← zero_add a]
[GOAL]
case a.s.a
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| 0 + a
case a.s.b
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| b - a + a
case a.f
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| fun i => f ↑(i + 1)
case a x₀ : ℝ a b : ℕ f : ℝ → ℝ hab : a ≤ b hf : AntitoneOn f (Icc ↑a ↑b) | ∫ (x : ℝ) in ↑a..↑(b - a) + ↑a, f x
[PROOFSTEP]
·skip
[GOAL]
case a.s.a
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| 0 + a
[PROOFSTEP]
skip
[GOAL]
case a.s.a
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| 0 + a
[PROOFSTEP]
skip
[GOAL]
case a.s.a
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| 0 + a
[PROOFSTEP]
skip
[GOAL]
case a.s.b
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| b - a + a
case a.f
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| fun i => f ↑(i + 1)
case a x₀ : ℝ a b : ℕ f : ℝ → ℝ hab : a ≤ b hf : AntitoneOn f (Icc ↑a ↑b) | ∫ (x : ℝ) in ↑a..↑(b - a) + ↑a, f x
[PROOFSTEP]
·skip
[GOAL]
case a.s.b
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| b - a + a
[PROOFSTEP]
skip
[GOAL]
case a.s.b
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| b - a + a
[PROOFSTEP]
skip
[GOAL]
case a.s.b
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| b - a + a
[PROOFSTEP]
skip
[GOAL]
case a.f
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| fun i => f ↑(i + 1)
case a x₀ : ℝ a b : ℕ f : ℝ → ℝ hab : a ≤ b hf : AntitoneOn f (Icc ↑a ↑b) | ∫ (x : ℝ) in ↑a..↑(b - a) + ↑a, f x
[PROOFSTEP]
·skip
[GOAL]
case a.f
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| fun i => f ↑(i + 1)
[PROOFSTEP]
skip
[GOAL]
case a.f
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| fun i => f ↑(i + 1)
[PROOFSTEP]
skip
[GOAL]
case a.f
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| fun i => f ↑(i + 1)
[PROOFSTEP]
skip
[GOAL]
case a
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ∫ (x : ℝ) in ↑a..↑(b - a) + ↑a, f x
[PROOFSTEP]
rw [add_comm]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∑ i in Finset.Ico (0 + a) (b - a + a), f ↑(i + 1) ≤ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x
[PROOFSTEP]
rw [← Finset.sum_Ico_add, Nat.Ico_zero_eq_range]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∑ x in Finset.range (b - a), f ↑(a + x + 1) ≤ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x
[PROOFSTEP]
conv =>
  lhs
  congr
  congr
  ·skip
  ext
  rw [add_assoc, Nat.cast_add]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ∑ x in Finset.range (b - a), f ↑(a + x + 1) ≤ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x
[PROOFSTEP]
  lhs
  congr
  congr
  ·skip
  ext
  rw [add_assoc, Nat.cast_add]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ∑ x in Finset.range (b - a), f ↑(a + x + 1) ≤ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x
[PROOFSTEP]
  lhs
  congr
  congr
  ·skip
  ext
  rw [add_assoc, Nat.cast_add]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ∑ x in Finset.range (b - a), f ↑(a + x + 1) ≤ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x
[PROOFSTEP]
lhs
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| ∑ x in Finset.range (b - a), f ↑(a + x + 1)
[PROOFSTEP]
congr
[GOAL]
case s
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| Finset.range (b - a)
case f x₀ : ℝ a b : ℕ f : ℝ → ℝ hab : a ≤ b hf : AntitoneOn f (Icc ↑a ↑b) | fun x => f ↑(a + x + 1)
[PROOFSTEP]
congr
[GOAL]
case s.n
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| b - a
case f x₀ : ℝ a b : ℕ f : ℝ → ℝ hab : a ≤ b hf : AntitoneOn f (Icc ↑a ↑b) | fun x => f ↑(a + x + 1)
[PROOFSTEP]
·skip
[GOAL]
case s.n
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| b - a
[PROOFSTEP]
skip
[GOAL]
case s.n
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| b - a
[PROOFSTEP]
skip
[GOAL]
case s.n
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| b - a
[PROOFSTEP]
skip
[GOAL]
case f
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
| fun x => f ↑(a + x + 1)
[PROOFSTEP]
ext
[GOAL]
case f.h
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
x✝ : ℕ
| f ↑(a + x✝ + 1)
[PROOFSTEP]
rw [add_assoc, Nat.cast_add]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∑ x in Finset.range (b - a), f (↑a + ↑(x + 1)) ≤ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x
[PROOFSTEP]
apply AntitoneOn.sum_le_integral
[GOAL]
case hf
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ AntitoneOn f (Icc (↑a) (↑a + ↑(b - a)))
[PROOFSTEP]
simp only [hf, hab, Nat.cast_sub, add_sub_cancel'_right]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : MonotoneOn f (Icc x₀ (x₀ + ↑a))
⊢ ∑ i in Finset.range a, f (x₀ + ↑i) ≤ ∫ (x : ℝ) in x₀..x₀ + ↑a, f x
[PROOFSTEP]
rw [← neg_le_neg_iff, ← Finset.sum_neg_distrib, ← intervalIntegral.integral_neg]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : MonotoneOn f (Icc x₀ (x₀ + ↑a))
⊢ ∫ (x : ℝ) in x₀..x₀ + ↑a, -f x ≤ ∑ x in Finset.range a, -f (x₀ + ↑x)
[PROOFSTEP]
exact hf.neg.integral_le_sum
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
⊢ ∑ x in Finset.Ico a b, f ↑x ≤ ∫ (x : ℝ) in ↑a..↑b, f x
[PROOFSTEP]
rw [← neg_le_neg_iff, ← Finset.sum_neg_distrib, ← intervalIntegral.integral_neg]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
⊢ ∫ (x : ℝ) in ↑a..↑b, -f x ≤ ∑ x in Finset.Ico a b, -f ↑x
[PROOFSTEP]
exact hf.neg.integral_le_sum_Ico hab
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : MonotoneOn f (Icc x₀ (x₀ + ↑a))
⊢ ∫ (x : ℝ) in x₀..x₀ + ↑a, f x ≤ ∑ i in Finset.range a, f (x₀ + ↑(i + 1))
[PROOFSTEP]
rw [← neg_le_neg_iff, ← Finset.sum_neg_distrib, ← intervalIntegral.integral_neg]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hf : MonotoneOn f (Icc x₀ (x₀ + ↑a))
⊢ ∑ x in Finset.range a, -f (x₀ + ↑(x + 1)) ≤ ∫ (x : ℝ) in x₀..x₀ + ↑a, -f x
[PROOFSTEP]
exact hf.neg.sum_le_integral
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
⊢ ∫ (x : ℝ) in ↑a..↑b, f x ≤ ∑ i in Finset.Ico a b, f ↑(i + 1)
[PROOFSTEP]
rw [← neg_le_neg_iff, ← Finset.sum_neg_distrib, ← intervalIntegral.integral_neg]
[GOAL]
x₀ : ℝ
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : MonotoneOn f (Icc ↑a ↑b)
⊢ ∑ x in Finset.Ico a b, -f ↑(x + 1) ≤ ∫ (x : ℝ) in ↑a..↑b, -f x
[PROOFSTEP]
exact hf.neg.sum_le_integral_Ico hab


[GOAL]
R : Type u_1
inst✝ : CommRing R
x✝ x : R
⊢ ↑(aeval x✝) ((fun a => ↑C a) x) = x
[PROOFSTEP]
exact eval_C
[GOAL]
R : Type u_1
inst✝ : CommRing R
x y : R
⊢ Ideal.span {↑C x, X - ↑C y} = Ideal.span {X - ↑C y} ⊔ ?m.223800 x y
[PROOFSTEP]
rw [Ideal.span_insert, sup_comm]
[GOAL]
R : Type u_1
inst✝ : CommRing R
x y : R
⊢ Ideal.map (↑(quotientSpanXSubCAlgEquiv y))
      (Ideal.map (Ideal.Quotient.mkₐ R (Ideal.span {X - ↑C y})) (Ideal.span {↑C x})) =
    Ideal.span {x}
[PROOFSTEP]
simp only [Ideal.map_span, Set.image_singleton]
[GOAL]
R : Type u_1
inst✝ : CommRing R
x y : R
⊢ Ideal.span {↑↑(quotientSpanXSubCAlgEquiv y) (↑(Ideal.Quotient.mkₐ R (Ideal.span {X - ↑C y})) (↑C x))} = Ideal.span {x}
[PROOFSTEP]
congr 2
[GOAL]
case e_s.e_a
R : Type u_1
inst✝ : CommRing R
x y : R
⊢ ↑↑(quotientSpanXSubCAlgEquiv y) (↑(Ideal.Quotient.mkₐ R (Ideal.span {X - ↑C y})) (↑C x)) = x
[PROOFSTEP]
exact eval_C
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0
[PROOFSTEP]
intro a ha
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
ha : a ∈ I
⊢ ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0
[PROOFSTEP]
rw [RingHom.comp_apply, Quotient.eq_zero_iff_mem]
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R
ha : a ∈ I
⊢ ↑C a ∈ map C I
[PROOFSTEP]
exact mem_map_of_mem _ ha
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0
[PROOFSTEP]
intro a ha
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
⊢ ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) a = 0
[PROOFSTEP]
rw [← sum_monomial_eq a]
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
⊢ ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) (sum a fun n a => ↑(monomial n) a) = 0
[PROOFSTEP]
dsimp
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
⊢ eval₂ (RingHom.comp C (Quotient.mk I)) X (sum a fun n a => ↑(monomial n) a) = 0
[PROOFSTEP]
rw [eval₂_sum]
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
⊢ (sum a fun n a => eval₂ (RingHom.comp C (Quotient.mk I)) X (↑(monomial n) a)) = 0
[PROOFSTEP]
refine' Finset.sum_eq_zero fun n _ => _
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ support a
⊢ (fun n a => eval₂ (RingHom.comp C (Quotient.mk I)) X (↑(monomial n) a)) n (coeff a n) = 0
[PROOFSTEP]
dsimp
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ support a
⊢ eval₂ (RingHom.comp C (Quotient.mk I)) X (↑(monomial n) (coeff a n)) = 0
[PROOFSTEP]
rw [eval₂_monomial (C.comp (Quotient.mk I)) X]
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ support a
⊢ ↑(RingHom.comp C (Quotient.mk I)) (coeff a n) * X ^ n = 0
[PROOFSTEP]
refine' mul_eq_zero_of_left (Polynomial.ext fun m => _) (X ^ n)
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ support a
m : ℕ
⊢ coeff (↑(RingHom.comp C (Quotient.mk I)) (coeff a n)) m = coeff 0 m
[PROOFSTEP]
erw [coeff_C]
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ support a
m : ℕ
⊢ (if m = 0 then ↑(Quotient.mk I) (coeff a n) else 0) = coeff 0 m
[PROOFSTEP]
by_cases h : m = 0
[GOAL]
case pos
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ support a
m : ℕ
h : m = 0
⊢ (if m = 0 then ↑(Quotient.mk I) (coeff a n) else 0) = coeff 0 m
[PROOFSTEP]
simpa [h] using Quotient.eq_zero_iff_mem.2 ((mem_map_C_iff.1 ha) n)
[GOAL]
case neg
R : Type u_1
inst✝ : CommRing R
I : Ideal R
a : R[X]
ha : a ∈ map C I
n : ℕ
x✝ : n ∈ support a
m : ℕ
h : ¬m = 0
⊢ (if m = 0 then ↑(Quotient.mk I) (coeff a n) else 0) = coeff 0 m
[PROOFSTEP]
simp [h]
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ Function.LeftInverse
    ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
        (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
    ↑(eval₂RingHom
        (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
          (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
        (↑(Quotient.mk (map C I)) X))
[PROOFSTEP]
intro f
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f : (R ⧸ I)[X]
⊢ ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
          (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
      (↑(eval₂RingHom
            (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
              (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
            (↑(Quotient.mk (map C I)) X))
        f) =
    f
[PROOFSTEP]
refine Polynomial.induction_on' f ?_ ?_
[GOAL]
case refine_1
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f : (R ⧸ I)[X]
⊢ ∀ (p q : (R ⧸ I)[X]),
    ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
              (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
          (↑(eval₂RingHom
                (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                  (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                (↑(Quotient.mk (map C I)) X))
            p) =
        p →
      ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
            (↑(eval₂RingHom
                  (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                    (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                  (↑(Quotient.mk (map C I)) X))
              q) =
          q →
        ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
            (↑(eval₂RingHom
                  (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                    (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                  (↑(Quotient.mk (map C I)) X))
              (p + q)) =
          p + q
[PROOFSTEP]
intro p q hp hq
[GOAL]
case refine_1
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f p q : (R ⧸ I)[X]
hp :
  ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
          (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
      (↑(eval₂RingHom
            (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
              (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
            (↑(Quotient.mk (map C I)) X))
        p) =
    p
hq :
  ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
          (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
      (↑(eval₂RingHom
            (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
              (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
            (↑(Quotient.mk (map C I)) X))
        q) =
    q
⊢ ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
          (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
      (↑(eval₂RingHom
            (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
              (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
            (↑(Quotient.mk (map C I)) X))
        (p + q)) =
    p + q
[PROOFSTEP]
simp only [coe_eval₂RingHom] at hp hq
[GOAL]
case refine_1
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f p q : (R ⧸ I)[X]
hp :
  ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
          (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
      (eval₂
        (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
          (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
        (↑(Quotient.mk (map C I)) X) p) =
    p
hq :
  ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
          (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
      (eval₂
        (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
          (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
        (↑(Quotient.mk (map C I)) X) q) =
    q
⊢ ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
          (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
      (↑(eval₂RingHom
            (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
              (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
            (↑(Quotient.mk (map C I)) X))
        (p + q)) =
    p + q
[PROOFSTEP]
simp only [coe_eval₂RingHom, hp, hq, RingHom.map_add]
[GOAL]
case refine_2
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f : (R ⧸ I)[X]
⊢ ∀ (n : ℕ) (a : R ⧸ I),
    ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
            (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
        (↑(eval₂RingHom
              (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
              (↑(Quotient.mk (map C I)) X))
          (↑(monomial n) a)) =
      ↑(monomial n) a
[PROOFSTEP]
rintro n ⟨x⟩
[GOAL]
case refine_2.mk
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f : (R ⧸ I)[X]
n : ℕ
a✝ : R ⧸ I
x : R
⊢ ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
          (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
      (↑(eval₂RingHom
            (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
              (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
            (↑(Quotient.mk (map C I)) X))
        (↑(monomial n) (Quot.mk Setoid.r x))) =
    ↑(monomial n) (Quot.mk Setoid.r x)
[PROOFSTEP]
simp only [← smul_X_eq_monomial, C_mul', Quotient.lift_mk, Submodule.Quotient.quot_mk_eq_mk, Quotient.mk_eq_mk,
  eval₂_X_pow, eval₂_smul, coe_eval₂RingHom, RingHom.map_pow, eval₂_C, RingHom.coe_comp, RingHom.map_mul, eval₂_X,
  Function.comp_apply]
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ Function.RightInverse
    ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
        (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
    ↑(eval₂RingHom
        (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
          (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
        (↑(Quotient.mk (map C I)) X))
[PROOFSTEP]
rintro ⟨f⟩
[GOAL]
case mk
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x✝ : R[X] ⧸ map C I
f : R[X]
⊢ ↑(eval₂RingHom
          (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
            (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
          (↑(Quotient.mk (map C I)) X))
      (↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
            (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
        (Quot.mk Setoid.r f)) =
    Quot.mk Setoid.r f
[PROOFSTEP]
refine Polynomial.induction_on' f ?_ ?_
[GOAL]
case mk.refine_1
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x✝ : R[X] ⧸ map C I
f : R[X]
⊢ ∀ (p q : R[X]),
    ↑(eval₂RingHom
              (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
              (↑(Quotient.mk (map C I)) X))
          (↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
            (Quot.mk Setoid.r p)) =
        Quot.mk Setoid.r p →
      ↑(eval₂RingHom
                (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                  (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                (↑(Quotient.mk (map C I)) X))
            (↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                  (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
              (Quot.mk Setoid.r q)) =
          Quot.mk Setoid.r q →
        ↑(eval₂RingHom
                (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                  (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                (↑(Quotient.mk (map C I)) X))
            (↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                  (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
              (Quot.mk Setoid.r (p + q))) =
          Quot.mk Setoid.r (p + q)
[PROOFSTEP]
intros p q hp hq
[GOAL]
case mk.refine_1
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x✝ : R[X] ⧸ map C I
f p q : R[X]
hp :
  ↑(eval₂RingHom
          (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
            (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
          (↑(Quotient.mk (map C I)) X))
      (↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
            (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
        (Quot.mk Setoid.r p)) =
    Quot.mk Setoid.r p
hq :
  ↑(eval₂RingHom
          (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
            (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
          (↑(Quotient.mk (map C I)) X))
      (↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
            (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
        (Quot.mk Setoid.r q)) =
    Quot.mk Setoid.r q
⊢ ↑(eval₂RingHom
          (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
            (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
          (↑(Quotient.mk (map C I)) X))
      (↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
            (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
        (Quot.mk Setoid.r (p + q))) =
    Quot.mk Setoid.r (p + q)
[PROOFSTEP]
simp only [Submodule.Quotient.quot_mk_eq_mk, Quotient.mk_eq_mk, map_add, Quotient.lift_mk, coe_eval₂RingHom] at hp hq ⊢
[GOAL]
case mk.refine_1
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x✝ : R[X] ⧸ map C I
f p q : R[X]
hp :
  eval₂
      (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
        (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
      (↑(Quotient.mk (map C I)) X) (eval₂ (RingHom.comp C (Quotient.mk I)) X p) =
    ↑(Quotient.mk (map C I)) p
hq :
  eval₂
      (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
        (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
      (↑(Quotient.mk (map C I)) X) (eval₂ (RingHom.comp C (Quotient.mk I)) X q) =
    ↑(Quotient.mk (map C I)) q
⊢ eval₂
        (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
          (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
        (↑(Quotient.mk (map C I)) X) (eval₂ (RingHom.comp C (Quotient.mk I)) X p) +
      eval₂
        (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
          (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
        (↑(Quotient.mk (map C I)) X) (eval₂ (RingHom.comp C (Quotient.mk I)) X q) =
    ↑(Quotient.mk (map C I)) p + ↑(Quotient.mk (map C I)) q
[PROOFSTEP]
rw [hp, hq]
[GOAL]
case mk.refine_2
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x✝ : R[X] ⧸ map C I
f : R[X]
⊢ ∀ (n : ℕ) (a : R),
    ↑(eval₂RingHom
            (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
              (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
            (↑(Quotient.mk (map C I)) X))
        (↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
              (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
          (Quot.mk Setoid.r (↑(monomial n) a))) =
      Quot.mk Setoid.r (↑(monomial n) a)
[PROOFSTEP]
intro n a
[GOAL]
case mk.refine_2
R : Type u_1
inst✝ : CommRing R
I : Ideal R
x✝ : R[X] ⧸ map C I
f : R[X]
n : ℕ
a : R
⊢ ↑(eval₂RingHom
          (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
            (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
          (↑(Quotient.mk (map C I)) X))
      (↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
            (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
        (Quot.mk Setoid.r (↑(monomial n) a))) =
    Quot.mk Setoid.r (↑(monomial n) a)
[PROOFSTEP]
simp only [← smul_X_eq_monomial, ← C_mul' a (X ^ n), Quotient.lift_mk, Submodule.Quotient.quot_mk_eq_mk,
  Quotient.mk_eq_mk, eval₂_X_pow, eval₂_smul, coe_eval₂RingHom, RingHom.map_pow, eval₂_C, RingHom.coe_comp,
  RingHom.map_mul, eval₂_X, Function.comp_apply]
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f g : (R ⧸ I)[X]
⊢ Equiv.toFun
      {
        toFun :=
          ↑(eval₂RingHom
              (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
              (↑(Quotient.mk (map C I)) X)),
        invFun :=
          ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
              (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0)),
        left_inv :=
          (_ :
            ∀ (f : (R ⧸ I)[X]),
              ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                      (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
                  (↑(eval₂RingHom
                        (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                          (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                        (↑(Quotient.mk (map C I)) X))
                    f) =
                f),
        right_inv :=
          (_ :
            ∀ (x : R[X] ⧸ map C I),
              ↑(eval₂RingHom
                      (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                        (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                      (↑(Quotient.mk (map C I)) X))
                  (↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                        (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
                    x) =
                x) }
      (f * g) =
    Equiv.toFun
        {
          toFun :=
            ↑(eval₂RingHom
                (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                  (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                (↑(Quotient.mk (map C I)) X)),
          invFun :=
            ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0)),
          left_inv :=
            (_ :
              ∀ (f : (R ⧸ I)[X]),
                ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                        (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
                    (↑(eval₂RingHom
                          (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                            (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                          (↑(Quotient.mk (map C I)) X))
                      f) =
                  f),
          right_inv :=
            (_ :
              ∀ (x : R[X] ⧸ map C I),
                ↑(eval₂RingHom
                        (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                          (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                        (↑(Quotient.mk (map C I)) X))
                    (↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                          (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
                      x) =
                  x) }
        f *
      Equiv.toFun
        {
          toFun :=
            ↑(eval₂RingHom
                (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                  (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                (↑(Quotient.mk (map C I)) X)),
          invFun :=
            ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0)),
          left_inv :=
            (_ :
              ∀ (f : (R ⧸ I)[X]),
                ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                        (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
                    (↑(eval₂RingHom
                          (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                            (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                          (↑(Quotient.mk (map C I)) X))
                      f) =
                  f),
          right_inv :=
            (_ :
              ∀ (x : R[X] ⧸ map C I),
                ↑(eval₂RingHom
                        (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                          (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                        (↑(Quotient.mk (map C I)) X))
                    (↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                          (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
                      x) =
                  x) }
        g
[PROOFSTEP]
simp only [coe_eval₂RingHom, eval₂_mul]
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f g : (R ⧸ I)[X]
⊢ Equiv.toFun
      {
        toFun :=
          ↑(eval₂RingHom
              (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
              (↑(Quotient.mk (map C I)) X)),
        invFun :=
          ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
              (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0)),
        left_inv :=
          (_ :
            ∀ (f : (R ⧸ I)[X]),
              ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                      (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
                  (↑(eval₂RingHom
                        (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                          (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                        (↑(Quotient.mk (map C I)) X))
                    f) =
                f),
        right_inv :=
          (_ :
            ∀ (x : R[X] ⧸ map C I),
              ↑(eval₂RingHom
                      (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                        (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                      (↑(Quotient.mk (map C I)) X))
                  (↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                        (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
                    x) =
                x) }
      (f + g) =
    Equiv.toFun
        {
          toFun :=
            ↑(eval₂RingHom
                (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                  (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                (↑(Quotient.mk (map C I)) X)),
          invFun :=
            ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0)),
          left_inv :=
            (_ :
              ∀ (f : (R ⧸ I)[X]),
                ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                        (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
                    (↑(eval₂RingHom
                          (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                            (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                          (↑(Quotient.mk (map C I)) X))
                      f) =
                  f),
          right_inv :=
            (_ :
              ∀ (x : R[X] ⧸ map C I),
                ↑(eval₂RingHom
                        (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                          (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                        (↑(Quotient.mk (map C I)) X))
                    (↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                          (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
                      x) =
                  x) }
        f +
      Equiv.toFun
        {
          toFun :=
            ↑(eval₂RingHom
                (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                  (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                (↑(Quotient.mk (map C I)) X)),
          invFun :=
            ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0)),
          left_inv :=
            (_ :
              ∀ (f : (R ⧸ I)[X]),
                ↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                        (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
                    (↑(eval₂RingHom
                          (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                            (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                          (↑(Quotient.mk (map C I)) X))
                      f) =
                  f),
          right_inv :=
            (_ :
              ∀ (x : R[X] ⧸ map C I),
                ↑(eval₂RingHom
                        (Quotient.lift I (RingHom.comp (Quotient.mk (map C I)) C)
                          (_ : ∀ (a : R), a ∈ I → ↑(RingHom.comp (Quotient.mk (map C I)) C) a = 0))
                        (↑(Quotient.mk (map C I)) X))
                    (↑(Quotient.lift (map C I) (eval₂RingHom (RingHom.comp C (Quotient.mk I)) X)
                          (_ : ∀ (f : R[X]), f ∈ map C I → ↑(eval₂RingHom (RingHom.comp C (Quotient.mk I)) X) f = 0))
                      x) =
                  x) }
        g
[PROOFSTEP]
simp only [eval₂_add, coe_eval₂RingHom]
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f : R[X]
⊢ ↑(RingEquiv.symm (polynomialQuotientEquivQuotientPolynomial I)) (↑(Quotient.mk (map C I)) f) =
    Polynomial.map (Quotient.mk I) f
[PROOFSTEP]
rw [polynomialQuotientEquivQuotientPolynomial, RingEquiv.symm_mk, RingEquiv.coe_mk, Equiv.coe_fn_mk, Quotient.lift_mk,
  coe_eval₂RingHom, eval₂_eq_eval_map, ← Polynomial.map_map, ← eval₂_eq_eval_map, Polynomial.eval₂_C_X]
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f : R[X]
⊢ ↑(polynomialQuotientEquivQuotientPolynomial I) (Polynomial.map (Quotient.mk I) f) = ↑(Quotient.mk (map C I)) f
[PROOFSTEP]
apply (polynomialQuotientEquivQuotientPolynomial I).symm.injective
[GOAL]
case a
R : Type u_1
inst✝ : CommRing R
I : Ideal R
f : R[X]
⊢ ↑(RingEquiv.symm (polynomialQuotientEquivQuotientPolynomial I))
      (↑(polynomialQuotientEquivQuotientPolynomial I) (Polynomial.map (Quotient.mk I) f)) =
    ↑(RingEquiv.symm (polynomialQuotientEquivQuotientPolynomial I)) (↑(Quotient.mk (map C I)) f)
[PROOFSTEP]
rw [RingEquiv.symm_apply_apply, polynomialQuotientEquivQuotientPolynomial_symm_mk]
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) }
hx : ↑C x ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
⊢ x = 0
[PROOFSTEP]
let i := ((Quotient.mk I).comp C).rangeRestrict
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) }
hx : ↑C x ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
⊢ x = 0
[PROOFSTEP]
have hi' : RingHom.ker (Polynomial.mapRingHom i) ≤ I :=
  by
  refine' fun f hf => polynomial_mem_ideal_of_coeff_mem_ideal I f fun n => _
  rw [mem_comap, ← Quotient.eq_zero_iff_mem, ← RingHom.comp_apply]
  rw [RingHom.mem_ker, coe_mapRingHom] at hf
  replace hf := congr_arg (fun f : Polynomial _ => f.coeff n) hf
  simp only [coeff_map, coeff_zero] at hf
  rwa [Subtype.ext_iff, RingHom.coe_rangeRestrict] at hf
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) }
hx : ↑C x ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
⊢ RingHom.ker (mapRingHom i) ≤ I
[PROOFSTEP]
refine' fun f hf => polynomial_mem_ideal_of_coeff_mem_ideal I f fun n => _
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) }
hx : ↑C x ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
f : R[X]
hf : f ∈ RingHom.ker (mapRingHom i)
n : ℕ
⊢ coeff f n ∈ comap C I
[PROOFSTEP]
rw [mem_comap, ← Quotient.eq_zero_iff_mem, ← RingHom.comp_apply]
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) }
hx : ↑C x ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
f : R[X]
hf : f ∈ RingHom.ker (mapRingHom i)
n : ℕ
⊢ ↑(RingHom.comp (Quotient.mk I) C) (coeff f n) = 0
[PROOFSTEP]
rw [RingHom.mem_ker, coe_mapRingHom] at hf
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) }
hx : ↑C x ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
f : R[X]
hf : Polynomial.map i f = 0
n : ℕ
⊢ ↑(RingHom.comp (Quotient.mk I) C) (coeff f n) = 0
[PROOFSTEP]
replace hf := congr_arg (fun f : Polynomial _ => f.coeff n) hf
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) }
hx : ↑C x ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
f : R[X]
n : ℕ
hf : (fun f => coeff f n) (Polynomial.map i f) = (fun f => coeff f n) 0
⊢ ↑(RingHom.comp (Quotient.mk I) C) (coeff f n) = 0
[PROOFSTEP]
simp only [coeff_map, coeff_zero] at hf
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) }
hx : ↑C x ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
f : R[X]
n : ℕ
hf : ↑(RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)) (coeff f n) = 0
⊢ ↑(RingHom.comp (Quotient.mk I) C) (coeff f n) = 0
[PROOFSTEP]
rwa [Subtype.ext_iff, RingHom.coe_rangeRestrict] at hf
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
x : { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) }
hx : ↑C x ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
⊢ x = 0
[PROOFSTEP]
obtain ⟨x, hx'⟩ := x
[GOAL]
case mk
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
x : R[X] ⧸ I
hx' : x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C)
hx : ↑C { val := x, property := hx' } ∈ map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
⊢ { val := x, property := hx' } = 0
[PROOFSTEP]
obtain ⟨y, rfl⟩ := RingHom.mem_range.1 hx'
[GOAL]
case mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' : ↑(RingHom.comp (Quotient.mk I) C) y ∈ RingHom.range (RingHom.comp (Quotient.mk I) C)
hx :
  ↑C { val := ↑(RingHom.comp (Quotient.mk I) C) y, property := hx' } ∈
    map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
⊢ { val := ↑(RingHom.comp (Quotient.mk I) C) y, property := hx' } = 0
[PROOFSTEP]
refine' Subtype.eq _
[GOAL]
case mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' : ↑(RingHom.comp (Quotient.mk I) C) y ∈ RingHom.range (RingHom.comp (Quotient.mk I) C)
hx :
  ↑C { val := ↑(RingHom.comp (Quotient.mk I) C) y, property := hx' } ∈
    map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
⊢ ↑{ val := ↑(RingHom.comp (Quotient.mk I) C) y, property := hx' } = ↑0
[PROOFSTEP]
simp only [RingHom.comp_apply, Quotient.eq_zero_iff_mem, ZeroMemClass.coe_zero]
[GOAL]
case mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' : ↑(RingHom.comp (Quotient.mk I) C) y ∈ RingHom.range (RingHom.comp (Quotient.mk I) C)
hx :
  ↑C { val := ↑(RingHom.comp (Quotient.mk I) C) y, property := hx' } ∈
    map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
⊢ ↑C y ∈ I
[PROOFSTEP]
suffices C (i y) ∈ I.map (Polynomial.mapRingHom i)
  by
  obtain ⟨f, hf⟩ :=
    mem_image_of_mem_map_of_surjective (Polynomial.mapRingHom i)
      (Polynomial.map_surjective _ (RingHom.rangeRestrict_surjective ((Quotient.mk I).comp C))) this
  refine' sub_add_cancel (C y) f ▸ I.add_mem (hi' _ : C y - f ∈ I) hf.1
  rw [RingHom.mem_ker, RingHom.map_sub, hf.2, sub_eq_zero, coe_mapRingHom, map_C]
[GOAL]
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' : ↑(RingHom.comp (Quotient.mk I) C) y ∈ RingHom.range (RingHom.comp (Quotient.mk I) C)
hx :
  ↑C { val := ↑(RingHom.comp (Quotient.mk I) C) y, property := hx' } ∈
    map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
this : ↑C (↑i y) ∈ map (mapRingHom i) I
⊢ ↑C y ∈ I
[PROOFSTEP]
obtain ⟨f, hf⟩ :=
  mem_image_of_mem_map_of_surjective (Polynomial.mapRingHom i)
    (Polynomial.map_surjective _ (RingHom.rangeRestrict_surjective ((Quotient.mk I).comp C))) this
[GOAL]
case intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' : ↑(RingHom.comp (Quotient.mk I) C) y ∈ RingHom.range (RingHom.comp (Quotient.mk I) C)
hx :
  ↑C { val := ↑(RingHom.comp (Quotient.mk I) C) y, property := hx' } ∈
    map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
this : ↑C (↑i y) ∈ map (mapRingHom i) I
f : R[X]
hf : f ∈ ↑I ∧ ↑(mapRingHom i) f = ↑C (↑i y)
⊢ ↑C y ∈ I
[PROOFSTEP]
refine' sub_add_cancel (C y) f ▸ I.add_mem (hi' _ : C y - f ∈ I) hf.1
[GOAL]
case intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' : ↑(RingHom.comp (Quotient.mk I) C) y ∈ RingHom.range (RingHom.comp (Quotient.mk I) C)
hx :
  ↑C { val := ↑(RingHom.comp (Quotient.mk I) C) y, property := hx' } ∈
    map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
this : ↑C (↑i y) ∈ map (mapRingHom i) I
f : R[X]
hf : f ∈ ↑I ∧ ↑(mapRingHom i) f = ↑C (↑i y)
⊢ ↑C y - f ∈ RingHom.ker (mapRingHom i)
[PROOFSTEP]
rw [RingHom.mem_ker, RingHom.map_sub, hf.2, sub_eq_zero, coe_mapRingHom, map_C]
[GOAL]
case mk.intro
R : Type u_1
inst✝ : CommRing R
I : Ideal R[X]
i : R →+* { x // x ∈ RingHom.range (RingHom.comp (Quotient.mk I) C) } :=
  RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C)
hi' : RingHom.ker (mapRingHom i) ≤ I
y : R
hx' : ↑(RingHom.comp (Quotient.mk I) C) y ∈ RingHom.range (RingHom.comp (Quotient.mk I) C)
hx :
  ↑C { val := ↑(RingHom.comp (Quotient.mk I) C) y, property := hx' } ∈
    map (mapRingHom (RingHom.rangeRestrict (RingHom.comp (Quotient.mk I) C))) I
⊢ ↑C (↑i y) ∈ map (mapRingHom i) I
[PROOFSTEP]
exact hx
[GOAL]
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
i : R
hi : i ∈ I
⊢ ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0
[PROOFSTEP]
simp only [Function.comp_apply, RingHom.coe_comp, Ideal.Quotient.eq_zero_iff_mem]
[GOAL]
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
i : R
hi : i ∈ I
⊢ ↑C i ∈ Ideal.map C I
[PROOFSTEP]
exact Ideal.mem_map_of_mem _ hi
[GOAL]
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
⊢ ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0
[PROOFSTEP]
rw [as_sum a]
[GOAL]
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
⊢ ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) (Finset.sum (support a) fun v => ↑(monomial v) (coeff v a)) = 0
[PROOFSTEP]
rw [coe_eval₂Hom, eval₂_sum]
[GOAL]
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
⊢ (Finset.sum (support a) fun x => eval₂ (RingHom.comp C (Ideal.Quotient.mk I)) X (↑(monomial x) (coeff x a))) = 0
[PROOFSTEP]
refine' Finset.sum_eq_zero fun n _ => _
[GOAL]
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
n : σ →₀ ℕ
x✝ : n ∈ support a
⊢ eval₂ (RingHom.comp C (Ideal.Quotient.mk I)) X (↑(monomial n) (coeff n a)) = 0
[PROOFSTEP]
simp only [eval₂_monomial, Function.comp_apply, RingHom.coe_comp]
[GOAL]
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
n : σ →₀ ℕ
x✝ : n ∈ support a
⊢ (↑C (↑(Ideal.Quotient.mk I) (coeff n a)) * Finsupp.prod n fun n e => X n ^ e) = 0
[PROOFSTEP]
refine' mul_eq_zero_of_left _ _
[GOAL]
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
n : σ →₀ ℕ
x✝ : n ∈ support a
⊢ ↑C (↑(Ideal.Quotient.mk I) (coeff n a)) = 0
[PROOFSTEP]
suffices coeff n a ∈ I by
  rw [← @Ideal.mk_ker R _ I, RingHom.mem_ker] at this
  simp only [this, C_0]
[GOAL]
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
n : σ →₀ ℕ
x✝ : n ∈ support a
this : coeff n a ∈ I
⊢ ↑C (↑(Ideal.Quotient.mk I) (coeff n a)) = 0
[PROOFSTEP]
rw [← @Ideal.mk_ker R _ I, RingHom.mem_ker] at this
[GOAL]
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
n : σ →₀ ℕ
x✝ : n ∈ support a
this : ↑(Ideal.Quotient.mk I) (coeff n a) = 0
⊢ ↑C (↑(Ideal.Quotient.mk I) (coeff n a)) = 0
[PROOFSTEP]
simp only [this, C_0]
[GOAL]
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
a : MvPolynomial σ R
ha : a ∈ Ideal.map C I
n : σ →₀ ℕ
x✝ : n ∈ support a
⊢ coeff n a ∈ I
[PROOFSTEP]
exact mem_map_C_iff.1 ha n
[GOAL]
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
⊢ Function.RightInverse
    (eval₂
      (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
        (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
      fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i))
    ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
        (_ : ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
[PROOFSTEP]
intro f
[GOAL]
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
f : MvPolynomial σ (R ⧸ I)
⊢ ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
          (_ :
            ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
      (eval₂
        (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
          (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
        (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) f) =
    f
[PROOFSTEP]
apply induction_on f
[GOAL]
case h_C
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
f : MvPolynomial σ (R ⧸ I)
⊢ ∀ (a : R ⧸ I),
    ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
            (_ :
              ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
        (eval₂
          (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
            (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
          (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) (↑C a)) =
      ↑C a
[PROOFSTEP]
intro r
[GOAL]
case h_C
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r✝ : R
I : Ideal R
f : MvPolynomial σ (R ⧸ I)
r : R ⧸ I
⊢ ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
          (_ :
            ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
      (eval₂
        (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
          (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
        (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) (↑C r)) =
    ↑C r
[PROOFSTEP]
obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective r
[GOAL]
case h_C.intro
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r✝ : R
I : Ideal R
f : MvPolynomial σ (R ⧸ I)
r : R
⊢ ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
          (_ :
            ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
      (eval₂
        (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
          (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
        (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) (↑C (↑(Ideal.Quotient.mk I) r))) =
    ↑C (↑(Ideal.Quotient.mk I) r)
[PROOFSTEP]
rw [eval₂_C, Ideal.Quotient.lift_mk, RingHom.comp_apply, Ideal.Quotient.lift_mk, eval₂Hom_C, RingHom.comp_apply]
[GOAL]
case h_add
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
f : MvPolynomial σ (R ⧸ I)
⊢ ∀ (p q : MvPolynomial σ (R ⧸ I)),
    ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
              (_ :
                ∀ (a : MvPolynomial σ R),
                  a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
          (eval₂
            (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
              (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
            (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) p) =
        p →
      ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
                (_ :
                  ∀ (a : MvPolynomial σ R),
                    a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
            (eval₂
              (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
                (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
              (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) q) =
          q →
        ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
                (_ :
                  ∀ (a : MvPolynomial σ R),
                    a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
            (eval₂
              (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
                (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
              (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) (p + q)) =
          p + q
[PROOFSTEP]
intros p q hp hq
[GOAL]
case h_add
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
f p q : MvPolynomial σ (R ⧸ I)
hp :
  ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
          (_ :
            ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
      (eval₂
        (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
          (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
        (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) p) =
    p
hq :
  ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
          (_ :
            ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
      (eval₂
        (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
          (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
        (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) q) =
    q
⊢ ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
          (_ :
            ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
      (eval₂
        (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
          (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
        (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) (p + q)) =
    p + q
[PROOFSTEP]
simp only [RingHom.map_add, MvPolynomial.coe_eval₂Hom, coe_eval₂Hom, MvPolynomial.eval₂_add] at hp hq ⊢
[GOAL]
case h_add
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
f p q : MvPolynomial σ (R ⧸ I)
hp :
  ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
          (_ :
            ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
      (eval₂
        (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
          (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
        (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) p) =
    p
hq :
  ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
          (_ :
            ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
      (eval₂
        (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
          (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
        (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) q) =
    q
⊢ ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
            (_ :
              ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
        (eval₂
          (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
            (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
          (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) p) +
      ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
            (_ :
              ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
        (eval₂
          (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
            (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
          (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) q) =
    p + q
[PROOFSTEP]
rw [hp, hq]
[GOAL]
case h_X
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
f : MvPolynomial σ (R ⧸ I)
⊢ ∀ (p : MvPolynomial σ (R ⧸ I)) (n : σ),
    ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
              (_ :
                ∀ (a : MvPolynomial σ R),
                  a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
          (eval₂
            (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
              (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
            (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) p) =
        p →
      ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
              (_ :
                ∀ (a : MvPolynomial σ R),
                  a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
          (eval₂
            (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
              (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
            (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) (p * X n)) =
        p * X n
[PROOFSTEP]
intros p i hp
[GOAL]
case h_X
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
f p : MvPolynomial σ (R ⧸ I)
i : σ
hp :
  ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
          (_ :
            ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
      (eval₂
        (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
          (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
        (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) p) =
    p
⊢ ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
          (_ :
            ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
      (eval₂
        (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
          (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
        (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) (p * X i)) =
    p * X i
[PROOFSTEP]
simp only [coe_eval₂Hom] at hp
[GOAL]
case h_X
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
f p : MvPolynomial σ (R ⧸ I)
i : σ
hp :
  ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
          (_ :
            ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
      (eval₂
        (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
          (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
        (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) p) =
    p
⊢ ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
          (_ :
            ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
      (eval₂
        (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
          (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
        (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) (p * X i)) =
    p * X i
[PROOFSTEP]
simp only [hp, coe_eval₂Hom, Ideal.Quotient.lift_mk, eval₂_mul, RingHom.map_mul, eval₂_X]
[GOAL]
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
⊢ Function.LeftInverse
    (eval₂
      (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
        (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
      fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i))
    ↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
        (_ : ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
[PROOFSTEP]
intro f
[GOAL]
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
f : MvPolynomial σ R ⧸ Ideal.map C I
⊢ eval₂
      (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
        (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
      (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i))
      (↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
            (_ :
              ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
        f) =
    f
[PROOFSTEP]
obtain ⟨f, rfl⟩ := Ideal.Quotient.mk_surjective f
[GOAL]
case intro
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
f : MvPolynomial σ R
⊢ eval₂
      (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
        (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
      (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i))
      (↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
            (_ :
              ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
        (↑(Ideal.Quotient.mk (Ideal.map C I)) f)) =
    ↑(Ideal.Quotient.mk (Ideal.map C I)) f
[PROOFSTEP]
apply induction_on f
[GOAL]
case intro.h_C
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
f : MvPolynomial σ R
⊢ ∀ (a : R),
    eval₂
        (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
          (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
        (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i))
        (↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
              (_ :
                ∀ (a : MvPolynomial σ R),
                  a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
          (↑(Ideal.Quotient.mk (Ideal.map C I)) (↑C a))) =
      ↑(Ideal.Quotient.mk (Ideal.map C I)) (↑C a)
[PROOFSTEP]
intro r
[GOAL]
case intro.h_C
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r✝ : R
I : Ideal R
f : MvPolynomial σ R
r : R
⊢ eval₂
      (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
        (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
      (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i))
      (↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
            (_ :
              ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
        (↑(Ideal.Quotient.mk (Ideal.map C I)) (↑C r))) =
    ↑(Ideal.Quotient.mk (Ideal.map C I)) (↑C r)
[PROOFSTEP]
rw [Ideal.Quotient.lift_mk, eval₂Hom_C, RingHom.comp_apply, eval₂_C, Ideal.Quotient.lift_mk, RingHom.comp_apply]
[GOAL]
case intro.h_add
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
f : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    eval₂
          (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
            (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
          (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i))
          (↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
                (_ :
                  ∀ (a : MvPolynomial σ R),
                    a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
            (↑(Ideal.Quotient.mk (Ideal.map C I)) p)) =
        ↑(Ideal.Quotient.mk (Ideal.map C I)) p →
      eval₂
            (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
              (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
            (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i))
            (↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
                  (_ :
                    ∀ (a : MvPolynomial σ R),
                      a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
              (↑(Ideal.Quotient.mk (Ideal.map C I)) q)) =
          ↑(Ideal.Quotient.mk (Ideal.map C I)) q →
        eval₂
            (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
              (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
            (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i))
            (↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
                  (_ :
                    ∀ (a : MvPolynomial σ R),
                      a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
              (↑(Ideal.Quotient.mk (Ideal.map C I)) (p + q))) =
          ↑(Ideal.Quotient.mk (Ideal.map C I)) (p + q)
[PROOFSTEP]
intros p q hp hq
[GOAL]
case intro.h_add
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
f p q : MvPolynomial σ R
hp :
  eval₂
      (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
        (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
      (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i))
      (↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
            (_ :
              ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
        (↑(Ideal.Quotient.mk (Ideal.map C I)) p)) =
    ↑(Ideal.Quotient.mk (Ideal.map C I)) p
hq :
  eval₂
      (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
        (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
      (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i))
      (↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
            (_ :
              ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
        (↑(Ideal.Quotient.mk (Ideal.map C I)) q)) =
    ↑(Ideal.Quotient.mk (Ideal.map C I)) q
⊢ eval₂
      (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
        (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
      (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i))
      (↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
            (_ :
              ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
        (↑(Ideal.Quotient.mk (Ideal.map C I)) (p + q))) =
    ↑(Ideal.Quotient.mk (Ideal.map C I)) (p + q)
[PROOFSTEP]
erw [Ideal.Quotient.lift_mk] at hp hq ⊢
[GOAL]
case intro.h_add
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
f p q : MvPolynomial σ R
hp :
  eval₂
      (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
        (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
      (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) (↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) p) =
    ↑(Ideal.Quotient.mk (Ideal.map C I)) p
hq :
  eval₂
      (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
        (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
      (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) (↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) q) =
    ↑(Ideal.Quotient.mk (Ideal.map C I)) q
⊢ eval₂
      (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
        (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
      (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i))
      (↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) (p + q)) =
    ↑(Ideal.Quotient.mk (Ideal.map C I)) (p + q)
[PROOFSTEP]
simp only [Submodule.Quotient.quot_mk_eq_mk, eval₂_add, RingHom.map_add, coe_eval₂Hom, Ideal.Quotient.lift_mk,
  Ideal.Quotient.mk_eq_mk] at hp hq ⊢
[GOAL]
case intro.h_add
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
f p q : MvPolynomial σ R
hp :
  eval₂
      (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
        (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
      (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) (eval₂ (RingHom.comp C (Ideal.Quotient.mk I)) X p) =
    ↑(Ideal.Quotient.mk (Ideal.map C I)) p
hq :
  eval₂
      (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
        (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
      (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) (eval₂ (RingHom.comp C (Ideal.Quotient.mk I)) X q) =
    ↑(Ideal.Quotient.mk (Ideal.map C I)) q
⊢ eval₂
        (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
          (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
        (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) (eval₂ (RingHom.comp C (Ideal.Quotient.mk I)) X p) +
      eval₂
        (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
          (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
        (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) (eval₂ (RingHom.comp C (Ideal.Quotient.mk I)) X q) =
    ↑(Ideal.Quotient.mk (Ideal.map C I)) p + ↑(Ideal.Quotient.mk (Ideal.map C I)) q
[PROOFSTEP]
rw [hp, hq]
[GOAL]
case intro.h_X
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
f : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    eval₂
          (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
            (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
          (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i))
          (↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
                (_ :
                  ∀ (a : MvPolynomial σ R),
                    a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
            (↑(Ideal.Quotient.mk (Ideal.map C I)) p)) =
        ↑(Ideal.Quotient.mk (Ideal.map C I)) p →
      eval₂
          (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
            (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
          (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i))
          (↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
                (_ :
                  ∀ (a : MvPolynomial σ R),
                    a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
            (↑(Ideal.Quotient.mk (Ideal.map C I)) (p * X n))) =
        ↑(Ideal.Quotient.mk (Ideal.map C I)) (p * X n)
[PROOFSTEP]
intros p i hp
[GOAL]
case intro.h_X
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
f p : MvPolynomial σ R
i : σ
hp :
  eval₂
      (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
        (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
      (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i))
      (↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
            (_ :
              ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
        (↑(Ideal.Quotient.mk (Ideal.map C I)) p)) =
    ↑(Ideal.Quotient.mk (Ideal.map C I)) p
⊢ eval₂
      (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
        (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
      (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i))
      (↑(Ideal.Quotient.lift (Ideal.map C I) (eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X)
            (_ :
              ∀ (a : MvPolynomial σ R), a ∈ Ideal.map C I → ↑(eval₂Hom (RingHom.comp C (Ideal.Quotient.mk I)) X) a = 0))
        (↑(Ideal.Quotient.mk (Ideal.map C I)) (p * X i))) =
    ↑(Ideal.Quotient.mk (Ideal.map C I)) (p * X i)
[PROOFSTEP]
simp only [Submodule.Quotient.quot_mk_eq_mk, coe_eval₂Hom, Ideal.Quotient.lift_mk, Ideal.Quotient.mk_eq_mk, eval₂_mul,
  RingHom.map_mul, eval₂_X] at hp ⊢
[GOAL]
case intro.h_X
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
r : R
I : Ideal R
f p : MvPolynomial σ R
i : σ
hp :
  eval₂
      (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
        (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
      (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) (eval₂ (RingHom.comp C (Ideal.Quotient.mk I)) X p) =
    ↑(Ideal.Quotient.mk (Ideal.map C I)) p
⊢ eval₂
        (Ideal.Quotient.lift I (RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C)
          (_ : ∀ (i : R), i ∈ I → ↑(RingHom.comp (Ideal.Quotient.mk (Ideal.map C I)) C) i = 0))
        (fun i => ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)) (eval₂ (RingHom.comp C (Ideal.Quotient.mk I)) X p) *
      ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i) =
    ↑(Ideal.Quotient.mk (Ideal.map C I)) p * ↑(Ideal.Quotient.mk (Ideal.map C I)) (X i)
[PROOFSTEP]
simp only [hp]
  -- Porting note: this definition was split to avoid timeouts.