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
f g : R⟦ℕ⟧
n : ℕ
⊢ Eq.{u_2 + 1} (α := R) (∑ ij ∈ addAntidiagonal (s := f.support) (t := g.support) ⋯ ⋯ n, f.coeff ij.1 * g.coeff ij.2)
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, f.coeff x.1 * g.coeff x.2)
have h : {x ∈ addAntidiagonal (s := f.support) (t := g.support) sorry sorry n | f.coeff x.1 * g.coeff x.2 ≠ 0} =
  {x ∈ @antidiagonal _ Nat.instAddMonoid _ n | f.coeff x.1 * g.coeff x.2 ≠ 0}
Tactic: classical
    refine (sum_filter_ne_zero _).symm.trans <| (sum_congr ?_ fun _ _ ↦ rfl).trans <|
      sum_filter_ne_zero _
    ext m
    simp only [mem_antidiagonal, mem_addAntidiagonal, and_congr_left_iff, mem_filter,
      mem_support]
    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
f g : R⟦ℕ⟧
n : ℕ
h :
  {x ∈ addAntidiagonal (s := f.support) (t := g.support) ⋯ ⋯ n | f.coeff x.1 * g.coeff x.2 ≠ 0} =
    {x ∈ @antidiagonal _ Nat.instAddMonoid _ n | f.coeff x.1 * g.coeff x.2 ≠ 0}
⊢ Eq.{u_2 + 1} (α := R) (∑ ij ∈ addAntidiagonal (s := f.support) (t := g.support) ⋯ ⋯ n, f.coeff ij.1 * g.coeff ij.2)
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, f.coeff x.1 * g.coeff x.2)
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 _ Nat.instAddMonoid _ n | f.coeff x.1 * g.coeff x.2 ≠ 0}
Tactic: classical
    refine (sum_filter_ne_zero _).symm.trans <| (sum_congr ?_ fun _ _ ↦ rfl).trans <|
      sum_filter_ne_zero _
    ext m
    simp only [mem_antidiagonal, mem_addAntidiagonal, and_congr_left_iff, mem_filter,
      mem_support]
    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
f g : R⟦ℕ⟧
n : ℕ
h :
  {x ∈ addAntidiagonal (s := f.support) (t := g.support) ⋯ ⋯ n | f.coeff x.1 * g.coeff x.2 ≠ 0} =
    {x ∈ @antidiagonal _ Nat.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 _ Nat.instAddMonoid _ n | f.coeff x.1 * g.coeff x.2 ≠ 0}
⊢ Eq.{u_2 + 1} (α := R) (∑ ij ∈ addAntidiagonal (s := f.support) (t := g.support) ⋯ ⋯ n, f.coeff ij.1 * g.coeff ij.2)
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n, f.coeff x.1 * g.coeff x.2)
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
    refine (sum_filter_ne_zero _).symm.trans <| (sum_congr ?_ fun _ _ ↦ rfl).trans <|
      sum_filter_ne_zero _
    ext m
    simp only [mem_antidiagonal, mem_addAntidiagonal, and_congr_left_iff, mem_filter,
      mem_support]
    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
f g : R⟦ℕ⟧
⊢ PowerSeries.mk (f + g).coeff = PowerSeries.mk f.coeff + PowerSeries.mk g.coeff
have h : ∀ (n : ℕ),
  Eq (α := R) ((PowerSeries.coeff n : (a : PowerSeries R) → R) (PowerSeries.mk (f + g).coeff) : R)
    ((PowerSeries.coeff n : (a : PowerSeries R) → R) (PowerSeries.mk f.coeff + PowerSeries.mk g.coeff) : R)
Tactic: ext
-- 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 Γ
x : PowerSeries R
⊢ ∀ {a b : ℕ},
    LE.le.{u_1} (α := Γ) (({ toFun := Nat.cast, inj' := ⋯ } : (a : ℕ) → Γ) a : Γ)
        (({ toFun := Nat.cast, inj' := ⋯ } : (a : ℕ) → Γ) b : Γ) ↔
      a ≤ b
have simp : ∀ {a b : ℕ}, LE.le.{u_1} (α := Γ) (↑a : Γ) (↑b : Γ) ↔ a ≤ b
Tactic: simp only [Function.Embedding.coeFn_mk]
-- 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 Γ
r : R
⊢ Eq (α := R⟦Γ⟧)
    (((ofPowerSeries Γ R : PowerSeries R →+* R⟦Γ⟧) : (a : PowerSeries R) → R⟦Γ⟧)
        ((PowerSeries.C : (a : R) → PowerSeries R) r) :
      R⟦Γ⟧)
    ((C : (a : R) → R⟦Γ⟧) r : R⟦Γ⟧)
have coeff : ∀ (n : Γ),
  Eq.{u_2 + 1} (α := R)
    (coeff
      (((ofPowerSeries Γ R : PowerSeries R →+* R⟦Γ⟧) : (a : PowerSeries R) → R⟦Γ⟧)
        ((PowerSeries.C : (a : R) → PowerSeries R) r))
      n)
    (coeff ((C : (a : R) → R⟦Γ⟧) r) n)
Tactic: ext n
-- 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 Γ
r : R
n : Γ
⊢ Eq.{u_2 + 1} (α := R)
    (coeff
      (((ofPowerSeries Γ R : PowerSeries R →+* R⟦Γ⟧) : (a : PowerSeries R) → R⟦Γ⟧)
        ((PowerSeries.C : (a : R) → PowerSeries R) r))
      n)
    (coeff ((C : (a : R) → R⟦Γ⟧) r) n)
have coeff : coeff
    (embDomain
      (RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ) ↦ x1 ≤ x2)
        { toFun := Nat.cast, inj' := sorry : ℕ ↪ Γ } sorry)
      ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) ((PowerSeries.C : (a : R) → PowerSeries R) r)))
    n =
  if n = 0 then r else 0
Tactic: simp only [ofPowerSeries_apply, C, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
    coeff_single]
-- 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 Γ
r : R
n : Γ
⊢ coeff
      (embDomain
        (RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ) ↦ x1 ≤ x2)
          { toFun := Nat.cast, inj' := ⋯ : ℕ ↪ Γ } ⋯)
        ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) ((PowerSeries.C : (a : R) → PowerSeries R) r)))
      n =
    if n = 0 then r else 0
have pos : ∀ (hn : n = 0),
  coeff
      (embDomain
        (RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ) ↦ x1 ≤ x2)
          { toFun := Nat.cast, inj' := sorry : ℕ ↪ Γ } sorry)
        ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) ((PowerSeries.C : (a : R) → PowerSeries R) r)))
      n =
    r
Tactic: split_ifs with hn
-- 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 Γ
r : R
n : Γ
pos :
  ∀ (hn : n = 0),
    coeff
        (embDomain
          (RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ) ↦ x1 ≤ x2)
            { toFun := Nat.cast, inj' := ⋯ : ℕ ↪ Γ } ⋯)
          ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) ((PowerSeries.C : (a : R) → PowerSeries R) r)))
        n =
      r
⊢ coeff
      (embDomain
        (RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ) ↦ x1 ≤ x2)
          { toFun := Nat.cast, inj' := ⋯ : ℕ ↪ Γ } ⋯)
        ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) ((PowerSeries.C : (a : R) → PowerSeries R) r)))
      n =
    if n = 0 then r else 0
have neg : ∀ (hn : ¬n = 0),
  Eq.{u_2 + 1} (α := R)
    (coeff
      (embDomain
        (RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ) ↦ x1 ≤ x2)
          { toFun := Nat.cast, inj' := sorry : ℕ ↪ Γ } sorry)
        ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) ((PowerSeries.C : (a : R) → PowerSeries R) r)))
      n)
    0
Tactic: split_ifs with hn
-- 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 Γ
r : R
n : Γ
hn : n = 0
⊢ coeff
      (embDomain
        (RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ) ↦ x1 ≤ x2)
          { toFun := Nat.cast, inj' := ⋯ : ℕ ↪ Γ } ⋯)
        ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) ((PowerSeries.C : (a : R) → PowerSeries R) r)))
      n =
    r
have pos : coeff.{u_1, u_2} (Γ := Γ)
    (embDomain
      (RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ) ↦ x1 ≤ x2)
        { toFun := Nat.cast, inj' := sorry : ℕ ↪ Γ } sorry)
      ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) ((PowerSeries.C : (a : R) → PowerSeries R) r)))
    0 =
  r
Tactic: subst hn
Cleared hypotheses: n, hn
-- 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 Γ
r : R
⊢ coeff.{u_1, u_2} (Γ := Γ)
      (embDomain
        (RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ) ↦ x1 ≤ x2)
          { toFun := Nat.cast, inj' := ⋯ : ℕ ↪ Γ } ⋯)
        ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) ((PowerSeries.C : (a : R) → PowerSeries R) r)))
      0 =
    r
have h : Eq.{u_1 + 1} (α := Γ) (0 : Γ)
  ((RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ) ↦ x1 ≤ x2) { toFun := Nat.cast, inj' := sorry }
          sorry :
        (a : ℕ) → Γ)
      0 :
    Γ)
Tactic: convert! embDomain_coeff (a := 0)
-- 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 Γ
r : R
h :
  Eq.{u_1 + 1} (α := Γ) (0 : Γ)
    ((RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ) ↦ x1 ≤ x2) { toFun := Nat.cast, inj' := ⋯ }
            ⋯ :
          (a : ℕ) → Γ)
        0 :
      Γ)
⊢ coeff.{u_1, u_2} (Γ := Γ)
      (embDomain
        (RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ) ↦ x1 ≤ x2)
          { toFun := Nat.cast, inj' := ⋯ : ℕ ↪ Γ } ⋯)
        ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) ((PowerSeries.C : (a : R) → PowerSeries R) r)))
      0 =
    r
have h₁ : r =
  coeff (Γ := ℕ)
    ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) ((PowerSeries.C : (a : R) → PowerSeries R) r)) 0
Tactic: convert! embDomain_coeff (a := 0)
-- 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 Γ
r : R
n : Γ
hn : ¬n = 0
⊢ Eq.{u_2 + 1} (α := R)
    (coeff
      (embDomain
        (RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ) ↦ x1 ≤ x2)
          { toFun := Nat.cast, inj' := ⋯ : ℕ ↪ Γ } ⋯)
        ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) ((PowerSeries.C : (a : R) → PowerSeries R) r)))
      n)
    0
have neg : n ∉
  Set.image (α := ℕ)
    (⇑(RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ) ↦ x1 ≤ x2)
          { toFun := Nat.cast, inj' := sorry } sorry) :
      (a : ℕ) → Γ)
    (support.{0, u_2} (R := R)
      ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) ((PowerSeries.C : (a : R) → PowerSeries R) r)))
Tactic: rw [embDomain_notin_image_support]
-- 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 Γ
r : R
n : Γ
hn : ¬n = 0
⊢ n ∉
    Set.image (α := ℕ)
      (⇑(RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ) ↦ x1 ≤ x2)
            { toFun := Nat.cast, inj' := ⋯ } ⋯) :
        (a : ℕ) → Γ)
      (support.{0, u_2} (R := R)
        ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) ((PowerSeries.C : (a : R) → PowerSeries R) r)))
have neg : ∀ (x : ℕ),
  ¬((if x = 0 then r else 0) ≠ 0 ∧
      (RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ) ↦ x1 ≤ x2)
              { toFun := Nat.cast, inj' := sorry } sorry :
            (a : ℕ) → Γ)
          x =
        n)
Tactic: simp only [not_exists, Set.mem_image, toPowerSeries_symm_apply_coeff, mem_support,
      PowerSeries.coeff_C]
-- 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 Γ
⊢ Eq (α := R⟦Γ⟧) (((ofPowerSeries Γ R : PowerSeries R →+* R⟦Γ⟧) : (a : PowerSeries R) → R⟦Γ⟧) PowerSeries.X : R⟦Γ⟧)
    ((single 1 : (a : R) → R⟦Γ⟧) 1 : R⟦Γ⟧)
have coeff : ∀ (n : Γ),
  Eq.{u_2 + 1} (α := R)
    (coeff (((ofPowerSeries Γ R : PowerSeries R →+* R⟦Γ⟧) : (a : PowerSeries R) → R⟦Γ⟧) PowerSeries.X) n)
    (coeff ((single 1 : (a : R) → R⟦Γ⟧) 1) n)
Tactic: ext n
-- 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 Γ
n : Γ
⊢ Eq.{u_2 + 1} (α := R)
    (coeff (((ofPowerSeries Γ R : PowerSeries R →+* R⟦Γ⟧) : (a : PowerSeries R) → R⟦Γ⟧) PowerSeries.X) n)
    (coeff ((single 1 : (a : R) → R⟦Γ⟧) 1) n)
have coeff : Eq.{u_2 + 1} (α := R)
  (coeff
    (embDomain
      (RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ) ↦ x1 ≤ x2)
        { toFun := Nat.cast, inj' := sorry : ℕ ↪ Γ } sorry)
      ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) PowerSeries.X))
    n)
  (if n = 1 then 1 else 0)
Tactic: simp only [coeff_single, ofPowerSeries_apply]
-- 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 Γ
n : Γ
⊢ Eq.{u_2 + 1} (α := R)
    (coeff
      (embDomain
        (RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ) ↦ x1 ≤ x2)
          { toFun := Nat.cast, inj' := ⋯ : ℕ ↪ Γ } ⋯)
        ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) PowerSeries.X))
      n)
    (if n = 1 then 1 else 0)
have pos : ∀ (hn : n = 1),
  Eq.{u_2 + 1} (α := R)
    (coeff
      (embDomain
        (RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ) ↦ x1 ≤ x2)
          { toFun := Nat.cast, inj' := sorry : ℕ ↪ Γ } sorry)
        ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) PowerSeries.X))
      n)
    1
Tactic: split_ifs with hn
-- 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 Γ
n : Γ
pos :
  ∀ (hn : n = 1),
    Eq.{u_2 + 1} (α := R)
      (coeff
        (embDomain
          (RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ) ↦ x1 ≤ x2)
            { toFun := Nat.cast, inj' := ⋯ : ℕ ↪ Γ } ⋯)
          ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) PowerSeries.X))
        n)
      1
⊢ Eq.{u_2 + 1} (α := R)
    (coeff
      (embDomain
        (RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ) ↦ x1 ≤ x2)
          { toFun := Nat.cast, inj' := ⋯ : ℕ ↪ Γ } ⋯)
        ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) PowerSeries.X))
      n)
    (if n = 1 then 1 else 0)
have neg : ∀ (hn : ¬n = 1),
  Eq.{u_2 + 1} (α := R)
    (coeff
      (embDomain
        (RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ) ↦ x1 ≤ x2)
          { toFun := Nat.cast, inj' := sorry : ℕ ↪ Γ } sorry)
        ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) PowerSeries.X))
      n)
    0
Tactic: split_ifs with hn
-- 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 Γ
n : Γ
hn : n = 1
⊢ Eq.{u_2 + 1} (α := R)
    (coeff
      (embDomain
        (RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ) ↦ x1 ≤ x2)
          { toFun := Nat.cast, inj' := ⋯ : ℕ ↪ Γ } ⋯)
        ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) PowerSeries.X))
      n)
    1
have pos : Eq.{u_2 + 1} (α := R)
  (coeff.{u_1, u_2} (Γ := Γ)
    (embDomain
      (RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ) ↦ x1 ≤ x2)
        { toFun := Nat.cast, inj' := sorry : ℕ ↪ Γ } sorry)
      ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) PowerSeries.X))
    1)
  1
Tactic: rw [hn]
-- 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 Γ
n : Γ
hn : n = 1
⊢ Eq.{u_2 + 1} (α := R)
    (coeff.{u_1, u_2} (Γ := Γ)
      (embDomain
        (RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ) ↦ x1 ≤ x2)
          { toFun := Nat.cast, inj' := ⋯ : ℕ ↪ Γ } ⋯)
        ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) PowerSeries.X))
      1)
    1
have h : Eq.{u_1 + 1} (α := Γ) (1 : Γ)
  ((RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ) ↦ x1 ≤ x2) { toFun := Nat.cast, inj' := sorry }
          sorry :
        (a : ℕ) → Γ)
      1 :
    Γ)
Tactic: convert! embDomain_coeff (a := 1)
-- 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 Γ
n : Γ
hn : n = 1
h :
  Eq.{u_1 + 1} (α := Γ) (1 : Γ)
    ((RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ) ↦ x1 ≤ x2) { toFun := Nat.cast, inj' := ⋯ }
            ⋯ :
          (a : ℕ) → Γ)
        1 :
      Γ)
⊢ Eq.{u_2 + 1} (α := R)
    (coeff.{u_1, u_2} (Γ := Γ)
      (embDomain
        (RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ) ↦ x1 ≤ x2)
          { toFun := Nat.cast, inj' := ⋯ : ℕ ↪ Γ } ⋯)
        ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) PowerSeries.X))
      1)
    1
have h₁ : Eq.{u_2 + 1} (α := R) 1 (coeff (Γ := ℕ) ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) PowerSeries.X) 1)
Tactic: convert! embDomain_coeff (a := 1)
-- 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 Γ
n : Γ
hn : ¬n = 1
⊢ Eq.{u_2 + 1} (α := R)
    (coeff
      (embDomain
        (RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ) ↦ x1 ≤ x2)
          { toFun := Nat.cast, inj' := ⋯ : ℕ ↪ Γ } ⋯)
        ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) PowerSeries.X))
      n)
    0
have neg : n ∉
  Set.image (α := ℕ)
    (⇑(RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ) ↦ x1 ≤ x2)
          { toFun := Nat.cast, inj' := sorry } sorry) :
      (a : ℕ) → Γ)
    (support.{0, u_2} (R := R) ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) PowerSeries.X))
Tactic: rw [embDomain_notin_image_support]
-- 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 Γ
n : Γ
hn : ¬n = 1
⊢ n ∉
    Set.image (α := ℕ)
      (⇑(RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ) ↦ x1 ≤ x2)
            { toFun := Nat.cast, inj' := ⋯ } ⋯) :
        (a : ℕ) → Γ)
      (support.{0, u_2} (R := R) ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) PowerSeries.X))
have neg : ∀ (x : ℕ),
  ¬(Ne.{u_2 + 1} (α := R) (if x = 1 then 1 else 0) 0 ∧
      (RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ) ↦ x1 ≤ x2)
              { toFun := Nat.cast, inj' := sorry } sorry :
            (a : ℕ) → Γ)
          x =
        n)
Tactic: simp only [not_exists, Set.mem_image, toPowerSeries_symm_apply_coeff, mem_support,
      PowerSeries.coeff_X]
-- 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 : HahnSeries.{u_3, u_2} (σ →₀ ℕ) R
⊢ (fun (f : MvPowerSeries σ R) ↦ ({ coeff := f, isPWO_support' := ⋯ } : HahnSeries.{u_3, u_2} (σ →₀ ℕ) R))
      ((fun (f : HahnSeries.{u_3, u_2} (σ →₀ ℕ) R) ↦ f.coeff) f) =
    f
have coeff : ∀ (x : σ →₀ ℕ),
  coeff
      ((fun (f : MvPowerSeries σ R) ↦ ({ coeff := f, isPWO_support' := sorry } : HahnSeries.{u_3, u_2} (σ →₀ ℕ) R))
        ((fun (f : HahnSeries.{u_3, u_2} (σ →₀ ℕ) R) ↦ f.coeff) f))
      x =
    f.coeff x
Tactic: ext
-- 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 : MvPowerSeries σ R
⊢ (fun (f : HahnSeries.{u_3, u_2} (σ →₀ ℕ) R) ↦ f.coeff)
      ((fun (f : MvPowerSeries σ R) ↦ ({ coeff := f, isPWO_support' := ⋯ } : HahnSeries.{u_3, u_2} (σ →₀ ℕ) R)) f) =
    f
have h : ∀ (n : σ →₀ ℕ),
  Eq.{u_2 + 1} (α := R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
        ((fun (f : HahnSeries.{u_3, u_2} (σ →₀ ℕ) R) ↦ f.coeff)
          ((fun (f : MvPowerSeries σ R) ↦ ({ coeff := f, isPWO_support' := sorry } : HahnSeries.{u_3, u_2} (σ →₀ ℕ) R))
            f)) :
      R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) f : R)
Tactic: ext
-- 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 n
-- 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: change (f * g).coeff n = _
-- 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 : σ →₀ ℕ
⊢ (f * g).coeff n = (MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (f.coeff * g.coeff)
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: simp_rw [coeff_mul]
-- 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)
    (∑ 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)
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: refine (sum_filter_ne_zero _).symm.trans <| (sum_congr ?_ fun _ _ ↦ rfl).trans <|
        sum_filter_ne_zero _