awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) ((fun (b : α) ↦ Ι b a) b) x ↔ Membership.mem (γ := Set α) ((fun (b : α) ↦ Ι b a) c) x
ha : a < b
inr : b ≤ c
⊢ b = c

Tactic:
refine
      eq_of_mem_uIoc_of_mem_uIoc ((h _).1 <| left_mem_uIoc.2 ha)
        ((h _).2 <| left_mem_uIoc.2 <| ha.trans_le ?_)

Premises used: Iff.mpr, Set.left_mem_uIoc, LT.lt.trans_le, Iff.mp, Set.eq_of_mem_uIoc_of_mem_uIoc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) ((fun (b : α) ↦ Ι b a) b) x ↔ Membership.mem (γ := Set α) ((fun (b : α) ↦ Ι b a) c) x
ha : a < b
⊢ b ≤ c

Tactic:
simpa [ha, ha.not_ge, mem_uIoc] using h b

Premises used: Set.mem_uIoc, LT.lt.not_ge
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a : α
⊢ Injective (Ι a)

Tactic:
simpa only [uIoc_comm] using uIoc_injective_right a

Premises used: Set.uIoc_comm, Set.uIoc_injective_right
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h : b ∈ [[a, c]]
inr :
  ∀ (this : ∀ {a c : α} (h : b ∈ [[a, c]]) (hac : a ≤ c), Ι a b ∪ Ι b c = Ι a c) (hac : ¬a ≤ c), Ι a b ∪ Ι b c = Ι a c
wlog : ∀ {a c : α} (h : b ∈ [[a, c]]) (hac : a ≤ c), Ι a b ∪ Ι b c = Ι a c
⊢ Ι a b ∪ Ι b c = Ι a c

Tactic:
wlog hac : a ≤ c generalizing a c
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h : b ∈ [[a, c]]
this : ∀ {a c : α} (h : b ∈ [[a, c]]) (hac : a ≤ c), Ι a b ∪ Ι b c = Ι a c
hac : ¬a ≤ c
rw : b ∈ [[c, a]]
⊢ Ι a b ∪ Ι b c = Ι a c

Tactic:
rw [uIoc_comm, union_comm, uIoc_comm, this _ (le_of_not_ge hac), uIoc_comm]

Premises used: Set.uIoc_comm, le_of_not_ge, Set.union_comm
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b c : α
h : b ∈ [[a, c]]
this : ∀ {a c : α} (h : b ∈ [[a, c]]) (hac : a ≤ c), Ι a b ∪ Ι b c = Ι a c
hac : ¬a ≤ c
rwa rwa₁ rwa₂ rwa₃ : b ∈ [[a, c]]
⊢ b ∈ [[c, a]]

Tactic:
rwa [uIcc_comm]

Premises used: Set.uIcc_comm
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a_1 b c_1 a c : α
h : b ∈ [[a, c]]
hac : a ≤ c
⊢ b ∈ Icc a c

Tactic:
rw [uIcc_of_le hac] at h

Premises used: Set.uIcc_of_le
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a_1 b c_1 a c : α
h : b ∈ [[a, c]]
hac : a ≤ c
h₁ : b ∈ Icc a c
⊢ a ≤ c

Tactic:
rw [uIcc_of_le hac] at h

Premises used: Set.uIcc_of_le
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a_1 b c_1 a c : α
h : b ∈ Icc a c
hac : a ≤ c
rw : Ioc a b ∪ Ι b c = Ι a c
rw₁ : Ioc a b ∪ Ioc b c = Ι a c
rw₂ : Ioc a b ∪ Ioc b c = Ioc a c
rw₃ rw₄ : Ioc a c = Ioc a c
⊢ Ι a b ∪ Ι b c = Ι a c

Tactic:
rw [uIoc_of_le h.1, uIoc_of_le h.2, uIoc_of_le hac, Ioc_union_Ioc_eq_Ioc h.1 h.2]

Premises used: Set.Ioc_union_Ioc_eq_Ioc, And.right, And.left, Set.uIoc_of_le
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ Eq (α := Set αᵒᵈ) (uIoo ((toDual : (a : α) → αᵒᵈ) a) ((toDual : (a : α) → αᵒᵈ) b) : Set αᵒᵈ)
    ((⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' uIoo a b : Set αᵒᵈ)

Tactic:
Ioo_toDual (α := α)

Premises used: Set.uIoo, Set.Ioo_toDual
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : αᵒᵈ
⊢ Eq (α := Set α) (uIoo ((ofDual : (a : αᵒᵈ) → α) a) ((ofDual : (a : αᵒᵈ) → α) b) : Set α)
    ((⇑toDual : (a : α) → αᵒᵈ) ⁻¹' uIoo a b : Set α)

Tactic:
Ioo_ofDual

Premises used: Set.Ioo_ofDual, Set.uIoo
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
rw : Ioo (min a b) (max a b) = Ioo a b
rw₁ : Ioo a (max a b) = Ioo a b
rw₂ rw₃ : Ioo a b = Ioo a b
⊢ uIoo a b = Ioo a b

Tactic:
rw [uIoo, inf_eq_left.2 h, sup_eq_right.2 h]

Premises used: Iff.mpr, Set.uIoo, sup_eq_right, inf_eq_left
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : b ≤ a
rw : Ioo (min a b) (max a b) = Ioo b a
rw₁ : Ioo b (max a b) = Ioo b a
rw₂ rw₃ : Ioo b a = Ioo b a
⊢ uIoo a b = Ioo b a

Tactic:
rw [uIoo, inf_eq_right.2 h, sup_eq_left.2 h]

Premises used: Iff.mpr, sup_eq_left, Set.uIoo, inf_eq_right
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
simp_rw : Ioo (min a b) (max a b) = Ioo (min b a) (max b a)
simp_rw₁ : Ioo (min a b) (max a b) = Ioo (min a b) (max b a)
⊢ uIoo a b = uIoo b a

Tactic:
simp_rw [uIoo, inf_comm, sup_comm]

Premises used: inf_comm, Set.uIoo, sup_comm
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a < b
⊢ uIoo a b = Ioo a b

Tactic:
uIoo_of_le h.le

Premises used: LT.lt.le, Set.uIoo_of_le
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : b < a
⊢ uIoo a b = Ioo b a

Tactic:
uIoo_of_ge h.le

Premises used: Set.uIoo_of_ge, LT.lt.le
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a : α
⊢ uIoo a a = ∅

Tactic:
simp [uIoo]

Premises used: Set.uIoo
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ a ∉ uIoo a b

Tactic:
simp +contextual [uIoo, le_of_lt]

Premises used: le_of_lt, Set.uIoo
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ b ∉ uIoo a b

Tactic:
simp +contextual [uIoo, le_of_lt]

Premises used: le_of_lt, Set.uIoo
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ Ioo a b ⊆ uIoo a b

Tactic:
Ioo_subset_Ioo inf_le_left le_sup_right

Premises used: le_sup_right, Set.uIoo, inf_le_left, Set.Ioo_subset_Ioo
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ Ioo b a ⊆ uIoo a b

Tactic:
Ioo_subset_Ioo inf_le_right le_sup_left

Premises used: le_sup_left, inf_le_right, Set.uIoo, Set.Ioo_subset_Ioo
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b x : α
ha : a < x
hb : x < b
⊢ x ∈ uIoo a b

Tactic:
Ioo_subset_uIoo ⟨ha, hb⟩

Premises used: Set.Ioo_subset_uIoo, And.intro
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b x : α
hb : b < x
ha : x < a
⊢ x ∈ uIoo a b

Tactic:
Ioo_subset_uIoo' ⟨hb, ha⟩

Premises used: And.intro, Set.Ioo_subset_uIoo'
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ Ioo (min a b) (max a b) = uIoo a b

Tactic:
rfl

Premises used: Set.uIoo, rfl
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : ¬a ≤ b
⊢ uIoo a b = Ioo b a

Tactic:
uIoo_of_gt <| lt_of_not_ge h

Premises used: lt_of_not_ge, Set.uIoo_of_gt
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : ¬b ≤ a
⊢ uIoo a b = Ioo a b

Tactic:
uIoo_of_lt <| lt_of_not_ge h

Premises used: lt_of_not_ge, Set.uIoo_of_lt
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ uIoo a b ⊆ [[a, b]]

Tactic:
simp [uIoo, uIcc, Ioo_subset_Icc_self]

Premises used: Set.Ioo_subset_Icc_self, Set.uIoo, Set.uIcc
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
ha : a₁ ∈ Icc a₂ b₂
hb : b₁ ∈ Icc a₂ b₂
⊢ uIoo a₁ b₁ ⊆ Ioo a₂ b₂

Tactic:
Ioo_subset_Ioo (le_inf ha.1 hb.1) (sup_le ha.2 hb.2)

Premises used: le_inf, Set.uIoo, And.right, And.left, sup_le, Set.Ioo_subset_Ioo
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
inst_1 : DenselyOrdered α
⊢ (uIoo a b).Nonempty ↔ a ≠ b

Tactic:
simp [uIoo, eq_comm]

Premises used: eq_comm, Set.uIoo
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ (Ι a b).Nonempty ↔ a ≠ b

Tactic:
simp [uIoc, eq_comm]

Premises used: Set.uIoc, eq_comm
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
inl : ∀ (h : a < b), uIoo a b = Ioo a b ∪ Ioo b a
inr : ∀ (h : b ≤ a), uIoo a b = Ioo a b ∪ Ioo b a
⊢ uIoo a b = Ioo a b ∪ Ioo b a

Tactic:
rcases lt_or_ge a b with h | h

Premises used: lt_or_ge
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a < b
⊢ uIoo a b = Ioo a b ∪ Ioo b a

Tactic:
simp [uIoo_of_lt, h, Ioo_eq_empty_of_le h.le]

Premises used: Set.Ioo_eq_empty_of_le, Set.uIoo_of_lt, LT.lt.le
-- Module: Mathlib.Order.Interval.Set.UnorderedInterval
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : b ≤ a
⊢ uIoo a b = Ioo a b ∪ Ioo b a

Tactic:
simp [uIoo_of_ge, h]

Premises used: Set.uIoo_of_ge
-- Module: Mathlib.Order.Interval.Set.WithBotTop
Goal:
α : Type u_1
⊢ Eq (α := Set α) (some ⁻¹' {⊤}) ∅

Tactic:
eq_empty_of_subset_empty fun _ => coe_ne_top

Premises used: Set.eq_empty_of_subset_empty, WithTop.coe_ne_top
-- Module: Mathlib.Order.Interval.Set.WithBotTop
Goal:
α : Type u_1
inst : Preorder α
h :
  ∀ (x : WithTop α),
    Membership.mem (γ := Set (WithTop α)) (range some) x ↔ Membership.mem (γ := Set (WithTop α)) (Iio ⊤) x
⊢ Eq.{u_1 + 1} (α := Set (WithTop α)) (range some) (Iio ⊤)

Tactic:
ext
-- Module: Mathlib.Order.Interval.Set.WithBotTop
Goal:
α : Type u_1
inst : Preorder α
x : WithTop α
⊢ Membership.mem (γ := Set (WithTop α)) (range some) x ↔ Membership.mem (γ := Set (WithTop α)) (Iio ⊤) x

Tactic:
simp [mem_range, WithTop.lt_top_iff_ne_top, ne_top_iff_exists]

Premises used: Set.mem_range, WithTop.ne_top_iff_exists, WithTop.lt_top_iff_ne_top
-- Module: Mathlib.Order.Interval.Set.WithBotTop
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ some ⁻¹' Ioi (↑a : WithTop α) = Ioi a

Tactic:
ext fun _ => coe_lt_coe

Premises used: Set.ext, WithTop.coe_lt_coe
-- Module: Mathlib.Order.Interval.Set.WithBotTop
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ some ⁻¹' Ici (↑a : WithTop α) = Ici a

Tactic:
ext fun _ => coe_le_coe

Premises used: Set.ext, WithTop.coe_le_coe
-- Module: Mathlib.Order.Interval.Set.WithBotTop
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ some ⁻¹' Iio (↑a : WithTop α) = Iio a

Tactic:
ext fun _ => coe_lt_coe

Premises used: Set.ext, WithTop.coe_lt_coe
-- Module: Mathlib.Order.Interval.Set.WithBotTop
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ some ⁻¹' Iic (↑a : WithTop α) = Iic a

Tactic:
ext fun _ => coe_le_coe

Premises used: Set.ext, WithTop.coe_le_coe
-- Module: Mathlib.Order.Interval.Set.WithBotTop
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ some ⁻¹' Icc (↑a : WithTop α) (↑b : WithTop α) = Icc a b

Tactic:
simp [← Ici_inter_Iic]

Premises used: Set.Ici_inter_Iic
-- Module: Mathlib.Order.Interval.Set.WithBotTop
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ some ⁻¹' Ico (↑a : WithTop α) (↑b : WithTop α) = Ico a b

Tactic:
simp [← Ici_inter_Iio]

Premises used: Set.Ici_inter_Iio
-- Module: Mathlib.Order.Interval.Set.WithBotTop
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ some ⁻¹' Ioc (↑a : WithTop α) (↑b : WithTop α) = Ioc a b

Tactic:
simp [← Ioi_inter_Iic]

Premises used: Set.Ioi_inter_Iic
-- Module: Mathlib.Order.Interval.Set.WithBotTop
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ some ⁻¹' Ioo (↑a : WithTop α) (↑b : WithTop α) = Ioo a b

Tactic:
simp [← Ioi_inter_Iio]

Premises used: Set.Ioi_inter_Iio
-- Module: Mathlib.Order.Interval.Set.WithBotTop
Goal:
α : Type u_1
inst : Preorder α
rw : Eq.{u_1 + 1} (α := Set α) (some ⁻¹' range some) univ
rw₁ rw₂ : Eq.{u_1 + 1} (α := Set α) univ univ
⊢ Eq.{u_1 + 1} (α := Set α) (some ⁻¹' Iio ⊤) univ

Tactic:
rw [← range_coe, preimage_range]

Premises used: Set.preimage_range, WithTop.range_coe
-- Module: Mathlib.Order.Interval.Set.WithBotTop
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ some ⁻¹' Ico (↑a : WithTop α) ⊤ = Ici a

Tactic:
simp [← Ici_inter_Iio]

Premises used: Set.Ici_inter_Iio
-- Module: Mathlib.Order.Interval.Set.WithBotTop
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ some ⁻¹' Ioo (↑a : WithTop α) ⊤ = Ioi a

Tactic:
simp [← Ioi_inter_Iio]

Premises used: Set.Ioi_inter_Iio
-- Module: Mathlib.Order.Interval.Set.WithBotTop
Goal:
α : Type u_1
inst : Preorder α
a : α
rw : some '' some ⁻¹' Ioi (↑a : WithTop α) = Ioo (↑a : WithTop α) ⊤
rw₁ : Ioi (↑a : WithTop α) ∩ range some = Ioo (↑a : WithTop α) ⊤
rw₂ : Ioi (↑a : WithTop α) ∩ Iio ⊤ = Ioo (↑a : WithTop α) ⊤
rw₃ rw₄ : Ioo (↑a : WithTop α) ⊤ = Ioo (↑a : WithTop α) ⊤
⊢ some '' Ioi a = Ioo (↑a : WithTop α) ⊤

Tactic:
rw [← preimage_coe_Ioi, image_preimage_eq_inter_range, range_coe, Ioi_inter_Iio]

Premises used: Set.image_preimage_eq_inter_range, Set.Ioi_inter_Iio, WithTop.preimage_coe_Ioi, WithTop.range_coe
-- Module: Mathlib.Order.Interval.Set.WithBotTop
Goal:
α : Type u_1
inst : Preorder α
a : α
rw : some '' some ⁻¹' Ici (↑a : WithTop α) = Ico (↑a : WithTop α) ⊤
rw₁ : Ici (↑a : WithTop α) ∩ range some = Ico (↑a : WithTop α) ⊤
rw₂ : Ici (↑a : WithTop α) ∩ Iio ⊤ = Ico (↑a : WithTop α) ⊤
rw₃ rw₄ : Ico (↑a : WithTop α) ⊤ = Ico (↑a : WithTop α) ⊤
⊢ some '' Ici a = Ico (↑a : WithTop α) ⊤

Tactic:
rw [← preimage_coe_Ici, image_preimage_eq_inter_range, range_coe, Ici_inter_Iio]

Premises used: Set.Ici_inter_Iio, WithTop.preimage_coe_Ici, Set.image_preimage_eq_inter_range, WithTop.range_coe
-- Module: Mathlib.Order.Interval.Set.WithBotTop
Goal:
α : Type u_1
inst : Preorder α
a : α
rw : some '' some ⁻¹' Iio (↑a : WithTop α) = Iio (↑a : WithTop α)
rw₁ : Iio (↑a : WithTop α) ∩ range some = Iio (↑a : WithTop α)
rw₂ : Iio (↑a : WithTop α) ∩ Iio ⊤ = Iio (↑a : WithTop α)
rw₃ rw₄ : Iio (↑a : WithTop α) = Iio (↑a : WithTop α)
⊢ some '' Iio a = Iio (↑a : WithTop α)

Tactic:
rw [← preimage_coe_Iio, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Iio_subset_Iio le_top)]

Premises used: WithTop.preimage_coe_Iio, Set.image_preimage_eq_inter_range, Set.Iio_subset_Iio, le_top, WithTop.range_coe, Set.inter_eq_self_of_subset_left
-- Module: Mathlib.Order.Interval.Set.WithBotTop
Goal:
α : Type u_1
inst : Preorder α
a : α
rw : some '' some ⁻¹' Iic (↑a : WithTop α) = Iic (↑a : WithTop α)
rw₁ : Iic (↑a : WithTop α) ∩ range some = Iic (↑a : WithTop α)
rw₂ : Iic (↑a : WithTop α) ∩ Iio ⊤ = Iic (↑a : WithTop α)
rw₃ rw₄ : Iic (↑a : WithTop α) = Iic (↑a : WithTop α)
⊢ some '' Iic a = Iic (↑a : WithTop α)

Tactic:
rw [← preimage_coe_Iic, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Iic_subset_Iio.2 <| coe_lt_top a)]

Premises used: Iff.mpr, WithTop.coe_lt_top, Set.Iic_subset_Iio, Set.image_preimage_eq_inter_range, WithTop.preimage_coe_Iic, WithTop.range_coe, Set.inter_eq_self_of_subset_left
-- Module: Mathlib.Order.Interval.Set.WithBotTop
Goal:
α : Type u_1
inst : Preorder α
a b : α
rw : some '' some ⁻¹' Icc (↑a : WithTop α) (↑b : WithTop α) = Icc (↑a : WithTop α) (↑b : WithTop α)
rw₁ : Icc (↑a : WithTop α) (↑b : WithTop α) ∩ range some = Icc (↑a : WithTop α) (↑b : WithTop α)
rw₂ : Icc (↑a : WithTop α) (↑b : WithTop α) ∩ Iio ⊤ = Icc (↑a : WithTop α) (↑b : WithTop α)
rw₃ rw₄ : Icc (↑a : WithTop α) (↑b : WithTop α) = Icc (↑a : WithTop α) (↑b : WithTop α)
⊢ some '' Icc a b = Icc (↑a : WithTop α) (↑b : WithTop α)

Tactic:
rw [← preimage_coe_Icc, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left
      (Subset.trans Icc_subset_Iic_self <| Iic_subset_Iio.2 <| coe_lt_top b)]

Premises used: Iff.mpr, WithTop.coe_lt_top, Set.Subset.trans, Set.Icc_subset_Iic_self, Set.Iic_subset_Iio, Set.image_preimage_eq_inter_range, WithTop.preimage_coe_Icc, WithTop.range_coe, Set.inter_eq_self_of_subset_left
-- Module: Mathlib.Order.Interval.Set.WithBotTop
Goal:
α : Type u_1
inst : Preorder α
a b : α
rw : some '' some ⁻¹' Ico (↑a : WithTop α) (↑b : WithTop α) = Ico (↑a : WithTop α) (↑b : WithTop α)
rw₁ : Ico (↑a : WithTop α) (↑b : WithTop α) ∩ range some = Ico (↑a : WithTop α) (↑b : WithTop α)
rw₂ : Ico (↑a : WithTop α) (↑b : WithTop α) ∩ Iio ⊤ = Ico (↑a : WithTop α) (↑b : WithTop α)
rw₃ rw₄ : Ico (↑a : WithTop α) (↑b : WithTop α) = Ico (↑a : WithTop α) (↑b : WithTop α)
⊢ some '' Ico a b = Ico (↑a : WithTop α) (↑b : WithTop α)

Tactic:
rw [← preimage_coe_Ico, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Subset.trans Ico_subset_Iio_self <| Iio_subset_Iio le_top)]

Premises used: Set.Ico_subset_Iio_self, Set.Subset.trans, WithTop.preimage_coe_Ico, Set.image_preimage_eq_inter_range, Set.Iio_subset_Iio, le_top, WithTop.range_coe, Set.inter_eq_self_of_subset_left
-- Module: Mathlib.Order.Interval.Set.WithBotTop
Goal:
α : Type u_1
inst : Preorder α
a b : α
rw : some '' some ⁻¹' Ioc (↑a : WithTop α) (↑b : WithTop α) = Ioc (↑a : WithTop α) (↑b : WithTop α)
rw₁ : Ioc (↑a : WithTop α) (↑b : WithTop α) ∩ range some = Ioc (↑a : WithTop α) (↑b : WithTop α)
rw₂ : Ioc (↑a : WithTop α) (↑b : WithTop α) ∩ Iio ⊤ = Ioc (↑a : WithTop α) (↑b : WithTop α)
rw₃ rw₄ : Ioc (↑a : WithTop α) (↑b : WithTop α) = Ioc (↑a : WithTop α) (↑b : WithTop α)
⊢ some '' Ioc a b = Ioc (↑a : WithTop α) (↑b : WithTop α)

Tactic:
rw [← preimage_coe_Ioc, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left
      (Subset.trans Ioc_subset_Iic_self <| Iic_subset_Iio.2 <| coe_lt_top b)]

Premises used: Iff.mpr, WithTop.coe_lt_top, Set.Subset.trans, WithTop.preimage_coe_Ioc, Set.Iic_subset_Iio, Set.Ioc_subset_Iic_self, Set.image_preimage_eq_inter_range, WithTop.range_coe, Set.inter_eq_self_of_subset_left
-- Module: Mathlib.Order.Interval.Set.WithBotTop
Goal:
α : Type u_1
inst : Preorder α
a b : α
rw : some '' some ⁻¹' Ioo (↑a : WithTop α) (↑b : WithTop α) = Ioo (↑a : WithTop α) (↑b : WithTop α)
rw₁ : Ioo (↑a : WithTop α) (↑b : WithTop α) ∩ range some = Ioo (↑a : WithTop α) (↑b : WithTop α)
rw₂ : Ioo (↑a : WithTop α) (↑b : WithTop α) ∩ Iio ⊤ = Ioo (↑a : WithTop α) (↑b : WithTop α)
rw₃ rw₄ : Ioo (↑a : WithTop α) (↑b : WithTop α) = Ioo (↑a : WithTop α) (↑b : WithTop α)
⊢ some '' Ioo a b = Ioo (↑a : WithTop α) (↑b : WithTop α)

Tactic:
rw [← preimage_coe_Ioo, image_preimage_eq_inter_range, range_coe,
    inter_eq_self_of_subset_left (Subset.trans Ioo_subset_Iio_self <| Iio_subset_Iio le_top)]

Premises used: Set.Subset.trans, Set.image_preimage_eq_inter_range, Set.Ioo_subset_Iio_self, Set.Iio_subset_Iio, WithTop.preimage_coe_Ioo, le_top, WithTop.range_coe, Set.inter_eq_self_of_subset_left
-- Module: Mathlib.Order.Interval.Set.WithBotTop
Goal:
α : Type u_1
inst : Preorder α
a : α
h : ∀ (x : WithTop α), x ∈ Ioi (↑a : WithTop α) ↔ x ∈ some '' Ioi a ∪ {⊤}
⊢ Ioi (↑a : WithTop α) = some '' Ioi a ∪ {⊤}

Tactic:
ext x
-- Module: Mathlib.Order.Interval.Set.WithBotTop
Goal:
α : Type u_1
inst : Preorder α
a : α
x : WithTop α
h : ⊤ ∈ Ioi (↑a : WithTop α) ↔ ⊤ ∈ some '' Ioi a ∪ {⊤}
h₁ : ∀ (a_1 : α), (↑a_1 : WithTop α) ∈ Ioi (↑a : WithTop α) ↔ (↑a_1 : WithTop α) ∈ some '' Ioi a ∪ {⊤}
⊢ x ∈ Ioi (↑a : WithTop α) ↔ x ∈ some '' Ioi a ∪ {⊤}

Tactic:
induction x
-- Module: Mathlib.Order.Interval.Set.WithBotTop
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ ⊤ ∈ Ioi (↑a : WithTop α) ↔ ⊤ ∈ some '' Ioi a ∪ {⊤}

Tactic:
simp
-- Module: Mathlib.Order.Interval.Set.WithBotTop
Goal:
α : Type u_1
inst : Preorder α
a a_1 : α
⊢ (↑a_1 : WithTop α) ∈ Ioi (↑a : WithTop α) ↔ (↑a_1 : WithTop α) ∈ some '' Ioi a ∪ {⊤}

Tactic:
simp
-- Module: Mathlib.Order.Interval.Set.WithBotTop
Goal:
α : Type u_1
inst : Preorder α
a : α
h : ∀ (x : WithTop α), x ∈ Ici (↑a : WithTop α) ↔ x ∈ some '' Ici a ∪ {⊤}
⊢ Ici (↑a : WithTop α) = some '' Ici a ∪ {⊤}

Tactic:
ext x
-- Module: Mathlib.Order.Interval.Set.WithBotTop
Goal:
α : Type u_1
inst : Preorder α
a : α
x : WithTop α
h : ⊤ ∈ Ici (↑a : WithTop α) ↔ ⊤ ∈ some '' Ici a ∪ {⊤}
h₁ : ∀ (a_1 : α), (↑a_1 : WithTop α) ∈ Ici (↑a : WithTop α) ↔ (↑a_1 : WithTop α) ∈ some '' Ici a ∪ {⊤}
⊢ x ∈ Ici (↑a : WithTop α) ↔ x ∈ some '' Ici a ∪ {⊤}

Tactic:
induction x
-- Module: Mathlib.Order.Interval.Set.WithBotTop
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ ⊤ ∈ Ici (↑a : WithTop α) ↔ ⊤ ∈ some '' Ici a ∪ {⊤}

Tactic:
simp
-- Module: Mathlib.Order.Interval.Set.WithBotTop
Goal:
α : Type u_1
inst : Preorder α
a a_1 : α
⊢ (↑a_1 : WithTop α) ∈ Ici (↑a : WithTop α) ↔ (↑a_1 : WithTop α) ∈ some '' Ici a ∪ {⊤}

Tactic:
simp
-- Module: Mathlib.Order.Interval.Set.WithBotTop
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ Iio (↑a : WithTop α) = some '' Iio a

Tactic:
image_coe_Iio.symm

Premises used: WithTop.image_coe_Iio, Eq.symm
-- Module: Mathlib.Order.Interval.Set.WithBotTop
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ Iic (↑a : WithTop α) = some '' Iic a

Tactic:
image_coe_Iic.symm

Premises used: WithTop.image_coe_Iic, Eq.symm
-- Module: Mathlib.Order.Interval.Set.WithBotTop
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Icc (↑a : WithTop α) (↑b : WithTop α) = some '' Icc a b

Tactic:
image_coe_Icc.symm

Premises used: Eq.symm, WithTop.image_coe_Icc
-- Module: Mathlib.Order.Interval.Set.WithBotTop
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Ico (↑a : WithTop α) (↑b : WithTop α) = some '' Ico a b

Tactic:
image_coe_Ico.symm

Premises used: WithTop.image_coe_Ico, Eq.symm
-- Module: Mathlib.Order.Interval.Set.WithBotTop
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Ioc (↑a : WithTop α) (↑b : WithTop α) = some '' Ioc a b

Tactic:
image_coe_Ioc.symm

Premises used: WithTop.image_coe_Ioc, Eq.symm
-- Module: Mathlib.Order.Interval.Set.WithBotTop
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Ioo (↑a : WithTop α) (↑b : WithTop α) = some '' Ioo a b

Tactic:
image_coe_Ioo.symm

Premises used: WithTop.image_coe_Ioo, Eq.symm
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeSup α
a : α
ha : SupIrred a
⊢ ¬IsMin a

Tactic:
ha.1

Premises used: And.left
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeSup α
a : α
ha : SupPrime a
⊢ ¬IsMin a

Tactic:
ha.1

Premises used: And.left
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeSup α
a : α
ha : IsMin a
⊢ ¬SupIrred a

Tactic:
fun h => h.1 ha

Premises used: And.left, Not
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeSup α
a : α
ha : IsMin a
⊢ ¬SupPrime a

Tactic:
fun h => h.1 ha

Premises used: And.left, Not
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeSup α
a : α
rw : (¬¬IsMin a ∨ ¬∀ ⦃b c : α⦄, b ⊔ c = a → b = a ∨ c = a) ↔ IsMin a ∨ ∃ (b : α) (c : α), b ⊔ c = a ∧ b < a ∧ c < a
⊢ ¬SupIrred a ↔ IsMin a ∨ ∃ (b : α) (c : α), b ⊔ c = a ∧ b < a ∧ c < a

Tactic:
rw [SupIrred, not_and_or]

Premises used: not_and_or, SupIrred
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeSup α
a : α
push : (IsMin a ∨ ∃ (b : α) (c : α), b ⊔ c = a ∧ b ≠ a ∧ c ≠ a) ↔ IsMin a ∨ ∃ (b : α) (c : α), b ⊔ c = a ∧ b < a ∧ c < a
⊢ (¬¬IsMin a ∨ ¬∀ ⦃b c : α⦄, b ⊔ c = a → b = a ∨ c = a) ↔ IsMin a ∨ ∃ (b : α) (c : α), b ⊔ c = a ∧ b < a ∧ c < a

Tactic:
push Not

Premises used: Not
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeSup α
a : α
rw : ∀ (a_1 b : α), a_1 ⊔ b = a ∧ a_1 ≠ a ∧ b ≠ a ↔ a_1 ⊔ b = a ∧ a_1 < a ∧ b < a
⊢ (IsMin a ∨ ∃ (b : α) (c : α), b ⊔ c = a ∧ b ≠ a ∧ c ≠ a) ↔ IsMin a ∨ ∃ (b : α) (c : α), b ⊔ c = a ∧ b < a ∧ c < a

Tactic:
rw [exists₂_congr]

Premises used: exists₂_congr
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeSup α
a : α
⊢ ∀ (a_1 b : α), a_1 ⊔ b = a ∧ a_1 ≠ a ∧ b ≠ a ↔ a_1 ⊔ b = a ∧ a_1 < a ∧ b < a

Tactic:
simp +contextual [@eq_comm _ _ a]

Premises used: eq_comm
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeSup α
a : α
rw : (¬¬IsMin a ∨ ¬∀ ⦃b c : α⦄, a ≤ b ⊔ c → a ≤ b ∨ a ≤ c) ↔ IsMin a ∨ ∃ (b : α) (c : α), a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c
⊢ ¬SupPrime a ↔ IsMin a ∨ ∃ (b : α) (c : α), a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c

Tactic:
rw [SupPrime, not_and_or]

Premises used: SupPrime, not_and_or
-- Module: Mathlib.Order.Irreducible
Goal:
α : Type u_2
inst : SemilatticeSup α
a : α
push :
  (IsMin a ∨ ∃ (b : α) (c : α), a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c) ↔ IsMin a ∨ ∃ (b : α) (c : α), a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c
⊢ (¬¬IsMin a ∨ ¬∀ ⦃b c : α⦄, a ≤ b ⊔ c → a ≤ b ∨ a ≤ c) ↔ IsMin a ∨ ∃ (b : α) (c : α), a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c

Tactic:
push Not

Premises used: Not