awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : s.Nonempty
left : sSup s ∈ upperBounds s
⊢ IsLUB s (sSup s)
have right : sSup s ∈ lowerBounds (upperBounds s)
Tactic: classical
  constructor
  · change ite _ _ _ ∈ _
    split_ifs with h₁ h₂
    · intro _ _
      exact le_top
    · rintro (⟨⟩ | a) ha
      · contradiction
      apply coe_le_coe.2
      exact le_csSup h₂ ha
    · intro _ _
      exact le_top
  · change ite _ _ _ ∈ _
    split_ifs with h₁ h₂
    · rintro (⟨⟩ | a) ha
      · exact le_rfl
      · exact False.elim (not_top_le_coe a (ha h₁))
    · rintro (⟨⟩ | b) hb
      · exact le_top
      refine coe_le_coe.2 (csSup_le ?_ ?_)
      · rcases hs with ⟨⟨⟩ | b, hb⟩
        · exact absurd hb h₁
        · exact ⟨b, hb⟩
      · intro a ha
        exact coe_le_coe.1 (hb ha)
    · rintro (⟨⟩ | b) hb
      · exact le_rfl
      · exfalso
        apply h₂
        use b
        intro a ha
        exact coe_le_coe.1 (hb ha)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
⊢ IsLUB s (sSup s)
have inl : IsLUB.{u_1} (α := WithTop α) ∅ (sSup ∅)
Tactic: rcases s.eq_empty_or_nonempty with rfl | hs
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
inl : IsLUB.{u_1} (α := WithTop α) ∅ (sSup ∅)
⊢ IsLUB s (sSup s)
have inr : ∀ (hs : s.Nonempty), IsLUB s (sSup s)
Tactic: rcases s.eq_empty_or_nonempty with rfl | hs
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
⊢ IsGLB s (sInf s)
have left : sInf s ∈ lowerBounds s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
left : sInf s ∈ lowerBounds s
⊢ IsGLB s (sInf s)
have right : sInf s ∈ upperBounds (lowerBounds s)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
⊢ (if s ⊆ {⊤} ∨ ¬BddBelow s then ⊤ else (↑(sInf ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β)) ∈ lowerBounds s
have left : (if s ⊆ {⊤} then ⊤ else (↑(sInf ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β)) ∈ lowerBounds s
Tactic: simp only [hs, not_true_eq_false, or_false]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
⊢ (if s ⊆ {⊤} then ⊤ else (↑(sInf ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β)) ∈ lowerBounds s
have pos : ∀ (h : s ⊆ {⊤}), ⊤ ∈ lowerBounds s
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
pos : ∀ (h : s ⊆ {⊤}), ⊤ ∈ lowerBounds s
⊢ (if s ⊆ {⊤} then ⊤ else (↑(sInf ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β)) ∈ lowerBounds s
have neg : ∀ (h : ¬s ⊆ {⊤}), (↑(sInf ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β) ∈ lowerBounds s
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
⊢ (↑(sInf ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β) ≤ Option.some a
have neg : BddBelow (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
Tactic: refine coe_le_coe.2 (csInf_le ?_ ha)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
⊢ BddBelow (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
have neg : ∀ (hb : none ∈ lowerBounds s), BddBelow (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
Tactic: rcases hs with ⟨⟨⟩ | b, hb⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
neg : ∀ (hb : none ∈ lowerBounds s), BddBelow (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
⊢ BddBelow (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
have neg₁ : ∀ (b : β) (hb : Option.some b ∈ lowerBounds s), BddBelow (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
Tactic: rcases hs with ⟨⟨⟩ | b, hb⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
hb : none ∈ lowerBounds s
⊢ BddBelow (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
have neg : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
hb : none ∈ lowerBounds s
⊢ False
have neg : s ⊆ {⊤}
Tactic: apply h
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
hb : none ∈ lowerBounds s
c : WithTop β
hc : c ∈ s
⊢ Membership.mem (γ := Set (WithTop β)) {⊤} c
have neg : ⊤ ≤ c
Tactic: rw [mem_singleton_iff, ← top_le_iff]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ s
b : β
hb : Option.some b ∈ lowerBounds s
⊢ BddBelow (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
have h₁ : Membership.mem (γ := Set β) (lowerBounds ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) b
Tactic: use b
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
⊢ (if s ⊆ {⊤} ∨ ¬BddBelow s then ⊤ else (↑(sInf ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β)) ∈
    upperBounds (lowerBounds s)
have right : (if s ⊆ {⊤} then ⊤ else (↑(sInf ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β)) ∈ upperBounds (lowerBounds s)
Tactic: simp only [hs, not_true_eq_false, or_false]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
⊢ (if s ⊆ {⊤} then ⊤ else (↑(sInf ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β)) ∈ upperBounds (lowerBounds s)
have pos : ∀ (h : s ⊆ {⊤}), ⊤ ∈ upperBounds (lowerBounds s)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
pos : ∀ (h : s ⊆ {⊤}), ⊤ ∈ upperBounds (lowerBounds s)
⊢ (if s ⊆ {⊤} then ⊤ else (↑(sInf ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β)) ∈ upperBounds (lowerBounds s)
have neg : ∀ (h : ¬s ⊆ {⊤}), (↑(sInf ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β) ∈ upperBounds (lowerBounds s)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
ha : none ∈ lowerBounds s
⊢ LE.le (α := WithTop β) none (↑(sInf ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β)
have neg : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
ha : none ∈ lowerBounds s
⊢ False
have neg : s ⊆ {⊤}
Tactic: apply h
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
⊢ Option.some a ≤ (↑(sInf ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β)
have neg : Set.Nonempty (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
Tactic: refine coe_le_coe.2 (le_csInf ?_ ?_)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
neg : Set.Nonempty (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
⊢ Option.some a ≤ (↑(sInf ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)) : WithTop β)
have neg₁ : ∀ (b : β), Membership.mem (γ := Set β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s) b → a ≤ b
Tactic: refine coe_le_coe.2 (le_csInf ?_ ?_)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
⊢ Set.Nonempty (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
have neg : ∀ (h : Eq (α := Set β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s) ∅), s ⊆ {⊤}
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
⊢ Set.Nonempty (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
have neg : ∀ (h : ¬s ⊆ {⊤}), Set.Nonempty (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
Tactic: classical
            contrapose! h
            rintro (⟨⟩ | a) ha
            · exact mem_singleton ⊤
            · exact (not_nonempty_iff_eq_empty.2 h ⟨a, ha⟩).elim
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
neg neg₁ : ∀ (h : ¬s ⊆ {⊤}), Set.Nonempty (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
⊢ Set.Nonempty (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
have neg₂ : Eq (α := Set β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s) ∅ → s ⊆ {⊤}
Tactic: classical
            contrapose! h
            rintro (⟨⟩ | a) ha
            · exact mem_singleton ⊤
            · exact (not_nonempty_iff_eq_empty.2 h ⟨a, ha⟩).elim
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
neg neg₁ : ∀ (h : ¬s ⊆ {⊤}), Set.Nonempty (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
neg₂ neg₃ neg₄ : ∀ (h : Eq (α := Set β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s) ∅), s ⊆ {⊤}
⊢ Set.Nonempty (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
have neg₅ : ∀ (h : Eq (α := Set β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s) ∅) (ha : none ∈ s),
  Membership.mem (γ := Set (WithTop β)) {⊤} none
Tactic: classical
            contrapose! h
            rintro (⟨⟩ | a) ha
            · exact mem_singleton ⊤
            · exact (not_nonempty_iff_eq_empty.2 h ⟨a, ha⟩).elim
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
neg neg₁ : ∀ (h : ¬s ⊆ {⊤}), Set.Nonempty (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
neg₂ neg₃ neg₄ : ∀ (h : Eq (α := Set β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s) ∅), s ⊆ {⊤}
neg₅ :
  ∀ (h : Eq (α := Set β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s) ∅) (ha : none ∈ s),
    Membership.mem (γ := Set (WithTop β)) {⊤} none
⊢ Set.Nonempty (α := β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s)
have neg₆ : ∀ (h : Eq (α := Set β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s) ∅) (a : β) (ha : Option.some a ∈ s),
  Membership.mem (γ := Set (WithTop β)) {⊤} (Option.some a)
Tactic: classical
            contrapose! h
            rintro (⟨⟩ | a) ha
            · exact mem_singleton ⊤
            · exact (not_nonempty_iff_eq_empty.2 h ⟨a, ha⟩).elim
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
h : ¬s ⊆ {⊤}
a : β
ha : Option.some a ∈ lowerBounds s
b : β
hb : Membership.mem (γ := Set β) ((fun (a : β) ↦ (↑a : WithTop β)) ⁻¹' s) b
⊢ a ≤ b
have neg : (↑a : WithTop β) ≤ (↑b : WithTop β)
Tactic: rw [← coe_le_coe]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
⊢ IsGLB s (sInf s)
have left : sInf s ∈ lowerBounds s
Tactic: classical
  constructor
  · change ite _ _ _ ∈ _
    simp only [hs, not_true_eq_false, or_false]
    split_ifs with h
    · intro a ha
      exact top_le_iff.2 (Set.mem_singleton_iff.1 (h ha))
    · rintro (⟨⟩ | a) ha
      · exact le_top
      refine coe_le_coe.2 (csInf_le ?_ ha)
      rcases hs with ⟨⟨⟩ | b, hb⟩
      · exfalso
        apply h
        intro c hc
        rw [mem_singleton_iff, ← top_le_iff]
        exact hb hc
      use b
      intro c hc
      exact coe_le_coe.1 (hb hc)
  · change ite _ _ _ ∈ _
    simp only [hs, not_true_eq_false, or_false]
    split_ifs with h
    · intro _ _
      exact le_top
    · rintro (⟨⟩ | a) ha
      · exfalso
        apply h
        intro b hb
        exact Set.mem_singleton_iff.2 (top_le_iff.1 (ha hb))
      · refine coe_le_coe.2 (le_csInf ?_ ?_)
        · classical
            contrapose! h
            rintro (⟨⟩ | a) ha
            · exact mem_singleton ⊤
            · exact (not_nonempty_iff_eq_empty.2 h ⟨a, ha⟩).elim
        · intro b hb
          rw [← coe_le_coe]
          exact ha hb
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
β : Type u_5
inst : ConditionallyCompleteLattice β
s : Set (WithTop β)
hs : BddBelow s
left : sInf s ∈ lowerBounds s
⊢ IsGLB s (sInf s)
have right : sInf s ∈ upperBounds (lowerBounds s)
Tactic: classical
  constructor
  · change ite _ _ _ ∈ _
    simp only [hs, not_true_eq_false, or_false]
    split_ifs with h
    · intro a ha
      exact top_le_iff.2 (Set.mem_singleton_iff.1 (h ha))
    · rintro (⟨⟩ | a) ha
      · exact le_top
      refine coe_le_coe.2 (csInf_le ?_ ha)
      rcases hs with ⟨⟨⟩ | b, hb⟩
      · exfalso
        apply h
        intro c hc
        rw [mem_singleton_iff, ← top_le_iff]
        exact hb hc
      use b
      intro c hc
      exact coe_le_coe.1 (hb hc)
  · change ite _ _ _ ∈ _
    simp only [hs, not_true_eq_false, or_false]
    split_ifs with h
    · intro _ _
      exact le_top
    · rintro (⟨⟩ | a) ha
      · exfalso
        apply h
        intro b hb
        exact Set.mem_singleton_iff.2 (top_le_iff.1 (ha hb))
      · refine coe_le_coe.2 (le_csInf ?_ ?_)
        · classical
            contrapose! h
            rintro (⟨⟩ | a) ha
            · exact mem_singleton ⊤
            · exact (not_nonempty_iff_eq_empty.2 h ⟨a, ha⟩).elim
        · intro b hb
          rw [← coe_le_coe]
          exact ha hb
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
⊢ IsGLB s (sInf s)
have pos : ∀ (hs : BddBelow s), IsGLB s (sInf s)
Tactic: by_cases hs : BddBelow s
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s : Set (WithTop α)
pos : ∀ (hs : BddBelow s), IsGLB s (sInf s)
⊢ IsGLB s (sInf s)
have neg : ∀ (hs : ¬BddBelow s), IsGLB s (sInf s)
Tactic: by_cases hs : BddBelow s
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
hb : BddAbove s
⊢ (↑(sSup s) : WithTop α) = ⨆ a ∈ s, (↑a : WithTop α)
have rw : Eq (α := WithTop α) (sSup ((fun (a : α) ↦ (↑a : WithTop α)) '' s)) (⨆ a ∈ s, (↑a : WithTop α))
Tactic: rw [coe_sSup' hb, sSup_image]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
hb : BddAbove s
rw : Eq (α := WithTop α) (sSup ((fun (a : α) ↦ (↑a : WithTop α)) '' s)) (⨆ a ∈ s, (↑a : WithTop α))
⊢ (↑(sSup s) : WithTop α) = ⨆ a ∈ s, (↑a : WithTop α)
have rw₁ : Eq.{u_1 + 1} (α := WithTop α) (⨆ a ∈ s, (↑a : WithTop α)) (⨆ a ∈ s, (↑a : WithTop α))
Tactic: rw [coe_sSup' hb, sSup_image]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : s.Nonempty
h's : BddBelow s
⊢ (↑(sInf s) : WithTop α) = ⨅ a ∈ s, (↑a : WithTop α)
have rw : Eq (α := WithTop α) (sInf ((fun (a : α) ↦ (↑a : WithTop α)) '' s)) (⨅ a ∈ s, (↑a : WithTop α))
Tactic: rw [coe_sInf' hs h's, sInf_image]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : s.Nonempty
h's : BddBelow s
rw : Eq (α := WithTop α) (sInf ((fun (a : α) ↦ (↑a : WithTop α)) '' s)) (⨅ a ∈ s, (↑a : WithTop α))
⊢ (↑(sInf s) : WithTop α) = ⨅ a ∈ s, (↑a : WithTop α)
have rw₁ : Eq.{u_1 + 1} (α := WithTop α) (⨅ a ∈ s, (↑a : WithTop α)) (⨅ a ∈ s, (↑a : WithTop α))
Tactic: rw [coe_sInf' hs h's, sInf_image]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
⊢ sInf (f '' s) = sInf (f '' t)
have inl : ∀ (hst : ∅ ⊆ t) (h : ∀ y ∈ t, ∃ (x : α), Membership.mem (γ := Set α) ∅ x ∧ x ≤ y), sInf (f '' ∅) = sInf (f '' t)
Tactic: obtain rfl | hs := Set.eq_empty_or_nonempty s
Cleared hypotheses: s, hst, h
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
inl : ∀ (hst : ∅ ⊆ t) (h : ∀ y ∈ t, ∃ (x : α), Membership.mem (γ := Set α) ∅ x ∧ x ≤ y), sInf (f '' ∅) = sInf (f '' t)
⊢ sInf (f '' s) = sInf (f '' t)
have inr : ∀ (hs : s.Nonempty), sInf (f '' s) = sInf (f '' t)
Tactic: obtain rfl | hs := Set.eq_empty_or_nonempty s
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : ∅ ⊆ t
h : ∀ y ∈ t, ∃ (x : α), Membership.mem (γ := Set α) ∅ x ∧ x ≤ y
⊢ sInf (f '' ∅) = sInf (f '' t)
have inl : ∀ (ht : BddBelow (f '' ∅)) (hf : MonotoneOn f ∅) (hst : Subset.{u_1} (α := Set α) ∅ ∅)
  (h : ∀ (y : α), Membership.mem (γ := Set α) ∅ y → ∃ (x : α), Membership.mem (γ := Set α) ∅ x ∧ x ≤ y),
  sInf (f '' ∅) = sInf (f '' ∅)
Tactic: obtain rfl : t = ∅ := by simpa [Set.eq_empty_iff_forall_notMem] using h
Cleared hypotheses: t, ht, hf, hst, h
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
ht₁ : BddBelow (f '' t)
⊢ sInf (f '' t) ≤ sInf (f '' s)
have hs₁ : (f '' s).Nonempty
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
⊢ sInf (f '' s) = sInf (f '' t)
have inr : sInf (f '' s) ≤ sInf (f '' t)
Tactic: refine le_antisymm ?_ (by gcongr; exacts [ht, hs.image f])
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
⊢ sInf (f '' s) ≤ sInf (f '' t)
have inr : ∀ b ∈ f '' t, sInf (f '' s) ≤ b
Tactic: refine le_csInf ((hs.mono hst).image f) ?_
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
⊢ ∀ b ∈ f '' t, sInf (f '' s) ≤ b
have inr : ∀ a ∈ t, sInf (f '' s) ≤ f a
Tactic: simp only [mem_image, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
s t : Set α
ht : BddBelow (f '' t)
hf : MonotoneOn f t
hst : s ⊆ t
h : ∀ y ∈ t, ∃ x ∈ s, x ≤ y
hs : s.Nonempty
a : α
ha : a ∈ t
⊢ sInf (f '' s) ≤ f a
have inr : ∀ (x : α) (hxs : x ∈ s) (hxa : x ≤ a), sInf (f '' s) ≤ f a
Tactic: obtain ⟨x, hxs, hxa⟩ := h a ha
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
⊢ sInf (f '' Icc a b) = f a
have refine : IsGLB (f '' Icc a b) (f a)
Tactic: refine IsGLB.csInf_eq ?_ ((nonempty_Icc.mpr hab).image f)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
⊢ IsGLB (f '' Icc a b) (f a)
have refine_1 : ∀ b' ≤ f a, b' ∈ lowerBounds (f '' Icc a b)
Tactic: refine isGLB_iff_le_iff.mpr (fun b' ↦ ⟨?_, ?_⟩)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
refine_1 : ∀ b' ≤ f a, b' ∈ lowerBounds (f '' Icc a b)
⊢ IsGLB (f '' Icc a b) (f a)
have refine_2 : ∀ b' ∈ lowerBounds (f '' Icc a b), b' ≤ f a
Tactic: refine isGLB_iff_le_iff.mpr (fun b' ↦ ⟨?_, ?_⟩)
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
⊢ Icc a b = Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a)
have rw : Icc a b = (⇑ofDual : (a : αᵒᵈ) → α) ⁻¹' Icc a b
Tactic: rw [Icc_toDual]
-- Lean 4 proof step from Mathlib.Order.ConditionallyCompleteLattice.Basic (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : ConditionallyCompleteLattice β
f : α → β
a b : α
hab : a ≤ b
h' : MonotoneOn f (Icc a b)
⊢ sSup (f '' Icc a b) = f b
have this : Icc a b = Icc ((toDual : (a : α) → αᵒᵈ) b) ((toDual : (a : α) → αᵒᵈ) a)
Tactic: have : Icc a b = Icc (α := αᵒᵈ) (toDual b) (toDual a) := by rw [Icc_toDual]; rfl