awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
h : a < b
rw : Icc (succ a) b = Ioc a b
⊢ insert (succ a) (Ioc (succ a) b) = Ioc a b
have rw₁ : Ioc a b = Ioc a b
Tactic: rw [Ioc_insert_left (succ_le_of_lt h), Icc_succ_left_of_not_isMax h.not_isMax]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a b : α
⊢ Ioc a (pred b) = Ioo a b
have pos : ∀ (hb : IsMin b), Ioc a (pred b) = Ioo a b
Tactic: by_cases hb : IsMin b
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a b : α
pos : ∀ (hb : IsMin b), Ioc a (pred b) = Ioo a b
⊢ Ioc a (pred b) = Ioo a b
have neg : ∀ (hb : ¬IsMin b), Ioc a (pred b) = Ioo a b
Tactic: by_cases hb : IsMin b
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a b : α
hb : IsMin b
⊢ Ioc a (pred b) = Ioo a b
have pos : ∅ = Ioo a b
Tactic: rw [Ioc_eq_empty (hb.mono <| pred_le _).not_lt, Ioo_eq_empty hb.not_lt]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a b : α
hb : IsMin b
pos : ∅ = Ioo a b
⊢ Ioc a (pred b) = Ioo a b
have pos₁ : Eq.{u_1 + 1} (α := Set α) ∅ ∅
Tactic: rw [Ioc_eq_empty (hb.mono <| pred_le _).not_lt, Ioo_eq_empty hb.not_lt]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a b : α
hb : ¬IsMin b
⊢ Ioc a (pred b) = Ioo a b
have neg : ∀ (x : α), x ∈ Ioc a (pred b) ↔ x ∈ Ioo a b
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a b : α
hb : ¬IsMin b
x : α
⊢ x ∈ Ioc a (pred b) ↔ x ∈ Ioo a b
have neg : a < x ∧ x ≤ pred b ↔ x ∈ Ioo a b
Tactic: rw [mem_Ioc, mem_Ioo, le_pred_iff_of_not_isMin hb]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a b : α
hb : ¬IsMin b
x : α
neg : a < x ∧ x ≤ pred b ↔ x ∈ Ioo a b
⊢ x ∈ Ioc a (pred b) ↔ x ∈ Ioo a b
have neg₁ : a < x ∧ x ≤ pred b ↔ a < x ∧ x < b
Tactic: rw [mem_Ioc, mem_Ioo, le_pred_iff_of_not_isMin hb]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a b : α
hb : ¬IsMin b
x : α
neg : a < x ∧ x ≤ pred b ↔ x ∈ Ioo a b
neg₁ : a < x ∧ x ≤ pred b ↔ a < x ∧ x < b
⊢ x ∈ Ioc a (pred b) ↔ x ∈ Ioo a b
have neg₂ : a < x ∧ x < b ↔ a < x ∧ x < b
Tactic: rw [mem_Ioc, mem_Ioo, le_pred_iff_of_not_isMin hb]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
b : α
hb : ¬IsMin b
a : α
⊢ Icc a (pred b) = Ico a b
have h : ∀ (x : α), x ∈ Icc a (pred b) ↔ x ∈ Ico a b
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
b : α
hb : ¬IsMin b
a x : α
⊢ x ∈ Icc a (pred b) ↔ x ∈ Ico a b
have h : a ≤ x ∧ x ≤ pred b ↔ x ∈ Ico a b
Tactic: rw [mem_Icc, mem_Ico, le_pred_iff_of_not_isMin hb]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
b : α
hb : ¬IsMin b
a x : α
h : a ≤ x ∧ x ≤ pred b ↔ x ∈ Ico a b
⊢ x ∈ Icc a (pred b) ↔ x ∈ Ico a b
have h₁ : a ≤ x ∧ x ≤ pred b ↔ a ≤ x ∧ x < b
Tactic: rw [mem_Icc, mem_Ico, le_pred_iff_of_not_isMin hb]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
b : α
hb : ¬IsMin b
a x : α
h : a ≤ x ∧ x ≤ pred b ↔ x ∈ Ico a b
h₁ : a ≤ x ∧ x ≤ pred b ↔ a ≤ x ∧ x < b
⊢ x ∈ Icc a (pred b) ↔ x ∈ Ico a b
have h₂ : a ≤ x ∧ x < b ↔ a ≤ x ∧ x < b
Tactic: rw [mem_Icc, mem_Ico, le_pred_iff_of_not_isMin hb]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ioc (pred a) b = Icc a b
have h : ∀ (x : α), x ∈ Ioc (pred a) b ↔ x ∈ Icc a b
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a : α
ha : ¬IsMin a
b x : α
⊢ x ∈ Ioc (pred a) b ↔ x ∈ Icc a b
have h : pred a < x ∧ x ≤ b ↔ x ∈ Icc a b
Tactic: rw [mem_Ioc, mem_Icc, pred_lt_iff_of_not_isMin ha]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
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
⊢ x ∈ Ioc (pred a) b ↔ x ∈ Icc a b
have h₁ : pred a < x ∧ x ≤ b ↔ a ≤ x ∧ x ≤ b
Tactic: rw [mem_Ioc, mem_Icc, pred_lt_iff_of_not_isMin ha]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
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
⊢ x ∈ Ioc (pred a) b ↔ x ∈ Icc a b
have h₂ : a ≤ x ∧ x ≤ b ↔ a ≤ x ∧ x ≤ b
Tactic: rw [mem_Ioc, mem_Icc, pred_lt_iff_of_not_isMin ha]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ioo (pred a) b = Ico a b
have h : ∀ (x : α), x ∈ Ioo (pred a) b ↔ x ∈ Ico a b
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a : α
ha : ¬IsMin a
b x : α
⊢ x ∈ Ioo (pred a) b ↔ x ∈ Ico a b
have h : pred a < x ∧ x < b ↔ x ∈ Ico a b
Tactic: rw [mem_Ioo, mem_Ico, pred_lt_iff_of_not_isMin ha]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
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
⊢ x ∈ Ioo (pred a) b ↔ x ∈ Ico a b
have h₁ : pred a < x ∧ x < b ↔ a ≤ x ∧ x < b
Tactic: rw [mem_Ioo, mem_Ico, pred_lt_iff_of_not_isMin ha]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
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
⊢ x ∈ Ioo (pred a) b ↔ x ∈ Ico a b
have h₂ : a ≤ x ∧ x < b ↔ a ≤ x ∧ x < b
Tactic: rw [mem_Ioo, mem_Ico, pred_lt_iff_of_not_isMin ha]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a : α
ha : ¬IsMin a
b : α
⊢ Ioc (pred a) (pred b) = Ico a b
have rw : Ioo (pred a) b = Ico a b
Tactic: rw [Ioc_pred_right_eq_Ioo, Ioo_pred_left_eq_Ioc_of_not_isMin ha]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a : α
ha : ¬IsMin a
b : α
rw : Ioo (pred a) b = Ico a b
⊢ Ioc (pred a) (pred b) = Ico a b
have rw₁ : Ico a b = Ico a b
Tactic: rw [Ioc_pred_right_eq_Ioo, Ioo_pred_left_eq_Ioc_of_not_isMin ha]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a b : α
h : a ≤ b
⊢ insert b (Icc a (pred b)) = Icc a b
have h₁ : ∀ (x : α), x ∈ insert b (Icc a (pred b)) ↔ x ∈ Icc a b
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a b : α
h : a ≤ b
x : α
⊢ x ∈ insert b (Icc a (pred b)) ↔ x ∈ Icc a b
have h₁ : x ≤ b → x = b → a ≤ x
Tactic: simp [or_and_left, ← le_iff_eq_or_le_pred]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a b : α
h : pred a ≤ b
⊢ insert (pred a) (Icc a b) = Icc (pred a) b
have h₁ : ∀ (x : α), x ∈ insert (pred a) (Icc a b) ↔ x ∈ Icc (pred a) b
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a b : α
h : pred a ≤ b
x : α
⊢ x ∈ insert (pred a) (Icc a b) ↔ x ∈ Icc (pred a) b
have h₁ : x = pred a ∨ a ≤ x → x = pred a → x ≤ b
Tactic: simp [or_and_left, pred_le_iff_eq_or_le]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a b : α
h : a ≤ b
ha : ¬IsMin a
⊢ insert a (Ioc a b) = Ioc (pred a) b
have rw : insert a (Ioc a b) = Icc a b
Tactic: rw [Ioc_pred_left_of_not_isMin ha, Ioc_insert_left h]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
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
⊢ insert a (Ioc a b) = Ioc (pred a) b
have rw₁ : Icc a b = Icc a b
Tactic: rw [Ioc_pred_left_of_not_isMin ha, Ioc_insert_left h]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a b : α
h : a < b
⊢ insert b (Ioc a (pred b)) = Ioc a b
have rw : insert b (Ioo a b) = Ioc a b
Tactic: rw [Ioc_pred_right_of_not_isMin h.not_isMin, Ioo_insert_right h]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a b : α
h : a < b
rw : insert b (Ioo a b) = Ioc a b
⊢ insert b (Ioc a (pred b)) = Ioc a b
have rw₁ : Ioc a b = Ioc a b
Tactic: rw [Ioc_pred_right_of_not_isMin h.not_isMin, Ioo_insert_right h]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a b : α
h : a ≤ b
ha : ¬IsMin a
⊢ insert (pred a) (Ico a b) = Ico (pred a) b
have h₁ : ∀ (x : α), x ∈ insert (pred a) (Ico a b) ↔ x ∈ Ico (pred a) b
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a b : α
h : a < b
⊢ insert (pred b) (Ico a (pred b)) = Ico a b
have rw : Icc 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]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a b : α
h : a < b
rw : Icc a (pred b) = Ico a b
⊢ insert (pred b) (Ico a (pred b)) = Ico a b
have rw₁ : Ico a b = Ico a b
Tactic: rw [Ico_insert_right (le_pred_of_lt h), Icc_pred_right_of_not_isMin h.not_isMin]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
inst_3 : Nontrivial α
a b : α
⊢ Icc (succ a) (pred b) = Ioo a b
have pos : ∀ (hb : IsMin b), Icc (succ a) (pred b) = Ioo a b
Tactic: by_cases hb : IsMin b
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
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
⊢ Icc (succ a) (pred b) = Ioo a b
have neg : ∀ (hb : ¬IsMin b), Icc (succ a) (pred b) = Ioo a b
Tactic: by_cases hb : IsMin b
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
inst_3 : Nontrivial α
a b : α
hb : IsMin b
⊢ Icc (succ a) (pred b) = Ioo a b
have pos : ¬succ a ≤ pred b
Tactic: rw [Icc_eq_empty, Ioo_eq_empty hb.not_lt]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : PredOrder α
inst_3 : Nontrivial α
a b : α
hb : ¬IsMin b
⊢ Icc (succ a) (pred b) = Ioo a b
have neg : Ico (succ a) b = Ioo a b
Tactic: rw [Icc_pred_right_eq_Ico_of_not_isMin hb, Ico_succ_left_eq_Ioo]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
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
⊢ Icc (succ a) (pred b) = Ioo a b
have neg₁ : Ioo a b = Ioo a b
Tactic: rw [Icc_pred_right_eq_Ico_of_not_isMin hb, Ico_succ_left_eq_Ioo]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
b : α
hb : ¬IsMax b
⊢ Iio (succ b) = Iic b
have h : ∀ (x : α), x ∈ Iio (succ b) ↔ x ∈ Iic b
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
b : α
hb : ¬IsMax b
x : α
⊢ x ∈ Iio (succ b) ↔ x ∈ Iic b
have h : x < succ b ↔ x ∈ Iic b
Tactic: rw [mem_Iio, mem_Iic, lt_succ_iff_of_not_isMax hb]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
b : α
hb : ¬IsMax b
x : α
h : x < succ b ↔ x ∈ Iic b
⊢ x ∈ Iio (succ b) ↔ x ∈ Iic b
have h₁ : x < succ b ↔ x ≤ b
Tactic: rw [mem_Iio, mem_Iic, lt_succ_iff_of_not_isMax hb]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
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
⊢ x ∈ Iio (succ b) ↔ x ∈ Iic b
have h₂ : x ≤ b ↔ x ≤ b
Tactic: rw [mem_Iio, mem_Iic, lt_succ_iff_of_not_isMax hb]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
b : α
hb : ¬IsMin b
⊢ Iic (pred b) = Iio b
have h : ∀ (x : α), x ∈ Iic (pred b) ↔ x ∈ Iio b
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
b : α
hb : ¬IsMin b
x : α
⊢ x ∈ Iic (pred b) ↔ x ∈ Iio b
have h : x ≤ pred b ↔ x ∈ Iio b
Tactic: rw [mem_Iic, mem_Iio, le_pred_iff_of_not_isMin hb]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
b : α
hb : ¬IsMin b
x : α
h : x ≤ pred b ↔ x ∈ Iio b
⊢ x ∈ Iic (pred b) ↔ x ∈ Iio b
have h₁ : x ≤ pred b ↔ x < b
Tactic: rw [mem_Iic, mem_Iio, le_pred_iff_of_not_isMin hb]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
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
⊢ x ∈ Iic (pred b) ↔ x ∈ Iio b
have h₂ : x < b ↔ x < b
Tactic: rw [mem_Iic, mem_Iio, le_pred_iff_of_not_isMin hb]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a : α
ha : ¬IsMax a
⊢ Ici (succ a) = Ioi a
have h : ∀ (x : α), x ∈ Ici (succ a) ↔ x ∈ Ioi a
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a : α
ha : ¬IsMax a
x : α
⊢ x ∈ Ici (succ a) ↔ x ∈ Ioi a
have h : succ a ≤ x ↔ x ∈ Ioi a
Tactic: rw [mem_Ici, mem_Ioi, succ_le_iff_of_not_isMax ha]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a : α
ha : ¬IsMax a
x : α
h : succ a ≤ x ↔ x ∈ Ioi a
⊢ x ∈ Ici (succ a) ↔ x ∈ Ioi a
have h₁ : succ a ≤ x ↔ a < x
Tactic: rw [mem_Ici, mem_Ioi, succ_le_iff_of_not_isMax ha]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
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
⊢ x ∈ Ici (succ a) ↔ x ∈ Ioi a
have h₂ : a < x ↔ a < x
Tactic: rw [mem_Ici, mem_Ioi, succ_le_iff_of_not_isMax ha]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a : α
ha : ¬IsMin a
⊢ Ioi (pred a) = Ici a
have h : ∀ (x : α), x ∈ Ioi (pred a) ↔ x ∈ Ici a
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a : α
ha : ¬IsMin a
x : α
⊢ x ∈ Ioi (pred a) ↔ x ∈ Ici a
have h : pred a < x ↔ x ∈ Ici a
Tactic: rw [mem_Ioi, mem_Ici, pred_lt_iff_of_not_isMin ha]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
a : α
ha : ¬IsMin a
x : α
h : pred a < x ↔ x ∈ Ici a
⊢ x ∈ Ioi (pred a) ↔ x ∈ Ici a
have h₁ : pred a < x ↔ a ≤ x
Tactic: rw [mem_Ioi, mem_Ici, pred_lt_iff_of_not_isMin ha]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
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
⊢ x ∈ Ioi (pred a) ↔ x ∈ Ici a
have h₂ : a ≤ x ↔ a ≤ x
Tactic: rw [mem_Ioi, mem_Ici, pred_lt_iff_of_not_isMin ha]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SurjOn (goal)
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)
⊢ p ∈ f '' Ioo a b
have rcases : ∀ (x : α) (hp : f x ∈ Ioo (f a) (f b)), f x ∈ f '' Ioo a b
Tactic: rcases h_surj p with ⟨x, rfl⟩
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SurjOn (goal)
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
have refine : a < x ∧ x < b
Tactic: refine ⟨x, mem_Ioo.2 ?_, rfl⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SurjOn (goal)
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)
⊢ a < x ∧ x < b
have contrapose! : ∀ (hp : ∀ (_ : a < x), b ≤ x), ¬f x ∈ Ioo (f a) (f b)
Tactic: contrapose! hp
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SurjOn (goal)
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 (Ico a b) (Ico (f a) (f b))
have inl : ∀ (hab : a < b), SurjOn f (Ico a b) (Ico (f a) (f b))
Tactic: obtain hab | hab := lt_or_ge a b
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SurjOn (goal)
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))
⊢ SurjOn f (Ico a b) (Ico (f a) (f b))
have inr : ∀ (hab : b ≤ a), SurjOn f (Ico a b) (Ico (f a) (f b))
Tactic: obtain hab | hab := lt_or_ge a b
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SurjOn (goal)
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)
⊢ p ∈ f '' Ico a b
have inl : ∀ (hp : f a ∈ Ico (f a) (f b)), f a ∈ f '' Ico a b
Tactic: rcases eq_left_or_mem_Ioo_of_mem_Ico hp with (rfl | hp')
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SurjOn (goal)
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
⊢ p ∈ f '' Ico a b
have inl₁ : ∀ (hp' : p ∈ Ioo (f a) (f b)), p ∈ f '' Ico a b
Tactic: rcases eq_left_or_mem_Ioo_of_mem_Ico hp with (rfl | hp')
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SurjOn (goal)
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) (Ico (f a) (f b))
have inr : SurjOn f (Ico a b) ∅
Tactic: rw [Ico_eq_empty (h_mono hab).not_gt]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SurjOn (goal)
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)
⊢ p ∈ f '' Icc a b
have inl : ∀ (hp : f a ∈ Icc (f a) (f b)), f a ∈ f '' Icc a b
Tactic: rcases eq_endpoints_or_mem_Ioo_of_mem_Icc hp with (rfl | rfl | hp')
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SurjOn (goal)
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
⊢ p ∈ f '' Icc a b
have inr : ∀ (hp : f b ∈ Icc (f a) (f b)), f b ∈ f '' Icc a b
Tactic: rcases eq_endpoints_or_mem_Ioo_of_mem_Icc hp with (rfl | rfl | hp')
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SurjOn (goal)
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
⊢ p ∈ f '' Icc a b
have inr₁ : ∀ (hp' : p ∈ Ioo (f a) (f b)), p ∈ f '' Icc a b
Tactic: rcases eq_endpoints_or_mem_Ioo_of_mem_Icc hp with (rfl | rfl | hp')
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SurjOn (goal)
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) (Ioi (f a))
have rw : SurjOn f (Iic a)ᶜ (Ioi (f a))ᶜᶜ
Tactic: rw [← compl_Iic, ← compl_compl (Ioi (f a))]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SurjOn (goal)
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))ᶜᶜ
have refine : MapsTo f (Iic a) (Ioi (f a))ᶜ
Tactic: refine MapsTo.surjOn_compl ?_ h_surj
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SurjOn (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a : α
⊢ SurjOn f (Ici a) (Ici (f a))
have rw : SurjOn f (Ioi a ∪ {a}) (Ioi (f a) ∪ {f a})
Tactic: rw [← Ioi_union_left, ← Ioi_union_left]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Union (goal)
Goal:
X : Type u_1
inst : LinearOrder X
a : ℕ → X
N : ℕ
ih : Ioc (a 0) (a N) ⊆ ⋃ i ∈ Finset.range N, Ioc (a i) (a (i + 1))
⊢ Ioc (a 0) (a (N + 1)) ⊆ ⋃ i ∈ Finset.range (N + 1), Ioc (a i) (a (i + 1))
have _ : Ioc (a 0) (a N) ∪ Ioc (a N) (a (N + 1)) ⊆ ⋃ i ∈ Finset.range (N + 1), Ioc (a i) (a (i + 1))
Tactic: calc
    _ ⊆ Ioc (a 0) (a N) ∪ Ioc (a N) (a (N + 1)) := Ioc_subset_Ioc_union_Ioc
    _ ⊆ _ := by simpa [Finset.range_add_one] using
                  union_subset_union_right (Ioc (a N) (a (N + 1))) ih
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Union (goal)
Goal:
X : Type u_1
inst : LinearOrder X
N : ℕ
a : ℕ → X
⊢ Ioc (a 0) (a N) ⊆ ⋃ i ∈ Finset.range N, Ioc (a i) (a (i + 1))
have zero : Ioc (a 0) (a 0) ⊆ ⋃ i ∈ Finset.range 0, Ioc (a i) (a (i + 1))
Tactic: induction N with
  | zero => simp
  | succ N ih => calc
    _ ⊆ Ioc (a 0) (a N) ∪ Ioc (a N) (a (N + 1)) := Ioc_subset_Ioc_union_Ioc
    _ ⊆ _ := by simpa [Finset.range_add_one] using
                  union_subset_union_right (Ioc (a N) (a (N + 1))) ih
Cleared hypotheses: N
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Union (goal)
Goal:
X : Type u_1
inst : LinearOrder X
N : ℕ
a : ℕ → X
zero : Ioc (a 0) (a 0) ⊆ ⋃ i ∈ Finset.range 0, Ioc (a i) (a (i + 1))
⊢ Ioc (a 0) (a N) ⊆ ⋃ i ∈ Finset.range N, Ioc (a i) (a (i + 1))
have succ : ∀ (N : ℕ) (ih : Ioc (a 0) (a N) ⊆ ⋃ i ∈ Finset.range N, Ioc (a i) (a (i + 1))),
  Ioc (a 0) (a (N + 1)) ⊆ ⋃ i ∈ Finset.range (N + 1), Ioc (a i) (a (i + 1))
Tactic: induction N with
  | zero => simp
  | succ N ih => calc
    _ ⊆ Ioc (a 0) (a N) ∪ Ioc (a N) (a (N + 1)) := Ioc_subset_Ioc_union_Ioc
    _ ⊆ _ := by simpa [Finset.range_add_one] using
                  union_subset_union_right (Ioc (a N) (a (N + 1))) ih
Cleared hypotheses: N