awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
x : RatFuncAdicCompl K
hx :
  Membership.mem (γ := ValuationSubring (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)))
    (adicCompletionIntegers K⟮X⟯ (idealX K)) x
f : K⸨X⸩ := (ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x
hf : f = (ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x
H_x :
  AbstractCompletion.compare (LaurentSeriesPkg K) ratfuncAdicComplPkg
      ((ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x) =
    x
hx₁ :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (WithZero (Multiplicative ℤ))) :
          (a : adicCompletion K⟮X⟯ (idealX K)) → WithZero (Multiplicative ℤ))
        (AbstractCompletion.compare (LaurentSeriesPkg K) ratfuncAdicComplPkg
          ((ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
⊢ let f : K⸨X⸩ := (ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x;
  f = (ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x

Tactic:
rw [mem_adicCompletionIntegers, ← H_x] at hx

Premises used: IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
x : RatFuncAdicCompl K
hx :
  Membership.mem (γ := ValuationSubring (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)))
    (adicCompletionIntegers K⟮X⟯ (idealX K)) x
f : K⸨X⸩ := (ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x
hf : f = (ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x
H_x :
  AbstractCompletion.compare (LaurentSeriesPkg K) ratfuncAdicComplPkg
      ((ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x) =
    x
hx₁ :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (WithZero (Multiplicative ℤ))) :
          (a : adicCompletion K⟮X⟯ (idealX K)) → WithZero (Multiplicative ℤ))
        (AbstractCompletion.compare (LaurentSeriesPkg K) ratfuncAdicComplPkg
          ((ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
hf₁ :
  let f : K⸨X⸩ := (ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x;
  f = (ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x
⊢ AbstractCompletion.compare (LaurentSeriesPkg K) ratfuncAdicComplPkg
      ((ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x) =
    x

Tactic:
rw [mem_adicCompletionIntegers, ← H_x] at hx

Premises used: IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
x : RatFuncAdicCompl K
hx :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (WithZero (Multiplicative ℤ))) :
          (a : adicCompletion K⟮X⟯ (idealX K)) → WithZero (Multiplicative ℤ))
        (AbstractCompletion.compare (LaurentSeriesPkg K) ratfuncAdicComplPkg
          ((ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
f : K⸨X⸩ := (ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x
hf : f = (ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x
H_x :
  AbstractCompletion.compare (LaurentSeriesPkg K) ratfuncAdicComplPkg
      ((ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x) =
    x
obtain :
  ∀ (F : K⟦X⟧) (hF : ((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F = f),
    ∃ (F : K⟦X⟧),
      (LaurentSeriesRingEquiv K : (a : K⸨X⸩) → RatFuncAdicCompl K)
          (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F) =
        x
⊢ ∃ (F : K⟦X⟧),
    (LaurentSeriesRingEquiv K : (a : K⸨X⸩) → RatFuncAdicCompl K)
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F) =
      x

Tactic:
obtain ⟨F, hF⟩ := (val_le_one_iff_eq_coe K f).mp (valuation_compare _ f ▸ hx)

Premises used: LaurentSeries.val_le_one_iff_eq_coe, Eq.rec, LaurentSeries.valuation_compare, Iff.mp
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
x : RatFuncAdicCompl K
hx :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (WithZero (Multiplicative ℤ))) :
          (a : adicCompletion K⟮X⟯ (idealX K)) → WithZero (Multiplicative ℤ))
        (AbstractCompletion.compare (LaurentSeriesPkg K) ratfuncAdicComplPkg
          ((ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
f : K⸨X⸩ := (ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x
hf : f = (ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x
H_x :
  AbstractCompletion.compare (LaurentSeriesPkg K) ratfuncAdicComplPkg
      ((ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x) =
    x
F : K⟦X⟧
hF : ((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F = f
rw : (LaurentSeriesRingEquiv K : (a : K⸨X⸩) → RatFuncAdicCompl K) f = x
rw₁ :
  (LaurentSeriesRingEquiv K : (a : K⸨X⸩) → RatFuncAdicCompl K)
      ((ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x) =
    x
rw₂ rw₃ : x = x
⊢ (LaurentSeriesRingEquiv K : (a : K⸨X⸩) → RatFuncAdicCompl K)
      (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F) =
    x

Tactic:
rw [hF, hf, RingEquiv.symm_apply_apply]

Premises used: RingEquiv.symm_apply_apply
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
x : RatFuncAdicCompl K
hx :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (WithZero (Multiplicative ℤ))) :
          (a : adicCompletion K⟮X⟯ (idealX K)) → WithZero (Multiplicative ℤ))
        (AbstractCompletion.compare (LaurentSeriesPkg K) ratfuncAdicComplPkg
          ((ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
f : K⸨X⸩ := (ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x
hf : f = (ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x
H_x :
  AbstractCompletion.compare (LaurentSeriesPkg K) ratfuncAdicComplPkg
      ((ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x) =
    x
F : K⟦X⟧
hF : ((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F = f
⊢ ∃ (F : K⟦X⟧),
    (LaurentSeriesRingEquiv K : (a : K⸨X⸩) → RatFuncAdicCompl K)
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F) =
      x

Tactic:
exact ⟨F, by rw [hF, hf, RingEquiv.symm_apply_apply]⟩
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
h :
  ∀ (x : RatFuncAdicCompl K),
    Membership.mem (γ := Subring (RatFuncAdicCompl K))
        (Subring.map (RingEquiv.toRingHom (LaurentSeriesRingEquiv K)) (powerSeries_as_subring K)) x ↔
      Membership.mem (γ := Subring (RatFuncAdicCompl K))
        (ValuationSubring.toSubring (adicCompletionIntegers K⟮X⟯ (idealX K))) x
⊢ Eq (α := Subring (RatFuncAdicCompl K))
    (Subring.map (RingEquiv.toRingHom (LaurentSeriesRingEquiv K)) (powerSeries_as_subring K))
    (ValuationSubring.toSubring (adicCompletionIntegers K⟮X⟯ (idealX K)))

Tactic:
ext x
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
x : RatFuncAdicCompl K
⊢ Membership.mem (γ := Subring (RatFuncAdicCompl K))
      (Subring.map (RingEquiv.toRingHom (LaurentSeriesRingEquiv K)) (powerSeries_as_subring K)) x ↔
    Membership.mem (γ := Subring (RatFuncAdicCompl K))
      (ValuationSubring.toSubring (adicCompletionIntegers K⟮X⟯ (idealX K))) x

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

Premises used: _private.0.LaurentSeries.powerSeries_ext_subring.match_1, Membership.mem, RatFunc, Iff.intro, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers, Polynomial.idealX, ValuationSubring.toSubring
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
x : RatFuncAdicCompl K
h :
  Membership.mem (γ := Subring (RatFuncAdicCompl K))
      (Subring.map (RingEquiv.toRingHom (LaurentSeriesRingEquiv K)) (powerSeries_as_subring K)) x →
    ∀ (f : K⸨X⸩) (F : K⟦X⟧),
      Membership.mem (γ := Set K⟦X⟧)
          (Subsemigroup.carrier (Submonoid.toSubsemigroup (Subsemiring.toSubmonoid (Subring.toSubsemiring ⊤)))) F →
        ∀ (coe_F : ((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⸨X⸩) F = f)
          (hF : (RingEquiv.toRingHom (LaurentSeriesRingEquiv K) : (a : K⸨X⸩) → RatFuncAdicCompl K) f = x),
          Membership.mem (γ := Subring (RatFuncAdicCompl K))
            (ValuationSubring.toSubring (adicCompletionIntegers K⟮X⟯ (idealX K))) x
h₁ :
  ∀
    (H :
      Membership.mem (γ := Subring (RatFuncAdicCompl K))
        (ValuationSubring.toSubring (adicCompletionIntegers K⟮X⟯ (idealX K))) x),
    Membership.mem (γ := Subring (RatFuncAdicCompl K))
      (Subring.map (RingEquiv.toRingHom (LaurentSeriesRingEquiv K)) (powerSeries_as_subring K)) x
⊢ Membership.mem (γ := Subring (RatFuncAdicCompl K))
      (Subring.map (RingEquiv.toRingHom (LaurentSeriesRingEquiv K)) (powerSeries_as_subring K)) x ↔
    Membership.mem (γ := Subring (RatFuncAdicCompl K))
      (ValuationSubring.toSubring (adicCompletionIntegers K⟮X⟯ (idealX K))) x

Tactic:
refine ⟨fun ⟨f, ⟨F, _, coe_F⟩, hF⟩ ↦ ?_, fun H ↦ ?_⟩
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
x : RatFuncAdicCompl K
h_1 :
  Membership.mem (γ := Subring (RatFuncAdicCompl K))
    (Subring.map (RingEquiv.toRingHom (LaurentSeriesRingEquiv K)) (powerSeries_as_subring K)) x
f : K⸨X⸩
F : K⟦X⟧
left :
  Membership.mem (γ := Set K⟦X⟧)
    (Subsemigroup.carrier (Submonoid.toSubsemigroup (Subsemiring.toSubmonoid (Subring.toSubsemiring ⊤)))) F
coe_F : ((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⸨X⸩) F = f
hF : (RingEquiv.toRingHom (LaurentSeriesRingEquiv K) : (a : K⸨X⸩) → RatFuncAdicCompl K) f = x
h :
  Membership.mem (α := RatFuncAdicCompl K) (γ := ValuationSubring (RatFuncAdicCompl K))
    (adicCompletionIntegers K⟮X⟯ (idealX K))
    ((RingEquiv.toRingHom (LaurentSeriesRingEquiv K) : (a : K⸨X⸩) → RatFuncAdicCompl K)
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⸨X⸩) F) :
      RatFuncAdicCompl K)
⊢ Membership.mem (γ := Subring (RatFuncAdicCompl K))
    (ValuationSubring.toSubring (adicCompletionIntegers K⟮X⟯ (idealX K))) x

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

Premises used: ValuationSubring.mem_toSubring
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
x : RatFuncAdicCompl K
h :
  Membership.mem (γ := Subring (RatFuncAdicCompl K))
    (Subring.map (RingEquiv.toRingHom (LaurentSeriesRingEquiv K)) (powerSeries_as_subring K)) x
f : K⸨X⸩
F : K⟦X⟧
left :
  Membership.mem (γ := Set K⟦X⟧)
    (Subsemigroup.carrier (Submonoid.toSubsemigroup (Subsemiring.toSubmonoid (Subring.toSubsemiring ⊤)))) F
coe_F : ((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⸨X⸩) F = f
hF : (RingEquiv.toRingHom (LaurentSeriesRingEquiv K) : (a : K⸨X⸩) → RatFuncAdicCompl K) f = x
⊢ Membership.mem (α := RatFuncAdicCompl K) (γ := ValuationSubring (RatFuncAdicCompl K))
    (adicCompletionIntegers K⟮X⟯ (idealX K))
    ((RingEquiv.toRingHom (LaurentSeriesRingEquiv K) : (a : K⸨X⸩) → RatFuncAdicCompl K)
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⸨X⸩) F) :
      RatFuncAdicCompl K)

Tactic:
apply mem_integers_of_powerSeries

Premises used: LaurentSeries.mem_integers_of_powerSeries
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
x : RatFuncAdicCompl K
H :
  Membership.mem (γ := Subring (RatFuncAdicCompl K))
    (ValuationSubring.toSubring (adicCompletionIntegers K⟮X⟯ (idealX K))) x
h :
  ∀ (F : K⟦X⟧)
    (hF :
      (LaurentSeriesRingEquiv K : (a : K⸨X⸩) → RatFuncAdicCompl K)
          (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F) =
        x),
    Membership.mem (γ := Subring (RatFuncAdicCompl K))
      (Subring.map (RingEquiv.toRingHom (LaurentSeriesRingEquiv K)) (powerSeries_as_subring K)) x
⊢ Membership.mem (γ := Subring (RatFuncAdicCompl K))
    (Subring.map (RingEquiv.toRingHom (LaurentSeriesRingEquiv K)) (powerSeries_as_subring K)) x

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

Premises used: LaurentSeries.exists_powerSeries_of_memIntegers
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
x : RatFuncAdicCompl K
H :
  Membership.mem (γ := Subring (RatFuncAdicCompl K))
    (ValuationSubring.toSubring (adicCompletionIntegers K⟮X⟯ (idealX K))) x
F : K⟦X⟧
hF :
  (LaurentSeriesRingEquiv K : (a : K⸨X⸩) → RatFuncAdicCompl K)
      (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F) =
    x
⊢ ∃ (x_1 : K⸨X⸩),
    (∃ (x : K⟦X⟧),
        Membership.mem (γ := Subring K⟦X⟧) ⊤ x ∧ ((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⸨X⸩) x = x_1) ∧
      (RingEquiv.toRingHom (LaurentSeriesRingEquiv K) : (a : K⸨X⸩) → RatFuncAdicCompl K) x_1 = x

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

Premises used: trivial, Int, And.intro, Exists.intro, DFunLike.coe, rfl, HahnSeries.ofPowerSeries
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
x : RatFuncAdicCompl K
H :
  Membership.mem (γ := Subring (RatFuncAdicCompl K))
    (ValuationSubring.toSubring (adicCompletionIntegers K⟮X⟯ (idealX K))) x
F : K⟦X⟧
hF :
  (LaurentSeriesRingEquiv K : (a : K⸨X⸩) → RatFuncAdicCompl K)
      (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F) =
    x
⊢ ∃ (x_1 : K⸨X⸩),
    (∃ (x : K⟦X⟧),
        Membership.mem (γ := Subring K⟦X⟧) ⊤ x ∧ ((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⸨X⸩) x = x_1) ∧
      (RingEquiv.toRingHom (LaurentSeriesRingEquiv K) : (a : K⸨X⸩) → RatFuncAdicCompl K) x_1 = x

Tactic:
exact ⟨F, ⟨F, trivial, rfl⟩, hF⟩
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⟦X⟧
⊢ Eq (α := adicCompletion (R := K[X]) K⟮X⟯ (idealX K))
    ((↑((powerSeriesRingEquiv K : (a : K⟦X⟧) → ↥(adicCompletionIntegers K⟮X⟯ (idealX K))) f) :
        adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) :
      adicCompletion (R := K[X]) K⟮X⟯ (idealX K))
    ((LaurentSeriesRingEquiv K : (a : K⸨X⸩) → RatFuncAdicCompl K)
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) f) :
      RatFuncAdicCompl K)

Tactic:
rfl

Premises used: AbstractCompletion.compare, AbstractCompletion.extend, rfl, ite
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f : K⟦X⟧
rw :
  ∃ (F : K⟦X⟧),
    Eq (α := K⟦ℤ⟧) (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F : K⟦ℤ⟧)
      (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) f : K⟦ℤ⟧)
⊢ LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation (RatFuncAdicCompl K) (WithZero (Multiplicative ℤ))) :
          (a : RatFuncAdicCompl K) → WithZero (Multiplicative ℤ))
        ((LaurentSeriesRingEquiv K : (a : K⸨X⸩) → RatFuncAdicCompl K)
          (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) f)) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))

Tactic:
rw [LaurentSeriesRingEquiv_def, valuation_compare, val_le_one_iff_eq_coe]

Premises used: LaurentSeries.LaurentSeriesRingEquiv_def, LaurentSeries.val_le_one_iff_eq_coe, LaurentSeries.valuation_compare
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
f w : K⟦X⟧
h :
  Eq (α := K⟦ℤ⟧) (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) f : K⟦ℤ⟧)
    (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) f : K⟦ℤ⟧)
⊢ ∃ (F : K⟦X⟧),
    Eq (α := K⟦ℤ⟧) (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F : K⟦ℤ⟧)
      (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) f : K⟦ℤ⟧)

Tactic:
use f
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
x : K
⊢ Eq (α := K⟦ℤ⟧) ((HahnSeries.C : (a : K) → K⟦ℤ⟧) x : K⟦ℤ⟧)
    (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) ((PowerSeries.C : (a : K) → K⟦X⟧) x) : K⟦ℤ⟧)

Tactic:
simp [C_apply, ofPowerSeries_C]

Premises used: HahnSeries.C_apply, HahnSeries.ofPowerSeries_C
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
x : K
⊢ Eq (α := K⟦ℤ⟧) ((HahnSeries.C : (a : K) → K⟦ℤ⟧) x : K⟦ℤ⟧)
    (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) ((PowerSeries.C : (a : K) → K⟦X⟧) x) : K⟦ℤ⟧)

Tactic:
have : HahnSeries.C x = ofPowerSeries ℤ K (PowerSeries.C x) := by
    simp [C_apply, ofPowerSeries_C]
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
x : K
this :
  Eq (α := K⟦ℤ⟧) ((HahnSeries.C : (a : K) → K⟦ℤ⟧) x : K⟦ℤ⟧)
    (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) ((PowerSeries.C : (a : K) → K⟦X⟧) x) : K⟦ℤ⟧)
simp :
  Membership.mem (α := RatFuncAdicCompl K) (γ := ValuationSubring (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)))
    (adicCompletionIntegers K⟮X⟯ (idealX K))
    ((LaurentSeriesRingEquiv K : (a : K⸨X⸩) → RatFuncAdicCompl K)
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) ((PowerSeries.C : (a : K) → K⟦X⟧) x)) :
      RatFuncAdicCompl K)
⊢ Membership.mem (α := RatFuncAdicCompl K) (γ := ValuationSubring (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)))
    (adicCompletionIntegers K⟮X⟯ (idealX K))
    ((RingHom.comp (RingEquiv.toRingHom (LaurentSeriesRingEquiv K)) HahnSeries.C : (a : K) → RatFuncAdicCompl K) x :
      RatFuncAdicCompl K)

Tactic:
simp only [RingHom.comp_apply, RingEquiv.toRingHom_eq_coe, RingHom.coe_coe, this]

Premises used: RingHom.coe_coe, RingHom.comp_apply, RingEquiv.toRingHom_eq_coe
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
K : Type u_2
inst : Field K
x : K
this :
  Eq (α := K⟦ℤ⟧) ((HahnSeries.C : (a : K) → K⟦ℤ⟧) x : K⟦ℤ⟧)
    (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) ((PowerSeries.C : (a : K) → K⟦X⟧) x) : K⟦ℤ⟧)
⊢ Membership.mem (α := RatFuncAdicCompl K) (γ := ValuationSubring (adicCompletion (R := K[X]) K⟮X⟯ (idealX K)))
    (adicCompletionIntegers K⟮X⟯ (idealX K))
    ((LaurentSeriesRingEquiv K : (a : K⸨X⸩) → RatFuncAdicCompl K)
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) ((PowerSeries.C : (a : K) → K⟦X⟧) x)) :
      RatFuncAdicCompl K)

Tactic:
apply LaurentSeriesRingEquiv_mem_valuationSubring

Premises used: LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
K : Type u_2
inst : Field K
apply :
  ∀ (x : K),
    Eq (α := ↥(adicCompletionIntegers K⟮X⟯ (idealX K)))
      ((powerSeriesRingEquiv K : (a : K⟦X⟧) → ↥(adicCompletionIntegers K⟮X⟯ (idealX K)))
          ((algebraMap K K⟦X⟧ : (a : K) → K⟦X⟧) x) :
        ↥(adicCompletionIntegers K⟮X⟯ (idealX K)))
      ((algebraMap K ↥(adicCompletionIntegers K⟮X⟯ (idealX K)) : (a : K) → ↥(adicCompletionIntegers K⟮X⟯ (idealX K)))
          x :
        ↥(adicCompletionIntegers K⟮X⟯ (idealX K)))
⊢ K⟦X⟧ ≃ₐ[K] ↥(adicCompletionIntegers K⟮X⟯ (idealX K))

Tactic:
apply AlgEquiv.ofRingEquiv (f := powerSeriesRingEquiv K)

Premises used: AlgEquiv.ofRingEquiv
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
K : Type u_2
inst : Field K
a : K
rw :
  Eq (α := adicCompletion (R := K[X]) K⟮X⟯ (idealX K))
    ((LaurentSeriesRingEquiv K : (a : K⸨X⸩) → RatFuncAdicCompl K)
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) ((PowerSeries.C : (a : K) → K⟦X⟧) a)) :
      RatFuncAdicCompl K)
    ((RingHom.comp (RingEquiv.toRingHom (LaurentSeriesRingEquiv K)) HahnSeries.C : (a : K) → RatFuncAdicCompl K) a :
      RatFuncAdicCompl K)
⊢ Eq (α := ↥(adicCompletionIntegers K⟮X⟯ (idealX K)))
    ((powerSeriesRingEquiv K : (a : K⟦X⟧) → ↥(adicCompletionIntegers K⟮X⟯ (idealX K)))
        ((algebraMap K K⟦X⟧ : (a : K) → K⟦X⟧) a) :
      ↥(adicCompletionIntegers K⟮X⟯ (idealX K)))
    ((algebraMap K ↥(adicCompletionIntegers K⟮X⟯ (idealX K)) : (a : K) → ↥(adicCompletionIntegers K⟮X⟯ (idealX K))) a :
      ↥(adicCompletionIntegers K⟮X⟯ (idealX K)))

Tactic:
rw [PowerSeries.algebraMap_eq, RingHom.algebraMap_toAlgebra, ← Subtype.coe_inj,
    powerSeriesRingEquiv_coe_apply,
    RingHom.codRestrict_apply _ _ (algebraMap_C_mem_adicCompletionIntegers K)]

Premises used: LaurentSeries.algebraMap_C_mem_adicCompletionIntegers, Subtype.coe_inj, LaurentSeries.powerSeriesRingEquiv_coe_apply, RingHom.codRestrict_apply, PowerSeries.algebraMap_eq, RingHom.algebraMap_toAlgebra
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
K : Type u_2
inst : Field K
a : K
⊢ Eq (α := adicCompletion (R := K[X]) K⟮X⟯ (idealX K))
    ((LaurentSeriesRingEquiv K : (a : K⸨X⸩) → RatFuncAdicCompl K)
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) ((PowerSeries.C : (a : K) → K⟦X⟧) a)) :
      RatFuncAdicCompl K)
    ((RingHom.comp (RingEquiv.toRingHom (LaurentSeriesRingEquiv K)) HahnSeries.C : (a : K) → RatFuncAdicCompl K) a :
      RatFuncAdicCompl K)

Tactic:
simp
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ Order.krullDim.{u_2} (Submodule R M) ≠ ⊥

Tactic:
simp [Order.krullDim_eq_bot_iff]

Premises used: Order.krullDim_eq_bot_iff
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ (↑(length R M) : WithBot ℕ∞) = Order.krullDim.{u_2} (Submodule R M)

Tactic:
WithBot.coe_unbot _ _

Premises used: WithBot.coe_unbot, Module.length
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
a : (↑(length R M) : WithBot ℕ∞) = (↑(Order.height.{u_2} (α := Submodule R M) ⊤) : WithBot ℕ∞)
⊢ length R M = Order.height.{u_2} (α := Submodule R M) ⊤

Tactic:
apply WithBot.coe_injective

Premises used: WithBot.coe_injective
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
a : Order.krullDim.{u_2} (Submodule R M) = (↑(Order.height.{u_2} (α := Submodule R M) ⊤) : WithBot ℕ∞)
a₁ a₂ : Order.krullDim.{u_2} (Submodule R M) = Order.krullDim.{u_2} (Submodule R M)
⊢ (↑(length R M) : WithBot ℕ∞) = (↑(Order.height.{u_2} (α := Submodule R M) ⊤) : WithBot ℕ∞)

Tactic:
rw [Module.coe_length, Order.height_top_eq_krullDim]

Premises used: Module.coe_length, Order.height_top_eq_krullDim
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
a : (↑(length R M) : WithBot ℕ∞) = (↑(Order.coheight.{u_2} (α := Submodule R M) ⊥) : WithBot ℕ∞)
⊢ length R M = Order.coheight.{u_2} (α := Submodule R M) ⊥

Tactic:
apply WithBot.coe_injective

Premises used: WithBot.coe_injective
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
a : Order.krullDim.{u_2} (Submodule R M) = (↑(Order.coheight.{u_2} (α := Submodule R M) ⊥) : WithBot ℕ∞)
a₁ a₂ : Order.krullDim.{u_2} (Submodule R M) = Order.krullDim.{u_2} (Submodule R M)
⊢ (↑(length R M) : WithBot ℕ∞) = (↑(Order.coheight.{u_2} (α := Submodule R M) ⊥) : WithBot ℕ∞)

Tactic:
rw [Module.coe_length, Order.coheight_bot_eq_krullDim]

Premises used: Module.coe_length, Order.coheight_bot_eq_krullDim
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
rw : (↑(length R M) : WithBot ℕ∞) = (↑0 : WithBot ℕ∞) ↔ Subsingleton M
rw₁ : Order.krullDim.{u_2} (Submodule R M) = (↑0 : WithBot ℕ∞) ↔ Subsingleton M
rw₂ : Order.krullDim.{u_2} (Submodule R M) = 0 ↔ Subsingleton M
rw₃ : Subsingleton.{u_2 + 1} (Submodule R M) ↔ Subsingleton M
rw₄ rw₅ : Subsingleton M ↔ Subsingleton M
⊢ length R M = 0 ↔ Subsingleton M

Tactic:
rw [← WithBot.coe_inj, Module.coe_length, WithBot.coe_zero,
    Order.krullDim_eq_zero_iff_of_orderTop, Submodule.subsingleton_iff]

Premises used: Submodule.subsingleton_iff, Module.coe_length, Order.krullDim_eq_zero_iff_of_orderTop, WithBot.coe_inj, WithBot.coe_zero
-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Subsingleton M
⊢ length R M = 0

Tactic:
Module.length_eq_zero_iff.mpr ‹_›

Premises used: Iff.mpr, Module.length_eq_zero_iff