awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a : α
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
⊢ (Iio a).Nonempty ↔ ¬IsMin a
have contrapose! : Iio a = ∅ ↔ IsMin a
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
inst_2 : OrderTop α
inst_3 : Fintype α
⊢ Eq.{u_2 + 1} (α := Finset α) (Iic ⊤) univ
have h : ∀ (a : α), Membership.mem (γ := Finset α) (Iic ⊤) a ↔ Membership.mem (γ := Finset α) univ a
Tactic: ext a
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
a_1 a₁ a₂ b_1 b₁ b₂ c x : α
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
inst_2 : LocallyFiniteOrder α
a : α
b : (↑(Set.Iic a) : Type u_2)
⊢ (↑b : α) ∈ Iic a
have rw : (↑b : α) ∈ Set.Iic a
Tactic: rw [← mem_coe, coe_Iic a]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
a : α
inst_2 : Fintype α
inst_3 : DecidablePred fun (x : α) ↦ a < x
⊢ {x : α | a < x} = Ioi a
have h : ∀ (a_1 : α), Membership.mem (γ := Finset α) {x : α | a < x} a_1 ↔ a_1 ∈ Ioi a
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
a : α
inst_2 : Fintype α
inst_3 : DecidablePred fun (x : α) ↦ a ≤ x
⊢ {x : α | a ≤ x} = Ici a
have h : ∀ (a_1 : α), Membership.mem (γ := Finset α) {x : α | a ≤ x} a_1 ↔ a_1 ∈ Ici a
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
a : α
inst_2 : Fintype α
inst_3 : DecidablePred fun (x : α) ↦ x < a
⊢ {x : α | x < a} = Iio a
have h : ∀ (a_1 : α), Membership.mem (γ := Finset α) {x : α | x < a} a_1 ↔ a_1 ∈ Iio a
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrderBot α
a : α
inst_2 : Fintype α
inst_3 : DecidablePred fun (x : α) ↦ x ≤ a
⊢ {x : α | x ≤ a} = Iic a
have h : ∀ (a_1 : α), Membership.mem (γ := Finset α) {x : α | x ≤ a} a_1 ↔ a_1 ∈ Iic a
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : BoundedOrder α
inst_3 : Fintype α
⊢ Eq.{u_2 + 1} (α := Finset α) (Icc ⊥ ⊤) univ
have rw : Eq.{u_2 + 1} (α := Finset α) (Iic ⊤) univ
Tactic: rw [Icc_bot, Iic_top]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : BoundedOrder α
inst_3 : Fintype α
rw : Eq.{u_2 + 1} (α := Finset α) (Iic ⊤) univ
⊢ Eq.{u_2 + 1} (α := Finset α) (Icc ⊥ ⊤) univ
have rw₁ : Eq.{u_2 + 1} (α := Finset α) univ univ
Tactic: rw [Icc_bot, Iic_top]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a : α
⊢ Icc a a = {a}
have rw : (↑(Icc a a) : Set α) = {a}
Tactic: rw [← coe_eq_singleton, coe_Icc, Set.Icc_self]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a : α
rw : (↑(Icc a a) : Set α) = {a}
⊢ Icc a a = {a}
have rw₁ : Set.Icc a a = {a}
Tactic: rw [← coe_eq_singleton, coe_Icc, Set.Icc_self]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a : α
rw : (↑(Icc a a) : Set α) = {a}
rw₁ : Set.Icc a a = {a}
⊢ Icc a a = {a}
have rw₂ : Eq (α := Set α) {a} {a}
Tactic: rw [← coe_eq_singleton, coe_Icc, Set.Icc_self]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
⊢ Icc a b = {c} ↔ a = c ∧ b = c
have rw : (↑(Icc a b) : Set α) = {c} ↔ a = c ∧ b = c
Tactic: rw [← coe_eq_singleton, coe_Icc, Set.Icc_eq_singleton_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
rw : (↑(Icc a b) : Set α) = {c} ↔ a = c ∧ b = c
⊢ Icc a b = {c} ↔ a = c ∧ b = c
have rw₁ : Set.Icc a b = {c} ↔ a = c ∧ b = c
Tactic: rw [← coe_eq_singleton, coe_Icc, Set.Icc_eq_singleton_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
rw : (↑(Icc a b) : Set α) = {c} ↔ a = c ∧ b = c
rw₁ : Set.Icc a b = {c} ↔ a = c ∧ b = c
⊢ Icc a b = {c} ↔ a = c ∧ b = c
have rw₂ : a = c ∧ b = c ↔ a = c ∧ b = c
Tactic: rw [← coe_eq_singleton, coe_Icc, Set.Icc_eq_singleton_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
a_1 a₁ a₂ b_1 b₁ b₂ c_1 x : α
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
inst_2 : OrderBot α
⊢ Unique ↥(Iic ⊥)
have rw : Unique ↥{⊥}
Tactic: rw [Iic_bot]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidableEq α
h : a ≤ b
⊢ insert b (Ico a b) = Icc a b
have rw : (↑(insert b (Ico a b)) : Set α) = (↑(Icc a b) : Set α)
Tactic: rw [← coe_inj, coe_insert, coe_Icc, coe_Ico, Set.insert_eq, Set.union_comm, Set.Ico_union_right h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidableEq α
h : a ≤ b
rw : (↑(insert b (Ico a b)) : Set α) = (↑(Icc a b) : Set α)
⊢ insert b (Ico a b) = Icc a b
have rw₁ : insert b (↑(Ico a b) : Set α) = (↑(Icc a b) : Set α)
Tactic: rw [← coe_inj, coe_insert, coe_Icc, coe_Ico, Set.insert_eq, Set.union_comm, Set.Ico_union_right h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidableEq α
h : a ≤ b
rw : (↑(insert b (Ico a b)) : Set α) = (↑(Icc a b) : Set α)
rw₁ : insert b (↑(Ico a b) : Set α) = (↑(Icc a b) : Set α)
⊢ insert b (Ico a b) = Icc a b
have rw₂ : insert b (↑(Ico a b) : Set α) = Set.Icc a b
Tactic: rw [← coe_inj, coe_insert, coe_Icc, coe_Ico, Set.insert_eq, Set.union_comm, Set.Ico_union_right h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidableEq α
h : a ≤ b
rw : (↑(insert b (Ico a b)) : Set α) = (↑(Icc a b) : Set α)
rw₁ : insert b (↑(Ico a b) : Set α) = (↑(Icc a b) : Set α)
rw₂ : insert b (↑(Ico a b) : Set α) = Set.Icc a b
⊢ insert b (Ico a b) = Icc a b
have rw₃ : insert b (Set.Ico a b) = Set.Icc a b
Tactic: rw [← coe_inj, coe_insert, coe_Icc, coe_Ico, Set.insert_eq, Set.union_comm, Set.Ico_union_right h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidableEq α
h : a ≤ b
rw : (↑(insert b (Ico a b)) : Set α) = (↑(Icc a b) : Set α)
rw₁ : insert b (↑(Ico a b) : Set α) = (↑(Icc a b) : Set α)
rw₂ : insert b (↑(Ico a b) : Set α) = Set.Icc a b
rw₃ : insert b (Set.Ico a b) = Set.Icc a b
⊢ insert b (Ico a b) = Icc a b
have rw₄ : {b} ∪ Set.Ico a b = Set.Icc a b
Tactic: rw [← coe_inj, coe_insert, coe_Icc, coe_Ico, Set.insert_eq, Set.union_comm, Set.Ico_union_right h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidableEq α
h : a ≤ b
rw : (↑(insert b (Ico a b)) : Set α) = (↑(Icc a b) : Set α)
rw₁ : insert b (↑(Ico a b) : Set α) = (↑(Icc a b) : Set α)
rw₂ : insert b (↑(Ico a b) : Set α) = Set.Icc a b
rw₃ : insert b (Set.Ico a b) = Set.Icc a b
rw₄ : {b} ∪ Set.Ico a b = Set.Icc a b
⊢ insert b (Ico a b) = Icc a b
have rw₅ : Set.Ico a b ∪ {b} = Set.Icc a b
Tactic: rw [← coe_inj, coe_insert, coe_Icc, coe_Ico, Set.insert_eq, Set.union_comm, Set.Ico_union_right h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidableEq α
h : a ≤ b
rw : (↑(insert b (Ico a b)) : Set α) = (↑(Icc a b) : Set α)
rw₁ : insert b (↑(Ico a b) : Set α) = (↑(Icc a b) : Set α)
rw₂ : insert b (↑(Ico a b) : Set α) = Set.Icc a b
rw₃ : insert b (Set.Ico a b) = Set.Icc a b
rw₄ : {b} ∪ Set.Ico a b = Set.Icc a b
rw₅ : Set.Ico a b ∪ {b} = Set.Icc a b
⊢ insert b (Ico a b) = Icc a b
have rw₆ : Set.Icc a b = Set.Icc a b
Tactic: rw [← coe_inj, coe_insert, coe_Icc, coe_Ico, Set.insert_eq, Set.union_comm, Set.Ico_union_right h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidableEq α
h : a ≤ b
⊢ insert a (Ioc a b) = Icc a b
have rw : (↑(insert a (Ioc a b)) : Set α) = (↑(Icc a b) : Set α)
Tactic: rw [← coe_inj, coe_insert, coe_Ioc, coe_Icc, Set.insert_eq, Set.union_comm, Set.Ioc_union_left h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidableEq α
h : a ≤ b
rw : (↑(insert a (Ioc a b)) : Set α) = (↑(Icc a b) : Set α)
⊢ insert a (Ioc a b) = Icc a b
have rw₁ : insert a (↑(Ioc a b) : Set α) = (↑(Icc a b) : Set α)
Tactic: rw [← coe_inj, coe_insert, coe_Ioc, coe_Icc, Set.insert_eq, Set.union_comm, Set.Ioc_union_left h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidableEq α
h : a ≤ b
rw : (↑(insert a (Ioc a b)) : Set α) = (↑(Icc a b) : Set α)
rw₁ : insert a (↑(Ioc a b) : Set α) = (↑(Icc a b) : Set α)
⊢ insert a (Ioc a b) = Icc a b
have rw₂ : insert a (Set.Ioc a b) = (↑(Icc a b) : Set α)
Tactic: rw [← coe_inj, coe_insert, coe_Ioc, coe_Icc, Set.insert_eq, Set.union_comm, Set.Ioc_union_left h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidableEq α
h : a ≤ b
rw : (↑(insert a (Ioc a b)) : Set α) = (↑(Icc a b) : Set α)
rw₁ : insert a (↑(Ioc a b) : Set α) = (↑(Icc a b) : Set α)
rw₂ : insert a (Set.Ioc a b) = (↑(Icc a b) : Set α)
⊢ insert a (Ioc a b) = Icc a b
have rw₃ : insert a (Set.Ioc a b) = Set.Icc a b
Tactic: rw [← coe_inj, coe_insert, coe_Ioc, coe_Icc, Set.insert_eq, Set.union_comm, Set.Ioc_union_left h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidableEq α
h : a ≤ b
rw : (↑(insert a (Ioc a b)) : Set α) = (↑(Icc a b) : Set α)
rw₁ : insert a (↑(Ioc a b) : Set α) = (↑(Icc a b) : Set α)
rw₂ : insert a (Set.Ioc a b) = (↑(Icc a b) : Set α)
rw₃ : insert a (Set.Ioc a b) = Set.Icc a b
⊢ insert a (Ioc a b) = Icc a b
have rw₄ : {a} ∪ Set.Ioc a b = Set.Icc a b
Tactic: rw [← coe_inj, coe_insert, coe_Ioc, coe_Icc, Set.insert_eq, Set.union_comm, Set.Ioc_union_left h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidableEq α
h : a ≤ b
rw : (↑(insert a (Ioc a b)) : Set α) = (↑(Icc a b) : Set α)
rw₁ : insert a (↑(Ioc a b) : Set α) = (↑(Icc a b) : Set α)
rw₂ : insert a (Set.Ioc a b) = (↑(Icc a b) : Set α)
rw₃ : insert a (Set.Ioc a b) = Set.Icc a b
rw₄ : {a} ∪ Set.Ioc a b = Set.Icc a b
⊢ insert a (Ioc a b) = Icc a b
have rw₅ : Set.Ioc a b ∪ {a} = Set.Icc a b
Tactic: rw [← coe_inj, coe_insert, coe_Ioc, coe_Icc, Set.insert_eq, Set.union_comm, Set.Ioc_union_left h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidableEq α
h : a ≤ b
rw : (↑(insert a (Ioc a b)) : Set α) = (↑(Icc a b) : Set α)
rw₁ : insert a (↑(Ioc a b) : Set α) = (↑(Icc a b) : Set α)
rw₂ : insert a (Set.Ioc a b) = (↑(Icc a b) : Set α)
rw₃ : insert a (Set.Ioc a b) = Set.Icc a b
rw₄ : {a} ∪ Set.Ioc a b = Set.Icc a b
rw₅ : Set.Ioc a b ∪ {a} = Set.Icc a b
⊢ insert a (Ioc a b) = Icc a b
have rw₆ : Set.Icc a b = Set.Icc a b
Tactic: rw [← coe_inj, coe_insert, coe_Ioc, coe_Icc, Set.insert_eq, Set.union_comm, Set.Ioc_union_left h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidableEq α
h : a < b
⊢ insert a (Ioo a b) = Ico a b
have rw : (↑(insert a (Ioo a b)) : Set α) = (↑(Ico a b) : Set α)
Tactic: rw [← coe_inj, coe_insert, coe_Ioo, coe_Ico, Set.insert_eq, Set.union_comm, Set.Ioo_union_left h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidableEq α
h : a < b
rw : (↑(insert a (Ioo a b)) : Set α) = (↑(Ico a b) : Set α)
⊢ insert a (Ioo a b) = Ico a b
have rw₁ : insert a (↑(Ioo a b) : Set α) = (↑(Ico a b) : Set α)
Tactic: rw [← coe_inj, coe_insert, coe_Ioo, coe_Ico, Set.insert_eq, Set.union_comm, Set.Ioo_union_left h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidableEq α
h : a < b
rw : (↑(insert a (Ioo a b)) : Set α) = (↑(Ico a b) : Set α)
rw₁ : insert a (↑(Ioo a b) : Set α) = (↑(Ico a b) : Set α)
⊢ insert a (Ioo a b) = Ico a b
have rw₂ : insert a (Set.Ioo a b) = (↑(Ico a b) : Set α)
Tactic: rw [← coe_inj, coe_insert, coe_Ioo, coe_Ico, Set.insert_eq, Set.union_comm, Set.Ioo_union_left h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidableEq α
h : a < b
rw : (↑(insert a (Ioo a b)) : Set α) = (↑(Ico a b) : Set α)
rw₁ : insert a (↑(Ioo a b) : Set α) = (↑(Ico a b) : Set α)
rw₂ : insert a (Set.Ioo a b) = (↑(Ico a b) : Set α)
⊢ insert a (Ioo a b) = Ico a b
have rw₃ : insert a (Set.Ioo a b) = Set.Ico a b
Tactic: rw [← coe_inj, coe_insert, coe_Ioo, coe_Ico, Set.insert_eq, Set.union_comm, Set.Ioo_union_left h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidableEq α
h : a < b
rw : (↑(insert a (Ioo a b)) : Set α) = (↑(Ico a b) : Set α)
rw₁ : insert a (↑(Ioo a b) : Set α) = (↑(Ico a b) : Set α)
rw₂ : insert a (Set.Ioo a b) = (↑(Ico a b) : Set α)
rw₃ : insert a (Set.Ioo a b) = Set.Ico a b
⊢ insert a (Ioo a b) = Ico a b
have rw₄ : {a} ∪ Set.Ioo a b = Set.Ico a b
Tactic: rw [← coe_inj, coe_insert, coe_Ioo, coe_Ico, Set.insert_eq, Set.union_comm, Set.Ioo_union_left h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidableEq α
h : a < b
rw : (↑(insert a (Ioo a b)) : Set α) = (↑(Ico a b) : Set α)
rw₁ : insert a (↑(Ioo a b) : Set α) = (↑(Ico a b) : Set α)
rw₂ : insert a (Set.Ioo a b) = (↑(Ico a b) : Set α)
rw₃ : insert a (Set.Ioo a b) = Set.Ico a b
rw₄ : {a} ∪ Set.Ioo a b = Set.Ico a b
⊢ insert a (Ioo a b) = Ico a b
have rw₅ : Set.Ioo a b ∪ {a} = Set.Ico a b
Tactic: rw [← coe_inj, coe_insert, coe_Ioo, coe_Ico, Set.insert_eq, Set.union_comm, Set.Ioo_union_left h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidableEq α
h : a < b
rw : (↑(insert a (Ioo a b)) : Set α) = (↑(Ico a b) : Set α)
rw₁ : insert a (↑(Ioo a b) : Set α) = (↑(Ico a b) : Set α)
rw₂ : insert a (Set.Ioo a b) = (↑(Ico a b) : Set α)
rw₃ : insert a (Set.Ioo a b) = Set.Ico a b
rw₄ : {a} ∪ Set.Ioo a b = Set.Ico a b
rw₅ : Set.Ioo a b ∪ {a} = Set.Ico a b
⊢ insert a (Ioo a b) = Ico a b
have rw₆ : Set.Ico a b = Set.Ico a b
Tactic: rw [← coe_inj, coe_insert, coe_Ioo, coe_Ico, Set.insert_eq, Set.union_comm, Set.Ioo_union_left h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidableEq α
h : a < b
⊢ insert b (Ioo a b) = Ioc a b
have rw : (↑(insert b (Ioo a b)) : Set α) = (↑(Ioc a b) : Set α)
Tactic: rw [← coe_inj, coe_insert, coe_Ioo, coe_Ioc, Set.insert_eq, Set.union_comm, Set.Ioo_union_right h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidableEq α
h : a < b
rw : (↑(insert b (Ioo a b)) : Set α) = (↑(Ioc a b) : Set α)
⊢ insert b (Ioo a b) = Ioc a b
have rw₁ : insert b (↑(Ioo a b) : Set α) = (↑(Ioc a b) : Set α)
Tactic: rw [← coe_inj, coe_insert, coe_Ioo, coe_Ioc, Set.insert_eq, Set.union_comm, Set.Ioo_union_right h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidableEq α
h : a < b
rw : (↑(insert b (Ioo a b)) : Set α) = (↑(Ioc a b) : Set α)
rw₁ : insert b (↑(Ioo a b) : Set α) = (↑(Ioc a b) : Set α)
⊢ insert b (Ioo a b) = Ioc a b
have rw₂ : insert b (Set.Ioo a b) = (↑(Ioc a b) : Set α)
Tactic: rw [← coe_inj, coe_insert, coe_Ioo, coe_Ioc, Set.insert_eq, Set.union_comm, Set.Ioo_union_right h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidableEq α
h : a < b
rw : (↑(insert b (Ioo a b)) : Set α) = (↑(Ioc a b) : Set α)
rw₁ : insert b (↑(Ioo a b) : Set α) = (↑(Ioc a b) : Set α)
rw₂ : insert b (Set.Ioo a b) = (↑(Ioc a b) : Set α)
⊢ insert b (Ioo a b) = Ioc a b
have rw₃ : insert b (Set.Ioo a b) = Set.Ioc a b
Tactic: rw [← coe_inj, coe_insert, coe_Ioo, coe_Ioc, Set.insert_eq, Set.union_comm, Set.Ioo_union_right h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidableEq α
h : a < b
rw : (↑(insert b (Ioo a b)) : Set α) = (↑(Ioc a b) : Set α)
rw₁ : insert b (↑(Ioo a b) : Set α) = (↑(Ioc a b) : Set α)
rw₂ : insert b (Set.Ioo a b) = (↑(Ioc a b) : Set α)
rw₃ : insert b (Set.Ioo a b) = Set.Ioc a b
⊢ insert b (Ioo a b) = Ioc a b
have rw₄ : {b} ∪ Set.Ioo a b = Set.Ioc a b
Tactic: rw [← coe_inj, coe_insert, coe_Ioo, coe_Ioc, Set.insert_eq, Set.union_comm, Set.Ioo_union_right h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidableEq α
h : a < b
rw : (↑(insert b (Ioo a b)) : Set α) = (↑(Ioc a b) : Set α)
rw₁ : insert b (↑(Ioo a b) : Set α) = (↑(Ioc a b) : Set α)
rw₂ : insert b (Set.Ioo a b) = (↑(Ioc a b) : Set α)
rw₃ : insert b (Set.Ioo a b) = Set.Ioc a b
rw₄ : {b} ∪ Set.Ioo a b = Set.Ioc a b
⊢ insert b (Ioo a b) = Ioc a b
have rw₅ : Set.Ioo a b ∪ {b} = Set.Ioc a b
Tactic: rw [← coe_inj, coe_insert, coe_Ioo, coe_Ioc, Set.insert_eq, Set.union_comm, Set.Ioo_union_right h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidableEq α
h : a < b
rw : (↑(insert b (Ioo a b)) : Set α) = (↑(Ioc a b) : Set α)
rw₁ : insert b (↑(Ioo a b) : Set α) = (↑(Ioc a b) : Set α)
rw₂ : insert b (Set.Ioo a b) = (↑(Ioc a b) : Set α)
rw₃ : insert b (Set.Ioo a b) = Set.Ioc a b
rw₄ : {b} ∪ Set.Ioo a b = Set.Ioc a b
rw₅ : Set.Ioo a b ∪ {b} = Set.Ioc a b
⊢ insert b (Ioo a b) = Ioc a b
have rw₆ : Set.Ioc a b = Set.Ioc a b
Tactic: rw [← coe_inj, coe_insert, coe_Ioo, coe_Ioc, Set.insert_eq, Set.union_comm, Set.Ioo_union_right h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ Icc a b = cons b (Ico a b) ⋯
have rw : Icc a b = insert b (Ico a b)
Tactic: rw [cons_eq_insert, Ico_insert_right h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a ≤ b
rw : Icc a b = insert b (Ico a b)
⊢ Icc a b = cons b (Ico a b) ⋯
have rw₁ : Icc a b = Icc a b
Tactic: rw [cons_eq_insert, Ico_insert_right h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ Icc a b = cons b (Ico a b) ⋯
have classical : Icc a b = insert b (Ico a b)
Tactic: classical rw [cons_eq_insert, Ico_insert_right h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a ≤ b
classical : Icc a b = insert b (Ico a b)
⊢ Icc a b = cons b (Ico a b) ⋯
have classical₁ : Icc a b = Icc a b
Tactic: classical rw [cons_eq_insert, Ico_insert_right h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ Icc a b = cons a (Ioc a b) ⋯
have rw : Icc a b = insert a (Ioc a b)
Tactic: rw [cons_eq_insert, Ioc_insert_left h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a ≤ b
rw : Icc a b = insert a (Ioc a b)
⊢ Icc a b = cons a (Ioc a b) ⋯
have rw₁ : Icc a b = Icc a b
Tactic: rw [cons_eq_insert, Ioc_insert_left h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ Icc a b = cons a (Ioc a b) ⋯
have classical : Icc a b = insert a (Ioc a b)
Tactic: classical rw [cons_eq_insert, Ioc_insert_left h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a ≤ b
classical : Icc a b = insert a (Ioc a b)
⊢ Icc a b = cons a (Ioc a b) ⋯
have classical₁ : Icc a b = Icc a b
Tactic: classical rw [cons_eq_insert, Ioc_insert_left h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a < b
⊢ Ioc a b = cons b (Ioo a b) ⋯
have rw : Ioc a b = insert b (Ioo a b)
Tactic: rw [cons_eq_insert, Ioo_insert_right h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a < b
rw : Ioc a b = insert b (Ioo a b)
⊢ Ioc a b = cons b (Ioo a b) ⋯
have rw₁ : Ioc a b = Ioc a b
Tactic: rw [cons_eq_insert, Ioo_insert_right h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a < b
⊢ Ioc a b = cons b (Ioo a b) ⋯
have classical : Ioc a b = insert b (Ioo a b)
Tactic: classical rw [cons_eq_insert, Ioo_insert_right h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a < b
classical : Ioc a b = insert b (Ioo a b)
⊢ Ioc a b = cons b (Ioo a b) ⋯
have classical₁ : Ioc a b = Ioc a b
Tactic: classical rw [cons_eq_insert, Ioo_insert_right h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a < b
⊢ Ico a b = cons a (Ioo a b) ⋯
have rw : Ico a b = insert a (Ioo a b)
Tactic: rw [cons_eq_insert, Ioo_insert_left h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a < b
rw : Ico a b = insert a (Ioo a b)
⊢ Ico a b = cons a (Ioo a b) ⋯
have rw₁ : Ico a b = Ico a b
Tactic: rw [cons_eq_insert, Ioo_insert_left h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a < b
⊢ Ico a b = cons a (Ioo a b) ⋯
have classical : Ico a b = insert a (Ioo a b)
Tactic: classical rw [cons_eq_insert, Ioo_insert_left h]