awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw₂ : Eq (α := k) ((constantCoeff : (a : k⟦X⟧) → k) x : k) (0 : 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) ↔
  Eq (α := k) ((constantCoeff : (a : k⟦X⟧) → k) x : k) (0 : k)
Tactic: rw [RingHom.mem_ker, maximalIdeal_eq_span_X, Ideal.mem_span_singleton, X_dvd_iff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Log (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
A' : Type u_2
inst_2 : CommRing A'
inst_3 : Algebra ℚ A'
f : A →+* A'
⊢ (map f : (a : A⟦X⟧) → A'⟦X⟧) (log A) = log A'
have h : ∀ (n : ℕ),
  Eq.{u_2 + 1} (α := A') ((coeff n : (a : A'⟦X⟧) → A') ((map f : (a : A⟦X⟧) → A'⟦X⟧) (log A) : A'⟦X⟧) : A')
    ((coeff n : (a : A'⟦X⟧) → A') (log A') : A')
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Log (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
A' : Type u_2
inst_2 : CommRing A'
inst_3 : Algebra ℚ A'
f : A →+* A'
n : ℕ
⊢ Eq.{u_2 + 1} (α := A') ((coeff n : (a : A'⟦X⟧) → A') ((map f : (a : A⟦X⟧) → A'⟦X⟧) (log A) : A'⟦X⟧) : A')
    ((coeff n : (a : A'⟦X⟧) → A') (log A') : A')
have h : Eq.{u_2 + 1} (α := A')
  ((f : (a : A) → A')
      (if n = 0 then 0 else (algebraMap ℚ A : (a : ℚ) → A) (HPow.hPow (α := ℚ) (-1) (n + 1) / (↑n : ℚ)) : A) :
    A')
  (if n = 0 then 0 else (algebraMap ℚ A' : (a : ℚ) → A') (HPow.hPow (α := ℚ) (-1) (n + 1) / (↑n : ℚ)) : A')
Tactic: simp only [coeff_map, coeff_log]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Log (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
A' : Type u_2
inst_2 : CommRing A'
inst_3 : Algebra ℚ A'
f : A →+* A'
n : ℕ
⊢ Eq.{u_2 + 1} (α := A')
    ((f : (a : A) → A')
        (if n = 0 then 0 else (algebraMap ℚ A : (a : ℚ) → A) (HPow.hPow (α := ℚ) (-1) (n + 1) / (↑n : ℚ)) : A) :
      A')
    (if n = 0 then 0 else (algebraMap ℚ A' : (a : ℚ) → A') (HPow.hPow (α := ℚ) (-1) (n + 1) / (↑n : ℚ)) : A')
have pos : n = 0 → Eq.{u_2 + 1} (α := A') ((f : (a : A) → A') 0 : A') (0 : A')
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Log (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
A' : Type u_2
inst_2 : CommRing A'
inst_3 : Algebra ℚ A'
f : A →+* A'
n : ℕ
pos : n = 0 → Eq.{u_2 + 1} (α := A') ((f : (a : A) → A') 0 : A') (0 : A')
⊢ Eq.{u_2 + 1} (α := A')
    ((f : (a : A) → A')
        (if n = 0 then 0 else (algebraMap ℚ A : (a : ℚ) → A) (HPow.hPow (α := ℚ) (-1) (n + 1) / (↑n : ℚ)) : A) :
      A')
    (if n = 0 then 0 else (algebraMap ℚ A' : (a : ℚ) → A') (HPow.hPow (α := ℚ) (-1) (n + 1) / (↑n : ℚ)) : A')
have neg : ¬n = 0 →
  Eq.{u_2 + 1} (α := A')
    ((f : (a : A) → A') ((algebraMap ℚ A : (a : ℚ) → A) (HPow.hPow (α := ℚ) (-1) (n + 1) / (↑n : ℚ)) : A) : A')
    ((algebraMap ℚ A' : (a : ℚ) → A') (HPow.hPow (α := ℚ) (-1) (n + 1) / (↑n : ℚ)) : A')
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Log (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
⊢ Eq (α := A⟦X⟧) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) (log A) : A⟦X⟧)
    (mk fun (n : ℕ) ↦ (algebraMap ℚ A : (a : ℚ) → A) (HPow.hPow (α := ℚ) (-1) n) : A⟦X⟧)
have h : ∀ (n : ℕ),
  Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) (log A) : A⟦X⟧) : A)
    ((coeff n : (a : A⟦X⟧) → A) (mk fun (n : ℕ) ↦ (algebraMap ℚ A : (a : ℚ) → A) (HPow.hPow (α := ℚ) (-1) n)) : A)
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Log (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
⊢ Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) (log A) : A⟦X⟧) : A)
    ((coeff n : (a : A⟦X⟧) → A) (mk fun (n : ℕ) ↦ (algebraMap ℚ A : (a : ℚ) → A) (HPow.hPow (α := ℚ) (-1) n)) : A)
have this : HAdd.hAdd (α := A) (↑n : A) 1 = (algebraMap ℚ A : (a : ℚ) → A) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1)
Tactic: have : (n + 1) = algebraMap ℚ A (n + 1) := by simp
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Log (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
n : ℕ
this : HAdd.hAdd (α := A) (↑n : A) 1 = (algebraMap ℚ A : (a : ℚ) → A) (HAdd.hAdd (α := ℚ) (↑n : ℚ) 1)
⊢ Eq (α := A) ((coeff n : (a : A⟦X⟧) → A) ((d⁄dX A : (a : A⟦X⟧) → A⟦X⟧) (log A) : A⟦X⟧) : A)
    ((coeff n : (a : A⟦X⟧) → A) (mk fun (n : ℕ) ↦ (algebraMap ℚ A : (a : ℚ) → A) (HPow.hPow (α := ℚ) (-1) n)) : A)
have h : HMul.hMul (α := A)
    (if n + 1 = 0 then 0 else (algebraMap ℚ A : (a : ℚ) → A) (HPow.hPow (α := ℚ) (-1) (n + 1 + 1) / (↑(n + 1) : ℚ)) : A)
    (HAdd.hAdd (α := A) (↑n : A) 1) =
  (algebraMap ℚ A : (a : ℚ) → A) (HPow.hPow (α := ℚ) (-1) n)
Tactic: rw [coeff_derivative, coeff_log, coeff_mk]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Log (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
f : A⟦X⟧
hf : Eq (α := A) ((constantCoeff : (a : A⟦X⟧) → A) f : A) (1 : A)
⊢ Eq (α := A) ((constantCoeff : (a : A⟦X⟧) → A) f.logOf : A) (0 : A)
have rw : Eq (α := A) ((constantCoeff : (a : A⟦X⟧) → A) (subst (f - 1) (log A)) : A) (0 : A)
Tactic: rw [logOf_eq]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Log (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
f : A⟦X⟧
hf : Eq (α := A) ((constantCoeff : (a : A⟦X⟧) → A) f : A) (1 : A)
⊢ Eq (α := A) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries Unit A) → A) (f - 1) : A) (0 : A)
have rw : HSub.hSub (α := A) (β := A) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries Unit A) → A) f : A)
    ((MvPowerSeries.constantCoeff : (a : MvPowerSeries Unit A) → A) 1 : A) =
  0
Tactic: rw [map_sub, map_one, ← constantCoeff_eq, hf, sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Log (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
f : A⟦X⟧
hf : Eq (α := A) ((constantCoeff : (a : A⟦X⟧) → A) f : A) (1 : A)
rw :
  HSub.hSub (α := A) (β := A) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries Unit A) → A) f : A)
      ((MvPowerSeries.constantCoeff : (a : MvPowerSeries Unit A) → A) 1 : A) =
    0
⊢ Eq (α := A) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries Unit A) → A) (f - 1) : A) (0 : A)
have rw₁ : HSub.hSub (α := A) (β := A) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries Unit A) → A) f : A) (1 : A) = 0
Tactic: rw [map_sub, map_one, ← constantCoeff_eq, hf, sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Log (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
f : A⟦X⟧
hf : Eq (α := A) ((constantCoeff : (a : A⟦X⟧) → A) f : A) (1 : A)
rw :
  HSub.hSub (α := A) (β := A) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries Unit A) → A) f : A)
      ((MvPowerSeries.constantCoeff : (a : MvPowerSeries Unit A) → A) 1 : A) =
    0
rw₁ : HSub.hSub (α := A) (β := A) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries Unit A) → A) f : A) (1 : A) = 0
⊢ Eq (α := A) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries Unit A) → A) (f - 1) : A) (0 : A)
have rw₂ : HSub.hSub (α := A) (β := A) ((constantCoeff : (a : A⟦X⟧) → A) f : A) (1 : A) = 0
Tactic: rw [map_sub, map_one, ← constantCoeff_eq, hf, sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Log (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
f : A⟦X⟧
hf : Eq (α := A) ((constantCoeff : (a : A⟦X⟧) → A) f : A) (1 : A)
rw :
  HSub.hSub (α := A) (β := A) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries Unit A) → A) f : A)
      ((MvPowerSeries.constantCoeff : (a : MvPowerSeries Unit A) → A) 1 : A) =
    0
rw₁ : HSub.hSub (α := A) (β := A) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries Unit A) → A) f : A) (1 : A) = 0
rw₂ : HSub.hSub (α := A) (β := A) ((constantCoeff : (a : A⟦X⟧) → A) f : A) (1 : A) = 0
⊢ Eq (α := A) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries Unit A) → A) (f - 1) : A) (0 : A)
have rw₃ : HSub.hSub (α := A) 1 1 = 0
Tactic: rw [map_sub, map_one, ← constantCoeff_eq, hf, sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Log (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
f : A⟦X⟧
hf : Eq (α := A) ((constantCoeff : (a : A⟦X⟧) → A) f : A) (1 : A)
rw :
  HSub.hSub (α := A) (β := A) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries Unit A) → A) f : A)
      ((MvPowerSeries.constantCoeff : (a : MvPowerSeries Unit A) → A) 1 : A) =
    0
rw₁ : HSub.hSub (α := A) (β := A) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries Unit A) → A) f : A) (1 : A) = 0
rw₂ : HSub.hSub (α := A) (β := A) ((constantCoeff : (a : A⟦X⟧) → A) f : A) (1 : A) = 0
rw₃ : HSub.hSub (α := A) 1 1 = 0
⊢ Eq (α := A) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries Unit A) → A) (f - 1) : A) (0 : A)
have rw₄ : Eq.{u_1 + 1} (α := A) 0 0
Tactic: rw [map_sub, map_one, ← constantCoeff_eq, hf, sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Log (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
f : A⟦X⟧
hf : Eq (α := A) ((constantCoeff : (a : A⟦X⟧) → A) f : A) (1 : A)
⊢ Eq (α := A) ((constantCoeff : (a : A⟦X⟧) → A) (subst (f - 1) (log A)) : A) (0 : A)
have h : Eq (α := A) ((MvPowerSeries.constantCoeff : (a : MvPowerSeries Unit A) → A) (f - 1) : A) (0 : A)
Tactic: have h : MvPowerSeries.constantCoeff (f - 1 : A⟦X⟧) = 0 := by
    rw [map_sub, map_one, ← constantCoeff_eq, hf, sub_self]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Log (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
⊢ (HAdd.hAdd (α := A⟦X⟧) 1 X).logOf = log A
have rw : subst (HAdd.hAdd (α := A⟦X⟧) 1 X - 1) (log A) = log A
Tactic: rw [logOf_eq, add_sub_cancel_left, X_subst]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Log (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
rw : subst (HAdd.hAdd (α := A⟦X⟧) 1 X - 1) (log A) = log A
⊢ (HAdd.hAdd (α := A⟦X⟧) 1 X).logOf = log A
have rw₁ : subst X (log A) = log A
Tactic: rw [logOf_eq, add_sub_cancel_left, X_subst]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Log (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : Algebra ℚ A
rw : subst (HAdd.hAdd (α := A⟦X⟧) 1 X - 1) (log A) = log A
rw₁ : subst X (log A) = log A
⊢ (HAdd.hAdd (α := A⟦X⟧) 1 X).logOf = log A
have rw₂ : log A = log A
Tactic: rw [logOf_eq, add_sub_cancel_left, X_subst]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.NoZeroDivisors (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ * ψ = 0
⊢ φ = 0 ∨ ψ = 0
have simp_rw : ∀ (h : φ.order + ψ.order = ⊤), φ.order = ⊤ ∨ ψ.order = ⊤
Tactic: simp_rw [← order_eq_top, order_mul] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.NoZeroDivisors (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
this : Eq (α := Ideal R⟦X⟧) (Ideal.span {X}) (RingHom.ker (F := R⟦X⟧ →+* R) constantCoeff)
⊢ Ideal.IsPrime (α := R⟦X⟧) (Ideal.span {X})
have rw : Ideal.IsPrime (RingHom.ker (F := R⟦X⟧ →+* R) constantCoeff)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.NoZeroDivisors (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
⊢ Ideal.IsPrime (α := R⟦X⟧) (Ideal.span {X})
have suffices : Eq (α := Ideal R⟦X⟧) (Ideal.span {X}) (RingHom.ker (F := R⟦X⟧ →+* R) constantCoeff)
Tactic: suffices Ideal.span ({X} : Set R⟦X⟧) = RingHom.ker constantCoeff by
    rw [this]
    exact RingHom.ker_isPrime _
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.NoZeroDivisors (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
⊢ Eq (α := Ideal R⟦X⟧) (Ideal.span {X}) (RingHom.ker (F := R⟦X⟧ →+* R) constantCoeff)
have h : ∀ (x : R⟦X⟧),
  Membership.mem (γ := Ideal R⟦X⟧) (Ideal.span {X}) x ↔
    Membership.mem (γ := Ideal R⟦X⟧) (RingHom.ker (F := R⟦X⟧ →+* R) constantCoeff) x
Tactic: apply Ideal.ext
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.NoZeroDivisors (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
φ : R⟦X⟧
⊢ Membership.mem (γ := Ideal R⟦X⟧) (Ideal.span {X}) φ ↔
    Membership.mem (γ := Ideal R⟦X⟧) (RingHom.ker (F := R⟦X⟧ →+* R) constantCoeff) φ
have h : Membership.mem (γ := Ideal R⟦X⟧) (Ideal.span {X}) φ ↔ Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
Tactic: rw [RingHom.mem_ker, Ideal.mem_span_singleton, X_dvd_iff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.NoZeroDivisors (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
φ : R⟦X⟧
h : Membership.mem (γ := Ideal R⟦X⟧) (Ideal.span {X}) φ ↔ Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ Membership.mem (γ := Ideal R⟦X⟧) (Ideal.span {X}) φ ↔
    Membership.mem (γ := Ideal R⟦X⟧) (RingHom.ker (F := R⟦X⟧ →+* R) constantCoeff) φ
have h₁ : X ∣ φ ↔ Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
Tactic: rw [RingHom.mem_ker, Ideal.mem_span_singleton, X_dvd_iff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.NoZeroDivisors (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
φ : R⟦X⟧
h : Membership.mem (γ := Ideal R⟦X⟧) (Ideal.span {X}) φ ↔ Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
h₁ : X ∣ φ ↔ Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ Membership.mem (γ := Ideal R⟦X⟧) (Ideal.span {X}) φ ↔
    Membership.mem (γ := Ideal R⟦X⟧) (RingHom.ker (F := R⟦X⟧ →+* R) constantCoeff) φ
have h₂ : Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R) ↔
  Eq (α := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) (0 : R)
Tactic: rw [RingHom.mem_ker, Ideal.mem_span_singleton, X_dvd_iff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.NoZeroDivisors (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
⊢ Prime.{u_1} (M := R⟦X⟧) X
have rw : Ideal.IsPrime (α := R⟦X⟧) (Ideal.span {X})
Tactic: rw [← Ideal.span_singleton_prime]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.NoZeroDivisors (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
rw : Ideal.IsPrime (α := R⟦X⟧) (Ideal.span {X})
⊢ Prime.{u_1} (M := R⟦X⟧) X
have rw₁ : Ne.{u_1 + 1} (α := R⟦X⟧) X 0
Tactic: rw [← Ideal.span_singleton_prime]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.NoZeroDivisors (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
a : R
ha : a ≠ 0
p q : R⟦X⟧
h : Eq (α := R⟦X⟧) ((rescale a : (a : R⟦X⟧) → R⟦X⟧) p : R⟦X⟧) ((rescale a : (a : R⟦X⟧) → R⟦X⟧) q : R⟦X⟧)
⊢ p = q
have rw : ∀
  (h :
    ∀ (n : ℕ),
      Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((rescale a : (a : R⟦X⟧) → R⟦X⟧) p : R⟦X⟧) : R)
        ((coeff n : (a : R⟦X⟧) → R) ((rescale a : (a : R⟦X⟧) → R⟦X⟧) q : R⟦X⟧) : R))
  (n : ℕ), Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) p : R) ((coeff n : (a : R⟦X⟧) → R) q : R)
Tactic: rw [PowerSeries.ext_iff] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.NoZeroDivisors (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
a : R
ha : a ≠ 0
p q : R⟦X⟧
h :
  ∀ (n : ℕ),
    Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((rescale a : (a : R⟦X⟧) → R⟦X⟧) p : R⟦X⟧) : R)
      ((coeff n : (a : R⟦X⟧) → R) ((rescale a : (a : R⟦X⟧) → R⟦X⟧) q : R⟦X⟧) : R)
n : ℕ
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) p : R) ((coeff n : (a : R⟦X⟧) → R) q : R)
have h₁ : Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((rescale a : (a : R⟦X⟧) → R⟦X⟧) p : R⟦X⟧) : R)
  ((coeff n : (a : R⟦X⟧) → R) ((rescale a : (a : R⟦X⟧) → R⟦X⟧) q : R⟦X⟧) : R)
Tactic: specialize h n
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.NoZeroDivisors (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
a : R
ha : a ≠ 0
p q : R⟦X⟧
n : ℕ
h :
  Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((rescale a : (a : R⟦X⟧) → R⟦X⟧) p : R⟦X⟧) : R)
    ((coeff n : (a : R⟦X⟧) → R) ((rescale a : (a : R⟦X⟧) → R⟦X⟧) q : R⟦X⟧) : R)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) p : R) ((coeff n : (a : R⟦X⟧) → R) q : R)
have rwa : ∀
  (h :
    HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) p : R) =
      (coeff n : (a : R⟦X⟧) → R) ((rescale a : (a : R⟦X⟧) → R⟦X⟧) q : R⟦X⟧)),
  Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) p : R) ((coeff n : (a : R⟦X⟧) → R) q : R)
Tactic: rwa [coeff_rescale, coeff_rescale, mul_right_inj' <| pow_ne_zero _ ha] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.NoZeroDivisors (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
a : R
ha : a ≠ 0
p q : R⟦X⟧
n : ℕ
h :
  Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((rescale a : (a : R⟦X⟧) → R⟦X⟧) p : R⟦X⟧) : R)
    ((coeff n : (a : R⟦X⟧) → R) ((rescale a : (a : R⟦X⟧) → R⟦X⟧) q : R⟦X⟧) : R)
rwa :
  ∀
    (h :
      HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) p : R) =
        (coeff n : (a : R⟦X⟧) → R) ((rescale a : (a : R⟦X⟧) → R⟦X⟧) q : R⟦X⟧)),
    Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) p : R) ((coeff n : (a : R⟦X⟧) → R) q : R)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) p : R) ((coeff n : (a : R⟦X⟧) → R) q : R)
have rwa₁ : ∀
  (h :
    HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) p : R) =
      HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) q : R)),
  Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) p : R) ((coeff n : (a : R⟦X⟧) → R) q : R)
Tactic: rwa [coeff_rescale, coeff_rescale, mul_right_inj' <| pow_ne_zero _ ha] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.NoZeroDivisors (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
a : R
ha : a ≠ 0
p q : R⟦X⟧
n : ℕ
h :
  Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) ((rescale a : (a : R⟦X⟧) → R⟦X⟧) p : R⟦X⟧) : R)
    ((coeff n : (a : R⟦X⟧) → R) ((rescale a : (a : R⟦X⟧) → R⟦X⟧) q : R⟦X⟧) : R)
rwa :
  ∀
    (h :
      HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) p : R) =
        (coeff n : (a : R⟦X⟧) → R) ((rescale a : (a : R⟦X⟧) → R⟦X⟧) q : R⟦X⟧)),
    Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) p : R) ((coeff n : (a : R⟦X⟧) → R) q : R)
rwa₁ :
  ∀
    (h :
      HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) p : R) =
        HMul.hMul (β := R) (a ^ n) ((coeff n : (a : R⟦X⟧) → R) q : R)),
    Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) p : R) ((coeff n : (a : R⟦X⟧) → R) q : R)
⊢ Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) p : R) ((coeff n : (a : R⟦X⟧) → R) q : R)
have rwa₂ : ∀ (h : Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) p : R) ((coeff n : (a : R⟦X⟧) → R) q : R)),
  Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) p : R) ((coeff n : (a : R⟦X⟧) → R) q : R)
Tactic: rwa [coeff_rescale, coeff_rescale, mul_right_inj' <| pow_ne_zero _ ha] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
⊢ (∃ (n : ℕ), Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) ↔ φ ≠ 0
have contrapose! : (∀ (n : ℕ), Eq (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) ↔ φ = 0
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
⊢ LT.lt (α := ℕ∞)
      (if h : φ = 0 then ⊤
      else (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) ⋯) : ℕ∞))
      ⊤ ↔
    φ ≠ 0
have pos : ∀ (h : φ = 0), LT.lt (α := ℕ∞) ⊤ ⊤ ↔ φ ≠ 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
pos : ∀ (h : φ = 0), LT.lt (α := ℕ∞) ⊤ ⊤ ↔ φ ≠ 0
⊢ LT.lt (α := ℕ∞)
      (if h : φ = 0 then ⊤
      else (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) ⋯) : ℕ∞))
      ⊤ ↔
    φ ≠ 0
have neg : ∀ (h : ¬φ = 0),
  LT.lt (α := ℕ∞) (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) sorry) : ℕ∞) ⊤ ↔
    φ ≠ 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
hf : φ ≠ 0
⊢ (↑φ.order.toNat : ℕ∞) = φ.order
have rw : φ.order = φ.order
Tactic: rw [ENat.coe_toNat_eq_self.mpr (order_eq_top.not.mpr hf)]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
h : φ ≠ 0
⊢ Ne (α := R) ((coeff φ.order.toNat : (a : R⟦X⟧) → R) φ : R) (0 : R)
have simp : Ne (α := R)
  ((coeff
          (ENat.toNat
            (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) sorry) : ℕ∞)) :
        (a : R⟦X⟧) → R)
      φ :
    R)
  (0 : R)
Tactic: simp only [order, h, not_false_iff, dif_neg]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
h : φ ≠ 0
⊢ Ne (α := R)
    ((coeff
            (ENat.toNat
              (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) ⋯) : ℕ∞)) :
          (a : R⟦X⟧) → R)
        φ :
      R)
    (0 : R)
have generalize_proofs : ∀ (h : ∃ (n : ℕ), Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)),
  Ne (α := R)
    ((coeff
            (ENat.toNat
              (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) h) : ℕ∞)) :
          (a : R⟦X⟧) → R)
        φ :
      R)
    (0 : R)
Tactic: generalize_proofs h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
h : φ ≠ 0
⊢ Ne (α := R) ((coeff φ.order.toNat : (a : R⟦X⟧) → R) φ : R) (0 : R)
have simp : Ne (α := R)
  ((coeff
          (ENat.toNat
            (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) sorry) : ℕ∞)) :
        (a : R⟦X⟧) → R)
      φ :
    R)
  (0 : R)
Tactic: classical
  simp only [order, h, not_false_iff, dif_neg]
  generalize_proofs h
  exact Nat.find_spec h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
h : φ ≠ 0
simp :
  Ne (α := R)
    ((coeff
            (ENat.toNat
              (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) ⋯) : ℕ∞)) :
          (a : R⟦X⟧) → R)
        φ :
      R)
    (0 : R)
⊢ Ne (α := R) ((coeff φ.order.toNat : (a : R⟦X⟧) → R) φ : R) (0 : R)
have simp₁ : ∀ (h : ∃ (n : ℕ), Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)),
  Ne (α := R)
    ((coeff
            (ENat.toNat
              (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) h) : ℕ∞)) :
          (a : R⟦X⟧) → R)
        φ :
      R)
    (0 : R)
Tactic: classical
  simp only [order, h, not_false_iff, dif_neg]
  generalize_proofs h
  exact Nat.find_spec h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
h : Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ φ.order ≤ (↑n : ℕ∞)
have rw : LE.le (α := ℕ∞) (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) sorry) : ℕ∞)
  (↑n : ℕ∞)
Tactic: rw [order, dif_neg]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
h : Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)
rw :
  LE.le (α := ℕ∞) (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) ⋯) : ℕ∞)
    (↑n : ℕ∞)
⊢ φ.order ≤ (↑n : ℕ∞)
have hnc : ¬φ = 0
Tactic: rw [order, dif_neg]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Order (goal)
Goal:
R : Type u_1
inst : Semiring R
φ : R⟦X⟧
n : ℕ
h : Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)
⊢ φ.order ≤ (↑n : ℕ∞)
have rw : LE.le (α := ℕ∞)
  (if h : φ = 0 then ⊤
  else (↑(Nat.find (p := fun (n : ℕ) ↦ Ne (α := R) ((coeff n : (a : R⟦X⟧) → R) φ : R) (0 : R)) sorry) : ℕ∞))
  (↑n : ℕ∞)
Tactic: classical
  rw [order, dif_neg]
  · simpa using ⟨n, le_rfl, h⟩
  · exact exists_coeff_ne_zero_iff_ne_zero.mp ⟨n, h⟩