awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.SuccPred.CompleteLinearOrder (hypothesis)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : SuccOrder α
x : α
⊢ ⨆ (a : (↑(Iio x) : Type u_2)), succ (↑a : α) = x
have H : BddAbove.{u_2} (α := α) (range fun (a : (↑(Iio x) : Type u_2)) ↦ succ (↑a : α))
Tactic: have H : BddAbove (range fun a : Iio x ↦ succ a.1) :=
    ⟨succ x, by simp +contextual [upperBounds, succ_le_succ, le_of_lt]⟩
-- Lean 4 proof step from Mathlib.Order.SuccPred.CompleteLinearOrder (goal)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : SuccOrder α
x : α
H : BddAbove.{u_2} (α := α) (range fun (a : (↑(Iio x) : Type u_2)) ↦ succ (↑a : α))
⊢ ⨆ (a : (↑(Iio x) : Type u_2)), succ (↑a : α) = x
have apply : ⨆ (a : (↑(Iio x) : Type u_2)), succ (↑a : α) ≤ x
Tactic: apply le_antisymm _ (le_of_forall_lt fun y hy ↦ ?_)
-- Lean 4 proof step from Mathlib.Order.SuccPred.CompleteLinearOrder (goal)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : SuccOrder α
x : α
H : BddAbove.{u_2} (α := α) (range fun (a : (↑(Iio x) : Type u_2)) ↦ succ (↑a : α))
apply : ⨆ (a : (↑(Iio x) : Type u_2)), succ (↑a : α) ≤ x
⊢ ⨆ (a : (↑(Iio x) : Type u_2)), succ (↑a : α) = x
have apply₁ : ∀ (y : α) (hy : y < x), y < ⨆ (a : (↑(Iio x) : Type u_2)), succ (↑a : α)
Tactic: apply le_antisymm _ (le_of_forall_lt fun y hy ↦ ?_)
-- Lean 4 proof step from Mathlib.Order.SuccPred.CompleteLinearOrder (goal)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : SuccOrder α
x : α
H : BddAbove.{u_2} (α := α) (range fun (a : (↑(Iio x) : Type u_2)) ↦ succ (↑a : α))
⊢ ⨆ (a : (↑(Iio x) : Type u_2)), succ (↑a : α) ≤ x
have rw : ∀ (i : (↑(Iio x) : Type u_2)), succ (↑i : α) ≤ x
Tactic: rw [ciSup_le_iff' H]
-- Lean 4 proof step from Mathlib.Order.SuccPred.CompleteLinearOrder (goal)
Goal:
α : Type u_2
inst : ConditionallyCompleteLinearOrderBot α
inst_1 : SuccOrder α
x : α
H : BddAbove.{u_2} (α := α) (range fun (a : (↑(Iio x) : Type u_2)) ↦ succ (↑a : α))
y : α
hy : y < x
⊢ y < ⨆ (a : (↑(Iio x) : Type u_2)), succ (↑a : α)
have rw : ∃ (i : (↑(Iio x) : Type u_2)), y < succ (↑i : α)
Tactic: rw [lt_ciSup_iff' H]
-- Lean 4 proof step from Mathlib.Order.SuccPred.CompleteLinearOrder (goal)
Goal:
α : Type u_2
inst : CompleteLinearOrder α
s : Set α
hlim : ¬IsSuccPrelimit (sSup s)
⊢ sSup s ∈ s
have obtain : ∀ (y : α) (hy : y ⋖ sSup s), sSup s ∈ s
Tactic: obtain ⟨y, hy⟩ := not_forall_not.mp hlim
-- Lean 4 proof step from Mathlib.Order.SuccPred.CompleteLinearOrder (goal)
Goal:
α : Type u_2
inst : CompleteLinearOrder α
s : Set α
hlim : ¬IsSuccPrelimit (sSup s)
y : α
hy : y ⋖ sSup s
⊢ sSup s ∈ s
have obtain : ∀ (i : α) (his : i ∈ s) (hi : y < i), sSup s ∈ s
Tactic: obtain ⟨i, his, hi⟩ := lt_sSup_iff.mp hy.lt
-- Lean 4 proof step from Mathlib.Order.SuccPred.CompleteLinearOrder (goal)
Goal:
α : Type u_2
inst : CompleteLinearOrder α
s : Set α
hlim : ¬IsPredPrelimit (sInf s)
⊢ sInf s ∈ s
have obtain : ∀ (y : α) (hy : sInf s ⋖ y), sInf s ∈ s
Tactic: obtain ⟨y, hy⟩ := not_forall_not.mp hlim
-- Lean 4 proof step from Mathlib.Order.SuccPred.CompleteLinearOrder (goal)
Goal:
α : Type u_2
inst : CompleteLinearOrder α
s : Set α
hlim : ¬IsPredPrelimit (sInf s)
y : α
hy : sInf s ⋖ y
⊢ sInf s ∈ s
have obtain : ∀ (i : α) (his : i ∈ s) (hi : i < y), sInf s ∈ s
Tactic: obtain ⟨i, his, hi⟩ := sInf_lt_iff.mp hy.lt
-- Lean 4 proof step from Mathlib.Order.SuccPred.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
inst : PartialOrder α
inst_1 : PartialOrder β
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
⊢ IsSuccPrelimit.{u_2} (α := β) ((f : (a : α) → β) a : β) ↔ IsSuccPrelimit a
have mp : IsSuccPrelimit.{u_2} (α := β) ((f : (a : α) → β) a : β) → IsSuccPrelimit a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.SuccPred.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
inst : PartialOrder α
inst_1 : PartialOrder β
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
mp : IsSuccPrelimit.{u_2} (α := β) ((f : (a : α) → β) a : β) → IsSuccPrelimit a
⊢ IsSuccPrelimit.{u_2} (α := β) ((f : (a : α) → β) a : β) ↔ IsSuccPrelimit a
have mpr : IsSuccPrelimit a → IsSuccPrelimit.{u_2} (α := β) ((f : (a : α) → β) a : β)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.SuccPred.InitialSeg (hypothesis)
Goal:
α : Type u_1
β : Type u_2
a : α
inst : PartialOrder α
inst_1 : PartialOrder β
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
h : IsSuccPrelimit.{u_2} (α := β) ((f : (a : α) → β) a : β)
b : α
hb : b ⋖ a
⊢ False
have hb₁ : CovBy.{u_2} (α := β) ((f : (a : α) → β) b : β) ((f : (a : α) → β) a : β)
Tactic: rw [← f.apply_covBy_apply_iff] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Order.SuccPred.InitialSeg (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
inst : PartialOrder α
inst_1 : PartialOrder β
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
h : IsSuccPrelimit a
b : β
hb : b ⋖ (f : (a : α) → β) a
⊢ False
have mpr : ∀ (c : α) (hb : CovBy.{u_2} (α := β) ((f : (a : α) → β) c : β) ((f : (a : α) → β) a : β)), False
Tactic: obtain ⟨c, rfl⟩ := f.mem_range_of_rel hb.lt
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Order.SuccPred.InitialSeg (hypothesis)
Goal:
α : Type u_1
β : Type u_2
a : α
inst : PartialOrder α
inst_1 : PartialOrder β
f : (fun (x1 x2 : α) ↦ x1 < x2) ≼i fun (x1 x2 : β) ↦ x1 < x2
h : IsSuccPrelimit a
c : α
hb : CovBy.{u_2} (α := β) ((f : (a : α) → β) c : β) ((f : (a : α) → β) a : β)
⊢ False
have hb₁ : c ⋖ a
Tactic: rw [f.apply_covBy_apply_iff] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Order.SuccPred.IntervalSucc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : LinearOrder β
f : α → β
a : α
hf : ∀ i ∈ Ici a, f a ≤ f i
h2f : ¬BddAbove (f '' Ici a)
⊢ ⋃ i ∈ Ici a, Ico (f i) (f (succ i)) = Ici (f a)
have apply : Ici (f a) ⊆ ⋃ i ∈ Ici a, Ico (f i) (f (succ i))
Tactic: apply subset_antisymm <|
    iUnion₂_subset fun i hi ↦ Ico_subset_Ico_left (hf i hi) |>.trans Ico_subset_Ici_self
-- Lean 4 proof step from Mathlib.Order.SuccPred.IntervalSucc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : LinearOrder β
f : α → β
a : α
hf : ∀ i ∈ Ici a, f a ≤ f i
h2f : ¬BddAbove (f '' Ici a)
b : β
hb : b ∈ Ici (f a)
⊢ Membership.mem (γ := Set β) (⋃ i ∈ Ici a, Ico (f i) (f (succ i))) b
have contrapose : ∀ (h2f : b ∉ ⋃ i ∈ Ici a, Ico (f i) (f (succ i))), BddAbove (f '' Ici a)
Tactic: contrapose h2f
Cleared hypotheses: h2f
-- Lean 4 proof step from Mathlib.Order.SuccPred.IntervalSucc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : LinearOrder β
f : α → β
a : α
hf : ∀ i ∈ Ici a, f a ≤ f i
b : β
hb : b ∈ Ici (f a)
h2f : b ∉ ⋃ i ∈ Ici a, Ico (f i) (f (succ i))
⊢ BddAbove (f '' Ici a)
have h : b ∈ upperBounds (f '' Ici a)
Tactic: use b
-- Lean 4 proof step from Mathlib.Order.SuccPred.IntervalSucc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : LinearOrder β
f : α → β
a : α
hf : ∀ i ∈ Ici a, f a ≤ f i
b : β
hb : b ∈ Ici (f a)
h2f : b ∉ ⋃ i ∈ Ici a, Ico (f i) (f (succ i))
⊢ b ∈ upperBounds (f '' Ici a)
have h : Membership.mem (γ := Set β) {x : β | ∀ a_1 ∈ Ici a, f a_1 ≤ x} b
Tactic: simp only [upperBounds, mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
-- Lean 4 proof step from Mathlib.Order.SuccPred.IntervalSucc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : LinearOrder β
f : α → β
a : α
hf : ∀ i ∈ Ici a, f a ≤ f i
h2f : ¬BddAbove (f '' Ici a)
⊢ ⋃ i ∈ Ici a, Ioc (f i) (f (succ i)) = Ioi (f a)
have apply : Ioi (f a) ⊆ ⋃ i ∈ Ici a, Ioc (f i) (f (succ i))
Tactic: apply subset_antisymm <|
    iUnion₂_subset fun i hi ↦ Ioc_subset_Ioc_left (hf i hi) |>.trans Ioc_subset_Ioi_self
-- Lean 4 proof step from Mathlib.Order.SuccPred.IntervalSucc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : LinearOrder β
f : α → β
a : α
hf : ∀ i ∈ Ici a, f a ≤ f i
h2f : ¬BddAbove (f '' Ici a)
b : β
hb : b ∈ Ioi (f a)
⊢ Membership.mem (γ := Set β) (⋃ i ∈ Ici a, Ioc (f i) (f (succ i))) b
have contrapose : ∀ (h2f : b ∉ ⋃ i ∈ Ici a, Ioc (f i) (f (succ i))), BddAbove (f '' Ici a)
Tactic: contrapose h2f
Cleared hypotheses: h2f
-- Lean 4 proof step from Mathlib.Order.SuccPred.IntervalSucc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : LinearOrder β
f : α → β
a : α
hf : ∀ i ∈ Ici a, f a ≤ f i
b : β
hb : b ∈ Ioi (f a)
h2f : b ∉ ⋃ i ∈ Ici a, Ioc (f i) (f (succ i))
⊢ BddAbove (f '' Ici a)
have suffices : ∀ (i : α), a ≤ i → f i < b
Tactic: suffices ∀ i, a ≤ i → f i < b from ⟨b, by aesop (add simp [upperBounds, le_of_lt])⟩
-- Lean 4 proof step from Mathlib.Order.SuccPred.IntervalSucc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : LinearOrder β
f : α → β
hf : Monotone f
m n : α
⊢ ⋃ i ∈ Ico m n, Ioc (f i) (f (succ i)) = Ioc (f m) (f n)
have inl : ∀ (hnm : n ≤ m), ⋃ i ∈ Ico m n, Ioc (f i) (f (succ i)) = Ioc (f m) (f n)
Tactic: rcases le_total n m with hnm | hmn
-- Lean 4 proof step from Mathlib.Order.SuccPred.IntervalSucc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : LinearOrder β
f : α → β
hf : Monotone f
m n : α
inl : ∀ (hnm : n ≤ m), ⋃ i ∈ Ico m n, Ioc (f i) (f (succ i)) = Ioc (f m) (f n)
⊢ ⋃ i ∈ Ico m n, Ioc (f i) (f (succ i)) = Ioc (f m) (f n)
have inr : ∀ (hmn : m ≤ n), ⋃ i ∈ Ico m n, Ioc (f i) (f (succ i)) = Ioc (f m) (f n)
Tactic: rcases le_total n m with hnm | hmn
-- Lean 4 proof step from Mathlib.Order.SuccPred.IntervalSucc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : LinearOrder β
f : α → β
hf : Monotone f
m n : α
hnm : n ≤ m
⊢ ⋃ i ∈ Ico m n, Ioc (f i) (f (succ i)) = Ioc (f m) (f n)
have inl : ⋃ (i : α), ⋃ (_ : Membership.mem (γ := Set α) ∅ i), Ioc (f i) (f (succ i)) = Ioc (f m) (f n)
Tactic: rw [Ico_eq_empty_of_le hnm, Ioc_eq_empty_of_le (hf hnm), biUnion_empty]
-- Lean 4 proof step from Mathlib.Order.SuccPred.IntervalSucc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : LinearOrder β
f : α → β
hf : Monotone f
m n : α
hnm : n ≤ m
inl : ⋃ (i : α), ⋃ (_ : Membership.mem (γ := Set α) ∅ i), Ioc (f i) (f (succ i)) = Ioc (f m) (f n)
⊢ ⋃ i ∈ Ico m n, Ioc (f i) (f (succ i)) = Ioc (f m) (f n)
have inl₁ : Eq.{u_2 + 1} (α := Set β) (⋃ (i : α), ⋃ (_ : Membership.mem (γ := Set α) ∅ i), Ioc (f i) (f (succ i))) ∅
Tactic: rw [Ico_eq_empty_of_le hnm, Ioc_eq_empty_of_le (hf hnm), biUnion_empty]
-- Lean 4 proof step from Mathlib.Order.SuccPred.IntervalSucc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : LinearOrder β
f : α → β
hf : Monotone f
m n : α
hnm : n ≤ m
inl : ⋃ (i : α), ⋃ (_ : Membership.mem (γ := Set α) ∅ i), Ioc (f i) (f (succ i)) = Ioc (f m) (f n)
inl₁ : Eq.{u_2 + 1} (α := Set β) (⋃ (i : α), ⋃ (_ : Membership.mem (γ := Set α) ∅ i), Ioc (f i) (f (succ i))) ∅
⊢ ⋃ i ∈ Ico m n, Ioc (f i) (f (succ i)) = Ioc (f m) (f n)
have inl₂ : Eq.{u_2 + 1} (α := Set β) ∅ ∅
Tactic: rw [Ico_eq_empty_of_le hnm, Ioc_eq_empty_of_le (hf hnm), biUnion_empty]
-- Lean 4 proof step from Mathlib.Order.SuccPred.IntervalSucc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : LinearOrder β
f : α → β
hf : Monotone f
m n : α
hmn : m ≤ n
⊢ ⋃ i ∈ Ico m n, Ioc (f i) (f (succ i)) = Ioc (f m) (f n)
have inr : ⋃ i ∈ Ico m m, Ioc (f i) (f (succ i)) = Ioc (f m) (f m)
Tactic: refine Succ.rec ?_ ?_ hmn
-- Lean 4 proof step from Mathlib.Order.SuccPred.IntervalSucc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : LinearOrder β
f : α → β
hf : Monotone f
m n : α
hmn : m ≤ n
inr : ⋃ i ∈ Ico m m, Ioc (f i) (f (succ i)) = Ioc (f m) (f m)
⊢ ⋃ i ∈ Ico m n, Ioc (f i) (f (succ i)) = Ioc (f m) (f n)
have inr₁ : ∀ (n : α) (hmn : m ≤ n),
  ⋃ i ∈ Ico m n, Ioc (f i) (f (succ i)) = Ioc (f m) (f n) →
    ⋃ i ∈ Ico m (succ n), Ioc (f i) (f (succ i)) = Ioc (f m) (f (succ n))
Tactic: refine Succ.rec ?_ ?_ hmn
-- Lean 4 proof step from Mathlib.Order.SuccPred.IntervalSucc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : LinearOrder β
f : α → β
hf : Monotone f
m n : α
hmn : m ≤ n
k : α
hmk : m ≤ k
ihk : ⋃ i ∈ Ico m k, Ioc (f i) (f (succ i)) = Ioc (f m) (f k)
⊢ ⋃ i ∈ Ico m (succ k), Ioc (f i) (f (succ i)) = Ioc (f m) (f (succ k))
have inr : ⋃ i ∈ Ico m (succ k), Ioc (f i) (f (succ i)) = Ioc (f k) (f (succ k)) ∪ ⋃ i ∈ Ico m k, Ioc (f i) (f (succ i))
Tactic: rw [← Ioc_union_Ioc_eq_Ioc (hf hmk) (hf <| le_succ _), union_comm, ← ihk]
-- Lean 4 proof step from Mathlib.Order.SuccPred.IntervalSucc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : LinearOrder β
f : α → β
hf : Monotone f
m n : α
hmn : m ≤ n
k : α
hmk : m ≤ k
ihk : ⋃ i ∈ Ico m k, Ioc (f i) (f (succ i)) = Ioc (f m) (f k)
⊢ ⋃ i ∈ Ico m (succ k), Ioc (f i) (f (succ i)) = Ioc (f k) (f (succ k)) ∪ ⋃ i ∈ Ico m k, Ioc (f i) (f (succ i))
have pos : ∀ (hk : IsMax k),
  ⋃ i ∈ Ico m (succ k), Ioc (f i) (f (succ i)) = Ioc (f k) (f (succ k)) ∪ ⋃ i ∈ Ico m k, Ioc (f i) (f (succ i))
Tactic: by_cases hk : IsMax k
-- Lean 4 proof step from Mathlib.Order.SuccPred.IntervalSucc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : LinearOrder β
f : α → β
hf : Monotone f
m n : α
hmn : m ≤ n
k : α
hmk : m ≤ k
ihk : ⋃ i ∈ Ico m k, Ioc (f i) (f (succ i)) = Ioc (f m) (f k)
pos :
  ∀ (hk : IsMax k),
    ⋃ i ∈ Ico m (succ k), Ioc (f i) (f (succ i)) = Ioc (f k) (f (succ k)) ∪ ⋃ i ∈ Ico m k, Ioc (f i) (f (succ i))
⊢ ⋃ i ∈ Ico m (succ k), Ioc (f i) (f (succ i)) = Ioc (f k) (f (succ k)) ∪ ⋃ i ∈ Ico m k, Ioc (f i) (f (succ i))
have neg : ∀ (hk : ¬IsMax k),
  ⋃ i ∈ Ico m (succ k), Ioc (f i) (f (succ i)) = Ioc (f k) (f (succ k)) ∪ ⋃ i ∈ Ico m k, Ioc (f i) (f (succ i))
Tactic: by_cases hk : IsMax k
-- Lean 4 proof step from Mathlib.Order.SuccPred.IntervalSucc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : LinearOrder β
f : α → β
hf : Monotone f
m n : α
hmn : m ≤ n
k : α
hmk : m ≤ k
ihk : ⋃ i ∈ Ico m k, Ioc (f i) (f (succ i)) = Ioc (f m) (f k)
hk : IsMax k
⊢ ⋃ i ∈ Ico m (succ k), Ioc (f i) (f (succ i)) = Ioc (f k) (f (succ k)) ∪ ⋃ i ∈ Ico m k, Ioc (f i) (f (succ i))
have pos : ⋃ i ∈ Ico m k, Ioc (f i) (f (succ i)) = Ioc (f k) (f k) ∪ ⋃ i ∈ Ico m k, Ioc (f i) (f (succ i))
Tactic: rw [hk.succ_eq, Ioc_self, empty_union]
-- Lean 4 proof step from Mathlib.Order.SuccPred.IntervalSucc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : LinearOrder β
f : α → β
hf : Monotone f
m n : α
hmn : m ≤ n
k : α
hmk : m ≤ k
ihk : ⋃ i ∈ Ico m k, Ioc (f i) (f (succ i)) = Ioc (f m) (f k)
hk : IsMax k
pos : ⋃ i ∈ Ico m k, Ioc (f i) (f (succ i)) = Ioc (f k) (f k) ∪ ⋃ i ∈ Ico m k, Ioc (f i) (f (succ i))
⊢ ⋃ i ∈ Ico m (succ k), Ioc (f i) (f (succ i)) = Ioc (f k) (f (succ k)) ∪ ⋃ i ∈ Ico m k, Ioc (f i) (f (succ i))
have pos₁ : Eq.{u_2 + 1} (α := Set β) (⋃ i ∈ Ico m k, Ioc (f i) (f (succ i))) (∅ ∪ ⋃ i ∈ Ico m k, Ioc (f i) (f (succ i)))
Tactic: rw [hk.succ_eq, Ioc_self, empty_union]
-- Lean 4 proof step from Mathlib.Order.SuccPred.IntervalSucc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : LinearOrder β
f : α → β
hf : Monotone f
m n : α
hmn : m ≤ n
k : α
hmk : m ≤ k
ihk : ⋃ i ∈ Ico m k, Ioc (f i) (f (succ i)) = Ioc (f m) (f k)
hk : IsMax k
pos : ⋃ i ∈ Ico m k, Ioc (f i) (f (succ i)) = Ioc (f k) (f k) ∪ ⋃ i ∈ Ico m k, Ioc (f i) (f (succ i))
pos₁ : Eq.{u_2 + 1} (α := Set β) (⋃ i ∈ Ico m k, Ioc (f i) (f (succ i))) (∅ ∪ ⋃ i ∈ Ico m k, Ioc (f i) (f (succ i)))
⊢ ⋃ i ∈ Ico m (succ k), Ioc (f i) (f (succ i)) = Ioc (f k) (f (succ k)) ∪ ⋃ i ∈ Ico m k, Ioc (f i) (f (succ i))
have pos₂ : Eq.{u_2 + 1} (α := Set β) (⋃ i ∈ Ico m k, Ioc (f i) (f (succ i))) (⋃ i ∈ Ico m k, Ioc (f i) (f (succ i)))
Tactic: rw [hk.succ_eq, Ioc_self, empty_union]
-- Lean 4 proof step from Mathlib.Order.SuccPred.IntervalSucc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : LinearOrder β
f : α → β
hf : Monotone f
m n : α
hmn : m ≤ n
k : α
hmk : m ≤ k
ihk : ⋃ i ∈ Ico m k, Ioc (f i) (f (succ i)) = Ioc (f m) (f k)
hk : ¬IsMax k
⊢ ⋃ i ∈ Ico m (succ k), Ioc (f i) (f (succ i)) = Ioc (f k) (f (succ k)) ∪ ⋃ i ∈ Ico m k, Ioc (f i) (f (succ i))
have neg : ⋃ i ∈ insert k (Ico m k), Ioc (f i) (f (succ i)) = Ioc (f k) (f (succ k)) ∪ ⋃ i ∈ Ico m k, Ioc (f i) (f (succ i))
Tactic: rw [Ico_succ_right_eq_insert_of_not_isMax hmk hk, biUnion_insert]
-- Lean 4 proof step from Mathlib.Order.SuccPred.IntervalSucc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : LinearOrder β
f : α → β
hf : Monotone f
m n : α
hmn : m ≤ n
k : α
hmk : m ≤ k
ihk : ⋃ i ∈ Ico m k, Ioc (f i) (f (succ i)) = Ioc (f m) (f k)
hk : ¬IsMax k
neg : ⋃ i ∈ insert k (Ico m k), Ioc (f i) (f (succ i)) = Ioc (f k) (f (succ k)) ∪ ⋃ i ∈ Ico m k, Ioc (f i) (f (succ i))
⊢ ⋃ i ∈ Ico m (succ k), Ioc (f i) (f (succ i)) = Ioc (f k) (f (succ k)) ∪ ⋃ i ∈ Ico m k, Ioc (f i) (f (succ i))
have neg₁ : Ioc (f k) (f (succ k)) ∪ ⋃ x ∈ Ico m k, Ioc (f x) (f (succ x)) =
  Ioc (f k) (f (succ k)) ∪ ⋃ i ∈ Ico m k, Ioc (f i) (f (succ i))
Tactic: rw [Ico_succ_right_eq_insert_of_not_isMax hmk hk, biUnion_insert]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
a : α
inst : Preorder α
h : IsSuccPrelimit a
⊢ NoMaxOrder.{u_1} (↑(Iio a) : Type u_1)
have refine : ∀ (x : (↑(Iio a) : Type u_1)) (b : α) (hb : b ∈ Iio a),
  ∃ (b_1 : (↑(Iio a) : Type u_1)), Subtype.mk (p := fun (x : α) ↦ x ∈ Iio a) b hb < b_1
Tactic: refine ⟨fun ⟨b, hb⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
a : α
inst : Preorder α
h : IsSuccPrelimit a
x : (↑(Iio a) : Type u_1)
b : α
hb : b ∈ Iio a
⊢ ∃ (b_1 : (↑(Iio a) : Type u_1)), Subtype.mk (p := fun (x : α) ↦ x ∈ Iio a) b hb < b_1
have obtain : ∀ (c : α) (hbc : b < c) (hca : c < a),
  ∃ (b_1 : (↑(Iio a) : Type u_1)), Subtype.mk (p := fun (x : α) ↦ x ∈ Iio a) b hb < b_1
Tactic: obtain ⟨c, hbc, hca⟩ := (not_covBy_iff hb).1 (h b)
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
a : α
inst : Preorder α
⊢ ¬IsSuccLimit a ↔ IsMin a ∨ ¬IsSuccPrelimit a
have rw : ¬(¬IsMin a ∧ IsSuccPrelimit a) ↔ IsMin a ∨ ¬IsSuccPrelimit a
Tactic: rw [IsSuccLimit, not_and_or, not_not]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
a : α
inst : Preorder α
rw : ¬(¬IsMin a ∧ IsSuccPrelimit a) ↔ IsMin a ∨ ¬IsSuccPrelimit a
⊢ ¬IsSuccLimit a ↔ IsMin a ∨ ¬IsSuccPrelimit a
have rw₁ : ¬¬IsMin a ∨ ¬IsSuccPrelimit a ↔ IsMin a ∨ ¬IsSuccPrelimit a
Tactic: rw [IsSuccLimit, not_and_or, not_not]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
a : α
inst : Preorder α
rw : ¬(¬IsMin a ∧ IsSuccPrelimit a) ↔ IsMin a ∨ ¬IsSuccPrelimit a
rw₁ : ¬¬IsMin a ∨ ¬IsSuccPrelimit a ↔ IsMin a ∨ ¬IsSuccPrelimit a
⊢ ¬IsSuccLimit a ↔ IsMin a ∨ ¬IsSuccPrelimit a
have rw₂ : IsMin a ∨ ¬IsSuccPrelimit a ↔ IsMin a ∨ ¬IsSuccPrelimit a
Tactic: rw [IsSuccLimit, not_and_or, not_not]
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
s : Set α
hs : IsLowerSet s
a : (↑s : Type u_1)
ha : IsSuccPrelimit a
b : α
hb : b ⋖ (↑a : α)
⊢ False
have this : ¬Subtype.mk (p := fun (x : α) ↦ x ∈ s) b sorry ⋖ a
Tactic: have := ha ⟨b, hs hb.le a.2⟩
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
inst : Preorder α
s : Set α
hs : IsLowerSet s
a : (↑s : Type u_1)
ha : IsSuccPrelimit a
b : α
hb : b ⋖ (↑a : α)
this : ¬Subtype.mk (p := fun (x : α) ↦ x ∈ s) b ⋯ ⋖ a
⊢ False
have rw : ∀ (this : ∃ (c : (↑s : Type u_1)), Subtype.mk (p := fun (x : α) ↦ x ∈ s) b sorry < c ∧ c < a), False
Tactic: rw [not_covBy_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
inst : Preorder α
s : Set α
hs : IsLowerSet s
a : (↑s : Type u_1)
ha : IsSuccPrelimit a
b : α
hb : b ⋖ (↑a : α)
this : ¬Subtype.mk (p := fun (x : α) ↦ x ∈ s) b ⋯ ⋖ a
rw : ∀ (this : ∃ (c : (↑s : Type u_1)), Subtype.mk (p := fun (x : α) ↦ x ∈ s) b ⋯ < c ∧ c < a), False
⊢ False
have rw₁ : Subtype.mk (p := fun (x : α) ↦ x ∈ s) b sorry < a
Tactic: rw [not_covBy_iff] at this
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
inst : Preorder α
s : Set α
hs : IsLowerSet s
a : (↑s : Type u_1)
ha : IsSuccPrelimit a
b : α
hb : b ⋖ (↑a : α)
this : ∃ (c : (↑s : Type u_1)), Subtype.mk (p := fun (x : α) ↦ x ∈ s) b ⋯ < c ∧ c < a
⊢ False
have obtain : ∀ (c : (↑s : Type u_1)) (hc : Subtype.mk (p := fun (x : α) ↦ x ∈ s) b sorry < c) (hc' : c < a), False
Tactic: obtain ⟨c, hc, hc'⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
inst : Preorder α
s : Set α
hs : IsLowerSet s
a : (↑s : Type u_1)
ha : IsSuccLimit a
⊢ IsSuccLimit (↑a : α)
have refine : ¬IsMin (↑a : α)
Tactic: refine ⟨?_, ha.isSuccPrelimit.subtypeVal hs⟩
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (hypothesis)
Goal:
α : Type u_1
inst : Preorder α
s : Set α
hs : IsLowerSet s
a : (↑s : Type u_1)
ha : IsSuccLimit a
⊢ ¬IsMin (↑a : α)
have this : ¬IsMin a
Tactic: have := ha.1
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
inst : Preorder α
s : Set α
hs : IsLowerSet s
a : (↑s : Type u_1)
ha : IsSuccLimit a
this : ¬IsMin a
⊢ ¬IsMin (↑a : α)
have rw : ∀ (this : ∃ (b : (↑s : Type u_1)), b < a), ∃ (b : α), b < (↑a : α)
Tactic: rw [not_isMin_iff] at ⊢ this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
inst : Preorder α
s : Set α
hs : IsLowerSet s
a : (↑s : Type u_1)
ha : IsSuccLimit a
this : ∃ (b : (↑s : Type u_1)), b < a
⊢ ∃ (b : α), b < (↑a : α)
have obtain : ∀ (b : (↑s : Type u_1)) (hb : b < a), ∃ (b : α), b < (↑a : α)
Tactic: obtain ⟨b, hb⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
x : WithTop α
⊢ IsSuccPrelimit x ↔ x = ⊤ ∨ ∃ (y : α), x = (↑y : WithTop α) ∧ IsSuccPrelimit y
have coe : ∀ (x : α),
  IsSuccPrelimit (↑x : WithTop α) ↔
    (↑x : WithTop α) = ⊤ ∨ ∃ (y : α), (↑x : WithTop α) = (↑y : WithTop α) ∧ IsSuccPrelimit y
Tactic: cases x with
  | coe x => simp [IsSuccPrelimit, WithTop.forall]
  | top => simp [IsSuccPrelimit]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : NoMaxOrder α
x : WithTop α
coe :
  ∀ (x : α),
    IsSuccPrelimit (↑x : WithTop α) ↔
      (↑x : WithTop α) = ⊤ ∨ ∃ (y : α), (↑x : WithTop α) = (↑y : WithTop α) ∧ IsSuccPrelimit y
⊢ IsSuccPrelimit x ↔ x = ⊤ ∨ ∃ (y : α), x = (↑y : WithTop α) ∧ IsSuccPrelimit y
have top : IsSuccPrelimit.{u_1} (α := WithTop α) ⊤ ↔
  Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤ ∨ ∃ (y : α), ⊤ = (↑y : WithTop α) ∧ IsSuccPrelimit y
Tactic: cases x with
  | coe x => simp [IsSuccPrelimit, WithTop.forall]
  | top => simp [IsSuccPrelimit]
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.SuccPred.Limit (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Nonempty α
inst_2 : NoMaxOrder α
x : WithTop α
⊢ IsSuccLimit x ↔ x = ⊤ ∨ ∃ (y : α), x = (↑y : WithTop α) ∧ IsSuccLimit y
have coe : ∀ (x : α),
  IsSuccLimit (↑x : WithTop α) ↔ (↑x : WithTop α) = ⊤ ∨ ∃ (y : α), (↑x : WithTop α) = (↑y : WithTop α) ∧ IsSuccLimit y
Tactic: cases x with
  | coe x => simp [IsSuccLimit, WithTop.isSuccPrelimit_iff, WithTop.exists]
  | top => simp [IsSuccLimit, WithTop.exists]
Cleared hypotheses: x