awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
γ : Type u_3
inst : SemilatticeSup γ
inst_1 : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
h₂ : a < x ⊔ a
y : γ
lty : a < y
ylt : y < x ⊔ a
⊢ x ≤ a
have apply : x ≤ b
Tactic: apply (not_lt_of_ge (sup_le (hx ⟨lty, ylt.trans_le (sup_le _ h.le)⟩) lty.le) ylt).elim
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
γ : Type u_3
inst : SemilatticeSup γ
inst_1 : DenselyOrdered γ
a b : γ
h : a < b
x : γ
hx : x ∈ lowerBounds (Ioo a b)
h₂ : a < x ⊔ a
y : γ
lty : a < y
ylt : y < x ⊔ a
⊢ x ≤ b
have obtain : ∀ (u : γ) (au : a < u) (ub : u < b), x ≤ b
Tactic: obtain ⟨u, au, ub⟩ := exists_between h
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
γ : Type u_3
inst : PartialOrder γ
inst_1 : OrderTop γ
⊢ Eq (α := Set γ) (upperBounds univ) {⊤}
have rw : Eq (α := Set γ) (Ici ⊤) {⊤}
Tactic: rw [isGreatest_univ.upperBounds_eq, Ici_top]
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
γ : Type u_3
inst : PartialOrder γ
inst_1 : OrderTop γ
rw : Eq (α := Set γ) (Ici ⊤) {⊤}
⊢ Eq (α := Set γ) (upperBounds univ) {⊤}
have rw₁ : Eq (α := Set γ) {⊤} {⊤}
Tactic: rw [isGreatest_univ.upperBounds_eq, Ici_top]
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
s : Set α
a : α
inst_1 : NoBotOrder α
hs : IsLUB s a
h : s = ∅
x : α
⊢ x ∈ upperBounds s
have rw : Membership.mem (γ := Set α) univ x
Tactic: rw [h, upperBounds_empty]
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
s : Set α
⊢ upperBounds (insert a s) = Ici a ∩ upperBounds s
have rw : upperBounds ({a} ∪ s) = Ici a ∩ upperBounds s
Tactic: rw [insert_eq, upperBounds_union, upperBounds_singleton]
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
s : Set α
rw : upperBounds ({a} ∪ s) = Ici a ∩ upperBounds s
⊢ upperBounds (insert a s) = Ici a ∩ upperBounds s
have rw₁ : upperBounds {a} ∩ upperBounds s = Ici a ∩ upperBounds s
Tactic: rw [insert_eq, upperBounds_union, upperBounds_singleton]
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
s : Set α
rw : upperBounds ({a} ∪ s) = Ici a ∩ upperBounds s
rw₁ : upperBounds {a} ∩ upperBounds s = Ici a ∩ upperBounds s
⊢ upperBounds (insert a s) = Ici a ∩ upperBounds s
have rw₂ : Ici a ∩ upperBounds s = Ici a ∩ upperBounds s
Tactic: rw [insert_eq, upperBounds_union, upperBounds_singleton]
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
s : Set α
a b : α
h : DirectedOn (fun (x y : α) ↦ y ≤ x) s
hMin : Minimal (fun (x : α) ↦ x ∈ s) a
hb : b ∈ s
⊢ a ≤ b
have obtain : ∀ (z : α) (hz : z ∈ s) (hza : z ≤ a) (hzb : z ≤ b), a ≤ b
Tactic: obtain ⟨z, hz, hza, hzb⟩ := h a hMin.1 b hb
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
s : Set α
a b : α
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hMax : Maximal (fun (x : α) ↦ x ∈ s) a
hb : b ∈ s
⊢ b ≤ a
have obtain : ∀ (z : α) (hz : z ∈ s) (haz : a ≤ z) (hbz : b ≤ z), b ≤ a
Tactic: obtain ⟨z, hz, haz, hbz⟩ := h a hMax.1 b hb
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
s s' : Set α
a b : α
h : (s ∩ s').Nonempty
ha : a ∈ lowerBounds s
hb : b ∈ upperBounds s'
⊢ a ≤ b
have have : ∀ (x : α) (hx : x ∈ s) (hx' : x ∈ s'), a ≤ b
Tactic: have ⟨x, hx, hx'⟩ := h
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set α
t : Set β
hs : s.Nonempty
ht : t.Nonempty
⊢ upperBounds (s ×ˢ t) = upperBounds s ×ˢ upperBounds t
have h : ∀ (x : α × β), x ∈ upperBounds (s ×ˢ t) ↔ x ∈ upperBounds s ×ˢ upperBounds t
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set α
t : Set β
hs : s.Nonempty
ht : t.Nonempty
x : α × β
⊢ x ∈ upperBounds (s ×ˢ t) ↔ x ∈ upperBounds s ×ˢ upperBounds t
have h : ∀ (hs : Nonempty.{u_1 + 1} (↑s : Type u_1)) (ht : Nonempty.{u_2 + 1} (↑t : Type u_2)) (x : α × β),
  x ∈ upperBounds (s ×ˢ t) ↔ x ∈ upperBounds s ×ˢ upperBounds t
Tactic: rw [← nonempty_coe_sort] at hs ht
Cleared hypotheses: hs, ht, x
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
a b : α
h : IsLUB s a
⊢ b < a ↔ ∃ c ∈ s, b < c
have simp_rw : ¬a ≤ b ↔ ∃ c ∈ s, ¬c ≤ b
Tactic: simp_rw [← not_le, isLUB_le_iff h, mem_upperBounds, not_forall, not_le, exists_prop]
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
a b : α
h : IsLUB s a
simp_rw : ¬a ≤ b ↔ ∃ c ∈ s, ¬c ≤ b
⊢ b < a ↔ ∃ c ∈ s, b < c
have simp_rw₁ : b ∉ upperBounds s ↔ ∃ c ∈ s, ¬c ≤ b
Tactic: simp_rw [← not_le, isLUB_le_iff h, mem_upperBounds, not_forall, not_le, exists_prop]
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
a b : α
h : IsLUB s a
simp_rw : ¬a ≤ b ↔ ∃ c ∈ s, ¬c ≤ b
simp_rw₁ : b ∉ upperBounds s ↔ ∃ c ∈ s, ¬c ≤ b
⊢ b < a ↔ ∃ c ∈ s, b < c
have simp_rw₂ : (¬∀ x ∈ s, x ≤ b) ↔ ∃ c ∈ s, ¬c ≤ b
Tactic: simp_rw [← not_le, isLUB_le_iff h, mem_upperBounds, not_forall, not_le, exists_prop]
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
a b : α
h : IsLUB s a
simp_rw : ¬a ≤ b ↔ ∃ c ∈ s, ¬c ≤ b
simp_rw₁ : b ∉ upperBounds s ↔ ∃ c ∈ s, ¬c ≤ b
simp_rw₂ : (¬∀ x ∈ s, x ≤ b) ↔ ∃ c ∈ s, ¬c ≤ b
⊢ b < a ↔ ∃ c ∈ s, b < c
have simp_rw₃ : (∃ (x : α) (_ : x ∈ s), ¬x ≤ b) ↔ ∃ c ∈ s, ¬c ≤ b
Tactic: simp_rw [← not_le, isLUB_le_iff h, mem_upperBounds, not_forall, not_le, exists_prop]
-- Lean 4 proof step from Mathlib.Order.Bounds.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
a b : α
h : IsLUB s a
simp_rw : ¬a ≤ b ↔ ∃ c ∈ s, ¬c ≤ b
simp_rw₁ : b ∉ upperBounds s ↔ ∃ c ∈ s, ¬c ≤ b
simp_rw₂ : (¬∀ x ∈ s, x ≤ b) ↔ ∃ c ∈ s, ¬c ≤ b
simp_rw₃ : (∃ (x : α) (_ : x ∈ s), ¬x ≤ b) ↔ ∃ c ∈ s, ¬c ≤ b
⊢ b < a ↔ ∃ c ∈ s, b < c
have simp_rw₄ : (∃ (x : α) (_ : x ∈ s), b < x) ↔ ∃ c ∈ s, b < c
Tactic: simp_rw [← not_le, isLUB_le_iff h, mem_upperBounds, not_forall, not_le, exists_prop]
-- Lean 4 proof step from Mathlib.Order.Bounds.Image (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s t : Set α
f : α → β
hst : IsCofinalFor s t
hf : Monotone f
⊢ IsCofinalFor (f '' s) (f '' t)
have simp : ∀ ⦃x : α⦄, x ∈ s → ∃ x_1 ∈ t, f x ≤ f x_1
Tactic: simp only [IsCofinalFor, forall_mem_image, exists_mem_image]
-- Lean 4 proof step from Mathlib.Order.Bounds.Image (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s t : Set α
f : α → β
hst : IsCofinalFor s t
hf : Monotone f
a : α
ha : a ∈ s
⊢ ∃ x ∈ t, f a ≤ f x
have obtain : ∀ (b : α) (hb : b ∈ t) (hab : a ≤ b), ∃ x ∈ t, f a ≤ f x
Tactic: obtain ⟨b, hb, hab⟩ := hst ha
-- Lean 4 proof step from Mathlib.Order.Bounds.Image (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s t : Set α
f : α → β
hst : IsCofinalFor s t
hf : Antitone f
⊢ IsCoinitialFor (f '' s) (f '' t)
have simp : ∀ ⦃x : α⦄, x ∈ s → ∃ x_1 ∈ t, f x_1 ≤ f x
Tactic: simp only [IsCoinitialFor, forall_mem_image, exists_mem_image]
-- Lean 4 proof step from Mathlib.Order.Bounds.Image (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s t : Set α
f : α → β
hst : IsCofinalFor s t
hf : Antitone f
a : α
ha : a ∈ s
⊢ ∃ x ∈ t, f x ≤ f a
have obtain : ∀ (b : α) (hb : b ∈ t) (hab : a ≤ b), ∃ x ∈ t, f x ≤ f a
Tactic: obtain ⟨b, hb, hab⟩ := hst ha
-- Lean 4 proof step from Mathlib.Order.Bounds.Image (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set (α × β)
p : α × β
⊢ IsLUB s p ↔ IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2
have refine_1 : ∀ (H : IsLUB s p) (a : α) (ha : a ∈ upperBounds (Prod.fst '' s)), p.1 ≤ a
Tactic: refine
    ⟨fun H =>
      ⟨⟨monotone_fst.mem_upperBounds_image H.1, fun a ha => ?_⟩,
        ⟨monotone_snd.mem_upperBounds_image H.1, fun a ha => ?_⟩⟩,
      fun H => ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.Bounds.Image (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set (α × β)
p : α × β
refine_1 : ∀ (H : IsLUB s p) (a : α) (ha : a ∈ upperBounds (Prod.fst '' s)), p.1 ≤ a
⊢ IsLUB s p ↔ IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2
have refine_2 : ∀ (H : IsLUB s p) (a : β) (ha : a ∈ upperBounds (Prod.snd '' s)), p.2 ≤ a
Tactic: refine
    ⟨fun H =>
      ⟨⟨monotone_fst.mem_upperBounds_image H.1, fun a ha => ?_⟩,
        ⟨monotone_snd.mem_upperBounds_image H.1, fun a ha => ?_⟩⟩,
      fun H => ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.Bounds.Image (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set (α × β)
p : α × β
refine_1 : ∀ (H : IsLUB s p) (a : α) (ha : a ∈ upperBounds (Prod.fst '' s)), p.1 ≤ a
refine_2 : ∀ (H : IsLUB s p) (a : β) (ha : a ∈ upperBounds (Prod.snd '' s)), p.2 ≤ a
⊢ IsLUB s p ↔ IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2
have refine_3 : ∀ (H : IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2), p ∈ upperBounds s
Tactic: refine
    ⟨fun H =>
      ⟨⟨monotone_fst.mem_upperBounds_image H.1, fun a ha => ?_⟩,
        ⟨monotone_snd.mem_upperBounds_image H.1, fun a ha => ?_⟩⟩,
      fun H => ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.Bounds.Image (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set (α × β)
p : α × β
refine_1 : ∀ (H : IsLUB s p) (a : α) (ha : a ∈ upperBounds (Prod.fst '' s)), p.1 ≤ a
refine_2 : ∀ (H : IsLUB s p) (a : β) (ha : a ∈ upperBounds (Prod.snd '' s)), p.2 ≤ a
refine_3 : ∀ (H : IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2), p ∈ upperBounds s
⊢ IsLUB s p ↔ IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2
have refine_4 : ∀ (H : IsLUB (Prod.fst '' s) p.1 ∧ IsLUB (Prod.snd '' s) p.2), p ∈ lowerBounds (upperBounds s)
Tactic: refine
    ⟨fun H =>
      ⟨⟨monotone_fst.mem_upperBounds_image H.1, fun a ha => ?_⟩,
        ⟨monotone_snd.mem_upperBounds_image H.1, fun a ha => ?_⟩⟩,
      fun H => ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.Bounds.Image (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB s p
a : α
ha : a ∈ upperBounds (Prod.fst '' s)
⊢ p.1 ≤ a
have refine_1 : (a, p.2) ∈ upperBounds s
Tactic: suffices h : (a, p.2) ∈ upperBounds s from (H.2 h).1
-- Lean 4 proof step from Mathlib.Order.Bounds.Image (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set (α × β)
p : α × β
H : IsLUB s p
a : β
ha : a ∈ upperBounds (Prod.snd '' s)
⊢ p.2 ≤ a
have refine_2 : (p.1, a) ∈ upperBounds s
Tactic: suffices h : (p.1, a) ∈ upperBounds s from (H.2 h).2
-- Lean 4 proof step from Mathlib.Order.Bounds.Image (goal)
Goal:
α : Type u
ι : Sort x
π : α → Type u_1
inst : (a : α) → Preorder (π a)
F : ι → (a : α) → π a
⊢ BddAbove (range F) ↔ ∀ (a : α), BddAbove.{u_1} (α := π a) (range fun (i : ι) ↦ F i a)
have simp : (∀ (a : α), BddAbove (range (eval (β := π) a ∘ F))) ↔ ∀ (a : α), BddAbove.{u_1} (α := π a) (range fun (i : ι) ↦ F i a)
Tactic: simp only [bddAbove_pi, ← range_comp]
-- Lean 4 proof step from Mathlib.Order.Bounds.Image (goal)
Goal:
α : Type u
π : α → Type u_1
inst : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
⊢ IsLUB s f ↔ ∀ (a : α), IsLUB (eval (β := π) a '' s) (f a)
have refine_1 : ∀ (H : IsLUB s f) (a : α) (b : π a) (hb : b ∈ upperBounds (eval (β := π) a '' s)), f a ≤ b
Tactic: refine
      ⟨fun H a => ⟨(Function.monotone_eval a).mem_upperBounds_image H.1, fun b hb => ?_⟩, fun H =>
        ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.Bounds.Image (goal)
Goal:
α : Type u
π : α → Type u_1
inst : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
refine_1 : ∀ (H : IsLUB s f) (a : α) (b : π a) (hb : b ∈ upperBounds (eval (β := π) a '' s)), f a ≤ b
⊢ IsLUB s f ↔ ∀ (a : α), IsLUB (eval (β := π) a '' s) (f a)
have refine_2 : ∀ (H : ∀ (a : α), IsLUB (eval (β := π) a '' s) (f a)), f ∈ upperBounds s
Tactic: refine
      ⟨fun H a => ⟨(Function.monotone_eval a).mem_upperBounds_image H.1, fun b hb => ?_⟩, fun H =>
        ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.Bounds.Image (goal)
Goal:
α : Type u
π : α → Type u_1
inst : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
refine_1 : ∀ (H : IsLUB s f) (a : α) (b : π a) (hb : b ∈ upperBounds (eval (β := π) a '' s)), f a ≤ b
refine_2 : ∀ (H : ∀ (a : α), IsLUB (eval (β := π) a '' s) (f a)), f ∈ upperBounds s
⊢ IsLUB s f ↔ ∀ (a : α), IsLUB (eval (β := π) a '' s) (f a)
have refine_3 : ∀ (H : ∀ (a : α), IsLUB (eval (β := π) a '' s) (f a)), f ∈ lowerBounds (upperBounds s)
Tactic: refine
      ⟨fun H a => ⟨(Function.monotone_eval a).mem_upperBounds_image H.1, fun b hb => ?_⟩, fun H =>
        ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.Bounds.Image (goal)
Goal:
α : Type u
π : α → Type u_1
inst : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : IsLUB s f
a : α
b : π a
hb : b ∈ upperBounds (eval (β := π) a '' s)
⊢ f a ≤ b
have refine_1 : update (β := π) f a b ∈ upperBounds s
Tactic: suffices h : Function.update f a b ∈ upperBounds s from Function.update_self a b f ▸ H.2 h a
-- Lean 4 proof step from Mathlib.Order.Bounds.Image (goal)
Goal:
α : Type u
π : α → Type u_1
inst : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
⊢ IsLUB s f ↔ ∀ (a : α), IsLUB (eval (β := π) a '' s) (f a)
have refine_1 : ∀ (H : IsLUB s f) (a : α) (b : π a) (hb : b ∈ upperBounds (eval (β := π) a '' s)), f a ≤ b
Tactic: classical
    refine
      ⟨fun H a => ⟨(Function.monotone_eval a).mem_upperBounds_image H.1, fun b hb => ?_⟩, fun H =>
        ⟨?_, ?_⟩⟩
    · suffices h : Function.update f a b ∈ upperBounds s from Function.update_self a b f ▸ H.2 h a
      exact fun g hg => le_update_iff.2 ⟨hb <| mem_image_of_mem _ hg, fun i _ => H.1 hg i⟩
    · exact fun g hg a => (H a).1 (mem_image_of_mem _ hg)
    · exact fun g hg a => (H a).2 ((Function.monotone_eval a).mem_upperBounds_image hg)
-- Lean 4 proof step from Mathlib.Order.Bounds.Image (goal)
Goal:
α : Type u
π : α → Type u_1
inst : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
refine_1 : ∀ (H : IsLUB s f) (a : α) (b : π a) (hb : b ∈ upperBounds (eval (β := π) a '' s)), f a ≤ b
⊢ IsLUB s f ↔ ∀ (a : α), IsLUB (eval (β := π) a '' s) (f a)
have refine_2 : ∀ (H : ∀ (a : α), IsLUB (eval (β := π) a '' s) (f a)), f ∈ upperBounds s
Tactic: classical
    refine
      ⟨fun H a => ⟨(Function.monotone_eval a).mem_upperBounds_image H.1, fun b hb => ?_⟩, fun H =>
        ⟨?_, ?_⟩⟩
    · suffices h : Function.update f a b ∈ upperBounds s from Function.update_self a b f ▸ H.2 h a
      exact fun g hg => le_update_iff.2 ⟨hb <| mem_image_of_mem _ hg, fun i _ => H.1 hg i⟩
    · exact fun g hg a => (H a).1 (mem_image_of_mem _ hg)
    · exact fun g hg a => (H a).2 ((Function.monotone_eval a).mem_upperBounds_image hg)
-- Lean 4 proof step from Mathlib.Order.Bounds.Image (goal)
Goal:
α : Type u
π : α → Type u_1
inst : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
refine_1 : ∀ (H : IsLUB s f) (a : α) (b : π a) (hb : b ∈ upperBounds (eval (β := π) a '' s)), f a ≤ b
refine_2 : ∀ (H : ∀ (a : α), IsLUB (eval (β := π) a '' s) (f a)), f ∈ upperBounds s
⊢ IsLUB s f ↔ ∀ (a : α), IsLUB (eval (β := π) a '' s) (f a)
have refine_3 : ∀ (H : ∀ (a : α), IsLUB (eval (β := π) a '' s) (f a)), f ∈ lowerBounds (upperBounds s)
Tactic: classical
    refine
      ⟨fun H a => ⟨(Function.monotone_eval a).mem_upperBounds_image H.1, fun b hb => ?_⟩, fun H =>
        ⟨?_, ?_⟩⟩
    · suffices h : Function.update f a b ∈ upperBounds s from Function.update_self a b f ▸ H.2 h a
      exact fun g hg => le_update_iff.2 ⟨hb <| mem_image_of_mem _ hg, fun i _ => H.1 hg i⟩
    · exact fun g hg a => (H a).1 (mem_image_of_mem _ hg)
    · exact fun g hg a => (H a).2 ((Function.monotone_eval a).mem_upperBounds_image hg)
-- Lean 4 proof step from Mathlib.Order.Bounds.Image (goal)
Goal:
α : Type u
β : Type v
inst : Preorder β
f g : α → β
h : ∀ (a : α), f a ≤ g a
hbdd : BddAbove (range g)
⊢ BddAbove (range f)
have obtain : ∀ (C : β) (hC : C ∈ upperBounds (range g)), BddAbove (range f)
Tactic: obtain ⟨C, hC⟩ := hbdd
Cleared hypotheses: hbdd
-- Lean 4 proof step from Mathlib.Order.Bounds.Image (goal)
Goal:
α : Type u
β : Type v
inst : Preorder β
f g : α → β
h : ∀ (a : α), f a ≤ g a
C : β
hC : C ∈ upperBounds (range g)
⊢ BddAbove (range f)
have h₁ : C ∈ upperBounds (range f)
Tactic: use C
-- Lean 4 proof step from Mathlib.Order.Bounds.Image (goal)
Goal:
α : Type u
β : Type v
γ : Type u_1
inst : Preorder β
inst_1 : Preorder γ
f : α → β
g : β → γ
hf : BddAbove (range f)
hg : Monotone g
⊢ BddAbove.{u_1} (α := γ) (range fun (x : α) ↦ g (f x))
have change : BddAbove (range (g ∘ f))
Tactic: change BddAbove (range (g ∘ f))
-- Lean 4 proof step from Mathlib.Order.Bounds.Lattice (goal)
Goal:
α : Type u_1
inst : Preorder α
ι : Sort u_2
s : ι → Set α
u : ι → α
hs : ∀ (i : ι), IsLUB (s i) (u i)
c : α
⊢ IsLUB (range u) c ↔ IsLUB (⋃ (i : ι), s i) c
have refine : upperBounds (range u) = upperBounds (⋃ (i : ι), s i)
Tactic: refine isLUB_congr ?_
-- Lean 4 proof step from Mathlib.Order.Bounds.Lattice (goal)
Goal:
α : Type u_1
inst : Preorder α
ι : Sort u_2
s : ι → Set α
u : ι → α
hs : ∀ (i : ι), IsLUB (s i) (u i)
c : α
⊢ upperBounds (range u) = upperBounds (⋃ (i : ι), s i)
have simp_rw : Eq.{u_1 + 1} (α := Set α) (upperBounds (⋃ (i : ι), {u i})) (upperBounds (⋃ (i : ι), s i))
Tactic: simp_rw [range_eq_iUnion, upperBounds_iUnion, upperBounds_singleton, (hs _).upperBounds_eq]
-- Lean 4 proof step from Mathlib.Order.Bounds.Lattice (goal)
Goal:
α : Type u_1
inst : Preorder α
ι : Sort u_2
s : ι → Set α
u : ι → α
hs : ∀ (i : ι), IsLUB (s i) (u i)
c : α
simp_rw : Eq.{u_1 + 1} (α := Set α) (upperBounds (⋃ (i : ι), {u i})) (upperBounds (⋃ (i : ι), s i))
⊢ upperBounds (range u) = upperBounds (⋃ (i : ι), s i)
have simp_rw₁ : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), upperBounds {u i}) (⋂ (i : ι), upperBounds (s i))
Tactic: simp_rw [range_eq_iUnion, upperBounds_iUnion, upperBounds_singleton, (hs _).upperBounds_eq]
-- Lean 4 proof step from Mathlib.Order.Bounds.Lattice (goal)
Goal:
α : Type u_1
inst : Preorder α
ι : Sort u_2
s : ι → Set α
u : ι → α
hs : ∀ (i : ι), IsLUB (s i) (u i)
c : α
simp_rw : Eq.{u_1 + 1} (α := Set α) (upperBounds (⋃ (i : ι), {u i})) (upperBounds (⋃ (i : ι), s i))
simp_rw₁ : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), upperBounds {u i}) (⋂ (i : ι), upperBounds (s i))
⊢ upperBounds (range u) = upperBounds (⋃ (i : ι), s i)
have simp_rw₂ : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), Ici (u i)) (⋂ (i : ι), upperBounds (s i))
Tactic: simp_rw [range_eq_iUnion, upperBounds_iUnion, upperBounds_singleton, (hs _).upperBounds_eq]
-- Lean 4 proof step from Mathlib.Order.Bounds.Lattice (goal)
Goal:
α : Type u_1
inst : Preorder α
ι : Sort u_2
s : ι → Set α
u : ι → α
hs : ∀ (i : ι), IsGLB (s i) (u i)
c : α
⊢ IsGLB (range u) c ↔ IsGLB (⋃ (i : ι), s i) c
have refine : lowerBounds (range u) = lowerBounds (⋃ (i : ι), s i)
Tactic: refine isGLB_congr ?_
-- Lean 4 proof step from Mathlib.Order.Bounds.Lattice (goal)
Goal:
α : Type u_1
inst : Preorder α
ι : Sort u_2
s : ι → Set α
u : ι → α
hs : ∀ (i : ι), IsGLB (s i) (u i)
c : α
⊢ lowerBounds (range u) = lowerBounds (⋃ (i : ι), s i)
have simp_rw : Eq.{u_1 + 1} (α := Set α) (lowerBounds (⋃ (i : ι), {u i})) (lowerBounds (⋃ (i : ι), s i))
Tactic: simp_rw [range_eq_iUnion, lowerBounds_iUnion, lowerBounds_singleton, (hs _).lowerBounds_eq]
-- Lean 4 proof step from Mathlib.Order.Bounds.Lattice (goal)
Goal:
α : Type u_1
inst : Preorder α
ι : Sort u_2
s : ι → Set α
u : ι → α
hs : ∀ (i : ι), IsGLB (s i) (u i)
c : α
simp_rw : Eq.{u_1 + 1} (α := Set α) (lowerBounds (⋃ (i : ι), {u i})) (lowerBounds (⋃ (i : ι), s i))
⊢ lowerBounds (range u) = lowerBounds (⋃ (i : ι), s i)
have simp_rw₁ : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), lowerBounds {u i}) (⋂ (i : ι), lowerBounds (s i))
Tactic: simp_rw [range_eq_iUnion, lowerBounds_iUnion, lowerBounds_singleton, (hs _).lowerBounds_eq]
-- Lean 4 proof step from Mathlib.Order.Bounds.Lattice (goal)
Goal:
α : Type u_1
inst : Preorder α
ι : Sort u_2
s : ι → Set α
u : ι → α
hs : ∀ (i : ι), IsGLB (s i) (u i)
c : α
simp_rw : Eq.{u_1 + 1} (α := Set α) (lowerBounds (⋃ (i : ι), {u i})) (lowerBounds (⋃ (i : ι), s i))
simp_rw₁ : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), lowerBounds {u i}) (⋂ (i : ι), lowerBounds (s i))
⊢ lowerBounds (range u) = lowerBounds (⋃ (i : ι), s i)
have simp_rw₂ : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), Iic (u i)) (⋂ (i : ι), lowerBounds (s i))
Tactic: simp_rw [range_eq_iUnion, lowerBounds_iUnion, lowerBounds_singleton, (hs _).lowerBounds_eq]
-- Lean 4 proof step from Mathlib.Order.Bounds.OrderIso (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
s : Set α
x : α
⊢ IsLUB.{u_2} (α := β) ((⇑f : (a : α) → β) '' s : Set β) ((f : (a : α) → β) x : β) ↔ IsLUB s x
have rw : IsLUB s ((f.symm : (a : β) → α) ((f : (a : α) → β) x : β)) ↔ IsLUB s x
Tactic: rw [isLUB_image, f.symm_apply_apply]
-- Lean 4 proof step from Mathlib.Order.Bounds.OrderIso (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
s : Set α
x : α
rw : IsLUB s ((f.symm : (a : β) → α) ((f : (a : α) → β) x : β)) ↔ IsLUB s x
⊢ IsLUB.{u_2} (α := β) ((⇑f : (a : α) → β) '' s : Set β) ((f : (a : α) → β) x : β) ↔ IsLUB s x
have rw₁ : IsLUB s x ↔ IsLUB s x
Tactic: rw [isLUB_image, f.symm_apply_apply]
-- Lean 4 proof step from Mathlib.Order.Bounds.OrderIso (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
s : Set β
x : α
⊢ IsLUB ((⇑f : (a : α) → β) ⁻¹' s) x ↔ IsLUB s ((f : (a : α) → β) x)
have rw : IsLUB ((⇑f.symm.symm : (a : α) → β) ⁻¹' s) x ↔ IsLUB s ((f.symm.symm : (a : α) → β) x)
Tactic: rw [← f.symm_symm, ← image_eq_preimage_symm, isLUB_image]
-- Lean 4 proof step from Mathlib.Order.Bounds.OrderIso (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
s : Set β
x : α
rw : IsLUB ((⇑f.symm.symm : (a : α) → β) ⁻¹' s) x ↔ IsLUB s ((f.symm.symm : (a : α) → β) x)
⊢ IsLUB ((⇑f : (a : α) → β) ⁻¹' s) x ↔ IsLUB s ((f : (a : α) → β) x)
have rw₁ : IsLUB ((⇑f.symm : (a : β) → α) '' s) x ↔ IsLUB s ((f.symm.symm : (a : α) → β) x)
Tactic: rw [← f.symm_symm, ← image_eq_preimage_symm, isLUB_image]
-- Lean 4 proof step from Mathlib.Order.Bounds.OrderIso (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
s : Set β
x : α
rw : IsLUB ((⇑f.symm.symm : (a : α) → β) ⁻¹' s) x ↔ IsLUB s ((f.symm.symm : (a : α) → β) x)
rw₁ : IsLUB ((⇑f.symm : (a : β) → α) '' s) x ↔ IsLUB s ((f.symm.symm : (a : α) → β) x)
⊢ IsLUB ((⇑f : (a : α) → β) ⁻¹' s) x ↔ IsLUB s ((f : (a : α) → β) x)
have rw₂ : IsLUB s ((f.symm.symm : (a : α) → β) x) ↔ IsLUB s ((f.symm.symm : (a : α) → β) x)
Tactic: rw [← f.symm_symm, ← image_eq_preimage_symm, isLUB_image]
-- Lean 4 proof step from Mathlib.Order.Bounds.OrderIso (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
s : Set β
x : β
⊢ IsLUB.{u_1} (α := α) ((⇑f : (a : α) → β) ⁻¹' s : Set α) ((f.symm : (a : β) → α) x : α) ↔ IsLUB s x
have rw : IsLUB s ((f : (a : α) → β) ((f.symm : (a : β) → α) x : α)) ↔ IsLUB s x
Tactic: rw [isLUB_preimage, f.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Order.Bounds.OrderIso (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
s : Set β
x : β
rw : IsLUB s ((f : (a : α) → β) ((f.symm : (a : β) → α) x : α)) ↔ IsLUB s x
⊢ IsLUB.{u_1} (α := α) ((⇑f : (a : α) → β) ⁻¹' s : Set α) ((f.symm : (a : β) → α) x : α) ↔ IsLUB s x
have rw₁ : IsLUB s x ↔ IsLUB s x
Tactic: rw [isLUB_preimage, f.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : (↑c : Set α) ⊆ Ici x
⊢ cSup c ∈ Ici x
have have : ∀ (y : α) (hy : y ∈ c.carrier), cSup c ∈ Ici x
Tactic: have ⟨y, hy⟩ := c.Nonempty'
-- Lean 4 proof step from Mathlib.Order.BourbakiWitt (goal)
Goal:
α : Type u_1
inst : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ IsLeast (bot x f) x
have left : x ∈ bot x f
Tactic: constructor