[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : PartialOrder β
f g : C(α, β)
x✝ : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : PartialOrder β
g : C(α, β)
toFun✝ : α → β
continuous_toFun✝ : Continuous toFun✝
x✝ : (fun f => f.toFun) (mk toFun✝) = (fun f => f.toFun) g
⊢ mk toFun✝ = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : PartialOrder β
toFun✝¹ : α → β
continuous_toFun✝¹ : Continuous toFun✝¹
toFun✝ : α → β
continuous_toFun✝ : Continuous toFun✝
x✝ : (fun f => f.toFun) (mk toFun✝¹) = (fun f => f.toFun) (mk toFun✝)
⊢ mk toFun✝¹ = mk toFun✝
[PROOFSTEP]
congr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
src✝¹ : PartialOrder C(α, β) := partialOrder
src✝ : Sup C(α, β) := sup
f g : C(α, β)
⊢ ∀ (a : α), ↑f a ≤ ↑(f ⊔ g) a
[PROOFSTEP]
simp [le_refl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
src✝¹ : PartialOrder C(α, β) := partialOrder
src✝ : Sup C(α, β) := sup
f g : C(α, β)
⊢ ∀ (a : α), ↑g a ≤ ↑(f ⊔ g) a
[PROOFSTEP]
simp [le_refl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
src✝¹ : PartialOrder C(α, β) := partialOrder
src✝ : Sup C(α, β) := sup
f₁ f₂ g : C(α, β)
w₁ : f₁ ≤ g
w₂ : f₂ ≤ g
a : α
⊢ ↑(f₁ ⊔ f₂) a ≤ ↑g a
[PROOFSTEP]
simp [le_def.mp w₁ a, le_def.mp w₂ a]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
src✝¹ : PartialOrder C(α, β) := partialOrder
src✝ : Inf C(α, β) := inf
f g : C(α, β)
⊢ ∀ (a : α), ↑(f ⊓ g) a ≤ ↑f a
[PROOFSTEP]
simp [le_refl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
src✝¹ : PartialOrder C(α, β) := partialOrder
src✝ : Inf C(α, β) := inf
f g : C(α, β)
⊢ ∀ (a : α), ↑(f ⊓ g) a ≤ ↑g a
[PROOFSTEP]
simp [le_refl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
src✝¹ : PartialOrder C(α, β) := partialOrder
src✝ : Inf C(α, β) := inf
f₁ f₂ g : C(α, β)
w₁ : f₁ ≤ f₂
w₂ : f₁ ≤ g
a : α
⊢ ↑f₁ a ≤ ↑(f₂ ⊓ g) a
[PROOFSTEP]
simp [le_def.mp w₁ a, le_def.mp w₂ a]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LinearOrder γ
inst✝ : OrderClosedTopology γ
ι : Type u_4
s : Finset ι
H : Finset.Nonempty s
f : ι → C(β, γ)
⊢ ↑(Finset.sup' s H f) = Finset.sup' s H fun a => ↑(f a)
[PROOFSTEP]
ext
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : LinearOrder γ
inst✝ : OrderClosedTopology γ
ι : Type u_4
s : Finset ι
H : Finset.Nonempty s
f : ι → C(β, γ)
x✝ : β
⊢ ↑(Finset.sup' s H f) x✝ = Finset.sup' s H (fun a => ↑(f a)) x✝
[PROOFSTEP]
simp [sup'_apply]
