case h
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.163005
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
⊢ x ∈ update f i ⁻¹' pi s t ↔ x ∈ t i
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.163005
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
⊢ update f i ⁻¹' pi s t = t i
ext x
case h.refine'_1
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.163005
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
h : x ∈ update f i ⁻¹' pi s t
⊢ x ∈ t i

case h.refine'_2
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.163005
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
hx : x ∈ t i
j : ι
hj : j ∈ s
⊢ update f i x j ∈ t j
case h
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.163005
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
⊢ x ∈ update f i ⁻¹' pi s t ↔ x ∈ t i
refine' ⟨fun h => _, fun hx j hj => _⟩
case h.e'_4
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.163005
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
h : x ∈ update f i ⁻¹' pi s t
⊢ x = update f i x i
case h.refine'_1
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.163005
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
h : x ∈ update f i ⁻¹' pi s t
⊢ x ∈ t i
convert h i hi
no goals
case h.e'_4
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.163005
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
h : x ∈ update f i ⁻¹' pi s t
⊢ x = update f i x i
simp
case h.refine'_2.inl
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.163005
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
inst✝ : DecidableEq ι
f : (i : ι) → α i
j : ι
hj hi : j ∈ s
hf : ∀ (j_1 : ι), j_1 ∈ s → j_1 ≠ j → f j_1 ∈ t j_1
x : α j
hx : x ∈ t j
⊢ update f j x j ∈ t j

case h.refine'_2.inr
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.163005
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
hx : x ∈ t i
j : ι
hj : j ∈ s
h : j ≠ i
⊢ update f i x j ∈ t j
case h.refine'_2
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.163005
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
hx : x ∈ t i
j : ι
hj : j ∈ s
⊢ update f i x j ∈ t j
obtain rfl | h := eq_or_ne j i
no goals
case h.refine'_2.inl
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.163005
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
inst✝ : DecidableEq ι
f : (i : ι) → α i
j : ι
hj hi : j ∈ s
hf : ∀ (j_1 : ι), j_1 ∈ s → j_1 ≠ j → f j_1 ∈ t j_1
x : α j
hx : x ∈ t j
⊢ update f j x j ∈ t j
simpa
case h.refine'_2.inr
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.163005
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
hx : x ∈ t i
j : ι
hj : j ∈ s
h : j ≠ i
⊢ f j ∈ t j
case h.refine'_2.inr
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.163005
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
hx : x ∈ t i
j : ι
hj : j ∈ s
h : j ≠ i
⊢ update f i x j ∈ t j
rw [update_noteq h]
no goals
case h.refine'_2.inr
ι : Type u_1
α : ι → Type u_2
β : ι → Type ?u.163005
s s₁ s₂ : Set ι
t t₁ t₂ : (i : ι) → Set (α i)
i : ι
inst✝ : DecidableEq ι
f : (i : ι) → α i
hi : i ∈ s
hf : ∀ (j : ι), j ∈ s → j ≠ i → f j ∈ t j
x : α i
hx : x ∈ t i
j : ι
hj : j ∈ s
h : j ≠ i
⊢ f j ∈ t j
exact hf j hj h