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

Proof state:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
⊢ (s.product t).SupIndep f ↔
    (s.SupIndep fun i => t.sup fun i' => f (i, i')) ∧ t.SupIndep fun i' => s.sup fun i => f (i, i')

Tactic:
refine ⟨?_, fun h => h.1.product h.2⟩

Result:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
⊢ (s.product t).SupIndep f →
    (s.SupIndep fun i => t.sup fun i' => f (i, i')) ∧ t.SupIndep fun i' => s.sup fun i => f (i, i')

Proof state:
case refine_2
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
h : (↑(s.product t)).PairwiseDisjoint f
i : ι'
hi : i ∈ ↑t
j : ι'
hj : j ∈ ↑t
hij : i ≠ j
i' : ι
hi' : i' ∈ s
j' : ι
hj' : j' ∈ s
⊢ Disjoint (f (i', i)) (f (j', j))

Tactic:
exact h (mk_mem_product hi' hi) (mk_mem_product hj' hj) (ne_of_apply_ne Prod.snd hij)

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
⊢ (s.product t).SupIndep f →
    (s.SupIndep fun i => t.sup fun i' => f (i, i')) ∧ t.SupIndep fun i' => s.sup fun i => f (i, i')

Tactic:
simp_rw [supIndep_iff_pairwiseDisjoint]

Result:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
⊢ (↑(s.product t)).PairwiseDisjoint f →
    ((↑s).PairwiseDisjoint fun i => t.sup fun i' => f (i, i')) ∧
      (↑t).PairwiseDisjoint fun i' => s.sup fun i => f (i, i')

Proof state:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
⊢ (↑(s.product t)).PairwiseDisjoint f →
    ((↑s).PairwiseDisjoint fun i => t.sup fun i' => f (i, i')) ∧
      (↑t).PairwiseDisjoint fun i' => s.sup fun i => f (i, i')

Tactic:
refine fun h => ⟨fun i hi j hj hij => ?_, fun i hi j hj hij => ?_⟩ <;>
    simp_rw [Finset.disjoint_sup_left, Finset.disjoint_sup_right] <;>
  intro i' hi' j' hj'

Result:
case refine_1
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
h : (↑(s.product t)).PairwiseDisjoint f
i : ι
hi : i ∈ ↑s
j : ι
hj : j ∈ ↑s
hij : i ≠ j
i' : ι'
hi' : i' ∈ t
j' : ι'
hj' : j' ∈ t
⊢ Disjoint (f (i, i')) (f (j, j'))

case refine_2
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
h : (↑(s.product t)).PairwiseDisjoint f
i : ι'
hi : i ∈ ↑t
j : ι'
hj : j ∈ ↑t
hij : i ≠ j
i' : ι
hi' : i' ∈ s
j' : ι
hj' : j' ∈ s
⊢ Disjoint (f (i', i)) (f (j', j))

Proof state:
case refine_1
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
h : (↑(s.product t)).PairwiseDisjoint f
i : ι
hi : i ∈ ↑s
j : ι
hj : j ∈ ↑s
hij : i ≠ j
i' : ι'
hi' : i' ∈ t
j' : ι'
hj' : j' ∈ t
⊢ Disjoint (f (i, i')) (f (j, j'))

Tactic:
exact h (mk_mem_product hi hi') (mk_mem_product hj hj') (ne_of_apply_ne Prod.fst hij)

Result:
no goals