-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem toLaurent_support (f : R[X]) : f.toLaurent.support = f.support.map Nat.castEmbedding

Proof state:
R : Type u_1
inst✝ : Semiring R
s : Finset ℕ
⊢ ∀ (f : R[X]), f.support = s → (toLaurent f).support = Finset.map Nat.castEmbedding s

Tactic:
refine Finset.induction_on s ?_ ?_ <;> clear s

Result:
case refine_1
R : Type u_1
inst✝ : Semiring R
⊢ ∀ (f : R[X]), f.support = ∅ → (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]), f.support = s → (toLaurent f).support = Finset.map Nat.castEmbedding s) →
        ∀ (f : R[X]), f.support = insert a s → (toLaurent f).support = Finset.map Nat.castEmbedding (insert a s)

Proof state:
case refine_2.e_a
R : Type u_1
inst✝ : Semiring R
a : ℕ
s : Finset ℕ
as : a ∉ s
hf : ∀ (f : R[X]), f.support = s → (toLaurent f).support = Finset.map Nat.castEmbedding s
f : R[X]
fs : f.support = insert a s
this : (toLaurent (Polynomial.erase a f)).support = Finset.map Nat.castEmbedding s
⊢ (C (f.coeff a) * T ↑a).support = {Nat.castEmbedding a}

Tactic:
exact support_C_mul_T_of_ne_zero (Polynomial.mem_support_iff.mp (by simp [fs])) _

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
s : Finset ℕ
hd : f.support = s
⊢ (toLaurent f).support = Finset.map Nat.castEmbedding s

Tactic:
revert f

Result:
R : Type u_1
inst✝ : Semiring R
s : Finset ℕ
⊢ ∀ (f : R[X]), f.support = s → (toLaurent f).support = Finset.map Nat.castEmbedding s

Proof state:
case refine_1
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : f.support = ∅
⊢ (toLaurent f).support = Finset.map Nat.castEmbedding ∅

Tactic:
rw [Finset.map_empty, Finsupp.support_eq_empty, toLaurent_eq_zero]

Result:
case refine_1
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : f.support = ∅
⊢ f = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
a : ℕ
s : Finset ℕ
as : a ∉ s
hf : ∀ (f : R[X]), f.support = s → (toLaurent f).support = Finset.map Nat.castEmbedding s
f : R[X]
fs : f.support = insert a s
⊢ (toLaurent (Polynomial.erase a f)).support = Finset.map Nat.castEmbedding s

Tactic:
refine hf (f.erase a) ?_

Result:
R : Type u_1
inst✝ : Semiring R
a : ℕ
s : Finset ℕ
as : a ∉ s
hf : ∀ (f : R[X]), f.support = s → (toLaurent f).support = Finset.map Nat.castEmbedding s
f : R[X]
fs : f.support = insert a s
⊢ (Polynomial.erase a f).support = s

Proof state:
case refine_2
R : Type u_1
inst✝ : Semiring R
a : ℕ
s : Finset ℕ
as : a ∉ s
hf : ∀ (f : R[X]), f.support = s → (toLaurent f).support = Finset.map Nat.castEmbedding s
f : R[X]
fs : f.support = insert a s
this : (toLaurent (Polynomial.erase a f)).support = Finset.map Nat.castEmbedding s
⊢ Disjoint (C (f.coeff a) * T ↑a).support (toLaurent (Polynomial.erase a f)).support

Tactic:
rw [this]

Result:
case refine_2
R : Type u_1
inst✝ : Semiring R
a : ℕ
s : Finset ℕ
as : a ∉ s
hf : ∀ (f : R[X]), f.support = s → (toLaurent f).support = Finset.map Nat.castEmbedding s
f : R[X]
fs : f.support = insert a s
this : (toLaurent (Polynomial.erase a f)).support = Finset.map Nat.castEmbedding s
⊢ Disjoint (C (f.coeff a) * T ↑a).support (Finset.map Nat.castEmbedding s)

Proof state:
case refine_2
R : Type u_1
inst✝ : Semiring R
a : ℕ
s : Finset ℕ
as : a ∉ s
hf : ∀ (f : R[X]), f.support = s → (toLaurent f).support = Finset.map Nat.castEmbedding s
f : R[X]
fs : f.support = insert a s
⊢ (toLaurent f).support = Finset.map Nat.castEmbedding (insert a s)

Tactic:
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]

Result:
case refine_2
R : Type u_1
inst✝ : Semiring R
a : ℕ
s : Finset ℕ
as : a ∉ s
hf : ∀ (f : R[X]), f.support = s → (toLaurent f).support = Finset.map Nat.castEmbedding s
f : R[X]
fs : f.support = 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)

Proof state:
R : Type u_1
inst✝ : Semiring R
a : ℕ
s : Finset ℕ
as : a ∉ s
hf : ∀ (f : R[X]), f.support = s → (toLaurent f).support = Finset.map Nat.castEmbedding s
f : R[X]
fs : f.support = insert a s
⊢ (Polynomial.erase a f).support = s

Tactic:
simp only [fs, Finset.erase_eq_of_not_mem as, Polynomial.support_erase,
  Finset.erase_insert_eq_erase]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
a : ℕ
s : Finset ℕ
as : a ∉ s
hf : ∀ (f : R[X]), f.support = s → (toLaurent f).support = Finset.map Nat.castEmbedding s
f : R[X]
fs : f.support = insert a s
this : (toLaurent (Polynomial.erase a f)).support = Finset.map Nat.castEmbedding s
⊢ a ∈ f.support

Tactic:
simp [fs]

Result:
no goals

Proof state:
case refine_1
R : Type u_1
inst✝ : Semiring R
f : R[X]
hf : f.support = ∅
⊢ f = 0

Tactic:
exact Polynomial.support_eq_empty.mp hf

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (toLaurent f).support = Finset.map Nat.castEmbedding f.support

Tactic:
generalize hd : f.support = s

Result:
R : Type u_1
inst✝ : Semiring R
f : R[X]
s : Finset ℕ
hd : f.support = s
⊢ (toLaurent f).support = Finset.map Nat.castEmbedding s

Proof state:
case refine_2
R : Type u_1
inst✝ : Semiring R
⊢ ∀ ⦃a : ℕ⦄ {s : Finset ℕ},
    a ∉ s →
      (∀ (f : R[X]), f.support = s → (toLaurent f).support = Finset.map Nat.castEmbedding s) →
        ∀ (f : R[X]), f.support = insert a s → (toLaurent f).support = Finset.map Nat.castEmbedding (insert a s)

Tactic:
intro a s as hf f fs

Result:
case refine_2
R : Type u_1
inst✝ : Semiring R
a : ℕ
s : Finset ℕ
as : a ∉ s
hf : ∀ (f : R[X]), f.support = s → (toLaurent f).support = Finset.map Nat.castEmbedding s
f : R[X]
fs : f.support = insert a s
⊢ (toLaurent f).support = Finset.map Nat.castEmbedding (insert a s)

Proof state:
R : Type u_1
inst✝ : Semiring R
a : ℕ
s : Finset ℕ
as : a ∉ s
hf : ∀ (f : R[X]), f.support = s → (toLaurent f).support = Finset.map Nat.castEmbedding s
f : R[X]
fs : f.support = insert a s
this : (toLaurent (Polynomial.erase a f)).support = Finset.map Nat.castEmbedding s
⊢ Disjoint {↑a} (Finset.map Nat.castEmbedding s)

Tactic:
simpa

Result:
no goals

Proof state:
case refine_2
R : Type u_1
inst✝ : Semiring R
a : ℕ
s : Finset ℕ
as : a ∉ s
hf : ∀ (f : R[X]), f.support = s → (toLaurent f).support = Finset.map Nat.castEmbedding s
f : R[X]
fs : f.support = insert a s
this : (toLaurent (Polynomial.erase a f)).support = Finset.map Nat.castEmbedding s
⊢ (C (f.coeff a) * T ↑a).support ∪ (toLaurent (Polynomial.erase a f)).support =
    {Nat.castEmbedding a} ∪ (toLaurent (Polynomial.erase a f)).support

Tactic:
congr

Result:
case refine_2.e_a
R : Type u_1
inst✝ : Semiring R
a : ℕ
s : Finset ℕ
as : a ∉ s
hf : ∀ (f : R[X]), f.support = s → (toLaurent f).support = Finset.map Nat.castEmbedding s
f : R[X]
fs : f.support = insert a s
this : (toLaurent (Polynomial.erase a f)).support = Finset.map Nat.castEmbedding s
⊢ (C (f.coeff a) * T ↑a).support = {Nat.castEmbedding a}

Proof state:
case refine_2
R : Type u_1
inst✝ : Semiring R
a : ℕ
s : Finset ℕ
as : a ∉ s
hf : ∀ (f : R[X]), f.support = s → (toLaurent f).support = Finset.map Nat.castEmbedding s
f : R[X]
fs : f.support = insert a s
this : (toLaurent (Polynomial.erase a f)).support = Finset.map Nat.castEmbedding s
⊢ Disjoint (C (f.coeff a) * T ↑a).support (Finset.map Nat.castEmbedding s)

Tactic:
exact Disjoint.mono_left (support_C_mul_T _ _) (by simpa)

Result:
no goals