awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : DecidableLE α
S : Set (Interval α)
change :
  (↑(if h :
            ⊥ ∉ S ∧
              ∀ ⦃s : NonemptyInterval α⦄,
                (↑s : Interval α) ∈ S → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ S → s.toProd.1 ≤ t.toProd.2 then
          (↑{ fst := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ S), s.toProd.1,
                snd := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ S), s.toProd.2, fst_le_snd := ⋯ :
                NonemptyInterval α } :
            Interval α)
        else ⊥) :
      Set α) =
    ⋂ s ∈ S, (↑s : Set α)
pos :
  ∀
    (h :
      ⊥ ∉ S ∧
        ∀ ⦃s : NonemptyInterval α⦄,
          (↑s : Interval α) ∈ S → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ S → s.toProd.1 ≤ t.toProd.2),
    (↑(↑{ fst := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ S), s.toProd.1,
                snd := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ S), s.toProd.2, fst_le_snd := ⋯ :
                NonemptyInterval α } :
            Interval α) :
        Set α) =
      ⋂ s ∈ S, (↑s : Set α)
neg neg₁ :
  ∀
    (h :
      ¬(⊥ ∉ S ∧
          ∀ ⦃s : NonemptyInterval α⦄,
            (↑s : Interval α) ∈ S → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ S → s.toProd.1 ≤ t.toProd.2)),
    (↑⊥ : Set α) = ⋂ s ∈ S, (↑s : Set α)
neg₂ :
  ∀
    (h :
      ⊥ ∈ S ∨
        ¬∀ ⦃s : NonemptyInterval α⦄,
            (↑s : Interval α) ∈ S → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ S → s.toProd.1 ≤ t.toProd.2),
    (↑⊥ : Set α) = ⋂ s ∈ S, (↑s : Set α)
⊢ (↑(sInf S) : Set α) = ⋂ s ∈ S, (↑s : Set α)
have neg₃ : ∀ (h : ⊥ ∈ S), (↑⊥ : Set α) = ⋂ s ∈ S, (↑s : Set α)
Tactic: classical
  change ((dite _ _ _ : Interval α) : Set α) = ⋂ (s : Interval α) (_ : s ∈ S), (s : Set α)
  split_ifs with h
  · ext
    simp [Interval.forall, h.1, ← forall_and, ← NonemptyInterval.mem_def]
  simp_rw [not_and_or, Classical.not_not] at h
  rcases h with h | h
  · refine (eq_empty_of_subset_empty ?_).symm
    exact iInter₂_subset_of_subset _ h Subset.rfl
  · refine (not_nonempty_iff_eq_empty.1 ?_).symm
    rintro ⟨x, hx⟩
    rw [mem_iInter₂] at hx
    exact h fun s ha t hb => (hx _ ha).1.trans (hx _ hb).2
-- Lean 4 proof step from Mathlib.Order.Interval.Basic (goal)
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : DecidableLE α
S : Set (Interval α)
change :
  (↑(if h :
            ⊥ ∉ S ∧
              ∀ ⦃s : NonemptyInterval α⦄,
                (↑s : Interval α) ∈ S → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ S → s.toProd.1 ≤ t.toProd.2 then
          (↑{ fst := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ S), s.toProd.1,
                snd := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ S), s.toProd.2, fst_le_snd := ⋯ :
                NonemptyInterval α } :
            Interval α)
        else ⊥) :
      Set α) =
    ⋂ s ∈ S, (↑s : Set α)
pos :
  ∀
    (h :
      ⊥ ∉ S ∧
        ∀ ⦃s : NonemptyInterval α⦄,
          (↑s : Interval α) ∈ S → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ S → s.toProd.1 ≤ t.toProd.2),
    (↑(↑{ fst := ⨆ (s : NonemptyInterval α), ⨆ (_ : (↑s : Interval α) ∈ S), s.toProd.1,
                snd := ⨅ (s : NonemptyInterval α), ⨅ (_ : (↑s : Interval α) ∈ S), s.toProd.2, fst_le_snd := ⋯ :
                NonemptyInterval α } :
            Interval α) :
        Set α) =
      ⋂ s ∈ S, (↑s : Set α)
neg neg₁ :
  ∀
    (h :
      ¬(⊥ ∉ S ∧
          ∀ ⦃s : NonemptyInterval α⦄,
            (↑s : Interval α) ∈ S → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ S → s.toProd.1 ≤ t.toProd.2)),
    (↑⊥ : Set α) = ⋂ s ∈ S, (↑s : Set α)
neg₂ :
  ∀
    (h :
      ⊥ ∈ S ∨
        ¬∀ ⦃s : NonemptyInterval α⦄,
            (↑s : Interval α) ∈ S → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ S → s.toProd.1 ≤ t.toProd.2),
    (↑⊥ : Set α) = ⋂ s ∈ S, (↑s : Set α)
neg₃ : ∀ (h : ⊥ ∈ S), (↑⊥ : Set α) = ⋂ s ∈ S, (↑s : Set α)
⊢ (↑(sInf S) : Set α) = ⋂ s ∈ S, (↑s : Set α)
have neg₄ : ∀
  (h :
    ¬∀ ⦃s : NonemptyInterval α⦄,
        (↑s : Interval α) ∈ S → ∀ ⦃t : NonemptyInterval α⦄, (↑t : Interval α) ∈ S → s.toProd.1 ≤ t.toProd.2),
  (↑⊥ : Set α) = ⋂ s ∈ S, (↑s : Set α)
Tactic: classical
  change ((dite _ _ _ : Interval α) : Set α) = ⋂ (s : Interval α) (_ : s ∈ S), (s : Set α)
  split_ifs with h
  · ext
    simp [Interval.forall, h.1, ← forall_and, ← NonemptyInterval.mem_def]
  simp_rw [not_and_or, Classical.not_not] at h
  rcases h with h | h
  · refine (eq_empty_of_subset_empty ?_).symm
    exact iInter₂_subset_of_subset _ h Subset.rfl
  · refine (not_nonempty_iff_eq_empty.1 ?_).symm
    rintro ⟨x, hx⟩
    rw [mem_iInter₂] at hx
    exact h fun s ha t hb => (hx _ ha).1.trans (hx _ hb).2
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
⊢ (Icc a b).Nonempty ↔ a ≤ b
have rw : (↑(Icc a b) : Set α).Nonempty ↔ a ≤ b
Tactic: rw [← coe_nonempty, coe_Icc, Set.nonempty_Icc]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
rw : (↑(Icc a b) : Set α).Nonempty ↔ a ≤ b
⊢ (Icc a b).Nonempty ↔ a ≤ b
have rw₁ : (Set.Icc a b).Nonempty ↔ a ≤ b
Tactic: rw [← coe_nonempty, coe_Icc, Set.nonempty_Icc]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
rw : (↑(Icc a b) : Set α).Nonempty ↔ a ≤ b
rw₁ : (Set.Icc a b).Nonempty ↔ a ≤ b
⊢ (Icc a b).Nonempty ↔ a ≤ b
have rw₂ : a ≤ b ↔ a ≤ b
Tactic: rw [← coe_nonempty, coe_Icc, Set.nonempty_Icc]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
⊢ (Ico a b).Nonempty ↔ a < b
have rw : (↑(Ico a b) : Set α).Nonempty ↔ a < b
Tactic: rw [← coe_nonempty, coe_Ico, Set.nonempty_Ico]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
rw : (↑(Ico a b) : Set α).Nonempty ↔ a < b
⊢ (Ico a b).Nonempty ↔ a < b
have rw₁ : (Set.Ico a b).Nonempty ↔ a < b
Tactic: rw [← coe_nonempty, coe_Ico, Set.nonempty_Ico]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
rw : (↑(Ico a b) : Set α).Nonempty ↔ a < b
rw₁ : (Set.Ico a b).Nonempty ↔ a < b
⊢ (Ico a b).Nonempty ↔ a < b
have rw₂ : a < b ↔ a < b
Tactic: rw [← coe_nonempty, coe_Ico, Set.nonempty_Ico]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
⊢ (Ioc a b).Nonempty ↔ a < b
have rw : (↑(Ioc a b) : Set α).Nonempty ↔ a < b
Tactic: rw [← coe_nonempty, coe_Ioc, Set.nonempty_Ioc]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
rw : (↑(Ioc a b) : Set α).Nonempty ↔ a < b
⊢ (Ioc a b).Nonempty ↔ a < b
have rw₁ : (Set.Ioc a b).Nonempty ↔ a < b
Tactic: rw [← coe_nonempty, coe_Ioc, Set.nonempty_Ioc]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
rw : (↑(Ioc a b) : Set α).Nonempty ↔ a < b
rw₁ : (Set.Ioc a b).Nonempty ↔ a < b
⊢ (Ioc a b).Nonempty ↔ a < b
have rw₂ : a < b ↔ a < b
Tactic: rw [← coe_nonempty, coe_Ioc, Set.nonempty_Ioc]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DenselyOrdered α
⊢ (Ioo a b).Nonempty ↔ a < b
have rw : (↑(Ioo a b) : Set α).Nonempty ↔ a < b
Tactic: rw [← coe_nonempty, coe_Ioo, Set.nonempty_Ioo]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DenselyOrdered α
rw : (↑(Ioo a b) : Set α).Nonempty ↔ a < b
⊢ (Ioo a b).Nonempty ↔ a < b
have rw₁ : (Set.Ioo a b).Nonempty ↔ a < b
Tactic: rw [← coe_nonempty, coe_Ioo, Set.nonempty_Ioo]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DenselyOrdered α
rw : (↑(Ioo a b) : Set α).Nonempty ↔ a < b
rw₁ : (Set.Ioo a b).Nonempty ↔ a < b
⊢ (Ioo a b).Nonempty ↔ a < b
have rw₂ : a < b ↔ a < b
Tactic: rw [← coe_nonempty, coe_Ioo, Set.nonempty_Ioo]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
⊢ Icc a b = ∅ ↔ ¬a ≤ b
have rw : (↑(Icc a b) : Set α) = ∅ ↔ ¬a ≤ b
Tactic: rw [← coe_eq_empty, coe_Icc, Set.Icc_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
rw : (↑(Icc a b) : Set α) = ∅ ↔ ¬a ≤ b
⊢ Icc a b = ∅ ↔ ¬a ≤ b
have rw₁ : Set.Icc a b = ∅ ↔ ¬a ≤ b
Tactic: rw [← coe_eq_empty, coe_Icc, Set.Icc_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
rw : (↑(Icc a b) : Set α) = ∅ ↔ ¬a ≤ b
rw₁ : Set.Icc a b = ∅ ↔ ¬a ≤ b
⊢ Icc a b = ∅ ↔ ¬a ≤ b
have rw₂ : ¬a ≤ b ↔ ¬a ≤ b
Tactic: rw [← coe_eq_empty, coe_Icc, Set.Icc_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
⊢ Ico a b = ∅ ↔ ¬a < b
have rw : (↑(Ico a b) : Set α) = ∅ ↔ ¬a < b
Tactic: rw [← coe_eq_empty, coe_Ico, Set.Ico_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
rw : (↑(Ico a b) : Set α) = ∅ ↔ ¬a < b
⊢ Ico a b = ∅ ↔ ¬a < b
have rw₁ : Set.Ico a b = ∅ ↔ ¬a < b
Tactic: rw [← coe_eq_empty, coe_Ico, Set.Ico_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
rw : (↑(Ico a b) : Set α) = ∅ ↔ ¬a < b
rw₁ : Set.Ico a b = ∅ ↔ ¬a < b
⊢ Ico a b = ∅ ↔ ¬a < b
have rw₂ : ¬a < b ↔ ¬a < b
Tactic: rw [← coe_eq_empty, coe_Ico, Set.Ico_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
⊢ Ioc a b = ∅ ↔ ¬a < b
have rw : (↑(Ioc a b) : Set α) = ∅ ↔ ¬a < b
Tactic: rw [← coe_eq_empty, coe_Ioc, Set.Ioc_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
rw : (↑(Ioc a b) : Set α) = ∅ ↔ ¬a < b
⊢ Ioc a b = ∅ ↔ ¬a < b
have rw₁ : Set.Ioc a b = ∅ ↔ ¬a < b
Tactic: rw [← coe_eq_empty, coe_Ioc, Set.Ioc_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
rw : (↑(Ioc a b) : Set α) = ∅ ↔ ¬a < b
rw₁ : Set.Ioc a b = ∅ ↔ ¬a < b
⊢ Ioc a b = ∅ ↔ ¬a < b
have rw₂ : ¬a < b ↔ ¬a < b
Tactic: rw [← coe_eq_empty, coe_Ioc, Set.Ioc_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DenselyOrdered α
⊢ Ioo a b = ∅ ↔ ¬a < b
have rw : (↑(Ioo a b) : Set α) = ∅ ↔ ¬a < b
Tactic: rw [← coe_eq_empty, coe_Ioo, Set.Ioo_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DenselyOrdered α
rw : (↑(Ioo a b) : Set α) = ∅ ↔ ¬a < b
⊢ Ioo a b = ∅ ↔ ¬a < b
have rw₁ : Set.Ioo a b = ∅ ↔ ¬a < b
Tactic: rw [← coe_eq_empty, coe_Ioo, Set.Ioo_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DenselyOrdered α
rw : (↑(Ioo a b) : Set α) = ∅ ↔ ¬a < b
rw₁ : Set.Ioo a b = ∅ ↔ ¬a < b
⊢ Ioo a b = ∅ ↔ ¬a < b
have rw₂ : ¬a < b ↔ ¬a < b
Tactic: rw [← coe_eq_empty, coe_Ioo, Set.Ioo_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a₁ a₂ b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h : a₁ < a₂
⊢ Ico a₂ b ⊆ Ioo a₁ b
have rw : Set.Ico a₂ b ⊆ Set.Ioo a₁ b
Tactic: rw [← coe_subset, coe_Ico, coe_Ioo]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h : b₁ < b₂
⊢ Ioc a b₁ ⊆ Ioo a b₂
have rw : Set.Ioc a b₁ ⊆ Set.Ioo a b₂
Tactic: rw [← coe_subset, coe_Ioc, coe_Ioo]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h : b₁ < b₂
⊢ Icc a b₁ ⊆ Ico a b₂
have rw : Set.Icc a b₁ ⊆ Set.Ico a b₂
Tactic: rw [← coe_subset, coe_Icc, coe_Ico]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
⊢ Ioo a b ⊆ Ico a b
have rw : Set.Ioo a b ⊆ Set.Ico a b
Tactic: rw [← coe_subset, coe_Ioo, coe_Ico]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
⊢ Ioo a b ⊆ Ioc a b
have rw : Set.Ioo a b ⊆ Set.Ioc a b
Tactic: rw [← coe_subset, coe_Ioo, coe_Ioc]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
⊢ Ico a b ⊆ Icc a b
have rw : Set.Ico a b ⊆ Set.Icc a b
Tactic: rw [← coe_subset, coe_Ico, coe_Icc]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
⊢ Ioc a b ⊆ Icc a b
have rw : Set.Ioc a b ⊆ Set.Icc a b
Tactic: rw [← coe_subset, coe_Ioc, coe_Icc]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
⊢ Icc a₁ b₁ ⊆ Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
have rw : (↑(Icc a₁ b₁) : Set α) ⊆ (↑(Icc a₂ b₂) : Set α) ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
Tactic: rw [← coe_subset, coe_Icc, coe_Icc, Set.Icc_subset_Icc_iff h₁]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
rw : (↑(Icc a₁ b₁) : Set α) ⊆ (↑(Icc a₂ b₂) : Set α) ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
⊢ Icc a₁ b₁ ⊆ Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
have rw₁ : Set.Icc a₁ b₁ ⊆ (↑(Icc a₂ b₂) : Set α) ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
Tactic: rw [← coe_subset, coe_Icc, coe_Icc, Set.Icc_subset_Icc_iff h₁]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
rw : (↑(Icc a₁ b₁) : Set α) ⊆ (↑(Icc a₂ b₂) : Set α) ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
rw₁ : Set.Icc a₁ b₁ ⊆ (↑(Icc a₂ b₂) : Set α) ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
⊢ Icc a₁ b₁ ⊆ Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
have rw₂ : Set.Icc a₁ b₁ ⊆ Set.Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
Tactic: rw [← coe_subset, coe_Icc, coe_Icc, Set.Icc_subset_Icc_iff h₁]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
rw : (↑(Icc a₁ b₁) : Set α) ⊆ (↑(Icc a₂ b₂) : Set α) ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
rw₁ : Set.Icc a₁ b₁ ⊆ (↑(Icc a₂ b₂) : Set α) ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
rw₂ : Set.Icc a₁ b₁ ⊆ Set.Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
⊢ Icc a₁ b₁ ⊆ Icc a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
have rw₃ : a₂ ≤ a₁ ∧ b₁ ≤ b₂ ↔ a₂ ≤ a₁ ∧ b₁ ≤ b₂
Tactic: rw [← coe_subset, coe_Icc, coe_Icc, Set.Icc_subset_Icc_iff h₁]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
⊢ Icc a₁ b₁ ⊆ Ioo a₂ b₂ ↔ a₂ < a₁ ∧ b₁ < b₂
have rw : (↑(Icc a₁ b₁) : Set α) ⊆ (↑(Ioo a₂ b₂) : Set α) ↔ a₂ < a₁ ∧ b₁ < b₂
Tactic: rw [← coe_subset, coe_Icc, coe_Ioo, Set.Icc_subset_Ioo_iff h₁]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
rw : (↑(Icc a₁ b₁) : Set α) ⊆ (↑(Ioo a₂ b₂) : Set α) ↔ a₂ < a₁ ∧ b₁ < b₂
⊢ Icc a₁ b₁ ⊆ Ioo a₂ b₂ ↔ a₂ < a₁ ∧ b₁ < b₂
have rw₁ : Set.Icc a₁ b₁ ⊆ (↑(Ioo a₂ b₂) : Set α) ↔ a₂ < a₁ ∧ b₁ < b₂
Tactic: rw [← coe_subset, coe_Icc, coe_Ioo, Set.Icc_subset_Ioo_iff h₁]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
rw : (↑(Icc a₁ b₁) : Set α) ⊆ (↑(Ioo a₂ b₂) : Set α) ↔ a₂ < a₁ ∧ b₁ < b₂
rw₁ : Set.Icc a₁ b₁ ⊆ (↑(Ioo a₂ b₂) : Set α) ↔ a₂ < a₁ ∧ b₁ < b₂
⊢ Icc a₁ b₁ ⊆ Ioo a₂ b₂ ↔ a₂ < a₁ ∧ b₁ < b₂
have rw₂ : Set.Icc a₁ b₁ ⊆ Set.Ioo a₂ b₂ ↔ a₂ < a₁ ∧ b₁ < b₂
Tactic: rw [← coe_subset, coe_Icc, coe_Ioo, Set.Icc_subset_Ioo_iff h₁]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
rw : (↑(Icc a₁ b₁) : Set α) ⊆ (↑(Ioo a₂ b₂) : Set α) ↔ a₂ < a₁ ∧ b₁ < b₂
rw₁ : Set.Icc a₁ b₁ ⊆ (↑(Ioo a₂ b₂) : Set α) ↔ a₂ < a₁ ∧ b₁ < b₂
rw₂ : Set.Icc a₁ b₁ ⊆ Set.Ioo a₂ b₂ ↔ a₂ < a₁ ∧ b₁ < b₂
⊢ Icc a₁ b₁ ⊆ Ioo a₂ b₂ ↔ a₂ < a₁ ∧ b₁ < b₂
have rw₃ : a₂ < a₁ ∧ b₁ < b₂ ↔ a₂ < a₁ ∧ b₁ < b₂
Tactic: rw [← coe_subset, coe_Icc, coe_Ioo, Set.Icc_subset_Ioo_iff h₁]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
⊢ Icc a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ < b₂
have rw : (↑(Icc a₁ b₁) : Set α) ⊆ (↑(Ico a₂ b₂) : Set α) ↔ a₂ ≤ a₁ ∧ b₁ < b₂
Tactic: rw [← coe_subset, coe_Icc, coe_Ico, Set.Icc_subset_Ico_iff h₁]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
rw : (↑(Icc a₁ b₁) : Set α) ⊆ (↑(Ico a₂ b₂) : Set α) ↔ a₂ ≤ a₁ ∧ b₁ < b₂
⊢ Icc a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ < b₂
have rw₁ : Set.Icc a₁ b₁ ⊆ (↑(Ico a₂ b₂) : Set α) ↔ a₂ ≤ a₁ ∧ b₁ < b₂
Tactic: rw [← coe_subset, coe_Icc, coe_Ico, Set.Icc_subset_Ico_iff h₁]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
rw : (↑(Icc a₁ b₁) : Set α) ⊆ (↑(Ico a₂ b₂) : Set α) ↔ a₂ ≤ a₁ ∧ b₁ < b₂
rw₁ : Set.Icc a₁ b₁ ⊆ (↑(Ico a₂ b₂) : Set α) ↔ a₂ ≤ a₁ ∧ b₁ < b₂
⊢ Icc a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ < b₂
have rw₂ : Set.Icc a₁ b₁ ⊆ Set.Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ < b₂
Tactic: rw [← coe_subset, coe_Icc, coe_Ico, Set.Icc_subset_Ico_iff h₁]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
h₁ : a₁ ≤ b₁
rw : (↑(Icc a₁ b₁) : Set α) ⊆ (↑(Ico a₂ b₂) : Set α) ↔ a₂ ≤ a₁ ∧ b₁ < b₂
rw₁ : Set.Icc a₁ b₁ ⊆ (↑(Ico a₂ b₂) : Set α) ↔ a₂ ≤ a₁ ∧ b₁ < b₂
rw₂ : Set.Icc a₁ b₁ ⊆ Set.Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ < b₂
⊢ Icc a₁ b₁ ⊆ Ico a₂ b₂ ↔ a₂ ≤ a₁ ∧ b₁ < b₂
have rw₃ : a₂ ≤ a₁ ∧ b₁ < b₂ ↔ a₂ ≤ a₁ ∧ b₁ < b₂
Tactic: rw [← coe_subset, coe_Icc, coe_Ico, Set.Icc_subset_Ico_iff h₁]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
hI : a₂ ≤ b₂
ha : a₂ < a₁
hb : b₁ ≤ b₂
⊢ Icc a₁ b₁ ⊂ Icc a₂ b₂
have rw : Set.Icc a₁ b₁ ⊂ Set.Icc a₂ b₂
Tactic: rw [← coe_ssubset, coe_Icc, coe_Icc]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
hI : a₂ ≤ b₂
ha : a₂ ≤ a₁
hb : b₁ < b₂
⊢ Icc a₁ b₁ ⊂ Icc a₂ b₂
have rw : Set.Icc a₁ b₁ ⊂ Set.Icc a₂ b₂
Tactic: rw [← coe_ssubset, coe_Icc, coe_Icc]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DenselyOrdered α
a b : α
h : a < b
⊢ False
have H : ∀ (i : Finset α) (ih : ∀ t ⊂ i, ∀ (b : α) (h : a < b) (hs : Icc a b = t), False) (b : α) (h : a < b) (hs : Icc a b = i),
  False
Tactic: induction hs : Finset.Icc a b using Finset.strongInduction generalizing b with | H i ih
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (hypothesis)
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DenselyOrdered α
a : α
i : Finset α
ih : ∀ t ⊂ i, ∀ (b : α) (h : a < b) (hs : Icc a b = t), False
b : α
h : a < b
hs : Icc a b = i
⊢ False
have ih₁ : ∀ t ⊂ Icc a b, ∀ (b : α) (h : a < b) (hs : Icc a b = t), False
Tactic: subst hs
Cleared hypotheses: i, ih, hs
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DenselyOrdered α
a b : α
h : a < b
ih : ∀ t ⊂ Icc a b, ∀ (b : α) (h : a < b) (hs : Icc a b = t), False
⊢ False
have H : ∀ (c : α) (hac : a < c) (hcb : c < b), False
Tactic: obtain ⟨c, hac, hcb⟩ := exists_between h
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : DenselyOrdered α
a b : α
h : a < b
ih : ∀ t ⊂ Icc a b, ∀ (b : α) (h : a < b) (hs : Icc a b = t), False
c : α
hac : a < c
hcb : c < b
⊢ False
have H : Icc a c ⊂ Icc a b
Tactic: refine ih _ ?_ c hac rfl
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : Fintype α
inst_3 : DecidablePred fun (j : α) ↦ a < j ∧ j < b
⊢ {j : α | a < j ∧ j < b} = Ioo a b
have h : ∀ (a_1 : α), Membership.mem (γ := Finset α) {j : α | a < j ∧ j < b} a_1 ↔ a_1 ∈ Ioo a b
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : Fintype α
inst_3 : DecidablePred fun (j : α) ↦ a < j ∧ j ≤ b
⊢ {j : α | a < j ∧ j ≤ b} = Ioc a b
have h : ∀ (a_1 : α), Membership.mem (γ := Finset α) {j : α | a < j ∧ j ≤ b} a_1 ↔ a_1 ∈ Ioc a b
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : Fintype α
inst_3 : DecidablePred fun (j : α) ↦ a ≤ j ∧ j < b
⊢ {j : α | a ≤ j ∧ j < b} = Ico a b
have h : ∀ (a_1 : α), Membership.mem (γ := Finset α) {j : α | a ≤ j ∧ j < b} a_1 ↔ a_1 ∈ Ico a b
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a b : α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : Fintype α
inst_3 : DecidablePred fun (j : α) ↦ a ≤ j ∧ j ≤ b
⊢ {j : α | a ≤ j ∧ j ≤ b} = Icc a b
have h : ∀ (a_1 : α), Membership.mem (γ := Finset α) {j : α | a ≤ j ∧ j ≤ b} a_1 ↔ a_1 ∈ Icc a b
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a : α
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
⊢ Ioi a = ∅ ↔ IsMax a
have rw : (↑(Ioi a) : Set α) = ∅ ↔ IsMax a
Tactic: rw [← coe_eq_empty, coe_Ioi, Set.Ioi_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a : α
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
rw : (↑(Ioi a) : Set α) = ∅ ↔ IsMax a
⊢ Ioi a = ∅ ↔ IsMax a
have rw₁ : Set.Ioi a = ∅ ↔ IsMax a
Tactic: rw [← coe_eq_empty, coe_Ioi, Set.Ioi_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a : α
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
rw : (↑(Ioi a) : Set α) = ∅ ↔ IsMax a
rw₁ : Set.Ioi a = ∅ ↔ IsMax a
⊢ Ioi a = ∅ ↔ IsMax a
have rw₂ : IsMax a ↔ IsMax a
Tactic: rw [← coe_eq_empty, coe_Ioi, Set.Ioi_eq_empty_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
a : α
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
⊢ (Ioi a).Nonempty ↔ ¬IsMax a
have contrapose! : Ioi a = ∅ ↔ IsMax a
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Order.Interval.Finset.Basic (goal)
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrderTop α
inst_2 : OrderBot α
inst_3 : Fintype α
⊢ Eq.{u_2 + 1} (α := Finset α) (Ici ⊥) univ
have h : ∀ (a : α), Membership.mem (γ := Finset α) (Ici ⊥) a ↔ Membership.mem (γ := Finset α) univ a
Tactic: ext a