awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
⊢ Ioc a b ⊆ s
have pos : ∀ (ho : Ioc a b \ {b} ⊆ s) (hc : s ⊆ Icc a b) (ha : ¬a ∈ s) (hb : b ∈ s), Ioc a b ⊆ s
Tactic: rwa [← Ioc_diff_right, diff_singleton_subset_iff, insert_eq_of_mem hb] at ho
Cleared hypotheses: ho, hc, ha, hb
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
pos : ∀ (ho : Ioc a b \ {b} ⊆ s) (hc : s ⊆ Icc a b) (ha : ¬a ∈ s) (hb : b ∈ s), Ioc a b ⊆ s
⊢ Ioc a b ⊆ s
have pos₁ : ∀ (ho : Ioc a b ⊆ insert b s) (hc : s ⊆ Icc a b) (ha : ¬a ∈ s) (hb : b ∈ s), Ioc a b ⊆ s
Tactic: rwa [← Ioc_diff_right, diff_singleton_subset_iff, insert_eq_of_mem hb] at ho
Cleared hypotheses: ho, hc, ha, hb
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : b ∈ s
pos : ∀ (ho : Ioc a b \ {b} ⊆ s) (hc : s ⊆ Icc a b) (ha : ¬a ∈ s) (hb : b ∈ s), Ioc a b ⊆ s
pos₁ : ∀ (ho : Ioc a b ⊆ insert b s) (hc : s ⊆ Icc a b) (ha : ¬a ∈ s) (hb : b ∈ s), Ioc a b ⊆ s
⊢ Ioc a b ⊆ s
have pos₂ : ∀ (ho : Ioc a b ⊆ s) (hc : s ⊆ Icc a b) (ha : ¬a ∈ s) (hb : b ∈ s), Ioc a b ⊆ s
Tactic: rwa [← Ioc_diff_right, diff_singleton_subset_iff, insert_eq_of_mem hb] at ho
Cleared hypotheses: ho, hc, ha, hb
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : ¬b ∈ s
⊢ Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
have neg : s ⊆ Ioo a b
Tactic: refine Or.inr <| Or.inr <| Or.inr <| Subset.antisymm ?_ ho
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : ¬a ∈ s
hb : ¬b ∈ s
⊢ s ⊆ Ioo a b
have neg : s ⊆ (Icc a b \ {b}) \ {a}
Tactic: rw [← Ico_diff_left, ← Icc_diff_right]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
⊢ Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
have pos : ∀ (ha : a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
Tactic: classical
    by_cases ha : a ∈ s <;> by_cases hb : b ∈ s
    · refine Or.inl (Subset.antisymm hc ?_)
      rwa [← Ico_diff_left, diff_singleton_subset_iff, insert_eq_of_mem ha, ← Icc_diff_right,
        diff_singleton_subset_iff, insert_eq_of_mem hb] at ho
    · refine Or.inr <| Or.inl <| Subset.antisymm ?_ ?_
      · rw [← Icc_diff_right]
        exact subset_diff_singleton hc hb
      · rwa [← Ico_diff_left, diff_singleton_subset_iff, insert_eq_of_mem ha] at ho
    · refine Or.inr <| Or.inr <| Or.inl <| Subset.antisymm ?_ ?_
      · rw [← Icc_diff_left]
        exact subset_diff_singleton hc ha
      · rwa [← Ioc_diff_right, diff_singleton_subset_iff, insert_eq_of_mem hb] at ho
    · refine Or.inr <| Or.inr <| Or.inr <| Subset.antisymm ?_ ho
      rw [← Ico_diff_left, ← Icc_diff_right]
      apply_rules [subset_diff_singleton]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
pos : ∀ (ha : a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
⊢ Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
have neg : ∀ (ha : ¬a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
Tactic: classical
    by_cases ha : a ∈ s <;> by_cases hb : b ∈ s
    · refine Or.inl (Subset.antisymm hc ?_)
      rwa [← Ico_diff_left, diff_singleton_subset_iff, insert_eq_of_mem ha, ← Icc_diff_right,
        diff_singleton_subset_iff, insert_eq_of_mem hb] at ho
    · refine Or.inr <| Or.inl <| Subset.antisymm ?_ ?_
      · rw [← Icc_diff_right]
        exact subset_diff_singleton hc hb
      · rwa [← Ico_diff_left, diff_singleton_subset_iff, insert_eq_of_mem ha] at ho
    · refine Or.inr <| Or.inr <| Or.inl <| Subset.antisymm ?_ ?_
      · rw [← Icc_diff_left]
        exact subset_diff_singleton hc ha
      · rwa [← Ioc_diff_right, diff_singleton_subset_iff, insert_eq_of_mem hb] at ho
    · refine Or.inr <| Or.inr <| Or.inr <| Subset.antisymm ?_ ho
      rw [← Ico_diff_left, ← Icc_diff_right]
      apply_rules [subset_diff_singleton]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
pos : ∀ (ha : a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
neg : ∀ (ha : ¬a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
pos₁ : ∀ (ha : a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
neg₁ : ∀ (ha : ¬a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
pos₂ : ∀ (ha : a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
neg₂ : ∀ (ha : ¬a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
pos₃ : ∀ (ha : a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
neg₃ : ∀ (ha : ¬a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
⊢ Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
have pos₄ : ∀ (ha : a ∈ s) (hb : b ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
Tactic: classical
    by_cases ha : a ∈ s <;> by_cases hb : b ∈ s
    · refine Or.inl (Subset.antisymm hc ?_)
      rwa [← Ico_diff_left, diff_singleton_subset_iff, insert_eq_of_mem ha, ← Icc_diff_right,
        diff_singleton_subset_iff, insert_eq_of_mem hb] at ho
    · refine Or.inr <| Or.inl <| Subset.antisymm ?_ ?_
      · rw [← Icc_diff_right]
        exact subset_diff_singleton hc hb
      · rwa [← Ico_diff_left, diff_singleton_subset_iff, insert_eq_of_mem ha] at ho
    · refine Or.inr <| Or.inr <| Or.inl <| Subset.antisymm ?_ ?_
      · rw [← Icc_diff_left]
        exact subset_diff_singleton hc ha
      · rwa [← Ioc_diff_right, diff_singleton_subset_iff, insert_eq_of_mem hb] at ho
    · refine Or.inr <| Or.inr <| Or.inr <| Subset.antisymm ?_ ho
      rw [← Ico_diff_left, ← Icc_diff_right]
      apply_rules [subset_diff_singleton]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
pos : ∀ (ha : a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
neg : ∀ (ha : ¬a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
pos₁ : ∀ (ha : a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
neg₁ : ∀ (ha : ¬a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
pos₂ : ∀ (ha : a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
neg₂ : ∀ (ha : ¬a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
pos₃ : ∀ (ha : a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
neg₃ : ∀ (ha : ¬a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
pos₄ : ∀ (ha : a ∈ s) (hb : b ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
⊢ Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
have neg₄ : ∀ (ha : a ∈ s) (hb : ¬b ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
Tactic: classical
    by_cases ha : a ∈ s <;> by_cases hb : b ∈ s
    · refine Or.inl (Subset.antisymm hc ?_)
      rwa [← Ico_diff_left, diff_singleton_subset_iff, insert_eq_of_mem ha, ← Icc_diff_right,
        diff_singleton_subset_iff, insert_eq_of_mem hb] at ho
    · refine Or.inr <| Or.inl <| Subset.antisymm ?_ ?_
      · rw [← Icc_diff_right]
        exact subset_diff_singleton hc hb
      · rwa [← Ico_diff_left, diff_singleton_subset_iff, insert_eq_of_mem ha] at ho
    · refine Or.inr <| Or.inr <| Or.inl <| Subset.antisymm ?_ ?_
      · rw [← Icc_diff_left]
        exact subset_diff_singleton hc ha
      · rwa [← Ioc_diff_right, diff_singleton_subset_iff, insert_eq_of_mem hb] at ho
    · refine Or.inr <| Or.inr <| Or.inr <| Subset.antisymm ?_ ho
      rw [← Ico_diff_left, ← Icc_diff_right]
      apply_rules [subset_diff_singleton]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
pos : ∀ (ha : a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
neg : ∀ (ha : ¬a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
pos₁ : ∀ (ha : a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
neg₁ : ∀ (ha : ¬a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
pos₂ : ∀ (ha : a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
neg₂ : ∀ (ha : ¬a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
pos₃ : ∀ (ha : a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
neg₃ : ∀ (ha : ¬a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
pos₄ : ∀ (ha : a ∈ s) (hb : b ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
neg₄ : ∀ (ha : a ∈ s) (hb : ¬b ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
⊢ Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
have pos₅ : ∀ (ha : ¬a ∈ s) (hb : b ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
Tactic: classical
    by_cases ha : a ∈ s <;> by_cases hb : b ∈ s
    · refine Or.inl (Subset.antisymm hc ?_)
      rwa [← Ico_diff_left, diff_singleton_subset_iff, insert_eq_of_mem ha, ← Icc_diff_right,
        diff_singleton_subset_iff, insert_eq_of_mem hb] at ho
    · refine Or.inr <| Or.inl <| Subset.antisymm ?_ ?_
      · rw [← Icc_diff_right]
        exact subset_diff_singleton hc hb
      · rwa [← Ico_diff_left, diff_singleton_subset_iff, insert_eq_of_mem ha] at ho
    · refine Or.inr <| Or.inr <| Or.inl <| Subset.antisymm ?_ ?_
      · rw [← Icc_diff_left]
        exact subset_diff_singleton hc ha
      · rwa [← Ioc_diff_right, diff_singleton_subset_iff, insert_eq_of_mem hb] at ho
    · refine Or.inr <| Or.inr <| Or.inr <| Subset.antisymm ?_ ho
      rw [← Ico_diff_left, ← Icc_diff_right]
      apply_rules [subset_diff_singleton]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
pos : ∀ (ha : a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
neg : ∀ (ha : ¬a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
pos₁ : ∀ (ha : a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
neg₁ : ∀ (ha : ¬a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
pos₂ : ∀ (ha : a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
neg₂ : ∀ (ha : ¬a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
pos₃ : ∀ (ha : a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
neg₃ : ∀ (ha : ¬a ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
pos₄ : ∀ (ha : a ∈ s) (hb : b ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
neg₄ : ∀ (ha : a ∈ s) (hb : ¬b ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
pos₅ : ∀ (ha : ¬a ∈ s) (hb : b ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
⊢ Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
have neg₅ : ∀ (ha : ¬a ∈ s) (hb : ¬b ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
Tactic: classical
    by_cases ha : a ∈ s <;> by_cases hb : b ∈ s
    · refine Or.inl (Subset.antisymm hc ?_)
      rwa [← Ico_diff_left, diff_singleton_subset_iff, insert_eq_of_mem ha, ← Icc_diff_right,
        diff_singleton_subset_iff, insert_eq_of_mem hb] at ho
    · refine Or.inr <| Or.inl <| Subset.antisymm ?_ ?_
      · rw [← Icc_diff_right]
        exact subset_diff_singleton hc hb
      · rwa [← Ico_diff_left, diff_singleton_subset_iff, insert_eq_of_mem ha] at ho
    · refine Or.inr <| Or.inr <| Or.inl <| Subset.antisymm ?_ ?_
      · rw [← Icc_diff_left]
        exact subset_diff_singleton hc ha
      · rwa [← Ioc_diff_right, diff_singleton_subset_iff, insert_eq_of_mem hb] at ho
    · refine Or.inr <| Or.inr <| Or.inr <| Subset.antisymm ?_ ho
      rw [← Ico_diff_left, ← Icc_diff_right]
      apply_rules [subset_diff_singleton]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ Icc a b ∩ Icc b c = {b}
have rw : Ici a ∩ Iic c ∩ Icc b b = {b}
Tactic: rw [← Ici_inter_Iic, ← Iic_inter_Ici, inter_inter_inter_comm, Iic_inter_Ici]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b c d : α
h : a ≤ b
⊢ Icc a b = Icc c d ↔ a = c ∧ b = d
have refine : ∀ (heq : Icc a b = Icc c d), a = c ∧ b = d
Tactic: refine ⟨fun heq ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b c d : α
h : a ≤ b
heq : Icc a b = Icc c d
⊢ c ≤ d
have by_contra : ∀ (contra : ¬c ≤ d), False
Tactic: by_contra contra
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (hypothesis)
Goal:
α : Type u_1
inst : PartialOrder α
a b c d : α
h : a ≤ b
heq : Icc a b = Icc c d
contra : ¬c ≤ d
⊢ False
have heq₁ : ¬a ≤ b
Tactic: rw [Icc_eq_empty_iff.mpr contra, Icc_eq_empty_iff] at heq
Cleared hypotheses: heq, contra
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (hypothesis)
Goal:
α : Type u_1
inst : PartialOrder α
a b c d : α
h : a ≤ b
heq : Icc a b = Icc c d
⊢ a = c ∧ b = d
have h' : c ≤ d
Tactic: have h' : c ≤ d := by
    by_contra contra; rw [Icc_eq_empty_iff.mpr contra, Icc_eq_empty_iff] at heq; contradiction
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (hypothesis)
Goal:
α : Type u_1
inst : PartialOrder α
a b c d : α
h : a ≤ b
heq : Icc a b = Icc c d
h' : c ≤ d
⊢ a = c ∧ b = d
have heq₁ : ∀ (x : α), a ≤ x ∧ x ≤ b ↔ c ≤ x ∧ x ≤ d
Tactic: simp only [Set.ext_iff, mem_Icc] at heq
Cleared hypotheses: heq
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (hypothesis)
Goal:
α : Type u_1
inst : PartialOrder α
a b c d : α
h : a ≤ b
h' : c ≤ d
heq : ∀ (x : α), a ≤ x ∧ x ≤ b ↔ c ≤ x ∧ x ≤ d
⊢ a = c ∧ b = d
have h₁ : b ≤ d
Tactic: obtain ⟨-, h₁⟩ := (heq b).mp ⟨h, le_refl _⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (hypothesis)
Goal:
α : Type u_1
inst : PartialOrder α
a b c d : α
h : a ≤ b
h' : c ≤ d
heq : ∀ (x : α), a ≤ x ∧ x ≤ b ↔ c ≤ x ∧ x ≤ d
h₁ : b ≤ d
⊢ a = c ∧ b = d
have h₂ : c ≤ a
Tactic: obtain ⟨h₂, -⟩ := (heq a).mp ⟨le_refl _, h⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (hypothesis)
Goal:
α : Type u_1
inst : PartialOrder α
a b c d : α
h : a ≤ b
h' : c ≤ d
heq : ∀ (x : α), a ≤ x ∧ x ≤ b ↔ c ≤ x ∧ x ≤ d
h₁ : b ≤ d
h₂ : c ≤ a
⊢ a = c ∧ b = d
have h₃ : a ≤ c
Tactic: obtain ⟨h₃, -⟩ := (heq c).mpr ⟨le_refl _, h'⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (hypothesis)
Goal:
α : Type u_1
inst : PartialOrder α
a b c d : α
h : a ≤ b
h' : c ≤ d
heq : ∀ (x : α), a ≤ x ∧ x ≤ b ↔ c ≤ x ∧ x ≤ d
h₁ : b ≤ d
h₂ : c ≤ a
h₃ : a ≤ c
⊢ a = c ∧ b = d
have h₄ : d ≤ b
Tactic: obtain ⟨-, h₄⟩ := (heq d).mpr ⟨h', le_refl _⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
a b : α
⊢ Iic a ∩ Iic b = Iic (a ⊓ b)
have h : ∀ (x : α), x ∈ Iic a ∩ Iic b ↔ x ∈ Iic (a ⊓ b)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
a b c : α
⊢ Ioc a b ∩ Iic c = Ioc a (b ⊓ c)
have rw : Ioi a ∩ Iic b ∩ Iic c = Ioc a (b ⊓ c)
Tactic: rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, inter_assoc, Iic_inter_Iic]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
a b c : α
rw : Ioi a ∩ Iic b ∩ Iic c = Ioc a (b ⊓ c)
⊢ Ioc a b ∩ Iic c = Ioc a (b ⊓ c)
have rw₁ : Ioi a ∩ Iic b ∩ Iic c = Ioi a ∩ Iic (b ⊓ c)
Tactic: rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, inter_assoc, Iic_inter_Iic]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
a b c : α
rw : Ioi a ∩ Iic b ∩ Iic c = Ioc a (b ⊓ c)
rw₁ : Ioi a ∩ Iic b ∩ Iic c = Ioi a ∩ Iic (b ⊓ c)
⊢ Ioc a b ∩ Iic c = Ioc a (b ⊓ c)
have rw₂ : Ioi a ∩ (Iic b ∩ Iic c) = Ioi a ∩ Iic (b ⊓ c)
Tactic: rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, inter_assoc, Iic_inter_Iic]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : SemilatticeInf α
a b c : α
rw : Ioi a ∩ Iic b ∩ Iic c = Ioc a (b ⊓ c)
rw₁ : Ioi a ∩ Iic b ∩ Iic c = Ioi a ∩ Iic (b ⊓ c)
rw₂ : Ioi a ∩ (Iic b ∩ Iic c) = Ioi a ∩ Iic (b ⊓ c)
⊢ Ioc a b ∩ Iic c = Ioc a (b ⊓ c)
have rw₃ : Ioi a ∩ Iic (b ⊓ c) = Ioi a ∩ Iic (b ⊓ c)
Tactic: rw [← Ioi_inter_Iic, ← Ioi_inter_Iic, inter_assoc, Iic_inter_Iic]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : Lattice α
a₁ a₂ b₁ b₂ : α
⊢ Icc a₁ b₁ ∩ Icc a₂ b₂ = Icc (a₁ ⊔ a₂) (b₁ ⊓ b₂)
have simp : Ici a₁ ∩ Iic b₁ ∩ (Ici a₂ ∩ Iic b₂) = Ici a₁ ∩ Ici a₂ ∩ (Iic b₁ ∩ Iic b₂)
Tactic: simp only [Ici_inter_Iic.symm, Ici_inter_Ici.symm, Iic_inter_Iic.symm]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
a₁ a₂ : α
b₁ b₂ : β
⊢ Icc a₁ a₂ ×ˢ Icc b₁ b₂ = Icc (a₁, b₁) (a₂, b₂)
have h : ∀ (x : α) (y : β), (x, y) ∈ Icc a₁ a₂ ×ˢ Icc b₁ b₂ ↔ (x, y) ∈ Icc (a₁, b₁) (a₂, b₂)
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DenselyOrdered α
x y : α
x_1 : (↑(Ioo x y) : Type u_1)
a : α
ha : a ∈ Ioo x y
⊢ ∃ (b : (↑(Ioo x y) : Type u_1)), b < Subtype.mk (p := fun (x_2 : α) ↦ x_2 ∈ Ioo x y) a ha
have rcases : ∀ (b : α) (hb₁ : x < b) (hb₂ : b < a),
  ∃ (b : (↑(Ioo x y) : Type u_1)), b < Subtype.mk (p := fun (x_2 : α) ↦ x_2 ∈ Ioo x y) a ha
Tactic: rcases exists_between ha.1 with ⟨b, hb₁, hb₂⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DenselyOrdered α
x y : α
x_1 : (↑(Ioc x y) : Type u_1)
a : α
ha : a ∈ Ioc x y
⊢ ∃ (b : (↑(Ioc x y) : Type u_1)), b < Subtype.mk (p := fun (x_2 : α) ↦ x_2 ∈ Ioc x y) a ha
have rcases : ∀ (b : α) (hb₁ : x < b) (hb₂ : b < a),
  ∃ (b : (↑(Ioc x y) : Type u_1)), b < Subtype.mk (p := fun (x_2 : α) ↦ x_2 ∈ Ioc x y) a ha
Tactic: rcases exists_between ha.1 with ⟨b, hb₁, hb₂⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : DenselyOrdered α
x y : α
x_1 : (↑(Ioi x) : Type u_1)
a : α
ha : a ∈ Ioi x
⊢ ∃ (b : (↑(Ioi x) : Type u_1)), b < Subtype.mk (p := fun (x_2 : α) ↦ x_2 ∈ Ioi x) a ha
have rcases : ∀ (b : α) (hb₁ : x < b) (hb₂ : b < a),
  ∃ (b : (↑(Ioi x) : Type u_1)), b < Subtype.mk (p := fun (x_2 : α) ↦ x_2 ∈ Ioi x) a ha
Tactic: rcases exists_between ha with ⟨b, hb₁, hb₂⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Disjoint (goal)
Goal:
α : Type v
inst : Preorder α
a b : α
⊢ Disjoint (Ici a) (Iic b) ↔ ¬a ≤ b
have rw : Ici a ∩ Iic b = ∅ ↔ ¬a ≤ b
Tactic: rw [Set.disjoint_iff_inter_eq_empty, Ici_inter_Iic, Icc_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Disjoint (goal)
Goal:
α : Type v
inst : Preorder α
a b : α
rw : Ici a ∩ Iic b = ∅ ↔ ¬a ≤ b
⊢ Disjoint (Ici a) (Iic b) ↔ ¬a ≤ b
have rw₁ : Icc a b = ∅ ↔ ¬a ≤ b
Tactic: rw [Set.disjoint_iff_inter_eq_empty, Ici_inter_Iic, Icc_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Disjoint (goal)
Goal:
α : Type v
inst : Preorder α
a b : α
rw : Ici a ∩ Iic b = ∅ ↔ ¬a ≤ b
rw₁ : Icc a b = ∅ ↔ ¬a ≤ b
⊢ Disjoint (Ici a) (Iic b) ↔ ¬a ≤ b
have rw₂ : ¬a ≤ b ↔ ¬a ≤ b
Tactic: rw [Set.disjoint_iff_inter_eq_empty, Ici_inter_Iic, Icc_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Disjoint (goal)
Goal:
α : Type v
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
⊢ Disjoint (Ico a₁ a₂) (Ico b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁
have simp_rw : Ico a₁ a₂ ∩ Ico b₁ b₂ = ∅ ↔ min a₂ b₂ ≤ max a₁ b₁
Tactic: simp_rw [Set.disjoint_iff_inter_eq_empty, Ico_inter_Ico, Ico_eq_empty_iff, not_lt]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Disjoint (goal)
Goal:
α : Type v
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
simp_rw : Ico a₁ a₂ ∩ Ico b₁ b₂ = ∅ ↔ min a₂ b₂ ≤ max a₁ b₁
⊢ Disjoint (Ico a₁ a₂) (Ico b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁
have simp_rw₁ : Ico (max a₁ b₁) (min a₂ b₂) = ∅ ↔ min a₂ b₂ ≤ max a₁ b₁
Tactic: simp_rw [Set.disjoint_iff_inter_eq_empty, Ico_inter_Ico, Ico_eq_empty_iff, not_lt]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Disjoint (goal)
Goal:
α : Type v
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
simp_rw : Ico a₁ a₂ ∩ Ico b₁ b₂ = ∅ ↔ min a₂ b₂ ≤ max a₁ b₁
simp_rw₁ : Ico (max a₁ b₁) (min a₂ b₂) = ∅ ↔ min a₂ b₂ ≤ max a₁ b₁
⊢ Disjoint (Ico a₁ a₂) (Ico 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 [Set.disjoint_iff_inter_eq_empty, Ico_inter_Ico, Ico_eq_empty_iff, not_lt]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Disjoint (hypothesis)
Goal:
α : Type v
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
⊢ Disjoint (Ioc a₁ a₂) (Ioc b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁
have h : Disjoint (α := Set αᵒᵈ) (Ico ((toDual : (a : α) → αᵒᵈ) a₂) ((toDual : (a : α) → αᵒᵈ) a₁) : Set αᵒᵈ)
    (Ico ((toDual : (a : α) → αᵒᵈ) b₂) ((toDual : (a : α) → αᵒᵈ) b₁) : Set αᵒᵈ) ↔
  LE.le (α := αᵒᵈ) (min ((toDual : (a : α) → αᵒᵈ) a₁) ((toDual : (a : α) → αᵒᵈ) b₁) : αᵒᵈ)
    (max ((toDual : (a : α) → αᵒᵈ) a₂) ((toDual : (a : α) → αᵒᵈ) b₂) : αᵒᵈ)
Tactic: have h : _ ↔ min (toDual a₁) (toDual b₁) ≤ max (toDual a₂) (toDual b₂) := Ico_disjoint_Ico
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Disjoint (goal)
Goal:
α : Type v
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst_1 : DenselyOrdered α
⊢ Disjoint (Ioo a₁ a₂) (Ioo b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁
have simp_rw : Ioo a₁ a₂ ∩ Ioo b₁ b₂ = ∅ ↔ min a₂ b₂ ≤ max a₁ b₁
Tactic: simp_rw [Set.disjoint_iff_inter_eq_empty, Ioo_inter_Ioo, Ioo_eq_empty_iff, not_lt]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Disjoint (goal)
Goal:
α : Type v
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst_1 : DenselyOrdered α
simp_rw : Ioo a₁ a₂ ∩ Ioo b₁ b₂ = ∅ ↔ min a₂ b₂ ≤ max a₁ b₁
⊢ Disjoint (Ioo a₁ a₂) (Ioo b₁ b₂) ↔ min a₂ b₂ ≤ max a₁ b₁
have simp_rw₁ : Ioo (max a₁ b₁) (min a₂ b₂) = ∅ ↔ min a₂ b₂ ≤ max a₁ b₁
Tactic: simp_rw [Set.disjoint_iff_inter_eq_empty, Ioo_inter_Ioo, Ioo_eq_empty_iff, not_lt]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Disjoint (goal)
Goal:
α : Type v
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst_1 : DenselyOrdered α
simp_rw : Ioo a₁ a₂ ∩ Ioo b₁ b₂ = ∅ ↔ min a₂ b₂ ≤ max a₁ b₁
simp_rw₁ : Ioo (max a₁ b₁) (min a₂ b₂) = ∅ ↔ min a₂ b₂ ≤ max a₁ b₁
⊢ Disjoint (Ioo a₁ a₂) (Ioo 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 [Set.disjoint_iff_inter_eq_empty, Ioo_inter_Ioo, Ioo_eq_empty_iff, not_lt]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Disjoint (hypothesis)
Goal:
α : Type v
inst : LinearOrder α
x₁ x₂ y₁ y₂ : α
h : Disjoint (Ico x₁ x₂) (Ico y₁ y₂)
hx : x₁ < x₂
h2 : x₂ ∈ Ico y₁ y₂
⊢ y₁ = x₂
have h₁ : x₂ ≤ x₁ ∨ x₂ ≤ y₁
Tactic: rw [Ico_disjoint_Ico, min_eq_left (le_of_lt h2.2), le_max_iff] at h
Cleared hypotheses: h, hx, h2
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Disjoint (goal)
Goal:
α : Type v
inst : LinearOrder α
x₁ x₂ y₁ y₂ : α
h : x₂ ≤ x₁ ∨ x₂ ≤ y₁
hx : x₁ < x₂
h2 : x₂ ∈ Ico y₁ y₂
⊢ y₁ = x₂
have apply : x₂ ≤ y₁
Tactic: apply le_antisymm h2.1