-- Mathlib/Data/Set/Pairwise/Lattice.lean
theorem PairwiseDisjoint.biUnion {s : Set ι'} {g : ι' → Set ι} {f : ι → α}
    (hs : s.PairwiseDisjoint fun i' : ι' => ⨆ i ∈ g i', f i)
    (hg : ∀ i ∈ s, (g i).PairwiseDisjoint f) : (⋃ i ∈ s, g i).PairwiseDisjoint f

Proof state:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι'
g : ι' → Set ι
f : ι → α
hs : s.PairwiseDisjoint fun i' => ⨆ i ∈ g i', f i
hg : ∀ i ∈ s, (g i).PairwiseDisjoint f
a b : ι
hab : a ≠ b
ha : ∃ i, ∃ (_ : i ∈ s), a ∈ g i
hb : ∃ i, ∃ (_ : i ∈ s), b ∈ g i
⊢ (Disjoint on f) a b

Tactic:
obtain ⟨c, hc, ha⟩ := ha

Result:
case intro.intro
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι'
g : ι' → Set ι
f : ι → α
hs : s.PairwiseDisjoint fun i' => ⨆ i ∈ g i', f i
hg : ∀ i ∈ s, (g i).PairwiseDisjoint f
a b : ι
hab : a ≠ b
hb : ∃ i, ∃ (_ : i ∈ s), b ∈ g i
c : ι'
hc : c ∈ s
ha : a ∈ g c
⊢ (Disjoint on f) a b

Proof state:
case intro.intro.intro.intro.inr
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι'
g : ι' → Set ι
f : ι → α
hs : s.PairwiseDisjoint fun i' => ⨆ i ∈ g i', f i
hg : ∀ i ∈ s, (g i).PairwiseDisjoint f
a b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
ha : a ∈ g c
d : ι'
hd : d ∈ s
hb : b ∈ g d
hcd : g c ≠ g d
⊢ (Disjoint on f) a b

Tactic:
exact (hs hc hd <| ne_of_apply_ne _ hcd).mono
  (le_iSup₂ (f := fun i (_ : i ∈ g c) => f i) a ha)
  (le_iSup₂ (f := fun i (_ : i ∈ g d) => f i) b hb)

Result:
no goals

Proof state:
case intro.intro.intro.intro.inl
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι'
g : ι' → Set ι
f : ι → α
hs : s.PairwiseDisjoint fun i' => ⨆ i ∈ g i', f i
hg : ∀ i ∈ s, (g i).PairwiseDisjoint f
a b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
ha : a ∈ g c
d : ι'
hd : d ∈ s
hb : b ∈ g d
hcd : g c = g d
⊢ (Disjoint on f) a b

Tactic:
exact hg d hd (hcd ▸ ha) hb hab

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι'
g : ι' → Set ι
f : ι → α
hs : s.PairwiseDisjoint fun i' => ⨆ i ∈ g i', f i
hg : ∀ i ∈ s, (g i).PairwiseDisjoint f
a b : ι
hab : a ≠ b
hb : ∃ i, ∃ (_ : i ∈ s), b ∈ g i
c : ι'
hc : c ∈ s
ha : a ∈ g c
⊢ (Disjoint on f) a b

Tactic:
obtain ⟨d, hd, hb⟩ := hb

Result:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι'
g : ι' → Set ι
f : ι → α
hs : s.PairwiseDisjoint fun i' => ⨆ i ∈ g i', f i
hg : ∀ i ∈ s, (g i).PairwiseDisjoint f
a b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
ha : a ∈ g c
d : ι'
hd : d ∈ s
hb : b ∈ g d
⊢ (Disjoint on f) a b

Proof state:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι'
g : ι' → Set ι
f : ι → α
hs : s.PairwiseDisjoint fun i' => ⨆ i ∈ g i', f i
hg : ∀ i ∈ s, (g i).PairwiseDisjoint f
a b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
ha : a ∈ g c
d : ι'
hd : d ∈ s
hb : b ∈ g d
⊢ (Disjoint on f) a b

Tactic:
obtain hcd | hcd := eq_or_ne (g c) (g d)

Result:
case intro.intro.intro.intro.inl
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι'
g : ι' → Set ι
f : ι → α
hs : s.PairwiseDisjoint fun i' => ⨆ i ∈ g i', f i
hg : ∀ i ∈ s, (g i).PairwiseDisjoint f
a b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
ha : a ∈ g c
d : ι'
hd : d ∈ s
hb : b ∈ g d
hcd : g c = g d
⊢ (Disjoint on f) a b

case intro.intro.intro.intro.inr
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι'
g : ι' → Set ι
f : ι → α
hs : s.PairwiseDisjoint fun i' => ⨆ i ∈ g i', f i
hg : ∀ i ∈ s, (g i).PairwiseDisjoint f
a b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
ha : a ∈ g c
d : ι'
hd : d ∈ s
hb : b ∈ g d
hcd : g c ≠ g d
⊢ (Disjoint on f) a b

Proof state:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι'
g : ι' → Set ι
f : ι → α
hs : s.PairwiseDisjoint fun i' => ⨆ i ∈ g i', f i
hg : ∀ i ∈ s, (g i).PairwiseDisjoint f
⊢ (⋃ i ∈ s, g i).PairwiseDisjoint f

Tactic:
rintro a ha b hb hab

Result:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι'
g : ι' → Set ι
f : ι → α
hs : s.PairwiseDisjoint fun i' => ⨆ i ∈ g i', f i
hg : ∀ i ∈ s, (g i).PairwiseDisjoint f
a : ι
ha : a ∈ ⋃ i ∈ s, g i
b : ι
hb : b ∈ ⋃ i ∈ s, g i
hab : a ≠ b
⊢ (Disjoint on f) a b

Proof state:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι'
g : ι' → Set ι
f : ι → α
hs : s.PairwiseDisjoint fun i' => ⨆ i ∈ g i', f i
hg : ∀ i ∈ s, (g i).PairwiseDisjoint f
a : ι
ha : a ∈ ⋃ i ∈ s, g i
b : ι
hb : b ∈ ⋃ i ∈ s, g i
hab : a ≠ b
⊢ (Disjoint on f) a b

Tactic:
simp_rw [Set.mem_iUnion] at ha hb

Result:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι'
g : ι' → Set ι
f : ι → α
hs : s.PairwiseDisjoint fun i' => ⨆ i ∈ g i', f i
hg : ∀ i ∈ s, (g i).PairwiseDisjoint f
a b : ι
hab : a ≠ b
ha : ∃ i, ∃ (_ : i ∈ s), a ∈ g i
hb : ∃ i, ∃ (_ : i ∈ s), b ∈ g i
⊢ (Disjoint on f) a b