-- Mathlib/Algebra/Polynomial/Reverse.lean
theorem eval₂_reflect_mul_pow (i : R →+* S) (x : S) [Invertible x] (N : ℕ) (f : R[X])
    (hf : f.natDegree ≤ N) : eval₂ i (⅟ x) (reflect N f) * x ^ N = eval₂ i x f

Proof state:
case refine_3
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
f✝ g✝ : R[X]
a✝³ : f✝.natDegree < g✝.natDegree
a✝² : g✝.natDegree ≤ N
a✝¹ : eval₂ i (⅟x) (reflect N f✝) * x ^ N = eval₂ i x f✝
a✝ : eval₂ i (⅟x) (reflect N g✝) * x ^ N = eval₂ i x g✝
⊢ eval₂ i (⅟x) (reflect N (f✝ + g✝)) * x ^ N = eval₂ i x (f✝ + g✝)

Tactic:
simp [*, add_mul]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
⊢ eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f

Tactic:
refine
  induction_with_natDegree_le (fun f => eval₂ i (⅟ x) (reflect N f) * x ^ N = eval₂ i x f) _ ?_ ?_
    ?_ f hf

Result:
case refine_1
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
⊢ (fun f => eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f) 0

case refine_2
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
⊢ ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → (fun f => eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f) (C r * X ^ n)

case refine_3
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
⊢ ∀ (f g : R[X]),
    f.natDegree < g.natDegree →
      g.natDegree ≤ N →
        (fun f => eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f) f →
          (fun f => eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f) g →
            (fun f => eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f) (f + g)

Proof state:
case refine_1
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
⊢ (fun f => eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f) 0

Tactic:
simp

Result:
no goals

Proof state:
case refine_3
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
⊢ ∀ (f g : R[X]),
    f.natDegree < g.natDegree →
      g.natDegree ≤ N →
        (fun f => eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f) f →
          (fun f => eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f) g →
            (fun f => eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f) (f + g)

Tactic:
intros

Result:
case refine_3
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
f✝ g✝ : R[X]
a✝³ : f✝.natDegree < g✝.natDegree
a✝² : g✝.natDegree ≤ N
a✝¹ : eval₂ i (⅟x) (reflect N f✝) * x ^ N = eval₂ i x f✝
a✝ : eval₂ i (⅟x) (reflect N g✝) * x ^ N = eval₂ i x g✝
⊢ eval₂ i (⅟x) (reflect N (f✝ + g✝)) * x ^ N = eval₂ i x (f✝ + g✝)

Proof state:
case refine_2
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
n : ℕ
r : R
a✝ : r ≠ 0
hnN : n ≤ N
⊢ i r * ⅟x ^ (N - n) * x ^ N = i r * x ^ n

Tactic:
conv in x ^ N => rw [← Nat.sub_add_cancel hnN]

Result:
case refine_2
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
n : ℕ
r : R
a✝ : r ≠ 0
hnN : n ≤ N
⊢ i r * ⅟x ^ (N - n) * x ^ (N - n + n) = i r * x ^ n

Proof state:
case refine_2
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
n : ℕ
r : R
a✝ : r ≠ 0
hnN : n ≤ N
⊢ eval₂ i (⅟x) (reflect N (C r * X ^ n)) * x ^ N = eval₂ i x (C r * X ^ n)

Tactic:
simp only [revAt_le hnN, reflect_C_mul_X_pow, eval₂_X_pow, eval₂_C, eval₂_mul]

Result:
case refine_2
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
n : ℕ
r : R
a✝ : r ≠ 0
hnN : n ≤ N
⊢ i r * ⅟x ^ (N - n) * x ^ N = i r * x ^ n

Proof state:
case refine_2
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
⊢ ∀ (n : ℕ) (r : R), r ≠ 0 → n ≤ N → (fun f => eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f) (C r * X ^ n)

Tactic:
intro n r _ hnN

Result:
case refine_2
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
n : ℕ
r : R
a✝ : r ≠ 0
hnN : n ≤ N
⊢ eval₂ i (⅟x) (reflect N (C r * X ^ n)) * x ^ N = eval₂ i x (C r * X ^ n)

Proof state:
case refine_2
R : Type u_1
inst✝² : Semiring R
S : Type u_2
inst✝¹ : CommSemiring S
i : R →+* S
x : S
inst✝ : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
n : ℕ
r : R
a✝ : r ≠ 0
hnN : n ≤ N
⊢ i r * ⅟x ^ (N - n) * x ^ (N - n + n) = i r * x ^ n

Tactic:
rw [pow_add, ← mul_assoc, mul_assoc (i r), ← mul_pow, invOf_mul_self, one_pow, mul_one]

Result:
no goals