case h
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.138170
s✝ s₁ s₂ : Set ι
t t₁✝ t₂✝ : (i : ι) → Set (α i)
i : ι
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ (f ∈ pi s fun i => if p i then t₁ i else t₂ i) ↔ f ∈ pi {i | i ∈ s ∧ p i} t₁ ∩ pi {i | i ∈ s ∧ ¬p i} t₂
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.138170
s✝ s₁ s₂ : Set ι
t t₁✝ t₂✝ : (i : ι) → Set (α i)
i : ι
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
⊢ (pi s fun i => if p i then t₁ i else t₂ i) = pi {i | i ∈ s ∧ p i} t₁ ∩ pi {i | i ∈ s ∧ ¬p i} t₂
ext f
case h.refine'_1
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.138170
s✝ s₁ s₂ : Set ι
t t₁✝ t₂✝ : (i : ι) → Set (α i)
i : ι
p : ι → Prop
h✝ : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h : f ∈ pi s fun i => if p i then t₁ i else t₂ i
⊢ f ∈ pi {i | i ∈ s ∧ p i} t₁ ∩ pi {i | i ∈ s ∧ ¬p i} t₂

case h.refine'_2
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.138170
s✝ s₁ s₂ : Set ι
t t₁✝ t₂✝ : (i : ι) → Set (α i)
i : ι
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ f ∈ pi {i | i ∈ s ∧ p i} t₁ ∩ pi {i | i ∈ s ∧ ¬p i} t₂ → f ∈ pi s fun i => if p i then t₁ i else t₂ i
case h
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.138170
s✝ s₁ s₂ : Set ι
t t₁✝ t₂✝ : (i : ι) → Set (α i)
i : ι
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ (f ∈ pi s fun i => if p i then t₁ i else t₂ i) ↔ f ∈ pi {i | i ∈ s ∧ p i} t₁ ∩ pi {i | i ∈ s ∧ ¬p i} t₂
refine' ⟨fun h => _, _⟩
case h.refine'_1.right.intro
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.138170
s✝ s₁ s₂ : Set ι
t t₁✝ t₂✝ : (i : ι) → Set (α i)
i✝ : ι
p : ι → Prop
h✝ : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h : f ∈ pi s fun i => if p i then t₁ i else t₂ i
i : ι
his : i ∈ s
hpi : ¬p i
⊢ f i ∈ t₂ i
case h.refine'_1.right
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.138170
s✝ s₁ s₂ : Set ι
t t₁✝ t₂✝ : (i : ι) → Set (α i)
i : ι
p : ι → Prop
h✝ : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h : f ∈ pi s fun i => if p i then t₁ i else t₂ i
⊢ f ∈ pi {i | i ∈ s ∧ ¬p i} t₂
rintro i ⟨his, hpi⟩
no goals
case h.refine'_1.right.intro
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.138170
s✝ s₁ s₂ : Set ι
t t₁✝ t₂✝ : (i : ι) → Set (α i)
i✝ : ι
p : ι → Prop
h✝ : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h : f ∈ pi s fun i => if p i then t₁ i else t₂ i
i : ι
his : i ∈ s
hpi : ¬p i
⊢ f i ∈ t₂ i
simpa [*] using h i
case h.refine'_2.intro
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.138170
s✝ s₁ s₂ : Set ι
t t₁✝ t₂✝ : (i : ι) → Set (α i)
i✝ : ι
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
ht₁ : f ∈ pi {i | i ∈ s ∧ p i} t₁
ht₂ : f ∈ pi {i | i ∈ s ∧ ¬p i} t₂
i : ι
his : i ∈ s
⊢ f i ∈ (fun i => if p i then t₁ i else t₂ i) i
case h.refine'_2
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.138170
s✝ s₁ s₂ : Set ι
t t₁✝ t₂✝ : (i : ι) → Set (α i)
i : ι
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ f ∈ pi {i | i ∈ s ∧ p i} t₁ ∩ pi {i | i ∈ s ∧ ¬p i} t₂ → f ∈ pi s fun i => if p i then t₁ i else t₂ i
rintro ⟨ht₁, ht₂⟩ i his
no goals
case h.refine'_2.intro
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.138170
s✝ s₁ s₂ : Set ι
t t₁✝ t₂✝ : (i : ι) → Set (α i)
i✝ : ι
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
ht₁ : f ∈ pi {i | i ∈ s ∧ p i} t₁
ht₂ : f ∈ pi {i | i ∈ s ∧ ¬p i} t₂
i : ι
his : i ∈ s
⊢ f i ∈ (fun i => if p i then t₁ i else t₂ i) i
by_cases p i <;> simp_all