Theorem: Finset.biUnion_union (LeanSAT/Upstream/ToMathlib.lean)

State before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
⊢ Finset.biUnion (s1 ∪ s2) f = Finset.biUnion s1 f ∪ Finset.biUnion s2 f
Tactic:
ext b
State after:
case a
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b : β
⊢ b ∈ Finset.biUnion (s1 ∪ s2) f ↔ b ∈ Finset.biUnion s1 f ∪ Finset.biUnion s2 f

State before:
case a
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b : β
⊢ b ∈ Finset.biUnion (s1 ∪ s2) f ↔ b ∈ Finset.biUnion s1 f ∪ Finset.biUnion s2 f
Tactic:
simp only [mem_biUnion, mem_union]
State after:
case a
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b : β
⊢ (∃ a, (a ∈ s1 ∨ a ∈ s2) ∧ b ∈ f a) ↔ (∃ a ∈ s1, b ∈ f a) ∨ ∃ a ∈ s2, b ∈ f a

State before:
case a
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b : β
⊢ (∃ a, (a ∈ s1 ∨ a ∈ s2) ∧ b ∈ f a) ↔ (∃ a ∈ s1, b ∈ f a) ∨ ∃ a ∈ s2, b ∈ f a
Tactic:
constructor
State after:
case a.mp
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b : β
⊢ (∃ a, (a ∈ s1 ∨ a ∈ s2) ∧ b ∈ f a) → (∃ a ∈ s1, b ∈ f a) ∨ ∃ a ∈ s2, b ∈ f a

case a.mpr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b : β
⊢ ((∃ a ∈ s1, b ∈ f a) ∨ ∃ a ∈ s2, b ∈ f a) → ∃ a, (a ∈ s1 ∨ a ∈ s2) ∧ b ∈ f a

State before:
case a.mp
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b : β
⊢ (∃ a, (a ∈ s1 ∨ a ∈ s2) ∧ b ∈ f a) → (∃ a ∈ s1, b ∈ f a) ∨ ∃ a ∈ s2, b ∈ f a
Tactic:
rintro ⟨a,b|b⟩
State after:
case a.mp.intro.intro.inl
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b✝ : β
a : α
right✝ : b✝ ∈ f a
b : a ∈ s1
⊢ (∃ a ∈ s1, b✝ ∈ f a) ∨ ∃ a ∈ s2, b✝ ∈ f a

case a.mp.intro.intro.inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b✝ : β
a : α
right✝ : b✝ ∈ f a
b : a ∈ s2
⊢ (∃ a ∈ s1, b✝ ∈ f a) ∨ ∃ a ∈ s2, b✝ ∈ f a

State before:
case a.mp.intro.intro.inl
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b✝ : β
a : α
right✝ : b✝ ∈ f a
b : a ∈ s1
⊢ (∃ a ∈ s1, b✝ ∈ f a) ∨ ∃ a ∈ s2, b✝ ∈ f a
Tactic:
refine Or.inl ⟨a,?_⟩
State after:
case a.mp.intro.intro.inl
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b✝ : β
a : α
right✝ : b✝ ∈ f a
b : a ∈ s1
⊢ a ∈ s1 ∧ b✝ ∈ f a

State before:
case a.mp.intro.intro.inl
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b✝ : β
a : α
right✝ : b✝ ∈ f a
b : a ∈ s1
⊢ a ∈ s1 ∧ b✝ ∈ f a
Tactic:
simp only [and_self, *]
State after:
no goals

State before:
case a.mp.intro.intro.inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b✝ : β
a : α
right✝ : b✝ ∈ f a
b : a ∈ s2
⊢ (∃ a ∈ s1, b✝ ∈ f a) ∨ ∃ a ∈ s2, b✝ ∈ f a
Tactic:
refine Or.inr ⟨a,?_⟩
State after:
case a.mp.intro.intro.inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b✝ : β
a : α
right✝ : b✝ ∈ f a
b : a ∈ s2
⊢ a ∈ s2 ∧ b✝ ∈ f a

State before:
case a.mp.intro.intro.inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b✝ : β
a : α
right✝ : b✝ ∈ f a
b : a ∈ s2
⊢ a ∈ s2 ∧ b✝ ∈ f a
Tactic:
simp only [and_self, *]
State after:
no goals

State before:
case a.mpr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b : β
⊢ ((∃ a ∈ s1, b ∈ f a) ∨ ∃ a ∈ s2, b ∈ f a) → ∃ a, (a ∈ s1 ∨ a ∈ s2) ∧ b ∈ f a
Tactic:
rintro (⟨a,b,c⟩|⟨a,b,c⟩)
  <;> refine ⟨a, ?_⟩
State after:
case a.mpr.inl.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b✝ : β
a : α
b : a ∈ s1
c : b✝ ∈ f a
⊢ (a ∈ s1 ∨ a ∈ s2) ∧ b✝ ∈ f a

case a.mpr.inr.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b✝ : β
a : α
b : a ∈ s2
c : b✝ ∈ f a
⊢ (a ∈ s1 ∨ a ∈ s2) ∧ b✝ ∈ f a

State before:
case a.mpr.inl.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b✝ : β
a : α
b : a ∈ s1
c : b✝ ∈ f a
⊢ (a ∈ s1 ∨ a ∈ s2) ∧ b✝ ∈ f a
Tactic:
simp only [and_self, true_or, *]
State after:
no goals

State before:
case a.mpr.inr.intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s1 s2 : Finset α
f : α → Finset β
b✝ : β
a : α
b : a ∈ s2
c : b✝ ∈ f a
⊢ (a ∈ s1 ∨ a ∈ s2) ∧ b✝ ∈ f a
Tactic:
simp only [and_self, or_true, *]
State after:
no goals