awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : PartialOrder Γ'
inst_4 : AddAction Γ Γ'
inst_5 : IsOrderedCancelVAdd Γ Γ'
inst_6 : Semiring R
inst_7 : AddCommMonoid V
inst_8 : Module R V
x : SummableFamily Γ' V α
x_1 : α
rw :
  Eq (α := V⟦Γ'⟧)
    ((Equiv.symm (HahnModule.of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
        (HSMul.hSMul (α := R⟦Γ⟧) (β := HahnModule Γ' R V) 1
          ((HahnModule.of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) ((x : (a : α) → V⟦Γ'⟧) x_1) : HahnModule Γ' R V)) :
      V⟦Γ'⟧)
    ((x : (a : α) → V⟦Γ'⟧) x_1 : V⟦Γ'⟧)
⊢ Eq (α := V⟦Γ'⟧) ((HSMul.hSMul (α := R⟦Γ⟧) 1 x : (a : α) → V⟦Γ'⟧) x_1 : V⟦Γ'⟧) ((x : (a : α) → V⟦Γ'⟧) x_1 : V⟦Γ'⟧)
have rw₁ : Eq (α := V⟦Γ'⟧)
  ((Equiv.symm (HahnModule.of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
      ((HahnModule.of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) ((x : (a : α) → V⟦Γ'⟧) x_1)) :
    V⟦Γ'⟧)
  ((x : (a : α) → V⟦Γ'⟧) x_1 : V⟦Γ'⟧)
Tactic: rw [smul_apply, HahnModule.one_smul', Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : PartialOrder Γ'
inst_4 : AddAction Γ Γ'
inst_5 : IsOrderedCancelVAdd Γ Γ'
inst_6 : Semiring R
inst_7 : AddCommMonoid V
inst_8 : Module R V
x : SummableFamily Γ' V α
x_1 : α
rw :
  Eq (α := V⟦Γ'⟧)
    ((Equiv.symm (HahnModule.of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
        (HSMul.hSMul (α := R⟦Γ⟧) (β := HahnModule Γ' R V) 1
          ((HahnModule.of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) ((x : (a : α) → V⟦Γ'⟧) x_1) : HahnModule Γ' R V)) :
      V⟦Γ'⟧)
    ((x : (a : α) → V⟦Γ'⟧) x_1 : V⟦Γ'⟧)
rw₁ :
  Eq (α := V⟦Γ'⟧)
    ((Equiv.symm (HahnModule.of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧)
        ((HahnModule.of R : (a : V⟦Γ'⟧) → HahnModule Γ' R V) ((x : (a : α) → V⟦Γ'⟧) x_1)) :
      V⟦Γ'⟧)
    ((x : (a : α) → V⟦Γ'⟧) x_1 : V⟦Γ'⟧)
⊢ Eq (α := V⟦Γ'⟧) ((HSMul.hSMul (α := R⟦Γ⟧) 1 x : (a : α) → V⟦Γ'⟧) x_1 : V⟦Γ'⟧) ((x : (a : α) → V⟦Γ'⟧) x_1 : V⟦Γ'⟧)
have rw₂ : Eq (α := V⟦Γ'⟧) ((x : (a : α) → V⟦Γ'⟧) x_1 : V⟦Γ'⟧) ((x : (a : α) → V⟦Γ'⟧) x_1 : V⟦Γ'⟧)
Tactic: rw [smul_apply, HahnModule.one_smul', Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
x : R⟦Γ⟧
s : SummableFamily Γ R α
⊢ (x • s).hsum = x * s.hsum
have rw : (Equiv.symm (HahnModule.of R) : (a : HahnModule Γ R R) → R⟦Γ⟧)
    (HSMul.hSMul (β := HahnModule Γ R R) x
      ((HahnModule.of R : (a : R⟦Γ⟧) → HahnModule Γ R R) s.hsum : HahnModule Γ R R)) =
  x * s.hsum
Tactic: rw [hsum_smul_module, of_symm_smul_of_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
x : R⟦Γ⟧
s : SummableFamily Γ R α
rw :
  (Equiv.symm (HahnModule.of R) : (a : HahnModule Γ R R) → R⟦Γ⟧)
      (HSMul.hSMul (β := HahnModule Γ R R) x
        ((HahnModule.of R : (a : R⟦Γ⟧) → HahnModule Γ R R) s.hsum : HahnModule Γ R R)) =
    x * s.hsum
⊢ (x • s).hsum = x * s.hsum
have rw₁ : x * s.hsum = x * s.hsum
Tactic: rw [hsum_smul_module, of_symm_smul_of_eq_mul]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
α : Type u_5
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
R : Type u_7
inst_3 : Ring R
s t : SummableFamily Γ R α
⊢ (s - t).hsum = s.hsum - t.hsum
have rw : (lsum : (a : SummableFamily Γ R α) → R⟦Γ⟧) (s - t) = s.hsum - t.hsum
Tactic: rw [← lsum_apply, map_sub, lsum_apply, lsum_apply]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
α : Type u_5
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
R : Type u_7
inst_3 : Ring R
s t : SummableFamily Γ R α
rw : (lsum : (a : SummableFamily Γ R α) → R⟦Γ⟧) (s - t) = s.hsum - t.hsum
⊢ (s - t).hsum = s.hsum - t.hsum
have rw₁ : HSub.hSub (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((lsum : (a : SummableFamily Γ R α) → R⟦Γ⟧) s : R⟦Γ⟧)
    ((lsum : (a : SummableFamily Γ R α) → R⟦Γ⟧) t : R⟦Γ⟧) =
  s.hsum - t.hsum
Tactic: rw [← lsum_apply, map_sub, lsum_apply, lsum_apply]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
α : Type u_5
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
R : Type u_7
inst_3 : Ring R
s t : SummableFamily Γ R α
rw : (lsum : (a : SummableFamily Γ R α) → R⟦Γ⟧) (s - t) = s.hsum - t.hsum
rw₁ :
  HSub.hSub (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((lsum : (a : SummableFamily Γ R α) → R⟦Γ⟧) s : R⟦Γ⟧)
      ((lsum : (a : SummableFamily Γ R α) → R⟦Γ⟧) t : R⟦Γ⟧) =
    s.hsum - t.hsum
⊢ (s - t).hsum = s.hsum - t.hsum
have rw₂ : HSub.hSub (β := R⟦Γ⟧) s.hsum ((lsum : (a : SummableFamily Γ R α) → R⟦Γ⟧) t : R⟦Γ⟧) = s.hsum - t.hsum
Tactic: rw [← lsum_apply, map_sub, lsum_apply, lsum_apply]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
α : Type u_5
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
R : Type u_7
inst_3 : Ring R
s t : SummableFamily Γ R α
rw : (lsum : (a : SummableFamily Γ R α) → R⟦Γ⟧) (s - t) = s.hsum - t.hsum
rw₁ :
  HSub.hSub (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((lsum : (a : SummableFamily Γ R α) → R⟦Γ⟧) s : R⟦Γ⟧)
      ((lsum : (a : SummableFamily Γ R α) → R⟦Γ⟧) t : R⟦Γ⟧) =
    s.hsum - t.hsum
rw₂ : HSub.hSub (β := R⟦Γ⟧) s.hsum ((lsum : (a : SummableFamily Γ R α) → R⟦Γ⟧) t : R⟦Γ⟧) = s.hsum - t.hsum
⊢ (s - t).hsum = s.hsum - t.hsum
have rw₃ : s.hsum - t.hsum = s.hsum - t.hsum
Tactic: rw [← lsum_apply, map_sub, lsum_apply, lsum_apply]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
s : SummableFamily Γ R α
t : SummableFamily Γ R β
g : Γ
⊢ (s.mul t).hsum.coeff g =
    ∑
      gh ∈
        addAntidiagonal (s := ⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) (t :=
          ⋃ (a : β), support.{u_1, u_3} (R := R) ((t : (a : β) → R⟦Γ⟧) a)) ⋯ ⋯ g,
      s.hsum.coeff gh.1 * t.hsum.coeff gh.2
have simp_rw : (s.smul t).hsum.coeff g =
  ∑
    x ∈
      addAntidiagonal (s := ⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) (t :=
        ⋃ (a : β), support.{u_1, u_3} (R := R) ((t : (a : β) → R⟦Γ⟧) a)) sorry sorry g,
    s.hsum.coeff x.1 • t.hsum.coeff x.2
Tactic: simp_rw [← smul_eq_mul, mul_eq_smul]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : Semiring R
s : SummableFamily Γ R α
t : SummableFamily Γ R β
⊢ (s.mul t).hsum = s.hsum * t.hsum
have rw : (s.smul t).hsum = s.hsum • t.hsum
Tactic: rw [← smul_eq_mul, mul_eq_smul]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
f : α →₀ R⟦Γ⟧
⊢ Set.IsPWO.{u_1} (α := Γ) (⋃ (a : α), support.{u_1, u_3} (R := R) ((f : (a : α) → R⟦Γ⟧) a))
have apply : Subset.{u_1} (α := Set Γ) (⋃ (a : α), support.{u_1, u_3} (R := R) ((f : (a : α) → R⟦Γ⟧) a))
  (⋃ i ∈ f.support, support.{u_1, u_3} (R := R) ((f : (a : α) → R⟦Γ⟧) i))
Tactic: apply (f.support.isPWO_bUnion.2 fun a _ => (f a).isPWO_support).mono
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
f : α →₀ R⟦Γ⟧
⊢ Subset.{u_1} (α := Set Γ) (⋃ (a : α), support.{u_1, u_3} (R := R) ((f : (a : α) → R⟦Γ⟧) a))
    (⋃ i ∈ f.support, support.{u_1, u_3} (R := R) ((f : (a : α) → R⟦Γ⟧) i))
have refine : ∀ (a : α) (g : Γ) (hg : Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := R) ((f : (a : α) → R⟦Γ⟧) a)) g),
  Membership.mem (γ := Set Γ) (⋃ i ∈ f.support, support.{u_1, u_3} (R := R) ((f : (a : α) → R⟦Γ⟧) i)) g
Tactic: refine Set.iUnion_subset_iff.2 fun a g hg => ?_
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
f : α →₀ R⟦Γ⟧
a : α
g : Γ
hg : Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := R) ((f : (a : α) → R⟦Γ⟧) a)) g
⊢ a ∈ f.support
have rw : Set.Nonempty.{u_1} (α := Γ) (support.{u_1, u_3} (R := R) ((f : (a : α) → R⟦Γ⟧) a))
Tactic: rw [Finsupp.mem_support_iff, ← support_nonempty_iff]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (hypothesis)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
f : α →₀ R⟦Γ⟧
a : α
g : Γ
hg : Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := R) ((f : (a : α) → R⟦Γ⟧) a)) g
⊢ Membership.mem (γ := Set Γ) (⋃ i ∈ f.support, support.{u_1, u_3} (R := R) ((f : (a : α) → R⟦Γ⟧) i)) g
have haf : a ∈ f.support
Tactic: have haf : a ∈ f.support := by
      rw [Finsupp.mem_support_iff, ← support_nonempty_iff]
      exact ⟨g, hg⟩
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
f : α →₀ R⟦Γ⟧
g : Γ
⊢ Set.Finite.{u_5} (α := α) {a : α | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((f : (a : α) → R⟦Γ⟧) a) g) 0}
have refine : ∀ (a : α)
  (ha : Membership.mem (γ := Set α) {a : α | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((f : (a : α) → R⟦Γ⟧) a) g) 0} a),
  a ∈ (↑f.support : Set α)
Tactic: refine f.support.finite_toSet.subset fun a ha => ?_
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
f : α →₀ R⟦Γ⟧
g : Γ
a : α
ha : Membership.mem (γ := Set α) {a : α | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((f : (a : α) → R⟦Γ⟧) a) g) 0} a
⊢ a ∈ (↑f.support : Set α)
have simp : ¬Eq (α := R⟦Γ⟧) ((f : (a : α) → R⟦Γ⟧) a : R⟦Γ⟧) (0 : R⟦Γ⟧)
Tactic: simp only [mem_coe, Finsupp.mem_support_iff, Ne]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
f : α →₀ R⟦Γ⟧
g : Γ
a : α
ha : Membership.mem (γ := Set α) {a : α | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((f : (a : α) → R⟦Γ⟧) a) g) 0} a
⊢ ¬Eq (α := R⟦Γ⟧) ((f : (a : α) → R⟦Γ⟧) a : R⟦Γ⟧) (0 : R⟦Γ⟧)
have contrapose : ∀ (ha : Eq (α := R⟦Γ⟧) ((f : (a : α) → R⟦Γ⟧) a : R⟦Γ⟧) (0 : R⟦Γ⟧)),
  a ∉ {a : α | Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((f : (a : α) → R⟦Γ⟧) a) g) 0}
Tactic: contrapose ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
f : α →₀ R⟦Γ⟧
⊢ (ofFinsupp f).hsum = f.sum fun (x : α) ↦ id
have coeff : ∀ (g : Γ), (ofFinsupp f).hsum.coeff g = HahnSeries.coeff (f.sum fun (x : α) ↦ id) g
Tactic: ext g
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
f : α →₀ R⟦Γ⟧
g : Γ
⊢ (ofFinsupp f).hsum.coeff g = HahnSeries.coeff (f.sum fun (x : α) ↦ id) g
have coeff : Eq.{u_3 + 1} (α := R) (∑ᶠ (i : α), HahnSeries.coeff ((f : (a : α) → R⟦Γ⟧) i) g)
  (HahnSeries.coeff (∑ x ∈ f.support, id ((f : (a : α) → R⟦Γ⟧) x)) g)
Tactic: simp only [coeff_hsum, coe_ofFinsupp, Finsupp.sum]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
f : α →₀ R⟦Γ⟧
g : Γ
⊢ Eq.{u_3 + 1} (α := R) (∑ᶠ (i : α), HahnSeries.coeff ((f : (a : α) → R⟦Γ⟧) i) g)
    (HahnSeries.coeff (∑ x ∈ f.support, id ((f : (a : α) → R⟦Γ⟧) x)) g)
have coeff : Eq.{u_3 + 1} (α := R) (∑ᶠ (i : α), (coeff.addMonoidHom g : (a : R⟦Γ⟧) → R) ((f : (a : α) → R⟦Γ⟧) i : R⟦Γ⟧) : R)
  ((coeff.addMonoidHom g : (a : R⟦Γ⟧) → R) (∑ x ∈ f.support, (f : (a : α) → R⟦Γ⟧) x) : R)
Tactic: simp_rw [← coeff.addMonoidHom_apply, id]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
f : α →₀ R⟦Γ⟧
g : Γ
⊢ Eq.{u_3 + 1} (α := R) (∑ᶠ (i : α), (coeff.addMonoidHom g : (a : R⟦Γ⟧) → R) ((f : (a : α) → R⟦Γ⟧) i : R⟦Γ⟧) : R)
    ((coeff.addMonoidHom g : (a : R⟦Γ⟧) → R) (∑ x ∈ f.support, (f : (a : α) → R⟦Γ⟧) x) : R)
have coeff : (Function.support.{u_5, u_3} (M := R) fun (i : α) ↦
    (coeff.addMonoidHom g : (a : R⟦Γ⟧) → R) ((f : (a : α) → R⟦Γ⟧) i : R⟦Γ⟧)) ⊆
  (↑f.support : Set α)
Tactic: rw [map_sum, finsum_eq_sum_of_support_subset]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
f : α →₀ R⟦Γ⟧
g : Γ
x : α
h :
  Membership.mem (γ := Set α)
    (Function.support.{u_5, u_3} (M := R) fun (i : α) ↦
      (coeff.addMonoidHom g : (a : R⟦Γ⟧) → R) ((f : (a : α) → R⟦Γ⟧) i : R⟦Γ⟧))
    x
⊢ x ∈ (↑f.support : Set α)
have coeff : ¬Eq (α := R⟦Γ⟧) ((f : (a : α) → R⟦Γ⟧) x : R⟦Γ⟧) (0 : R⟦Γ⟧)
Tactic: simp only [mem_coe, Finsupp.mem_support_iff, Ne]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
f : α →₀ R⟦Γ⟧
g : Γ
x : α
h :
  Membership.mem (γ := Set α)
    (Function.support.{u_5, u_3} (M := R) fun (i : α) ↦
      (coeff.addMonoidHom g : (a : R⟦Γ⟧) → R) ((f : (a : α) → R⟦Γ⟧) i : R⟦Γ⟧))
    x
⊢ ¬Eq (α := R⟦Γ⟧) ((f : (a : α) → R⟦Γ⟧) x : R⟦Γ⟧) (0 : R⟦Γ⟧)
have coeff : ∀ (h : Eq (α := R⟦Γ⟧) ((f : (a : α) → R⟦Γ⟧) x : R⟦Γ⟧) (0 : R⟦Γ⟧)),
  x ∉
    Function.support.{u_5, u_3} (M := R) fun (i : α) ↦
      (coeff.addMonoidHom g : (a : R⟦Γ⟧) → R) ((f : (a : α) → R⟦Γ⟧) i : R⟦Γ⟧)
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s : SummableFamily Γ R α
f : α ↪ β
⊢ Set.IsPWO.{u_1} (α := Γ)
    (⋃ (a : β),
      support.{u_1, u_3} (R := R)
        (if h : Membership.mem (γ := Set β) (Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)) a then
          (s : (a : α) → R⟦Γ⟧) (Classical.choose (p := fun (x : α) ↦ (f : (a : α) → β) x = a) h)
        else 0))
have refine : ∀ (b : β) (g : Γ)
  (h :
    Membership.mem (γ := Set Γ)
      (support.{u_1, u_3} (R := R)
        (if h : Membership.mem (γ := Set β) (Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)) b then
          (s : (a : α) → R⟦Γ⟧) (Classical.choose (p := fun (x : α) ↦ (f : (a : α) → β) x = b) h)
        else 0))
      g),
  Membership.mem (γ := Set Γ) (⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) g
Tactic: refine s.isPWO_iUnion_support.mono (Set.iUnion_subset fun b g h => ?_)
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s : SummableFamily Γ R α
f : α ↪ β
b : β
g : Γ
h :
  Membership.mem (γ := Set Γ)
    (support.{u_1, u_3} (R := R)
      (if h : Membership.mem (γ := Set β) (Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)) b then
        (s : (a : α) → R⟦Γ⟧) (Classical.choose (p := fun (x : α) ↦ (f : (a : α) → β) x = b) h)
      else 0))
    g
⊢ Membership.mem (γ := Set Γ) (⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) g
have pos : ∀ (hb : Membership.mem (γ := Set β) (Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)) b),
  Membership.mem (γ := Set Γ) (⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) g
Tactic: by_cases hb : b ∈ Set.range f
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s : SummableFamily Γ R α
f : α ↪ β
b : β
g : Γ
h :
  Membership.mem (γ := Set Γ)
    (support.{u_1, u_3} (R := R)
      (if h : Membership.mem (γ := Set β) (Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)) b then
        (s : (a : α) → R⟦Γ⟧) (Classical.choose (p := fun (x : α) ↦ (f : (a : α) → β) x = b) h)
      else 0))
    g
pos :
  ∀ (hb : Membership.mem (γ := Set β) (Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)) b),
    Membership.mem (γ := Set Γ) (⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) g
⊢ Membership.mem (γ := Set Γ) (⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) g
have neg : ∀ (hb : b ∉ Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)),
  Membership.mem (γ := Set Γ) (⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) g
Tactic: by_cases hb : b ∈ Set.range f
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (hypothesis)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s : SummableFamily Γ R α
f : α ↪ β
b : β
g : Γ
h :
  Membership.mem (γ := Set Γ)
    (support.{u_1, u_3} (R := R)
      (if h : Membership.mem (γ := Set β) (Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)) b then
        (s : (a : α) → R⟦Γ⟧) (Classical.choose (p := fun (x : α) ↦ (f : (a : α) → β) x = b) h)
      else 0))
    g
hb : Membership.mem (γ := Set β) (Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)) b
⊢ Membership.mem (γ := Set Γ) (⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) g
have h₁ : Membership.mem (γ := Set Γ)
  (support.{u_1, u_3} (R := R)
    ((s : (a : α) → R⟦Γ⟧) (Classical.choose (p := fun (x : α) ↦ (f : (a : α) → β) x = b) hb)))
  g
Tactic: rw [dif_pos hb] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s : SummableFamily Γ R α
f : α ↪ β
g : Γ
b : β
h :
  Membership.mem (γ := Set β)
    {a : β |
      Ne.{u_3 + 1} (α := R)
        (HahnSeries.coeff
          (if h : Membership.mem (γ := Set β) (Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)) a then
            (s : (a : α) → R⟦Γ⟧) (Classical.choose (p := fun (x : α) ↦ (f : (a : α) → β) x = a) h)
          else 0)
          g)
        0}
    b
⊢ Membership.mem (γ := Set β)
    (Set.image.{u_5, u_6} (α := α) (⇑f : (a : α) → β)
      (Function.support.{u_5, u_3} (M := R) fun (a : α) ↦ HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g))
    b
have pos : ∀ (hb : Membership.mem (γ := Set β) (Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)) b),
  Membership.mem (γ := Set β)
    (Set.image.{u_5, u_6} (α := α) (⇑f : (a : α) → β)
      (Function.support.{u_5, u_3} (M := R) fun (a : α) ↦ HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g))
    b
Tactic: by_cases hb : b ∈ Set.range f
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s : SummableFamily Γ R α
f : α ↪ β
g : Γ
b : β
h :
  Membership.mem (γ := Set β)
    {a : β |
      Ne.{u_3 + 1} (α := R)
        (HahnSeries.coeff
          (if h : Membership.mem (γ := Set β) (Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)) a then
            (s : (a : α) → R⟦Γ⟧) (Classical.choose (p := fun (x : α) ↦ (f : (a : α) → β) x = a) h)
          else 0)
          g)
        0}
    b
pos :
  ∀ (hb : Membership.mem (γ := Set β) (Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)) b),
    Membership.mem (γ := Set β)
      (Set.image.{u_5, u_6} (α := α) (⇑f : (a : α) → β)
        (Function.support.{u_5, u_3} (M := R) fun (a : α) ↦ HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g))
      b
⊢ Membership.mem (γ := Set β)
    (Set.image.{u_5, u_6} (α := α) (⇑f : (a : α) → β)
      (Function.support.{u_5, u_3} (M := R) fun (a : α) ↦ HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g))
    b
have neg : ∀ (hb : b ∉ Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)),
  Membership.mem (γ := Set β)
    (Set.image.{u_5, u_6} (α := α) (⇑f : (a : α) → β)
      (Function.support.{u_5, u_3} (M := R) fun (a : α) ↦ HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g))
    b
Tactic: by_cases hb : b ∈ Set.range f
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (hypothesis)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s : SummableFamily Γ R α
f : α ↪ β
g : Γ
b : β
h :
  Membership.mem (γ := Set β)
    {a : β |
      Ne.{u_3 + 1} (α := R)
        (HahnSeries.coeff
          (if h : Membership.mem (γ := Set β) (Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)) a then
            (s : (a : α) → R⟦Γ⟧) (Classical.choose (p := fun (x : α) ↦ (f : (a : α) → β) x = a) h)
          else 0)
          g)
        0}
    b
hb : Membership.mem (γ := Set β) (Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)) b
⊢ Membership.mem (γ := Set β)
    (Set.image.{u_5, u_6} (α := α) (⇑f : (a : α) → β)
      (Function.support.{u_5, u_3} (M := R) fun (a : α) ↦ HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g))
    b
have h₁ : ¬Eq.{u_3 + 1} (α := R)
    (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) (Classical.choose (p := fun (x : α) ↦ (f : (a : α) → β) x = b) hb)) g) 0
Tactic: simp only [Ne, Set.mem_setOf_eq, dif_pos hb] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s : SummableFamily Γ R α
f : α ↪ β
a : α
⊢ Eq (α := R⟦Γ⟧) ((s.embDomain f : (a : β) → R⟦Γ⟧) ((f : (a : α) → β) a) : R⟦Γ⟧) ((s : (a : α) → R⟦Γ⟧) a : R⟦Γ⟧)
have rw : Eq (α := R⟦Γ⟧)
  ((s : (a : α) → R⟦Γ⟧)
      (Classical.choose (p := fun (x : α) ↦ Eq.{u_6 + 1} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) a : β))
        sorry) :
    R⟦Γ⟧)
  ((s : (a : α) → R⟦Γ⟧) a : R⟦Γ⟧)
Tactic: rw [embDomain_apply, dif_pos (Set.mem_range_self a)]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s : SummableFamily Γ R α
f : α ↪ β
b : β
h : b ∉ Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)
⊢ Eq (α := R⟦Γ⟧) ((s.embDomain f : (a : β) → R⟦Γ⟧) b : R⟦Γ⟧) (0 : R⟦Γ⟧)
have rw : Eq (α := R⟦Γ⟧)
  (if h : Membership.mem (γ := Set β) (Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)) b then
    (s : (a : α) → R⟦Γ⟧) (Classical.choose (p := fun (x : α) ↦ (f : (a : α) → β) x = b) h)
  else 0)
  0
Tactic: rw [embDomain_apply, dif_neg h]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s : SummableFamily Γ R α
f : α ↪ β
b : β
h : b ∉ Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)
rw :
  Eq (α := R⟦Γ⟧)
    (if h : Membership.mem (γ := Set β) (Set.range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → β)) b then
      (s : (a : α) → R⟦Γ⟧) (Classical.choose (p := fun (x : α) ↦ (f : (a : α) → β) x = b) h)
    else 0)
    0
⊢ Eq (α := R⟦Γ⟧) ((s.embDomain f : (a : β) → R⟦Γ⟧) b : R⟦Γ⟧) (0 : R⟦Γ⟧)
have rw₁ : Eq (α := R⟦Γ⟧) 0 0
Tactic: rw [embDomain_apply, dif_neg h]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (goal)
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s : SummableFamily Γ R α
f : α ↪ β
⊢ (s.embDomain f).hsum = s.hsum
have coeff : ∀ (g : Γ), (s.embDomain f).hsum.coeff g = s.hsum.coeff g
Tactic: ext g