awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderBot α
inst_3 : IsAtomic α
inst_4 : OrderBot β
l : α → β
u : β → α
gi : GaloisInsertion l u
hbot : u ⊥ = ⊥
h_atom : ∀ (a : α), IsAtom a → u (l a) = a
a : α
hla : IsAtom (l a)
a' : α
ha' : IsAtom a'
hab' : a' ≤ u (l a)
this : l a' = l a
⊢ a = a'

Tactic:
have haa' : a = a' :=
    (ha'.le_iff.mp <|
          (gi.gc.le_u_l a).trans_eq (h_atom a' ha' ▸ congr_arg u this.symm)).resolve_left
      (mt (congr_arg l) (gi.gc.l_bot.symm ▸ hla.1))
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderBot α
inst_3 : IsAtomic α
inst_4 : OrderBot β
l : α → β
u : β → α
gi : GaloisInsertion l u
hbot : u ⊥ = ⊥
h_atom : ∀ (a : α), IsAtom a → u (l a) = a
a : α
hla : IsAtom (l a)
a' : α
ha' : IsAtom a'
hab' : a' ≤ u (l a)
this : l a' = l a
haa' : a = a'
⊢ IsAtom a

Tactic:
haa'.symm ▸ ha'

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderBot α
inst_3 : IsAtomic α
inst_4 : OrderBot β
l : α → β
u : β → α
gi : GaloisInsertion l u
hbot : u ⊥ = ⊥
h_atom : ∀ (a : α), IsAtom a → u (l a) = a
a : α
hla : IsAtom (l a)
a' : α
ha' : IsAtom a'
hab' : a' ≤ u (l a)
this : l a' = l a
haa' : a = a'
⊢ IsAtom a

Tactic:
exact haa'.symm ▸ ha'
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderBot α
inst_3 : IsAtomic α
inst_4 : OrderBot β
l : α → β
u : β → α
gi : GaloisInsertion l u
hbot : u ⊥ = ⊥
h_atom : ∀ (a : α), IsAtom a → u (l a) = a
b : β
rw : IsAtom (l (u b)) ↔ IsAtom b
rw₁ rw₂ : IsAtom b ↔ IsAtom b
⊢ IsAtom (u b) ↔ IsAtom b

Tactic:
rw [← gi.isAtom_iff hbot h_atom, gi.l_u_eq]

Premises used: GaloisInsertion.isAtom_iff, GaloisInsertion.l_u_eq
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderTop α
inst_3 : OrderTop β
l : α → β
u : β → α
gi : GaloisInsertion l u
b : β
hb : IsCoatom (u b)
⊢ IsCoatom b

Tactic:
OrderEmbedding.isCoatom_of_map_top_of_image
    ⟨⟨u, gi.u_injective⟩, @GaloisInsertion.u_le_u_iff _ _ _ _ _ _ gi⟩ gi.gc.u_top hb

Premises used: OrderEmbedding.isCoatom_of_map_top_of_image, RelEmbedding.mk, Function.Embedding.mk, GaloisInsertion.u_injective, GaloisConnection.u_top, GaloisInsertion.u_le_u_iff, GaloisInsertion.gc
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderTop α
inst_3 : IsCoatomic α
inst_4 : OrderTop β
l : α → β
u : β → α
gi : GaloisInsertion l u
h_coatom : ∀ (a : α), IsCoatom a → u (l a) = a
b : β
⊢ IsCoatom (u b) ↔ IsCoatom b

Tactic:
⟨fun hb => gi.isCoatom_of_image hb, fun hb => ?_⟩

Premises used: GaloisInsertion.isCoatom_of_image, Iff.intro
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderTop α
inst_3 : IsCoatomic α
inst_4 : OrderTop β
l : α → β
u : β → α
gi : GaloisInsertion l u
h_coatom : ∀ (a : α), IsCoatom a → u (l a) = a
b : β
refine : ∀ (hb : IsCoatom b), IsCoatom (u b)
⊢ IsCoatom (u b) ↔ IsCoatom b

Tactic:
refine ⟨fun hb => gi.isCoatom_of_image hb, fun hb => ?_⟩
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderTop α
inst_3 : IsCoatomic α
inst_4 : OrderTop β
l : α → β
u : β → α
gi : GaloisInsertion l u
h_coatom : ∀ (a : α), IsCoatom a → u (l a) = a
b : β
hb : IsCoatom b
obtain : ∀ (a : α) (ha : IsCoatom a) (hab : u b ≤ a), IsCoatom (u b)
⊢ IsCoatom (u b)

Tactic:
obtain ⟨a, ha, hab⟩ :=
    (eq_top_or_exists_le_coatom (u b)).resolve_left fun h =>
      hb.1 <| (gi.gc.u_top ▸ gi.l_u_eq ⊤ : l ⊤ = ⊤) ▸ gi.l_u_eq b ▸ congr_arg l h

Premises used: Eq.rec, Or.resolve_left, IsCoatomic.eq_top_or_exists_le_coatom, congr_arg, GaloisConnection.u_top, And.left, Top.top, GaloisInsertion.l_u_eq, GaloisInsertion.gc
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderTop α
inst_3 : IsCoatomic α
inst_4 : OrderTop β
l : α → β
u : β → α
gi : GaloisInsertion l u
h_coatom : ∀ (a : α), IsCoatom a → u (l a) = a
b : β
hb : IsCoatom b
a : α
ha : IsCoatom a
hab : u b ≤ a
⊢ l a = b

Tactic:
have : l a = b :=
    (hb.le_iff.mp (gi.l_u_eq b ▸ gi.gc.monotone_l hab : b ≤ l a)).resolve_left fun hla =>
      ha.1 (gi.gc.u_top ▸ h_coatom a ha ▸ congr_arg u hla)
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderTop α
inst_3 : IsCoatomic α
inst_4 : OrderTop β
l : α → β
u : β → α
gi : GaloisInsertion l u
h_coatom : ∀ (a : α), IsCoatom a → u (l a) = a
b : β
hb : IsCoatom b
a : α
ha : IsCoatom a
hab : u b ≤ a
this : l a = b
⊢ IsCoatom (u b)

Tactic:
this ▸ (h_coatom a ha).symm ▸ ha

Premises used: Eq.rec, Eq.symm
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderTop α
inst_3 : IsCoatomic α
inst_4 : OrderTop β
l : α → β
u : β → α
gi : GaloisInsertion l u
h_coatom : ∀ (a : α), IsCoatom a → u (l a) = a
b : β
hb : IsCoatom b
a : α
ha : IsCoatom a
hab : u b ≤ a
this : l a = b
⊢ IsCoatom (u b)

Tactic:
exact this ▸ (h_coatom a ha).symm ▸ ha
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderTop α
inst_3 : OrderTop β
l : α → β
u : β → α
gi : GaloisCoinsertion l u
hbot : l ⊤ = ⊤
a : α
hb : IsCoatom (l a)
⊢ IsCoatom a

Tactic:
gi.dual.isAtom_of_u_bot hbot hb.dual

Premises used: IsCoatom, GaloisCoinsertion.dual, OrderDual, IsCoatom.dual, GaloisInsertion.isAtom_of_u_bot
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderTop α
inst_3 : OrderTop β
inst_4 : IsCoatomic β
l : α → β
u : β → α
gi : GaloisCoinsertion l u
htop : l ⊤ = ⊤
h_coatom : ∀ (b : β), IsCoatom b → l (u b) = b
b : β
⊢ IsCoatom (u b) ↔ IsCoatom b

Tactic:
gi.dual.isAtom_iff htop h_coatom b

Premises used: GaloisInsertion.isAtom_iff, IsCoatom, GaloisCoinsertion.dual, OrderDual
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderTop α
inst_3 : OrderTop β
inst_4 : IsCoatomic β
l : α → β
u : β → α
gi : GaloisCoinsertion l u
htop : l ⊤ = ⊤
h_coatom : ∀ (b : β), IsCoatom b → l (u b) = b
a : α
⊢ IsCoatom (l a) ↔ IsCoatom a

Tactic:
gi.dual.isAtom_iff' htop h_coatom a

Premises used: IsCoatom, GaloisCoinsertion.dual, OrderDual, GaloisInsertion.isAtom_iff'
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderBot α
inst_3 : OrderBot β
l : α → β
u : β → α
gi : GaloisCoinsertion l u
a : α
hb : IsAtom (l a)
⊢ IsAtom a

Tactic:
gi.dual.isCoatom_of_image hb.dual

Premises used: IsAtom.dual, GaloisInsertion.isCoatom_of_image, GaloisCoinsertion.dual, IsAtom, OrderDual
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderBot α
inst_3 : OrderBot β
inst_4 : IsAtomic β
l : α → β
u : β → α
gi : GaloisCoinsertion l u
h_atom : ∀ (b : β), IsAtom b → l (u b) = b
a : α
⊢ IsAtom (l a) ↔ IsAtom a

Tactic:
gi.dual.isCoatom_iff h_atom a

Premises used: GaloisInsertion.isCoatom_iff, GaloisCoinsertion.dual, IsAtom, OrderDual
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderBot α
inst_3 : OrderBot β
f : α ≃o β
a : α
⊢ IsAtom.{u_3} (α := β) ((f : (a : α) → β) a : β) ↔ IsAtom a

Tactic:
⟨f.toGaloisCoinsertion.isAtom_of_image, fun ha =>
    f.toGaloisInsertion.isAtom_of_u_bot (map_bot f.symm) <| (f.symm_apply_apply a).symm ▸ ha⟩

Premises used: OrderIso.toGaloisCoinsertion, Eq.rec, OrderIso.symm, OrderIso.toGaloisInsertion, Iff.intro, OrderIso.symm_apply_apply, GaloisInsertion.isAtom_of_u_bot, Eq.symm, OrderIso.map_bot, GaloisCoinsertion.isAtom_of_image
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderTop α
inst_3 : OrderTop β
f : α ≃o β
a : α
⊢ IsCoatom.{u_3} (α := β) ((f : (a : α) → β) a : β) ↔ IsCoatom a

Tactic:
f.dual.isAtom_iff a

Premises used: OrderIso.isAtom_iff, IsCoatom, OrderIso.dual, OrderDual
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : BoundedOrder α
inst_3 : BoundedOrder β
f : α ≃o β
rw : IsAtom.{u_2} (α := α) ⊤ ↔ IsSimpleOrder β
rw₁ : IsAtom.{u_2} (α := α) ⊤ ↔ IsAtom.{u_3} (α := β) ⊤
rw₂ : IsAtom.{u_3} (α := β) ((f : (a : α) → β) ⊤ : β) ↔ IsAtom.{u_3} (α := β) ⊤
rw₃ rw₄ : IsAtom.{u_3} (α := β) ⊤ ↔ IsAtom.{u_3} (α := β) ⊤
⊢ IsSimpleOrder α ↔ IsSimpleOrder β

Tactic:
rw [isSimpleOrder_iff_isAtom_top, isSimpleOrder_iff_isAtom_top, ← f.isAtom_iff ⊤,
    f.map_top]

Premises used: isSimpleOrder_iff_isAtom_top, OrderIso.isAtom_iff, OrderIso.map_top, Top.top
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : BoundedOrder α
inst_3 : BoundedOrder β
h : IsSimpleOrder β
f : α ≃o β
⊢ IsSimpleOrder α

Tactic:
f.isSimpleOrder_iff.mpr h

Premises used: Iff.mpr, OrderIso.isSimpleOrder_iff
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderBot α
inst_3 : OrderBot β
f : α ≃o β
⊢ IsAtomic α ↔ IsAtomic β

Tactic:
simp only [isAtomic_iff, f.surjective.forall, f.surjective.exists, ← map_bot f, f.eq_iff_eq,
    f.le_iff_le, f.isAtom_iff]

Premises used: Function.Surjective.forall, RelIso.eq_iff_eq, Function.Surjective.exists, OrderIso.isAtom_iff, isAtomic_iff, OrderIso.le_iff_le, OrderIso.surjective, OrderIso.map_bot
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : OrderTop α
inst_3 : OrderTop β
f : α ≃o β
⊢ IsCoatomic α ↔ IsCoatomic β

Tactic:
simp only [← isAtomic_dual_iff_isCoatomic, f.dual.isAtomic_iff]

Premises used: OrderIso.dual, isAtomic_dual_iff_isCoatomic, OrderIso.isAtomic_iff
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsUpperModularLattice α
inst_3 : IsAtomistic α
a b : α
hab : a < b
obtain : ∀ (s : Set α) (hsb : IsLUB s b) (h : ∀ a ∈ s, IsAtom a), ∃ (x : α), a ⋖ x ∧ x ≤ b
⊢ ∃ (x : α), a ⋖ x ∧ x ≤ b

Tactic:
obtain ⟨s, hsb, h⟩ := isLUB_atoms b

Premises used: IsAtomistic.isLUB_atoms
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsUpperModularLattice α
inst_3 : IsAtomistic α
a b : α
hab : a < b
s : Set α
hsb : IsLUB s b
h : ∀ a ∈ s, IsAtom a
⊢ ∃ (x : α), a ⋖ x ∧ x ≤ b

Tactic:
by_contra fun hcon ↦ hab.not_ge <| (isLUB_le_iff hsb).2 fun x hx ↦ ?_

Premises used: Iff.mpr, isLUB_le_iff, by_contra, LT.lt.not_ge
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsUpperModularLattice α
inst_3 : IsAtomistic α
a b : α
hab : a < b
s : Set α
hsb : IsLUB s b
h : ∀ a ∈ s, IsAtom a
refine : ∀ (hcon : ¬∃ (x : α), a ⋖ x ∧ x ≤ b) (x : α) (hx : x ∈ s), x ≤ a
⊢ ∃ (x : α), a ⋖ x ∧ x ≤ b

Tactic:
refine by_contra fun hcon ↦ hab.not_ge <| (isLUB_le_iff hsb).2 fun x hx ↦ ?_

Premises used: Iff.mpr, isLUB_le_iff, by_contra, LT.lt.not_ge
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsUpperModularLattice α
inst_3 : IsAtomistic α
a b : α
hab : a < b
s : Set α
hsb : IsLUB s b
h : ∀ a ∈ s, IsAtom a
hcon : ¬∃ (x : α), a ⋖ x ∧ x ≤ b
x : α
hx : x ∈ s
⊢ ∀ x ≤ b, ¬a ⋖ x

Tactic:
simp_rw [not_exists, and_comm (b := _ ≤ _), not_and] at hcon

Premises used: not_exists, and_comm, not_and
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsUpperModularLattice α
inst_3 : IsAtomistic α
a b : α
hab : a < b
s : Set α
hsb : IsLUB s b
h : ∀ a ∈ s, IsAtom a
x : α
hx : x ∈ s
hcon : ∀ x ≤ b, ¬a ⋖ x
⊢ ¬a ⋖ x ⊔ a

Tactic:
specialize hcon (x ⊔ a) (sup_le (hsb.1 hx) hab.le)

Premises used: LT.lt.le, And.left, Max.max, sup_le
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsUpperModularLattice α
inst_3 : IsAtomistic α
a b : α
hab : a < b
s : Set α
hsb : IsLUB s b
h : ∀ a ∈ s, IsAtom a
x : α
hx : x ∈ s
hcon : ¬a ⋖ x ⊔ a
⊢ ⊥ ≤ x ⊓ a

Tactic:
simp
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsUpperModularLattice α
inst_3 : IsAtomistic α
a b : α
hab : a < b
s : Set α
hsb : IsLUB s b
h : ∀ a ∈ s, IsAtom a
x : α
hx : x ∈ s
hcon : ¬a ⋖ x ⊔ a
⊢ x ⊓ a ≤ x

Tactic:
simp
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsUpperModularLattice α
inst_3 : IsAtomistic α
a b : α
hab : a < b
s : Set α
hsb : IsLUB s b
h : ∀ a ∈ s, IsAtom a
x : α
hx : x ∈ s
hcon : ¬a ⋖ x ⊔ a
inl : ∀ (hbot : x ⊓ a = ⊥), x ≤ a
inr : ∀ (h_inf : x ⊓ a = x), x ≤ a
⊢ x ≤ a

Tactic:
obtain (hbot | h_inf) := (h x hx).bot_covBy.eq_or_eq (c := x ⊓ a) (by simp) (by simp)

Premises used: IsAtom.bot_covBy, CovBy.eq_or_eq
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsUpperModularLattice α
inst_3 : IsAtomistic α
a b : α
hab : a < b
s : Set α
hsb : IsLUB s b
h : ∀ a ∈ s, IsAtom a
x : α
hx : x ∈ s
hcon : ¬a ⋖ x ⊔ a
hbot : x ⊓ a = ⊥
⊢ x ≤ a

Tactic:
False.elim <| hcon <|
        (hbot ▸ IsUpperModularLattice.covBy_sup_of_inf_covBy) (h x hx).bot_covBy

Premises used: False.elim
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsUpperModularLattice α
inst_3 : IsAtomistic α
a b : α
hab : a < b
s : Set α
hsb : IsLUB s b
h : ∀ a ∈ s, IsAtom a
x : α
hx : x ∈ s
hcon : ¬a ⋖ x ⊔ a
hbot : x ⊓ a = ⊥
⊢ x ≤ a

Tactic:
exact False.elim <| hcon <|
        (hbot ▸ IsUpperModularLattice.covBy_sup_of_inf_covBy) (h x hx).bot_covBy

Premises used: False.elim
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsUpperModularLattice α
inst_3 : IsAtomistic α
a b : α
hab : a < b
s : Set α
hsb : IsLUB s b
h : ∀ a ∈ s, IsAtom a
x : α
hx : x ∈ s
hcon : ¬a ⋖ x ⊔ a
h_inf : x ⊓ a = x
inr inr₁ inr₂ inr₃ : ∀ (h_inf : x ≤ a), x ≤ a
⊢ x ≤ a

Tactic:
rwa [inf_eq_left] at h_inf

Premises used: inf_eq_left
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : OrderTop α
inst_2 : IsLowerModularLattice α
inst_3 : IsCoatomistic α
rw : IsStronglyAtomic.{u_2} αᵒᵈ
⊢ IsStronglyCoatomic α

Tactic:
rw [← isStronglyAtomic_dual_iff_is_stronglyCoatomic]

Premises used: isStronglyAtomic_dual_iff_is_stronglyCoatomic
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : OrderTop α
inst_2 : IsLowerModularLattice α
inst_3 : IsCoatomistic α
⊢ IsStronglyAtomic.{u_2} αᵒᵈ

Tactic:
Lattice.isStronglyAtomic

Premises used: Lattice.isStronglyAtomic
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : OrderTop α
inst_2 : IsLowerModularLattice α
inst_3 : IsCoatomistic α
⊢ IsStronglyAtomic.{u_2} αᵒᵈ

Tactic:
exact Lattice.isStronglyAtomic

Premises used: Lattice.isStronglyAtomic
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
a b : α
hc : IsCompl a b
⊢ IsAtom a ↔ IsCoatom b

Tactic:
Set.isSimpleOrder_Iic_iff_isAtom.symm.trans <|
    hc.IicOrderIsoIci.isSimpleOrder_iff.trans Set.isSimpleOrder_Ici_iff_isCoatom

Premises used: IsCompl.IicOrderIsoIci, Set.isSimpleOrder_Iic_iff_isAtom, OrderIso.isSimpleOrder_iff, Iff.trans, Set.isSimpleOrder_Ici_iff_isCoatom, Iff.symm
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
a b : α
hc : IsCompl a b
⊢ IsCoatom a ↔ IsAtom b

Tactic:
hc.symm.isAtom_iff_isCoatom.symm

Premises used: IsCompl.isAtom_iff_isCoatom, Iff.symm, IsCompl.symm
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
inst_3 : ComplementedLattice α
inst_4 : IsAtomic α
x : α
rcases : ∀ (y : α) (xy : IsCompl x y), x = ⊤ ∨ ∃ (a : α), IsCoatom a ∧ x ≤ a
⊢ x = ⊤ ∨ ∃ (a : α), IsCoatom a ∧ x ≤ a

Tactic:
rcases exists_isCompl x with ⟨y, xy⟩

Premises used: ComplementedLattice.exists_isCompl
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
inst_3 : ComplementedLattice α
inst_4 : IsAtomic α
x y : α
xy : IsCompl x y
apply : y = ⊥ → x = ⊤
apply₁ : (∃ (a : α), IsAtom a ∧ a ≤ y) → ∃ (a : α), IsCoatom a ∧ x ≤ a
⊢ x = ⊤ ∨ ∃ (a : α), IsCoatom a ∧ x ≤ a

Tactic:
apply (eq_bot_or_exists_atom_le y).imp _ _

Premises used: IsAtomic.eq_bot_or_exists_atom_le, Or.imp
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
inst_3 : ComplementedLattice α
inst_4 : IsAtomic α
x : α
xy : IsCompl x ⊥
⊢ x = ⊤

Tactic:
eq_top_of_isCompl_bot xy

Premises used: eq_top_of_isCompl_bot
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
inst_3 : ComplementedLattice α
inst_4 : IsAtomic α
x : α
xy : IsCompl x ⊥
⊢ x = ⊤

Tactic:
exact eq_top_of_isCompl_bot xy

Premises used: eq_top_of_isCompl_bot
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
inst_3 : ComplementedLattice α
inst_4 : IsAtomic α
x y : α
xy : IsCompl x y
a : α
ha : IsAtom a
ay : a ≤ y
rcases :
  ∀ (b : α) (xb : b ∈ Set.Ici x)
    (hb :
      IsCompl
        ((⋯.IicOrderIsoIci : (a : (↑(Set.Iic y) : Type u_2)) → (↑(Set.Ici x) : Type u_2))
          (Subtype.mk (p := fun (x : α) ↦ x ∈ Set.Iic y) a ay))
        (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Set.Ici x) b xb)),
    ∃ (a : α), IsCoatom a ∧ x ≤ a
⊢ ∃ (a : α), IsCoatom a ∧ x ≤ a

Tactic:
rcases exists_isCompl (xy.symm.IicOrderIsoIci ⟨a, ay⟩) with ⟨⟨b, xb⟩, hb⟩

Premises used: IsCompl.IicOrderIsoIci, ComplementedLattice.exists_isCompl, Subtype.mk, DFunLike.coe, IsCompl.symm
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
inst_3 : ComplementedLattice α
inst_4 : IsAtomic α
x y : α
xy : IsCompl x y
a : α
ha : IsAtom a
ay : a ≤ y
b : α
xb : b ∈ Set.Ici x
hb :
  IsCompl
    ((⋯.IicOrderIsoIci : (a : (↑(Set.Iic y) : Type u_2)) → (↑(Set.Ici x) : Type u_2))
      (Subtype.mk (p := fun (x : α) ↦ x ∈ Set.Iic y) a ay))
    (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Set.Ici x) b xb)
⊢ ∃ (a : α), IsCoatom a ∧ x ≤ a

Tactic:
⟨↑(⟨b, xb⟩ : Set.Ici x), IsCoatom.of_isCoatom_coe_Ici ?_, xb⟩

Premises used: IsCoatom.of_isCoatom_coe_Ici, Subtype.mk, And.intro, Exists.intro, Subtype.val
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
inst_3 : ComplementedLattice α
inst_4 : IsAtomic α
x y : α
xy : IsCompl x y
a : α
ha : IsAtom a
ay : a ≤ y
b : α
xb : b ∈ Set.Ici x
hb :
  IsCompl
    ((⋯.IicOrderIsoIci : (a : (↑(Set.Iic y) : Type u_2)) → (↑(Set.Ici x) : Type u_2))
      (Subtype.mk (p := fun (x : α) ↦ x ∈ Set.Iic y) a ay))
    (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Set.Ici x) b xb)
refine : IsCoatom (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Set.Ici x) b xb)
⊢ ∃ (a : α), IsCoatom a ∧ x ≤ a

Tactic:
refine ⟨↑(⟨b, xb⟩ : Set.Ici x), IsCoatom.of_isCoatom_coe_Ici ?_, xb⟩
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
inst_3 : ComplementedLattice α
inst_4 : IsAtomic α
x y : α
xy : IsCompl x y
a : α
ha : IsAtom a
ay : a ≤ y
b : α
xb : b ∈ Set.Ici x
hb :
  IsCompl
    ((⋯.IicOrderIsoIci : (a : (↑(Set.Iic y) : Type u_2)) → (↑(Set.Ici x) : Type u_2))
      (Subtype.mk (p := fun (x : α) ↦ x ∈ Set.Iic y) a ay))
    (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Set.Ici x) b xb)
rw : IsAtom (α := (↑(Set.Iic y) : Type u_2)) (Subtype.mk (p := fun (x : α) ↦ x ∈ Set.Iic y) a ay)
⊢ IsCoatom (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Set.Ici x) b xb)

Tactic:
rw [← hb.isAtom_iff_isCoatom, OrderIso.isAtom_iff]

Premises used: OrderIso.isAtom_iff, IsCompl.isAtom_iff_isCoatom
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
inst_3 : ComplementedLattice α
inst_4 : IsAtomic α
x y : α
xy : IsCompl x y
a : α
ha : IsAtom a
ay : a ≤ y
b : α
xb : b ∈ Set.Ici x
hb :
  IsCompl
    ((⋯.IicOrderIsoIci : (a : (↑(Set.Iic y) : Type u_2)) → (↑(Set.Ici x) : Type u_2))
      (Subtype.mk (p := fun (x : α) ↦ x ∈ Set.Iic y) a ay))
    (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Set.Ici x) b xb)
⊢ IsAtom (α := (↑(Set.Iic y) : Type u_2)) (Subtype.mk (p := fun (x : α) ↦ x ∈ Set.Iic y) a ay)

Tactic:
apply ha.Iic

Premises used: IsAtom.Iic
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
inst_3 : ComplementedLattice α
inst_4 : IsCoatomic α
⊢ IsAtomic α

Tactic:
isCoatomic_dual_iff_isAtomic.1 isCoatomic_of_isAtomic_of_complementedLattice_of_isModular

Premises used: isCoatomic_dual_iff_isAtomic, Iff.mp, isCoatomic_of_isAtomic_of_complementedLattice_of_isModular
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
inst_3 : ComplementedLattice α
⊢ IsAtomic α ↔ IsCoatomic α

Tactic:
⟨fun _ => isCoatomic_of_isAtomic_of_complementedLattice_of_isModular,
   fun _ => isAtomic_of_isCoatomic_of_complementedLattice_of_isModular⟩

Premises used: isAtomic_of_isCoatomic_of_complementedLattice_of_isModular, Iff.intro, isCoatomic_of_isAtomic_of_complementedLattice_of_isModular
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
inst_3 : ComplementedLattice α
inst_4 : IsAtomic α
a b : α
hab : a < b
obtain :
  ∀ (a' : α) (ha'b : a' ≤ b)
    (ha' :
      IsCompl (α := (↑(Set.Iic b) : Type u_2)) (Subtype.mk (p := fun (x : α) ↦ x ∈ Set.Iic b) a ⋯)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ Set.Iic b) a' ha'b)),
    ∃ (x : α), a ⋖ x ∧ x ≤ b
⊢ ∃ (x : α), a ⋖ x ∧ x ≤ b

Tactic:
obtain ⟨⟨a', ha'b : a' ≤ b⟩, ha'⟩ := exists_isCompl (α := Set.Iic b) ⟨a, hab.le⟩

Premises used: LT.lt.le, ComplementedLattice.exists_isCompl, Subtype.mk
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
inst_3 : ComplementedLattice α
inst_4 : IsAtomic α
a b : α
hab : a < b
a' : α
ha'b : a' ≤ b
ha' :
  IsCompl (α := (↑(Set.Iic b) : Type u_2)) (Subtype.mk (p := fun (x : α) ↦ x ∈ Set.Iic b) a ⋯)
    (Subtype.mk (p := fun (x : α) ↦ x ∈ Set.Iic b) a' ha'b)
inl :
  ∀ (ha'b : ⊥ ≤ b)
    (ha' :
      IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ Set.Iic b) a ⋯)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ Set.Iic b) ⊥ ha'b)),
    ∃ (x : α), a ⋖ x ∧ x ≤ b
inr : ∀ (d : α) (hd : IsAtom d ∧ d ≤ a'), ∃ (x : α), a ⋖ x ∧ x ≤ b
⊢ ∃ (x : α), a ⋖ x ∧ x ≤ b

Tactic:
obtain (rfl | ⟨d, hd⟩) := eq_bot_or_exists_atom_le a'

Premises used: IsAtomic.eq_bot_or_exists_atom_le, rfl
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
inst_3 : ComplementedLattice α
inst_4 : IsAtomic α
a b : α
hab : a < b
ha'b : ⊥ ≤ b
ha' : IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ Set.Iic b) a ⋯) (Subtype.mk (p := fun (x : α) ↦ x ∈ Set.Iic b) ⊥ ha'b)
⊢ a = b

Tactic:
simpa [codisjoint_bot, ← Subtype.coe_inj] using ha'.codisjoint

Premises used: codisjoint_bot, Subtype.coe_inj, IsCompl.codisjoint
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
inst_3 : ComplementedLattice α
inst_4 : IsAtomic α
a b : α
hab : a < b
ha'b : ⊥ ≤ b
ha' : IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ Set.Iic b) a ⋯) (Subtype.mk (p := fun (x : α) ↦ x ∈ Set.Iic b) ⊥ ha'b)
inl :
  ∀ (hab : a < a) (ha'b : ⊥ ≤ a)
    (ha' :
      IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ Set.Iic a) a ⋯)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ Set.Iic a) ⊥ ha'b)),
    ∃ (x : α), a ⋖ x ∧ x ≤ a
⊢ ∃ (x : α), a ⋖ x ∧ x ≤ b

Tactic:
obtain rfl : a = b := by simpa [codisjoint_bot, ← Subtype.coe_inj] using ha'.codisjoint

Premises used: rfl