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 })
R : Type u_1
inst✝ : CommSemiring R
t : { x // x ∈ Submonoid.closure {X} }
⊢ IsUnit (↑(algebraMap R[X] R[T;T⁻¹]) ↑t)
cases' t with t ht
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 })
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 })
rcases Submonoid.mem_closure_singleton.mp ht with ⟨n, rfl⟩
no goals
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 })
simp only [isUnit_T n, algebraMap_eq_toLaurent, Polynomial.toLaurent_X_pow]
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
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
induction' f using LaurentPolynomial.induction_on_mul_T with f n
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
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
have := (Submonoid.closure ({X} : Set R[X])).pow_mem Submonoid.mem_closure_singleton_self n
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
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
refine' ⟨(f, ⟨_, this⟩), _⟩
no goals
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
simp only [algebraMap_eq_toLaurent, Polynomial.toLaurent_X_pow, mul_T_assoc,
  add_left_neg, T_zero, mul_one]
R : Type u_1
inst✝ : CommSemiring R
f g : R[X]
⊢ f = g ↔ ∃ c, ↑c * f = ↑c * g
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
rw [algebraMap_eq_toLaurent, algebraMap_eq_toLaurent, Polynomial.toLaurent_inj]
case refine'_1
R : Type u_1
inst✝ : CommSemiring R
f g : R[X]
⊢ f = g → ∃ c, ↑c * f = ↑c * g

case refine'_2
R : Type u_1
inst✝ : CommSemiring R
f g : R[X]
⊢ (∃ c, ↑c * f = ↑c * g) → f = g
R : Type u_1
inst✝ : CommSemiring R
f g : R[X]
⊢ f = g ↔ ∃ c, ↑c * f = ↑c * g
refine' ⟨_, _⟩
case refine'_1
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
⊢ ∃ c, ↑c * f = ↑c * f
case refine'_1
R : Type u_1
inst✝ : CommSemiring R
f g : R[X]
⊢ f = g → ∃ c, ↑c * f = ↑c * g
rintro rfl
no goals
case refine'_1
R : Type u_1
inst✝ : CommSemiring R
f : R[X]
⊢ ∃ c, ↑c * f = ↑c * f
exact ⟨1, rfl⟩
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
case refine'_2
R : Type u_1
inst✝ : CommSemiring R
f g : R[X]
⊢ (∃ c, ↑c * f = ↑c * g) → f = g
rintro ⟨⟨h, hX⟩, h⟩
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
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
rcases Submonoid.mem_closure_singleton.mp hX with ⟨n, rfl⟩
no goals
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
exact mul_X_pow_injective n h