awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.PowerSeries (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Semiring Γ
inst_2 : PartialOrder Γ
inst_3 : IsStrictOrderedRing Γ
σ : Type u_3
inst_4 : Finite σ
f g : HahnSeries.{u_3, u_2} (σ →₀ ℕ) R
n : σ →₀ ℕ
⊢ {x ∈ addAntidiagonal (s := f.support) (t := g.support) ⋯ ⋯ n | f.coeff x.1 * g.coeff x.2 ≠ 0} =
    {x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n | f.coeff x.1 * g.coeff x.2 ≠ 0}
have h : ∀ (m : (σ →₀ ℕ) × (σ →₀ ℕ)),
  m ∈ {x ∈ addAntidiagonal (s := f.support) (t := g.support) sorry sorry n | f.coeff x.1 * g.coeff x.2 ≠ 0} ↔
    m ∈ {x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n | f.coeff x.1 * g.coeff x.2 ≠ 0}
Tactic: ext m
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.PowerSeries (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Semiring Γ
inst_2 : PartialOrder Γ
inst_3 : IsStrictOrderedRing Γ
σ : Type u_3
inst_4 : Finite σ
f g : HahnSeries.{u_3, u_2} (σ →₀ ℕ) R
n : σ →₀ ℕ
m : (σ →₀ ℕ) × (σ →₀ ℕ)
⊢ m ∈ {x ∈ addAntidiagonal (s := f.support) (t := g.support) ⋯ ⋯ n | f.coeff x.1 * g.coeff x.2 ≠ 0} ↔
    m ∈ {x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n | f.coeff x.1 * g.coeff x.2 ≠ 0}
have h : f.coeff m.1 * g.coeff m.2 ≠ 0 → (f.coeff m.1 ≠ 0 ∧ g.coeff m.2 ≠ 0 ∧ m.1 + m.2 = n ↔ m.1 + m.2 = n)
Tactic: simp only [and_congr_left_iff, mem_addAntidiagonal, mem_filter, mem_support,
        Finset.mem_antidiagonal]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.PowerSeries (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Semiring Γ
inst_2 : PartialOrder Γ
inst_3 : IsStrictOrderedRing Γ
σ : Type u_3
inst_4 : Finite σ
f g : HahnSeries.{u_3, u_2} (σ →₀ ℕ) R
n : σ →₀ ℕ
m : (σ →₀ ℕ) × (σ →₀ ℕ)
h : f.coeff m.1 * g.coeff m.2 ≠ 0
⊢ f.coeff m.1 ≠ 0 ∧ g.coeff m.2 ≠ 0 ∧ m.1 + m.2 = n ↔ m.1 + m.2 = n
have h₁ : g.coeff m.2 ≠ 0 ∧ m.1 + m.2 = n ↔ m.1 + m.2 = n
Tactic: rw [and_iff_right (left_ne_zero_of_mul h), and_iff_right (right_ne_zero_of_mul h)]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.PowerSeries (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Semiring Γ
inst_2 : PartialOrder Γ
inst_3 : IsStrictOrderedRing Γ
σ : Type u_3
inst_4 : Finite σ
f g : HahnSeries.{u_3, u_2} (σ →₀ ℕ) R
n : σ →₀ ℕ
m : (σ →₀ ℕ) × (σ →₀ ℕ)
h : f.coeff m.1 * g.coeff m.2 ≠ 0
h₁ : g.coeff m.2 ≠ 0 ∧ m.1 + m.2 = n ↔ m.1 + m.2 = n
⊢ f.coeff m.1 ≠ 0 ∧ g.coeff m.2 ≠ 0 ∧ m.1 + m.2 = n ↔ m.1 + m.2 = n
have h₂ : m.1 + m.2 = n ↔ m.1 + m.2 = n
Tactic: rw [and_iff_right (left_ne_zero_of_mul h), and_iff_right (right_ne_zero_of_mul h)]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.PowerSeries (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Semiring Γ
inst_2 : PartialOrder Γ
inst_3 : IsStrictOrderedRing Γ
σ : Type u_3
inst_4 : Finite σ
f g : HahnSeries.{u_3, u_2} (σ →₀ ℕ) R
n : σ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := R) ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (f * g).coeff : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (f.coeff * g.coeff) : R)
have h : (f * g).coeff n = (MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (f.coeff * g.coeff)
Tactic: classical
      change (f * g).coeff n = _
      simp_rw [coeff_mul]
      refine (sum_filter_ne_zero _).symm.trans <| (sum_congr ?_ fun _ _ ↦ rfl).trans <|
        sum_filter_ne_zero _
      ext m
      simp only [and_congr_left_iff, mem_addAntidiagonal, mem_filter, mem_support,
        Finset.mem_antidiagonal]
      rintro h
      rw [and_iff_right (left_ne_zero_of_mul h), and_iff_right (right_ne_zero_of_mul h)]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.PowerSeries (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Semiring Γ
inst_2 : PartialOrder Γ
inst_3 : IsStrictOrderedRing Γ
σ : Type u_3
inst_4 : Finite σ
f g : HahnSeries.{u_3, u_2} (σ →₀ ℕ) R
n : σ →₀ ℕ
h : (f * g).coeff n = (MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (f.coeff * g.coeff)
⊢ Eq.{u_2 + 1} (α := R) ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (f * g).coeff : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (f.coeff * g.coeff) : R)
have h₁ : Eq.{u_2 + 1} (α := R) (∑ ij ∈ addAntidiagonal (s := f.support) (t := g.support) sorry sorry n, f.coeff ij.1 * g.coeff ij.2 : R)
  ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (f.coeff * g.coeff) : R)
Tactic: classical
      change (f * g).coeff n = _
      simp_rw [coeff_mul]
      refine (sum_filter_ne_zero _).symm.trans <| (sum_congr ?_ fun _ _ ↦ rfl).trans <|
        sum_filter_ne_zero _
      ext m
      simp only [and_congr_left_iff, mem_addAntidiagonal, mem_filter, mem_support,
        Finset.mem_antidiagonal]
      rintro h
      rw [and_iff_right (left_ne_zero_of_mul h), and_iff_right (right_ne_zero_of_mul h)]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.PowerSeries (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Semiring Γ
inst_2 : PartialOrder Γ
inst_3 : IsStrictOrderedRing Γ
σ : Type u_3
inst_4 : Finite σ
f g : HahnSeries.{u_3, u_2} (σ →₀ ℕ) R
n : σ →₀ ℕ
h : (f * g).coeff n = (MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (f.coeff * g.coeff)
h₁ :
  Eq.{u_2 + 1} (α := R)
    (∑ ij ∈ addAntidiagonal (s := f.support) (t := g.support) ⋯ ⋯ n, f.coeff ij.1 * g.coeff ij.2 : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (f.coeff * g.coeff) : R)
⊢ Eq.{u_2 + 1} (α := R) ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (f * g).coeff : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (f.coeff * g.coeff) : R)
have h₂ : {x ∈ addAntidiagonal (s := f.support) (t := g.support) sorry sorry n | f.coeff x.1 * g.coeff x.2 ≠ 0} =
  {x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n | f.coeff x.1 * g.coeff x.2 ≠ 0}
Tactic: classical
      change (f * g).coeff n = _
      simp_rw [coeff_mul]
      refine (sum_filter_ne_zero _).symm.trans <| (sum_congr ?_ fun _ _ ↦ rfl).trans <|
        sum_filter_ne_zero _
      ext m
      simp only [and_congr_left_iff, mem_addAntidiagonal, mem_filter, mem_support,
        Finset.mem_antidiagonal]
      rintro h
      rw [and_iff_right (left_ne_zero_of_mul h), and_iff_right (right_ne_zero_of_mul h)]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.PowerSeries (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Semiring Γ
inst_2 : PartialOrder Γ
inst_3 : IsStrictOrderedRing Γ
σ : Type u_3
inst_4 : Finite σ
f g : HahnSeries.{u_3, u_2} (σ →₀ ℕ) R
n : σ →₀ ℕ
h : (f * g).coeff n = (MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (f.coeff * g.coeff)
h₁ :
  Eq.{u_2 + 1} (α := R)
    (∑ ij ∈ addAntidiagonal (s := f.support) (t := g.support) ⋯ ⋯ n, f.coeff ij.1 * g.coeff ij.2 : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (f.coeff * g.coeff) : R)
h₂ :
  {x ∈ addAntidiagonal (s := f.support) (t := g.support) ⋯ ⋯ n | f.coeff x.1 * g.coeff x.2 ≠ 0} =
    {x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n | f.coeff x.1 * g.coeff x.2 ≠ 0}
⊢ Eq.{u_2 + 1} (α := R) ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (f * g).coeff : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (f.coeff * g.coeff) : R)
have h₃ : ∀ (m : (σ →₀ ℕ) × (σ →₀ ℕ)),
  m ∈ {x ∈ addAntidiagonal (s := f.support) (t := g.support) sorry sorry n | f.coeff x.1 * g.coeff x.2 ≠ 0} ↔
    m ∈ {x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n | f.coeff x.1 * g.coeff x.2 ≠ 0}
Tactic: classical
      change (f * g).coeff n = _
      simp_rw [coeff_mul]
      refine (sum_filter_ne_zero _).symm.trans <| (sum_congr ?_ fun _ _ ↦ rfl).trans <|
        sum_filter_ne_zero _
      ext m
      simp only [and_congr_left_iff, mem_addAntidiagonal, mem_filter, mem_support,
        Finset.mem_antidiagonal]
      rintro h
      rw [and_iff_right (left_ne_zero_of_mul h), and_iff_right (right_ne_zero_of_mul h)]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.PowerSeries (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Semiring Γ
inst_2 : PartialOrder Γ
inst_3 : IsStrictOrderedRing Γ
σ : Type u_3
inst_4 : Finite σ
f g : HahnSeries.{u_3, u_2} (σ →₀ ℕ) R
n : σ →₀ ℕ
h : (f * g).coeff n = (MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (f.coeff * g.coeff)
h₁ :
  Eq.{u_2 + 1} (α := R)
    (∑ ij ∈ addAntidiagonal (s := f.support) (t := g.support) ⋯ ⋯ n, f.coeff ij.1 * g.coeff ij.2 : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (f.coeff * g.coeff) : R)
h₂ :
  {x ∈ addAntidiagonal (s := f.support) (t := g.support) ⋯ ⋯ n | f.coeff x.1 * g.coeff x.2 ≠ 0} =
    {x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n | f.coeff x.1 * g.coeff x.2 ≠ 0}
h₃ :
  ∀ (m : (σ →₀ ℕ) × (σ →₀ ℕ)),
    m ∈ {x ∈ addAntidiagonal (s := f.support) (t := g.support) ⋯ ⋯ n | f.coeff x.1 * g.coeff x.2 ≠ 0} ↔
      m ∈ {x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n | f.coeff x.1 * g.coeff x.2 ≠ 0}
⊢ Eq.{u_2 + 1} (α := R) ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (f * g).coeff : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (f.coeff * g.coeff) : R)
have h₄ : ∀ (m : (σ →₀ ℕ) × (σ →₀ ℕ)),
  f.coeff m.1 * g.coeff m.2 ≠ 0 → (f.coeff m.1 ≠ 0 ∧ g.coeff m.2 ≠ 0 ∧ m.1 + m.2 = n ↔ m.1 + m.2 = n)
Tactic: classical
      change (f * g).coeff n = _
      simp_rw [coeff_mul]
      refine (sum_filter_ne_zero _).symm.trans <| (sum_congr ?_ fun _ _ ↦ rfl).trans <|
        sum_filter_ne_zero _
      ext m
      simp only [and_congr_left_iff, mem_addAntidiagonal, mem_filter, mem_support,
        Finset.mem_antidiagonal]
      rintro h
      rw [and_iff_right (left_ne_zero_of_mul h), and_iff_right (right_ne_zero_of_mul h)]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.PowerSeries (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : Semiring Γ
inst_2 : PartialOrder Γ
inst_3 : IsStrictOrderedRing Γ
σ : Type u_3
inst_4 : Finite σ
f g : HahnSeries.{u_3, u_2} (σ →₀ ℕ) R
⊢ (f + g).coeff = f.coeff + g.coeff
have h : ∀ (n : σ →₀ ℕ),
  Eq.{u_2 + 1} (α := R) ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (f + g).coeff : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (f.coeff + g.coeff) : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.PowerSeries (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
r : R
⊢ Eq.{u_3 + 1} (α := PowerSeries A)
    (Equiv.toFun (α := A⟦ℕ⟧) (RingEquiv.toEquiv toPowerSeries) ((algebraMap R A⟦ℕ⟧ : (a : R) → A⟦ℕ⟧) r))
    ((algebraMap R (PowerSeries A) : (a : R) → PowerSeries A) r)
have h : ∀ (n : ℕ),
  Eq.{u_3 + 1} (α := A)
    ((PowerSeries.coeff n : (a : PowerSeries A) → A)
        (Equiv.toFun (α := A⟦ℕ⟧) (RingEquiv.toEquiv toPowerSeries) ((algebraMap R A⟦ℕ⟧ : (a : R) → A⟦ℕ⟧) r)) :
      A)
    ((PowerSeries.coeff n : (a : PowerSeries A) → A)
        ((algebraMap R (PowerSeries A) : (a : R) → PowerSeries A) r : PowerSeries A) :
      A)
Tactic: ext n
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.PowerSeries (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
r : R
n : ℕ
⊢ Eq.{u_3 + 1} (α := A)
    ((PowerSeries.coeff n : (a : PowerSeries A) → A)
        (Equiv.toFun (α := A⟦ℕ⟧) (RingEquiv.toEquiv toPowerSeries) ((algebraMap R A⟦ℕ⟧ : (a : R) → A⟦ℕ⟧) r)) :
      A)
    ((PowerSeries.coeff n : (a : PowerSeries A) → A)
        ((algebraMap R (PowerSeries A) : (a : R) → PowerSeries A) r : PowerSeries A) :
      A)
have h : Eq.{u_3 + 1} (α := A)
  ((PowerSeries.coeff 0 : (a : PowerSeries A) → A)
      (Equiv.toFun (α := A⟦ℕ⟧) (RingEquiv.toEquiv toPowerSeries) ((algebraMap R A⟦ℕ⟧ : (a : R) → A⟦ℕ⟧) r)) :
    A)
  ((PowerSeries.coeff 0 : (a : PowerSeries A) → A)
      ((algebraMap R (PowerSeries A) : (a : R) → PowerSeries A) r : PowerSeries A) :
    A)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.PowerSeries (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : CommSemiring R
A : Type u_3
inst_1 : Semiring A
inst_2 : Algebra R A
r : R
n : ℕ
h :
  Eq.{u_3 + 1} (α := A)
    ((PowerSeries.coeff 0 : (a : PowerSeries A) → A)
        (Equiv.toFun (α := A⟦ℕ⟧) (RingEquiv.toEquiv toPowerSeries) ((algebraMap R A⟦ℕ⟧ : (a : R) → A⟦ℕ⟧) r)) :
      A)
    ((PowerSeries.coeff 0 : (a : PowerSeries A) → A)
        ((algebraMap R (PowerSeries A) : (a : R) → PowerSeries A) r : PowerSeries A) :
      A)
⊢ Eq.{u_3 + 1} (α := A)
    ((PowerSeries.coeff n : (a : PowerSeries A) → A)
        (Equiv.toFun (α := A⟦ℕ⟧) (RingEquiv.toEquiv toPowerSeries) ((algebraMap R A⟦ℕ⟧ : (a : R) → A⟦ℕ⟧) r)) :
      A)
    ((PowerSeries.coeff n : (a : PowerSeries A) → A)
        ((algebraMap R (PowerSeries A) : (a : R) → PowerSeries A) r : PowerSeries A) :
      A)
have h₁ : ∀ (n : ℕ),
  Eq.{u_3 + 1} (α := A)
    ((PowerSeries.coeff (n + 1) : (a : PowerSeries A) → A)
        (Equiv.toFun (α := A⟦ℕ⟧) (RingEquiv.toEquiv toPowerSeries) ((algebraMap R A⟦ℕ⟧ : (a : R) → A⟦ℕ⟧) r)) :
      A)
    ((PowerSeries.coeff (n + 1) : (a : PowerSeries A) → A)
        ((algebraMap R (PowerSeries A) : (a : R) → PowerSeries A) r : PowerSeries A) :
      A)
Tactic: cases n
Cleared hypotheses: n
-- 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
x y : SummableFamily Γ R α
⊢ Subset.{u_1} (α := Set Γ)
    (⋃ (a : α),
      (HAdd.hAdd (α := (a : α) → R⟦Γ⟧) (β := (a : α) → R⟦Γ⟧) (⇑x : (a : α) → R⟦Γ⟧) (⇑y : (a : α) → R⟦Γ⟧) a).support)
    ((⋃ (a : α), support.{u_1, u_3} (R := R) ((x : (a : α) → R⟦Γ⟧) a)) ∪
      ⋃ (a : α), support.{u_1, u_3} (R := R) ((y : (a : α) → R⟦Γ⟧) a))
have rw : Subset.{u_1} (α := Set Γ)
  (⋃ (a : α),
    (HAdd.hAdd (α := (a : α) → R⟦Γ⟧) (β := (a : α) → R⟦Γ⟧) (⇑x : (a : α) → R⟦Γ⟧) (⇑y : (a : α) → R⟦Γ⟧) a).support)
  (⋃ (i : α),
    support.{u_1, u_3} (R := R) ((x : (a : α) → R⟦Γ⟧) i) ∪ support.{u_1, u_3} (R := R) ((y : (a : α) → R⟦Γ⟧) i))
Tactic: rw [← Set.iUnion_union_distrib]
-- 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
x y : SummableFamily Γ R α
g : Γ
a : α
ha :
  Membership.mem (γ := Set α)
    {a : α |
      (HAdd.hAdd (α := (a : α) → R⟦Γ⟧) (β := (a : α) → R⟦Γ⟧) (⇑x : (a : α) → R⟦Γ⟧) (⇑y : (a : α) → R⟦Γ⟧) a).coeff g ≠ 0}
    a
⊢ Membership.mem (γ := Set α)
    ((Function.support.{u_5, u_3} (M := R) fun (a : α) ↦ coeff ((x : (a : α) → R⟦Γ⟧) a) g) ∪
      Function.support.{u_5, u_3} (M := R) fun (a : α) ↦ coeff ((y : (a : α) → R⟦Γ⟧) a) g)
    a
have ha₁ : HAdd.hAdd (α := R) (coeff ((x : (a : α) → R⟦Γ⟧) a) g) (coeff ((y : (a : α) → R⟦Γ⟧) a) g) ≠ 0
Tactic: change (x a).coeff g + (y a).coeff g ≠ 0 at ha
Cleared hypotheses: 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
x y : SummableFamily Γ R α
g : Γ
a : α
ha : HAdd.hAdd (α := R) (coeff ((x : (a : α) → R⟦Γ⟧) a) g) (coeff ((y : (a : α) → R⟦Γ⟧) a) g) ≠ 0
⊢ Ne.{u_3 + 1} (α := R) (coeff ((x : (a : α) → R⟦Γ⟧) a) g) 0 ∨
    Ne.{u_3 + 1} (α := R) (coeff ((y : (a : α) → R⟦Γ⟧) a) g) 0
have contrapose! : ∀
  (ha :
    Eq.{u_3 + 1} (α := R) (coeff ((x : (a : α) → R⟦Γ⟧) a) g) 0 ∧
      Eq.{u_3 + 1} (α := R) (coeff ((y : (a : α) → R⟦Γ⟧) a) g) 0),
  HAdd.hAdd (α := R) (coeff ((x : (a : α) → R⟦Γ⟧) a) g) (coeff ((y : (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
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
x y : SummableFamily Γ R α
g : Γ
a : α
ha :
  Eq.{u_3 + 1} (α := R) (coeff ((x : (a : α) → R⟦Γ⟧) a) g) 0 ∧
    Eq.{u_3 + 1} (α := R) (coeff ((y : (a : α) → R⟦Γ⟧) a) g) 0
⊢ HAdd.hAdd (α := R) (coeff ((x : (a : α) → R⟦Γ⟧) a) g) (coeff ((y : (a : α) → R⟦Γ⟧) a) g) = 0
have rw : HAdd.hAdd (α := R) 0 (coeff ((y : (a : α) → R⟦Γ⟧) a) g) = 0
Tactic: rw [ha.1, ha.2, add_zero]
-- 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
x y : SummableFamily Γ R α
g : Γ
a : α
ha :
  Eq.{u_3 + 1} (α := R) (coeff ((x : (a : α) → R⟦Γ⟧) a) g) 0 ∧
    Eq.{u_3 + 1} (α := R) (coeff ((y : (a : α) → R⟦Γ⟧) a) g) 0
rw : HAdd.hAdd (α := R) 0 (coeff ((y : (a : α) → R⟦Γ⟧) a) g) = 0
⊢ HAdd.hAdd (α := R) (coeff ((x : (a : α) → R⟦Γ⟧) a) g) (coeff ((y : (a : α) → R⟦Γ⟧) a) g) = 0
have rw₁ : HAdd.hAdd (α := R) 0 0 = 0
Tactic: rw [ha.1, ha.2, add_zero]
-- 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
x y : SummableFamily Γ R α
g : Γ
a : α
ha :
  Eq.{u_3 + 1} (α := R) (coeff ((x : (a : α) → R⟦Γ⟧) a) g) 0 ∧
    Eq.{u_3 + 1} (α := R) (coeff ((y : (a : α) → R⟦Γ⟧) a) g) 0
rw : HAdd.hAdd (α := R) 0 (coeff ((y : (a : α) → R⟦Γ⟧) a) g) = 0
rw₁ : HAdd.hAdd (α := R) 0 0 = 0
⊢ HAdd.hAdd (α := R) (coeff ((x : (a : α) → R⟦Γ⟧) a) g) (coeff ((y : (a : α) → R⟦Γ⟧) a) g) = 0
have rw₂ : Eq.{u_3 + 1} (α := R) 0 0
Tactic: rw [ha.1, ha.2, add_zero]
-- 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
M : Type u_7
inst_2 : SMulZeroClass M R
r : M
t : SummableFamily Γ R β
g : Γ
⊢ Set.Finite.{u_6} (α := β) {a : β | (HSMul.hSMul (β := (a : β) → R⟦Γ⟧) r (⇑t : (a : β) → R⟦Γ⟧) a).coeff g ≠ 0}
have refine : Subset.{u_6} (α := Set β) {a : β | (HSMul.hSMul (β := (a : β) → R⟦Γ⟧) r (⇑t : (a : β) → R⟦Γ⟧) a).coeff g ≠ 0}
  (Function.support.{u_6, u_3} (M := R) fun (a : β) ↦ coeff ((t : (a : β) → R⟦Γ⟧) a) g)
Tactic: refine (t.finite_co_support g).subset ?_
-- 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 α
g : Γ
⊢ Membership.mem (γ := Set Γ)
      (Function.support.{u_1, u_3} (M := R) fun (g : Γ) ↦ ∑ᶠ (i : α), HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g) g →
    Membership.mem (γ := Set Γ) (⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) g
have contrapose : g ∉ ⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a) →
  g ∉ Function.support.{u_1, u_3} (M := R) fun (g : Γ) ↦ ∑ᶠ (i : α), HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g
Tactic: contrapose
-- 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 α
g : Γ
⊢ g ∉ ⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a) →
    g ∉ Function.support.{u_1, u_3} (M := R) fun (g : Γ) ↦ ∑ᶠ (i : α), HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g
have rw : (∀ (x : α), g ∉ support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) x)) →
  Eq.{u_3 + 1} (α := R) (∑ᶠ (i : α), HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g) 0
Tactic: rw [Set.mem_iUnion, not_exists, Function.mem_support, Classical.not_not]
-- 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 α
g : Γ
⊢ (∀ (x : α), g ∉ support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) x)) →
    Eq.{u_3 + 1} (α := R) (∑ᶠ (i : α), HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g) 0
have simp_rw : (∀ (x : α), Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) x) g) 0) →
  Eq.{u_3 + 1} (α := R) (∑ᶠ (i : α), HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g) 0
Tactic: simp_rw [mem_support, Classical.not_not]
-- 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 α
g : Γ
h : ∀ (x : α), Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) x) g) 0
⊢ Eq.{u_3 + 1} (α := R) (∑ᶠ (i : α), HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g) 0
have rw : Eq.{u_3 + 1} (α := R) (∑ᶠ (x : α), 0) 0
Tactic: rw [finsum_congr h, finsum_zero]
-- 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 α
g : Γ
h : ∀ (x : α), Eq.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) x) g) 0
rw : Eq.{u_3 + 1} (α := R) (∑ᶠ (x : α), 0) 0
⊢ Eq.{u_3 + 1} (α := R) (∑ᶠ (i : α), HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g) 0
have rw₁ : Eq.{u_3 + 1} (α := R) 0 0
Tactic: rw [finsum_congr h, finsum_zero]
-- 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
⊢ Eq (α := R⟦Γ⟧) (hsum.{u_1, u_3, u_5} (α := α) 0) 0
have coeff : ∀ (x : Γ), Eq.{u_3 + 1} (α := R) (HahnSeries.coeff (hsum.{u_1, u_3, u_5} (α := α) 0) x) (HahnSeries.coeff 0 x)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Summable (hypothesis)
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
hg : g ∈ s.hsum.support
⊢ Membership.mem (γ := Set Γ) (⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) g
have hg₁ : Ne.{u_3 + 1} (α := R)
  (∑
    i ∈
      Set.Finite.toFinset (s :=
        Function.support.{u_5, u_3} (M := R) fun (a : α) ↦ HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g) sorry,
    HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g)
  0
Tactic: rw [mem_support, coeff_hsum, finsum_eq_sum _ (s.finite_co_support _)] at hg
Cleared hypotheses: hg
-- 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
s : SummableFamily Γ R α
g : Γ
hg :
  Ne.{u_3 + 1} (α := R)
    (∑
      i ∈
        Set.Finite.toFinset (s :=
          Function.support.{u_5, u_3} (M := R) fun (a : α) ↦ HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g) ⋯,
      HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g)
    0
⊢ Membership.mem (γ := Set Γ) (⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) g
have obtain : ∀
  a ∈
    Set.Finite.toFinset (s :=
      Function.support.{u_5, u_3} (M := R) fun (a : α) ↦ HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g) sorry,
  ∀ (h2 : Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g) 0),
    Membership.mem (γ := Set Γ) (⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) g
Tactic: obtain ⟨a, _, h2⟩ := exists_ne_zero_of_sum_ne_zero hg
-- 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
s : SummableFamily Γ R α
g : Γ
hg :
  Ne.{u_3 + 1} (α := R)
    (∑
      i ∈
        Set.Finite.toFinset (s :=
          Function.support.{u_5, u_3} (M := R) fun (a : α) ↦ HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g) ⋯,
      HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) i) g)
    0
a : α
left :
  a ∈
    Set.Finite.toFinset (s :=
      Function.support.{u_5, u_3} (M := R) fun (a : α) ↦ HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g) ⋯
h2 : Ne.{u_3 + 1} (α := R) (HahnSeries.coeff ((s : (a : α) → R⟦Γ⟧) a) g) 0
⊢ Membership.mem (γ := Set Γ) (⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a)) g
have rw : ∃ (i : α), Membership.mem (γ := Set Γ) (support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) i)) g
Tactic: rw [Set.mem_iUnion]
-- 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
s t : SummableFamily Γ R α
⊢ (s + t).hsum = s.hsum + t.hsum
have coeff : ∀ (g : Γ), (s + t).hsum.coeff g = (s.hsum + t.hsum).coeff g
Tactic: ext g