awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
i : α
n : ℕ
hin : ¬IsMax (succ^[n - 1] i)
zero : ∀ (hin : ¬IsMax (succ^[HSub.hSub (α := ℕ) 0 1] i)), pred^[0] (succ^[0] i) = i
⊢ pred^[n] (succ^[n] i) = i
have succ : ∀ (n : ℕ) (hn : ∀ (hin : ¬IsMax (succ^[n - 1] i)), pred^[n] (succ^[n] i) = i) (hin : ¬IsMax (succ^[n + 1 - 1] i)),
  pred^[n + 1] (succ^[n + 1] i) = i
Tactic: induction n with
  | zero => simp only [Function.iterate_zero, id]
  | succ n hn =>
    rw [Nat.succ_sub_succ_eq_sub, Nat.sub_zero] at hin
    have h_not_max : ¬IsMax (succ^[n - 1] i) := by
      rcases n with - | n
      · simpa using hin
      rw [Nat.succ_sub_succ_eq_sub, Nat.sub_zero] at hn ⊢
      have h_sub_le : succ^[n] i ≤ succ^[n.succ] i := by
        rw [Function.iterate_succ']
        exact le_succ _
      refine fun h_max => hin fun j hj => ?_
      have hj_le : j ≤ succ^[n] i := h_max (h_sub_le.trans hj)
      exact hj_le.trans h_sub_le
    rw [Function.iterate_succ, Function.iterate_succ']
    simp only [Function.comp_apply]
    rw [pred_succ_of_not_isMax hin]
    exact hn h_not_max
Cleared hypotheses: n, hin
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
a : WithTop α
⊢ a ≤
    match (motive := WithTop α → WithTop α) a with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else (↑(succ a) : WithTop α)
have none : LE.le.{u_1} (α := WithTop α) none
  (match (motive := WithTop α → WithTop α) none with
  | none => ⊤
  | Option.some a => if succ a = a then ⊤ else (↑(succ a) : WithTop α))
Tactic: obtain - | a := a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
a : WithTop α
none :
  LE.le.{u_1} (α := WithTop α) Option.none
    (match (motive := WithTop α → WithTop α) Option.none with
    | Option.none => ⊤
    | Option.some a => if succ a = a then ⊤ else (↑(succ a) : WithTop α))
⊢ a ≤
    match (motive := WithTop α → WithTop α) a with
    | Option.none => ⊤
    | Option.some a => if succ a = a then ⊤ else (↑(succ a) : WithTop α)
have some : ∀ (a : α),
  Option.some a ≤
    match (motive := WithTop α → WithTop α) Option.some a with
    | Option.none => ⊤
    | Option.some a => if succ a = a then ⊤ else (↑(succ a) : WithTop α)
Tactic: obtain - | a := a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
a : α
⊢ Option.some a ≤ if succ a = a then ⊤ else (↑(succ a) : WithTop α)
have pos : succ a = a → Option.some a ≤ ⊤
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
a : α
pos : succ a = a → Option.some a ≤ ⊤
⊢ Option.some a ≤ if succ a = a then ⊤ else (↑(succ a) : WithTop α)
have neg : ¬succ a = a → Option.some a ≤ (↑(succ a) : WithTop α)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
a : WithTop α
ha :
  (match (motive := WithTop α → WithTop α) a with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else (↑(succ a) : WithTop α)) ≤
    a
⊢ IsMax a
have top : ∀
  (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: cases a
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : (a : α) → Decidable (succ a = a)
a : WithTop α
ha :
  (match (motive := WithTop α → WithTop α) a with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else (↑(succ a) : WithTop α)) ≤
    a
top :
  ∀
    (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 α) ⊤
⊢ IsMax a
have coe : ∀ (a : α)
  (ha :
    (match (motive := WithTop α → WithTop α) (↑a : WithTop α) with
      | none => ⊤
      | Option.some a => if succ a = a then ⊤ else (↑(succ a) : WithTop α)) ≤
      (↑a : WithTop α)),
  IsMax (↑a : WithTop α)
Tactic: cases a
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
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 α)
⊢ IsMax (↑a : WithTop α)
have pos : ∀ (ha' : succ a = a) (ha : ⊤ ≤ (↑a : WithTop α)), IsMax (↑a : WithTop α)
Tactic: split_ifs at ha with ha'
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
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 α)
⊢ IsMax (↑a : WithTop α)
have neg : ∀ (ha' : ¬succ a = a) (ha : (↑(succ a) : WithTop α) ≤ (↑a : WithTop α)), IsMax (↑a : WithTop α)
Tactic: split_ifs at ha with ha'
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (hypothesis)
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 α)
⊢ IsMax (↑a : WithTop α)
have ha₁ : succ a = a
Tactic: rw [coe_le_coe, succ_le_iff_isMax, ← succ_eq_iff_isMax] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
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
⊢ (match (motive := WithTop α → WithTop α) a with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else (↑(succ a) : WithTop α)) ≤
    b
have 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 α)
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
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 α)
⊢ (match (motive := WithTop α → WithTop α) a with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else (↑(succ a) : WithTop α)) ≤
    b
have 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 α)
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
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 α)
⊢ (match (motive := WithTop α → WithTop α) a with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else (↑(succ a) : WithTop α)) ≤
    (↑a_1 : WithTop α)
have 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 α)
Tactic: cases a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
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 α)
⊢ (match (motive := WithTop α → WithTop α) a with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else (↑(succ a) : WithTop α)) ≤
    (↑a_1 : WithTop α)
have 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 α)
Tactic: cases a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (hypothesis)
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 α)
⊢ (match (motive := WithTop α → WithTop α) (↑a_1 : WithTop α) with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else (↑(succ a) : WithTop α)) ≤
    (↑a : WithTop α)
have h₁ : a_1 < a
Tactic: rw [coe_lt_coe] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
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
⊢ (if succ a_1 = a_1 then ⊤ else (↑(succ a_1) : WithTop α)) ≤ (↑a : WithTop α)
have pos : ∀ (ha : succ a_1 = a_1), ⊤ ≤ (↑a : WithTop α)
Tactic: split_ifs with ha
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
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 α)
⊢ (if succ a_1 = a_1 then ⊤ else (↑(succ a_1) : WithTop α)) ≤ (↑a : WithTop α)
have neg : ∀ (ha : ¬succ a_1 = a_1), (↑(succ a_1) : WithTop α) ≤ (↑a : WithTop α)
Tactic: split_ifs with ha
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (hypothesis)
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
⊢ ⊤ ≤ (↑a : WithTop α)
have ha₁ : IsMax a_1
Tactic: rw [succ_eq_iff_isMax] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
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 α)
⊢ IsMin a
have 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 α) ⊤
Tactic: cases a
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
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 α) ⊤
⊢ IsMin a
have coe : ∀ (a : α)
  (ha :
    (↑a : WithTop α) ≤
      match (motive := WithTop α → WithTop α) (↑a : WithTop α) with
      | none => (↑⊤ : WithTop α)
      | Option.some a => (↑(pred a) : WithTop α)),
  IsMin (↑a : WithTop α)
Tactic: cases a
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : OrderTop α
inst_2 : PredOrder α
a b : WithTop α
h : a < b
⊢ a ≤
    match (motive := WithTop α → WithTop α) b with
    | none => (↑⊤ : WithTop α)
    | Option.some a => (↑(pred a) : WithTop α)
have top : ∀ (h : ⊤ < b),
  LE.le (α := WithTop α) (⊤ : WithTop α)
    (match (motive := WithTop α → WithTop α) b with
      | none => (↑⊤ : WithTop α)
      | Option.some a => (↑(pred a) : WithTop α) :
      WithTop α)
Tactic: cases a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
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 α)
⊢ a ≤
    match (motive := WithTop α → WithTop α) b with
    | none => (↑⊤ : WithTop α)
    | Option.some a => (↑(pred a) : WithTop α)
have coe : ∀ (a : α) (h : (↑a : WithTop α) < b),
  (↑a : WithTop α) ≤
    match (motive := WithTop α → WithTop α) b with
    | none => (↑⊤ : WithTop α)
    | Option.some a => (↑(pred a) : WithTop α)
Tactic: cases a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : OrderTop α
inst_2 : PredOrder α
b : WithTop α
a : α
h : (↑a : WithTop α) < b
⊢ (↑a : WithTop α) ≤
    match (motive := WithTop α → WithTop α) b with
    | none => (↑⊤ : WithTop α)
    | Option.some a => (↑(pred a) : WithTop α)
have coe : ∀ (h : (↑a : WithTop α) < ⊤),
  (↑a : WithTop α) ≤
    match (motive := WithTop α → WithTop α) ⊤ with
    | none => (↑⊤ : WithTop α)
    | Option.some a => (↑(pred a) : WithTop α)
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
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 α)
⊢ (↑a : WithTop α) ≤
    match (motive := WithTop α → WithTop α) b with
    | none => (↑⊤ : WithTop α)
    | Option.some a => (↑(pred a) : WithTop α)
have 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 α)
Tactic: cases b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : OrderTop α
inst_2 : PredOrder α
a : WithTop α
ha : a ≠ ⊤
⊢ pred a ≠ ⊤
have top : ∀ (ha : Ne.{u_1 + 1} (α := WithTop α) ⊤ ⊤), Ne.{u_1 + 1} (α := WithTop α) (pred ⊤) ⊤
Tactic: induction a
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
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 ⊤) ⊤
⊢ pred a ≠ ⊤
have coe : ∀ (a : α) (ha : (↑a : WithTop α) ≠ ⊤), pred (↑a : WithTop α) ≠ ⊤
Tactic: induction a
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : NoMaxOrder α
hα : Nonempty α
a_1 : PredOrder (WithTop α)
a : α
h : pred ⊤ = (↑a : WithTop α)
⊢ False
have coe : ∀ (c : α) (hc : a < c), False
Tactic: obtain ⟨c, hc⟩ := exists_gt a
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (hypothesis)
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
⊢ False
have hc₁ : pred ⊤ < (↑c : WithTop α)
Tactic: rw [← coe_lt_coe, ← h] at hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : NoMaxOrder α
hα : Nonempty α
a : PredOrder (WithTop α)
⊢ False
have cases : ∀ (x : WithTop α) (h : pred ⊤ = x), 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
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
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
⊢ y ≤ (f : (a : X) → Y) (@succ _ inst _ ((f.symm : (a : Y) → X) y) : X)
have rw : EquivLike.inv f y ≤ @succ _ inst _ ((f.symm : (a : Y) → X) y)
Tactic: rw [← map_inv_le_iff f]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
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 a
have rw : IsMax.{u_3} (α := X) ((f.symm : (a : Y) → X) a : X)
Tactic: rw [← f.symm.isMax_apply]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
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)
have refine : LE.le.{u_3} (α := X) (@succ _ inst _ ((f.symm : (a : Y) → X) a) : X) ((f.symm : (a : Y) → X) a : X)
Tactic: refine max_of_succ_le ?_
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
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 : (a : X) → Y) (@succ _ inst _ ((f.symm : (a : Y) → X) a) : X) ≤ b
have rw : @succ _ inst _ ((f.symm : (a : Y) → X) a) ≤ EquivLike.inv f b
Tactic: rw [← le_map_inv_iff]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : PredOrder α
x_1 : (↑s : Type u_3)
x : α
hx : x ∈ s
⊢ (if h : pred (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) : α) ∈ s then
      Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) : α)) h
    else Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) ≤
    Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx
have dsimp : (if h : pred x ∈ s then Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred x) h
  else Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) ≤
  Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : PredOrder α
x_1 : (↑s : Type u_3)
x : α
hx : x ∈ s
⊢ (if h : pred x ∈ s then Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred x) h
    else Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) ≤
    Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx
have isTrue : ∀ (h : pred x ∈ s), Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred x) h ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx
Tactic: split
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : PredOrder α
x_1 : (↑s : Type u_3)
x : α
hx : x ∈ s
isTrue :
  ∀ (h : pred x ∈ s), Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred x) h ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx
⊢ (if h : pred x ∈ s then Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred x) h
    else Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx) ≤
    Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx
have isFalse : pred x ∉ s → Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx
Tactic: split
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : PredOrder α
x_1 : (↑s : Type u_3)
x : α
hx : x ∈ s
h :
  Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx ≤
    if h : pred x ∈ s then Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred x) h
    else Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx
⊢ IsMin (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)
have pos : ∀ (h' : pred x ∈ s)
  (h : Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred x) h'),
  IsMin (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)
Tactic: split_ifs at h with h'
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : PredOrder α
x_1 : (↑s : Type u_3)
x : α
hx : x ∈ s
h :
  Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx ≤
    if h : pred x ∈ s then Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred x) h
    else Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx
pos :
  ∀ (h' : pred x ∈ s)
    (h : Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred x) h'),
    IsMin (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)
⊢ IsMin (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)
have neg : ∀ (h' : pred x ∉ s) (h : Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx),
  IsMin (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)
Tactic: split_ifs at h with h'
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (hypothesis)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : PredOrder α
x_1 : (↑s : Type u_3)
x : α
hx : x ∈ s
h' : pred x ∈ s
h : Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) (pred x) h'
⊢ IsMin (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)
have h₁ : IsMin x
Tactic: simp only [Subtype.mk_le_mk, Order.le_pred_iff_isMin] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : PredOrder α
x_1 : (↑s : Type u_3)
x : α
hx : x ∈ s
h' : pred x ∉ s
h_1 : Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx
y : α
hy : y ∈ s
h : Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy
have neg : ∀ (h : Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy < Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx),
  Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy
Tactic: rcases h.lt_or_eq with h | h
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α_1 : Type u_1
β : Type u_2
α : Type u_3
inst : PartialOrder α
s : Set α
inst_1 : s.OrdConnected
inst_2 : PredOrder α
x_1 : (↑s : Type u_3)
x : α
hx : x ∈ s
h' : pred x ∉ s
h_1 : Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx
y : α
hy : y ∈ s
h : Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx
neg :
  ∀ (h : Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy < Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx),
    Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy
have neg₁ : ∀ (h : Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy = Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx),
  Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) y hy
Tactic: rcases h.lt_or_eq with h | h