awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V : Type u_6
α : Type u_7
inst : PartialOrder Γ
inst_1 : AddMonoid R
x : HahnSeries.{u_1, u_3} Γ Rᵃᵒᵖ
⊢ (Function.support.{u_1, u_3} (M := R) fun (a : Γ) ↦ AddOpposite.unop (x.coeff a)) = x.support
have h : ∀ (x_1 : Γ),
  Membership.mem (γ := Set Γ) (Function.support.{u_1, u_3} (M := R) fun (a : Γ) ↦ AddOpposite.unop (x.coeff a)) x_1 ↔
    x_1 ∈ x.support
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V : Type u_6
α : Type u_7
inst : PartialOrder Γ
inst_1 : AddMonoid R
x : R⟦Γ⟧ᵃᵒᵖ
⊢ Set.IsPWO.{u_1} (α := Γ)
    (Function.support.{u_1, u_3} (M := Rᵃᵒᵖ) fun (a : Γ) ↦ AddOpposite.op ((AddOpposite.unop x).coeff a))
have h : (Function.support.{u_1, u_3} (M := Rᵃᵒᵖ) fun (a : Γ) ↦ AddOpposite.op ((AddOpposite.unop x).coeff a)) =
  (AddOpposite.unop x).support
Tactic: convert! x.unop.isPWO_support
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V : Type u_6
α : Type u_7
inst : PartialOrder Γ
inst_1 : AddMonoid R
x : R⟦Γ⟧ᵃᵒᵖ
⊢ (Function.support.{u_1, u_3} (M := Rᵃᵒᵖ) fun (a : Γ) ↦ AddOpposite.op ((AddOpposite.unop x).coeff a)) =
    (AddOpposite.unop x).support
have h : ∀ (x_1 : Γ),
  Membership.mem (γ := Set Γ)
      (Function.support.{u_1, u_3} (M := Rᵃᵒᵖ) fun (a : Γ) ↦ AddOpposite.op ((AddOpposite.unop x).coeff a)) x_1 ↔
    x_1 ∈ (AddOpposite.unop x).support
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V : Type u_6
α : Type u_7
inst : PartialOrder Γ
inst_1 : AddMonoid R
x : R⟦Γ⟧ᵃᵒᵖ
⊢ (fun (x : HahnSeries.{u_1, u_3} Γ Rᵃᵒᵖ) ↦
        AddOpposite.op { coeff := fun (a : Γ) ↦ AddOpposite.unop (x.coeff a), isPWO_support' := ⋯ : R⟦Γ⟧ })
      ((fun (x : R⟦Γ⟧ᵃᵒᵖ) ↦
          { coeff := fun (a : Γ) ↦ AddOpposite.op ((AddOpposite.unop x).coeff a), isPWO_support' := ⋯ :
            HahnSeries.{u_1, u_3} Γ Rᵃᵒᵖ })
        x) =
    x
have a : AddOpposite.unop
    ((fun (x : HahnSeries.{u_1, u_3} Γ Rᵃᵒᵖ) ↦
        AddOpposite.op { coeff := fun (a : Γ) ↦ AddOpposite.unop (x.coeff a), isPWO_support' := sorry : R⟦Γ⟧ })
      ((fun (x : R⟦Γ⟧ᵃᵒᵖ) ↦
          { coeff := fun (a : Γ) ↦ AddOpposite.op ((AddOpposite.unop x).coeff a), isPWO_support' := sorry :
            HahnSeries.{u_1, u_3} Γ Rᵃᵒᵖ })
        x)) =
  AddOpposite.unop x
Tactic: apply AddOpposite.unop_injective
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V : Type u_6
α : Type u_7
inst : PartialOrder Γ
inst_1 : AddMonoid R
x y : HahnSeries.{u_1, u_3} Γ Rᵃᵒᵖ
⊢ AddOpposite.op { coeff := fun (a : Γ) ↦ AddOpposite.unop ((x + y).coeff a), isPWO_support' := ⋯ : R⟦Γ⟧ } =
    AddOpposite.op { coeff := fun (a : Γ) ↦ AddOpposite.unop (x.coeff a), isPWO_support' := ⋯ : R⟦Γ⟧ } +
      AddOpposite.op { coeff := fun (a : Γ) ↦ AddOpposite.unop (y.coeff a), isPWO_support' := ⋯ : R⟦Γ⟧ }
have a : AddOpposite.unop
    (AddOpposite.op { coeff := fun (a : Γ) ↦ AddOpposite.unop ((x + y).coeff a), isPWO_support' := sorry : R⟦Γ⟧ }) =
  AddOpposite.unop
    (AddOpposite.op { coeff := fun (a : Γ) ↦ AddOpposite.unop (x.coeff a), isPWO_support' := sorry : R⟦Γ⟧ } +
      AddOpposite.op { coeff := fun (a : Γ) ↦ AddOpposite.unop (y.coeff a), isPWO_support' := sorry : R⟦Γ⟧ })
Tactic: apply AddOpposite.unop_injective
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
S : Type u_4
U : Type u_5
V : Type u_6
α : Type u_7
inst : PartialOrder Γ
inst_1 : AddMonoid R
x y : HahnSeries.{u_1, u_3} Γ Rᵃᵒᵖ
⊢ AddOpposite.unop
      (AddOpposite.op { coeff := fun (a : Γ) ↦ AddOpposite.unop ((x + y).coeff a), isPWO_support' := ⋯ : R⟦Γ⟧ }) =
    AddOpposite.unop
      (AddOpposite.op { coeff := fun (a : Γ) ↦ AddOpposite.unop (x.coeff a), isPWO_support' := ⋯ : R⟦Γ⟧ } +
        AddOpposite.op { coeff := fun (a : Γ) ↦ AddOpposite.unop (y.coeff a), isPWO_support' := ⋯ : R⟦Γ⟧ })
have a : ∀ (x_1 : Γ),
  (AddOpposite.unop
          (AddOpposite.op
            { coeff := fun (a : Γ) ↦ AddOpposite.unop ((x + y).coeff a), isPWO_support' := sorry : R⟦Γ⟧ })).coeff
      x_1 =
    (AddOpposite.unop
          (AddOpposite.op { coeff := fun (a : Γ) ↦ AddOpposite.unop (x.coeff a), isPWO_support' := sorry : R⟦Γ⟧ } +
            AddOpposite.op { coeff := fun (a : Γ) ↦ AddOpposite.unop (y.coeff a), isPWO_support' := sorry : R⟦Γ⟧ })).coeff
      x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
x : HahnSeries.{u_1, u_3} Γ Rᵃᵒᵖ
⊢ support.{u_1, u_3} (R := R) (AddOpposite.unop ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) x)) = x.support
have h : ∀ (x_1 : Γ),
  Membership.mem (γ := Set Γ)
      (support.{u_1, u_3} (R := R) (AddOpposite.unop ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) x))) x_1 ↔
    x_1 ∈ x.support
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
x : R⟦Γ⟧ᵃᵒᵖ
⊢ support.{u_1, u_3} (R := Rᵃᵒᵖ) ((AddEquiv.symm addOppositeEquiv : (a : R⟦Γ⟧ᵃᵒᵖ) → Rᵃᵒᵖ⟦Γ⟧) x) =
    (AddOpposite.unop x).support
have rw : support.{u_1, u_3} (R := R)
    (AddOpposite.unop
      ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) ((AddEquiv.symm addOppositeEquiv : (a : R⟦Γ⟧ᵃᵒᵖ) → Rᵃᵒᵖ⟦Γ⟧) x))) =
  (AddOpposite.unop x).support
Tactic: rw [← addOppositeEquiv_support, AddEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
x : R⟦Γ⟧ᵃᵒᵖ
rw :
  support.{u_1, u_3} (R := R)
      (AddOpposite.unop
        ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) ((AddEquiv.symm addOppositeEquiv : (a : R⟦Γ⟧ᵃᵒᵖ) → Rᵃᵒᵖ⟦Γ⟧) x))) =
    (AddOpposite.unop x).support
⊢ support.{u_1, u_3} (R := Rᵃᵒᵖ) ((AddEquiv.symm addOppositeEquiv : (a : R⟦Γ⟧ᵃᵒᵖ) → Rᵃᵒᵖ⟦Γ⟧) x) =
    (AddOpposite.unop x).support
have rw₁ : (AddOpposite.unop x).support = (AddOpposite.unop x).support
Tactic: rw [← addOppositeEquiv_support, AddEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
x : HahnSeries.{u_1, u_3} Γ Rᵃᵒᵖ
⊢ orderTop.{u_1, u_3} (R := R) (AddOpposite.unop ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) x)) = x.orderTop
have simp : Eq.{u_1 + 1} (α := WithTop Γ)
  (if h : Eq (α := R⟦Γ⟧) (AddOpposite.unop ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) x)) 0 then ⊤
  else (↑(sorry.min (s := x.support) sorry) : WithTop Γ))
  (if h : x = 0 then ⊤ else (↑(sorry.min (s := x.support) sorry) : WithTop Γ))
Tactic: simp only [orderTop,
    addOppositeEquiv_support]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
x : HahnSeries.{u_1, u_3} Γ Rᵃᵒᵖ
⊢ Eq.{u_1 + 1} (α := WithTop Γ)
    (if h : Eq (α := R⟦Γ⟧) (AddOpposite.unop ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) x)) 0 then ⊤
    else (↑(⋯.min (s := x.support) ⋯) : WithTop Γ))
    (if h : x = 0 then ⊤ else (↑(⋯.min (s := x.support) ⋯) : WithTop Γ))
have simp : Eq.{u_1 + 1} (α := WithTop Γ)
  (if h : Eq (α := Γ → R) (fun (a : Γ) ↦ AddOpposite.unop (x.coeff a)) 0 then ⊤
  else (↑(sorry.min (s := x.support) sorry) : WithTop Γ))
  (if h : x = 0 then ⊤ else (↑(sorry.min (s := x.support) sorry) : WithTop Γ))
Tactic: simp only [addOppositeEquiv_apply, AddOpposite.unop_op, mk_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
x : HahnSeries.{u_1, u_3} Γ Rᵃᵒᵖ
⊢ Eq.{u_1 + 1} (α := WithTop Γ)
    (if h : Eq (α := Γ → R) (fun (a : Γ) ↦ AddOpposite.unop (x.coeff a)) 0 then ⊤
    else (↑(⋯.min (s := x.support) ⋯) : WithTop Γ))
    (if h : x = 0 then ⊤ else (↑(⋯.min (s := x.support) ⋯) : WithTop Γ))
have simp_rw : Eq.{u_1 + 1} (α := WithTop Γ)
  (if h : ∀ (x_1 : Γ), AddOpposite.unop (x.coeff x_1) = 0 x_1 then ⊤ else (↑(sorry.min (s := x.support) sorry) : WithTop Γ))
  (if h : ∀ (x_1 : Γ), x.coeff x_1 = coeff 0 x_1 then ⊤ else (↑(sorry.min (s := x.support) sorry) : WithTop Γ))
Tactic: simp_rw [HahnSeries.ext_iff, funext_iff]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
x : HahnSeries.{u_1, u_3} Γ Rᵃᵒᵖ
⊢ orderTop.{u_1, u_3} (R := R) (AddOpposite.unop ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) x)) = x.orderTop
have simp : Eq.{u_1 + 1} (α := WithTop Γ)
  (if h : Eq (α := R⟦Γ⟧) (AddOpposite.unop ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) x)) 0 then ⊤
  else (↑(sorry.min (s := x.support) sorry) : WithTop Γ))
  (if h : x = 0 then ⊤ else (↑(sorry.min (s := x.support) sorry) : WithTop Γ))
Tactic: classical
  simp only [orderTop,
    addOppositeEquiv_support]
  simp only [addOppositeEquiv_apply, AddOpposite.unop_op, mk_eq_zero]
  simp_rw [HahnSeries.ext_iff, funext_iff]
  simp only [Pi.zero_apply, AddOpposite.unop_eq_zero_iff, coeff_zero]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
x : HahnSeries.{u_1, u_3} Γ Rᵃᵒᵖ
simp :
  Eq.{u_1 + 1} (α := WithTop Γ)
    (if h : Eq (α := R⟦Γ⟧) (AddOpposite.unop ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) x)) 0 then ⊤
    else (↑(⋯.min (s := x.support) ⋯) : WithTop Γ))
    (if h : x = 0 then ⊤ else (↑(⋯.min (s := x.support) ⋯) : WithTop Γ))
⊢ orderTop.{u_1, u_3} (R := R) (AddOpposite.unop ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) x)) = x.orderTop
have simp₁ : Eq.{u_1 + 1} (α := WithTop Γ)
  (if h : Eq (α := Γ → R) (fun (a : Γ) ↦ AddOpposite.unop (x.coeff a)) 0 then ⊤
  else (↑(sorry.min (s := x.support) sorry) : WithTop Γ))
  (if h : x = 0 then ⊤ else (↑(sorry.min (s := x.support) sorry) : WithTop Γ))
Tactic: classical
  simp only [orderTop,
    addOppositeEquiv_support]
  simp only [addOppositeEquiv_apply, AddOpposite.unop_op, mk_eq_zero]
  simp_rw [HahnSeries.ext_iff, funext_iff]
  simp only [Pi.zero_apply, AddOpposite.unop_eq_zero_iff, coeff_zero]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
x : HahnSeries.{u_1, u_3} Γ Rᵃᵒᵖ
simp :
  Eq.{u_1 + 1} (α := WithTop Γ)
    (if h : Eq (α := R⟦Γ⟧) (AddOpposite.unop ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) x)) 0 then ⊤
    else (↑(⋯.min (s := x.support) ⋯) : WithTop Γ))
    (if h : x = 0 then ⊤ else (↑(⋯.min (s := x.support) ⋯) : WithTop Γ))
simp₁ :
  Eq.{u_1 + 1} (α := WithTop Γ)
    (if h : Eq (α := Γ → R) (fun (a : Γ) ↦ AddOpposite.unop (x.coeff a)) 0 then ⊤
    else (↑(⋯.min (s := x.support) ⋯) : WithTop Γ))
    (if h : x = 0 then ⊤ else (↑(⋯.min (s := x.support) ⋯) : WithTop Γ))
⊢ orderTop.{u_1, u_3} (R := R) (AddOpposite.unop ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) x)) = x.orderTop
have simp₂ : Eq.{u_1 + 1} (α := WithTop Γ)
  (if h : ∀ (x_1 : Γ), AddOpposite.unop (x.coeff x_1) = 0 x_1 then ⊤ else (↑(sorry.min (s := x.support) sorry) : WithTop Γ))
  (if h : ∀ (x_1 : Γ), x.coeff x_1 = coeff 0 x_1 then ⊤ else (↑(sorry.min (s := x.support) sorry) : WithTop Γ))
Tactic: classical
  simp only [orderTop,
    addOppositeEquiv_support]
  simp only [addOppositeEquiv_apply, AddOpposite.unop_op, mk_eq_zero]
  simp_rw [HahnSeries.ext_iff, funext_iff]
  simp only [Pi.zero_apply, AddOpposite.unop_eq_zero_iff, coeff_zero]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
x : R⟦Γ⟧ᵃᵒᵖ
⊢ orderTop.{u_1, u_3} (R := Rᵃᵒᵖ) ((AddEquiv.symm addOppositeEquiv : (a : R⟦Γ⟧ᵃᵒᵖ) → Rᵃᵒᵖ⟦Γ⟧) x) =
    (AddOpposite.unop x).orderTop
have rw : orderTop.{u_1, u_3} (R := R)
    (AddOpposite.unop
      ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) ((AddEquiv.symm addOppositeEquiv : (a : R⟦Γ⟧ᵃᵒᵖ) → Rᵃᵒᵖ⟦Γ⟧) x))) =
  (AddOpposite.unop x).orderTop
Tactic: rw [← addOppositeEquiv_orderTop, AddEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
x : R⟦Γ⟧ᵃᵒᵖ
rw :
  orderTop.{u_1, u_3} (R := R)
      (AddOpposite.unop
        ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) ((AddEquiv.symm addOppositeEquiv : (a : R⟦Γ⟧ᵃᵒᵖ) → Rᵃᵒᵖ⟦Γ⟧) x))) =
    (AddOpposite.unop x).orderTop
⊢ orderTop.{u_1, u_3} (R := Rᵃᵒᵖ) ((AddEquiv.symm addOppositeEquiv : (a : R⟦Γ⟧ᵃᵒᵖ) → Rᵃᵒᵖ⟦Γ⟧) x) =
    (AddOpposite.unop x).orderTop
have rw₁ : (AddOpposite.unop x).orderTop = (AddOpposite.unop x).orderTop
Tactic: rw [← addOppositeEquiv_orderTop, AddEquiv.apply_symm_apply]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
x : HahnSeries.{u_1, u_3} Γ Rᵃᵒᵖ
⊢ leadingCoeff.{u_1, u_3} (Γ := Γ) (AddOpposite.unop ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) x)) =
    AddOpposite.unop x.leadingCoeff
have inl : Eq.{u_3 + 1} (α := R)
  (leadingCoeff.{u_1, u_3} (Γ := Γ) (AddOpposite.unop ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) 0)))
  (AddOpposite.unop (leadingCoeff.{u_1, u_3} (Γ := Γ) 0))
Tactic: obtain rfl | hx := eq_or_ne x 0
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
x : HahnSeries.{u_1, u_3} Γ Rᵃᵒᵖ
inl :
  Eq.{u_3 + 1} (α := R)
    (leadingCoeff.{u_1, u_3} (Γ := Γ) (AddOpposite.unop ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) 0)))
    (AddOpposite.unop (leadingCoeff.{u_1, u_3} (Γ := Γ) 0))
⊢ leadingCoeff.{u_1, u_3} (Γ := Γ) (AddOpposite.unop ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) x)) =
    AddOpposite.unop x.leadingCoeff
have inr : ∀ (hx : x ≠ 0),
  leadingCoeff.{u_1, u_3} (Γ := Γ) (AddOpposite.unop ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) x)) =
    AddOpposite.unop x.leadingCoeff
Tactic: obtain rfl | hx := eq_or_ne x 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
x : HahnSeries.{u_1, u_3} Γ Rᵃᵒᵖ
hx : x ≠ 0
⊢ leadingCoeff.{u_1, u_3} (Γ := Γ) (AddOpposite.unop ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) x)) =
    AddOpposite.unop x.leadingCoeff
have inr : coeff (AddOpposite.unop ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) x)) (x.orderTop.untop sorry) =
  AddOpposite.unop (x.coeff (x.orderTop.untop sorry))
Tactic: simp only [ne_eq, AddOpposite.unop_eq_zero_iff, EmbeddingLike.map_eq_zero_iff, hx,
    not_false_eq_true, leadingCoeff_of_ne_zero, addOppositeEquiv_orderTop]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
x : HahnSeries.{u_1, u_3} Γ Rᵃᵒᵖ
⊢ leadingCoeff.{u_1, u_3} (Γ := Γ) (AddOpposite.unop ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) x)) =
    AddOpposite.unop x.leadingCoeff
have inl : Eq.{u_3 + 1} (α := R)
  (leadingCoeff.{u_1, u_3} (Γ := Γ) (AddOpposite.unop ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) 0)))
  (AddOpposite.unop (leadingCoeff.{u_1, u_3} (Γ := Γ) 0))
Tactic: classical
  obtain rfl | hx := eq_or_ne x 0
  · simp
  simp only [ne_eq, AddOpposite.unop_eq_zero_iff, EmbeddingLike.map_eq_zero_iff, hx,
    not_false_eq_true, leadingCoeff_of_ne_zero, addOppositeEquiv_orderTop]
  simp [addOppositeEquiv]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
x : HahnSeries.{u_1, u_3} Γ Rᵃᵒᵖ
inl :
  Eq.{u_3 + 1} (α := R)
    (leadingCoeff.{u_1, u_3} (Γ := Γ) (AddOpposite.unop ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) 0)))
    (AddOpposite.unop (leadingCoeff.{u_1, u_3} (Γ := Γ) 0))
⊢ leadingCoeff.{u_1, u_3} (Γ := Γ) (AddOpposite.unop ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) x)) =
    AddOpposite.unop x.leadingCoeff
have inr : ∀ (hx : x ≠ 0),
  leadingCoeff.{u_1, u_3} (Γ := Γ) (AddOpposite.unop ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) x)) =
    AddOpposite.unop x.leadingCoeff
Tactic: classical
  obtain rfl | hx := eq_or_ne x 0
  · simp
  simp only [ne_eq, AddOpposite.unop_eq_zero_iff, EmbeddingLike.map_eq_zero_iff, hx,
    not_false_eq_true, leadingCoeff_of_ne_zero, addOppositeEquiv_orderTop]
  simp [addOppositeEquiv]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
x : HahnSeries.{u_1, u_3} Γ Rᵃᵒᵖ
inl :
  Eq.{u_3 + 1} (α := R)
    (leadingCoeff.{u_1, u_3} (Γ := Γ) (AddOpposite.unop ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) 0)))
    (AddOpposite.unop (leadingCoeff.{u_1, u_3} (Γ := Γ) 0))
inr inr₁ :
  ∀ (hx : x ≠ 0),
    leadingCoeff.{u_1, u_3} (Γ := Γ) (AddOpposite.unop ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) x)) =
      AddOpposite.unop x.leadingCoeff
⊢ leadingCoeff.{u_1, u_3} (Γ := Γ) (AddOpposite.unop ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) x)) =
    AddOpposite.unop x.leadingCoeff
have inr₂ : ∀ (hx : x ≠ 0),
  coeff (AddOpposite.unop ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) x)) (x.orderTop.untop sorry) =
    AddOpposite.unop (x.coeff (x.orderTop.untop sorry))
Tactic: classical
  obtain rfl | hx := eq_or_ne x 0
  · simp
  simp only [ne_eq, AddOpposite.unop_eq_zero_iff, EmbeddingLike.map_eq_zero_iff, hx,
    not_false_eq_true, leadingCoeff_of_ne_zero, addOppositeEquiv_orderTop]
  simp [addOppositeEquiv]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
x : R⟦Γ⟧ᵃᵒᵖ
⊢ leadingCoeff.{u_1, u_3} (Γ := Γ) ((AddEquiv.symm addOppositeEquiv : (a : R⟦Γ⟧ᵃᵒᵖ) → Rᵃᵒᵖ⟦Γ⟧) x) =
    AddOpposite.op (AddOpposite.unop x).leadingCoeff
have a : AddOpposite.unop (leadingCoeff.{u_1, u_3} (Γ := Γ) ((AddEquiv.symm addOppositeEquiv : (a : R⟦Γ⟧ᵃᵒᵖ) → Rᵃᵒᵖ⟦Γ⟧) x)) =
  AddOpposite.unop (AddOpposite.op (AddOpposite.unop x).leadingCoeff)
Tactic: apply AddOpposite.unop_injective
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
x : R⟦Γ⟧ᵃᵒᵖ
⊢ AddOpposite.unop (leadingCoeff.{u_1, u_3} (Γ := Γ) ((AddEquiv.symm addOppositeEquiv : (a : R⟦Γ⟧ᵃᵒᵖ) → Rᵃᵒᵖ⟦Γ⟧) x)) =
    AddOpposite.unop (AddOpposite.op (AddOpposite.unop x).leadingCoeff)
have a : leadingCoeff.{u_1, u_3} (Γ := Γ)
    (AddOpposite.unop
      ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) ((AddEquiv.symm addOppositeEquiv : (a : R⟦Γ⟧ᵃᵒᵖ) → Rᵃᵒᵖ⟦Γ⟧) x))) =
  AddOpposite.unop (AddOpposite.op (AddOpposite.unop x).leadingCoeff)
Tactic: rw [← addOppositeEquiv_leadingCoeff, AddEquiv.apply_symm_apply, AddOpposite.unop_op]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
x : R⟦Γ⟧ᵃᵒᵖ
a :
  leadingCoeff.{u_1, u_3} (Γ := Γ)
      (AddOpposite.unop
        ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) ((AddEquiv.symm addOppositeEquiv : (a : R⟦Γ⟧ᵃᵒᵖ) → Rᵃᵒᵖ⟦Γ⟧) x))) =
    AddOpposite.unop (AddOpposite.op (AddOpposite.unop x).leadingCoeff)
⊢ AddOpposite.unop (leadingCoeff.{u_1, u_3} (Γ := Γ) ((AddEquiv.symm addOppositeEquiv : (a : R⟦Γ⟧ᵃᵒᵖ) → Rᵃᵒᵖ⟦Γ⟧) x)) =
    AddOpposite.unop (AddOpposite.op (AddOpposite.unop x).leadingCoeff)
have a₁ : (AddOpposite.unop x).leadingCoeff = AddOpposite.unop (AddOpposite.op (AddOpposite.unop x).leadingCoeff)
Tactic: rw [← addOppositeEquiv_leadingCoeff, AddEquiv.apply_symm_apply, AddOpposite.unop_op]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
x : R⟦Γ⟧ᵃᵒᵖ
a :
  leadingCoeff.{u_1, u_3} (Γ := Γ)
      (AddOpposite.unop
        ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) ((AddEquiv.symm addOppositeEquiv : (a : R⟦Γ⟧ᵃᵒᵖ) → Rᵃᵒᵖ⟦Γ⟧) x))) =
    AddOpposite.unop (AddOpposite.op (AddOpposite.unop x).leadingCoeff)
a₁ : (AddOpposite.unop x).leadingCoeff = AddOpposite.unop (AddOpposite.op (AddOpposite.unop x).leadingCoeff)
⊢ AddOpposite.unop (leadingCoeff.{u_1, u_3} (Γ := Γ) ((AddEquiv.symm addOppositeEquiv : (a : R⟦Γ⟧ᵃᵒᵖ) → Rᵃᵒᵖ⟦Γ⟧) x)) =
    AddOpposite.unop (AddOpposite.op (AddOpposite.unop x).leadingCoeff)
have a₂ : (AddOpposite.unop x).leadingCoeff = (AddOpposite.unop x).leadingCoeff
Tactic: rw [← addOppositeEquiv_leadingCoeff, AddEquiv.apply_symm_apply, AddOpposite.unop_op]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hx : x ≠ 0
hy : y ≠ 0
hxy : x + y ≠ 0
⊢ min (⋯.min (s := x.support) ⋯) (⋯.min (s := y.support) ⋯) ≤ ⋯.min (s := (x + y).support) ⋯
have rw : sorry.min (s := x.support ∪ y.support) sorry ≤ sorry.min (s := (x + y).support) sorry
Tactic: rw [← Set.IsWF.min_union]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
⊢ min x.orderTop y.orderTop ≤ (x + y).orderTop
have pos : ∀ (hx : x = 0), min x.orderTop y.orderTop ≤ (x + y).orderTop
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
pos : ∀ (hx : x = 0), min x.orderTop y.orderTop ≤ (x + y).orderTop
⊢ min x.orderTop y.orderTop ≤ (x + y).orderTop
have neg : ∀ (hx : ¬x = 0), min x.orderTop y.orderTop ≤ (x + y).orderTop
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hx : ¬x = 0
⊢ min x.orderTop y.orderTop ≤ (x + y).orderTop
have pos : ∀ (hy : y = 0), min x.orderTop y.orderTop ≤ (x + y).orderTop
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hx : ¬x = 0
pos : ∀ (hy : y = 0), min x.orderTop y.orderTop ≤ (x + y).orderTop
⊢ min x.orderTop y.orderTop ≤ (x + y).orderTop
have neg : ∀ (hy : ¬y = 0), min x.orderTop y.orderTop ≤ (x + y).orderTop
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hx : ¬x = 0
hy : ¬y = 0
⊢ min x.orderTop y.orderTop ≤ (x + y).orderTop
have pos : ∀ (hxy : x + y = 0), min x.orderTop y.orderTop ≤ (x + y).orderTop
Tactic: by_cases hxy : x + y = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hx : ¬x = 0
hy : ¬y = 0
pos : ∀ (hxy : x + y = 0), min x.orderTop y.orderTop ≤ (x + y).orderTop
⊢ min x.orderTop y.orderTop ≤ (x + y).orderTop
have neg : ∀ (hxy : ¬x + y = 0), min x.orderTop y.orderTop ≤ (x + y).orderTop
Tactic: by_cases hxy : x + y = 0
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : LinearOrder Γ
x y : R⟦Γ⟧
hx : ¬x = 0
hy : ¬y = 0
hxy : ¬x + y = 0
⊢ min x.orderTop y.orderTop ≤ (x + y).orderTop
have neg : min (sorry.min (s := x.support) sorry) (sorry.min (s := y.support) sorry) ≤ sorry.min (s := (x + y).support) sorry
Tactic: rw [orderTop_of_ne_zero hx, orderTop_of_ne_zero hy, orderTop_of_ne_zero hxy, ← WithTop.coe_min,
    WithTop.coe_le_coe]
-- Lean 4 proof step from Mathlib.RingTheory.HahnSeries.Addition (goal)
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : Zero Γ
inst_2 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x + y ≠ 0
⊢ min x.order y.order ≤ (x + y).order
have pos : ∀ (hx : x = 0), min x.order y.order ≤ (x + y).order
Tactic: by_cases hx : x = 0