awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_2
inst : PartialOrder α
a : α
b : (↑(Ici a) : Type u_2)
⊢ ⊥ ⋖ b ↔ a ⋖ (↑b : α)
have refine : OrdConnected.{u_2} (α := α)
  (range (ι := { c : α // a ≤ c }) (⇑(OrderEmbedding.subtype fun (c : α) ↦ a ≤ c) : (a : { c : α // a ≤ c }) → α))
Tactic: refine (Set.OrdConnected.apply_covBy_apply_iff (OrderEmbedding.subtype fun c => a ≤ c) ?_).symm
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_2
inst : PartialOrder α
b : α
a : (↑(Iic b) : Type u_2)
⊢ IsCoatom a ↔ (↑a : α) ⋖ b
have rw : a ⋖ ⊤ ↔ (↑a : α) ⋖ b
Tactic: rw [← covBy_top_iff]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_2
inst : PartialOrder α
b : α
a : (↑(Iic b) : Type u_2)
⊢ a ⋖ ⊤ ↔ (↑a : α) ⋖ b
have refine : OrdConnected.{u_2} (α := α)
  (range (ι := { c : α // c ≤ b }) (⇑(OrderEmbedding.subtype fun (c : α) ↦ c ≤ b) : (a : { c : α // c ≤ b }) → α))
Tactic: refine (Set.OrdConnected.apply_covBy_apply_iff (OrderEmbedding.subtype fun c => c ≤ b) ?_).symm
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_2
inst : SemilatticeInf α
inst_1 : OrderBot α
a b : α
ha : IsAtom a
⊢ ¬Disjoint a b ↔ a ≤ b
have rw : ¬a ⊓ b = ⊥ ↔ a ⊓ b = a
Tactic: rw [disjoint_iff, ← inf_eq_left]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_2
inst : SemilatticeSup α
inst_1 : OrderTop α
a b : α
ha : IsCoatom a
⊢ ¬Codisjoint a b ↔ b ≤ a
have rw : ¬a ⊔ b = ⊤ ↔ a ⊔ b = a
Tactic: rw [codisjoint_iff, ← sup_eq_left]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_4
inst : Preorder α
⊢ IsStronglyCoatomic.{u_4} αᵒᵈ ↔ IsStronglyAtomic α
have rw : IsStronglyAtomic.{u_4} αᵒᵈᵒᵈ ↔ IsStronglyAtomic α
Tactic: rw [← isStronglyAtomic_dual_iff_is_stronglyCoatomic]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
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_2 : α), IsAtom a_2 ∧ a_2 ≤ a
have rw : ⊥ < a → ∃ (a_3 : α), IsAtom a_3 ∧ a_3 ≤ a
Tactic: rw [or_iff_not_imp_left, ← Ne, ← bot_lt_iff_ne_bot]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
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
⊢ ∃ (a_2 : α), IsAtom a_2 ∧ a_2 ≤ a
have obtain : ∀ (x : α) (hx : ⊥ ⋖ x) (hxa : x ≤ a), ∃ (a_2 : α), IsAtom a_2 ∧ a_2 ≤ a
Tactic: obtain ⟨x, hx, hxa⟩ := hlt.exists_covby_le
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
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 : (↑s : Type u_4)),
    Subtype.mk (p := fun (x : α) ↦ x ∈ s) c hc ⋖ x ∧ x ≤ Subtype.mk (p := fun (x : α) ↦ x ∈ s) d hd
have 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
Tactic: obtain ⟨x, hcx, hxd⟩ := (Subtype.mk_lt_mk.1 hcd).exists_covby_le
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
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 α
⊢ IsStronglyCoatomic α
have rw : IsStronglyAtomic.{u_4} αᵒᵈ
Tactic: rw [← isStronglyAtomic_dual_iff_is_stronglyCoatomic]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_2
inst : PartialOrder α
h : WellFounded fun (x1 x2 : α) ↦ x1 < x2
a b : α
hab : a < b
⊢ ∃ (x : α), a ⋖ x ∧ x ≤ b
have refine : a ⋖ h.min (r := fun (x1 x2 : α) ↦ x1 < x2) (Set.Ioc a b) sorry ∧ h.min (r := fun (x1 x2 : α) ↦ x1 < x2) (Set.Ioc a b) sorry ≤ b
Tactic: refine ⟨WellFounded.min h (Set.Ioc a b) ⟨b, hab,rfl.le⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Atoms (hypothesis)
Goal:
α : Type u_2
inst : PartialOrder α
h : WellFounded fun (x1 x2 : α) ↦ x1 < x2
a b : α
hab : a < b
⊢ a ⋖ h.min (r := fun (x1 x2 : α) ↦ x1 < x2) (Set.Ioc a b) ⋯ ∧
    h.min (r := fun (x1 x2 : α) ↦ x1 < x2) (Set.Ioc a b) ⋯ ≤ b
have hmem : h.min (r := fun (x1 x2 : α) ↦ x1 < x2) (Set.Ioc a b) sorry ∈ Set.Ioc a b
Tactic: have hmem := (WellFounded.min_mem h (Set.Ioc a b) ⟨b, hab,rfl.le⟩)
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_4
inst : BooleanAlgebra α
inst_1 : IsAtomic α
x y : α
⊢ x ≤ y ↔ ∀ (a : α), IsAtom a → a ≤ x → a ≤ y
have refine : ∀ (h : ∀ (a : α), IsAtom a → a ≤ x → a ≤ y), x ≤ y
Tactic: refine ⟨fun h a _ => (le_trans · h), fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Order.Atoms (hypothesis)
Goal:
α : Type u_4
inst : BooleanAlgebra α
inst_1 : IsAtomic α
x y : α
h : ∀ (a : α), IsAtom a → a ≤ x → a ≤ y
⊢ x ≤ y
have this : x ⊓ yᶜ = ⊥
Tactic: have : x ⊓ yᶜ = ⊥ := of_not_not fun hbot =>
    have ⟨a, ha, hle⟩ := (eq_bot_or_exists_atom_le _).resolve_left hbot
    have ⟨hx, hy'⟩ := le_inf_iff.1 hle
    have hy := h a ha hx
    have : a ≤ y ⊓ yᶜ := le_inf_iff.2 ⟨hy, hy'⟩
    ha.1 (by simpa using this)
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_4
inst : BooleanAlgebra α
inst_1 : IsAtomic α
x y : α
⊢ x = y ↔ ∀ (a : α), IsAtom a → (a ≤ x ↔ a ≤ y)
have refine : ∀ (h : ∀ (a : α), IsAtom a → (a ≤ x ↔ a ≤ y)), x = y
Tactic: refine ⟨fun h => h ▸ by simp, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : OrderBot α
inst_2 : IsAtomistic α
b : α
⊢ b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b
have rcases : ∀ (s : Set α) (hsb : IsLUB s b) (hs : ∀ a ∈ s, IsAtom a), b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b
Tactic: rcases isLUB_atoms b with ⟨s, hsb, hs⟩
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : OrderBot α
inst_2 : IsAtomistic α
b : α
s : Set α
hsb : IsLUB s b
hs : ∀ a ∈ s, IsAtom a
⊢ b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b
have inl : ∀ (hsb : IsLUB ∅ b) (hs : ∀ (a : α), Membership.mem (γ := Set α) ∅ a → IsAtom a), b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b
Tactic: rcases s.eq_empty_or_nonempty with rfl | ⟨a, ha⟩
Cleared hypotheses: s, hsb, hs
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : OrderBot α
inst_2 : IsAtomistic α
b : α
s : Set α
hsb : IsLUB s b
hs : ∀ a ∈ s, IsAtom a
inl :
  ∀ (hsb : IsLUB ∅ b) (hs : ∀ (a : α), Membership.mem (γ := Set α) ∅ a → IsAtom a), b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b
⊢ b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b
have inr : ∀ (a : α) (ha : a ∈ s), b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b
Tactic: rcases s.eq_empty_or_nonempty with rfl | ⟨a, ha⟩
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderBot α
inst_2 : IsAtomistic α
b : α
⊢ IsLUB {a : α | IsAtom a ∧ a ≤ b} b
have rcases : ∀ (s : Set α) (hsb : IsLUB s b) (hs : ∀ a ∈ s, IsAtom a), IsLUB {a : α | IsAtom a ∧ a ≤ b} b
Tactic: rcases isLUB_atoms b with ⟨s, hsb, hs⟩
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderBot α
inst_2 : IsAtomistic α
a b : α
⊢ a = b ↔ ∀ (c : α), IsAtom c → (c ≤ a ↔ c ≤ b)
have refine : ∀ (h : ∀ (c : α), IsAtom c → (c ≤ a ↔ c ≤ b)), a = b
Tactic: refine ⟨fun h => by simp [h], fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : OrderBot α
inst_2 : IsAtomistic α
a b : α
h : ∀ (c : α), IsAtom c → (c ≤ a ↔ c ≤ b)
⊢ a = b
have rw : (∀ (c : α), IsAtom c → c ≤ a → c ≤ b) ∧ ∀ (c : α), IsAtom c → c ≤ b → c ≤ a
Tactic: rw [le_antisymm_iff, le_iff_atom_le_imp, le_iff_atom_le_imp]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : IsCoatomistic α
b : α
⊢ b = ⊤ ∨ ∃ (a : α), IsCoatom a ∧ b ≤ a
have rcases : ∀ (s : Set α) (hsb : IsGLB s b) (hs : ∀ a ∈ s, IsCoatom a), b = ⊤ ∨ ∃ (a : α), IsCoatom a ∧ b ≤ a
Tactic: rcases isGLB_coatoms b with ⟨s, hsb, hs⟩
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : IsCoatomistic α
b : α
s : Set α
hsb : IsGLB s b
hs : ∀ a ∈ s, IsCoatom a
⊢ b = ⊤ ∨ ∃ (a : α), IsCoatom a ∧ b ≤ a
have inl : ∀ (hsb : IsGLB ∅ b) (hs : ∀ (a : α), Membership.mem (γ := Set α) ∅ a → IsCoatom a),
  b = ⊤ ∨ ∃ (a : α), IsCoatom a ∧ b ≤ a
Tactic: rcases s.eq_empty_or_nonempty with rfl | ⟨a, ha⟩
Cleared hypotheses: s, hsb, hs
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : OrderTop α
inst_2 : IsCoatomistic α
b : α
s : Set α
hsb : IsGLB s b
hs : ∀ a ∈ s, IsCoatom a
inl :
  ∀ (hsb : IsGLB ∅ b) (hs : ∀ (a : α), Membership.mem (γ := Set α) ∅ a → IsCoatom a),
    b = ⊤ ∨ ∃ (a : α), IsCoatom a ∧ b ≤ a
⊢ b = ⊤ ∨ ∃ (a : α), IsCoatom a ∧ b ≤ a
have inr : ∀ (a : α) (ha : a ∈ s), b = ⊤ ∨ ∃ (a : α), IsCoatom a ∧ b ≤ a
Tactic: rcases s.eq_empty_or_nonempty with rfl | ⟨a, ha⟩
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_4
inst : CompleteLattice α
⊢ IsAtomistic α ↔ ∀ (b : α), ∃ (s : Set α), b = sSup s ∧ ∀ a ∈ s, IsAtom a
have simp_rw : (∀ (b : α), ∃ (s : Set α), IsLUB s b ∧ ∀ a ∈ s, IsAtom a) ↔ ∀ (b : α), ∃ (s : Set α), b = sSup s ∧ ∀ a ∈ s, IsAtom a
Tactic: simp_rw [isAtomistic_iff, isLUB_iff_sSup_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_4
inst : CompleteLattice α
simp_rw :
  (∀ (b : α), ∃ (s : Set α), IsLUB s b ∧ ∀ a ∈ s, IsAtom a) ↔ ∀ (b : α), ∃ (s : Set α), b = sSup s ∧ ∀ a ∈ s, IsAtom a
⊢ IsAtomistic α ↔ ∀ (b : α), ∃ (s : Set α), b = sSup s ∧ ∀ a ∈ s, IsAtom a
have simp_rw₁ : (∀ (b : α), ∃ (s : Set α), sSup s = b ∧ ∀ a ∈ s, IsAtom a) ↔ ∀ (b : α), ∃ (s : Set α), b = sSup s ∧ ∀ a ∈ s, IsAtom a
Tactic: simp_rw [isAtomistic_iff, isLUB_iff_sSup_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_4
inst : CompleteLattice α
⊢ IsCoatomistic α ↔ ∀ (b : α), ∃ (s : Set α), b = sInf s ∧ ∀ a ∈ s, IsCoatom a
have simp_rw : (∀ (b : α), ∃ (s : Set α), IsGLB s b ∧ ∀ a ∈ s, IsCoatom a) ↔ ∀ (b : α), ∃ (s : Set α), b = sInf s ∧ ∀ a ∈ s, IsCoatom a
Tactic: simp_rw [isCoatomistic_iff, isGLB_iff_sInf_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_4
inst : CompleteLattice α
simp_rw :
  (∀ (b : α), ∃ (s : Set α), IsGLB s b ∧ ∀ a ∈ s, IsCoatom a) ↔
    ∀ (b : α), ∃ (s : Set α), b = sInf s ∧ ∀ a ∈ s, IsCoatom a
⊢ IsCoatomistic α ↔ ∀ (b : α), ∃ (s : Set α), b = sInf s ∧ ∀ a ∈ s, IsCoatom a
have simp_rw₁ : (∀ (b : α), ∃ (s : Set α), sInf s = b ∧ ∀ a ∈ s, IsCoatom a) ↔
  ∀ (b : α), ∃ (s : Set α), b = sInf s ∧ ∀ a ∈ s, IsCoatom a
Tactic: simp_rw [isCoatomistic_iff, isGLB_iff_sInf_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
b : α
⊢ ∃ (s : Set α), b = sSup s ∧ ∀ a ∈ s, IsAtom a
have inhabit : ∀ (inhabited_h : Inhabited α), ∃ (s : Set α), b = sSup s ∧ ∀ a ∈ s, IsAtom a
Tactic: inhabit α
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
⊢ ∃ (s : Set α), b = sSup s ∧ ∀ a ∈ s, IsAtom a
have refine : b = sSup {a : α | IsAtom a ∧ a ≤ b}
Tactic: refine ⟨{ a | IsAtom a ∧ a ≤ b }, ?_, fun a ha => ha.1⟩
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
⊢ b = sSup {a : α | IsAtom a ∧ a ≤ b}
have refine : b ≤ sSup {a : α | IsAtom a ∧ a ≤ b}
Tactic: refine le_antisymm ?_ (sSup_le fun c hc => hc.2)
-- Lean 4 proof step from Mathlib.Order.Atoms (hypothesis)
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
⊢ b ≤ sSup {a : α | IsAtom a ∧ a ≤ b}
have this : (⨅ (c : α), ⨆ (x : Bool), b ⊓ bif x then c else cᶜ) = b
Tactic: have : (⨅ c : α, ⨆ x, b ⊓ cond x c (cᶜ)) = b := by simp [iSup_bool_eq]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
this : (⨅ (c : α), ⨆ (x : Bool), b ⊓ bif x then c else cᶜ) = b
⊢ b ≤ sSup {a : α | IsAtom a ∧ a ≤ b}
have rw : LE.le.{u_4} (α := α) (⨅ (c : α), ⨆ (x : Bool), b ⊓ bif x then c else cᶜ)
  (sSup {a : α | IsAtom a ∧ a ≤ ⨅ (c : α), ⨆ (x : Bool), b ⊓ bif x then c else cᶜ})
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
⊢ LE.le.{u_4} (α := α) (⨅ (c : α), ⨆ (x : Bool), b ⊓ bif x then c else cᶜ)
    (sSup {a : α | IsAtom a ∧ a ≤ ⨅ (c : α), ⨆ (x : Bool), b ⊓ bif x then c else cᶜ})
have simp_rw : ∀ (i : (a : α) → Bool),
  LE.le.{u_4} (α := α) (⨅ (a : α), b ⊓ bif i a then a else aᶜ)
    (sSup {a : α | IsAtom a ∧ a ≤ ⨆ (g : (a : α) → Bool), ⨅ (a : α), b ⊓ bif g a then a else aᶜ})
Tactic: simp_rw [iInf_iSup_eq, iSup_le_iff]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : (a : α) → Bool
h : ¬Eq.{u_4 + 1} (α := α) (⨅ (a : α), b ⊓ bif g a then a else aᶜ) ⊥
⊢ LE.le.{u_4} (α := α) (⨅ (a : α), b ⊓ bif g a then a else aᶜ)
    (sSup {a : α | IsAtom a ∧ a ≤ ⨆ (g : (a : α) → Bool), ⨅ (a : α), b ⊓ bif g a then a else aᶜ})
have refine : ∀ (c : α) (hc : c < ⨅ (a : α), b ⊓ bif g a then a else aᶜ), c = ⊥
Tactic: refine le_sSup ⟨⟨h, fun c hc => ?_⟩, le_trans (by rfl) (le_iSup _ g)⟩
-- Lean 4 proof step from Mathlib.Order.Atoms (hypothesis)
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : (a : α) → Bool
c : α
hc : c < ⨅ (a : α), b ⊓ bif g a then a else aᶜ
⊢ c = ⊥
have this : c < bif g c then c else cᶜ
Tactic: have := lt_of_lt_of_le hc (le_trans (iInf_le _ c) inf_le_right)
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : (a : α) → Bool
c : α
hc : c < ⨅ (a : α), b ⊓ bif g a then a else aᶜ
this : c < bif g c then c else cᶜ
⊢ c = ⊥
have revert : ∀ (this : c < bif g c then c else cᶜ), c = ⊥
Tactic: revert this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.Atoms (hypothesis)
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : (a : α) → Bool
c : α
hc : c < ⨅ (a : α), b ⊓ bif g a then a else aᶜ
⊢ ∀ (this : c < bif g c then c else cᶜ), c = ⊥
have a : Nontrivial α
Tactic: nontriviality α
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : (a : α) → Bool
c : α
hc : c < ⨅ (a : α), b ⊓ bif g a then a else aᶜ
h : Nontrivial α
⊢ ∀ (this : c < bif g c then c else cᶜ), c = ⊥
have false : ∀ (this : c < bif false then c else cᶜ), c = ⊥
Tactic: cases g c
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : (a : α) → Bool
c : α
hc : c < ⨅ (a : α), b ⊓ bif g a then a else aᶜ
h : Nontrivial α
false : ∀ (this : c < bif Bool.false then c else cᶜ), c = ⊥
⊢ ∀ (this : c < bif g c then c else cᶜ), c = ⊥
have true : ∀ (this : c < bif true then c else cᶜ), c = ⊥
Tactic: cases g c
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : (a : α) → Bool
⊢ LE.le.{u_4} (α := α) (⨅ (a : α), b ⊓ bif g a then a else aᶜ)
    (sSup {a : α | IsAtom a ∧ a ≤ ⨆ (g : (a : α) → Bool), ⨅ (a : α), b ⊓ bif g a then a else aᶜ})
have if : ∀ (h : Eq.{u_4 + 1} (α := α) (⨅ (a : α), b ⊓ bif g a then a else aᶜ) ⊥),
  LE.le.{u_4} (α := α) (⨅ (a : α), b ⊓ bif g a then a else aᶜ)
    (sSup {a : α | IsAtom a ∧ a ≤ ⨆ (g : (a : α) → Bool), ⨅ (a : α), b ⊓ bif g a then a else aᶜ})
Tactic: if h : (⨅ a, b ⊓ cond (g a) a (aᶜ)) = ⊥ then simp [h] else
    refine le_sSup ⟨⟨h, fun c hc => ?_⟩, le_trans (by rfl) (le_iSup _ g)⟩; clear h
    have := lt_of_lt_of_le hc (le_trans (iInf_le _ c) inf_le_right)
    revert this
    nontriviality α
    cases g c <;> simp
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : (a : α) → Bool
if :
  ∀ (h : Eq.{u_4 + 1} (α := α) (⨅ (a : α), b ⊓ bif g a then a else aᶜ) ⊥),
    LE.le.{u_4} (α := α) (⨅ (a : α), b ⊓ bif g a then a else aᶜ)
      (sSup {a : α | IsAtom a ∧ a ≤ ⨆ (g : (a : α) → Bool), ⨅ (a : α), b ⊓ bif g a then a else aᶜ})
⊢ LE.le.{u_4} (α := α) (⨅ (a : α), b ⊓ bif g a then a else aᶜ)
    (sSup {a : α | IsAtom a ∧ a ≤ ⨆ (g : (a : α) → Bool), ⨅ (a : α), b ⊓ bif g a then a else aᶜ})
have if₁ : ∀ (h : ¬Eq.{u_4 + 1} (α := α) (⨅ (a : α), b ⊓ bif g a then a else aᶜ) ⊥),
  LE.le.{u_4} (α := α) (⨅ (a : α), b ⊓ bif g a then a else aᶜ)
    (sSup {a : α | IsAtom a ∧ a ≤ ⨆ (g : (a : α) → Bool), ⨅ (a : α), b ⊓ bif g a then a else aᶜ})
Tactic: if h : (⨅ a, b ⊓ cond (g a) a (aᶜ)) = ⊥ then simp [h] else
    refine le_sSup ⟨⟨h, fun c hc => ?_⟩, le_trans (by rfl) (le_iSup _ g)⟩; clear h
    have := lt_of_lt_of_le hc (le_trans (iInf_le _ c) inf_le_right)
    revert this
    nontriviality α
    cases g c <;> simp
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_4
inst : CompleteAtomicBooleanAlgebra α
S : Set α
hS : ∀ a ∈ S, IsAtom a
⊢ S = {a : α | a ≤ sSup S ∧ IsAtom a}
have h : ∀ (a : α), a ∈ S ↔ Membership.mem (γ := Set α) {a : α | a ≤ sSup S ∧ IsAtom a} a
Tactic: ext a
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_4
inst : CompleteAtomicBooleanAlgebra α
S : Set α
hS : ∀ a ∈ S, IsAtom a
a : α
⊢ a ∈ S ↔ Membership.mem (γ := Set α) {a : α | a ≤ sSup S ∧ IsAtom a} a
have h : Membership.mem (γ := Set α) {a : α | a ≤ sSup S ∧ IsAtom a} a → ∀ (hale : a ≤ sSup S) (hatom : IsAtom a), a ∈ S
Tactic: refine ⟨fun h => ⟨le_sSup h, hS a h⟩, fun ⟨hale, hatom⟩ => ?_⟩
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_4
inst : CompleteAtomicBooleanAlgebra α
S : Set α
hS : ∀ a ∈ S, IsAtom a
a : α
h : Membership.mem (γ := Set α) {a : α | a ≤ sSup S ∧ IsAtom a} a
hale : a ≤ sSup S
hatom : IsAtom a
⊢ a ∈ S
have h : ∀ (b : α) (hbS : b ∈ S) (hba : a ≤ b), a ∈ S
Tactic: obtain ⟨b, hbS, hba⟩ := (IsAtom.le_sSup hatom).mp hale
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_4
inst : CompleteAtomicBooleanAlgebra α
S : Set α
hS : ∀ a ∈ S, IsAtom a
a : α
h : Membership.mem (γ := Set α) {a : α | a ≤ sSup S ∧ IsAtom a} a
hale : a ≤ sSup S
hatom : IsAtom a
b : α
hbS : b ∈ S
hba : a ≤ b
⊢ a ∈ S
have h : Membership.mem (γ := Set α) {a : α | a ≤ sSup S ∧ IsAtom a} ⊥ →
  ∀ (hale : ⊥ ≤ sSup S) (hatom : IsAtom.{u_4} (α := α) ⊥) (hba : ⊥ ≤ b), ⊥ ∈ S
Tactic: obtain rfl | rfl := (hS b hbS).le_iff.mp hba
Cleared hypotheses: a, h, hale, hatom, hba
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_4
inst : CompleteAtomicBooleanAlgebra α
S : Set α
hS : ∀ a ∈ S, IsAtom a
a : α
h_1 : Membership.mem (γ := Set α) {a : α | a ≤ sSup S ∧ IsAtom a} a
hale : a ≤ sSup S
hatom : IsAtom a
b : α
hbS : b ∈ S
hba : a ≤ b
h :
  Membership.mem (γ := Set α) {a : α | a ≤ sSup S ∧ IsAtom a} ⊥ →
    ∀ (hale : ⊥ ≤ sSup S) (hatom : IsAtom.{u_4} (α := α) ⊥) (hba : ⊥ ≤ b), ⊥ ∈ S
⊢ a ∈ S
have h₁ : ∀ (hbS : a ∈ S) (hba : a ≤ a), a ∈ S
Tactic: obtain rfl | rfl := (hS b hbS).le_iff.mp hba
Cleared hypotheses: b, hbS, hba
-- Lean 4 proof step from Mathlib.Order.Atoms (hypothesis)
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
S : Set { a : α // IsAtom a }
⊢ (fun (A : α) ↦ ({a : { a : α // IsAtom a } | (↑a : α) ≤ A} : Set { a : α // IsAtom a }))
      ((fun (S : Set { a : α // IsAtom a }) ↦ sSup (Subtype.val (p := fun (a : α) ↦ IsAtom a) '' S)) S) =
    S
have h : ∀ a ∈ Subtype.val (p := fun (a : α) ↦ IsAtom a) '' S, IsAtom a
Tactic: have h : ∀ a ∈ Subtype.val '' S, IsAtom a := by
      rintro a ⟨a', ha', rfl⟩
      exact a'.prop
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
S : Set { a : α // IsAtom a }
h : ∀ a ∈ Subtype.val (p := fun (a : α) ↦ IsAtom a) '' S, IsAtom a
⊢ (fun (A : α) ↦ ({a : { a : α // IsAtom a } | (↑a : α) ≤ A} : Set { a : α // IsAtom a }))
      ((fun (S : Set { a : α // IsAtom a }) ↦ sSup (Subtype.val (p := fun (a : α) ↦ IsAtom a) '' S)) S) =
    S
have rw : Eq.{u_4 + 1} (α := Set α)
  (Set.image (α := { a : α // IsAtom a }) (Subtype.val (p := fun (a : α) ↦ IsAtom a))
    ((fun (A : α) ↦ ({a : { a : α // IsAtom a } | (↑a : α) ≤ A} : Set { a : α // IsAtom a }))
      ((fun (S : Set { a : α // IsAtom a }) ↦ sSup (Subtype.val (p := fun (a : α) ↦ IsAtom a) '' S)) S)))
  {a : α | a ≤ sSup (Subtype.val (p := fun (a : α) ↦ IsAtom a) '' S) ∧ IsAtom a}
Tactic: rw [← Subtype.val_injective.image_injective.eq_iff, eq_setOf_le_sSup_and_isAtom h]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι : Sort u_1
α_1 : Type u_2
β : Type u_3
inst : PartialOrder α_1
α : Type u_4
inst_1 : CompleteAtomicBooleanAlgebra α
S : Set { a : α // IsAtom a }
h : ∀ a ∈ Subtype.val (p := fun (a : α) ↦ IsAtom a) '' S, IsAtom a
⊢ Eq.{u_4 + 1} (α := Set α)
    (Set.image (α := { a : α // IsAtom a }) (Subtype.val (p := fun (a : α) ↦ IsAtom a))
      ((fun (A : α) ↦ ({a : { a : α // IsAtom a } | (↑a : α) ≤ A} : Set { a : α // IsAtom a }))
        ((fun (S : Set { a : α // IsAtom a }) ↦ sSup (Subtype.val (p := fun (a : α) ↦ IsAtom a) '' S)) S)))
    {a : α | a ≤ sSup (Subtype.val (p := fun (a : α) ↦ IsAtom a) '' S) ∧ IsAtom a}
have h₁ : ∀ (a : α),
  Membership.mem (γ := Set α)
      (Set.image (α := { a : α // IsAtom a }) (Subtype.val (p := fun (a : α) ↦ IsAtom a))
        ((fun (A : α) ↦ ({a : { a : α // IsAtom a } | (↑a : α) ≤ A} : Set { a : α // IsAtom a }))
          ((fun (S : Set { a : α // IsAtom a }) ↦ sSup (Subtype.val (p := fun (a : α) ↦ IsAtom a) '' S)) S)))
      a ↔
    Membership.mem (γ := Set α) {a : α | a ≤ sSup (Subtype.val (p := fun (a : α) ↦ IsAtom a) '' S) ∧ IsAtom a} a
Tactic: ext a
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_2
inst : LE α
inst_1 : BoundedOrder α
⊢ IsSimpleOrder α ↔ IsSimpleOrder.{u_2} αᵒᵈ
have mp : IsSimpleOrder α → IsSimpleOrder.{u_2} αᵒᵈ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_2
inst : LE α
inst_1 : BoundedOrder α
mp : IsSimpleOrder α → IsSimpleOrder.{u_2} αᵒᵈ
⊢ IsSimpleOrder α ↔ IsSimpleOrder.{u_2} αᵒᵈ
have mpr : IsSimpleOrder.{u_2} αᵒᵈ → IsSimpleOrder α
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_2
inst : LE α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
⊢ Ne.{u_2 + 1} (α := α) ⊥ ⊤
have obtain : ∀ (a b : α) (h : a ≠ b), Ne.{u_2 + 1} (α := α) ⊥ ⊤
Tactic: obtain ⟨a, b, h⟩ := exists_pair_ne α
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_2
inst : LE α
inst_1 : BoundedOrder α
inst_2 : IsSimpleOrder α
a b : α
h : a ≠ b
⊢ Ne.{u_2 + 1} (α := α) ⊥ ⊤
have inl : ∀ (h : ⊥ ≠ b), Ne.{u_2 + 1} (α := α) ⊥ ⊤
Tactic: rcases eq_bot_or_eq_top a with (rfl | rfl)
Cleared hypotheses: a, h