Theorem: Finset.map_conj_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_conj]
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:
. intro h;
  constructor;
  . intro a ha;
    exact h a (Or.inl ha);
  . intro a ha;
    exact h a (Or.inr ha);
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:
. intro ⟨h₁, h₂⟩ a ha;
  cases ha <;> 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:
intro h
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 α
h : ∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a
⊢ (∀ a ∈ s₁, f a) ∧ ∀ 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 α
h : ∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a
⊢ (∀ a ∈ s₁, f a) ∧ ∀ a ∈ s₂, f a
Tactic:
constructor
State after:
case mp.left
α : 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 α
h : ∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a
⊢ ∀ a ∈ s₁, f a

case mp.right
α : 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 α
h : ∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a
⊢ ∀ a ∈ s₂, f a

State before:
case mp.left
α : 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 α
h : ∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a
⊢ ∀ a ∈ s₁, f a

case mp.right
α : 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 α
h : ∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a
⊢ ∀ a ∈ s₂, f a
Tactic:
. intro a ha;
  exact h a (Or.inl ha);
State after:
case mp.right
α : 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 α
h : ∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a
⊢ ∀ a ∈ s₂, f a

State before:
case mp.right
α : 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 α
h : ∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a
⊢ ∀ a ∈ s₂, f a
Tactic:
. intro a ha;
  exact h a (Or.inr ha);
State after:
no goals

State before:
case mp.left
α : 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 α
h : ∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a
⊢ ∀ a ∈ s₁, f a
Tactic:
intro a ha
State after:
case mp.left
α : 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 α
h : ∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a
a : α
ha : a ∈ s₁
⊢ f a

State before:
case mp.left
α : 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 α
h : ∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a
a : α
ha : a ∈ s₁
⊢ f a
Tactic:
exact h a (Or.inl ha)
State after:
no goals

State before:
case mp.right
α : 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 α
h : ∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a
⊢ ∀ a ∈ s₂, f a
Tactic:
intro a ha
State after:
case mp.right
α : 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 α
h : ∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a
a : α
ha : a ∈ s₂
⊢ f a

State before:
case mp.right
α : 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 α
h : ∀ (a : α), a ∈ s₁ ∨ a ∈ s₂ → f a
a : α
ha : a ∈ s₂
⊢ f a
Tactic:
exact h a (Or.inr ha)
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:
intro ⟨h₁, h₂⟩ a ha
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 α
h₁ : ∀ a ∈ s₁, f a
h₂ : ∀ a ∈ s₂, f a
a : α
ha : 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 α
h₁ : ∀ a ∈ s₁, f a
h₂ : ∀ a ∈ s₂, f a
a : α
ha : a ∈ s₁ ∨ a ∈ s₂
⊢ f a
Tactic:
cases ha <;> simp_all
State after:
no goals