-- Mathlib/Geometry/Euclidean/Basic.lean
theorem orthogonalProjection_vadd_eq_self {s : AffineSubspace ℝ P} [Nonempty s]
    [HasOrthogonalProjection s.direction] {p : P} (hp : p ∈ s) {v : V} (hv : v ∈ s.directionᗮ) :
    orthogonalProjection s (v +ᵥ p) = ⟨p, hp⟩

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
hp : p ∈ s
v : V
hv : v ∈ s.directionᗮ
h : (v +ᵥ p) -ᵥ ↑((orthogonalProjection s) (v +ᵥ p)) ∈ s.directionᗮ
⊢ (orthogonalProjection s) (v +ᵥ p) = ⟨p, hp⟩

Tactic:
rw [vadd_vsub_assoc, Submodule.add_mem_iff_right _ hv] at h

Result:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
hp : p ∈ s
v : V
hv : v ∈ s.directionᗮ
h : p -ᵥ ↑((orthogonalProjection s) (v +ᵥ p)) ∈ s.directionᗮ
⊢ (orthogonalProjection s) (v +ᵥ p) = ⟨p, hp⟩

Proof state:
case a
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
hp : p ∈ s
v : V
hv : v ∈ s.directionᗮ
h : p -ᵥ ↑((orthogonalProjection s) (v +ᵥ p)) ∈ s.directionᗮ
⊢ ↑(⟨p, hp⟩ -ᵥ (orthogonalProjection s) (v +ᵥ p)) ∈ s.direction

Tactic:
exact (_ : s.direction).2

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
hp : p ∈ s
v : V
hv : v ∈ s.directionᗮ
⊢ (orthogonalProjection s) (v +ᵥ p) = ⟨p, hp⟩

Tactic:
have h := vsub_orthogonalProjection_mem_direction_orthogonal s (v +ᵥ p)

Result:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
hp : p ∈ s
v : V
hv : v ∈ s.directionᗮ
h : (v +ᵥ p) -ᵥ ↑((orthogonalProjection s) (v +ᵥ p)) ∈ s.directionᗮ
⊢ (orthogonalProjection s) (v +ᵥ p) = ⟨p, hp⟩

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
hp : p ∈ s
v : V
hv : v ∈ s.directionᗮ
h : p -ᵥ ↑((orthogonalProjection s) (v +ᵥ p)) ∈ s.directionᗮ
⊢ ⟨p, hp⟩ -ᵥ (orthogonalProjection s) (v +ᵥ p) = 0

Tactic:
ext

Result:
case a
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
hp : p ∈ s
v : V
hv : v ∈ s.directionᗮ
h : p -ᵥ ↑((orthogonalProjection s) (v +ᵥ p)) ∈ s.directionᗮ
⊢ ↑(⟨p, hp⟩ -ᵥ (orthogonalProjection s) (v +ᵥ p)) = ↑0

Proof state:
case a
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
hp : p ∈ s
v : V
hv : v ∈ s.directionᗮ
h : p -ᵥ ↑((orthogonalProjection s) (v +ᵥ p)) ∈ s.directionᗮ
⊢ ↑(⟨p, hp⟩ -ᵥ (orthogonalProjection s) (v +ᵥ p)) = ↑0

Tactic:
refine Submodule.disjoint_def.1 s.direction.orthogonal_disjoint _ ?_ h

Result:
case a
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
hp : p ∈ s
v : V
hv : v ∈ s.directionᗮ
h : p -ᵥ ↑((orthogonalProjection s) (v +ᵥ p)) ∈ s.directionᗮ
⊢ ↑(⟨p, hp⟩ -ᵥ (orthogonalProjection s) (v +ᵥ p)) ∈ s.direction

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
hp : p ∈ s
v : V
hv : v ∈ s.directionᗮ
h : p -ᵥ ↑((orthogonalProjection s) (v +ᵥ p)) ∈ s.directionᗮ
⊢ (orthogonalProjection s) (v +ᵥ p) = ⟨p, hp⟩

Tactic:
refine (eq_of_vsub_eq_zero ?_).symm

Result:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥s
inst✝ : HasOrthogonalProjection s.direction
p : P
hp : p ∈ s
v : V
hv : v ∈ s.directionᗮ
h : p -ᵥ ↑((orthogonalProjection s) (v +ᵥ p)) ∈ s.directionᗮ
⊢ ⟨p, hp⟩ -ᵥ (orthogonalProjection s) (v +ᵥ p) = 0