-- Mathlib/Data/Set/Pairwise/Lattice.lean
theorem PairwiseDisjoint.prod_left {f : ι × ι' → α}
    (hs : s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i'))
    (ht : t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')) :
    (s ×ˢ t : Set (ι × ι')).PairwiseDisjoint f

Proof state:
case mk.mk.inr
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j : ι
j' : ι'
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
h : (i, i') ≠ (j, j')
hij : i ≠ j
⊢ (Disjoint on f) (i, i') (j, j')

Tactic:
refine (hs hi.1 hj.1 hij).mono ?_ ?_

Result:
case mk.mk.inr.refine_1
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j : ι
j' : ι'
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
h : (i, i') ≠ (j, j')
hij : i ≠ j
⊢ f (i, i') ≤ (fun i => ⨆ i' ∈ t, f (i, i')) (i, i').1

case mk.mk.inr.refine_2
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j : ι
j' : ι'
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
h : (i, i') ≠ (j, j')
hij : i ≠ j
⊢ f (j, j') ≤ (fun i => ⨆ i' ∈ t, f (i, i')) (j, j').1

Proof state:
case mk.mk.inl.refine_2
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j' : ι'
hj : (i, j').1 ∈ s ∧ (i, j').2 ∈ t
h : (i, i') ≠ (i, j')
⊢ f (i, j') ≤ (fun i' => ⨆ i ∈ s, f (i, i')) (i, j').2

Tactic:
convert le_iSup₂ (α := α) i hj.1

Result:
case h.e'_3
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j' : ι'
hj : (i, j').1 ∈ s ∧ (i, j').2 ∈ t
h : (i, i') ≠ (i, j')
⊢ f (i, j') = f (i, (i, j').2)

Proof state:
case h.e'_3
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j : ι
j' : ι'
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
h : (i, i') ≠ (j, j')
hij : i ≠ j
⊢ f (j, j') = f ((j, j').1, j')

Tactic:
rfl

Result:
no goals

Proof state:
case h.e'_3
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j' : ι'
hj : (i, j').1 ∈ s ∧ (i, j').2 ∈ t
h : (i, i') ≠ (i, j')
⊢ f (i, j') = f (i, (i, j').2)

Tactic:
rfl

Result:
no goals

Proof state:
case h.e'_3
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j : ι
j' : ι'
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
h : (i, i') ≠ (j, j')
hij : i ≠ j
⊢ f (i, i') = f ((i, i').1, i')

Tactic:
rfl

Result:
no goals

Proof state:
case mk.mk.inr.refine_1
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j : ι
j' : ι'
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
h : (i, i') ≠ (j, j')
hij : i ≠ j
⊢ f (i, i') ≤ (fun i => ⨆ i' ∈ t, f (i, i')) (i, i').1

Tactic:
convert le_iSup₂ (α := α) i' hi.2

Result:
case h.e'_3
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j : ι
j' : ι'
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
h : (i, i') ≠ (j, j')
hij : i ≠ j
⊢ f (i, i') = f ((i, i').1, i')

Proof state:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')
⊢ (s ×ˢ t).PairwiseDisjoint f

Tactic:
rintro ⟨i, i'⟩ hi ⟨j, j'⟩ hj h

Result:
case mk.mk
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i') ∈ s ×ˢ t
j : ι
j' : ι'
hj : (j, j') ∈ s ×ˢ t
h : (i, i') ≠ (j, j')
⊢ (Disjoint on f) (i, i') (j, j')

Proof state:
case mk.mk
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j : ι
j' : ι'
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
h : (i, i') ≠ (j, j')
⊢ (Disjoint on f) (i, i') (j, j')

Tactic:
obtain rfl | hij := eq_or_ne i j

Result:
case mk.mk.inl
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j' : ι'
hj : (i, j').1 ∈ s ∧ (i, j').2 ∈ t
h : (i, i') ≠ (i, j')
⊢ (Disjoint on f) (i, i') (i, j')

case mk.mk.inr
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j : ι
j' : ι'
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
h : (i, i') ≠ (j, j')
hij : i ≠ j
⊢ (Disjoint on f) (i, i') (j, j')

Proof state:
case h.e'_3
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j' : ι'
hj : (i, j').1 ∈ s ∧ (i, j').2 ∈ t
h : (i, i') ≠ (i, j')
⊢ f (i, i') = f (i, (i, i').2)

Tactic:
rfl

Result:
no goals

Proof state:
case mk.mk.inl.refine_1
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j' : ι'
hj : (i, j').1 ∈ s ∧ (i, j').2 ∈ t
h : (i, i') ≠ (i, j')
⊢ f (i, i') ≤ (fun i' => ⨆ i ∈ s, f (i, i')) (i, i').2

Tactic:
convert le_iSup₂ (α := α) i hi.1

Result:
case h.e'_3
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι
t : Set ι'
f : ι × ι' → α
hs : s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i')
ht : t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
j' : ι'
hj : (i, j').1 ∈ s ∧ (i, j').2 ∈ t
h : (i, i') ≠ (i, j')
⊢ f (i, i') = f (i, (i, i').2)