awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
R : Type u_3
inst : Zero R
Γ : Type u_5
inst_1 : Zero Γ
inst_2 : LinearOrder Γ
x : R⟦Γ⟧
g : Γ
h : x.coeff g ≠ 0
⊢ x.order ≤ g

Tactic:
le_trans (le_of_eq (order_of_ne (ne_zero_of_coeff_ne_zero h)))
    (Set.IsWF.min_le _ _ ((mem_support _ _).2 h))

Premises used: Iff.mpr, HahnSeries.ne_zero_of_coeff_ne_zero, HahnSeries.order_of_ne, Set.IsWF.min_le, le_of_eq, HahnSeries.mem_support, le_trans
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
a : Γ
r : R
inst_2 : Zero Γ
h : r ≠ 0
⊢ order.{u_1, u_3} (R := R) ((single a : (a : R) → R⟦Γ⟧) r) = a

Tactic:
(order_of_ne (single_ne_zero h)).trans
    (support_single_subset
      ((single a r).isWF_support.min_mem (support_nonempty_iff.2 (single_ne_zero h))))

Premises used: Iff.mpr, HahnSeries.single, Set.IsWF.min_mem, HahnSeries.support_nonempty_iff, HahnSeries.order_of_ne, HahnSeries.support_single_subset, HahnSeries.single_ne_zero, HahnSeries.isWF_support, DFunLike.coe, Eq.trans
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
i : Γ
hi : i < x.order
inl : ∀ (hi : i < order.{u_1, u_3} (R := R) 0), Eq.{u_3 + 1} (α := R) (coeff 0 i) 0
inr : ∀ (hx : x ≠ 0), x.coeff i = 0
⊢ x.coeff i = 0

Tactic:
rcases eq_or_ne x 0 with (rfl | hx)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
i : Γ
hi : i < order.{u_1, u_3} (R := R) 0
⊢ Eq.{u_3 + 1} (α := R) (coeff 0 i) 0

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
i : Γ
hi : i < x.order
hx : x ≠ 0
inr : ∀ (hi : x.coeff i ≠ 0), ¬i < x.order
⊢ x.coeff i = 0

Tactic:
contrapose! hi
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
i : Γ
hx : x ≠ 0
hi : x.coeff i ≠ 0
⊢ i ∈ x.support

Tactic:
rw [← mem_support] at hi

Premises used: HahnSeries.mem_support
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
i : Γ
hx : x ≠ 0
hi : i ∈ x.support
inr : ¬i < ⋯.min (s := x.support) ⋯
⊢ ¬i < x.order

Tactic:
rw [order_of_ne hx]

Premises used: HahnSeries.order_of_ne
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
i : Γ
hx : x ≠ 0
hi : i ∈ x.support
⊢ ¬i < ⋯.min (s := x.support) ⋯

Tactic:
Set.IsWF.not_lt_min _ _ hi

Premises used: Set.IsWF.not_lt_min
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
i : Γ
hx : x ≠ 0
hi : i ∈ x.support
⊢ ¬i < ⋯.min (s := x.support) ⋯

Tactic:
exact Set.IsWF.not_lt_min _ _ hi

Premises used: Set.IsWF.not_lt_min
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
hx : x ≠ 0
⊢ 0 < x.orderTop ↔ 0 < x.order

Tactic:
simp_all [orderTop_of_ne_zero hx, order_of_ne hx]

Premises used: HahnSeries.orderTop_of_ne_zero, HahnSeries.order_of_ne
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
hx : 0 < x.order
pos : ∀ (h : x = 0), 0 < x.orderTop
neg : ∀ (h : ¬x = 0), 0 < x.orderTop
⊢ 0 < x.orderTop

Tactic:
by_cases h : x = 0
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
hx : 0 < x.order
h : x = 0
⊢ 0 < x.orderTop

Tactic:
simp_all only [order_zero, lt_self_iff_false]

Premises used: HahnSeries.order_zero, lt_self_iff_false
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
hx : 0 < x.order
h : ¬x = 0
⊢ 0 < x.orderTop

Tactic:
(zero_lt_orderTop_iff h).mpr hx

Premises used: Iff.mpr, HahnSeries.zero_lt_orderTop_iff
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
hx : 0 < x.order
h : ¬x = 0
⊢ 0 < x.orderTop

Tactic:
exact (zero_lt_orderTop_iff h).mpr hx

Premises used: Iff.mpr, HahnSeries.zero_lt_orderTop_iff
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
pos : ∀ (h : x = 0), 0 ≤ x.orderTop ↔ 0 ≤ x.order
neg : ∀ (h : ¬x = 0), 0 ≤ x.orderTop ↔ 0 ≤ x.order
⊢ 0 ≤ x.orderTop ↔ 0 ≤ x.order

Tactic:
by_cases h : x = 0
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
h : x = 0
⊢ 0 ≤ x.orderTop ↔ 0 ≤ x.order

Tactic:
simp_all
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
h : ¬x = 0
⊢ 0 ≤ x.orderTop ↔ 0 ≤ x.order

Tactic:
simp_all [order_of_ne h, orderTop_of_ne_zero h]

Premises used: HahnSeries.orderTop_of_ne_zero, HahnSeries.order_of_ne
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
pos : ∀ (h : x = 0), x.leadingCoeff = x.coeff x.order
neg : ∀ (h : ¬x = 0), x.leadingCoeff = x.coeff x.order
⊢ x.leadingCoeff = x.coeff x.order

Tactic:
by_cases h : x = 0
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
h : x = 0
pos :
  Eq.{u_3 + 1} (α := R) (leadingCoeff.{u_1, u_3} (Γ := Γ) 0) (coeff.{u_1, u_3} (Γ := Γ) 0 (order.{u_1, u_3} (R := R) 0))
pos₁ : Eq.{u_3 + 1} (α := R) 0 (coeff.{u_1, u_3} (Γ := Γ) 0 (order.{u_1, u_3} (R := R) 0))
pos₂ pos₃ : Eq.{u_3 + 1} (α := R) 0 0
⊢ x.leadingCoeff = x.coeff x.order

Tactic:
rw [h, leadingCoeff_zero, coeff_zero]

Premises used: HahnSeries.coeff_zero, HahnSeries.leadingCoeff_zero
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : Zero Γ
x : R⟦Γ⟧
h : ¬x = 0
⊢ x.leadingCoeff = x.coeff x.order

Tactic:
simp [leadingCoeff_of_ne_zero, orderTop_of_ne_zero, order_of_ne, h]

Premises used: HahnSeries.orderTop_of_ne_zero, HahnSeries.order_of_ne, HahnSeries.leadingCoeff_of_ne_zero
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
a b : Γ
r : R
⊢ Eq (α := R⟦Γ⟧) { coeff := (⇑0 : (a : Γ) → R), isPWO_support' := ⋯ } 0

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
f : Γ →₀ R
a : Γ
⊢ Eq.{u_3 + 1} (α := R) (coeff ((ofFinsupp : (a : Γ →₀ R) → R⟦Γ⟧) f) a : R) ((f : (a : Γ) → R) a : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
a b_1 : Γ
r : R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
b : Γ'
hb :
  Membership.mem (γ := Set Γ')
    (Function.support.{u_2, u_3} (M := R) fun (b : Γ') ↦
      if h : Membership.mem (γ := Set Γ') ((⇑f : (a : Γ) → Γ') '' x.support) b then
        x.coeff (Classical.choose (p := fun (x_1 : Γ) ↦ x_1 ∈ x.support ∧ (f : (a : Γ) → Γ') x_1 = b) h)
      else 0)
    b
contrapose :
  ∀ (hb : b ∉ (⇑f : (a : Γ) → Γ') '' x.support),
    b ∉
      Function.support.{u_2, u_3} (M := R) fun (b : Γ') ↦
        if h : Membership.mem (γ := Set Γ') ((⇑f : (a : Γ) → Γ') '' x.support) b then
          x.coeff (Classical.choose (p := fun (x_1 : Γ) ↦ x_1 ∈ x.support ∧ (f : (a : Γ) → Γ') x_1 = b) h)
        else 0
⊢ Membership.mem (γ := Set Γ') ((⇑f : (a : Γ) → Γ') '' x.support) b

Tactic:
contrapose hb
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
inst : PartialOrder Γ
inst_1 : Zero R
a b_1 : Γ
r : R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
b : Γ'
hb : b ∉ (⇑f : (a : Γ) → Γ') '' x.support
rw :
  ¬Ne.{u_3 + 1} (α := R)
      (if h : Membership.mem (γ := Set Γ') ((⇑f : (a : Γ) → Γ') '' x.support) b then
        x.coeff (Classical.choose (p := fun (x_1 : Γ) ↦ x_1 ∈ x.support ∧ (f : (a : Γ) → Γ') x_1 = b) h)
      else 0)
      0
rw₁ : ¬Ne.{u_3 + 1} (α := R) 0 0
rw₂ rw₃ : Eq.{u_3 + 1} (α := R) 0 0
⊢ b ∉
    Function.support.{u_2, u_3} (M := R) fun (b : Γ') ↦
      if h : Membership.mem (γ := Set Γ') ((⇑f : (a : Γ) → Γ') '' x.support) b then
        x.coeff (Classical.choose (p := fun (x_1 : Γ) ↦ x_1 ∈ x.support ∧ (f : (a : Γ) → Γ') x_1 = b) h)
      else 0

Tactic:
rw [Function.mem_support, dif_neg hb, Classical.not_not]

Premises used: Classical.not_not, dif_neg, Function.mem_support
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
a : Γ
rw :
  {
          coeff := fun (b : Γ') ↦
            if h : Membership.mem (γ := Set Γ') ((⇑f : (a : Γ) → Γ') '' x.support) b then
              x.coeff (Classical.choose (p := fun (x_1 : Γ) ↦ x_1 ∈ x.support ∧ (f : (a : Γ) → Γ') x_1 = b) h)
            else 0,
          isPWO_support' := ⋯ : R⟦Γ'⟧ }.coeff
      ((f : (a : Γ) → Γ') a) =
    x.coeff a
⊢ (embDomain f x).coeff ((f : (a : Γ) → Γ') a) = x.coeff a

Tactic:
rw [embDomain]

Premises used: HahnSeries.embDomain
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
a : Γ
dsimp :
  (if h :
        Membership.mem.{u_2, u_2} (α := Γ') (γ := Set Γ') ((⇑f : (a : Γ) → Γ') '' x.support)
          ((f : (a : Γ) → Γ') a : Γ') then
      x.coeff
        (Classical.choose (p := fun (x_1 : Γ) ↦
          x_1 ∈ x.support ∧ Eq.{u_2 + 1} (α := Γ') ((f : (a : Γ) → Γ') x_1 : Γ') ((f : (a : Γ) → Γ') a : Γ')) h)
    else 0) =
    x.coeff a
⊢ {
          coeff := fun (b : Γ') ↦
            if h : Membership.mem (γ := Set Γ') ((⇑f : (a : Γ) → Γ') '' x.support) b then
              x.coeff (Classical.choose (p := fun (x_1 : Γ) ↦ x_1 ∈ x.support ∧ (f : (a : Γ) → Γ') x_1 = b) h)
            else 0,
          isPWO_support' := ⋯ : R⟦Γ'⟧ }.coeff
      ((f : (a : Γ) → Γ') a) =
    x.coeff a

Tactic:
dsimp only
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
a : Γ
pos :
  ∀ (ha : a ∈ x.support),
    (if h :
          Membership.mem.{u_2, u_2} (α := Γ') (γ := Set Γ') ((⇑f : (a : Γ) → Γ') '' x.support)
            ((f : (a : Γ) → Γ') a : Γ') then
        x.coeff
          (Classical.choose (p := fun (x_1 : Γ) ↦
            x_1 ∈ x.support ∧ Eq.{u_2 + 1} (α := Γ') ((f : (a : Γ) → Γ') x_1 : Γ') ((f : (a : Γ) → Γ') a : Γ')) h)
      else 0) =
      x.coeff a
neg :
  ∀ (ha : a ∉ x.support),
    (if h :
          Membership.mem.{u_2, u_2} (α := Γ') (γ := Set Γ') ((⇑f : (a : Γ) → Γ') '' x.support)
            ((f : (a : Γ) → Γ') a : Γ') then
        x.coeff
          (Classical.choose (p := fun (x_1 : Γ) ↦
            x_1 ∈ x.support ∧ Eq.{u_2 + 1} (α := Γ') ((f : (a : Γ) → Γ') x_1 : Γ') ((f : (a : Γ) → Γ') a : Γ')) h)
      else 0) =
      x.coeff a
⊢ (if h :
        Membership.mem.{u_2, u_2} (α := Γ') (γ := Set Γ') ((⇑f : (a : Γ) → Γ') '' x.support)
          ((f : (a : Γ) → Γ') a : Γ') then
      x.coeff
        (Classical.choose (p := fun (x_1 : Γ) ↦
          x_1 ∈ x.support ∧ Eq.{u_2 + 1} (α := Γ') ((f : (a : Γ) → Γ') x_1 : Γ') ((f : (a : Γ) → Γ') a : Γ')) h)
    else 0) =
    x.coeff a

Tactic:
by_cases ha : a ∈ x.support

Premises used: HahnSeries.support
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
a : Γ
ha : a ∈ x.support
pos :
  x.coeff
      (Classical.choose (p := fun (x_1 : Γ) ↦
        x_1 ∈ x.support ∧ Eq.{u_2 + 1} (α := Γ') ((f : (a : Γ) → Γ') x_1 : Γ') ((f : (a : Γ) → Γ') a : Γ')) ⋯) =
    x.coeff a
⊢ (if h :
        Membership.mem.{u_2, u_2} (α := Γ') (γ := Set Γ') ((⇑f : (a : Γ) → Γ') '' x.support)
          ((f : (a : Γ) → Γ') a : Γ') then
      x.coeff
        (Classical.choose (p := fun (x_1 : Γ) ↦
          x_1 ∈ x.support ∧ Eq.{u_2 + 1} (α := Γ') ((f : (a : Γ) → Γ') x_1 : Γ') ((f : (a : Γ) → Γ') a : Γ')) h)
    else 0) =
    x.coeff a

Tactic:
rw [dif_pos (Set.mem_image_of_mem f ha)]

Premises used: dif_pos, Set.mem_image_of_mem, DFunLike.coe
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
a : Γ
ha : a ∈ x.support
⊢ x.coeff
      (Classical.choose (p := fun (x_1 : Γ) ↦
        x_1 ∈ x.support ∧ Eq.{u_2 + 1} (α := Γ') ((f : (a : Γ) → Γ') x_1 : Γ') ((f : (a : Γ) → Γ') a : Γ')) ⋯) =
    x.coeff a

Tactic:
congr rfl (f.injective (Classical.choose_spec (Set.mem_image_of_mem f ha)).2)

Premises used: RelEmbedding.injective, Classical.choose_spec, And.right, Set.mem_image_of_mem, congr, DFunLike.coe, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
a : Γ
ha : a ∈ x.support
⊢ x.coeff
      (Classical.choose (p := fun (x_1 : Γ) ↦
        x_1 ∈ x.support ∧ Eq.{u_2 + 1} (α := Γ') ((f : (a : Γ) → Γ') x_1 : Γ') ((f : (a : Γ) → Γ') a : Γ')) ⋯) =
    x.coeff a

Tactic:
exact congr rfl (f.injective (Classical.choose_spec (Set.mem_image_of_mem f ha)).2)

Premises used: RelEmbedding.injective, Classical.choose_spec, And.right, Set.mem_image_of_mem, congr, DFunLike.coe, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
a : Γ
ha : a ∉ x.support
neg : ((f : (a : Γ) → Γ') a : Γ') ∉ (⇑f : (a : Γ) → Γ') '' x.support
⊢ (if h :
        Membership.mem.{u_2, u_2} (α := Γ') (γ := Set Γ') ((⇑f : (a : Γ) → Γ') '' x.support)
          ((f : (a : Γ) → Γ') a : Γ') then
      x.coeff
        (Classical.choose (p := fun (x_1 : Γ) ↦
          x_1 ∈ x.support ∧ Eq.{u_2 + 1} (α := Γ') ((f : (a : Γ) → Γ') x_1 : Γ') ((f : (a : Γ) → Γ') a : Γ')) h)
    else 0) =
    x.coeff a

Tactic:
rw [dif_neg, Classical.not_not.1 fun c => ha ((mem_support _ _).2 c)]

Premises used: Iff.mpr, Classical.not_not, dif_neg, Iff.mp, HahnSeries.mem_support
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
a : Γ
ha : a ∉ x.support
neg :
  ∀
    (ha :
      Membership.mem.{u_2, u_2} (α := Γ') (γ := Set Γ') ((⇑f : (a : Γ) → Γ') '' x.support) ((f : (a : Γ) → Γ') a : Γ')),
    a ∈ x.support
⊢ ((f : (a : Γ) → Γ') a : Γ') ∉ (⇑f : (a : Γ) → Γ') '' x.support

Tactic:
contrapose ha
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
a : Γ
ha : Membership.mem.{u_2, u_2} (α := Γ') (γ := Set Γ') ((⇑f : (a : Γ) → Γ') '' x.support) ((f : (a : Γ) → Γ') a : Γ')
neg :
  ∀ (b : Γ) (hb1 : b ∈ x.support)
    (hb2 : Eq.{u_2 + 1} (α := Γ') ((f : (a : Γ) → Γ') b : Γ') ((f : (a : Γ) → Γ') a : Γ')), a ∈ x.support
⊢ a ∈ x.support

Tactic:
obtain ⟨b, hb1, hb2⟩ := (Set.mem_image _ _ _).1 ha

Premises used: Set.mem_image, Iff.mp
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
a : Γ
ha : Membership.mem.{u_2, u_2} (α := Γ') (γ := Set Γ') ((⇑f : (a : Γ) → Γ') '' x.support) ((f : (a : Γ) → Γ') a : Γ')
b : Γ
hb1 : b ∈ x.support
hb2 : Eq.{u_2 + 1} (α := Γ') ((f : (a : Γ) → Γ') b : Γ') ((f : (a : Γ) → Γ') a : Γ')
neg neg₁ neg₂ neg₃ :
  ∀ (hb1 : a ∈ x.support) (hb2 : Eq.{u_2 + 1} (α := Γ') ((f : (a : Γ) → Γ') b : Γ') ((f : (a : Γ) → Γ') a : Γ')),
    a ∈ x.support
⊢ a ∈ x.support

Tactic:
rwa [f.injective hb2] at hb1

Premises used: RelEmbedding.injective
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
f : Γ → Γ'
hfi : Injective f
hf : ∀ (g g' : Γ), f g ≤ f g' ↔ g ≤ g'
x : R⟦Γ⟧
a : Γ
⊢ coeff
      (embDomain
        (RelEmbedding.mk (r := fun (x1 x2 : Γ) ↦ x1 ≤ x2) (s := fun (x1 x2 : Γ') ↦ x1 ≤ x2)
          { toFun := f, inj' := hfi : Γ ↪ Γ' } ⋯)
        x)
      (f a) =
    x.coeff a

Tactic:
embDomain_coeff

Premises used: Set.Mem, HahnSeries.embDomain_coeff
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
b : Γ'
hb : b ∉ (⇑f : (a : Γ) → Γ') '' x.support
⊢ (embDomain f x).coeff b = 0

Tactic:
dif_neg hb

Premises used: dif_neg, dite
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
g : Γ'
hg : g ∈ (embDomain f x).support
contrapose : ∀ (hg : g ∉ (⇑f : (a : Γ) → Γ') '' x.support), g ∉ (embDomain f x).support
⊢ Membership.mem (γ := Set Γ') ((⇑f : (a : Γ) → Γ') '' x.support) g

Tactic:
contrapose hg
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
g : Γ'
hg : g ∉ (⇑f : (a : Γ) → Γ') '' x.support
rw : ¬(embDomain f x).coeff g ≠ 0
rw₁ : ¬Ne.{u_3 + 1} (α := R) 0 0
rw₂ rw₃ : Eq.{u_3 + 1} (α := R) 0 0
⊢ g ∉ (embDomain f x).support

Tactic:
rw [mem_support, embDomain_notin_image_support hg, Classical.not_not]

Premises used: Classical.not_not, HahnSeries.embDomain_notin_image_support, HahnSeries.mem_support
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
x : R⟦Γ⟧
b : Γ'
hb : b ∉ Set.range.{u_2, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')
⊢ (embDomain f x).coeff b = 0

Tactic:
embDomain_notin_image_support fun con => hb (Set.image_subset_range _ _ con)

Premises used: HahnSeries.support, HahnSeries.embDomain_notin_image_support, Set.image_subset_range, DFunLike.coe
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
coeff : ∀ (x : Γ'), Eq.{u_3 + 1} (α := R) (HahnSeries.coeff (embDomain f 0) x) (HahnSeries.coeff 0 x)
⊢ Eq (α := R⟦Γ'⟧) (embDomain f 0) 0

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
x : Γ'
⊢ Eq.{u_3 + 1} (α := R) (coeff (embDomain f 0) x) (coeff 0 x)

Tactic:
simp [embDomain_notin_image_support]

Premises used: HahnSeries.embDomain_notin_image_support
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
g : Γ
r : R
coeff :
  ∀ (g' : Γ'),
    Eq.{u_3 + 1} (α := R) (HahnSeries.coeff (embDomain f ((single g : (a : R) → R⟦Γ⟧) r)) g')
      (HahnSeries.coeff (((single ((f : (a : Γ) → Γ') g) : ZeroHom R R⟦Γ'⟧) : (a : R) → R⟦Γ'⟧) r) g')
⊢ Eq (α := R⟦Γ'⟧) (embDomain f ((single g : (a : R) → R⟦Γ⟧) r))
    (((single ((f : (a : Γ) → Γ') g) : ZeroHom R R⟦Γ'⟧) : (a : R) → R⟦Γ'⟧) r)

Tactic:
ext g'
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
g : Γ
r : R
g' : Γ'
pos :
  ∀ (h : g' = (f : (a : Γ) → Γ') g),
    Eq.{u_3 + 1} (α := R) (coeff (embDomain f ((single g : (a : R) → R⟦Γ⟧) r)) g')
      (coeff (((single ((f : (a : Γ) → Γ') g) : ZeroHom R R⟦Γ'⟧) : (a : R) → R⟦Γ'⟧) r) g')
neg :
  ∀ (h : ¬g' = (f : (a : Γ) → Γ') g),
    Eq.{u_3 + 1} (α := R) (coeff (embDomain f ((single g : (a : R) → R⟦Γ⟧) r)) g')
      (coeff (((single ((f : (a : Γ) → Γ') g) : ZeroHom R R⟦Γ'⟧) : (a : R) → R⟦Γ'⟧) r) g')
⊢ Eq.{u_3 + 1} (α := R) (coeff (embDomain f ((single g : (a : R) → R⟦Γ⟧) r)) g')
    (coeff (((single ((f : (a : Γ) → Γ') g) : ZeroHom R R⟦Γ'⟧) : (a : R) → R⟦Γ'⟧) r) g')

Tactic:
by_cases h : g' = f g

Premises used: DFunLike.coe
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
g : Γ
r : R
g' : Γ'
h : g' = (f : (a : Γ) → Γ') g
⊢ Eq.{u_3 + 1} (α := R) (coeff (embDomain f ((single g : (a : R) → R⟦Γ⟧) r)) g')
    (coeff (((single ((f : (a : Γ) → Γ') g) : ZeroHom R R⟦Γ'⟧) : (a : R) → R⟦Γ'⟧) r) g')

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
g : Γ
r : R
g' : Γ'
h : ¬g' = (f : (a : Γ) → Γ') g
neg :
  g' ∉ Set.image.{u_1, u_2} (α := Γ) (⇑f : (a : Γ) → Γ') (support.{u_1, u_3} (R := R) ((single g : (a : R) → R⟦Γ⟧) r))
⊢ Eq.{u_3 + 1} (α := R) (coeff (embDomain f ((single g : (a : R) → R⟦Γ⟧) r)) g')
    (coeff (((single ((f : (a : Γ) → Γ') g) : ZeroHom R R⟦Γ'⟧) : (a : R) → R⟦Γ'⟧) r) g')

Tactic:
rw [embDomain_notin_image_support, coeff_single_of_ne h]

Premises used: HahnSeries.embDomain_notin_image_support, HahnSeries.coeff_single_of_ne
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
g : Γ
r : R
g' : Γ'
h : ¬g' = (f : (a : Γ) → Γ') g
pos :
  ∀ (hr : r = 0),
    g' ∉ Set.image.{u_1, u_2} (α := Γ) (⇑f : (a : Γ) → Γ') (support.{u_1, u_3} (R := R) ((single g : (a : R) → R⟦Γ⟧) r))
neg :
  ∀ (hr : ¬r = 0),
    g' ∉ Set.image.{u_1, u_2} (α := Γ) (⇑f : (a : Γ) → Γ') (support.{u_1, u_3} (R := R) ((single g : (a : R) → R⟦Γ⟧) r))
⊢ g' ∉ Set.image.{u_1, u_2} (α := Γ) (⇑f : (a : Γ) → Γ') (support.{u_1, u_3} (R := R) ((single g : (a : R) → R⟦Γ⟧) r))

Tactic:
by_cases hr : r = 0
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
g : Γ
r : R
g' : Γ'
h : ¬g' = (f : (a : Γ) → Γ') g
hr : r = 0
⊢ g' ∉ Set.image.{u_1, u_2} (α := Γ) (⇑f : (a : Γ) → Γ') (support.{u_1, u_3} (R := R) ((single g : (a : R) → R⟦Γ⟧) r))

Tactic:
simp [hr]
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
g : Γ
r : R
g' : Γ'
h : ¬g' = (f : (a : Γ) → Γ') g
hr : ¬r = 0
neg : g' ∉ Set.image (α := Γ) (⇑f : (a : Γ) → Γ') {g}
neg₁ : g' ∉ singleton (α := Γ') ((f : (a : Γ) → Γ') g : Γ')
neg₂ neg₃ neg₄ neg₅ : ¬g' = (f : (a : Γ) → Γ') g
⊢ g' ∉ Set.image.{u_1, u_2} (α := Γ) (⇑f : (a : Γ) → Γ') (support.{u_1, u_3} (R := R) ((single g : (a : R) → R⟦Γ⟧) r))

Tactic:
rwa [support_single_of_ne hr, Set.image_singleton, Set.mem_singleton_iff]

Premises used: Set.image_singleton, Set.mem_singleton_iff, HahnSeries.support_single_of_ne
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
x y : R⟦Γ⟧
xy : embDomain f x = embDomain f y
coeff : ∀ (g : Γ), x.coeff g = y.coeff g
⊢ x = y

Tactic:
ext g
-- Module: Mathlib.RingTheory.HahnSeries.Basic
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
x y : R⟦Γ⟧
xy : embDomain f x = embDomain f y
g : Γ
coeff : ∀ (xy : ∀ (x_1 : Γ'), (embDomain f x).coeff x_1 = (embDomain f y).coeff x_1) (g : Γ), x.coeff g = y.coeff g
⊢ x.coeff g = y.coeff g

Tactic:
rw [HahnSeries.ext_iff, funext_iff] at xy

Premises used: funext_iff, HahnSeries.ext_iff