awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
Goal:
Γ : Type u_1
R : Type u_2
inst : Semiring R
f g : 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
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}
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) (∑ 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)

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)]

Premises used: Finset.sum_filter_ne_zero, Finset.HasAntidiagonal.mem_antidiagonal, and_congr_left_iff, 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
f g : R⟦ℕ⟧
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)
⊢ PowerSeries.mk (f + g).coeff = PowerSeries.mk f.coeff + PowerSeries.mk g.coeff

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
Goal:
Γ : Type u_1
R : Type u_2
inst : Semiring R
f g : R⟦ℕ⟧
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:
simp
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
Goal:
R : Type u_2
inst : Semiring R
f : R⟦ℕ⟧
n : ℕ
⊢ (PowerSeries.coeff n : (a : PowerSeries R) → R) ((toPowerSeries : (a : R⟦ℕ⟧) → PowerSeries R) f : PowerSeries R) =
    f.coeff n

Tactic:
PowerSeries.coeff_mk _ _

Premises used: PowerSeries.coeff_mk, PowerSeries.mk
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
Goal:
R : Type u_2
inst : Semiring R
f : PowerSeries R
n : ℕ
⊢ Eq (α := R) (coeff ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) f) n : R)
    ((PowerSeries.coeff n : (a : PowerSeries R) → R) f : R)

Tactic:
rfl

Premises used: rfl
-- 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 Γ
⊢ Injective (α := PowerSeries R) (β := R⟦Γ⟧)
    (⇑(ofPowerSeries Γ R : PowerSeries R →+* R⟦Γ⟧) : (a : PowerSeries R) → R⟦Γ⟧)

Tactic:
embDomain_injective.comp toPowerSeries.symm.injective

Premises used: HahnSeries.embDomain, RingEquiv.injective, HahnSeries.embDomain_injective, HahnSeries.toPowerSeries, Function.Injective.comp, RingEquiv.symm
-- 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 Γ
x : PowerSeries R
simp : ∀ {a b : ℕ}, LE.le.{u_1} (α := Γ) (↑a : Γ) (↑b : Γ) ↔ a ≤ b
⊢ ∀ {a b : ℕ},
    LE.le.{u_1} (α := Γ) (({ toFun := Nat.cast, inj' := ⋯ } : (a : ℕ) → Γ) a : Γ)
        (({ toFun := Nat.cast, inj' := ⋯ } : (a : ℕ) → Γ) b : Γ) ↔
      a ≤ b

Tactic:
simp only [Function.Embedding.coeFn_mk]

Premises used: Function.Embedding.coeFn_mk
-- 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 Γ
x : PowerSeries R
a b : ℕ
⊢ LE.le.{u_1} (α := Γ) (↑a : Γ) (↑b : Γ) ↔ a ≤ b

Tactic:
Nat.cast_le

Premises used: Nat.cast_le
-- 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 Γ
x : PowerSeries R
⊢ ∀ {a b : ℕ}, LE.le.{u_1} (α := Γ) (↑a : Γ) (↑b : Γ) ↔ a ≤ b

Tactic:
exact Nat.cast_le

Premises used: Nat.cast_le
-- 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 Γ
x : PowerSeries R
⊢ Eq (α := R⟦Γ⟧) (((ofPowerSeries Γ R : PowerSeries R →+* R⟦Γ⟧) : (a : PowerSeries R) → R⟦Γ⟧) x : R⟦Γ⟧)
    (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⟦ℕ⟧) 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 : Semiring R
inst_1 : Semiring Γ
inst_2 : PartialOrder Γ
inst_3 : IsStrictOrderedRing Γ
x : PowerSeries R
n : ℕ
⊢ Eq (α := R)
    (coeff.{u_1, u_2} (Γ := Γ) (((ofPowerSeries Γ R : PowerSeries R →+* R⟦Γ⟧) : (a : PowerSeries R) → R⟦Γ⟧) x)
        (↑n : Γ) :
      R)
    ((PowerSeries.coeff n : (a : PowerSeries R) → R) x : R)

Tactic:
simp [ofPowerSeries_apply]

Premises used: HahnSeries.ofPowerSeries_apply
-- 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 Γ
r : R
coeff :
  ∀ (n : Γ),
    Eq.{u_2 + 1} (α := R)
      (HahnSeries.coeff
        (((ofPowerSeries Γ R : PowerSeries R →+* R⟦Γ⟧) : (a : PowerSeries R) → R⟦Γ⟧)
          ((PowerSeries.C : (a : R) → PowerSeries R) r))
        n)
      (HahnSeries.coeff ((C : (a : R) → R⟦Γ⟧) r) n)
⊢ 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⟦Γ⟧)

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 Γ
r : R
n : Γ
coeff :
  HahnSeries.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
⊢ Eq.{u_2 + 1} (α := R)
    (HahnSeries.coeff
      (((ofPowerSeries Γ R : PowerSeries R →+* R⟦Γ⟧) : (a : PowerSeries R) → R⟦Γ⟧)
        ((PowerSeries.C : (a : R) → PowerSeries R) r))
      n)
    (HahnSeries.coeff ((C : (a : R) → R⟦Γ⟧) r) n)

Tactic:
simp only [ofPowerSeries_apply, C, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk,
    coeff_single]

Premises used: OneHom.coe_mk, HahnSeries.coeff_single, MonoidHom.coe_mk, RingHom.coe_mk, HahnSeries.ofPowerSeries_apply, HahnSeries.C
-- 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 Γ
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
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' := ⋯ : ℕ ↪ Γ } ⋯)
          ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) ((PowerSeries.C : (a : R) → PowerSeries R) r)))
        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 =
    if n = 0 then r else 0

Tactic:
split_ifs with hn
-- 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 Γ
r : R
n : Γ
hn : n = 0
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' := ⋯ : ℕ ↪ Γ } ⋯)
        ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) ((PowerSeries.C : (a : R) → PowerSeries R) r)))
      0 =
    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 =
    r

Tactic:
subst hn
-- 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 Γ
r : R
⊢ 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.C : (a : R) → PowerSeries R) r)) :
        R⟦Γ⟧)
      ((RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ) ↦ x1 ≤ x2)
              { toFun := Nat.cast, inj' := ⋯ } ⋯ :
            (a : ℕ) → Γ)
          0 :
        Γ))
    (coeff (Γ := ℕ)
      ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) ((PowerSeries.C : (a : R) → PowerSeries R) r)) 0)

Tactic:
embDomain_coeff (a := 0)

Premises used: HahnSeries.embDomain_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 Γ
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 :
      Γ)
h₁ :
  r =
    coeff (Γ := ℕ)
      ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) ((PowerSeries.C : (a : R) → PowerSeries R) r)) 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

Tactic:
convert! embDomain_coeff (a := 0)

Premises used: HahnSeries.embDomain_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 Γ
r : R
⊢ 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 :
      Γ)

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 Γ
r : R
⊢ r =
    coeff (Γ := ℕ)
      ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) ((PowerSeries.C : (a : R) → PowerSeries R) r)) 0

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 Γ
r : R
n : Γ
hn : ¬n = 0
neg :
  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)))
⊢ 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

Tactic:
rw [embDomain_notin_image_support]

Premises used: HahnSeries.embDomain_notin_image_support
-- 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 Γ
r : R
n : Γ
hn : ¬n = 0
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' := ⋯ } ⋯ :
              (a : ℕ) → Γ)
            x =
          n)
⊢ 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)))

Tactic:
simp only [not_exists, Set.mem_image, toPowerSeries_symm_apply_coeff, mem_support,
      PowerSeries.coeff_C]

Premises used: Set.mem_image, not_exists, PowerSeries.coeff_C, HahnSeries.toPowerSeries_symm_apply_coeff, HahnSeries.mem_support
-- 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 Γ
r : R
n : Γ
hn : ¬n = 0
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' := ⋯ } ⋯ :
            (a : ℕ) → Γ)
          x =
        n)

Tactic:
simp +contextual [Ne.symm hn]

Premises used: Ne.symm
-- 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 Γ
coeff :
  ∀ (n : Γ),
    Eq.{u_2 + 1} (α := R)
      (HahnSeries.coeff (((ofPowerSeries Γ R : PowerSeries R →+* R⟦Γ⟧) : (a : PowerSeries R) → R⟦Γ⟧) PowerSeries.X) n)
      (HahnSeries.coeff ((single 1 : (a : R) → R⟦Γ⟧) 1) n)
⊢ Eq (α := R⟦Γ⟧) (((ofPowerSeries Γ R : PowerSeries R →+* R⟦Γ⟧) : (a : PowerSeries R) → R⟦Γ⟧) PowerSeries.X : R⟦Γ⟧)
    ((single 1 : (a : R) → R⟦Γ⟧) 1 : R⟦Γ⟧)

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 Γ
n : Γ
coeff :
  Eq.{u_2 + 1} (α := R)
    (HahnSeries.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)
⊢ Eq.{u_2 + 1} (α := R)
    (HahnSeries.coeff (((ofPowerSeries Γ R : PowerSeries R →+* R⟦Γ⟧) : (a : PowerSeries R) → R⟦Γ⟧) PowerSeries.X) n)
    (HahnSeries.coeff ((single 1 : (a : R) → R⟦Γ⟧) 1) n)

Tactic:
simp only [coeff_single, ofPowerSeries_apply]

Premises used: HahnSeries.coeff_single, HahnSeries.ofPowerSeries_apply
-- 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 Γ
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
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' := ⋯ : ℕ ↪ Γ } ⋯)
          ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) PowerSeries.X))
        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.X))
      n)
    (if n = 1 then 1 else 0)

Tactic:
split_ifs with hn
-- 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 Γ
n : Γ
hn : n = 1
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' := ⋯ : ℕ ↪ Γ } ⋯)
        ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) PowerSeries.X))
      1)
    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

Tactic:
rw [hn]
-- 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 Γ
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) :
        R⟦Γ⟧)
      ((RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ) ↦ x1 ≤ x2)
              { toFun := Nat.cast, inj' := ⋯ } ⋯ :
            (a : ℕ) → Γ)
          1 :
        Γ))
    (coeff (Γ := ℕ) ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) PowerSeries.X) 1)

Tactic:
embDomain_coeff (a := 1)

Premises used: HahnSeries.embDomain_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 Γ
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 :
      Γ)
h₁ :
  Eq.{u_2 + 1} (α := R) 1 (coeff (Γ := ℕ) ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) PowerSeries.X) 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

Tactic:
convert! embDomain_coeff (a := 1)

Premises used: HahnSeries.embDomain_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 Γ
n : Γ
hn : n = 1
⊢ 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 :
      Γ)

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 Γ
n : Γ
hn : n = 1
⊢ Eq.{u_2 + 1} (α := R) 1 (coeff (Γ := ℕ) ((RingEquiv.symm toPowerSeries : (a : PowerSeries R) → R⟦ℕ⟧) PowerSeries.X) 1)

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 Γ
n : Γ
hn : ¬n = 1
neg :
  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))
⊢ 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

Tactic:
rw [embDomain_notin_image_support]

Premises used: HahnSeries.embDomain_notin_image_support
-- 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 Γ
n : Γ
hn : ¬n = 1
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' := ⋯ } ⋯ :
              (a : ℕ) → Γ)
            x =
          n)
⊢ 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))

Tactic:
simp only [not_exists, Set.mem_image, toPowerSeries_symm_apply_coeff, mem_support,
      PowerSeries.coeff_X]

Premises used: Set.mem_image, not_exists, PowerSeries.coeff_X, HahnSeries.toPowerSeries_symm_apply_coeff, HahnSeries.mem_support
-- 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 Γ
n : Γ
hn : ¬n = 1
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' := ⋯ } ⋯ :
            (a : ℕ) → Γ)
          x =
        n)

Tactic:
simp +contextual [Ne.symm hn]

Premises used: Ne.symm
-- Module: Mathlib.RingTheory.HahnSeries.PowerSeries
Goal:
Γ : Type u_1
inst : Semiring Γ
inst_1 : PartialOrder Γ
inst_2 : IsStrictOrderedRing Γ
R : Type u_3
inst_3 : Semiring R
n : ℕ
⊢ Eq (α := R⟦Γ⟧)
    (((ofPowerSeries Γ R : PowerSeries R →+* R⟦Γ⟧) : (a : PowerSeries R) → R⟦Γ⟧)
        (HPow.hPow (α := PowerSeries R) PowerSeries.X n) :
      R⟦Γ⟧)
    ((single (↑n : Γ) : (a : R) → R⟦Γ⟧) 1 : R⟦Γ⟧)

Tactic:
simp