awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.HahnSeries.Addition
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ᵃᵒᵖ
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
⊢ (Function.support.{u_1, u_3} (M := R) fun (a : Γ) ↦ AddOpposite.unop (x.coeff a)) = x.support

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.Addition
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ᵃᵒᵖ
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:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Addition
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⟦Γ⟧ᵃᵒᵖ
⊢ (AddOpposite.unop x).support.IsPWO

Tactic:
x.unop.isPWO_support

Premises used: HahnSeries.isPWO_support, AddOpposite.unop
-- Module: Mathlib.RingTheory.HahnSeries.Addition
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⟦Γ⟧ᵃᵒᵖ
h :
  (Function.support.{u_1, u_3} (M := Rᵃᵒᵖ) fun (a : Γ) ↦ AddOpposite.op ((AddOpposite.unop x).coeff a)) =
    (AddOpposite.unop x).support
⊢ Set.IsPWO.{u_1} (α := Γ)
    (Function.support.{u_1, u_3} (M := Rᵃᵒᵖ) fun (a : Γ) ↦ AddOpposite.op ((AddOpposite.unop x).coeff a))

Tactic:
convert! x.unop.isPWO_support

Premises used: HahnSeries.isPWO_support, AddOpposite.unop
-- Module: Mathlib.RingTheory.HahnSeries.Addition
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⟦Γ⟧ᵃᵒᵖ
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
⊢ (Function.support.{u_1, u_3} (M := Rᵃᵒᵖ) fun (a : Γ) ↦ AddOpposite.op ((AddOpposite.unop x).coeff a)) =
    (AddOpposite.unop x).support

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.Addition
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⟦Γ⟧ᵃᵒᵖ
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:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Addition
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ᵃᵒᵖ
⊢ (fun (x : R⟦Γ⟧ᵃᵒᵖ) ↦
        { coeff := fun (a : Γ) ↦ AddOpposite.op ((AddOpposite.unop x).coeff a), isPWO_support' := ⋯ :
          HahnSeries.{u_1, u_3} Γ Rᵃᵒᵖ })
      ((fun (x : HahnSeries.{u_1, u_3} Γ Rᵃᵒᵖ) ↦
          AddOpposite.op { coeff := fun (a : Γ) ↦ AddOpposite.unop (x.coeff a), isPWO_support' := ⋯ : R⟦Γ⟧ })
        x) =
    x

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Addition
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⟦Γ⟧ᵃᵒᵖ
a :
  AddOpposite.unop
      ((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)) =
    AddOpposite.unop x
⊢ (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

Tactic:
apply AddOpposite.unop_injective

Premises used: AddOpposite.unop_injective
-- Module: Mathlib.RingTheory.HahnSeries.Addition
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⟦Γ⟧ᵃᵒᵖ
⊢ AddOpposite.unop
      ((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)) =
    AddOpposite.unop x

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Addition
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ᵃᵒᵖ
a :
  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⟦Γ⟧ })
⊢ 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⟦Γ⟧ }

Tactic:
apply AddOpposite.unop_injective

Premises used: AddOpposite.unop_injective
-- Module: Mathlib.RingTheory.HahnSeries.Addition
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ᵃᵒᵖ
a :
  ∀ (x_1 : Γ),
    (AddOpposite.unop
            (AddOpposite.op
              { coeff := fun (a : Γ) ↦ AddOpposite.unop ((x + y).coeff a), isPWO_support' := ⋯ : R⟦Γ⟧ })).coeff
        x_1 =
      (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⟦Γ⟧ })).coeff
        x_1
⊢ 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⟦Γ⟧ })

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.Addition
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ᵃᵒᵖ
x_1 : Γ
⊢ (AddOpposite.unop
          (AddOpposite.op
            { coeff := fun (a : Γ) ↦ AddOpposite.unop ((x + y).coeff a), isPWO_support' := ⋯ : R⟦Γ⟧ })).coeff
      x_1 =
    (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⟦Γ⟧ })).coeff
      x_1

Tactic:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
x : HahnSeries.{u_1, u_3} Γ Rᵃᵒᵖ
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
⊢ support.{u_1, u_3} (R := R) (AddOpposite.unop ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) x)) = x.support

Tactic:
ext
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
x : HahnSeries.{u_1, u_3} Γ Rᵃᵒᵖ
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:
simp [addOppositeEquiv_apply]

Premises used: HahnSeries.addOppositeEquiv_apply
-- Module: Mathlib.RingTheory.HahnSeries.Addition
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
rw₁ rw₂ : (AddOpposite.unop x).support = (AddOpposite.unop x).support
⊢ support.{u_1, u_3} (R := Rᵃᵒᵖ) ((AddEquiv.symm addOppositeEquiv : (a : R⟦Γ⟧ᵃᵒᵖ) → Rᵃᵒᵖ⟦Γ⟧) x) =
    (AddOpposite.unop x).support

Tactic:
rw [← addOppositeEquiv_support, AddEquiv.apply_symm_apply]

Premises used: HahnSeries.addOppositeEquiv_support, AddEquiv.apply_symm_apply
-- Module: Mathlib.RingTheory.HahnSeries.Addition
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

Tactic:
simp only [orderTop,
    addOppositeEquiv_support]

Premises used: HahnSeries.orderTop, HahnSeries.addOppositeEquiv_support
-- Module: Mathlib.RingTheory.HahnSeries.Addition
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) (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 Γ))
⊢ 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 Γ))

Tactic:
simp only [addOppositeEquiv_apply, AddOpposite.unop_op, mk_eq_zero]

Premises used: HahnSeries.mk_eq_zero, AddOpposite.unop_op, HahnSeries.addOppositeEquiv_apply
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
x : HahnSeries.{u_1, u_3} Γ Rᵃᵒᵖ
simp_rw :
  Eq.{u_1 + 1} (α := WithTop Γ)
    (if h : ∀ (x_1 : Γ), AddOpposite.unop (x.coeff x_1) = 0 x_1 then ⊤ else (↑(⋯.min (s := x.support) ⋯) : WithTop Γ))
    (if h : ∀ (x_1 : Γ), x.coeff x_1 = coeff 0 x_1 then ⊤ else (↑(⋯.min (s := x.support) ⋯) : WithTop Γ))
⊢ 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 Γ))

Tactic:
simp_rw [HahnSeries.ext_iff, funext_iff]

Premises used: funext_iff, HahnSeries.ext_iff
-- Module: Mathlib.RingTheory.HahnSeries.Addition
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 : ∀ (x_1 : Γ), AddOpposite.unop (x.coeff x_1) = 0 x_1 then ⊤ else (↑(⋯.min (s := x.support) ⋯) : WithTop Γ))
    (if h : ∀ (x_1 : Γ), x.coeff x_1 = coeff 0 x_1 then ⊤ else (↑(⋯.min (s := x.support) ⋯) : WithTop Γ))

Tactic:
simp only [Pi.zero_apply, AddOpposite.unop_eq_zero_iff, coeff_zero]

Premises used: Pi.zero_apply, AddOpposite.unop_eq_zero_iff, HahnSeries.coeff_zero
-- Module: Mathlib.RingTheory.HahnSeries.Addition
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 Γ))
simp₂ :
  Eq.{u_1 + 1} (α := WithTop Γ)
    (if h : ∀ (x_1 : Γ), AddOpposite.unop (x.coeff x_1) = 0 x_1 then ⊤ else (↑(⋯.min (s := x.support) ⋯) : WithTop Γ))
    (if h : ∀ (x_1 : Γ), x.coeff x_1 = coeff 0 x_1 then ⊤ else (↑(⋯.min (s := x.support) ⋯) : WithTop Γ))
⊢ orderTop.{u_1, u_3} (R := R) (AddOpposite.unop ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) x)) = x.orderTop

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]

Premises used: HahnSeries.orderTop, HahnSeries.addOppositeEquiv_support, funext_iff, Pi.zero_apply, AddOpposite.unop_eq_zero_iff, HahnSeries.mk_eq_zero, AddOpposite.unop_op, HahnSeries.ext_iff, HahnSeries.coeff_zero, HahnSeries.addOppositeEquiv_apply
-- Module: Mathlib.RingTheory.HahnSeries.Addition
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
rw₁ rw₂ : (AddOpposite.unop x).orderTop = (AddOpposite.unop x).orderTop
⊢ orderTop.{u_1, u_3} (R := Rᵃᵒᵖ) ((AddEquiv.symm addOppositeEquiv : (a : R⟦Γ⟧ᵃᵒᵖ) → Rᵃᵒᵖ⟦Γ⟧) x) =
    (AddOpposite.unop x).orderTop

Tactic:
rw [← addOppositeEquiv_orderTop, AddEquiv.apply_symm_apply]

Premises used: AddEquiv.apply_symm_apply, HahnSeries.addOppositeEquiv_orderTop
-- Module: Mathlib.RingTheory.HahnSeries.Addition
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 :
  ∀ (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

Tactic:
obtain rfl | hx := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
⊢ 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:
simp
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
x : HahnSeries.{u_1, u_3} Γ Rᵃᵒᵖ
hx : x ≠ 0
inr :
  coeff (AddOpposite.unop ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) x)) (x.orderTop.untop ⋯) =
    AddOpposite.unop (x.coeff (x.orderTop.untop ⋯))
⊢ leadingCoeff.{u_1, u_3} (Γ := Γ) (AddOpposite.unop ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) x)) =
    AddOpposite.unop x.leadingCoeff

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]

Premises used: AddOpposite.unop_eq_zero_iff, ne_eq, HahnSeries.addOppositeEquiv_orderTop, not_false_eq_true, EmbeddingLike.map_eq_zero_iff, HahnSeries.leadingCoeff_of_ne_zero
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
x : HahnSeries.{u_1, u_3} Γ Rᵃᵒᵖ
hx : x ≠ 0
⊢ coeff (AddOpposite.unop ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) x)) (x.orderTop.untop ⋯) =
    AddOpposite.unop (x.coeff (x.orderTop.untop ⋯))

Tactic:
simp [addOppositeEquiv]

Premises used: HahnSeries.addOppositeEquiv
-- Module: Mathlib.RingTheory.HahnSeries.Addition
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
inr₂ :
  ∀ (hx : x ≠ 0),
    coeff (AddOpposite.unop ((addOppositeEquiv : (a : Rᵃᵒᵖ⟦Γ⟧) → R⟦Γ⟧ᵃᵒᵖ) x)) (x.orderTop.untop ⋯) =
      AddOpposite.unop (x.coeff (x.orderTop.untop ⋯))
⊢ 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]

Premises used: AddOpposite.unop_eq_zero_iff, ne_eq, HahnSeries.addOppositeEquiv_orderTop, eq_or_ne, OfNat.ofNat, HahnSeries.addOppositeEquiv, not_false_eq_true, rfl, EmbeddingLike.map_eq_zero_iff, HahnSeries.leadingCoeff_of_ne_zero
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
Γ : Type u_1
R : Type u_3
inst : PartialOrder Γ
inst_1 : AddMonoid R
x : R⟦Γ⟧ᵃᵒᵖ
a :
  AddOpposite.unop (leadingCoeff.{u_1, u_3} (Γ := Γ) ((AddEquiv.symm addOppositeEquiv : (a : R⟦Γ⟧ᵃᵒᵖ) → Rᵃᵒᵖ⟦Γ⟧) x)) =
    AddOpposite.unop (AddOpposite.op (AddOpposite.unop x).leadingCoeff)
⊢ leadingCoeff.{u_1, u_3} (Γ := Γ) ((AddEquiv.symm addOppositeEquiv : (a : R⟦Γ⟧ᵃᵒᵖ) → Rᵃᵒᵖ⟦Γ⟧) x) =
    AddOpposite.op (AddOpposite.unop x).leadingCoeff

Tactic:
apply AddOpposite.unop_injective

Premises used: AddOpposite.unop_injective
-- Module: Mathlib.RingTheory.HahnSeries.Addition
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)
a₂ a₃ : (AddOpposite.unop x).leadingCoeff = (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)

Tactic:
rw [← addOppositeEquiv_leadingCoeff, AddEquiv.apply_symm_apply, AddOpposite.unop_op]

Premises used: AddEquiv.apply_symm_apply, HahnSeries.addOppositeEquiv_leadingCoeff, AddOpposite.unop_op
-- Module: Mathlib.RingTheory.HahnSeries.Addition
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
rw : ⋯.min (s := x.support ∪ y.support) ⋯ ≤ ⋯.min (s := (x + y).support) ⋯
⊢ min (⋯.min (s := x.support) ⋯) (⋯.min (s := y.support) ⋯) ≤ ⋯.min (s := (x + y).support) ⋯

Tactic:
rw [← Set.IsWF.min_union]

Premises used: Set.IsWF.min_union
-- Module: Mathlib.RingTheory.HahnSeries.Addition
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 (s := x.support ∪ y.support) ⋯ ≤ ⋯.min (s := (x + y).support) ⋯

Tactic:
Set.IsWF.min_le_min_of_subset (support_add_subset (x := x) (y := y))

Premises used: Set.IsWF.min_le_min_of_subset, HahnSeries.support_add_subset
-- Module: Mathlib.RingTheory.HahnSeries.Addition
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 (s := x.support ∪ y.support) ⋯ ≤ ⋯.min (s := (x + y).support) ⋯

Tactic:
exact Set.IsWF.min_le_min_of_subset (support_add_subset (x := x) (y := y))

Premises used: Set.IsWF.min_le_min_of_subset, HahnSeries.support_add_subset
-- Module: Mathlib.RingTheory.HahnSeries.Addition
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
neg : ∀ (hx : ¬x = 0), min x.orderTop y.orderTop ≤ (x + y).orderTop
⊢ min x.orderTop y.orderTop ≤ (x + y).orderTop

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.RingTheory.HahnSeries.Addition
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

Tactic:
simp [hx]
-- Module: Mathlib.RingTheory.HahnSeries.Addition
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
neg : ∀ (hy : ¬y = 0), min x.orderTop y.orderTop ≤ (x + y).orderTop
⊢ min x.orderTop y.orderTop ≤ (x + y).orderTop

Tactic:
by_cases hy : y = 0
-- Module: Mathlib.RingTheory.HahnSeries.Addition
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

Tactic:
simp [hy]
-- Module: Mathlib.RingTheory.HahnSeries.Addition
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
neg : ∀ (hxy : ¬x + y = 0), min x.orderTop y.orderTop ≤ (x + y).orderTop
⊢ min x.orderTop y.orderTop ≤ (x + y).orderTop

Tactic:
by_cases hxy : x + y = 0
-- Module: Mathlib.RingTheory.HahnSeries.Addition
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

Tactic:
simp [hxy]
-- Module: Mathlib.RingTheory.HahnSeries.Addition
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
neg : min (⋯.min (s := x.support) ⋯) (⋯.min (s := y.support) ⋯) ≤ ⋯.min (s := (x + y).support) ⋯
⊢ min x.orderTop y.orderTop ≤ (x + y).orderTop

Tactic:
rw [orderTop_of_ne_zero hx, orderTop_of_ne_zero hy, orderTop_of_ne_zero hxy, ← WithTop.coe_min,
    WithTop.coe_le_coe]

Premises used: HahnSeries.orderTop_of_ne_zero, WithTop.coe_le_coe, WithTop.coe_min
-- Module: Mathlib.RingTheory.HahnSeries.Addition
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) ⋯

Tactic:
HahnSeries.min_le_min_add hx hy hxy

Premises used: HahnSeries.min_le_min_add
-- Module: Mathlib.RingTheory.HahnSeries.Addition
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) ⋯

Tactic:
exact HahnSeries.min_le_min_add hx hy hxy

Premises used: HahnSeries.min_le_min_add
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : Zero Γ
inst_2 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x + y ≠ 0
pos : ∀ (hx : x = 0), min x.order y.order ≤ (x + y).order
neg : ∀ (hx : ¬x = 0), min x.order y.order ≤ (x + y).order
⊢ min x.order y.order ≤ (x + y).order

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.RingTheory.HahnSeries.Addition
Goal:
R : Type u_3
inst : AddMonoid R
Γ : Type u_8
inst_1 : Zero Γ
inst_2 : LinearOrder Γ
x y : R⟦Γ⟧
hxy : x + y ≠ 0
hx : x = 0
⊢ min x.order y.order ≤ (x + y).order

Tactic:
simp [hx]