awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
this : UniformSpace (space (α := WithVal (R := K⟮X⟯) (polynomialValuationX K)) ratfuncAdicComplPkg) :=
  uniformStruct ratfuncAdicComplPkg
x : WithZero (Multiplicative ℤ)
⊢ ∃ (a : WithVal (R := K⟮X⟯) (polynomialValuationX K)),
    ((Valued.v : Valuation (WithVal (R := K⟮X⟯) (polynomialValuationX K)) (WithZero (Multiplicative ℤ))) :
          (a : WithVal (polynomialValuationX K)) → WithZero (Multiplicative ℤ))
        a =
      x
have cont_f : ∀ (y : K⟮X⟯),
  ∃ (a : WithVal (R := K⟮X⟯) (polynomialValuationX K)),
    Eq (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation (WithVal (R := K⟮X⟯) (polynomialValuationX K)) (WithZero (Multiplicative ℤ))) :
            (a : WithVal (polynomialValuationX K)) → WithZero (Multiplicative ℤ))
          a :
        WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⟮X⟯ (WithZero (Multiplicative ℤ))) : (a : K⟮X⟯) → WithZero (Multiplicative ℤ)) y :
        WithZero (Multiplicative ℤ))
Tactic: obtain ⟨y, rfl⟩ := RatFunc.valuation_surjective K x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (hypothesis)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
this : UniformSpace (space (α := WithVal (R := K⟮X⟯) (polynomialValuationX K)) ratfuncAdicComplPkg) :=
  uniformStruct ratfuncAdicComplPkg
x : space (α := WithVal (R := K⟮X⟯) (polynomialValuationX K)) ratfuncAdicComplPkg
⊢ Tendsto (β := WithZero (Multiplicative ℤ))
    (⇑Valued.v : (a : WithVal (polynomialValuationX K)) → WithZero (Multiplicative ℤ))
    (Filter.comap (AbstractCompletion.coe ratfuncAdicComplPkg) (𝓝 x))
    (𝓝 (IsDenseInducing.extend ⋯ (⇑Valued.v : (a : WithVal (polynomialValuationX K)) → WithZero (Multiplicative ℤ)) x))
have h_cont : Continuous.{u_2, 0} (X := adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (Y := WithZero (Multiplicative ℤ))
  (⇑Valued.v : (a : adicCompletion K⟮X⟯ (idealX K)) → WithZero (Multiplicative ℤ))
Tactic: have h_cont := Valued.continuous_valuation_of_surjective
      (valuedAdicCompletion_surjective K⟮X⟯ (idealX K))
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
this : UniformSpace (space (α := WithVal (R := K⟮X⟯) (polynomialValuationX K)) ratfuncAdicComplPkg) :=
  uniformStruct ratfuncAdicComplPkg
x : space (α := WithVal (R := K⟮X⟯) (polynomialValuationX K)) ratfuncAdicComplPkg
h_cont :
  Continuous.{u_2, 0} (X := adicCompletion (R := K[X]) K⟮X⟯ (idealX K)) (Y := WithZero (Multiplicative ℤ))
    (⇑Valued.v : (a : adicCompletion K⟮X⟯ (idealX K)) → WithZero (Multiplicative ℤ))
⊢ Tendsto (β := WithZero (Multiplicative ℤ))
    (⇑Valued.v : (a : WithVal (polynomialValuationX K)) → WithZero (Multiplicative ℤ))
    (Filter.comap (AbstractCompletion.coe ratfuncAdicComplPkg) (𝓝 x))
    (𝓝 (IsDenseInducing.extend ⋯ (⇑Valued.v : (a : WithVal (polynomialValuationX K)) → WithZero (Multiplicative ℤ)) x))
have a : Tendsto (β := WithZero (Multiplicative ℤ))
  ((⇑Valued.v : (a : WithVal (R := K⟮X⟯) (polynomialValuationX K)) → WithZero (Multiplicative ℤ)) :
    (a : WithVal (R := K⟮X⟯) (polynomialValuationX K)) → WithZero (Multiplicative ℤ))
  (Filter.comap (AbstractCompletion.coe ratfuncAdicComplPkg) (𝓝 x))
  (𝓝
      (((Valued.v :
            Valuation (UniformSpace.Completion (WithVal (R := K⟮X⟯) (polynomialValuationX K)))
              (WithZero (Multiplicative ℤ))) :
          (a : UniformSpace.Completion (WithVal (polynomialValuationX K))) → WithZero (Multiplicative ℤ))
        x) :
    Filter (WithZero (Multiplicative ℤ)))
Tactic: rw [ratfuncAdicComplPkg.isDenseInducing.extend_unique
        Valued.valuedCompletion_apply h_cont]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
F : K⟦X⟧
⊢ 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⟦ℤ⟧) F) :
      RatFuncAdicCompl K)
have simp : ∃ (F_1 : K⟦X⟧),
  Eq (α := K⟦ℤ⟧) (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F_1 : K⟦ℤ⟧)
    (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F : K⟦ℤ⟧)
Tactic: simp only [mem_adicCompletionIntegers, LaurentSeriesRingEquiv_def,
    valuation_compare, val_le_one_iff_eq_coe]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (hypothesis)
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⟧),
    (LaurentSeriesRingEquiv K : (a : K⸨X⸩) → RatFuncAdicCompl K)
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F) =
      x
have hf : let f : K⸨X⸩ := (ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x;
f = (ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x
Tactic: set f := (ratfuncAdicComplRingEquiv K) x with hf
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (hypothesis)
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
⊢ ∃ (F : K⟦X⟧),
    (LaurentSeriesRingEquiv K : (a : K⸨X⸩) → RatFuncAdicCompl K)
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F) =
      x
have H_x : AbstractCompletion.compare (LaurentSeriesPkg K) ratfuncAdicComplPkg
    ((ratfuncAdicComplRingEquiv K : (a : RatFuncAdicCompl K) → K⸨X⸩) x) =
  x
Tactic: have H_x : (LaurentSeriesPkg K).compare ratfuncAdicComplPkg ((ratfuncAdicComplRingEquiv K) x) =
      x := congr_fun (inverse_compare (LaurentSeriesPkg K) ratfuncAdicComplPkg) x
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (hypothesis)
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
⊢ ∃ (F : K⟦X⟧),
    (LaurentSeriesRingEquiv K : (a : K⸨X⸩) → RatFuncAdicCompl K)
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F) =
      x
have 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 ℤ))
Tactic: rw [mem_adicCompletionIntegers, ← H_x] at hx
Cleared hypotheses: hx, f, hf, H_x
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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⟧),
    (LaurentSeriesRingEquiv K : (a : K⸨X⸩) → RatFuncAdicCompl K)
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F) =
      x
have 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
Tactic: obtain ⟨F, hF⟩ := (val_le_one_iff_eq_coe K f).mp (valuation_compare _ f ▸ hx)
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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
⊢ (LaurentSeriesRingEquiv K : (a : K⸨X⸩) → RatFuncAdicCompl K)
      (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F) =
    x
have rw : (LaurentSeriesRingEquiv K : (a : K⸨X⸩) → RatFuncAdicCompl K) f = x
Tactic: rw [hF, hf, RingEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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
⊢ (LaurentSeriesRingEquiv K : (a : K⸨X⸩) → RatFuncAdicCompl K)
      (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F) =
    x
have rw₂ : x = x
Tactic: rw [hF, hf, RingEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
⊢ Eq (α := Subring (RatFuncAdicCompl K))
    (Subring.map (RingEquiv.toRingHom (LaurentSeriesRingEquiv K)) (powerSeries_as_subring K))
    (ValuationSubring.toSubring (adicCompletionIntegers K⟮X⟯ (idealX K)))
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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
have 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
Tactic: refine ⟨fun ⟨f, ⟨F, _, coe_F⟩, hF⟩ ↦ ?_, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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
⊢ 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
have 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
Tactic: refine ⟨fun ⟨f, ⟨F, _, coe_F⟩, hF⟩ ↦ ?_, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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 (γ := Subring (RatFuncAdicCompl K))
    (ValuationSubring.toSubring (adicCompletionIntegers K⟮X⟯ (idealX K))) x
have 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)
Tactic: simp only [ValuationSubring.mem_toSubring, ← hF, ← coe_F]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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
⊢ Membership.mem (γ := Subring (RatFuncAdicCompl K))
    (Subring.map (RingEquiv.toRingHom (LaurentSeriesRingEquiv K)) (powerSeries_as_subring K)) x
have 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
Tactic: obtain ⟨F, hF⟩ := exists_powerSeries_of_memIntegers K H
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⟦X⟧
⊢ 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 ℤ))
have 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⟦ℤ⟧)
Tactic: rw [LaurentSeriesRingEquiv_def, valuation_compare, val_le_one_iff_eq_coe]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f w : K⟦X⟧
⊢ ∃ (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⟦ℤ⟧)
have 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⟦ℤ⟧)
Tactic: use f
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (hypothesis)
Goal:
K : Type u_2
inst : Field K
x : 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)
have 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⟦ℤ⟧)
Tactic: have : HahnSeries.C x = ofPowerSeries ℤ K (PowerSeries.C x) := by
    simp [C_apply, ofPowerSeries_C]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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))
    ((RingHom.comp (RingEquiv.toRingHom (LaurentSeriesRingEquiv K)) HahnSeries.C : (a : K) → RatFuncAdicCompl K) x :
      RatFuncAdicCompl K)
have 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)
Tactic: simp only [RingHom.comp_apply, RingEquiv.toRingHom_eq_coe, RingHom.coe_coe, this]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
K : Type u_2
inst : Field K
⊢ K⟦X⟧ ≃ₐ[K] ↥(adicCompletionIntegers K⟮X⟯ (idealX K))
have 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)))
Tactic: apply AlgEquiv.ofRingEquiv (f := powerSeriesRingEquiv K)
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
K : Type u_2
inst : Field K
a : 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)))
have 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)
Tactic: rw [PowerSeries.algebraMap_eq, RingHom.algebraMap_toAlgebra, ← Subtype.coe_inj,
    powerSeriesRingEquiv_coe_apply,
    RingHom.codRestrict_apply _ _ (algebraMap_C_mem_adicCompletionIntegers K)]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ length R M = Order.height.{u_2} (α := Submodule R M) ⊤
have a : (↑(length R M) : WithBot ℕ∞) = (↑(Order.height.{u_2} (α := Submodule R M) ⊤) : WithBot ℕ∞)
Tactic: apply WithBot.coe_injective
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
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.height.{u_2} (α := Submodule R M) ⊤) : WithBot ℕ∞)
have a : Order.krullDim.{u_2} (Submodule R M) = (↑(Order.height.{u_2} (α := Submodule R M) ⊤) : WithBot ℕ∞)
Tactic: rw [Module.coe_length, Order.height_top_eq_krullDim]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
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 ℕ∞)
⊢ (↑(length R M) : WithBot ℕ∞) = (↑(Order.height.{u_2} (α := Submodule R M) ⊤) : WithBot ℕ∞)
have a₁ : Order.krullDim.{u_2} (Submodule R M) = Order.krullDim.{u_2} (Submodule R M)
Tactic: rw [Module.coe_length, Order.height_top_eq_krullDim]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ length R M = Order.coheight.{u_2} (α := Submodule R M) ⊥
have a : (↑(length R M) : WithBot ℕ∞) = (↑(Order.coheight.{u_2} (α := Submodule R M) ⊥) : WithBot ℕ∞)
Tactic: apply WithBot.coe_injective
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
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.coheight.{u_2} (α := Submodule R M) ⊥) : WithBot ℕ∞)
have a : Order.krullDim.{u_2} (Submodule R M) = (↑(Order.coheight.{u_2} (α := Submodule R M) ⊥) : WithBot ℕ∞)
Tactic: rw [Module.coe_length, Order.coheight_bot_eq_krullDim]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
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 ℕ∞)
⊢ (↑(length R M) : WithBot ℕ∞) = (↑(Order.coheight.{u_2} (α := Submodule R M) ⊥) : WithBot ℕ∞)
have a₁ : Order.krullDim.{u_2} (Submodule R M) = Order.krullDim.{u_2} (Submodule R M)
Tactic: rw [Module.coe_length, Order.coheight_bot_eq_krullDim]
-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
⊢ length R M = 0 ↔ Subsingleton M
have rw : (↑(length R M) : WithBot ℕ∞) = (↑0 : WithBot ℕ∞) ↔ Subsingleton M
Tactic: rw [← WithBot.coe_inj, Module.coe_length, WithBot.coe_zero,
    Order.krullDim_eq_zero_iff_of_orderTop, Submodule.subsingleton_iff]