awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
ha :
  LE.le.{u_1} (α := WithTop α)
    (match (motive := WithTop α → WithTop α) ⊤ with
      | none => ⊤
      | Option.some a => if succ a = a then ⊤ else (↑(succ a) : WithTop α) :
      WithTop α)
    (⊤ : WithTop α)
⊢ IsMax.{u_1} (α := WithTop α) ⊤

Tactic:
isMax_top

Premises used: isMax_top
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
ha :
  LE.le.{u_1} (α := WithTop α)
    (match (motive := WithTop α → WithTop α) ⊤ with
      | none => ⊤
      | Option.some a => if succ a = a then ⊤ else (↑(succ a) : WithTop α) :
      WithTop α)
    (⊤ : WithTop α)
⊢ IsMax.{u_1} (α := WithTop α) ⊤

Tactic:
exact isMax_top

Premises used: isMax_top
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
a : α
ha : (if succ a = a then ⊤ else (↑(succ a) : WithTop α)) ≤ (↑a : WithTop α)
pos : ∀ (ha' : succ a = a) (ha : ⊤ ≤ (↑a : WithTop α)), IsMax (↑a : WithTop α)
neg : ∀ (ha' : ¬succ a = a) (ha : (↑(succ a) : WithTop α) ≤ (↑a : WithTop α)), IsMax (↑a : WithTop α)
⊢ IsMax (↑a : WithTop α)

Tactic:
split_ifs at ha with ha'
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
a : α
ha' : succ a = a
ha : ⊤ ≤ (↑a : WithTop α)
⊢ IsMax (↑a : WithTop α)

Tactic:
(not_top_le_coe _ ha).elim

Premises used: False.elim, WithTop.not_top_le_coe
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
a : α
ha' : succ a = a
ha : ⊤ ≤ (↑a : WithTop α)
⊢ IsMax (↑a : WithTop α)

Tactic:
exact (not_top_le_coe _ ha).elim

Premises used: False.elim, WithTop.not_top_le_coe
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
a : α
ha' : ¬succ a = a
ha : (↑(succ a) : WithTop α) ≤ (↑a : WithTop α)
⊢ succ a = a

Tactic:
rw [coe_le_coe, succ_le_iff_isMax, ← succ_eq_iff_isMax] at ha

Premises used: Order.succ_eq_iff_isMax, Order.succ_le_iff_isMax, WithTop.coe_le_coe
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
a : α
ha' : ¬succ a = a
ha : succ a = a
⊢ IsMax (↑a : WithTop α)

Tactic:
(ha' ha).elim

Premises used: False.elim
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
a : α
ha' : ¬succ a = a
ha : succ a = a
⊢ IsMax (↑a : WithTop α)

Tactic:
exact (ha' ha).elim

Premises used: False.elim
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
a b : WithTop α
h : a < b
top :
  ∀ (h : a < ⊤),
    LE.le (α := WithTop α)
      (match (motive := WithTop α → WithTop α) a with
        | none => ⊤
        | Option.some a => if succ a = a then ⊤ else (↑(succ a) : WithTop α) :
        WithTop α)
      (⊤ : WithTop α)
coe :
  ∀ (a_1 : α) (h : a < (↑a_1 : WithTop α)),
    (match (motive := WithTop α → WithTop α) a with
      | none => ⊤
      | Option.some a => if succ a = a then ⊤ else (↑(succ a) : WithTop α)) ≤
      (↑a_1 : WithTop α)
⊢ (match (motive := WithTop α → WithTop α) a with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else (↑(succ a) : WithTop α)) ≤
    b

Tactic:
cases b
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
a : WithTop α
h : a < ⊤
⊢ LE.le (α := WithTop α)
    (match (motive := WithTop α → WithTop α) a with
      | none => ⊤
      | Option.some a => if succ a = a then ⊤ else (↑(succ a) : WithTop α) :
      WithTop α)
    (⊤ : WithTop α)

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
a : WithTop α
h : a < ⊤
⊢ LE.le (α := WithTop α)
    (match (motive := WithTop α → WithTop α) a with
      | none => ⊤
      | Option.some a => if succ a = a then ⊤ else (↑(succ a) : WithTop α) :
      WithTop α)
    (⊤ : WithTop α)

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
a : WithTop α
a_1 : α
h : a < (↑a_1 : WithTop α)
coe :
  ∀ (h : ⊤ < (↑a_1 : WithTop α)),
    (match (motive := WithTop α → WithTop α) ⊤ with
      | none => ⊤
      | Option.some a => if succ a = a then ⊤ else (↑(succ a) : WithTop α)) ≤
      (↑a_1 : WithTop α)
coe₁ :
  ∀ (a : α) (h : (↑a : WithTop α) < (↑a_1 : WithTop α)),
    (match (motive := WithTop α → WithTop α) (↑a : WithTop α) with
      | none => ⊤
      | Option.some a => if succ a = a then ⊤ else (↑(succ a) : WithTop α)) ≤
      (↑a_1 : WithTop α)
⊢ (match (motive := WithTop α → WithTop α) a with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else (↑(succ a) : WithTop α)) ≤
    (↑a_1 : WithTop α)

Tactic:
cases a
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
a : α
h : ⊤ < (↑a : WithTop α)
⊢ (match (motive := WithTop α → WithTop α) ⊤ with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else (↑(succ a) : WithTop α)) ≤
    (↑a : WithTop α)

Tactic:
(not_top_lt h).elim

Premises used: False.elim, not_top_lt
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
a : α
h : ⊤ < (↑a : WithTop α)
⊢ (match (motive := WithTop α → WithTop α) ⊤ with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else (↑(succ a) : WithTop α)) ≤
    (↑a : WithTop α)

Tactic:
exact (not_top_lt h).elim

Premises used: False.elim, not_top_lt
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
a a_1 : α
h : (↑a_1 : WithTop α) < (↑a : WithTop α)
⊢ a_1 < a

Tactic:
rw [coe_lt_coe] at h

Premises used: WithTop.coe_lt_coe
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
a a_1 : α
h : a_1 < a
pos : ∀ (ha : succ a_1 = a_1), ⊤ ≤ (↑a : WithTop α)
neg : ∀ (ha : ¬succ a_1 = a_1), (↑(succ a_1) : WithTop α) ≤ (↑a : WithTop α)
⊢ (if succ a_1 = a_1 then ⊤ else (↑(succ a_1) : WithTop α)) ≤ (↑a : WithTop α)

Tactic:
split_ifs with ha
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
a a_1 : α
h : a_1 < a
ha : succ a_1 = a_1
⊢ IsMax a_1

Tactic:
rw [succ_eq_iff_isMax] at ha

Premises used: Order.succ_eq_iff_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
a a_1 : α
h : a_1 < a
ha : IsMax a_1
⊢ ⊤ ≤ (↑a : WithTop α)

Tactic:
(ha.not_lt h).elim

Premises used: False.elim, IsMax.not_lt
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
a a_1 : α
h : a_1 < a
ha : IsMax a_1
⊢ ⊤ ≤ (↑a : WithTop α)

Tactic:
exact (ha.not_lt h).elim

Premises used: False.elim, IsMax.not_lt
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
a a_1 : α
h : a_1 < a
ha : ¬succ a_1 = a_1
⊢ (↑(succ a_1) : WithTop α) ≤ (↑a : WithTop α)

Tactic:
coe_le_coe.2 (succ_le_of_lt h)

Premises used: Iff.mpr, Order.succ_le_of_lt, WithTop.coe_le_coe
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
a a_1 : α
h : a_1 < a
ha : ¬succ a_1 = a_1
⊢ (↑(succ a_1) : WithTop α) ≤ (↑a : WithTop α)

Tactic:
exact coe_le_coe.2 (succ_le_of_lt h)

Premises used: Iff.mpr, Order.succ_le_of_lt, WithTop.coe_le_coe
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
a : α
h : IsMax a
⊢ succ (↑a : WithTop α) = ⊤

Tactic:
dif_pos (succ_eq_iff_isMax.2 h)

Premises used: Iff.mpr, Order.succ, dif_pos, Order.succ_eq_iff_isMax, dite, ite
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
a : α
h : ¬IsMax a
⊢ succ (↑a : WithTop α) = (↑(succ a) : WithTop α)

Tactic:
dif_neg (succ_eq_iff_isMax.not.2 h)

Premises used: Iff.mpr, Order.succ, Iff.not, Order.succ_eq_iff_isMax, dif_neg, dite, ite
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
inst_3 : NoMaxOrder α
a : α
⊢ succ (↑a : WithTop α) = (↑(succ a) : WithTop α)

Tactic:
succ_coe_of_not_isMax <| not_isMax a

Premises used: not_isMax, WithTop.succ_coe_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : OrderTop α
inst_2 : PredOrder α
a : WithTop α
ha :
  a ≤
    match (motive := WithTop α → WithTop α) a with
    | none => (↑⊤ : WithTop α)
    | Option.some a => (↑(pred a) : WithTop α)
top :
  ∀
    (ha :
      LE.le.{u_1} (α := WithTop α) (⊤ : WithTop α)
        (match (motive := WithTop α → WithTop α) ⊤ with
          | none => (↑⊤ : WithTop α)
          | Option.some a => (↑(pred a) : WithTop α) :
          WithTop α)),
    IsMin.{u_1} (α := WithTop α) ⊤
coe :
  ∀ (a : α)
    (ha :
      (↑a : WithTop α) ≤
        match (motive := WithTop α → WithTop α) (↑a : WithTop α) with
        | none => (↑⊤ : WithTop α)
        | Option.some a => (↑(pred a) : WithTop α)),
    IsMin (↑a : WithTop α)
⊢ IsMin a

Tactic:
cases a
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : OrderTop α
inst_2 : PredOrder α
ha :
  LE.le.{u_1} (α := WithTop α) (⊤ : WithTop α)
    (match (motive := WithTop α → WithTop α) ⊤ with
      | none => (↑⊤ : WithTop α)
      | Option.some a => (↑(pred a) : WithTop α) :
      WithTop α)
⊢ IsMin.{u_1} (α := WithTop α) ⊤

Tactic:
((coe_lt_top (⊤ : α)).not_ge ha).elim

Premises used: WithTop.coe_lt_top, False.elim, LT.lt.not_ge, Top.top
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : OrderTop α
inst_2 : PredOrder α
ha :
  LE.le.{u_1} (α := WithTop α) (⊤ : WithTop α)
    (match (motive := WithTop α → WithTop α) ⊤ with
      | none => (↑⊤ : WithTop α)
      | Option.some a => (↑(pred a) : WithTop α) :
      WithTop α)
⊢ IsMin.{u_1} (α := WithTop α) ⊤

Tactic:
exact ((coe_lt_top (⊤ : α)).not_ge ha).elim

Premises used: WithTop.coe_lt_top, False.elim, LT.lt.not_ge, Top.top
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : OrderTop α
inst_2 : PredOrder α
a : α
ha :
  (↑a : WithTop α) ≤
    match (motive := WithTop α → WithTop α) (↑a : WithTop α) with
    | none => (↑⊤ : WithTop α)
    | Option.some a => (↑(pred a) : WithTop α)
⊢ IsMin (↑a : WithTop α)

Tactic:
(min_of_le_pred <| coe_le_coe.1 ha).withTop

Premises used: Order.min_of_le_pred, Iff.mp, WithTop.coe_le_coe, IsMin.withTop
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : OrderTop α
inst_2 : PredOrder α
a : α
ha :
  (↑a : WithTop α) ≤
    match (motive := WithTop α → WithTop α) (↑a : WithTop α) with
    | none => (↑⊤ : WithTop α)
    | Option.some a => (↑(pred a) : WithTop α)
⊢ IsMin (↑a : WithTop α)

Tactic:
exact (min_of_le_pred <| coe_le_coe.1 ha).withTop

Premises used: Order.min_of_le_pred, Iff.mp, WithTop.coe_le_coe, IsMin.withTop
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : OrderTop α
inst_2 : PredOrder α
a b : WithTop α
h : a < b
top :
  ∀ (h : ⊤ < b),
    LE.le (α := WithTop α) (⊤ : WithTop α)
      (match (motive := WithTop α → WithTop α) b with
        | none => (↑⊤ : WithTop α)
        | Option.some a => (↑(pred a) : WithTop α) :
        WithTop α)
coe :
  ∀ (a : α) (h : (↑a : WithTop α) < b),
    (↑a : WithTop α) ≤
      match (motive := WithTop α → WithTop α) b with
      | none => (↑⊤ : WithTop α)
      | Option.some a => (↑(pred a) : WithTop α)
⊢ a ≤
    match (motive := WithTop α → WithTop α) b with
    | none => (↑⊤ : WithTop α)
    | Option.some a => (↑(pred a) : WithTop α)

Tactic:
cases a
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : OrderTop α
inst_2 : PredOrder α
b : WithTop α
h : ⊤ < b
⊢ LE.le (α := WithTop α) (⊤ : WithTop α)
    (match (motive := WithTop α → WithTop α) b with
      | none => (↑⊤ : WithTop α)
      | Option.some a => (↑(pred a) : WithTop α) :
      WithTop α)

Tactic:
(le_top.not_gt h).elim

Premises used: False.elim, LE.le.not_gt, le_top
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : OrderTop α
inst_2 : PredOrder α
b : WithTop α
h : ⊤ < b
⊢ LE.le (α := WithTop α) (⊤ : WithTop α)
    (match (motive := WithTop α → WithTop α) b with
      | none => (↑⊤ : WithTop α)
      | Option.some a => (↑(pred a) : WithTop α) :
      WithTop α)

Tactic:
exact (le_top.not_gt h).elim

Premises used: False.elim, LE.le.not_gt, le_top
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : OrderTop α
inst_2 : PredOrder α
b : WithTop α
a : α
h : (↑a : WithTop α) < b
coe :
  ∀ (h : (↑a : WithTop α) < ⊤),
    (↑a : WithTop α) ≤
      match (motive := WithTop α → WithTop α) ⊤ with
      | none => (↑⊤ : WithTop α)
      | Option.some a => (↑(pred a) : WithTop α)
coe₁ :
  ∀ (a_1 : α) (h : (↑a : WithTop α) < (↑a_1 : WithTop α)),
    (↑a : WithTop α) ≤
      match (motive := WithTop α → WithTop α) (↑a_1 : WithTop α) with
      | none => (↑⊤ : WithTop α)
      | Option.some a => (↑(pred a) : WithTop α)
⊢ (↑a : WithTop α) ≤
    match (motive := WithTop α → WithTop α) b with
    | none => (↑⊤ : WithTop α)
    | Option.some a => (↑(pred a) : WithTop α)

Tactic:
cases b
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : OrderTop α
inst_2 : PredOrder α
a : α
h : (↑a : WithTop α) < ⊤
⊢ (↑a : WithTop α) ≤
    match (motive := WithTop α → WithTop α) ⊤ with
    | none => (↑⊤ : WithTop α)
    | Option.some a => (↑(pred a) : WithTop α)

Tactic:
coe_le_coe.2 le_top

Premises used: Iff.mpr, le_top, WithTop.coe_le_coe
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : OrderTop α
inst_2 : PredOrder α
a : α
h : (↑a : WithTop α) < ⊤
⊢ (↑a : WithTop α) ≤
    match (motive := WithTop α → WithTop α) ⊤ with
    | none => (↑⊤ : WithTop α)
    | Option.some a => (↑(pred a) : WithTop α)

Tactic:
exact coe_le_coe.2 le_top

Premises used: Iff.mpr, le_top, WithTop.coe_le_coe
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : OrderTop α
inst_2 : PredOrder α
a a_1 : α
h : (↑a : WithTop α) < (↑a_1 : WithTop α)
⊢ (↑a : WithTop α) ≤
    match (motive := WithTop α → WithTop α) (↑a_1 : WithTop α) with
    | none => (↑⊤ : WithTop α)
    | Option.some a => (↑(pred a) : WithTop α)

Tactic:
coe_le_coe.2 (le_pred_of_lt <| coe_lt_coe.1 h)

Premises used: Iff.mpr, Order.le_pred_of_lt, WithTop.coe_lt_coe, Iff.mp, WithTop.coe_le_coe
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : OrderTop α
inst_2 : PredOrder α
a a_1 : α
h : (↑a : WithTop α) < (↑a_1 : WithTop α)
⊢ (↑a : WithTop α) ≤
    match (motive := WithTop α → WithTop α) (↑a_1 : WithTop α) with
    | none => (↑⊤ : WithTop α)
    | Option.some a => (↑(pred a) : WithTop α)

Tactic:
exact coe_le_coe.2 (le_pred_of_lt <| coe_lt_coe.1 h)

Premises used: Iff.mpr, Order.le_pred_of_lt, WithTop.coe_lt_coe, Iff.mp, WithTop.coe_le_coe
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderTop α
inst_2 : PredOrder α
⊢ Eq.{u_1 + 1} (α := WithTop α) (pred ⊤) (↑⊤ : WithTop α)

Tactic:
rfl

Premises used: WithTop.some, rfl
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderTop α
inst_2 : PredOrder α
a : α
⊢ pred (↑a : WithTop α) = (↑(pred a) : WithTop α)

Tactic:
rfl

Premises used: WithTop.some, rfl
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : OrderTop α
inst_2 : PredOrder α
a : WithTop α
ha : a ≠ ⊤
top : ∀ (ha : Ne.{u_1 + 1} (α := WithTop α) ⊤ ⊤), Ne.{u_1 + 1} (α := WithTop α) (pred ⊤) ⊤
coe : ∀ (a : α) (ha : (↑a : WithTop α) ≠ ⊤), pred (↑a : WithTop α) ≠ ⊤
⊢ pred a ≠ ⊤

Tactic:
induction a
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : OrderTop α
inst_2 : PredOrder α
ha : Ne.{u_1 + 1} (α := WithTop α) ⊤ ⊤
⊢ Ne.{u_1 + 1} (α := WithTop α) (pred ⊤) ⊤

Tactic:
simp
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : OrderTop α
inst_2 : PredOrder α
a : α
ha : (↑a : WithTop α) ≠ ⊤
⊢ pred (↑a : WithTop α) ≠ ⊤

Tactic:
simp
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : NoMaxOrder α
hα : Nonempty α
a : PredOrder (WithTop α)
h : Eq.{u_1 + 1} (α := WithTop α) (pred ⊤) ⊤
⊢ False

Tactic:
hα.elim fun a => (min_of_le_pred h.ge).not_lt <| coe_lt_top a

Premises used: Eq.ge, WithTop.coe_lt_top, Nonempty.elim, Order.min_of_le_pred, IsMin.not_lt
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : NoMaxOrder α
hα : Nonempty α
a : PredOrder (WithTop α)
h : Eq.{u_1 + 1} (α := WithTop α) (pred ⊤) ⊤
⊢ False

Tactic:
exact hα.elim fun a => (min_of_le_pred h.ge).not_lt <| coe_lt_top a

Premises used: Eq.ge, WithTop.coe_lt_top, Nonempty.elim, Order.min_of_le_pred, IsMin.not_lt
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : NoMaxOrder α
hα : Nonempty α
a_1 : PredOrder (WithTop α)
a : α
h : pred ⊤ = (↑a : WithTop α)
coe : ∀ (c : α) (hc : a < c), False
⊢ False

Tactic:
obtain ⟨c, hc⟩ := exists_gt a

Premises used: NoMaxOrder.exists_gt
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : NoMaxOrder α
hα : Nonempty α
a_1 : PredOrder (WithTop α)
a : α
h : pred ⊤ = (↑a : WithTop α)
c : α
hc : a < c
⊢ pred ⊤ < (↑c : WithTop α)

Tactic:
rw [← coe_lt_coe, ← h] at hc

Premises used: WithTop.coe_lt_coe
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : NoMaxOrder α
hα : Nonempty α
a_1 : PredOrder (WithTop α)
a : α
h : pred ⊤ = (↑a : WithTop α)
c : α
hc : pred ⊤ < (↑c : WithTop α)
⊢ False

Tactic:
(le_pred_of_lt (coe_lt_top c)).not_gt hc

Premises used: WithTop.coe_lt_top, Order.le_pred_of_lt, LE.le.not_gt
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : NoMaxOrder α
hα : Nonempty α
a_1 : PredOrder (WithTop α)
a : α
h : pred ⊤ = (↑a : WithTop α)
c : α
hc : pred ⊤ < (↑c : WithTop α)
⊢ False

Tactic:
exact (le_pred_of_lt (coe_lt_top c)).not_gt hc

Premises used: WithTop.coe_lt_top, Order.le_pred_of_lt, LE.le.not_gt
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : NoMaxOrder α
hα : Nonempty α
a : PredOrder (WithTop α)
cases : ∀ (x : WithTop α) (h : pred ⊤ = x), False
⊢ False

Tactic:
cases h : pred (⊤ : WithTop α) with
    | top => exact hα.elim fun a => (min_of_le_pred h.ge).not_lt <| coe_lt_top a
    | coe a =>
      obtain ⟨c, hc⟩ := exists_gt a
      rw [← coe_lt_coe, ← h] at hc
      exact (le_pred_of_lt (coe_lt_top c)).not_gt hc

Premises used: WithTop.coe_lt_coe, WithTop.top, Order.pred, Top.top, WithTop.coe
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
X : Type u_3
Y : Type u_4
inst : Preorder X
inst_1 : Preorder Y
inst_2 : SuccOrder X
f : X ≃o Y
y : Y
rw : EquivLike.inv f y ≤ @succ _ inst _ ((f.symm : (a : Y) → X) y)
⊢ y ≤ (f : (a : X) → Y) (@succ _ inst _ ((f.symm : (a : Y) → X) y) : X)

Tactic:
rw [← map_inv_le_iff f]

Premises used: map_inv_le_iff
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
X : Type u_3
Y : Type u_4
inst : Preorder X
inst_1 : Preorder Y
inst_2 : SuccOrder X
f : X ≃o Y
y : Y
⊢ EquivLike.inv f y ≤ @succ _ inst _ ((f.symm : (a : Y) → X) y)

Tactic:
le_succ (f.symm y)

Premises used: OrderIso.symm, SuccOrder.le_succ, DFunLike.coe
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
X : Type u_3
Y : Type u_4
inst : Preorder X
inst_1 : Preorder Y
inst_2 : SuccOrder X
f : X ≃o Y
y : Y
⊢ EquivLike.inv f y ≤ @succ _ inst _ ((f.symm : (a : Y) → X) y)

Tactic:
exact le_succ (f.symm y)

Premises used: OrderIso.symm, SuccOrder.le_succ, DFunLike.coe
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
X : Type u_3
Y : Type u_4
inst : Preorder X
inst_1 : Preorder Y
inst_2 : SuccOrder X
f : X ≃o Y
a : Y
h : (f : (a : X) → Y) (@succ _ inst _ ((f.symm : (a : Y) → X) a) : X) ≤ a
rw : IsMax.{u_3} (α := X) ((f.symm : (a : Y) → X) a : X)
⊢ IsMax a

Tactic:
rw [← f.symm.isMax_apply]

Premises used: OrderIso.symm, OrderIso.isMax_apply
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
X : Type u_3
Y : Type u_4
inst : Preorder X
inst_1 : Preorder Y
inst_2 : SuccOrder X
f : X ≃o Y
a : Y
h : (f : (a : X) → Y) (@succ _ inst _ ((f.symm : (a : Y) → X) a) : X) ≤ a
⊢ IsMax.{u_3} (α := X) ((f.symm : (a : Y) → X) a : X)

Tactic:
max_of_succ_le ?_

Premises used: SuccOrder.max_of_succ_le
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
X : Type u_3
Y : Type u_4
inst : Preorder X
inst_1 : Preorder Y
inst_2 : SuccOrder X
f : X ≃o Y
a : Y
h : (f : (a : X) → Y) (@succ _ inst _ ((f.symm : (a : Y) → X) a) : X) ≤ a
refine : LE.le.{u_3} (α := X) (@succ _ inst _ ((f.symm : (a : Y) → X) a) : X) ((f.symm : (a : Y) → X) a : X)
⊢ IsMax.{u_3} (α := X) ((f.symm : (a : Y) → X) a : X)

Tactic:
refine max_of_succ_le ?_

Premises used: SuccOrder.max_of_succ_le
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
X : Type u_3
Y : Type u_4
inst : Preorder X
inst_1 : Preorder Y
inst_2 : SuccOrder X
f : X ≃o Y
a : Y
h : (f : (a : X) → Y) (@succ _ inst _ ((f.symm : (a : Y) → X) a) : X) ≤ a
⊢ LE.le.{u_3} (α := X) (@succ _ inst _ ((f.symm : (a : Y) → X) a) : X) ((f.symm : (a : Y) → X) a : X)

Tactic:
simp [f.le_symm_apply, h]

Premises used: OrderIso.le_symm_apply
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
X : Type u_3
Y : Type u_4
inst : Preorder X
inst_1 : Preorder Y
inst_2 : SuccOrder X
f : X ≃o Y
a b : Y
h : a < b
rw : @succ _ inst _ ((f.symm : (a : Y) → X) a) ≤ EquivLike.inv f b
⊢ (f : (a : X) → Y) (@succ _ inst _ ((f.symm : (a : Y) → X) a) : X) ≤ b

Tactic:
rw [← le_map_inv_iff]

Premises used: le_map_inv_iff
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
X : Type u_3
Y : Type u_4
inst : Preorder X
inst_1 : Preorder Y
inst_2 : SuccOrder X
f : X ≃o Y
a b : Y
h : a < b
⊢ (f.symm : (a : Y) → X) a < EquivLike.inv f b

Tactic:
simp [h]
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
X : Type u_3
Y : Type u_4
inst : Preorder X
inst_1 : Preorder Y
inst_2 : SuccOrder X
f : X ≃o Y
a b : Y
h : a < b
⊢ @succ _ inst _ ((f.symm : (a : Y) → X) a) ≤ EquivLike.inv f b

Tactic:
exact succ_le_of_lt (by simp [h])

Premises used: SuccOrder.succ_le_of_lt