awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.SuccPred.InitialSeg
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 : β)
⊢ c ⋖ a

Tactic:
rw [f.apply_covBy_apply_iff] at hb

Premises used: InitialSeg.apply_covBy_apply_iff
-- Module: Mathlib.Order.SuccPred.InitialSeg
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 : c ⋖ a
⊢ False

Tactic:
h _ hb
-- Module: Mathlib.Order.SuccPred.InitialSeg
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 : c ⋖ a
⊢ False

Tactic:
exact h _ hb
-- Module: Mathlib.Order.SuccPred.InitialSeg
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
⊢ IsSuccLimit.{u_2} (α := β) ((f : (a : α) → β) a : β) ↔ IsSuccLimit a

Tactic:
simp [IsSuccLimit]

Premises used: Order.IsSuccLimit
-- Module: Mathlib.Order.SuccPred.InitialSeg
Goal:
α : Type u_1
β : Type u_2
a b : α
inst : PartialOrder α
inst_1 : PartialOrder β
f : PrincipalSeg (fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : β) ↦ x1 < x2
⊢ CovBy.{u_2} (α := β)
      ((f.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2) : (a : α) → β) a : β)
      ((f.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2) : (a : α) → β) b : β) ↔
    a ⋖ b

Tactic:
(f : α ≤i β).apply_covBy_apply_iff

Premises used: PrincipalSeg.toRelEmbedding, PrincipalSeg.mem_range_of_rel, InitialSeg.apply_covBy_apply_iff, InitialSeg.mk
-- Module: Mathlib.Order.SuccPred.InitialSeg
Goal:
α : Type u_1
β : Type u_2
a b : α
inst : PartialOrder α
inst_1 : PartialOrder β
f : PrincipalSeg (fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : β) ↦ x1 < x2
⊢ WCovBy.{u_2} (α := β)
      ((f.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2) : (a : α) → β) a : β)
      ((f.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2) : (a : α) → β) b : β) ↔
    a ⩿ b

Tactic:
(f : α ≤i β).apply_wCovBy_apply_iff

Premises used: PrincipalSeg.toRelEmbedding, PrincipalSeg.mem_range_of_rel, InitialSeg.apply_wCovBy_apply_iff, InitialSeg.mk
-- Module: Mathlib.Order.SuccPred.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : SuccOrder α
inst_3 : NoMaxOrder α
inst_4 : SuccOrder β
f : PrincipalSeg (fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : β) ↦ x1 < x2
a : α
⊢ Eq.{u_2 + 1} (α := β)
    ((f.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2) : (a : α) → β) (succ a) : β)
    (succ ((f.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2) : (a : α) → β) a) : β)

Tactic:
(f : α ≤i β).map_succ a

Premises used: InitialSeg.map_succ, PrincipalSeg.toRelEmbedding, PrincipalSeg.mem_range_of_rel, InitialSeg.mk
-- Module: Mathlib.Order.SuccPred.InitialSeg
Goal:
α : Type u_1
β : Type u_2
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : PredOrder α
inst_3 : NoMinOrder α
inst_4 : PredOrder β
f : InitialSeg (fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : β) ↦ x1 < x2
a : α
⊢ Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) (pred a) : β) (pred ((f : (a : α) → β) a) : β)

Tactic:
(f : α ≤i β).map_pred a

Premises used: InitialSeg.map_pred
-- Module: Mathlib.Order.SuccPred.InitialSeg
Goal:
α : Type u_1
β : Type u_2
a : α
inst : PartialOrder α
inst_1 : PartialOrder β
f : PrincipalSeg (fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : β) ↦ x1 < x2
⊢ IsSuccPrelimit.{u_2} (α := β)
      ((f.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2) : (a : α) → β) a : β) ↔
    IsSuccPrelimit a

Tactic:
(f : α ≤i β).isSuccPrelimit_apply_iff

Premises used: PrincipalSeg.toRelEmbedding, PrincipalSeg.mem_range_of_rel, InitialSeg.isSuccPrelimit_apply_iff, InitialSeg.mk
-- Module: Mathlib.Order.SuccPred.InitialSeg
Goal:
α : Type u_1
β : Type u_2
a : α
inst : PartialOrder α
inst_1 : PartialOrder β
f : PrincipalSeg (fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : β) ↦ x1 < x2
⊢ IsSuccLimit.{u_2} (α := β)
      ((f.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2) : (a : α) → β) a : β) ↔
    IsSuccLimit a

Tactic:
(f : α ≤i β).isSuccLimit_apply_iff

Premises used: PrincipalSeg.toRelEmbedding, PrincipalSeg.mem_range_of_rel, InitialSeg.isSuccLimit_apply_iff, InitialSeg.mk
-- Module: Mathlib.Order.SuccPred.IntervalSucc
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)
apply : Ici (f a) ⊆ ⋃ i ∈ Ici a, Ico (f i) (f (succ i))
⊢ ⋃ i ∈ Ici a, Ico (f i) (f (succ i)) = Ici (f a)

Tactic:
apply subset_antisymm <|
    iUnion₂_subset fun i hi ↦ Ico_subset_Ico_left (hf i hi) |>.trans Ico_subset_Ici_self

Premises used: Set.iUnion₂_subset, HasSubset.Subset.trans, subset_antisymm, Set.Ico_subset_Ici_self, Set.Ico_subset_Ico_left
-- Module: Mathlib.Order.SuccPred.IntervalSucc
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)
contrapose : ∀ (h2f : b ∉ ⋃ i ∈ Ici a, Ico (f i) (f (succ i))), BddAbove (f '' Ici a)
⊢ Membership.mem (γ := Set β) (⋃ i ∈ Ici a, Ico (f i) (f (succ i))) b

Tactic:
contrapose h2f
-- Module: Mathlib.Order.SuccPred.IntervalSucc
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))
h : b ∈ upperBounds (f '' Ici a)
⊢ BddAbove (f '' Ici a)

Tactic:
use b
-- Module: Mathlib.Order.SuccPred.IntervalSucc
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))
h : Membership.mem (γ := Set β) {x : β | ∀ a_1 ∈ Ici a, f a_1 ≤ x} b
⊢ b ∈ upperBounds (f '' Ici a)

Tactic:
simp only [upperBounds, mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]

Premises used: and_imp, Set.mem_image, forall_exists_index, upperBounds, forall_apply_eq_imp_iff₂
-- Module: Mathlib.Order.SuccPred.IntervalSucc
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))
⊢ ∀ (n : α) (hmn : a ≤ n), (fun (i : α) (x : a ≤ i) ↦ f i ≤ b) n hmn → (fun (i : α) (x : a ≤ i) ↦ f i ≤ b) (succ n) ⋯

Tactic:
simp_all
-- Module: Mathlib.Order.SuccPred.IntervalSucc
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))
⊢ Membership.mem (γ := Set β) {x : β | ∀ a_1 ∈ Ici a, f a_1 ≤ x} b

Tactic:
exact Succ.rec (P := fun i _ ↦ f i ≤ b) hb (by simp_all)

Premises used: Succ.rec
-- Module: Mathlib.Order.SuccPred.IntervalSucc
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)
apply : Ioi (f a) ⊆ ⋃ i ∈ Ici a, Ioc (f i) (f (succ i))
⊢ ⋃ i ∈ Ici a, Ioc (f i) (f (succ i)) = Ioi (f a)

Tactic:
apply subset_antisymm <|
    iUnion₂_subset fun i hi ↦ Ioc_subset_Ioc_left (hf i hi) |>.trans Ioc_subset_Ioi_self

Premises used: Set.iUnion₂_subset, Set.Ioc_subset_Ioc_left, HasSubset.Subset.trans, subset_antisymm, Set.Ioc_subset_Ioi_self
-- Module: Mathlib.Order.SuccPred.IntervalSucc
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)
contrapose : ∀ (h2f : b ∉ ⋃ i ∈ Ici a, Ioc (f i) (f (succ i))), BddAbove (f '' Ici a)
⊢ Membership.mem (γ := Set β) (⋃ i ∈ Ici a, Ioc (f i) (f (succ i))) b

Tactic:
contrapose h2f
-- Module: Mathlib.Order.SuccPred.IntervalSucc
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))
this : ∀ (i : α), a ≤ i → f i < b
⊢ b ∈ upperBounds (f '' Ici a)

Tactic:
aesop (add simp [upperBounds, le_of_lt])

Premises used: le_of_lt, upperBounds
-- Module: Mathlib.Order.SuccPred.IntervalSucc
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))
suffices : ∀ (i : α), a ≤ i → f i < b
⊢ BddAbove (f '' Ici a)

Tactic:
suffices ∀ i, a ≤ i → f i < b from ⟨b, by aesop (add simp [upperBounds, le_of_lt])⟩
-- Module: Mathlib.Order.SuccPred.IntervalSucc
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))
⊢ ∀ (n : α) (hmn : a ≤ n), (fun (i : α) (x : a ≤ i) ↦ f i < b) n hmn → (fun (i : α) (x : a ≤ i) ↦ f i < b) (succ n) ⋯

Tactic:
simp_all
-- Module: Mathlib.Order.SuccPred.IntervalSucc
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))
⊢ ∀ (i : α), a ≤ i → f i < b

Tactic:
exact Succ.rec (P := fun i _ ↦ f i < b) hb (by simp_all)

Premises used: Succ.rec
-- Module: Mathlib.Order.SuccPred.IntervalSucc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : OrderBot α
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
inst_4 : LinearOrder β
f : α → β
hf : ∀ (a : α), f ⊥ ≤ f a
h2f : ¬BddAbove (range f)
⊢ ∀ (i : α), Membership.mem (γ := Set α) (Ici ⊥) i → f ⊥ ≤ f i

Tactic:
simpa
-- Module: Mathlib.Order.SuccPred.IntervalSucc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : OrderBot α
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
inst_4 : LinearOrder β
f : α → β
hf : ∀ (a : α), f ⊥ ≤ f a
h2f : ¬BddAbove (range f)
⊢ ¬BddAbove (f '' Ici ⊥)

Tactic:
simpa
-- Module: Mathlib.Order.SuccPred.IntervalSucc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : OrderBot α
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
inst_4 : LinearOrder β
f : α → β
hf : ∀ (a : α), f ⊥ ≤ f a
h2f : ¬BddAbove (range f)
⊢ ⋃ (a : α), Ico (f a) (f (succ a)) = Ici (f ⊥)

Tactic:
simpa using biUnion_Ici_Ico_map_succ (f := f) (a := ⊥) (by simpa) (by simpa)

Premises used: biUnion_Ici_Ico_map_succ
-- Module: Mathlib.Order.SuccPred.IntervalSucc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : OrderBot α
inst_2 : SuccOrder α
inst_3 : IsSuccArchimedean α
inst_4 : LinearOrder β
f : α → β
hf : ∀ (a : α), f ⊥ ≤ f a
h2f : ¬BddAbove (range f)
⊢ ⋃ (a : α), Ioc (f a) (f (succ a)) = Ioi (f ⊥)

Tactic:
simpa using biUnion_Ici_Ioc_map_succ (f := f) (a := ⊥) (by simpa) (by simpa)

Premises used: biUnion_Ici_Ioc_map_succ
-- Module: Mathlib.Order.SuccPred.IntervalSucc
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)
inr : ∀ (hmn : m ≤ n), ⋃ 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)

Tactic:
rcases le_total n m with hnm | hmn

Premises used: le_total
-- Module: Mathlib.Order.SuccPred.IntervalSucc
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))) ∅
inl₂ inl₃ : Eq.{u_2 + 1} (α := Set β) ∅ ∅
⊢ ⋃ i ∈ Ico m n, 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]

Premises used: Set.biUnion_empty, Set.Ioc_eq_empty_of_le, Set.Ico_eq_empty_of_le
-- Module: Mathlib.Order.SuccPred.IntervalSucc
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)

Tactic:
Succ.rec ?_ ?_ hmn

Premises used: Succ.rec
-- Module: Mathlib.Order.SuccPred.IntervalSucc
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)
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))
⊢ ⋃ i ∈ Ico m n, Ioc (f i) (f (succ i)) = Ioc (f m) (f n)

Tactic:
refine Succ.rec ?_ ?_ hmn
-- Module: Mathlib.Order.SuccPred.IntervalSucc
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 m, Ioc (f i) (f (succ i)) = Ioc (f m) (f m)

Tactic:
simp
-- Module: Mathlib.Order.SuccPred.IntervalSucc
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)
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))
⊢ ⋃ i ∈ Ico m (succ k), Ioc (f i) (f (succ i)) = Ioc (f m) (f (succ k))

Tactic:
rw [← Ioc_union_Ioc_eq_Ioc (hf hmk) (hf <| le_succ _), union_comm, ← ihk]

Premises used: Set.Ioc_union_Ioc_eq_Ioc, Set.union_comm, Order.le_succ
-- Module: Mathlib.Order.SuccPred.IntervalSucc
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))
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))
⊢ ⋃ 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

Premises used: IsMax
-- Module: Mathlib.Order.SuccPred.IntervalSucc
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)))
pos₂ 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))

Tactic:
rw [hk.succ_eq, Ioc_self, empty_union]

Premises used: Set.empty_union, Set.Ioc_self, IsMax.succ_eq
-- Module: Mathlib.Order.SuccPred.IntervalSucc
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))
neg₁ 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))
⊢ ⋃ 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 [Ico_succ_right_eq_insert_of_not_isMax hmk hk, biUnion_insert]

Premises used: Set.biUnion_insert, Order.Ico_succ_right_eq_insert_of_not_isMax
-- Module: Mathlib.Order.SuccPred.IntervalSucc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : Preorder β
f : α → β
hf : Monotone f
⊢ Pairwise.{u_1} (α := α)
    (Function.onFun.{u_1 + 1, u_2 + 1, 1} (β := Set β) Disjoint fun (n : α) ↦ Ioc (f n) (f (succ n)))

Tactic:
(pairwise_disjoint_on _).2 fun _ _ hmn =>
    disjoint_iff_inf_le.mpr fun _ ⟨⟨_, h₁⟩, ⟨h₂, _⟩⟩ =>
      h₂.not_ge <| h₁.trans <| hf <| succ_le_of_lt hmn

Premises used: Iff.mpr, Membership.mem, Order.succ_le_of_lt, Bot.bot, LE.le.trans, _private.0.Monotone.pairwise_disjoint_on_Ioc_succ.match_1, LT.lt.not_ge, disjoint_iff_inf_le, pairwise_disjoint_on
-- Module: Mathlib.Order.SuccPred.IntervalSucc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : Preorder β
f : α → β
hf : Monotone f
⊢ Pairwise.{u_1} (α := α)
    (Function.onFun.{u_1 + 1, u_2 + 1, 1} (β := Set β) Disjoint fun (n : α) ↦ Ico (f n) (f (succ n)))

Tactic:
(pairwise_disjoint_on _).2 fun _ _ hmn =>
    disjoint_iff_inf_le.mpr fun _ ⟨⟨_, h₁⟩, ⟨h₂, _⟩⟩ =>
      h₁.not_ge <| (hf <| succ_le_of_lt hmn).trans h₂

Premises used: Iff.mpr, Membership.mem, Order.succ_le_of_lt, Bot.bot, LE.le.trans, LT.lt.not_ge, disjoint_iff_inf_le, _private.0.Monotone.pairwise_disjoint_on_Ico_succ.match_1, pairwise_disjoint_on
-- Module: Mathlib.Order.SuccPred.IntervalSucc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : Preorder β
f : α → β
hf : Monotone f
⊢ Pairwise.{u_1} (α := α)
    (Function.onFun.{u_1 + 1, u_2 + 1, 1} (β := Set β) Disjoint fun (n : α) ↦ Ioo (f n) (f (succ n)))

Tactic:
hf.pairwise_disjoint_on_Ico_succ.mono fun _ _ h => h.mono Ioo_subset_Ico_self Ioo_subset_Ico_self

Premises used: Set.Ioo_subset_Ico_self, Disjoint.mono, Pairwise.mono, Monotone.pairwise_disjoint_on_Ico_succ
-- Module: Mathlib.Order.SuccPred.IntervalSucc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PredOrder α
inst_2 : Preorder β
f : α → β
hf : Monotone f
⊢ Pairwise.{u_1} (α := α)
    (Function.onFun.{u_1 + 1, u_2 + 1, 1} (β := Set β) Disjoint fun (n : α) ↦ Ioc (f (pred n)) (f n))

Tactic:
simpa using hf.dual.pairwise_disjoint_on_Ico_succ

Premises used: Monotone.dual, Monotone.pairwise_disjoint_on_Ico_succ
-- Module: Mathlib.Order.SuccPred.IntervalSucc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PredOrder α
inst_2 : Preorder β
f : α → β
hf : Monotone f
⊢ Pairwise.{u_1} (α := α)
    (Function.onFun.{u_1 + 1, u_2 + 1, 1} (β := Set β) Disjoint fun (n : α) ↦ Ico (f (pred n)) (f n))

Tactic:
simpa using hf.dual.pairwise_disjoint_on_Ioc_succ

Premises used: Monotone.dual, Monotone.pairwise_disjoint_on_Ioc_succ
-- Module: Mathlib.Order.SuccPred.IntervalSucc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PredOrder α
inst_2 : Preorder β
f : α → β
hf : Monotone f
⊢ Pairwise.{u_1} (α := α)
    (Function.onFun.{u_1 + 1, u_2 + 1, 1} (β := Set β) Disjoint fun (n : α) ↦ Ioo (f (pred n)) (f n))

Tactic:
simpa using hf.dual.pairwise_disjoint_on_Ioo_succ

Premises used: Monotone.dual, Monotone.pairwise_disjoint_on_Ioo_succ
-- Module: Mathlib.Order.SuccPred.IntervalSucc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : Preorder β
f : α → β
hf : Antitone f
⊢ Pairwise.{u_1} (α := α)
    (Function.onFun.{u_1 + 1, u_2 + 1, 1} (β := Set β) Disjoint fun (n : α) ↦ Ioc (f (succ n)) (f n))

Tactic:
hf.dual_left.pairwise_disjoint_on_Ioc_pred

Premises used: Order.succ, Monotone.pairwise_disjoint_on_Ioc_pred, Antitone.dual_left, Order.pred, OrderDual
-- Module: Mathlib.Order.SuccPred.IntervalSucc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : Preorder β
f : α → β
hf : Antitone f
⊢ Pairwise.{u_1} (α := α)
    (Function.onFun.{u_1 + 1, u_2 + 1, 1} (β := Set β) Disjoint fun (n : α) ↦ Ico (f (succ n)) (f n))

Tactic:
hf.dual_left.pairwise_disjoint_on_Ico_pred

Premises used: Order.succ, Antitone.dual_left, Monotone.pairwise_disjoint_on_Ico_pred, Order.pred, OrderDual
-- Module: Mathlib.Order.SuccPred.IntervalSucc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : Preorder β
f : α → β
hf : Antitone f
⊢ Pairwise.{u_1} (α := α)
    (Function.onFun.{u_1 + 1, u_2 + 1, 1} (β := Set β) Disjoint fun (n : α) ↦ Ioo (f (succ n)) (f n))

Tactic:
hf.dual_left.pairwise_disjoint_on_Ioo_pred

Premises used: Order.succ, Antitone.dual_left, Monotone.pairwise_disjoint_on_Ioo_pred, Order.pred, OrderDual
-- Module: Mathlib.Order.SuccPred.IntervalSucc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PredOrder α
inst_2 : Preorder β
f : α → β
hf : Antitone f
⊢ Pairwise.{u_1} (α := α)
    (Function.onFun.{u_1 + 1, u_2 + 1, 1} (β := Set β) Disjoint fun (n : α) ↦ Ioc (f n) (f (pred n)))

Tactic:
hf.dual_left.pairwise_disjoint_on_Ioc_succ

Premises used: Order.succ, Antitone.dual_left, Monotone.pairwise_disjoint_on_Ioc_succ, Order.pred, OrderDual
-- Module: Mathlib.Order.SuccPred.IntervalSucc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PredOrder α
inst_2 : Preorder β
f : α → β
hf : Antitone f
⊢ Pairwise.{u_1} (α := α)
    (Function.onFun.{u_1 + 1, u_2 + 1, 1} (β := Set β) Disjoint fun (n : α) ↦ Ico (f n) (f (pred n)))

Tactic:
hf.dual_left.pairwise_disjoint_on_Ico_succ

Premises used: Order.succ, Antitone.dual_left, Order.pred, OrderDual, Monotone.pairwise_disjoint_on_Ico_succ
-- Module: Mathlib.Order.SuccPred.IntervalSucc
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PredOrder α
inst_2 : Preorder β
f : α → β
hf : Antitone f
⊢ Pairwise.{u_1} (α := α)
    (Function.onFun.{u_1 + 1, u_2 + 1, 1} (β := Set β) Disjoint fun (n : α) ↦ Ioo (f n) (f (pred n)))

Tactic:
hf.dual_left.pairwise_disjoint_on_Ioo_succ

Premises used: Order.succ, Antitone.dual_left, Monotone.pairwise_disjoint_on_Ioo_succ, Order.pred, OrderDual
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : LT α
a : α
⊢ ¬IsSuccPrelimit a ↔ ∃ (b : α), b ⋖ a

Tactic:
simp [IsSuccPrelimit]

Premises used: Order.IsSuccPrelimit
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
inst : LT α
inst_1 : DenselyOrdered α
a : α
⊢ IsSuccPrelimit a

Tactic:
fun _ => not_covBy

Premises used: not_covBy, Order.IsSuccPrelimit
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : LT α
⊢ IsSuccPrelimit (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ↔ IsPredPrelimit a

Tactic:
simp [IsSuccPrelimit, IsPredPrelimit]

Premises used: Order.IsSuccPrelimit, Order.IsPredPrelimit
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : Preorder α
⊢ IsSuccLimit (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ↔ IsPredLimit a

Tactic:
simp [IsSuccLimit, IsPredLimit]

Premises used: Order.IsSuccLimit, Order.IsPredLimit
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : Preorder α
h : IsSuccLimit a
⊢ ¬IsMin a

Tactic:
h.1

Premises used: And.left
-- Module: Mathlib.Order.SuccPred.Limit
Goal:
α : Type u_1
a : α
inst : Preorder α
h : IsSuccLimit a
⊢ IsSuccPrelimit a

Tactic:
h.2

Premises used: And.right