[GOAL]
R : Type u_1
inst✝ : CommSemiring R
⊢ R[X] →ₐ[R] R[T;T⁻¹]
[PROOFSTEP]
refine' AlgHom.comp _ (toFinsuppIsoAlg R).toAlgHom
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
⊢ AddMonoidAlgebra R ℕ →ₐ[R] R[T;T⁻¹]
[PROOFSTEP]
exact mapDomainAlgHom R R Int.ofNatHom
[GOAL]
R : Type u_1
inst✝ : Semiring R
m n : ℤ
⊢ T (m + n) = T m * T n
[PROOFSTEP]
simp [T, single_mul_single]
[GOAL]
R : Type u_1
inst✝ : Semiring R
m n : ℤ
⊢ T (m - n) = T m * T (-n)
[PROOFSTEP]
rw [← T_add, sub_eq_add_neg]
[GOAL]
R : Type u_1
inst✝ : Semiring R
m : ℤ
n : ℕ
⊢ T m ^ n = T (↑n * m)
[PROOFSTEP]
rw [T, T, single_pow n, one_pow, nsmul_eq_mul]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
m n : ℤ
⊢ f * T m * T n = f * T (m + n)
[PROOFSTEP]
simp [← T_add, mul_assoc]
[GOAL]
R : Type u_1
inst✝ : Semiring R
r : R
n : ℤ
⊢ Finsupp.single n r = ↑C r * T n
[PROOFSTEP]
simp [C, T, single_mul_single]
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℕ
r : R
⊢ Finsupp.mapDomain Nat.cast (↑(monomial n) r).toFinsupp = ↑C r * T ↑n
[PROOFSTEP]
rw [toFinsupp_monomial, Finsupp.mapDomain_single, single_eq_C_mul_T]
[GOAL]
R : Type u_1
inst✝ : Semiring R
r : R
⊢ ↑toLaurent (↑Polynomial.C r) = ↑C r
[PROOFSTEP]
convert Polynomial.toLaurent_C_mul_T 0 r
[GOAL]
case h.e'_3
R : Type u_1
inst✝ : Semiring R
r : R
⊢ ↑C r = ↑C r * T ↑0
[PROOFSTEP]
simp only [Int.ofNat_zero, T_zero, mul_one]
[GOAL]
R : Type u_1
inst✝ : Semiring R
⊢ ↑toLaurent X = T 1
[PROOFSTEP]
have : (Polynomial.X : R[X]) = monomial 1 1 := by simp [← C_mul_X_pow_eq_monomial]
[GOAL]
R : Type u_1
inst✝ : Semiring R
⊢ X = ↑(monomial 1) 1
[PROOFSTEP]
simp [← C_mul_X_pow_eq_monomial]
[GOAL]
R : Type u_1
inst✝ : Semiring R
this : X = ↑(monomial 1) 1
⊢ ↑toLaurent X = T 1
[PROOFSTEP]
simp [this, Polynomial.toLaurent_C_mul_T]
[GOAL]
R : Type u_1
inst✝ : Semiring R
r : R
f : R[X]
⊢ ↑toLaurent (↑Polynomial.C r * f) = ↑C r * ↑toLaurent f
[PROOFSTEP]
simp only [_root_.map_mul, Polynomial.toLaurent_C]
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℕ
⊢ ↑toLaurent (X ^ n) = T ↑n
[PROOFSTEP]
simp only [map_pow, Polynomial.toLaurent_X, T_pow, mul_one]
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℕ
r : R
⊢ ↑toLaurent (↑Polynomial.C r * X ^ n) = ↑C r * T ↑n
[PROOFSTEP]
simp only [_root_.map_mul, Polynomial.toLaurent_C, Polynomial.toLaurent_X_pow]
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℤ
⊢ T (-n) * T n = 1
[PROOFSTEP]
rw [← T_add, add_left_neg, T_zero]
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℤ
⊢ T n * T (-n) = 1
[PROOFSTEP]
rw [← T_add, add_right_neg, T_zero]
[GOAL]
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
⊢ M p
[PROOFSTEP]
have A : ∀ {n : ℤ} {a : R}, M (C a * T n) := by
  intro n a
  refine Int.induction_on n ?_ ?_ ?_
  · simpa only [T_zero, mul_one] using h_C a
  · exact fun m => h_C_mul_T m a
  · exact fun m => h_C_mul_T_Z m a
[GOAL]
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
⊢ ∀ {n : ℤ} {a : R}, M (↑C a * T n)
[PROOFSTEP]
intro n a
[GOAL]
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
n : ℤ
a : R
⊢ M (↑C a * T n)
[PROOFSTEP]
refine Int.induction_on n ?_ ?_ ?_
[GOAL]
case refine_1
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
n : ℤ
a : R
⊢ M (↑C a * T 0)
[PROOFSTEP]
simpa only [T_zero, mul_one] using h_C a
[GOAL]
case refine_2
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
n : ℤ
a : R
⊢ ∀ (i : ℕ), M (↑C a * T ↑i) → M (↑C a * T (↑i + 1))
[PROOFSTEP]
exact fun m => h_C_mul_T m a
[GOAL]
case refine_3
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
n : ℤ
a : R
⊢ ∀ (i : ℕ), M (↑C a * T (-↑i)) → M (↑C a * T (-↑i - 1))
[PROOFSTEP]
exact fun m => h_C_mul_T_Z m a
[GOAL]
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
⊢ M p
[PROOFSTEP]
have B : ∀ s : Finset ℤ, M (s.sum fun n : ℤ => C (p.toFun n) * T n) :=
  by
  apply Finset.induction
  · convert h_C 0
    simp only [Finset.sum_empty, _root_.map_zero]
  · intro n s ns ih
    rw [Finset.sum_insert ns]
    exact h_add A ih
[GOAL]
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
⊢ ∀ (s : Finset ℤ), M (∑ n in s, ↑C (toFun p n) * T n)
[PROOFSTEP]
apply Finset.induction
[GOAL]
case empty
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
⊢ M (∑ n in ∅, ↑C (toFun p n) * T n)
[PROOFSTEP]
convert h_C 0
[GOAL]
case h.e'_1
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
⊢ ∑ n in ∅, ↑C (toFun p n) * T n = ↑C 0
[PROOFSTEP]
simp only [Finset.sum_empty, _root_.map_zero]
[GOAL]
case insert
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
⊢ ∀ ⦃a : ℤ⦄ {s : Finset ℤ}, ¬a ∈ s → M (∑ n in s, ↑C (toFun p n) * T n) → M (∑ n in insert a s, ↑C (toFun p n) * T n)
[PROOFSTEP]
intro n s ns ih
[GOAL]
case insert
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
n : ℤ
s : Finset ℤ
ns : ¬n ∈ s
ih : M (∑ n in s, ↑C (toFun p n) * T n)
⊢ M (∑ n in insert n s, ↑C (toFun p n) * T n)
[PROOFSTEP]
rw [Finset.sum_insert ns]
[GOAL]
case insert
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
n : ℤ
s : Finset ℤ
ns : ¬n ∈ s
ih : M (∑ n in s, ↑C (toFun p n) * T n)
⊢ M (↑C (toFun p n) * T n + ∑ x in s, ↑C (toFun p x) * T x)
[PROOFSTEP]
exact h_add A ih
[GOAL]
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n in s, ↑C (toFun p n) * T n)
⊢ M p
[PROOFSTEP]
convert B p.support
[GOAL]
case h.e'_1
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n in s, ↑C (toFun p n) * T n)
⊢ p = ∑ n in p.support, ↑C (toFun p n) * T n
[PROOFSTEP]
ext a
[GOAL]
case h.e'_1.h
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n in s, ↑C (toFun p n) * T n)
a : ℤ
⊢ ↑p a = ↑(∑ n in p.support, ↑C (toFun p n) * T n) a
[PROOFSTEP]
simp_rw [← single_eq_C_mul_T]
  -- Porting note: did not make progress in `simp_rw`
[GOAL]
case h.e'_1.h
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n in s, ↑C (toFun p n) * T n)
a : ℤ
⊢ ↑p a = ↑(∑ x in p.support, Finsupp.single x (toFun p x)) a
[PROOFSTEP]
rw [Finset.sum_apply']
[GOAL]
case h.e'_1.h
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n in s, ↑C (toFun p n) * T n)
a : ℤ
⊢ ↑p a = ∑ k in p.support, ↑(Finsupp.single k (toFun p k)) a
[PROOFSTEP]
simp_rw [Finsupp.single_apply, Finset.sum_ite_eq']
[GOAL]
case h.e'_1.h
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n in s, ↑C (toFun p n) * T n)
a : ℤ
⊢ ↑p a = if a ∈ p.support then toFun p a else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n in s, ↑C (toFun p n) * T n)
a : ℤ
h : a ∈ p.support
⊢ ↑p a = toFun p a
[PROOFSTEP]
rfl
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_C : ∀ (a : R), M (↑C a)
h_add : ∀ {p q : R[T;T⁻¹]}, M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
h_C_mul_T_Z : ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
A : ∀ {n : ℤ} {a : R}, M (↑C a * T n)
B : ∀ (s : Finset ℤ), M (∑ n in s, ↑C (toFun p n) * T n)
a : ℤ
h : ¬a ∈ p.support
⊢ ↑p a = 0
[PROOFSTEP]
exact Finsupp.not_mem_support_iff.mp h
[GOAL]
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_add : ∀ (p q : R[T;T⁻¹]), M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℤ) (a : R), M (↑C a * T n)
⊢ M p
[PROOFSTEP]
refine' p.induction_on (fun a => _) (fun {p q} => h_add p q) _ _
[GOAL]
case refine'_1
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_add : ∀ (p q : R[T;T⁻¹]), M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℤ) (a : R), M (↑C a * T n)
a : R
⊢ M (↑C a)
[PROOFSTEP]
try exact fun n f _ => h_C_mul_T _ f
[GOAL]
case refine'_1
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_add : ∀ (p q : R[T;T⁻¹]), M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℤ) (a : R), M (↑C a * T n)
a : R
⊢ M (↑C a)
[PROOFSTEP]
exact fun n f _ => h_C_mul_T _ f
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_add : ∀ (p q : R[T;T⁻¹]), M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℤ) (a : R), M (↑C a * T n)
⊢ ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
[PROOFSTEP]
try exact fun n f _ => h_C_mul_T _ f
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_add : ∀ (p q : R[T;T⁻¹]), M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℤ) (a : R), M (↑C a * T n)
⊢ ∀ (n : ℕ) (a : R), M (↑C a * T ↑n) → M (↑C a * T (↑n + 1))
[PROOFSTEP]
exact fun n f _ => h_C_mul_T _ f
[GOAL]
case refine'_3
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_add : ∀ (p q : R[T;T⁻¹]), M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℤ) (a : R), M (↑C a * T n)
⊢ ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
[PROOFSTEP]
try exact fun n f _ => h_C_mul_T _ f
[GOAL]
case refine'_3
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_add : ∀ (p q : R[T;T⁻¹]), M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℤ) (a : R), M (↑C a * T n)
⊢ ∀ (n : ℕ) (a : R), M (↑C a * T (-↑n)) → M (↑C a * T (-↑n - 1))
[PROOFSTEP]
exact fun n f _ => h_C_mul_T _ f
[GOAL]
case refine'_1
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_add : ∀ (p q : R[T;T⁻¹]), M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℤ) (a : R), M (↑C a * T n)
a : R
⊢ M (↑C a)
[PROOFSTEP]
convert h_C_mul_T 0 a
[GOAL]
case h.e'_1
R : Type u_1
inst✝ : Semiring R
M : R[T;T⁻¹] → Prop
p : R[T;T⁻¹]
h_add : ∀ (p q : R[T;T⁻¹]), M p → M q → M (p + q)
h_C_mul_T : ∀ (n : ℤ) (a : R), M (↑C a * T n)
a : R
⊢ ↑C a = ↑C a * T 0
[PROOFSTEP]
exact (mul_one _).symm
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℤ
f : R[T;T⁻¹]
m : ℤ
a : R
⊢ T n * (↑C a * T m) = ↑C a * T m * T n
[PROOFSTEP]
rw [T, T, ← single_eq_C, single_mul_single, single_mul_single, single_mul_single]
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℤ
f : R[T;T⁻¹]
m : ℤ
a : R
⊢ AddMonoidAlgebra.single (n + (0 + m)) (1 * (a * 1)) = AddMonoidAlgebra.single (0 + m + n) (a * 1 * 1)
[PROOFSTEP]
simp [add_comm]
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
⊢ ↑trunc (↑C r * T n) = if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0
[PROOFSTEP]
have : Function.Injective Int.ofNat := fun x y h => Int.ofNat_inj.mp h
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
⊢ ↑trunc (↑C r * T n) = if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0
[PROOFSTEP]
apply (toFinsuppIso R).injective
[GOAL]
case a
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
⊢ ↑(toFinsuppIso R) (↑trunc (↑C r * T n)) = ↑(toFinsuppIso R) (if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0)
[PROOFSTEP]
rw [← single_eq_C_mul_T, trunc, AddMonoidHom.coe_comp, Function.comp_apply]
  -- Porting note: was `rw`
[GOAL]
case a
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
⊢ ↑(toFinsuppIso R)
      (↑(RingEquiv.toAddMonoidHom (RingEquiv.symm (toFinsuppIso R)))
        (↑(comapDomain.addMonoidHom (_ : ∀ (x x_1 : ℕ), Int.ofNat x = Int.ofNat x_1 → x = x_1)) (Finsupp.single n r))) =
    ↑(toFinsuppIso R) (if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0)
[PROOFSTEP]
erw [comapDomain.addMonoidHom_apply this]
[GOAL]
case a
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
⊢ comapDomain Int.ofNat (Finsupp.single n r) (_ : Set.InjOn Int.ofNat (Int.ofNat ⁻¹' ↑(Finsupp.single n r).support)) =
    ↑(toFinsuppIso R) (if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0)
[PROOFSTEP]
rw [toFinsuppIso_apply]
  -- Porting note: rewrote proof below relative to mathlib3.
[GOAL]
case a
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
⊢ comapDomain Int.ofNat (Finsupp.single n r) (_ : Set.InjOn Int.ofNat (Int.ofNat ⁻¹' ↑(Finsupp.single n r).support)) =
    (if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0).toFinsupp
[PROOFSTEP]
by_cases n0 : 0 ≤ n
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
n0 : 0 ≤ n
⊢ comapDomain Int.ofNat (Finsupp.single n r) (_ : Set.InjOn Int.ofNat (Int.ofNat ⁻¹' ↑(Finsupp.single n r).support)) =
    (if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0).toFinsupp
[PROOFSTEP]
lift n to ℕ using n0
[GOAL]
case pos.intro
R : Type u_1
inst✝ : Semiring R
r : R
this : Function.Injective Int.ofNat
n : ℕ
⊢ comapDomain Int.ofNat (Finsupp.single (↑n) r)
      (_ : Set.InjOn Int.ofNat (Int.ofNat ⁻¹' ↑(Finsupp.single (↑n) r).support)) =
    (if 0 ≤ ↑n then ↑(monomial (Int.toNat ↑n)) r else 0).toFinsupp
[PROOFSTEP]
erw [comapDomain_single]
[GOAL]
case pos.intro
R : Type u_1
inst✝ : Semiring R
r : R
this : Function.Injective Int.ofNat
n : ℕ
⊢ Finsupp.single n r = (if 0 ≤ ↑n then ↑(monomial (Int.toNat ↑n)) r else 0).toFinsupp
[PROOFSTEP]
simp only [Nat.cast_nonneg, Int.toNat_ofNat, ite_true, toFinsupp_monomial]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
n0 : ¬0 ≤ n
⊢ comapDomain Int.ofNat (Finsupp.single n r) (_ : Set.InjOn Int.ofNat (Int.ofNat ⁻¹' ↑(Finsupp.single n r).support)) =
    (if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0).toFinsupp
[PROOFSTEP]
lift -n to ℕ using (neg_pos.mpr (not_le.mp n0)).le with m
[GOAL]
case neg.intro
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
n0 : ¬0 ≤ n
m : ℕ
trunc_C_mul_T✝ trunc_C_mul_T : ∀ (n : ℤ) (r : R), ↑trunc (↑C r * T n) = if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0
⊢ comapDomain Int.ofNat (Finsupp.single n r) (_ : Set.InjOn Int.ofNat (Int.ofNat ⁻¹' ↑(Finsupp.single n r).support)) =
    (if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0).toFinsupp
[PROOFSTEP]
rw [toFinsupp_inj, if_neg n0]
[GOAL]
case neg.intro
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
n0 : ¬0 ≤ n
m : ℕ
trunc_C_mul_T✝ trunc_C_mul_T : ∀ (n : ℤ) (r : R), ↑trunc (↑C r * T n) = if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0
⊢ {
      toFinsupp :=
        comapDomain Int.ofNat (Finsupp.single n r)
          (_ : Set.InjOn Int.ofNat (Int.ofNat ⁻¹' ↑(Finsupp.single n r).support)) } =
    0
[PROOFSTEP]
ext a
[GOAL]
case neg.intro.a
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this : Function.Injective Int.ofNat
n0 : ¬0 ≤ n
m : ℕ
trunc_C_mul_T✝ trunc_C_mul_T : ∀ (n : ℤ) (r : R), ↑trunc (↑C r * T n) = if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0
a : ℕ
⊢ coeff
      {
        toFinsupp :=
          comapDomain Int.ofNat (Finsupp.single n r)
            (_ : Set.InjOn Int.ofNat (Int.ofNat ⁻¹' ↑(Finsupp.single n r).support)) }
      a =
    coeff 0 a
[PROOFSTEP]
have := ((not_le.mp n0).trans_le (Int.ofNat_zero_le a)).ne
[GOAL]
case neg.intro.a
R : Type u_1
inst✝ : Semiring R
n : ℤ
r : R
this✝ : Function.Injective Int.ofNat
n0 : ¬0 ≤ n
m : ℕ
trunc_C_mul_T✝ trunc_C_mul_T : ∀ (n : ℤ) (r : R), ↑trunc (↑C r * T n) = if 0 ≤ n then ↑(monomial (Int.toNat n)) r else 0
a : ℕ
this : n ≠ ↑a
⊢ coeff
      {
        toFinsupp :=
          comapDomain Int.ofNat (Finsupp.single n r)
            (_ : Set.InjOn Int.ofNat (Int.ofNat ⁻¹' ↑(Finsupp.single n r).support)) }
      a =
    coeff 0 a
[PROOFSTEP]
simp only [coeff_ofFinsupp, comapDomain_apply, Int.ofNat_eq_coe, coeff_zero, single_eq_of_ne this]
[GOAL]
R : Type u_1
inst✝ : Semiring R
⊢ Function.LeftInverse ↑trunc ↑toLaurent
[PROOFSTEP]
refine' fun f => f.induction_on' _ _
[GOAL]
case refine'_1
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ ∀ (p q : R[X]), ↑trunc (↑toLaurent p) = p → ↑trunc (↑toLaurent q) = q → ↑trunc (↑toLaurent (p + q)) = p + q
[PROOFSTEP]
intro f g hf hg
[GOAL]
case refine'_1
R : Type u_1
inst✝ : Semiring R
f✝ f g : R[X]
hf : ↑trunc (↑toLaurent f) = f
hg : ↑trunc (↑toLaurent g) = g
⊢ ↑trunc (↑toLaurent (f + g)) = f + g
[PROOFSTEP]
simp only [hf, hg, _root_.map_add]
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ ∀ (n : ℕ) (a : R), ↑trunc (↑toLaurent (↑(monomial n) a)) = ↑(monomial n) a
[PROOFSTEP]
intro n r
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
r : R
⊢ ↑trunc (↑toLaurent (↑(monomial n) r)) = ↑(monomial n) r
[PROOFSTEP]
simp only [Polynomial.toLaurent_C_mul_T, trunc_C_mul_T, Int.coe_nat_nonneg, Int.toNat_coe_nat, if_true]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
⊢ ∃ n f', ↑toLaurent f' = f * T ↑n
[PROOFSTEP]
refine f.induction_on' ?_ fun n a => ?_
[GOAL]
case refine_1
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
⊢ ∀ (p q : R[T;T⁻¹]),
    (∃ n f', ↑toLaurent f' = p * T ↑n) → (∃ n f', ↑toLaurent f' = q * T ↑n) → ∃ n f', ↑toLaurent f' = (p + q) * T ↑n
[PROOFSTEP]
clear f
[GOAL]
case refine_2
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
n : ℤ
a : R
⊢ ∃ n_1 f', ↑toLaurent f' = ↑C a * T n * T ↑n_1
[PROOFSTEP]
clear f
[GOAL]
case refine_1
R : Type u_1
inst✝ : Semiring R
⊢ ∀ (p q : R[T;T⁻¹]),
    (∃ n f', ↑toLaurent f' = p * T ↑n) → (∃ n f', ↑toLaurent f' = q * T ↑n) → ∃ n f', ↑toLaurent f' = (p + q) * T ↑n
[PROOFSTEP]
rintro f g ⟨m, fn, hf⟩ ⟨n, gn, hg⟩
[GOAL]
case refine_1.intro.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
f g : R[T;T⁻¹]
m : ℕ
fn : R[X]
hf : ↑toLaurent fn = f * T ↑m
n : ℕ
gn : R[X]
hg : ↑toLaurent gn = g * T ↑n
⊢ ∃ n f', ↑toLaurent f' = (f + g) * T ↑n
[PROOFSTEP]
refine' ⟨m + n, fn * X ^ n + gn * X ^ m, _⟩
[GOAL]
case refine_1.intro.intro.intro.intro
R : Type u_1
inst✝ : Semiring R
f g : R[T;T⁻¹]
m : ℕ
fn : R[X]
hf : ↑toLaurent fn = f * T ↑m
n : ℕ
gn : R[X]
hg : ↑toLaurent gn = g * T ↑n
⊢ ↑toLaurent (fn * X ^ n + gn * X ^ m) = (f + g) * T ↑(m + n)
[PROOFSTEP]
simp only [hf, hg, add_mul, add_comm (n : ℤ), map_add, map_mul, Polynomial.toLaurent_X_pow, mul_T_assoc, Int.ofNat_add]
[GOAL]
case refine_2
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
⊢ ∃ n_1 f', ↑toLaurent f' = ↑C a * T n * T ↑n_1
[PROOFSTEP]
cases' n with n n
[GOAL]
case refine_2.ofNat
R : Type u_1
inst✝ : Semiring R
a : R
n : ℕ
⊢ ∃ n_1 f', ↑toLaurent f' = ↑C a * T (Int.ofNat n) * T ↑n_1
[PROOFSTEP]
exact ⟨0, Polynomial.C a * X ^ n, by simp⟩
[GOAL]
R : Type u_1
inst✝ : Semiring R
a : R
n : ℕ
⊢ ↑toLaurent (↑Polynomial.C a * X ^ n) = ↑C a * T (Int.ofNat n) * T ↑0
[PROOFSTEP]
simp
[GOAL]
case refine_2.negSucc
R : Type u_1
inst✝ : Semiring R
a : R
n : ℕ
⊢ ∃ n_1 f', ↑toLaurent f' = ↑C a * T (Int.negSucc n) * T ↑n_1
[PROOFSTEP]
refine' ⟨n + 1, Polynomial.C a, _⟩
[GOAL]
case refine_2.negSucc
R : Type u_1
inst✝ : Semiring R
a : R
n : ℕ
⊢ ↑toLaurent (↑Polynomial.C a) = ↑C a * T (Int.negSucc n) * T ↑(n + 1)
[PROOFSTEP]
simp only [Int.negSucc_eq, Polynomial.toLaurent_C, Int.ofNat_succ, mul_T_assoc, add_left_neg, T_zero, mul_one]
[GOAL]
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
f : R[T;T⁻¹]
Qf : ∀ {f : R[X]} {n : ℕ}, Q (↑toLaurent f * T (-↑n))
⊢ Q f
[PROOFSTEP]
rcases f.exists_T_pow with ⟨n, f', hf⟩
[GOAL]
case intro.intro
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
f : R[T;T⁻¹]
Qf : ∀ {f : R[X]} {n : ℕ}, Q (↑toLaurent f * T (-↑n))
n : ℕ
f' : R[X]
hf : ↑toLaurent f' = f * T ↑n
⊢ Q f
[PROOFSTEP]
rw [← mul_one f, ← T_zero, ← Nat.cast_zero, ← Nat.sub_self n, Nat.cast_sub rfl.le, T_sub, ← mul_assoc, ← hf]
[GOAL]
case intro.intro
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
f : R[T;T⁻¹]
Qf : ∀ {f : R[X]} {n : ℕ}, Q (↑toLaurent f * T (-↑n))
n : ℕ
f' : R[X]
hf : ↑toLaurent f' = f * T ↑n
⊢ Q (↑toLaurent f' * T (-↑n))
[PROOFSTEP]
exact Qf
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q (↑toLaurent f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
⊢ Q f
[PROOFSTEP]
induction' f using LaurentPolynomial.induction_on_mul_T with f n
[GOAL]
case Qf
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q (↑toLaurent f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
f : R[X]
n : ℕ
⊢ Q (↑toLaurent f * T (-↑n))
[PROOFSTEP]
induction' n with n hn
[GOAL]
case Qf.zero
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q (↑toLaurent f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
f : R[X]
⊢ Q (↑toLaurent f * T (-↑Nat.zero))
[PROOFSTEP]
simpa only [Nat.zero_eq, Nat.cast_zero, neg_zero, T_zero, mul_one] using Qf _
[GOAL]
case Qf.succ
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q (↑toLaurent f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
f : R[X]
n : ℕ
hn : Q (↑toLaurent f * T (-↑n))
⊢ Q (↑toLaurent f * T (-↑(Nat.succ n)))
[PROOFSTEP]
convert QT _ _
[GOAL]
case Qf.succ.convert_2
R : Type u_1
inst✝ : Semiring R
Q : R[T;T⁻¹] → Prop
Qf : ∀ (f : R[X]), Q (↑toLaurent f)
QT : ∀ (f : R[T;T⁻¹]), Q (f * T 1) → Q f
f : R[X]
n : ℕ
hn : Q (↑toLaurent f * T (-↑n))
⊢ Q (↑toLaurent f * T (-↑(Nat.succ n)) * T 1)
[PROOFSTEP]
simpa using hn
[GOAL]
R : Type u_1
inst✝ : Semiring R
a : R
n : ℤ
⊢ (↑C a * T n).support ⊆ {n}
[PROOFSTEP]
rw [← single_eq_C_mul_T]
[GOAL]
R : Type u_1
inst✝ : Semiring R
a : R
n : ℤ
⊢ (Finsupp.single n a).support ⊆ {n}
[PROOFSTEP]
exact support_single_subset
[GOAL]
R : Type u_1
inst✝ : Semiring R
a : R
a0 : a ≠ 0
n : ℤ
⊢ (↑C a * T n).support = {n}
[PROOFSTEP]
rw [← single_eq_C_mul_T]
[GOAL]
R : Type u_1
inst✝ : Semiring R
a : R
a0 : a ≠ 0
n : ℤ
⊢ (Finsupp.single n a).support = {n}
[PROOFSTEP]
exact support_single_ne_zero _ a0
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (↑toLaurent f).support = Finset.map Nat.castEmbedding (Polynomial.support f)
[PROOFSTEP]
generalize hd : f.support = s
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[X]
s : Finset ℕ
hd : Polynomial.support f = s
⊢ (↑toLaurent f).support = Finset.map Nat.castEmbedding s
[PROOFSTEP]
revert f
[GOAL]
R : Type u_1
inst✝ : Semiring R
s : Finset ℕ
⊢ ∀ (f : R[X]), Polynomial.support f = s → (↑toLaurent f).support = Finset.map Nat.castEmbedding s
[PROOFSTEP]
refine' Finset.induction_on s _ _
[GOAL]
case refine'_1
R : Type u_1
inst✝ : Semiring R
s : Finset ℕ
⊢ ∀ (f : R[X]), Polynomial.support f = ∅ → (↑toLaurent f).support = Finset.map Nat.castEmbedding ∅
[PROOFSTEP]
clear s
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semiring R
s : Finset ℕ
⊢ ∀ ⦃a : ℕ⦄ {s : Finset ℕ},
    ¬a ∈ s →
      (∀ (f : R[X]), Polynomial.support f = s → (↑toLaurent f).support = Finset.map Nat.castEmbedding s) →
        ∀ (f : R[X]),
          Polynomial.support f = insert a s → (↑toLaurent f).support = Finset.map Nat.castEmbedding (insert a s)
[PROOFSTEP]
clear s
[GOAL]
case refine'_1
R : Type u_1
inst✝ : Semiring R
⊢ ∀ (f : R[X]), Polynomial.support f = ∅ → (↑toLaurent f).support = Finset.map Nat.castEmbedding ∅
[PROOFSTEP]
simp (config := { contextual := true }) only [Polynomial.support_eq_empty, map_zero, Finsupp.support_zero,
  eq_self_iff_true, imp_true_iff, Finset.map_empty, Finsupp.support_eq_empty]
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semiring R
⊢ ∀ ⦃a : ℕ⦄ {s : Finset ℕ},
    ¬a ∈ s →
      (∀ (f : R[X]), Polynomial.support f = s → (↑toLaurent f).support = Finset.map Nat.castEmbedding s) →
        ∀ (f : R[X]),
          Polynomial.support f = insert a s → (↑toLaurent f).support = Finset.map Nat.castEmbedding (insert a s)
[PROOFSTEP]
intro a s as hf f fs
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semiring R
a : ℕ
s : Finset ℕ
as : ¬a ∈ s
hf : ∀ (f : R[X]), Polynomial.support f = s → (↑toLaurent f).support = Finset.map Nat.castEmbedding s
f : R[X]
fs : Polynomial.support f = insert a s
⊢ (↑toLaurent f).support = Finset.map Nat.castEmbedding (insert a s)
[PROOFSTEP]
have : (erase a f).toLaurent.support = s.map Nat.castEmbedding :=
  by
  refine' hf (f.erase a) _
  simp only [fs, Finset.erase_eq_of_not_mem as, Polynomial.support_erase, Finset.erase_insert_eq_erase]
[GOAL]
R : Type u_1
inst✝ : Semiring R
a : ℕ
s : Finset ℕ
as : ¬a ∈ s
hf : ∀ (f : R[X]), Polynomial.support f = s → (↑toLaurent f).support = Finset.map Nat.castEmbedding s
f : R[X]
fs : Polynomial.support f = insert a s
⊢ (↑toLaurent (Polynomial.erase a f)).support = Finset.map Nat.castEmbedding s
[PROOFSTEP]
refine' hf (f.erase a) _
[GOAL]
R : Type u_1
inst✝ : Semiring R
a : ℕ
s : Finset ℕ
as : ¬a ∈ s
hf : ∀ (f : R[X]), Polynomial.support f = s → (↑toLaurent f).support = Finset.map Nat.castEmbedding s
f : R[X]
fs : Polynomial.support f = insert a s
⊢ Polynomial.support (Polynomial.erase a f) = s
[PROOFSTEP]
simp only [fs, Finset.erase_eq_of_not_mem as, Polynomial.support_erase, Finset.erase_insert_eq_erase]
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semiring R
a : ℕ
s : Finset ℕ
as : ¬a ∈ s
hf : ∀ (f : R[X]), Polynomial.support f = s → (↑toLaurent f).support = Finset.map Nat.castEmbedding s
f : R[X]
fs : Polynomial.support f = insert a s
this : (↑toLaurent (Polynomial.erase a f)).support = Finset.map Nat.castEmbedding s
⊢ (↑toLaurent f).support = Finset.map Nat.castEmbedding (insert a s)
[PROOFSTEP]
rw [← monomial_add_erase f a, Finset.map_insert, ← this, map_add, Polynomial.toLaurent_C_mul_T, support_add_eq,
  Finset.insert_eq]
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semiring R
a : ℕ
s : Finset ℕ
as : ¬a ∈ s
hf : ∀ (f : R[X]), Polynomial.support f = s → (↑toLaurent f).support = Finset.map Nat.castEmbedding s
f : R[X]
fs : Polynomial.support f = insert a s
this : (↑toLaurent (Polynomial.erase a f)).support = Finset.map Nat.castEmbedding s
⊢ (↑C (coeff f a) * T ↑a).support ∪ (↑toLaurent (Polynomial.erase a f)).support =
    {↑Nat.castEmbedding a} ∪ (↑toLaurent (Polynomial.erase a f)).support
[PROOFSTEP]
congr
[GOAL]
case refine'_2.e_a
R : Type u_1
inst✝ : Semiring R
a : ℕ
s : Finset ℕ
as : ¬a ∈ s
hf : ∀ (f : R[X]), Polynomial.support f = s → (↑toLaurent f).support = Finset.map Nat.castEmbedding s
f : R[X]
fs : Polynomial.support f = insert a s
this : (↑toLaurent (Polynomial.erase a f)).support = Finset.map Nat.castEmbedding s
⊢ (↑C (coeff f a) * T ↑a).support = {↑Nat.castEmbedding a}
[PROOFSTEP]
exact support_C_mul_T_of_ne_zero (Polynomial.mem_support_iff.mp (by simp [fs])) _
[GOAL]
R : Type u_1
inst✝ : Semiring R
a : ℕ
s : Finset ℕ
as : ¬a ∈ s
hf : ∀ (f : R[X]), Polynomial.support f = s → (↑toLaurent f).support = Finset.map Nat.castEmbedding s
f : R[X]
fs : Polynomial.support f = insert a s
this : (↑toLaurent (Polynomial.erase a f)).support = Finset.map Nat.castEmbedding s
⊢ a ∈ Polynomial.support f
[PROOFSTEP]
simp [fs]
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semiring R
a : ℕ
s : Finset ℕ
as : ¬a ∈ s
hf : ∀ (f : R[X]), Polynomial.support f = s → (↑toLaurent f).support = Finset.map Nat.castEmbedding s
f : R[X]
fs : Polynomial.support f = insert a s
this : (↑toLaurent (Polynomial.erase a f)).support = Finset.map Nat.castEmbedding s
⊢ Disjoint (↑C (coeff f a) * T ↑a).support (↑toLaurent (Polynomial.erase a f)).support
[PROOFSTEP]
rw [this]
[GOAL]
case refine'_2
R : Type u_1
inst✝ : Semiring R
a : ℕ
s : Finset ℕ
as : ¬a ∈ s
hf : ∀ (f : R[X]), Polynomial.support f = s → (↑toLaurent f).support = Finset.map Nat.castEmbedding s
f : R[X]
fs : Polynomial.support f = insert a s
this : (↑toLaurent (Polynomial.erase a f)).support = Finset.map Nat.castEmbedding s
⊢ Disjoint (↑C (coeff f a) * T ↑a).support (Finset.map Nat.castEmbedding s)
[PROOFSTEP]
exact Disjoint.mono_left (support_C_mul_T _ _) (by simpa)
[GOAL]
R : Type u_1
inst✝ : Semiring R
a : ℕ
s : Finset ℕ
as : ¬a ∈ s
hf : ∀ (f : R[X]), Polynomial.support f = s → (↑toLaurent f).support = Finset.map Nat.castEmbedding s
f : R[X]
fs : Polynomial.support f = insert a s
this : (↑toLaurent (Polynomial.erase a f)).support = Finset.map Nat.castEmbedding s
⊢ Disjoint {↑a} (Finset.map Nat.castEmbedding s)
[PROOFSTEP]
simpa
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
⊢ degree f = ⊥ ↔ f = 0
[PROOFSTEP]
refine' ⟨fun h => _, fun h => by rw [h, degree_zero]⟩
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
h : f = 0
⊢ degree f = ⊥
[PROOFSTEP]
rw [h, degree_zero]
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
h : degree f = ⊥
⊢ f = 0
[PROOFSTEP]
rw [degree, Finset.max_eq_sup_withBot] at h 
[GOAL]
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
h : Finset.sup f.support WithBot.some = ⊥
⊢ f = 0
[PROOFSTEP]
ext n
[GOAL]
case h
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
h : Finset.sup f.support WithBot.some = ⊥
n : ℤ
⊢ ↑f n = ↑0 n
[PROOFSTEP]
refine' not_not.mp fun f0 => _
[GOAL]
case h
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
h : Finset.sup f.support WithBot.some = ⊥
n : ℤ
f0 : ¬↑f n = ↑0 n
⊢ False
[PROOFSTEP]
simp_rw [Finset.sup_eq_bot_iff, Finsupp.mem_support_iff, Ne.def, WithBot.coe_ne_bot] at h 
[GOAL]
case h
R : Type u_1
inst✝ : Semiring R
f : R[T;T⁻¹]
n : ℤ
f0 : ¬↑f n = ↑0 n
h : ∀ (s : ℤ), ¬↑f s = 0 → False
⊢ False
[PROOFSTEP]
exact h n f0
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
⊢ degree (↑C a * T n) = ↑n
[PROOFSTEP]
rw [degree]
  -- Porting note: was `convert Finset.max_singleton`
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
⊢ Finset.max (↑C a * T n).support = ↑n
[PROOFSTEP]
have : Finsupp.support (C a * T n) = { n } :=
  by
  refine' support_eq_singleton.mpr _
  rw [← single_eq_C_mul_T]
  simp only [single_eq_same, a0, Ne.def, not_false_iff, eq_self_iff_true, and_self_iff]
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
⊢ (↑C a * T n).support = {n}
[PROOFSTEP]
refine' support_eq_singleton.mpr _
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
⊢ ↑(↑C a * T n) n ≠ 0 ∧ ↑C a * T n = Finsupp.single n (↑(↑C a * T n) n)
[PROOFSTEP]
rw [← single_eq_C_mul_T]
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
⊢ ↑(Finsupp.single n a) n ≠ 0 ∧ Finsupp.single n a = Finsupp.single n (↑(Finsupp.single n a) n)
[PROOFSTEP]
simp only [single_eq_same, a0, Ne.def, not_false_iff, eq_self_iff_true, and_self_iff]
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
this : (↑C a * T n).support = {n}
⊢ Finset.max (↑C a * T n).support = ↑n
[PROOFSTEP]
rw [this]
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a ≠ 0
this : (↑C a * T n).support = {n}
⊢ Finset.max {n} = ↑n
[PROOFSTEP]
exact Finset.max_singleton
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
⊢ degree (↑C a * T n) = if a = 0 then ⊥ else ↑n
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
h : a = 0
⊢ degree (↑C a * T n) = ⊥
[PROOFSTEP]
simp only [h, map_zero, zero_mul, degree_zero, degree_C_mul_T, Ne.def, not_false_iff]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
h : ¬a = 0
⊢ degree (↑C a * T n) = ↑n
[PROOFSTEP]
simp only [h, map_zero, zero_mul, degree_zero, degree_C_mul_T, Ne.def, not_false_iff]
[GOAL]
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℤ
⊢ degree (T n) = ↑n
[PROOFSTEP]
rw [← one_mul (T n), ← map_one C]
[GOAL]
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
n : ℤ
⊢ degree (↑C 1 * T n) = ↑n
[PROOFSTEP]
exact degree_C_mul_T n 1 (one_ne_zero : (1 : R) ≠ 0)
[GOAL]
R : Type u_1
inst✝ : Semiring R
a : R
a0 : a ≠ 0
⊢ degree (↑C a) = 0
[PROOFSTEP]
rw [← mul_one (C a), ← T_zero]
[GOAL]
R : Type u_1
inst✝ : Semiring R
a : R
a0 : a ≠ 0
⊢ degree (↑C a * T 0) = 0
[PROOFSTEP]
exact degree_C_mul_T 0 a a0
[GOAL]
R : Type u_1
inst✝ : Semiring R
a : R
⊢ degree (↑C a) = if a = 0 then ⊥ else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
a : R
h : a = 0
⊢ degree (↑C a) = ⊥
[PROOFSTEP]
simp only [h, map_zero, degree_zero, degree_C, Ne.def, not_false_iff]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
a : R
h : ¬a = 0
⊢ degree (↑C a) = 0
[PROOFSTEP]
simp only [h, map_zero, degree_zero, degree_C, Ne.def, not_false_iff]
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
⊢ degree (↑C a * T n) ≤ ↑n
[PROOFSTEP]
by_cases a0 : a = 0
[GOAL]
case pos
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : a = 0
⊢ degree (↑C a * T n) ≤ ↑n
[PROOFSTEP]
simp only [a0, map_zero, zero_mul, degree_zero, bot_le]
[GOAL]
case neg
R : Type u_1
inst✝ : Semiring R
n : ℤ
a : R
a0 : ¬a = 0
⊢ degree (↑C a * T n) ≤ ↑n
[PROOFSTEP]
exact (degree_C_mul_T n a a0).le
[GOAL]
R : Type u_1
inst✝ : Semiring R
n : ℤ
⊢ degree (T n) = degree (↑C 1 * T n)
[PROOFSTEP]
rw [map_one, one_mul]
[GOAL]
R : Type u_1
inst✝ : Semiring R
a : R
⊢ degree (↑C a) = degree (↑C a * T 0)
[PROOFSTEP]
rw [T_zero, mul_one]
[GOAL]
R✝ : Type u_1
inst✝¹ : Semiring R✝
R : Type u_2
inst✝ : Semiring R
x y : R[X]
z : R[T;T⁻¹]
⊢ (x • y) • z = x • y • z
[PROOFSTEP]
simp only [(· • ·), SMul.smul, SMul.comp.smul, map_mul, mul_assoc]
[GOAL]
R✝ : Type u_1
inst✝¹ : CommSemiring R✝
R : Type u_2
inst✝ : CommSemiring R
src✝ : R[X] →+* R[T;T⁻¹] := toLaurent
f : R[X]
l : (fun x => R[T;T⁻¹]) f
⊢ ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : R[X]), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        f *
      l =
    l *
      ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : R[X]), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        f
[PROOFSTEP]
simp [mul_comm]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
t : { x // x ∈ Submonoid.closure {X} }
⊢ IsUnit (↑(algebraMap R[X] R[T;T⁻¹]) ↑t)
[PROOFSTEP]
cases' t with t ht
[GOAL]
case mk
R : Type u_1
inst✝ : CommSemiring R
t : R[X]
ht : t ∈ Submonoid.closure {X}
⊢ IsUnit (↑(algebraMap R[X] R[T;T⁻¹]) ↑{ val := t, property := ht })
[PROOFSTEP]
rcases Submonoid.mem_closure_singleton.mp ht with ⟨n, rfl⟩
[GOAL]
case mk.intro
R : Type u_1
inst✝ : CommSemiring R
n : ℕ
ht : X ^ n ∈ Submonoid.closure {X}
⊢ IsUnit (↑(algebraMap R[X] R[T;T⁻¹]) ↑{ val := X ^ n, property := ht })
[PROOFSTEP]
simp only [isUnit_T n, algebraMap_eq_toLaurent, Polynomial.toLaurent_X_pow]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
f : R[T;T⁻¹]
⊢ ∃ x, f * ↑(algebraMap R[X] R[T;T⁻¹]) ↑x.snd = ↑(algebraMap R[X] R[T;T⁻¹]) x.fst
[PROOFSTEP]
induction' f using LaurentPolynomial.induction_on_mul_T with f n
[GOAL]
case Qf
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
n : ℕ
⊢ ∃ x, ↑toLaurent f * T (-↑n) * ↑(algebraMap R[X] R[T;T⁻¹]) ↑x.snd = ↑(algebraMap R[X] R[T;T⁻¹]) x.fst
[PROOFSTEP]
have := (Submonoid.closure ({ X } : Set R[X])).pow_mem Submonoid.mem_closure_singleton_self n
[GOAL]
case Qf
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
n : ℕ
this : X ^ n ∈ Submonoid.closure {X}
⊢ ∃ x, ↑toLaurent f * T (-↑n) * ↑(algebraMap R[X] R[T;T⁻¹]) ↑x.snd = ↑(algebraMap R[X] R[T;T⁻¹]) x.fst
[PROOFSTEP]
refine' ⟨(f, ⟨_, this⟩), _⟩
[GOAL]
case Qf
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
n : ℕ
this : X ^ n ∈ Submonoid.closure {X}
⊢ ↑toLaurent f * T (-↑n) * ↑(algebraMap R[X] R[T;T⁻¹]) ↑(f, { val := X ^ n, property := this }).snd =
    ↑(algebraMap R[X] R[T;T⁻¹]) (f, { val := X ^ n, property := this }).fst
[PROOFSTEP]
simp only [algebraMap_eq_toLaurent, Polynomial.toLaurent_X_pow, mul_T_assoc, add_left_neg, T_zero, mul_one]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
f g : R[X]
⊢ ↑(algebraMap R[X] R[T;T⁻¹]) f = ↑(algebraMap R[X] R[T;T⁻¹]) g ↔ ∃ c, ↑c * f = ↑c * g
[PROOFSTEP]
rw [algebraMap_eq_toLaurent, algebraMap_eq_toLaurent, Polynomial.toLaurent_inj]
[GOAL]
R : Type u_1
inst✝ : CommSemiring R
f g : R[X]
⊢ f = g ↔ ∃ c, ↑c * f = ↑c * g
[PROOFSTEP]
refine' ⟨_, _⟩
[GOAL]
case refine'_1
R : Type u_1
inst✝ : CommSemiring R
f g : R[X]
⊢ f = g → ∃ c, ↑c * f = ↑c * g
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_1
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
⊢ ∃ c, ↑c * f = ↑c * f
[PROOFSTEP]
exact ⟨1, rfl⟩
[GOAL]
case refine'_2
R : Type u_1
inst✝ : CommSemiring R
f g : R[X]
⊢ (∃ c, ↑c * f = ↑c * g) → f = g
[PROOFSTEP]
rintro ⟨⟨h, hX⟩, h⟩
[GOAL]
case refine'_2.intro.mk
R : Type u_1
inst✝ : CommSemiring R
f g h✝ : R[X]
hX : h✝ ∈ Submonoid.closure {X}
h : ↑{ val := h✝, property := hX } * f = ↑{ val := h✝, property := hX } * g
⊢ f = g
[PROOFSTEP]
rcases Submonoid.mem_closure_singleton.mp hX with ⟨n, rfl⟩
[GOAL]
case refine'_2.intro.mk.intro
R : Type u_1
inst✝ : CommSemiring R
f g : R[X]
n : ℕ
hX : X ^ n ∈ Submonoid.closure {X}
h : ↑{ val := X ^ n, property := hX } * f = ↑{ val := X ^ n, property := hX } * g
⊢ f = g
[PROOFSTEP]
exact (isRegular_X_pow n).left h
