awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Sum.Order
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst : LE α_1
inst_1 : LE β_1
inst_2 : LE γ
inst_3 : LE α₁
inst_4 : LE α₂
inst_5 : LE β₁
inst_6 : LE β₂
inst_7 : LE γ₁
inst_8 : LE γ₂
a_1 : α_1
b_1 : β_1
c : γ
α : Type u_10
β : Type u_11
inst_9 : LE α
inst_10 : LE β
a b : β
⊢ LE.le (α := _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
      ((toLex : (a : βᵒᵈ ⊕ αᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) (inl ((toDual : (a : β) → βᵒᵈ) a)) :
        _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ))
      ((toLex : (a : βᵒᵈ ⊕ αᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) (inl ((toDual : (a : β) → βᵒᵈ) b)) :
        _root_.Lex (Sum.{u_11, u_10} βᵒᵈ αᵒᵈ)) ↔
    LE.le (α := (_root_.Lex (α ⊕ β))ᵒᵈ)
      ((toDual : (a : _root_.Lex (α ⊕ β)) → (_root_.Lex (α ⊕ β))ᵒᵈ)
          ((toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) (inr a)) :
        (_root_.Lex (α ⊕ β))ᵒᵈ)
      ((toDual : (a : _root_.Lex (α ⊕ β)) → (_root_.Lex (α ⊕ β))ᵒᵈ)
          ((toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) (inr b)) :
        (_root_.Lex (α ⊕ β))ᵒᵈ)

Tactic:
simp [toDual_le_toDual]

Premises used: OrderDual.toDual_le_toDual
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
a : α
⊢ Eq (α := _root_.Lex (Sum.{u_2, u_1} βᵒᵈ αᵒᵈ))
    ((sumLexDualAntidistrib α β : (a : (_root_.Lex (α ⊕ β))ᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ))
        ((toDual : (a : _root_.Lex (α ⊕ β)) → (_root_.Lex (α ⊕ β))ᵒᵈ) (inl a)) :
      _root_.Lex (Sum.{u_2, u_1} βᵒᵈ αᵒᵈ))
    (inr ((toDual : (a : α) → αᵒᵈ) a) : Sum.{u_2, u_1} βᵒᵈ αᵒᵈ)

Tactic:
rfl

Premises used: Sum.swap, OrderDual, rfl, Sum.elim
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
b : β
⊢ Eq (α := _root_.Lex (Sum.{u_2, u_1} βᵒᵈ αᵒᵈ))
    ((sumLexDualAntidistrib α β : (a : (_root_.Lex (α ⊕ β))ᵒᵈ) → _root_.Lex (βᵒᵈ ⊕ αᵒᵈ))
        ((toDual : (a : _root_.Lex (α ⊕ β)) → (_root_.Lex (α ⊕ β))ᵒᵈ) (inr b)) :
      _root_.Lex (Sum.{u_2, u_1} βᵒᵈ αᵒᵈ))
    (inl ((toDual : (a : β) → βᵒᵈ) b) : Sum.{u_2, u_1} βᵒᵈ αᵒᵈ)

Tactic:
rfl

Premises used: Sum.swap, OrderDual, rfl, Sum.elim
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
b : β
⊢ Eq (α := (_root_.Lex (α ⊕ β))ᵒᵈ)
    ((symm (sumLexDualAntidistrib α β) : (a : _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) → (_root_.Lex (α ⊕ β))ᵒᵈ)
        (inl ((toDual : (a : β) → βᵒᵈ) b)) :
      (_root_.Lex (α ⊕ β))ᵒᵈ)
    ((toDual : (a : α ⊕ β) → (α ⊕ β)ᵒᵈ) (inr b) : (α ⊕ β)ᵒᵈ)

Tactic:
rfl

Premises used: Sum.swap, rfl, Sum.elim
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
a : α
⊢ Eq (α := (_root_.Lex (α ⊕ β))ᵒᵈ)
    ((symm (sumLexDualAntidistrib α β) : (a : _root_.Lex (βᵒᵈ ⊕ αᵒᵈ)) → (_root_.Lex (α ⊕ β))ᵒᵈ)
        (inr ((toDual : (a : α) → αᵒᵈ) a)) :
      (_root_.Lex (α ⊕ β))ᵒᵈ)
    ((toDual : (a : α ⊕ β) → (α ⊕ β)ᵒᵈ) (inl a) : (α ⊕ β)ᵒᵈ)

Tactic:
rfl

Premises used: Sum.swap, rfl, Sum.elim
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
inst_2 : IsEmpty β
x : α
⊢ (sumLexEmpty : (a : _root_.Lex (α ⊕ β)) → α)
      ((toLex : (a : α ⊕ β) → _root_.Lex (α ⊕ β)) (inl x) : _root_.Lex (α ⊕ β)) =
    x

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
inst : LE α
inst_1 : LE β
inst_2 : IsEmpty β
x : α
⊢ (emptySumLex : (a : _root_.Lex (β ⊕ α)) → α)
      ((toLex : (a : β ⊕ α) → _root_.Lex (β ⊕ α)) (inr x) : _root_.Lex (β ⊕ α)) =
    x

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
a b : WithBot α
simp :
  Sum.Lex (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True) (fun (x1 x2 : α) ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) a, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) b, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    a ≤ b
⊢ LE.le (α := _root_.Lex (PUnit ⊕ α))
      (((Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit).trans toLex) :
            (a : WithBot α) → _root_.Lex (PUnit ⊕ α))
          a :
        _root_.Lex (PUnit ⊕ α))
      (((Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit).trans toLex) :
            (a : WithBot α) → _root_.Lex (PUnit ⊕ α))
          b :
        _root_.Lex (PUnit ⊕ α)) ↔
    a ≤ b

Tactic:
simp only [Equiv.optionEquivSumPUnit, Option.elim, Equiv.trans_apply, Equiv.coe_fn_mk,
      Equiv.sumComm_apply, swap, Lex.toLex_le_toLex, le_refl]

Premises used: Sum.swap, le_refl, Equiv.trans_apply, Sum.Lex.toLex_le_toLex, Equiv.optionEquivSumPUnit, Equiv.coe_fn_mk, Equiv.sumComm_apply, Option.elim
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
a b : WithBot α
bot :
  Sum.Lex (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True) (fun (x1 x2 : α) ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊥, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) b, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    ⊥ ≤ b
coe :
  ∀ (a : α),
    Sum.Lex (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True) (fun (x1 x2 : α) ↦ x1 ≤ x2)
        (Sum.elim inr inl
          (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a : WithBot α), inr PUnit.unit,
            inl with
          | Option.some x, x_1, f => f x
          | none, y, x => y))
        (Sum.elim inr inl
          (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) b, inr PUnit.unit, inl with
          | Option.some x, x_1, f => f x
          | none, y, x => y)) ↔
      (↑a : WithBot α) ≤ b
⊢ Sum.Lex (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True) (fun (x1 x2 : α) ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) a, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) b, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    a ≤ b

Tactic:
cases a
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
b : WithBot α
bot :
  Sum.Lex (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True) (fun (x1 x2 : α) ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊥, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊥, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    LE.le.{u_1} (α := WithBot α) ⊥ ⊥
bot₁ :
  ∀ (a : α),
    Sum.Lex (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True) (fun (x1 x2 : α) ↦ x1 ≤ x2)
        (Sum.elim inr inl
          (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊥, inr PUnit.unit, inl with
          | Option.some x, x_1, f => f x
          | none, y, x => y))
        (Sum.elim inr inl
          (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a : WithBot α), inr PUnit.unit,
            inl with
          | Option.some x, x_1, f => f x
          | none, y, x => y)) ↔
      ⊥ ≤ (↑a : WithBot α)
⊢ Sum.Lex (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True) (fun (x1 x2 : α) ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊥, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) b, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    ⊥ ≤ b

Tactic:
cases b
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
b : WithBot α
a : α
coe :
  Sum.Lex (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True) (fun (x1 x2 : α) ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a : WithBot α), inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊥, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    (↑a : WithBot α) ≤ ⊥
coe₁ :
  ∀ (a_1 : α),
    Sum.Lex (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True) (fun (x1 x2 : α) ↦ x1 ≤ x2)
        (Sum.elim inr inl
          (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a : WithBot α), inr PUnit.unit,
            inl with
          | Option.some x, x_1, f => f x
          | none, y, x => y))
        (Sum.elim inr inl
          (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a_1 : WithBot α), inr PUnit.unit,
            inl with
          | Option.some x, x_1, f => f x
          | none, y, x => y)) ↔
      (↑a : WithBot α) ≤ (↑a_1 : WithBot α)
⊢ Sum.Lex (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True) (fun (x1 x2 : α) ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a : WithBot α), inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) b, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    (↑a : WithBot α) ≤ b

Tactic:
cases b
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
⊢ Sum.Lex (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True) (fun (x1 x2 : α) ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊥, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊥, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    LE.le.{u_1} (α := WithBot α) ⊥ ⊥

Tactic:
simp only [elim_inr, lex_inl_inl, bot_le]

Premises used: Sum.lex_inl_inl, Sum.elim_inr, bot_le
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
a : α
⊢ Sum.Lex (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True) (fun (x1 x2 : α) ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊥, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a : WithBot α), inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    ⊥ ≤ (↑a : WithBot α)

Tactic:
simp only [elim_inr, elim_inl, Lex.sep, bot_le]

Premises used: Sum.elim_inr, Sum.Lex.sep, Sum.elim_inl, bot_le
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
a : α
coe : ¬(↑a : WithBot α) ≤ ⊥
⊢ Sum.Lex (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True) (fun (x1 x2 : α) ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a : WithBot α), inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊥, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    (↑a : WithBot α) ≤ ⊥

Tactic:
simp only [elim_inl, elim_inr, lex_inr_inl, false_iff]

Premises used: Sum.lex_inr_inl, false_iff, Sum.elim_inr, Sum.elim_inl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
a : α
⊢ ¬(↑a : WithBot α) ≤ ⊥

Tactic:
not_coe_le_bot _

Premises used: WithBot.not_coe_le_bot
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
a : α
⊢ ¬(↑a : WithBot α) ≤ ⊥

Tactic:
exact not_coe_le_bot _

Premises used: WithBot.not_coe_le_bot
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
a a_1 : α
⊢ Sum.Lex (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True) (fun (x1 x2 : α) ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a : WithBot α), inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a_1 : WithBot α), inr PUnit.unit,
          inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    (↑a : WithBot α) ≤ (↑a_1 : WithBot α)

Tactic:
simp only [elim_inl, lex_inr_inr, coe_le_coe]

Premises used: WithBot.coe_le_coe, Sum.elim_inl, Sum.lex_inr_inr
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
inst : LE α
⊢ Eq (α := _root_.Lex (PUnit ⊕ α))
    ((orderIsoPUnitSumLex : (a : WithBot α) → _root_.Lex (PUnit ⊕ α)) ⊥ : _root_.Lex (PUnit ⊕ α))
    ((toLex : (a : PUnit ⊕ α) → _root_.Lex (PUnit ⊕ α)) (inl PUnit.unit) : _root_.Lex (PUnit ⊕ α))

Tactic:
rfl

Premises used: Sum.swap, rfl, Sum.elim
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
inst : LE α
a : α
⊢ Eq (α := _root_.Lex (PUnit ⊕ α))
    ((orderIsoPUnitSumLex : (a : WithBot α) → _root_.Lex (PUnit ⊕ α)) (↑a : WithBot α) : _root_.Lex (PUnit ⊕ α))
    ((toLex : (a : PUnit ⊕ α) → _root_.Lex (PUnit ⊕ α)) (inr a) : _root_.Lex (PUnit ⊕ α))

Tactic:
rfl

Premises used: Sum.swap, rfl, Sum.elim
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
inst : LE α
x : PUnit
⊢ Eq.{u_1 + 1} (α := WithBot α)
    ((OrderIso.symm orderIsoPUnitSumLex : (a : _root_.Lex (PUnit ⊕ α)) → WithBot α)
        ((toLex : (a : PUnit ⊕ α) → _root_.Lex (PUnit ⊕ α)) (inl x)) :
      WithBot α)
    (⊥ : WithBot α)

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
inst : LE α
a : α
⊢ (OrderIso.symm orderIsoPUnitSumLex : (a : _root_.Lex (PUnit ⊕ α)) → WithBot α)
      ((toLex : (a : PUnit ⊕ α) → _root_.Lex (PUnit ⊕ α)) (inr a)) =
    (↑a : WithBot α)

Tactic:
rfl

Premises used: WithBot.some, rfl, Sum.elim
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
a b : WithTop α
simp :
  Sum.Lex (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) a, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) b, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    a ≤ b
⊢ LE.le (α := _root_.Lex (α ⊕ PUnit))
      (((Equiv.optionEquivSumPUnit α).trans toLex : (a : WithTop α) → _root_.Lex (α ⊕ PUnit)) a :
        _root_.Lex (α ⊕ PUnit))
      (((Equiv.optionEquivSumPUnit α).trans toLex : (a : WithTop α) → _root_.Lex (α ⊕ PUnit)) b :
        _root_.Lex (α ⊕ PUnit)) ↔
    a ≤ b

Tactic:
simp only [Equiv.optionEquivSumPUnit, Option.elim, Equiv.trans_apply, Equiv.coe_fn_mk,
      Lex.toLex_le_toLex, le_refl]

Premises used: le_refl, Equiv.trans_apply, Sum.Lex.toLex_le_toLex, Equiv.optionEquivSumPUnit, Equiv.coe_fn_mk, Option.elim
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
a b : WithTop α
top :
  Sum.Lex (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊤, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) b, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    ⊤ ≤ b
coe :
  ∀ (a : α),
    Sum.Lex (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True)
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a : WithTop α), inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) b, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y) ↔
      (↑a : WithTop α) ≤ b
⊢ Sum.Lex (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) a, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) b, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    a ≤ b

Tactic:
cases a
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
b : WithTop α
top :
  Sum.Lex (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊤, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊤, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    LE.le.{u_1} (α := WithTop α) ⊤ ⊤
top₁ :
  ∀ (a : α),
    Sum.Lex (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True)
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊤, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a : WithTop α), inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y) ↔
      ⊤ ≤ (↑a : WithTop α)
⊢ Sum.Lex (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊤, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) b, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    ⊤ ≤ b

Tactic:
cases b
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
b : WithTop α
a : α
coe :
  Sum.Lex (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a : WithTop α), inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊤, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    (↑a : WithTop α) ≤ ⊤
coe₁ :
  ∀ (a_1 : α),
    Sum.Lex (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True)
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a : WithTop α), inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)
        (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a_1 : WithTop α), inr PUnit.unit,
          inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y) ↔
      (↑a : WithTop α) ≤ (↑a_1 : WithTop α)
⊢ Sum.Lex (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a : WithTop α), inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) b, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    (↑a : WithTop α) ≤ b

Tactic:
cases b
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
⊢ Sum.Lex (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊤, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊤, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    LE.le.{u_1} (α := WithTop α) ⊤ ⊤

Tactic:
simp only [lex_inr_inr, le_top]

Premises used: le_top, Sum.lex_inr_inr
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
a : α
top : ¬⊤ ≤ (↑a : WithTop α)
⊢ Sum.Lex (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊤, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a : WithTop α), inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    ⊤ ≤ (↑a : WithTop α)

Tactic:
simp only [lex_inr_inl, false_iff]

Premises used: Sum.lex_inr_inl, false_iff
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
a : α
⊢ ¬⊤ ≤ (↑a : WithTop α)

Tactic:
not_top_le_coe _

Premises used: WithTop.not_top_le_coe
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
a : α
⊢ ¬⊤ ≤ (↑a : WithTop α)

Tactic:
exact not_top_le_coe _

Premises used: WithTop.not_top_le_coe
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
a : α
⊢ Sum.Lex (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a : WithTop α), inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) ⊤, inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    (↑a : WithTop α) ≤ ⊤

Tactic:
simp only [Lex.sep, le_top]

Premises used: Sum.Lex.sep, le_top
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : LE α
a a_1 : α
⊢ Sum.Lex (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : PUnit.{u_4 + 1}) ↦ True)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a : WithTop α), inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y)
      (match (motive := Option α → α ⊕ PUnit → (α → α ⊕ PUnit) → α ⊕ PUnit) (↑a_1 : WithTop α), inr PUnit.unit, inl with
      | Option.some x, x_1, f => f x
      | none, y, x => y) ↔
    (↑a : WithTop α) ≤ (↑a_1 : WithTop α)

Tactic:
simp only [lex_inl_inl, coe_le_coe]

Premises used: Sum.lex_inl_inl, WithTop.coe_le_coe
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
inst : LE α
⊢ Eq (α := _root_.Lex (α ⊕ PUnit))
    ((orderIsoSumLexPUnit : (a : WithTop α) → _root_.Lex (α ⊕ PUnit)) ⊤ : _root_.Lex (α ⊕ PUnit))
    ((toLex : (a : α ⊕ PUnit) → _root_.Lex (α ⊕ PUnit)) (inr PUnit.unit) : _root_.Lex (α ⊕ PUnit))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
inst : LE α
a : α
⊢ Eq (α := _root_.Lex (α ⊕ PUnit))
    ((orderIsoSumLexPUnit : (a : WithTop α) → _root_.Lex (α ⊕ PUnit)) (↑a : WithTop α) : _root_.Lex (α ⊕ PUnit))
    ((toLex : (a : α ⊕ PUnit) → _root_.Lex (α ⊕ PUnit)) (inl a) : _root_.Lex (α ⊕ PUnit))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Sum.Order
Goal:
α : Type u_1
inst : LE α
x : PUnit
⊢ Eq.{u_1 + 1} (α := WithTop α)
    ((OrderIso.symm orderIsoSumLexPUnit : (a : _root_.Lex (α ⊕ PUnit)) → WithTop α)
        ((toLex : (a : α ⊕ PUnit) → _root_.Lex (α ⊕ PUnit)) (inr x)) :
      WithTop α)
    (⊤ : WithTop α)

Tactic:
rfl

Premises used: rfl, Sum.elim