F : Type ?u.262044
α : Type u_2
β : Type u_1
γ : Type ?u.262053
ι : Type ?u.262056
κ : Type ?u.262059
inst✝ : SemilatticeSup α
f✝ : β → α
t : Finset β
f g : β → α
H : Finset.Nonempty t
h₂ : ∀ (x : β), x ∈ t → f x = g x
⊢ sup' t H f = sup' t (_ : Finset.Nonempty t) g
F : Type ?u.262044
α : Type u_2
β : Type u_1
γ : Type ?u.262053
ι : Type ?u.262056
κ : Type ?u.262059
inst✝ : SemilatticeSup α
s : Finset β
H : Finset.Nonempty s
f✝ : β → α
t : Finset β
f g : β → α
h₁ : s = t
h₂ : ∀ (x : β), x ∈ s → f x = g x
⊢ sup' s H f = sup' t (_ : Finset.Nonempty t) g
subst s
F : Type ?u.262044
α : Type u_2
β : Type u_1
γ : Type ?u.262053
ι : Type ?u.262056
κ : Type ?u.262059
inst✝ : SemilatticeSup α
f✝ : β → α
t : Finset β
f g : β → α
H : Finset.Nonempty t
h₂ : ∀ (x : β), x ∈ t → f x = g x
c : α
⊢ sup' t H f ≤ c ↔ sup' t (_ : Finset.Nonempty t) g ≤ c
F : Type ?u.262044
α : Type u_2
β : Type u_1
γ : Type ?u.262053
ι : Type ?u.262056
κ : Type ?u.262059
inst✝ : SemilatticeSup α
f✝ : β → α
t : Finset β
f g : β → α
H : Finset.Nonempty t
h₂ : ∀ (x : β), x ∈ t → f x = g x
⊢ sup' t H f = sup' t (_ : Finset.Nonempty t) g
refine' eq_of_forall_ge_iff fun c => _
no goals
F : Type ?u.262044
α : Type u_2
β : Type u_1
γ : Type ?u.262053
ι : Type ?u.262056
κ : Type ?u.262059
inst✝ : SemilatticeSup α
f✝ : β → α
t : Finset β
f g : β → α
H : Finset.Nonempty t
h₂ : ∀ (x : β), x ∈ t → f x = g x
c : α
⊢ sup' t H f ≤ c ↔ sup' t (_ : Finset.Nonempty t) g ≤ c
simp (config := { contextual := true }) only [sup'_le_iff, h₂]