awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : Ico a b = insert a (Ioo a b)
⊢ Ico a b = cons a (Ioo a b) ⋯
have classical₁ : Ico a b = Ico a b
Tactic: classical 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 : α
⊢ #(Ico a b) = #(Icc a b) - 1
have pos : ∀ (h : a ≤ b), #(Ico a b) = #(Icc a b) - 1
Tactic: by_cases h : a ≤ b
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
pos : ∀ (h : a ≤ b), #(Ico a b) = #(Icc a b) - 1
⊢ #(Ico a b) = #(Icc a b) - 1
have neg : ∀ (h : ¬a ≤ b), #(Ico a b) = #(Icc a b) - 1
Tactic: by_cases h : a ≤ b
-- 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) = #(Icc a b) - 1
have pos : #(Ico a b) = #(Ico a b) + 1 - 1
Tactic: rw [Icc_eq_cons_Ico h, card_cons]
-- 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) = #(Icc a b) - 1
have neg : card.{u_2} (α := α) ∅ = #(Icc a b) - 1
Tactic: rw [Ico_eq_empty fun h' => h h'.le, Icc_eq_empty h, card_empty, Nat.zero_sub]
-- 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
neg : card.{u_2} (α := α) ∅ = #(Icc a b) - 1
⊢ #(Ico a b) = #(Icc a b) - 1
have neg₁ : card.{u_2} (α := α) ∅ = card.{u_2} (α := α) ∅ - 1
Tactic: rw [Ico_eq_empty fun h' => h h'.le, Icc_eq_empty h, card_empty, Nat.zero_sub]
-- 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
neg : card.{u_2} (α := α) ∅ = #(Icc a b) - 1
neg₁ : card.{u_2} (α := α) ∅ = card.{u_2} (α := α) ∅ - 1
⊢ #(Ico a b) = #(Icc a b) - 1
have neg₂ : 0 = HSub.hSub (α := ℕ) 0 1
Tactic: rw [Ico_eq_empty fun h' => h h'.le, Icc_eq_empty h, card_empty, Nat.zero_sub]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ #(Ico a b) = #(Icc a b) - 1
have pos : ∀ (h : a ≤ b), #(Ico a b) = #(Icc a b) - 1
Tactic: classical
    by_cases h : a ≤ b
    · rw [Icc_eq_cons_Ico h, card_cons]
      exact (Nat.add_sub_cancel _ _).symm
    · rw [Ico_eq_empty fun h' => h h'.le, Icc_eq_empty h, card_empty, Nat.zero_sub]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
pos : ∀ (h : a ≤ b), #(Ico a b) = #(Icc a b) - 1
⊢ #(Ico a b) = #(Icc a b) - 1
have neg : ∀ (h : ¬a ≤ b), #(Ico a b) = #(Icc a b) - 1
Tactic: classical
    by_cases h : a ≤ b
    · rw [Icc_eq_cons_Ico h, card_cons]
      exact (Nat.add_sub_cancel _ _).symm
    · rw [Ico_eq_empty fun h' => h h'.le, Icc_eq_empty h, card_empty, Nat.zero_sub]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ #(Ioo a b) = #(Ico a b) - 1
have pos : ∀ (h : a < b), #(Ioo a b) = #(Ico a b) - 1
Tactic: by_cases h : a < b
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
pos : ∀ (h : a < b), #(Ioo a b) = #(Ico a b) - 1
⊢ #(Ioo a b) = #(Ico a b) - 1
have neg : ∀ (h : ¬a < b), #(Ioo a b) = #(Ico a b) - 1
Tactic: by_cases h : a < b
-- 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
⊢ #(Ioo a b) = #(Ico a b) - 1
have pos : #(Ioo a b) = #(Ioo a b) + 1 - 1
Tactic: rw [Ico_eq_cons_Ioo h, card_cons]
-- 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
⊢ #(Ioo a b) = #(Ico a b) - 1
have neg : card.{u_2} (α := α) ∅ = #(Ico a b) - 1
Tactic: rw [Ioo_eq_empty h, Ico_eq_empty h, card_empty, Nat.zero_sub]
-- 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
neg : card.{u_2} (α := α) ∅ = #(Ico a b) - 1
⊢ #(Ioo a b) = #(Ico a b) - 1
have neg₁ : card.{u_2} (α := α) ∅ = card.{u_2} (α := α) ∅ - 1
Tactic: rw [Ioo_eq_empty h, Ico_eq_empty h, card_empty, Nat.zero_sub]
-- 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
neg : card.{u_2} (α := α) ∅ = #(Ico a b) - 1
neg₁ : card.{u_2} (α := α) ∅ = card.{u_2} (α := α) ∅ - 1
⊢ #(Ioo a b) = #(Ico a b) - 1
have neg₂ : 0 = HSub.hSub (α := ℕ) 0 1
Tactic: rw [Ioo_eq_empty h, Ico_eq_empty h, card_empty, Nat.zero_sub]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ #(Ioo a b) = #(Ico a b) - 1
have pos : ∀ (h : a < b), #(Ioo a b) = #(Ico a b) - 1
Tactic: classical
    by_cases h : a < b
    · rw [Ico_eq_cons_Ioo h, card_cons]
      exact (Nat.add_sub_cancel _ _).symm
    · rw [Ioo_eq_empty h, Ico_eq_empty h, card_empty, Nat.zero_sub]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
pos : ∀ (h : a < b), #(Ioo a b) = #(Ico a b) - 1
⊢ #(Ioo a b) = #(Ico a b) - 1
have neg : ∀ (h : ¬a < b), #(Ioo a b) = #(Ico a b) - 1
Tactic: classical
    by_cases h : a < b
    · rw [Ico_eq_cons_Ioo h, card_cons]
      exact (Nat.add_sub_cancel _ _).symm
    · rw [Ioo_eq_empty h, Ico_eq_empty h, card_empty, Nat.zero_sub]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ #(Ioo a b) = #(Icc a b) - 2
have rw : #(Icc a b) - 1 - 1 = #(Icc a b) - 2
Tactic: rw [card_Ioo_eq_card_Ico_sub_one, card_Ico_eq_card_Icc_sub_one]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderTop α
inst_2 : DecidableEq α
a : α
⊢ (Ici a).erase a = Ioi a
have h : ∀ (a_1 : α), a_1 ∈ (Ici a).erase a ↔ a_1 ∈ Ioi a
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderTop α
inst_2 : DecidableEq α
a a_1 : α
⊢ a_1 ∈ (Ici a).erase a ↔ a_1 ∈ Ioi a
have h : a_1 ≠ a ∧ a_1 ∈ Ici a ↔ a_1 ∈ Ioi a
Tactic: simp_rw [Finset.mem_erase, mem_Ici, mem_Ioi, lt_iff_le_and_ne, and_comm, ne_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderTop α
inst_2 : DecidableEq α
a a_1 : α
h : a_1 ≠ a ∧ a_1 ∈ Ici a ↔ a_1 ∈ Ioi a
⊢ a_1 ∈ (Ici a).erase a ↔ a_1 ∈ Ioi a
have h₁ : a_1 ≠ a ∧ a ≤ a_1 ↔ a_1 ∈ Ioi a
Tactic: simp_rw [Finset.mem_erase, mem_Ici, mem_Ioi, lt_iff_le_and_ne, and_comm, ne_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderTop α
inst_2 : DecidableEq α
a a_1 : α
h : a_1 ≠ a ∧ a_1 ∈ Ici a ↔ a_1 ∈ Ioi a
h₁ : a_1 ≠ a ∧ a ≤ a_1 ↔ a_1 ∈ Ioi a
⊢ a_1 ∈ (Ici a).erase a ↔ a_1 ∈ Ioi a
have h₂ : a_1 ≠ a ∧ a ≤ a_1 ↔ a < a_1
Tactic: simp_rw [Finset.mem_erase, mem_Ici, mem_Ioi, lt_iff_le_and_ne, and_comm, ne_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderTop α
inst_2 : DecidableEq α
a a_1 : α
h : a_1 ≠ a ∧ a_1 ∈ Ici a ↔ a_1 ∈ Ioi a
h₁ : a_1 ≠ a ∧ a ≤ a_1 ↔ a_1 ∈ Ioi a
h₂ : a_1 ≠ a ∧ a ≤ a_1 ↔ a < a_1
⊢ a_1 ∈ (Ici a).erase a ↔ a_1 ∈ Ioi a
have h₃ : a_1 ≠ a ∧ a ≤ a_1 ↔ a ≤ a_1 ∧ a ≠ a_1
Tactic: simp_rw [Finset.mem_erase, mem_Ici, mem_Ioi, lt_iff_le_and_ne, and_comm, ne_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderTop α
inst_2 : DecidableEq α
a a_1 : α
h : a_1 ≠ a ∧ a_1 ∈ Ici a ↔ a_1 ∈ Ioi a
h₁ : a_1 ≠ a ∧ a ≤ a_1 ↔ a_1 ∈ Ioi a
h₂ : a_1 ≠ a ∧ a ≤ a_1 ↔ a < a_1
h₃ : a_1 ≠ a ∧ a ≤ a_1 ↔ a ≤ a_1 ∧ a ≠ a_1
⊢ a_1 ∈ (Ici a).erase a ↔ a_1 ∈ Ioi a
have h₄ : a_1 ≠ a ∧ a ≤ a_1 ↔ a ≠ a_1 ∧ a ≤ a_1
Tactic: simp_rw [Finset.mem_erase, mem_Ici, mem_Ioi, lt_iff_le_and_ne, and_comm, ne_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderTop α
inst_2 : DecidableEq α
a : α
⊢ insert a (Ioi a) = Ici a
have h : ∀ (a_1 : α), a_1 ∈ insert a (Ioi a) ↔ a_1 ∈ Ici a
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderTop α
inst_2 : DecidableEq α
a a_1 : α
⊢ a_1 ∈ insert a (Ioi a) ↔ a_1 ∈ Ici a
have h : a_1 = a ∨ a_1 ∈ Ioi a ↔ a_1 ∈ Ici a
Tactic: simp_rw [Finset.mem_insert, mem_Ici, mem_Ioi, le_iff_lt_or_eq, or_comm, eq_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderTop α
inst_2 : DecidableEq α
a a_1 : α
h : a_1 = a ∨ a_1 ∈ Ioi a ↔ a_1 ∈ Ici a
⊢ a_1 ∈ insert a (Ioi a) ↔ a_1 ∈ Ici a
have h₁ : a_1 = a ∨ a_1 ∈ Ioi a ↔ a ≤ a_1
Tactic: simp_rw [Finset.mem_insert, mem_Ici, mem_Ioi, le_iff_lt_or_eq, or_comm, eq_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderTop α
inst_2 : DecidableEq α
a a_1 : α
h : a_1 = a ∨ a_1 ∈ Ioi a ↔ a_1 ∈ Ici a
h₁ : a_1 = a ∨ a_1 ∈ Ioi a ↔ a ≤ a_1
⊢ a_1 ∈ insert a (Ioi a) ↔ a_1 ∈ Ici a
have h₂ : a_1 = a ∨ a < a_1 ↔ a ≤ a_1
Tactic: simp_rw [Finset.mem_insert, mem_Ici, mem_Ioi, le_iff_lt_or_eq, or_comm, eq_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderTop α
inst_2 : DecidableEq α
a a_1 : α
h : a_1 = a ∨ a_1 ∈ Ioi a ↔ a_1 ∈ Ici a
h₁ : a_1 = a ∨ a_1 ∈ Ioi a ↔ a ≤ a_1
h₂ : a_1 = a ∨ a < a_1 ↔ a ≤ a_1
⊢ a_1 ∈ insert a (Ioi a) ↔ a_1 ∈ Ici a
have h₃ : a_1 = a ∨ a < a_1 ↔ a < a_1 ∨ a = a_1
Tactic: simp_rw [Finset.mem_insert, mem_Ici, mem_Ioi, le_iff_lt_or_eq, or_comm, eq_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderTop α
inst_2 : DecidableEq α
a a_1 : α
h : a_1 = a ∨ a_1 ∈ Ioi a ↔ a_1 ∈ Ici a
h₁ : a_1 = a ∨ a_1 ∈ Ioi a ↔ a ≤ a_1
h₂ : a_1 = a ∨ a < a_1 ↔ a ≤ a_1
h₃ : a_1 = a ∨ a < a_1 ↔ a < a_1 ∨ a = a_1
⊢ a_1 ∈ insert a (Ioi a) ↔ a_1 ∈ Ici a
have h₄ : a_1 = a ∨ a < a_1 ↔ a = a_1 ∨ a < a_1
Tactic: simp_rw [Finset.mem_insert, mem_Ici, mem_Ioi, le_iff_lt_or_eq, or_comm, eq_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderTop α
a : α
⊢ Ici a = cons a (Ioi a) ⋯
have rw : Ici a = insert a (Ioi a)
Tactic: rw [cons_eq_insert, Ioi_insert]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderTop α
a : α
rw : Ici a = insert a (Ioi a)
⊢ Ici a = cons a (Ioi a) ⋯
have rw₁ : Ici a = Ici a
Tactic: rw [cons_eq_insert, Ioi_insert]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderTop α
a : α
⊢ Ici a = cons a (Ioi a) ⋯
have classical : Ici a = insert a (Ioi a)
Tactic: classical rw [cons_eq_insert, Ioi_insert]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderTop α
a : α
classical : Ici a = insert a (Ioi a)
⊢ Ici a = cons a (Ioi a) ⋯
have classical₁ : Ici a = Ici a
Tactic: classical rw [cons_eq_insert, Ioi_insert]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderTop α
a : α
⊢ #(Ioi a) = #(Ici a) - 1
have rw : #(Ioi a) = #(cons a (Ioi a) sorry) - 1
Tactic: rw [Ici_eq_cons_Ioi, card_cons, Nat.add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderTop α
a : α
rw : #(Ioi a) = #(cons a (Ioi a) ⋯) - 1
⊢ #(Ioi a) = #(Ici a) - 1
have rw₁ : #(Ioi a) = #(Ioi a) + 1 - 1
Tactic: rw [Ici_eq_cons_Ioi, card_cons, Nat.add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderTop α
a : α
rw : #(Ioi a) = #(cons a (Ioi a) ⋯) - 1
rw₁ : #(Ioi a) = #(Ioi a) + 1 - 1
⊢ #(Ioi a) = #(Ici a) - 1
have rw₂ : #(Ioi a) = #(Ioi a)
Tactic: rw [Ici_eq_cons_Ioi, card_cons, Nat.add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderBot α
inst_2 : DecidableEq α
b : α
⊢ (Iic b).erase b = Iio b
have h : ∀ (a : α), a ∈ (Iic b).erase b ↔ a ∈ Iio b
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderBot α
inst_2 : DecidableEq α
b a : α
⊢ a ∈ (Iic b).erase b ↔ a ∈ Iio b
have h : a ≠ b ∧ a ∈ Iic b ↔ a ∈ Iio b
Tactic: simp_rw [Finset.mem_erase, mem_Iic, mem_Iio, lt_iff_le_and_ne, and_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderBot α
inst_2 : DecidableEq α
b a : α
h : a ≠ b ∧ a ∈ Iic b ↔ a ∈ Iio b
⊢ a ∈ (Iic b).erase b ↔ a ∈ Iio b
have h₁ : a ≠ b ∧ a ≤ b ↔ a ∈ Iio b
Tactic: simp_rw [Finset.mem_erase, mem_Iic, mem_Iio, lt_iff_le_and_ne, and_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderBot α
inst_2 : DecidableEq α
b a : α
h : a ≠ b ∧ a ∈ Iic b ↔ a ∈ Iio b
h₁ : a ≠ b ∧ a ≤ b ↔ a ∈ Iio b
⊢ a ∈ (Iic b).erase b ↔ a ∈ Iio b
have h₂ : a ≠ b ∧ a ≤ b ↔ a < b
Tactic: simp_rw [Finset.mem_erase, mem_Iic, mem_Iio, lt_iff_le_and_ne, and_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderBot α
inst_2 : DecidableEq α
b a : α
h : a ≠ b ∧ a ∈ Iic b ↔ a ∈ Iio b
h₁ : a ≠ b ∧ a ≤ b ↔ a ∈ Iio b
h₂ : a ≠ b ∧ a ≤ b ↔ a < b
⊢ a ∈ (Iic b).erase b ↔ a ∈ Iio b
have h₃ : a ≠ b ∧ a ≤ b ↔ a ≤ b ∧ a ≠ b
Tactic: simp_rw [Finset.mem_erase, mem_Iic, mem_Iio, lt_iff_le_and_ne, and_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderBot α
inst_2 : DecidableEq α
b : α
⊢ insert b (Iio b) = Iic b
have h : ∀ (a : α), a ∈ insert b (Iio b) ↔ a ∈ Iic b
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderBot α
inst_2 : DecidableEq α
b a : α
⊢ a ∈ insert b (Iio b) ↔ a ∈ Iic b
have h : a = b ∨ a ∈ Iio b ↔ a ∈ Iic b
Tactic: simp_rw [Finset.mem_insert, mem_Iic, mem_Iio, le_iff_lt_or_eq, or_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderBot α
inst_2 : DecidableEq α
b a : α
h : a = b ∨ a ∈ Iio b ↔ a ∈ Iic b
⊢ a ∈ insert b (Iio b) ↔ a ∈ Iic b
have h₁ : a = b ∨ a ∈ Iio b ↔ a ≤ b
Tactic: simp_rw [Finset.mem_insert, mem_Iic, mem_Iio, le_iff_lt_or_eq, or_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderBot α
inst_2 : DecidableEq α
b a : α
h : a = b ∨ a ∈ Iio b ↔ a ∈ Iic b
h₁ : a = b ∨ a ∈ Iio b ↔ a ≤ b
⊢ a ∈ insert b (Iio b) ↔ a ∈ Iic b
have h₂ : a = b ∨ a < b ↔ a ≤ b
Tactic: simp_rw [Finset.mem_insert, mem_Iic, mem_Iio, le_iff_lt_or_eq, or_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderBot α
inst_2 : DecidableEq α
b a : α
h : a = b ∨ a ∈ Iio b ↔ a ∈ Iic b
h₁ : a = b ∨ a ∈ Iio b ↔ a ≤ b
h₂ : a = b ∨ a < b ↔ a ≤ b
⊢ a ∈ insert b (Iio b) ↔ a ∈ Iic b
have h₃ : a = b ∨ a < b ↔ a < b ∨ a = b
Tactic: simp_rw [Finset.mem_insert, mem_Iic, mem_Iio, le_iff_lt_or_eq, or_comm]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderBot α
b : α
⊢ Iic b = cons b (Iio b) ⋯
have rw : Iic b = insert b (Iio b)
Tactic: rw [cons_eq_insert, Iio_insert]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderBot α
b : α
rw : Iic b = insert b (Iio b)
⊢ Iic b = cons b (Iio b) ⋯
have rw₁ : Iic b = Iic b
Tactic: rw [cons_eq_insert, Iio_insert]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderBot α
b : α
⊢ Iic b = cons b (Iio b) ⋯
have classical : Iic b = insert b (Iio b)
Tactic: classical rw [cons_eq_insert, Iio_insert]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderBot α
b : α
classical : Iic b = insert b (Iio b)
⊢ Iic b = cons b (Iio b) ⋯
have classical₁ : Iic b = Iic b
Tactic: classical rw [cons_eq_insert, Iio_insert]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderBot α
a : α
⊢ #(Iio a) = #(Iic a) - 1
have rw : #(Iio a) = #(cons a (Iio a) sorry) - 1
Tactic: rw [Iic_eq_cons_Iio, card_cons, Nat.add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderBot α
a : α
rw : #(Iio a) = #(cons a (Iio a) ⋯) - 1
⊢ #(Iio a) = #(Iic a) - 1
have rw₁ : #(Iio a) = #(Iio a) + 1 - 1
Tactic: rw [Iic_eq_cons_Iio, card_cons, Nat.add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrderBot α
a : α
rw : #(Iio a) = #(cons a (Iio a) ⋯) - 1
rw₁ : #(Iio a) = #(Iio a) + 1 - 1
⊢ #(Iio a) = #(Iic a) - 1
have rw₂ : #(Iio a) = #(Iio a)
Tactic: rw [Iic_eq_cons_Iio, card_cons, Nat.add_sub_cancel_right]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : SemilatticeSup α
inst_1 : LocallyFiniteOrderBot α
inst_2 : OrderBot α
inst_3 : DecidableEq α
f : ι → α
s : Finset ι
⊢ image f s ⊆ Iic (s.sup f)
have refine : ∀ (i : α) (hi : i ∈ image f s), i ≤ s.sup f
Tactic: refine fun i hi ↦ mem_Iic.2 ?_
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : SemilatticeSup α
inst_1 : LocallyFiniteOrderBot α
inst_2 : OrderBot α
inst_3 : DecidableEq α
f : ι → α
s : Finset ι
i : α
hi : i ∈ image f s
⊢ i ≤ s.sup f
have obtain : ∀ (j : ι) (hj : j ∈ s) (hi : f j ∈ image f s), f j ≤ s.sup f
Tactic: obtain ⟨j, hj, rfl⟩ := mem_image.1 hi
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a₁ b₁ a₂ b₂ : α
h : a₁ < b₁
⊢ Ico a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
have rw : (↑(Ico a₁ b₁) : Set α) ⊆ (↑(Ico a₂ b₂) : Set α) ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
Tactic: rw [← coe_subset, coe_Ico, coe_Ico, Set.Ico_subset_Ico_iff h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a₁ b₁ a₂ b₂ : α
h : a₁ < b₁
rw : (↑(Ico a₁ b₁) : Set α) ⊆ (↑(Ico a₂ b₂) : Set α) ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
⊢ Ico a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
have rw₁ : Set.Ico a₁ b₁ ⊆ (↑(Ico a₂ b₂) : Set α) ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
Tactic: rw [← coe_subset, coe_Ico, coe_Ico, Set.Ico_subset_Ico_iff h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a₁ b₁ a₂ b₂ : α
h : a₁ < b₁
rw : (↑(Ico a₁ b₁) : Set α) ⊆ (↑(Ico a₂ b₂) : Set α) ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
rw₁ : Set.Ico a₁ b₁ ⊆ (↑(Ico a₂ b₂) : Set α) ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
⊢ Ico a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
have rw₂ : Set.Ico a₁ b₁ ⊆ Set.Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
Tactic: rw [← coe_subset, coe_Ico, coe_Ico, Set.Ico_subset_Ico_iff h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a₁ b₁ a₂ b₂ : α
h : a₁ < b₁
rw : (↑(Ico a₁ b₁) : Set α) ⊆ (↑(Ico a₂ b₂) : Set α) ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
rw₁ : Set.Ico a₁ b₁ ⊆ (↑(Ico a₂ b₂) : Set α) ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
rw₂ : Set.Ico a₁ b₁ ⊆ Set.Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
⊢ Ico a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
have rw₃ : a₂ ≤ a₁ ∧ b₁ ≤ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
Tactic: rw [← coe_subset, coe_Ico, coe_Ico, Set.Ico_subset_Ico_iff h]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
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) : Set α) = (↑(Ico a c) : Set α)
Tactic: rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico_eq_Ico hab hbc]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
rw : (↑(Ico a b ∪ Ico b c) : Set α) = (↑(Ico a c) : Set α)
⊢ Ico a b ∪ Ico b c = Ico a c
have rw₁ : (↑(Ico a b) : Set α) ∪ (↑(Ico b c) : Set α) = (↑(Ico a c) : Set α)
Tactic: rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico_eq_Ico hab hbc]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
rw : (↑(Ico a b ∪ Ico b c) : Set α) = (↑(Ico a c) : Set α)
rw₁ : (↑(Ico a b) : Set α) ∪ (↑(Ico b c) : Set α) = (↑(Ico a c) : Set α)
⊢ Ico a b ∪ Ico b c = Ico a c
have rw₂ : Set.Ico a b ∪ (↑(Ico b c) : Set α) = (↑(Ico a c) : Set α)
Tactic: rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico_eq_Ico hab hbc]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
rw : (↑(Ico a b ∪ Ico b c) : Set α) = (↑(Ico a c) : Set α)
rw₁ : (↑(Ico a b) : Set α) ∪ (↑(Ico b c) : Set α) = (↑(Ico a c) : Set α)
rw₂ : Set.Ico a b ∪ (↑(Ico b c) : Set α) = (↑(Ico a c) : Set α)
⊢ Ico a b ∪ Ico b c = Ico a c
have rw₃ : Set.Ico a b ∪ Set.Ico b c = (↑(Ico a c) : Set α)
Tactic: rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico_eq_Ico hab hbc]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
rw : (↑(Ico a b ∪ Ico b c) : Set α) = (↑(Ico a c) : Set α)
rw₁ : (↑(Ico a b) : Set α) ∪ (↑(Ico b c) : Set α) = (↑(Ico a c) : Set α)
rw₂ : Set.Ico a b ∪ (↑(Ico b c) : Set α) = (↑(Ico a c) : Set α)
rw₃ : Set.Ico a b ∪ Set.Ico b c = (↑(Ico a c) : Set α)
⊢ Ico a b ∪ Ico b c = Ico a c
have rw₄ : Set.Ico a b ∪ Set.Ico b c = Set.Ico a c
Tactic: rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico_eq_Ico hab hbc]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
hab : a ≤ b
hbc : b ≤ c
rw : (↑(Ico a b ∪ Ico b c) : Set α) = (↑(Ico a c) : Set α)
rw₁ : (↑(Ico a b) : Set α) ∪ (↑(Ico b c) : Set α) = (↑(Ico a c) : Set α)
rw₂ : Set.Ico a b ∪ (↑(Ico b c) : Set α) = (↑(Ico a c) : Set α)
rw₃ : Set.Ico a b ∪ Set.Ico b c = (↑(Ico a c) : Set α)
rw₄ : Set.Ico a b ∪ Set.Ico b c = Set.Ico a c
⊢ Ico a b ∪ Ico b c = Ico a c
have rw₅ : Set.Ico a c = Set.Ico a c
Tactic: rw [← coe_inj, coe_union, coe_Ico, coe_Ico, coe_Ico, Set.Ico_union_Ico_eq_Ico hab hbc]