awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst : Zero R
inst_1 : PartialOrder Γ
inst_2 : DecidableLT Γ
c : Γ
⊢ Eq (α := R⟦Γ⟧) { coeff := fun (i : Γ) ↦ if i < c then coeff 0 i else 0, isPWO_support' := ⋯ } 0
have coeff : ∀ (x : Γ),
  Eq.{u_3 + 1} (α := R) (coeff { coeff := fun (i : Γ) ↦ if i < c then coeff 0 i else 0, isPWO_support' := sorry } x)
    (coeff 0 x)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : PartialOrder Γ
inst_2 : DecidableLT Γ
c : Γ
x : R⟦Γ⟧
⊢ support.{u_1, u_3} (R := R) ((truncLT c : (a : R⟦Γ⟧) → R⟦Γ⟧) x) ⊆ x.support
have rw : {y : Γ | y ∈ x.support ∧ y < c} ⊆ x.support
Tactic: rw [support_truncLT]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Binomial (goal)
Goal:
Γ : Type u_1
R : Type u_2
A : Type u_3
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
inst_5 : CommRing A
inst_6 : Algebra R A
x : A⟦Γ⟧
hx : ¬0 < (x - 1).orderTop
r : R
n : ℕ
⊢ (binomialFamily x r : (a : ℕ) → A⟦Γ⟧) n = HPow.hPow (α := A⟦Γ⟧) 0 n
have rw : (powerSeriesFamily 0 (PowerSeries.binomialSeries A r) : (a : ℕ) → A⟦Γ⟧) n = HPow.hPow (α := A⟦Γ⟧) 0 n
Tactic: rw [binomialFamily, powerSeriesFamily_of_not_orderTop_pos hx]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Binomial (goal)
Goal:
Γ : Type u_1
R : Type u_2
A : Type u_3
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
inst_5 : CommRing A
inst_6 : Algebra R A
x : A⟦Γ⟧
hx : ¬0 < (x - 1).orderTop
r : R
n : ℕ
⊢ (powerSeriesFamily 0 (PowerSeries.binomialSeries A r) : (a : ℕ) → A⟦Γ⟧) n = HPow.hPow (α := A⟦Γ⟧) 0 n
have pos : ∀ (hn : n = 0), (powerSeriesFamily 0 (PowerSeries.binomialSeries A r) : (a : ℕ) → A⟦Γ⟧) n = HPow.hPow (α := A⟦Γ⟧) 0 n
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Binomial (goal)
Goal:
Γ : Type u_1
R : Type u_2
A : Type u_3
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
inst_5 : CommRing A
inst_6 : Algebra R A
x : A⟦Γ⟧
hx : ¬0 < (x - 1).orderTop
r : R
n : ℕ
pos :
  ∀ (hn : n = 0), (powerSeriesFamily 0 (PowerSeries.binomialSeries A r) : (a : ℕ) → A⟦Γ⟧) n = HPow.hPow (α := A⟦Γ⟧) 0 n
⊢ (powerSeriesFamily 0 (PowerSeries.binomialSeries A r) : (a : ℕ) → A⟦Γ⟧) n = HPow.hPow (α := A⟦Γ⟧) 0 n
have neg : ∀ (hn : ¬n = 0), (powerSeriesFamily 0 (PowerSeries.binomialSeries A r) : (a : ℕ) → A⟦Γ⟧) n = HPow.hPow (α := A⟦Γ⟧) 0 n
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Binomial (goal)
Goal:
Γ : Type u_1
R : Type u_2
A : Type u_3
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
inst_5 : CommRing A
inst_6 : Algebra R A
x : A⟦Γ⟧
hx : 0 < (x - 1).orderTop
r : R
n : ℕ
hn : 0 < n
⊢ LT.lt.{u_1} (α := WithTop Γ) 0 (orderTop.{u_1, u_3} (R := A) ((binomialFamily x r : (a : ℕ) → A⟦Γ⟧) n))
have simp : 0 < (Ring.choose r n • (x - 1) ^ n).orderTop
Tactic: simp only [binomialFamily, smulFamily_toFun, PowerSeries.binomialSeries_coeff, powers_toFun, hx,
    ↓reduceIte, smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Binomial (hypothesis)
Goal:
Γ : Type u_1
R : Type u_2
A : Type u_3
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
inst_5 : CommRing A
inst_6 : Algebra R A
x : A⟦Γ⟧
hx : 0 < (x - 1).orderTop
r : R
n : ℕ
hn : 0 < n
⊢ 0 < (Ring.choose r n • (x - 1) ^ n).orderTop
have this : n ≠ 0
Tactic: have : n ≠ 0 := by exact Nat.ne_zero_of_lt hn
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Binomial (goal)
Goal:
Γ : Type u_1
R : Type u_2
A : Type u_3
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
inst_5 : CommRing A
inst_6 : Algebra R A
x : A⟦Γ⟧
hx : 0 < (x - 1).orderTop
r : R
n : ℕ
g : Γ
hg : Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := A) ((binomialFamily x r : (a : ℕ) → A⟦Γ⟧) n)) g
⊢ 0 ≤ g
have pos : ∀ (hn : n = 0), 0 ≤ g
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Binomial (goal)
Goal:
Γ : Type u_1
R : Type u_2
A : Type u_3
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
inst_5 : CommRing A
inst_6 : Algebra R A
x : A⟦Γ⟧
hx : 0 < (x - 1).orderTop
r : R
n : ℕ
g : Γ
hg : Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := A) ((binomialFamily x r : (a : ℕ) → A⟦Γ⟧) n)) g
pos : ∀ (hn : n = 0), 0 ≤ g
⊢ 0 ≤ g
have neg : ∀ (hn : ¬n = 0), 0 ≤ g
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Binomial (goal)
Goal:
Γ : Type u_1
R : Type u_2
A : Type u_3
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
inst_5 : CommRing A
inst_6 : Algebra R A
x : A⟦Γ⟧
hx : 0 < (x - 1).orderTop
r : R
⊢ 0 < ((binomialFamily x r).hsum - 1).orderTop
have inl : Subsingleton A → 0 < ((binomialFamily x r).hsum - 1).orderTop
Tactic: obtain (_ | _) := subsingleton_or_nontrivial A
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Binomial (goal)
Goal:
Γ : Type u_1
R : Type u_2
A : Type u_3
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
inst_5 : CommRing A
inst_6 : Algebra R A
x : A⟦Γ⟧
hx : 0 < (x - 1).orderTop
r : R
inl : Subsingleton A → 0 < ((binomialFamily x r).hsum - 1).orderTop
⊢ 0 < ((binomialFamily x r).hsum - 1).orderTop
have inr : Nontrivial A → 0 < ((binomialFamily x r).hsum - 1).orderTop
Tactic: obtain (_ | _) := subsingleton_or_nontrivial A
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Binomial (goal)
Goal:
Γ : Type u_1
R : Type u_2
A : Type u_3
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
inst_5 : CommRing A
inst_6 : Algebra R A
x : A⟦Γ⟧
hx : 0 < (x - 1).orderTop
r : R
h : Nontrivial A
⊢ 0 < ((binomialFamily x r).hsum - 1).orderTop
have inr : (binomialFamily x r).hsum.orderTop = 0 ∧ (binomialFamily x r).hsum.leadingCoeff = 1
Tactic: refine (orderTop_self_sub_one_pos_iff (binomialFamily x r).hsum).mpr ?_
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Binomial (goal)
Goal:
Γ : Type u_1
R : Type u_2
A : Type u_3
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
inst_5 : CommRing A
inst_6 : Algebra R A
x : A⟦Γ⟧
hx : 0 < (x - 1).orderTop
r : R
h : Nontrivial A
⊢ (binomialFamily x r).hsum.orderTop = 0 ∧ (binomialFamily x r).hsum.leadingCoeff = 1
have inr : (binomialFamily x r).hsum.orderTop = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Binomial (goal)
Goal:
Γ : Type u_1
R : Type u_2
A : Type u_3
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
inst_5 : CommRing A
inst_6 : Algebra R A
x : A⟦Γ⟧
hx : 0 < (x - 1).orderTop
r : R
h : Nontrivial A
inr : (binomialFamily x r).hsum.orderTop = 0
⊢ (binomialFamily x r).hsum.orderTop = 0 ∧ (binomialFamily x r).hsum.leadingCoeff = 1
have inr₁ : (binomialFamily x r).hsum.leadingCoeff = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Binomial (hypothesis)
Goal:
Γ : Type u_1
R : Type u_2
A : Type u_3
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
inst_5 : CommRing A
inst_6 : Algebra R A
x : A⟦Γ⟧
hx : 0 < (x - 1).orderTop
r : R
h : Nontrivial A
⊢ (binomialFamily x r).hsum.leadingCoeff = 1
have this : Eq (α := A) (HahnSeries.coeff.{u_1, u_3} (Γ := Γ) ((binomialFamily x r : (a : ℕ) → A⟦Γ⟧) 0) 0 : A) (1 : A)
Tactic: have : (binomialFamily x r 0).coeff 0 = 1 := by simp [hx]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Binomial (goal)
Goal:
Γ : Type u_1
R : Type u_2
A : Type u_3
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
inst_5 : CommRing A
inst_6 : Algebra R A
x : A⟦Γ⟧
hx : 0 < (x - 1).orderTop
r : R
h : Nontrivial A
this : Eq (α := A) (HahnSeries.coeff.{u_1, u_3} (Γ := Γ) ((binomialFamily x r : (a : ℕ) → A⟦Γ⟧) 0) 0 : A) (1 : A)
⊢ (binomialFamily x r).hsum.leadingCoeff = 1
have inr : (binomialFamily x r).hsum.leadingCoeff =
  HahnSeries.coeff.{u_1, u_3} (Γ := Γ) ((binomialFamily x r : (a : ℕ) → A⟦Γ⟧) 0) 0
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Binomial (goal)
Goal:
Γ : Type u_1
R : Type u_2
A : Type u_3
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
inst_5 : CommRing A
inst_6 : Algebra R A
x : A⟦Γ⟧
hx : 0 < (x - 1).orderTop
r : R
h : Nontrivial A
this : Eq (α := A) (HahnSeries.coeff.{u_1, u_3} (Γ := Γ) ((binomialFamily x r : (a : ℕ) → A⟦Γ⟧) 0) 0 : A) (1 : A)
⊢ (binomialFamily x r).hsum.leadingCoeff =
    HahnSeries.coeff.{u_1, u_3} (Γ := Γ) ((binomialFamily x r : (a : ℕ) → A⟦Γ⟧) 0) 0
have inr : ∀ (b : ℕ) (g' : Γ),
  Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := A) ((binomialFamily x r : (a : ℕ) → A⟦Γ⟧) b)) g' → 0 ≤ g'
Tactic: refine hsum_leadingCoeff_of_le (g := 0) (a := 0) (by simp [hx]) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Binomial (goal)
Goal:
Γ : Type u_1
R : Type u_2
A : Type u_3
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
inst_5 : CommRing A
inst_6 : Algebra R A
x : A⟦Γ⟧
hx : 0 < (x - 1).orderTop
r : R
h : Nontrivial A
this : Eq (α := A) (HahnSeries.coeff.{u_1, u_3} (Γ := Γ) ((binomialFamily x r : (a : ℕ) → A⟦Γ⟧) 0) 0 : A) (1 : A)
inr :
  ∀ (b : ℕ) (g' : Γ),
    Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := A) ((binomialFamily x r : (a : ℕ) → A⟦Γ⟧) b)) g' → 0 ≤ g'
⊢ (binomialFamily x r).hsum.leadingCoeff =
    HahnSeries.coeff.{u_1, u_3} (Γ := Γ) ((binomialFamily x r : (a : ℕ) → A⟦Γ⟧) 0) 0
have inr₁ : ∀ (b : ℕ),
  b ≠ 0 → Eq.{u_3 + 1} (α := A) (HahnSeries.coeff.{u_1, u_3} (Γ := Γ) ((binomialFamily x r : (a : ℕ) → A⟦Γ⟧) b) 0) 0
Tactic: refine hsum_leadingCoeff_of_le (g := 0) (a := 0) (by simp [hx]) ?_ ?_
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Binomial (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
x : ↥(orderTopSubOnePos Γ R)
r s : R
⊢ x ^ (r + s) = x ^ r * x ^ s
have suffices : (↑(x ^ (r + s)) : R⟦Γ⟧ˣ) = (↑(x ^ r * x ^ s) : R⟦Γ⟧ˣ)
Tactic: suffices (x ^ (r + s)).val = (x ^ r * x ^ s).val by exact SetLike.coe_eq_coe.mp this
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Binomial (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
x : ↥(orderTopSubOnePos Γ R)
r s : R
⊢ (↑(x ^ (r + s)) : R⟦Γ⟧ˣ) = (↑(x ^ r * x ^ s) : R⟦Γ⟧ˣ)
have suffices : (↑(↑(x ^ (r + s)) : R⟦Γ⟧ˣ) : R⟦Γ⟧) = (↑(↑(x ^ r * x ^ s) : R⟦Γ⟧ˣ) : R⟦Γ⟧)
Tactic: suffices (x ^ (r + s)).val.val = (x ^ r * x ^ s).val.val by exact Units.val_inj.mp this
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Binomial (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
g : Γ
hg : 0 < g
r s : R
k : ℕ
⊢ (↑(↑(HPow.hPow (α := ↥(orderTopSubOnePos Γ R))
                  (toOrderTopSubOnePos (x :=
                    HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) (1 : R⟦Γ⟧) ((single g : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)) ⋯)
                  s) :
              R⟦Γ⟧ˣ) :
          R⟦Γ⟧).coeff
      (k • g) =
    Ring.choose s k • r ^ k
have simp : ∑ᶠ (i : ℕ),
    coeff
      ((binomialFamily (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) (1 : R⟦Γ⟧) ((single g : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)) s :
          (a : ℕ) → R⟦Γ⟧)
        i)
      (k • g) =
  Ring.choose s k * r ^ k
Tactic: simp only [val_toOrderTopSubOnePos_coe, binomial_power, coeff_hsum, smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Binomial (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
g : Γ
hg : 0 < g
r s : R
k : ℕ
⊢ ∑ᶠ (i : ℕ),
      coeff
        ((binomialFamily (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) (1 : R⟦Γ⟧) ((single g : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)) s :
            (a : ℕ) → R⟦Γ⟧)
          i)
        (k • g) =
    Ring.choose s k * r ^ k
have rw : ∀ (x : ℕ),
  x ≠ k →
    Eq.{u_2 + 1} (α := R)
      (coeff
        ((binomialFamily (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) (1 : R⟦Γ⟧) ((single g : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)) s :
            (a : ℕ) → R⟦Γ⟧)
          x)
        (k • g))
      0
Tactic: rw [finsum_eq_single _ k, binomialFamily_apply (orderTop_sub_pos hg r), add_sub_cancel_left,
    single_pow, coeff_smul, coeff_single_same (k • g) (r ^ k), smul_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Binomial (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
g : Γ
hg : 0 < g
r s : R
k n : ℕ
hn : n ≠ k
⊢ Eq.{u_2 + 1} (α := R)
    (coeff
      ((binomialFamily (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) (1 : R⟦Γ⟧) ((single g : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)) s :
          (a : ℕ) → R⟦Γ⟧)
        n)
      (k • g))
    0
have rw : k • g ≠ n • g
Tactic: rw [binomialFamily_apply, add_sub_cancel_left, coeff_smul, single_pow, coeff_single_of_ne,
    smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Binomial (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
g : Γ
hg : 0 < g
r s : R
k n : ℕ
hn : n ≠ k
rw : k • g ≠ n • g
⊢ Eq.{u_2 + 1} (α := R)
    (coeff
      ((binomialFamily (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) (1 : R⟦Γ⟧) ((single g : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)) s :
          (a : ℕ) → R⟦Γ⟧)
        n)
      (k • g))
    0
have hx : 0 < (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) (1 : R⟦Γ⟧) ((single g : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) - 1).orderTop
Tactic: rw [binomialFamily_apply, add_sub_cancel_left, coeff_smul, single_pow, coeff_single_of_ne,
    smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Binomial (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
g : Γ
hg : 0 < g
r s : R
k n : ℕ
hn : n ≠ k
⊢ k • g ≠ n • g
have contrapose : ∀ (hn : k • g = n • g), n = k
Tactic: contrapose hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Binomial (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
g : Γ
hg : 0 < g
r s : R
k n : ℕ
hn : n ≠ k
⊢ 0 < (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) (1 : R⟦Γ⟧) ((single g : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) - 1).orderTop
have pos : ∀ (hr : r = 0), 0 < (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) (1 : R⟦Γ⟧) ((single g : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) - 1).orderTop
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Binomial (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : BinomialRing R
g : Γ
hg : 0 < g
r s : R
k n : ℕ
hn : n ≠ k
pos :
  ∀ (hr : r = 0), 0 < (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) (1 : R⟦Γ⟧) ((single g : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) - 1).orderTop
⊢ 0 < (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) (1 : R⟦Γ⟧) ((single g : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) - 1).orderTop
have neg : ∀ (hr : ¬r = 0), 0 < (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) (1 : R⟦Γ⟧) ((single g : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) - 1).orderTop
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Cardinal (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : PartialOrder Γ
inst_1 : Zero R
a : Γ
r : R
h : r ≠ 0
⊢ cardSupp.{u_1, u_2} (Γ := Γ) (R := R) ((single a : (a : R) → R⟦Γ⟧) r) = 1
have rw : #(↑(support.{u_1, u_2} (R := R) ((single a : (a : R) → R⟦Γ⟧) r)) : Type u_1) = 1
Tactic: rw [cardSupp, support_single_of_ne h, mk_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Cardinal (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : PartialOrder Γ
inst_1 : Zero R
a : Γ
r : R
h : r ≠ 0
rw : #(↑(support.{u_1, u_2} (R := R) ((single a : (a : R) → R⟦Γ⟧) r)) : Type u_1) = 1
⊢ cardSupp.{u_1, u_2} (Γ := Γ) (R := R) ((single a : (a : R) → R⟦Γ⟧) r) = 1
have rw₁ : #(↑{a} : Type u_1) = 1
Tactic: rw [cardSupp, support_single_of_ne h, mk_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Cardinal (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : PartialOrder Γ
inst_1 : Zero R
a : Γ
r : R
h : r ≠ 0
rw : #(↑(support.{u_1, u_2} (R := R) ((single a : (a : R) → R⟦Γ⟧) r)) : Type u_1) = 1
rw₁ : #(↑{a} : Type u_1) = 1
⊢ cardSupp.{u_1, u_2} (Γ := Γ) (R := R) ((single a : (a : R) → R⟦Γ⟧) r) = 1
have rw₂ : Eq.{u_1 + 2} (α := Cardinal.{u_1}) 1 1
Tactic: rw [cardSupp, support_single_of_ne h, mk_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Cardinal (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : PartialOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
x : R⟦Γ⟧
n : ℕ
⊢ (x ^ n).cardSupp ≤ x.cardSupp ^ n
have zero : (HPow.hPow (β := ℕ) x 0).cardSupp ≤ HPow.hPow (β := ℕ) x.cardSupp 0
Tactic: induction n with
  | zero => simp
  | succ n IH =>
    simpa [pow_succ] using (cardSupp_mul_le ..).trans <| mul_le_mul_left IH _
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Cardinal (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : PartialOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
x : R⟦Γ⟧
n : ℕ
zero : (HPow.hPow (β := ℕ) x 0).cardSupp ≤ HPow.hPow (β := ℕ) x.cardSupp 0
⊢ (x ^ n).cardSupp ≤ x.cardSupp ^ n
have succ : ∀ (n : ℕ) (IH : (x ^ n).cardSupp ≤ x.cardSupp ^ n), (x ^ (n + 1)).cardSupp ≤ x.cardSupp ^ (n + 1)
Tactic: induction n with
  | zero => simp
  | succ n IH =>
    simpa [pow_succ] using (cardSupp_mul_le ..).trans <| mul_le_mul_left IH _
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Cardinal (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
⊢ (SummableFamily.powers x).hsum.cardSupp ≤ max ℵ₀ x.cardSupp
have H : ∀ (i : ℕ), cardSupp.{u_1, u_2} (Γ := Γ) (R := R) ((SummableFamily.powers x : (a : ℕ) → R⟦Γ⟧) i) ≤ x.cardSupp ^ i
Tactic: grw [← lift_uzero (cardSupp _), ← sum_pow_le_max_aleph0, cardSupp_hsum_le, sum_le_sum]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Cardinal (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
i : ℕ
⊢ ((if 0 < x.orderTop then x else 0) ^ i).cardSupp ≤ x.cardSupp ^ i
have pos : 0 < x.orderTop → (x ^ i).cardSupp ≤ x.cardSupp ^ i
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Cardinal (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
i : ℕ
pos : 0 < x.orderTop → (x ^ i).cardSupp ≤ x.cardSupp ^ i
⊢ ((if 0 < x.orderTop then x else 0) ^ i).cardSupp ≤ x.cardSupp ^ i
have neg : ¬0 < x.orderTop → (HPow.hPow (α := R⟦Γ⟧) 0 i).cardSupp ≤ x.cardSupp ^ i
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Cardinal (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
i : ℕ
h : ¬0 < x.orderTop
⊢ (HPow.hPow (α := R⟦Γ⟧) 0 i).cardSupp ≤ x.cardSupp ^ i
have neg : (HPow.hPow (α := R⟦Γ⟧) (β := ℕ) 0 0).cardSupp ≤ HPow.hPow (β := ℕ) x.cardSupp 0
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Cardinal (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
i : ℕ
h : ¬0 < x.orderTop
neg : (HPow.hPow (α := R⟦Γ⟧) (β := ℕ) 0 0).cardSupp ≤ HPow.hPow (β := ℕ) x.cardSupp 0
⊢ (HPow.hPow (α := R⟦Γ⟧) 0 i).cardSupp ≤ x.cardSupp ^ i
have neg₁ : ∀ (n : ℕ), (HPow.hPow (α := R⟦Γ⟧) 0 (n + 1)).cardSupp ≤ x.cardSupp ^ (n + 1)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Cardinal (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : AddCommGroup Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
x : R⟦Γ⟧
⊢ x⁻¹.cardSupp ≤ max ℵ₀ x.cardSupp
have inl : cardSupp.{u_1, u_2} (Γ := Γ) (R := R) 0⁻¹ ≤ max ℵ₀ (cardSupp.{u_1, u_2} (Γ := Γ) (R := R) 0)
Tactic: obtain rfl | hx := eq_or_ne x 0
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Cardinal (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : AddCommGroup Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
x : R⟦Γ⟧
inl : cardSupp.{u_1, u_2} (Γ := Γ) (R := R) 0⁻¹ ≤ max ℵ₀ (cardSupp.{u_1, u_2} (Γ := Γ) (R := R) 0)
⊢ x⁻¹.cardSupp ≤ max ℵ₀ x.cardSupp
have inr : ∀ (hx : x ≠ 0), x⁻¹.cardSupp ≤ max ℵ₀ x.cardSupp
Tactic: obtain rfl | hx := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Cardinal (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : AddCommGroup Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
x : R⟦Γ⟧
hx : x ≠ 0
⊢ x⁻¹.cardSupp ≤ max ℵ₀ x.cardSupp
have apply : max ℵ₀ (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x).cardSupp ≤
  max ℵ₀ x.cardSupp
Tactic: apply (cardSupp_single_mul_le ..).trans <| (cardSupp_hsum_powers_le ..).trans _
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Cardinal (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : AddCommGroup Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
x : R⟦Γ⟧
hx : x ≠ 0
⊢ max ℵ₀ (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x).cardSupp ≤
    max ℵ₀ x.cardSupp
have h₂ : (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x).cardSupp ≤ x.cardSupp
Tactic: gcongr
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Cardinal (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : AddCommGroup Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
x : R⟦Γ⟧
hx : x ≠ 0
⊢ (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x).cardSupp ≤ x.cardSupp
have h₂ : ∀ x_1 ∈ (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x).support,
  x_1 ∈ (HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x).support
Tactic: refine (cardSupp_single_mul_le _ (-x.order) x.leadingCoeff⁻¹).trans' <| cardSupp_mono fun _ ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.HEval (goal)
Goal:
Γ : Type u_1
R : Type u_3
V : Type u_4
inst : AddCommMonoid Γ
inst_1 : LinearOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
inst_4 : CommRing V
inst_5 : Algebra R V
x : V⟦Γ⟧
hx : ¬0 < x.orderTop
f : PowerSeries R
⊢ powerSeriesFamily x f = powerSeriesFamily 0 f
have h : ∀ (n : ℕ) (g : Γ),
  Eq.{u_4 + 1} (α := V) (HahnSeries.coeff ((powerSeriesFamily x f : (a : ℕ) → V⟦Γ⟧) n) g)
    (HahnSeries.coeff ((powerSeriesFamily 0 f : (a : ℕ) → V⟦Γ⟧) n) g)
Tactic: ext n g