awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
inst : LE α
⊢ (↑⊤ : Set α) = ∅

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
inst : LE α
⊢ (↑⊥ : Set α) = univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
inst : LE α
s : UpperSet α
⊢ (↑s : Set α) = univ ↔ s = ⊥

Tactic:
simp [SetLike.ext'_iff]

Premises used: SetLike.ext'_iff
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
inst : LE α
s : UpperSet α
⊢ (↑s : Set α) = ∅ ↔ s = ⊤

Tactic:
simp [SetLike.ext'_iff]

Premises used: SetLike.ext'_iff
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
inst : LE α
s : UpperSet α
⊢ (↑s : Set α).Nonempty ↔ s ≠ ⊤

Tactic:
nonempty_iff_ne_empty.trans coe_eq_empty.not

Premises used: UpperSet.coe_eq_empty, Iff.not, Set.nonempty_iff_ne_empty, Iff.trans
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
inst : LE α
s t : UpperSet α
⊢ (↑(s ⊔ t) : Set α) = (↑s : Set α) ∩ (↑t : Set α)

Tactic:
rfl

Premises used: setOf, Set.inter, rfl
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
inst : LE α
s t : UpperSet α
⊢ (↑(s ⊓ t) : Set α) = (↑s : Set α) ∪ (↑t : Set α)

Tactic:
rfl

Premises used: Set.union, setOf, rfl
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
inst : LE α
S : Set (UpperSet α)
⊢ (↑(sSup S) : Set α) = ⋂ s ∈ S, (↑s : Set α)

Tactic:
rfl

Premises used: iInf, Set.iInter, setOf, rfl
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
inst : LE α
S : Set (UpperSet α)
⊢ (↑(sInf S) : Set α) = ⋃ s ∈ S, (↑s : Set α)

Tactic:
rfl

Premises used: iSup, setOf, Set.iUnion, rfl
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
ι : Sort u_4
inst : LE α
f : ι → UpperSet α
⊢ (↑(⨆ (i : ι), f i) : Set α) = ⋂ (i : ι), (↑(f i) : Set α)

Tactic:
simp [iSup]

Premises used: iSup
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
ι : Sort u_4
inst : LE α
f : ι → UpperSet α
⊢ (↑(⨅ (i : ι), f i) : Set α) = ⋃ (i : ι), (↑(f i) : Set α)

Tactic:
simp [iInf]

Premises used: iInf
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst : LE α
f : (i : ι) → κ i → UpperSet α
⊢ (↑(⨆ (i : ι), ⨆ (j : κ i), f i j) : Set α) = ⋂ (i : ι), ⋂ (j : κ i), (↑(f i j) : Set α)

Tactic:
simp
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst : LE α
f : (i : ι) → κ i → UpperSet α
⊢ (↑(⨅ (i : ι), ⨅ (j : κ i), f i j) : Set α) = ⋃ (i : ι), ⋃ (j : κ i), (↑(f i j) : Set α)

Tactic:
simp
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
inst : LE α
a : α
⊢ a ∉ ⊤

Tactic:
id

Premises used: Set.Mem, id, Not
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
inst : LE α
a : α
⊢ Membership.mem (γ := UpperSet α) ⊥ a

Tactic:
trivial

Premises used: trivial, Set.Mem, Set.univ, setOf
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
inst : LE α
s t : UpperSet α
a : α
⊢ a ∈ s ⊔ t ↔ a ∈ s ∧ a ∈ t

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
inst : LE α
s t : UpperSet α
a : α
⊢ a ∈ s ⊓ t ↔ a ∈ s ∨ a ∈ t

Tactic:
Iff.rfl

Premises used: Set.union, Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
inst : LE α
S : Set (UpperSet α)
a : α
⊢ a ∈ sSup S ↔ ∀ s ∈ S, a ∈ s

Tactic:
mem_iInter₂

Premises used: iInf, Set.Mem, Set.iInter, setOf, Set.mem_iInter₂
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
inst : LE α
S : Set (UpperSet α)
a : α
⊢ (∃ (i : UpperSet α) (_ : i ∈ S), a ∈ (↑i : Set α)) ↔ ∃ s ∈ S, a ∈ s

Tactic:
simp only [exists_prop, SetLike.mem_coe]

Premises used: exists_prop, SetLike.mem_coe
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
ι : Sort u_4
inst : LE α
a : α
f : ι → UpperSet α
rw : Membership.mem (γ := Set α) (⋂ (i : ι), (↑(f i) : Set α)) a ↔ ∀ (i : ι), a ∈ f i
⊢ Membership.mem (γ := UpperSet α) (⨆ (i : ι), f i) a ↔ ∀ (i : ι), a ∈ f i

Tactic:
rw [← SetLike.mem_coe, coe_iSup]

Premises used: UpperSet.coe_iSup, SetLike.mem_coe
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
ι : Sort u_4
inst : LE α
a : α
f : ι → UpperSet α
⊢ Membership.mem (γ := Set α) (⋂ (i : ι), (↑(f i) : Set α)) a ↔ ∀ (i : ι), a ∈ f i

Tactic:
mem_iInter

Premises used: Set.mem_iInter
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
ι : Sort u_4
inst : LE α
a : α
f : ι → UpperSet α
⊢ Membership.mem (γ := Set α) (⋂ (i : ι), (↑(f i) : Set α)) a ↔ ∀ (i : ι), a ∈ f i

Tactic:
exact mem_iInter

Premises used: Set.mem_iInter
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
ι : Sort u_4
inst : LE α
a : α
f : ι → UpperSet α
rw : Membership.mem (γ := Set α) (⋃ (i : ι), (↑(f i) : Set α)) a ↔ ∃ (i : ι), a ∈ f i
⊢ Membership.mem (γ := UpperSet α) (⨅ (i : ι), f i) a ↔ ∃ (i : ι), a ∈ f i

Tactic:
rw [← SetLike.mem_coe, coe_iInf]

Premises used: UpperSet.coe_iInf, SetLike.mem_coe
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
ι : Sort u_4
inst : LE α
a : α
f : ι → UpperSet α
⊢ Membership.mem (γ := Set α) (⋃ (i : ι), (↑(f i) : Set α)) a ↔ ∃ (i : ι), a ∈ f i

Tactic:
mem_iUnion

Premises used: Set.mem_iUnion
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
ι : Sort u_4
inst : LE α
a : α
f : ι → UpperSet α
⊢ Membership.mem (γ := Set α) (⋃ (i : ι), (↑(f i) : Set α)) a ↔ ∃ (i : ι), a ∈ f i

Tactic:
exact mem_iUnion

Premises used: Set.mem_iUnion
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst : LE α
a : α
f : (i : ι) → κ i → UpperSet α
⊢ Membership.mem (γ := UpperSet α) (⨆ (i : ι), ⨆ (j : κ i), f i j) a ↔ ∀ (i : ι) (j : κ i), a ∈ f i j

Tactic:
simp
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst : LE α
a : α
f : (i : ι) → κ i → UpperSet α
⊢ Membership.mem (γ := UpperSet α) (⨅ (i : ι), ⨅ (j : κ i), f i j) a ↔ ∃ (i : ι) (j : κ i), a ∈ f i j

Tactic:
simp
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
inst : LE α
s t : UpperSet α
⊢ Codisjoint (↑s : Set α) (↑t : Set α) ↔ Disjoint s t

Tactic:
simp [disjoint_iff, codisjoint_iff, SetLike.ext'_iff]

Premises used: codisjoint_iff, disjoint_iff, SetLike.ext'_iff
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
inst : LE α
s : UpperSet α
⊢ (↑s.compl : Set α) = (↑s : Set α)ᶜ

Tactic:
rfl

Premises used: setOf, Not, rfl
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
inst : LE α
s : UpperSet α
a : α
⊢ a ∈ s.compl ↔ a ∉ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Not
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
inst : LE α
s : UpperSet α
⊢ s.compl.compl = s

Tactic:
UpperSet.ext <| compl_compl _

Premises used: compl_compl, UpperSet.ext
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
inst : LE α
s t : UpperSet α
⊢ s.compl ≤ t.compl ↔ s ≤ t

Tactic:
compl_subset_compl

Premises used: setOf, Set.compl_subset_compl, Not
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
inst : LE α
s t : UpperSet α
⊢ (s ⊔ t).compl = s.compl ⊔ t.compl

Tactic:
LowerSet.ext compl_inf

Premises used: compl_inf, LowerSet.ext
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
inst : LE α
s t : UpperSet α
⊢ (s ⊓ t).compl = s.compl ⊓ t.compl

Tactic:
LowerSet.ext compl_sup

Premises used: LowerSet.ext, compl_sup
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
inst : LE α
⊢ Eq.{u_1 + 1} (α := LowerSet α) (compl ⊤) ⊤

Tactic:
LowerSet.ext compl_empty

Premises used: LowerSet.ext, Set.compl_empty
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
inst : LE α
⊢ Eq.{u_1 + 1} (α := LowerSet α) (compl ⊥) ⊥

Tactic:
LowerSet.ext compl_univ

Premises used: Set.compl_univ, LowerSet.ext
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
inst : LE α
S : Set (UpperSet α)
⊢ (↑(sSup S).compl : Set α) = (↑(⨆ s ∈ S, s.compl) : Set α)

Tactic:
simp only [coe_compl, coe_sSup, compl_iInter₂, LowerSet.coe_iSup₂]

Premises used: Set.compl_iInter₂, UpperSet.coe_compl, LowerSet.coe_iSup₂, UpperSet.coe_sSup
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
inst : LE α
S : Set (UpperSet α)
⊢ (↑(sInf S).compl : Set α) = (↑(⨅ s ∈ S, s.compl) : Set α)

Tactic:
simp only [coe_compl, coe_sInf, compl_iUnion₂, LowerSet.coe_iInf₂]

Premises used: UpperSet.coe_compl, Set.compl_iUnion₂, LowerSet.coe_iInf₂, UpperSet.coe_sInf
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
ι : Sort u_4
inst : LE α
f : ι → UpperSet α
⊢ (↑(compl (⨆ (i : ι), f i)) : Set α) = (↑(⨆ (i : ι), (f i).compl) : Set α)

Tactic:
simp only [coe_compl, coe_iSup, compl_iInter, LowerSet.coe_iSup]

Premises used: Set.compl_iInter, LowerSet.coe_iSup, UpperSet.coe_compl, UpperSet.coe_iSup
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
ι : Sort u_4
inst : LE α
f : ι → UpperSet α
⊢ (↑(compl (⨅ (i : ι), f i)) : Set α) = (↑(⨅ (i : ι), (f i).compl) : Set α)

Tactic:
simp only [coe_compl, coe_iInf, compl_iUnion, LowerSet.coe_iInf]

Premises used: UpperSet.coe_compl, Set.compl_iUnion, LowerSet.coe_iInf, UpperSet.coe_iInf
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst : LE α
f : (i : ι) → κ i → UpperSet α
⊢ Eq.{u_1 + 1} (α := LowerSet α) (compl (⨆ (i : ι), ⨆ (j : κ i), f i j)) (⨆ (i : ι), ⨆ (j : κ i), (f i j).compl)

Tactic:
simp
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst : LE α
f : (i : ι) → κ i → UpperSet α
⊢ Eq.{u_1 + 1} (α := LowerSet α) (compl (⨅ (i : ι), ⨅ (j : κ i), f i j)) (⨅ (i : ι), ⨅ (j : κ i), (f i j).compl)

Tactic:
simp
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : LinearOrder α
⊢ Std.Total fun (x1 x2 : UpperSet α) ↦ x1 ≤ x2

Tactic:
⟨fun s t => t.upper.total s.upper⟩

Premises used: IsUpperSet.total, UpperSet.upper, Std.Total.mk
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : LinearOrder α
⊢ LinearOrder (UpperSet α)

Tactic:
exact Lattice.toLinearOrder _

Premises used: Lattice.toLinearOrder
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : LinearOrder α
⊢ LinearOrder (UpperSet α)

Tactic:
classical exact Lattice.toLinearOrder _

Premises used: Lattice.toLinearOrder
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : LinearOrder α
⊢ Std.Total fun (x1 x2 : LowerSet α) ↦ x1 ≤ x2

Tactic:
⟨fun s t => s.lower.total t.lower⟩

Premises used: Std.Total.mk, LowerSet.lower, IsLowerSet.total
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : LinearOrder α
⊢ LinearOrder (LowerSet α)

Tactic:
exact Lattice.toLinearOrder _

Premises used: Lattice.toLinearOrder
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
κ : ι → Sort u_5
inst : LinearOrder α
⊢ LinearOrder (LowerSet α)

Tactic:
classical exact Lattice.toLinearOrder _

Premises used: Lattice.toLinearOrder
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
h :
  ∀ (x : UpperSet β) (x_1 : α),
    x_1 ∈ (↑(((map f).symm : (a : UpperSet β) → UpperSet α) x : UpperSet α) : Set α) ↔
      x_1 ∈ (↑((map f.symm : (a : UpperSet β) → UpperSet α) x : UpperSet α) : Set α)
⊢ (map f).symm = map f.symm

Tactic:
ext
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
x : UpperSet β
x_1 : α
⊢ x_1 ∈ (↑(((map f).symm : (a : UpperSet β) → UpperSet α) x : UpperSet α) : Set α) ↔
    x_1 ∈ (↑((map f.symm : (a : UpperSet β) → UpperSet α) x : UpperSet α) : Set α)

Tactic:
simp [map, OrderIso.symm_apply_eq]

Premises used: OrderIso.symm_apply_eq, UpperSet.map
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
s : UpperSet α
b : β
rw :
  Membership.mem (γ := UpperSet β) (((map f.symm).symm : (a : UpperSet α) → UpperSet β) s : UpperSet β) b ↔
    Membership.mem (α := α) s ((f.symm : (a : β) → α) b : α)
⊢ Membership.mem (γ := UpperSet β) ((map f : (a : UpperSet α) → UpperSet β) s : UpperSet β) b ↔
    Membership.mem (α := α) s ((f.symm : (a : β) → α) b : α)

Tactic:
rw [← f.symm_symm, ← symm_map, f.symm_symm]

Premises used: OrderIso.symm_symm, UpperSet.symm_map
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
s : UpperSet α
b : β
⊢ Membership.mem (γ := UpperSet β) (((map f.symm).symm : (a : UpperSet α) → UpperSet β) s : UpperSet β) b ↔
    Membership.mem (α := α) s ((f.symm : (a : β) → α) b : α)

Tactic:
rfl
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
inst : Preorder α
h :
  ∀ (x : UpperSet α) (x_1 : α),
    x_1 ∈ (↑((map (OrderIso.refl α) : (a : UpperSet α) → UpperSet α) x : UpperSet α) : Set α) ↔
      x_1 ∈ (↑((OrderIso.refl (UpperSet α) : (a : UpperSet α) → UpperSet α) x : UpperSet α) : Set α)
⊢ Eq (α := UpperSet α ≃o UpperSet α) (map (OrderIso.refl α)) (OrderIso.refl (UpperSet α))

Tactic:
ext
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
inst : Preorder α
x : UpperSet α
x_1 : α
⊢ x_1 ∈ (↑((map (OrderIso.refl α) : (a : UpperSet α) → UpperSet α) x : UpperSet α) : Set α) ↔
    x_1 ∈ (↑((OrderIso.refl (UpperSet α) : (a : UpperSet α) → UpperSet α) x : UpperSet α) : Set α)

Tactic:
simp
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
s : UpperSet α
g : β ≃o γ
f : α ≃o β
a :
  ∀ (x : γ),
    x ∈ (↑((map g : (a : UpperSet β) → UpperSet γ) ((map f : (a : UpperSet α) → UpperSet β) s) : UpperSet γ) : Set γ) ↔
      x ∈ (↑((map (f.trans g) : (a : UpperSet α) → UpperSet γ) s : UpperSet γ) : Set γ)
⊢ Eq.{u_3 + 1} (α := UpperSet γ)
    ((map g : (a : UpperSet β) → UpperSet γ) ((map f : (a : UpperSet α) → UpperSet β) s) : UpperSet γ)
    ((map (f.trans g) : (a : UpperSet α) → UpperSet γ) s : UpperSet γ)

Tactic:
ext
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
s : UpperSet α
g : β ≃o γ
f : α ≃o β
x : γ
⊢ x ∈ (↑((map g : (a : UpperSet β) → UpperSet γ) ((map f : (a : UpperSet α) → UpperSet β) s) : UpperSet γ) : Set γ) ↔
    x ∈ (↑((map (f.trans g) : (a : UpperSet α) → UpperSet γ) s : UpperSet γ) : Set γ)

Tactic:
simp
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
s : UpperSet α
⊢ (↑((map f : (a : UpperSet α) → UpperSet β) s : UpperSet β) : Set β) = (⇑f : (a : α) → β) '' (↑s : Set α)

Tactic:
rfl

Premises used: setOf, Set.image, rfl
-- Module: Mathlib.Order.UpperLower.CompleteLattice
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α ≃o β
s : UpperSet α
⊢ Eq.{u_2 + 1} (α := LowerSet β) (compl ((map f : (a : UpperSet α) → UpperSet β) s))
    ((LowerSet.map f : (a : LowerSet α) → LowerSet β) s.compl)

Tactic:
SetLike.coe_injective (Set.image_compl_eq f.bijective).symm

Premises used: OrderIso.bijective, Set.image_compl_eq, SetLike.coe_injective, Eq.symm
-- Module: Mathlib.Order.UpperLower.Fibration
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LE α
inst_1 : LE β
hf : Fibration (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : β) ↦ x1 ≤ x2) f
s : Set α
hs : IsLowerSet s
y' : β
x : α
hx : x ∈ s
e : y' ≤ f x
obtain : ∀ (y : α) (e' : y ≤ x) (e : f y ≤ f x), f y ∈ f '' s
⊢ y' ∈ f '' s

Tactic:
obtain ⟨y, e', rfl⟩ := hf e

Premises used: rfl
-- Module: Mathlib.Order.UpperLower.Fibration
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LE α
inst_1 : LE β
hf : Fibration (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : β) ↦ x1 ≤ x2) f
s : Set α
hs : IsLowerSet s
x : α
hx : x ∈ s
y : α
e' : y ≤ x
e : f y ≤ f x
⊢ f y ∈ f '' s

Tactic:
⟨_, hs e' hx, rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.Order.UpperLower.Fibration
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LE α
inst_1 : LE β
hf : Fibration (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : β) ↦ x1 ≤ x2) f
s : Set α
hs : IsLowerSet s
x : α
hx : x ∈ s
y : α
e' : y ≤ x
e : f y ≤ f x
⊢ f y ∈ f '' s

Tactic:
exact ⟨_, hs e' hx, rfl⟩
-- Module: Mathlib.Order.UpperLower.Fibration
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : LE β
⊢ Fibration (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : β) ↦ x1 ≤ x2) f ↔ ∀ (x : α), IsLowerSet (f '' Iic x)

Tactic:
⟨fun h x ↦ (isLowerSet_Iic x).image_fibration h, fun H x _ e ↦ H x e ⟨x, le_rfl, rfl⟩⟩

Premises used: le_rfl, And.intro, Iff.intro, Exists.intro, IsLowerSet.image_fibration, rfl, isLowerSet_Iic
-- Module: Mathlib.Order.UpperLower.Fibration
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : LE β
⊢ Fibration (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : β) ↦ x1 ≤ x2) f ↔
    ∀ (s : Set α), IsLowerSet s → IsLowerSet (f '' s)

Tactic:
⟨Fibration.isLowerSet_image,
    fun H ↦ fibration_iff_isLowerSet_image_Iic.mpr (H _ <| isLowerSet_Iic ·)⟩

Premises used: Iff.mpr, Relation.Fibration.isLowerSet_image, Iff.intro, Set.Iic, Relation.fibration_iff_isLowerSet_image_Iic, isLowerSet_Iic
-- Module: Mathlib.Order.UpperLower.Fibration
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
hf : Monotone f
⊢ Fibration (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x1 x2 : β) ↦ x1 ≤ x2) f ↔ ∀ (x : α), f '' Iic x = Iic (f x)

Tactic:
⟨fun H x ↦ le_antisymm (fun _ ⟨_, hy, e⟩ ↦ e ▸ hf hy)
    ((H.isLowerSet_image (isLowerSet_Iic x)).Iic_subset ⟨x, le_rfl, rfl⟩),
    fun H ↦ fibration_iff_isLowerSet_image_Iic.mpr (fun x ↦ (H x).symm ▸ isLowerSet_Iic (f x))⟩

Premises used: Iff.mpr, IsLowerSet.Iic_subset, le_rfl, Eq.rec, Relation.Fibration.isLowerSet_image, le_antisymm, And.intro, Iff.intro, Exists.intro, Relation.fibration_iff_isLowerSet_image_Iic, Eq.symm, rfl, isLowerSet_Iic
-- Module: Mathlib.Order.UpperLower.Fibration
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LE α
inst_1 : LE β
hf : Fibration (fun (x1 x2 : α) ↦ x1 ≥ x2) (fun (x1 x2 : β) ↦ x1 ≥ x2) f
s : Set α
hs : IsUpperSet s
⊢ IsUpperSet (f '' s)

Tactic:
@Fibration.isLowerSet_image αᵒᵈ βᵒᵈ _ _ _ hf s hs

Premises used: Set.Mem, IsUpperSet, Relation.Fibration.isLowerSet_image, OrderDual
-- Module: Mathlib.Order.UpperLower.Fibration
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : LE β
⊢ Fibration (fun (x1 x2 : α) ↦ x1 ≥ x2) (fun (x1 x2 : β) ↦ x1 ≥ x2) f ↔ ∀ (x : α), IsUpperSet (f '' Ici x)

Tactic:
@fibration_iff_isLowerSet_image_Iic αᵒᵈ βᵒᵈ _ _ _

Premises used: Set.Ici, Set.Mem, setOf, IsUpperSet, OrderDual, Relation.fibration_iff_isLowerSet_image_Iic
-- Module: Mathlib.Order.UpperLower.Fibration
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : LE β
⊢ Fibration (fun (x1 x2 : α) ↦ x1 ≥ x2) (fun (x1 x2 : β) ↦ x1 ≥ x2) f ↔
    ∀ (s : Set α), IsUpperSet s → IsUpperSet (f '' s)

Tactic:
@fibration_iff_isLowerSet_image αᵒᵈ βᵒᵈ _ _ _

Premises used: Set.Mem, Relation.fibration_iff_isLowerSet_image, IsUpperSet, OrderDual
-- Module: Mathlib.Order.UpperLower.Fibration
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : Preorder α
inst_1 : Preorder β
hf : Monotone f
⊢ Fibration (fun (x1 x2 : α) ↦ x1 ≥ x2) (fun (x1 x2 : β) ↦ x1 ≥ x2) f ↔ ∀ (x : α), f '' Ici x = Ici (f x)

Tactic:
fibration_iff_image_Iic hf.dual

Premises used: Set.Ici, setOf, Monotone.dual, OrderDual, Relation.fibration_iff_image_Iic
-- Module: Mathlib.Order.UpperLower.Hom
Goal:
α : Type u_1
inst : SemilatticeSup α
⊢ Eq.{u_1 + 1} (α := (a : α) → UpperSet α) (⇑iciSupHom : (a : α) → UpperSet α) Ici

Tactic:
rfl

Premises used: UpperSet.Ici, rfl
-- Module: Mathlib.Order.UpperLower.Hom
Goal:
α : Type u_1
inst : SemilatticeSup α
a : α
⊢ Eq (α := UpperSet α) ((iciSupHom : (a : α) → UpperSet α) a : UpperSet α) (Ici a : UpperSet α)

Tactic:
rfl

Premises used: UpperSet.Ici, rfl
-- Module: Mathlib.Order.UpperLower.Hom
Goal:
α : Type u_1
inst : CompleteLattice α
⊢ Eq.{u_1 + 1} (α := (a : α) → UpperSet α) (⇑icisSupHom : (a : α) → UpperSet α) Ici

Tactic:
rfl

Premises used: UpperSet.Ici, rfl
-- Module: Mathlib.Order.UpperLower.Hom
Goal:
α : Type u_1
inst : CompleteLattice α
a : α
⊢ Eq (α := UpperSet α) ((icisSupHom : (a : α) → UpperSet α) a : UpperSet α) (Ici a : UpperSet α)

Tactic:
rfl

Premises used: UpperSet.Ici, rfl
-- Module: Mathlib.Order.UpperLower.Hom
Goal:
α : Type u_1
inst : SemilatticeInf α
⊢ Eq.{u_1 + 1} (α := (a : α) → LowerSet α) (⇑iicInfHom : (a : α) → LowerSet α) Iic

Tactic:
rfl

Premises used: rfl, LowerSet.Iic
-- Module: Mathlib.Order.UpperLower.Hom
Goal:
α : Type u_1
inst : SemilatticeInf α
a : α
⊢ Eq (α := LowerSet α) ((iicInfHom : (a : α) → LowerSet α) a : LowerSet α) (Iic a : LowerSet α)

Tactic:
rfl

Premises used: rfl, LowerSet.Iic
-- Module: Mathlib.Order.UpperLower.Hom
Goal:
α : Type u_1
inst : CompleteLattice α
⊢ Eq.{u_1 + 1} (α := (a : α) → LowerSet α) (⇑iicsInfHom : (a : α) → LowerSet α) Iic

Tactic:
rfl

Premises used: rfl, LowerSet.Iic
-- Module: Mathlib.Order.UpperLower.Hom
Goal:
α : Type u_1
inst : CompleteLattice α
a : α
⊢ Eq (α := LowerSet α) ((iicsInfHom : (a : α) → LowerSet α) a : LowerSet α) (Iic a : LowerSet α)

Tactic:
rfl

Premises used: rfl, LowerSet.Iic
-- Module: Mathlib.Order.UpperLower.LocallyFinite
Goal:
α : Type u_1
inst : Preorder α
s : Set α
inst_1 : LocallyFiniteOrderTop α
hs : s.Finite
rw : Set.Finite.{u_1} (α := α) (⋃ a ∈ s, Ici a)
⊢ (↑(upperClosure s) : Set α).Finite

Tactic:
rw [coe_upperClosure]

Premises used: coe_upperClosure
-- Module: Mathlib.Order.UpperLower.LocallyFinite
Goal:
α : Type u_1
inst : Preorder α
s : Set α
inst_1 : LocallyFiniteOrderTop α
hs : s.Finite
⊢ Set.Finite.{u_1} (α := α) (⋃ a ∈ s, Ici a)

Tactic:
hs.biUnion fun _ _ => finite_Ici _

Premises used: Set.Finite.biUnion, Set.finite_Ici
-- Module: Mathlib.Order.UpperLower.LocallyFinite
Goal:
α : Type u_1
inst : Preorder α
s : Set α
inst_1 : LocallyFiniteOrderTop α
hs : s.Finite
⊢ Set.Finite.{u_1} (α := α) (⋃ a ∈ s, Ici a)

Tactic:
exact hs.biUnion fun _ _ => finite_Ici _

Premises used: Set.Finite.biUnion, Set.finite_Ici
-- Module: Mathlib.Order.UpperLower.LocallyFinite
Goal:
α : Type u_1
inst : Preorder α
s : Set α
inst_1 : LocallyFiniteOrderBot α
hs : s.Finite
rw : Set.Finite.{u_1} (α := α) (⋃ a ∈ s, Iic a)
⊢ (↑(lowerClosure s) : Set α).Finite

Tactic:
rw [coe_lowerClosure]

Premises used: coe_lowerClosure
-- Module: Mathlib.Order.UpperLower.LocallyFinite
Goal:
α : Type u_1
inst : Preorder α
s : Set α
inst_1 : LocallyFiniteOrderBot α
hs : s.Finite
⊢ Set.Finite.{u_1} (α := α) (⋃ a ∈ s, Iic a)

Tactic:
hs.biUnion fun _ _ => finite_Iic _

Premises used: Set.finite_Iic, Set.Finite.biUnion
-- Module: Mathlib.Order.UpperLower.LocallyFinite
Goal:
α : Type u_1
inst : Preorder α
s : Set α
inst_1 : LocallyFiniteOrderBot α
hs : s.Finite
⊢ Set.Finite.{u_1} (α := α) (⋃ a ∈ s, Iic a)

Tactic:
exact hs.biUnion fun _ _ => finite_Iic _

Premises used: Set.finite_Iic, Set.Finite.biUnion
-- Module: Mathlib.Order.UpperLower.Principal
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ (↑(Ici a) : Set α) = Set.Ici a

Tactic:
rfl

Premises used: Set.Ici, setOf, rfl
-- Module: Mathlib.Order.UpperLower.Principal
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ (↑(Ioi a) : Set α) = Set.Ioi a

Tactic:
rfl

Premises used: Set.Ioi, setOf, rfl
-- Module: Mathlib.Order.UpperLower.Principal
Goal:
α : Type u_1
inst : Preorder α
a b : α
⊢ Membership.mem (γ := UpperSet α) (Ici a) b ↔ a ≤ b

Tactic:
Iff.rfl

Premises used: Set.Ici, Set.Mem, Iff.rfl, setOf