awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
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
coeff :
  ∀ (x : σ →₀ ℕ),
    HahnSeries.coeff
        ((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))
        x =
      f.coeff x
⊢ (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

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
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
x : σ →₀ ℕ
⊢ coeff
      ((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))
      x =
    f.coeff x

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
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
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' := ⋯ } : HahnSeries.{u_3, u_2} (σ →₀ ℕ) R))
              f)) :
        R)
      ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) f : 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

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
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
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' := ⋯ } : HahnSeries.{u_3, u_2} (σ →₀ ℕ) R))
            f)) :
      R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) f : R)

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
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
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)
⊢ (f * g).coeff = f.coeff * g.coeff

Tactic:
ext n
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
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)

Tactic:
change (f * g).coeff n = _

Premises used: HMul.hMul, HahnSeries.coeff
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
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 :
  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)
⊢ (f * g).coeff n = (MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) (f.coeff * g.coeff)

Tactic:
simp_rw [coeff_mul]

Premises used: HahnSeries.coeff_mul
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
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)

Tactic:
(sum_filter_ne_zero _).symm.trans <| (sum_congr ?_ fun _ _ ↦ rfl).trans <|
        sum_filter_ne_zero _

Premises used: Finset.sum_filter_ne_zero, Eq.symm, Finset.sum_congr, rfl, Eq.trans
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
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 :
  {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)
    (∑ 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)

Tactic:
refine (sum_filter_ne_zero _).symm.trans <| (sum_congr ?_ fun _ _ ↦ rfl).trans <|
        sum_filter_ne_zero _

Premises used: Finset.sum_filter_ne_zero, Eq.symm, Finset.sum_congr, rfl, Eq.trans
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
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 :
  ∀ (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}
⊢ {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}

Tactic:
ext m
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
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)
⊢ 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}

Tactic:
simp only [and_congr_left_iff, mem_addAntidiagonal, mem_filter, mem_support,
        Finset.mem_antidiagonal]

Premises used: Finset.HasAntidiagonal.mem_antidiagonal, and_congr_left_iff, Finset.mem_filter, HahnSeries.mem_support, Finset.mem_addAntidiagonal
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
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
h₂ h₃ : 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

Tactic:
rw [and_iff_right (left_ne_zero_of_mul h), and_iff_right (right_ne_zero_of_mul h)]

Premises used: right_ne_zero_of_mul, and_iff_right, left_ne_zero_of_mul
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
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}
h₄ h₅ :
  ∀ (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
⊢ 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:
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)]

Premises used: HMul.hMul, HahnSeries.coeff_mul, Finset.sum_filter_ne_zero, Finset.HasAntidiagonal.mem_antidiagonal, and_congr_left_iff, HahnSeries.coeff, Finset.mem_filter, Eq.symm, Finset.sum_congr, rfl, HahnSeries.mem_support, Finset.mem_addAntidiagonal, Eq.trans
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
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
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)
⊢ (f + g).coeff = f.coeff + g.coeff

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
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)

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
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 σ
inst_5 : NoZeroDivisors R
⊢ NoZeroDivisors (HahnSeries.{u_3, u_2} (σ →₀ ℕ) R)

Tactic:
toMvPowerSeries.toMulEquiv.noZeroDivisors (A := R⟦σ →₀ ℕ⟧) (MvPowerSeries σ R)

Premises used: HahnSeries.toMvPowerSeries, RingEquiv.toMulEquiv, MvPowerSeries, MulEquiv.noZeroDivisors
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
Goal:
R : Type u_2
inst : Semiring R
σ : Type u_3
inst_1 : Finite σ
f : HahnSeries.{u_3, u_2} (σ →₀ ℕ) R
n : σ →₀ ℕ
⊢ (MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R)
      ((toMvPowerSeries : (a : R⟦σ →₀ ℕ⟧) → MvPowerSeries σ R) f : MvPowerSeries σ R) =
    f.coeff n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
Goal:
R : Type u_2
inst : Semiring R
σ : Type u_3
inst_1 : Finite σ
f : MvPowerSeries σ R
n : σ →₀ ℕ
⊢ Eq.{u_2 + 1} (α := R) (coeff ((RingEquiv.symm toMvPowerSeries : (a : MvPowerSeries σ R) → R⟦σ →₀ ℕ⟧) f) n : R)
    ((MvPowerSeries.coeff n : (a : MvPowerSeries σ R) → R) f : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
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
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)
⊢ 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)

Tactic:
ext n
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
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)
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)
⊢ 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:
cases n
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
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} (α := 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:
simp [algebraMap_apply, PowerSeries.algebraMap_apply]

Premises used: HahnSeries.algebraMap_apply, PowerSeries.algebraMap_apply
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
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 + 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:
simp [algebraMap_apply, PowerSeries.algebraMap_apply]

Premises used: HahnSeries.algebraMap_apply, PowerSeries.algebraMap_apply
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
Goal:
Γ : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : Semiring Γ
inst_2 : PartialOrder Γ
inst_3 : IsStrictOrderedRing Γ
S : Type u_4
inst_4 : CommSemiring S
inst_5 : Algebra.{u_4, u_2} S (PowerSeries R)
x : S
⊢ Eq (α := R⟦Γ⟧) ((algebraMap S R⟦Γ⟧ : (a : S) → R⟦Γ⟧) x : R⟦Γ⟧)
    (((ofPowerSeries Γ R : PowerSeries R →+* R⟦Γ⟧) : (a : PowerSeries R) → R⟦Γ⟧)
        ((algebraMap S (PowerSeries R) : (a : S) → PowerSeries R) x) :
      R⟦Γ⟧)

Tactic:
rfl

Premises used: HahnSeries.embDomain, Set.Mem, rfl
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
Goal:
Γ : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : Semiring Γ
inst_2 : PartialOrder Γ
inst_3 : IsStrictOrderedRing Γ
f : R[X]
⊢ Eq (α := R⟦Γ⟧) ((algebraMap R[X] R⟦Γ⟧ : (a : R[X]) → R⟦Γ⟧) f : R⟦Γ⟧)
    (((ofPowerSeries Γ R : PowerSeries R →+* R⟦Γ⟧) : (a : PowerSeries R) → R⟦Γ⟧) (↑f : PowerSeries R) : R⟦Γ⟧)

Tactic:
rfl

Premises used: HahnSeries.embDomain, Set.Mem, Polynomial.coeff, Polynomial.toPowerSeries, PowerSeries.mk, rfl
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
Goal:
Γ : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : Semiring Γ
inst_2 : PartialOrder Γ
inst_3 : IsStrictOrderedRing Γ
⊢ Injective (α := R[X]) (β := R⟦Γ⟧) (⇑(algebraMap R[X] R⟦Γ⟧) : (a : R[X]) → R⟦Γ⟧)

Tactic:
ofPowerSeries_injective.comp (Polynomial.coe_injective R)

Premises used: HahnSeries.embDomain, Function.Injective.comp, Polynomial.coe_injective, HahnSeries.ofPowerSeries_injective
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
toFun : α → R⟦Γ⟧
h1 : Set.IsPWO.{u_1} (α := Γ) (⋃ (a : α), (toFun a).support)
h2 : ∀ (g : Γ), Set.Finite.{u_5} (α := α) {a : α | (toFun a).coeff g ≠ 0}
⊢ (⇑{ toFun := toFun, isPWO_iUnion_support' := h1, finite_co_support' := h2 : SummableFamily Γ R α } : (a : α) → R⟦Γ⟧) =
    toFun

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s : SummableFamily Γ R α
⊢ Set.IsPWO.{u_1} (α := Γ) (⋃ (a : α), support.{u_1, u_3} (R := R) ((s : (a : α) → R⟦Γ⟧) a))

Tactic:
s.isPWO_iUnion_support'

Premises used: HahnSeries.SummableFamily.isPWO_iUnion_support'
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s : SummableFamily Γ R α
g : Γ
⊢ HasFiniteSupport.{u_5, u_3} (M := R) fun (a : α) ↦ coeff ((s : (a : α) → R⟦Γ⟧) a) g

Tactic:
s.finite_co_support' g

Premises used: Function.HasFiniteSupport, setOf, Function.support, HahnSeries.SummableFamily.finite_co_support'
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
⊢ Injective (α := SummableFamily Γ R α) (β := α → R⟦Γ⟧) (DFunLike.coe (β := fun (x : α) ↦ R⟦Γ⟧))

Tactic:
DFunLike.coe_injective

Premises used: DFunLike.coe_injective
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s t : SummableFamily Γ R α
h : ∀ (a : α), Eq (α := R⟦Γ⟧) ((s : (a : α) → R⟦Γ⟧) a : R⟦Γ⟧) ((t : (a : α) → R⟦Γ⟧) a : R⟦Γ⟧)
⊢ s = t

Tactic:
DFunLike.ext s t h

Premises used: DFunLike.ext
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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 α
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))
⊢ 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))

Tactic:
rw [← Set.iUnion_union_distrib]

Premises used: Set.iUnion_union_distrib
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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)
    (⋃ (i : α),
      support.{u_1, u_3} (R := R) ((x : (a : α) → R⟦Γ⟧) i) ∪ support.{u_1, u_3} (R := R) ((y : (a : α) → R⟦Γ⟧) i))

Tactic:
Set.iUnion_mono fun a => support_add_subset ..

Premises used: Set.iUnion_mono, HahnSeries.support_add_subset, DFunLike.coe
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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)
    (⋃ (i : α),
      support.{u_1, u_3} (R := R) ((x : (a : α) → R⟦Γ⟧) i) ∪ support.{u_1, u_3} (R := R) ((y : (a : α) → R⟦Γ⟧) i))

Tactic:
exact Set.iUnion_mono fun a => support_add_subset ..

Premises used: Set.iUnion_mono, HahnSeries.support_add_subset
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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
⊢ 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

Premises used: HahnSeries.coeff, DFunLike.coe
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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
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
⊢ Ne.{u_3 + 1} (α := R) (coeff ((x : (a : α) → R⟦Γ⟧) a) g) 0 ∨
    Ne.{u_3 + 1} (α := R) (coeff ((y : (a : α) → R⟦Γ⟧) a) g) 0

Tactic:
contrapose! ha
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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
rw₂ rw₃ : Eq.{u_3 + 1} (α := R) 0 0
⊢ HAdd.hAdd (α := R) (coeff ((x : (a : α) → R⟦Γ⟧) a) g) (coeff ((y : (a : α) → R⟦Γ⟧) a) g) = 0

Tactic:
rw [ha.1, ha.2, add_zero]

Premises used: And.right, And.left, add_zero
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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
⊢ Set.IsPWO.{u_1} (α := Γ) (⋃ (a : α), support.{u_1, u_3} (R := R) (0 a))

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Summable
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
⊢ ∀ (g : Γ), Set.Finite.{u_5} (α := α) {a : α | Ne.{u_3 + 1} (α := R) (coeff (0 a) g) 0}

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s t : SummableFamily Γ R α
⊢ (⇑(s + t) : (a : α) → R⟦Γ⟧) = HAdd.hAdd (α := (a : α) → R⟦Γ⟧) (⇑s : (a : α) → R⟦Γ⟧) (⇑t : (a : α) → R⟦Γ⟧)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Summable
Goal:
Γ : Type u_1
R : Type u_3
α : Type u_5
inst : PartialOrder Γ
inst_1 : AddCommMonoid R
s t : SummableFamily Γ R α
a : α
⊢ (s + t : (a : α) → R⟦Γ⟧) a =
    HAdd.hAdd (α := R⟦Γ⟧) (β := R⟦Γ⟧) ((s : (a : α) → R⟦Γ⟧) a : R⟦Γ⟧) ((t : (a : α) → R⟦Γ⟧) a : R⟦Γ⟧)

Tactic:
rfl

Premises used: rfl