-- Mathlib/RingTheory/LaurentSeries.lean
theorem powerSeries_ext_subring :
    Subring.map (LaurentSeriesRingEquiv K).toRingHom (powerSeries_as_subring K) =
      ((idealX K).adicCompletionIntegers (RatFunc K)).toSubring

Proof state:
K : Type u_2
inst✝ : Field K
⊢ Subring.map (LaurentSeriesRingEquiv K).toRingHom (powerSeries_as_subring K) =
    (adicCompletionIntegers (RatFunc K) (idealX K)).toSubring

Tactic:
ext x

Result:
case h
K : Type u_2
inst✝ : Field K
x : RatFuncAdicCompl K
⊢ x ∈ Subring.map (LaurentSeriesRingEquiv K).toRingHom (powerSeries_as_subring K) ↔
    x ∈ (adicCompletionIntegers (RatFunc K) (idealX K)).toSubring

Proof state:
case h
K : Type u_2
inst✝ : Field K
x : RatFuncAdicCompl K
⊢ x ∈ Subring.map (LaurentSeriesRingEquiv K).toRingHom (powerSeries_as_subring K) ↔
    x ∈ (adicCompletionIntegers (RatFunc K) (idealX K)).toSubring

Tactic:
refine ⟨fun ⟨f, ⟨F, _, coe_F⟩, hF⟩ ↦ ?_, fun H ↦ ?_⟩

Result:
case h.refine_1
K : Type u_2
inst✝ : Field K
x : RatFuncAdicCompl K
x✝ : x ∈ Subring.map (LaurentSeriesRingEquiv K).toRingHom (powerSeries_as_subring K)
f : K⸨X⸩
F : K⟦X⟧
left✝ : F ∈ ⊤.carrier
coe_F : (ofPowerSeries ℤ K) F = f
hF : (LaurentSeriesRingEquiv K).toRingHom f = x
⊢ x ∈ (adicCompletionIntegers (RatFunc K) (idealX K)).toSubring

case h.refine_2
K : Type u_2
inst✝ : Field K
x : RatFuncAdicCompl K
H : x ∈ (adicCompletionIntegers (RatFunc K) (idealX K)).toSubring
⊢ x ∈ Subring.map (LaurentSeriesRingEquiv K).toRingHom (powerSeries_as_subring K)

Proof state:
case h.refine_2
K : Type u_2
inst✝ : Field K
x : RatFuncAdicCompl K
H : x ∈ (adicCompletionIntegers (RatFunc K) (idealX K)).toSubring
⊢ x ∈ Subring.map (LaurentSeriesRingEquiv K).toRingHom (powerSeries_as_subring K)

Tactic:
obtain ⟨F, hF⟩ := exists_powerSeries_of_memIntegers K H

Result:
case h.refine_2.intro
K : Type u_2
inst✝ : Field K
x : RatFuncAdicCompl K
H : x ∈ (adicCompletionIntegers (RatFunc K) (idealX K)).toSubring
F : K⟦X⟧
hF : (LaurentSeriesRingEquiv K) ((ofPowerSeries ℤ K) F) = x
⊢ x ∈ Subring.map (LaurentSeriesRingEquiv K).toRingHom (powerSeries_as_subring K)

Proof state:
case h.refine_1
K : Type u_2
inst✝ : Field K
x : RatFuncAdicCompl K
x✝ : x ∈ Subring.map (LaurentSeriesRingEquiv K).toRingHom (powerSeries_as_subring K)
f : K⸨X⸩
F : K⟦X⟧
left✝ : F ∈ ⊤.carrier
coe_F : (ofPowerSeries ℤ K) F = f
hF : (LaurentSeriesRingEquiv K).toRingHom f = x
⊢ x ∈ (adicCompletionIntegers (RatFunc K) (idealX K)).toSubring

Tactic:
simp only [ValuationSubring.mem_toSubring, ← hF, ← coe_F]

Result:
case h.refine_1
K : Type u_2
inst✝ : Field K
x : RatFuncAdicCompl K
x✝ : x ∈ Subring.map (LaurentSeriesRingEquiv K).toRingHom (powerSeries_as_subring K)
f : K⸨X⸩
F : K⟦X⟧
left✝ : F ∈ ⊤.carrier
coe_F : (ofPowerSeries ℤ K) F = f
hF : (LaurentSeriesRingEquiv K).toRingHom f = x
⊢ (LaurentSeriesRingEquiv K).toRingHom ((ofPowerSeries ℤ K) F) ∈ adicCompletionIntegers (RatFunc K) (idealX K)

Proof state:
case h.refine_2.intro
K : Type u_2
inst✝ : Field K
x : RatFuncAdicCompl K
H : x ∈ (adicCompletionIntegers (RatFunc K) (idealX K)).toSubring
F : K⟦X⟧
hF : (LaurentSeriesRingEquiv K) ((ofPowerSeries ℤ K) F) = x
⊢ ∃ x_1, (∃ x ∈ ⊤, (ofPowerSeries ℤ K) x = x_1) ∧ (LaurentSeriesRingEquiv K).toRingHom x_1 = x

Tactic:
exact ⟨F, ⟨F, trivial, rfl⟩, hF⟩

Result:
no goals

Proof state:
case h.refine_2.intro
K : Type u_2
inst✝ : Field K
x : RatFuncAdicCompl K
H : x ∈ (adicCompletionIntegers (RatFunc K) (idealX K)).toSubring
F : K⟦X⟧
hF : (LaurentSeriesRingEquiv K) ((ofPowerSeries ℤ K) F) = x
⊢ x ∈ Subring.map (LaurentSeriesRingEquiv K).toRingHom (powerSeries_as_subring K)

Tactic:
simp only [Equiv.toFun_as_coe, UniformEquiv.coe_toEquiv, exists_exists_eq_and,
  UniformEquiv.coe_symm_toEquiv, Subring.mem_map, Equiv.invFun_as_coe]

Result:
case h.refine_2.intro
K : Type u_2
inst✝ : Field K
x : RatFuncAdicCompl K
H : x ∈ (adicCompletionIntegers (RatFunc K) (idealX K)).toSubring
F : K⟦X⟧
hF : (LaurentSeriesRingEquiv K) ((ofPowerSeries ℤ K) F) = x
⊢ ∃ x_1, (∃ x ∈ ⊤, (ofPowerSeries ℤ K) x = x_1) ∧ (LaurentSeriesRingEquiv K).toRingHom x_1 = x

Proof state:
case h.refine_1
K : Type u_2
inst✝ : Field K
x : RatFuncAdicCompl K
x✝ : x ∈ Subring.map (LaurentSeriesRingEquiv K).toRingHom (powerSeries_as_subring K)
f : K⸨X⸩
F : K⟦X⟧
left✝ : F ∈ ⊤.carrier
coe_F : (ofPowerSeries ℤ K) F = f
hF : (LaurentSeriesRingEquiv K).toRingHom f = x
⊢ (LaurentSeriesRingEquiv K).toRingHom ((ofPowerSeries ℤ K) F) ∈ adicCompletionIntegers (RatFunc K) (idealX K)

Tactic:
apply mem_integers_of_powerSeries

Result:
no goals