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
p : P
mp : (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = p → p ∈ s
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = p ↔ p ∈ s
have mpr : p ∈ s → (↑((orthogonalProjection s : (a : P) → ↥s) p) : 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 : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p : P
h : p ∈ s
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = p
have hp : p ∈ (↑s : Set P) ∩ (↑(mk' p s.directionᗮ) : Set P)
Tactic: have hp : p ∈ (s : Set P) ∩ mk' p s.directionᗮ := ⟨h, self_mem_mk' p _⟩
-- 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 : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p : P
h : p ∈ s
hp : p ∈ (↑s : Set P) ∩ (↑(mk' p s.directionᗮ) : Set P)
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = p
have hp₁ : Membership.mem (γ := Set P) {(↑((orthogonalProjection s : (a : P) → ↥s) p) : P)} p
Tactic: rw [inter_eq_singleton_orthogonalProjection p] at hp
Cleared hypotheses: 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 : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p : P
h : p ∈ s
hp : Membership.mem (γ := Set P) {(↑((orthogonalProjection s : (a : P) → ↥s) p) : P)} p
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = p
have mpr : p = (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
Tactic: symm
-- 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 : ↥s
⊢ (orthogonalProjection s : (a : P) → ↥s) (↑p : P) = p
have a : (↑((orthogonalProjection s : (a : P) → ↥s) (↑p : P)) : P) = (↑p : 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
p : ↥s
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) (↑p : P)) : P) = (↑p : P)
have a : (↑p : P) ∈ s
Tactic: rw [orthogonalProjection_eq_self_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 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
h : s = s'
p : P
⊢ Eq.{u_3 + 1} (α := P) (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
    (↑((orthogonalProjection s' : (a : P) → ↥s') p) : P)
have subst : ∀ [inst_9 : Nonempty.{u_3 + 1} ↥s] [inst_10 : s.direction.HasOrthogonalProjection],
  Eq.{u_3 + 1} (α := P) (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
    (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
Tactic: subst h
Cleared hypotheses: s', inst_6, inst_8, h
-- 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
p₁ p₂ : P
⊢ (↑((orthogonalProjection (affineSpan 𝕜 {p₁}) : (a : P) → ↥(affineSpan 𝕜 {p₁})) p₂) : P) = p₁
have h : Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 {p₁})
  (↑((orthogonalProjection (affineSpan 𝕜 {p₁}) : (a : P) → ↥(affineSpan 𝕜 {p₁})) p₂) : P)
Tactic: have h := SetLike.coe_mem (orthogonalProjection (affineSpan 𝕜 {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
p₁ p₂ : P
h :
  Membership.mem (γ := AffineSubspace 𝕜 P) (affineSpan 𝕜 {p₁})
    (↑((orthogonalProjection (affineSpan 𝕜 {p₁}) : (a : P) → ↥(affineSpan 𝕜 {p₁})) p₂) : P)
⊢ (↑((orthogonalProjection (affineSpan 𝕜 {p₁}) : (a : P) → ↥(affineSpan 𝕜 {p₁})) p₂) : P) = p₁
have rwa : ∀ (h : (↑((orthogonalProjection (affineSpan 𝕜 {p₁}) : (a : P) → ↥(affineSpan 𝕜 {p₁})) p₂) : P) = p₁),
  (↑((orthogonalProjection (affineSpan 𝕜 {p₁}) : (a : P) → ↥(affineSpan 𝕜 {p₁})) p₂) : P) = p₁
Tactic: rwa [mem_affineSpan_singleton] 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 : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p : P
⊢ dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = 0 ↔ p ∈ s
have rw : dist (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p = 0 ↔ p ∈ s
Tactic: rw [dist_comm, dist_eq_zero, orthogonalProjection_eq_self_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
rw : dist (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p = 0 ↔ p ∈ s
⊢ dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = 0 ↔ p ∈ s
have rw₁ : (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = p ↔ p ∈ s
Tactic: rw [dist_comm, dist_eq_zero, orthogonalProjection_eq_self_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
rw : dist (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) p = 0 ↔ p ∈ s
rw₁ : (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = p ↔ p ∈ s
⊢ dist p (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = 0 ↔ p ∈ s
have rw₂ : p ∈ s ↔ p ∈ s
Tactic: rw [dist_comm, dist_eq_zero, orthogonalProjection_eq_self_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
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) -ᵥ p ∈ s.directionᗮ
have rw : Membership.mem (γ := AffineSubspace 𝕜 P) (mk' p s.directionᗮ) (↑((orthogonalProjection s : (a : P) → ↥s) p) : P)
Tactic: rw [← mem_mk']
-- 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 q : P
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = q ↔ q ∈ s ∧ p -ᵥ q ∈ s.directionᗮ
have mp : (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = q → q ∈ s ∧ p -ᵥ q ∈ s.directionᗮ
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 : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p q : P
mp : (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = q → q ∈ s ∧ p -ᵥ q ∈ s.directionᗮ
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = q ↔ q ∈ s ∧ p -ᵥ q ∈ s.directionᗮ
have mpr : q ∈ s ∧ p -ᵥ q ∈ s.directionᗮ → (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = q
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 : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p q : P
hqs : q ∈ s
hpq : p -ᵥ q ∈ s.directionᗮ
⊢ Membership.mem (γ := AffineSubspace 𝕜 P) (mk' p s.directionᗮ) q
have rwa : q -ᵥ p ∈ s.directionᗮ
Tactic: rwa [mem_mk', ← neg_mem_iff, neg_vsub_eq_vsub_rev]
-- 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 q : P
hqs : q ∈ s
hpq : p -ᵥ q ∈ s.directionᗮ
rwa : q -ᵥ p ∈ s.directionᗮ
⊢ Membership.mem (γ := AffineSubspace 𝕜 P) (mk' p s.directionᗮ) q
have rwa₁ : -(q -ᵥ p) ∈ s.directionᗮ
Tactic: rwa [mem_mk', ← neg_mem_iff, neg_vsub_eq_vsub_rev]
-- 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 : AffineSubspace 𝕜 P
inst_5 : Nonempty.{u_3 + 1} ↥s
inst_6 : s.direction.HasOrthogonalProjection
p q : P
hqs : q ∈ s
hpq : p -ᵥ q ∈ s.directionᗮ
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = q
have hq : Membership.mem (γ := AffineSubspace 𝕜 P) (mk' p s.directionᗮ) q
Tactic: have hq : q ∈ mk' p s.directionᗮ := by
      rwa [mem_mk', ← neg_mem_iff, neg_vsub_eq_vsub_rev]
-- 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 q : P
hqs : q ∈ s
hpq : p -ᵥ q ∈ s.directionᗮ
hq : Membership.mem (γ := AffineSubspace 𝕜 P) (mk' p s.directionᗮ) q
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) p) : P) = q
have mpr : Membership.mem (γ := Set P) {(↑((orthogonalProjection s : (a : P) → ↥s) p) : P)} q
Tactic: suffices q ∈ ({(orthogonalProjection s p : P)} : Set P) by
      simpa [eq_comm] using this
-- 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 q : P
hqs : q ∈ s
hpq : p -ᵥ q ∈ s.directionᗮ
hq : Membership.mem (γ := AffineSubspace 𝕜 P) (mk' p s.directionᗮ) q
⊢ Membership.mem (γ := Set P) {(↑((orthogonalProjection s : (a : P) → ↥s) p) : P)} q
have mpr : q ∈ (↑s : Set P) ∩ (↑(mk' p s.directionᗮ) : Set P)
Tactic: rw [← inter_eq_singleton_orthogonalProjection]
-- 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 q : P
⊢ Eq (α := ↥s) ((orthogonalProjection s : (a : P) → ↥s) p : ↥s) ((orthogonalProjection s : (a : P) → ↥s) q : ↥s) ↔
    p -ᵥ q ∈ s.directionᗮ
have rw : p -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) q) : P) ∈ s.directionᗮ ↔
  p -ᵥ q + (q -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) q) : P)) ∈ s.directionᗮ
Tactic: rw [orthogonalProjection_eq_iff_mem, ← s.directionᗮ.add_mem_iff_left (x := p -ᵥ q)
    (vsub_orthogonalProjection_mem_direction_orthogonal s q)]
-- 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)
inst_9 : (s₁ ⊔ s₂).direction.HasOrthogonalProjection
⊢ Eq.{u_3 + 1} (α := P) (↑((orthogonalProjection (s₁ ⊔ s₂) : (a : P) → ↥(s₁ ⊔ s₂)) p) : P)
    (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P)
have rw : (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ∈ s₁ ⊔ s₂ ∧
  p -ᵥ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ∈ (s₁ ⊔ 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
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)
inst_9 : (s₁ ⊔ s₂).direction.HasOrthogonalProjection
⊢ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ∈ s₁ ⊔ s₂ ∧
    p -ᵥ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ∈ (s₁ ⊔ s₂).directionᗮ
have refine : p -ᵥ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ∈ (s₁ ⊔ s₂).directionᗮ
Tactic: refine ⟨SetLike.le_def.1 le_sup_left (orthogonalProjection_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
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)
inst_9 : (s₁ ⊔ s₂).direction.HasOrthogonalProjection
⊢ p -ᵥ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ∈ (s₁ ⊔ s₂).directionᗮ
have rw : p -ᵥ (↑((orthogonalProjection s₁ : (a : P) → ↥s₁) p) : P) ∈ s₁.directionᗮ ⊓ s₂.directionᗮ
Tactic: rw [direction_sup_eq_sup_direction (orthogonalProjection_mem p) (h ▸ orthogonalProjection_mem p),
    ← Submodule.inf_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
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ᗮ
⊢ (orthogonalProjection s : (a : P) → ↥s) (v +ᵥ p) = Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp
have a : (↑((orthogonalProjection s : (a : P) → ↥s) (v +ᵥ p)) : P) = (↑(Subtype.mk (p := fun (x : P) ↦ x ∈ s) p hp) : 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₁ 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
h : s₁ ≤ s₂
p : P
⊢ Eq (α := ↥s₁) ((orthogonalProjection s₁ : (a : P) → ↥s₁) (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) : ↥s₁)
    ((orthogonalProjection s₁ : (a : P) → ↥s₁) p : ↥s₁)
have rw : (↑((orthogonalProjection s₂ : (a : P) → ↥s₂) p) : P) -ᵥ p ∈ s₁.directionᗮ
Tactic: rw [orthogonalProjection_eq_orthogonalProjection_iff_vsub_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
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
hp₁ : p₁ ∈ s
⊢ dist p₁ p₂ * dist p₁ p₂ =
    dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₂) : P) *
        dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₂) : P) +
      dist p₂ (↑((orthogonalProjection s : (a : P) → ↥s) p₂) : P) *
        dist p₂ (↑((orthogonalProjection s : (a : P) → ↥s) p₂) : P)
have h : inner 𝕜 (p₁ -ᵥ (↑((orthogonalProjection s : (a : P) → ↥s) p₂) : P))
    ((↑((orthogonalProjection s : (a : P) → ↥s) p₂) : P) -ᵥ p₂) =
  0
Tactic: rw [dist_comm p₂ _, dist_eq_norm_vsub V p₁ _, dist_eq_norm_vsub V p₁ _, dist_eq_norm_vsub V _ p₂,
    ← vsub_add_vsub_cancel p₁ (orthogonalProjection s p₂) p₂,
    norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero (𝕜 := 𝕜)]
-- 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 : AffineSubspace 𝕜 P
inst_5 : s.direction.HasOrthogonalProjection
p₁ p₂ : P
hp₂ : p₂ ∈ s
⊢ dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = dist p₁ p₂ ↔
    (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂
have this : Nonempty.{u_3 + 1} ↥s
Tactic: haveI : Nonempty s := ⟨p₂, 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 : AffineSubspace 𝕜 P
inst_5 : s.direction.HasOrthogonalProjection
p₁ p₂ : P
hp₂ : p₂ ∈ s
this : Nonempty.{u_3 + 1} ↥s
⊢ dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = dist p₁ p₂ ↔
    (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂
have mp : dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = dist p₁ p₂ →
  (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : 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 : AffineSubspace 𝕜 P
inst_5 : s.direction.HasOrthogonalProjection
p₁ p₂ : P
hp₂ : p₂ ∈ s
this : Nonempty.{u_3 + 1} ↥s
mp :
  dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = dist p₁ p₂ →
    (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂
⊢ dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = dist p₁ p₂ ↔
    (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂
have mpr : (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂ →
  dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = dist 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 : AffineSubspace 𝕜 P
inst_5 : s.direction.HasOrthogonalProjection
p₁ p₂ : P
hp₂ : p₂ ∈ s
this : Nonempty.{u_3 + 1} ↥s
h : dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = dist p₁ p₂
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂
have mp : ∀
  (h :
    HPow.hPow (β := ℕ) (dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P)) 2 =
      HPow.hPow (β := ℕ) (dist p₁ p₂) 2),
  (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂
Tactic: rwa [← sq_eq_sq₀ dist_nonneg dist_nonneg, pow_two, pow_two, dist_comm _ p₂,
      dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq _ hp₂,
      right_eq_add, mul_eq_zero, dist_eq_zero, or_self, eq_comm] 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 : AffineSubspace 𝕜 P
inst_5 : s.direction.HasOrthogonalProjection
p₁ p₂ : P
hp₂ : p₂ ∈ s
this : Nonempty.{u_3 + 1} ↥s
h : dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = dist p₁ p₂
mp :
  ∀
    (h :
      HPow.hPow (β := ℕ) (dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P)) 2 =
        HPow.hPow (β := ℕ) (dist p₁ p₂) 2),
    (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂
have mp₁ : ∀
  (h :
    dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) *
        dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) =
      HPow.hPow (β := ℕ) (dist p₁ p₂) 2),
  (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂
Tactic: rwa [← sq_eq_sq₀ dist_nonneg dist_nonneg, pow_two, pow_two, dist_comm _ p₂,
      dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq _ hp₂,
      right_eq_add, mul_eq_zero, dist_eq_zero, or_self, eq_comm] 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 : AffineSubspace 𝕜 P
inst_5 : s.direction.HasOrthogonalProjection
p₁ p₂ : P
hp₂ : p₂ ∈ s
this : Nonempty.{u_3 + 1} ↥s
h : dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = dist p₁ p₂
mp :
  ∀
    (h :
      HPow.hPow (β := ℕ) (dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P)) 2 =
        HPow.hPow (β := ℕ) (dist p₁ p₂) 2),
    (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂
mp₁ :
  ∀
    (h :
      dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) *
          dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) =
        HPow.hPow (β := ℕ) (dist p₁ p₂) 2),
    (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂
⊢ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂
have mp₂ : ∀
  (h :
    dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) *
        dist p₁ (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) =
      dist p₁ p₂ * dist p₁ p₂),
  (↑((orthogonalProjection s : (a : P) → ↥s) p₁) : P) = p₂
Tactic: rwa [← sq_eq_sq₀ dist_nonneg dist_nonneg, pow_two, pow_two, dist_comm _ p₂,
      dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq _ hp₂,
      right_eq_add, mul_eq_zero, dist_eq_zero, or_self, eq_comm] at h
Cleared hypotheses: h