awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
⊢ (reflection s).symm = reflection s
have h : ∀ (x : P), Eq (α := P) (((reflection s).symm : (a : P) → P) x : P) ((reflection s : (a : P) → P) x : P)
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
x : P
⊢ Eq (α := P) (((reflection s).symm : (a : P) → P) x : P) ((reflection s : (a : P) → P) x : P)
have h : Eq (α := P) ((reflection s : (a : P) → P) (((reflection s).symm : (a : P) → P) x : P) : P)
  ((reflection s : (a : P) → P) ((reflection s : (a : P) → P) x : P) : P)
Tactic: rw [← (reflection s).injective.eq_iff]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p : P
⊢ (reflection s : (a : P) → P) p = p ↔ p ∈ s
have rw : (∃ p₂ ∈ s, p -ᵥ (↑(Classical.arbitrary ↥s) : P) = p₂ -ᵥ (↑(Classical.arbitrary ↥s) : P)) ↔ p ∈ s
Tactic: rw [reflection_apply, Eq.comm, eq_vadd_iff_vsub_eq, Eq.comm, s.direction.reflection_eq_self_iff,
    s.mem_direction_iff_eq_vsub_right (SetLike.coe_mem (Classical.arbitrary s))]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s₁ s₂ : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s₁
inst_6 : Nonempty.{u_3 + 1} ↥s₂
inst_7 : s₁.direction.HasOrthogonalProjection
inst_8 : s₂.direction.HasOrthogonalProjection
p : P
⊢ Eq (α := P) ((reflection s₁ : (a : P) → P) p : P) ((reflection s₂ : (a : P) → P) p : P) ↔
    Eq.{u_3 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
      (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have rw : HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) -ᵥ p)
      (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
    HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) -ᵥ p)
      (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ↔
  Eq.{u_3 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
    (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
Tactic: rw [reflection_apply', reflection_apply']
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s₁ s₂ : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s₁
inst_6 : Nonempty.{u_3 + 1} ↥s₂
inst_7 : s₁.direction.HasOrthogonalProjection
inst_8 : s₂.direction.HasOrthogonalProjection
p : P
⊢ HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) -ᵥ p)
        (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) -ᵥ p)
        (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ↔
    Eq.{u_3 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
      (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have mp : HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) -ᵥ p)
      (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
    HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) -ᵥ p)
      (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) →
  Eq.{u_3 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
    (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s₁ s₂ : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s₁
inst_6 : Nonempty.{u_3 + 1} ↥s₂
inst_7 : s₁.direction.HasOrthogonalProjection
inst_8 : s₂.direction.HasOrthogonalProjection
p : P
mp :
  HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) -ᵥ p)
        (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) -ᵥ p)
        (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) →
    Eq.{u_3 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
      (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
⊢ HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) -ᵥ p)
        (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
      HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) -ᵥ p)
        (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) ↔
    Eq.{u_3 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
      (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have mpr : Eq.{u_3 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
    (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) →
  HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) -ᵥ p)
      (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
    HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) -ᵥ p)
      (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (hypothesis)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s₁ s₂ : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s₁
inst_6 : Nonempty.{u_3 + 1} ↥s₂
inst_7 : s₁.direction.HasOrthogonalProjection
inst_8 : s₂.direction.HasOrthogonalProjection
p : P
h :
  HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) -ᵥ p)
      (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
    HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) -ᵥ p)
      (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
⊢ Eq.{u_3 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
    (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have h₁ : Eq.{u_1 + 1} (α := 𝕜) 2 0 ∨
  VSub.vsub.{u_2, u_3} (P := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
      (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) =
    0
Tactic: rw [← @vsub_eq_zero_iff_eq V, vsub_vadd_eq_vsub_sub, vadd_vsub_assoc, add_comm, add_sub_assoc,
      vsub_sub_vsub_cancel_right, ←
      two_smul 𝕜 ((orthogonalProjection s₁ p : P) -ᵥ orthogonalProjection s₂ p), smul_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s₁ s₂ : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s₁
inst_6 : Nonempty.{u_3 + 1} ↥s₂
inst_7 : s₁.direction.HasOrthogonalProjection
inst_8 : s₂.direction.HasOrthogonalProjection
p : P
h :
  Eq.{u_3 + 1} (α := P) (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
    (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
⊢ HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) -ᵥ p)
      (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) =
    HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) -ᵥ p)
      (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
have mpr : HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) -ᵥ p)
    (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) =
  HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) -ᵥ p)
    (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p₁ p₂ : P
| dist p₁ ((reflection s : (a : P) → P) p₂)
have rw : dist (α := P) ((reflection s : (a : P) → P) ((reflection s : (a : P) → P) p₁ : P) : P)
  ((reflection s : (a : P) → P) p₂ : P)
Tactic: rw [← reflection_reflection s p₁]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p₁ p₂ : P
⊢ dist p₁ ((reflection s : (a : P) → P) p₂) = dist ((reflection s : (a : P) → P) p₁) p₂
have conv_lhs : dist (α := P) ((reflection s : (a : P) → P) ((reflection s : (a : P) → P) p₁ : P) : P)
    ((reflection s : (a : P) → P) p₂ : P) =
  dist ((reflection s : (a : P) → P) p₁) p₂
Tactic: conv_lhs => rw [← reflection_reflection s p₁]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p₁ : P
hp₁ : p₁ ∈ s
p₂ : P
⊢ dist p₁ ((reflection s : (a : P) → P) p₂) = dist p₁ p₂
have rw : ∀ (hp₁ : (reflection s : (a : P) → P) p₁ = p₁) (p₂ : P), dist p₁ ((reflection s : (a : P) → P) p₂) = dist p₁ p₂
Tactic: rw [← reflection_eq_self_iff p₁] at hp₁
Cleared hypotheses: hp₁, p₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p₁ : P
hp₁ : (reflection s : (a : P) → P) p₁ = p₁
p₂ : P
⊢ dist p₁ ((reflection s : (a : P) → P) p₂) = dist p₁ p₂
have h : p₁ = (reflection s : (a : P) → P) p₁
Tactic: convert! (reflection s).dist_map p₁ p₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p₁ : P
hp₁ : (reflection s : (a : P) → P) p₁ = p₁
p₂ : P
⊢ p₁ = (reflection s : (a : P) → P) p₁
have h : p₁ = p₁
Tactic: rw [hp₁]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s₁ s₂ : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s₁
inst_6 : s₁.direction.HasOrthogonalProjection
hle : s₁ ≤ s₂
p : P
hp : p ∈ s₂
⊢ Membership.mem (α := P) s₂ ((reflection s₁ : (a : P) → P) p : P)
have rw : HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) -ᵥ p)
    (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ∈
  s₂
Tactic: rw [reflection_apply']
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (hypothesis)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s₁ s₂ : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s₁
inst_6 : s₁.direction.HasOrthogonalProjection
hle : s₁ ≤ s₂
p : P
hp : p ∈ s₂
⊢ HVAdd.hVAdd (β := P) ((↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) -ᵥ p)
      (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ∈
    s₂
have ho : (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ∈ s₂
Tactic: have ho : ↑(orthogonalProjection s₁ p) ∈ s₂ := hle (orthogonalProjection_mem p)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : MetricSpace P
inst_4 : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p : P
hp : p ∈ s
v : V
hv : v ∈ s.directionᗮ
⊢ (reflection s : (a : P) → P) (v +ᵥ p) = -v +ᵥ p
have rw : ((↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P) -ᵥ p - v) +ᵥ (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : P) =
  -v +ᵥ p
Tactic: rw [reflection_apply', orthogonalProjection_vadd_eq_self hp hv, vsub_vadd_eq_vsub_sub]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
V₂ : Type u_4
P₂ : Type u_5
inst_3 : NormedAddCommGroup V₂
inst_4 : InnerProductSpace 𝕜 V₂
inst_5 : MetricSpace P
inst_6 : NormedAddTorsor V P
inst_7 : MetricSpace P₂
inst_8 : NormedAddTorsor V₂ P₂
s : AffineSubspace 𝕜 P
inst_9 : Nonempty.{u_3 + 1} ↥s
inst_10 : s.direction.HasOrthogonalProjection
f : P →ᵃⁱ[𝕜] P₂
inst_11 : (map f.toAffineMap s).direction.HasOrthogonalProjection
p : P
⊢ Eq.{u_5 + 1} (α := P₂)
    ((↑((orthogonalProjection (map f.toAffineMap s) : (a : P₂) → ↥(map f.toAffineMap s)) ((f : (a : P) → P₂) p)) : P₂) :
      P₂)
    ((f : (a : P) → P₂) (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) : P₂)
have rw : Membership.mem (α := P₂) (map f.toAffineMap s)
    ((f : (a : P) → P₂) (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) : P₂) ∧
  VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P) → P₂) p : P₂)
      ((f : (a : P) → P₂) (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) : P₂) ∈
    (map f.toAffineMap s).directionᗮ
Tactic: rw [coe_orthogonalProjection_eq_iff_mem]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
V₂ : Type u_4
P₂ : Type u_5
inst_3 : NormedAddCommGroup V₂
inst_4 : InnerProductSpace 𝕜 V₂
inst_5 : MetricSpace P
inst_6 : NormedAddTorsor V P
inst_7 : MetricSpace P₂
inst_8 : NormedAddTorsor V₂ P₂
s : AffineSubspace 𝕜 P
inst_9 : Nonempty.{u_3 + 1} ↥s
inst_10 : s.direction.HasOrthogonalProjection
f : P →ᵃⁱ[𝕜] P₂
inst_11 : (map f.toAffineMap s).direction.HasOrthogonalProjection
p : P
⊢ Membership.mem (α := P₂) (map f.toAffineMap s)
      ((f : (a : P) → P₂) (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) : P₂) ∧
    VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P) → P₂) p : P₂)
        ((f : (a : P) → P₂) (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) : P₂) ∈
      (map f.toAffineMap s).directionᗮ
have simp : VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P) → P₂) p : P₂)
    ((f : (a : P) → P₂) (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) : P₂) ∈
  (Submodule.map f.linearIsometry.toLinearMap s.direction)ᗮ
Tactic: simp only [mem_map, AffineIsometry.coe_toAffineMap, AffineIsometry.map_eq_iff, exists_eq_right,
    SetLike.coe_mem, map_direction, AffineIsometry.linear_eq_linearIsometry, true_and]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
V₂ : Type u_4
P₂ : Type u_5
inst_3 : NormedAddCommGroup V₂
inst_4 : InnerProductSpace 𝕜 V₂
inst_5 : MetricSpace P
inst_6 : NormedAddTorsor V P
inst_7 : MetricSpace P₂
inst_8 : NormedAddTorsor V₂ P₂
s : AffineSubspace 𝕜 P
inst_9 : Nonempty.{u_3 + 1} ↥s
inst_10 : s.direction.HasOrthogonalProjection
f : P →ᵃⁱ[𝕜] P₂
inst_11 : (map f.toAffineMap s).direction.HasOrthogonalProjection
p : P
⊢ VSub.vsub.{u_4, u_5} (P := P₂) ((f : (a : P) → P₂) p : P₂)
      ((f : (a : P) → P₂) (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) : P₂) ∈
    (Submodule.map f.linearIsometry.toLinearMap s.direction)ᗮ
have rw : ∀ u ∈ Submodule.map f.linearIsometry.toLinearMap s.direction,
  inner 𝕜 u ((f.linear : (a : V) → V₂) (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P))) = 0
Tactic: rw [← AffineIsometry.coe_toAffineMap, ← AffineMap.linearMap_vsub, Submodule.mem_orthogonal]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (hypothesis)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
V₂ : Type u_4
P₂ : Type u_5
inst_3 : NormedAddCommGroup V₂
inst_4 : InnerProductSpace 𝕜 V₂
inst_5 : MetricSpace P
inst_6 : NormedAddTorsor V P
inst_7 : MetricSpace P₂
inst_8 : NormedAddTorsor V₂ P₂
s : AffineSubspace 𝕜 P
inst_9 : Nonempty.{u_3 + 1} ↥s
inst_10 : s.direction.HasOrthogonalProjection
f : P →ᵃⁱ[𝕜] P₂
inst_11 : (map f.toAffineMap s).direction.HasOrthogonalProjection
p : P
u : V₂
hu : u ∈ Submodule.map f.linearIsometry.toLinearMap s.direction
⊢ inner 𝕜 u ((f.linear : (a : V) → V₂) (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P))) = 0
have hu₁ : ∃ y ∈ s.direction, (f.linearIsometry.toLinearMap : (a : V) → V₂) y = u
Tactic: rw [Submodule.mem_map] at hu
Cleared hypotheses: hu
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
V₂ : Type u_4
P₂ : Type u_5
inst_3 : NormedAddCommGroup V₂
inst_4 : InnerProductSpace 𝕜 V₂
inst_5 : MetricSpace P
inst_6 : NormedAddTorsor V P
inst_7 : MetricSpace P₂
inst_8 : NormedAddTorsor V₂ P₂
s : AffineSubspace 𝕜 P
inst_9 : Nonempty.{u_3 + 1} ↥s
inst_10 : s.direction.HasOrthogonalProjection
f : P →ᵃⁱ[𝕜] P₂
inst_11 : (map f.toAffineMap s).direction.HasOrthogonalProjection
p : P
u : V₂
hu : ∃ y ∈ s.direction, (f.linearIsometry.toLinearMap : (a : V) → V₂) y = u
⊢ inner 𝕜 u ((f.linear : (a : V) → V₂) (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P))) = 0
have obtain : ∀ (v : V) (hv : v ∈ s.direction),
  inner.{u_1, u_4} 𝕜 (E := V₂) ((f.linearIsometry.toLinearMap : (a : V) → V₂) v : V₂)
      ((f.linear : (a : V) → V₂) (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) : V₂) =
    0
Tactic: obtain ⟨v, hv, rfl⟩ := hu
Cleared hypotheses: u, hu
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
V₂ : Type u_4
P₂ : Type u_5
inst_3 : NormedAddCommGroup V₂
inst_4 : InnerProductSpace 𝕜 V₂
inst_5 : MetricSpace P
inst_6 : NormedAddTorsor V P
inst_7 : MetricSpace P₂
inst_8 : NormedAddTorsor V₂ P₂
s : AffineSubspace 𝕜 P
inst_9 : Nonempty.{u_3 + 1} ↥s
inst_10 : s.direction.HasOrthogonalProjection
f : P →ᵃⁱ[𝕜] P₂
inst_11 : (map f.toAffineMap s).direction.HasOrthogonalProjection
p : P
v : V
hv : v ∈ s.direction
⊢ inner.{u_1, u_4} 𝕜 (E := V₂) ((f.linearIsometry.toLinearMap : (a : V) → V₂) v : V₂)
      ((f.linear : (a : V) → V₂) (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) : V₂) =
    0
have rw : inner.{u_1, u_4} 𝕜 (E := V₂) ((f.linearIsometry.toLinearMap : (a : V) → V₂) v : V₂)
    ((f.linearIsometry.toLinearMap : (a : V) → V₂) (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) : V₂) =
  0
Tactic: rw [AffineIsometry.linear_eq_linearIsometry, LinearIsometry.coe_toLinearMap,
    LinearIsometry.inner_map_map, Submodule.inner_right_of_mem_orthogonal hv
      (vsub_orthogonalProjection_mem_direction_orthogonal _ _)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
V₂ : Type u_4
P₂ : Type u_5
inst_3 : NormedAddCommGroup V₂
inst_4 : InnerProductSpace 𝕜 V₂
inst_5 : MetricSpace P
inst_6 : NormedAddTorsor V P
inst_7 : MetricSpace P₂
inst_8 : NormedAddTorsor V₂ P₂
s : AffineSubspace 𝕜 P
inst_9 : Nonempty.{u_3 + 1} ↥s
inst_10 : s.direction.HasOrthogonalProjection
f : P →ᵃⁱ[𝕜] P₂
inst_11 : (map f.toAffineMap s).direction.HasOrthogonalProjection
p : P
v : V
hv : v ∈ s.direction
rw :
  inner.{u_1, u_4} 𝕜 (E := V₂) ((f.linearIsometry.toLinearMap : (a : V) → V₂) v : V₂)
      ((f.linearIsometry.toLinearMap : (a : V) → V₂) (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) : V₂) =
    0
⊢ inner.{u_1, u_4} 𝕜 (E := V₂) ((f.linearIsometry.toLinearMap : (a : V) → V₂) v : V₂)
      ((f.linear : (a : V) → V₂) (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) : V₂) =
    0
have rw₁ : inner.{u_1, u_4} 𝕜 (E := V₂) ((f.linearIsometry : (a : V) → V₂) v : V₂)
    ((f.linearIsometry : (a : V) → V₂) (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) : V₂) =
  0
Tactic: rw [AffineIsometry.linear_eq_linearIsometry, LinearIsometry.coe_toLinearMap,
    LinearIsometry.inner_map_map, Submodule.inner_right_of_mem_orthogonal hv
      (vsub_orthogonalProjection_mem_direction_orthogonal _ _)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Projection (goal)
Goal:
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
V₂ : Type u_4
P₂ : Type u_5
inst_3 : NormedAddCommGroup V₂
inst_4 : InnerProductSpace 𝕜 V₂
inst_5 : MetricSpace P
inst_6 : NormedAddTorsor V P
inst_7 : MetricSpace P₂
inst_8 : NormedAddTorsor V₂ P₂
s : AffineSubspace 𝕜 P
inst_9 : Nonempty.{u_3 + 1} ↥s
inst_10 : s.direction.HasOrthogonalProjection
f : P →ᵃⁱ[𝕜] P₂
inst_11 : (map f.toAffineMap s).direction.HasOrthogonalProjection
p : P
v : V
hv : v ∈ s.direction
rw :
  inner.{u_1, u_4} 𝕜 (E := V₂) ((f.linearIsometry.toLinearMap : (a : V) → V₂) v : V₂)
      ((f.linearIsometry.toLinearMap : (a : V) → V₂) (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) : V₂) =
    0
rw₁ :
  inner.{u_1, u_4} 𝕜 (E := V₂) ((f.linearIsometry : (a : V) → V₂) v : V₂)
      ((f.linearIsometry : (a : V) → V₂) (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) : V₂) =
    0
⊢ inner.{u_1, u_4} 𝕜 (E := V₂) ((f.linearIsometry.toLinearMap : (a : V) → V₂) v : V₂)
      ((f.linear : (a : V) → V₂) (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) : V₂) =
    0
have rw₂ : inner 𝕜 v (p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)) = 0
Tactic: rw [AffineIsometry.linear_eq_linearIsometry, LinearIsometry.coe_toLinearMap,
    LinearIsometry.inner_map_map, Submodule.inner_right_of_mem_orthogonal hv
      (vsub_orthogonalProjection_mem_direction_orthogonal _ _)]