awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
Γ' : Type u_3
inst_2 : LinearOrder Γ'
f : Γ ↪o Γ'
inst_3 : Zero R
a b : Lex R⟦Γ⟧
mp :
  (∃ (i : Γ'),
        (∀ j < i,
            Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) j)
              (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) j)) ∧
          LT.lt.{u_2} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) i)
            (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) i)) ∨
      Eq (α := R⟦Γ'⟧) (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a))
        (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) →
    (∃ (i : Γ),
        (∀ j < i,
            Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) j)
              (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) j)) ∧
          LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i)
            (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)) ∨
      a = b
⊢ (∃ (i : Γ'),
        (∀ j < i,
            Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) j)
              (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) j)) ∧
          LT.lt.{u_2} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) i)
            (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) i)) ∨
      Eq (α := R⟦Γ'⟧) (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a))
        (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) ↔
    (∃ (i : Γ),
        (∀ j < i,
            Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) j)
              (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) j)) ∧
          LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i)
            (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)) ∨
      a = b
have mpr : (∃ (i : Γ),
      (∀ j < i,
          Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) j)
            (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) j)) ∧
        LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i)
          (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)) ∨
    a = b →
  (∃ (i : Γ'),
      (∀ j < i,
          Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) j)
            (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) j)) ∧
        LT.lt.{u_2} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) i)
          (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) i)) ∨
    Eq (α := R⟦Γ'⟧) (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b))
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
Γ' : Type u_3
inst_2 : LinearOrder Γ'
f : Γ ↪o Γ'
inst_3 : Zero R
a b : Lex R⟦Γ⟧
i : Γ'
hj :
  ∀ j < i,
    Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) j)
      (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) j)
hi :
  LT.lt.{u_2} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) i)
    (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) i)
⊢ Membership.mem (γ := Set Γ') (Set.range.{u_3, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')) i
have contrapose : ∀ (hi : i ∉ Set.range.{u_3, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')),
  ¬LT.lt.{u_2} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) i)
      (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) i)
Tactic: contrapose hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (hypothesis)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
Γ' : Type u_3
inst_2 : LinearOrder Γ'
f : Γ ↪o Γ'
inst_3 : Zero R
a b : Lex R⟦Γ⟧
i : Γ'
hj :
  ∀ j < i,
    Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) j)
      (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) j)
hi :
  LT.lt.{u_2} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) i)
    (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) i)
⊢ (∃ (i : Γ),
      (∀ j < i,
          Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) j)
            (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) j)) ∧
        LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i)
          (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)) ∨
    a = b
have himem : Membership.mem (γ := Set Γ') (Set.range.{u_3, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')) i
Tactic: have himem : i ∈ Set.range f := by
          contrapose hi
          simp [embDomain_notin_range hi]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
Γ' : Type u_3
inst_2 : LinearOrder Γ'
f : Γ ↪o Γ'
inst_3 : Zero R
a b : Lex R⟦Γ⟧
i : Γ'
hj :
  ∀ j < i,
    Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) j)
      (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) j)
hi :
  LT.lt.{u_2} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) i)
    (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) i)
himem : Membership.mem (γ := Set Γ') (Set.range.{u_3, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')) i
⊢ (∃ (i : Γ),
      (∀ j < i,
          Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) j)
            (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) j)) ∧
        LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i)
          (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)) ∨
    a = b
have mp : ∀ (k : Γ)
  (hj :
    ∀ j < (f : (a : Γ) → Γ') k,
      Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) j)
        (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) j))
  (hi :
    LT.lt.{u_2} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) ((f : (a : Γ) → Γ') k))
      (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) ((f : (a : Γ) → Γ') k))),
  (∃ (i : Γ),
      (∀ j < i,
          Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) j)
            (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) j)) ∧
        LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i)
          (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)) ∨
    a = b
Tactic: obtain ⟨k, rfl⟩ := himem
Cleared hypotheses: i, hj, hi, himem
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
Γ' : Type u_3
inst_2 : LinearOrder Γ'
f : Γ ↪o Γ'
inst_3 : Zero R
a b : Lex R⟦Γ⟧
k : Γ
hj :
  ∀ j < (f : (a : Γ) → Γ') k,
    Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) j)
      (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) j)
hi :
  LT.lt.{u_2} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) ((f : (a : Γ) → Γ') k))
    (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) ((f : (a : Γ) → Γ') k))
⊢ (∃ (i : Γ),
      (∀ j < i,
          Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) j)
            (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) j)) ∧
        LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i)
          (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)) ∨
    a = b
have mp : ∀ (j : Γ) (hjk : j < k),
  Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) j) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) j)
Tactic: refine Or.inl ⟨k, fun j hjk ↦ ?_, by simpa using hi⟩
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
Γ' : Type u_3
inst_2 : LinearOrder Γ'
f : Γ ↪o Γ'
inst_3 : Zero R
a b : Lex R⟦Γ⟧
i : Γ
hj :
  ∀ j < i,
    Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) j) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) j)
hi : LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)
⊢ (∃ (i : Γ'),
      (∀ j < i,
          Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) j)
            (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) j)) ∧
        LT.lt.{u_2} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) i)
          (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) i)) ∨
    Eq (α := R⟦Γ'⟧) (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b))
have mpr : ∀ (k : Γ') (hki : k < (f : (a : Γ) → Γ') i),
  Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) k)
    (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) k)
Tactic: refine Or.inl ⟨f i, fun k hki ↦ ?_, by simpa using hi⟩
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
Γ' : Type u_3
inst_2 : LinearOrder Γ'
f : Γ ↪o Γ'
inst_3 : Zero R
a b : Lex R⟦Γ⟧
i : Γ
hj :
  ∀ j < i,
    Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) j) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) j)
hi : LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)
k : Γ'
hki : k < (f : (a : Γ) → Γ') i
⊢ Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) k)
    (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) k)
have pos : ∀ (hkmem : Membership.mem (γ := Set Γ') (Set.range.{u_3, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')) k),
  Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) k)
    (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) k)
Tactic: by_cases hkmem : k ∈ Set.range f
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
Γ' : Type u_3
inst_2 : LinearOrder Γ'
f : Γ ↪o Γ'
inst_3 : Zero R
a b : Lex R⟦Γ⟧
i : Γ
hj :
  ∀ j < i,
    Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) j) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) j)
hi : LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)
k : Γ'
hki : k < (f : (a : Γ) → Γ') i
pos :
  ∀ (hkmem : Membership.mem (γ := Set Γ') (Set.range.{u_3, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')) k),
    Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) k)
      (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) k)
⊢ Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) k)
    (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) k)
have neg : ∀ (hkmem : k ∉ Set.range.{u_3, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')),
  Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) k)
    (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) k)
Tactic: by_cases hkmem : k ∈ Set.range f
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Lex (goal)
Goal:
Γ : Type u_1
R : Type u_2
inst : LinearOrder Γ
inst_1 : PartialOrder R
Γ' : Type u_3
inst_2 : LinearOrder Γ'
f : Γ ↪o Γ'
inst_3 : Zero R
a b : Lex R⟦Γ⟧
i : Γ
hj :
  ∀ j < i,
    Eq.{u_2 + 1} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) j) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) j)
hi : LT.lt.{u_2} (α := R) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a) i) (coeff ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b) i)
k : Γ'
hki : k < (f : (a : Γ) → Γ') i
hkmem : Membership.mem (γ := Set Γ') (Set.range.{u_3, u_1 + 1} (ι := Γ) (⇑f : (a : Γ) → Γ')) k
⊢ Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) k)
    (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) k)
have pos : ∀ (j' : Γ) (hki : LT.lt.{u_3} (α := Γ') ((f : (a : Γ) → Γ') j' : Γ') ((f : (a : Γ) → Γ') i : Γ')),
  Eq.{u_2 + 1} (α := R) (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) a)) ((f : (a : Γ) → Γ') j'))
    (coeff (embDomain f ((ofLex : (a : Lex R⟦Γ⟧) → R⟦Γ⟧) b)) ((f : (a : Γ) → Γ') j'))
Tactic: obtain ⟨j', rfl⟩ := hkmem
Cleared hypotheses: k, hki, hkmem
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero Γ
inst_1 : PartialOrder Γ
inst_2 : Zero R
inst_3 : One R
inst_4 : NeZero.{u_3} (R := R) 1
⊢ Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_3} (R := R) 1) 0
have rw : Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_3} (R := R) ((single 0 : (a : R) → R⟦Γ⟧) 1)) 0
Tactic: rw [← single_zero_one, orderTop_single one_ne_zero, WithTop.coe_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero Γ
inst_1 : PartialOrder Γ
inst_2 : Zero R
inst_3 : One R
inst_4 : NeZero.{u_3} (R := R) 1
rw : Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_3} (R := R) ((single 0 : (a : R) → R⟦Γ⟧) 1)) 0
⊢ Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_3} (R := R) 1) 0
have rw₁ : Eq.{u_1 + 1} (α := WithTop Γ) (↑0 : WithTop Γ) 0
Tactic: rw [← single_zero_one, orderTop_single one_ne_zero, WithTop.coe_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero Γ
inst_1 : PartialOrder Γ
inst_2 : Zero R
inst_3 : One R
inst_4 : NeZero.{u_3} (R := R) 1
rw : Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_3} (R := R) ((single 0 : (a : R) → R⟦Γ⟧) 1)) 0
rw₁ : Eq.{u_1 + 1} (α := WithTop Γ) (↑0 : WithTop Γ) 0
⊢ Eq.{u_1 + 1} (α := WithTop Γ) (orderTop.{u_1, u_3} (R := R) 1) 0
have rw₂ : Eq.{u_1 + 1} (α := Γ) 0 0
Tactic: rw [← single_zero_one, orderTop_single one_ne_zero, WithTop.coe_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero Γ
inst_1 : PartialOrder Γ
inst_2 : MulZeroOneClass R
⊢ Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_3} (R := R) 1) 0
have inl : Subsingleton R → Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_3} (R := R) 1) 0
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero Γ
inst_1 : PartialOrder Γ
inst_2 : MulZeroOneClass R
inl : Subsingleton R → Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_3} (R := R) 1) 0
⊢ Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_3} (R := R) 1) 0
have inr : Nontrivial R → Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_3} (R := R) 1) 0
Tactic: cases subsingleton_or_nontrivial R
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero Γ
inst_1 : PartialOrder Γ
inst_2 : MulZeroOneClass R
h : Subsingleton R
⊢ Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_3} (R := R) 1) 0
have inl : Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_3} (R := R) 0) 0
Tactic: rw [Subsingleton.elim (1 : R⟦Γ⟧) 0, order_zero]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : Zero Γ
inst_1 : PartialOrder Γ
inst_2 : MulZeroOneClass R
h : Subsingleton R
inl : Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_3} (R := R) 0) 0
⊢ Eq.{u_1 + 1} (α := Γ) (order.{u_1, u_3} (R := R) 1) 0
have inl₁ : Eq.{u_1 + 1} (α := Γ) 0 0
Tactic: rw [Subsingleton.elim (1 : R⟦Γ⟧) 0, order_zero]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : PartialOrder Γ
inst_1 : SMul R V
inst_2 : PartialOrder Γ'
inst_3 : VAdd Γ Γ'
inst_4 : IsOrderedCancelVAdd Γ Γ'
inst_5 : Zero R
inst_6 : AddCommMonoid V
x : R⟦Γ⟧
y : HahnModule Γ' R V
a : Γ'
ha :
  Membership.mem (γ := Set Γ')
    {a : Γ' |
      Ne.{u_5 + 1} (α := V)
        (∑
          ij ∈
            VAddAntidiagonal (s := x.support) (t :=
              HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)) a ⋯,
          HSMul.hSMul (β := V) (x.coeff ij.1) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) ij.2))
        0}
    a
⊢ (VAddAntidiagonal (s := x.support) (t :=
      HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)) a ⋯).Nonempty
have contrapose! : ∀
  (ha :
    VAddAntidiagonal (s := x.support) (t :=
        HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)) a sorry =
      ∅),
  a ∉
    {a : Γ' |
      Ne.{u_5 + 1} (α := V)
        (∑
          ij ∈
            VAddAntidiagonal (s := x.support) (t :=
              HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)) a sorry,
          HSMul.hSMul (β := V) (x.coeff ij.1) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) ij.2))
        0}
Tactic: contrapose! ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : Zero R
inst_6 : SMulZeroClass R V
x : R⟦Γ⟧
⊢ HSMul.hSMul (β := HahnModule Γ' R V) x 0 = 0
have h : ∀ (x_1 : Γ'),
  Eq.{u_5 + 1} (α := V)
    (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (HSMul.hSMul (β := HahnModule Γ' R V) x 0)) x_1)
    (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) 0) x_1)
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : Zero R
inst_6 : SMulZeroClass R V
x : R⟦Γ⟧
y : HahnModule Γ' R V
a : Γ'
s : Set Γ'
hs : s.IsPWO
hys : HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) ⊆ s
⊢ Eq.{u_5 + 1} (α := V)
    (∑
      ij ∈
        VAddAntidiagonal (s := x.support) (t :=
          HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)) a ⋯,
      HSMul.hSMul (β := V) (x.coeff ij.1) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) ij.2))
    (∑ ij ∈ VAddAntidiagonal (s := x.support) (t := s) a ⋯,
      HSMul.hSMul (β := V) (x.coeff ij.1) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) ij.2))
have apply : ∀
  x_1 ∈
    VAddAntidiagonal (s := x.support) (t := s) a sorry \
      VAddAntidiagonal (s := x.support) (t :=
        HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)) a sorry,
  HSMul.hSMul (β := V) (x.coeff x_1.1) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) x_1.2) = 0
Tactic: apply sum_subset_zero_on_sdiff (vaddAntidiagonal_mono_right _ _ _ hys) _ fun _ _ => rfl
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (hypothesis)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : Zero R
inst_6 : SMulZeroClass R V
x : R⟦Γ⟧
y : HahnModule Γ' R V
a : Γ'
s : Set Γ'
hs : s.IsPWO
hys : HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) ⊆ s
b : Γ × Γ'
hb :
  b ∈
    VAddAntidiagonal (s := x.support) (t := s) a ⋯ \
      VAddAntidiagonal (s := x.support) (t :=
        HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)) a ⋯
⊢ HSMul.hSMul (β := V) (x.coeff b.1) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) b.2) = 0
have hb₁ : (x.coeff b.1 ≠ 0 ∧ b.2 ∈ s ∧ b.1 +ᵥ b.2 = a) ∧
  (x.coeff b.1 ≠ 0 →
    b.1 +ᵥ b.2 = a → Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) b.2) 0)
Tactic: simp only [not_and, mem_sdiff, mem_vaddAntidiagonal, HahnSeries.mem_support, not_imp_not] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : Zero R
inst_6 : SMulZeroClass R V
x : R⟦Γ⟧
y : HahnModule Γ' R V
a : Γ'
s : Set Γ'
hs : s.IsPWO
hys : HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) ⊆ s
b : Γ × Γ'
hb :
  (x.coeff b.1 ≠ 0 ∧ b.2 ∈ s ∧ b.1 +ᵥ b.2 = a) ∧
    (x.coeff b.1 ≠ 0 →
      b.1 +ᵥ b.2 = a → Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) b.2) 0)
⊢ HSMul.hSMul (β := V) (x.coeff b.1) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) b.2) = 0
have rw : HSMul.hSMul (β := V) (x.coeff b.1) 0 = 0
Tactic: rw [hb.2 hb.1.1 hb.1.2.2, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : Zero R
inst_6 : SMulZeroClass R V
x : R⟦Γ⟧
y : HahnModule Γ' R V
a : Γ'
s : Set Γ'
hs : s.IsPWO
hys : HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) ⊆ s
b : Γ × Γ'
hb :
  (x.coeff b.1 ≠ 0 ∧ b.2 ∈ s ∧ b.1 +ᵥ b.2 = a) ∧
    (x.coeff b.1 ≠ 0 →
      b.1 +ᵥ b.2 = a → Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) b.2) 0)
rw : HSMul.hSMul (β := V) (x.coeff b.1) 0 = 0
⊢ HSMul.hSMul (β := V) (x.coeff b.1) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) b.2) = 0
have rw₁ : Eq.{u_5 + 1} (α := V) 0 0
Tactic: rw [hb.2 hb.1.1 hb.1.2.2, smul_zero]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Multiplication (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : PartialOrder Γ
inst_1 : PartialOrder Γ'
inst_2 : VAdd Γ Γ'
inst_3 : IsOrderedCancelVAdd Γ Γ'
inst_4 : AddCommMonoid V
inst_5 : Zero R
inst_6 : SMulZeroClass R V
x : R⟦Γ⟧
y : HahnModule Γ' R V
a : Γ'
s : Set Γ'
hs : s.IsPWO
hys : HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) ⊆ s
⊢ Eq.{u_5 + 1} (α := V) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) (x • y)) a)
    (∑ ij ∈ VAddAntidiagonal (s := x.support) (t := s) a ⋯,
      HSMul.hSMul (β := V) (x.coeff ij.1) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) ij.2))
have rw : Eq.{u_5 + 1} (α := V)
  (∑
    ij ∈
      VAddAntidiagonal (s := x.support) (t :=
        HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y)) a sorry,
    HSMul.hSMul (β := V) (x.coeff ij.1) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) ij.2))
  (∑ ij ∈ VAddAntidiagonal (s := x.support) (t := s) a sorry,
    HSMul.hSMul (β := V) (x.coeff ij.1) (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) y) ij.2))
Tactic: classical
  rw [coeff_smul]
  apply sum_subset_zero_on_sdiff (vaddAntidiagonal_mono_right _ _ _ hys) _ fun _ _ => rfl
  intro b hb
  simp only [not_and, mem_sdiff, mem_vaddAntidiagonal, HahnSeries.mem_support, not_imp_not] at hb
  rw [hb.2 hb.1.1 hb.1.2.2, smul_zero]