awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
mp : ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mpr : a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mp₁ mp₂ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mp₃ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ c
mp₄ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ b
mpr₁ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₂ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₃ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₄ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₅ : a ≤ b → a ≤ c → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mpr₆ : ¬a ≤ c → ¬a ≤ b → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mp₅ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ b → False
mp₆ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ c → False
mp₇ : a ≤ c → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ b → False
mp₈ : a ≤ c → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ c → False
mp₉ : a ≤ c → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ b → False
mp₁₀ : a ≤ c → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ c → False
mp₁₁ : a ≤ c → ¬a ≤ c → ¬a ≤ b → ¬a ≤ b → False
mp₁₂ : a ≤ c → ¬a ≤ c → ¬a ≤ b → ¬a ≤ c → False
mp₁₃ : a ≤ b → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ b → False
mp₁₄ : a ≤ b → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ c → False
mp₁₅ : a ≤ b → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ b → False
mp₁₆ : a ≤ b → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ c → False
mp₁₇ : a ≤ b → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ b → False
mp₁₈ : a ≤ b → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ c → False
mp₁₉ : a ≤ b → ¬a ≤ c → ¬a ≤ b → ¬a ≤ b → False
mp₂₀ : a ≤ b → ¬a ≤ c → ¬a ≤ b → ¬a ≤ c → False
⊢ ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) ↔ a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
have mpr₇ : a ≤ b → a ≤ c → ¬a ≤ b → a ≤ c → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
mp : ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mpr : a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mp₁ mp₂ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mp₃ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ c
mp₄ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ b
mpr₁ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₂ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₃ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₄ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₅ : a ≤ b → a ≤ c → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mpr₆ : ¬a ≤ c → ¬a ≤ b → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mp₅ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ b → False
mp₆ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ c → False
mp₇ : a ≤ c → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ b → False
mp₈ : a ≤ c → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ c → False
mp₉ : a ≤ c → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ b → False
mp₁₀ : a ≤ c → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ c → False
mp₁₁ : a ≤ c → ¬a ≤ c → ¬a ≤ b → ¬a ≤ b → False
mp₁₂ : a ≤ c → ¬a ≤ c → ¬a ≤ b → ¬a ≤ c → False
mp₁₃ : a ≤ b → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ b → False
mp₁₄ : a ≤ b → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ c → False
mp₁₅ : a ≤ b → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ b → False
mp₁₆ : a ≤ b → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ c → False
mp₁₇ : a ≤ b → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ b → False
mp₁₈ : a ≤ b → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ c → False
mp₁₉ : a ≤ b → ¬a ≤ c → ¬a ≤ b → ¬a ≤ b → False
mp₂₀ : a ≤ b → ¬a ≤ c → ¬a ≤ b → ¬a ≤ c → False
mpr₇ : a ≤ b → a ≤ c → ¬a ≤ b → a ≤ c → False
⊢ ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) ↔ a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
have mpr₈ : a ≤ b → a ≤ c → ¬a ≤ c → a ≤ b → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
mp : ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mpr : a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mp₁ mp₂ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mp₃ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ c
mp₄ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ b
mpr₁ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₂ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₃ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₄ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₅ : a ≤ b → a ≤ c → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mpr₆ : ¬a ≤ c → ¬a ≤ b → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mp₅ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ b → False
mp₆ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ c → False
mp₇ : a ≤ c → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ b → False
mp₈ : a ≤ c → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ c → False
mp₉ : a ≤ c → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ b → False
mp₁₀ : a ≤ c → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ c → False
mp₁₁ : a ≤ c → ¬a ≤ c → ¬a ≤ b → ¬a ≤ b → False
mp₁₂ : a ≤ c → ¬a ≤ c → ¬a ≤ b → ¬a ≤ c → False
mp₁₃ : a ≤ b → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ b → False
mp₁₄ : a ≤ b → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ c → False
mp₁₅ : a ≤ b → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ b → False
mp₁₆ : a ≤ b → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ c → False
mp₁₇ : a ≤ b → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ b → False
mp₁₈ : a ≤ b → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ c → False
mp₁₉ : a ≤ b → ¬a ≤ c → ¬a ≤ b → ¬a ≤ b → False
mp₂₀ : a ≤ b → ¬a ≤ c → ¬a ≤ b → ¬a ≤ c → False
mpr₇ : a ≤ b → a ≤ c → ¬a ≤ b → a ≤ c → False
mpr₈ : a ≤ b → a ≤ c → ¬a ≤ c → a ≤ b → False
⊢ ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) ↔ a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
have mpr₉ : ¬a ≤ c → ¬a ≤ b → ¬a ≤ b → a ≤ c → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
mp : ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mpr : a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mp₁ mp₂ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
mp₃ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ c
mp₄ : ¬(¬a ≤ b ∧ a ≤ c) → ¬(¬a ≤ c ∧ a ≤ b) → ¬(a ≤ b ∧ a ≤ c) → ¬a ≤ b
mpr₁ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₂ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₃ : a ≤ b → a ≤ c → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₄ : ¬a ≤ c → ¬a ≤ b → ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b)
mpr₅ : a ≤ b → a ≤ c → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mpr₆ : ¬a ≤ c → ¬a ≤ b → ¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b → False
mp₅ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ b → False
mp₆ : a ≤ c → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ c → False
mp₇ : a ≤ c → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ b → False
mp₈ : a ≤ c → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ c → False
mp₉ : a ≤ c → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ b → False
mp₁₀ : a ≤ c → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ c → False
mp₁₁ : a ≤ c → ¬a ≤ c → ¬a ≤ b → ¬a ≤ b → False
mp₁₂ : a ≤ c → ¬a ≤ c → ¬a ≤ b → ¬a ≤ c → False
mp₁₃ : a ≤ b → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ b → False
mp₁₄ : a ≤ b → ¬¬a ≤ b → ¬¬a ≤ c → ¬a ≤ c → False
mp₁₅ : a ≤ b → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ b → False
mp₁₆ : a ≤ b → ¬¬a ≤ b → ¬a ≤ b → ¬a ≤ c → False
mp₁₇ : a ≤ b → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ b → False
mp₁₈ : a ≤ b → ¬a ≤ c → ¬¬a ≤ c → ¬a ≤ c → False
mp₁₉ : a ≤ b → ¬a ≤ c → ¬a ≤ b → ¬a ≤ b → False
mp₂₀ : a ≤ b → ¬a ≤ c → ¬a ≤ b → ¬a ≤ c → False
mpr₇ : a ≤ b → a ≤ c → ¬a ≤ b → a ≤ c → False
mpr₈ : a ≤ b → a ≤ c → ¬a ≤ c → a ≤ b → False
mpr₉ : ¬a ≤ c → ¬a ≤ b → ¬a ≤ b → a ≤ c → False
⊢ ¬(¬a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ a ≤ b) ↔ a ≤ b ∧ a ≤ c ∨ ¬a ≤ c ∧ ¬a ≤ b
have mpr₁₀ : ¬a ≤ c → ¬a ≤ b → ¬a ≤ c → a ≤ b → False
Tactic: tauto
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
⊢ a ∈ Ι b c → b ∈ Ι a c → a = b
have simp_rw : b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b → a < b ∧ b ≤ c ∨ c < b ∧ b ≤ a → a = b
Tactic: simp_rw [mem_uIoc]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
left : b < a
right : a ≤ c
left_1 : a < b
right_1 : b ≤ c
⊢ a = b
have inl : a ≤ b
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
left : b < a
right : a ≤ c
left_1 : a < b
right_1 : b ≤ c
inl : a ≤ b
⊢ a = b
have inl₁ : b ≤ a
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
left : b < a
right : a ≤ c
left_1 : c < b
right_1 : b ≤ a
⊢ a = b
have inl : a ≤ b
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
left : c < a
right : a ≤ b
left_1 : a < b
right_1 : b ≤ c
inr : a ≤ b
⊢ a = b
have inr₁ : b ≤ a
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h : Eq.{u_1 + 1} (α := Set α) ((fun (b : α) ↦ Ι b a) b) ((fun (b : α) ↦ Ι b a) c)
⊢ b = c
have h₁ : ∀ (x : α),
  Membership.mem (γ := Set α) ((fun (b : α) ↦ Ι b a) b) x ↔ Membership.mem (γ := Set α) ((fun (b : α) ↦ Ι b a) c) x
Tactic: rw [Set.ext_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) ((fun (b : α) ↦ Ι b a) b) x ↔ Membership.mem (γ := Set α) ((fun (b : α) ↦ Ι b a) c) x
⊢ b = c
have inl : ∀ (ha : b ≤ a), b = c
Tactic: obtain ha | ha := le_or_gt b a
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) ((fun (b : α) ↦ Ι b a) b) x ↔ Membership.mem (γ := Set α) ((fun (b : α) ↦ Ι b a) c) x
inl : ∀ (ha : b ≤ a), b = c
⊢ b = c
have inr : ∀ (ha : a < b), b = c
Tactic: obtain ha | ha := le_or_gt b a
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) ((fun (b : α) ↦ Ι b a) b) x ↔ Membership.mem (γ := Set α) ((fun (b : α) ↦ Ι b a) c) x
ha : b ≤ a
⊢ b = c
have hb : b ∉ (fun (b : α) ↦ Ι b a) b ↔ b ∉ (fun (b : α) ↦ Ι b a) c
Tactic: have hb := (h b).not
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) ((fun (b : α) ↦ Ι b a) b) x ↔ Membership.mem (γ := Set α) ((fun (b : α) ↦ Ι b a) c) x
ha : b ≤ a
hb : b ∉ (fun (b : α) ↦ Ι b a) b ↔ b ∉ (fun (b : α) ↦ Ι b a) c
⊢ b = c
have hb₁ : b ≤ c
Tactic: simp only [ha, left_mem_uIoc, true_iff, notMem_uIoc, ← not_le,
      and_true, not_true, false_and, not_false_iff, or_false] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) ((fun (b : α) ↦ Ι b a) b) x ↔ Membership.mem (γ := Set α) ((fun (b : α) ↦ Ι b a) c) x
ha : b ≤ a
hb : b ≤ c
⊢ b = c
have inl : ∀ (hc : b < c), False
Tactic: refine hb.eq_of_not_lt fun hc => ?_
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) ((fun (b : α) ↦ Ι b a) b) x ↔ Membership.mem (γ := Set α) ((fun (b : α) ↦ Ι b a) c) x
ha : a < b
⊢ b = c
have inr : b ≤ c
Tactic: refine
      eq_of_mem_uIoc_of_mem_uIoc ((h _).1 <| left_mem_uIoc.2 ha)
        ((h _).2 <| left_mem_uIoc.2 <| ha.trans_le ?_)
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h : b ∈ [[a, c]]
⊢ Ι a b ∪ Ι b c = Ι a c
have inr : ∀ (this : ∀ {a c : α} (h : b ∈ [[a, c]]) (hac : a ≤ c), Ι a b ∪ Ι b c = Ι a c) (hac : ¬a ≤ c), Ι a b ∪ Ι b c = Ι a c
Tactic: wlog hac : a ≤ c generalizing a c
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h : b ∈ [[a, c]]
inr :
  ∀ (this : ∀ {a c : α} (h : b ∈ [[a, c]]) (hac : a ≤ c), Ι a b ∪ Ι b c = Ι a c) (hac : ¬a ≤ c), Ι a b ∪ Ι b c = Ι a c
⊢ Ι a b ∪ Ι b c = Ι a c
have wlog : ∀ {a c : α} (h : b ∈ [[a, c]]) (hac : a ≤ c), Ι a b ∪ Ι b c = Ι a c
Tactic: wlog hac : a ≤ c generalizing a c
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h : b ∈ [[a, c]]
this : ∀ {a c : α} (h : b ∈ [[a, c]]) (hac : a ≤ c), Ι a b ∪ Ι b c = Ι a c
hac : ¬a ≤ c
⊢ Ι a b ∪ Ι b c = Ι a c
have rw : b ∈ [[c, a]]
Tactic: rw [uIoc_comm, union_comm, uIoc_comm, this _ (le_of_not_ge hac), uIoc_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
a_1 b c_1 a c : α
h : b ∈ [[a, c]]
hac : a ≤ c
⊢ Ι a b ∪ Ι b c = Ι a c
have h₁ : b ∈ Icc a c
Tactic: rw [uIcc_of_le hac] at h
Cleared hypotheses: h, hac
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a_1 b c_1 a c : α
h : b ∈ Icc a c
hac : a ≤ c
⊢ Ι a b ∪ Ι b c = Ι a c
have rw : Ioc a b ∪ Ι b c = Ι a c
Tactic: rw [uIoc_of_le h.1, uIoc_of_le h.2, uIoc_of_le hac, Ioc_union_Ioc_eq_Ioc h.1 h.2]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a_1 b c_1 a c : α
h : b ∈ Icc a c
hac : a ≤ c
rw : Ioc a b ∪ Ι b c = Ι a c
⊢ Ι a b ∪ Ι b c = Ι a c
have rw₁ : Ioc a b ∪ Ioc b c = Ι a c
Tactic: rw [uIoc_of_le h.1, uIoc_of_le h.2, uIoc_of_le hac, Ioc_union_Ioc_eq_Ioc h.1 h.2]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a_1 b c_1 a c : α
h : b ∈ Icc a c
hac : a ≤ c
rw : Ioc a b ∪ Ι b c = Ι a c
rw₁ : Ioc a b ∪ Ioc b c = Ι a c
⊢ Ι a b ∪ Ι b c = Ι a c
have rw₂ : Ioc a b ∪ Ioc b c = Ioc a c
Tactic: rw [uIoc_of_le h.1, uIoc_of_le h.2, uIoc_of_le hac, Ioc_union_Ioc_eq_Ioc h.1 h.2]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a_1 b c_1 a c : α
h : b ∈ Icc a c
hac : a ≤ c
rw : Ioc a b ∪ Ι b c = Ι a c
rw₁ : Ioc a b ∪ Ioc b c = Ι a c
rw₂ : Ioc a b ∪ Ioc b c = Ioc a c
⊢ Ι a b ∪ Ι b c = Ι a c
have rw₃ : Ioc a c = Ioc a c
Tactic: rw [uIoc_of_le h.1, uIoc_of_le h.2, uIoc_of_le hac, Ioc_union_Ioc_eq_Ioc h.1 h.2]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
⊢ uIoo a b = Ioo a b
have rw : Ioo (min a b) (max a b) = Ioo a b
Tactic: rw [uIoo, inf_eq_left.2 h, sup_eq_right.2 h]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
rw : Ioo (min a b) (max a b) = Ioo a b
⊢ uIoo a b = Ioo a b
have rw₁ : Ioo a (max a b) = Ioo a b
Tactic: rw [uIoo, inf_eq_left.2 h, sup_eq_right.2 h]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
rw : Ioo (min a b) (max a b) = Ioo a b
rw₁ : Ioo a (max a b) = Ioo a b
⊢ uIoo a b = Ioo a b
have rw₂ : Ioo a b = Ioo a b
Tactic: rw [uIoo, inf_eq_left.2 h, sup_eq_right.2 h]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : b ≤ a
⊢ uIoo a b = Ioo b a
have rw : Ioo (min a b) (max a b) = Ioo b a
Tactic: rw [uIoo, inf_eq_right.2 h, sup_eq_left.2 h]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : b ≤ a
rw : Ioo (min a b) (max a b) = Ioo b a
⊢ uIoo a b = Ioo b a
have rw₁ : Ioo b (max a b) = Ioo b a
Tactic: rw [uIoo, inf_eq_right.2 h, sup_eq_left.2 h]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : b ≤ a
rw : Ioo (min a b) (max a b) = Ioo b a
rw₁ : Ioo b (max a b) = Ioo b a
⊢ uIoo a b = Ioo b a
have rw₂ : Ioo b a = Ioo b a
Tactic: rw [uIoo, inf_eq_right.2 h, sup_eq_left.2 h]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ uIoo a b = uIoo b a
have simp_rw : Ioo (min a b) (max a b) = Ioo (min b a) (max b a)
Tactic: simp_rw [uIoo, inf_comm, sup_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
simp_rw : Ioo (min a b) (max a b) = Ioo (min b a) (max b a)
⊢ uIoo a b = uIoo b a
have simp_rw₁ : Ioo (min a b) (max a b) = Ioo (min a b) (max b a)
Tactic: simp_rw [uIoo, inf_comm, sup_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ uIoo a b = Ioo a b ∪ Ioo b a
have inl : ∀ (h : a < b), uIoo a b = Ioo a b ∪ Ioo b a
Tactic: rcases lt_or_ge a b with h | h
-- Lean 4 proof step from Mathlib.Order.Interval.Set.UnorderedInterval (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
inl : ∀ (h : a < b), uIoo a b = Ioo a b ∪ Ioo b a
⊢ uIoo a b = Ioo a b ∪ Ioo b a
have inr : ∀ (h : b ≤ a), uIoo a b = Ioo a b ∪ Ioo b a
Tactic: rcases lt_or_ge a b with h | h
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
⊢ Eq.{u_1 + 1} (α := Set (WithTop α)) (range some) (Iio ⊤)
have h : ∀ (x : WithTop α),
  Membership.mem (γ := Set (WithTop α)) (range some) x ↔ Membership.mem (γ := Set (WithTop α)) (Iio ⊤) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
⊢ Eq.{u_1 + 1} (α := Set α) (some ⁻¹' Iio ⊤) univ
have rw : Eq.{u_1 + 1} (α := Set α) (some ⁻¹' range some) univ
Tactic: rw [← range_coe, preimage_range]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
rw : Eq.{u_1 + 1} (α := Set α) (some ⁻¹' range some) univ
⊢ Eq.{u_1 + 1} (α := Set α) (some ⁻¹' Iio ⊤) univ
have rw₁ : Eq.{u_1 + 1} (α := Set α) univ univ
Tactic: rw [← range_coe, preimage_range]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ some '' Ioi a = Ioo (↑a : WithTop α) ⊤
have rw : some '' some ⁻¹' Ioi (↑a : WithTop α) = Ioo (↑a : WithTop α) ⊤
Tactic: rw [← preimage_coe_Ioi, image_preimage_eq_inter_range, range_coe, Ioi_inter_Iio]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
rw : some '' some ⁻¹' Ioi (↑a : WithTop α) = Ioo (↑a : WithTop α) ⊤
⊢ some '' Ioi a = Ioo (↑a : WithTop α) ⊤
have rw₁ : Ioi (↑a : WithTop α) ∩ range some = Ioo (↑a : WithTop α) ⊤
Tactic: rw [← preimage_coe_Ioi, image_preimage_eq_inter_range, range_coe, Ioi_inter_Iio]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
rw : some '' some ⁻¹' Ioi (↑a : WithTop α) = Ioo (↑a : WithTop α) ⊤
rw₁ : Ioi (↑a : WithTop α) ∩ range some = Ioo (↑a : WithTop α) ⊤
⊢ some '' Ioi a = Ioo (↑a : WithTop α) ⊤
have rw₂ : Ioi (↑a : WithTop α) ∩ Iio ⊤ = Ioo (↑a : WithTop α) ⊤
Tactic: rw [← preimage_coe_Ioi, image_preimage_eq_inter_range, range_coe, Ioi_inter_Iio]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
rw : some '' some ⁻¹' Ioi (↑a : WithTop α) = Ioo (↑a : WithTop α) ⊤
rw₁ : Ioi (↑a : WithTop α) ∩ range some = Ioo (↑a : WithTop α) ⊤
rw₂ : Ioi (↑a : WithTop α) ∩ Iio ⊤ = Ioo (↑a : WithTop α) ⊤
⊢ some '' Ioi a = Ioo (↑a : WithTop α) ⊤
have rw₃ : Ioo (↑a : WithTop α) ⊤ = Ioo (↑a : WithTop α) ⊤
Tactic: rw [← preimage_coe_Ioi, image_preimage_eq_inter_range, range_coe, Ioi_inter_Iio]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ some '' Ici a = Ico (↑a : WithTop α) ⊤
have rw : some '' some ⁻¹' Ici (↑a : WithTop α) = Ico (↑a : WithTop α) ⊤
Tactic: rw [← preimage_coe_Ici, image_preimage_eq_inter_range, range_coe, Ici_inter_Iio]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
rw : some '' some ⁻¹' Ici (↑a : WithTop α) = Ico (↑a : WithTop α) ⊤
⊢ some '' Ici a = Ico (↑a : WithTop α) ⊤
have rw₁ : Ici (↑a : WithTop α) ∩ range some = Ico (↑a : WithTop α) ⊤
Tactic: rw [← preimage_coe_Ici, image_preimage_eq_inter_range, range_coe, Ici_inter_Iio]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
rw : some '' some ⁻¹' Ici (↑a : WithTop α) = Ico (↑a : WithTop α) ⊤
rw₁ : Ici (↑a : WithTop α) ∩ range some = Ico (↑a : WithTop α) ⊤
⊢ some '' Ici a = Ico (↑a : WithTop α) ⊤
have rw₂ : Ici (↑a : WithTop α) ∩ Iio ⊤ = Ico (↑a : WithTop α) ⊤
Tactic: rw [← preimage_coe_Ici, image_preimage_eq_inter_range, range_coe, Ici_inter_Iio]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
rw : some '' some ⁻¹' Ici (↑a : WithTop α) = Ico (↑a : WithTop α) ⊤
rw₁ : Ici (↑a : WithTop α) ∩ range some = Ico (↑a : WithTop α) ⊤
rw₂ : Ici (↑a : WithTop α) ∩ Iio ⊤ = Ico (↑a : WithTop α) ⊤
⊢ some '' Ici a = Ico (↑a : WithTop α) ⊤
have rw₃ : Ico (↑a : WithTop α) ⊤ = Ico (↑a : WithTop α) ⊤
Tactic: rw [← preimage_coe_Ici, image_preimage_eq_inter_range, range_coe, Ici_inter_Iio]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ some '' Iio a = Iio (↑a : WithTop α)
have rw : some '' some ⁻¹' Iio (↑a : WithTop α) = Iio (↑a : WithTop α)
Tactic: rw [← preimage_coe_Iio, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Iio_subset_Iio le_top)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
rw : some '' some ⁻¹' Iio (↑a : WithTop α) = Iio (↑a : WithTop α)
⊢ some '' Iio a = Iio (↑a : WithTop α)
have rw₁ : Iio (↑a : WithTop α) ∩ range some = Iio (↑a : WithTop α)
Tactic: rw [← preimage_coe_Iio, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Iio_subset_Iio le_top)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
rw : some '' some ⁻¹' Iio (↑a : WithTop α) = Iio (↑a : WithTop α)
rw₁ : Iio (↑a : WithTop α) ∩ range some = Iio (↑a : WithTop α)
⊢ some '' Iio a = Iio (↑a : WithTop α)
have rw₂ : Iio (↑a : WithTop α) ∩ Iio ⊤ = Iio (↑a : WithTop α)
Tactic: rw [← preimage_coe_Iio, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Iio_subset_Iio le_top)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
rw : some '' some ⁻¹' Iio (↑a : WithTop α) = Iio (↑a : WithTop α)
rw₁ : Iio (↑a : WithTop α) ∩ range some = Iio (↑a : WithTop α)
rw₂ : Iio (↑a : WithTop α) ∩ Iio ⊤ = Iio (↑a : WithTop α)
⊢ some '' Iio a = Iio (↑a : WithTop α)
have rw₃ : Iio (↑a : WithTop α) = Iio (↑a : WithTop α)
Tactic: rw [← preimage_coe_Iio, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Iio_subset_Iio le_top)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ some '' Iic a = Iic (↑a : WithTop α)
have rw : some '' some ⁻¹' Iic (↑a : WithTop α) = Iic (↑a : WithTop α)
Tactic: rw [← preimage_coe_Iic, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Iic_subset_Iio.2 <| coe_lt_top a)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
rw : some '' some ⁻¹' Iic (↑a : WithTop α) = Iic (↑a : WithTop α)
⊢ some '' Iic a = Iic (↑a : WithTop α)
have rw₁ : Iic (↑a : WithTop α) ∩ range some = Iic (↑a : WithTop α)
Tactic: rw [← preimage_coe_Iic, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Iic_subset_Iio.2 <| coe_lt_top a)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.WithBotTop (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
rw : some '' some ⁻¹' Iic (↑a : WithTop α) = Iic (↑a : WithTop α)
rw₁ : Iic (↑a : WithTop α) ∩ range some = Iic (↑a : WithTop α)
⊢ some '' Iic a = Iic (↑a : WithTop α)
have rw₂ : Iic (↑a : WithTop α) ∩ Iio ⊤ = Iic (↑a : WithTop α)
Tactic: rw [← preimage_coe_Iic, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Iic_subset_Iio.2 <| coe_lt_top a)]