awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (hypothesis)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) ≤ f a
b : α
hb : b ∈ s
n : ℕ
hn : ∀ (ha : pred^[n] b ∈ s), f (pred^[n] b) ≤ f b
ha : pred (pred^[n] b) ∈ s
⊢ f (pred (pred^[n] b)) ≤ f b
have this : pred^[n] b ∈ s
Tactic: have : pred^[n] b ∈ s := hs.1 ha hb ⟨pred_le _, pred_iterate_le ..⟩
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) ≤ f a
b : α
hb : b ∈ s
n : ℕ
hn : ∀ (ha : pred^[n] b ∈ s), f (pred^[n] b) ≤ f b
ha : pred (pred^[n] b) ∈ s
this : pred^[n] b ∈ s
⊢ f (pred (pred^[n] b)) ≤ f b
have pos : ∀ (ha' : IsMin (pred^[n] b)), f (pred (pred^[n] b)) ≤ f b
Tactic: by_cases ha' : IsMin (pred^[n] b)
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) ≤ f a
b : α
hb : b ∈ s
n : ℕ
hn : ∀ (ha : pred^[n] b ∈ s), f (pred^[n] b) ≤ f b
ha : pred (pred^[n] b) ∈ s
this : pred^[n] b ∈ s
pos : ∀ (ha' : IsMin (pred^[n] b)), f (pred (pred^[n] b)) ≤ f b
⊢ f (pred (pred^[n] b)) ≤ f b
have neg : ∀ (ha' : ¬IsMin (pred^[n] b)), f (pred (pred^[n] b)) ≤ f b
Tactic: by_cases ha' : IsMin (pred^[n] b)
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) ≤ f a
b : α
hb : b ∈ s
n : ℕ
hn : ∀ (ha : pred^[n] b ∈ s), f (pred^[n] b) ≤ f b
ha : pred (pred^[n] b) ∈ s
this : pred^[n] b ∈ s
ha' : IsMin (pred^[n] b)
⊢ f (pred (pred^[n] b)) ≤ f b
have pos : f (pred^[n] b) ≤ f b
Tactic: rw [pred_eq_iff_isMin.2 ha']
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) ≤ f a
b : α
hb : b ∈ s
n : ℕ
ha : pred^[n] b ∈ s
⊢ f (pred^[n] b) ≤ f b
have zero : ∀ (ha : pred^[0] b ∈ s), f (pred^[0] b) ≤ f b
Tactic: induction n with
  | zero => simp
  | succ n hn =>
    rw [Function.iterate_succ_apply'] at ha ⊢
    have : pred^[n] b ∈ s := hs.1 ha hb ⟨pred_le _, pred_iterate_le ..⟩
    by_cases ha' : IsMin (pred^[n] b)
    · rw [pred_eq_iff_isMin.2 ha']
      exact hn this
    · exact (hn this).trans' (hf _ ha' this ha)
Cleared hypotheses: n, ha
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) ≤ f a
b : α
hb : b ∈ s
n : ℕ
ha : pred^[n] b ∈ s
zero : ∀ (ha : pred^[0] b ∈ s), f (pred^[0] b) ≤ f b
⊢ f (pred^[n] b) ≤ f b
have succ : ∀ (n : ℕ) (hn : ∀ (ha : pred^[n] b ∈ s), f (pred^[n] b) ≤ f b) (ha : pred^[n + 1] b ∈ s), f (pred^[n + 1] b) ≤ f b
Tactic: induction n with
  | zero => simp
  | succ n hn =>
    rw [Function.iterate_succ_apply'] at ha ⊢
    have : pred^[n] b ∈ s := hs.1 ha hb ⟨pred_le _, pred_iterate_le ..⟩
    by_cases ha' : IsMin (pred^[n] b)
    · rw [pred_eq_iff_isMin.2 ha']
      exact hn this
    · exact (hn this).trans' (hf _ ha' this ha)
Cleared hypotheses: n, ha
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a < b
⊢ f a < f b
have obtain : ∀ (n : ℕ) (ha : pred^[n] b ∈ s) (hab : pred^[n] b < b), f (pred^[n] b) < f b
Tactic: obtain ⟨n, rfl⟩ := exists_pred_iterate_of_le hab.le
Cleared hypotheses: a, ha, hab
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a
b : α
hb : b ∈ s
n : ℕ
ha : pred^[n] b ∈ s
hab : pred^[n] b < b
⊢ f (pred^[n] b) < f b
have zero : ∀ (ha : pred^[0] b ∈ s) (hab : pred^[0] b < b), f (pred^[0] b) < f b
Tactic: obtain _ | n := n
Cleared hypotheses: n, ha, hab
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a
b : α
hb : b ∈ s
n : ℕ
ha : pred^[n] b ∈ s
hab : pred^[n] b < b
zero : ∀ (ha : pred^[0] b ∈ s) (hab : pred^[0] b < b), f (pred^[0] b) < f b
⊢ f (pred^[n] b) < f b
have succ : ∀ (n : ℕ) (ha : pred^[n + 1] b ∈ s) (hab : pred^[n + 1] b < b), f (pred^[n + 1] b) < f b
Tactic: obtain _ | n := n
Cleared hypotheses: n, ha, hab
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (hypothesis)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a
b : α
hb : b ∈ s
n : ℕ
ha : pred^[n + 1] b ∈ s
hab : pred^[n + 1] b < b
⊢ f (pred^[n + 1] b) < f b
have hab₁ : ¬IsMin b
Tactic: apply not_isMin_of_lt at hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a
b : α
hb : b ∈ s
hab : ¬IsMin b
n : ℕ
hn : ∀ (ha : pred^[n + 1] b ∈ s), f (pred^[n + 1] b) < f b
ha : pred^[n + 1 + 1] b ∈ s
⊢ f (pred^[n + 1 + 1] b) < f b
have succ : ∀ (ha : pred (pred^[n + 1] b) ∈ s), f (pred (pred^[n + 1] b)) < f b
Tactic: rw [Function.iterate_succ_apply'] at ha ⊢
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (hypothesis)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a
b : α
hb : b ∈ s
hab : ¬IsMin b
n : ℕ
hn : ∀ (ha : pred^[n + 1] b ∈ s), f (pred^[n + 1] b) < f b
ha : pred (pred^[n + 1] b) ∈ s
⊢ f (pred (pred^[n + 1] b)) < f b
have this : pred^[n + 1] b ∈ s
Tactic: have : pred^[n + 1] b ∈ s := hs.1 ha hb ⟨pred_le _, pred_iterate_le ..⟩
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a
b : α
hb : b ∈ s
hab : ¬IsMin b
n : ℕ
hn : ∀ (ha : pred^[n + 1] b ∈ s), f (pred^[n + 1] b) < f b
ha : pred (pred^[n + 1] b) ∈ s
this : pred^[n + 1] b ∈ s
⊢ f (pred (pred^[n + 1] b)) < f b
have pos : ∀ (ha' : IsMin (pred^[n + 1] b)), f (pred (pred^[n + 1] b)) < f b
Tactic: by_cases ha' : IsMin (pred^[n + 1] b)
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a
b : α
hb : b ∈ s
hab : ¬IsMin b
n : ℕ
hn : ∀ (ha : pred^[n + 1] b ∈ s), f (pred^[n + 1] b) < f b
ha : pred (pred^[n + 1] b) ∈ s
this : pred^[n + 1] b ∈ s
pos : ∀ (ha' : IsMin (pred^[n + 1] b)), f (pred (pred^[n + 1] b)) < f b
⊢ f (pred (pred^[n + 1] b)) < f b
have neg : ∀ (ha' : ¬IsMin (pred^[n + 1] b)), f (pred (pred^[n + 1] b)) < f b
Tactic: by_cases ha' : IsMin (pred^[n + 1] b)
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a
b : α
hb : b ∈ s
hab : ¬IsMin b
n : ℕ
hn : ∀ (ha : pred^[n + 1] b ∈ s), f (pred^[n + 1] b) < f b
ha : pred (pred^[n + 1] b) ∈ s
this : pred^[n + 1] b ∈ s
ha' : IsMin (pred^[n + 1] b)
⊢ f (pred (pred^[n + 1] b)) < f b
have pos : f (pred^[n + 1] b) < f b
Tactic: rw [pred_eq_iff_isMin.2 ha']
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a
b : α
hb : b ∈ s
n : ℕ
ha : pred^[n + 1] b ∈ s
hab : ¬IsMin b
⊢ f (pred^[n + 1] b) < f b
have succ : ∀ (ha : pred^[HAdd.hAdd (α := ℕ) 0 1] b ∈ s), f (pred^[HAdd.hAdd (α := ℕ) 0 1] b) < f b
Tactic: induction n with
  | zero => simpa using hf _ hab hb ha
  | succ n hn =>
    rw [Function.iterate_succ_apply'] at ha ⊢
    have : pred^[n + 1] b ∈ s := hs.1 ha hb ⟨pred_le _, pred_iterate_le ..⟩
    by_cases ha' : IsMin (pred^[n + 1] b)
    · rw [pred_eq_iff_isMin.2 ha']
      exact hn this
    · exact (hn this).trans' (hf _ ha' this ha)
Cleared hypotheses: n, ha
-- Lean 4 proof step from Mathlib.Order.SuccPred.Archimedean (goal)
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a
b : α
hb : b ∈ s
n : ℕ
ha : pred^[n + 1] b ∈ s
hab : ¬IsMin b
succ : ∀ (ha : pred^[HAdd.hAdd (α := ℕ) 0 1] b ∈ s), f (pred^[HAdd.hAdd (α := ℕ) 0 1] b) < f b
⊢ f (pred^[n + 1] b) < f b
have succ₁ : ∀ (n : ℕ) (hn : ∀ (ha : pred^[n + 1] b ∈ s), f (pred^[n + 1] b) < f b) (ha : pred^[n + 1 + 1] b ∈ s),
  f (pred^[n + 1 + 1] b) < f b
Tactic: induction n with
  | zero => simpa using hf _ hab hb ha
  | succ n hn =>
    rw [Function.iterate_succ_apply'] at ha ⊢
    have : pred^[n + 1] b ∈ s := hs.1 ha hb ⟨pred_le _, pred_iterate_le ..⟩
    by_cases ha' : IsMin (pred^[n + 1] b)
    · rw [pred_eq_iff_isMin.2 ha']
      exact hn this
    · exact (hn this).trans' (hf _ ha' this ha)
Cleared hypotheses: n, ha
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
a : α
ha : ¬IsMax a
x : α
⊢ a < x ↔
    (fun (a : α) ↦
          (if h : (Ioi a).Nonempty then WellFounded.min (r := fun (x1 x2 : α) ↦ x1 < x2) ⋯ (Ioi a) h else a : α))
        a ≤
      x
have rw : ∀ (ha : ∃ (b : α), a < b) (x : α),
  a < x ↔
    (fun (a : α) ↦
          (if h : (Ioi a).Nonempty then WellFounded.min (r := fun (x1 x2 : α) ↦ x1 < x2) sorry (Ioi a) h else a : α))
        a ≤
      x
Tactic: rw [not_isMax_iff] at ha
Cleared hypotheses: ha, x
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
a : α
ha : ∃ (b : α), a < b
x : α
⊢ a < x ↔
    (fun (a : α) ↦
          (if h : (Ioi a).Nonempty then WellFounded.min (r := fun (x1 x2 : α) ↦ x1 < x2) ⋯ (Ioi a) h else a : α))
        a ≤
      x
have simp_rw : a < x ↔ WellFounded.min (r := fun (x1 x2 : α) ↦ x1 < x2) sorry (Ioi a) sorry ≤ x
Tactic: simp_rw [Set.Nonempty, mem_Ioi, dif_pos ha]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
h : a ≤ b
⊢ succ a ≤ succ b
have pos : ∀ (hb : IsMax b), succ a ≤ succ b
Tactic: by_cases hb : IsMax b
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
h : a ≤ b
pos : ∀ (hb : IsMax b), succ a ≤ succ b
⊢ succ a ≤ succ b
have neg : ∀ (hb : ¬IsMax b), succ a ≤ succ b
Tactic: by_cases hb : IsMax b
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
h : a ≤ b
hb : IsMax b
⊢ succ a ≤ succ b
have pos : ∀ (hba : b ≤ a), succ a ≤ succ b
Tactic: by_cases hba : b ≤ a
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
h : a ≤ b
hb : IsMax b
pos : ∀ (hba : b ≤ a), succ a ≤ succ b
⊢ succ a ≤ succ b
have neg : ∀ (hba : ¬b ≤ a), succ a ≤ succ b
Tactic: by_cases hba : b ≤ a
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
⊢ succ a ≤ succ b
have neg : a < succ b
Tactic: rw [succ_le_iff_of_not_isMax fun ha => hb <| ha.mono h]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
h : a ⩿ b
⊢ b ≤ succ a
have inl : ∀ (hab : a ⋖ b), b ≤ succ a
Tactic: obtain hab | ⟨-, hba⟩ := h.covBy_or_le_and_le
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
h : a ⩿ b
inl : ∀ (hab : a ⋖ b), b ≤ succ a
⊢ b ≤ succ a
have inr : ∀ (hba : b ≤ a), b ≤ succ a
Tactic: obtain hab | ⟨-, hba⟩ := h.covBy_or_le_and_le
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
h : a ⩿ b
hab : a ⋖ b
⊢ b ≤ succ a
have inl : ∀ (hba : ¬b ≤ succ a), False
Tactic: by_contra hba
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_lt : n < m
⊢ IsMax (succ^[n] a)
have refine : succ (succ^[n] a) ≤ succ^[m] a
Tactic: refine max_of_succ_le (le_trans ?_ h_eq.symm.le)
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_lt : n < m
⊢ succ (succ^[n] a) ≤ succ^[m] a
have rw : succ^[n.succ] a ≤ succ^[m] a
Tactic: rw [← iterate_succ_apply' succ]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_lt : n < m
⊢ succ^[n.succ] a ≤ succ^[m] a
have h_le : n + 1 ≤ m
Tactic: have h_le : n + 1 ≤ m := Nat.succ_le_of_lt h_lt
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_ne : n ≠ m
⊢ IsMax (succ^[n] a)
have inl : ∀ (h : n ≤ m), IsMax (succ^[n] a)
Tactic: rcases le_total n m with h | h
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_ne : n ≠ m
inl : ∀ (h : n ≤ m), IsMax (succ^[n] a)
⊢ IsMax (succ^[n] a)
have inr : ∀ (h : m ≤ n), IsMax (succ^[n] a)
Tactic: rcases le_total n m with h | h
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_ne : n ≠ m
h : m ≤ n
⊢ IsMax (succ^[n] a)
have inr : IsMax (succ^[m] a)
Tactic: rw [h_eq]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ Icc a b ⊆ Ico a (succ b)
have rw : Ici a ∩ Iic b ⊆ Ici a ∩ Iio (succ b)
Tactic: rw [← Ici_inter_Iio, ← Ici_inter_Iic]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ Ici a ∩ Iic b ⊆ Ici a ∩ Iio (succ b)
have h₂ : Iic b ⊆ Iio (succ b)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ Ioc a b ⊆ Ioo a (succ b)
have rw : Ioi a ∩ Iic b ⊆ Ioi a ∩ Iio (succ b)
Tactic: rw [← Ioi_inter_Iio, ← Ioi_inter_Iic]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ Ioi a ∩ Iic b ⊆ Ioi a ∩ Iio (succ b)
have h₂ : Iic b ⊆ Iio (succ b)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ Icc (succ a) b = Ioc a b
have rw : Ici (succ a) ∩ Iic b = Ioc a b
Tactic: rw [← Ici_inter_Iic, Ici_succ_of_not_isMax ha, Ioi_inter_Iic]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
ha : ¬IsMax a
rw : Ici (succ a) ∩ Iic b = Ioc a b
⊢ Icc (succ a) b = Ioc a b
have rw₁ : Ioi a ∩ Iic b = Ioc a b
Tactic: rw [← Ici_inter_Iic, Ici_succ_of_not_isMax ha, Ioi_inter_Iic]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
ha : ¬IsMax a
rw : Ici (succ a) ∩ Iic b = Ioc a b
rw₁ : Ioi a ∩ Iic b = Ioc a b
⊢ Icc (succ a) b = Ioc a b
have rw₂ : Ioc a b = Ioc a b
Tactic: rw [← Ici_inter_Iic, Ici_succ_of_not_isMax ha, Ioi_inter_Iic]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ Ico (succ a) b = Ioo a b
have rw : Ici (succ a) ∩ Iio b = Ioo a b
Tactic: rw [← Ici_inter_Iio, Ici_succ_of_not_isMax ha, Ioi_inter_Iio]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
ha : ¬IsMax a
rw : Ici (succ a) ∩ Iio b = Ioo a b
⊢ Ico (succ a) b = Ioo a b
have rw₁ : Ioi a ∩ Iio b = Ioo a b
Tactic: rw [← Ici_inter_Iio, Ici_succ_of_not_isMax ha, Ioi_inter_Iio]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
ha : ¬IsMax a
rw : Ici (succ a) ∩ Iio b = Ioo a b
rw₁ : Ioi a ∩ Iio b = Ioo a b
⊢ Ico (succ a) b = Ioo a b
have rw₂ : Ioo a b = Ioo a b
Tactic: rw [← Ici_inter_Iio, Ici_succ_of_not_isMax ha, Ioi_inter_Iio]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a b : α
⊢ a ≤ b ↔ a = b ∨ succ a ≤ b
have pos : ∀ (ha : IsMax a), a ≤ b ↔ a = b ∨ succ a ≤ b
Tactic: by_cases ha : IsMax a
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a b : α
pos : ∀ (ha : IsMax a), a ≤ b ↔ a = b ∨ succ a ≤ b
⊢ a ≤ b ↔ a = b ∨ succ a ≤ b
have neg : ∀ (ha : ¬IsMax a), a ≤ b ↔ a = b ∨ succ a ≤ b
Tactic: by_cases ha : IsMax a
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ a ≤ b ↔ a = b ∨ succ a ≤ b
have neg : a ≤ b ↔ a = b ∨ a < b
Tactic: rw [succ_le_iff_of_not_isMax ha, le_iff_eq_or_lt]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a b : α
ha : ¬IsMax a
neg : a ≤ b ↔ a = b ∨ a < b
⊢ a ≤ b ↔ a = b ∨ succ a ≤ b
have neg₁ : a = b ∨ a < b ↔ a = b ∨ a < b
Tactic: rw [succ_le_iff_of_not_isMax ha, le_iff_eq_or_lt]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a b : α
⊢ a ≤ b ↔ b = a ∨ succ a ≤ b
have rw : a ≤ b ↔ a = b ∨ succ a ≤ b
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a b : α
⊢ a ≤ b ∧ b ≤ succ a ↔ b = a ∨ b = succ a
have refine : b = a ∨ b = succ a → a ≤ b ∧ b ≤ succ a
Tactic: refine ⟨fun h ↦ or_iff_not_imp_left.2 fun hba : b ≠ a ↦
    h.2.antisymm (succ_le_of_lt <| h.1.lt_of_ne <| hba.symm), ?_⟩
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
a b : α
⊢ b ≤ succ a ∧ a ≤ b ↔ b = a ∨ b = succ a
have rw : a ≤ b ∧ b ≤ succ a ↔ b = a ∨ b = succ a
Tactic: rw [and_comm]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PartialOrder β
inst_3 : SuccOrder β
f : α ≃o β
a : α
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) (succ a) : β) (succ ((f : (a : α) → β) a) : β)
have pos : ∀ (h : IsMax a), Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) (succ a) : β) (succ ((f : (a : α) → β) a) : β)
Tactic: by_cases h : IsMax 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 : PartialOrder β
inst_3 : SuccOrder β
f : α ≃o β
a : α
pos : ∀ (h : IsMax a), Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) (succ a) : β) (succ ((f : (a : α) → β) a) : β)
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) (succ a) : β) (succ ((f : (a : α) → β) a) : β)
have neg : ∀ (h : ¬IsMax a), Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) (succ a) : β) (succ ((f : (a : α) → β) a) : β)
Tactic: by_cases h : IsMax 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 : PartialOrder β
inst_3 : SuccOrder β
f : α ≃o β
a : α
h : IsMax a
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) (succ a) : β) (succ ((f : (a : α) → β) a) : β)
have pos : Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a : β) (succ ((f : (a : α) → β) a) : β)
Tactic: rw [h.succ_eq, (f.isMax_apply.2 h).succ_eq]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PartialOrder β
inst_3 : SuccOrder β
f : α ≃o β
a : α
h : IsMax a
pos : Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a : β) (succ ((f : (a : α) → β) a) : β)
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) (succ a) : β) (succ ((f : (a : α) → β) a) : β)
have pos₁ : Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) a : β)
Tactic: rw [h.succ_eq, (f.isMax_apply.2 h).succ_eq]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : OrderTop α
⊢ Eq.{u_1 + 1} (α := α) (succ ⊤) ⊤
have rw : IsMax.{u_1} (α := α) ⊤
Tactic: rw [succ_eq_iff_isMax, isMax_iff_eq_top]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : OrderTop α
rw : IsMax.{u_1} (α := α) ⊤
⊢ Eq.{u_1 + 1} (α := α) (succ ⊤) ⊤
have rw₁ : Eq.{u_1 + 1} (α := α) ⊤ ⊤
Tactic: rw [succ_eq_iff_isMax, isMax_iff_eq_top]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
h : a < succ b
⊢ a ≤ b
have by_contra! : ∀ (nh : b < a), False
Tactic: by_contra! nh
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
ha : ¬IsMax a
hb : ¬IsMax b
⊢ succ a < succ b ↔ a < b
have rw : succ a ≤ b ↔ a < b
Tactic: rw [lt_succ_iff_of_not_isMax hb, succ_le_iff_of_not_isMax ha]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
ha : ¬IsMax a
hb : ¬IsMax b
rw : succ a ≤ b ↔ a < b
⊢ succ a < succ b ↔ a < b
have rw₁ : a < b ↔ a < b
Tactic: rw [lt_succ_iff_of_not_isMax hb, succ_le_iff_of_not_isMax ha]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
ha : ¬IsMax a
hb : ¬IsMax b
⊢ succ a ≤ succ b ↔ a ≤ b
have rw : a < succ b ↔ a ≤ b
Tactic: rw [succ_le_iff_of_not_isMax ha, lt_succ_iff_of_not_isMax hb]