awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
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
⊢ IsAtom (u b) ↔ IsAtom b
have rw₁ : IsAtom b ↔ IsAtom b
Tactic: rw [← gi.isAtom_iff hbot h_atom, gi.l_u_eq]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
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
have refine : ∀ (hb : IsCoatom b), IsCoatom (u b)
Tactic: refine ⟨fun hb => gi.isCoatom_of_image hb, fun hb => ?_⟩
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
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
⊢ IsCoatom (u b)
have obtain : ∀ (a : α) (ha : IsCoatom a) (hab : u b ≤ a), 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
-- Lean 4 proof step from Mathlib.Order.Atoms (hypothesis)
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
⊢ IsCoatom (u b)
have this : 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)
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : PartialOrder β
inst_2 : BoundedOrder α
inst_3 : BoundedOrder β
f : α ≃o β
⊢ IsSimpleOrder α ↔ IsSimpleOrder β
have rw : IsAtom.{u_2} (α := α) ⊤ ↔ IsSimpleOrder β
Tactic: rw [isSimpleOrder_iff_isAtom_top, isSimpleOrder_iff_isAtom_top, ← f.isAtom_iff ⊤,
    f.map_top]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
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 β
⊢ IsSimpleOrder α ↔ IsSimpleOrder β
have rw₁ : IsAtom.{u_2} (α := α) ⊤ ↔ IsAtom.{u_3} (α := β) ⊤
Tactic: rw [isSimpleOrder_iff_isAtom_top, isSimpleOrder_iff_isAtom_top, ← f.isAtom_iff ⊤,
    f.map_top]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
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} (α := β) ⊤
⊢ IsSimpleOrder α ↔ IsSimpleOrder β
have rw₂ : IsAtom.{u_3} (α := β) ((f : (a : α) → β) ⊤ : β) ↔ IsAtom.{u_3} (α := β) ⊤
Tactic: rw [isSimpleOrder_iff_isAtom_top, isSimpleOrder_iff_isAtom_top, ← f.isAtom_iff ⊤,
    f.map_top]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
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} (α := β) ⊤
⊢ IsSimpleOrder α ↔ IsSimpleOrder β
have rw₃ : IsAtom.{u_3} (α := β) ⊤ ↔ IsAtom.{u_3} (α := β) ⊤
Tactic: rw [isSimpleOrder_iff_isAtom_top, isSimpleOrder_iff_isAtom_top, ← f.isAtom_iff ⊤,
    f.map_top]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_2
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsUpperModularLattice α
inst_3 : IsAtomistic α
a b : α
hab : a < b
⊢ ∃ (x : α), a ⋖ x ∧ x ≤ b
have obtain : ∀ (s : Set α) (hsb : IsLUB s b) (h : ∀ a ∈ s, IsAtom a), ∃ (x : α), a ⋖ x ∧ x ≤ b
Tactic: obtain ⟨s, hsb, h⟩ := isLUB_atoms b
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
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
have refine : ∀ (hcon : ¬∃ (x : α), a ⋖ x ∧ x ≤ b) (x : α) (hx : x ∈ s), x ≤ a
Tactic: refine by_contra fun hcon ↦ hab.not_ge <| (isLUB_le_iff hsb).2 fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Order.Atoms (hypothesis)
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 ≤ a
have hcon₁ : ∀ x ≤ b, ¬a ⋖ x
Tactic: simp_rw [not_exists, and_comm (b := _ ≤ _), not_and] at hcon
Cleared hypotheses: hcon
-- Lean 4 proof step from Mathlib.Order.Atoms (hypothesis)
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
⊢ x ≤ a
have hcon₁ : ¬a ⋖ x ⊔ a
Tactic: specialize hcon (x ⊔ a) (sup_le (hsb.1 hx) hab.le)
Cleared hypotheses: hcon
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
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
have inl : ∀ (hbot : x ⊓ a = ⊥), x ≤ a
Tactic: obtain (hbot | h_inf) := (h x hx).bot_covBy.eq_or_eq (c := x ⊓ a) (by simp) (by simp)
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
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
⊢ x ≤ a
have inr : ∀ (h_inf : x ⊓ a = x), x ≤ a
Tactic: obtain (hbot | h_inf) := (h x hx).bot_covBy.eq_or_eq (c := x ⊓ a) (by simp) (by simp)
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
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
⊢ x ≤ a
have inr : ∀ (h_inf : x ≤ a), x ≤ a
Tactic: rwa [inf_eq_left] at h_inf
Cleared hypotheses: h_inf
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_2
inst : Lattice α
inst_1 : OrderTop α
inst_2 : IsLowerModularLattice α
inst_3 : IsCoatomistic α
⊢ IsStronglyCoatomic α
have rw : IsStronglyAtomic.{u_2} αᵒᵈ
Tactic: rw [← isStronglyAtomic_dual_iff_is_stronglyCoatomic]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_2
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
inst_3 : ComplementedLattice α
inst_4 : IsAtomic α
x : α
⊢ x = ⊤ ∨ ∃ (a : α), IsCoatom a ∧ x ≤ a
have rcases : ∀ (y : α) (xy : IsCompl x y), x = ⊤ ∨ ∃ (a : α), IsCoatom a ∧ x ≤ a
Tactic: rcases exists_isCompl x with ⟨y, xy⟩
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_2
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
inst_3 : ComplementedLattice α
inst_4 : IsAtomic α
x y : α
xy : IsCompl x y
⊢ x = ⊤ ∨ ∃ (a : α), IsCoatom a ∧ x ≤ a
have apply : y = ⊥ → x = ⊤
Tactic: apply (eq_bot_or_exists_atom_le y).imp _ _
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
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 = ⊤
⊢ x = ⊤ ∨ ∃ (a : α), IsCoatom a ∧ x ≤ a
have apply₁ : (∃ (a : α), IsAtom a ∧ a ≤ y) → ∃ (a : α), IsCoatom a ∧ x ≤ a
Tactic: apply (eq_bot_or_exists_atom_le y).imp _ _
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
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
⊢ ∃ (a : α), IsCoatom a ∧ x ≤ a
have rcases : ∀ (b : α) (xb : b ∈ Set.Ici x)
  (hb :
    IsCompl
      ((sorry.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: rcases exists_isCompl (xy.symm.IicOrderIsoIci ⟨a, ay⟩) with ⟨⟨b, xb⟩, hb⟩
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
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
have refine : IsCoatom (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Set.Ici x) b xb)
Tactic: refine ⟨↑(⟨b, xb⟩ : Set.Ici x), IsCoatom.of_isCoatom_coe_Ici ?_, xb⟩
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
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)
⊢ IsCoatom (Subtype.mk (p := fun (x_1 : α) ↦ x_1 ∈ Set.Ici x) b xb)
have rw : IsAtom (α := (↑(Set.Iic y) : Type u_2)) (Subtype.mk (p := fun (x : α) ↦ x ∈ Set.Iic y) a ay)
Tactic: rw [← hb.isAtom_iff_isCoatom, OrderIso.isAtom_iff]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_2
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
inst_3 : ComplementedLattice α
inst_4 : IsAtomic α
a b : α
hab : a < b
⊢ ∃ (x : α), a ⋖ x ∧ x ≤ b
have obtain : ∀ (a' : α) (ha'b : a' ≤ b)
  (ha' :
    IsCompl (α := (↑(Set.Iic b) : Type u_2)) (Subtype.mk (p := fun (x : α) ↦ x ∈ Set.Iic b) a sorry)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ Set.Iic b) a' ha'b)),
  ∃ (x : α), a ⋖ x ∧ x ≤ b
Tactic: obtain ⟨⟨a', ha'b : a' ≤ b⟩, ha'⟩ := exists_isCompl (α := Set.Iic b) ⟨a, hab.le⟩
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
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)
⊢ ∃ (x : α), a ⋖ x ∧ x ≤ b
have inl : ∀ (ha'b : ⊥ ≤ b)
  (ha' :
    IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ Set.Iic b) a sorry) (Subtype.mk (p := fun (x : α) ↦ x ∈ Set.Iic b) ⊥ ha'b)),
  ∃ (x : α), a ⋖ x ∧ x ≤ b
Tactic: obtain (rfl | ⟨d, hd⟩) := eq_bot_or_exists_atom_le a'
Cleared hypotheses: a', ha'b, ha'
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
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
⊢ ∃ (x : α), a ⋖ x ∧ x ≤ b
have inr : ∀ (d : α) (hd : IsAtom d ∧ d ≤ a'), ∃ (x : α), a ⋖ x ∧ x ≤ b
Tactic: obtain (rfl | ⟨d, hd⟩) := eq_bot_or_exists_atom_le a'
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
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)
⊢ ∃ (x : α), a ⋖ x ∧ x ≤ b
have inl : ∀ (hab : a < a) (ha'b : ⊥ ≤ a)
  (ha' :
    IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ Set.Iic a) a sorry) (Subtype.mk (p := fun (x : α) ↦ x ∈ Set.Iic a) ⊥ ha'b)),
  ∃ (x : α), a ⋖ x ∧ x ≤ a
Tactic: obtain rfl : a = b := by simpa [codisjoint_bot, ← Subtype.coe_inj] using ha'.codisjoint
Cleared hypotheses: b, hab, ha'b, ha'
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
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
have inr : d ⊓ a ⋖ d
Tactic: refine ⟨d ⊔ a, IsUpperModularLattice.covBy_sup_of_inf_covBy ?_, sup_le (hd.2.trans ha'b) hab.le⟩
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
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 ⊓ a ⋖ d
have h : d ⊓ a = ⊥
Tactic: convert! hd.1.bot_covBy
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
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 ⊓ a = ⊥
have h : a ⊓ d ≤ a ⊓ a'
Tactic: rw [← le_bot_iff, ← show a ⊓ a' = ⊥ by simpa using Subtype.coe_inj.2 ha'.inf_eq_bot, inf_comm]
-- Lean 4 proof step from Mathlib.Order.Atoms (hypothesis)
Goal:
α : Type u_2
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
inst_3 : ComplementedLattice α
h : IsAtomic α
⊢ IsStronglyCoatomic α
have h₁ : IsCoatomic α
Tactic: rw [isAtomic_iff_isCoatomic] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Atoms (hypothesis)
Goal:
α : Type u_2
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
inst_3 : ComplementedLattice α
h : IsCoatomic α
⊢ IsStronglyAtomic α
have h₁ : IsAtomic α
Tactic: rw [← isAtomic_iff_isCoatomic] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
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
⊢ ∃ (s_1 : Set ((i : ι) → π i)), IsLUB s_1 s ∧ ∀ a ∈ s_1, IsAtom a
have refine : IsLUB {f : (i : ι) → π i | IsAtom f ∧ f ≤ s} s
Tactic: refine ⟨{f | IsAtom f ∧ f ≤ s}, ?_, by simp +contextual⟩
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
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
⊢ IsLUB {f : (i : ι) → π i | IsAtom f ∧ f ≤ s} s
have rw : ∀ (a : ι), IsLUB (Function.eval (β := π) a '' {f : (i : ι) → π i | IsAtom f ∧ f ≤ s}) (s a)
Tactic: rw [isLUB_pi]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
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 | IsAtom f ∧ f ≤ s}) (s i)
have simp_rw : IsLUB
  (Function.eval (β := π) i ''
    {f : (i : ι) → π i | (∃ (i : ι) (a : π i), IsAtom a ∧ f = Function.update (β := π) ⊥ i a) ∧ f ≤ s})
  (s i)
Tactic: simp_rw [isAtom_iff_eq_single]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
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)
have 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)
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
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)
⊢ IsLUB
    (Function.eval (β := π) i ''
      {f : (i : ι) → π i | (∃ (i : ι) (a : π i), IsAtom a ∧ f = Function.update (β := π) ⊥ i a) ∧ f ≤ s})
    (s i)
have 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)
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
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)
have 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
Tactic: refine fun j hj ↦ (isLUB_atoms_le (s i)).2 fun x ⟨hx₁, hx₂⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
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
⊢ ∃ (s_1 : Set ((i : ι) → π i)), IsLUB s_1 s ∧ ∀ a ∈ s_1, IsAtom a
have refine : IsLUB {f : (i : ι) → π i | IsAtom f ∧ f ≤ s} s
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⟩
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
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
have refine₁ : ∀ (a : ι), IsLUB (Function.eval (β := π) a '' {f : (i : ι) → π i | IsAtom f ∧ f ≤ s}) (s 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⟩
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
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)
⊢ ∃ (s_1 : Set ((i : ι) → π i)), IsLUB s_1 s ∧ ∀ a ∈ s_1, IsAtom a
have refine₃ : ∀ (i : ι),
  IsLUB
    (Function.eval (β := π) i ''
      {f : (i : ι) → π i | (∃ (i : ι) (a : π i), IsAtom a ∧ f = Function.update (β := π) ⊥ i a) ∧ f ≤ s})
    (s i)
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⟩
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
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)
⊢ ∃ (s_1 : Set ((i : ι) → π i)), IsLUB s_1 s ∧ ∀ a ∈ s_1, IsAtom a
have 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)
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⟩