-- Mathlib/Order/SupIndep.lean
theorem SupIndep.product {s : Finset ι} {t : Finset ι'} {f : ι × ι' → α}
    (hs : s.SupIndep fun i => t.sup fun i' => f (i, i'))
    (ht : t.SupIndep fun i' => s.sup fun i => f (i, i')) : (s ×ˢ t).SupIndep f

Proof state:
case mk.mk
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : s.SupIndep fun i => t.sup fun i' => f (i, i')
ht : t.SupIndep fun i' => s.sup fun i => f (i, i')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
hiu : (i, i') ∉ u
j : ι
j' : ι'
hij : (i, i') ≠ (j, j')
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
⊢ Disjoint (f (i, i')) (f (j, j'))

Tactic:
obtain rfl | hij := eq_or_ne i j

Result:
case mk.mk.inl
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : s.SupIndep fun i => t.sup fun i' => f (i, i')
ht : t.SupIndep fun i' => s.sup fun i => f (i, i')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
hiu : (i, i') ∉ u
j' : ι'
hij : (i, i') ≠ (i, j')
hj : (i, j').1 ∈ s ∧ (i, j').2 ∈ t
⊢ Disjoint (f (i, i')) (f (i, j'))

case mk.mk.inr
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : s.SupIndep fun i => t.sup fun i' => f (i, i')
ht : t.SupIndep fun i' => s.sup fun i => f (i, i')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
hiu : (i, i') ∉ u
j : ι
j' : ι'
hij✝ : (i, i') ≠ (j, j')
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
hij : i ≠ j
⊢ Disjoint (f (i, i')) (f (j, j'))

Proof state:
case h.e'_3
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : s.SupIndep fun i => t.sup fun i' => f (i, i')
ht : t.SupIndep fun i' => s.sup fun i => f (i, i')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
hiu : (i, i') ∉ u
j' : ι'
hij : (i, i') ≠ (i, j')
hj : (i, j').1 ∈ s ∧ (i, j').2 ∈ t
⊢ f (i, j') = f ((i, j').1, (i, j').2)

Tactic:
simp

Result:
no goals

Proof state:
case mk
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : s.SupIndep fun i => t.sup fun i' => f (i, i')
ht : t.SupIndep fun i' => s.sup fun i => f (i, i')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i') ∈ s ×ˢ t
hiu : (i, i') ∉ u
⊢ Disjoint (f (i, i')) (u.sup f)

Tactic:
rw [Finset.disjoint_sup_right]

Result:
case mk
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : s.SupIndep fun i => t.sup fun i' => f (i, i')
ht : t.SupIndep fun i' => s.sup fun i => f (i, i')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i') ∈ s ×ˢ t
hiu : (i, i') ∉ u
⊢ ∀ ⦃i_1 : ι × ι'⦄, i_1 ∈ u → Disjoint (f (i, i')) (f i_1)

Proof state:
case mk.mk.inl.refine_2
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : s.SupIndep fun i => t.sup fun i' => f (i, i')
ht : t.SupIndep fun i' => s.sup fun i => f (i, i')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
hiu : (i, i') ∉ u
j' : ι'
hij : (i, i') ≠ (i, j')
hj : (i, j').1 ∈ s ∧ (i, j').2 ∈ t
⊢ f (i, j') ≤ (fun i' => s.sup fun i => f (i, i')) (i, j').2

Tactic:
convert le_sup (α := α) hj.1

Result:
case h.e'_3
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : s.SupIndep fun i => t.sup fun i' => f (i, i')
ht : t.SupIndep fun i' => s.sup fun i => f (i, i')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
hiu : (i, i') ∉ u
j' : ι'
hij : (i, i') ≠ (i, j')
hj : (i, j').1 ∈ s ∧ (i, j').2 ∈ t
⊢ f (i, j') = f ((i, j').1, (i, j').2)

Proof state:
case mk.mk
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : s.SupIndep fun i => t.sup fun i' => f (i, i')
ht : t.SupIndep fun i' => s.sup fun i => f (i, i')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i') ∈ s ×ˢ t
hiu : (i, i') ∉ u
j : ι
j' : ι'
hj : (j, j') ∈ u
hij : (i, i') ≠ (j, j')
⊢ Disjoint (f (i, i')) (f (j, j'))

Tactic:
replace hj := hu hj

Result:
case mk.mk
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : s.SupIndep fun i => t.sup fun i' => f (i, i')
ht : t.SupIndep fun i' => s.sup fun i => f (i, i')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i') ∈ s ×ˢ t
hiu : (i, i') ∉ u
j : ι
j' : ι'
hij : (i, i') ≠ (j, j')
hj : (j, j') ∈ s ×ˢ t
⊢ Disjoint (f (i, i')) (f (j, j'))

Proof state:
case h.e'_3
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : s.SupIndep fun i => t.sup fun i' => f (i, i')
ht : t.SupIndep fun i' => s.sup fun i => f (i, i')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
hiu : (i, i') ∉ u
j : ι
j' : ι'
hij✝ : (i, i') ≠ (j, j')
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
hij : i ≠ j
⊢ f (j, j') = f ((j, j').1, (j, j').2)

Tactic:
simp

Result:
no goals

Proof state:
case mk.mk.inr.refine_2
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : s.SupIndep fun i => t.sup fun i' => f (i, i')
ht : t.SupIndep fun i' => s.sup fun i => f (i, i')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
hiu : (i, i') ∉ u
j : ι
j' : ι'
hij✝ : (i, i') ≠ (j, j')
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
hij : i ≠ j
⊢ f (j, j') ≤ (fun i => t.sup fun i' => f (i, i')) (j, j').1

Tactic:
convert le_sup (α := α) hj.2

Result:
case h.e'_3
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : s.SupIndep fun i => t.sup fun i' => f (i, i')
ht : t.SupIndep fun i' => s.sup fun i => f (i, i')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
hiu : (i, i') ∉ u
j : ι
j' : ι'
hij✝ : (i, i') ≠ (j, j')
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
hij : i ≠ j
⊢ f (j, j') = f ((j, j').1, (j, j').2)

Proof state:
case mk.mk.inr
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : s.SupIndep fun i => t.sup fun i' => f (i, i')
ht : t.SupIndep fun i' => s.sup fun i => f (i, i')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
hiu : (i, i') ∉ u
j : ι
j' : ι'
hij✝ : (i, i') ≠ (j, j')
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
hij : i ≠ j
⊢ Disjoint (f (i, i')) (f (j, j'))

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

Result:
case mk.mk.inr.refine_1
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : s.SupIndep fun i => t.sup fun i' => f (i, i')
ht : t.SupIndep fun i' => s.sup fun i => f (i, i')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
hiu : (i, i') ∉ u
j : ι
j' : ι'
hij✝ : (i, i') ≠ (j, j')
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
hij : i ≠ j
⊢ f (i, i') ≤ (fun i => t.sup fun i' => f (i, i')) (i, i').1

case mk.mk.inr.refine_2
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : s.SupIndep fun i => t.sup fun i' => f (i, i')
ht : t.SupIndep fun i' => s.sup fun i => f (i, i')
u : Finset (ι × ι')
hu : u ⊆ s ×ˢ t
i : ι
i' : ι'
hi : (i, i').1 ∈ s ∧ (i, i').2 ∈ t
hiu : (i, i') ∉ u
j : ι
j' : ι'
hij✝ : (i, i') ≠ (j, j')
hj : (j, j').1 ∈ s ∧ (j, j').2 ∈ t
hij : i ≠ j
⊢ f (j, j') ≤ (fun i => t.sup fun i' => f (i, i')) (j, j').1