awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
e_a : Eq (α := Finset (Fin (n + 3))) {i₁, i₂}ᶜ {i₂, i₁}ᶜ
⊢ Eq (α := AffineSubspace ℝ P)
    (mk' (Finset.centroid ℝ {i₁, i₂}ᶜ s.points) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ affineSpan ℝ (Set.range s.points))
    (mk' (Finset.centroid ℝ {i₂, i₁}ᶜ s.points) (ℝ ∙ (s.points i₂ -ᵥ s.points i₁))ᗮ ⊓ affineSpan ℝ (Set.range s.points))
have e_a₁ : Eq (α := Submodule ℝ V) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂)) (ℝ ∙ (s.points i₂ -ᵥ s.points i₁))
Tactic: congr 3
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
⊢ Eq (α := Finset (Fin (n + 3))) {i₁, i₂}ᶜ {i₂, i₁}ᶜ
have e_a : Eq (α := Finset (Fin (n + 3))) {i₁, i₂} {i₂, i₁}
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
⊢ Eq (α := Submodule ℝ V) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂)) (ℝ ∙ (s.points i₂ -ᵥ s.points i₁))
have e_a : ∀ (x : V),
  Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂)) x ↔
    Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (s.points i₂ -ᵥ s.points i₁)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
x : V
⊢ Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂)) x ↔
    Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (s.points i₂ -ᵥ s.points i₁)) x
have e_a : (∃ (a : ℝ), a • (s.points i₁ -ᵥ s.points i₂) = x) ↔ ∃ (a : ℝ), a • (s.points i₂ -ᵥ s.points i₁) = x
Tactic: simp_rw [Submodule.mem_span_singleton]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
x : V
⊢ (∃ (a : ℝ), a • (s.points i₁ -ᵥ s.points i₂) = x) ↔ ∃ (a : ℝ), a • (s.points i₂ -ᵥ s.points i₁) = x
have e_a : (∃ (a : ℝ), a • (s.points i₁ -ᵥ s.points i₂) = x) → ∃ (a : ℝ), a • (s.points i₂ -ᵥ s.points i₁) = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
x : V
e_a : (∃ (a : ℝ), a • (s.points i₁ -ᵥ s.points i₂) = x) → ∃ (a : ℝ), a • (s.points i₂ -ᵥ s.points i₁) = x
⊢ (∃ (a : ℝ), a • (s.points i₁ -ᵥ s.points i₂) = x) ↔ ∃ (a : ℝ), a • (s.points i₂ -ᵥ s.points i₁) = x
have e_a₁ : (∃ (a : ℝ), a • (s.points i₂ -ᵥ s.points i₁) = x) → ∃ (a : ℝ), a • (s.points i₁ -ᵥ s.points i₂) = x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
r : ℝ
⊢ ∃ (a : ℝ), a • (s.points i₂ -ᵥ s.points i₁) = r • (s.points i₁ -ᵥ s.points i₂)
have h : -r • (s.points i₂ -ᵥ s.points i₁) = r • (s.points i₁ -ᵥ s.points i₂)
Tactic: use -r
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
r : ℝ
⊢ -r • (s.points i₂ -ᵥ s.points i₁) = r • (s.points i₁ -ᵥ s.points i₂)
have h : -(r • (s.points i₂ -ᵥ s.points i₁)) = r • (s.points i₁ -ᵥ s.points i₂)
Tactic: rw [neg_smul, ← smul_neg, neg_vsub_eq_vsub_rev]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
r : ℝ
h : -(r • (s.points i₂ -ᵥ s.points i₁)) = r • (s.points i₁ -ᵥ s.points i₂)
⊢ -r • (s.points i₂ -ᵥ s.points i₁) = r • (s.points i₁ -ᵥ s.points i₂)
have h₁ : r • -(s.points i₂ -ᵥ s.points i₁) = r • (s.points i₁ -ᵥ s.points i₂)
Tactic: rw [neg_smul, ← smul_neg, neg_vsub_eq_vsub_rev]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
r : ℝ
h : -(r • (s.points i₂ -ᵥ s.points i₁)) = r • (s.points i₁ -ᵥ s.points i₂)
h₁ : r • -(s.points i₂ -ᵥ s.points i₁) = r • (s.points i₁ -ᵥ s.points i₂)
⊢ -r • (s.points i₂ -ᵥ s.points i₁) = r • (s.points i₁ -ᵥ s.points i₂)
have h₂ : r • (s.points i₁ -ᵥ s.points i₂) = r • (s.points i₁ -ᵥ s.points i₂)
Tactic: rw [neg_smul, ← smul_neg, neg_vsub_eq_vsub_rev]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
r : ℝ
⊢ ∃ (a : ℝ), a • (s.points i₁ -ᵥ s.points i₂) = r • (s.points i₂ -ᵥ s.points i₁)
have h : -r • (s.points i₁ -ᵥ s.points i₂) = r • (s.points i₂ -ᵥ s.points i₁)
Tactic: use -r
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
r : ℝ
⊢ -r • (s.points i₁ -ᵥ s.points i₂) = r • (s.points i₂ -ᵥ s.points i₁)
have h : -(r • (s.points i₁ -ᵥ s.points i₂)) = r • (s.points i₂ -ᵥ s.points i₁)
Tactic: rw [neg_smul, ← smul_neg, neg_vsub_eq_vsub_rev]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
r : ℝ
h : -(r • (s.points i₁ -ᵥ s.points i₂)) = r • (s.points i₂ -ᵥ s.points i₁)
⊢ -r • (s.points i₁ -ᵥ s.points i₂) = r • (s.points i₂ -ᵥ s.points i₁)
have h₁ : r • -(s.points i₁ -ᵥ s.points i₂) = r • (s.points i₂ -ᵥ s.points i₁)
Tactic: rw [neg_smul, ← smul_neg, neg_vsub_eq_vsub_rev]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
r : ℝ
h : -(r • (s.points i₁ -ᵥ s.points i₂)) = r • (s.points i₂ -ᵥ s.points i₁)
h₁ : r • -(s.points i₁ -ᵥ s.points i₂) = r • (s.points i₂ -ᵥ s.points i₁)
⊢ -r • (s.points i₁ -ᵥ s.points i₂) = r • (s.points i₂ -ᵥ s.points i₁)
have h₂ : r • (s.points i₂ -ᵥ s.points i₁) = r • (s.points i₂ -ᵥ s.points i₁)
Tactic: rw [neg_smul, ← smul_neg, neg_vsub_eq_vsub_rev]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
⊢ s.mongePoint ∈ s.mongePlane i₁ i₂
have rw : (∀ (u : V),
    Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂)) u →
      ⟪s.mongePoint -ᵥ Finset.centroid ℝ {i₁, i₂}ᶜ s.points, u⟫ = 0) ∧
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) s.mongePoint
Tactic: rw [mongePlane_def, mem_inf_iff, ← vsub_right_mem_direction_iff_mem (self_mem_mk' _ _),
    direction_mk', Submodule.mem_orthogonal']
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
⊢ (∀ (u : V),
      Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂)) u →
        ⟪s.mongePoint -ᵥ Finset.centroid ℝ {i₁, i₂}ᶜ s.points, u⟫ = 0) ∧
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) s.mongePoint
have refine : ∀ (u : V),
  Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂)) u →
    ⟪s.mongePoint -ᵥ Finset.centroid ℝ {i₁, i₂}ᶜ s.points, u⟫ = 0
Tactic: refine ⟨?_, s.mongePoint_mem_affineSpan⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
v : V
hv : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂)) v
⊢ ⟪s.mongePoint -ᵥ Finset.centroid ℝ {i₁, i₂}ᶜ s.points, v⟫ = 0
have rcases : ∀ (r : ℝ)
  (hv : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂)) (r • (s.points i₁ -ᵥ s.points i₂))),
  ⟪s.mongePoint -ᵥ Finset.centroid ℝ {i₁, i₂}ᶜ s.points, r • (s.points i₁ -ᵥ s.points i₂)⟫ = 0
Tactic: rcases Submodule.mem_span_singleton.mp hv with ⟨r, rfl⟩
Cleared hypotheses: v, hv
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
r : ℝ
hv : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂)) (r • (s.points i₁ -ᵥ s.points i₂))
⊢ ⟪s.mongePoint -ᵥ Finset.centroid ℝ {i₁, i₂}ᶜ s.points, r • (s.points i₁ -ᵥ s.points i₂)⟫ = 0
have rw : r * ⟪s.mongePoint -ᵥ Finset.centroid ℝ {i₁, i₂}ᶜ s.points, s.points i₁ -ᵥ s.points i₂⟫ = 0
Tactic: rw [inner_smul_right, s.inner_mongePoint_vsub_face_centroid_vsub, mul_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
r : ℝ
hv : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂)) (r • (s.points i₁ -ᵥ s.points i₂))
rw : r * ⟪s.mongePoint -ᵥ Finset.centroid ℝ {i₁, i₂}ᶜ s.points, s.points i₁ -ᵥ s.points i₂⟫ = 0
⊢ ⟪s.mongePoint -ᵥ Finset.centroid ℝ {i₁, i₂}ᶜ s.points, r • (s.points i₁ -ᵥ s.points i₂)⟫ = 0
have rw₁ : r * 0 = 0
Tactic: rw [inner_smul_right, s.inner_mongePoint_vsub_face_centroid_vsub, mul_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
r : ℝ
hv : Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂)) (r • (s.points i₁ -ᵥ s.points i₂))
rw : r * ⟪s.mongePoint -ᵥ Finset.centroid ℝ {i₁, i₂}ᶜ s.points, s.points i₁ -ᵥ s.points i₂⟫ = 0
rw₁ : r * 0 = 0
⊢ ⟪s.mongePoint -ᵥ Finset.centroid ℝ {i₁, i₂}ᶜ s.points, r • (s.points i₁ -ᵥ s.points i₂)⟫ = 0
have rw₂ : Eq (α := ℝ) 0 0
Tactic: rw [inner_smul_right, s.inner_mongePoint_vsub_face_centroid_vsub, mul_zero]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
⊢ (s.mongePlane i₁ i₂).direction = (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
have rw : Eq (α := Submodule ℝ V)
  (direction
    (mk' (Finset.centroid ℝ {i₁, i₂}ᶜ s.points) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓
      affineSpan ℝ (Set.range s.points)))
  ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
Tactic: rw [mongePlane_def, direction_inf_of_mem_inf s.mongePoint_mem_mongePlane, direction_mk',
    direction_affineSpan]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
rw :
  Eq (α := Submodule ℝ V)
    (direction
      (mk' (Finset.centroid ℝ {i₁, i₂}ᶜ s.points) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓
        affineSpan ℝ (Set.range s.points)))
    ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
⊢ (s.mongePlane i₁ i₂).direction = (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
have rw₁ : Eq (α := Submodule ℝ V)
  (direction (mk' (Finset.centroid ℝ {i₁, i₂}ᶜ s.points) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ) ⊓
    direction (affineSpan ℝ (Set.range s.points)))
  ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
Tactic: rw [mongePlane_def, direction_inf_of_mem_inf s.mongePoint_mem_mongePlane, direction_mk',
    direction_affineSpan]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
rw :
  Eq (α := Submodule ℝ V)
    (direction
      (mk' (Finset.centroid ℝ {i₁, i₂}ᶜ s.points) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓
        affineSpan ℝ (Set.range s.points)))
    ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
rw₁ :
  Eq (α := Submodule ℝ V)
    (direction (mk' (Finset.centroid ℝ {i₁, i₂}ᶜ s.points) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ) ⊓
      direction (affineSpan ℝ (Set.range s.points)))
    ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
⊢ (s.mongePlane i₁ i₂).direction = (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
have rw₂ : Eq (α := Submodule ℝ V) ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ direction (affineSpan ℝ (Set.range s.points)))
  ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
Tactic: rw [mongePlane_def, direction_inf_of_mem_inf s.mongePoint_mem_mongePlane, direction_mk',
    direction_affineSpan]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ i₂ : Fin (n + 3)
rw :
  Eq (α := Submodule ℝ V)
    (direction
      (mk' (Finset.centroid ℝ {i₁, i₂}ᶜ s.points) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓
        affineSpan ℝ (Set.range s.points)))
    ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
rw₁ :
  Eq (α := Submodule ℝ V)
    (direction (mk' (Finset.centroid ℝ {i₁, i₂}ᶜ s.points) (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ) ⊓
      direction (affineSpan ℝ (Set.range s.points)))
    ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
rw₂ :
  Eq (α := Submodule ℝ V) ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ direction (affineSpan ℝ (Set.range s.points)))
    ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
⊢ (s.mongePlane i₁ i₂).direction = (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
have rw₃ : Eq (α := Submodule ℝ V) ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
  ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
Tactic: rw [mongePlane_def, direction_inf_of_mem_inf s.mongePoint_mem_mongePlane, direction_mk',
    direction_affineSpan]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
⊢ p = s.mongePoint
have rw : p -ᵥ s.mongePoint = 0
Tactic: rw [← @vsub_eq_zero_iff_eq V]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
i₂ : Fin (n + 3)
hne : i₁ ≠ i₂
⊢ Membership.mem (γ := Submodule ℝ V) ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
    (p -ᵥ s.mongePoint)
have rw : p ∈ s.mongePlane i₁ i₂
Tactic: rw [← s.direction_mongePlane, vsub_right_mem_direction_iff_mem s.mongePoint_mem_mongePlane]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
⊢ p -ᵥ s.mongePoint = 0
have h' : ∀ (i₂ : Fin (n + 3)),
  i₁ ≠ i₂ →
    Membership.mem (γ := Submodule ℝ V) ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
      (p -ᵥ s.mongePoint)
Tactic: have h' : ∀ i₂, i₁ ≠ i₂ → p -ᵥ s.mongePoint ∈
      (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points) := by
    intro i₂ hne
    rw [← s.direction_mongePlane, vsub_right_mem_direction_iff_mem s.mongePoint_mem_mongePlane]
    exact h i₂ hne
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ →
      Membership.mem (γ := Submodule ℝ V) ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
        (p -ᵥ s.mongePoint)
⊢ Membership.mem (γ := Submodule ℝ V)
    (⨅ (i₂ : { i : Fin (n + 3) // i₁ ≠ i }), (ℝ ∙ (s.points i₁ -ᵥ s.points (↑i₂ : Fin (n + 3))))ᗮ) (p -ᵥ s.mongePoint)
have rw : ∀ (i : { i : Fin (n + 3) // i₁ ≠ i }),
  Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))))ᗮ (p -ᵥ s.mongePoint)
Tactic: rw [Submodule.mem_iInf]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ →
      Membership.mem (γ := Submodule ℝ V) ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
        (p -ᵥ s.mongePoint)
⊢ p -ᵥ s.mongePoint = 0
have hi : Membership.mem (γ := Submodule ℝ V)
  (⨅ (i₂ : { i : Fin (n + 3) // i₁ ≠ i }), (ℝ ∙ (s.points i₁ -ᵥ s.points (↑i₂ : Fin (n + 3))))ᗮ) (p -ᵥ s.mongePoint)
Tactic: have hi : p -ᵥ s.mongePoint ∈ ⨅ i₂ : { i // i₁ ≠ i }, (ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ := by
    rw [Submodule.mem_iInf]
    exact fun i => (Submodule.mem_inf.1 (h' i i.property)).1
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (hypothesis)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ →
      Membership.mem (γ := Submodule ℝ V) ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
        (p -ᵥ s.mongePoint)
hi :
  Membership.mem (γ := Submodule ℝ V)
    (⨅ (i₂ : { i : Fin (n + 3) // i₁ ≠ i }), (ℝ ∙ (s.points i₁ -ᵥ s.points (↑i₂ : Fin (n + 3))))ᗮ) (p -ᵥ s.mongePoint)
⊢ p -ᵥ s.mongePoint = 0
have hi₁ : Membership.mem (γ := Submodule ℝ V)
  (Submodule.span ℝ (⋃ (i : { i : Fin (n + 3) // i₁ ≠ i }), {s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))}))ᗮ
  (p -ᵥ s.mongePoint)
Tactic: rw [Submodule.iInf_orthogonal, ← Submodule.span_iUnion] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ →
      Membership.mem (γ := Submodule ℝ V) ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
        (p -ᵥ s.mongePoint)
hi :
  Membership.mem (γ := Submodule ℝ V)
    (Submodule.span ℝ (⋃ (i : { i : Fin (n + 3) // i₁ ≠ i }), {s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))}))ᗮ
    (p -ᵥ s.mongePoint)
⊢ Eq.{u_1 + 1} (α := Set V) (⋃ (i : { i : Fin (n + 3) // i₁ ≠ i }), {s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))})
    ((fun (x : P) ↦ s.points i₁ -ᵥ x) '' s.points '' (Set.univ \ {i₁}))
have rw : Eq.{u_1 + 1} (α := Set V) (⋃ (i : { i : Fin (n + 3) // i₁ ≠ i }), {s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))})
  ((fun (x : Fin (n + 2 + 1)) ↦ s.points i₁ -ᵥ s.points x) '' (Set.univ \ {i₁}))
Tactic: rw [Set.image_image]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ →
      Membership.mem (γ := Submodule ℝ V) ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
        (p -ᵥ s.mongePoint)
hi :
  Membership.mem (γ := Submodule ℝ V)
    (Submodule.span ℝ (⋃ (i : { i : Fin (n + 3) // i₁ ≠ i }), {s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))}))ᗮ
    (p -ᵥ s.mongePoint)
⊢ Eq.{u_1 + 1} (α := Set V) (⋃ (i : { i : Fin (n + 3) // i₁ ≠ i }), {s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))})
    ((fun (x : Fin (n + 2 + 1)) ↦ s.points i₁ -ᵥ s.points x) '' (Set.univ \ {i₁}))
have h₁ : ∀ (x : V),
  Membership.mem (γ := Set V) (⋃ (i : { i : Fin (n + 3) // i₁ ≠ i }), {s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))}) x ↔
    Membership.mem (γ := Set V) ((fun (x : Fin (n + 2 + 1)) ↦ s.points i₁ -ᵥ s.points x) '' (Set.univ \ {i₁})) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.MongePoint (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P (n + 2)
i₁ : Fin (n + 3)
p : P
h : ∀ (i₂ : Fin (n + 3)), i₁ ≠ i₂ → p ∈ s.mongePlane i₁ i₂
h' :
  ∀ (i₂ : Fin (n + 3)),
    i₁ ≠ i₂ →
      Membership.mem (γ := Submodule ℝ V) ((ℝ ∙ (s.points i₁ -ᵥ s.points i₂))ᗮ ⊓ vectorSpan ℝ (Set.range s.points))
        (p -ᵥ s.mongePoint)
hi :
  Membership.mem (γ := Submodule ℝ V)
    (Submodule.span ℝ (⋃ (i : { i : Fin (n + 3) // i₁ ≠ i }), {s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))}))ᗮ
    (p -ᵥ s.mongePoint)
x : V
⊢ Membership.mem (γ := Set V) (⋃ (i : { i : Fin (n + 3) // i₁ ≠ i }), {s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))}) x ↔
    Membership.mem (γ := Set V) ((fun (x : Fin (n + 2 + 1)) ↦ s.points i₁ -ᵥ s.points x) '' (Set.univ \ {i₁})) x
have h₁ : (∃ (i : { i : Fin (n + 3) // i₁ ≠ i }), x = s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))) ↔
  ∃ (x_1 : Fin (n + 2 + 1)),
    (Membership.mem (γ := Set (Fin (n + 2 + 1))) Set.univ x_1 ∧ x_1 ≠ i₁) ∧ s.points i₁ -ᵥ s.points x_1 = x
Tactic: simp_rw [Set.mem_iUnion, Set.mem_image, Set.mem_singleton_iff, Set.mem_diff_singleton]