awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : a < succ b ↔ a ≤ b
⊢ succ a ≤ succ b ↔ a ≤ b
have rw₁ : a ≤ b ↔ a ≤ b
Tactic: rw [succ_le_iff_of_not_isMax ha, lt_succ_iff_of_not_isMax hb]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ Ico a (succ b) = Icc a b
have rw : Ici a ∩ Iio (succ b) = Icc a b
Tactic: rw [← Ici_inter_Iio, Iio_succ_of_not_isMax hb, Ici_inter_Iic]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
hb : ¬IsMax b
rw : Ici a ∩ Iio (succ b) = Icc a b
⊢ Ico a (succ b) = Icc a b
have rw₁ : Ici a ∩ Iic b = Icc a b
Tactic: rw [← Ici_inter_Iio, Iio_succ_of_not_isMax hb, Ici_inter_Iic]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
hb : ¬IsMax b
rw : Ici a ∩ Iio (succ b) = Icc a b
rw₁ : Ici a ∩ Iic b = Icc a b
⊢ Ico a (succ b) = Icc a b
have rw₂ : Icc a b = Icc a b
Tactic: rw [← Ici_inter_Iio, Iio_succ_of_not_isMax hb, Ici_inter_Iic]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ Ioo a (succ b) = Ioc a b
have rw : Ioi a ∩ Iio (succ b) = Ioc a b
Tactic: rw [← Ioi_inter_Iio, Iio_succ_of_not_isMax hb, Ioi_inter_Iic]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
hb : ¬IsMax b
rw : Ioi a ∩ Iio (succ b) = Ioc a b
⊢ Ioo a (succ b) = Ioc a b
have rw₁ : Ioi a ∩ Iic b = Ioc a b
Tactic: rw [← Ioi_inter_Iio, Iio_succ_of_not_isMax hb, Ioi_inter_Iic]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
hb : ¬IsMax b
rw : Ioi a ∩ Iio (succ b) = Ioc a b
rw₁ : Ioi a ∩ Iic b = Ioc a b
⊢ Ioo a (succ b) = Ioc a b
have rw₂ : Ioc a b = Ioc a b
Tactic: rw [← Ioi_inter_Iio, Iio_succ_of_not_isMax hb, Ioi_inter_Iic]
-- 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 ≤ succ b ∧ ¬succ a < succ b ↔ a = b
Tactic: rw [eq_iff_le_not_lt, eq_iff_le_not_lt, succ_le_succ_iff_of_not_isMax ha hb,
    succ_lt_succ_iff_of_not_isMax ha hb]
-- 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 ≤ succ b ∧ ¬succ a < succ b ↔ a = b
⊢ succ a = succ b ↔ a = b
have rw₁ : succ a ≤ succ b ∧ ¬succ a < succ b ↔ a ≤ b ∧ ¬a < b
Tactic: rw [eq_iff_le_not_lt, eq_iff_le_not_lt, succ_le_succ_iff_of_not_isMax ha hb,
    succ_lt_succ_iff_of_not_isMax ha hb]
-- 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 ≤ succ b ∧ ¬succ a < succ b ↔ a = b
rw₁ : succ a ≤ succ b ∧ ¬succ a < succ b ↔ a ≤ b ∧ ¬a < b
⊢ succ a = succ b ↔ a = b
have rw₂ : a ≤ b ∧ ¬succ a < succ b ↔ a ≤ b ∧ ¬a < b
Tactic: rw [eq_iff_le_not_lt, eq_iff_le_not_lt, succ_le_succ_iff_of_not_isMax ha hb,
    succ_lt_succ_iff_of_not_isMax ha hb]
-- 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 ≤ succ b ∧ ¬succ a < succ b ↔ a = b
rw₁ : succ a ≤ succ b ∧ ¬succ a < succ b ↔ a ≤ b ∧ ¬a < b
rw₂ : a ≤ b ∧ ¬succ a < succ b ↔ a ≤ b ∧ ¬a < b
⊢ succ a = succ b ↔ a = b
have rw₃ : a ≤ b ∧ ¬a < b ↔ a ≤ b ∧ ¬a < b
Tactic: rw [eq_iff_le_not_lt, eq_iff_le_not_lt, succ_le_succ_iff_of_not_isMax ha hb,
    succ_lt_succ_iff_of_not_isMax ha hb]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
⊢ a ≤ succ b ↔ a = succ b ∨ a ≤ b
have pos : ∀ (hb : IsMax b), a ≤ succ b ↔ a = succ b ∨ a ≤ b
Tactic: by_cases hb : IsMax b
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
pos : ∀ (hb : IsMax b), a ≤ succ b ↔ a = succ b ∨ a ≤ b
⊢ a ≤ succ b ↔ a = succ b ∨ a ≤ b
have neg : ∀ (hb : ¬IsMax b), a ≤ succ b ↔ a = succ b ∨ a ≤ b
Tactic: by_cases hb : IsMax b
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
hb : IsMax b
⊢ a ≤ succ b ↔ a = succ b ∨ a ≤ b
have pos : a ≤ b ↔ a = b ∨ a ≤ b
Tactic: rw [hb.succ_eq, or_iff_right_of_imp le_of_eq]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
hb : IsMax b
pos : a ≤ b ↔ a = b ∨ a ≤ b
⊢ a ≤ succ b ↔ a = succ b ∨ a ≤ b
have pos₁ : a ≤ b ↔ a ≤ b
Tactic: rw [hb.succ_eq, or_iff_right_of_imp le_of_eq]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
hb : ¬IsMax b
⊢ a ≤ succ b ↔ a = succ b ∨ a ≤ b
have neg : a ≤ succ b ↔ a = succ b ∨ a < succ b
Tactic: rw [← lt_succ_iff_of_not_isMax hb, le_iff_eq_or_lt]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
hb : ¬IsMax b
neg : a ≤ succ b ↔ a = succ b ∨ a < succ b
⊢ a ≤ succ b ↔ a = succ b ∨ a ≤ b
have neg₁ : a = succ b ∨ a < succ b ↔ a = succ b ∨ a < succ b
Tactic: rw [← lt_succ_iff_of_not_isMax hb, le_iff_eq_or_lt]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : Nontrivial α
a : α
⊢ ¬IsMin (succ a)
have inl : ∀ (ha : a = succ a), ¬IsMin (succ a)
Tactic: obtain ha | ha := (le_succ a).eq_or_lt
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : Nontrivial α
a : α
inl : ∀ (ha : a = succ a), ¬IsMin (succ a)
⊢ ¬IsMin (succ a)
have inr : ∀ (ha : a < succ a), ¬IsMin (succ a)
Tactic: obtain ha | ha := (le_succ a).eq_or_lt
-- 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
⊢ Icc a (succ b) = insert (succ b) (Icc a b)
have simp_rw : Ici a ∩ Iic (succ b) = insert (succ b) (Ici a ∩ Iic b)
Tactic: simp_rw [← Ici_inter_Iic, Iic_succ, inter_insert_of_mem (mem_Ici.2 h)]
-- 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
simp_rw : Ici a ∩ Iic (succ b) = insert (succ b) (Ici a ∩ Iic b)
⊢ Icc a (succ b) = insert (succ b) (Icc a b)
have simp_rw₁ : Ici a ∩ insert (succ b) (Iic b) = insert (succ b) (Ici a ∩ Iic b)
Tactic: simp_rw [← Ici_inter_Iic, Iic_succ, inter_insert_of_mem (mem_Ici.2 h)]
-- 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
⊢ Ioc a (succ b) = insert (succ b) (Ioc a b)
have simp_rw : Ioi a ∩ Iic (succ b) = insert (succ b) (Ioi a ∩ Iic b)
Tactic: simp_rw [← Ioi_inter_Iic, Iic_succ, inter_insert_of_mem (mem_Ioi.2 h)]
-- 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
simp_rw : Ioi a ∩ Iic (succ b) = insert (succ b) (Ioi a ∩ Iic b)
⊢ Ioc a (succ b) = insert (succ b) (Ioc a b)
have simp_rw₁ : Ioi a ∩ insert (succ b) (Iic b) = insert (succ b) (Ioi a ∩ Iic b)
Tactic: simp_rw [← Ioi_inter_Iic, Iic_succ, inter_insert_of_mem (mem_Ioi.2 h)]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
h₁ : a ≤ b
h₂ : ¬IsMax b
⊢ Ico a (succ b) = insert b (Ico a b)
have simp_rw : Iio (succ b) ∩ Ici a = insert b (Iio b ∩ Ici a)
Tactic: simp_rw [← Iio_inter_Ici, Iio_succ_eq_insert_of_not_isMax h₂, insert_inter_of_mem (mem_Ici.2 h₁)]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
h₁ : a ≤ b
h₂ : ¬IsMax b
simp_rw : Iio (succ b) ∩ Ici a = insert b (Iio b ∩ Ici a)
⊢ Ico a (succ b) = insert b (Ico a b)
have simp_rw₁ : insert b (Iio b) ∩ Ici a = insert b (Iio b ∩ Ici a)
Tactic: simp_rw [← Iio_inter_Ici, Iio_succ_eq_insert_of_not_isMax h₂, insert_inter_of_mem (mem_Ici.2 h₁)]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
h₁ : a < b
h₂ : ¬IsMax b
⊢ Ioo a (succ b) = insert b (Ioo a b)
have simp_rw : Iio (succ b) ∩ Ioi a = insert b (Iio b ∩ Ioi a)
Tactic: simp_rw [← Iio_inter_Ioi, Iio_succ_eq_insert_of_not_isMax h₂, insert_inter_of_mem (mem_Ioi.2 h₁)]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
h₁ : a < b
h₂ : ¬IsMax b
simp_rw : Iio (succ b) ∩ Ioi a = insert b (Iio b ∩ Ioi a)
⊢ Ioo a (succ b) = insert b (Ioo a b)
have simp_rw₁ : insert b (Iio b) ∩ Ioi a = insert b (Iio b ∩ Ioi a)
Tactic: simp_rw [← Iio_inter_Ioi, Iio_succ_eq_insert_of_not_isMax h₂, insert_inter_of_mem (mem_Ioi.2 h₁)]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
inst_2 : NoMaxOrder α
⊢ a < succ b ↔ b = a ∨ a < b
have rw : a < succ b ↔ a = b ∨ a < b
Tactic: rw [eq_comm, lt_succ_iff_eq_or_lt]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
inst_2 : NoMaxOrder α
rw : a < succ b ↔ a = b ∨ a < b
⊢ a < succ b ↔ b = a ∨ a < b
have rw₁ : a = b ∨ a < b ↔ a = b ∨ a < b
Tactic: rw [eq_comm, lt_succ_iff_eq_or_lt]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
inst_2 : NoMaxOrder α
⊢ Ioo a b = ∅ ↔ b ≤ succ a
have refine_1 : ∀ (h : Ioo a b = ∅), b ≤ succ a
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
inst_2 : NoMaxOrder α
refine_1 : ∀ (h : Ioo a b = ∅), b ≤ succ a
⊢ Ioo a b = ∅ ↔ b ≤ succ a
have refine_2 : ∀ (h : b ≤ succ a), Ioo a b = ∅
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
inst_2 : NoMaxOrder α
h : Ioo a b = ∅
⊢ b ≤ succ a
have refine_1 : ∀ (h : succ a < b), (Ioo a b).Nonempty
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
inst_2 : NoMaxOrder α
h : b ≤ succ a
⊢ Ioo a b = ∅
have refine_2 : ∀ (x : α), x ∈ Ioo a b ↔ Membership.mem (γ := Set α) ∅ x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
inst_2 : NoMaxOrder α
h : b ≤ succ a
x : α
⊢ x ∈ Ioo a b ↔ Membership.mem (γ := Set α) ∅ x
have refine_2 : a < x → b ≤ x
Tactic: suffices a < x → b ≤ x by simpa
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a : α
inst_2 : OrderBot α
inst_3 : NoMaxOrder α
⊢ a < succ ⊥ ↔ a = ⊥
have rw : a ≤ ⊥ ↔ a = ⊥
Tactic: rw [lt_succ_iff, le_bot_iff]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a : α
inst_2 : OrderBot α
inst_3 : NoMaxOrder α
rw : a ≤ ⊥ ↔ a = ⊥
⊢ a < succ ⊥ ↔ a = ⊥
have rw₁ : a = ⊥ ↔ a = ⊥
Tactic: rw [lt_succ_iff, le_bot_iff]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a : α
inst_2 : OrderBot α
⊢ a ≤ succ ⊥ ↔ a = ⊥ ∨ a = succ ⊥
have rw : a = succ ⊥ ∨ a ≤ ⊥ ↔ a = ⊥ ∨ a = succ ⊥
Tactic: rw [le_succ_iff_eq_or_le, le_bot_iff, or_comm]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a : α
inst_2 : OrderBot α
rw : a = succ ⊥ ∨ a ≤ ⊥ ↔ a = ⊥ ∨ a = succ ⊥
⊢ a ≤ succ ⊥ ↔ a = ⊥ ∨ a = succ ⊥
have rw₁ : a = succ ⊥ ∨ a = ⊥ ↔ a = ⊥ ∨ a = succ ⊥
Tactic: rw [le_succ_iff_eq_or_le, le_bot_iff, or_comm]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a : α
inst_2 : OrderBot α
rw : a = succ ⊥ ∨ a ≤ ⊥ ↔ a = ⊥ ∨ a = succ ⊥
rw₁ : a = succ ⊥ ∨ a = ⊥ ↔ a = ⊥ ∨ a = succ ⊥
⊢ a ≤ succ ⊥ ↔ a = ⊥ ∨ a = succ ⊥
have rw₂ : a = ⊥ ∨ a = succ ⊥ ↔ a = ⊥ ∨ a = succ ⊥
Tactic: rw [le_succ_iff_eq_or_le, le_bot_iff, or_comm]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
h₀ h₁ : SuccOrder α
⊢ h₀ = h₁
have succ : ∀ (a : α), @SuccOrder.succ _ PartialOrder.toPreorder _ a = @SuccOrder.succ _ PartialOrder.toPreorder _ a
Tactic: ext a
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
h₀ h₁ : SuccOrder α
a : α
⊢ @SuccOrder.succ _ PartialOrder.toPreorder _ a = @SuccOrder.succ _ PartialOrder.toPreorder _ a
have pos : ∀ (ha : IsMax a), @SuccOrder.succ _ PartialOrder.toPreorder _ a = @SuccOrder.succ _ PartialOrder.toPreorder _ a
Tactic: by_cases ha : IsMax a
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
h₀ h₁ : SuccOrder α
a : α
pos : ∀ (ha : IsMax a), @SuccOrder.succ _ PartialOrder.toPreorder _ a = @SuccOrder.succ _ PartialOrder.toPreorder _ a
⊢ @SuccOrder.succ _ PartialOrder.toPreorder _ a = @SuccOrder.succ _ PartialOrder.toPreorder _ a
have neg : ∀ (ha : ¬IsMax a), @SuccOrder.succ _ PartialOrder.toPreorder _ a = @SuccOrder.succ _ PartialOrder.toPreorder _ a
Tactic: by_cases ha : IsMax a
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : SuccOrder α
a : α
⊢ succ a = sInf (Ioi a)
have apply : sInf (Ioi a) ≤ succ a
Tactic: apply (le_sInf fun b => succ_le_of_lt).antisymm
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : SuccOrder α
a : α
⊢ sInf (Ioi a) ≤ succ a
have inl : LE.le.{u_1} (α := α) (sInf (Ioi ⊤)) (succ ⊤)
Tactic: obtain rfl | ha := eq_or_ne a ⊤
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : SuccOrder α
a : α
inl : LE.le.{u_1} (α := α) (sInf (Ioi ⊤)) (succ ⊤)
⊢ sInf (Ioi a) ≤ succ a
have inr : ∀ (ha : a ≠ ⊤), sInf (Ioi a) ≤ succ a
Tactic: obtain rfl | ha := eq_or_ne a ⊤
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : SuccOrder α
⊢ LE.le.{u_1} (α := α) (sInf (Ioi ⊤)) (succ ⊤)
have inl : LE.le.{u_1} (α := α) (sInf (Ioi ⊤)) ⊤
Tactic: rw [succ_top]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : SuccOrder α
a : α
⊢ succ a = ⨅ (b : α), ⨅ (_ : b > a), b
have rw : sInf (Ioi a) = ⨅ (b : α), ⨅ (_ : b > a), b
Tactic: rw [succ_eq_sInf, iInf_subtype', iInf, Subtype.range_coe_subtype, Ioi]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : SuccOrder α
a : α
rw : sInf (Ioi a) = ⨅ (b : α), ⨅ (_ : b > a), b
⊢ succ a = ⨅ (b : α), ⨅ (_ : b > a), b
have rw₁ : sInf (Ioi a) = ⨅ (x : { b : α // b > a }), (↑x : α)
Tactic: rw [succ_eq_sInf, iInf_subtype', iInf, Subtype.range_coe_subtype, Ioi]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : SuccOrder α
a : α
rw : sInf (Ioi a) = ⨅ (b : α), ⨅ (_ : b > a), b
rw₁ : sInf (Ioi a) = ⨅ (x : { b : α // b > a }), (↑x : α)
⊢ succ a = ⨅ (b : α), ⨅ (_ : b > a), b
have rw₂ : sInf (Ioi a) = sInf (range fun (x : { b : α // b > a }) ↦ (↑x : α))
Tactic: rw [succ_eq_sInf, iInf_subtype', iInf, Subtype.range_coe_subtype, Ioi]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : SuccOrder α
a : α
rw : sInf (Ioi a) = ⨅ (b : α), ⨅ (_ : b > a), b
rw₁ : sInf (Ioi a) = ⨅ (x : { b : α // b > a }), (↑x : α)
rw₂ : sInf (Ioi a) = sInf (range fun (x : { b : α // b > a }) ↦ (↑x : α))
⊢ succ a = ⨅ (b : α), ⨅ (_ : b > a), b
have rw₃ : sInf (Ioi a) = sInf {x : α | x > a}
Tactic: rw [succ_eq_sInf, iInf_subtype', iInf, Subtype.range_coe_subtype, Ioi]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : SuccOrder α
a : α
rw : sInf (Ioi a) = ⨅ (b : α), ⨅ (_ : b > a), b
rw₁ : sInf (Ioi a) = ⨅ (x : { b : α // b > a }), (↑x : α)
rw₂ : sInf (Ioi a) = sInf (range fun (x : { b : α // b > a }) ↦ (↑x : α))
rw₃ : sInf (Ioi a) = sInf {x : α | x > a}
⊢ succ a = ⨅ (b : α), ⨅ (_ : b > a), b
have rw₄ : Eq.{u_1 + 1} (α := α) (sInf {x : α | a < x}) (sInf {x : α | x > a})
Tactic: rw [succ_eq_sInf, iInf_subtype', iInf, Subtype.range_coe_subtype, Ioi]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
inst_1 : SuccOrder α
inst_2 : NoMaxOrder α
a : α
⊢ succ a = sInf (Ioi a)
have apply : sInf (Ioi a) ≤ succ a
Tactic: apply (le_csInf nonempty_Ioi fun b => succ_le_of_lt).antisymm
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (hypothesis)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
i : α
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
have hin₁ : ¬IsMax (succ^[n] i)
Tactic: rw [Nat.succ_sub_succ_eq_sub, Nat.sub_zero] at hin
Cleared hypotheses: hin
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
i : α
n : ℕ
hn : ∀ (hin : ¬IsMax (succ^[n - 1] i)), pred^[n] (succ^[n] i) = i
hin : ¬IsMax (succ^[n] i)
⊢ ¬IsMax (succ^[n - 1] i)
have zero : ∀ (hn : ∀ (hin : ¬IsMax (succ^[HSub.hSub (α := ℕ) 0 1] i)), pred^[0] (succ^[0] i) = i) (hin : ¬IsMax (succ^[0] i)),
  ¬IsMax (succ^[HSub.hSub (α := ℕ) 0 1] i)
Tactic: rcases n with - | n
Cleared hypotheses: n, hn, hin
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
i : α
n : ℕ
hn : ∀ (hin : ¬IsMax (succ^[n - 1] i)), pred^[n] (succ^[n] i) = i
hin : ¬IsMax (succ^[n] i)
zero :
  ∀ (hn : ∀ (hin : ¬IsMax (succ^[HSub.hSub (α := ℕ) 0 1] i)), pred^[0] (succ^[0] i) = i) (hin : ¬IsMax (succ^[0] i)),
    ¬IsMax (succ^[HSub.hSub (α := ℕ) 0 1] i)
⊢ ¬IsMax (succ^[n - 1] i)
have succ : ∀ (n : ℕ) (hn : ∀ (hin : ¬IsMax (succ^[n + 1 - 1] i)), pred^[n + 1] (succ^[n + 1] i) = i)
  (hin : ¬IsMax (succ^[n + 1] i)), ¬IsMax (succ^[n + 1 - 1] i)
Tactic: rcases n with - | n
Cleared hypotheses: n, hn, hin
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
i : α
n : ℕ
hn : ∀ (hin : ¬IsMax (succ^[n + 1 - 1] i)), pred^[n + 1] (succ^[n + 1] i) = i
hin : ¬IsMax (succ^[n + 1] i)
⊢ ¬IsMax (succ^[n + 1 - 1] i)
have succ : ∀ (hn : ∀ (hin : ¬IsMax (succ^[n] i)), pred^[n + 1] (succ^[n + 1] i) = i) (hin : ¬IsMax (succ^[n + 1] i)),
  ¬IsMax (succ^[n] i)
Tactic: rw [Nat.succ_sub_succ_eq_sub, Nat.sub_zero] at hn ⊢
Cleared hypotheses: hn, hin
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
i : α
n : ℕ
hn : ∀ (hin : ¬IsMax (succ^[n] i)), pred^[n + 1] (succ^[n + 1] i) = i
hin : ¬IsMax (succ^[n + 1] i)
⊢ succ^[n] i ≤ succ^[n.succ] i
have rw : succ^[n] i ≤ (succ ∘ succ^[n]) i
Tactic: rw [Function.iterate_succ']
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (hypothesis)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
i : α
n : ℕ
hn : ∀ (hin : ¬IsMax (succ^[n] i)), pred^[n + 1] (succ^[n + 1] i) = i
hin : ¬IsMax (succ^[n + 1] i)
⊢ ¬IsMax (succ^[n] i)
have h_sub_le : succ^[n] i ≤ succ^[n.succ] i
Tactic: have h_sub_le : succ^[n] i ≤ succ^[n.succ] i := by
        rw [Function.iterate_succ']
        exact le_succ _
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
i : α
n : ℕ
hn : ∀ (hin : ¬IsMax (succ^[n] i)), pred^[n + 1] (succ^[n + 1] i) = i
hin : ¬IsMax (succ^[n + 1] i)
h_sub_le : succ^[n] i ≤ succ^[n.succ] i
⊢ ¬IsMax (succ^[n] i)
have succ : ∀ (h_max : IsMax (succ^[n] i)) (j : α) (hj : succ^[n + 1] i ≤ j), j ≤ succ^[n + 1] i
Tactic: refine fun h_max => hin fun j hj => ?_
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (hypothesis)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
i : α
n : ℕ
hn : ∀ (hin : ¬IsMax (succ^[n] i)), pred^[n + 1] (succ^[n + 1] i) = i
hin : ¬IsMax (succ^[n + 1] i)
h_sub_le : succ^[n] i ≤ succ^[n.succ] i
h_max : IsMax (succ^[n] i)
j : α
hj : succ^[n + 1] i ≤ j
⊢ j ≤ succ^[n + 1] i
have hj_le : j ≤ succ^[n] i
Tactic: have hj_le : j ≤ succ^[n] i := h_max (h_sub_le.trans hj)
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (hypothesis)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
i : α
n : ℕ
hn : ∀ (hin : ¬IsMax (succ^[n - 1] i)), pred^[n] (succ^[n] i) = i
hin : ¬IsMax (succ^[n] i)
⊢ pred^[n + 1] (succ^[n + 1] i) = i
have h_not_max : ¬IsMax (succ^[n - 1] i)
Tactic: 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
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
i : α
n : ℕ
hn : ∀ (hin : ¬IsMax (succ^[n - 1] i)), pred^[n] (succ^[n] i) = i
hin : ¬IsMax (succ^[n] i)
h_not_max : ¬IsMax (succ^[n - 1] i)
⊢ pred^[n + 1] (succ^[n + 1] i) = i
have succ : (pred^[n] ∘ pred) ((succ ∘ succ^[n]) i) = i
Tactic: rw [Function.iterate_succ, Function.iterate_succ']
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
i : α
n : ℕ
hn : ∀ (hin : ¬IsMax (succ^[n - 1] i)), pred^[n] (succ^[n] i) = i
hin : ¬IsMax (succ^[n] i)
h_not_max : ¬IsMax (succ^[n - 1] i)
⊢ (pred^[n] ∘ pred) ((succ ∘ succ^[n]) i) = i
have succ : pred^[n] (pred (succ (succ^[n] i))) = i
Tactic: simp only [Function.comp_apply]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
i : α
n : ℕ
hn : ∀ (hin : ¬IsMax (succ^[n - 1] i)), pred^[n] (succ^[n] i) = i
hin : ¬IsMax (succ^[n] i)
h_not_max : ¬IsMax (succ^[n - 1] i)
⊢ pred^[n] (pred (succ (succ^[n] i))) = i
have succ : pred^[n] (succ^[n] i) = i
Tactic: rw [pred_succ_of_not_isMax hin]
-- 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)
⊢ pred^[n] (succ^[n] i) = i
have zero : ∀ (hin : ¬IsMax (succ^[HSub.hSub (α := ℕ) 0 1] i)), pred^[0] (succ^[0] 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