awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
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
neg : ∀ (hn : ¬n = 0), 0 ≤ g
⊢ 0 ≤ g

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
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
hn : n = 0
⊢ 0 ≤ g

Tactic:
simp_all
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
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
hn : ¬n = 0
⊢ 0 ≤ g

Tactic:
le_of_lt (WithTop.coe_pos.mp (lt_of_lt_of_le (binomialFamily_orderTop_pos hx r
    (Nat.pos_of_ne_zero hn)) (orderTop_le_of_coeff_ne_zero hg)))

Premises used: HahnSeries.SummableFamily.binomialFamily_orderTop_pos, le_of_lt, HahnSeries.orderTop_le_of_coeff_ne_zero, Nat.pos_of_ne_zero, Iff.mp, WithTop.coe_pos, lt_of_lt_of_le
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
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
hn : ¬n = 0
⊢ 0 ≤ g

Tactic:
exact le_of_lt (WithTop.coe_pos.mp (lt_of_lt_of_le (binomialFamily_orderTop_pos hx r
    (Nat.pos_of_ne_zero hn)) (orderTop_le_of_coeff_ne_zero hg)))

Premises used: HahnSeries.SummableFamily.binomialFamily_orderTop_pos, le_of_lt, HahnSeries.orderTop_le_of_coeff_ne_zero, Nat.pos_of_ne_zero, Iff.mp, WithTop.coe_pos, lt_of_lt_of_le
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
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
inr : Nontrivial A → 0 < ((binomialFamily x r).hsum - 1).orderTop
⊢ 0 < ((binomialFamily x r).hsum - 1).orderTop

Tactic:
obtain (_ | _) := subsingleton_or_nontrivial A

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
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 : Subsingleton A
⊢ 0 < ((binomialFamily x r).hsum - 1).orderTop

Tactic:
simp [Subsingleton.eq_zero ((binomialFamily x r).hsum - 1)]

Premises used: HSub.hSub, HahnSeries.SummableFamily.binomialFamily, Subsingleton.eq_zero, OfNat.ofNat, HahnSeries.SummableFamily.hsum
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
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

Tactic:
(orderTop_self_sub_one_pos_iff (binomialFamily x r).hsum).mpr ?_

Premises used: Iff.mpr, HahnSeries.SummableFamily.binomialFamily, HahnSeries.orderTop_self_sub_one_pos_iff, HahnSeries.SummableFamily.hsum
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
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.leadingCoeff = 1
⊢ 0 < ((binomialFamily x r).hsum - 1).orderTop

Tactic:
refine (orderTop_self_sub_one_pos_iff (binomialFamily x r).hsum).mpr ?_

Premises used: Iff.mpr, HahnSeries.SummableFamily.binomialFamily, HahnSeries.orderTop_self_sub_one_pos_iff, HahnSeries.SummableFamily.hsum
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
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
inr₁ : (binomialFamily x r).hsum.leadingCoeff = 1
⊢ (binomialFamily x r).hsum.orderTop = 0 ∧ (binomialFamily x r).hsum.leadingCoeff = 1

Tactic:
constructor
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
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
⊢ Eq.{u_1 + 1} (α := WithTop Γ) (↑0 : WithTop Γ) (orderTop (R := A) ((binomialFamily x r : (a : ℕ) → A⟦Γ⟧) 0 : A⟦Γ⟧))

Tactic:
simp [hx]
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
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

Tactic:
exact hsum_orderTop_of_le (by simp [hx]) (fun b g hg => binomialFamily_mem_support
        hx r b hg) fun b hb => coeff_eq_zero_of_lt_orderTop <| binomialFamily_orderTop_pos hx r <|
        Nat.zero_lt_of_ne_zero hb

Premises used: HahnSeries.SummableFamily.hsum_orderTop_of_le, HahnSeries.SummableFamily.binomialFamily_orderTop_pos, Nat.zero_lt_of_ne_zero, HahnSeries.SummableFamily.binomialFamily_mem_support, HahnSeries.coeff_eq_zero_of_lt_orderTop
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
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
⊢ Eq (α := A) (HahnSeries.coeff.{u_1, u_3} (Γ := Γ) ((binomialFamily x r : (a : ℕ) → A⟦Γ⟧) 0) 0 : A) (1 : A)

Tactic:
simp [hx]
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
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
⊢ 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]
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
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 :
  (binomialFamily x r).hsum.leadingCoeff =
    HahnSeries.coeff.{u_1, u_3} (Γ := Γ) ((binomialFamily x r : (a : ℕ) → A⟦Γ⟧) 0) 0
⊢ (binomialFamily x r).hsum.leadingCoeff = 1

Tactic:
rw [← this]
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
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)
⊢ Eq.{u_1 + 1} (α := WithTop Γ) (↑0 : WithTop Γ) (orderTop (R := A) ((binomialFamily x r : (a : ℕ) → A⟦Γ⟧) 0 : A⟦Γ⟧))

Tactic:
simp [hx]
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
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'
inr₁ :
  ∀ (b : ℕ),
    b ≠ 0 → Eq.{u_3 + 1} (α := A) (HahnSeries.coeff.{u_1, u_3} (Γ := Γ) ((binomialFamily x r : (a : ℕ) → A⟦Γ⟧) b) 0) 0
⊢ (binomialFamily x r).hsum.leadingCoeff =
    HahnSeries.coeff.{u_1, u_3} (Γ := Γ) ((binomialFamily x r : (a : ℕ) → A⟦Γ⟧) 0) 0

Tactic:
refine hsum_leadingCoeff_of_le (g := 0) (a := 0) (by simp [hx]) ?_ ?_

Premises used: HahnSeries.SummableFamily.hsum_leadingCoeff_of_le
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
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)
b : ℕ
g' : Γ
hg' : Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := A) ((binomialFamily x r : (a : ℕ) → A⟦Γ⟧) b)) g'
⊢ 0 ≤ g'

Tactic:
binomialFamily_mem_support hx r b hg'

Premises used: HahnSeries.SummableFamily.binomialFamily_mem_support
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
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)
b : ℕ
g' : Γ
hg' : Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := A) ((binomialFamily x r : (a : ℕ) → A⟦Γ⟧) b)) g'
⊢ 0 ≤ g'

Tactic:
exact binomialFamily_mem_support hx r b hg'

Premises used: HahnSeries.SummableFamily.binomialFamily_mem_support
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
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)
b : ℕ
hb : b ≠ 0
⊢ Eq.{u_3 + 1} (α := A) (HahnSeries.coeff.{u_1, u_3} (Γ := Γ) ((binomialFamily x r : (a : ℕ) → A⟦Γ⟧) b) 0) 0

Tactic:
coeff_eq_zero_of_lt_orderTop <| binomialFamily_orderTop_pos hx r <|
        Nat.zero_lt_of_ne_zero hb

Premises used: HahnSeries.SummableFamily.binomialFamily_orderTop_pos, Nat.zero_lt_of_ne_zero, HahnSeries.coeff_eq_zero_of_lt_orderTop
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
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)
b : ℕ
hb : b ≠ 0
⊢ Eq.{u_3 + 1} (α := A) (HahnSeries.coeff.{u_1, u_3} (Γ := Γ) ((binomialFamily x r : (a : ℕ) → A⟦Γ⟧) b) 0) 0

Tactic:
exact coeff_eq_zero_of_lt_orderTop <| binomialFamily_orderTop_pos hx r <|
        Nat.zero_lt_of_ne_zero hb

Premises used: HahnSeries.SummableFamily.binomialFamily_orderTop_pos, Nat.zero_lt_of_ne_zero, HahnSeries.coeff_eq_zero_of_lt_orderTop
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
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 : R
⊢ x ^ r = toOrderTopSubOnePos (x := (binomialFamily (↑(↑x : R⟦Γ⟧ˣ) : R⟦Γ⟧) r).hsum) ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
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
this : (↑(x ^ (r + s)) : R⟦Γ⟧ˣ) = (↑(x ^ r * x ^ s) : R⟦Γ⟧ˣ)
⊢ x ^ (r + s) = x ^ r * x ^ s

Tactic:
SetLike.coe_eq_coe.mp this

Premises used: SetLike.coe_eq_coe, Iff.mp
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
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
this : (↑(x ^ (r + s)) : R⟦Γ⟧ˣ) = (↑(x ^ r * x ^ s) : R⟦Γ⟧ˣ)
⊢ x ^ (r + s) = x ^ r * x ^ s

Tactic:
exact SetLike.coe_eq_coe.mp this

Premises used: SetLike.coe_eq_coe, Iff.mp
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
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
suffices : (↑(x ^ (r + s)) : R⟦Γ⟧ˣ) = (↑(x ^ r * x ^ s) : R⟦Γ⟧ˣ)
⊢ x ^ (r + s) = x ^ r * x ^ s

Tactic:
suffices (x ^ (r + s)).val = (x ^ r * x ^ s).val by exact SetLike.coe_eq_coe.mp this
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
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
this : (↑(↑(x ^ (r + s)) : R⟦Γ⟧ˣ) : R⟦Γ⟧) = (↑(↑(x ^ r * x ^ s) : R⟦Γ⟧ˣ) : R⟦Γ⟧)
⊢ (↑(x ^ (r + s)) : R⟦Γ⟧ˣ) = (↑(x ^ r * x ^ s) : R⟦Γ⟧ˣ)

Tactic:
Units.val_inj.mp this

Premises used: Units.val_inj, Iff.mp
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
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
this : (↑(↑(x ^ (r + s)) : R⟦Γ⟧ˣ) : R⟦Γ⟧) = (↑(↑(x ^ r * x ^ s) : R⟦Γ⟧ˣ) : R⟦Γ⟧)
⊢ (↑(x ^ (r + s)) : R⟦Γ⟧ˣ) = (↑(x ^ r * x ^ s) : R⟦Γ⟧ˣ)

Tactic:
exact Units.val_inj.mp this

Premises used: Units.val_inj, Iff.mp
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
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
suffices : (↑(↑(x ^ (r + s)) : R⟦Γ⟧ˣ) : R⟦Γ⟧) = (↑(↑(x ^ r * x ^ s) : R⟦Γ⟧ˣ) : R⟦Γ⟧)
⊢ (↑(x ^ (r + s)) : R⟦Γ⟧ˣ) = (↑(x ^ r * x ^ s) : R⟦Γ⟧ˣ)

Tactic:
suffices (x ^ (r + s)).val.val = (x ^ r * x ^ s).val.val by exact Units.val_inj.mp this
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
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⟦Γ⟧ˣ) : R⟦Γ⟧) = (↑(↑(x ^ r * x ^ s) : R⟦Γ⟧ˣ) : R⟦Γ⟧)

Tactic:
simp [binomialFamily, hsum_powerSeriesFamily_mul, hsum_mul]

Premises used: HahnSeries.SummableFamily.hsum_powerSeriesFamily_mul, HahnSeries.SummableFamily.binomialFamily, HahnSeries.SummableFamily.hsum_mul
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
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 : ℕ
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
⊢ (↑(↑(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

Tactic:
simp only [val_toOrderTopSubOnePos_coe, binomial_power, coeff_hsum, smul_eq_mul]

Premises used: HahnSeries.binomial_power, HahnSeries.SummableFamily.coeff_hsum, smul_eq_mul, HahnSeries.val_toOrderTopSubOnePos_coe
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
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 : ℕ
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
⊢ ∑ᶠ (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:
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]

Premises used: HahnSeries.orderTop_sub_pos, HahnSeries.single_pow, HahnSeries.coeff_single_same, add_sub_cancel_left, HahnSeries.coeff_smul, HPow.hPow, HahnSeries.SummableFamily.binomialFamily_apply, HSMul.hSMul, smul_eq_mul, finsum_eq_single
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
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
hx : 0 < (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) (1 : R⟦Γ⟧) ((single g : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) - 1).orderTop
⊢ 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

Tactic:
rw [binomialFamily_apply, add_sub_cancel_left, coeff_smul, single_pow, coeff_single_of_ne,
    smul_zero]

Premises used: HahnSeries.single_pow, add_sub_cancel_left, HahnSeries.coeff_smul, smul_zero, HahnSeries.coeff_single_of_ne, HahnSeries.SummableFamily.binomialFamily_apply
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
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
contrapose : ∀ (hn : k • g = n • g), n = k
⊢ k • g ≠ n • g

Tactic:
contrapose hn
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
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 : k • g = n • g
⊢ n = k

Tactic:
apply (StrictMono.injective (nsmul_left_strictMono hg)) hn.symm

Premises used: StrictMono.injective, Eq.symm, nsmul_left_strictMono
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
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
neg :
  ∀ (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

Tactic:
by_cases hr : r = 0
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
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
hr : r = 0
⊢ 0 < (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) (1 : R⟦Γ⟧) ((single g : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) - 1).orderTop

Tactic:
simp [hr, hg]
-- Module: Mathlib.RingTheory.HahnSeries.Binomial
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
hr : ¬r = 0
⊢ 0 < (HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) (1 : R⟦Γ⟧) ((single g : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) - 1).orderTop

Tactic:
simp [hr, hg]
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
Goal:
Γ : Type u_1
R : Type u_2
S : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero S
x : R⟦Γ⟧
y : S⟦Γ⟧
h : x.support ⊆ y.support
⊢ x.cardSupp ≤ y.cardSupp

Tactic:
mk_le_mk_of_subset h

Premises used: Cardinal.mk_le_mk_of_subset
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
Goal:
Γ : Type u_1
R : Type u_2
inst : PartialOrder Γ
inst_1 : Zero R
⊢ cardSupp.{u_1, u_2} (Γ := Γ) (R := R) 0 = 0

Tactic:
simp [cardSupp]

Premises used: HahnSeries.cardSupp
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
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
rw₂ rw₃ : Eq.{u_1 + 2} (α := Cardinal.{u_1}) 1 1
⊢ cardSupp.{u_1, u_2} (Γ := Γ) (R := R) ((single a : (a : R) → R⟦Γ⟧) r) = 1

Tactic:
rw [cardSupp, support_single_of_ne h, mk_singleton]

Premises used: HahnSeries.support_single_of_ne, Cardinal.mk_singleton, HahnSeries.cardSupp
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
Goal:
Γ : Type u_1
R : Type u_2
inst : PartialOrder Γ
inst_1 : Zero R
a : Γ
r : R
⊢ cardSupp.{u_1, u_2} (Γ := Γ) (R := R) ((single a : (a : R) → R⟦Γ⟧) r) ≤ 1

Tactic:
(mk_le_mk_of_subset support_single_subset).trans_eq (mk_singleton a)

Premises used: LE.le.trans_eq, Cardinal.mk_le_mk_of_subset, HahnSeries.support_single_subset, Cardinal.mk_singleton
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
Goal:
Γ : Type u_1
R : Type u_2
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
inst_3 : One R
⊢ cardSupp.{u_1, u_2} (Γ := Γ) (R := R) 1 ≤ 1

Tactic:
cardSupp_single_le ..

Premises used: HahnSeries.cardSupp_single_le
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
Goal:
Γ : Type u_1
R : Type u_2
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
inst_3 : One R
inst_4 : NeZero.{u_2} (R := R) 1
⊢ cardSupp.{u_1, u_2} (Γ := Γ) (R := R) 1 = 1

Tactic:
cardSupp_single_of_ne _ one_ne_zero

Premises used: HahnSeries.cardSupp_single_of_ne, one_ne_zero
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
Goal:
Γ : Type u_1
R : Type u_2
S : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero S
x : R⟦Γ⟧
f : ZeroHom R S
⊢ cardSupp (x.map f) ≤ x.cardSupp

Tactic:
cardSupp_mono <| support_map_subset ..

Premises used: HahnSeries.cardSupp_mono, HahnSeries.support_map_subset
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
Goal:
Γ : Type u_1
R : Type u_2
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : DecidableLT Γ
x : R⟦Γ⟧
c : Γ
⊢ cardSupp.{u_1, u_2} (Γ := Γ) (R := R) ((truncLT c : (a : R⟦Γ⟧) → R⟦Γ⟧) x) ≤ x.cardSupp

Tactic:
cardSupp_mono <| support_truncLT_subset ..

Premises used: HahnSeries.cardSupp_mono, HahnSeries.support_truncLT_subset