Module: Mathlib.Topology.UniformSpace.ProdApproximation

Goal state before:
pp: case pos
X : Type u_1
Y : Type u_2
R : Type u_3
V : Type u_4
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : TotallyDisconnectedSpace X
inst✝⁹ : T2Space X
inst✝⁸ : CompactSpace X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : CompactSpace Y
inst✝⁵ : AddCommGroup V
inst✝⁴ : UniformSpace V
inst✝³ : IsUniformAddGroup V
S : Set (V × V)
inst✝² : TopologicalSpace R
inst✝¹ : MonoidWithZero R
inst✝ : MulActionWithZero R V
f : C(X × Y, V)
hS : S ∈ 𝓤 V
hS' : {(f, g) | ∀ (y : Y), (f y, g y) ∈ S} ∈ 𝓤 C(Y, V)
n : ℕ
U : Fin n → TopologicalSpace.Clopens X
v : Fin n → C(Y, V)
hv : ∀ (x : X), (f.curry x, ∑ n, (↑(U n)).indicator (fun x ↦ v n) x) ∈ {(f, g) | ∀ (y : Y), (f y, g y) ∈ S}
x : X
y : Y
i : Fin n
hi : x ∈ U i
⊢ { toFun := (↑(U i)).indicator fun x ↦ 1, continuous_toFun := ⋯ } x • (v i) y = ((↑(U i)).indicator (fun x ↦ v i) x) y

pp: case neg
X : Type u_1
Y : Type u_2
R : Type u_3
V : Type u_4
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : TotallyDisconnectedSpace X
inst✝⁹ : T2Space X
inst✝⁸ : CompactSpace X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : CompactSpace Y
inst✝⁵ : AddCommGroup V
inst✝⁴ : UniformSpace V
inst✝³ : IsUniformAddGroup V
S : Set (V × V)
inst✝² : TopologicalSpace R
inst✝¹ : MonoidWithZero R
inst✝ : MulActionWithZero R V
f : C(X × Y, V)
hS : S ∈ 𝓤 V
hS' : {(f, g) | ∀ (y : Y), (f y, g y) ∈ S} ∈ 𝓤 C(Y, V)
n : ℕ
U : Fin n → TopologicalSpace.Clopens X
v : Fin n → C(Y, V)
hv : ∀ (x : X), (f.curry x, ∑ n, (↑(U n)).indicator (fun x ↦ v n) x) ∈ {(f, g) | ∀ (y : Y), (f y, g y) ∈ S}
x : X
y : Y
i : Fin n
hi : x ∉ U i
⊢ { toFun := (↑(U i)).indicator fun x ↦ 1, continuous_toFun := ⋯ } x • (v i) y = ((↑(U i)).indicator (fun x ↦ v i) x) y

Tactic:
<;>

Goal state after:
case pos
X : Type u_1
Y : Type u_2
R : Type u_3
V : Type u_4
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : TotallyDisconnectedSpace X
inst✝⁹ : T2Space X
inst✝⁸ : CompactSpace X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : CompactSpace Y
inst✝⁵ : AddCommGroup V
inst✝⁴ : UniformSpace V
inst✝³ : IsUniformAddGroup V
S : Set (V × V)
inst✝² : TopologicalSpace R
inst✝¹ : MonoidWithZero R
inst✝ : MulActionWithZero R V
f : C(X × Y, V)
hS : S ∈ 𝓤 V
hS' : {(f, g) | ∀ (y : Y), (f y, g y) ∈ S} ∈ 𝓤 C(Y, V)
n : ℕ
U : Fin n → TopologicalSpace.Clopens X
v : Fin n → C(Y, V)
hv : ∀ (x : X), (f.curry x, ∑ n, (↑(U n)).indicator (fun x ↦ v n) x) ∈ {(f, g) | ∀ (y : Y), (f y, g y) ∈ S}
x : X
y : Y
i : Fin n
hi : x ∈ U i
⊢ { toFun := (↑(U i)).indicator fun x ↦ 1, continuous_toFun := ⋯ } x • (v i) y = ((↑(U i)).indicator (fun x ↦ v i) x) y

case neg
X : Type u_1
Y : Type u_2
R : Type u_3
V : Type u_4
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : TotallyDisconnectedSpace X
inst✝⁹ : T2Space X
inst✝⁸ : CompactSpace X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : CompactSpace Y
inst✝⁵ : AddCommGroup V
inst✝⁴ : UniformSpace V
inst✝³ : IsUniformAddGroup V
S : Set (V × V)
inst✝² : TopologicalSpace R
inst✝¹ : MonoidWithZero R
inst✝ : MulActionWithZero R V
f : C(X × Y, V)
hS : S ∈ 𝓤 V
hS' : {(f, g) | ∀ (y : Y), (f y, g y) ∈ S} ∈ 𝓤 C(Y, V)
n : ℕ
U : Fin n → TopologicalSpace.Clopens X
v : Fin n → C(Y, V)
hv : ∀ (x : X), (f.curry x, ∑ n, (↑(U n)).indicator (fun x ↦ v n) x) ∈ {(f, g) | ∀ (y : Y), (f y, g y) ∈ S}
x : X
y : Y
i : Fin n
hi : x ∉ U i
⊢ { toFun := (↑(U i)).indicator fun x ↦ 1, continuous_toFun := ⋯ } x • (v i) y = ((↑(U i)).indicator (fun x ↦ v i) x) y