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

Proof state:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : s.PairwiseDisjoint fun i' => (g i').sup f
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)
⊢ Function.onFun Disjoint 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✝¹ : Lattice α
inst✝ : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : s.PairwiseDisjoint fun i' => (g i').sup f
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
⊢ Function.onFun Disjoint f a b

case intro.intro.intro.intro.inr
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : s.PairwiseDisjoint fun i' => (g i').sup f
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
⊢ Function.onFun Disjoint f a b

Proof state:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : s.PairwiseDisjoint fun i' => (g i').sup f
hg : ∀ i ∈ s, (↑(g i)).PairwiseDisjoint f
a : ι
ha : a ∈ ⋃ i ∈ s, ↑(g i)
b : ι
hb : b ∈ ⋃ i ∈ s, ↑(g i)
hab : a ≠ b
⊢ Function.onFun Disjoint f a b

Tactic:
simp_rw [Set.mem_iUnion] at ha hb

Result:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : s.PairwiseDisjoint fun i' => (g i').sup f
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)
⊢ Function.onFun Disjoint f a b

Proof state:
case intro.intro.intro.intro.inl
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : s.PairwiseDisjoint fun i' => (g i').sup f
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
⊢ Function.onFun Disjoint f a b

Tactic:
exact hg d hd (by rwa [hcd] at ha) hb hab

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : s.PairwiseDisjoint fun i' => (g i').sup f
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
⊢ a ∈ ↑(g d)

Tactic:
rwa [hcd] at ha

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : s.PairwiseDisjoint fun i' => (g i').sup f
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)
⊢ Function.onFun Disjoint f a b

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

Result:
case intro.intro
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : s.PairwiseDisjoint fun i' => (g i').sup f
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)
⊢ Function.onFun Disjoint f a b

Proof state:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : s.PairwiseDisjoint fun i' => (g i').sup f
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✝¹ : Lattice α
inst✝ : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : s.PairwiseDisjoint fun i' => (g i').sup f
hg : ∀ i ∈ s, (↑(g i)).PairwiseDisjoint f
a : ι
ha : a ∈ ⋃ i ∈ s, ↑(g i)
b : ι
hb : b ∈ ⋃ i ∈ s, ↑(g i)
hab : a ≠ b
⊢ Function.onFun Disjoint f a b

Proof state:
case intro.intro.intro.intro.inr
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : s.PairwiseDisjoint fun i' => (g i').sup f
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
⊢ Function.onFun Disjoint f a b

Tactic:
exact (hs hc hd (ne_of_apply_ne _ hcd)).mono (Finset.le_sup ha) (Finset.le_sup hb)

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : s.PairwiseDisjoint fun i' => (g i').sup f
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)
⊢ Function.onFun Disjoint 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✝¹ : Lattice α
inst✝ : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : s.PairwiseDisjoint fun i' => (g i').sup f
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)
⊢ Function.onFun Disjoint f a b