awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.BooleanSubalgebra (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
p : (g : α) → Membership.mem (γ := BooleanSubalgebra α) (closure s) g → Prop
sdiff : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s), p (x \ y) ⋯
sup :
  ∀ (x : α) (hx : Membership.mem (γ := BooleanSubalgebra α) (closure s) x) (y : α)
    (hy : Membership.mem (γ := BooleanSubalgebra α) (closure s) y), p x hx → p y hy → p (x ⊔ y) ⋯
t : Finset ((↑s : Type u_2) × (↑s : Type u_2))
⊢ ∀
    (hx :
      Membership.mem (γ := BooleanSubalgebra α) (closure s)
        (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))),
    p (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) hx
have refine : ∀ (x : (↑s : Type u_2) × (↑s : Type u_2)) (t : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
  x ∉ t →
    ∀
      (ih :
        ∀
          (hx :
            Membership.mem (γ := BooleanSubalgebra α) (closure s)
              (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))),
          p (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) hx)
      (hxt :
        Membership.mem (γ := BooleanSubalgebra α) (closure s)
          ((insert x t).sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))),
      p ((insert x t).sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) hxt
Tactic: refine t.induction (by simpa using sdiff _ bot_mem _ bot_mem) fun x t _ ih hxt ↦ ?_
-- Lean 4 proof step from Mathlib.Order.BooleanSubalgebra (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
p : (g : α) → Membership.mem (γ := BooleanSubalgebra α) (closure s) g → Prop
sdiff : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s), p (x \ y) ⋯
sup :
  ∀ (x : α) (hx : Membership.mem (γ := BooleanSubalgebra α) (closure s) x) (y : α)
    (hy : Membership.mem (γ := BooleanSubalgebra α) (closure s) y), p x hx → p y hy → p (x ⊔ y) ⋯
t_1 : Finset ((↑s : Type u_2) × (↑s : Type u_2))
x : (↑s : Type u_2) × (↑s : Type u_2)
t : Finset ((↑s : Type u_2) × (↑s : Type u_2))
h : x ∉ t
ih :
  ∀
    (hx :
      Membership.mem (γ := BooleanSubalgebra α) (closure s)
        (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))),
    p (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) hx
hxt :
  Membership.mem (γ := BooleanSubalgebra α) (closure s)
    ((insert x t).sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))
⊢ p ((insert x t).sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) hxt
have simp : ∀
  (hxt_1 :
    Membership.mem (γ := BooleanSubalgebra α) (closure s)
      ((↑x.1 : α) \ (↑x.2 : α) ⊔ t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))),
  p ((↑x.1 : α) \ (↑x.2 : α) ⊔ t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) sorry
Tactic: simp only [Finset.sup_insert] at hxt ⊢
-- Lean 4 proof step from Mathlib.Order.BooleanSubalgebra (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
p : (g : α) → Membership.mem (γ := BooleanSubalgebra α) (closure s) g → Prop
sdiff : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s), p (x \ y) ⋯
sup :
  ∀ (x : α) (hx : Membership.mem (γ := BooleanSubalgebra α) (closure s) x) (y : α)
    (hy : Membership.mem (γ := BooleanSubalgebra α) (closure s) y), p x hx → p y hy → p (x ⊔ y) ⋯
t : Finset ((↑s : Type u_2) × (↑s : Type u_2))
⊢ ∀
    (hx :
      Membership.mem (γ := BooleanSubalgebra α) (closure s)
        (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))),
    p (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) hx
have refine : ∀ (x : (↑s : Type u_2) × (↑s : Type u_2)) (t : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
  x ∉ t →
    ∀
      (ih :
        ∀
          (hx :
            Membership.mem (γ := BooleanSubalgebra α) (closure s)
              (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))),
          p (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) hx)
      (hxt :
        Membership.mem (γ := BooleanSubalgebra α) (closure s)
          ((insert x t).sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))),
      p ((insert x t).sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) hxt
Tactic: classical
  refine t.induction (by simpa using sdiff _ bot_mem _ bot_mem) fun x t _ ih hxt ↦ ?_
  simp only [Finset.sup_insert] at hxt ⊢
  exact sup _ _ _ ((mem_closure_iff_sup_sdiff isSublattice bot_mem top_mem).mpr ⟨_, rfl⟩)
    (sdiff _ x.1.2 _ x.2.2) (ih _)
-- Lean 4 proof step from Mathlib.Order.BooleanSubalgebra (goal)
Goal:
α : Type u_2
inst : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
p : (g : α) → Membership.mem (γ := BooleanSubalgebra α) (closure s) g → Prop
sdiff : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s), p (x \ y) ⋯
sup :
  ∀ (x : α) (hx : Membership.mem (γ := BooleanSubalgebra α) (closure s) x) (y : α)
    (hy : Membership.mem (γ := BooleanSubalgebra α) (closure s) y), p x hx → p y hy → p (x ⊔ y) ⋯
t : Finset ((↑s : Type u_2) × (↑s : Type u_2))
refine :
  ∀ (x : (↑s : Type u_2) × (↑s : Type u_2)) (t : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
    x ∉ t →
      ∀
        (ih :
          ∀
            (hx :
              Membership.mem (γ := BooleanSubalgebra α) (closure s)
                (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))),
            p (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) hx)
        (hxt :
          Membership.mem (γ := BooleanSubalgebra α) (closure s)
            ((insert x t).sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))),
        p ((insert x t).sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) hxt
⊢ ∀
    (hx :
      Membership.mem (γ := BooleanSubalgebra α) (closure s)
        (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))),
    p (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) hx
have refine₁ : ∀ (x : (↑s : Type u_2) × (↑s : Type u_2)) (t : Finset ((↑s : Type u_2) × (↑s : Type u_2))),
  x ∉ t →
    ∀
      (ih :
        ∀
          (hx :
            Membership.mem (γ := BooleanSubalgebra α) (closure s)
              (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))),
          p (t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) hx)
      (hxt :
        Membership.mem (γ := BooleanSubalgebra α) (closure s)
          ((insert x t).sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)))
      (hxt_1 :
        Membership.mem (γ := BooleanSubalgebra α) (closure s)
          ((↑x.1 : α) \ (↑x.2 : α) ⊔ t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α))),
      p ((↑x.1 : α) \ (↑x.2 : α) ⊔ t.sup fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ (↑x.1 : α) \ (↑x.2 : α)) sorry
Tactic: classical
  refine t.induction (by simpa using sdiff _ bot_mem _ bot_mem) fun x t _ ih hxt ↦ ?_
  simp only [Finset.sup_insert] at hxt ⊢
  exact sup _ _ _ ((mem_closure_iff_sup_sdiff isSublattice bot_mem top_mem).mpr ⟨_, rfl⟩)
    (sdiff _ x.1.2 _ x.2.2) (ih _)
-- Lean 4 proof step from Mathlib.Order.Booleanisation (goal)
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a_1 b_1 a b : α
hab : a ≤ b
hba : b ≤ a
⊢ lift a = lift b
have rw : lift b = lift b
Tactic: rw [hab.antisymm hba]
-- Lean 4 proof step from Mathlib.Order.Booleanisation (goal)
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a_1 b_1 a b : α
hab : b ≤ a
hba : a ≤ b
⊢ comp a = comp b
have rw : comp a = comp a
Tactic: rw [hab.antisymm hba]
-- Lean 4 proof step from Mathlib.Order.Booleanisation (goal)
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a_1 b_1 a b c : α
⊢ (b ⊔ c) \ a ≤ b \ a ⊔ c \ a
have rw : b \ a ⊔ c \ a ≤ b \ a ⊔ c \ a
Tactic: rw [sup_sdiff]
-- Lean 4 proof step from Mathlib.Order.Booleanisation (goal)
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a_1 b_1 a b c : α
⊢ a \ (b ⊓ c) ≤ a \ b ⊔ a \ c
have rw : a \ b ⊔ a \ c ≤ a \ b ⊔ a \ c
Tactic: rw [sdiff_inf]
-- Lean 4 proof step from Mathlib.Order.Booleanisation (goal)
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a_1 b_1 a b c : α
⊢ a \ (b \ c) ≤ a \ b ⊔ a ⊓ c
have rw : a \ b ⊔ a ⊓ c ≤ a \ b ⊔ a ⊓ c
Tactic: rw [sdiff_sdiff_right']
-- Lean 4 proof step from Mathlib.Order.Booleanisation (goal)
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a_1 b_1 a b c : α
⊢ a \ (c \ b) ≤ a ⊓ b ⊔ a \ c
have rw : a \ c ⊔ a ⊓ b ≤ a ⊓ b ⊔ a \ c
Tactic: rw [sdiff_sdiff_right', sup_comm]
-- Lean 4 proof step from Mathlib.Order.Booleanisation (goal)
Goal:
α : Type u_1
inst : GeneralizedBooleanAlgebra α
a_1 b_1 a b c : α
rw : a \ c ⊔ a ⊓ b ≤ a ⊓ b ⊔ a \ c
⊢ a \ (c \ b) ≤ a ⊓ b ⊔ a \ c
have rw₁ : a ⊓ b ⊔ a \ c ≤ a ⊓ b ⊔ a \ c
Tactic: rw [sdiff_sdiff_right', sup_comm]
-- Lean 4 proof step from Mathlib.Order.Bounded (goal)
Goal:
α : Type u_1
s : Set α
inst : Preorder α
inst_1 : NoMaxOrder α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s ↔ Bounded (fun (x1 x2 : α) ↦ x1 < x2) s
have refine : ∀ (h : Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s), Bounded (fun (x1 x2 : α) ↦ x1 < x2) s
Tactic: refine ⟨fun h => ?_, bounded_le_of_bounded_lt⟩
-- Lean 4 proof step from Mathlib.Order.Bounded (goal)
Goal:
α : Type u_1
s : Set α
inst : Preorder α
inst_1 : NoMaxOrder α
h : Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s
⊢ Bounded (fun (x1 x2 : α) ↦ x1 < x2) s
have obtain : ∀ (a : α) (ha : ∀ (b : α), b ∈ s → (fun (x1 x2 : α) ↦ x1 ≤ x2) b a), Bounded (fun (x1 x2 : α) ↦ x1 < x2) s
Tactic: obtain ⟨a, ha⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Bounded (goal)
Goal:
α : Type u_1
s : Set α
inst : Preorder α
inst_1 : NoMaxOrder α
a : α
ha : ∀ (b : α), b ∈ s → (fun (x1 x2 : α) ↦ x1 ≤ x2) b a
⊢ Bounded (fun (x1 x2 : α) ↦ x1 < x2) s
have obtain : ∀ (b : α) (hb : a < b), Bounded (fun (x1 x2 : α) ↦ x1 < x2) s
Tactic: obtain ⟨b, hb⟩ := exists_gt a
-- Lean 4 proof step from Mathlib.Order.Bounded (goal)
Goal:
α : Type u_1
s : Set α
inst : Preorder α
inst_1 : NoMaxOrder α
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 < x2) s ↔ Unbounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s
have simp_rw : ¬Bounded (fun (x1 x2 : α) ↦ x1 < x2) s ↔ ¬Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s
Tactic: simp_rw [← not_bounded_iff, bounded_le_iff_bounded_lt]
-- Lean 4 proof step from Mathlib.Order.Bounded (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
H : ∀ (a b : α), ∃ (m : α), ∀ (c : α), r c a ∨ r c b → r c m
a : α
⊢ Bounded r (s ∩ {b : α | ¬r b a}) ↔ Bounded r s
have refine : Bounded r (s ∩ {b : α | ¬r b a}) → Bounded r s
Tactic: refine ⟨?_, Bounded.mono inter_subset_left⟩
-- Lean 4 proof step from Mathlib.Order.Bounded (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
H : ∀ (a b : α), ∃ (m : α), ∀ (c : α), r c a ∨ r c b → r c m
a b : α
hb : ∀ (b_1 : α), b_1 ∈ s ∩ {b : α | ¬r b a} → r b_1 b
⊢ Bounded r s
have obtain : ∀ (m : α) (hm : ∀ (c : α), r c a ∨ r c b → r c m), Bounded r s
Tactic: obtain ⟨m, hm⟩ := H a b
-- Lean 4 proof step from Mathlib.Order.Bounded (goal)
Goal:
α : Type u_1
r : α → α → Prop
s : Set α
H : ∀ (a b : α), ∃ (m : α), ∀ (c : α), r c a ∨ r c b → r c m
a : α
⊢ Unbounded r (s ∩ {b : α | ¬r b a}) ↔ Unbounded r s
have simp_rw : ¬Bounded r (s ∩ {b : α | ¬r b a}) ↔ ¬Bounded r s
Tactic: simp_rw [← not_bounded_iff, bounded_inter_not H]
-- Lean 4 proof step from Mathlib.Order.Bounded (goal)
Goal:
α : Type u_1
s : Set α
inst : SemilatticeSup α
a : α
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | ¬b ≤ a}) ↔ Unbounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s
have rw : Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | ¬b ≤ a}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s
Tactic: rw [← not_bounded_iff, ← not_bounded_iff, not_iff_not]
-- Lean 4 proof step from Mathlib.Order.Bounded (goal)
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
a : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | a < b}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s
have simp_rw : Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | ¬b ≤ a}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s
Tactic: simp_rw [← not_le, bounded_le_inter_not_le]
-- Lean 4 proof step from Mathlib.Order.Bounded (goal)
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
a : α
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | a < b}) ↔ Unbounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s
have h : ∀ (x : α), a < x ↔ ¬x ≤ a
Tactic: convert! @unbounded_le_inter_not_le _ s _ a
-- Lean 4 proof step from Mathlib.Order.Bounded (goal)
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
a : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | a ≤ b}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s
have refine : Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | a ≤ b}) → Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s
Tactic: refine ⟨?_, Bounded.mono Set.inter_subset_left⟩
-- Lean 4 proof step from Mathlib.Order.Bounded (goal)
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
a : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | a ≤ b}) → Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s
have rw : Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | a ≤ b}) → Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | a < b})
Tactic: rw [← @bounded_le_inter_lt _ s _ a]
-- Lean 4 proof step from Mathlib.Order.Bounded (goal)
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
a : α
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | a ≤ b}) ↔ Unbounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s
have rw : Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | a ≤ b}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s
Tactic: rw [← not_bounded_iff, ← not_bounded_iff, not_iff_not]
-- Lean 4 proof step from Mathlib.Order.Bounded (goal)
Goal:
α : Type u_1
s : Set α
inst : SemilatticeSup α
a : α
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 < x2) (s ∩ {b : α | ¬b < a}) ↔ Unbounded (fun (x1 x2 : α) ↦ x1 < x2) s
have rw : Bounded (fun (x1 x2 : α) ↦ x1 < x2) (s ∩ {b : α | ¬b < a}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 < x2) s
Tactic: rw [← not_bounded_iff, ← not_bounded_iff, not_iff_not]
-- Lean 4 proof step from Mathlib.Order.Bounded (goal)
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
a : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 < x2) (s ∩ {b : α | a ≤ b}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 < x2) s
have h : ∀ (x : α), a ≤ x ↔ ¬x < a
Tactic: convert! @bounded_lt_inter_not_lt _ s _ a
-- Lean 4 proof step from Mathlib.Order.Bounded (goal)
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
a : α
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 < x2) (s ∩ {b : α | a ≤ b}) ↔ Unbounded (fun (x1 x2 : α) ↦ x1 < x2) s
have h : ∀ (x : α), a ≤ x ↔ ¬x < a
Tactic: convert! @unbounded_lt_inter_not_lt _ s _ a
-- Lean 4 proof step from Mathlib.Order.Bounded (goal)
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
inst_1 : NoMaxOrder α
a : α
⊢ Bounded (fun (x1 x2 : α) ↦ x1 < x2) (s ∩ {b : α | a < b}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 < x2) s
have rw : Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) (s ∩ {b : α | a < b}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 ≤ x2) s
Tactic: rw [← bounded_le_iff_bounded_lt, ← bounded_le_iff_bounded_lt]
-- Lean 4 proof step from Mathlib.Order.Bounded (goal)
Goal:
α : Type u_1
s : Set α
inst : LinearOrder α
inst_1 : NoMaxOrder α
a : α
⊢ Unbounded (fun (x1 x2 : α) ↦ x1 < x2) (s ∩ {b : α | a < b}) ↔ Unbounded (fun (x1 x2 : α) ↦ x1 < x2) s
have rw : Bounded (fun (x1 x2 : α) ↦ x1 < x2) (s ∩ {b : α | a < b}) ↔ Bounded (fun (x1 x2 : α) ↦ x1 < x2) s
Tactic: rw [← not_bounded_iff, ← not_bounded_iff, not_iff_not]
-- Lean 4 proof step from Mathlib.Order.BoundedOrder.Basic (goal)
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : LE α
⊢ OrderTop α ⊕' NoTopOrder α
have pos : (H : ∀ (a : α), ∃ (b : α), ¬b ≤ a) → OrderTop α ⊕' NoTopOrder α
Tactic: by_cases! H : ∀ a : α, ∃ b, ¬b ≤ a
-- Lean 4 proof step from Mathlib.Order.BoundedOrder.Basic (goal)
Goal:
α_1 : Type u
β : Type v
α : Type u_1
inst : LE α
pos : (H : ∀ (a : α), ∃ (b : α), ¬b ≤ a) → OrderTop α ⊕' NoTopOrder α
⊢ OrderTop α ⊕' NoTopOrder α
have neg : (H : ∃ (a : α), ∀ (b : α), b ≤ a) → OrderTop α ⊕' NoTopOrder α
Tactic: by_cases! H : ∀ a : α, ∃ b, ¬b ≤ a
-- Lean 4 proof step from Mathlib.Order.BoundedOrder.Basic (goal)
Goal:
α : Type u
inst : Preorder α
inst_1 : OrderTop α
a : α
⊢ ¬IsMax a ↔ a < ⊤
have rw : (∃ (b : α), a < b) ↔ a < ⊤
Tactic: rw [not_isMax_iff]
-- Lean 4 proof step from Mathlib.Order.BoundedOrder.Basic (goal)
Goal:
α : Type u_1
hA : PartialOrder α
A : OrderTop α
hB : PartialOrder α
B : OrderTop α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ Eq.{u_1 + 1} (α := α) ⊤ ⊤
have refl : ∀ (B : OrderTop α) (H : ∀ (x y : α), x ≤ y ↔ x ≤ y), Eq.{u_1 + 1} (α := α) ⊤ ⊤
Tactic: cases PartialOrder.ext H
Cleared hypotheses: hB, B, H
-- Lean 4 proof step from Mathlib.Order.BoundedOrder.Basic (goal)
Goal:
α : Type u_1
hA : PartialOrder α
A B : OrderTop α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
⊢ Eq.{u_1 + 1} (α := α) ⊤ ⊤
have refl : LE.le.{u_1} (α := α) ⊤ ⊤
Tactic: apply top_unique
-- Lean 4 proof step from Mathlib.Order.BoundedOrder.Basic (goal)
Goal:
α : Type u
β : Type v
inst : PartialOrder α
a : α
ha : ∀ (a_1 : α), ⊥ ≤ a_1
b : α
hb : ∀ (a : α), ⊥ ≤ a
⊢ { bot := a, bot_le := ha : OrderBot α } = { bot := b, bot_le := hb }
have e_toBot : a = b
Tactic: congr
-- Lean 4 proof step from Mathlib.Order.BoundedOrder.Basic (goal)
Goal:
α : Type u
β : Type v
inst : PartialOrder α
toOrderTop : OrderTop α
toOrderBot : OrderBot α
toOrderTop_1 : OrderTop α
toOrderBot_1 : OrderBot α
⊢ Eq.{u + 1} (α := BoundedOrder α) { toOrderTop := toOrderTop, toOrderBot := toOrderBot }
    { toOrderTop := toOrderTop_1, toOrderBot := toOrderBot_1 }
have e_toOrderTop : toOrderTop = toOrderTop_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Order.BoundedOrder.Basic (goal)
Goal:
α : Type u
β : Type v
inst : PartialOrder α
toOrderTop : OrderTop α
toOrderBot : OrderBot α
toOrderTop_1 : OrderTop α
toOrderBot_1 : OrderBot α
e_toOrderTop : toOrderTop = toOrderTop_1
⊢ Eq.{u + 1} (α := BoundedOrder α) { toOrderTop := toOrderTop, toOrderBot := toOrderBot }
    { toOrderTop := toOrderTop_1, toOrderBot := toOrderBot_1 }
have e_toOrderBot : toOrderBot = toOrderBot_1
Tactic: congr
-- Lean 4 proof step from Mathlib.Order.BoundedOrder.Basic (goal)
Goal:
α : Type u
β : Type v
inst : LE α
inst_1 : Top α
inst_2 : LE β
inst_3 : OrderTop β
f : α → β
map_le : ∀ (a b : α), f a ≤ f b → a ≤ b
map_top : f ⊤ = ⊤
a : α
⊢ f a ≤ f ⊤
have rw : f a ≤ ⊤
Tactic: rw [map_top]
-- Lean 4 proof step from Mathlib.Order.BoundedOrder.Basic (goal)
Goal:
α : Type u
p : α → Prop
inst : PartialOrder α
inst_1 : OrderBot α
inst_2 : OrderBot (Subtype p)
hbot : p ⊥
x : { x : α // p x }
⊢ (↑x : α) = ⊥ ↔ x = ⊥
have rw : (↑x : α) = (↑⊥ : α) ↔ x = ⊥
Tactic: rw [← coe_bot hbot, Subtype.ext_iff]
-- Lean 4 proof step from Mathlib.Order.BoundedOrder.Basic (goal)
Goal:
α : Type u
p : α → Prop
inst : PartialOrder α
inst_1 : OrderBot α
inst_2 : OrderBot (Subtype p)
hbot : p ⊥
x : { x : α // p x }
rw : (↑x : α) = (↑⊥ : α) ↔ x = ⊥
⊢ (↑x : α) = ⊥ ↔ x = ⊥
have rw₁ : (↑x : α) = (↑⊥ : α) ↔ (↑x : α) = (↑⊥ : α)
Tactic: rw [← coe_bot hbot, Subtype.ext_iff]
-- Lean 4 proof step from Mathlib.Order.BoundedOrder.Lattice (goal)
Goal:
α : Type u_1
inst : SemilatticeSup α
inst_1 : OrderBot α
a b : α
⊢ a ⊔ b = ⊥ ↔ a = ⊥ ∧ b = ⊥
have rw : a ≤ ⊥ ∧ b ≤ ⊥ ↔ a = ⊥ ∧ b = ⊥
Tactic: rw [eq_bot_iff, sup_le_iff]
-- Lean 4 proof step from Mathlib.Order.BoundedOrder.Lattice (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : OrderBot α
a b : α
⊢ min a b = ⊥ ↔ a = ⊥ ∨ b = ⊥
have simp_rw : min a b ≤ ⊥ ↔ a ≤ ⊥ ∨ b ≤ ⊥
Tactic: simp_rw [← le_bot_iff, inf_le_iff]
-- Lean 4 proof step from Mathlib.Order.BoundedOrder.Lattice (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : WellFoundedGT α
inst_2 : OrderTop α
P : α → Prop
hexists : ∃ (M : α), P M
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ (M : α), M > N ∧ P M
⊢ P ⊤
have contrapose! : ∀ (hexists : ¬P ⊤) (M : α), ¬P M
Tactic: contrapose! hexists
Cleared hypotheses: hexists
-- Lean 4 proof step from Mathlib.Order.BoundedOrder.Lattice (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : WellFoundedGT α
inst_2 : OrderTop α
P : α → Prop
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ (M : α), M > N ∧ P M
hexists : ¬P ⊤
x : α
IH : ∀ (y : α), x < y → ¬P y
⊢ ¬P x
have pos : ∀ (hx : x = ⊤), ¬P x
Tactic: by_cases hx : x = ⊤
-- Lean 4 proof step from Mathlib.Order.BoundedOrder.Lattice (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : WellFoundedGT α
inst_2 : OrderTop α
P : α → Prop
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ (M : α), M > N ∧ P M
hexists : ¬P ⊤
x : α
IH : ∀ (y : α), x < y → ¬P y
pos : ∀ (hx : x = ⊤), ¬P x
⊢ ¬P x
have neg : ∀ (hx : ¬x = ⊤), ¬P x
Tactic: by_cases hx : x = ⊤
-- Lean 4 proof step from Mathlib.Order.BoundedOrder.Lattice (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : WellFoundedGT α
inst_2 : OrderTop α
P : α → Prop
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ (M : α), M > N ∧ P M
hexists : ¬P ⊤
x : α
IH : ∀ (y : α), x < y → ¬P y
hx : ¬x = ⊤
hx' : P x
⊢ False
have neg : ∀ (M : α) (hM : M > x) (hM' : P M), False
Tactic: obtain ⟨M, hM, hM'⟩ := hind x hx hx'
-- Lean 4 proof step from Mathlib.Order.BoundedOrder.Lattice (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : WellFoundedGT α
inst_2 : OrderTop α
P : α → Prop
hind : ∀ (N : α), N ≠ ⊤ → P N → ∃ (M : α), M > N ∧ P M
hexists : ¬P ⊤
M : α
⊢ ¬P M
have ind : ∀ (x : α) (IH : ∀ (y : α), x < y → ¬P y), ¬P x
Tactic: induction M using WellFoundedGT.induction with
  | ind x IH =>
    by_cases hx : x = ⊤
    · exact hx ▸ hexists
    · intro hx'
      obtain ⟨M, hM, hM'⟩ := hind x hx hx'
      exact IH _ hM hM'
Cleared hypotheses: M
-- Lean 4 proof step from Mathlib.Order.BoundedOrder.Monotone (goal)
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
inst_2 : OrderTop β
f : α → β
H : StrictMono f
a : α
h_top : f a = ⊤
x : α
p : β
⊢ p ≤ f a
have rw : p ≤ ⊤
Tactic: rw [h_top]
-- Lean 4 proof step from Mathlib.Order.BoundedOrder.Monotone (goal)
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
inst_2 : OrderBot β
f : α → β
H : StrictMono f
a : α
h_bot : f a = ⊥
x : α
p : β
⊢ f a ≤ p
have rw : ⊥ ≤ p
Tactic: rw [h_bot]
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
a : α
h : upperBounds s = upperBounds t
⊢ IsLUB s a ↔ IsLUB t a
have rw : IsLeast (upperBounds s) a ↔ IsLUB t a
Tactic: rw [IsLUB, IsLUB, h]
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
a : α
h : upperBounds s = upperBounds t
rw : IsLeast (upperBounds s) a ↔ IsLUB t a
⊢ IsLUB s a ↔ IsLUB t a
have rw₁ : IsLeast (upperBounds s) a ↔ IsLeast (upperBounds t) a
Tactic: rw [IsLUB, IsLUB, h]
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
a : α
h : upperBounds s = upperBounds t
rw : IsLeast (upperBounds s) a ↔ IsLUB t a
rw₁ : IsLeast (upperBounds s) a ↔ IsLeast (upperBounds t) a
⊢ IsLUB s a ↔ IsLUB t a
have rw₂ : IsLeast (upperBounds t) a ↔ IsLeast (upperBounds t) a
Tactic: rw [IsLUB, IsLUB, h]
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
β : Type u_4
inst_1 : Preorder β
s : Set (α × β)
hs : DirectedOn (fun (x1 x2 : α × β) ↦ x1 ≤ x2) s
x : α × β
hx : x ∈ s
y : α × β
hy : y ∈ s
⊢ ∃ b ∈ s, (x.1, y.2) ≤ b
have obtain : ∀ (z : α × β) (hz : z ∈ s) (hxz : x ≤ z) (hyz : y ≤ z), ∃ b ∈ s, (x.1, y.2) ≤ b
Tactic: obtain ⟨z, hz, hxz, hyz⟩ := hs _ hx _ hy
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
hc : IsCofinalFor s t
⊢ IsCofinalFor (t ∪ s) t
have rw : IsCofinalFor (s ∪ t) t
Tactic: rw [union_comm]
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
s t : Set α
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) t
hst : s ⊆ t
hc : IsCofinalFor t s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ ∃ z ∈ s, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z
have obtain : ∀ (z : α) (hz : z ∈ t) (hxz : x ≤ z) (hyz : y ≤ z),
  ∃ z ∈ s, (fun (x1 x2 : α) ↦ x1 ≤ x2) x z ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) y z
Tactic: obtain ⟨z, hz, hxz, hyz⟩ := hd x (hst hx) y (hst hy)