-- Mathlib/RingTheory/LaurentSeries.lean
theorem val_le_one_iff_eq_coe (f : K⸨X⸩) : Valued.v f ≤ (1 : ℤₘ₀) ↔
    ∃ F : K⟦X⟧, F = f

Proof state:
case refine_1.coeff.h.negSucc
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
n : ℕ
⊢ ((ofPowerSeries ℤ K) (PowerSeries.mk fun n => f.coeff ↑n)).coeff (Int.negSucc n) = f.coeff (Int.negSucc n)

case refine_2
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
⊢ (∃ F, (ofPowerSeries ℤ K) F = f) → ∀ n < 0, f.coeff n = 0

Tactic:
on_goal 1 => simp only [h (Int.negSucc n) (Int.negSucc_lt_zero n)]

Result:
case refine_1.coeff.h.negSucc
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
n : ℕ
⊢ ((ofPowerSeries ℤ K) (PowerSeries.mk fun n => f.coeff ↑n)).coeff (Int.negSucc n) = 0

case refine_2
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
⊢ (∃ F, (ofPowerSeries ℤ K) F = f) → ∀ n < 0, f.coeff n = 0

Proof state:
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
⊢ (∀ n < 0, f.coeff n = 0) ↔ ∃ F, (ofPowerSeries ℤ K) F = f

Tactic:
refine ⟨fun h => ⟨PowerSeries.mk fun n => f.coeff n, ?_⟩, ?_⟩

Result:
case refine_1
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
⊢ (ofPowerSeries ℤ K) (PowerSeries.mk fun n => f.coeff ↑n) = f

case refine_2
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
⊢ (∃ F, (ofPowerSeries ℤ K) F = f) → ∀ n < 0, f.coeff n = 0

Proof state:
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
⊢ Valued.v f ≤ 1 ↔ ∃ F, (ofPowerSeries ℤ K) F = f

Tactic:
rw [← WithZero.coe_one, ← ofAdd_zero, ← neg_zero, valuation_le_iff_coeff_lt_eq_zero]

Result:
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
⊢ (∀ n < 0, f.coeff n = 0) ↔ ∃ F, (ofPowerSeries ℤ K) F = f

Proof state:
case refine_1.coeff.h.ofNat
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
a✝ : ℕ
⊢ ((ofPowerSeries ℤ K) (PowerSeries.mk fun n => f.coeff ↑n)).coeff (Int.ofNat a✝) = f.coeff (Int.ofNat a✝)

Tactic:
simp only [Int.ofNat_eq_coe, coeff_coe_powerSeries, coeff_mk]

Result:
no goals

Proof state:
case refine_2.intro.hb
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
n✝ : ℤ
a✝ : n✝ < 0
x✝ : ℕ
⊢ ¬↑x✝ = n✝

Tactic:
omega

Result:
no goals

Proof state:
case refine_1
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
⊢ (ofPowerSeries ℤ K) (PowerSeries.mk fun n => f.coeff ↑n) = f

case refine_2
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
⊢ (∃ F, (ofPowerSeries ℤ K) F = f) → ∀ n < 0, f.coeff n = 0

Tactic:
on_goal 1 => ext (_ | n)

Result:
case refine_1.coeff.h.ofNat
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
a✝ : ℕ
⊢ ((ofPowerSeries ℤ K) (PowerSeries.mk fun n => f.coeff ↑n)).coeff (Int.ofNat a✝) = f.coeff (Int.ofNat a✝)

case refine_1.coeff.h.negSucc
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
n : ℕ
⊢ ((ofPowerSeries ℤ K) (PowerSeries.mk fun n => f.coeff ↑n)).coeff (Int.negSucc n) = f.coeff (Int.negSucc n)

case refine_2
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
⊢ (∃ F, (ofPowerSeries ℤ K) F = f) → ∀ n < 0, f.coeff n = 0

Proof state:
case refine_1.coeff.h.negSucc.hb
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
n x✝ : ℕ
⊢ ¬False

Tactic:
simp only [not_false_eq_true]

Result:
no goals

Proof state:
case refine_1.coeff.h.negSucc
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
n : ℕ
⊢ ((ofPowerSeries ℤ K) (PowerSeries.mk fun n => f.coeff ↑n)).coeff (Int.negSucc n) = f.coeff (Int.negSucc n)

Tactic:
simp only [h (Int.negSucc n) (Int.negSucc_lt_zero n)]

Result:
case refine_1.coeff.h.negSucc
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
n : ℕ
⊢ ((ofPowerSeries ℤ K) (PowerSeries.mk fun n => f.coeff ↑n)).coeff (Int.negSucc n) = 0

Proof state:
case refine_2.intro.hb
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
n✝ : ℤ
a✝ : n✝ < 0
⊢ n✝ ∉ Set.range ⇑{ toFun := ⇑(Nat.castAddMonoidHom ℤ), inj' := ⋯, map_rel_iff' := ⋯ }

Tactic:
simp only [Nat.coe_castAddMonoidHom, RelEmbedding.coe_mk, Function.Embedding.coeFn_mk,
  Set.mem_range, not_exists, Int.negSucc_lt_zero, reduceCtorEq]

Result:
case refine_2.intro.hb
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
n✝ : ℤ
a✝ : n✝ < 0
⊢ ∀ (x : ℕ), ¬↑x = n✝

Proof state:
case refine_2
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
⊢ (∃ F, (ofPowerSeries ℤ K) F = f) → ∀ n < 0, f.coeff n = 0

Tactic:
rintro ⟨F, rfl⟩ _ _

Result:
case refine_2.intro
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
n✝ : ℤ
a✝ : n✝ < 0
⊢ ((ofPowerSeries ℤ K) F).coeff n✝ = 0

Proof state:
case refine_1.coeff.h.negSucc
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
n : ℕ
⊢ ((ofPowerSeries ℤ K) (PowerSeries.mk fun n => f.coeff ↑n)).coeff (Int.negSucc n) = 0

case refine_2.intro
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
n✝ : ℤ
a✝ : n✝ < 0
⊢ ((ofPowerSeries ℤ K) F).coeff n✝ = 0

Tactic:
all_goals
  apply HahnSeries.embDomain_notin_range
  simp only [Nat.coe_castAddMonoidHom, RelEmbedding.coe_mk, Function.Embedding.coeFn_mk,
    Set.mem_range, not_exists, Int.negSucc_lt_zero, reduceCtorEq]
  intro

Result:
case refine_1.coeff.h.negSucc.hb
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
n x✝ : ℕ
⊢ ¬False

case refine_2.intro.hb
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
n✝ : ℤ
a✝ : n✝ < 0
x✝ : ℕ
⊢ ¬↑x✝ = n✝

Proof state:
case refine_2.intro
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
n✝ : ℤ
a✝ : n✝ < 0
⊢ ((ofPowerSeries ℤ K) F).coeff n✝ = 0

Tactic:
apply HahnSeries.embDomain_notin_range

Result:
case refine_2.intro.hb
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
n✝ : ℤ
a✝ : n✝ < 0
⊢ n✝ ∉ Set.range ⇑{ toFun := ⇑(Nat.castAddMonoidHom ℤ), inj' := ⋯, map_rel_iff' := ⋯ }

Proof state:
case refine_2.intro.hb
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
n✝ : ℤ
a✝ : n✝ < 0
⊢ ∀ (x : ℕ), ¬↑x = n✝

Tactic:
intro

Result:
case refine_2.intro.hb
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
n✝ : ℤ
a✝ : n✝ < 0
x✝ : ℕ
⊢ ¬↑x✝ = n✝

Proof state:
case refine_1
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
⊢ (ofPowerSeries ℤ K) (PowerSeries.mk fun n => f.coeff ↑n) = f

Tactic:
ext (_ | n)

Result:
case refine_1.coeff.h.ofNat
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
a✝ : ℕ
⊢ ((ofPowerSeries ℤ K) (PowerSeries.mk fun n => f.coeff ↑n)).coeff (Int.ofNat a✝) = f.coeff (Int.ofNat a✝)

case refine_1.coeff.h.negSucc
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
n : ℕ
⊢ ((ofPowerSeries ℤ K) (PowerSeries.mk fun n => f.coeff ↑n)).coeff (Int.negSucc n) = f.coeff (Int.negSucc n)

Proof state:
case refine_1.coeff.h.negSucc
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
n : ℕ
⊢ ((ofPowerSeries ℤ K) (PowerSeries.mk fun n => f.coeff ↑n)).coeff (Int.negSucc n) = 0

case refine_2
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
⊢ (∃ F, (ofPowerSeries ℤ K) F = f) → ∀ n < 0, f.coeff n = 0

Tactic:
on_goal 2 => rintro ⟨F, rfl⟩ _ _

Result:
case refine_1.coeff.h.negSucc
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
n : ℕ
⊢ ((ofPowerSeries ℤ K) (PowerSeries.mk fun n => f.coeff ↑n)).coeff (Int.negSucc n) = 0

case refine_2.intro
K : Type u_2
inst✝ : Field K
F : K⟦X⟧
n✝ : ℤ
a✝ : n✝ < 0
⊢ ((ofPowerSeries ℤ K) F).coeff n✝ = 0