-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem LinearIsometry.map_orthogonalProjection {E E' : Type*} [NormedAddCommGroup E]
    [NormedAddCommGroup E'] [InnerProductSpace 𝕜 E] [InnerProductSpace 𝕜 E'] (f : E →ₗᵢ[𝕜] E')
    (p : Submodule 𝕜 E) [HasOrthogonalProjection p] [HasOrthogonalProjection (p.map f.toLinearMap)]
    (x : E) : f (orthogonalProjection p x) = orthogonalProjection (p.map f.toLinearMap) (f x)

Proof state:
case refine_1
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_4
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 E'
f : E →ₗᵢ[𝕜] E'
p : Submodule 𝕜 E
inst✝¹ : HasOrthogonalProjection p
inst✝ : HasOrthogonalProjection (Submodule.map f.toLinearMap p)
x : E
⊢ f ↑((orthogonalProjection p) x) ∈ Submodule.map f.toLinearMap p

Tactic:
refine Submodule.apply_coe_mem_map _ _

Result:
no goals

Proof state:
case refine_2.intro.intro
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_4
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 E'
f : E →ₗᵢ[𝕜] E'
p : Submodule 𝕜 E
inst✝¹ : HasOrthogonalProjection p
inst✝ : HasOrthogonalProjection (Submodule.map f.toLinearMap p)
x x' : E
hx' : x' ∈ ↑p
⊢ ⟪f x - f ↑((orthogonalProjection p) x), f x'⟫_𝕜 = 0

Tactic:
rw [← f.map_sub, f.inner_map_map, orthogonalProjection_inner_eq_zero x x' hx']

Result:
no goals

Proof state:
case refine_2
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_4
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 E'
f : E →ₗᵢ[𝕜] E'
p : Submodule 𝕜 E
inst✝¹ : HasOrthogonalProjection p
inst✝ : HasOrthogonalProjection (Submodule.map f.toLinearMap p)
x : E
y : E'
hy : y ∈ Submodule.map f.toLinearMap p
⊢ ⟪f x - f ↑((orthogonalProjection p) x), y⟫_𝕜 = 0

Tactic:
rcases hy with ⟨x', hx', rfl : f x' = y⟩

Result:
case refine_2.intro.intro
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_4
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 E'
f : E →ₗᵢ[𝕜] E'
p : Submodule 𝕜 E
inst✝¹ : HasOrthogonalProjection p
inst✝ : HasOrthogonalProjection (Submodule.map f.toLinearMap p)
x x' : E
hx' : x' ∈ ↑p
⊢ ⟪f x - f ↑((orthogonalProjection p) x), f x'⟫_𝕜 = 0

Proof state:
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_4
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 E'
f : E →ₗᵢ[𝕜] E'
p : Submodule 𝕜 E
inst✝¹ : HasOrthogonalProjection p
inst✝ : HasOrthogonalProjection (Submodule.map f.toLinearMap p)
x : E
⊢ f ↑((orthogonalProjection p) x) = ↑((orthogonalProjection (Submodule.map f.toLinearMap p)) (f x))

Tactic:
refine (eq_orthogonalProjection_of_mem_of_inner_eq_zero ?_ fun y hy => ?_).symm

Result:
case refine_1
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_4
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 E'
f : E →ₗᵢ[𝕜] E'
p : Submodule 𝕜 E
inst✝¹ : HasOrthogonalProjection p
inst✝ : HasOrthogonalProjection (Submodule.map f.toLinearMap p)
x : E
⊢ f ↑((orthogonalProjection p) x) ∈ Submodule.map f.toLinearMap p

case refine_2
𝕜 : Type u_1
inst✝⁶ : RCLike 𝕜
E : Type u_4
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 E'
f : E →ₗᵢ[𝕜] E'
p : Submodule 𝕜 E
inst✝¹ : HasOrthogonalProjection p
inst✝ : HasOrthogonalProjection (Submodule.map f.toLinearMap p)
x : E
y : E'
hy : y ∈ Submodule.map f.toLinearMap p
⊢ ⟪f x - f ↑((orthogonalProjection p) x), y⟫_𝕜 = 0