awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
H : j < n
neg :
  HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R)
      ((coeff (i, j).2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R) =
    HMul.hMul (α := R) (β := R)
      ((MvPowerSeries.coeff
              (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
                | (a, b) => (single () a, single () b)).1 :
            (a : MvPowerSeries Unit R) → R)
          φ :
        R)
      ((MvPowerSeries.coeff
              (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
                | (a, b) => (single () a, single () b)).2 :
            (a : MvPowerSeries Unit R) → R)
          (MvPowerSeries.inv.aux a φ) :
        R)
⊢ (if (i, j).2 < n then
      HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R)
        ((coeff (i, j).2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R)
    else 0) =
    if
        LT.lt (α := Unit →₀ ℕ)
          (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
            | (a, b) => (single () a, single () b)).2
          (single () n) then
      HMul.hMul (α := R) (β := R)
        ((MvPowerSeries.coeff
                (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
                  | (a, b) => (single () a, single () b)).1 :
              (a : MvPowerSeries Unit R) → R)
            φ :
          R)
        ((MvPowerSeries.coeff
                (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
                  | (a, b) => (single () a, single () b)).2 :
              (a : MvPowerSeries Unit R) → R)
            (MvPowerSeries.inv.aux a φ) :
          R)
    else 0
have neg₁ : LT.lt (α := Unit →₀ ℕ)
  (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
    | (a, b) => (single () a, single () b)).2
  (single () n)
Tactic: rw [if_pos H, if_pos]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
H : j < n
⊢ LT.lt (α := Unit →₀ ℕ)
    (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
      | (a, b) => (single () a, single () b)).2
    (single () n)
have neg : LE.le (α := Unit →₀ ℕ)
  (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
    | (a, b) => (single () a, single () b)).2
  (single () n)
Tactic: refine ⟨?_, fun hh ↦ H.not_ge ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
H : j < n
neg :
  LE.le (α := Unit →₀ ℕ)
    (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
      | (a, b) => (single () a, single () b)).2
    (single () n)
⊢ LT.lt (α := Unit →₀ ℕ)
    (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
      | (a, b) => (single () a, single () b)).2
    (single () n)
have neg₁ : ∀
  (hh :
    LE.le (α := Unit →₀ ℕ) (single () n)
      (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
        | (a, b) => (single () a, single () b)).2),
  n ≤ j
Tactic: refine ⟨?_, fun hh ↦ H.not_ge ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
R : Type u_1
inst : Ring R
φ : R⟦X⟧
u : Rˣ
⊢ (constantCoeff : (a : R⟦X⟧) → R) (φ.invOfUnit u) = (↑u⁻¹ : R)
have rw : (coeff 0 : (a : R⟦X⟧) → R) (φ.invOfUnit u) = (↑u⁻¹ : R)
Tactic: rw [← coeff_zero_eq_constantCoeff_apply, coeff_invOfUnit, if_pos rfl]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
R : Type u_1
inst : Ring R
φ : R⟦X⟧
u : Rˣ
rw : (coeff 0 : (a : R⟦X⟧) → R) (φ.invOfUnit u) = (↑u⁻¹ : R)
⊢ (constantCoeff : (a : R⟦X⟧) → R) (φ.invOfUnit u) = (↑u⁻¹ : R)
have rw₁ : (if Eq (α := ℕ) 0 0 then (↑u⁻¹ : R)
  else
    -(↑u⁻¹ : R) *
      ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ 0,
        if x.2 < 0 then
          HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) φ : R)
            ((coeff x.2 : (a : R⟦X⟧) → R) (φ.invOfUnit u) : R)
        else 0) =
  (↑u⁻¹ : R)
Tactic: rw [← coeff_zero_eq_constantCoeff_apply, coeff_invOfUnit, if_pos rfl]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
R : Type u_1
inst : Ring R
φ : R⟦X⟧
u : Rˣ
rw : (coeff 0 : (a : R⟦X⟧) → R) (φ.invOfUnit u) = (↑u⁻¹ : R)
rw₁ :
  (if Eq (α := ℕ) 0 0 then (↑u⁻¹ : R)
    else
      -(↑u⁻¹ : R) *
        ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ 0,
          if x.2 < 0 then
            HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) φ : R)
              ((coeff x.2 : (a : R⟦X⟧) → R) (φ.invOfUnit u) : R)
          else 0) =
    (↑u⁻¹ : R)
⊢ (constantCoeff : (a : R⟦X⟧) → R) (φ.invOfUnit u) = (↑u⁻¹ : R)
have rw₂ : (↑u⁻¹ : R) = (↑u⁻¹ : R)
Tactic: rw [← coeff_zero_eq_constantCoeff_apply, coeff_invOfUnit, if_pos rfl]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
k : Type u_2
inst : Field k
n : ℕ
φ : k⟦X⟧
⊢ Eq (α := k) ((coeff n : (a : k⟦X⟧) → k) φ⁻¹ : k)
    (if n = 0 then ((constantCoeff : (a : k⟦X⟧) → k) φ)⁻¹
      else
        HMul.hMul (α := k) (β := k) (-((constantCoeff : (a : k⟦X⟧) → k) φ)⁻¹ : k)
          (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
              if x.2 < n then
                HMul.hMul (α := k) (β := k) ((coeff x.1 : (a : k⟦X⟧) → k) φ : k) ((coeff x.2 : (a : k⟦X⟧) → k) φ⁻¹ : k)
              else 0 :
            k) :
      k)
have rw : Eq (α := k) ((coeff n : (a : k⟦X⟧) → k) (inv.aux ((constantCoeff : (a : k⟦X⟧) → k) φ)⁻¹ φ : k⟦X⟧) : k)
  (if n = 0 then ((constantCoeff : (a : k⟦X⟧) → k) φ)⁻¹
    else
      HMul.hMul (α := k) (β := k) (-((constantCoeff : (a : k⟦X⟧) → k) φ)⁻¹ : k)
        (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
            if x.2 < n then
              HMul.hMul (α := k) (β := k) ((coeff x.1 : (a : k⟦X⟧) → k) φ : k)
                ((coeff x.2 : (a : k⟦X⟧) → k) (inv.aux ((constantCoeff : (a : k⟦X⟧) → k) φ)⁻¹ φ : k⟦X⟧) : k)
            else 0 :
          k) :
    k)
Tactic: rw [inv_eq_inv_aux, coeff_inv_aux n (constantCoeff φ)⁻¹ φ]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
k : Type u_2
inst : Field k
n : ℕ
φ : k⟦X⟧
rw :
  Eq (α := k) ((coeff n : (a : k⟦X⟧) → k) (inv.aux ((constantCoeff : (a : k⟦X⟧) → k) φ)⁻¹ φ : k⟦X⟧) : k)
    (if n = 0 then ((constantCoeff : (a : k⟦X⟧) → k) φ)⁻¹
      else
        HMul.hMul (α := k) (β := k) (-((constantCoeff : (a : k⟦X⟧) → k) φ)⁻¹ : k)
          (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
              if x.2 < n then
                HMul.hMul (α := k) (β := k) ((coeff x.1 : (a : k⟦X⟧) → k) φ : k)
                  ((coeff x.2 : (a : k⟦X⟧) → k) (inv.aux ((constantCoeff : (a : k⟦X⟧) → k) φ)⁻¹ φ : k⟦X⟧) : k)
              else 0 :
            k) :
      k)
⊢ Eq (α := k) ((coeff n : (a : k⟦X⟧) → k) φ⁻¹ : k)
    (if n = 0 then ((constantCoeff : (a : k⟦X⟧) → k) φ)⁻¹
      else
        HMul.hMul (α := k) (β := k) (-((constantCoeff : (a : k⟦X⟧) → k) φ)⁻¹ : k)
          (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
              if x.2 < n then
                HMul.hMul (α := k) (β := k) ((coeff x.1 : (a : k⟦X⟧) → k) φ : k) ((coeff x.2 : (a : k⟦X⟧) → k) φ⁻¹ : k)
              else 0 :
            k) :
      k)
have rw₁ : Eq (α := k)
  (if n = 0 then ((constantCoeff : (a : k⟦X⟧) → k) φ)⁻¹
    else
      HMul.hMul (α := k) (β := k) (-((constantCoeff : (a : k⟦X⟧) → k) φ)⁻¹ : k)
        (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
            if x.2 < n then
              HMul.hMul (α := k) (β := k) ((coeff x.1 : (a : k⟦X⟧) → k) φ : k)
                ((coeff x.2 : (a : k⟦X⟧) → k) (inv.aux ((constantCoeff : (a : k⟦X⟧) → k) φ)⁻¹ φ : k⟦X⟧) : k)
            else 0 :
          k) :
    k)
  (if n = 0 then ((constantCoeff : (a : k⟦X⟧) → k) φ)⁻¹
    else
      HMul.hMul (α := k) (β := k) (-((constantCoeff : (a : k⟦X⟧) → k) φ)⁻¹ : k)
        (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
            if x.2 < n then
              HMul.hMul (α := k) (β := k) ((coeff x.1 : (a : k⟦X⟧) → k) φ : k)
                ((coeff x.2 : (a : k⟦X⟧) → k) (inv.aux ((constantCoeff : (a : k⟦X⟧) → k) φ)⁻¹ φ : k⟦X⟧) : k)
            else 0 :
          k) :
    k)
Tactic: rw [inv_eq_inv_aux, coeff_inv_aux n (constantCoeff φ)⁻¹ φ]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
R : Type u_1
k : Type u_2
inst : Field k
f : k⟦X⟧
hf : f ≠ 0
⊢ Invertible (α := k) ((constantCoeff : (a : k⟦X⟧) → k) f.divXPowOrder : k)
have h : Ne (α := k) ((constantCoeff : (a : k⟦X⟧) → k) f.divXPowOrder : k) (0 : k)
Tactic: apply invertibleOfNonzero
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
k : Type u_2
inst : Field k
f : k⟦X⟧
hf : f ≠ 0
⊢ Inv_divided_by_X_pow_order hf * f.divXPowOrder = 1
have rw : f.divXPowOrder * Inv_divided_by_X_pow_order hf = 1
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
k : Type u_2
inst : Field k
f : k⟦X⟧
hf : f ≠ 0
h : f = f.divXPowOrder
⊢ IsUnit f
have rw : IsUnit f.divXPowOrder
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (hypothesis)
Goal:
k : Type u_2
inst : Field k
f : k⟦X⟧
hf : f ≠ 0
h : IsUnit f
⊢ f = f.divXPowOrder
have this : f.order = 0
Tactic: have : f.order = 0 := by
      simp [order_zero_of_unit h]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
k : Type u_2
inst : Field k
f : k⟦X⟧
hf : f ≠ 0
h : IsUnit f
this : f.order = 0
| f
have rw : f.divXPowOrder
Tactic: rw [← X_pow_order_mul_divXPowOrder (f := f), this, ENat.toNat_zero,
      pow_zero, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
k : Type u_2
inst : Field k
f : k⟦X⟧
hf : f ≠ 0
h : IsUnit f
this : f.order = 0
⊢ f = f.divXPowOrder
have conv_lhs : f = f.divXPowOrder
Tactic: conv_lhs => rw [← X_pow_order_mul_divXPowOrder (f := f), this, ENat.toNat_zero,
      pow_zero, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
k : Type u_2
inst : Field k
f : k⟦X⟧
hf : f ≠ 0
h : IsUnit f
this : f.order = 0
conv_lhs : f = f.divXPowOrder
⊢ f = f.divXPowOrder
have conv_lhs₁ : f.divXPowOrder = f.divXPowOrder
Tactic: conv_lhs => rw [← X_pow_order_mul_divXPowOrder (f := f), this, ENat.toNat_zero,
      pow_zero, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
k : Type u_2
inst : Field k
f : k⟦X⟧
hf : f ≠ 0
⊢ ∃ (n : ℕ), Associated (HPow.hPow (α := k⟦X⟧) X n) f
have h : Associated (HPow.hPow (α := k⟦X⟧) X f.order.toNat) f
Tactic: use f.order.toNat
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
k : Type u_2
inst : Field k
f : k⟦X⟧
hf : f ≠ 0
⊢ Associated (HPow.hPow (α := k⟦X⟧) X f.order.toNat) f
have h : HPow.hPow (α := k⟦X⟧) X f.order.toNat * (↑f.Unit_of_divided_by_X_pow_order : k⟦X⟧) = f
Tactic: use Unit_of_divided_by_X_pow_order f
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
k : Type u_2
inst : Field k
f : k⟦X⟧
hf : f ≠ 0
⊢ HPow.hPow (α := k⟦X⟧) X f.order.toNat * (↑f.Unit_of_divided_by_X_pow_order : k⟦X⟧) = f
have h : HPow.hPow (α := k⟦X⟧) X f.order.toNat * f.divXPowOrder = f
Tactic: simp only [Unit_of_divided_by_X_pow_order_nonzero hf]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
k : Type u_2
inst : Field k
⊢ Ideal.IsMaximal (α := k⟦X⟧) (Ideal.span {X})
have rw : 1 ∉ Ideal.span {X} ∧ ∀ (J : Ideal k⟦X⟧) (x : k⟦X⟧), Ideal.span {X} ≤ J → x ∉ Ideal.span {X} → x ∈ J → 1 ∈ J
Tactic: rw [Ideal.isMaximal_iff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
k : Type u_2
inst : Field k
⊢ 1 ∉ Ideal.span {X} ∧ ∀ (J : Ideal k⟦X⟧) (x : k⟦X⟧), Ideal.span {X} ≤ J → x ∉ Ideal.span {X} → x ∈ J → 1 ∈ J
have left : 1 ∉ Ideal.span {X}
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
k : Type u_2
inst : Field k
left : 1 ∉ Ideal.span {X}
⊢ 1 ∉ Ideal.span {X} ∧ ∀ (J : Ideal k⟦X⟧) (x : k⟦X⟧), Ideal.span {X} ≤ J → x ∉ Ideal.span {X} → x ∈ J → 1 ∈ J
have right : ∀ (J : Ideal k⟦X⟧) (x : k⟦X⟧), Ideal.span {X} ≤ J → x ∉ Ideal.span {X} → x ∈ J → 1 ∈ J
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
k : Type u_2
inst : Field k
⊢ 1 ∉ Ideal.span {X}
have left : ¬Dvd.dvd.{u_2} (α := k⟦X⟧) X 1
Tactic: rw [Ideal.mem_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (hypothesis)
Goal:
k : Type u_2
inst : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : f ∉ Ideal.span {X}
hfI : f ∈ I
⊢ 1 ∈ I
have hfX₁ : ¬Eq (α := k) ((constantCoeff : (a : k⟦X⟧) → k) f : k) (0 : k)
Tactic: rw [Ideal.mem_span_singleton, X_dvd_iff] at hfX
Cleared hypotheses: hfX, hfI
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
k : Type u_2
inst : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬Eq (α := k) ((constantCoeff : (a : k⟦X⟧) → k) f : k) (0 : k)
hfI : f ∈ I
⊢ (C : (a : k) → k⟦X⟧) (f 0) = f - HSub.hSub (β := k⟦X⟧) f ((C : (a : k) → k⟦X⟧) (f 0) : k⟦X⟧)
have rw : Eq (α := k⟦X⟧) ((C : (a : k) → k⟦X⟧) (f 0) : k⟦X⟧) ((C : (a : k) → k⟦X⟧) (f 0) : k⟦X⟧)
Tactic: rw [sub_sub_cancel]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (hypothesis)
Goal:
k : Type u_2
inst : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬Eq (α := k) ((constantCoeff : (a : k⟦X⟧) → k) f : k) (0 : k)
hfI : f ∈ I
⊢ Membership.mem (α := k⟦X⟧) I ((C : (a : k) → k⟦X⟧) (f 0) : k⟦X⟧)
have this : (C : (a : k) → k⟦X⟧) (f 0) = f - HSub.hSub (β := k⟦X⟧) f ((C : (a : k) → k⟦X⟧) (f 0) : k⟦X⟧)
Tactic: have : C (f 0) = f - (f - C (f 0)) := by rw [sub_sub_cancel]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
k : Type u_2
inst : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬Eq (α := k) ((constantCoeff : (a : k⟦X⟧) → k) f : k) (0 : k)
hfI : f ∈ I
this : (C : (a : k) → k⟦X⟧) (f 0) = f - HSub.hSub (β := k⟦X⟧) f ((C : (a : k) → k⟦X⟧) (f 0) : k⟦X⟧)
⊢ Membership.mem (α := k⟦X⟧) I ((C : (a : k) → k⟦X⟧) (f 0) : k⟦X⟧)
have rw : f - HSub.hSub (β := k⟦X⟧) f ((C : (a : k) → k⟦X⟧) (f 0) : k⟦X⟧) ∈ I
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
k : Type u_2
inst : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬Eq (α := k) ((constantCoeff : (a : k⟦X⟧) → k) f : k) (0 : k)
hfI : f ∈ I
this : (C : (a : k) → k⟦X⟧) (f 0) = f - HSub.hSub (β := k⟦X⟧) f ((C : (a : k) → k⟦X⟧) (f 0) : k⟦X⟧)
⊢ f - HSub.hSub (β := k⟦X⟧) f ((C : (a : k) → k⟦X⟧) (f 0) : k⟦X⟧) ∈ I
have apply : HSub.hSub (β := k⟦X⟧) f ((C : (a : k) → k⟦X⟧) (f 0) : k⟦X⟧) ∈ I
Tactic: apply Ideal.sub_mem I hfI
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
k : Type u_2
inst : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬Eq (α := k) ((constantCoeff : (a : k⟦X⟧) → k) f : k) (0 : k)
hfI : f ∈ I
this : (C : (a : k) → k⟦X⟧) (f 0) = f - HSub.hSub (β := k⟦X⟧) f ((C : (a : k) → k⟦X⟧) (f 0) : k⟦X⟧)
⊢ HSub.hSub (β := k⟦X⟧) f ((C : (a : k) → k⟦X⟧) (f 0) : k⟦X⟧) ∈ I
have a : Membership.mem (γ := Submodule k⟦X⟧ k⟦X⟧) (Ideal.span {X}) (HSub.hSub (β := k⟦X⟧) f ((C : (a : k) → k⟦X⟧) (f 0) : k⟦X⟧))
Tactic: apply hI
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
k : Type u_2
inst : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬Eq (α := k) ((constantCoeff : (a : k⟦X⟧) → k) f : k) (0 : k)
hfI : f ∈ I
this : (C : (a : k) → k⟦X⟧) (f 0) = f - HSub.hSub (β := k⟦X⟧) f ((C : (a : k) → k⟦X⟧) (f 0) : k⟦X⟧)
⊢ Membership.mem (γ := Submodule k⟦X⟧ k⟦X⟧) (Ideal.span {X})
    (HSub.hSub (β := k⟦X⟧) f ((C : (a : k) → k⟦X⟧) (f 0) : k⟦X⟧))
have a : (constantCoeff : (a : k⟦X⟧) → k) f = f 0
Tactic: rw [Ideal.mem_span_singleton, X_dvd_iff, map_sub, constantCoeff_C, ←
          coeff_zero_eq_constantCoeff_apply, sub_eq_zero, coeff_zero_eq_constantCoeff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (hypothesis)
Goal:
k : Type u_2
inst : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬Eq (α := k) ((constantCoeff : (a : k⟦X⟧) → k) f : k) (0 : k)
hfI : f ∈ I
⊢ 1 ∈ I
have hfI0 : Membership.mem (α := k⟦X⟧) I ((C : (a : k) → k⟦X⟧) (f 0) : k⟦X⟧)
Tactic: have hfI0 : C (f 0) ∈ I := by
        have : C (f 0) = f - (f - C (f 0)) := by rw [sub_sub_cancel]
        rw [this]
        apply Ideal.sub_mem I hfI
        apply hI
        rw [Ideal.mem_span_singleton, X_dvd_iff, map_sub, constantCoeff_C, ←
          coeff_zero_eq_constantCoeff_apply, sub_eq_zero, coeff_zero_eq_constantCoeff]
        rfl
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
k : Type u_2
inst : Field k
I : Ideal k⟦X⟧
f : k⟦X⟧
hI : Ideal.span {X} ≤ I
hfX : ¬Eq (α := k) ((constantCoeff : (a : k⟦X⟧) → k) f : k) (0 : k)
hfI : f ∈ I
hfI0 : Membership.mem (α := k⟦X⟧) I ((C : (a : k) → k⟦X⟧) (f 0) : k⟦X⟧)
⊢ 1 ∈ I
have right : I = ⊤
Tactic: rw [← Ideal.eq_top_iff_one]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (hypothesis)
Goal:
k : Type u_2
inst : Field k
⊢ Eq (α := Ideal k⟦X⟧) (IsLocalRing.maximalIdeal k⟦X⟧) (Ideal.span {X})
have hX : Ideal.IsMaximal (α := k⟦X⟧) (Ideal.span {X})
Tactic: have hX : (Ideal.span {(X : k⟦X⟧)}).IsMaximal := by
    rw [Ideal.isMaximal_iff]
    constructor
    · rw [Ideal.mem_span_singleton]
      exact Prime.not_dvd_one X_prime
    · intro I f hI hfX hfI
      rw [Ideal.mem_span_singleton, X_dvd_iff] at hfX
      have hfI0 : C (f 0) ∈ I := by
        have : C (f 0) = f - (f - C (f 0)) := by rw [sub_sub_cancel]
        rw [this]
        apply Ideal.sub_mem I hfI
        apply hI
        rw [Ideal.mem_span_singleton, X_dvd_iff, map_sub, constantCoeff_C, ←
          coeff_zero_eq_constantCoeff_apply, sub_eq_zero, coeff_zero_eq_constantCoeff]
        rfl
      rw [← Ideal.eq_top_iff_one]
      apply Ideal.eq_top_of_isUnit_mem I hfI0 (IsUnit.map C (Ne.isUnit hfX))
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
k : Type u_2
inst : Field k
hX : Ideal.IsMaximal (α := k⟦X⟧) (Ideal.span {X})
⊢ Eq (α := Ideal k⟦X⟧) (IsLocalRing.maximalIdeal k⟦X⟧) (Ideal.span {X})
have rw : Eq.{u_2 + 1} (α := Ideal k⟦X⟧) (IsLocalRing.maximalIdeal k⟦X⟧) (IsLocalRing.maximalIdeal k⟦X⟧)
Tactic: rw [IsLocalRing.eq_maximalIdeal hX]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
R : Type u_1
k : Type u_2
inst : Field k
a b : k⟦X⟧
hf : a ≠ 0
hg : b ≠ 0
⊢ (a * b).Unit_of_divided_by_X_pow_order⁻¹ =
    HMul.hMul (α := k⟦X⟧ˣ) a.Unit_of_divided_by_X_pow_order⁻¹ b.Unit_of_divided_by_X_pow_order⁻¹
have simp : (a * b).Unit_of_divided_by_X_pow_order =
  HMul.hMul (α := k⟦X⟧ˣ) a.Unit_of_divided_by_X_pow_order b.Unit_of_divided_by_X_pow_order
Tactic: simp only [← mul_inv, inv_inj]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
R : Type u_1
k : Type u_2
inst : Field k
u : k⟦X⟧ˣ
⊢ (↑u : k⟦X⟧).Unit_of_divided_by_X_pow_order⁻¹ = u⁻¹
have set : let u₀ := (↑u : k⟦X⟧);
∀ (hu : u₀ = (↑u : k⟦X⟧)), u₀.Unit_of_divided_by_X_pow_order⁻¹ = u⁻¹
Tactic: set u₀ := u.1 with hu
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (hypothesis)
Goal:
R : Type u_1
k : Type u_2
inst : Field k
u : k⟦X⟧ˣ
u₀ : k⟦X⟧ := (↑u : k⟦X⟧)
hu : u₀ = (↑u : k⟦X⟧)
⊢ u₀.Unit_of_divided_by_X_pow_order⁻¹ = u⁻¹
have h₀ : IsUnit u₀
Tactic: have h₀ : IsUnit u₀ := ⟨u, hu.symm⟩
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
R : Type u_1
k : Type u_2
inst : Field k
u : k⟦X⟧ˣ
u₀ : k⟦X⟧ := (↑u : k⟦X⟧)
hu : u₀ = (↑u : k⟦X⟧)
h₀ : IsUnit u₀
⊢ u₀.Unit_of_divided_by_X_pow_order⁻¹ = u⁻¹
have rw : u₀.divXPowOrder = u₀
Tactic: rw [inv_inj, Units.ext_iff, ← hu, Unit_of_divided_by_X_pow_order_nonzero h₀.ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
k : Type u_2
inst : Field k
P : k[X]
hP : P ≠ 0
⊢ Multiset.count X (normalizedFactors (↑P : k⟦X⟧)) = Multiset.count Polynomial.X (normalizedFactors P)
have H : ∀ (c : ℕ), c ≤ Multiset.count X (normalizedFactors (↑P : k⟦X⟧)) ↔ c ≤ Multiset.count Polynomial.X (normalizedFactors P)
Tactic: apply eq_of_forall_le_iff
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
k : Type u_2
inst : Field k
P : k[X]
hP : P ≠ 0
⊢ ∀ (c : ℕ),
    c ≤ Multiset.count X (normalizedFactors (↑P : k⟦X⟧)) ↔ c ≤ Multiset.count Polynomial.X (normalizedFactors P)
have H : ∀ (c : ℕ),
  LE.le (α := ℕ∞) (↑c : ℕ∞) (↑(Multiset.count X (normalizedFactors (↑P : k⟦X⟧))) : ℕ∞) ↔
    LE.le (α := ℕ∞) (↑c : ℕ∞) (↑(Multiset.count Polynomial.X (normalizedFactors P)) : ℕ∞)
Tactic: simp only [← Nat.cast_le (α := ℕ∞)]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
k : Type u_2
inst : Field k
P : k[X]
hP : P ≠ 0
⊢ ∀ (c : ℕ),
    LE.le (α := ℕ∞) (↑c : ℕ∞) (↑(Multiset.count X (normalizedFactors (↑P : k⟦X⟧))) : ℕ∞) ↔
      LE.le (α := ℕ∞) (↑c : ℕ∞) (↑(Multiset.count Polynomial.X (normalizedFactors P)) : ℕ∞)
have H : ∀ (c : ℕ), (↑c : ℕ∞) ≤ emultiplicity X (↑P : k⟦X⟧) ↔ (↑c : ℕ∞) ≤ emultiplicity Polynomial.X P
Tactic: rw [X_eq_normalize, PowerSeries.X_eq_normalizeX, ← emultiplicity_eq_count_normalizedFactors
    irreducible_X hP, ← emultiplicity_eq_count_normalizedFactors X_irreducible]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
k : Type u_2
inst : Field k
P : k[X]
hP : P ≠ 0
H : ∀ (c : ℕ), (↑c : ℕ∞) ≤ emultiplicity X (↑P : k⟦X⟧) ↔ (↑c : ℕ∞) ≤ emultiplicity Polynomial.X P
⊢ ∀ (c : ℕ),
    LE.le (α := ℕ∞) (↑c : ℕ∞) (↑(Multiset.count X (normalizedFactors (↑P : k⟦X⟧))) : ℕ∞) ↔
      LE.le (α := ℕ∞) (↑c : ℕ∞) (↑(Multiset.count Polynomial.X (normalizedFactors P)) : ℕ∞)
have H₁ : (↑P : k⟦X⟧) ≠ 0
Tactic: rw [X_eq_normalize, PowerSeries.X_eq_normalizeX, ← emultiplicity_eq_count_normalizedFactors
    irreducible_X hP, ← emultiplicity_eq_count_normalizedFactors X_irreducible]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
k : Type u_2
inst : Field k
x : k⟦X⟧
⊢ Membership.mem (γ := Ideal k⟦X⟧) (RingHom.ker (F := k⟦X⟧ →+* k) constantCoeff) x ↔
    Membership.mem (γ := Ideal k⟦X⟧) (maximalIdeal k⟦X⟧ : Ideal k⟦X⟧) x
have rw : Eq (α := k) ((constantCoeff : (a : k⟦X⟧) → k) x : k) (0 : k) ↔
  Membership.mem (γ := Ideal k⟦X⟧) (maximalIdeal k⟦X⟧ : Ideal k⟦X⟧) x
Tactic: rw [RingHom.mem_ker, maximalIdeal_eq_span_X, Ideal.mem_span_singleton, X_dvd_iff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
k : Type u_2
inst : Field k
x : k⟦X⟧
rw :
  Eq (α := k) ((constantCoeff : (a : k⟦X⟧) → k) x : k) (0 : k) ↔
    Membership.mem (γ := Ideal k⟦X⟧) (maximalIdeal k⟦X⟧ : Ideal k⟦X⟧) x
⊢ Membership.mem (γ := Ideal k⟦X⟧) (RingHom.ker (F := k⟦X⟧ →+* k) constantCoeff) x ↔
    Membership.mem (γ := Ideal k⟦X⟧) (maximalIdeal k⟦X⟧ : Ideal k⟦X⟧) x
have rw₁ : Eq (α := k) ((constantCoeff : (a : k⟦X⟧) → k) x : k) (0 : k) ↔ Membership.mem (γ := Ideal k⟦X⟧) (Ideal.span {X}) x
Tactic: rw [RingHom.mem_ker, maximalIdeal_eq_span_X, Ideal.mem_span_singleton, X_dvd_iff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
k : Type u_2
inst : Field k
x : k⟦X⟧
rw :
  Eq (α := k) ((constantCoeff : (a : k⟦X⟧) → k) x : k) (0 : k) ↔
    Membership.mem (γ := Ideal k⟦X⟧) (maximalIdeal k⟦X⟧ : Ideal k⟦X⟧) x
rw₁ : Eq (α := k) ((constantCoeff : (a : k⟦X⟧) → k) x : k) (0 : k) ↔ Membership.mem (γ := Ideal k⟦X⟧) (Ideal.span {X}) x
⊢ Membership.mem (γ := Ideal k⟦X⟧) (RingHom.ker (F := k⟦X⟧ →+* k) constantCoeff) x ↔
    Membership.mem (γ := Ideal k⟦X⟧) (maximalIdeal k⟦X⟧ : Ideal k⟦X⟧) x
have rw₂ : Eq (α := k) ((constantCoeff : (a : k⟦X⟧) → k) x : k) (0 : k) ↔ X ∣ x
Tactic: rw [RingHom.mem_ker, maximalIdeal_eq_span_X, Ideal.mem_span_singleton, X_dvd_iff]