awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
simp_rw : (K ≤ H ∧ H ≤ L) ∧ ¬H ≤ K ∧ H ≠ L ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ K, x ∈ H ∧ H ≠ L
simp_rw₁ : K ≤ H ∧ H ≤ L ∧ ¬H ≤ K ∧ H ≠ L ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ K, x ∈ H ∧ H ≠ L
simp_rw₂ : K ≤ H → H ≤ L → (¬H ≤ K ∧ H ≠ L ↔ ∃ x ∉ K, x ∈ H ∧ H ≠ L)
simp_rw₃ : K ≤ H → H ≤ L → (¬H ≤ K ∧ H ≠ L ↔ ∃ (x : B), (x ∉ K ∧ x ∈ H) ∧ H ≠ L)
simp_rw₄ : K ≤ H → H ≤ L → (H ≠ L ∧ ¬H ≤ K ↔ ∃ (x : B), H ≠ L ∧ x ∉ K ∧ x ∈ H)
simp_rw₅ : K ≤ H → H ≤ L → (H ≠ L ∧ ¬H ≤ K ↔ H ≠ L ∧ ∃ x ∉ K, x ∈ H)
simp_rw₆ : K ≤ H → H ≤ L → ((H ≠ L ∧ ∃ x ∈ H, x ∉ K) ↔ H ≠ L ∧ ∃ x ∉ K, x ∈ H)
simp_rw₇ : K ≤ H → H ≤ L → True
⊢ (K ≤ H ∧ H ≤ L) ∧ ¬H ≤ K ∧ H ≠ L ↔ ∃ (g : B), K ≤ H ∧ H ≤ L ∧ g ∉ K ∧ g ∈ H ∧ H ≠ L

Tactic:
simp_rw [exists_and_left, and_assoc, and_congr_right_iff, ← and_assoc, and_comm, exists_and_left,
    SetLike.not_le_iff_exists, and_comm, implies_true]

Premises used: exists_and_left, and_congr_right_iff, and_comm, and_assoc, implies_true, SetLike.not_le_iff_exists
-- 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 ∉ H → g ∈ L → H = K

Tactic:
and_congr_right fun _ ↦ forall_congr' fun H ↦ not_iff_not.mp ?_

Premises used: not_iff_not, CovBy, and_congr_right, Iff.mp, 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 ∉ H → g ∈ L → H = K
⊢ K ⋖ L ↔ K < L ∧ ∀ (H : A) (g : B), K ≤ H → H ≤ L → g ∉ H → g ∈ L → H = K

Tactic:
refine and_congr_right fun _ ↦ forall_congr' fun H ↦ not_iff_not.mp ?_

Premises used: not_iff_not, and_congr_right, Iff.mp, 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
push : K < H ∧ H < L ↔ ∃ (g : B), K ≤ H ∧ H ≤ L ∧ g ∉ H ∧ g ∈ L ∧ H ≠ K
⊢ ¬(K < H → ¬H < L) ↔ ¬∀ (g : B), K ≤ H → H ≤ L → g ∉ H → g ∈ L → H = K

Tactic:
push Not

Premises used: Not
-- 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) ∧ K ≠ H ∧ ¬L ≤ H ↔ ∃ (g : B), K ≤ H ∧ H ≤ L ∧ g ∉ H ∧ g ∈ L ∧ H ≠ K
⊢ K < H ∧ H < L ↔ ∃ (g : B), K ≤ H ∧ H ≤ L ∧ g ∉ H ∧ g ∈ L ∧ H ≠ K

Tactic:
rw [lt_iff_le_and_ne, lt_iff_le_not_ge, and_and_and_comm]

Premises used: lt_iff_le_and_ne, lt_iff_le_not_ge, and_and_and_comm
-- 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
simp_rw : (K ≤ H ∧ H ≤ L) ∧ K ≠ H ∧ ¬L ≤ H ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ H, x ∈ L ∧ H ≠ K
simp_rw₁ : K ≤ H ∧ H ≤ L ∧ K ≠ H ∧ ¬L ≤ H ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ H, x ∈ L ∧ H ≠ K
simp_rw₂ : K ≤ H → H ≤ L → (K ≠ H ∧ ¬L ≤ H ↔ ∃ x ∉ H, x ∈ L ∧ H ≠ K)
simp_rw₃ : K ≤ H → H ≤ L → (K ≠ H ∧ ¬L ≤ H ↔ ∃ (x : B), (x ∉ H ∧ x ∈ L) ∧ H ≠ K)
simp_rw₄ : K ≤ H → H ≤ L → (K ≠ H ∧ ¬L ≤ H ↔ ∃ (x : B), H ≠ K ∧ x ∈ L ∧ x ∉ H)
simp_rw₅ : K ≤ H → H ≤ L → (K ≠ H ∧ ¬L ≤ H ↔ H ≠ K ∧ ∃ x ∈ L, x ∉ H)
simp_rw₆ : K ≤ H → H ≤ L → ((K ≠ H ∧ ∃ x ∈ L, x ∉ H) ↔ H ≠ K ∧ ∃ x ∈ L, x ∉ H)
simp_rw₇ : K ≤ H → H ≤ L → True
⊢ (K ≤ H ∧ H ≤ L) ∧ K ≠ H ∧ ¬L ≤ H ↔ ∃ (g : B), K ≤ H ∧ H ≤ L ∧ g ∉ H ∧ g ∈ L ∧ H ≠ K

Tactic:
simp_rw [exists_and_left, and_assoc, and_congr_right_iff, ← and_assoc, and_comm, exists_and_left,
    SetLike.not_le_iff_exists, ne_comm, implies_true]

Premises used: exists_and_left, and_congr_right_iff, and_comm, and_assoc, ne_comm, implies_true, SetLike.not_le_iff_exists
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
inst : Coframe α
f : ι → α
a : α
ha : IsCoatom a
⊢ iInf f ≤ a ↔ ∃ (i : ι), f i ≤ a

Tactic:
IsAtom.le_iSup (α := αᵒᵈ) ha

Premises used: iInf, IsAtom.le_iSup, OrderDual
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Coframe α
s : Set α
a : α
ha : IsCoatom a
⊢ sInf s ≤ a ↔ ∃ b ∈ s, b ≤ a

Tactic:
simp [sInf_eq_iInf', ha.iInf_le]

Premises used: sInf_eq_iInf', IsCoatom.iInf_le
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
a : α
b : (↑(Ici a) : Type u_2)
rw : ⊥ ⋖ b ↔ a ⋖ (↑b : α)
⊢ IsAtom b ↔ a ⋖ (↑b : α)

Tactic:
rw [← bot_covBy_iff]

Premises used: bot_covBy_iff
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
a : α
b : (↑(Ici a) : Type u_2)
⊢ ⊥ ⋖ b ↔ a ⋖ (↑b : α)

Tactic:
(Set.OrdConnected.apply_covBy_apply_iff (OrderEmbedding.subtype fun c => a ≤ c) ?_).symm

Premises used: Set.Ici, Set.Mem, setOf, LE.le, OrderEmbedding.subtype, Set.OrdConnected.apply_covBy_apply_iff, Iff.symm
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
a : α
b : (↑(Ici a) : Type u_2)
refine :
  OrdConnected.{u_2} (α := α)
    (range (ι := { c : α // a ≤ c }) (⇑(OrderEmbedding.subtype fun (c : α) ↦ a ≤ c) : (a : { c : α // a ≤ c }) → α))
⊢ ⊥ ⋖ b ↔ a ⋖ (↑b : α)

Tactic:
refine (Set.OrdConnected.apply_covBy_apply_iff (OrderEmbedding.subtype fun c => a ≤ c) ?_).symm

Premises used: LE.le, OrderEmbedding.subtype, Set.OrdConnected.apply_covBy_apply_iff, Iff.symm
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
a : α
b : (↑(Ici a) : Type u_2)
⊢ OrdConnected.{u_2} (α := α)
    (range (ι := { c : α // a ≤ c }) (⇑(OrderEmbedding.subtype fun (c : α) ↦ a ≤ c) : (a : { c : α // a ≤ c }) → α))

Tactic:
simpa only [OrderEmbedding.coe_subtype, Subtype.range_coe_subtype] using Set.ordConnected_Ici

Premises used: Set.ordConnected_Ici, Subtype.range_coe_subtype, OrderEmbedding.coe_subtype
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
b : α
a : (↑(Iic b) : Type u_2)
rw : a ⋖ ⊤ ↔ (↑a : α) ⋖ b
⊢ IsCoatom a ↔ (↑a : α) ⋖ b

Tactic:
rw [← covBy_top_iff]

Premises used: covBy_top_iff
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
b : α
a : (↑(Iic b) : Type u_2)
⊢ a ⋖ ⊤ ↔ (↑a : α) ⋖ b

Tactic:
(Set.OrdConnected.apply_covBy_apply_iff (OrderEmbedding.subtype fun c => c ≤ b) ?_).symm

Premises used: Set.Mem, setOf, LE.le, OrderEmbedding.subtype, Set.Iic, Set.OrdConnected.apply_covBy_apply_iff, Iff.symm
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
b : α
a : (↑(Iic b) : Type u_2)
refine :
  OrdConnected.{u_2} (α := α)
    (range (ι := { c : α // c ≤ b }) (⇑(OrderEmbedding.subtype fun (c : α) ↦ c ≤ b) : (a : { c : α // c ≤ b }) → α))
⊢ a ⋖ ⊤ ↔ (↑a : α) ⋖ b

Tactic:
refine (Set.OrdConnected.apply_covBy_apply_iff (OrderEmbedding.subtype fun c => c ≤ b) ?_).symm

Premises used: LE.le, OrderEmbedding.subtype, Set.OrdConnected.apply_covBy_apply_iff, Iff.symm
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
b : α
a : (↑(Iic b) : Type u_2)
⊢ OrdConnected.{u_2} (α := α)
    (range (ι := { c : α // c ≤ b }) (⇑(OrderEmbedding.subtype fun (c : α) ↦ c ≤ b) : (a : { c : α // c ≤ b }) → α))

Tactic:
simpa only [OrderEmbedding.coe_subtype, Subtype.range_coe_subtype] using Set.ordConnected_Iic

Premises used: Set.ordConnected_Iic, Subtype.range_coe_subtype, OrderEmbedding.coe_subtype
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
a b : α
h : a ≤ b
⊢ a ⋖ b ↔ IsAtom (Subtype.mk (p := fun (x : α) ↦ x ∈ Set.Ici a) b h)

Tactic:
simp
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
a b : α
h : a ≤ b
⊢ a ⋖ b ↔ IsCoatom (α := { x : α // x ∈ Set.Iic b }) (Subtype.mk (p := fun (x : α) ↦ x ∈ Set.Iic b) a h)

Tactic:
simp
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : SemilatticeInf α
inst_1 : OrderBot α
a b : α
ha : IsAtom a
rw : ¬a ⊓ b = ⊥ ↔ a ⊓ b = a
⊢ ¬Disjoint a b ↔ a ≤ b

Tactic:
rw [disjoint_iff, ← inf_eq_left]

Premises used: disjoint_iff, inf_eq_left
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : SemilatticeInf α
inst_1 : OrderBot α
a b : α
ha : IsAtom a
⊢ ¬a ⊓ b = ⊥ ↔ a ⊓ b = a

Tactic:
ha.ne_bot_iff_eq inf_le_left

Premises used: IsAtom.ne_bot_iff_eq, inf_le_left
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : SemilatticeInf α
inst_1 : OrderBot α
a b : α
ha : IsAtom a
⊢ ¬a ⊓ b = ⊥ ↔ a ⊓ b = a

Tactic:
exact ha.ne_bot_iff_eq inf_le_left

Premises used: IsAtom.ne_bot_iff_eq, inf_le_left
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : SemilatticeInf α
inst_1 : OrderBot α
a b : α
ha : IsAtom a
⊢ ¬a ≤ b ↔ Disjoint a b

Tactic:
ha.not_disjoint_iff_le.not_right.symm

Premises used: Iff.not_right, IsAtom.not_disjoint_iff_le, Iff.symm
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : SemilatticeInf α
inst_1 : OrderBot α
a b : α
ha : IsAtom a
hb : IsAtom b
hab : a ≠ b
⊢ Disjoint a b

Tactic:
simp [← ha.not_le_iff_disjoint, hb.le_iff, hab, ha.ne_bot]

Premises used: IsAtom.not_le_iff_disjoint, IsAtom.ne_bot, IsAtom.le_iff
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderTop α
a b : α
ha : IsCoatom a
rw : ¬a ⊔ b = ⊤ ↔ a ⊔ b = a
⊢ ¬Codisjoint a b ↔ b ≤ a

Tactic:
rw [codisjoint_iff, ← sup_eq_left]

Premises used: codisjoint_iff, sup_eq_left
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderTop α
a b : α
ha : IsCoatom a
⊢ ¬a ⊔ b = ⊤ ↔ a ⊔ b = a

Tactic:
ha.ne_top_iff_eq le_sup_left

Premises used: IsCoatom.ne_top_iff_eq, le_sup_left
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderTop α
a b : α
ha : IsCoatom a
⊢ ¬a ⊔ b = ⊤ ↔ a ⊔ b = a

Tactic:
exact ha.ne_top_iff_eq le_sup_left

Premises used: IsCoatom.ne_top_iff_eq, le_sup_left
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderTop α
a b : α
ha : IsCoatom a
⊢ ¬b ≤ a ↔ Codisjoint a b

Tactic:
ha.not_codisjoint_iff_le.not_right.symm

Premises used: IsCoatom.not_codisjoint_iff_le, Iff.not_right, Iff.symm
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderTop α
a b : α
ha : IsCoatom a
hb : IsCoatom b
hab : a ≠ b
⊢ Codisjoint a b

Tactic:
simp [← ha.not_le_iff_codisjoint, hb.le_iff, hab, ha.ne_top]

Premises used: IsCoatom.le_iff, IsCoatom.not_le_iff_codisjoint, IsCoatom.ne_top
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderTop α
a b : α
ha : IsCoatom a
hb : IsCoatom b
hab : a ≠ b
⊢ a ⊔ b = ⊤

Tactic:
codisjoint_iff.1 <| ha.codisjoint_of_ne hb hab

Premises used: codisjoint_iff, IsCoatom.codisjoint_of_ne, Iff.mp
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderBot α
inst_2 : Nontrivial α
inst_3 : IsAtomic α
⊢ ∃ (a : α), IsAtom a

Tactic:
have ⟨b, hb⟩ := exists_ne (⊥ : α)
  have ⟨a, ha⟩ := (eq_bot_or_exists_atom_le b).resolve_left hb
  ⟨a, ha.1⟩

Premises used: IsAtomic.eq_bot_or_exists_atom_le, Exists, exists_ne, Or.resolve_left, Bot.bot, And.left, Exists.intro, IsAtom, _private.0.IsAtomic.exists_atom.match_1, _private.0.IsAtomic.exists_atom.match_2
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : Nontrivial α
inst_3 : IsCoatomic α
⊢ ∃ (a : α), IsCoatom a

Tactic:
have ⟨b, hb⟩ := exists_ne (⊤ : α)
  have ⟨a, ha⟩ := (eq_top_or_exists_le_coatom b).resolve_left hb
  ⟨a, ha.1⟩

Premises used: _private.0.IsCoatomic.exists_coatom.match_1, Exists, exists_ne, Or.resolve_left, IsCoatomic.eq_top_or_exists_le_coatom, IsCoatom, _private.0.IsCoatomic.exists_coatom.match_2, And.left, Exists.intro, Top.top
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderBot α
h : IsCoatomic.{u_2} αᵒᵈ
b : α
⊢ b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b

Tactic:
apply h.eq_top_or_exists_le_coatom

Premises used: IsCoatomic.eq_top_or_exists_le_coatom
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderBot α
h : IsAtomic α
b : αᵒᵈ
⊢ b = ⊤ ∨ ∃ (a : αᵒᵈ), IsCoatom a ∧ b ≤ a

Tactic:
apply h.eq_bot_or_exists_atom_le

Premises used: IsAtomic.eq_bot_or_exists_atom_le
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
h : IsAtomic.{u_2} αᵒᵈ
b : α
⊢ b = ⊤ ∨ ∃ (a : α), IsCoatom a ∧ b ≤ a

Tactic:
apply h.eq_bot_or_exists_atom_le

Premises used: IsAtomic.eq_bot_or_exists_atom_le
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
h : IsCoatomic α
b : αᵒᵈ
⊢ b = ⊥ ∨ ∃ (a : αᵒᵈ), IsAtom a ∧ a ≤ b

Tactic:
apply h.eq_top_or_exists_le_coatom

Premises used: IsCoatomic.eq_top_or_exists_le_coatom
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : OrderBot α
inst_2 : IsAtomic α
⊢ IsCoatomic.{u_2} αᵒᵈ

Tactic:
isCoatomic_dual_iff_isAtomic.2 ‹IsAtomic α›

Premises used: Iff.mpr, isCoatomic_dual_iff_isAtomic
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : OrderBot α
inst_2 : IsAtomic α
x : α
⊢ IsAtomic.{u_2} (↑(Set.Iic x) : Type u_2)

Tactic:
⟨fun ⟨y, hy⟩ =>
    (eq_bot_or_exists_atom_le y).imp Subtype.mk_eq_mk.2 fun ⟨a, ha, hay⟩ =>
      ⟨⟨a, hay.trans hy⟩, ha.Iic (hay.trans hy), hay⟩⟩

Premises used: Iff.mpr, IsAtomic.eq_bot_or_exists_atom_le, Exists, Bot.bot, LE.le, And, _private.0.IsAtomic.Set.Iic.isAtomic.match_2, Subtype.mk_eq_mk, IsAtom, Or, Or.imp, IsAtomic.mk, Eq
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : IsCoatomic α
⊢ IsAtomic.{u_2} αᵒᵈ

Tactic:
isAtomic_dual_iff_isCoatomic.2 ‹IsCoatomic α›

Premises used: Iff.mpr, isAtomic_dual_iff_isCoatomic
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : IsCoatomic α
x : α
⊢ IsCoatomic.{u_2} (↑(Set.Ici x) : Type u_2)

Tactic:
⟨fun ⟨y, hy⟩ =>
    (eq_top_or_exists_le_coatom y).imp Subtype.mk_eq_mk.2 fun ⟨a, ha, hay⟩ =>
      ⟨⟨a, le_trans hy hay⟩, ha.Ici (le_trans hy hay), hay⟩⟩

Premises used: Iff.mpr, Exists, IsCoatomic.mk, IsCoatomic.eq_top_or_exists_le_coatom, LE.le, IsCoatom, And, Subtype.mk_eq_mk, Or, Or.imp, Top.top, _private.0.IsCoatomic.Set.Ici.isCoatomic.match_2, Eq
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderBot α
⊢ IsAtomic α ↔ ∀ (x : α), IsAtomic.{u_2} (↑(Set.Iic x) : Type u_2)

Tactic:
⟨@IsAtomic.Set.Iic.isAtomic _ _ _, fun h =>
    ⟨fun x =>
      ((@eq_bot_or_exists_atom_le _ _ _ (h x)) (⊤ : Set.Iic x)).imp Subtype.mk_eq_mk.1
        (Exists.imp' (↑) fun ⟨_, _⟩ => And.imp_left IsAtom.of_isAtom_coe_Iic)⟩⟩

Premises used: IsAtomic.eq_bot_or_exists_atom_le, IsAtomic.Set.Iic.isAtomic, Exists.imp', Iff.intro, Subtype.mk_eq_mk, Iff.mp, Or.imp, Top.top, IsAtomic.mk
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderTop α
⊢ IsCoatomic α ↔ ∀ (x : α), IsCoatomic.{u_2} (↑(Set.Ici x) : Type u_2)

Tactic:
isAtomic_dual_iff_isCoatomic.symm.trans <|
    isAtomic_iff_forall_isAtomic_Iic.trans <|
      forall_congr' fun _ => isCoatomic_dual_iff_isAtomic.symm.trans Iff.rfl

Premises used: isCoatomic_dual_iff_isAtomic, isAtomic_iff_forall_isAtomic_Iic, Iff.rfl, isAtomic_dual_iff_isCoatomic, forall_congr', Iff.trans, Iff.symm
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_4
a b : α
inst : Preorder α
inst_1 : IsStronglyAtomic α
h : a < b
⊢ ∃ (x : α), a ⋖ x ∧ x ≤ b

Tactic:
IsStronglyAtomic.exists_covBy_le_of_lt a b h

Premises used: IsStronglyAtomic.exists_covBy_le_of_lt
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_4
a b : α
inst : Preorder α
inst_1 : IsStronglyCoatomic α
h : a < b
⊢ ∃ (x : α), a ≤ x ∧ x ⋖ b

Tactic:
IsStronglyCoatomic.exists_le_covBy_of_lt a b h

Premises used: IsStronglyCoatomic.exists_le_covBy_of_lt
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_4
inst : Preorder α
⊢ IsStronglyAtomic.{u_4} αᵒᵈ ↔ IsStronglyCoatomic α

Tactic:
simpa [isStronglyAtomic_iff, OrderDual.exists, OrderDual.forall,
    OrderDual.toDual_le_toDual, and_comm, isStronglyCoatomic_iff] using forall_comm

Premises used: isStronglyAtomic_iff, OrderDual.toDual_le_toDual, forall_comm, and_comm, isStronglyCoatomic_iff, OrderDual.exists, OrderDual.forall
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_4
inst : Preorder α
rw : IsStronglyAtomic.{u_4} αᵒᵈᵒᵈ ↔ IsStronglyAtomic α
⊢ IsStronglyCoatomic.{u_4} αᵒᵈ ↔ IsStronglyAtomic α

Tactic:
rw [← isStronglyAtomic_dual_iff_is_stronglyCoatomic]

Premises used: isStronglyAtomic_dual_iff_is_stronglyCoatomic
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_4
inst : Preorder α
⊢ IsStronglyAtomic.{u_4} αᵒᵈᵒᵈ ↔ IsStronglyAtomic α

Tactic:
rfl
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
a b : α
inst_1 : Preorder α
inst_2 rwa rwa₁ rwa₂ rwa₃ : IsStronglyAtomic α
⊢ IsStronglyCoatomic.{u_4} αᵒᵈ

Tactic:
rwa [isStronglyCoatomic_dual_iff_is_stronglyAtomic]

Premises used: isStronglyCoatomic_dual_iff_is_stronglyAtomic
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
a b : α
inst_1 : Preorder α
inst_2 rwa rwa₁ rwa₂ rwa₃ : IsStronglyCoatomic α
⊢ IsStronglyAtomic.{u_4} αᵒᵈ

Tactic:
rwa [isStronglyAtomic_dual_iff_is_stronglyCoatomic]

Premises used: isStronglyAtomic_dual_iff_is_stronglyCoatomic
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α_2 : Type u_4
a_1 b : α_2
inst_1 : Preorder α_2
α : Type u_5
inst_2 : PartialOrder α
inst_3 : OrderBot α
inst_4 : IsStronglyAtomic α
a : α
rw : ⊥ < a → ∃ (a_3 : α), IsAtom a_3 ∧ a_3 ≤ a
⊢ a = ⊥ ∨ ∃ (a_2 : α), IsAtom a_2 ∧ a_2 ≤ a

Tactic:
rw [or_iff_not_imp_left, ← Ne, ← bot_lt_iff_ne_bot]

Premises used: bot_lt_iff_ne_bot, Ne, Classical.or_iff_not_imp_left
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α_2 : Type u_4
a_1 b : α_2
inst_1 : Preorder α_2
α : Type u_5
inst_2 : PartialOrder α
inst_3 : OrderBot α
inst_4 : IsStronglyAtomic α
a : α
⊢ ⊥ < a → ∃ (a_3 : α), IsAtom a_3 ∧ a_3 ≤ a

Tactic:
fun hlt ↦ ?_
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α_2 : Type u_4
a_1 b : α_2
inst_1 : Preorder α_2
α : Type u_5
inst_2 : PartialOrder α
inst_3 : OrderBot α
inst_4 : IsStronglyAtomic α
a : α
refine : ∀ (hlt : ⊥ < a), ∃ (a_2 : α), IsAtom a_2 ∧ a_2 ≤ a
⊢ ⊥ < a → ∃ (a_3 : α), IsAtom a_3 ∧ a_3 ≤ a

Tactic:
refine fun hlt ↦ ?_
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α_2 : Type u_4
a_1 b : α_2
inst_1 : Preorder α_2
α : Type u_5
inst_2 : PartialOrder α
inst_3 : OrderBot α
inst_4 : IsStronglyAtomic α
a : α
hlt : ⊥ < a
obtain : ∀ (x : α) (hx : ⊥ ⋖ x) (hxa : x ≤ a), ∃ (a_2 : α), IsAtom a_2 ∧ a_2 ≤ a
⊢ ∃ (a_2 : α), IsAtom a_2 ∧ a_2 ≤ a

Tactic:
obtain ⟨x, hx, hxa⟩ := hlt.exists_covby_le

Premises used: LT.lt.exists_covby_le
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α_2 : Type u_4
a_1 b : α_2
inst_1 : Preorder α_2
α : Type u_5
inst_2 : PartialOrder α
inst_3 : OrderBot α
inst_4 : IsStronglyAtomic α
a : α
hlt : ⊥ < a
x : α
hx : ⊥ ⋖ x
hxa : x ≤ a
⊢ ∃ (a_2 : α), IsAtom a_2 ∧ a_2 ≤ a

Tactic:
⟨x, bot_covBy_iff.1 hx, hxa⟩

Premises used: bot_covBy_iff, And.intro, Exists.intro, Iff.mp
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α_2 : Type u_4
a_1 b : α_2
inst_1 : Preorder α_2
α : Type u_5
inst_2 : PartialOrder α
inst_3 : OrderBot α
inst_4 : IsStronglyAtomic α
a : α
hlt : ⊥ < a
x : α
hx : ⊥ ⋖ x
hxa : x ≤ a
⊢ ∃ (a_2 : α), IsAtom a_2 ∧ a_2 ≤ a

Tactic:
exact ⟨x, bot_covBy_iff.1 hx, hxa⟩
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α_2 : Type u_4
a b : α_2
inst_1 : Preorder α_2
α : Type u_5
inst_2 : PartialOrder α
inst_3 : OrderTop α
inst_4 : IsStronglyCoatomic α
⊢ IsCoatomic α

Tactic:
isAtomic_dual_iff_isCoatomic.1 <| IsStronglyAtomic.isAtomic (α := αᵒᵈ)

Premises used: IsStronglyAtomic.isAtomic, isAtomic_dual_iff_isCoatomic, Iff.mp, OrderDual
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_4
inst : Preorder α
inst_1 : IsStronglyAtomic α
s : Set α
h : s.OrdConnected
c : α
hc : c ∈ s
d : α
hd : d ∈ s
hcd : Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc < Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd
obtain :
  ∀ (x : α) (hcx : c ⋖ x) (hxd : x ≤ d),
    ∃ (x : (↑s : Type u_4)),
      Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc ⋖ x ∧ x ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd
⊢ ∃ (x : (↑s : Type u_4)),
    Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc ⋖ x ∧ x ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd

Tactic:
obtain ⟨x, hcx, hxd⟩ := (Subtype.mk_lt_mk.1 hcd).exists_covby_le

Premises used: Subtype.mk_lt_mk, LT.lt.exists_covby_le, Iff.mp
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_4
inst : Preorder α
inst_1 : IsStronglyAtomic α
s : Set α
h : s.OrdConnected
c : α
hc : c ∈ s
d : α
hd : d ∈ s
hcd : Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc < Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd
x : α
hcx : c ⋖ x
hxd : x ≤ d
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc < Subtype.mk (p := fun (x : α) ↦ x ∈ s) x ⋯

Tactic:
simpa using hcx.lt

Premises used: CovBy.lt
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_4
inst : Preorder α
inst_1 : IsStronglyAtomic α
s : Set α
h : s.OrdConnected
c : α
hc : c ∈ s
d : α
hd : d ∈ s
hcd : Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc < Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd
x : α
hcx : c ⋖ x
hxd : x ≤ d
y : (↑s : Type u_4)
hy : Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc < y
hy' : y < Subtype.mk (p := fun (x : α) ↦ x ∈ s) x ⋯
⊢ c < (↑y : α)

Tactic:
simpa using hy
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_4
inst : Preorder α
inst_1 : IsStronglyAtomic α
s : Set α
h : s.OrdConnected
c : α
hc : c ∈ s
d : α
hd : d ∈ s
hcd : Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc < Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd
x : α
hcx : c ⋖ x
hxd : x ≤ d
y : (↑s : Type u_4)
hy : Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc < y
hy' : y < Subtype.mk (p := fun (x : α) ↦ x ∈ s) x ⋯
⊢ (↑y : α) < x

Tactic:
simpa using hy'
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_4
inst : Preorder α
inst_1 : IsStronglyAtomic α
s : Set α
h : s.OrdConnected
c : α
hc : c ∈ s
d : α
hd : d ∈ s
hcd : Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc < Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd
x : α
hcx : c ⋖ x
hxd : x ≤ d
⊢ ∃ (x : (↑s : Type u_4)),
    Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc ⋖ x ∧ x ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd

Tactic:
exact ⟨⟨x, h.out' hc hd ⟨hcx.le, hxd⟩⟩,
      ⟨by simpa using hcx.lt, fun y hy hy' ↦ hcx.2 (by simpa using hy) (by simpa using hy')⟩, hxd⟩
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_4
inst : Preorder α
inst_1 : IsStronglyCoatomic α
s : Set α
h : s.OrdConnected
⊢ IsStronglyCoatomic.{u_4} (↑s : Type u_4)

Tactic:
isStronglyAtomic_dual_iff_is_stronglyCoatomic.1 h.dual.isStronglyAtomic

Premises used: isStronglyAtomic_dual_iff_is_stronglyCoatomic, Set.OrdConnected.isStronglyAtomic, Set.OrdConnected.dual, Iff.mp
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
a b : α
inst_1 : Preorder α
inst_2 : IsStronglyAtomic α
s : Set α
inst_3 : s.OrdConnected
⊢ s.OrdConnected

Tactic:
assumption
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
a b : α
inst_1 : Preorder α
inst_2 : IsStronglyCoatomic α
s : Set α
h : s.OrdConnected
⊢ s.OrdConnected

Tactic:
assumption
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
a b : α
inst_1 : Preorder α
inst_2 : PredOrder α
rw : IsStronglyAtomic.{u_4} αᵒᵈ
⊢ IsStronglyCoatomic α

Tactic:
rw [← isStronglyAtomic_dual_iff_is_stronglyCoatomic]

Premises used: isStronglyAtomic_dual_iff_is_stronglyCoatomic
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
a b : α
inst_1 : Preorder α
inst_2 : PredOrder α
⊢ IsStronglyAtomic.{u_4} αᵒᵈ

Tactic:
infer_instance
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : PartialOrder α
h : WellFounded fun (x1 x2 : α) ↦ x1 < x2
a b : α
hab : a < b
⊢ ∃ (x : α), a ⋖ x ∧ x ≤ b

Tactic:
⟨WellFounded.min h (Set.Ioc a b) ⟨b, hab,rfl.le⟩, ?_⟩

Premises used: Set.Ioc, Eq.le, And.intro, WellFounded.min, Exists.intro, rfl