awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Atoms.Finite
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
hab : a < b
⊢ b ∈ @LocallyFiniteOrder.finsetIoc _ inst _ a b

Tactic:
simpa [LocallyFiniteOrder.finset_mem_Ioc]

Premises used: LocallyFiniteOrder.finset_mem_Ioc
-- Module: Mathlib.Order.Atoms.Finite
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
hab : a < b
obtain :
  ∀ (x : α) (hx : x ∈ @LocallyFiniteOrder.finsetIoc _ inst _ a b)
    (hxmin : ∀ ⦃y : α⦄, (fun (x : α) ↦ x ∈ @LocallyFiniteOrder.finsetIoc _ inst _ a b) y → y ≤ x → x ≤ y),
    ∃ (x : α), a ⋖ x ∧ x ≤ b
⊢ ∃ (x : α), a ⋖ x ∧ x ≤ b

Tactic:
obtain ⟨x, hx, hxmin⟩ := (LocallyFiniteOrder.finsetIoc a b).exists_minimal
      ⟨b, by simpa [LocallyFiniteOrder.finset_mem_Ioc]⟩

Premises used: Finset.exists_minimal, Exists.intro
-- Module: Mathlib.Order.Atoms.Finite
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
hab : a < b
x : α
hx : x ∈ @LocallyFiniteOrder.finsetIoc _ inst _ a b
hxmin : ∀ ⦃y : α⦄, (fun (x : α) ↦ x ∈ @LocallyFiniteOrder.finsetIoc _ inst _ a b) y → y ≤ x → x ≤ y
⊢ a < x ∧ x ≤ b

Tactic:
simp only [LocallyFiniteOrder.finset_mem_Ioc] at hx hxmin

Premises used: LocallyFiniteOrder.finset_mem_Ioc
-- Module: Mathlib.Order.Atoms.Finite
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
hab : a < b
x : α
hx : x ∈ @LocallyFiniteOrder.finsetIoc _ inst _ a b
hxmin : ∀ ⦃y : α⦄, (fun (x : α) ↦ x ∈ @LocallyFiniteOrder.finsetIoc _ inst _ a b) y → y ≤ x → x ≤ y
hx₁ : a < x ∧ x ≤ b
⊢ ∀ ⦃y : α⦄, a < y ∧ y ≤ b → y ≤ x → x ≤ y

Tactic:
simp only [LocallyFiniteOrder.finset_mem_Ioc] at hx hxmin

Premises used: LocallyFiniteOrder.finset_mem_Ioc
-- Module: Mathlib.Order.Atoms.Finite
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
hab : a < b
x : α
hx : a < x ∧ x ≤ b
hxmin : ∀ ⦃y : α⦄, a < y ∧ y ≤ b → y ≤ x → x ≤ y
⊢ ∃ (x : α), a ⋖ x ∧ x ≤ b

Tactic:
⟨x, ⟨hx.1, fun c hac hcx ↦ hcx.not_ge <| hxmin ⟨hac, hcx.le.trans hx.2⟩ hcx.le⟩, hx.2⟩

Premises used: LT.lt.le, And.right, And.left, And.intro, Exists.intro, LE.le.trans, LT.lt.not_ge
-- Module: Mathlib.Order.Atoms.Finite
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a b : α
hab : a < b
x : α
hx : a < x ∧ x ≤ b
hxmin : ∀ ⦃y : α⦄, a < y ∧ y ≤ b → y ≤ x → x ≤ y
⊢ ∃ (x : α), a ⋖ x ∧ x ≤ b

Tactic:
exact ⟨x, ⟨hx.1, fun c hac hcx ↦ hcx.not_ge <| hxmin ⟨hac, hcx.le.trans hx.2⟩ hcx.le⟩, hx.2⟩
-- Module: Mathlib.Order.Atoms.Finite
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
rw : IsStronglyAtomic.{u_1} αᵒᵈ
⊢ IsStronglyCoatomic α

Tactic:
rw [← isStronglyAtomic_dual_iff_is_stronglyCoatomic]

Premises used: isStronglyAtomic_dual_iff_is_stronglyCoatomic
-- Module: Mathlib.Order.Atoms.Finite
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
⊢ IsStronglyAtomic.{u_1} αᵒᵈ

Tactic:
infer_instance
-- Module: Mathlib.Order.Atoms.Finite
Goal:
α : Type u_1
inst : PartialOrder α
a : α
inst_1 : IsStronglyAtomic α
ha : (Set.Ici a).Infinite
hfin : Set.Finite.{u_1} (α := α) {x : α | a ⋖ x}
by_contra! : ∀ (h : ∀ (b : α) (_ : a ⋖ b), (Set.Ici b).Finite), False
⊢ ∃ (b : α), a ⋖ b ∧ (Set.Ici b).Infinite

Tactic:
by_contra! h
-- Module: Mathlib.Order.Atoms.Finite
Goal:
α : Type u_1
inst : PartialOrder α
a : α
inst_1 : IsStronglyAtomic α
ha : (Set.Ici a).Infinite
hfin : Set.Finite.{u_1} (α := α) {x : α | a ⋖ x}
h : ∀ (b : α) (_ : a ⋖ b), (Set.Ici b).Finite
⊢ ∀ (i : α), Membership.mem (γ := Set α) {x : α | a ⋖ x} i → (Set.Ici i).Finite

Tactic:
simpa using h
-- Module: Mathlib.Order.Atoms.Finite
Goal:
α : Type u_1
inst : PartialOrder α
a : α
inst_1 : IsStronglyAtomic α
ha : (Set.Ici a).Infinite
hfin : Set.Finite.{u_1} (α := α) {x : α | a ⋖ x}
h : ∀ (b : α) (_ : a ⋖ b), (Set.Ici b).Finite
refine :
  ∀ (b : α) (hb : b ∈ Set.Ici a \ {a}),
    Membership.mem (γ := Set α) (⋃ (i : α), ⋃ (_ : Membership.mem (γ := Set α) {x : α | a ⋖ x} i), Set.Ici i) b
⊢ False

Tactic:
refine ((hfin.biUnion (t := Set.Ici) (by simpa using h)).subset (fun b hb ↦ ?_)).not_infinite
    (ha.diff (Set.finite_singleton a))

Premises used: Set.Finite.not_infinite, Set.Finite.subset, Set.Finite.biUnion, Set.finite_singleton, Set.Infinite.diff
-- Module: Mathlib.Order.Atoms.Finite
Goal:
α : Type u_1
inst : PartialOrder α
a : α
inst_1 : IsStronglyAtomic α
ha : (Set.Ici a).Infinite
hfin : Set.Finite.{u_1} (α := α) {x : α | a ⋖ x}
h : ∀ (b : α) (_ : a ⋖ b), (Set.Ici b).Finite
b : α
hb : b ∈ Set.Ici a \ {a}
obtain :
  ∀ (x : α) (hax : a ⋖ x) (hxb : x ≤ b),
    Membership.mem (γ := Set α) (⋃ (i : α), ⋃ (_ : Membership.mem (γ := Set α) {x : α | a ⋖ x} i), Set.Ici i) b
⊢ Membership.mem (γ := Set α) (⋃ (i : α), ⋃ (_ : Membership.mem (γ := Set α) {x : α | a ⋖ x} i), Set.Ici i) b

Tactic:
obtain ⟨x, hax, hxb⟩ := ((show a ≤ b from hb.1).lt_of_ne (Ne.symm hb.2)).exists_covby_le

Premises used: Ne.symm, LT.lt.exists_covby_le, LE.le.lt_of_ne, And.right, And.left
-- Module: Mathlib.Order.Atoms.Finite
Goal:
α : Type u_1
inst : PartialOrder α
a : α
inst_1 : IsStronglyAtomic α
ha : (Set.Ici a).Infinite
hfin : Set.Finite.{u_1} (α := α) {x : α | a ⋖ x}
h : ∀ (b : α) (_ : a ⋖ b), (Set.Ici b).Finite
b : α
hb : b ∈ Set.Ici a \ {a}
x : α
hax : a ⋖ x
hxb : x ≤ b
⊢ Membership.mem (γ := Set α) (⋃ (i : α), ⋃ (_ : Membership.mem (γ := Set α) {x : α | a ⋖ x} i), Set.Ici i) b

Tactic:
Set.mem_biUnion hax hxb

Premises used: Set.mem_biUnion
-- Module: Mathlib.Order.Atoms.Finite
Goal:
α : Type u_1
inst : PartialOrder α
a : α
inst_1 : IsStronglyAtomic α
ha : (Set.Ici a).Infinite
hfin : Set.Finite.{u_1} (α := α) {x : α | a ⋖ x}
h : ∀ (b : α) (_ : a ⋖ b), (Set.Ici b).Finite
b : α
hb : b ∈ Set.Ici a \ {a}
x : α
hax : a ⋖ x
hxb : x ≤ b
⊢ Membership.mem (γ := Set α) (⋃ (i : α), ⋃ (_ : Membership.mem (γ := Set α) {x : α | a ⋖ x} i), Set.Ici i) b

Tactic:
exact Set.mem_biUnion hax hxb

Premises used: Set.mem_biUnion
-- Module: Mathlib.Order.Atoms.Finite
Goal:
α : Type u_1
inst : PartialOrder α
a : α
inst_1 : IsStronglyCoatomic α
ha : (Set.Iic a).Infinite
hfin : Set.Finite.{u_1} (α := α) {x : α | x ⋖ a}
simp_rw :
  ∀
    (hfin :
      Set.Finite.{u_1} (α := α)
        {x : α |
          CovBy (α := αᵒᵈ) ((OrderDual.toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((OrderDual.toDual : (a : α) → αᵒᵈ) x : αᵒᵈ)}),
    ∃ (b : α),
      CovBy (α := αᵒᵈ) ((OrderDual.toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((OrderDual.toDual : (a : α) → αᵒᵈ) b : αᵒᵈ) ∧
        (Set.Iic b).Infinite
⊢ ∃ (b : α), b ⋖ a ∧ (Set.Iic b).Infinite

Tactic:
simp_rw [← toDual_covBy_toDual_iff (α := α)] at hfin ⊢

Premises used: toDual_covBy_toDual_iff
-- Module: Mathlib.Order.Atoms.Finite
Goal:
α : Type u_1
inst : PartialOrder α
a : α
inst_1 : IsStronglyCoatomic α
ha : (Set.Iic a).Infinite
hfin :
  Set.Finite.{u_1} (α := α)
    {x : α | CovBy (α := αᵒᵈ) ((OrderDual.toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((OrderDual.toDual : (a : α) → αᵒᵈ) x : αᵒᵈ)}
⊢ ∃ (b : α),
    CovBy (α := αᵒᵈ) ((OrderDual.toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((OrderDual.toDual : (a : α) → αᵒᵈ) b : αᵒᵈ) ∧
      (Set.Iic b).Infinite

Tactic:
exists_covby_infinite_Ici_of_infinite_Ici (α := αᵒᵈ) ha hfin

Premises used: setOf, exists_covby_infinite_Ici_of_infinite_Ici, Set.Iic, OrderDual
-- Module: Mathlib.Order.Atoms.Finite
Goal:
α : Type u_1
inst : PartialOrder α
a : α
inst_1 : IsStronglyCoatomic α
ha : (Set.Iic a).Infinite
hfin :
  Set.Finite.{u_1} (α := α)
    {x : α | CovBy (α := αᵒᵈ) ((OrderDual.toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((OrderDual.toDual : (a : α) → αᵒᵈ) x : αᵒᵈ)}
⊢ ∃ (b : α),
    CovBy (α := αᵒᵈ) ((OrderDual.toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((OrderDual.toDual : (a : α) → αᵒᵈ) b : αᵒᵈ) ∧
      (Set.Iic b).Infinite

Tactic:
exact exists_covby_infinite_Ici_of_infinite_Ici (α := αᵒᵈ) ha hfin

Premises used: exists_covby_infinite_Ici_of_infinite_Ici
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Preorder α
inst_1 : OrderBot α
a x : α
ha : IsAtom a
hax : a ≤ x
⊢ IsAtom (α := { x_1 : α // x_1 ∈ Set.Iic x }) (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Set.Iic x) a hax)

Tactic:
⟨fun con => ha.1 (Subtype.mk_eq_mk.1 con), fun ⟨b, _⟩ hba => Subtype.mk_eq_mk.2 (ha.2 b hba)⟩

Premises used: Iff.mpr, _private.0.IsAtom.Iic.match_1, Bot.bot, And.right, And.left, And.intro, Subtype.mk_eq_mk, Iff.mp, IsAtom, Eq
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Preorder α
inst_1 : OrderBot α
x : α
a : (↑(Set.Iic x) : Type u_2)
ha : IsAtom a
⊢ IsAtom (↑a : α)

Tactic:
⟨fun con => ha.1 (Subtype.ext con), fun b hba =>
    Subtype.mk_eq_mk.1 (ha.2 ⟨b, hba.le.trans a.prop⟩ hba)⟩

Premises used: LT.lt.le, Subtype.mk, And.right, And.left, Subtype.prop, And.intro, Subtype.mk_eq_mk, Iff.mp, IsAtom, LE.le.trans, Subtype.ext
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Preorder α
inst_1 : OrderBot α
a b : α
⊢ b < a → b = ⊥ ↔ b ≠ ⊥ → b ≤ a → a ≤ b

Tactic:
simp only [Ne, @not_imp_comm (b = ⊥), Classical.not_imp, lt_iff_le_not_ge]

Premises used: lt_iff_le_not_ge, not_imp_comm, Ne, Classical.not_imp
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Preorder α
inst_1 : OrderBot α
a : α
ha : IsAtom a
⊢ a ≠ ⊥

Tactic:
ha.1

Premises used: And.left
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderBot α
a x : α
h : IsAtom a
⊢ x < a ↔ x = ⊥

Tactic:
⟨h.2 x, fun hx => hx.symm ▸ h.1.bot_lt⟩

Premises used: Eq.rec, And.right, And.left, Iff.intro, Eq.symm, Ne.bot_lt
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderBot α
a x : α
h : IsAtom a
rw : x < a ∨ x = a ↔ x = ⊥ ∨ x = a
rw₁ rw₂ : x = ⊥ ∨ x = a ↔ x = ⊥ ∨ x = a
⊢ x ≤ a ↔ x = ⊥ ∨ x = a

Tactic:
rw [le_iff_lt_or_eq, h.lt_iff]

Premises used: IsAtom.lt_iff, le_iff_lt_or_eq
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderBot α
a : α
h : IsAtom a
⊢ ⊥ < a

Tactic:
h.lt_iff.mpr rfl

Premises used: IsAtom.lt_iff, Iff.mpr, rfl
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderBot α
a b : α
ha : IsAtom a
hb : b ≠ ⊥
⊢ b ≤ a ↔ b = a

Tactic:
ha.le_iff.trans <| or_iff_right hb

Premises used: IsAtom.le_iff, or_iff_right, Iff.trans
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderBot α
a : α
ha : IsAtom a
hba : ⊥ ≤ a
⊢ ⊥ ≠ a

Tactic:
ha.ne_bot.symm

Premises used: Ne.symm, IsAtom.ne_bot
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderBot α
a : α
ha : IsAtom a
hba : ⊥ ≤ a
⊢ ⊥ ≠ a

Tactic:
exact ha.ne_bot.symm

Premises used: Ne.symm, IsAtom.ne_bot
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderBot α
a b : α
ha : IsAtom a
hba : b ≤ a
⊢ b ≠ ⊥ ↔ b = a

Tactic:
(ha.ne_iff_eq_bot hba).not_right.symm

Premises used: Iff.not_right, IsAtom.ne_iff_eq_bot, Iff.symm
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderBot α
a : α
h : IsAtom a
⊢ Set.Iic a = {⊥, a}

Tactic:
Set.ext fun _ => h.le_iff

Premises used: Set.ext, IsAtom.le_iff
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderBot α
a : α
⊢ ⊥ ⋖ a ↔ IsAtom a

Tactic:
simp only [CovBy, bot_lt_iff_ne_bot, IsAtom, not_imp_not]

Premises used: CovBy, bot_lt_iff_ne_bot, IsAtom, not_imp_not
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
inst : Frame α
f : ι → α
a : α
ha : IsAtom a
⊢ a ≤ iSup f ↔ ∃ (i : ι), a ≤ f i

Tactic:
⟨?_, fun ⟨i, hi⟩ => le_trans hi (le_iSup _ _)⟩

Premises used: iSup, _private.0.IsAtom.le_iSup.match_1, le_iSup, LE.le, Iff.intro, le_trans
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
inst : Frame α
f : ι → α
a : α
ha : IsAtom a
refine : a ≤ iSup f → ∃ (i : ι), a ≤ f i
⊢ a ≤ iSup f ↔ ∃ (i : ι), a ≤ f i

Tactic:
refine ⟨?_, fun ⟨i, hi⟩ => le_trans hi (le_iSup _ _)⟩
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
inst : Frame α
f : ι → α
a : α
ha : IsAtom a
change : a ≤ ⨆ (i : ι), f i → ∃ (i : ι), a ≤ f i
⊢ a ≤ iSup f → ∃ (i : ι), a ≤ f i

Tactic:
change (a ≤ ⨆ i, f i) → _
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
inst : Frame α
f : ι → α
a : α
ha : IsAtom a
⊢ a ≤ ⨆ (i : ι), f i → ∃ (i : ι), a ≤ f i

Tactic:
fun h => of_not_not fun ha' => ?_

Premises used: of_not_not
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
inst : Frame α
f : ι → α
a : α
ha : IsAtom a
refine : ∀ (h : a ≤ ⨆ (i : ι), f i) (ha' : ¬∃ (i : ι), a ≤ f i), False
⊢ a ≤ ⨆ (i : ι), f i → ∃ (i : ι), a ≤ f i

Tactic:
refine fun h => of_not_not fun ha' => ?_

Premises used: of_not_not
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
inst : Frame α
f : ι → α
a : α
ha : IsAtom a
h : a ≤ ⨆ (i : ι), f i
ha' : ¬∃ (i : ι), a ≤ f i
⊢ ∀ (i : ι), ¬a ≤ f i

Tactic:
push Not at ha'

Premises used: Not
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
inst : Frame α
f : ι → α
i : ι
x : α
hxf : x ≤ f i
hx : ¬x = ⊥
ha : IsAtom x
h : x ≤ ⨆ (i : ι), f i
ha' : ∀ (i : ι), ¬x ≤ f i
hxa : x ≤ x
⊢ False

Tactic:
ha' _ hxf
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
inst : Frame α
f : ι → α
i : ι
x : α
hxf : x ≤ f i
hx : ¬x = ⊥
ha : IsAtom x
h : x ≤ ⨆ (i : ι), f i
ha' : ∀ (i : ι), ¬x ≤ f i
hxa : x ≤ x
⊢ False

Tactic:
exact ha' _ hxf
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
inst : Frame α
f : ι → α
a : α
ha : IsAtom a
h : a ≤ ⨆ (i : ι), f i
ha' : ∀ (i : ι), ¬a ≤ f i
⊢ Disjoint a (⨆ (i : ι), f i)

Tactic:
have ha'' : Disjoint a (⨆ i, f i) :=
    disjoint_iSup_iff.2 fun i => fun x hxa hxf => le_bot_iff.2 <| of_not_not fun hx =>
      have hxa : x < a := (le_iff_eq_or_lt.1 hxa).resolve_left (by rintro rfl; exact ha' _ hxf)
      hx (ha.2 _ hxa)
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
inst : Frame α
f : ι → α
a : α
ha : IsAtom a
h : a ≤ ⨆ (i : ι), f i
ha' : ∀ (i : ι), ¬a ≤ f i
ha'' : Disjoint a (⨆ (i : ι), f i)
⊢ IsAtom.{u_2} (α := α) ⊥

Tactic:
obtain rfl := le_bot_iff.1 (ha'' le_rfl h)

Premises used: le_bot_iff, le_rfl, Iff.mp, rfl
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
inst : Frame α
f : ι → α
a : α
ha : IsAtom a
h : a ≤ ⨆ (i : ι), f i
ha' : ∀ (i : ι), ¬a ≤ f i
ha'' : Disjoint a (⨆ (i : ι), f i)
ha₁ : IsAtom.{u_2} (α := α) ⊥
⊢ LE.le.{u_2} (α := α) ⊥ (⨆ (i : ι), f i)

Tactic:
obtain rfl := le_bot_iff.1 (ha'' le_rfl h)

Premises used: le_bot_iff, le_rfl, Iff.mp, rfl
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
inst : Frame α
f : ι → α
a : α
ha : IsAtom a
h : a ≤ ⨆ (i : ι), f i
ha' : ∀ (i : ι), ¬a ≤ f i
ha'' : Disjoint a (⨆ (i : ι), f i)
ha₁ : IsAtom.{u_2} (α := α) ⊥
h₁ : LE.le.{u_2} (α := α) ⊥ (⨆ (i : ι), f i)
⊢ ∀ (i : ι), ¬⊥ ≤ f i

Tactic:
obtain rfl := le_bot_iff.1 (ha'' le_rfl h)

Premises used: le_bot_iff, le_rfl, Iff.mp, rfl
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
inst : Frame α
f : ι → α
a : α
ha : IsAtom a
h : a ≤ ⨆ (i : ι), f i
ha' : ∀ (i : ι), ¬a ≤ f i
ha'' : Disjoint a (⨆ (i : ι), f i)
ha₁ : IsAtom.{u_2} (α := α) ⊥
h₁ : LE.le.{u_2} (α := α) ⊥ (⨆ (i : ι), f i)
ha'₁ : ∀ (i : ι), ¬⊥ ≤ f i
⊢ Disjoint.{u_2} (α := α) ⊥ (⨆ (i : ι), f i)

Tactic:
obtain rfl := le_bot_iff.1 (ha'' le_rfl h)

Premises used: le_bot_iff, le_rfl, Iff.mp, rfl
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
inst : Frame α
f : ι → α
ha : IsAtom.{u_2} (α := α) ⊥
h : LE.le.{u_2} (α := α) ⊥ (⨆ (i : ι), f i)
ha' : ∀ (i : ι), ¬⊥ ≤ f i
ha'' : Disjoint.{u_2} (α := α) ⊥ (⨆ (i : ι), f i)
⊢ False

Tactic:
ha.1 rfl

Premises used: And.left, rfl
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
inst : Frame α
f : ι → α
ha : IsAtom.{u_2} (α := α) ⊥
h : LE.le.{u_2} (α := α) ⊥ (⨆ (i : ι), f i)
ha' : ∀ (i : ι), ¬⊥ ≤ f i
ha'' : Disjoint.{u_2} (α := α) ⊥ (⨆ (i : ι), f i)
⊢ False

Tactic:
exact ha.1 rfl

Premises used: And.left, rfl
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Frame α
s : Set α
a : α
ha : IsAtom a
⊢ a ≤ sSup s ↔ ∃ b ∈ s, a ≤ b

Tactic:
simp [sSup_eq_iSup', ha.le_iSup]

Premises used: IsAtom.le_iSup, sSup_eq_iSup'
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Preorder α
inst_1 : OrderBot α
a : α
⊢ IsCoatom (α := αᵒᵈ) ((OrderDual.toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ↔ IsAtom a

Tactic:
Iff.rfl

Premises used: Iff.rfl, IsAtom, OrderDual
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Preorder α
inst_1 : OrderTop α
a : α
⊢ IsAtom (α := αᵒᵈ) ((OrderDual.toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ↔ IsCoatom a

Tactic:
Iff.rfl

Premises used: Iff.rfl, IsCoatom, OrderDual
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Preorder α
inst_1 : OrderTop α
a x : α
ha : IsCoatom a
hax : x ≤ a
⊢ IsCoatom (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Set.Ici x) a hax)

Tactic:
ha.dual.Iic hax

Premises used: Set.Ici, Set.Mem, setOf, IsAtom.Iic, IsCoatom, OrderDual, IsCoatom.dual
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Preorder α
inst_1 : OrderTop α
x : α
a : (↑(Set.Ici x) : Type u_2)
ha : IsCoatom a
⊢ IsCoatom (↑a : α)

Tactic:
@IsAtom.of_isAtom_coe_Iic αᵒᵈ _ _ x a ha

Premises used: IsAtom.of_isAtom_coe_Iic, IsCoatom, OrderDual
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Preorder α
inst_1 : OrderTop α
a : α
⊢ IsCoatom a ↔ a ≠ ⊤ ∧ ∀ (b : α), b ≠ ⊤ → a ≤ b → b ≤ a

Tactic:
isAtom_iff_le_of_ge (α := αᵒᵈ)

Premises used: IsCoatom, OrderDual, isAtom_iff_le_of_ge
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Preorder α
inst_1 : OrderTop α
a : α
ha : IsCoatom a
⊢ a ≠ ⊤

Tactic:
ha.1

Premises used: And.left
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
a x : α
h : IsCoatom a
⊢ a < x ↔ x = ⊤

Tactic:
h.dual.lt_iff

Premises used: IsAtom.lt_iff, OrderDual, IsCoatom.dual
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
a x : α
h : IsCoatom a
⊢ a ≤ x ↔ x = ⊤ ∨ x = a

Tactic:
h.dual.le_iff

Premises used: IsAtom.le_iff, OrderDual, IsCoatom.dual
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
a : α
h : IsCoatom a
⊢ a < ⊤

Tactic:
h.lt_iff.mpr rfl

Premises used: Iff.mpr, IsCoatom.lt_iff, rfl
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
a b : α
ha : IsCoatom a
hb : b ≠ ⊤
⊢ a ≤ b ↔ b = a

Tactic:
ha.dual.le_iff_eq hb

Premises used: IsAtom.le_iff_eq, OrderDual, IsCoatom.dual
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
a : α
ha : IsCoatom a
hab : a ≤ ⊤
⊢ ⊤ ≠ a

Tactic:
ha.ne_top.symm

Premises used: Ne.symm, IsCoatom.ne_top
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
a : α
ha : IsCoatom a
hab : a ≤ ⊤
⊢ ⊤ ≠ a

Tactic:
exact ha.ne_top.symm

Premises used: Ne.symm, IsCoatom.ne_top
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
a b : α
ha : IsCoatom a
hab : a ≤ b
⊢ b ≠ ⊤ ↔ b = a

Tactic:
(ha.ne_iff_eq_top hab).not_right.symm

Premises used: IsCoatom.ne_iff_eq_top, Iff.not_right, Iff.symm
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
a : α
h : IsCoatom a
⊢ Set.Ici a = {⊤, a}

Tactic:
h.dual.Iic_eq

Premises used: Set.Ici, setOf, IsAtom.Iic_eq, OrderDual, IsCoatom.dual
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
a : α
⊢ a ⋖ ⊤ ↔ IsCoatom a

Tactic:
toDual_covBy_toDual_iff.symm.trans bot_covBy_iff

Premises used: bot_covBy_iff, Iff.trans, Iff.symm, toDual_covBy_toDual_iff
-- Module: Mathlib.Order.Atoms
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
inst_3 : OrderBot A
K : A
simp_rw : (K ≠ ⊥ ∧ ∀ b < K, b = ⊥) ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥
simp_rw₁ : (K ≠ ⊥ ∧ ∀ (b : A), b ≤ K ∧ ¬K ≤ b → b = ⊥) ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥
simp_rw₂ :
  (K ≠ ⊥ ∧ ∀ (b : A), (b ≤ K ∧ ∃ x ∈ K, x ∉ b) → b = ⊥) ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥
simp_rw₃ :
  (K ≠ ⊥ ∧ ∀ (b : A), (∃ x ∈ K, x ∉ b) ∧ b ≤ K → b = ⊥) ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥
simp_rw₄ :
  (K ≠ ⊥ ∧ ∀ (b : A), (∃ x ∈ K, x ∉ b) → b ≤ K → b = ⊥) ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥
simp_rw₅ :
  (K ≠ ⊥ ∧ ∀ (b : A) (x : B), x ∈ K ∧ x ∉ b → b ≤ K → b = ⊥) ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥
simp_rw₆ :
  (K ≠ ⊥ ∧ ∀ (b : A) (x : B), (x ∈ K ∧ x ∉ b) ∧ b ≤ K → b = ⊥) ↔
    K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K ∧ g ∉ H ∧ g ∈ K → H = ⊥
⊢ IsAtom K ↔ K ≠ ⊥ ∧ ∀ (H : A) (g : B), H ≤ K → g ∉ H → g ∈ K → H = ⊥

Tactic:
simp_rw [IsAtom, lt_iff_le_not_ge, SetLike.not_le_iff_exists,
    and_comm (a := _ ≤ _), and_imp, exists_imp, ← and_imp, and_comm]

Premises used: lt_iff_le_not_ge, and_imp, and_comm, IsAtom, SetLike.not_le_iff_exists, exists_imp
-- Module: Mathlib.Order.Atoms
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
inst_3 : OrderTop A
K : A
simp_rw : (K ≠ ⊤ ∧ ∀ (b : A), K < b → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
simp_rw₁ : (K ≠ ⊤ ∧ ∀ (b : A), K ≤ b ∧ ¬b ≤ K → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
simp_rw₂ :
  (K ≠ ⊤ ∧ ∀ (b : A), (K ≤ b ∧ ∃ x ∈ b, x ∉ K) → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
simp_rw₃ :
  (K ≠ ⊤ ∧ ∀ (b : A), (∃ x ∈ b, x ∉ K) ∧ K ≤ b → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
simp_rw₄ :
  (K ≠ ⊤ ∧ ∀ (b : A), (∃ x ∈ b, x ∉ K) → K ≤ b → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
simp_rw₅ :
  (K ≠ ⊤ ∧ ∀ (b : A) (x : B), x ∈ b ∧ x ∉ K → K ≤ b → b = ⊤) ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤
simp_rw₆ :
  (K ≠ ⊤ ∧ ∀ (b : A) (x : B), (x ∈ b ∧ x ∉ K) ∧ K ≤ b → b = ⊤) ↔
    K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H ∧ g ∉ K ∧ g ∈ H → H = ⊤
⊢ IsCoatom K ↔ K ≠ ⊤ ∧ ∀ (H : A) (g : B), K ≤ H → g ∉ K → g ∈ H → H = ⊤

Tactic:
simp_rw [IsCoatom, lt_iff_le_not_ge, SetLike.not_le_iff_exists,
    and_comm (a := _ ≤ _), and_imp, exists_imp, ← and_imp, and_comm]

Premises used: lt_iff_le_not_ge, and_imp, and_comm, IsCoatom, SetLike.not_le_iff_exists, exists_imp
-- Module: Mathlib.Order.Atoms
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
K L : A
⊢ K ⋖ L ↔ K < L ∧ ∀ (H : A) (g : B), K ≤ H → H ≤ L → g ∉ K → g ∈ H → H = L

Tactic:
and_congr_right fun _ ↦ forall_congr' fun H ↦ ?_

Premises used: CovBy, and_congr_right, forall_congr'
-- Module: Mathlib.Order.Atoms
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
K L : A
refine : K < L → ∀ (H : A), K < H → ¬H < L ↔ ∀ (g : B), K ≤ H → H ≤ L → g ∉ K → g ∈ H → H = L
⊢ K ⋖ L ↔ K < L ∧ ∀ (H : A) (g : B), K ≤ H → H ≤ L → g ∉ K → g ∈ H → H = L

Tactic:
refine and_congr_right fun _ ↦ forall_congr' fun H ↦ ?_

Premises used: and_congr_right, forall_congr'
-- Module: Mathlib.Order.Atoms
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
K L : A
h : K < L
H : A
contrapose! : K < H ∧ H < L ↔ ∃ (g : B), K ≤ H ∧ H ≤ L ∧ g ∉ K ∧ g ∈ H ∧ H ≠ L
⊢ K < H → ¬H < L ↔ ∀ (g : B), K ≤ H → H ≤ L → g ∉ K → g ∈ H → H = L

Tactic:
contrapose!
-- Module: Mathlib.Order.Atoms
Goal:
A : Type u_4
B : Type u_5
inst : PartialOrder A
inst_1 : SetLike A B
inst_2 : IsConcreteLE A B
K L : A
h : K < L
H : A
rw : (K ≤ H ∧ H ≤ L) ∧ ¬H ≤ K ∧ H ≠ L ↔ ∃ (g : B), K ≤ H ∧ H ≤ L ∧ g ∉ K ∧ g ∈ H ∧ H ≠ L
⊢ K < H ∧ H < L ↔ ∃ (g : B), K ≤ H ∧ H ≤ L ∧ g ∉ K ∧ g ∈ H ∧ H ≠ L

Tactic:
rw [lt_iff_le_not_ge, lt_iff_le_and_ne, and_and_and_comm]

Premises used: lt_iff_le_and_ne, lt_iff_le_not_ge, and_and_and_comm