awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a : α
rw : (Finset.Ico a a).val = 0
rw₁ : Eq.{u_1 + 1} (α := Multiset α) (Finset.val ∅) 0
⊢ Ico a a = 0
have rw₂ : Eq.{u_1 + 1} (α := Multiset α) 0 0
Tactic: rw [Ico, Finset.Ico_self, Finset.empty_val]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a : α
⊢ Ioc a a = 0
have rw : (Finset.Ioc a a).val = 0
Tactic: rw [Ioc, Finset.Ioc_self, Finset.empty_val]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a : α
rw : (Finset.Ioc a a).val = 0
⊢ Ioc a a = 0
have rw₁ : Eq.{u_1 + 1} (α := Multiset α) (Finset.val ∅) 0
Tactic: rw [Ioc, Finset.Ioc_self, Finset.empty_val]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a : α
rw : (Finset.Ioc a a).val = 0
rw₁ : Eq.{u_1 + 1} (α := Multiset α) (Finset.val ∅) 0
⊢ Ioc a a = 0
have rw₂ : Eq.{u_1 + 1} (α := Multiset α) 0 0
Tactic: rw [Ioc, Finset.Ioc_self, Finset.empty_val]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a : α
⊢ Ioo a a = 0
have rw : (Finset.Ioo a a).val = 0
Tactic: rw [Ioo, Finset.Ioo_self, Finset.empty_val]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a : α
rw : (Finset.Ioo a a).val = 0
⊢ Ioo a a = 0
have rw₁ : Eq.{u_1 + 1} (α := Multiset α) (Finset.val ∅) 0
Tactic: rw [Ioo, Finset.Ioo_self, Finset.empty_val]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a : α
rw : (Finset.Ioo a a).val = 0
rw₁ : Eq.{u_1 + 1} (α := Multiset α) (Finset.val ∅) 0
⊢ Ioo a a = 0
have rw₂ : Eq.{u_1 + 1} (α := Multiset α) 0 0
Tactic: rw [Ioo, Finset.Ioo_self, Finset.empty_val]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b c : α
inst_2 : DecidablePred fun (x : α) ↦ x < c
hca : c ≤ a
⊢ filter (fun (x : α) ↦ x < c) (Ico a b) = ∅
have rw : Eq.{u_1 + 1} (α := Multiset α) (Finset.val ∅) ∅
Tactic: rw [Ico, ← Finset.filter_val, Finset.Ico_filter_lt_of_le_left hca]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b c : α
inst_2 : DecidablePred fun (x : α) ↦ x < c
hbc : b ≤ c
⊢ filter (fun (x : α) ↦ x < c) (Ico a b) = Ico a b
have rw : filter (fun (x : α) ↦ x < c) (Finset.Ico a b).val = (Finset.Ico a b).val
Tactic: rw [Ico, ← Finset.filter_val, Finset.Ico_filter_lt_of_right_le hbc]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b c : α
inst_2 : DecidablePred fun (x : α) ↦ x < c
hbc : b ≤ c
rw : filter (fun (x : α) ↦ x < c) (Finset.Ico a b).val = (Finset.Ico a b).val
⊢ filter (fun (x : α) ↦ x < c) (Ico a b) = Ico a b
have rw₁ : {x ∈ Finset.Ico a b | x < c}.val = (Finset.Ico a b).val
Tactic: rw [Ico, ← Finset.filter_val, Finset.Ico_filter_lt_of_right_le hbc]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b c : α
inst_2 : DecidablePred fun (x : α) ↦ x < c
hbc : b ≤ c
rw : filter (fun (x : α) ↦ x < c) (Finset.Ico a b).val = (Finset.Ico a b).val
rw₁ : {x ∈ Finset.Ico a b | x < c}.val = (Finset.Ico a b).val
⊢ filter (fun (x : α) ↦ x < c) (Ico a b) = Ico a b
have rw₂ : (Finset.Ico a b).val = (Finset.Ico a b).val
Tactic: rw [Ico, ← Finset.filter_val, Finset.Ico_filter_lt_of_right_le hbc]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b c : α
inst_2 : DecidablePred fun (x : α) ↦ x < c
hcb : c ≤ b
⊢ filter (fun (x : α) ↦ x < c) (Ico a b) = Ico a c
have rw : (Finset.Ico a c).val = Ico a c
Tactic: rw [Ico, ← Finset.filter_val, Finset.Ico_filter_lt_of_le_right hcb]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b c : α
inst_2 : DecidablePred fun (x : α) ↦ c ≤ x
hca : c ≤ a
⊢ filter (fun (x : α) ↦ c ≤ x) (Ico a b) = Ico a b
have rw : filter (fun (x : α) ↦ c ≤ x) (Finset.Ico a b).val = (Finset.Ico a b).val
Tactic: rw [Ico, ← Finset.filter_val, Finset.Ico_filter_le_of_le_left hca]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b c : α
inst_2 : DecidablePred fun (x : α) ↦ c ≤ x
hca : c ≤ a
rw : filter (fun (x : α) ↦ c ≤ x) (Finset.Ico a b).val = (Finset.Ico a b).val
⊢ filter (fun (x : α) ↦ c ≤ x) (Ico a b) = Ico a b
have rw₁ : {x ∈ Finset.Ico a b | c ≤ x}.val = (Finset.Ico a b).val
Tactic: rw [Ico, ← Finset.filter_val, Finset.Ico_filter_le_of_le_left hca]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b c : α
inst_2 : DecidablePred fun (x : α) ↦ c ≤ x
hca : c ≤ a
rw : filter (fun (x : α) ↦ c ≤ x) (Finset.Ico a b).val = (Finset.Ico a b).val
rw₁ : {x ∈ Finset.Ico a b | c ≤ x}.val = (Finset.Ico a b).val
⊢ filter (fun (x : α) ↦ c ≤ x) (Ico a b) = Ico a b
have rw₂ : (Finset.Ico a b).val = (Finset.Ico a b).val
Tactic: rw [Ico, ← Finset.filter_val, Finset.Ico_filter_le_of_le_left hca]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidablePred fun (x : α) ↦ b ≤ x
⊢ filter (fun (x : α) ↦ b ≤ x) (Ico a b) = ∅
have rw : Eq.{u_1 + 1} (α := Multiset α) (Finset.val ∅) ∅
Tactic: rw [Ico, ← Finset.filter_val, Finset.Ico_filter_le_of_right_le]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b c : α
inst_2 : DecidablePred fun (x : α) ↦ c ≤ x
hac : a ≤ c
⊢ filter (fun (x : α) ↦ c ≤ x) (Ico a b) = Ico c b
have rw : (Finset.Ico c b).val = Ico c b
Tactic: rw [Ico, ← Finset.filter_val, Finset.Ico_filter_le_of_left_le hac]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a : α
⊢ Icc a a = {a}
have rw : (Finset.Icc a a).val = {a}
Tactic: rw [Icc, Finset.Icc_self, Finset.singleton_val]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a : α
rw : (Finset.Icc a a).val = {a}
⊢ Icc a a = {a}
have rw₁ : Eq (α := Multiset α) (Finset.val {a}) {a}
Tactic: rw [Icc, Finset.Icc_self, Finset.singleton_val]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a : α
rw : (Finset.Icc a a).val = {a}
rw₁ : Eq (α := Multiset α) (Finset.val {a}) {a}
⊢ Icc a a = {a}
have rw₂ : Eq (α := Multiset α) {a} {a}
Tactic: rw [Icc, Finset.Icc_self, Finset.singleton_val]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ b ::ₘ Ico a b = Icc a b
have rw : (Finset.Icc a b).val = Icc a b
Tactic: rw [Ico, ← Finset.insert_val_of_notMem right_notMem_Ico, Finset.Ico_insert_right h]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ b ::ₘ Ico a b = Icc a b
have rw : b ::ₘ (Finset.Ico a b).val = Icc a b
Tactic: classical
    rw [Ico, ← Finset.insert_val_of_notMem right_notMem_Ico, Finset.Ico_insert_right h]
    rfl
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a ≤ b
rw : b ::ₘ (Finset.Ico a b).val = Icc a b
⊢ b ::ₘ Ico a b = Icc a b
have rw₁ : (insert b (Finset.Ico a b)).val = Icc a b
Tactic: classical
    rw [Ico, ← Finset.insert_val_of_notMem right_notMem_Ico, Finset.Ico_insert_right h]
    rfl
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a ≤ b
rw : b ::ₘ (Finset.Ico a b).val = Icc a b
rw₁ : (insert b (Finset.Ico a b)).val = Icc a b
⊢ b ::ₘ Ico a b = Icc a b
have rw₂ : (Finset.Icc a b).val = Icc a b
Tactic: classical
    rw [Ico, ← Finset.insert_val_of_notMem right_notMem_Ico, Finset.Ico_insert_right h]
    rfl
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a < b
⊢ a ::ₘ Ioo a b = Ico a b
have rw : (Finset.Ico a b).val = Ico a b
Tactic: rw [Ioo, ← Finset.insert_val_of_notMem left_notMem_Ioo, Finset.Ioo_insert_left h]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a < b
⊢ a ::ₘ Ioo a b = Ico a b
have rw : a ::ₘ (Finset.Ioo a b).val = Ico a b
Tactic: classical
    rw [Ioo, ← Finset.insert_val_of_notMem left_notMem_Ioo, Finset.Ioo_insert_left h]
    rfl
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a < b
rw : a ::ₘ (Finset.Ioo a b).val = Ico a b
⊢ a ::ₘ Ioo a b = Ico a b
have rw₁ : (insert a (Finset.Ioo a b)).val = Ico a b
Tactic: classical
    rw [Ioo, ← Finset.insert_val_of_notMem left_notMem_Ioo, Finset.Ioo_insert_left h]
    rfl
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : a < b
rw : a ::ₘ (Finset.Ioo a b).val = Ico a b
rw₁ : (insert a (Finset.Ioo a b)).val = Ico a b
⊢ a ::ₘ Ioo a b = Ico a b
have rw₂ : (Finset.Ico a b).val = Ico a b
Tactic: classical
    rw [Ioo, ← Finset.insert_val_of_notMem left_notMem_Ioo, Finset.Ioo_insert_left h]
    rfl
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (hypothesis)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b c d : α
h : b ≤ c
a_1 : α
hab : a_1 ∈ Ico a b
hbc : a_1 ∈ Ico c d
⊢ False
have hab₁ : a ≤ a_1 ∧ a_1 < b
Tactic: rw [mem_Ico] at hab hbc
Cleared hypotheses: hab, hbc
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (hypothesis)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b c d : α
h : b ≤ c
a_1 : α
hab : a_1 ∈ Ico a b
hbc : a_1 ∈ Ico c d
hab₁ : a ≤ a_1 ∧ a_1 < b
⊢ False
have hbc₁ : c ≤ a_1 ∧ a_1 < d
Tactic: rw [mem_Ico] at hab hbc
Cleared hypotheses: hab, hbc
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
inst_2 : DecidablePred fun (x : α) ↦ x ≤ a
hab : a < b
⊢ filter (fun (x : α) ↦ x ≤ a) (Ico a b) = {a}
have rw : Eq (α := Multiset α) (Finset.val {a}) {a}
Tactic: rw [Ico, ← Finset.filter_val, Finset.Ico_filter_le_left hab]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
⊢ Ico a b + Ico b c = Ico a c
have rw : Ico a b ∪ Ico b c = Ico a c
Tactic: rw [add_eq_union_iff_disjoint.2 (Ico_disjoint_Ico le_rfl), Ico, Ico, Ico, ← Finset.union_val,
    Finset.Ico_union_Ico_eq_Ico hab hbc]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
rw : Ico a b ∪ Ico b c = Ico a c
⊢ Ico a b + Ico b c = Ico a c
have rw₁ : (Finset.Ico a b).val ∪ Ico b c = Ico a c
Tactic: rw [add_eq_union_iff_disjoint.2 (Ico_disjoint_Ico le_rfl), Ico, Ico, Ico, ← Finset.union_val,
    Finset.Ico_union_Ico_eq_Ico hab hbc]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
rw : Ico a b ∪ Ico b c = Ico a c
rw₁ : (Finset.Ico a b).val ∪ Ico b c = Ico a c
⊢ Ico a b + Ico b c = Ico a c
have rw₂ : (Finset.Ico a b).val ∪ (Finset.Ico b c).val = Ico a c
Tactic: rw [add_eq_union_iff_disjoint.2 (Ico_disjoint_Ico le_rfl), Ico, Ico, Ico, ← Finset.union_val,
    Finset.Ico_union_Ico_eq_Ico hab hbc]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
rw : Ico a b ∪ Ico b c = Ico a c
rw₁ : (Finset.Ico a b).val ∪ Ico b c = Ico a c
rw₂ : (Finset.Ico a b).val ∪ (Finset.Ico b c).val = Ico a c
⊢ Ico a b + Ico b c = Ico a c
have rw₃ : (Finset.Ico a b).val ∪ (Finset.Ico b c).val = (Finset.Ico a c).val
Tactic: rw [add_eq_union_iff_disjoint.2 (Ico_disjoint_Ico le_rfl), Ico, Ico, Ico, ← Finset.union_val,
    Finset.Ico_union_Ico_eq_Ico hab hbc]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
rw : Ico a b ∪ Ico b c = Ico a c
rw₁ : (Finset.Ico a b).val ∪ Ico b c = Ico a c
rw₂ : (Finset.Ico a b).val ∪ (Finset.Ico b c).val = Ico a c
rw₃ : (Finset.Ico a b).val ∪ (Finset.Ico b c).val = (Finset.Ico a c).val
⊢ Ico a b + Ico b c = Ico a c
have rw₄ : (Finset.Ico a b ∪ Finset.Ico b c).val = (Finset.Ico a c).val
Tactic: rw [add_eq_union_iff_disjoint.2 (Ico_disjoint_Ico le_rfl), Ico, Ico, Ico, ← Finset.union_val,
    Finset.Ico_union_Ico_eq_Ico hab hbc]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
rw : Ico a b ∪ Ico b c = Ico a c
rw₁ : (Finset.Ico a b).val ∪ Ico b c = Ico a c
rw₂ : (Finset.Ico a b).val ∪ (Finset.Ico b c).val = Ico a c
rw₃ : (Finset.Ico a b).val ∪ (Finset.Ico b c).val = (Finset.Ico a c).val
rw₄ : (Finset.Ico a b ∪ Finset.Ico b c).val = (Finset.Ico a c).val
⊢ Ico a b + Ico b c = Ico a c
have rw₅ : (Finset.Ico a c).val = (Finset.Ico a c).val
Tactic: rw [add_eq_union_iff_disjoint.2 (Ico_disjoint_Ico le_rfl), Ico, Ico, Ico, ← Finset.union_val,
    Finset.Ico_union_Ico_eq_Ico hab hbc]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c d : α
⊢ Ico a b ∩ Ico c d = Ico (max a c) (min b d)
have rw : (Finset.Ico a b).val ∩ Ico c d = Ico (max a c) (min b d)
Tactic: rw [Ico, Ico, Ico, ← Finset.inter_val, Finset.Ico_inter_Ico]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c d : α
rw : (Finset.Ico a b).val ∩ Ico c d = Ico (max a c) (min b d)
⊢ Ico a b ∩ Ico c d = Ico (max a c) (min b d)
have rw₁ : (Finset.Ico a b).val ∩ (Finset.Ico c d).val = Ico (max a c) (min b d)
Tactic: rw [Ico, Ico, Ico, ← Finset.inter_val, Finset.Ico_inter_Ico]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c d : α
rw : (Finset.Ico a b).val ∩ Ico c d = Ico (max a c) (min b d)
rw₁ : (Finset.Ico a b).val ∩ (Finset.Ico c d).val = Ico (max a c) (min b d)
⊢ Ico a b ∩ Ico c d = Ico (max a c) (min b d)
have rw₂ : (Finset.Ico a b).val ∩ (Finset.Ico c d).val = (Finset.Ico (max a c) (min b d)).val
Tactic: rw [Ico, Ico, Ico, ← Finset.inter_val, Finset.Ico_inter_Ico]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c d : α
rw : (Finset.Ico a b).val ∩ Ico c d = Ico (max a c) (min b d)
rw₁ : (Finset.Ico a b).val ∩ (Finset.Ico c d).val = Ico (max a c) (min b d)
rw₂ : (Finset.Ico a b).val ∩ (Finset.Ico c d).val = (Finset.Ico (max a c) (min b d)).val
⊢ Ico a b ∩ Ico c d = Ico (max a c) (min b d)
have rw₃ : (Finset.Ico a b ∩ Finset.Ico c d).val = (Finset.Ico (max a c) (min b d)).val
Tactic: rw [Ico, Ico, Ico, ← Finset.inter_val, Finset.Ico_inter_Ico]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c d : α
rw : (Finset.Ico a b).val ∩ Ico c d = Ico (max a c) (min b d)
rw₁ : (Finset.Ico a b).val ∩ (Finset.Ico c d).val = Ico (max a c) (min b d)
rw₂ : (Finset.Ico a b).val ∩ (Finset.Ico c d).val = (Finset.Ico (max a c) (min b d)).val
rw₃ : (Finset.Ico a b ∩ Finset.Ico c d).val = (Finset.Ico (max a c) (min b d)).val
⊢ Ico a b ∩ Ico c d = Ico (max a c) (min b d)
have rw₄ : (Finset.Ico (max a c) (min b d)).val = (Finset.Ico (max a c) (min b d)).val
Tactic: rw [Ico, Ico, Ico, ← Finset.inter_val, Finset.Ico_inter_Ico]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
⊢ filter (fun (x : α) ↦ x < c) (Ico a b) = Ico a (min b c)
have rw : filter (fun (x : α) ↦ x < c) (Finset.Ico a b).val = Ico a (min b c)
Tactic: rw [Ico, Ico, ← Finset.filter_val, Finset.Ico_filter_lt]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
rw : filter (fun (x : α) ↦ x < c) (Finset.Ico a b).val = Ico a (min b c)
⊢ filter (fun (x : α) ↦ x < c) (Ico a b) = Ico a (min b c)
have rw₁ : filter (fun (x : α) ↦ x < c) (Finset.Ico a b).val = (Finset.Ico a (min b c)).val
Tactic: rw [Ico, Ico, ← Finset.filter_val, Finset.Ico_filter_lt]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
rw : filter (fun (x : α) ↦ x < c) (Finset.Ico a b).val = Ico a (min b c)
rw₁ : filter (fun (x : α) ↦ x < c) (Finset.Ico a b).val = (Finset.Ico a (min b c)).val
⊢ filter (fun (x : α) ↦ x < c) (Ico a b) = Ico a (min b c)
have rw₂ : {x ∈ Finset.Ico a b | x < c}.val = (Finset.Ico a (min b c)).val
Tactic: rw [Ico, Ico, ← Finset.filter_val, Finset.Ico_filter_lt]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
rw : filter (fun (x : α) ↦ x < c) (Finset.Ico a b).val = Ico a (min b c)
rw₁ : filter (fun (x : α) ↦ x < c) (Finset.Ico a b).val = (Finset.Ico a (min b c)).val
rw₂ : {x ∈ Finset.Ico a b | x < c}.val = (Finset.Ico a (min b c)).val
⊢ filter (fun (x : α) ↦ x < c) (Ico a 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, ← Finset.filter_val, Finset.Ico_filter_lt]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
⊢ filter (fun (x : α) ↦ c ≤ x) (Ico a b) = Ico (max a c) b
have rw : filter (fun (x : α) ↦ c ≤ x) (Finset.Ico a b).val = Ico (max a c) b
Tactic: rw [Ico, Ico, ← Finset.filter_val, Finset.Ico_filter_le]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
rw : filter (fun (x : α) ↦ c ≤ x) (Finset.Ico a b).val = Ico (max a c) b
⊢ filter (fun (x : α) ↦ c ≤ x) (Ico a b) = Ico (max a c) b
have rw₁ : filter (fun (x : α) ↦ c ≤ x) (Finset.Ico a b).val = (Finset.Ico (max a c) b).val
Tactic: rw [Ico, Ico, ← Finset.filter_val, Finset.Ico_filter_le]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
rw : filter (fun (x : α) ↦ c ≤ x) (Finset.Ico a b).val = Ico (max a c) b
rw₁ : filter (fun (x : α) ↦ c ≤ x) (Finset.Ico a b).val = (Finset.Ico (max a c) b).val
⊢ filter (fun (x : α) ↦ c ≤ x) (Ico a b) = Ico (max a c) b
have rw₂ : {x ∈ Finset.Ico a b | c ≤ x}.val = (Finset.Ico (max a c) b).val
Tactic: rw [Ico, Ico, ← Finset.filter_val, Finset.Ico_filter_le]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
rw : filter (fun (x : α) ↦ c ≤ x) (Finset.Ico a b).val = Ico (max a c) b
rw₁ : filter (fun (x : α) ↦ c ≤ x) (Finset.Ico a b).val = (Finset.Ico (max a c) b).val
rw₂ : {x ∈ Finset.Ico a b | c ≤ x}.val = (Finset.Ico (max a c) b).val
⊢ filter (fun (x : α) ↦ c ≤ x) (Ico a b) = Ico (max a c) b
have rw₃ : (Finset.Ico (max a c) b).val = (Finset.Ico (max a c) b).val
Tactic: rw [Ico, Ico, ← Finset.filter_val, Finset.Ico_filter_le]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
⊢ Ico a b - Ico a c = Ico (max a c) b
have rw : (Finset.Ico a b).val - Ico a c = Ico (max a c) b
Tactic: rw [Ico, Ico, Ico, ← Finset.sdiff_val, Finset.Ico_diff_Ico_left]
-- 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 a c = Ico (max a c) b
⊢ Ico a b - Ico a c = Ico (max a c) b
have rw₁ : (Finset.Ico a b).val - (Finset.Ico a c).val = Ico (max a c) b
Tactic: rw [Ico, Ico, Ico, ← Finset.sdiff_val, Finset.Ico_diff_Ico_left]
-- 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 a c = Ico (max a c) b
rw₁ : (Finset.Ico a b).val - (Finset.Ico a c).val = Ico (max a c) b
⊢ Ico a b - Ico a c = Ico (max a c) b
have rw₂ : (Finset.Ico a b).val - (Finset.Ico a c).val = (Finset.Ico (max a c) b).val
Tactic: rw [Ico, Ico, Ico, ← Finset.sdiff_val, Finset.Ico_diff_Ico_left]
-- 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 a c = Ico (max a c) b
rw₁ : (Finset.Ico a b).val - (Finset.Ico a c).val = Ico (max a c) b
rw₂ : (Finset.Ico a b).val - (Finset.Ico a c).val = (Finset.Ico (max a c) b).val
⊢ Ico a b - Ico a c = Ico (max a c) b
have rw₃ : (Finset.Ico a b \ Finset.Ico a c).val = (Finset.Ico (max a c) b).val
Tactic: rw [Ico, Ico, Ico, ← Finset.sdiff_val, Finset.Ico_diff_Ico_left]
-- 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 a c = Ico (max a c) b
rw₁ : (Finset.Ico a b).val - (Finset.Ico a c).val = Ico (max a c) b
rw₂ : (Finset.Ico a b).val - (Finset.Ico a c).val = (Finset.Ico (max a c) b).val
rw₃ : (Finset.Ico a b \ Finset.Ico a c).val = (Finset.Ico (max a c) b).val
⊢ Ico a b - Ico a c = Ico (max a c) b
have rw₄ : (Finset.Ico (max a c) b).val = (Finset.Ico (max a c) b).val
Tactic: rw [Ico, Ico, Ico, ← Finset.sdiff_val, Finset.Ico_diff_Ico_left]
-- Lean 4 proof step from Mathlib.Order.Interval.Multiset (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
⊢ Ico a b - Ico c b = Ico a (min b c)
have rw : (Finset.Ico a b).val - Ico c b = Ico a (min b c)
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)
⊢ Ico a b - Ico c b = Ico a (min b c)
have rw₁ : (Finset.Ico a b).val - (Finset.Ico c b).val = Ico a (min b c)
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)
⊢ Ico a b - Ico c b = Ico a (min b c)
have rw₂ : (Finset.Ico a b).val - (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]