awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : Fact (a ≤ b)
S : Set (↑(Icc a b) : Type u_2)
hS : ¬S = ∅
⊢ IsLUB S (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) (sSup (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S)) ⋯)

Tactic:
.of_image Subtype.coe_le_coe <| isLUB_csSup ((Set.nonempty_iff_ne_empty.mpr hS).image _)
        ((Subtype.mono_coe _).map_bddAbove (OrderTop.bddAbove S))

Premises used: Iff.mpr, Set.Mem, OrderTop.bddAbove, Subtype.mono_coe, Monotone.map_bddAbove, IsLUB.of_image, Set.Nonempty.image, Set.nonempty_iff_ne_empty, isLUB_csSup
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : Fact (a ≤ b)
S : Set (↑(Icc a b) : Type u_2)
hS : ¬S = ∅
⊢ IsLUB S (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) (sSup (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S)) ⋯)

Tactic:
exact .of_image Subtype.coe_le_coe <| isLUB_csSup ((Set.nonempty_iff_ne_empty.mpr hS).image _)
        ((Subtype.mono_coe _).map_bddAbove (OrderTop.bddAbove S))

Premises used: Iff.mpr, OrderTop.bddAbove, Subtype.mono_coe, Monotone.map_bddAbove, Set.Nonempty.image, Set.nonempty_iff_ne_empty, isLUB_csSup
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : Fact (a ≤ b)
S : Set (↑(Icc a b) : Type u_2)
hS : S.Nonempty
⊢ sInf (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S) ∈ Icc a b

Tactic:
⟨le_csInf (hS.image Subtype.val) (fun _ ⟨c, _, hc⟩ ↦ hc ▸ c.2.1), ?_⟩

Premises used: Set.Mem, le_csInf, setOf, _private.0.Set.Icc.completeLattice.match_1, Eq.rec, LE.le, Set.Icc, And.left, Set.Nonempty.image, And.intro, Subtype.val, Subtype.property
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : Fact (a ≤ b)
S : Set (↑(Icc a b) : Type u_2)
hS : S.Nonempty
refine : sInf (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S) ≤ b
⊢ sInf (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S) ∈ Icc a b

Tactic:
refine ⟨le_csInf (hS.image Subtype.val) (fun _ ⟨c, _, hc⟩ ↦ hc ▸ c.2.1), ?_⟩
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : Fact (a ≤ b)
S : Set (↑(Icc a b) : Type u_2)
hS : S.Nonempty
obtain : ∀ (c : (↑(Icc a b) : Type u_2)) (hc : c ∈ S), sInf (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S) ≤ b
⊢ sInf (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S) ≤ b

Tactic:
obtain ⟨c, hc⟩ := hS
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : Fact (a ≤ b)
S : Set (↑(Icc a b) : Type u_2)
c : (↑(Icc a b) : Type u_2)
hc : c ∈ S
⊢ sInf (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S) ≤ b

Tactic:
le_trans (csInf_le ⟨a, fun _ ⟨d, _, hd⟩ ↦ hd ▸ d.2.1⟩ ⟨c, hc, rfl⟩) c.2.2

Premises used: _private.0.Set.Icc.completeLattice.match_1, Eq.rec, LE.le, And.right, And.left, And.intro, Exists.intro, csInf_le, rfl, Subtype.property, le_trans
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : Fact (a ≤ b)
S : Set (↑(Icc a b) : Type u_2)
c : (↑(Icc a b) : Type u_2)
hc : c ∈ S
⊢ sInf (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S) ≤ b

Tactic:
exact le_trans (csInf_le ⟨a, fun _ ⟨d, _, hd⟩ ↦ hd ▸ d.2.1⟩ ⟨c, hc, rfl⟩) c.2.2
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : Fact (a ≤ b)
S : Set (↑(Icc a b) : Type u_2)
pos : ∀ (hS : S = ∅), IsGLB S (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) b ⋯)
neg :
  ∀ (hS : ¬S = ∅),
    IsGLB S (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) (sInf (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S)) ⋯)
⊢ IsGLB S
    (if hS : S = ∅ then Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) b ⋯
    else Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) (sInf (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S)) ⋯)

Tactic:
split_ifs with hS
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : Fact (a ≤ b)
S : Set (↑(Icc a b) : Type u_2)
hS : S = ∅
pos : IsGLB (α := (↑(Icc a b) : Type u_2)) ∅ (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) b ⋯)
⊢ IsGLB S (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) b ⋯)

Tactic:
subst hS
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : Fact (a ≤ b)
pos : Eq (α := (↑(Icc a b) : Type u_2)) (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) b ⋯) ⊤
⊢ IsGLB (α := (↑(Icc a b) : Type u_2)) ∅ (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) b ⋯)

Tactic:
simp only [isGLB_empty_iff, isTop_iff_eq_top]

Premises used: isGLB_empty_iff, isTop_iff_eq_top
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : Fact (a ≤ b)
⊢ Eq (α := (↑(Icc a b) : Type u_2)) (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) b ⋯) ⊤

Tactic:
rfl
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : Fact (a ≤ b)
S : Set (↑(Icc a b) : Type u_2)
hS : ¬S = ∅
⊢ IsGLB S (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) (sInf (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S)) ⋯)

Tactic:
.of_image Subtype.coe_le_coe <| isGLB_csInf ((Set.nonempty_iff_ne_empty.mpr hS).image _)
        ((Subtype.mono_coe _).map_bddBelow (OrderBot.bddBelow S))

Premises used: Iff.mpr, IsGLB.of_image, Set.Mem, Subtype.mono_coe, isGLB_csInf, Set.Nonempty.image, Set.nonempty_iff_ne_empty, Monotone.map_bddBelow, OrderBot.bddBelow
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : ConditionallyCompleteLattice α
a b : α
inst_1 : Fact (a ≤ b)
S : Set (↑(Icc a b) : Type u_2)
hS : ¬S = ∅
⊢ IsGLB S (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) (sInf (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S)) ⋯)

Tactic:
exact .of_image Subtype.coe_le_coe <| isGLB_csInf ((Set.nonempty_iff_ne_empty.mpr hS).image _)
        ((Subtype.mono_coe _).map_bddBelow (OrderBot.bddBelow S))

Premises used: Iff.mpr, Subtype.mono_coe, isGLB_csInf, Set.Nonempty.image, Set.nonempty_iff_ne_empty, Monotone.map_bddBelow, OrderBot.bddBelow
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
α : Type u_2
inst : ConditionallyCompleteLattice α
a b : α
h : a ≤ b
S : Set (↑(Icc a b) : Type u_2)
hS : S.Nonempty
⊢ have this := ⋯;
  (↑(sSup S) : α) = sSup (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S)

Tactic:
congrArg Subtype.val (dif_neg hS.ne_empty)

Premises used: congrArg, Set.Nonempty.ne_empty, dif_neg, Subtype.val
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
α : Type u_2
inst : ConditionallyCompleteLattice α
a b : α
h : a ≤ b
S : Set (↑(Icc a b) : Type u_2)
hS : S.Nonempty
⊢ have this := ⋯;
  (↑(sInf S) : α) = sInf (Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b) '' S)

Tactic:
congrArg Subtype.val (dif_neg hS.ne_empty)

Premises used: congrArg, Set.Nonempty.ne_empty, dif_neg, Subtype.val
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
inst : ConditionallyCompleteLattice α
a b : α
h : a ≤ b
inst_1 : Nonempty ι
S : ι → (↑(Icc a b) : Type u_2)
⊢ have this := ⋯;
  (↑(iSup S) : α) = ⨆ (i : ι), (↑(S i) : α)

Tactic:
(Set.Icc.coe_sSup h (range_nonempty S)).trans (congrArg sSup (range_comp Subtype.val S).symm)

Premises used: Set.range_comp, Set.Icc.coe_sSup, congrArg, Set.range_nonempty, Eq.symm, Subtype.val, SupSet.sSup, Eq.trans
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
inst : ConditionallyCompleteLattice α
a b : α
h : a ≤ b
inst_1 : Nonempty ι
S : ι → (↑(Icc a b) : Type u_2)
⊢ have this := ⋯;
  (↑(iInf S) : α) = ⨅ (i : ι), (↑(S i) : α)

Tactic:
(Set.Icc.coe_sInf h (range_nonempty S)).trans (congrArg sInf (range_comp Subtype.val S).symm)

Premises used: Set.range_comp, congrArg, Set.Icc.coe_sInf, Set.range_nonempty, Eq.symm, Subtype.val, InfSet.sInf, Eq.trans
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : CompleteLattice α
a : α
S : Set (↑(Iic a) : Type u_2)
⊢ sSup (Subtype.val (p := fun (x : α) ↦ x ∈ Iic a) '' S) ∈ Iic a

Tactic:
simpa using fun b hb _ ↦ hb
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : CompleteLattice α
a : α
S : Set (↑(Iic a) : Type u_2)
⊢ a ⊓ sInf (Subtype.val (p := fun (x : α) ↦ x ∈ Iic a) '' S) ∈ Iic a

Tactic:
simp
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : CompleteLattice α
a : α
⊢ ∀ (a_1 : (↑(Iic a) : Type u_2)), a_1 ≤ ⊤

Tactic:
simp
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
s : Set α
inst : CompleteLattice α
a : α
⊢ ∀ (a_1 : (↑(Iic a) : Type u_2)), ⊥ ≤ a_1

Tactic:
simp
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
α : Type u_2
inst : CompleteLattice α
a : α
S : Set (↑(Iic a) : Type u_2)
⊢ (↑(sSup S) : α) = sSup (Subtype.val (p := fun (x : α) ↦ x ∈ Iic a) '' S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
a : α
f : ι → (↑(Iic a) : Type u_2)
rw :
  Eq.{u_2 + 1} (α := α)
    (sSup (image (α := (↑(Iic a) : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ Iic a)) (range fun (i : ι) ↦ f i)))
    (⨆ (i : ι), (↑(f i) : α))
⊢ Eq.{u_2 + 1} (α := α) (↑(⨆ (i : ι), f i) : α) (⨆ (i : ι), (↑(f i) : α))

Tactic:
rw [iSup, coe_sSup]

Premises used: iSup, Set.Iic.coe_sSup
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
a : α
f : ι → (↑(Iic a) : Type u_2)
e_a :
  Eq.{u_2 + 1} (α := Set α)
    (image (α := (↑(Iic a) : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ Iic a)) (range fun (i : ι) ↦ f i))
    (range fun (i : ι) ↦ (↑(f i) : α))
⊢ Eq.{u_2 + 1} (α := α)
    (sSup (image (α := (↑(Iic a) : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ Iic a)) (range fun (i : ι) ↦ f i)))
    (⨆ (i : ι), (↑(f i) : α))

Tactic:
congr
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
a : α
f : ι → (↑(Iic a) : Type u_2)
e_a :
  ∀ (x : α),
    Membership.mem (γ := Set α)
        (image (α := (↑(Iic a) : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ Iic a)) (range fun (i : ι) ↦ f i)) x ↔
      Membership.mem (γ := Set α) (range fun (i : ι) ↦ (↑(f i) : α)) x
⊢ Eq.{u_2 + 1} (α := Set α)
    (image (α := (↑(Iic a) : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ Iic a)) (range fun (i : ι) ↦ f i))
    (range fun (i : ι) ↦ (↑(f i) : α))

Tactic:
ext
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
a : α
f : ι → (↑(Iic a) : Type u_2)
x : α
⊢ Membership.mem (γ := Set α)
      (image (α := (↑(Iic a) : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ Iic a)) (range fun (i : ι) ↦ f i)) x ↔
    Membership.mem (γ := Set α) (range fun (i : ι) ↦ (↑(f i) : α)) x

Tactic:
simp
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
a : α
f : ι → (↑(Iic a) : Type u_2)
p : ι → Prop
⊢ Eq.{u_2 + 1} (α := α) (↑(⨆ (i : ι), ⨆ (_ : p i), f i) : α) (⨆ (i : ι), ⨆ (_ : p i), (↑(f i) : α))

Tactic:
simp
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
α : Type u_2
inst : CompleteLattice α
a : α
S : Set (↑(Iic a) : Type u_2)
⊢ (↑(sInf S) : α) = a ⊓ sInf (Subtype.val (p := fun (x : α) ↦ x ∈ Iic a) '' S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
a : α
f : ι → (↑(Iic a) : Type u_2)
rw :
  a ⊓ sInf (image (α := (↑(Iic a) : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ Iic a)) (range fun (i : ι) ↦ f i)) =
    a ⊓ ⨅ (i : ι), (↑(f i) : α)
⊢ (↑(⨅ (i : ι), f i) : α) = a ⊓ ⨅ (i : ι), (↑(f i) : α)

Tactic:
rw [iInf, coe_sInf]

Premises used: Set.Iic.coe_sInf, iInf
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
a : α
f : ι → (↑(Iic a) : Type u_2)
e_a :
  Eq.{u_2 + 1} (α := Set α)
    (image (α := (↑(Iic a) : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ Iic a)) (range fun (i : ι) ↦ f i))
    (range fun (i : ι) ↦ (↑(f i) : α))
⊢ a ⊓ sInf (image (α := (↑(Iic a) : Type u_2)) (Subtype.val (p := fun (x : α) ↦ x ∈ Iic a)) (range fun (i : ι) ↦ f i)) =
    a ⊓ ⨅ (i : ι), (↑(f i) : α)

Tactic:
congr
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
a : α
f : ι → (↑(Iic a) : Type u_2)
p : ι → Prop
inl : IsEmpty ι → (↑(⨅ (i : ι), ⨅ (_ : p i), f i) : α) = a ⊓ ⨅ (i : ι), ⨅ (_ : p i), (↑(f i) : α)
inr : Nonempty ι → (↑(⨅ (i : ι), ⨅ (_ : p i), f i) : α) = a ⊓ ⨅ (i : ι), ⨅ (_ : p i), (↑(f i) : α)
⊢ (↑(⨅ (i : ι), ⨅ (_ : p i), f i) : α) = a ⊓ ⨅ (i : ι), ⨅ (_ : p i), (↑(f i) : α)

Tactic:
cases isEmpty_or_nonempty ι

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
a : α
f : ι → (↑(Iic a) : Type u_2)
p : ι → Prop
h : IsEmpty ι
⊢ (↑(⨅ (i : ι), ⨅ (_ : p i), f i) : α) = a ⊓ ⨅ (i : ι), ⨅ (_ : p i), (↑(f i) : α)

Tactic:
simp
-- Module: Mathlib.Order.CompleteLatticeIntervals
Goal:
ι : Sort u_1
α : Type u_2
inst : CompleteLattice α
a : α
f : ι → (↑(Iic a) : Type u_2)
p : ι → Prop
h : Nonempty ι
inr : a ⊓ ⨅ (i : ι), a ⊓ ⨅ (_ : p i), (↑(f i) : α) = a ⊓ ⨅ (i : ι), ⨅ (_ : p i), (↑(f i) : α)
inr₁ : a ⊓ (a ⊓ ⨅ (x : ι), ⨅ (_ : p x), (↑(f x) : α)) = a ⊓ ⨅ (x : ι), ⨅ (_ : p x), (↑(f x) : α)
inr₂ : a ⊓ a ⊓ ⨅ (x : ι), ⨅ (_ : p x), (↑(f x) : α) = a ⊓ ⨅ (x : ι), ⨅ (_ : p x), (↑(f x) : α)
⊢ (↑(⨅ (i : ι), ⨅ (_ : p i), f i) : α) = a ⊓ ⨅ (i : ι), ⨅ (_ : p i), (↑(f i) : α)

Tactic:
simp_rw [coe_iInf, ← inf_iInf, ← inf_assoc, inf_idem]

Premises used: Set.Iic.coe_iInf, inf_iInf, inf_assoc, inf_idem
-- Module: Mathlib.Order.CompletePartialOrder
Goal:
α : Type u_2
inst : CompletePartialOrder α
d : Set α
⊢ DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → IsLUB d (sSup d)

Tactic:
CompletePartialOrder.lubOfDirected _

Premises used: CompletePartialOrder.lubOfDirected
-- Module: Mathlib.Order.CompletePartialOrder
Goal:
α : Type u_2
inst : CompletePartialOrder α
d : Set α
a : α
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
ha : a ∈ d
⊢ a ≤ sSup d

Tactic:
hd.isLUB_sSup.1 ha

Premises used: DirectedOn.isLUB_sSup, And.left
-- Module: Mathlib.Order.CompletePartialOrder
Goal:
α : Type u_2
inst : CompletePartialOrder α
d : Set α
a : α
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
ha : ∀ b ∈ d, b ≤ a
⊢ sSup d ≤ a

Tactic:
hd.isLUB_sSup.2 ha

Premises used: DirectedOn.isLUB_sSup, And.right
-- Module: Mathlib.Order.CompletePartialOrder
Goal:
ι : Sort u_1
α : Type u_2
inst : CompletePartialOrder α
f : ι → α
hf : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
i : ι
⊢ f i ≤ ⨆ (j : ι), f j

Tactic:
hf.directedOn_range.le_sSup <| Set.mem_range_self _

Premises used: Set.mem_range_self, iSup, Directed.directedOn_range, DirectedOn.le_sSup
-- Module: Mathlib.Order.CompletePartialOrder
Goal:
ι : Sort u_1
α : Type u_2
inst : CompletePartialOrder α
f : ι → α
a : α
hf : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
ha : ∀ (i : ι), f i ≤ a
⊢ ⨆ (i : ι), f i ≤ a

Tactic:
hf.directedOn_range.sSup_le <| Set.forall_mem_range.2 ha

Premises used: Iff.mpr, Set.forall_mem_range, iSup, Directed.directedOn_range, DirectedOn.sSup_le
-- Module: Mathlib.Order.CompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : CompletePartialOrder α
inst_1 : Preorder β
f : α → β
⊢ ScottContinuous f ↔ ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → IsLUB (f '' d) (f (sSup d))

Tactic:
⟨fun h d hd₁ hd₂ ↦ h hd₁ hd₂ hd₂.isLUB_sSup, fun h d hne hd a hda ↦ ?_⟩

Premises used: DirectedOn.isLUB_sSup, Iff.intro
-- Module: Mathlib.Order.CompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : CompletePartialOrder α
inst_1 : Preorder β
f : α → β
refine :
  ∀ (h : ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → IsLUB (f '' d) (f (sSup d))) (d : Set α)
    (hne : d.Nonempty) (hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d) (a : α) (hda : IsLUB d a), IsLUB (f '' d) (f a)
⊢ ScottContinuous f ↔ ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → IsLUB (f '' d) (f (sSup d))

Tactic:
refine ⟨fun h d hd₁ hd₂ ↦ h hd₁ hd₂ hd₂.isLUB_sSup, fun h d hne hd a hda ↦ ?_⟩
-- Module: Mathlib.Order.CompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : CompletePartialOrder α
inst_1 : Preorder β
f : α → β
h : ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → IsLUB (f '' d) (f (sSup d))
d : Set α
hne : d.Nonempty
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
rw : IsLUB (f '' d) (f (sSup d))
⊢ IsLUB (f '' d) (f a)

Tactic:
rw [hda.unique hd.isLUB_sSup]

Premises used: DirectedOn.isLUB_sSup, IsLUB.unique
-- Module: Mathlib.Order.CompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : CompletePartialOrder α
inst_1 : Preorder β
f : α → β
h : ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → IsLUB (f '' d) (f (sSup d))
d : Set α
hne : d.Nonempty
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
⊢ IsLUB (f '' d) (f (sSup d))

Tactic:
h hne hd
-- Module: Mathlib.Order.CompletePartialOrder
Goal:
α : Type u_2
β : Type u_3
inst : CompletePartialOrder α
inst_1 : Preorder β
f : α → β
h : ∀ ⦃d : Set α⦄, d.Nonempty → DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d → IsLUB (f '' d) (f (sSup d))
d : Set α
hne : d.Nonempty
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
⊢ IsLUB (f '' d) (f (sSup d))

Tactic:
exact h hne hd
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : CompleteLatticeHom α β
carrier : Set α
sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sSup s ∈ carrier
sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sInf s ∈ carrier
x : α
hx : x ∈ carrier
y : α
hy : y ∈ carrier
this : x ⊔ y = sSup {x, y}
z : α
hz : Membership.mem (γ := Set α) {x, y} z
⊢ z ∈ carrier

Tactic:
aesop
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : CompleteLatticeHom α β
carrier : Set α
sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sSup s ∈ carrier
sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sInf s ∈ carrier
x : α
hx : x ∈ carrier
y : α
hy : y ∈ carrier
this : x ⊔ y = sSup {x, y}
⊢ x ⊔ y ∈ carrier

Tactic:
exact this ▸ sSupClosed' (fun z hz ↦ by aesop)
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : CompleteLatticeHom α β
carrier : Set α
sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sSup s ∈ carrier
sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sInf s ∈ carrier
x : α
hx : x ∈ carrier
y : α
hy : y ∈ carrier
suffices : x ⊔ y = sSup {x, y}
⊢ x ⊔ y ∈ carrier

Tactic:
suffices x ⊔ y = sSup {x, y} by exact this ▸ sSupClosed' (fun z hz ↦ by aesop)
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : CompleteLatticeHom α β
carrier : Set α
sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sSup s ∈ carrier
sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sInf s ∈ carrier
x : α
hx : x ∈ carrier
y : α
hy : y ∈ carrier
⊢ x ⊔ y = sSup {x, y}

Tactic:
simp [sSup_singleton]

Premises used: sSup_singleton
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : CompleteLatticeHom α β
carrier : Set α
sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sSup s ∈ carrier
sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sInf s ∈ carrier
x : α
hx : x ∈ carrier
y : α
hy : y ∈ carrier
this : x ⊓ y = sInf {x, y}
z : α
hz : Membership.mem (γ := Set α) {x, y} z
⊢ z ∈ carrier

Tactic:
aesop
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : CompleteLatticeHom α β
carrier : Set α
sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sSup s ∈ carrier
sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sInf s ∈ carrier
x : α
hx : x ∈ carrier
y : α
hy : y ∈ carrier
this : x ⊓ y = sInf {x, y}
⊢ x ⊓ y ∈ carrier

Tactic:
exact this ▸ sInfClosed' (fun z hz ↦ by aesop)
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : CompleteLatticeHom α β
carrier : Set α
sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sSup s ∈ carrier
sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sInf s ∈ carrier
x : α
hx : x ∈ carrier
y : α
hy : y ∈ carrier
suffices : x ⊓ y = sInf {x, y}
⊢ x ⊓ y ∈ carrier

Tactic:
suffices x ⊓ y = sInf {x, y} by exact this ▸ sInfClosed' (fun z hz ↦ by aesop)
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : CompleteLatticeHom α β
carrier : Set α
sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sSup s ∈ carrier
sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sInf s ∈ carrier
x : α
hx : x ∈ carrier
y : α
hy : y ∈ carrier
⊢ x ⊓ y = sInf {x, y}

Tactic:
simp [sInf_singleton]

Premises used: sInf_singleton
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : CompleteLatticeHom α β
L_1 L M : CompleteSublattice α
h :
  Eq.{u_1 + 1} (α := Set α) ((fun (L : CompleteSublattice α) ↦ L.carrier) L)
    ((fun (L : CompleteSublattice α) ↦ L.carrier) M)
mk :
  ∀ (toSublattice : Sublattice α)
    (sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ toSublattice.carrier → sSup s ∈ toSublattice.carrier)
    (sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ toSublattice.carrier → sInf s ∈ toSublattice.carrier)
    (h :
      Eq.{u_1 + 1} (α := Set α)
        ((fun (L : CompleteSublattice α) ↦ L.carrier)
          { toSublattice := toSublattice, sSupClosed' := sSupClosed', sInfClosed' := sInfClosed' })
        ((fun (L : CompleteSublattice α) ↦ L.carrier) M)),
    { toSublattice := toSublattice, sSupClosed' := sSupClosed', sInfClosed' := sInfClosed' : CompleteSublattice α } = M
⊢ L = M

Tactic:
cases L
-- Module: Mathlib.Order.CompleteSublattice
Goal:
α : Type u_1
β : Type u_2
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : CompleteLatticeHom α β
L M : CompleteSublattice α
toSublattice : Sublattice α
sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ toSublattice.carrier → sSup s ∈ toSublattice.carrier
sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ toSublattice.carrier → sInf s ∈ toSublattice.carrier
h :
  Eq.{u_1 + 1} (α := Set α)
    ((fun (L : CompleteSublattice α) ↦ L.carrier)
      { toSublattice := toSublattice, sSupClosed' := sSupClosed', sInfClosed' := sInfClosed' })
    ((fun (L : CompleteSublattice α) ↦ L.carrier) M)
mk :
  ∀ (toSublattice_1 : Sublattice α)
    (sSupClosed'_1 : ∀ ⦃s : Set α⦄, s ⊆ toSublattice_1.carrier → sSup s ∈ toSublattice_1.carrier)
    (sInfClosed'_1 : ∀ ⦃s : Set α⦄, s ⊆ toSublattice_1.carrier → sInf s ∈ toSublattice_1.carrier)
    (h :
      Eq.{u_1 + 1} (α := Set α)
        ((fun (L : CompleteSublattice α) ↦ L.carrier)
          { toSublattice := toSublattice, sSupClosed' := sSupClosed', sInfClosed' := sInfClosed' })
        ((fun (L : CompleteSublattice α) ↦ L.carrier)
          { toSublattice := toSublattice_1, sSupClosed' := sSupClosed'_1, sInfClosed' := sInfClosed'_1 })),
    { toSublattice := toSublattice, sSupClosed' := sSupClosed', sInfClosed' := sInfClosed' : CompleteSublattice α } =
      { toSublattice := toSublattice_1, sSupClosed' := sSupClosed'_1, sInfClosed' := sInfClosed'_1 }
⊢ { toSublattice := toSublattice, sSupClosed' := sSupClosed', sInfClosed' := sInfClosed' : CompleteSublattice α } = M

Tactic:
cases M