Theorem: Finset.map_disj_union (Logic/Logic/LogicSymbol.lean)

State before:
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
⊢ f (⋁(s₁ ∪ s₂)) ↔ f (⋁s₁ ⋎ ⋁s₂)
Tactic:
simp [map_disj]
State after:
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
⊢ (∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a) ↔ (∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a

State before:
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
⊢ (∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a) ↔ (∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a
Tactic:
constructor
State after:
case mp
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
⊢ (∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a) → (∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a

case mpr
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
⊢ ((∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a) → ∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a

State before:
case mp
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
⊢ (∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a) → (∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a

case mpr
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
⊢ ((∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a) → ∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a
Tactic:
. rintro ⟨a, h₁ | h₂, hb⟩;
  . left; use a;
  . right; use a;
State after:
case mpr
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
⊢ ((∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a) → ∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a

State before:
case mpr
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
⊢ ((∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a) → ∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a
Tactic:
. rintro (⟨a₁, h₁⟩ | ⟨a₂, h₂⟩);
  . use a₁; simp_all;
  . use a₂; simp_all;
State after:
no goals

State before:
case mp
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
⊢ (∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a) → (∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a
Tactic:
rintro ⟨a, h₁ | h₂, hb⟩
State after:
case mp.intro.intro.inl
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a : α
hb : f a
h₁ : a ∈ s₁
⊢ (∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a

case mp.intro.intro.inr
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a : α
hb : f a
h₂ : a ∈ s₂
⊢ (∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a

State before:
case mp.intro.intro.inl
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a : α
hb : f a
h₁ : a ∈ s₁
⊢ (∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a

case mp.intro.intro.inr
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a : α
hb : f a
h₂ : a ∈ s₂
⊢ (∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a
Tactic:
. left; use a;
State after:
case mp.intro.intro.inr
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a : α
hb : f a
h₂ : a ∈ s₂
⊢ (∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a

State before:
case mp.intro.intro.inr
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a : α
hb : f a
h₂ : a ∈ s₂
⊢ (∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a
Tactic:
. right; use a;
State after:
no goals

State before:
case mp.intro.intro.inl
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a : α
hb : f a
h₁ : a ∈ s₁
⊢ (∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a
Tactic:
left
State after:
case mp.intro.intro.inl.h
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a : α
hb : f a
h₁ : a ∈ s₁
⊢ ∃ a ∈ s₁, f a

State before:
case mp.intro.intro.inl.h
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a : α
hb : f a
h₁ : a ∈ s₁
⊢ ∃ a ∈ s₁, f a
Tactic:
use a
State after:
no goals

State before:
case mp.intro.intro.inr
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a : α
hb : f a
h₂ : a ∈ s₂
⊢ (∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a
Tactic:
right
State after:
case mp.intro.intro.inr.h
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a : α
hb : f a
h₂ : a ∈ s₂
⊢ ∃ a ∈ s₂, f a

State before:
case mp.intro.intro.inr.h
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a : α
hb : f a
h₂ : a ∈ s₂
⊢ ∃ a ∈ s₂, f a
Tactic:
use a
State after:
no goals

State before:
case mpr
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
⊢ ((∃ a ∈ s₁, f a) ∨ ∃ a ∈ s₂, f a) → ∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a
Tactic:
rintro (⟨a₁, h₁⟩ | ⟨a₂, h₂⟩)
State after:
case mpr.inl.intro
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a₁ : α
h₁ : a₁ ∈ s₁ ∧ f a₁
⊢ ∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a

case mpr.inr.intro
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a₂ : α
h₂ : a₂ ∈ s₂ ∧ f a₂
⊢ ∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a

State before:
case mpr.inl.intro
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a₁ : α
h₁ : a₁ ∈ s₁ ∧ f a₁
⊢ ∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a

case mpr.inr.intro
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a₂ : α
h₂ : a₂ ∈ s₂ ∧ f a₂
⊢ ∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a
Tactic:
. use a₁; simp_all;
State after:
case mpr.inr.intro
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a₂ : α
h₂ : a₂ ∈ s₂ ∧ f a₂
⊢ ∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a

State before:
case mpr.inr.intro
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a₂ : α
h₂ : a₂ ∈ s₂ ∧ f a₂
⊢ ∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a
Tactic:
. use a₂; simp_all;
State after:
no goals

State before:
case mpr.inl.intro
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a₁ : α
h₁ : a₁ ∈ s₁ ∧ f a₁
⊢ ∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a
Tactic:
use a₁
State after:
case h
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a₁ : α
h₁ : a₁ ∈ s₁ ∧ f a₁
⊢ (a₁ ∈ s₁ ∨ a₁ ∈ s₂) ∧ f a₁

State before:
case h
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a₁ : α
h₁ : a₁ ∈ s₁ ∧ f a₁
⊢ (a₁ ∈ s₁ ∨ a₁ ∈ s₂) ∧ f a₁
Tactic:
simp_all
State after:
no goals

State before:
case mpr.inr.intro
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a₂ : α
h₂ : a₂ ∈ s₂ ∧ f a₂
⊢ ∃ a, (a ∈ s₁ ∨ a ∈ s₂) ∧ f a
Tactic:
use a₂
State after:
case h
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a₂ : α
h₂ : a₂ ∈ s₂ ∧ f a₂
⊢ (a₂ ∈ s₁ ∨ a₂ ∈ s₂) ∧ f a₂

State before:
case h
α : Type u_2
inst✝³ : LogicalConnective α
inst✝² : DecidableEq α
F : Type u_1
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
s₁ s₂ : Finset α
a₂ : α
h₂ : a₂ ∈ s₂ ∧ f a₂
⊢ (a₂ ∈ s₁ ∨ a₂ ∈ s₂) ∧ f a₂
Tactic:
simp_all
State after:
no goals