awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_6
inst : PartialOrder α
c : Concept α α fun (x1 x2 : α) ↦ x1 < x2
a b : α
hb_1 : b ≤ a
ha : a ∈ c.extent (r := fun (x1 x2 : α) ↦ x1 < x2)
hb : b < a
⊢ b ∈ c.extent (r := fun (x1 x2 : α) ↦ x1 < x2)

Tactic:
exact mem_extent_of_rel_extent hb ha

Premises used: Concept.mem_extent_of_rel_extent
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_6
inst : PartialOrder α
c : Concept α α fun (x1 x2 : α) ↦ x1 < x2
a b : α
hb : a ≤ b
ha : a ∈ c.intent (r := fun (x1 x2 : α) ↦ x1 < x2)
inl : ∀ (hb : a ≤ a), a ∈ c.intent (r := fun (x1 x2 : α) ↦ x1 < x2)
inr : ∀ (hb : a < b), b ∈ c.intent (r := fun (x1 x2 : α) ↦ x1 < x2)
⊢ b ∈ c.intent (r := fun (x1 x2 : α) ↦ x1 < x2)

Tactic:
obtain rfl | hb := hb.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_6
inst : PartialOrder α
c : Concept α α fun (x1 x2 : α) ↦ x1 < x2
a : α
ha : a ∈ c.intent (r := fun (x1 x2 : α) ↦ x1 < x2)
hb : a ≤ a
⊢ a ∈ c.intent (r := fun (x1 x2 : α) ↦ x1 < x2)

Tactic:
assumption
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_6
inst : PartialOrder α
c : Concept α α fun (x1 x2 : α) ↦ x1 < x2
a b : α
hb_1 : a ≤ b
ha : a ∈ c.intent (r := fun (x1 x2 : α) ↦ x1 < x2)
hb : a < b
⊢ b ∈ c.intent (r := fun (x1 x2 : α) ↦ x1 < x2)

Tactic:
mem_intent_of_intent_rel hb ha

Premises used: Concept.mem_intent_of_intent_rel
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_6
inst : PartialOrder α
c : Concept α α fun (x1 x2 : α) ↦ x1 < x2
a b : α
hb_1 : a ≤ b
ha : a ∈ c.intent (r := fun (x1 x2 : α) ↦ x1 < x2)
hb : a < b
⊢ b ∈ c.intent (r := fun (x1 x2 : α) ↦ x1 < x2)

Tactic:
exact mem_intent_of_intent_rel hb ha

Premises used: Concept.mem_intent_of_intent_rel
-- Module: Mathlib.Order.Concept
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s : Set α
t : Set β
a : α
b : β
r' : α → α → Prop
c d : Concept α β r
c' : Concept α α r'
⊢ ∀ {x y : Concept α β r},
    LE.le (α := (Set β)ᵒᵈ) (((⇑toDual : (a : Set β) → (Set β)ᵒᵈ) ∘ intent (r := r)) x)
        (((⇑toDual : (a : Set β) → (Set β)ᵒᵈ) ∘ intent (r := r)) y) ↔
      x ≤ y

Tactic:
simp
-- Module: Mathlib.Order.Concept
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s : Set α
t : Set β
a : α
b : β
r' : α → α → Prop
c d : Concept α β r
c' : Concept α α r'
⊢ ∀ {x y : Concept α β r},
    LT.lt (α := (Set β)ᵒᵈ) (((⇑toDual : (a : Set β) → (Set β)ᵒᵈ) ∘ intent (r := r)) x)
        (((⇑toDual : (a : Set β) → (Set β)ᵒᵈ) ∘ intent (r := r)) y) ↔
      x < y

Tactic:
simp
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Set α
c : Concept α β r
⊢ (ofObjects r s).extent (r := r) ⊆ c.extent (r := r) ↔ s ⊆ c.extent (r := r)

Tactic:
⟨((subset_lowerPolar_upperPolar r s).trans ·),
    (isExtent_extent c).lowerPolar_upperPolar_subset⟩

Premises used: subset_lowerPolar_upperPolar, Order.IsExtent.lowerPolar_upperPolar_subset, HasSubset.Subset.trans, Iff.intro, Concept.isExtent_extent
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Set α
c : Concept α β r
⊢ (ofObjects r s).extent (r := r) ⊆ c.extent (r := r) ↔ s ⊆ c.extent (r := r)

Tactic:
exact ⟨((subset_lowerPolar_upperPolar r s).trans ·),
    (isExtent_extent c).lowerPolar_upperPolar_subset⟩
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Set α
c : Concept α β r
h : c.extent (r := r) ⊆ s
⊢ c ≤ ofObjects r s

Tactic:
simpa using (lowerPolar_anti r).comp (upperPolar_anti r) h

Premises used: lowerPolar_anti, Antitone.comp, upperPolar_anti
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
t : Set β
c : Concept α β r
rw : (ofAttributes r t).intent (r := r) ⊆ c.intent (r := r) ↔ t ⊆ c.intent (r := r)
⊢ c ≤ ofAttributes r t ↔ t ⊆ c.intent (r := r)

Tactic:
rw [← intent_subset_intent_iff]

Premises used: Concept.intent_subset_intent_iff
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
t : Set β
c : Concept α β r
⊢ (ofAttributes r t).intent (r := r) ⊆ c.intent (r := r) ↔ t ⊆ c.intent (r := r)

Tactic:
⟨((subset_upperPolar_lowerPolar r t).trans ·),
    (isIntent_intent c).upperPolar_lowerPolar_subset⟩

Premises used: subset_upperPolar_lowerPolar, Concept.isIntent_intent, HasSubset.Subset.trans, Iff.intro, Order.IsIntent.upperPolar_lowerPolar_subset
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
t : Set β
c : Concept α β r
⊢ (ofAttributes r t).intent (r := r) ⊆ c.intent (r := r) ↔ t ⊆ c.intent (r := r)

Tactic:
exact ⟨((subset_upperPolar_lowerPolar r t).trans ·),
    (isIntent_intent c).upperPolar_lowerPolar_subset⟩
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
t : Set β
c : Concept α β r
h : c.intent (r := r) ⊆ t
rw : c.intent (r := r) ⊆ (ofAttributes r t).intent (r := r)
⊢ ofAttributes r t ≤ c

Tactic:
rw [← intent_subset_intent_iff]

Premises used: Concept.intent_subset_intent_iff
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
t : Set β
c : Concept α β r
h : c.intent (r := r) ⊆ t
⊢ c.intent (r := r) ⊆ (ofAttributes r t).intent (r := r)

Tactic:
simpa using (upperPolar_anti r).comp (lowerPolar_anti r) h

Premises used: lowerPolar_anti, Antitone.comp, upperPolar_anti
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
a : α
b : β
⊢ ofObject r a ≤ ofAttribute r b ↔ r a b

Tactic:
simp
-- Module: Mathlib.Order.Concept
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s_1 : Set α
t : Set β
a : α
b : β
r' : α → α → Prop
c d : Concept α β r
c' : Concept α α r'
s : Set (Concept α β r)
⊢ IsLUB s (sSup s)

Tactic:
⟨fun _ hc ↦ ?_, fun _ hc ↦ ?_⟩

Premises used: IsLeast, And.intro, IsLUB
-- Module: Mathlib.Order.Concept
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s_1 : Set α
t : Set β
a : α
b : β
r' : α → α → Prop
c d : Concept α β r
c' : Concept α α r'
s : Set (Concept α β r)
refine_1 : ∀ (x : Concept α β r) (hc : x ∈ s), x ≤ sSup s
refine_2 : ∀ (x : Concept α β r) (hc : x ∈ upperBounds s), sSup s ≤ x
⊢ IsLUB s (sSup s)

Tactic:
refine ⟨fun _ hc ↦ ?_, fun _ hc ↦ ?_⟩
-- Module: Mathlib.Order.Concept
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s_1 : Set α
t : Set β
a : α
b : β
r' : α → α → Prop
c d : Concept α β r
c' : Concept α α r'
s : Set (Concept α β r)
x : Concept α β r
hc : x ∈ s
⊢ x ≤ sSup s

Tactic:
intent_subset_intent_iff.1 <| biInter_subset_of_mem hc

Premises used: Concept.intent_subset_intent_iff, Set.biInter_subset_of_mem, Iff.mp
-- Module: Mathlib.Order.Concept
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s_1 : Set α
t : Set β
a : α
b : β
r' : α → α → Prop
c d : Concept α β r
c' : Concept α α r'
s : Set (Concept α β r)
x : Concept α β r
hc : x ∈ s
⊢ x ≤ sSup s

Tactic:
exact intent_subset_intent_iff.1 <| biInter_subset_of_mem hc

Premises used: Concept.intent_subset_intent_iff, Set.biInter_subset_of_mem, Iff.mp
-- Module: Mathlib.Order.Concept
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s_1 : Set α
t : Set β
a : α
b : β
r' : α → α → Prop
c d : Concept α β r
c' : Concept α α r'
s : Set (Concept α β r)
x : Concept α β r
hc : x ∈ upperBounds s
⊢ sSup s ≤ x

Tactic:
intent_subset_intent_iff.1 <|
        subset_iInter₂ fun a ha ↦ intent_subset_intent_iff.2 (hc ha)

Premises used: Iff.mpr, Concept.intent_subset_intent_iff, Set.subset_iInter₂, Iff.mp
-- Module: Mathlib.Order.Concept
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s_1 : Set α
t : Set β
a : α
b : β
r' : α → α → Prop
c d : Concept α β r
c' : Concept α α r'
s : Set (Concept α β r)
x : Concept α β r
hc : x ∈ upperBounds s
⊢ sSup s ≤ x

Tactic:
exact intent_subset_intent_iff.1 <|
        subset_iInter₂ fun a ha ↦ intent_subset_intent_iff.2 (hc ha)

Premises used: Iff.mpr, Concept.intent_subset_intent_iff, Set.subset_iInter₂, Iff.mp
-- Module: Mathlib.Order.Concept
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
f : ι → Concept α β r
simp_rw : extent (r := r) (sSup (range fun (i : ι) ↦ f i)) = lowerPolar r (⋂ (i : ι), (f i).intent (r := r))
simp_rw₁ :
  lowerPolar r
      (⋂ (i : Concept α β r),
        ⋂ (_ : Membership.mem (γ := Set (Concept α β r)) (range fun (i : ι) ↦ f i) i), i.intent (r := r)) =
    lowerPolar r (⋂ (i : ι), (f i).intent (r := r))
simp_rw₂ :
  lowerPolar r
      (⨅ (i : Concept α β r),
        ⨅ (_ : Membership.mem (γ := Set (Concept α β r)) (range fun (i : ι) ↦ f i) i), i.intent (r := r)) =
    lowerPolar r (⨅ (i : ι), (f i).intent (r := r))
⊢ extent (r := r) (⨆ (i : ι), f i) = lowerPolar r (⋂ (i : ι), (f i).intent (r := r))

Tactic:
simp_rw [iSup, extent_sSup, ← Set.iInf_eq_iInter, iInf_range]

Premises used: Concept.extent_sSup, Set.iInf_eq_iInter, iSup, iInf_range
-- Module: Mathlib.Order.Concept
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
f : ι → Concept α β r
simp_rw :
  Eq.{u_3 + 1} (α := Set β) (intent (r := r) (sSup (range fun (i : ι) ↦ f i))) (⋂ (i : ι), (f i).intent (r := r))
simp_rw₁ :
  Eq.{u_3 + 1} (α := Set β)
    (⋂ (i : Concept α β r),
      ⋂ (_ : Membership.mem (γ := Set (Concept α β r)) (range fun (i : ι) ↦ f i) i), i.intent (r := r))
    (⋂ (i : ι), (f i).intent (r := r))
simp_rw₂ :
  Eq.{u_3 + 1} (α := Set β)
    (⨅ (i : Concept α β r),
      ⨅ (_ : Membership.mem (γ := Set (Concept α β r)) (range fun (i : ι) ↦ f i) i), i.intent (r := r))
    (⨅ (i : ι), (f i).intent (r := r))
⊢ Eq.{u_3 + 1} (α := Set β) (intent (r := r) (⨆ (i : ι), f i)) (⋂ (i : ι), (f i).intent (r := r))

Tactic:
simp_rw [iSup, intent_sSup, ← Set.iInf_eq_iInter, iInf_range]

Premises used: Set.iInf_eq_iInter, iSup, Concept.intent_sSup, iInf_range
-- Module: Mathlib.Order.Concept
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
f : ι → Concept α β r
simp_rw :
  Eq.{u_2 + 1} (α := Set α) (extent (r := r) (sInf (range fun (i : ι) ↦ f i))) (⋂ (i : ι), (f i).extent (r := r))
simp_rw₁ :
  Eq.{u_2 + 1} (α := Set α)
    (⋂ (i : Concept α β r),
      ⋂ (_ : Membership.mem (γ := Set (Concept α β r)) (range fun (i : ι) ↦ f i) i), i.extent (r := r))
    (⋂ (i : ι), (f i).extent (r := r))
simp_rw₂ :
  Eq.{u_2 + 1} (α := Set α)
    (⨅ (i : Concept α β r),
      ⨅ (_ : Membership.mem (γ := Set (Concept α β r)) (range fun (i : ι) ↦ f i) i), i.extent (r := r))
    (⨅ (i : ι), (f i).extent (r := r))
⊢ Eq.{u_2 + 1} (α := Set α) (extent (r := r) (⨅ (i : ι), f i)) (⋂ (i : ι), (f i).extent (r := r))

Tactic:
simp_rw [iInf, extent_sInf, ← Set.iInf_eq_iInter, iInf_range]

Premises used: iInf, Set.iInf_eq_iInter, iInf_range, Concept.extent_sInf
-- Module: Mathlib.Order.Concept
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
f : ι → Concept α β r
simp_rw : intent (r := r) (sInf (range fun (i : ι) ↦ f i)) = upperPolar r (⋂ (i : ι), (f i).extent (r := r))
simp_rw₁ :
  upperPolar r
      (⋂ (i : Concept α β r),
        ⋂ (_ : Membership.mem (γ := Set (Concept α β r)) (range fun (i : ι) ↦ f i) i), i.extent (r := r)) =
    upperPolar r (⋂ (i : ι), (f i).extent (r := r))
simp_rw₂ :
  upperPolar r
      (⨅ (i : Concept α β r),
        ⨅ (_ : Membership.mem (γ := Set (Concept α β r)) (range fun (i : ι) ↦ f i) i), i.extent (r := r)) =
    upperPolar r (⨅ (i : ι), (f i).extent (r := r))
⊢ intent (r := r) (⨅ (i : ι), f i) = upperPolar r (⋂ (i : ι), (f i).extent (r := r))

Tactic:
simp_rw [iInf, intent_sInf, ← Set.iInf_eq_iInter, iInf_range]

Premises used: iInf, Set.iInf_eq_iInter, iInf_range, Concept.intent_sInf
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
c : Concept α β r
⊢ c.swap (r := r).swap (r := Function.swap (φ := fun (a : α) (a_1 : β) ↦ Prop) r) = c

Tactic:
ext rfl

Premises used: Concept.ext, rfl
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
⊢ c.swap (r := r) ≤ d.swap (r := r) ↔ d ≤ c

Tactic:
intent_subset_intent_iff

Premises used: Concept.intent_subset_intent_iff
-- Module: Mathlib.Order.Concept
Goal:
α : Type u_2
β : Type u_3
r : α → β → Prop
c d : Concept α β r
⊢ c.swap (r := r) < d.swap (r := r) ↔ d < c

Tactic:
intent_ssubset_intent_iff

Premises used: Concept.intent_ssubset_intent_iff
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SupSet α
s : Set (WithTop α)
hs : ⊤ ∉ s
hs' : BddAbove (some ⁻¹' s)
⊢ sSup s = (↑(sSup (some ⁻¹' s)) : WithTop α)

Tactic:
(if_neg hs).trans <| if_pos hs'

Premises used: if_pos, if_neg, Eq.trans
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : InfSet α
s : Set (WithTop α)
hs : ¬s ⊆ {⊤}
h's : BddBelow s
⊢ ¬(s ⊆ {⊤} ∨ ¬BddBelow s)

Tactic:
simp [hs, h's]
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : InfSet α
s : Set (WithBot α)
hs : ⊥ ∉ s
hs' : BddBelow (some ⁻¹' s)
⊢ sInf s = (↑(sInf (some ⁻¹' s)) : WithBot α)

Tactic:
(if_neg hs).trans <| if_pos hs'

Premises used: Set.Mem, if_pos, OrderDual, if_neg, Eq.trans, WithTop
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SupSet α
s : Set (WithBot α)
hs : ¬s ⊆ {⊥}
h's : BddAbove s
⊢ sSup s = (↑(sSup (some ⁻¹' s)) : WithBot α)

Tactic:
WithTop.sInf_eq (α := αᵒᵈ) hs h's

Premises used: WithBot.some, WithBot, WithTop.sInf_eq, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : InfSet α
⊢ Subset (α := Set (WithTop α)) ∅ {⊤} ∨ ¬BddBelow.{u_1} (α := WithTop α) ∅

Tactic:
simp
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : InfSet α
s : Set α
hs : s.Nonempty
h's : BddBelow s
obtain : ∀ (x : α) (hx : x ∈ s), (↑(sInf s) : WithTop α) = sInf ((fun (a : α) ↦ (↑a : WithTop α)) '' s)
⊢ (↑(sInf s) : WithTop α) = sInf ((fun (a : α) ↦ (↑a : WithTop α)) '' s)

Tactic:
obtain ⟨x, hx⟩ := hs
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
pos :
  ∀
    (h :
      Subset (α := Set (WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) {⊤} ∨
        ¬BddBelow (α := WithTop α) ((fun (a : α) ↦ (↑a : WithTop α)) '' s)),
    (↑(sInf s) : WithTop α) = ⊤
neg :
  ∀
    (h :
      ¬(Subset (α := Set (WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) {⊤} ∨
          ¬BddBelow (α := WithTop α) ((fun (a : α) ↦ (↑a : WithTop α)) '' s))),
    (↑(sInf s) : WithTop α) =
      (↑(sInf (preimage (β := WithTop α) (fun (a : α) ↦ (↑a : WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s))) :
        WithTop α)
⊢ (↑(sInf s) : WithTop α) =
    if
        Subset (α := Set (WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) {⊤} ∨
          ¬BddBelow (α := WithTop α) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) then
      ⊤
    else
      (↑(sInf (preimage (β := WithTop α) (fun (a : α) ↦ (↑a : WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s))) :
        WithTop α)

Tactic:
split_ifs with h
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
h :
  Subset (α := Set (WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) {⊤} ∨
    ¬BddBelow (α := WithTop α) ((fun (a : α) ↦ (↑a : WithTop α)) '' s)
pos : ∀ (h1 : Subset (α := Set (WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) {⊤}), (↑(sInf s) : WithTop α) = ⊤
pos₁ : ∀ (h2 : ¬BddBelow (α := WithTop α) ((fun (a : α) ↦ (↑a : WithTop α)) '' s)), (↑(sInf s) : WithTop α) = ⊤
⊢ (↑(sInf s) : WithTop α) = ⊤

Tactic:
rcases h with h1 | h2
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
h1 : Subset (α := Set (WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) {⊤}
⊢ (↑(sInf s) : WithTop α) = ⊤

Tactic:
cases h1 (mem_image_of_mem _ hx)

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
h2 : ¬BddBelow (α := WithTop α) ((fun (a : α) ↦ (↑a : WithTop α)) '' s)
⊢ (↑(sInf s) : WithTop α) = ⊤

Tactic:
(h2 (Monotone.map_bddBelow coe_mono h's)).elim

Premises used: WithTop.coe_mono, False.elim, Monotone.map_bddBelow
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
h2 : ¬BddBelow (α := WithTop α) ((fun (a : α) ↦ (↑a : WithTop α)) '' s)
⊢ (↑(sInf s) : WithTop α) = ⊤

Tactic:
exact (h2 (Monotone.map_bddBelow coe_mono h's)).elim

Premises used: WithTop.coe_mono, False.elim, Monotone.map_bddBelow
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
h :
  ¬(Subset (α := Set (WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) {⊤} ∨
      ¬BddBelow (α := WithTop α) ((fun (a : α) ↦ (↑a : WithTop α)) '' s))
neg : Injective (β := WithTop α) fun (a : α) ↦ (↑a : WithTop α)
⊢ (↑(sInf s) : WithTop α) =
    (↑(sInf (preimage (β := WithTop α) (fun (a : α) ↦ (↑a : WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s))) :
      WithTop α)

Tactic:
rw [preimage_image_eq]

Premises used: Set.preimage_image_eq
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
h :
  ¬(Subset (α := Set (WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) {⊤} ∨
      ¬BddBelow (α := WithTop α) ((fun (a : α) ↦ (↑a : WithTop α)) '' s))
⊢ Injective (β := WithTop α) fun (a : α) ↦ (↑a : WithTop α)

Tactic:
Option.some_injective _

Premises used: WithTop.some, Option.some_injective, WithTop
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : InfSet α
s : Set α
h's : BddBelow s
x : α
hx : x ∈ s
h :
  ¬(Subset (α := Set (WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) {⊤} ∨
      ¬BddBelow (α := WithTop α) ((fun (a : α) ↦ (↑a : WithTop α)) '' s))
⊢ Injective (β := WithTop α) fun (a : α) ↦ (↑a : WithTop α)

Tactic:
exact Option.some_injective _

Premises used: Option.some_injective
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : InfSet α
s : Set α
hs : s.Nonempty
h's : BddBelow s
obtain : ∀ (x : α) (hx : x ∈ s), (↑(sInf s) : WithTop α) = sInf ((fun (a : α) ↦ (↑a : WithTop α)) '' s)
obtain₁ :
  ∀ (x : α) (hx : x ∈ s),
    (↑(sInf s) : WithTop α) =
      if
          Subset (α := Set (WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) {⊤} ∨
            ¬BddBelow (α := WithTop α) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) then
        ⊤
      else
        (↑(sInf (preimage (β := WithTop α) (fun (a : α) ↦ (↑a : WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s))) :
          WithTop α)
pos :
  ∀ (x : α) (hx : x ∈ s)
    (h :
      Subset (α := Set (WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) {⊤} ∨
        ¬BddBelow (α := WithTop α) ((fun (a : α) ↦ (↑a : WithTop α)) '' s)),
    (↑(sInf s) : WithTop α) = ⊤
neg neg₁ :
  ∀ (x : α) (hx : x ∈ s)
    (h :
      ¬(Subset (α := Set (WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) {⊤} ∨
          ¬BddBelow (α := WithTop α) ((fun (a : α) ↦ (↑a : WithTop α)) '' s))),
    (↑(sInf s) : WithTop α) =
      (↑(sInf (preimage (β := WithTop α) (fun (a : α) ↦ (↑a : WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s))) :
        WithTop α)
⊢ (↑(sInf s) : WithTop α) = sInf ((fun (a : α) ↦ (↑a : WithTop α)) '' s)

Tactic:
classical
  obtain ⟨x, hx⟩ := hs
  change _ = ite _ _ _
  split_ifs with h
  · rcases h with h1 | h2
    · cases h1 (mem_image_of_mem _ hx)
    · exact (h2 (Monotone.map_bddBelow coe_mono h's)).elim
  · rw [preimage_image_eq]
    exact Option.some_injective _

Premises used: Set.preimage_image_eq, Option.some_injective, ite
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SupSet α
s : Set α
hs : BddAbove s
h : Injective (β := WithTop α) fun (a : α) ↦ (↑a : WithTop α)
hnc : ⊤ ∉ (fun (a : α) ↦ (↑a : WithTop α)) '' s
⊢ (↑(sSup s) : WithTop α) =
    if Membership.mem (γ := Set (WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) ⊤ then ⊤
    else
      if
          BddAbove (α := α)
            (preimage (β := WithTop α) (fun (a : α) ↦ (↑a : WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s)) then
        (↑(sSup (preimage (β := WithTop α) (fun (a : α) ↦ (↑a : WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s))) :
          WithTop α)
      else ⊤

Tactic:
rw [if_neg, preimage_image_eq, if_pos hs]

Premises used: if_pos, Set.preimage_image_eq, if_neg
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SupSet α
s : Set α
hs : BddAbove s
⊢ Injective (β := WithTop α) fun (a : α) ↦ (↑a : WithTop α)

Tactic:
Option.some_injective _

Premises used: WithTop.some, Option.some_injective, WithTop
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SupSet α
s : Set α
hs : BddAbove s
⊢ Injective (β := WithTop α) fun (a : α) ↦ (↑a : WithTop α)

Tactic:
exact Option.some_injective _

Premises used: Option.some_injective
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SupSet α
s : Set α
hs : BddAbove s
change :
  (↑(sSup s) : WithTop α) =
    if Membership.mem (γ := Set (WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s) ⊤ then ⊤
    else
      if
          BddAbove (α := α)
            (preimage (β := WithTop α) (fun (a : α) ↦ (↑a : WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s)) then
        (↑(sSup (preimage (β := WithTop α) (fun (a : α) ↦ (↑a : WithTop α)) ((fun (a : α) ↦ (↑a : WithTop α)) '' s))) :
          WithTop α)
      else ⊤
h : Injective (β := WithTop α) fun (a : α) ↦ (↑a : WithTop α)
hnc hnc₁ : ⊤ ∉ (fun (a : α) ↦ (↑a : WithTop α)) '' s
⊢ (↑(sSup s) : WithTop α) = sSup ((fun (a : α) ↦ (↑a : WithTop α)) '' s)

Tactic:
classical
  change _ = ite _ _ _
  rw [if_neg, preimage_image_eq, if_pos hs]
  · exact Option.some_injective _
  · rintro ⟨x, _, ⟨⟩⟩

Premises used: if_pos, Set.preimage_image_eq, Option.some_injective, if_neg, ite
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SupSet α
⊢ Eq.{u_1 + 1} (α := WithBot α) (sSup ∅) ⊥

Tactic:
WithTop.sInf_empty (α := αᵒᵈ)

Premises used: WithBot, WithTop.sInf_empty, OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_5
inst : CompleteLattice α
⊢ ⊥ ∉ ∅

Tactic:
simp
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_5
inst : CompleteLattice α
rw : Eq.{u_5 + 1} (α := WithBot α) (↑(sInf (some ⁻¹' ∅)) : WithBot α) ⊤
rw₁ : Eq.{u_5 + 1} (α := WithBot α) (↑(sInf ∅) : WithBot α) ⊤
rw₂ : Eq.{u_5 + 1} (α := WithBot α) (↑⊤ : WithBot α) ⊤
rw₃ rw₄ : Eq.{u_5 + 1} (α := WithBot α) ⊤ ⊤
⊢ Eq.{u_5 + 1} (α := WithBot α) (sInf ∅) ⊤

Tactic:
rw [WithBot.sInf_eq (by simp) (OrderBot.bddBelow _), Set.preimage_empty, _root_.sInf_empty,
    WithBot.coe_top]

Premises used: WithBot.sInf_eq, Set.preimage_empty, WithBot.coe_top, sInf_empty, OrderBot.bddBelow
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : SupSet α
s : Set α
hs : s.Nonempty
h's : BddAbove s
⊢ (↑(sSup s) : WithBot α) = sSup ((fun (a : α) ↦ (↑a : WithBot α)) '' s)

Tactic:
WithTop.coe_sInf' (α := αᵒᵈ) hs h's

Premises used: WithBot.some, WithBot, WithTop.coe_sInf', OrderDual
-- Module: Mathlib.Order.ConditionallyCompleteLattice.Basic
Goal:
α : Type u_1
inst : Preorder α
inst_1 : InfSet α
s : Set α
hs : BddBelow s
⊢ (↑(sInf s) : WithBot α) = sInf ((fun (a : α) ↦ (↑a : WithBot α)) '' s)

Tactic:
WithTop.coe_sSup' (α := αᵒᵈ) hs

Premises used: WithBot.some, WithBot, Set.Mem, WithTop.coe_sSup', OrderDual