ι : Type u_2
α : ι → Type u_3
β : Type u_1
s s₁ s₂ : Finset ι
t t₁ t₂ : (i : ι) → Finset (α i)
f : (i : ι) × α i → β
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
⊢ (∀ (a : ι) (b : α a),
      a ∈ s → b ∈ t a → f { fst := a, snd := b } ≤ sup s fun i => sup (t i) fun b => f { fst := i, snd := b }) ∧
    ∀ (b : ι), b ∈ s → ∀ (b_1 : α b), b_1 ∈ t b → f { fst := b, snd := b_1 } ≤ sup (Finset.sigma s t) f
ι : Type u_2
α : ι → Type u_3
β : Type u_1
s s₁ s₂ : Finset ι
t t₁ t₂ : (i : ι) → Finset (α i)
f : (i : ι) × α i → β
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
⊢ sup (Finset.sigma s t) f = sup s fun i => sup (t i) fun b => f { fst := i, snd := b }
simp only [le_antisymm_iff, Finset.sup_le_iff, mem_sigma, and_imp, Sigma.forall]
no goals
ι : Type u_2
α : ι → Type u_3
β : Type u_1
s s₁ s₂ : Finset ι
t t₁ t₂ : (i : ι) → Finset (α i)
f : (i : ι) × α i → β
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
⊢ (∀ (a : ι) (b : α a),
      a ∈ s → b ∈ t a → f { fst := a, snd := b } ≤ sup s fun i => sup (t i) fun b => f { fst := i, snd := b }) ∧
    ∀ (b : ι), b ∈ s → ∀ (b_1 : α b), b_1 ∈ t b → f { fst := b, snd := b_1 } ≤ sup (Finset.sigma s t) f
exact
  ⟨fun i a hi ha => (le_sup hi).trans' <| le_sup (f := fun a => f ⟨i, a⟩) ha, fun i hi a ha =>
    le_sup <| mem_sigma.2 ⟨hi, ha⟩⟩