refine ⟨fun h ↦ ⟨Module.piEquiv η R R x, ?_, by simp⟩, fun h ↦ ?_⟩
case h
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x✝ : η → R
U✝ V : Submodule R (η → R)
inst✝ : Fintype η
U : Submodule R (η → R)
x : η → R
⊢ (∀ y ∈ U, ∑ i : η, x i * y i = 0) ↔ ∃ y, (∀ w ∈ U, y w = 0) ∧ (Module.piEquiv η R R).symm y = x
case h.refine_1
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x✝ : η → R
U✝ V : Submodule R (η → R)
inst✝ : Fintype η
U : Submodule R (η → R)
x : η → R
h : ∀ y ∈ U, ∑ i : η, x i * y i = 0
⊢ ∀ w ∈ U, ((Module.piEquiv η R R) x) w = 0

case h.refine_2
α : Type u_1
R : Type u_2
η✝ : Type u_3
ι : Type u_4
η : Type u_5
inst✝¹ : CommRing R
x✝ : η → R
U✝ V : Submodule R (η → R)
inst✝ : Fintype η
U : Submodule R (η → R)
x : η → R
h : ∃ y, (∀ w ∈ U, y w = 0) ∧ (Module.piEquiv η R R).symm y = x
⊢ ∀ y ∈ U, ∑ i : η, x i * y i = 0