awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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)
⊢ ∀ (i : { i : Fin (n + 3) // i₁ ≠ i }),
    Membership.mem (γ := Submodule ℝ V) (ℝ ∙ (s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))))ᗮ (p -ᵥ s.mongePoint)

Tactic:
exact fun i => (Submodule.mem_inf.1 (h' i i.property)).1
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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)

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
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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)
⊢ 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

Premises used: Submodule.span_iUnion, Submodule.iInf_orthogonal
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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)
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₁}))
⊢ 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₁}))

Tactic:
rw [Set.image_image]

Premises used: Set.image_image
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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)
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
⊢ 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:
ext x
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
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
⊢ 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:
simp_rw [Set.mem_iUnion, Set.mem_image, Set.mem_singleton_iff, Set.mem_diff_singleton]

Premises used: Set.mem_iUnion, Set.mem_image, Set.mem_singleton_iff, Set.mem_diff_singleton
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
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
h₂ :
  (∃ (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) →
    ∃ (i : { i : Fin (n + 3) // i₁ ≠ i }), x = s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))
⊢ (∃ (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:
constructor
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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)
i : { i : Fin (n + 3) // i₁ ≠ i }
w : Fin (n + 2 + 1)
left : Membership.mem (γ := Set (Fin (n + 2 + 1))) Set.univ (↑i : Fin (n + 3)) ∧ (↑i : Fin (n + 3)) ≠ i₁
right : s.points i₁ -ᵥ s.points (↑i : Fin (n + 3)) = s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))
⊢ ∃ (x : Fin (n + 2 + 1)),
    (Membership.mem (γ := Set (Fin (n + 2 + 1))) Set.univ x ∧ x ≠ i₁) ∧
      s.points i₁ -ᵥ s.points x = s.points i₁ -ᵥ s.points (↑i : Fin (n + 3))

Tactic:
use i, ⟨Set.mem_univ _, i.property.symm⟩
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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_1 :
  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)
i : Fin (n + 2 + 1)
hi : i ≠ i₁
w : { i : Fin (n + 3) // i₁ ≠ i }
h₁ :
  s.points i₁ -ᵥ s.points i =
    s.points i₁ -ᵥ s.points (↑(Subtype.mk (p := fun (i : Fin (n + 3)) ↦ i₁ ≠ i) i ⋯) : Fin (n + 3))
⊢ ∃ (i_1 : { i : Fin (n + 3) // i₁ ≠ i }), s.points i₁ -ᵥ s.points i = s.points i₁ -ᵥ s.points (↑i_1 : Fin (n + 3))

Tactic:
use ⟨i, hi.symm⟩
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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₁}))

Tactic:
have hu :
    ⋃ i : { i // i₁ ≠ i }, ({s.points i₁ -ᵥ s.points i} : Set V) =
      (s.points i₁ -ᵥ ·) '' s.points '' (Set.univ \ {i₁}) := by
    rw [Set.image_image]
    ext x
    simp_rw [Set.mem_iUnion, Set.mem_image, Set.mem_singleton_iff, Set.mem_diff_singleton]
    constructor
    · rintro ⟨i, rfl⟩
      use i, ⟨Set.mem_univ _, i.property.symm⟩
    · rintro ⟨i, ⟨-, hi⟩, rfl⟩
      use ⟨i, hi.symm⟩
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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)
hu :
  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₁}))
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))ᗮ (p -ᵥ s.mongePoint)

Tactic:
rw [hu, ← vectorSpan_image_eq_span_vsub_set_left_ne ℝ _ (Set.mem_univ _), Set.image_univ] at hi

Premises used: Set.image_univ, Real, vectorSpan_image_eq_span_vsub_set_left_ne, Set.mem_univ
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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)
hu :
  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₁}))
hi₁ : Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))ᗮ (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₁}))

Tactic:
rw [hu, ← vectorSpan_image_eq_span_vsub_set_left_ne ℝ _ (Set.mem_univ _), Set.image_univ] at hi

Premises used: Set.image_univ, Real, vectorSpan_image_eq_span_vsub_set_left_ne, Set.mem_univ
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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) (vectorSpan ℝ (Set.range s.points))ᗮ (p -ᵥ s.mongePoint)
hu :
  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₁}))
s₁ : Finset (Fin (n + 3)) := erase univ i₁
⊢ 0 < #s₁

Tactic:
simp [s₁, card_erase_of_mem]

Premises used: Finset.card_erase_of_mem
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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) (vectorSpan ℝ (Set.range s.points))ᗮ (p -ᵥ s.mongePoint)
hu :
  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₁}))
s₁ : Finset (Fin (n + 3)) := erase univ i₁
obtain :
  ∀ (i₂ : Fin (n + 3)) (h₂ : i₂ ∈ s₁),
    Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points)) (p -ᵥ s.mongePoint)
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points)) (p -ᵥ s.mongePoint)

Tactic:
obtain ⟨i₂, h₂⟩ := card_pos.1 (show 0 < #s₁ by simp [s₁, card_erase_of_mem])

Premises used: Iff.mp, Finset.card_pos
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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) (vectorSpan ℝ (Set.range s.points))ᗮ (p -ᵥ s.mongePoint)
hu :
  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₁}))
s₁ : Finset (Fin (n + 3)) := erase univ i₁
i₂ : Fin (n + 3)
h₂ : i₂ ∈ s₁
⊢ i₁ ≠ i₂

Tactic:
have h₁₂ : i₁ ≠ i₂ := (ne_of_mem_erase h₂).symm
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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) (vectorSpan ℝ (Set.range s.points))ᗮ (p -ᵥ s.mongePoint)
hu :
  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₁}))
s₁ : Finset (Fin (n + 3)) := erase univ i₁
i₂ : Fin (n + 3)
h₂ : i₂ ∈ s₁
h₁₂ : i₁ ≠ i₂
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points)) (p -ᵥ s.mongePoint)

Tactic:
(Submodule.mem_inf.1 (h' i₂ h₁₂)).2

Premises used: Set.Mem, setOf, Submodule.mem_inf, And.right, Iff.mp
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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) (vectorSpan ℝ (Set.range s.points))ᗮ (p -ᵥ s.mongePoint)
hu :
  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₁}))
s₁ : Finset (Fin (n + 3)) := erase univ i₁
i₂ : Fin (n + 3)
h₂ : i₂ ∈ s₁
h₁₂ : i₁ ≠ i₂
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points)) (p -ᵥ s.mongePoint)

Tactic:
exact (Submodule.mem_inf.1 (h' i₂ h₁₂)).2

Premises used: Submodule.mem_inf, And.right, Iff.mp
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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) (vectorSpan ℝ (Set.range s.points))ᗮ (p -ᵥ s.mongePoint)
hu :
  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₁}))
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points)) (p -ᵥ s.mongePoint)

Tactic:
have hv : p -ᵥ s.mongePoint ∈ vectorSpan ℝ (Set.range s.points) := by
    let s₁ : Finset (Fin (n + 3)) := univ.erase i₁
    obtain ⟨i₂, h₂⟩ := card_pos.1 (show 0 < #s₁ by simp [s₁, card_erase_of_mem])
    have h₁₂ : i₁ ≠ i₂ := (ne_of_mem_erase h₂).symm
    exact (Submodule.mem_inf.1 (h' i₂ h₁₂)).2
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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) (vectorSpan ℝ (Set.range s.points))ᗮ (p -ᵥ s.mongePoint)
hu :
  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₁}))
hv : Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points)) (p -ᵥ s.mongePoint)
⊢ p -ᵥ s.mongePoint = 0

Tactic:
Submodule.disjoint_def.1 (vectorSpan ℝ (Set.range s.points)).orthogonal_disjoint _ hv hi

Premises used: Affine.Simplex.points, Real, Submodule.orthogonal_disjoint, vectorSpan, Iff.mp, Set.range, Submodule.disjoint_def
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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) (vectorSpan ℝ (Set.range s.points))ᗮ (p -ᵥ s.mongePoint)
hu :
  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₁}))
hv : Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points)) (p -ᵥ s.mongePoint)
⊢ p -ᵥ s.mongePoint = 0

Tactic:
exact Submodule.disjoint_def.1 (vectorSpan ℝ (Set.range s.points)).orthogonal_disjoint _ hv hi

Premises used: Affine.Simplex.points, Real, Submodule.orthogonal_disjoint, vectorSpan, Iff.mp, Set.range, Submodule.disjoint_def
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
t : Triangle ℝ P
⊢ t.orthocenter = mongePoint t

Tactic:
rfl

Premises used: Affine.Triangle.orthocenter, rfl
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
t : Triangle ℝ P
e : Fin 3 ≃ Fin 3
⊢ orthocenter (reindex t e) = t.orthocenter

Tactic:
t.mongePoint_reindex e

Premises used: Affine.Triangle.orthocenter, Affine.Simplex.mongePoint_reindex
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
t : Triangle ℝ P
rw :
  HDiv.hDiv (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 2 1) : ℝ) (↑(HSub.hSub (α := ℕ) 2 1) : ℝ) •
        (Finset.centroid ℝ univ t.points -ᵥ circumcenter t) +ᵥ
      circumcenter t =
    HSMul.hSMul (α := ℝ) 3 (Finset.centroid ℝ univ t.points -ᵥ circumcenter t) +ᵥ circumcenter t
⊢ t.orthocenter = HSMul.hSMul (α := ℝ) 3 (Finset.centroid ℝ univ t.points -ᵥ circumcenter t) +ᵥ circumcenter t

Tactic:
rw [orthocenter_eq_mongePoint, mongePoint_eq_smul_vsub_vadd_circumcenter]

Premises used: Affine.Simplex.mongePoint_eq_smul_vsub_vadd_circumcenter, Affine.Triangle.orthocenter_eq_mongePoint
-- Module: Mathlib.Geometry.Euclidean.MongePoint
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
t : Triangle ℝ P
⊢ HDiv.hDiv (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 2 1) : ℝ) (↑(HSub.hSub (α := ℕ) 2 1) : ℝ) •
        (Finset.centroid ℝ univ t.points -ᵥ circumcenter t) +ᵥ
      circumcenter t =
    HSMul.hSMul (α := ℝ) 3 (Finset.centroid ℝ univ t.points -ᵥ circumcenter t) +ᵥ circumcenter t

Tactic:
simp