awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
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 : Γ
⊢ {
          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
have 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
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
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 : Γ
⊢ (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
have 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
Tactic: by_cases ha : a ∈ x.support
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
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
⊢ (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
have 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
Tactic: by_cases ha : a ∈ x.support
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
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
⊢ (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
have pos : x.coeff
    (Classical.choose (p := fun (x_1 : Γ) ↦
      x_1 ∈ x.support ∧ Eq.{u_2 + 1} (α := Γ') ((f : (a : Γ) → Γ') x_1 : Γ') ((f : (a : Γ) → Γ') a : Γ')) sorry) =
  x.coeff a
Tactic: rw [dif_pos (Set.mem_image_of_mem f ha)]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
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
⊢ (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
have neg : ((f : (a : Γ) → Γ') a : Γ') ∉ (⇑f : (a : Γ) → Γ') '' x.support
Tactic: rw [dif_neg, Classical.not_not.1 fun c => ha ((mem_support _ _).2 c)]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
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
⊢ ((f : (a : Γ) → Γ') a : Γ') ∉ (⇑f : (a : Γ) → Γ') '' x.support
have neg : ∀
  (ha :
    Membership.mem.{u_2, u_2} (α := Γ') (γ := Set Γ') ((⇑f : (a : Γ) → Γ') '' x.support) ((f : (a : Γ) → Γ') a : Γ')),
  a ∈ x.support
Tactic: contrapose ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
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 : Γ')
⊢ a ∈ x.support
have neg : ∀ (b : Γ) (hb1 : b ∈ x.support) (hb2 : Eq.{u_2 + 1} (α := Γ') ((f : (a : Γ) → Γ') b : Γ') ((f : (a : Γ) → Γ') a : Γ')),
  a ∈ x.support
Tactic: obtain ⟨b, hb1, hb2⟩ := (Set.mem_image _ _ _).1 ha
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
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 : Γ')
⊢ a ∈ x.support
have neg : ∀ (hb1 : a ∈ x.support) (hb2 : Eq.{u_2 + 1} (α := Γ') ((f : (a : Γ) → Γ') b : Γ') ((f : (a : Γ) → Γ') a : Γ')),
  a ∈ x.support
Tactic: rwa [f.injective hb2] at hb1
Cleared hypotheses: hb1, hb2
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
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
⊢ Membership.mem (γ := Set Γ') ((⇑f : (a : Γ) → Γ') '' x.support) g
have contrapose : ∀ (hg : g ∉ (⇑f : (a : Γ) → Γ') '' x.support), g ∉ (embDomain f x).support
Tactic: contrapose hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
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
⊢ g ∉ (embDomain f x).support
have rw : ¬(embDomain f x).coeff g ≠ 0
Tactic: rw [mem_support, embDomain_notin_image_support hg, Classical.not_not]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
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
⊢ g ∉ (embDomain f x).support
have rw₁ : ¬Ne.{u_3 + 1} (α := R) 0 0
Tactic: rw [mem_support, embDomain_notin_image_support hg, Classical.not_not]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
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
⊢ g ∉ (embDomain f x).support
have rw₂ : Eq.{u_3 + 1} (α := R) 0 0
Tactic: rw [mem_support, embDomain_notin_image_support hg, Classical.not_not]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
inst : PartialOrder Γ
inst_1 : Zero R
inst_2 : PartialOrder Γ'
f : Γ ↪o Γ'
⊢ Eq (α := R⟦Γ'⟧) (embDomain f 0) 0
have coeff : ∀ (x : Γ'), Eq.{u_3 + 1} (α := R) (coeff (embDomain f 0) x) (coeff 0 x)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
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
⊢ Eq (α := R⟦Γ'⟧) (embDomain f ((single g : (a : R) → R⟦Γ⟧) r))
    (((single ((f : (a : Γ) → Γ') g) : ZeroHom R R⟦Γ'⟧) : (a : R) → R⟦Γ'⟧) r)
have coeff : ∀ (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: ext g'
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
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' : Γ'
⊢ 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')
have 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')
Tactic: by_cases h : g' = f g
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
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')
⊢ 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')
have 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')
Tactic: by_cases h : g' = f g
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
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')
have neg : g' ∉ Set.image.{u_1, u_2} (α := Γ) (⇑f : (a : Γ) → Γ') (support.{u_1, u_3} (R := R) ((single g : (a : R) → R⟦Γ⟧) r))
Tactic: rw [embDomain_notin_image_support, coeff_single_of_ne h]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
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
⊢ g' ∉ Set.image.{u_1, u_2} (α := Γ) (⇑f : (a : Γ) → Γ') (support.{u_1, u_3} (R := R) ((single g : (a : R) → R⟦Γ⟧) r))
have 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))
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
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))
⊢ g' ∉ Set.image.{u_1, u_2} (α := Γ) (⇑f : (a : Γ) → Γ') (support.{u_1, u_3} (R := R) ((single g : (a : R) → R⟦Γ⟧) r))
have 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))
Tactic: by_cases hr : r = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
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))
have neg : g' ∉ Set.image (α := Γ) (⇑f : (a : Γ) → Γ') {g}
Tactic: rwa [support_single_of_ne hr, Set.image_singleton, Set.mem_singleton_iff]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
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}
⊢ g' ∉ Set.image.{u_1, u_2} (α := Γ) (⇑f : (a : Γ) → Γ') (support.{u_1, u_3} (R := R) ((single g : (a : R) → R⟦Γ⟧) r))
have neg₁ : g' ∉ singleton (α := Γ') ((f : (a : Γ) → Γ') g : Γ')
Tactic: rwa [support_single_of_ne hr, Set.image_singleton, Set.mem_singleton_iff]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
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
⊢ x = y
have coeff : ∀ (g : Γ), x.coeff g = y.coeff g
Tactic: ext g
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
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 : Γ
⊢ x.coeff g = y.coeff g
have coeff : ∀ (xy : ∀ (x_1 : Γ'), (embDomain f x).coeff x_1 = (embDomain f y).coeff x_1) (g : Γ), x.coeff g = y.coeff g
Tactic: rw [HahnSeries.ext_iff, funext_iff] at xy
Cleared hypotheses: xy, g
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (hypothesis)
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 : ∀ (x_1 : Γ'), (embDomain f x).coeff x_1 = (embDomain f y).coeff x_1
g : Γ
⊢ x.coeff g = y.coeff g
have xyg : (embDomain f x).coeff ((f : (a : Γ) → Γ') g) = (embDomain f y).coeff ((f : (a : Γ) → Γ') g)
Tactic: have xyg := xy (f g)
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
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 : ∀ (x_1 : Γ'), (embDomain f x).coeff x_1 = (embDomain f y).coeff x_1
g : Γ
xyg : (embDomain f x).coeff ((f : (a : Γ) → Γ') g) = (embDomain f y).coeff ((f : (a : Γ) → Γ') g)
⊢ x.coeff g = y.coeff g
have coeff : ∀ (xyg : x.coeff g = (embDomain f y).coeff ((f : (a : Γ) → Γ') g)), x.coeff g = y.coeff g
Tactic: rwa [embDomain_coeff, embDomain_coeff] at xyg
Cleared hypotheses: xyg
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
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 : ∀ (x_1 : Γ'), (embDomain f x).coeff x_1 = (embDomain f y).coeff x_1
g : Γ
xyg : (embDomain f x).coeff ((f : (a : Γ) → Γ') g) = (embDomain f y).coeff ((f : (a : Γ) → Γ') g)
coeff : ∀ (xyg : x.coeff g = (embDomain f y).coeff ((f : (a : Γ) → Γ') g)), x.coeff g = y.coeff g
⊢ x.coeff g = y.coeff g
have coeff₁ : ∀ (xyg : x.coeff g = y.coeff g), x.coeff g = y.coeff g
Tactic: rwa [embDomain_coeff, embDomain_coeff] at xyg
Cleared hypotheses: xyg
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ' : Type u_2
R : Type u_3
inst : Zero R
inst_1 : PartialOrder Γ'
Γ : Type u_5
inst_2 : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
⊢ (embDomain f x).orderTop = WithTop.map (⇑f : (a : Γ) → Γ') x.orderTop
have inl : orderTop.{u_2, u_3} (R := R) (embDomain f 0) =
  WithTop.map.{u_5, u_2} (α := Γ) (⇑f : (a : Γ) → Γ') (orderTop.{u_5, u_3} (R := R) 0)
Tactic: obtain rfl | hx := eq_or_ne x 0
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ' : Type u_2
R : Type u_3
inst : Zero R
inst_1 : PartialOrder Γ'
Γ : Type u_5
inst_2 : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
inl :
  orderTop.{u_2, u_3} (R := R) (embDomain f 0) =
    WithTop.map.{u_5, u_2} (α := Γ) (⇑f : (a : Γ) → Γ') (orderTop.{u_5, u_3} (R := R) 0)
⊢ (embDomain f x).orderTop = WithTop.map (⇑f : (a : Γ) → Γ') x.orderTop
have inr : ∀ (hx : x ≠ 0), (embDomain f x).orderTop = WithTop.map (⇑f : (a : Γ) → Γ') x.orderTop
Tactic: obtain rfl | hx := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ' : Type u_2
R : Type u_3
inst : Zero R
inst_1 : PartialOrder Γ'
Γ : Type u_5
inst_2 : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
hx : x ≠ 0
⊢ (embDomain f x).orderTop = WithTop.map (⇑f : (a : Γ) → Γ') x.orderTop
have inr : (embDomain f x).orderTop = (↑((f : (a : Γ) → Γ') (x.orderTop.untop sorry)) : WithTop Γ')
Tactic: rw [← WithTop.coe_untop x.orderTop (by simpa using hx), WithTop.map_coe]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ' : Type u_2
R : Type u_3
inst : Zero R
inst_1 : PartialOrder Γ'
Γ : Type u_5
inst_2 : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
hx : x ≠ 0
⊢ (embDomain f x).orderTop = (↑((f : (a : Γ) → Γ') (x.orderTop.untop ⋯)) : WithTop Γ')
have inr : Membership.mem (α := Γ') (embDomain f x).support ((f : (a : Γ) → Γ') (x.orderTop.untop sorry) : Γ')
Tactic: apply orderTop_eq_of_le
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ' : Type u_2
R : Type u_3
inst : Zero R
inst_1 : PartialOrder Γ'
Γ : Type u_5
inst_2 : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
hx : x ≠ 0
inr : Membership.mem (α := Γ') (embDomain f x).support ((f : (a : Γ) → Γ') (x.orderTop.untop ⋯) : Γ')
⊢ (embDomain f x).orderTop = (↑((f : (a : Γ) → Γ') (x.orderTop.untop ⋯)) : WithTop Γ')
have inr₁ : ∀ g' ∈ (embDomain f x).support, (f : (a : Γ) → Γ') (x.orderTop.untop sorry) ≤ g'
Tactic: apply orderTop_eq_of_le
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ' : Type u_2
R : Type u_3
inst : Zero R
inst_1 : PartialOrder Γ'
Γ : Type u_5
inst_2 : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
hx : x ≠ 0
y : Γ'
hy : y ∈ (embDomain f x).support
⊢ (f : (a : Γ) → Γ') (x.orderTop.untop ⋯) ≤ y
have inr : ∀ (z : Γ) (hz : z ∈ x.support) (hy : Membership.mem (α := Γ') (embDomain f x).support ((f : (a : Γ) → Γ') z : Γ')),
  LE.le.{u_2} (α := Γ') ((f : (a : Γ) → Γ') (x.orderTop.untop sorry) : Γ') ((f : (a : Γ) → Γ') z : Γ')
Tactic: obtain ⟨z, hz, rfl⟩ :=
    (Set.mem_image _ _ _).mp <| Set.mem_of_subset_of_mem support_embDomain_subset hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ' : Type u_2
R : Type u_3
inst : Zero R
inst_1 : PartialOrder Γ'
Γ : Type u_5
inst_2 : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
hx : x ≠ 0
z : Γ
hz : z ∈ x.support
hy : Membership.mem (α := Γ') (embDomain f x).support ((f : (a : Γ) → Γ') z : Γ')
⊢ LE.le.{u_2} (α := Γ') ((f : (a : Γ) → Γ') (x.orderTop.untop ⋯) : Γ') ((f : (a : Γ) → Γ') z : Γ')
have inr : x.orderTop ≤ (↑z : WithTop Γ)
Tactic: rw [OrderEmbedding.le_iff_le, WithTop.untop_le_iff]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ' : Type u_2
R : Type u_3
inst : Zero R
inst_1 : PartialOrder Γ'
Γ : Type u_5
inst_2 : LinearOrder Γ
f : Γ ↪o Γ'
x : R⟦Γ⟧
hx : x ≠ 0
z : Γ
hz : z ∈ x.support
hy : Membership.mem (α := Γ') (embDomain f x).support ((f : (a : Γ) → Γ') z : Γ')
⊢ x.orderTop ≤ (↑z : WithTop Γ)
have inr : x.coeff z ≠ 0
Tactic: apply orderTop_le_of_coeff_ne_zero
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
f : Γ → R
n : Γ
hn : ∀ m < n, f m = 0
⊢ BddBelow (Function.support f)
have refine : ∀ x ∈ Function.support f, n ≤ x
Tactic: refine ⟨n, fun _ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
f : Γ → R
n : Γ
hn : ∀ m < n, f m = 0
x : Γ
⊢ x ∈ Function.support f → n ≤ x
have contrapose : ¬n ≤ x → x ∉ Function.support f
Tactic: contrapose
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
x : R⟦Γ⟧
i : WithTop Γ
H : ∀ (j : Γ), (↑j : WithTop Γ) < i → x.coeff j = 0
⊢ i ≤ x.orderTop
have inl : ∀ (H : ∀ (j : Γ), (↑j : WithTop Γ) < i → Eq.{u_3 + 1} (α := R) (coeff 0 j) 0), i ≤ orderTop.{u_1, u_3} (R := R) 0
Tactic: obtain rfl | h := eq_or_ne x 0
Cleared hypotheses: x, H
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
x : R⟦Γ⟧
i : WithTop Γ
H : ∀ (j : Γ), (↑j : WithTop Γ) < i → x.coeff j = 0
inl : ∀ (H : ∀ (j : Γ), (↑j : WithTop Γ) < i → Eq.{u_3 + 1} (α := R) (coeff 0 j) 0), i ≤ orderTop.{u_1, u_3} (R := R) 0
⊢ i ≤ x.orderTop
have inr : ∀ (h : x ≠ 0), i ≤ x.orderTop
Tactic: obtain rfl | h := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
x : R⟦Γ⟧
i : WithTop Γ
H : ∀ (j : Γ), (↑j : WithTop Γ) < i → x.coeff j = 0
h : x ≠ 0
⊢ i ≤ x.orderTop
have inr : ∀ (hi : x.orderTop < i), False
Tactic: by_contra! hi
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
x : R⟦Γ⟧
i : WithTop Γ
⊢ x.orderTop < i ↔ ∃ (j : Γ), (↑j : WithTop Γ) < i ∧ x.coeff j ≠ 0
have rw : (¬∀ (j : Γ), (↑j : WithTop Γ) < i → x.coeff j = 0) ↔ ∃ (j : Γ), (↑j : WithTop Γ) < i ∧ x.coeff j ≠ 0
Tactic: rw [← not_le, le_orderTop_iff_forall]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
inst_2 : Zero Γ
x : R⟦Γ⟧
i : Γ
h : x ≠ 0
H : ∀ j < i, x.coeff j = 0
⊢ i ≤ x.order
have contrapose! : ∀ (h : x.order < i), x = 0
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (hypothesis)
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
inst_2 : Zero Γ
x : R⟦Γ⟧
i : Γ
H : ∀ j < i, x.coeff j = 0
h : x.order < i
⊢ x = 0
have this : x.coeff x.order = 0
Tactic: have := H _ h
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
inst_2 : Zero Γ
x : R⟦Γ⟧
i : Γ
H : ∀ j < i, x.coeff j = 0
h : x.order < i
this : x.coeff x.order = 0
⊢ x = 0
have rwa : ∀ (this : x = 0), x = 0
Tactic: rwa [coeff_order_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
inst_2 : Zero Γ
x : R⟦Γ⟧
i : Γ
h : x ≠ 0
⊢ x.order < i ↔ ∃ j < i, x.coeff j ≠ 0
have rw : (¬∀ j < i, x.coeff j = 0) ↔ ∃ j < i, x.coeff j ≠ 0
Tactic: rw [← not_le, le_order_iff_forall h]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
inst_2 : LocallyFiniteOrder Γ
inst_3 : Zero Γ
f : Γ → R
hf : f ≠ 0
n : Γ
hn : ∀ m < n, f m = 0
⊢ n ≤ (ofSuppBddBelow f ⋯).order
have rw : ∀ j < n, (ofSuppBddBelow f sorry).coeff j = 0
Tactic: rw [le_order_iff_forall]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Basic (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero R
inst_1 : LinearOrder Γ
inst_2 : LocallyFiniteOrder Γ
inst_3 : Zero Γ
f : Γ → R
hf : f ≠ 0
n : Γ
hn : ∀ m < n, f m = 0
rw : ∀ j < n, (ofSuppBddBelow f ⋯).coeff j = 0
⊢ n ≤ (ofSuppBddBelow f ⋯).order
have rw₁ : ofSuppBddBelow f sorry ≠ 0
Tactic: rw [le_order_iff_forall]