awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
Goal:
Γ : Type u_1
R : Type u_2
S : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
s : S
x : R⟦Γ⟧
inst_2 : SMulZeroClass S R
⊢ (s • x).cardSupp ≤ x.cardSupp

Tactic:
cardSupp_mono <| support_smul_subset ..

Premises used: HahnSeries.support_smul_subset, HahnSeries.cardSupp_mono
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
Goal:
Γ : Type u_1
R : Type u_2
inst : PartialOrder Γ
inst_1 : NegZeroClass R
x : R⟦Γ⟧
⊢ (-x).cardSupp ≤ x.cardSupp

Tactic:
cardSupp_mono <| support_neg_subset ..

Premises used: HahnSeries.support_neg_subset, HahnSeries.cardSupp_mono
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
Goal:
Γ : Type u_1
R : Type u_2
inst : PartialOrder Γ
inst_1 : AddMonoid R
x y : R⟦Γ⟧
⊢ (x + y).cardSupp ≤ x.cardSupp + y.cardSupp

Tactic:
(mk_le_mk_of_subset (support_add_subset ..)).trans (mk_union_le ..)

Premises used: Cardinal.mk_le_mk_of_subset, LE.le.trans, Cardinal.mk_union_le, HahnSeries.support_add_subset
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
Goal:
Γ : Type u_1
R : Type u_2
inst : PartialOrder Γ
inst_1 : AddGroup R
x : R⟦Γ⟧
⊢ (-x).cardSupp = x.cardSupp

Tactic:
cardSupp_congr support_neg

Premises used: HahnSeries.cardSupp_congr, HahnSeries.support_neg
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
Goal:
Γ : Type u_1
R : Type u_2
inst : PartialOrder Γ
inst_1 : AddGroup R
x y : R⟦Γ⟧
⊢ (x - y).cardSupp ≤ x.cardSupp + y.cardSupp

Tactic:
(mk_le_mk_of_subset (support_sub_subset ..)).trans (mk_union_le ..)

Premises used: HahnSeries.support_sub_subset, Cardinal.mk_le_mk_of_subset, LE.le.trans, Cardinal.mk_union_le
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
Goal:
Γ : Type u_1
R : Type u_2
inst : PartialOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
x y : R⟦Γ⟧
⊢ (x * y).cardSupp ≤ x.cardSupp * y.cardSupp

Tactic:
(mk_le_mk_of_subset (support_mul_subset ..)).trans mk_add_le

Premises used: Cardinal.mk_le_mk_of_subset, Cardinal.mk_add_le, HahnSeries.support_mul_subset, LE.le.trans
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
Goal:
Γ : Type u_1
R : Type u_2
inst : PartialOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
x : R⟦Γ⟧
a : Γ
r : R
⊢ (HMul.hMul (α := R⟦Γ⟧) ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧) x).cardSupp ≤ x.cardSupp

Tactic:
simpa using (cardSupp_mul_le ..).trans (mul_le_mul_left (cardSupp_single_le ..) _)

Premises used: HahnSeries.cardSupp_single_le, mul_le_mul_left, LE.le.trans, HahnSeries.cardSupp_mul_le
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
Goal:
Γ : Type u_1
R : Type u_2
inst : PartialOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalNonAssocSemiring R
x : R⟦Γ⟧
a : Γ
r : R
⊢ (HMul.hMul (β := R⟦Γ⟧) x ((single a : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)).cardSupp ≤ x.cardSupp

Tactic:
simpa using (cardSupp_mul_le ..).trans (mul_le_mul_right (cardSupp_single_le ..) _)

Premises used: HahnSeries.cardSupp_single_le, mul_le_mul_right, LE.le.trans, HahnSeries.cardSupp_mul_le
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
Goal:
Γ : Type u_1
R : Type u_2
inst : PartialOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
x : R⟦Γ⟧
⊢ (HPow.hPow (β := ℕ) x 0).cardSupp ≤ HPow.hPow (β := ℕ) x.cardSupp 0

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
Goal:
Γ : Type u_1
R : Type u_2
inst : PartialOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
x : R⟦Γ⟧
n : ℕ
IH : (x ^ n).cardSupp ≤ x.cardSupp ^ n
⊢ (x ^ (n + 1)).cardSupp ≤ x.cardSupp ^ (n + 1)

Tactic:
simpa [pow_succ] using (cardSupp_mul_le ..).trans <| mul_le_mul_left IH _

Premises used: pow_succ, mul_le_mul_left, LE.le.trans, HahnSeries.cardSupp_mul_le
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
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
succ : ∀ (n : ℕ) (IH : (x ^ n).cardSupp ≤ x.cardSupp ^ n), (x ^ (n + 1)).cardSupp ≤ x.cardSupp ^ (n + 1)
⊢ (x ^ n).cardSupp ≤ x.cardSupp ^ n

Tactic:
induction n with
  | zero => simp
  | succ n IH =>
    simpa [pow_succ] using (cardSupp_mul_le ..).trans <| mul_le_mul_left IH _

Premises used: pow_succ, LE.le.trans, HahnSeries.cardSupp_mul_le
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
Goal:
Γ : Type u_1
R : Type u_2
α : Type u_4
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s : SummableFamily Γ R α
⊢ lift.{u_4, u_1} s.hsum.cardSupp ≤
    sum.{u_4, u_1} fun (a : α) ↦ cardSupp.{u_1, u_2} (Γ := Γ) (R := R) ((s : (a : α) → R⟦Γ⟧) a)

Tactic:
(lift_le.2 <| mk_le_mk_of_subset (SummableFamily.support_hsum_subset ..)).trans
    mk_iUnion_le_sum_mk_lift

Premises used: Iff.mpr, HahnSeries.SummableFamily.support_hsum_subset, Cardinal.mk_iUnion_le_sum_mk_lift, Cardinal.mk_le_mk_of_subset, LE.le.trans, Cardinal.lift_le
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
H : ∀ (i : ℕ), cardSupp.{u_1, u_2} (Γ := Γ) (R := R) ((SummableFamily.powers x : (a : ℕ) → R⟦Γ⟧) i) ≤ x.cardSupp ^ i
⊢ (SummableFamily.powers x).hsum.cardSupp ≤ max ℵ₀ x.cardSupp

Tactic:
grw [← lift_uzero (cardSupp _), ← sum_pow_le_max_aleph0, cardSupp_hsum_le, sum_le_sum]

Premises used: Cardinal.sum_pow_le_max_aleph0, Cardinal.sum_le_sum, Cardinal.lift_uzero, HahnSeries.cardSupp, HahnSeries.cardSupp_hsum_le
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
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
neg : ¬0 < x.orderTop → (HPow.hPow (α := R⟦Γ⟧) 0 i).cardSupp ≤ x.cardSupp ^ i
⊢ ((if 0 < x.orderTop then x else 0) ^ i).cardSupp ≤ x.cardSupp ^ i

Tactic:
split_ifs
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
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
⊢ (x ^ i).cardSupp ≤ x.cardSupp ^ i

Tactic:
cardSupp_pow_le ..

Premises used: HahnSeries.cardSupp_pow_le
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
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
⊢ (x ^ i).cardSupp ≤ x.cardSupp ^ i

Tactic:
exact cardSupp_pow_le ..

Premises used: HahnSeries.cardSupp_pow_le
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
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
neg₁ : ∀ (n : ℕ), (HPow.hPow (α := R⟦Γ⟧) 0 (n + 1)).cardSupp ≤ x.cardSupp ^ (n + 1)
⊢ (HPow.hPow (α := R⟦Γ⟧) 0 i).cardSupp ≤ x.cardSupp ^ i

Tactic:
cases i
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
h : ¬0 < x.orderTop
⊢ (HPow.hPow (α := R⟦Γ⟧) (β := ℕ) 0 0).cardSupp ≤ HPow.hPow (β := ℕ) x.cardSupp 0

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : CommRing R
x : R⟦Γ⟧
h : ¬0 < x.orderTop
n : ℕ
⊢ (HPow.hPow (α := R⟦Γ⟧) 0 (n + 1)).cardSupp ≤ x.cardSupp ^ (n + 1)

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
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)
inr : ∀ (hx : x ≠ 0), x⁻¹.cardSupp ≤ max ℵ₀ x.cardSupp
⊢ x⁻¹.cardSupp ≤ max ℵ₀ x.cardSupp

Tactic:
obtain rfl | hx := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : AddCommGroup Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
⊢ cardSupp.{u_1, u_2} (Γ := Γ) (R := R) 0⁻¹ ≤ max ℵ₀ (cardSupp.{u_1, u_2} (Γ := Γ) (R := R) 0)

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
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
apply :
  max ℵ₀ (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x).cardSupp ≤
    max ℵ₀ x.cardSupp
⊢ x⁻¹.cardSupp ≤ max ℵ₀ x.cardSupp

Tactic:
apply (cardSupp_single_mul_le ..).trans <| (cardSupp_hsum_powers_le ..).trans _

Premises used: HahnSeries.cardSupp_single_mul_le, LE.le.trans, HahnSeries.cardSupp_hsum_powers_le
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
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
h₂ : (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x).cardSupp ≤ x.cardSupp
⊢ max ℵ₀ (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x).cardSupp ≤
    max ℵ₀ x.cardSupp

Tactic:
gcongr
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
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

Tactic:
(cardSupp_single_mul_le _ (-x.order) x.leadingCoeff⁻¹).trans' <| cardSupp_mono fun _ ↦ ?_

Premises used: HahnSeries.order, HahnSeries.cardSupp_single_mul_le, Inv.inv, HahnSeries.leadingCoeff, HahnSeries.cardSupp_mono, Neg.neg, LE.le.trans'
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
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
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
⊢ (1 - HMul.hMul (α := R⟦Γ⟧) ((single (-x.order) : (a : R) → R⟦Γ⟧) x.leadingCoeff⁻¹ : R⟦Γ⟧) x).cardSupp ≤ x.cardSupp

Tactic:
refine (cardSupp_single_mul_le _ (-x.order) x.leadingCoeff⁻¹).trans' <| cardSupp_mono fun _ ↦ ?_

Premises used: HahnSeries.order, HahnSeries.cardSupp_single_mul_le, Inv.inv, HahnSeries.leadingCoeff, HahnSeries.cardSupp_mono, Neg.neg, LE.le.trans'
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
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_1 : Γ
⊢ 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:
aesop (add simp [coeff_single_mul])

Premises used: HahnSeries.coeff_single_mul
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : AddCommGroup Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
x y : R⟦Γ⟧
⊢ (x / y).cardSupp ≤ x.cardSupp * max ℵ₀ y.cardSupp

Tactic:
(cardSupp_mul_le ..).trans <| mul_le_mul_right (cardSupp_inv_le y) _

Premises used: mul_le_mul_right, DivInvMonoid.div', LE.le.trans, HahnSeries.cardSupp_inv_le, HahnSeries.cardSupp_mul_le
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
Goal:
Γ : Type u_1
R : Type u_2
S : Type u_3
α : Type u_4
κ : Cardinal.{u_1}
inst : PartialOrder Γ
inst_1 : AddMonoid R
hκ : Fact (ℵ₀ ≤ κ)
⊢ Membership.mem (γ := Set R⟦Γ⟧) {x : R⟦Γ⟧ | x.cardSupp < κ} 0

Tactic:
simpa using aleph0_pos.trans_le hκ.out

Premises used: LT.lt.trans_le, Cardinal.aleph0_pos, Fact.out
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
Goal:
Γ : Type u_1
R : Type u_2
κ : Cardinal.{u_1}
inst : PartialOrder Γ
inst_1 : AddMonoid R
hκ : Fact (ℵ₀ ≤ κ)
x : R⟦Γ⟧
⊢ Membership.mem (γ := AddSubmonoid R⟦Γ⟧) (cardSuppLTAddSubmonoid Γ R κ) x ↔ x.cardSupp < κ

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
Goal:
Γ : Type u_1
R : Type u_2
S : Type u_3
α : Type u_4
κ : Cardinal.{u_1}
inst : PartialOrder Γ
inst_1 : AddGroup R
hκ : Fact (ℵ₀ ≤ κ)
⊢ ∀ {x : R⟦Γ⟧},
    Membership.mem (γ := Set R⟦Γ⟧)
        (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (cardSuppLTAddSubmonoid Γ R κ))) x →
      Membership.mem (γ := Set R⟦Γ⟧)
        (AddSubsemigroup.carrier (AddSubmonoid.toAddSubsemigroup (cardSuppLTAddSubmonoid Γ R κ))) (-x)

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
Goal:
Γ : Type u_1
R : Type u_2
κ : Cardinal.{u_1}
inst : PartialOrder Γ
inst_1 : AddGroup R
hκ : Fact (ℵ₀ ≤ κ)
x : R⟦Γ⟧
⊢ Membership.mem (γ := AddSubgroup R⟦Γ⟧) (cardSuppLTAddSubgroup Γ R κ) x ↔ x.cardSupp < κ

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
Goal:
Γ : Type u_1
R : Type u_2
κ : Cardinal.{u_1}
inst : PartialOrder Γ
inst_1 : AddCommMonoid Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Ring R
hκ : Fact (ℵ₀ ≤ κ)
x : R⟦Γ⟧
⊢ Membership.mem (γ := Subring R⟦Γ⟧) (cardSuppLTSubring Γ R κ) x ↔ x.cardSupp < κ

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
Goal:
Γ : Type u_1
R : Type u_2
S : Type u_3
α : Type u_4
κ : Cardinal.{u_1}
inst : LinearOrder Γ
inst_1 : AddCommGroup Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
hκ : Fact (ℵ₀ < κ)
x : R⟦Γ⟧
h :
  Membership.mem (γ := Set R⟦Γ⟧)
    (Subsemigroup.carrier
      (Submonoid.toSubsemigroup
        (Subsemiring.toSubmonoid
          (Subring.toSubsemiring
            (have this : Fact (ℵ₀ ≤ κ) := ⋯;
            cardSuppLTSubring Γ R κ)))))
    x
⊢ max ℵ₀ x.cardSupp < κ

Tactic:
simpa [hκ.out]

Premises used: Fact.out
-- Module: Mathlib.RingTheory.HahnSeries.Cardinal
Goal:
Γ : Type u_1
R : Type u_2
κ : Cardinal.{u_1}
inst : LinearOrder Γ
inst_1 : AddCommGroup Γ
inst_2 : IsOrderedAddMonoid Γ
inst_3 : Field R
hκ : Fact (ℵ₀ < κ)
x : R⟦Γ⟧
⊢ Membership.mem (γ := Subfield R⟦Γ⟧) (cardSuppLTSubfield Γ R κ) x ↔ x.cardSupp < κ

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.RingTheory.HahnSeries.HEval
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
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)
⊢ powerSeriesFamily x f = powerSeriesFamily 0 f

Tactic:
ext n g
-- Module: Mathlib.RingTheory.HahnSeries.HEval
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
n : ℕ
g : Γ
h :
  Eq (α := V) (HahnSeries.coeff ((powerSeriesFamily x f : (a : ℕ) → V⟦Γ⟧) 0) g : V)
    (HahnSeries.coeff ((powerSeriesFamily 0 f : (a : ℕ) → V⟦Γ⟧) 0) g : V)
h₁ :
  ∀ (hn : n ≠ 0),
    Eq.{u_4 + 1} (α := V) (HahnSeries.coeff ((powerSeriesFamily x f : (a : ℕ) → V⟦Γ⟧) n) g)
      (HahnSeries.coeff ((powerSeriesFamily 0 f : (a : ℕ) → V⟦Γ⟧) 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:
obtain rfl | hn := eq_or_ne n 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.HahnSeries.HEval
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
g : Γ
⊢ Eq (α := V) (HahnSeries.coeff ((powerSeriesFamily x f : (a : ℕ) → V⟦Γ⟧) 0) g : V)
    (HahnSeries.coeff ((powerSeriesFamily 0 f : (a : ℕ) → V⟦Γ⟧) 0) g : V)

Tactic:
simp [*]
-- Module: Mathlib.RingTheory.HahnSeries.HEval
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
n : ℕ
g : Γ
hn : n ≠ 0
⊢ Eq.{u_4 + 1} (α := V) (HahnSeries.coeff ((powerSeriesFamily x f : (a : ℕ) → V⟦Γ⟧) n) g)
    (HahnSeries.coeff ((powerSeriesFamily 0 f : (a : ℕ) → V⟦Γ⟧) n) g)

Tactic:
simp [*]
-- Module: Mathlib.RingTheory.HahnSeries.HEval
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
n : ℕ
⊢ (powerSeriesFamily x f : (a : ℕ) → V⟦Γ⟧) n =
    HSMul.hSMul (α := R) ((PowerSeries.coeff n : (a : PowerSeries R) → R) f : R) (x ^ n)

Tactic:
simp [hx]
-- Module: Mathlib.RingTheory.HahnSeries.HEval
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
f : PowerSeries R
coeff :
  ∀ (g : Γ),
    HahnSeries.coeff (hsum (powerSeriesFamily 0 f)) g =
      (HSMul.hSMul (α := R) (β := V⟦Γ⟧) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) 1).coeff g
⊢ hsum (powerSeriesFamily 0 f) =
    HSMul.hSMul (α := R) (β := V⟦Γ⟧) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) 1

Tactic:
ext g
-- Module: Mathlib.RingTheory.HahnSeries.HEval
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
f : PowerSeries R
g : Γ
pos :
  ∀ (hg : g = 0),
    HahnSeries.coeff (hsum (powerSeriesFamily 0 f)) g =
      (HSMul.hSMul (α := R) (β := V⟦Γ⟧) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) 1).coeff g
neg :
  ∀ (hg : ¬g = 0),
    HahnSeries.coeff (hsum (powerSeriesFamily 0 f)) g =
      (HSMul.hSMul (α := R) (β := V⟦Γ⟧) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) 1).coeff g
⊢ HahnSeries.coeff (hsum (powerSeriesFamily 0 f)) g =
    (HSMul.hSMul (α := R) (β := V⟦Γ⟧) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) 1).coeff g

Tactic:
by_cases hg : g = 0
-- Module: Mathlib.RingTheory.HahnSeries.HEval
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
f : PowerSeries R
g : Γ
hg : g = 0
pos :
  ∑ᶠ (i : ℕ), HahnSeries.coeff.{u_1, u_4} (Γ := Γ) ((powerSeriesFamily 0 f : (a : ℕ) → V⟦Γ⟧) i) 0 =
    (HSMul.hSMul (α := R) (β := V⟦Γ⟧) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) 1).coeff 0
⊢ HahnSeries.coeff (hsum (powerSeriesFamily 0 f)) g =
    (HSMul.hSMul (α := R) (β := V⟦Γ⟧) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) 1).coeff g

Tactic:
simp only [hg, coeff_hsum]

Premises used: HahnSeries.SummableFamily.coeff_hsum
-- Module: Mathlib.RingTheory.HahnSeries.HEval
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
f : PowerSeries R
g : Γ
hg : g = 0
n : ℕ
hn : n ≠ 0
⊢ Eq.{u_4 + 1} (α := V) (HahnSeries.coeff.{u_1, u_4} (Γ := Γ) ((powerSeriesFamily 0 f : (a : ℕ) → V⟦Γ⟧) n) 0) 0

Tactic:
simp [hn]
-- Module: Mathlib.RingTheory.HahnSeries.HEval
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
f : PowerSeries R
g : Γ
hg : g = 0
pos :
  HahnSeries.coeff.{u_1, u_4} (Γ := Γ) ((powerSeriesFamily 0 f : (a : ℕ) → V⟦Γ⟧) 0) 0 =
    (HSMul.hSMul (α := R) (β := V⟦Γ⟧) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) 1).coeff 0
⊢ ∑ᶠ (i : ℕ), HahnSeries.coeff.{u_1, u_4} (Γ := Γ) ((powerSeriesFamily 0 f : (a : ℕ) → V⟦Γ⟧) i) 0 =
    (HSMul.hSMul (α := R) (β := V⟦Γ⟧) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) 1).coeff 0

Tactic:
rw [finsum_eq_single _ 0 (fun n hn ↦ by simp [hn])]

Premises used: OfNat.ofNat, finsum_eq_single
-- Module: Mathlib.RingTheory.HahnSeries.HEval
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
f : PowerSeries R
g : Γ
hg : g = 0
⊢ HahnSeries.coeff.{u_1, u_4} (Γ := Γ) ((powerSeriesFamily 0 f : (a : ℕ) → V⟦Γ⟧) 0) 0 =
    (HSMul.hSMul (α := R) (β := V⟦Γ⟧) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) 1).coeff 0

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.HEval
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
f : PowerSeries R
g : Γ
hg : ¬g = 0
n : ℕ
pos : ∀ (hn : n = 0), Eq.{u_4 + 1} (α := V) (HahnSeries.coeff ((powerSeriesFamily 0 f : (a : ℕ) → V⟦Γ⟧) n) g) 0
neg : ∀ (hn : ¬n = 0), Eq.{u_4 + 1} (α := V) (HahnSeries.coeff ((powerSeriesFamily 0 f : (a : ℕ) → V⟦Γ⟧) n) g) 0
⊢ Eq.{u_4 + 1} (α := V) (HahnSeries.coeff ((powerSeriesFamily 0 f : (a : ℕ) → V⟦Γ⟧) n) g) 0

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.RingTheory.HahnSeries.HEval
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
f : PowerSeries R
g : Γ
hg : ¬g = 0
n : ℕ
hn : n = 0
⊢ Eq.{u_4 + 1} (α := V) (HahnSeries.coeff ((powerSeriesFamily 0 f : (a : ℕ) → V⟦Γ⟧) n) g) 0

Tactic:
simp [hg, hn]
-- Module: Mathlib.RingTheory.HahnSeries.HEval
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
f : PowerSeries R
g : Γ
hg : ¬g = 0
n : ℕ
hn : ¬n = 0
⊢ Eq.{u_4 + 1} (α := V) (HahnSeries.coeff ((powerSeriesFamily 0 f : (a : ℕ) → V⟦Γ⟧) n) g) 0

Tactic:
simp [hg, hn]
-- Module: Mathlib.RingTheory.HahnSeries.HEval
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
f : PowerSeries R
g : Γ
hg : ¬g = 0
neg : 0 = (HSMul.hSMul (α := R) (β := V⟦Γ⟧) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) 1).coeff g
⊢ HahnSeries.coeff (hsum (powerSeriesFamily 0 f)) g =
    (HSMul.hSMul (α := R) (β := V⟦Γ⟧) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) 1).coeff g

Tactic:
rw [coeff_hsum, finsum_eq_zero_of_forall_eq_zero
      fun n ↦ (by by_cases hn : n = 0 <;> simp [hg, hn])]

Premises used: HahnSeries.SummableFamily.coeff_hsum, finsum_eq_zero_of_forall_eq_zero
-- Module: Mathlib.RingTheory.HahnSeries.HEval
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
f : PowerSeries R
g : Γ
hg : ¬g = 0
⊢ 0 = (HSMul.hSMul (α := R) (β := V⟦Γ⟧) ((PowerSeries.constantCoeff : (a : PowerSeries R) → R) f : R) 1).coeff g

Tactic:
simp [hg]
-- Module: Mathlib.RingTheory.HahnSeries.HEval
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⟦Γ⟧
f g : PowerSeries R
h :
  ∀ (n : ℕ),
    Eq (α := V⟦Γ⟧) ((powerSeriesFamily x (f + g) : (a : ℕ) → V⟦Γ⟧) n : V⟦Γ⟧)
      ((powerSeriesFamily x f + powerSeriesFamily x g : (a : ℕ) → V⟦Γ⟧) n : V⟦Γ⟧)
⊢ powerSeriesFamily x (f + g) = powerSeriesFamily x f + powerSeriesFamily x g

Tactic:
ext1 n