F : Type ?u.55319
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.55331
κ : Type ?u.55334
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f✝ g : β → α
a : α
s : Finset β
t : Finset γ
f : β × γ → α
⊢ (∀ (a : β) (b : γ), a ∈ s → b ∈ t → f (a, b) ≤ sup s fun i => sup t fun i' => f (i, i')) ∧
    ∀ (b : β), b ∈ s → ∀ (b_1 : γ), b_1 ∈ t → f (b, b_1) ≤ sup (s ×ˢ t) f
F : Type ?u.55319
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.55331
κ : Type ?u.55334
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f✝ g : β → α
a : α
s : Finset β
t : Finset γ
f : β × γ → α
⊢ sup (s ×ˢ t) f = sup s fun i => sup t fun i' => f (i, i')
simp only [le_antisymm_iff, Finset.sup_le_iff, mem_product, and_imp, Prod.forall]
case refine_1
F : Type ?u.55319
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.55331
κ : Type ?u.55334
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f✝ g : β → α
a : α
s : Finset β
t : Finset γ
f : β × γ → α
b : β
c : γ
hb : b ∈ s
hc : c ∈ t
⊢ f (b, c) ≤ sup s fun i => sup t fun i' => f (i, i')

case refine_2
F : Type ?u.55319
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.55331
κ : Type ?u.55334
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f✝ g : β → α
a : α
s : Finset β
t : Finset γ
f : β × γ → α
b : β
hb : b ∈ s
c : γ
hc : c ∈ t
⊢ f (b, c) ≤ sup (s ×ˢ t) f
F : Type ?u.55319
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.55331
κ : Type ?u.55334
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f✝ g : β → α
a : α
s : Finset β
t : Finset γ
f : β × γ → α
⊢ (∀ (a : β) (b : γ), a ∈ s → b ∈ t → f (a, b) ≤ sup s fun i => sup t fun i' => f (i, i')) ∧
    ∀ (b : β), b ∈ s → ∀ (b_1 : γ), b_1 ∈ t → f (b, b_1) ≤ sup (s ×ˢ t) f
refine ⟨fun b c hb hc => ?_, fun b hb c hc => ?_⟩
case refine_1
F : Type ?u.55319
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.55331
κ : Type ?u.55334
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f✝ g : β → α
a : α
s : Finset β
t : Finset γ
f : β × γ → α
b : β
c : γ
hb : b ∈ s
hc : c ∈ t
⊢ f (b, c) ≤ sup t fun i' => f (b, i')
case refine_1
F : Type ?u.55319
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.55331
κ : Type ?u.55334
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f✝ g : β → α
a : α
s : Finset β
t : Finset γ
f : β × γ → α
b : β
c : γ
hb : b ∈ s
hc : c ∈ t
⊢ f (b, c) ≤ sup s fun i => sup t fun i' => f (i, i')
refine (le_sup hb).trans' ?_
no goals
case refine_1
F : Type ?u.55319
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.55331
κ : Type ?u.55334
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f✝ g : β → α
a : α
s : Finset β
t : Finset γ
f : β × γ → α
b : β
c : γ
hb : b ∈ s
hc : c ∈ t
⊢ f (b, c) ≤ sup t fun i' => f (b, i')
exact @le_sup _ _ _ _ _ (fun c => f (b, c)) c hc
no goals
case refine_2
F : Type ?u.55319
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.55331
κ : Type ?u.55334
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s✝ s₁ s₂ : Finset β
f✝ g : β → α
a : α
s : Finset β
t : Finset γ
f : β × γ → α
b : β
hb : b ∈ s
c : γ
hc : c ∈ t
⊢ f (b, c) ≤ sup (s ×ˢ t) f
exact le_sup <| mem_product.2 ⟨hb, hc⟩