awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
inst_1 : Nonempty ι
f : ι → α
hd : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hf : BddAbove (range f)
h :
  ∀ (x : α), Membership.mem (γ := Set α) (Ici (⨆ (i : ι), f i)) x ↔ Membership.mem (γ := Set α) (⋂ (i : ι), Ici (f i)) x
⊢ Eq.{u_1 + 1} (α := Set α) (Ici (⨆ (i : ι), f i)) (⋂ (i : ι), Ici (f i))

Tactic:
ext
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
inst_1 : Nonempty ι
f : ι → α
hd : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hf : BddAbove (range f)
x : α
⊢ Membership.mem (γ := Set α) (Ici (⨆ (i : ι), f i)) x ↔ Membership.mem (γ := Set α) (⋂ (i : ι), Ici (f i)) x

Tactic:
simpa using hd.ciSup_le_iff hf

Premises used: Directed.ciSup_le_iff
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompletePartialOrderSup α
inst_1 : Preorder β
f : β → α
a : β
hf : Monotone f
⊢ Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) fun (x : (↑(Iic a) : Type u_2)) ↦ f (↑x : β)

Tactic:
have hd : Directed (· ≤ ·) (fun x : Iic a ↦ f x) := fun x y ↦ ⟨⟨a, le_refl a⟩, ⟨hf x.2, hf y.2⟩⟩
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompletePartialOrderSup α
inst_1 : Preorder β
f : β → α
a : β
hf : Monotone f
hd : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) fun (x : (↑(Iic a) : Type u_2)) ↦ f (↑x : β)
x : α
⊢ Membership.mem (γ := Set α) (range fun (x : (↑(Iic a) : Type u_2)) ↦ f (↑x : β)) x → x ≤ f a

Tactic:
aesop
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompletePartialOrderSup α
inst_1 : Preorder β
f : β → α
a : β
hf : Monotone f
hd : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) fun (x : (↑(Iic a) : Type u_2)) ↦ f (↑x : β)
⊢ BddAbove.{u_1} (α := α) (range fun (x : (↑(Iic a) : Type u_2)) ↦ f (↑x : β))

Tactic:
have H : BddAbove (range fun x : Iic a ↦ f x) := ⟨f a, fun _ ↦ by aesop⟩
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompletePartialOrderSup α
inst_1 : Preorder β
f : β → α
a : β
hf : Monotone f
hd : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) fun (x : (↑(Iic a) : Type u_2)) ↦ f (↑x : β)
H : BddAbove.{u_1} (α := α) (range fun (x : (↑(Iic a) : Type u_2)) ↦ f (↑x : β))
apply :
  ⨆ (j : (↑(Iic a) : Type u_2)), f (↑j : β) ≤
    f (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ Iic a) a ⋯ : { x : β // x ∈ Iic a }) : β)
⊢ ⨆ (x : (↑(Iic a) : Type u_2)), f (↑x : β) = f a

Tactic:
apply (hd.le_ciSup H (⟨a, le_refl a⟩ : Iic a)).antisymm'

Premises used: le_refl, LE.le.antisymm', Subtype.mk, Directed.le_ciSup
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompletePartialOrderSup α
inst_1 : Preorder β
f : β → α
a : β
hf : Monotone f
hd : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) fun (x : (↑(Iic a) : Type u_2)) ↦ f (↑x : β)
H : BddAbove.{u_1} (α := α) (range fun (x : (↑(Iic a) : Type u_2)) ↦ f (↑x : β))
rw :
  ∀ (i : (↑(Iic a) : Type u_2)),
    f (↑i : β) ≤ f (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ Iic a) a ⋯ : { x : β // x ∈ Iic a }) : β)
⊢ ⨆ (j : (↑(Iic a) : Type u_2)), f (↑j : β) ≤
    f (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ Iic a) a ⋯ : { x : β // x ∈ Iic a }) : β)

Tactic:
rw [hd.ciSup_le_iff H]

Premises used: Directed.ciSup_le_iff
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompletePartialOrderSup α
inst_1 : Preorder β
f : β → α
a_1 : β
hf : Monotone f
hd : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) fun (x : (↑(Iic a_1) : Type u_2)) ↦ f (↑x : β)
H : BddAbove.{u_1} (α := α) (range fun (x : (↑(Iic a_1) : Type u_2)) ↦ f (↑x : β))
a : β
h : a ∈ Iic a_1
⊢ f (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ Iic a_1) a h) : β) ≤
    f (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ Iic a_1) a_1 ⋯ : { x : β // x ∈ Iic a_1 }) : β)

Tactic:
hf h
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompletePartialOrderSup α
inst_1 : Preorder β
f : β → α
a_1 : β
hf : Monotone f
hd : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) fun (x : (↑(Iic a_1) : Type u_2)) ↦ f (↑x : β)
H : BddAbove.{u_1} (α := α) (range fun (x : (↑(Iic a_1) : Type u_2)) ↦ f (↑x : β))
a : β
h : a ∈ Iic a_1
⊢ f (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ Iic a_1) a h) : β) ≤
    f (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ Iic a_1) a_1 ⋯ : { x : β // x ∈ Iic a_1 }) : β)

Tactic:
exact hf h
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
ι : Sort u_4
inst : ConditionallyCompletePartialOrder α
inst_1 : Nonempty ι
f : ι → α
hd : Directed (fun (x1 x2 : α) ↦ x1 ≥ x2) f
hf : BddBelow (range f)
hd' : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hf' : BddAbove (range f)
⊢ LE.le.{u_1} (α := α) (⨅ (i : ι), f i) (⨆ (i : ι), f i)

Tactic:
(hd.ciInf_le hf (Classical.arbitrary _)).trans <| hd'.le_ciSup hf' (Classical.arbitrary _)

Premises used: Directed.ciInf_le, Classical.arbitrary, LE.le.trans, Directed.le_ciSup
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompletePartialOrderSup α
inst_1 : ConditionallyCompletePartialOrderSup β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hne : s.Nonempty
hbdd : BddAbove s
⊢ l (sSup s) = sSup (l '' s)

Tactic:
gc.isLUB_l_image (hd.isLUB_csSup hne hbdd) |>.unique <|
    (hd.mono_comp gc.monotone_l).isLUB_csSup (hne.image l) (gc.monotone_l.map_bddAbove hbdd)

Premises used: GaloisConnection.isLUB_l_image, DirectedOn.mono_comp, Monotone.map_bddAbove, IsLUB.unique, Set.Nonempty.image, GaloisConnection.monotone_l, DirectedOn.isLUB_csSup
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompletePartialOrderSup α
inst_1 : ConditionallyCompletePartialOrderSup β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hne : s.Nonempty
hbdd : BddAbove s
⊢ l (sSup s) = ⨆ (x : (↑s : Type u_1)), l (↑x : α)

Tactic:
simpa only [← comp_def, ← sSup_range, range_comp, Subtype.range_coe_subtype, setOf_mem_eq]
    using gc.l_csSup_of_directedOn' hd hne hbdd

Premises used: Set.range_comp, Subtype.range_coe_subtype, Set.setOf_mem_eq, Function.comp_def, GaloisConnection.l_csSup_of_directedOn', sSup_range
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
inst_1 : ConditionallyCompletePartialOrderSup β
inst_2 : Nonempty ι
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
hd : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hf : BddAbove (range f)
rw : l (sSup (range fun (i : ι) ↦ f i)) = ⨆ (i : ι), l (f i)
rw₁ : Eq.{u_2 + 1} (α := β) (⨆ (x : (↑(range f) : Type u_1)), l (↑x : α)) (⨆ (i : ι), l (f i))
rw₂ rw₃ : Eq.{u_2 + 1} (α := β) (⨆ (i : ι), l (f i)) (⨆ (i : ι), l (f i))
⊢ l (⨆ (i : ι), f i) = ⨆ (i : ι), l (f i)

Tactic:
rw [iSup, gc.l_csSup_of_directedOn hd.directedOn_range (range_nonempty _) hf, iSup_range']

Premises used: iSup, Directed.directedOn_range, iSup_range', GaloisConnection.l_csSup_of_directedOn, Set.range_nonempty
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompletePartialOrderSup α
inst_1 : ConditionallyCompletePartialOrderSup β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (f '' s)
hf : BddAbove (f '' s)
hne : s.Nonempty
⊢ Nonempty.{u_3 + 1} (↑s : Type u_3)

Tactic:
haveI := hne.to_subtype
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompletePartialOrderSup α
inst_1 : ConditionallyCompletePartialOrderSup β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (f '' s)
hf : BddAbove (f '' s)
hne : s.Nonempty
this : Nonempty.{u_3 + 1} (↑s : Type u_3)
⊢ BddAbove.{u_1} (α := α) (range fun (x : (↑s : Type u_3)) ↦ f (↑x : γ))

Tactic:
rw [image_eq_range] at hf

Premises used: Set.image_eq_range
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompletePartialOrderSup α
inst_1 : ConditionallyCompletePartialOrderSup β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (f '' s)
hf : BddAbove (f '' s)
hne : s.Nonempty
this : Nonempty.{u_3 + 1} (↑s : Type u_3)
hf₁ : BddAbove.{u_1} (α := α) (range fun (x : (↑s : Type u_3)) ↦ f (↑x : γ))
⊢ s.Nonempty

Tactic:
rw [image_eq_range] at hf

Premises used: Set.image_eq_range
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompletePartialOrderSup α
inst_1 : ConditionallyCompletePartialOrderSup β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (f '' s)
hf : BddAbove (f '' s)
hne : s.Nonempty
this : Nonempty.{u_3 + 1} (↑s : Type u_3)
hf₁ : BddAbove.{u_1} (α := α) (range fun (x : (↑s : Type u_3)) ↦ f (↑x : γ))
hne₁ : s.Nonempty
⊢ Nonempty.{u_3 + 1} (↑s : Type u_3)

Tactic:
rw [image_eq_range] at hf

Premises used: Set.image_eq_range
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompletePartialOrderSup α
inst_1 : ConditionallyCompletePartialOrderSup β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (f '' s)
hf : BddAbove.{u_1} (α := α) (range fun (x : (↑s : Type u_3)) ↦ f (↑x : γ))
hne : s.Nonempty
this : Nonempty.{u_3 + 1} (↑s : Type u_3)
⊢ l (⨆ (i : (↑s : Type u_3)), f (↑i : γ)) = ⨆ (i : (↑s : Type u_3)), l (f (↑i : γ))

Tactic:
gc.l_ciSup_of_directed ?_ hf

Premises used: GaloisConnection.l_ciSup_of_directed
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompletePartialOrderSup α
inst_1 : ConditionallyCompletePartialOrderSup β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (f '' s)
hf : BddAbove.{u_1} (α := α) (range fun (x : (↑s : Type u_3)) ↦ f (↑x : γ))
hne : s.Nonempty
this : Nonempty.{u_3 + 1} (↑s : Type u_3)
refine : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) fun (i : (↑s : Type u_3)) ↦ f (↑i : γ)
⊢ l (⨆ (i : (↑s : Type u_3)), f (↑i : γ)) = ⨆ (i : (↑s : Type u_3)), l (f (↑i : γ))

Tactic:
refine gc.l_ciSup_of_directed ?_ hf

Premises used: GaloisConnection.l_ciSup_of_directed
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompletePartialOrderSup α
inst_1 : ConditionallyCompletePartialOrderSup β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → α
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (f '' s)
hf : BddAbove.{u_1} (α := α) (range fun (x : (↑s : Type u_3)) ↦ f (↑x : γ))
hne : s.Nonempty
this : Nonempty.{u_3 + 1} (↑s : Type u_3)
⊢ Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) fun (i : (↑s : Type u_3)) ↦ f (↑i : γ)

Tactic:
simpa [← directedOn_range, ← comp_def, range_comp]

Premises used: Set.range_comp, directedOn_range, Function.comp_def
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompletePartialOrderInf α
inst_1 : ConditionallyCompletePartialOrderInf β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set β
hd : DirectedOn (fun (x1 x2 : β) ↦ x1 ≥ x2) s
hne : s.Nonempty
hbdd : BddBelow s
⊢ u (sInf s) = ⨅ (x : (↑s : Type u_2)), u (↑x : β)

Tactic:
gc.dual.l_csSup_of_directedOn hd hne hbdd

Premises used: iInf, GaloisConnection.dual, GaloisConnection.l_csSup_of_directedOn, OrderDual
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompletePartialOrderInf α
inst_1 : ConditionallyCompletePartialOrderInf β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set β
hd : DirectedOn (fun (x1 x2 : β) ↦ x1 ≥ x2) s
hne : s.Nonempty
hbdd : BddBelow s
⊢ u (sInf s) = sInf (u '' s)

Tactic:
gc.dual.l_csSup_of_directedOn' hd hne hbdd

Premises used: GaloisConnection.dual, GaloisConnection.l_csSup_of_directedOn', OrderDual
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : ConditionallyCompletePartialOrderInf α
inst_1 : ConditionallyCompletePartialOrderInf β
inst_2 : Nonempty ι
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → β
hd : Directed (fun (x1 x2 : β) ↦ x1 ≥ x2) f
hf : BddBelow (range f)
⊢ u (⨅ (i : ι), f i) = ⨅ (i : ι), u (f i)

Tactic:
gc.dual.l_ciSup_of_directed hd hf

Premises used: iInf, iSup, GaloisConnection.dual, GaloisConnection.l_ciSup_of_directed, OrderDual
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompletePartialOrderInf α
inst_1 : ConditionallyCompletePartialOrderInf β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set γ
f : γ → β
hd : DirectedOn (fun (x1 x2 : β) ↦ x1 ≥ x2) (f '' s)
hf : BddBelow (f '' s)
hne : s.Nonempty
⊢ u (⨅ (i : (↑s : Type u_3)), f (↑i : γ)) = ⨅ (i : (↑s : Type u_3)), u (f (↑i : γ))

Tactic:
gc.dual.l_ciSup_set_of_directedOn hd hf hne

Premises used: iInf, iSup, GaloisConnection.l_ciSup_set_of_directedOn, GaloisConnection.dual, OrderDual
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompletePartialOrderSup α
inst_1 : ConditionallyCompletePartialOrderSup β
e : α ≃o β
s : Set α
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hne : s.Nonempty
hbdd : BddAbove s
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (⨆ (x : (↑s : Type u_1)), (e : (a : α) → β) (↑x : α) : β)

Tactic:
e.to_galoisConnection.l_csSup_of_directedOn hd hne hbdd

Premises used: OrderIso.to_galoisConnection, GaloisConnection.l_csSup_of_directedOn
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompletePartialOrderSup α
inst_1 : ConditionallyCompletePartialOrderSup β
e : α ≃o β
s : Set α
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
hne : s.Nonempty
hbdd : BddAbove s
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (sSup s) : β) (sSup ((⇑e : (a : α) → β) '' s) : β)

Tactic:
e.to_galoisConnection.l_csSup_of_directedOn' hd hne hbdd

Premises used: OrderIso.to_galoisConnection, GaloisConnection.l_csSup_of_directedOn'
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : ConditionallyCompletePartialOrderSup α
inst_1 : ConditionallyCompletePartialOrderSup β
inst_2 : Nonempty ι
e : α ≃o β
f : ι → α
hd : Directed (fun (x1 x2 : α) ↦ x1 ≤ x2) f
hf : BddAbove (range f)
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (⨆ (i : ι), f i) : β) (⨆ (i : ι), (e : (a : α) → β) (f i) : β)

Tactic:
e.to_galoisConnection.l_ciSup_of_directed hd hf

Premises used: OrderIso.to_galoisConnection, GaloisConnection.l_ciSup_of_directed
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompletePartialOrderSup α
inst_1 : ConditionallyCompletePartialOrderSup β
e : α ≃o β
s : Set γ
f : γ → α
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) (f '' s)
hf : BddAbove (f '' s)
hne : s.Nonempty
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (⨆ (i : (↑s : Type u_3)), f (↑i : γ)) : β)
    (⨆ (i : (↑s : Type u_3)), (e : (a : α) → β) (f (↑i : γ)) : β)

Tactic:
e.to_galoisConnection.l_ciSup_set_of_directedOn hd hf hne

Premises used: GaloisConnection.l_ciSup_set_of_directedOn, OrderIso.to_galoisConnection
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompletePartialOrderInf α
inst_1 : ConditionallyCompletePartialOrderInf β
e : α ≃o β
s : Set α
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≥ x2) s
hne : s.Nonempty
hbdd : BddBelow s
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (⨅ (x : (↑s : Type u_1)), (e : (a : α) → β) (↑x : α) : β)

Tactic:
e.dual.map_csSup_of_directedOn hd hne hbdd

Premises used: iInf, OrderIso.map_csSup_of_directedOn, OrderIso.dual, OrderDual
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
inst : ConditionallyCompletePartialOrderInf α
inst_1 : ConditionallyCompletePartialOrderInf β
e : α ≃o β
s : Set α
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≥ x2) s
hne : s.Nonempty
hbdd : BddBelow s
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (sInf s) : β) (sInf ((⇑e : (a : α) → β) '' s) : β)

Tactic:
e.dual.map_csSup_of_directedOn' hd hne hbdd

Premises used: OrderIso.dual, OrderDual, OrderIso.map_csSup_of_directedOn'
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst : ConditionallyCompletePartialOrderInf α
inst_1 : ConditionallyCompletePartialOrderInf β
inst_2 : Nonempty ι
e : α ≃o β
f : ι → α
hd : Directed (fun (x1 x2 : α) ↦ x1 ≥ x2) f
hf : BddBelow (range f)
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (⨅ (i : ι), f i) : β) (⨅ (i : ι), (e : (a : α) → β) (f i) : β)

Tactic:
e.dual.map_ciSup_of_directed hd hf

Premises used: iInf, OrderIso.dual, OrderIso.map_ciSup_of_directed, OrderDual
-- Module: Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : ConditionallyCompletePartialOrderInf α
inst_1 : ConditionallyCompletePartialOrderInf β
e : α ≃o β
s : Set γ
f : γ → α
hd : DirectedOn (fun (x1 x2 : α) ↦ x1 ≥ x2) (f '' s)
hf : BddBelow (f '' s)
hne : s.Nonempty
⊢ Eq.{u_2 + 1} (α := β) ((e : (a : α) → β) (⨅ (i : (↑s : Type u_3)), f (↑i : γ)) : β)
    (⨅ (i : (↑s : Type u_3)), (e : (a : α) → β) (f (↑i : γ)) : β)

Tactic:
e.dual.map_ciSup_set_of_directedOn hd hf hne

Premises used: iInf, OrderIso.dual, OrderIso.map_ciSup_set_of_directedOn, OrderDual
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
h h' : LE α
c : OrderTop α
top : α
⊢ Top α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
h h' : LE α
c : OrderTop α
top : α
eq_top : top = ⊤
le_eq : ∀ (x y : α), x ≤ y ↔ x ≤ y
x : α
⊢ x ≤ ⊤

Tactic:
simp [eq_top, le_eq]
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
h h' : LE α
c : OrderBot α
bot : α
⊢ Bot α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
h h' : LE α
c : OrderBot α
bot : α
eq_bot : bot = ⊥
le_eq : ∀ (x y : α), x ≤ y ↔ x ≤ y
x : α
⊢ ⊥ ≤ x

Tactic:
simp [eq_bot, le_eq]
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
h h' : LE α
c : BoundedOrder α
top : α
⊢ Top α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
h h' : LE α
c : BoundedOrder α
top : α
eq_top : top = ⊤
bot : α
⊢ Bot α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
h h' : LE α
c : BoundedOrder α
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
le_eq : ∀ (x y : α), x ≤ y ↔ x ≤ y
x : α
⊢ x ≤ ⊤

Tactic:
simp [eq_top, le_eq]
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
h h' : LE α
c : BoundedOrder α
top : α
eq_top : top = ⊤
bot : α
eq_bot : bot = ⊥
le_eq : ∀ (x y : α), x ≤ y ↔ x ≤ y
x : α
⊢ ⊥ ≤ x

Tactic:
simp [eq_bot, le_eq]
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Lattice α
le : α → α → Prop
⊢ LE α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
⊢ Max α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
⊢ Min α

Tactic:
infer_instance
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a : α
⊢ le a a

Tactic:
simp [eq_le]
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a : α
_ : ∀ (b c : α), le a b → le b c → le a c
⊢ ∀ (b c : α), le a b → le b c → le a c

Tactic:
_
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a b : α
_ : ∀ (c : α), le a b → le b c → le a c
⊢ ∀ (c : α), le a b → le b c → le a c

Tactic:
_
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a b c_1 : α
hab : le a b
hbc : le b c_1
rw : ∀ (hab : a ≤ b) (hbc : b ≤ c_1), a ≤ c_1
⊢ le a c_1

Tactic:
rw [eq_le] at hab hbc ⊢
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a b c_1 : α
hab : a ≤ b
hbc : b ≤ c_1
⊢ a ≤ c_1

Tactic:
le_trans hab hbc

Premises used: le_trans
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a b c_1 : α
hab : a ≤ b
hbc : b ≤ c_1
⊢ a ≤ c_1

Tactic:
exact le_trans hab hbc

Premises used: le_trans
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a : α
_ : ∀ (b : α), le a b → le b a → a = b
⊢ ∀ (b : α), le a b → le b a → a = b

Tactic:
_
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a b : α
hab : le a b
hba : le b a
⊢ a ≤ b

Tactic:
simp_rw [eq_le] at hab hba
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a b : α
hab : le a b
hba : le b a
hab₁ : a ≤ b
⊢ b ≤ a

Tactic:
simp_rw [eq_le] at hab hba
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a b : α
hab : a ≤ b
hba : b ≤ a
⊢ a = b

Tactic:
le_antisymm hab hba

Premises used: le_antisymm
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a b : α
hab : a ≤ b
hba : b ≤ a
⊢ a = b

Tactic:
exact le_antisymm hab hba

Premises used: le_antisymm
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a b : α
⊢ le a (sup a b)

Tactic:
simp [eq_le, eq_sup]
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a b : α
⊢ le b (sup a b)

Tactic:
simp [eq_le, eq_sup]
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a : α
_ : ∀ (b c : α), le a c → le b c → le (sup a b) c
⊢ ∀ (b c : α), le a c → le b c → le (sup a b) c

Tactic:
_
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a b : α
_ : ∀ (c : α), le a c → le b c → le (sup a b) c
⊢ ∀ (c : α), le a c → le b c → le (sup a b) c

Tactic:
_
-- Module: Mathlib.Order.Copy
Goal:
α : Type u
c : Lattice α
le : α → α → Prop
eq_le : le = LE.le
sup : α → α → α
eq_sup : sup = max
inf : α → α → α
eq_inf : inf = min
a b c_1 : α
hac : le a c_1
hbc : le b c_1
simp_rw : ∀ (hac : a ≤ c_1) (hbc : b ≤ c_1), sup a b ≤ c_1
⊢ le (sup a b) c_1

Tactic:
simp_rw [eq_le] at hac hbc ⊢