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
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (↑toLaurent f).support = Finset.map Nat.castEmbedding (Polynomial.support f)
generalize hd : f.support = s
R : Type u_1
inst✝ : Semiring R
s : Finset ℕ
⊢ ∀ (f : R[X]), Polynomial.support f = s → (↑toLaurent f).support = Finset.map Nat.castEmbedding s
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
revert f
case refine'_1
R : Type u_1
inst✝ : Semiring R
⊢ ∀ (f : R[X]), Polynomial.support f = ∅ → (↑toLaurent f).support = Finset.map Nat.castEmbedding ∅

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)
R : Type u_1
inst✝ : Semiring R
s : Finset ℕ
⊢ ∀ (f : R[X]), Polynomial.support f = s → (↑toLaurent f).support = Finset.map Nat.castEmbedding s
refine' Finset.induction_on s _ _ <;> clear s
no goals
case refine'_1
R : Type u_1
inst✝ : Semiring R
⊢ ∀ (f : R[X]), Polynomial.support f = ∅ → (↑toLaurent f).support = Finset.map Nat.castEmbedding ∅
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]
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)
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)
intro a s as hf f fs
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)
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)
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]
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

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
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)
rw [← monomial_add_erase f a, Finset.map_insert, ← this, map_add, Polynomial.toLaurent_C_mul_T,
  support_add_eq, Finset.insert_eq]
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
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
refine' hf (f.erase a) _
no goals
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
simp only [fs, Finset.erase_eq_of_not_mem as, Polynomial.support_erase,
  Finset.erase_insert_eq_erase]
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}
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
congr
no goals
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}
exact support_C_mul_T_of_ne_zero (Polynomial.mem_support_iff.mp (by simp [fs])) _
no goals
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
simp [fs]
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)
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
rw [this]
no goals
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)
exact Disjoint.mono_left (support_C_mul_T _ _) (by simpa)
no goals
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)
simpa