awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.SuccPred.Archimedean
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
neg : ∀ (ha' : ¬IsMin (pred^[n + 1] b)), f (pred (pred^[n + 1] b)) < f b
⊢ f (pred (pred^[n + 1] b)) < f b

Tactic:
by_cases ha' : IsMin (pred^[n + 1] b)

Premises used: Nat.iterate, HAdd.hAdd, Order.pred, OfNat.ofNat, IsMin
-- Module: Mathlib.Order.SuccPred.Archimedean
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)
pos : f (pred^[n + 1] b) < f b
⊢ f (pred (pred^[n + 1] b)) < f b

Tactic:
rw [pred_eq_iff_isMin.2 ha']

Premises used: Iff.mpr, Order.pred_eq_iff_isMin
-- Module: Mathlib.Order.SuccPred.Archimedean
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^[n + 1] b) < f b

Tactic:
hn this
-- Module: Mathlib.Order.SuccPred.Archimedean
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^[n + 1] b) < f b

Tactic:
exact hn this
-- Module: Mathlib.Order.SuccPred.Archimedean
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

Tactic:
(hn this).trans' (hf _ ha' this ha)

Premises used: LT.lt.trans'
-- Module: Mathlib.Order.SuccPred.Archimedean
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

Tactic:
exact (hn this).trans' (hf _ ha' this ha)

Premises used: LT.lt.trans'
-- Module: Mathlib.Order.SuccPred.Archimedean
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
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
⊢ f (pred^[n + 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)

Premises used: Function.iterate_succ_apply', Order.succ, Nat.iterate, HAdd.hAdd, Order.pred, OfNat.ofNat, IsMin
-- Module: Mathlib.Order.SuccPred.Archimedean
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 a < f (pred a)
⊢ StrictAntiOn f s

Tactic:
strictMonoOn_of_pred_lt (β := βᵒᵈ) hs hf

Premises used: StrictAntiOn, strictMonoOn_of_pred_lt
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f (pred a) ≤ f a
⊢ ∀ (a : α),
    ¬IsMin a → Membership.mem (γ := Set α) Set.univ a → Membership.mem (γ := Set α) Set.univ (pred a) → f (pred a) ≤ f a

Tactic:
simpa using hf
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f (pred a) ≤ f a
⊢ Monotone f

Tactic:
simpa using monotoneOn_of_pred_le Set.ordConnected_univ (by simpa using hf)

Premises used: Set.ordConnected_univ, monotoneOn_of_pred_le
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f a ≤ f (pred a)
⊢ ∀ (a : α),
    ¬IsMin a → Membership.mem (γ := Set α) Set.univ a → Membership.mem (γ := Set α) Set.univ (pred a) → f a ≤ f (pred a)

Tactic:
simpa using hf
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f a ≤ f (pred a)
⊢ Antitone f

Tactic:
simpa using antitoneOn_of_le_pred Set.ordConnected_univ (by simpa using hf)

Premises used: antitoneOn_of_le_pred, Set.ordConnected_univ
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f (pred a) < f a
⊢ ∀ (a : α),
    ¬IsMin a → Membership.mem (γ := Set α) Set.univ a → Membership.mem (γ := Set α) Set.univ (pred a) → f (pred a) < f a

Tactic:
simpa using hf
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f (pred a) < f a
⊢ StrictMono f

Tactic:
simpa using strictMonoOn_of_pred_lt Set.ordConnected_univ (by simpa using hf)

Premises used: Set.ordConnected_univ, strictMonoOn_of_pred_lt
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f a < f (pred a)
⊢ ∀ (a : α),
    ¬IsMin a → Membership.mem (γ := Set α) Set.univ a → Membership.mem (γ := Set α) Set.univ (pred a) → f a < f (pred a)

Tactic:
simpa using hf
-- Module: Mathlib.Order.SuccPred.Archimedean
Goal:
α : Type u_3
β : Type u_4
inst : PartialOrder α
inst_1 : Preorder β
inst_2 : PredOrder α
inst_3 : IsPredArchimedean α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f a < f (pred a)
⊢ StrictAnti f

Tactic:
simpa using strictAntiOn_of_lt_pred Set.ordConnected_univ (by simpa using hf)

Premises used: Set.ordConnected_univ, strictAntiOn_of_lt_pred
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : SuccOrder α
⊢ ∀ (a : αᵒᵈ), comp (β := α) (⇑toDual : (a : α) → αᵒᵈ) (@SuccOrder.succ _ inst _ ∘ (⇑ofDual : (a : αᵒᵈ) → α)) a ≤ a

Tactic:
simp [SuccOrder.le_succ]

Premises used: SuccOrder.le_succ
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : SuccOrder α
a : αᵒᵈ
h : a ≤ comp (β := α) (⇑toDual : (a : α) → αᵒᵈ) (@SuccOrder.succ _ inst _ ∘ (⇑ofDual : (a : αᵒᵈ) → α)) a
⊢ IsMin a

Tactic:
apply SuccOrder.max_of_succ_le h

Premises used: SuccOrder.max_of_succ_le
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
succ : α → α
hn : ∀ {a : α}, ¬IsMax a → ∀ (b : α), a < b ↔ succ a ≤ b
hm : ∀ (a : α), IsMax a → succ a = a
a : α
h : ¬IsMax a
⊢ a < succ a

Tactic:
simpa using (hn h a).not

Premises used: Iff.not
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
succ : α → α
hn : ∀ {a : α}, ¬IsMax a → ∀ (b : α), a < b ↔ succ a ≤ b
hm : ∀ (a : α), IsMax a → succ a = a
a : α
h : ¬IsMax a
⊢ ¬succ a ≤ a

Tactic:
simpa using (hn h a).not

Premises used: Iff.not
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
a : α
ha : ¬IsMax a
x : α
rw :
  ∀ (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
⊢ 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

Tactic:
rw [not_isMax_iff] at ha

Premises used: not_isMax_iff
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
a : α
ha : ∃ (b : α), a < b
x : α
simp_rw : a < x ↔ WellFounded.min (r := fun (x1 x2 : α) ↦ x1 < x2) ⋯ (Ioi 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

Tactic:
simp_rw [Set.Nonempty, mem_Ioi, dif_pos ha]

Premises used: Set.mem_Ioi, dif_pos, Set.Nonempty
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
a : α
ha : ∃ (b : α), a < b
x : α
⊢ a < x ↔ WellFounded.min (r := fun (x1 x2 : α) ↦ x1 < x2) ⋯ (Ioi a) ⋯ ≤ x

Tactic:
⟨wellFounded_lt.min_le (s := Ioi _), lt_of_lt_of_le (wellFounded_lt.prop_min ha)⟩

Premises used: WellFounded.prop_min, WellFounded.min_le, wellFounded_lt, Iff.intro, lt_of_lt_of_le
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
a : α
ha : ∃ (b : α), a < b
x : α
⊢ a < x ↔ WellFounded.min (r := fun (x1 x2 : α) ↦ x1 < x2) ⋯ (Ioi a) ⋯ ≤ x

Tactic:
exact ⟨wellFounded_lt.min_le (s := Ioi _), lt_of_lt_of_le (wellFounded_lt.prop_min ha)⟩
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
⊢ ∀ (a : α), a ≤ succ a

Tactic:
SuccOrder.le_succ

Premises used: Order.succ, SuccOrder.le_succ
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a : α
⊢ succ a ≤ a → IsMax a

Tactic:
SuccOrder.max_of_succ_le

Premises used: Order.succ, SuccOrder.max_of_succ_le
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
⊢ a < b → succ a ≤ b

Tactic:
SuccOrder.succ_le_of_lt

Premises used: Order.succ, SuccOrder.succ_le_of_lt
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a : α
⊢ succ a ≤ a ↔ IsMax a

Tactic:
⟨max_of_succ_le, fun h => h <| le_succ _⟩

Premises used: Order.max_of_succ_le, Iff.intro, Order.le_succ
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a : α
⊢ a < succ a ↔ ¬IsMax a

Tactic:
⟨not_isMax_of_lt, fun ha => (le_succ a).lt_of_not_ge fun h => ha <| max_of_succ_le h⟩

Premises used: LE.le.lt_of_not_ge, Order.max_of_succ_le, not_isMax_of_lt, Iff.intro, Order.le_succ
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a : α
⊢ a ⩿ succ a

Tactic:
⟨le_succ a, fun _ hb => (succ_le_of_lt hb).not_gt⟩

Premises used: Order.succ_le_of_lt, LE.le.not_gt, And.intro, WCovBy, Order.le_succ
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a : α
h : ¬IsMax a
⊢ a ⋖ succ a

Tactic:
(wcovBy_succ a).covBy_of_lt <| lt_succ_of_not_isMax h

Premises used: Order.lt_succ_of_not_isMax, WCovBy.covBy_of_lt, Order.wcovBy_succ
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
hab : b ≤ a
ha : ¬IsMax a
⊢ b < succ a

Tactic:
hab.trans_lt <| lt_succ_of_not_isMax ha

Premises used: Order.lt_succ_of_not_isMax, LE.le.trans_lt
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ succ a ≤ b ↔ a < b

Tactic:
⟨(lt_succ_of_not_isMax ha).trans_le, succ_le_of_lt⟩

Premises used: Order.succ_le_of_lt, Order.lt_succ_of_not_isMax, LT.lt.trans_le, Iff.intro
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
h : a < b
hb : ¬IsMax b
⊢ succ a < succ b

Tactic:
lt_succ_of_le_of_not_isMax (succ_le_of_lt h) hb

Premises used: Order.succ_le_of_lt, Order.lt_succ_of_le_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
h : a ≤ b
pos : ∀ (hb : IsMax b), succ a ≤ succ b
neg : ∀ (hb : ¬IsMax b), succ a ≤ succ b
⊢ succ a ≤ succ b

Tactic:
by_cases hb : IsMax b

Premises used: IsMax
-- Module: Mathlib.Order.SuccPred.Basic
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
neg : ∀ (hba : ¬b ≤ a), succ a ≤ succ b
⊢ succ a ≤ succ b

Tactic:
by_cases hba : b ≤ a
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
h : a ≤ b
hb : IsMax b
hba : b ≤ a
⊢ succ a ≤ succ b

Tactic:
(hb <| hba.trans <| le_succ _).trans (le_succ _)

Premises used: Order.le_succ, LE.le.trans
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
h : a ≤ b
hb : IsMax b
hba : b ≤ a
⊢ succ a ≤ succ b

Tactic:
exact (hb <| hba.trans <| le_succ _).trans (le_succ _)

Premises used: Order.le_succ, LE.le.trans
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
h : a ≤ b
hb : IsMax b
hba : ¬b ≤ a
⊢ succ a ≤ succ b

Tactic:
succ_le_of_lt ((h.lt_of_not_ge hba).trans_le <| le_succ b)

Premises used: LE.le.lt_of_not_ge, Order.succ_le_of_lt, LT.lt.trans_le, Order.le_succ
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
h : a ≤ b
hb : IsMax b
hba : ¬b ≤ a
⊢ succ a ≤ succ b

Tactic:
exact succ_le_of_lt ((h.lt_of_not_ge hba).trans_le <| le_succ b)

Premises used: LE.le.lt_of_not_ge, Order.succ_le_of_lt, LT.lt.trans_le, Order.le_succ
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
neg : a < succ b
⊢ succ a ≤ succ b

Tactic:
rw [succ_le_iff_of_not_isMax fun ha => hb <| ha.mono h]

Premises used: Order.succ_le_iff_of_not_isMax, IsMax.mono
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
⊢ a < succ b

Tactic:
apply lt_succ_of_le_of_not_isMax h hb

Premises used: Order.lt_succ_of_le_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
⊢ Monotone.{u_1, u_1} (α := α) succ

Tactic:
fun _ _ => succ_le_succ

Premises used: Monotone, Order.succ_le_succ
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
h : a ⩿ b
inl : ∀ (hab : a ⋖ b), b ≤ succ a
inr : ∀ (hba : b ≤ a), b ≤ succ a
⊢ b ≤ succ a

Tactic:
obtain hab | ⟨-, hba⟩ := h.covBy_or_le_and_le

Premises used: WCovBy.covBy_or_le_and_le
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
h : a ⩿ b
hab : a ⋖ b
inl : ∀ (hba : ¬b ≤ succ a), False
⊢ b ≤ succ a

Tactic:
by_contra hba
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
h : a ⩿ b
hab : a ⋖ b
hba : ¬b ≤ succ a
⊢ False

Tactic:
h.2 (lt_succ_of_not_isMax hab.lt.not_isMax) <| hab.lt.succ_le.lt_of_not_ge hba

Premises used: LE.le.lt_of_not_ge, Order.lt_succ_of_not_isMax, And.right, CovBy.lt, LT.lt.succ_le, LT.lt.not_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
h : a ⩿ b
hab : a ⋖ b
hba : ¬b ≤ succ a
⊢ False

Tactic:
exact h.2 (lt_succ_of_not_isMax hab.lt.not_isMax) <| hab.lt.succ_le.lt_of_not_ge hba

Premises used: LE.le.lt_of_not_ge, Order.lt_succ_of_not_isMax, And.right, CovBy.lt, LT.lt.succ_le, LT.lt.not_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
h : a ⩿ b
hba : b ≤ a
⊢ b ≤ succ a

Tactic:
hba.trans (le_succ _)

Premises used: Order.le_succ, LE.le.trans
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
h : a ⩿ b
hba : b ≤ a
⊢ b ≤ succ a

Tactic:
exact hba.trans (le_succ _)

Premises used: Order.le_succ, LE.le.trans
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
k : ℕ
x : α
⊢ x ≤ succ^[k] x

Tactic:
id_le_iterate_of_id_le le_succ _ _

Premises used: Order.le_succ, Function.id_le_iterate_of_id_le
-- Module: Mathlib.Order.SuccPred.Basic
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)

Tactic:
max_of_succ_le (le_trans ?_ h_eq.symm.le)

Premises used: Order.max_of_succ_le, Eq.le, Eq.symm, le_trans
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_lt : n < m
refine : succ (succ^[n] a) ≤ succ^[m] a
⊢ IsMax (succ^[n] a)

Tactic:
refine max_of_succ_le (le_trans ?_ h_eq.symm.le)

Premises used: Order.max_of_succ_le, Eq.le, Eq.symm, le_trans
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_lt : n < m
rw : succ^[n.succ] a ≤ succ^[m] a
⊢ succ (succ^[n] a) ≤ succ^[m] a

Tactic:
rw [← iterate_succ_apply' succ]

Premises used: Function.iterate_succ_apply', Order.succ
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_lt : n < m
⊢ n + 1 ≤ m

Tactic:
have h_le : n + 1 ≤ m := Nat.succ_le_of_lt h_lt
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_lt : n < m
h_le : n + 1 ≤ m
⊢ succ^[n.succ] a ≤ succ^[m] a

Tactic:
Monotone.monotone_iterate_of_le_map succ_mono (le_succ a) h_le

Premises used: Monotone.monotone_iterate_of_le_map, Order.succ_mono, Order.le_succ
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a : α
n m : ℕ
h_eq : succ^[n] a = succ^[m] a
h_lt : n < m
h_le : n + 1 ≤ m
⊢ succ^[n.succ] a ≤ succ^[m] a

Tactic:
exact Monotone.monotone_iterate_of_le_map succ_mono (le_succ a) h_le

Premises used: Monotone.monotone_iterate_of_le_map, Order.succ_mono, Order.le_succ
-- Module: Mathlib.Order.SuccPred.Basic
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)
inr : ∀ (h : m ≤ n), IsMax (succ^[n] a)
⊢ IsMax (succ^[n] a)

Tactic:
rcases le_total n m with h | h

Premises used: le_total
-- Module: Mathlib.Order.SuccPred.Basic
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 : n ≤ m
⊢ IsMax (succ^[n] a)

Tactic:
isMax_iterate_succ_of_eq_of_lt h_eq (lt_of_le_of_ne h h_ne)

Premises used: Order.isMax_iterate_succ_of_eq_of_lt, lt_of_le_of_ne
-- Module: Mathlib.Order.SuccPred.Basic
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 : n ≤ m
⊢ IsMax (succ^[n] a)

Tactic:
exact isMax_iterate_succ_of_eq_of_lt h_eq (lt_of_le_of_ne h h_ne)

Premises used: Order.isMax_iterate_succ_of_eq_of_lt, lt_of_le_of_ne
-- Module: Mathlib.Order.SuccPred.Basic
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
inr : IsMax (succ^[m] a)
⊢ IsMax (succ^[n] a)

Tactic:
rw [h_eq]
-- Module: Mathlib.Order.SuccPred.Basic
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^[m] a)

Tactic:
isMax_iterate_succ_of_eq_of_lt h_eq.symm (lt_of_le_of_ne h h_ne.symm)

Premises used: Ne.symm, Order.isMax_iterate_succ_of_eq_of_lt, Eq.symm, lt_of_le_of_ne
-- Module: Mathlib.Order.SuccPred.Basic
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^[m] a)

Tactic:
exact isMax_iterate_succ_of_eq_of_lt h_eq.symm (lt_of_le_of_ne h h_ne.symm)

Premises used: Ne.symm, Order.isMax_iterate_succ_of_eq_of_lt, Eq.symm, lt_of_le_of_ne
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a : α
ha : ¬IsMax a
⊢ Iic a ⊆ Iio (succ a)

Tactic:
fun _ => (lt_succ_of_le_of_not_isMax · ha)

Premises used: Set.Mem, setOf, Set.Subset, Order.lt_succ_of_le_of_not_isMax, Set.Iio
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a : α
ha : ¬IsMax a
⊢ Ici (succ a) = Ioi a

Tactic:
Set.ext fun _ => succ_le_iff_of_not_isMax ha

Premises used: Set.ext, Order.succ_le_iff_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
hb : ¬IsMax b
rw : Ici a ∩ Iic b ⊆ Ici a ∩ Iio (succ b)
⊢ Icc a b ⊆ Ico a (succ b)

Tactic:
rw [← Ici_inter_Iio, ← Ici_inter_Iic]

Premises used: Set.Ici_inter_Iio, Set.Ici_inter_Iic
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
hb : ¬IsMax b
h₂ : Iic b ⊆ Iio (succ b)
⊢ Ici a ∩ Iic b ⊆ Ici a ∩ Iio (succ b)

Tactic:
gcongr
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ Iic b ⊆ Iio (succ b)

Tactic:
Iic_subset_Iio_succ_of_not_isMax hb

Premises used: Order.Iic_subset_Iio_succ_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ Iic b ⊆ Iio (succ b)

Tactic:
exact Iic_subset_Iio_succ_of_not_isMax hb

Premises used: Order.Iic_subset_Iio_succ_of_not_isMax
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
hb : ¬IsMax b
rw : Ioi a ∩ Iic b ⊆ Ioi a ∩ Iio (succ b)
⊢ Ioc a b ⊆ Ioo a (succ b)

Tactic:
rw [← Ioi_inter_Iio, ← Ioi_inter_Iic]

Premises used: Set.Ioi_inter_Iic, Set.Ioi_inter_Iio
-- Module: Mathlib.Order.SuccPred.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SuccOrder α
a b : α
hb : ¬IsMax b
h₂ : Iic b ⊆ Iio (succ b)
⊢ Ioi a ∩ Iic b ⊆ Ioi a ∩ Iio (succ b)

Tactic:
gcongr
-- Module: Mathlib.Order.SuccPred.Basic
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
rw₂ rw₃ : Ioc a b = Ioc a b
⊢ Icc (succ a) b = Ioc a b

Tactic:
rw [← Ici_inter_Iic, Ici_succ_of_not_isMax ha, Ioi_inter_Iic]

Premises used: Set.Ioi_inter_Iic, Order.Ici_succ_of_not_isMax, Set.Ici_inter_Iic