-- Mathlib/Order/SupIndep.lean
theorem SupIndep.sigma {β : ι → Type*} {s : Finset ι} {g : ∀ i, Finset (β i)}
    {f : Sigma β → α} (hs : s.SupIndep fun i => (g i).sup fun b => f ⟨i, b⟩)
    (hg : ∀ i ∈ s, (g i).SupIndep fun b => f ⟨i, b⟩) : (s.sigma g).SupIndep f

Proof state:
case mk.mk.inr
α : Type u_1
ι : Type u_3
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
hs : s.SupIndep fun i => (g i).sup fun b => f ⟨i, b⟩
hg : ∀ i ∈ s, (g i).SupIndep fun b => f ⟨i, b⟩
t : Finset ((i : ι) × β i)
ht : t ⊆ s.sigma g
i : ι
b : β i
hi : ⟨i, b⟩.fst ∈ s ∧ ⟨i, b⟩.snd ∈ g ⟨i, b⟩.fst
hit : ⟨i, b⟩ ∉ t
j : ι
c : β j
hbc : ⟨i, b⟩ ≠ ⟨j, c⟩
hj : ⟨j, c⟩.fst ∈ s ∧ ⟨j, c⟩.snd ∈ g ⟨j, c⟩.fst
hij : i ≠ j
⊢ Disjoint (f ⟨i, b⟩) (f ⟨j, c⟩)

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

Result:
case mk.mk.inr.refine_1
α : Type u_1
ι : Type u_3
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
hs : s.SupIndep fun i => (g i).sup fun b => f ⟨i, b⟩
hg : ∀ i ∈ s, (g i).SupIndep fun b => f ⟨i, b⟩
t : Finset ((i : ι) × β i)
ht : t ⊆ s.sigma g
i : ι
b : β i
hi : ⟨i, b⟩.fst ∈ s ∧ ⟨i, b⟩.snd ∈ g ⟨i, b⟩.fst
hit : ⟨i, b⟩ ∉ t
j : ι
c : β j
hbc : ⟨i, b⟩ ≠ ⟨j, c⟩
hj : ⟨j, c⟩.fst ∈ s ∧ ⟨j, c⟩.snd ∈ g ⟨j, c⟩.fst
hij : i ≠ j
⊢ f ⟨i, b⟩ ≤ (fun i => (g i).sup fun b => f ⟨i, b⟩) ⟨i, b⟩.fst

case mk.mk.inr.refine_2
α : Type u_1
ι : Type u_3
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
hs : s.SupIndep fun i => (g i).sup fun b => f ⟨i, b⟩
hg : ∀ i ∈ s, (g i).SupIndep fun b => f ⟨i, b⟩
t : Finset ((i : ι) × β i)
ht : t ⊆ s.sigma g
i : ι
b : β i
hi : ⟨i, b⟩.fst ∈ s ∧ ⟨i, b⟩.snd ∈ g ⟨i, b⟩.fst
hit : ⟨i, b⟩ ∉ t
j : ι
c : β j
hbc : ⟨i, b⟩ ≠ ⟨j, c⟩
hj : ⟨j, c⟩.fst ∈ s ∧ ⟨j, c⟩.snd ∈ g ⟨j, c⟩.fst
hij : i ≠ j
⊢ f ⟨j, c⟩ ≤ (fun i => (g i).sup fun b => f ⟨i, b⟩) ⟨j, c⟩.fst

Proof state:
case mk.mk.inl
α : Type u_1
ι : Type u_3
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
hs : s.SupIndep fun i => (g i).sup fun b => f ⟨i, b⟩
hg : ∀ i ∈ s, (g i).SupIndep fun b => f ⟨i, b⟩
t : Finset ((i : ι) × β i)
ht : t ⊆ s.sigma g
i : ι
b : β i
hi : ⟨i, b⟩.fst ∈ s ∧ ⟨i, b⟩.snd ∈ g ⟨i, b⟩.fst
hit : ⟨i, b⟩ ∉ t
c : β i
hbc : ⟨i, b⟩ ≠ ⟨i, c⟩
hj : ⟨i, c⟩.fst ∈ s ∧ ⟨i, c⟩.snd ∈ g ⟨i, c⟩.fst
⊢ Disjoint (f ⟨i, b⟩) (f ⟨i, c⟩)

Tactic:
exact (hg _ hj.1).pairwiseDisjoint hi.2 hj.2 (sigma_mk_injective.ne_iff.1 hbc)

Result:
no goals

Proof state:
case mk
α : Type u_1
ι : Type u_3
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
hs : s.SupIndep fun i => (g i).sup fun b => f ⟨i, b⟩
hg : ∀ i ∈ s, (g i).SupIndep fun b => f ⟨i, b⟩
t : Finset ((i : ι) × β i)
ht : t ⊆ s.sigma g
i : ι
b : β i
hi : ⟨i, b⟩ ∈ s.sigma g
hit : ⟨i, b⟩ ∉ t
⊢ Disjoint (f ⟨i, b⟩) (t.sup f)

Tactic:
rw [Finset.disjoint_sup_right]

Result:
case mk
α : Type u_1
ι : Type u_3
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
hs : s.SupIndep fun i => (g i).sup fun b => f ⟨i, b⟩
hg : ∀ i ∈ s, (g i).SupIndep fun b => f ⟨i, b⟩
t : Finset ((i : ι) × β i)
ht : t ⊆ s.sigma g
i : ι
b : β i
hi : ⟨i, b⟩ ∈ s.sigma g
hit : ⟨i, b⟩ ∉ t
⊢ ∀ ⦃i_1 : (i : ι) × β i⦄, i_1 ∈ t → Disjoint (f ⟨i, b⟩) (f i_1)

Proof state:
case h.e'_3
α : Type u_1
ι : Type u_3
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
hs : s.SupIndep fun i => (g i).sup fun b => f ⟨i, b⟩
hg : ∀ i ∈ s, (g i).SupIndep fun b => f ⟨i, b⟩
t : Finset ((i : ι) × β i)
ht : t ⊆ s.sigma g
i : ι
b : β i
hi : ⟨i, b⟩.fst ∈ s ∧ ⟨i, b⟩.snd ∈ g ⟨i, b⟩.fst
hit : ⟨i, b⟩ ∉ t
j : ι
c : β j
hbc : ⟨i, b⟩ ≠ ⟨j, c⟩
hj : ⟨j, c⟩.fst ∈ s ∧ ⟨j, c⟩.snd ∈ g ⟨j, c⟩.fst
hij : i ≠ j
⊢ f ⟨j, c⟩ = f ⟨⟨j, c⟩.fst, ⟨j, c⟩.snd⟩

Tactic:
simp

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
ι : Type u_3
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
hs : s.SupIndep fun i => (g i).sup fun b => f ⟨i, b⟩
hg : ∀ i ∈ s, (g i).SupIndep fun b => f ⟨i, b⟩
t : Finset ((i : ι) × β i)
ht : t ⊆ s.sigma g
i : ι
b : β i
hi : ⟨i, b⟩ ∈ s.sigma g
hit : ⟨i, b⟩ ∉ t
j : ι
c : β j
hbc : ⟨i, b⟩ ≠ ⟨j, c⟩
hj : ⟨j, c⟩ ∈ s.sigma g
⊢ Disjoint (f ⟨i, b⟩) (f ⟨j, c⟩)

Tactic:
rw [mem_sigma] at hi hj

Result:
case mk.mk
α : Type u_1
ι : Type u_3
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
hs : s.SupIndep fun i => (g i).sup fun b => f ⟨i, b⟩
hg : ∀ i ∈ s, (g i).SupIndep fun b => f ⟨i, b⟩
t : Finset ((i : ι) × β i)
ht : t ⊆ s.sigma g
i : ι
b : β i
hi : ⟨i, b⟩.fst ∈ s ∧ ⟨i, b⟩.snd ∈ g ⟨i, b⟩.fst
hit : ⟨i, b⟩ ∉ t
j : ι
c : β j
hbc : ⟨i, b⟩ ≠ ⟨j, c⟩
hj : ⟨j, c⟩.fst ∈ s ∧ ⟨j, c⟩.snd ∈ g ⟨j, c⟩.fst
⊢ Disjoint (f ⟨i, b⟩) (f ⟨j, c⟩)

Proof state:
case mk
α : Type u_1
ι : Type u_3
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
hs : s.SupIndep fun i => (g i).sup fun b => f ⟨i, b⟩
hg : ∀ i ∈ s, (g i).SupIndep fun b => f ⟨i, b⟩
t : Finset ((i : ι) × β i)
ht : t ⊆ s.sigma g
i : ι
b : β i
hi : ⟨i, b⟩ ∈ s.sigma g
hit : ⟨i, b⟩ ∉ t
⊢ ∀ ⦃i_1 : (i : ι) × β i⦄, i_1 ∈ t → Disjoint (f ⟨i, b⟩) (f i_1)

Tactic:
rintro ⟨j, c⟩ hj

Result:
case mk.mk
α : Type u_1
ι : Type u_3
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
hs : s.SupIndep fun i => (g i).sup fun b => f ⟨i, b⟩
hg : ∀ i ∈ s, (g i).SupIndep fun b => f ⟨i, b⟩
t : Finset ((i : ι) × β i)
ht : t ⊆ s.sigma g
i : ι
b : β i
hi : ⟨i, b⟩ ∈ s.sigma g
hit : ⟨i, b⟩ ∉ t
j : ι
c : β j
hj : ⟨j, c⟩ ∈ t
⊢ Disjoint (f ⟨i, b⟩) (f ⟨j, c⟩)

Proof state:
case h.e'_3
α : Type u_1
ι : Type u_3
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
β : ι → Type u_5
s : Finset ι
g : (i : ι) → Finset (β i)
f : Sigma β → α
hs : s.SupIndep fun i => (g i).sup fun b => f ⟨i, b⟩
hg : ∀ i ∈ s, (g i).SupIndep fun b => f ⟨i, b⟩
t : Finset ((i : ι) × β i)
ht : t ⊆ s.sigma g
i : ι
b : β i
hi : ⟨i, b⟩.fst ∈ s ∧ ⟨i, b⟩.snd ∈ g ⟨i, b⟩.fst
hit : ⟨i, b⟩ ∉ t
j : ι
c : β j
hbc : ⟨i, b⟩ ≠ ⟨j, c⟩
hj : ⟨j, c⟩.fst ∈ s ∧ ⟨j, c⟩.snd ∈ g ⟨j, c⟩.fst
hij : i ≠ j
⊢ f ⟨i, b⟩ = f ⟨⟨i, b⟩.fst, ⟨i, b⟩.snd⟩

Tactic:
simp

Result:
no goals