awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
inst_3 : ComplementedLattice α
inst_4 : IsAtomic α
a : α
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

Tactic:
False.elim <| hab.ne rfl

Premises used: False.elim, rfl, LT.lt.ne
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
inst_3 : ComplementedLattice α
inst_4 : IsAtomic α
a : α
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

Tactic:
exact False.elim <| hab.ne rfl

Premises used: False.elim, rfl, LT.lt.ne
-- 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)
d : α
hd : IsAtom d ∧ d ≤ a'
⊢ ∃ (x : α), a ⋖ x ∧ x ≤ b

Tactic:
⟨d ⊔ a, IsUpperModularLattice.covBy_sup_of_inf_covBy ?_, sup_le (hd.2.trans ha'b) hab.le⟩

Premises used: IsUpperModularLattice.covBy_sup_of_inf_covBy, LT.lt.le, And.right, Max.max, And.intro, Exists.intro, sup_le, LE.le.trans
-- 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)
d : α
hd : IsAtom d ∧ d ≤ a'
inr : d ⊓ a ⋖ d
⊢ ∃ (x : α), a ⋖ x ∧ x ≤ b

Tactic:
refine ⟨d ⊔ a, IsUpperModularLattice.covBy_sup_of_inf_covBy ?_, sup_le (hd.2.trans ha'b) hab.le⟩
-- 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)
d : α
hd : IsAtom d ∧ d ≤ a'
⊢ ⊥ ⋖ d

Tactic:
hd.1.bot_covBy

Premises used: IsAtom.bot_covBy, And.left
-- 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)
d : α
hd : IsAtom d ∧ d ≤ a'
h : d ⊓ a = ⊥
⊢ d ⊓ a ⋖ d

Tactic:
convert! hd.1.bot_covBy

Premises used: IsAtom.bot_covBy, And.left
-- 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)
d : α
hd : IsAtom d ∧ d ≤ a'
⊢ a ⊓ a' = ⊥

Tactic:
simpa using Subtype.coe_inj.2 ha'.inf_eq_bot

Premises used: Iff.mpr, Subtype.coe_inj, IsCompl.inf_eq_bot
-- 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)
d : α
hd : IsAtom d ∧ d ≤ a'
h : a ⊓ d ≤ a ⊓ a'
⊢ d ⊓ a = ⊥

Tactic:
rw [← le_bot_iff, ← show a ⊓ a' = ⊥ by simpa using Subtype.coe_inj.2 ha'.inf_eq_bot, inf_comm]

Premises used: le_bot_iff, inf_comm
-- 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)
d : α
hd : IsAtom d ∧ d ≤ a'
⊢ a ⊓ d ≤ a ⊓ a'

Tactic:
inf_le_inf_left _ hd.2

Premises used: inf_le_inf_left, And.right
-- 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)
d : α
hd : IsAtom d ∧ d ≤ a'
⊢ a ⊓ d ≤ a ⊓ a'

Tactic:
exact inf_le_inf_left _ hd.2

Premises used: inf_le_inf_left, And.right
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
inst_3 : ComplementedLattice α
inst_4 : IsCoatomic α
⊢ IsStronglyCoatomic α

Tactic:
isStronglyAtomic_dual_iff_is_stronglyCoatomic.1 <| ComplementedLattice.isStronglyAtomic

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

Tactic:
rw [isAtomic_iff_isCoatomic] at h

Premises used: isAtomic_iff_isCoatomic
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
inst_3 : ComplementedLattice α
h : IsCoatomic α
⊢ IsStronglyCoatomic α

Tactic:
isStronglyCoatomic

Premises used: ComplementedLattice.isStronglyCoatomic
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
inst_3 : ComplementedLattice α
h : IsCoatomic α
⊢ IsStronglyCoatomic α

Tactic:
exact isStronglyCoatomic

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

Tactic:
rw [← isAtomic_iff_isCoatomic] at h

Premises used: isAtomic_iff_isCoatomic
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
inst_3 : ComplementedLattice α
h : IsAtomic α
⊢ IsStronglyAtomic α

Tactic:
isStronglyAtomic

Premises used: ComplementedLattice.isStronglyAtomic
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
inst_3 : ComplementedLattice α
h : IsAtomic α
⊢ IsStronglyAtomic α

Tactic:
exact isStronglyAtomic

Premises used: ComplementedLattice.isStronglyAtomic
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
p : Prop
⊢ p = ⊥ ∨ p = ⊤

Tactic:
simp [em']

Premises used: em'
-- Module: Mathlib.Order.Atoms
Goal:
p : Prop
⊢ IsAtom p ↔ p

Tactic:
simp
-- Module: Mathlib.Order.Atoms
Goal:
p : Prop
⊢ IsCoatom p ↔ ¬p

Tactic:
simp
-- Module: Mathlib.Order.Atoms
Goal:
ι : Type u_4
π : ι → Type u
inst : (i : ι) → Bot (π i)
f : (i : ι) → π i
⊢ f = ⊥ ↔ ∀ (i : ι), f i = ⊥

Tactic:
funext_iff

Premises used: funext_iff
-- Module: Mathlib.Order.Atoms
Goal:
ι : Type u_4
π : ι → Type u
f : (i : ι) → π i
inst : (i : ι) → PartialOrder (π i)
inst_1 : (i : ι) → OrderBot (π i)
⊢ IsAtom f ↔ ∃ (i : ι), IsAtom (f i) ∧ ∀ (j : ι), j ≠ i → f j = ⊥

Tactic:
simp only [← bot_covBy_iff, Pi.covBy_iff, bot_apply, eq_comm]

Premises used: Pi.bot_apply, Pi.covBy_iff, eq_comm, bot_covBy_iff
-- Module: Mathlib.Order.Atoms
Goal:
ι : Type u_4
π : ι → Type u
i : ι
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (π i)
inst_2 : (i : ι) → OrderBot (π i)
a : π i
h : IsAtom a
⊢ IsAtom (Function.update (β := π) ⊥ i a i)

Tactic:
simpa
-- Module: Mathlib.Order.Atoms
Goal:
ι : Type u_4
π : ι → Type u
inst : DecidableEq ι
inst_1 : (i : ι) → PartialOrder (π i)
inst_2 : (i : ι) → OrderBot (π i)
f : (i : ι) → π i
⊢ IsAtom f ↔ ∃ (i : ι) (a : π i), IsAtom a ∧ f = Function.update (β := π) ⊥ i a

Tactic:
simp [← bot_covBy_iff, covBy_iff_exists_right_eq]

Premises used: Pi.covBy_iff_exists_right_eq, bot_covBy_iff
-- Module: Mathlib.Order.Atoms
Goal:
ι_1 : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst : (i : ι) → PartialOrder (π i)
inst_1 : (i : ι) → OrderBot (π i)
inst_2 : ∀ (i : ι), IsAtomic.{u} (π i)
b : (i : ι) → π i
h : ¬b = ⊥
i : ι
hi : ¬b i = ⊥
a : π i
ha : IsAtom a
hab : a ≤ b i
⊢ ∀ (j : ι), j ≠ i → ⊥ j ≤ b j

Tactic:
simp
-- Module: Mathlib.Order.Atoms
Goal:
ι_1 : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst : (i : ι) → PartialOrder (π i)
inst_1 : (i : ι) → OrderBot (π i)
inst_2 : ∀ (i : ι), IsAtomic.{u} (π i)
b : (i : ι) → π i
h : ¬b = ⊥
i : ι
hi : ¬b i = ⊥
a : π i
ha : IsAtom a
hab : a ≤ b i
⊢ ∃ (a : (i : ι) → π i), IsAtom a ∧ a ≤ b

Tactic:
exact ⟨Function.update ⊥ i a, isAtom_single ha, update_le_iff.2 ⟨hab, by simp⟩⟩
-- Module: Mathlib.Order.Atoms
Goal:
ι_1 : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst : (i : ι) → PartialOrder (π i)
inst_1 : (i : ι) → OrderBot (π i)
inst_2 : ∀ (i : ι), IsAtomic.{u} (π i)
b : (i : ι) → π i
h : ¬b = ⊥
i : ι
hi : ¬b i = ⊥
a : π i
ha : IsAtom a
hab : a ≤ b i
⊢ ∃ (a : (i : ι) → π i), IsAtom a ∧ a ≤ b

Tactic:
classical exact ⟨Function.update ⊥ i a, isAtom_single ha, update_le_iff.2 ⟨hab, by simp⟩⟩
-- Module: Mathlib.Order.Atoms
Goal:
ι_1 : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst : (i : ι) → PartialOrder (π i)
inst_1 : (i : ι) → OrderTop (π i)
inst_2 : ∀ (i : ι), IsCoatomic.{u} (π i)
⊢ IsCoatomic ((i : ι) → π i)

Tactic:
isAtomic_dual_iff_isCoatomic.1 <|
    show IsAtomic (∀ i, (π i)ᵒᵈ) from inferInstance

Premises used: inferInstance, isAtomic_dual_iff_isCoatomic, Iff.mp
-- Module: Mathlib.Order.Atoms
Goal:
ι_1 : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst : (i : ι) → PartialOrder (π i)
inst_1 : (i : ι) → OrderBot (π i)
inst_2 : ∀ (i : ι), IsAtomistic.{u} (π i)
s : (i : ι) → π i
⊢ ∀ (a : (i : ι) → π i), Membership.mem (γ := Set ((i : ι) → π i)) {f : (i : ι) → π i | IsAtom f ∧ f ≤ s} a → IsAtom a

Tactic:
simp +contextual
-- Module: Mathlib.Order.Atoms
Goal:
ι_1 : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst : (i : ι) → PartialOrder (π i)
inst_1 : (i : ι) → OrderBot (π i)
inst_2 : ∀ (i : ι), IsAtomistic.{u} (π i)
s : (i : ι) → π i
refine : IsLUB {f : (i : ι) → π i | IsAtom f ∧ f ≤ s} s
⊢ ∃ (s_1 : Set ((i : ι) → π i)), IsLUB s_1 s ∧ ∀ a ∈ s_1, IsAtom a

Tactic:
refine ⟨{f | IsAtom f ∧ f ≤ s}, ?_, by simp +contextual⟩
-- Module: Mathlib.Order.Atoms
Goal:
ι_1 : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst : (i : ι) → PartialOrder (π i)
inst_1 : (i : ι) → OrderBot (π i)
inst_2 : ∀ (i : ι), IsAtomistic.{u} (π i)
s : (i : ι) → π i
rw : ∀ (a : ι), IsLUB (Function.eval (β := π) a '' {f : (i : ι) → π i | IsAtom f ∧ f ≤ s}) (s a)
⊢ IsLUB {f : (i : ι) → π i | IsAtom f ∧ f ≤ s} s

Tactic:
rw [isLUB_pi]

Premises used: isLUB_pi
-- Module: Mathlib.Order.Atoms
Goal:
ι_1 : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst : (i : ι) → PartialOrder (π i)
inst_1 : (i : ι) → OrderBot (π i)
inst_2 : ∀ (i : ι), IsAtomistic.{u} (π i)
s : (i : ι) → π i
i : ι
simp_rw :
  IsLUB
    (Function.eval (β := π) i ''
      {f : (i : ι) → π i | (∃ (i : ι) (a : π i), IsAtom a ∧ f = Function.update (β := π) ⊥ i a) ∧ f ≤ s})
    (s i)
⊢ IsLUB (Function.eval (β := π) i '' {f : (i : ι) → π i | IsAtom f ∧ f ≤ s}) (s i)

Tactic:
simp_rw [isAtom_iff_eq_single]

Premises used: Pi.isAtom_iff_eq_single
-- Module: Mathlib.Order.Atoms
Goal:
ι_1 : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst : (i : ι) → PartialOrder (π i)
inst_1 : (i : ι) → OrderBot (π i)
inst_2 : ∀ (i : ι), IsAtomistic.{u} (π i)
s : (i : ι) → π i
i : ι
⊢ IsLUB
    (Function.eval (β := π) i ''
      {f : (i : ι) → π i | (∃ (i : ι) (a : π i), IsAtom a ∧ f = Function.update (β := π) ⊥ i a) ∧ f ≤ s})
    (s i)

Tactic:
⟨?_, ?_⟩

Premises used: IsLeast, And.intro, IsLUB
-- Module: Mathlib.Order.Atoms
Goal:
ι_1 : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst : (i : ι) → PartialOrder (π i)
inst_1 : (i : ι) → OrderBot (π i)
inst_2 : ∀ (i : ι), IsAtomistic.{u} (π i)
s : (i : ι) → π i
i : ι
refine_1 :
  Membership.mem (γ := Set (π i))
    (upperBounds
      (Function.eval (β := π) i ''
        {f : (i : ι) → π i | (∃ (i : ι) (a : π i), IsAtom a ∧ f = Function.update (β := π) ⊥ i a) ∧ f ≤ s}))
    (s i)
refine_2 :
  Membership.mem (γ := Set (π i))
    (lowerBounds
      (upperBounds
        (Function.eval (β := π) i ''
          {f : (i : ι) → π i | (∃ (i : ι) (a : π i), IsAtom a ∧ f = Function.update (β := π) ⊥ i a) ∧ f ≤ s})))
    (s i)
⊢ IsLUB
    (Function.eval (β := π) i ''
      {f : (i : ι) → π i | (∃ (i : ι) (a : π i), IsAtom a ∧ f = Function.update (β := π) ⊥ i a) ∧ f ≤ s})
    (s i)

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.Order.Atoms
Goal:
ι_1 : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst : (i : ι) → PartialOrder (π i)
inst_1 : (i : ι) → OrderBot (π i)
inst_2 : ∀ (i : ι), IsAtomistic.{u} (π i)
s : (i : ι) → π i
i w : ι
w_1 : π w
left : IsAtom w_1
hs : Function.update (β := π) ⊥ w w_1 ≤ s
⊢ Function.eval (β := π) i (Function.update (β := π) ⊥ w w_1) ≤ s i

Tactic:
hs i
-- Module: Mathlib.Order.Atoms
Goal:
ι_1 : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst : (i : ι) → PartialOrder (π i)
inst_1 : (i : ι) → OrderBot (π i)
inst_2 : ∀ (i : ι), IsAtomistic.{u} (π i)
s : (i : ι) → π i
i w : ι
w_1 : π w
left : IsAtom w_1
hs : Function.update (β := π) ⊥ w w_1 ≤ s
⊢ Function.eval (β := π) i (Function.update (β := π) ⊥ w w_1) ≤ s i

Tactic:
exact hs i
-- Module: Mathlib.Order.Atoms
Goal:
ι_1 : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst : (i : ι) → PartialOrder (π i)
inst_1 : (i : ι) → OrderBot (π i)
inst_2 : ∀ (i : ι), IsAtomistic.{u} (π i)
s : (i : ι) → π i
i : ι
⊢ Membership.mem (γ := Set (π i))
    (lowerBounds
      (upperBounds
        (Function.eval (β := π) i ''
          {f : (i : ι) → π i | (∃ (i : ι) (a : π i), IsAtom a ∧ f = Function.update (β := π) ⊥ i a) ∧ f ≤ s})))
    (s i)

Tactic:
fun j hj ↦ (isLUB_atoms_le (s i)).2 fun x ⟨hx₁, hx₂⟩ ↦ ?_

Premises used: _private.0.Pi.isAtomistic.match_1, lowerBounds, Set.Mem, setOf, LE.le, And.right, isLUB_atoms_le
-- Module: Mathlib.Order.Atoms
Goal:
ι_1 : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst : (i : ι) → PartialOrder (π i)
inst_1 : (i : ι) → OrderBot (π i)
inst_2 : ∀ (i : ι), IsAtomistic.{u} (π i)
s : (i : ι) → π i
i : ι
refine_2 :
  ∀ (j : π i)
    (hj :
      Membership.mem (γ := Set (π i))
        (upperBounds
          (Function.eval (β := π) i ''
            {f : (i : ι) → π i | (∃ (i : ι) (a : π i), IsAtom a ∧ f = Function.update (β := π) ⊥ i a) ∧ f ≤ s}))
        j)
    (x : π i),
    Membership.mem (γ := Set (π i)) {a : π i | IsAtom a ∧ a ≤ s i} x → ∀ (hx₁ : IsAtom x) (hx₂ : x ≤ s i), x ≤ j
⊢ Membership.mem (γ := Set (π i))
    (lowerBounds
      (upperBounds
        (Function.eval (β := π) i ''
          {f : (i : ι) → π i | (∃ (i : ι) (a : π i), IsAtom a ∧ f = Function.update (β := π) ⊥ i a) ∧ f ≤ s})))
    (s i)

Tactic:
refine fun j hj ↦ (isLUB_atoms_le (s i)).2 fun x ⟨hx₁, hx₂⟩ ↦ ?_

Premises used: _private.0.Pi.isAtomistic.match_1, LE.le, And.right, isLUB_atoms_le
-- Module: Mathlib.Order.Atoms
Goal:
ι_1 : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst : (i : ι) → PartialOrder (π i)
inst_1 : (i : ι) → OrderBot (π i)
inst_2 : ∀ (i : ι), IsAtomistic.{u} (π i)
s : (i : ι) → π i
i : ι
j : π i
hj :
  Membership.mem (γ := Set (π i))
    (upperBounds
      (Function.eval (β := π) i ''
        {f : (i : ι) → π i | (∃ (i : ι) (a : π i), IsAtom a ∧ f = Function.update (β := π) ⊥ i a) ∧ f ≤ s}))
    j
x : π i
h : Membership.mem (γ := Set (π i)) {a : π i | IsAtom a ∧ a ≤ s i} x
hx₁ : IsAtom x
hx₂ : x ≤ s i
⊢ Function.update (β := π) ⊥ i x ≤ s

Tactic:
simp [update_le_iff, hx₂]

Premises used: update_le_iff
-- Module: Mathlib.Order.Atoms
Goal:
ι_1 : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst : (i : ι) → PartialOrder (π i)
inst_1 : (i : ι) → OrderBot (π i)
inst_2 : ∀ (i : ι), IsAtomistic.{u} (π i)
s : (i : ι) → π i
i : ι
j : π i
hj :
  Membership.mem (γ := Set (π i))
    (upperBounds
      (Function.eval (β := π) i ''
        {f : (i : ι) → π i | (∃ (i : ι) (a : π i), IsAtom a ∧ f = Function.update (β := π) ⊥ i a) ∧ f ≤ s}))
    j
x : π i
h : Membership.mem (γ := Set (π i)) {a : π i | IsAtom a ∧ a ≤ s i} x
hx₁ : IsAtom x
hx₂ : x ≤ s i
⊢ Function.eval (β := π) i (Function.update (β := π) ⊥ i x) = x

Tactic:
simp
-- Module: Mathlib.Order.Atoms
Goal:
ι_1 : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst : (i : ι) → PartialOrder (π i)
inst_1 : (i : ι) → OrderBot (π i)
inst_2 : ∀ (i : ι), IsAtomistic.{u} (π i)
s : (i : ι) → π i
i : ι
j : π i
hj :
  Membership.mem (γ := Set (π i))
    (upperBounds
      (Function.eval (β := π) i ''
        {f : (i : ι) → π i | (∃ (i : ι) (a : π i), IsAtom a ∧ f = Function.update (β := π) ⊥ i a) ∧ f ≤ s}))
    j
x : π i
h : Membership.mem (γ := Set (π i)) {a : π i | IsAtom a ∧ a ≤ s i} x
hx₁ : IsAtom x
hx₂ : x ≤ s i
⊢ x ≤ j

Tactic:
exact hj ⟨Function.update ⊥ i x, ⟨⟨_, x, hx₁, rfl⟩, by simp [update_le_iff, hx₂]⟩, by simp⟩

Premises used: Function.update, Bot.bot, And.intro, Exists.intro, rfl
-- Module: Mathlib.Order.Atoms
Goal:
ι_1 : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst : (i : ι) → PartialOrder (π i)
inst_1 : (i : ι) → OrderBot (π i)
inst_2 : ∀ (i : ι), IsAtomistic.{u} (π i)
s : (i : ι) → π i
refine : IsLUB {f : (i : ι) → π i | IsAtom f ∧ f ≤ s} s
refine₁ refine₂ : ∀ (i : ι), IsLUB (Function.eval (β := π) i '' {f : (i : ι) → π i | IsAtom f ∧ f ≤ s}) (s i)
refine₃ :
  ∀ (i : ι),
    IsLUB
      (Function.eval (β := π) i ''
        {f : (i : ι) → π i | (∃ (i : ι) (a : π i), IsAtom a ∧ f = Function.update (β := π) ⊥ i a) ∧ f ≤ s})
      (s i)
refine_1 :
  ∀ (i : ι),
    Membership.mem (γ := Set (π i))
      (upperBounds
        (Function.eval (β := π) i ''
          {f : (i : ι) → π i | (∃ (i : ι) (a : π i), IsAtom a ∧ f = Function.update (β := π) ⊥ i a) ∧ f ≤ s}))
      (s i)
refine_2 refine_2₁ :
  ∀ (i : ι),
    Membership.mem (γ := Set (π i))
      (lowerBounds
        (upperBounds
          (Function.eval (β := π) i ''
            {f : (i : ι) → π i | (∃ (i : ι) (a : π i), IsAtom a ∧ f = Function.update (β := π) ⊥ i a) ∧ f ≤ s})))
      (s i)
⊢ ∃ (s_1 : Set ((i : ι) → π i)), IsLUB s_1 s ∧ ∀ a ∈ s_1, IsAtom a

Tactic:
classical
    refine ⟨{f | IsAtom f ∧ f ≤ s}, ?_, by simp +contextual⟩
    rw [isLUB_pi]
    intro i
    simp_rw [isAtom_iff_eq_single]
    refine ⟨?_, ?_⟩
    · rintro _ ⟨_, ⟨⟨_, _, _, rfl⟩, hs⟩, rfl⟩
      exact hs i
    · refine fun j hj ↦ (isLUB_atoms_le (s i)).2 fun x ⟨hx₁, hx₂⟩ ↦ ?_
      exact hj ⟨Function.update ⊥ i x, ⟨⟨_, x, hx₁, rfl⟩, by simp [update_le_iff, hx₂]⟩, by simp⟩

Premises used: Pi.isAtom_iff_eq_single, isLUB_pi, rfl
-- Module: Mathlib.Order.Atoms
Goal:
ι_1 : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst : (i : ι) → CompleteLattice (π i)
inst_1 : ∀ (i : ι), IsCoatomistic.{u} (π i)
⊢ IsCoatomistic ((i : ι) → π i)

Tactic:
isAtomistic_dual_iff_isCoatomistic.1 <|
    show IsAtomistic (∀ i, (π i)ᵒᵈ) from inferInstance

Premises used: inferInstance, isAtomistic_dual_iff_isCoatomistic, Iff.mp
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : BooleanAlgebra α
a : α
⊢ IsAtom aᶜ ↔ IsCoatom a

Tactic:
isCompl_compl.symm.isAtom_iff_isCoatom

Premises used: isCompl_compl, IsCompl.isAtom_iff_isCoatom, IsCompl.symm
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
inst : BooleanAlgebra α
a : α
⊢ IsCoatom aᶜ ↔ IsAtom a

Tactic:
isCompl_compl.symm.isCoatom_iff_isAtom

Premises used: IsCompl.isCoatom_iff_isAtom, isCompl_compl, IsCompl.symm
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
x : α
⊢ IsAtom (α := Set α) {x}

Tactic:
⟨singleton_ne_empty _, fun _ hs => ssubset_singleton_iff.mp hs⟩

Premises used: And.intro, Iff.mp, IsAtom, Set.ssubset_singleton_iff, Set.singleton_ne_empty
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
x : α
⊢ IsAtom (α := Set α) {x}

Tactic:
isAtom_singleton x

Premises used: Set.isAtom_singleton
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
x : α
⊢ IsAtom (α := Set α) {x}

Tactic:
exact isAtom_singleton x

Premises used: Set.isAtom_singleton
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
s : Set α
rintro : IsAtom s → ∃ (x : α), s = {x}
⊢ IsAtom s ↔ ∃ (x : α), s = {x}

Tactic:
refine
    ⟨?_, by
      rintro ⟨x, rfl⟩
      exact isAtom_singleton x⟩
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
s : Set α
rw : (s.Nonempty ∧ ∀ (b : Set α), b ≠ ∅ → b ≤ s → s ≤ b) → ∃ (x : α), s = {x}
⊢ IsAtom s → ∃ (x : α), s = {x}

Tactic:
rw [isAtom_iff_le_of_ge, bot_eq_empty, ← nonempty_iff_ne_empty]

Premises used: Set.bot_eq_empty, Set.nonempty_iff_ne_empty, isAtom_iff_le_of_ge
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
s : Set α
hs : ∀ (b : Set α), b ≠ ∅ → b ≤ s → s ≤ b
x : α
hx : x ∈ s
⊢ ∃ (x : α), s = {x}

Tactic:
⟨x, eq_singleton_iff_unique_mem.2
        ⟨hx, fun y hy => (hs {y} (singleton_ne_empty _) (singleton_subset_iff.2 hy) hx).symm⟩⟩

Premises used: Iff.mpr, Set.singleton_subset_iff, And.intro, Exists.intro, Set.eq_singleton_iff_unique_mem, Singleton.singleton, Eq.symm, Set.singleton_ne_empty
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
s : Set α
hs : ∀ (b : Set α), b ≠ ∅ → b ≤ s → s ≤ b
x : α
hx : x ∈ s
⊢ ∃ (x : α), s = {x}

Tactic:
exact
    ⟨x, eq_singleton_iff_unique_mem.2
        ⟨hx, fun y hy => (hs {y} (singleton_ne_empty _) (singleton_subset_iff.2 hy) hx).symm⟩⟩
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
s : Set α
rw : (∃ (x : α), sᶜ = {x}) ↔ ∃ (x : α), s = {x}ᶜ
⊢ IsCoatom s ↔ ∃ (x : α), s = {x}ᶜ

Tactic:
rw [isCompl_compl.isCoatom_iff_isAtom, isAtom_iff]

Premises used: IsCompl.isCoatom_iff_isAtom, Set.isAtom_iff, isCompl_compl
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
s : Set α
simp_rw : (∃ (x : α), sᶜ = {x}) ↔ ∃ (x : α), {x}ᶜ = s
⊢ (∃ (x : α), sᶜ = {x}) ↔ ∃ (x : α), s = {x}ᶜ

Tactic:
simp_rw [@eq_comm _ s, compl_eq_comm]

Premises used: eq_comm, compl_eq_comm
-- Module: Mathlib.Order.Atoms
Goal:
α : Type u_2
x : α
⊢ IsCoatom (α := Set α) {x}ᶜ

Tactic:
(isCoatom_iff {x}ᶜ).mpr ⟨x, rfl⟩

Premises used: Iff.mpr, Compl.compl, Set.isCoatom_iff, Exists.intro, Singleton.singleton, rfl
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
⊢ IsAtomistic.{u_2} (Set α)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Order.Atoms
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
⊢ IsCoatomistic.{u_2} (Set α)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LE α
a b : α
h : a ≤ b
⊢ b ≥ a

Tactic:
h
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LE α
a b : α
h : a ≥ b
⊢ b ≤ a

Tactic:
h
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LE α
a b c : α
⊢ b ≤ c → a = b → a ≤ c

Tactic:
flip le_of_eq_of_le

Premises used: flip, le_of_eq_of_le
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LE α
a b c : α
⊢ b = c → a ≤ b → a ≤ c

Tactic:
flip le_of_le_of_eq

Premises used: le_of_le_of_eq, flip
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LT α
a b : α
h : a < b
⊢ b > a

Tactic:
h
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LT α
a b : α
h : a > b
⊢ b < a

Tactic:
h
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LT α
a b c : α
⊢ b < c → a = b → a < c

Tactic:
flip lt_of_eq_of_lt

Premises used: flip, lt_of_eq_of_lt
-- Module: Mathlib.Order.Basic
Goal:
α : Type u_2
inst : LT α
a b c : α
⊢ b = c → a < b → a < c

Tactic:
flip lt_of_lt_of_eq

Premises used: flip, lt_of_lt_of_eq