F : Type ?u.65870
α : Type u_1
β : Type u_2
γ : Type ?u.65879
ι : Type ?u.65882
κ : Type ?u.65885
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f✝ g : β → α
a : α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
this : SemilatticeSup { x // P x } := Subtype.semilatticeSup Psup
⊢ ↑(sup t f) = sup t fun x => ↑(f x)
F : Type ?u.65870
α : Type u_1
β : Type u_2
γ : Type ?u.65879
ι : Type ?u.65882
κ : Type ?u.65885
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f✝ g : β → α
a : α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
⊢ ↑(sup t f) = sup t fun x => ↑(f x)
letI := Subtype.semilatticeSup Psup
F : Type ?u.65870
α : Type u_1
β : Type u_2
γ : Type ?u.65879
ι : Type ?u.65882
κ : Type ?u.65885
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f✝ g : β → α
a : α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
this✝ : SemilatticeSup { x // P x } := Subtype.semilatticeSup Psup
this : OrderBot { x // P x } := Subtype.orderBot Pbot
⊢ ↑(sup t f) = sup t fun x => ↑(f x)
F : Type ?u.65870
α : Type u_1
β : Type u_2
γ : Type ?u.65879
ι : Type ?u.65882
κ : Type ?u.65885
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f✝ g : β → α
a : α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
this : SemilatticeSup { x // P x } := Subtype.semilatticeSup Psup
⊢ ↑(sup t f) = sup t fun x => ↑(f x)
letI := Subtype.orderBot Pbot
no goals
F : Type ?u.65870
α : Type u_1
β : Type u_2
γ : Type ?u.65879
ι : Type ?u.65882
κ : Type ?u.65885
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s s₁ s₂ : Finset β
f✝ g : β → α
a : α
P : α → Prop
Pbot : P ⊥
Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)
t : Finset β
f : β → { x // P x }
this✝ : SemilatticeSup { x // P x } := Subtype.semilatticeSup Psup
this : OrderBot { x // P x } := Subtype.orderBot Pbot
⊢ ↑(sup t f) = sup t fun x => ↑(f x)
apply comp_sup_eq_sup_comp Subtype.val <;> intros <;> rfl