awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
h₁ : a ≤ b
h₂ : b ≤ c
⊢ Ioc a b ∪ Ioc b c = Ioc a c
have rw : (↑(Ioc a b ∪ Ioc b c) : Set α) = (↑(Ioc a c) : Set α)
Tactic: rw [← coe_inj, coe_union, coe_Ioc, coe_Ioc, coe_Ioc, Set.Ioc_union_Ioc_eq_Ioc h₁ h₂]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
h₁ : a ≤ b
h₂ : b ≤ c
rw : (↑(Ioc a b ∪ Ioc b c) : Set α) = (↑(Ioc a c) : Set α)
⊢ Ioc a b ∪ Ioc b c = Ioc a c
have rw₁ : (↑(Ioc a b) : Set α) ∪ (↑(Ioc b c) : Set α) = (↑(Ioc a c) : Set α)
Tactic: rw [← coe_inj, coe_union, coe_Ioc, coe_Ioc, coe_Ioc, Set.Ioc_union_Ioc_eq_Ioc h₁ h₂]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
h₁ : a ≤ b
h₂ : b ≤ c
rw : (↑(Ioc a b ∪ Ioc b c) : Set α) = (↑(Ioc a c) : Set α)
rw₁ : (↑(Ioc a b) : Set α) ∪ (↑(Ioc b c) : Set α) = (↑(Ioc a c) : Set α)
⊢ Ioc a b ∪ Ioc b c = Ioc a c
have rw₂ : Set.Ioc a b ∪ (↑(Ioc b c) : Set α) = (↑(Ioc a c) : Set α)
Tactic: rw [← coe_inj, coe_union, coe_Ioc, coe_Ioc, coe_Ioc, Set.Ioc_union_Ioc_eq_Ioc h₁ h₂]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
h₁ : a ≤ b
h₂ : b ≤ c
rw : (↑(Ioc a b ∪ Ioc b c) : Set α) = (↑(Ioc a c) : Set α)
rw₁ : (↑(Ioc a b) : Set α) ∪ (↑(Ioc b c) : Set α) = (↑(Ioc a c) : Set α)
rw₂ : Set.Ioc a b ∪ (↑(Ioc b c) : Set α) = (↑(Ioc a c) : Set α)
⊢ Ioc a b ∪ Ioc b c = Ioc a c
have rw₃ : Set.Ioc a b ∪ Set.Ioc b c = (↑(Ioc a c) : Set α)
Tactic: rw [← coe_inj, coe_union, coe_Ioc, coe_Ioc, coe_Ioc, Set.Ioc_union_Ioc_eq_Ioc h₁ h₂]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
h₁ : a ≤ b
h₂ : b ≤ c
rw : (↑(Ioc a b ∪ Ioc b c) : Set α) = (↑(Ioc a c) : Set α)
rw₁ : (↑(Ioc a b) : Set α) ∪ (↑(Ioc b c) : Set α) = (↑(Ioc a c) : Set α)
rw₂ : Set.Ioc a b ∪ (↑(Ioc b c) : Set α) = (↑(Ioc a c) : Set α)
rw₃ : Set.Ioc a b ∪ Set.Ioc b c = (↑(Ioc a c) : Set α)
⊢ Ioc a b ∪ Ioc b c = Ioc a c
have rw₄ : Set.Ioc a b ∪ Set.Ioc b c = Set.Ioc a c
Tactic: rw [← coe_inj, coe_union, coe_Ioc, coe_Ioc, coe_Ioc, Set.Ioc_union_Ioc_eq_Ioc h₁ h₂]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
h₁ : a ≤ b
h₂ : b ≤ c
rw : (↑(Ioc a b ∪ Ioc b c) : Set α) = (↑(Ioc a c) : Set α)
rw₁ : (↑(Ioc a b) : Set α) ∪ (↑(Ioc b c) : Set α) = (↑(Ioc a c) : Set α)
rw₂ : Set.Ioc a b ∪ (↑(Ioc b c) : Set α) = (↑(Ioc a c) : Set α)
rw₃ : Set.Ioc a b ∪ Set.Ioc b c = (↑(Ioc a c) : Set α)
rw₄ : Set.Ioc a b ∪ Set.Ioc b c = Set.Ioc a c
⊢ Ioc a b ∪ Ioc b c = Ioc a c
have rw₅ : Set.Ioc a c = Set.Ioc a c
Tactic: rw [← coe_inj, coe_union, coe_Ioc, coe_Ioc, coe_Ioc, Set.Ioc_union_Ioc_eq_Ioc h₁ h₂]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
⊢ Ico a c ⊆ Ico a b ∪ Ico b c
have rw : Set.Ico a c ⊆ Set.Ico a b ∪ Set.Ico b c
Tactic: rw [← coe_subset, coe_union, coe_Ico, coe_Ico, coe_Ico]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
have rw : (↑(Ico a b ∪ Ico c d) : Set α) = (↑(Ico (min a c) (max b d)) : Set α)
Tactic: rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico h₁ h₂]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
rw : (↑(Ico a b ∪ Ico c d) : Set α) = (↑(Ico (min a c) (max b d)) : Set α)
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
have rw₁ : (↑(Ico a b) : Set α) ∪ (↑(Ico c d) : Set α) = (↑(Ico (min a c) (max b d)) : Set α)
Tactic: rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico h₁ h₂]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
rw : (↑(Ico a b ∪ Ico c d) : Set α) = (↑(Ico (min a c) (max b d)) : Set α)
rw₁ : (↑(Ico a b) : Set α) ∪ (↑(Ico c d) : Set α) = (↑(Ico (min a c) (max b d)) : Set α)
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
have rw₂ : Set.Ico a b ∪ (↑(Ico c d) : Set α) = (↑(Ico (min a c) (max b d)) : Set α)
Tactic: rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico h₁ h₂]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
rw : (↑(Ico a b ∪ Ico c d) : Set α) = (↑(Ico (min a c) (max b d)) : Set α)
rw₁ : (↑(Ico a b) : Set α) ∪ (↑(Ico c d) : Set α) = (↑(Ico (min a c) (max b d)) : Set α)
rw₂ : Set.Ico a b ∪ (↑(Ico c d) : Set α) = (↑(Ico (min a c) (max b d)) : Set α)
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
have rw₃ : Set.Ico a b ∪ Set.Ico c d = (↑(Ico (min a c) (max b d)) : Set α)
Tactic: rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico h₁ h₂]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
rw : (↑(Ico a b ∪ Ico c d) : Set α) = (↑(Ico (min a c) (max b d)) : Set α)
rw₁ : (↑(Ico a b) : Set α) ∪ (↑(Ico c d) : Set α) = (↑(Ico (min a c) (max b d)) : Set α)
rw₂ : Set.Ico a b ∪ (↑(Ico c d) : Set α) = (↑(Ico (min a c) (max b d)) : Set α)
rw₃ : Set.Ico a b ∪ Set.Ico c d = (↑(Ico (min a c) (max b d)) : Set α)
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
have rw₄ : Set.Ico a b ∪ Set.Ico c d = Set.Ico (min a c) (max b d)
Tactic: rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico h₁ h₂]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
rw : (↑(Ico a b ∪ Ico c d) : Set α) = (↑(Ico (min a c) (max b d)) : Set α)
rw₁ : (↑(Ico a b) : Set α) ∪ (↑(Ico c d) : Set α) = (↑(Ico (min a c) (max b d)) : Set α)
rw₂ : Set.Ico a b ∪ (↑(Ico c d) : Set α) = (↑(Ico (min a c) (max b d)) : Set α)
rw₃ : Set.Ico a b ∪ Set.Ico c d = (↑(Ico (min a c) (max b d)) : Set α)
rw₄ : Set.Ico a b ∪ Set.Ico c d = Set.Ico (min a c) (max b d)
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
have rw₅ : Set.Ico (min a c) (max b d) = Set.Ico (min a c) (max b d)
Tactic: rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico h₁ h₂]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c d : α
hcb : c ≤ b
had : a ≤ d
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
have rw : (↑(Ico a b ∪ Ico c d) : Set α) = (↑(Ico (min a c) (max b d)) : Set α)
Tactic: rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico' hcb had]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c d : α
hcb : c ≤ b
had : a ≤ d
rw : (↑(Ico a b ∪ Ico c d) : Set α) = (↑(Ico (min a c) (max b d)) : Set α)
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
have rw₁ : (↑(Ico a b) : Set α) ∪ (↑(Ico c d) : Set α) = (↑(Ico (min a c) (max b d)) : Set α)
Tactic: rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico' hcb had]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c d : α
hcb : c ≤ b
had : a ≤ d
rw : (↑(Ico a b ∪ Ico c d) : Set α) = (↑(Ico (min a c) (max b d)) : Set α)
rw₁ : (↑(Ico a b) : Set α) ∪ (↑(Ico c d) : Set α) = (↑(Ico (min a c) (max b d)) : Set α)
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
have rw₂ : Set.Ico a b ∪ (↑(Ico c d) : Set α) = (↑(Ico (min a c) (max b d)) : Set α)
Tactic: rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico' hcb had]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c d : α
hcb : c ≤ b
had : a ≤ d
rw : (↑(Ico a b ∪ Ico c d) : Set α) = (↑(Ico (min a c) (max b d)) : Set α)
rw₁ : (↑(Ico a b) : Set α) ∪ (↑(Ico c d) : Set α) = (↑(Ico (min a c) (max b d)) : Set α)
rw₂ : Set.Ico a b ∪ (↑(Ico c d) : Set α) = (↑(Ico (min a c) (max b d)) : Set α)
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
have rw₃ : Set.Ico a b ∪ Set.Ico c d = (↑(Ico (min a c) (max b d)) : Set α)
Tactic: rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico' hcb had]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c d : α
hcb : c ≤ b
had : a ≤ d
rw : (↑(Ico a b ∪ Ico c d) : Set α) = (↑(Ico (min a c) (max b d)) : Set α)
rw₁ : (↑(Ico a b) : Set α) ∪ (↑(Ico c d) : Set α) = (↑(Ico (min a c) (max b d)) : Set α)
rw₂ : Set.Ico a b ∪ (↑(Ico c d) : Set α) = (↑(Ico (min a c) (max b d)) : Set α)
rw₃ : Set.Ico a b ∪ Set.Ico c d = (↑(Ico (min a c) (max b d)) : Set α)
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
have rw₄ : Set.Ico a b ∪ Set.Ico c d = Set.Ico (min a c) (max b d)
Tactic: rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico' hcb had]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c d : α
hcb : c ≤ b
had : a ≤ d
rw : (↑(Ico a b ∪ Ico c d) : Set α) = (↑(Ico (min a c) (max b d)) : Set α)
rw₁ : (↑(Ico a b) : Set α) ∪ (↑(Ico c d) : Set α) = (↑(Ico (min a c) (max b d)) : Set α)
rw₂ : Set.Ico a b ∪ (↑(Ico c d) : Set α) = (↑(Ico (min a c) (max b d)) : Set α)
rw₃ : Set.Ico a b ∪ Set.Ico c d = (↑(Ico (min a c) (max b d)) : Set α)
rw₄ : Set.Ico a b ∪ Set.Ico c d = Set.Ico (min a c) (max b d)
⊢ Ico a b ∪ Ico c d = Ico (min a c) (max b d)
have rw₅ : Set.Ico (min a c) (max b d) = Set.Ico (min a c) (max b d)
Tactic: rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico' hcb had]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c d : α
⊢ Ico a b ∩ Ico c d = Ico (max a c) (min b d)
have rw : (↑(Ico a b ∩ Ico c d) : Set α) = (↑(Ico (max a c) (min b d)) : Set α)
Tactic: rw [← coe_inj, coe_inter, coe_Ico, coe_Ico, coe_Ico, Set.Ico_inter_Ico]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c d : α
rw : (↑(Ico a b ∩ Ico c d) : Set α) = (↑(Ico (max a c) (min b d)) : Set α)
⊢ Ico a b ∩ Ico c d = Ico (max a c) (min b d)
have rw₁ : (↑(Ico a b) : Set α) ∩ (↑(Ico c d) : Set α) = (↑(Ico (max a c) (min b d)) : Set α)
Tactic: rw [← coe_inj, coe_inter, coe_Ico, coe_Ico, coe_Ico, Set.Ico_inter_Ico]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c d : α
rw : (↑(Ico a b ∩ Ico c d) : Set α) = (↑(Ico (max a c) (min b d)) : Set α)
rw₁ : (↑(Ico a b) : Set α) ∩ (↑(Ico c d) : Set α) = (↑(Ico (max a c) (min b d)) : Set α)
⊢ Ico a b ∩ Ico c d = Ico (max a c) (min b d)
have rw₂ : Set.Ico a b ∩ (↑(Ico c d) : Set α) = (↑(Ico (max a c) (min b d)) : Set α)
Tactic: rw [← coe_inj, coe_inter, coe_Ico, coe_Ico, coe_Ico, Set.Ico_inter_Ico]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c d : α
rw : (↑(Ico a b ∩ Ico c d) : Set α) = (↑(Ico (max a c) (min b d)) : Set α)
rw₁ : (↑(Ico a b) : Set α) ∩ (↑(Ico c d) : Set α) = (↑(Ico (max a c) (min b d)) : Set α)
rw₂ : Set.Ico a b ∩ (↑(Ico c d) : Set α) = (↑(Ico (max a c) (min b d)) : Set α)
⊢ Ico a b ∩ Ico c d = Ico (max a c) (min b d)
have rw₃ : Set.Ico a b ∩ Set.Ico c d = (↑(Ico (max a c) (min b d)) : Set α)
Tactic: rw [← coe_inj, coe_inter, coe_Ico, coe_Ico, coe_Ico, Set.Ico_inter_Ico]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c d : α
rw : (↑(Ico a b ∩ Ico c d) : Set α) = (↑(Ico (max a c) (min b d)) : Set α)
rw₁ : (↑(Ico a b) : Set α) ∩ (↑(Ico c d) : Set α) = (↑(Ico (max a c) (min b d)) : Set α)
rw₂ : Set.Ico a b ∩ (↑(Ico c d) : Set α) = (↑(Ico (max a c) (min b d)) : Set α)
rw₃ : Set.Ico a b ∩ Set.Ico c d = (↑(Ico (max a c) (min b d)) : Set α)
⊢ Ico a b ∩ Ico c d = Ico (max a c) (min b d)
have rw₄ : Set.Ico a b ∩ Set.Ico c d = Set.Ico (max a c) (min b d)
Tactic: rw [← coe_inj, coe_inter, coe_Ico, coe_Ico, coe_Ico, Set.Ico_inter_Ico]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c d : α
rw : (↑(Ico a b ∩ Ico c d) : Set α) = (↑(Ico (max a c) (min b d)) : Set α)
rw₁ : (↑(Ico a b) : Set α) ∩ (↑(Ico c d) : Set α) = (↑(Ico (max a c) (min b d)) : Set α)
rw₂ : Set.Ico a b ∩ (↑(Ico c d) : Set α) = (↑(Ico (max a c) (min b d)) : Set α)
rw₃ : Set.Ico a b ∩ Set.Ico c d = (↑(Ico (max a c) (min b d)) : Set α)
rw₄ : Set.Ico a b ∩ Set.Ico c d = Set.Ico (max a c) (min b d)
⊢ Ico a b ∩ Ico c d = Ico (max a c) (min b d)
have rw₅ : Set.Ico (max a c) (min b d) = Set.Ico (max a c) (min b d)
Tactic: rw [← coe_inj, coe_inter, coe_Ico, coe_Ico, coe_Ico, Set.Ico_inter_Ico]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
⊢ Disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁
have simp_rw : Ioc a₁ a₂ ∩ Ioc b₁ b₂ = ∅ ↔ min a₂ b₂ ≤ max a₁ b₁
Tactic: simp_rw [disjoint_iff_inter_eq_empty, Ioc_inter_Ioc, Ioc_eq_empty_iff, not_lt]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
simp_rw : Ioc a₁ a₂ ∩ Ioc b₁ b₂ = ∅ ↔ min a₂ b₂ ≤ max a₁ b₁
⊢ Disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁
have simp_rw₁ : Ioc (max a₁ b₁) (min a₂ b₂) = ∅ ↔ min a₂ b₂ ≤ max a₁ b₁
Tactic: simp_rw [disjoint_iff_inter_eq_empty, Ioc_inter_Ioc, Ioc_eq_empty_iff, not_lt]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
simp_rw : Ioc a₁ a₂ ∩ Ioc b₁ b₂ = ∅ ↔ min a₂ b₂ ≤ max a₁ b₁
simp_rw₁ : Ioc (max a₁ b₁) (min a₂ b₂) = ∅ ↔ min a₂ b₂ ≤ max a₁ b₁
⊢ Disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁
have simp_rw₂ : ¬max a₁ b₁ < min a₂ b₂ ↔ min a₂ b₂ ≤ max a₁ b₁
Tactic: simp_rw [disjoint_iff_inter_eq_empty, Ioc_inter_Ioc, Ioc_eq_empty_iff, not_lt]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a b : α
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : LocallyFiniteOrderBot α
hab : a ≤ b
⊢ Iic b \ Ioc a b = Iic a
have rw : Iic (min a b) = Iic a
Tactic: rw [Iic_diff_Ioc, min_eq_left hab]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a b : α
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
inst_2 : LocallyFiniteOrderBot α
hab : a ≤ b
rw : Iic (min a b) = Iic a
⊢ Iic b \ Ioc a b = Iic a
have rw₁ : Iic a = Iic a
Tactic: rw [Iic_diff_Ioc, min_eq_left hab]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : Fintype α
inst_2 : LocallyFiniteOrderTop α
inst_3 : LocallyFiniteOrderBot α
a : α
⊢ (Ioi a).disjUnion (Iio a) ⋯ = {a}ᶜ
have h : ∀ (a_1 : α), a_1 ∈ (Ioi a).disjUnion (Iio a) sorry ↔ Membership.mem (γ := Finset α) {a}ᶜ a_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ [[a, b]] = Icc a b
have rw : Icc (a ⊓ b) (a ⊔ b) = Icc a b
Tactic: rw [uIcc, inf_eq_left.2 h, sup_eq_right.2 h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a b : α
h : a ≤ b
rw : Icc (a ⊓ b) (a ⊔ b) = Icc a b
⊢ [[a, b]] = Icc a b
have rw₁ : Icc a (a ⊔ b) = Icc a b
Tactic: rw [uIcc, inf_eq_left.2 h, sup_eq_right.2 h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a b : α
h : a ≤ b
rw : Icc (a ⊓ b) (a ⊔ b) = Icc a b
rw₁ : Icc a (a ⊔ b) = Icc a b
⊢ [[a, b]] = Icc a b
have rw₂ : Icc a b = Icc a b
Tactic: rw [uIcc, inf_eq_left.2 h, sup_eq_right.2 h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a b : α
h : b ≤ a
⊢ [[a, b]] = Icc b a
have rw : Icc (a ⊓ b) (a ⊔ b) = Icc b a
Tactic: rw [uIcc, inf_eq_right.2 h, sup_eq_left.2 h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a b : α
h : b ≤ a
rw : Icc (a ⊓ b) (a ⊔ b) = Icc b a
⊢ [[a, b]] = Icc b a
have rw₁ : Icc b (a ⊔ b) = Icc b a
Tactic: rw [uIcc, inf_eq_right.2 h, sup_eq_left.2 h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a b : α
h : b ≤ a
rw : Icc (a ⊓ b) (a ⊔ b) = Icc b a
rw₁ : Icc b (a ⊔ b) = Icc b a
⊢ [[a, b]] = Icc b a
have rw₂ : Icc b a = Icc b a
Tactic: rw [uIcc, inf_eq_right.2 h, sup_eq_left.2 h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ [[a, b]] = [[b, a]]
have rw : Icc (a ⊓ b) (a ⊔ b) = [[b, a]]
Tactic: rw [uIcc, uIcc, inf_comm, sup_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a b : α
rw : Icc (a ⊓ b) (a ⊔ b) = [[b, a]]
⊢ [[a, b]] = [[b, a]]
have rw₁ : Icc (a ⊓ b) (a ⊔ b) = Icc (b ⊓ a) (b ⊔ a)
Tactic: rw [uIcc, uIcc, inf_comm, sup_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a b : α
rw : Icc (a ⊓ b) (a ⊔ b) = [[b, a]]
rw₁ : Icc (a ⊓ b) (a ⊔ b) = Icc (b ⊓ a) (b ⊔ a)
⊢ [[a, b]] = [[b, a]]
have rw₂ : Icc (b ⊓ a) (a ⊔ b) = Icc (b ⊓ a) (b ⊔ a)
Tactic: rw [uIcc, uIcc, inf_comm, sup_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a b : α
rw : Icc (a ⊓ b) (a ⊔ b) = [[b, a]]
rw₁ : Icc (a ⊓ b) (a ⊔ b) = Icc (b ⊓ a) (b ⊔ a)
rw₂ : Icc (b ⊓ a) (a ⊔ b) = Icc (b ⊓ a) (b ⊔ a)
⊢ [[a, b]] = [[b, a]]
have rw₃ : Icc (b ⊓ a) (b ⊔ a) = Icc (b ⊓ a) (b ⊔ a)
Tactic: rw [uIcc, uIcc, inf_comm, sup_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (hypothesis)
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a₁ a₂ b₁ b₂ : α
h₁ : a₁ ∈ [[a₂, b₂]]
h₂ : b₁ ∈ [[a₂, b₂]]
⊢ [[a₁, b₁]] ⊆ [[a₂, b₂]]
have h₃ : a₂ ⊓ b₂ ≤ a₁ ∧ a₁ ≤ a₂ ⊔ b₂
Tactic: rw [mem_uIcc] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (hypothesis)
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a₁ a₂ b₁ b₂ : α
h₁ : a₁ ∈ [[a₂, b₂]]
h₂ : b₁ ∈ [[a₂, b₂]]
h₃ : a₂ ⊓ b₂ ≤ a₁ ∧ a₁ ≤ a₂ ⊔ b₂
⊢ [[a₁, b₁]] ⊆ [[a₂, b₂]]
have h₄ : a₂ ⊓ b₂ ≤ b₁ ∧ b₁ ≤ a₂ ⊔ b₂
Tactic: rw [mem_uIcc] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (hypothesis)
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a₁ a₂ b₁ b₂ : α
ha : a₁ ∈ Icc a₂ b₂
hb : b₁ ∈ Icc a₂ b₂
⊢ [[a₁, b₁]] ⊆ Icc a₂ b₂
have ha₁ : a₂ ≤ a₁ ∧ a₁ ≤ b₂
Tactic: rw [mem_Icc] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (hypothesis)
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a₁ a₂ b₁ b₂ : α
ha : a₁ ∈ Icc a₂ b₂
hb : b₁ ∈ Icc a₂ b₂
ha₁ : a₂ ≤ a₁ ∧ a₁ ≤ b₂
⊢ [[a₁, b₁]] ⊆ Icc a₂ b₂
have hb₁ : a₂ ≤ b₁ ∧ b₁ ≤ b₂
Tactic: rw [mem_Icc] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DistribLattice α
inst_1 : LocallyFiniteOrder α
a b c : α
⊢ a ∈ [[b, c]] → b ∈ [[a, c]] → a = b
have simp_rw : b ⊓ c ≤ a ∧ a ≤ b ⊔ c → a ⊓ c ≤ b ∧ b ≤ a ⊔ c → a = b
Tactic: simp_rw [mem_uIcc]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : DistribLattice α
inst_1 : LocallyFiniteOrder α
a b c : α
⊢ b ∈ [[a, c]] → c ∈ [[a, b]] → b = c
have simp_rw : a ⊓ c ≤ b ∧ b ≤ a ⊔ c → a ⊓ b ≤ c ∧ c ≤ a ⊔ b → b = c
Tactic: simp_rw [mem_uIcc]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (hypothesis)
Goal:
α : Type u_2
inst : DistribLattice α
inst_1 : LocallyFiniteOrder α
a b c : α
h : Eq.{u_2 + 1} (α := Finset α) ((fun (b : α) ↦ [[b, a]]) b) ((fun (b : α) ↦ [[b, a]]) c)
⊢ b = c
have h₁ : ∀ (a_1 : α),
  Membership.mem (γ := Finset α) ((fun (b : α) ↦ [[b, a]]) b) a_1 ↔
    Membership.mem (γ := Finset α) ((fun (b : α) ↦ [[b, a]]) c) a_1
Tactic: rw [Finset.ext_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ (↑[[a, b]] : Set α) = (↑(Icc a b ∪ Icc b a) : Set α)
have push_cast : Set.uIcc a b = Set.Icc a b ∪ Set.Icc b a
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
⊢ c < a → c < b → c ∉ [[a, b]]
have rw : c < a → c < b → ¬(min a b ≤ c ∧ c ≤ max a b)
Tactic: rw [mem_uIcc]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
⊢ a < c → b < c → c ∉ [[a, b]]
have rw : a < c → b < c → ¬(min a b ≤ c ∧ c ≤ max a b)
Tactic: rw [mem_uIcc]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
⊢ (↑[[a, c]] : Set α) ⊆ (↑([[a, b]] ∪ [[b, c]]) : Set α)
have push_cast : Set.uIcc a c ⊆ Set.uIcc a b ∪ Set.uIcc b c
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (hypothesis)
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
⊢ TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x y
have this : #(Ico x y) < #(Icc x y)
Tactic: have : #(Ico x y) < #(Icc x y) := card_lt_card <|
    ⟨Ico_subset_Icc_self, not_subset.mpr ⟨y, ⟨right_mem_Icc.mpr hxy, right_notMem_Ico⟩⟩⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
⊢ TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x y
have pos : ∀ (hxy' : y ≤ x), TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x y
Tactic: by_cases hxy' : y ≤ x
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
pos : ∀ (hxy' : y ≤ x), TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x y
⊢ TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x y
have neg : ∀ (hxy' : ¬y ≤ x), TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x y
Tactic: by_cases hxy' : y ≤ x
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : ¬y ≤ x
⊢ TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x y
have neg : ∀ (z : α) (hxz : x ≤ z) (hz : Maximal (fun (x_1 : α) ↦ x_1 ∈ Set.Ico x y) z), TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x y
Tactic: obtain ⟨z, hxz, hz⟩ :=
      (Set.finite_Ico x y).exists_le_maximal <| Set.left_mem_Ico.2 <| hxy.lt_of_not_ge hxy'