awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a : α
ha : ¬IsMin a
b x : α
h : pred a < x ∧ x ≤ b ↔ x ∈ Icc a b
h₁ : pred a < x ∧ x ≤ b ↔ a ≤ x ∧ x ≤ b
h₂ h₃ : a ≤ x ∧ x ≤ b ↔ a ≤ x ∧ x ≤ b
⊢ x ∈ Ioc (pred a) b ↔ x ∈ Icc a b

Tactic:
rw [mem_Ioc, mem_Icc, pred_lt_iff_of_not_isMin ha]

Premises used: Set.mem_Icc, Set.mem_Ioc, Order.pred_lt_iff_of_not_isMin
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a : α
ha : ¬IsMin a
b : α
h : ∀ (x : α), x ∈ Ioo (pred a) b ↔ x ∈ Ico a b
⊢ Ioo (pred a) b = Ico a b

Tactic:
ext x
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a : α
ha : ¬IsMin a
b x : α
h : pred a < x ∧ x < b ↔ x ∈ Ico a b
h₁ : pred a < x ∧ x < b ↔ a ≤ x ∧ x < b
h₂ h₃ : a ≤ x ∧ x < b ↔ a ≤ x ∧ x < b
⊢ x ∈ Ioo (pred a) b ↔ x ∈ Ico a b

Tactic:
rw [mem_Ioo, mem_Ico, pred_lt_iff_of_not_isMin ha]

Premises used: Set.mem_Ioo, Set.mem_Ico, Order.pred_lt_iff_of_not_isMin
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a : α
ha : ¬IsMin a
b : α
rw : Ioo (pred a) b = Ico a b
rw₁ rw₂ : Ico a b = Ico a b
⊢ Ioc (pred a) (pred b) = Ico a b

Tactic:
rw [Ioc_pred_right_eq_Ioo, Ioo_pred_left_eq_Ioc_of_not_isMin ha]

Premises used: Set.Ioo_pred_left_eq_Ioc_of_not_isMin, Set.Ioc_pred_right_eq_Ioo
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a b : α
h : a ≤ b
h₁ : ∀ (x : α), x ∈ insert b (Icc a (pred b)) ↔ x ∈ Icc a b
⊢ insert b (Icc a (pred b)) = Icc a b

Tactic:
ext x
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a b : α
h : a ≤ b
x : α
h₁ : x ≤ b → x = b → a ≤ x
⊢ x ∈ insert b (Icc a (pred b)) ↔ x ∈ Icc a b

Tactic:
simp [or_and_left, ← le_iff_eq_or_le_pred]

Premises used: or_and_left, Order.le_iff_eq_or_le_pred
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a b : α
h : a ≤ b
x : α
⊢ x ≤ b → x = b → a ≤ x

Tactic:
simp_all
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a b : α
h : pred a ≤ b
h₁ : ∀ (x : α), x ∈ insert (pred a) (Icc a b) ↔ x ∈ Icc (pred a) b
⊢ insert (pred a) (Icc a b) = Icc (pred a) b

Tactic:
ext x
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a b : α
h : pred a ≤ b
x : α
h₁ : x = pred a ∨ a ≤ x → x = pred a → x ≤ b
⊢ x ∈ insert (pred a) (Icc a b) ↔ x ∈ Icc (pred a) b

Tactic:
simp [or_and_left, pred_le_iff_eq_or_le]

Premises used: Order.pred_le_iff_eq_or_le, or_and_left
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a b : α
h : pred a ≤ b
x : α
⊢ x = pred a ∨ a ≤ x → x = pred a → x ≤ b

Tactic:
simp_all
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a b : α
h : a ≤ b
ha : ¬IsMin a
rw : insert a (Ioc a b) = Icc a b
rw₁ rw₂ : Icc a b = Icc a b
⊢ insert a (Ioc a b) = Ioc (pred a) b

Tactic:
rw [Ioc_pred_left_of_not_isMin ha, Ioc_insert_left h]

Premises used: Set.Ioc_insert_left, Order.Ioc_pred_left_of_not_isMin
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a b : α
h : a < b
rw : insert b (Ioo a b) = Ioc a b
rw₁ rw₂ : Ioc a b = Ioc a b
⊢ insert b (Ioc a (pred b)) = Ioc a b

Tactic:
rw [Ioc_pred_right_of_not_isMin h.not_isMin, Ioo_insert_right h]

Premises used: Set.Ioo_insert_right, LT.lt.not_isMin, Order.Ioc_pred_right_of_not_isMin
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a b : α
h : a ≤ b
ha : ¬IsMin a
h₁ : ∀ (x : α), x ∈ insert (pred a) (Ico a b) ↔ x ∈ Ico (pred a) b
⊢ insert (pred a) (Ico a b) = Ico (pred a) b

Tactic:
ext x
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a b : α
h : a ≤ b
ha : ¬IsMin a
x : α
⊢ x ∈ insert (pred a) (Ico a b) ↔ x ∈ Ico (pred a) b

Tactic:
simp +contextual [or_and_left, pred_le_iff_eq_or_le, pred_lt_of_le_of_not_isMin h ha]

Premises used: Order.pred_le_iff_eq_or_le, or_and_left, Order.pred_lt_of_le_of_not_isMin
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a b : α
h : a < b
rw : Icc a (pred b) = Ico a b
rw₁ rw₂ : Ico a b = Ico a b
⊢ insert (pred b) (Ico a (pred b)) = Ico a b

Tactic:
rw [Ico_insert_right (le_pred_of_lt h), Icc_pred_right_of_not_isMin h.not_isMin]

Premises used: Order.le_pred_of_lt, Set.Ico_insert_right, LT.lt.not_isMin, Order.Icc_pred_right_of_not_isMin
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
inst_2 : NoMinOrder α
a b : α
⊢ Icc a (pred b) = Ico a b

Tactic:
Icc_pred_right_eq_Ico_of_not_isMin (not_isMin _) _

Premises used: not_isMin, Set.Icc_pred_right_eq_Ico_of_not_isMin
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
inst_2 : NoMinOrder α
a b : α
⊢ Ioc (pred a) b = Icc a b

Tactic:
Ioc_pred_left_eq_Icc_of_not_isMin (not_isMin _) _

Premises used: not_isMin, Set.Ioc_pred_left_eq_Icc_of_not_isMin
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
inst_2 : NoMinOrder α
a b : α
⊢ Ioo (pred a) b = Ico a b

Tactic:
Ioo_pred_left_eq_Ioc_of_not_isMin (not_isMin _) _

Premises used: Set.Ioo_pred_left_eq_Ioc_of_not_isMin, not_isMin
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
inst_2 : NoMinOrder α
a b : α
⊢ Ioc (pred a) (pred b) = Ico a b

Tactic:
Ioc_pred_pred_eq_Ico_of_not_isMin (not_isMin _) _

Premises used: not_isMin, Set.Ioc_pred_pred_eq_Ico_of_not_isMin
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a b : α
inst_2 : NoMinOrder α
h : a ≤ b
⊢ insert a (Ioc a b) = Ioc (pred a) b

Tactic:
insert_Ioc_left_eq_Ioc_pred_of_not_isMin h (not_isMin _)

Premises used: not_isMin, Set.insert_Ioc_left_eq_Ioc_pred_of_not_isMin
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a b : α
inst_2 : NoMinOrder α
h : a ≤ b
⊢ insert (pred a) (Ico a b) = Ico (pred a) b

Tactic:
insert_Ico_left_eq_Ico_pred_of_not_isMin h (not_isMin _)

Premises used: not_isMin, Set.insert_Ico_left_eq_Ico_pred_of_not_isMin
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
inst_3 : Nontrivial α
a b : α
pos : ∀ (hb : IsMin b), Icc (succ a) (pred b) = Ioo a b
neg : ∀ (hb : ¬IsMin b), Icc (succ a) (pred b) = Ioo a b
⊢ Icc (succ a) (pred b) = Ioo a b

Tactic:
by_cases hb : IsMin b

Premises used: IsMin
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
inst_3 : Nontrivial α
a b : α
hb : IsMin b
pos : ¬succ a ≤ pred b
⊢ Icc (succ a) (pred b) = Ioo a b

Tactic:
rw [Icc_eq_empty, Ioo_eq_empty hb.not_lt]

Premises used: Set.Icc_eq_empty, IsMin.not_lt, Set.Ioo_eq_empty
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
inst_3 : Nontrivial α
a b : α
hb : IsMin b
⊢ ¬succ a ≤ pred b

Tactic:
fun h ↦ not_isMin_succ _ <| hb.mono <| h.trans <| pred_le _

Premises used: Order.not_isMin_succ, IsMin.mono, Order.pred_le, LE.le.trans, Not
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
inst_3 : Nontrivial α
a b : α
hb : IsMin b
⊢ ¬succ a ≤ pred b

Tactic:
exact fun h ↦ not_isMin_succ _ <| hb.mono <| h.trans <| pred_le _

Premises used: Order.not_isMin_succ, IsMin.mono
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
inst_3 : Nontrivial α
a b : α
hb : ¬IsMin b
neg : Ico (succ a) b = Ioo a b
neg₁ neg₂ : Ioo a b = Ioo a b
⊢ Icc (succ a) (pred b) = Ioo a b

Tactic:
rw [Icc_pred_right_eq_Ico_of_not_isMin hb, Ico_succ_left_eq_Ioo]

Premises used: Set.Ico_succ_left_eq_Ioo, Set.Icc_pred_right_eq_Ico_of_not_isMin
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
b : α
hb : ¬IsMax b
h : ∀ (x : α), x ∈ Iio (succ b) ↔ x ∈ Iic b
⊢ Iio (succ b) = Iic b

Tactic:
ext x
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
b : α
hb : ¬IsMax b
x : α
h : x < succ b ↔ x ∈ Iic b
h₁ : x < succ b ↔ x ≤ b
h₂ h₃ : x ≤ b ↔ x ≤ b
⊢ x ∈ Iio (succ b) ↔ x ∈ Iic b

Tactic:
rw [mem_Iio, mem_Iic, lt_succ_iff_of_not_isMax hb]

Premises used: Set.mem_Iio, Set.mem_Iic, Order.lt_succ_iff_of_not_isMax
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : NoMaxOrder α
b : α
⊢ Iio (succ b) = Iic b

Tactic:
Iio_succ_eq_Iic_of_not_isMax (not_isMax _)

Premises used: not_isMax, Set.Iio_succ_eq_Iic_of_not_isMax
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
b : α
hb : ¬IsMin b
h : ∀ (x : α), x ∈ Iic (pred b) ↔ x ∈ Iio b
⊢ Iic (pred b) = Iio b

Tactic:
ext x
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
b : α
hb : ¬IsMin b
x : α
h : x ≤ pred b ↔ x ∈ Iio b
h₁ : x ≤ pred b ↔ x < b
h₂ h₃ : x < b ↔ x < b
⊢ x ∈ Iic (pred b) ↔ x ∈ Iio b

Tactic:
rw [mem_Iic, mem_Iio, le_pred_iff_of_not_isMin hb]

Premises used: Set.mem_Iio, Order.le_pred_iff_of_not_isMin, Set.mem_Iic
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
inst_2 : NoMinOrder α
b : α
⊢ Iic (pred b) = Iio b

Tactic:
Iic_pred_eq_Iio_of_not_isMin (not_isMin _)

Premises used: not_isMin, Set.Iic_pred_eq_Iio_of_not_isMin
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a : α
ha : ¬IsMax a
h : ∀ (x : α), x ∈ Ici (succ a) ↔ x ∈ Ioi a
⊢ Ici (succ a) = Ioi a

Tactic:
ext x
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a : α
ha : ¬IsMax a
x : α
h : succ a ≤ x ↔ x ∈ Ioi a
h₁ : succ a ≤ x ↔ a < x
h₂ h₃ : a < x ↔ a < x
⊢ x ∈ Ici (succ a) ↔ x ∈ Ioi a

Tactic:
rw [mem_Ici, mem_Ioi, succ_le_iff_of_not_isMax ha]

Premises used: Order.succ_le_iff_of_not_isMax, Set.mem_Ioi, Set.mem_Ici
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : NoMaxOrder α
a : α
⊢ Ici (succ a) = Ioi a

Tactic:
Ici_succ_eq_Ioi_of_not_isMax (not_isMax _)

Premises used: not_isMax, Set.Ici_succ_eq_Ioi_of_not_isMax
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a : α
ha : ¬IsMin a
h : ∀ (x : α), x ∈ Ioi (pred a) ↔ x ∈ Ici a
⊢ Ioi (pred a) = Ici a

Tactic:
ext x
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a : α
ha : ¬IsMin a
x : α
h : pred a < x ↔ x ∈ Ici a
h₁ : pred a < x ↔ a ≤ x
h₂ h₃ : a ≤ x ↔ a ≤ x
⊢ x ∈ Ioi (pred a) ↔ x ∈ Ici a

Tactic:
rw [mem_Ioi, mem_Ici, pred_lt_iff_of_not_isMin ha]

Premises used: Set.mem_Ioi, Set.mem_Ici, Order.pred_lt_iff_of_not_isMin
-- Module: Mathlib.Order.Interval.Set.SuccPred
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
inst_2 : NoMinOrder α
a : α
⊢ Ioi (pred a) = Ici a

Tactic:
Ioi_pred_eq_Ici_of_not_isMin (not_isMin _)

Premises used: not_isMin, Set.Ioi_pred_eq_Ici_of_not_isMin
-- Module: Mathlib.Order.Interval.Set.SurjOn
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
p : β
hp : p ∈ Ioo (f a) (f b)
rcases : ∀ (x : α) (hp : f x ∈ Ioo (f a) (f b)), f x ∈ f '' Ioo a b
⊢ p ∈ f '' Ioo a b

Tactic:
rcases h_surj p with ⟨x, rfl⟩

Premises used: rfl
-- Module: Mathlib.Order.Interval.Set.SurjOn
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b x : α
hp : f x ∈ Ioo (f a) (f b)
⊢ f x ∈ f '' Ioo a b

Tactic:
⟨x, mem_Ioo.2 ?_, rfl⟩

Premises used: Iff.mpr, Set.mem_Ioo, Set.Mem, setOf, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.Order.Interval.Set.SurjOn
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b x : α
hp : f x ∈ Ioo (f a) (f b)
refine : a < x ∧ x < b
⊢ f x ∈ f '' Ioo a b

Tactic:
refine ⟨x, mem_Ioo.2 ?_, rfl⟩
-- Module: Mathlib.Order.Interval.Set.SurjOn
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b x : α
hp : f x ∈ Ioo (f a) (f b)
contrapose! : ∀ (hp : ∀ (_ : a < x), b ≤ x), ¬f x ∈ Ioo (f a) (f b)
⊢ a < x ∧ x < b

Tactic:
contrapose! hp
-- Module: Mathlib.Order.Interval.Set.SurjOn
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b x : α
hp : ∀ (_ : a < x), b ≤ x
⊢ ¬f x ∈ Ioo (f a) (f b)

Tactic:
fun h => h.2.not_ge (h_mono <| hp <| h_mono.reflect_lt h.1)

Premises used: Monotone.reflect_lt, And.right, And.left, LT.lt.not_ge, Not
-- Module: Mathlib.Order.Interval.Set.SurjOn
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b x : α
hp : ∀ (_ : a < x), b ≤ x
⊢ ¬f x ∈ Ioo (f a) (f b)

Tactic:
exact fun h => h.2.not_ge (h_mono <| hp <| h_mono.reflect_lt h.1)
-- Module: Mathlib.Order.Interval.Set.SurjOn
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
inl : ∀ (hab : a < b), SurjOn f (Ico a b) (Ico (f a) (f b))
inr : ∀ (hab : b ≤ a), SurjOn f (Ico a b) (Ico (f a) (f b))
⊢ SurjOn f (Ico a b) (Ico (f a) (f b))

Tactic:
obtain hab | hab := lt_or_ge a b

Premises used: lt_or_ge
-- Module: Mathlib.Order.Interval.Set.SurjOn
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : a < b
p : β
hp : p ∈ Ico (f a) (f b)
inl : ∀ (hp : f a ∈ Ico (f a) (f b)), f a ∈ f '' Ico a b
inl₁ : ∀ (hp' : p ∈ Ioo (f a) (f b)), p ∈ f '' Ico a b
⊢ p ∈ f '' Ico a b

Tactic:
rcases eq_left_or_mem_Ioo_of_mem_Ico hp with (rfl | hp')

Premises used: Set.eq_left_or_mem_Ioo_of_mem_Ico, rfl
-- Module: Mathlib.Order.Interval.Set.SurjOn
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : a < b
hp : f a ∈ Ico (f a) (f b)
⊢ f a ∈ f '' Ico a b

Tactic:
mem_image_of_mem f (left_mem_Ico.mpr hab)

Premises used: Iff.mpr, Set.left_mem_Ico, Set.mem_image_of_mem
-- Module: Mathlib.Order.Interval.Set.SurjOn
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : a < b
hp : f a ∈ Ico (f a) (f b)
⊢ f a ∈ f '' Ico a b

Tactic:
exact mem_image_of_mem f (left_mem_Ico.mpr hab)

Premises used: Iff.mpr, Set.left_mem_Ico, Set.mem_image_of_mem
-- Module: Mathlib.Order.Interval.Set.SurjOn
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : a < b
p : β
hp : p ∈ Ico (f a) (f b)
hp' : p ∈ Ioo (f a) (f b)
⊢ p ∈ f '' Ico a b

Tactic:
image_mono Ioo_subset_Ico_self <|
        surjOn_Ioo_of_monotone_surjective h_mono h_surj a b hp'

Premises used: Set.image_mono, surjOn_Ioo_of_monotone_surjective, Set.Ioo_subset_Ico_self
-- Module: Mathlib.Order.Interval.Set.SurjOn
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : a < b
p : β
hp : p ∈ Ico (f a) (f b)
hp' : p ∈ Ioo (f a) (f b)
⊢ p ∈ f '' Ico a b

Tactic:
exact image_mono Ioo_subset_Ico_self <|
        surjOn_Ioo_of_monotone_surjective h_mono h_surj a b hp'

Premises used: Set.image_mono, surjOn_Ioo_of_monotone_surjective, Set.Ioo_subset_Ico_self
-- Module: Mathlib.Order.Interval.Set.SurjOn
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : b ≤ a
inr : SurjOn f (Ico a b) ∅
⊢ SurjOn f (Ico a b) (Ico (f a) (f b))

Tactic:
rw [Ico_eq_empty (h_mono hab).not_gt]

Premises used: LE.le.not_gt, Set.Ico_eq_empty
-- Module: Mathlib.Order.Interval.Set.SurjOn
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : b ≤ a
⊢ SurjOn f (Ico a b) ∅

Tactic:
surjOn_empty f _

Premises used: Set.surjOn_empty
-- Module: Mathlib.Order.Interval.Set.SurjOn
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : b ≤ a
⊢ SurjOn f (Ico a b) ∅

Tactic:
exact surjOn_empty f _

Premises used: Set.surjOn_empty
-- Module: Mathlib.Order.Interval.Set.SurjOn
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
⊢ SurjOn f (Ioc a b) (Ioc (f a) (f b))

Tactic:
simpa using surjOn_Ico_of_monotone_surjective h_mono.dual h_surj (toDual b) (toDual a)

Premises used: OrderDual.toDual, Monotone.dual, surjOn_Ico_of_monotone_surjective, DFunLike.coe
-- Module: Mathlib.Order.Interval.Set.SurjOn
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : a ≤ b
p : β
hp : p ∈ Icc (f a) (f b)
inl : ∀ (hp : f a ∈ Icc (f a) (f b)), f a ∈ f '' Icc a b
inr : ∀ (hp : f b ∈ Icc (f a) (f b)), f b ∈ f '' Icc a b
inr₁ : ∀ (hp' : p ∈ Ioo (f a) (f b)), p ∈ f '' Icc a b
⊢ p ∈ f '' Icc a b

Tactic:
rcases eq_endpoints_or_mem_Ioo_of_mem_Icc hp with (rfl | rfl | hp')

Premises used: Set.eq_endpoints_or_mem_Ioo_of_mem_Icc, rfl
-- Module: Mathlib.Order.Interval.Set.SurjOn
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : a ≤ b
hp : f a ∈ Icc (f a) (f b)
⊢ f a ∈ f '' Icc a b

Tactic:
⟨a, left_mem_Icc.mpr hab, rfl⟩

Premises used: Iff.mpr, Set.Mem, setOf, Set.left_mem_Icc, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.Order.Interval.Set.SurjOn
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : a ≤ b
hp : f a ∈ Icc (f a) (f b)
⊢ f a ∈ f '' Icc a b

Tactic:
exact ⟨a, left_mem_Icc.mpr hab, rfl⟩
-- Module: Mathlib.Order.Interval.Set.SurjOn
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : a ≤ b
hp : f b ∈ Icc (f a) (f b)
⊢ f b ∈ f '' Icc a b

Tactic:
⟨b, right_mem_Icc.mpr hab, rfl⟩

Premises used: Iff.mpr, Set.right_mem_Icc, Set.Mem, setOf, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.Order.Interval.Set.SurjOn
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : a ≤ b
hp : f b ∈ Icc (f a) (f b)
⊢ f b ∈ f '' Icc a b

Tactic:
exact ⟨b, right_mem_Icc.mpr hab, rfl⟩
-- Module: Mathlib.Order.Interval.Set.SurjOn
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : a ≤ b
p : β
hp : p ∈ Icc (f a) (f b)
hp' : p ∈ Ioo (f a) (f b)
⊢ p ∈ f '' Icc a b

Tactic:
image_mono Ioo_subset_Icc_self <|
      surjOn_Ioo_of_monotone_surjective h_mono h_surj a b hp'

Premises used: Set.Ioo_subset_Icc_self, Set.image_mono, surjOn_Ioo_of_monotone_surjective
-- Module: Mathlib.Order.Interval.Set.SurjOn
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a b : α
hab : a ≤ b
p : β
hp : p ∈ Icc (f a) (f b)
hp' : p ∈ Ioo (f a) (f b)
⊢ p ∈ f '' Icc a b

Tactic:
exact image_mono Ioo_subset_Icc_self <|
      surjOn_Ioo_of_monotone_surjective h_mono h_surj a b hp'

Premises used: Set.Ioo_subset_Icc_self, Set.image_mono, surjOn_Ioo_of_monotone_surjective
-- Module: Mathlib.Order.Interval.Set.SurjOn
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a : α
rw : SurjOn f (Iic a)ᶜ (Ioi (f a))ᶜᶜ
⊢ SurjOn f (Ioi a) (Ioi (f a))

Tactic:
rw [← compl_Iic, ← compl_compl (Ioi (f a))]

Premises used: Set.Ioi, compl_compl, Set.compl_Iic
-- Module: Mathlib.Order.Interval.Set.SurjOn
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a : α
⊢ SurjOn f (Iic a)ᶜ (Ioi (f a))ᶜᶜ

Tactic:
MapsTo.surjOn_compl ?_ h_surj

Premises used: Set.MapsTo.surjOn_compl
-- Module: Mathlib.Order.Interval.Set.SurjOn
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a : α
refine : MapsTo f (Iic a) (Ioi (f a))ᶜ
⊢ SurjOn f (Iic a)ᶜ (Ioi (f a))ᶜᶜ

Tactic:
refine MapsTo.surjOn_compl ?_ h_surj

Premises used: Set.MapsTo.surjOn_compl
-- Module: Mathlib.Order.Interval.Set.SurjOn
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a : α
⊢ MapsTo f (Iic a) (Ioi (f a))ᶜ

Tactic:
fun x hx => (h_mono hx).not_gt

Premises used: Set.Ioi, Set.Mem, setOf, LE.le.not_gt, Set.MapsTo, Not
-- Module: Mathlib.Order.Interval.Set.SurjOn
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a : α
⊢ MapsTo f (Iic a) (Ioi (f a))ᶜ

Tactic:
exact fun x hx => (h_mono hx).not_gt

Premises used: LE.le.not_gt
-- Module: Mathlib.Order.Interval.Set.SurjOn
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a : α
⊢ SurjOn f (Iio a) (Iio (f a))

Tactic:
@surjOn_Ioi_of_monotone_surjective _ _ _ _ _ h_mono.dual h_surj a

Premises used: setOf, Monotone.dual, surjOn_Ioi_of_monotone_surjective, OrderDual, Set.Iio
-- Module: Mathlib.Order.Interval.Set.SurjOn
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a : α
rw : SurjOn f (Ioi a ∪ {a}) (Ioi (f a) ∪ {f a})
⊢ SurjOn f (Ici a) (Ici (f a))

Tactic:
rw [← Ioi_union_left, ← Ioi_union_left]

Premises used: Set.Ioi_union_left
-- Module: Mathlib.Order.Interval.Set.SurjOn
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a : α
⊢ SurjOn f (Ioi a ∪ {a}) (Ioi (f a) ∪ {f a})

Tactic:
(surjOn_Ioi_of_monotone_surjective h_mono h_surj a).union_union
      (@image_singleton _ _ f a ▸ surjOn_image _ _)

Premises used: Set.SurjOn.union_union, Set.surjOn_image, Set.image_singleton, Eq.rec, surjOn_Ioi_of_monotone_surjective
-- Module: Mathlib.Order.Interval.Set.SurjOn
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a : α
⊢ SurjOn f (Ioi a ∪ {a}) (Ioi (f a) ∪ {f a})

Tactic:
exact
    (surjOn_Ioi_of_monotone_surjective h_mono h_surj a).union_union
      (@image_singleton _ _ f a ▸ surjOn_image _ _)

Premises used: Set.SurjOn.union_union, surjOn_Ioi_of_monotone_surjective
-- Module: Mathlib.Order.Interval.Set.SurjOn
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a : α
⊢ SurjOn f (Iic a) (Iic (f a))

Tactic:
@surjOn_Ici_of_monotone_surjective _ _ _ _ _ h_mono.dual h_surj a

Premises used: setOf, Monotone.dual, Set.Iic, OrderDual, surjOn_Ici_of_monotone_surjective
-- Module: Mathlib.Order.Interval.Set.Union
Goal:
X : Type u_1
inst : LinearOrder X
a : ℕ → X
⊢ Ioc (a 0) (a 0) ⊆ ⋃ i ∈ Finset.range 0, Ioc (a i) (a (i + 1))

Tactic:
simp