awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
rw : (Finset.Ico a b).val - Ico c b = Ico a (min b c)
rw₁ : (Finset.Ico a b).val - (Finset.Ico c b).val = Ico a (min b c)
rw₂ : (Finset.Ico a b).val - (Finset.Ico c b).val = (Finset.Ico a (min b c)).val
⊢ Ico a b - Ico c b = Ico a (min b c)
have rw₃ : (Finset.Ico a b \ Finset.Ico c b).val = (Finset.Ico a (min b c)).val
Tactic: rw [Ico, Ico, Ico, ← Finset.sdiff_val, Finset.Ico_diff_Ico_right]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
rw : (Finset.Ico a b).val - Ico c b = Ico a (min b c)
rw₁ : (Finset.Ico a b).val - (Finset.Ico c b).val = Ico a (min b c)
rw₂ : (Finset.Ico a b).val - (Finset.Ico c b).val = (Finset.Ico a (min b c)).val
rw₃ : (Finset.Ico a b \ Finset.Ico c b).val = (Finset.Ico a (min b c)).val
⊢ Ico a b - Ico c b = Ico a (min b c)
have rw₄ : (Finset.Ico a (min b c)).val = (Finset.Ico a (min b c)).val
Tactic: rw [Ico, Ico, Ico, ← Finset.sdiff_val, Finset.Ico_diff_Ico_right]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : One α
inst_2 : IsBotOneClass α
⊢ Eq.{u_1 + 1} (α := Set α) (Iio 1) ∅
have h : ∀ (x : α), Membership.mem (γ := Set α) (Iio 1) x ↔ Membership.mem (γ := Set α) ∅ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : Iic a ⊂ Iic b
⊢ a < b
have obtain : ∀ (ab : Iic a ⊆ Iic b) (c : α) (cb : c ∈ Iic b) (ac : ¬c ∈ Iic a), a < b
Tactic: obtain ⟨ab, c, cb, ac⟩ := ssubset_iff_exists.mp h
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Icc a b = ∅ ↔ ¬a ≤ b
have contrapose! : (Icc a b).Nonempty ↔ a ≤ b
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Ico a b = ∅ ↔ ¬a < b
have contrapose! : (Ico a b).Nonempty ↔ a < b
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
inst_1 : DenselyOrdered α
⊢ Ioo a b = ∅ ↔ ¬a < b
have contrapose! : (Ioo a b).Nonempty ↔ a < b
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : ¬a ≤ b
⊢ Icc a b = Ioc a b
have rw : ∅ = Ioc a b
Tactic: rw [Icc_eq_empty h, Ioc_eq_empty (mt le_of_lt h)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : ¬a ≤ b
rw : ∅ = Ioc a b
⊢ Icc a b = Ioc a b
have rw₁ : Eq.{u_1 + 1} (α := Set α) ∅ ∅
Tactic: rw [Icc_eq_empty h, Ioc_eq_empty (mt le_of_lt h)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : ¬a ≤ b
⊢ Icc a b = Ioo a b
have rw : ∅ = Ioo a b
Tactic: rw [Icc_eq_empty h, Ioo_eq_empty (mt le_of_lt h)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : ¬a ≤ b
rw : ∅ = Ioo a b
⊢ Icc a b = Ioo a b
have rw₁ : Eq.{u_1 + 1} (α := Set α) ∅ ∅
Tactic: rw [Icc_eq_empty h, Ioo_eq_empty (mt le_of_lt h)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : ¬a < b
⊢ Ioc a b = Ico a b
have rw : ∅ = Ico a b
Tactic: rw [Ioc_eq_empty h, Ico_eq_empty h]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : ¬a < b
rw : ∅ = Ico a b
⊢ Ioc a b = Ico a b
have rw₁ : Eq.{u_1 + 1} (α := Set α) ∅ ∅
Tactic: rw [Ioc_eq_empty h, Ico_eq_empty h]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : ¬a < b
⊢ Ioo a b = Ioc a b
have rw : ∅ = Ioc a b
Tactic: rw [Ioo_eq_empty h, Ioc_eq_empty h]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
a b : α
h : ¬a < b
rw : ∅ = Ioc a b
⊢ Ioo a b = Ioc a b
have rw₁ : Eq.{u_1 + 1} (α := Set α) ∅ ∅
Tactic: rw [Ioo_eq_empty h, Ioc_eq_empty h]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
⊢ Icc a b = {c} ↔ a = c ∧ b = c
have refine_1 : ∀ (h : Icc a b = {c}), a = c ∧ b = c
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
refine_1 : ∀ (h : Icc a b = {c}), a = c ∧ b = c
⊢ Icc a b = {c} ↔ a = c ∧ b = c
have refine_2 : a = c ∧ b = c → Icc a b = {c}
Tactic: refine ⟨fun h => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (hypothesis)
Goal:
α : Type u_1
inst : PartialOrder α
a b c : α
h : Icc a b = {c}
⊢ a = c ∧ b = c
have hab : a ≤ b
Tactic: have hab : a ≤ b := nonempty_Icc.1 (h.symm.subst <| singleton_nonempty c)
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
⊢ (Icc a b).Subsingleton ↔ b ≤ a
have refine : ∀ (h : (Icc a b).Subsingleton), b ≤ a
Tactic: refine ⟨fun h ↦ ?_, subsingleton_Icc_of_ge⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
h : (Icc a b).Subsingleton
⊢ b ≤ a
have contrapose! : ∀ (h : a < b), (Icc a b).Nontrivial
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
⊢ Icc a b \ {a, b} = Ioo a b
have rw : Icc a b \ ({a} ∪ {b}) = Ioo a b
Tactic: rw [insert_eq, ← diff_diff, Icc_diff_left, Ioc_diff_right]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
rw : Icc a b \ ({a} ∪ {b}) = Ioo a b
⊢ Icc a b \ {a, b} = Ioo a b
have rw₁ : (Icc a b \ {a}) \ {b} = Ioo a b
Tactic: rw [insert_eq, ← diff_diff, Icc_diff_left, Ioc_diff_right]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
rw : Icc a b \ ({a} ∪ {b}) = Ioo a b
rw₁ : (Icc a b \ {a}) \ {b} = Ioo a b
⊢ Icc a b \ {a, b} = Ioo a b
have rw₂ : Ioc a b \ {b} = Ioo a b
Tactic: rw [insert_eq, ← diff_diff, Icc_diff_left, Ioc_diff_right]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
rw : Icc a b \ ({a} ∪ {b}) = Ioo a b
rw₁ : (Icc a b \ {a}) \ {b} = Ioo a b
rw₂ : Ioc a b \ {b} = Ioo a b
⊢ Icc a b \ {a, b} = Ioo a b
have rw₃ : Ioo a b = Ioo a b
Tactic: rw [insert_eq, ← diff_diff, Icc_diff_left, Ioc_diff_right]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a < b
⊢ Ico a b \ Ioo a b = {a}
have rw : Ico a b \ (Ico a b \ {a}) = {a}
Tactic: rw [← Ico_diff_left, diff_diff_cancel_left (singleton_subset_iff.2 <| left_mem_Ico.2 h)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a < b
rw : Ico a b \ (Ico a b \ {a}) = {a}
⊢ Ico a b \ Ioo a b = {a}
have rw₁ : Eq (α := Set α) {a} {a}
Tactic: rw [← Ico_diff_left, diff_diff_cancel_left (singleton_subset_iff.2 <| left_mem_Ico.2 h)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a ≤ b
⊢ Icc a b \ Ico a b = {b}
have rw : Icc a b \ (Icc a b \ {b}) = {b}
Tactic: rw [← Icc_diff_right, diff_diff_cancel_left (singleton_subset_iff.2 <| right_mem_Icc.2 h)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a ≤ b
rw : Icc a b \ (Icc a b \ {b}) = {b}
⊢ Icc a b \ Ico a b = {b}
have rw₁ : Eq (α := Set α) {b} {b}
Tactic: rw [← Icc_diff_right, diff_diff_cancel_left (singleton_subset_iff.2 <| right_mem_Icc.2 h)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a ≤ b
⊢ Icc a b \ Ioo a b = {a, b}
have rw : {a, b} ⊆ Icc a b
Tactic: rw [← Icc_diff_both, diff_diff_cancel_left]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a : α
⊢ Iic a \ Iio a = {a}
have rw : Iic a \ (Iic a \ {a}) = {a}
Tactic: rw [← Iic_diff_right, diff_diff_cancel_left (singleton_subset_iff.2 self_mem_Iic)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a : α
rw : Iic a \ (Iic a \ {a}) = {a}
⊢ Iic a \ Iio a = {a}
have rw₁ : Eq (α := Set α) {a} {a}
Tactic: rw [← Iic_diff_right, diff_diff_cancel_left (singleton_subset_iff.2 self_mem_Iic)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
hab : a < b
⊢ Ioo a b ∪ {a} = Ico a b
have rw : Ico a b \ {a} ∪ {a} = Ico a b
Tactic: rw [← Ico_diff_left, diff_union_self,
    union_eq_self_of_subset_right (singleton_subset_iff.2 <| left_mem_Ico.2 hab)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
hab : a < b
rw : Ico a b \ {a} ∪ {a} = Ico a b
⊢ Ioo a b ∪ {a} = Ico a b
have rw₁ : Ico a b ∪ {a} = Ico a b
Tactic: rw [← Ico_diff_left, diff_union_self,
    union_eq_self_of_subset_right (singleton_subset_iff.2 <| left_mem_Ico.2 hab)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
hab : a < b
rw : Ico a b \ {a} ∪ {a} = Ico a b
rw₁ : Ico a b ∪ {a} = Ico a b
⊢ Ioo a b ∪ {a} = Ico a b
have rw₂ : Ico a b = Ico a b
Tactic: rw [← Ico_diff_left, diff_union_self,
    union_eq_self_of_subset_right (singleton_subset_iff.2 <| left_mem_Ico.2 hab)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (hypothesis)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a ≤ b
⊢ Ioo a b ∪ {a, b} = Icc a b
have this : Icc a b \ {a, b} ∪ {a, b} = Icc a b
Tactic: have : (Icc a b \ {a, b}) ∪ {a, b} = Icc a b := diff_union_of_subset fun
    | x, .inl rfl => left_mem_Icc.mpr h
    | x, .inr rfl => right_mem_Icc.mpr h
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a ≤ b
this : Icc a b \ {a, b} ∪ {a, b} = Icc a b
⊢ Ioo a b ∪ {a, b} = Icc a b
have rw : Ioo a b ∪ {a, b} = Icc a b \ {a, b} ∪ {a, b}
Tactic: rw [← this, Icc_diff_both]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a ≤ b
this : Icc a b \ {a, b} ∪ {a, b} = Icc a b
rw : Ioo a b ∪ {a, b} = Icc a b \ {a, b} ∪ {a, b}
⊢ Ioo a b ∪ {a, b} = Icc a b
have rw₁ : Ioo a b ∪ {a, b} = Ioo a b ∪ {a, b}
Tactic: rw [← this, Icc_diff_both]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
hab : a ≤ b
⊢ Ioc a b ∪ {a} = Icc a b
have rw : Icc a b \ {a} ∪ {a} = Icc a b
Tactic: rw [← Icc_diff_left, diff_union_self,
    union_eq_self_of_subset_right (singleton_subset_iff.2 <| left_mem_Icc.2 hab)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
hab : a ≤ b
rw : Icc a b \ {a} ∪ {a} = Icc a b
⊢ Ioc a b ∪ {a} = Icc a b
have rw₁ : Icc a b ∪ {a} = Icc a b
Tactic: rw [← Icc_diff_left, diff_union_self,
    union_eq_self_of_subset_right (singleton_subset_iff.2 <| left_mem_Icc.2 hab)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
hab : a ≤ b
rw : Icc a b \ {a} ∪ {a} = Icc a b
rw₁ : Icc a b ∪ {a} = Icc a b
⊢ Ioc a b ∪ {a} = Icc a b
have rw₂ : Icc a b = Icc a b
Tactic: rw [← Icc_diff_left, diff_union_self,
    union_eq_self_of_subset_right (singleton_subset_iff.2 <| left_mem_Icc.2 hab)]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a ≤ b
⊢ insert b (Ico a b) = Icc a b
have rw : {b} ∪ Ico a b = Icc a b
Tactic: rw [insert_eq, union_comm, Ico_union_right h]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a ≤ b
rw : {b} ∪ Ico a b = Icc a b
⊢ insert b (Ico a b) = Icc a b
have rw₁ : Ico a b ∪ {b} = Icc a b
Tactic: rw [insert_eq, union_comm, Ico_union_right h]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a ≤ b
rw : {b} ∪ Ico a b = Icc a b
rw₁ : Ico a b ∪ {b} = Icc a b
⊢ insert b (Ico a b) = Icc a b
have rw₂ : Icc a b = Icc a b
Tactic: rw [insert_eq, union_comm, Ico_union_right h]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a < b
⊢ insert a (Ioo a b) = Ico a b
have rw : {a} ∪ Ioo a b = Ico a b
Tactic: rw [insert_eq, union_comm, Ioo_union_left h]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a < b
rw : {a} ∪ Ioo a b = Ico a b
⊢ insert a (Ioo a b) = Ico a b
have rw₁ : Ioo a b ∪ {a} = Ico a b
Tactic: rw [insert_eq, union_comm, Ioo_union_left h]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a b : α
h : a < b
rw : {a} ∪ Ioo a b = Ico a b
rw₁ : Ioo a b ∪ {a} = Ico a b
⊢ insert a (Ioo a b) = Ico a b
have rw₂ : Ico a b = Ico a b
Tactic: rw [insert_eq, union_comm, Ioo_union_left h]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Basic (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a : α
s : Set α
ho : Iio a ⊆ s
hc : s ⊆ Iic a
h : a ∈ s
⊢ Iic a ⊆ s
have rw : Iio a ⊆ s ∧ {a} ⊆ s
Tactic: rw [← Iio_union_right, union_subset_iff]
-- 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: by_cases ha : a ∈ s
-- 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: by_cases ha : a ∈ s
-- 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
⊢ Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
have pos : ∀ (hb : b ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
Tactic: by_cases hb : b ∈ s
-- 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
pos : ∀ (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 : ∀ (hb : ¬b ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
Tactic: by_cases hb : b ∈ s
-- 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
⊢ Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
have pos : ∀ (hb : b ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
Tactic: by_cases hb : b ∈ s
-- 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
pos : ∀ (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 : ∀ (hb : ¬b ∈ s), Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
Tactic: by_cases hb : b ∈ s
-- 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 pos : Icc a b ⊆ s
Tactic: refine Or.inl (Subset.antisymm hc ?_)
-- 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
⊢ Icc a b ⊆ s
have pos : ∀ (ho : Ico a b \ {a} ⊆ s) (hc : s ⊆ Icc a b) (ha : a ∈ s) (hb : b ∈ s), Icc a b ⊆ s
Tactic: 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
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 : Ico a b \ {a} ⊆ s) (hc : s ⊆ Icc a b) (ha : a ∈ s) (hb : b ∈ s), Icc a b ⊆ s
⊢ Icc a b ⊆ s
have pos₁ : ∀ (ho : Ico a b ⊆ insert a s) (hc : s ⊆ Icc a b) (ha : a ∈ s) (hb : b ∈ s), Icc a b ⊆ s
Tactic: 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
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 : Ico a b \ {a} ⊆ s) (hc : s ⊆ Icc a b) (ha : a ∈ s) (hb : b ∈ s), Icc a b ⊆ s
pos₁ : ∀ (ho : Ico a b ⊆ insert a s) (hc : s ⊆ Icc a b) (ha : a ∈ s) (hb : b ∈ s), Icc a b ⊆ s
⊢ Icc a b ⊆ s
have pos₂ : ∀ (ho : Ico a b ⊆ s) (hc : s ⊆ Icc a b) (ha : a ∈ s) (hb : b ∈ s), Icc a b ⊆ s
Tactic: 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
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 : Ico a b \ {a} ⊆ s) (hc : s ⊆ Icc a b) (ha : a ∈ s) (hb : b ∈ s), Icc a b ⊆ s
pos₁ : ∀ (ho : Ico a b ⊆ insert a s) (hc : s ⊆ Icc a b) (ha : a ∈ s) (hb : b ∈ s), Icc a b ⊆ s
pos₂ : ∀ (ho : Ico a b ⊆ s) (hc : s ⊆ Icc a b) (ha : a ∈ s) (hb : b ∈ s), Icc a b ⊆ s
⊢ Icc a b ⊆ s
have pos₃ : ∀ (ho : Icc a b \ {b} ⊆ s) (hc : s ⊆ Icc a b) (ha : a ∈ s) (hb : b ∈ s), Icc a b ⊆ s
Tactic: 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
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 : Ico a b \ {a} ⊆ s) (hc : s ⊆ Icc a b) (ha : a ∈ s) (hb : b ∈ s), Icc a b ⊆ s
pos₁ : ∀ (ho : Ico a b ⊆ insert a s) (hc : s ⊆ Icc a b) (ha : a ∈ s) (hb : b ∈ s), Icc a b ⊆ s
pos₂ : ∀ (ho : Ico a b ⊆ s) (hc : s ⊆ Icc a b) (ha : a ∈ s) (hb : b ∈ s), Icc a b ⊆ s
pos₃ : ∀ (ho : Icc a b \ {b} ⊆ s) (hc : s ⊆ Icc a b) (ha : a ∈ s) (hb : b ∈ s), Icc a b ⊆ s
⊢ Icc a b ⊆ s
have pos₄ : ∀ (ho : Icc a b ⊆ insert b s) (hc : s ⊆ Icc a b) (ha : a ∈ s) (hb : b ∈ s), Icc a b ⊆ s
Tactic: 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
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 : Ico a b \ {a} ⊆ s) (hc : s ⊆ Icc a b) (ha : a ∈ s) (hb : b ∈ s), Icc a b ⊆ s
pos₁ : ∀ (ho : Ico a b ⊆ insert a s) (hc : s ⊆ Icc a b) (ha : a ∈ s) (hb : b ∈ s), Icc a b ⊆ s
pos₂ : ∀ (ho : Ico a b ⊆ s) (hc : s ⊆ Icc a b) (ha : a ∈ s) (hb : b ∈ s), Icc a b ⊆ s
pos₃ : ∀ (ho : Icc a b \ {b} ⊆ s) (hc : s ⊆ Icc a b) (ha : a ∈ s) (hb : b ∈ s), Icc a b ⊆ s
pos₄ : ∀ (ho : Icc a b ⊆ insert b s) (hc : s ⊆ Icc a b) (ha : a ∈ s) (hb : b ∈ s), Icc a b ⊆ s
⊢ Icc a b ⊆ s
have pos₅ : ∀ (ho : Icc a b ⊆ s) (hc : s ⊆ Icc a b) (ha : a ∈ s) (hb : b ∈ s), Icc a b ⊆ s
Tactic: 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
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 ⊆ Ico a b
Tactic: refine Or.inr <| Or.inl <| Subset.antisymm ?_ ?_
-- 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
neg : s ⊆ Ico a b
⊢ Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
have neg₁ : Ico a b ⊆ s
Tactic: refine Or.inr <| Or.inl <| Subset.antisymm ?_ ?_
-- 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 ⊆ Ico a b
have neg : s ⊆ Icc a b \ {b}
Tactic: rw [← 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
ha : a ∈ s
hb : ¬b ∈ s
⊢ Ico a b ⊆ s
have neg : ∀ (ho : Ico a b \ {a} ⊆ s) (hc : s ⊆ Icc a b) (ha : a ∈ s) (hb : ¬b ∈ s), Ico a b ⊆ s
Tactic: rwa [← Ico_diff_left, diff_singleton_subset_iff, insert_eq_of_mem ha] 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
neg : ∀ (ho : Ico a b \ {a} ⊆ s) (hc : s ⊆ Icc a b) (ha : a ∈ s) (hb : ¬b ∈ s), Ico a b ⊆ s
⊢ Ico a b ⊆ s
have neg₁ : ∀ (ho : Ico a b ⊆ insert a s) (hc : s ⊆ Icc a b) (ha : a ∈ s) (hb : ¬b ∈ s), Ico a b ⊆ s
Tactic: rwa [← Ico_diff_left, diff_singleton_subset_iff, insert_eq_of_mem ha] 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
neg : ∀ (ho : Ico a b \ {a} ⊆ s) (hc : s ⊆ Icc a b) (ha : a ∈ s) (hb : ¬b ∈ s), Ico a b ⊆ s
neg₁ : ∀ (ho : Ico a b ⊆ insert a s) (hc : s ⊆ Icc a b) (ha : a ∈ s) (hb : ¬b ∈ s), Ico a b ⊆ s
⊢ Ico a b ⊆ s
have neg₂ : ∀ (ho : Ico a b ⊆ s) (hc : s ⊆ Icc a b) (ha : a ∈ s) (hb : ¬b ∈ s), Ico a b ⊆ s
Tactic: rwa [← Ico_diff_left, diff_singleton_subset_iff, insert_eq_of_mem ha] 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 pos : s ⊆ Ioc a b
Tactic: refine Or.inr <| Or.inr <| Or.inl <| Subset.antisymm ?_ ?_
-- 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 : s ⊆ Ioc a b
⊢ Membership.mem (γ := Set (Set α)) {Icc a b, Ico a b, Ioc a b, Ioo a b} s
have pos₁ : Ioc a b ⊆ s
Tactic: refine Or.inr <| Or.inr <| Or.inl <| Subset.antisymm ?_ ?_
-- 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 ⊆ Ioc a b
have pos : s ⊆ Icc a b \ {a}
Tactic: rw [← Icc_diff_left]