awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
refine :
  Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (Set.range s.points)))
    ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter))
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
    ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter)

Tactic:
refine AffineSubspace.vadd_mem_of_mem_direction ?_ s.circumcenter_mem_affineSpan

Premises used: Affine.Simplex.circumcenter_mem_affineSpan, AffineSubspace.vadd_mem_of_mem_direction
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
h : Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (Set.range s.points))) (s.centroid -ᵥ s.circumcenter)
⊢ Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (Set.range s.points)))
    ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter))

Tactic:
apply Submodule.smul_mem

Premises used: Submodule.smul_mem
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
⊢ Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (Set.range s.points))) (s.centroid -ᵥ s.circumcenter)

Tactic:
AffineSubspace.vsub_mem_direction s.centroid_mem_affineSpan s.circumcenter_mem_affineSpan

Premises used: Affine.Simplex.circumcenter_mem_affineSpan, Set.Mem, AffineSubspace.vsub_mem_direction, Affine.Simplex.centroid_mem_affineSpan
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
⊢ Membership.mem (γ := Submodule ℝ V) (direction (affineSpan ℝ (Set.range s.points))) (s.centroid -ᵥ s.circumcenter)

Tactic:
exact AffineSubspace.vsub_mem_direction s.centroid_mem_affineSpan s.circumcenter_mem_affineSpan

Premises used: Affine.Simplex.circumcenter_mem_affineSpan, AffineSubspace.vsub_mem_direction, Affine.Simplex.centroid_mem_affineSpan
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
⊢ s.ninePointCircle.radius = s.circumradius / (↑n : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
m n : ℕ
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
⊢ n = m

Tactic:
simpa using Fin.equiv_iff_eq.mp ⟨e⟩

Premises used: Nonempty.intro, Iff.mp, Fin.equiv_iff_eq
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
m n : ℕ
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
⊢ n = m

Tactic:
have h : n = m := by simpa using Fin.equiv_iff_eq.mp ⟨e⟩
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
m n : ℕ
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
h : n = m
center : (s.reindex e).ninePointCircle.center = s.ninePointCircle.center
radius : (s.reindex e).ninePointCircle.radius = s.ninePointCircle.radius
⊢ (s.reindex e).ninePointCircle = s.ninePointCircle

Tactic:
ext
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
m n : ℕ
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
h : n = m
⊢ (s.reindex e).ninePointCircle.center = s.ninePointCircle.center

Tactic:
simp [ninePointCircle_center, centroid_reindex, h]

Premises used: Affine.Simplex.centroid_reindex, Affine.Simplex.ninePointCircle_center
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
m n : ℕ
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
h : n = m
⊢ (s.reindex e).ninePointCircle.radius = s.ninePointCircle.radius

Tactic:
simp [ninePointCircle_radius, h]

Premises used: Affine.Simplex.ninePointCircle_radius
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
center :
  (s.map f.toAffineMap ⋯).ninePointCircle.center =
    Sphere.center { center := (f : (a : P) → P₂) s.ninePointCircle.center, radius := s.ninePointCircle.radius }
radius :
  (s.map f.toAffineMap ⋯).ninePointCircle.radius =
    Sphere.radius.{u_4} (P := P₂)
      ({ center := (f : (a : P) → P₂) s.ninePointCircle.center, radius := s.ninePointCircle.radius } : Sphere P₂)
⊢ (s.map f.toAffineMap ⋯).ninePointCircle =
    { center := (f : (a : P) → P₂) s.ninePointCircle.center, radius := s.ninePointCircle.radius }

Tactic:
ext
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
⊢ (s.map f.toAffineMap ⋯).ninePointCircle.center =
    Sphere.center { center := (f : (a : P) → P₂) s.ninePointCircle.center, radius := s.ninePointCircle.radius }

Tactic:
simp [ninePointCircle_center, centroid_map]

Premises used: Affine.Simplex.centroid_map, Affine.Simplex.ninePointCircle_center
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
⊢ (s.map f.toAffineMap ⋯).ninePointCircle.radius =
    Sphere.radius.{u_4} (P := P₂)
      ({ center := (f : (a : P) → P₂) s.ninePointCircle.center, radius := s.ninePointCircle.radius } : Sphere P₂)

Tactic:
simp [ninePointCircle_radius]

Premises used: Affine.Simplex.ninePointCircle_radius
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
center :
  (↑(Sphere.center ((s.restrict S hS).ninePointCircle (n := n))) : P) =
    (↑(Sphere.center
          { center := Subtype.mk (p := fun (x : P) ↦ x ∈ S) s.ninePointCircle.center ⋯,
            radius := s.ninePointCircle.radius : Sphere ↥S }) :
      P)
radius :
  Sphere.radius.{u_2} (P := ↥S) ((s.restrict S hS).ninePointCircle (n := n)) =
    Sphere.radius
      { center := Subtype.mk (p := fun (x : P) ↦ x ∈ S) s.ninePointCircle.center ⋯, radius := s.ninePointCircle.radius }
⊢ Eq (α := Sphere ↥S) ((s.restrict S hS).ninePointCircle (n := n))
    { center := Subtype.mk (p := fun (x : P) ↦ x ∈ S) s.ninePointCircle.center ⋯, radius := s.ninePointCircle.radius }

Tactic:
ext
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
⊢ (↑(Sphere.center ((s.restrict S hS).ninePointCircle (n := n))) : P) =
    (↑(Sphere.center
          { center := Subtype.mk (p := fun (x : P) ↦ x ∈ S) s.ninePointCircle.center ⋯,
            radius := s.ninePointCircle.radius : Sphere ↥S }) :
      P)

Tactic:
simp [ninePointCircle_center, centroid_restrict]

Premises used: Affine.Simplex.centroid_restrict, Affine.Simplex.ninePointCircle_center
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
⊢ Sphere.radius.{u_2} (P := ↥S) ((s.restrict S hS).ninePointCircle (n := n)) =
    Sphere.radius
      { center := Subtype.mk (p := fun (x : P) ↦ x ∈ S) s.ninePointCircle.center ⋯, radius := s.ninePointCircle.radius }

Tactic:
simp [ninePointCircle_radius]

Premises used: Affine.Simplex.ninePointCircle_radius
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
rw :
  dist (s.faceOppositeCentroid i)
      ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter) =
    dist s.circumcenter (s.points i) / (↑n : ℝ)
⊢ s.faceOppositeCentroid i ∈ s.ninePointCircle

Tactic:
rw [mem_sphere, ninePointCircle_center, ninePointCircle_radius,
    ← dist_circumcenter_eq_circumradius' s i]

Premises used: Affine.Simplex.ninePointCircle_radius, Affine.Simplex.dist_circumcenter_eq_circumradius', EuclideanGeometry.mem_sphere, Affine.Simplex.ninePointCircle_center
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
simp_rw :
  ‖s.faceOppositeCentroid i -ᵥ
        ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter)‖ =
    ‖s.circumcenter -ᵥ s.points i‖ / (↑n : ℝ)
⊢ dist (s.faceOppositeCentroid i)
      ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter) =
    dist s.circumcenter (s.points i) / (↑n : ℝ)

Tactic:
simp_rw [dist_eq_norm_vsub]

Premises used: dist_eq_norm_vsub
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ Ne (α := ℝ) (↑n : ℝ) 0

Tactic:
simpa using NeZero.ne n

Premises used: NeZero.ne
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
rw :
  (↑n : ℝ) *
      ‖s.faceOppositeCentroid i -ᵥ
          ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter)‖ =
    ‖s.circumcenter -ᵥ s.points i‖
⊢ ‖s.faceOppositeCentroid i -ᵥ
        ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter)‖ =
    ‖s.circumcenter -ᵥ s.points i‖ / (↑n : ℝ)

Tactic:
rw [eq_div_iff_mul_eq (by simpa using NeZero.ne n), mul_comm]

Premises used: eq_div_iff_mul_eq, mul_comm
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ (↑n : ℝ) = norm (E := ℝ) (↑n : ℝ)

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
nth_rw :
  norm (E := ℝ) (↑n : ℝ) *
      ‖s.faceOppositeCentroid i -ᵥ
          ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter)‖ =
    ‖s.circumcenter -ᵥ s.points i‖
⊢ (↑n : ℝ) *
      ‖s.faceOppositeCentroid i -ᵥ
          ((HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter)‖ =
    ‖s.circumcenter -ᵥ s.points i‖

Tactic:
nth_rw 1 [show (n : ℝ) = ‖(n : ℝ)‖ by simp]
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
a :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.medial.points)) s.ninePointCircle.center ∧
    Set.range s.medial.points ⊆ Metric.sphere s.ninePointCircle.center s.ninePointCircle.radius
⊢ s.ninePointCircle = s.medial.circumsphere

Tactic:
apply s.medial.circumsphere_unique_dist_eq.2

Premises used: Affine.Simplex.circumsphere_unique_dist_eq, Affine.Simplex.medial, And.right
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
a : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.medial.points)) s.ninePointCircle.center
a₁ : Set.range s.medial.points ⊆ Metric.sphere s.ninePointCircle.center s.ninePointCircle.radius
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.medial.points)) s.ninePointCircle.center ∧
    Set.range s.medial.points ⊆ Metric.sphere s.ninePointCircle.center s.ninePointCircle.radius

Tactic:
constructor
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.medial.points)) s.ninePointCircle.center

Tactic:
simpa using s.ninePointCircle_center_mem_affineSpan

Premises used: Affine.Simplex.ninePointCircle_center_mem_affineSpan
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
a : ∀ (y : Fin (n + 1)), s.medial.points y ∈ Metric.sphere s.ninePointCircle.center s.ninePointCircle.radius
⊢ Set.range s.medial.points ⊆ Metric.sphere s.ninePointCircle.center s.ninePointCircle.radius

Tactic:
rw [Set.range_subset_iff]

Premises used: Set.range_subset_iff
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
⊢ ∀ (y : Fin (n + 1)), s.medial.points y ∈ Metric.sphere s.ninePointCircle.center s.ninePointCircle.radius

Tactic:
simpa [medial_points] using s.faceOppositeCentroid_mem_ninePointCircle

Premises used: Affine.Simplex.medial_points, Affine.Simplex.faceOppositeCentroid_mem_ninePointCircle
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
m n : ℕ
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
h : n = m
h₁ : ∀ (i : Fin (m + 1)), (s.reindex e).eulerPoint i = (s.eulerPoint ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) i
⊢ (s.reindex e).eulerPoint = s.eulerPoint ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))

Tactic:
ext i
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
m n : ℕ
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
h : n = m
i : Fin (m + 1)
⊢ (s.reindex e).eulerPoint i = (s.eulerPoint ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) i

Tactic:
simp [eulerPoint, h]

Premises used: Affine.Simplex.eulerPoint
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
i : Fin (n + 1)
⊢ (s.map f.toAffineMap ⋯).eulerPoint i = (f : (a : P) → P₂) (s.eulerPoint i)

Tactic:
simp [eulerPoint]

Premises used: Affine.Simplex.eulerPoint
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
i : Fin (n + 1)
⊢ Nonempty.{u_2 + 1} ↥S

Tactic:
haveI := Nonempty.map (AffineSubspace.inclusion hS) inferInstance
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
i : Fin (n + 1)
this : Nonempty.{u_2 + 1} ↥S
⊢ (↑((s.restrict S hS).eulerPoint i) : P) = s.eulerPoint i

Tactic:
simp [eulerPoint]

Premises used: Affine.Simplex.eulerPoint
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
i : Fin (n + 1)
rw :
  s.points i -ᵥ s.mongePoint - HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.points i -ᵥ s.mongePoint) =
    (HSub.hSub (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.points i -ᵥ s.mongePoint)
⊢ s.points i -ᵥ s.eulerPoint i = (HSub.hSub (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.points i -ᵥ s.mongePoint)

Tactic:
rw [eulerPoint, vsub_vadd_eq_vsub_sub]

Premises used: Affine.Simplex.eulerPoint, vsub_vadd_eq_vsub_sub
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
i : Fin (n + 1)
pos :
  ∀ (hn : n = 0),
    s.points i -ᵥ s.mongePoint - HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.points i -ᵥ s.mongePoint) =
      (HSub.hSub (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.points i -ᵥ s.mongePoint)
neg :
  ∀ (hn : ¬n = 0),
    s.points i -ᵥ s.mongePoint - HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.points i -ᵥ s.mongePoint) =
      (HSub.hSub (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.points i -ᵥ s.mongePoint)
⊢ s.points i -ᵥ s.mongePoint - HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.points i -ᵥ s.mongePoint) =
    (HSub.hSub (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.points i -ᵥ s.mongePoint)

Tactic:
by_cases hn : n = 0
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
i : Fin (n + 1)
hn : n = 0
pos :
  ∀ (s : Simplex ℝ P 0) (i : Fin (HAdd.hAdd (α := ℕ) 0 1)),
    s.points i -ᵥ s.mongePoint - HSMul.hSMul (α := ℝ) (↑0 : ℝ)⁻¹ (s.points i -ᵥ s.mongePoint) =
      (HSub.hSub (α := ℝ) (↑0 : ℝ) 1 / (↑0 : ℝ)) • (s.points i -ᵥ s.mongePoint)
⊢ s.points i -ᵥ s.mongePoint - HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.points i -ᵥ s.mongePoint) =
    (HSub.hSub (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.points i -ᵥ s.mongePoint)

Tactic:
obtain rfl := hn

Premises used: rfl
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
s : Simplex ℝ P 0
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
⊢ Subsingleton (Fin (HAdd.hAdd (α := ℕ) 0 1))

Tactic:
have : Subsingleton (Fin (0 + 1)) := inferInstanceAs (Subsingleton (Fin 1))
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
s : Simplex ℝ P 0
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
this : Subsingleton (Fin (HAdd.hAdd (α := ℕ) 0 1))
⊢ i = 0

Tactic:
have hi : i = 0 := Subsingleton.eq_zero i
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
s : Simplex ℝ P 0
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
this : Subsingleton (Fin (HAdd.hAdd (α := ℕ) 0 1))
hi : i = 0
⊢ Set.range s.points = {s.points i}

Tactic:
simp [hi]
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
s : Simplex ℝ P 0
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
this : Subsingleton (Fin (HAdd.hAdd (α := ℕ) 0 1))
hi : i = 0
⊢ Set.range s.points = {s.points i}

Tactic:
have hrange : Set.range s.points = {s.points i} := by simp [hi]
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
s : Simplex ℝ P 0
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
this : Subsingleton (Fin (HAdd.hAdd (α := ℕ) 0 1))
hi : i = 0
hrange : Set.range s.points = {s.points i}
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) s.mongePoint

Tactic:
obtain hmonge := s.mongePoint_mem_affineSpan

Premises used: Affine.Simplex.mongePoint_mem_affineSpan
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
s : Simplex ℝ P 0
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
this : Subsingleton (Fin (HAdd.hAdd (α := ℕ) 0 1))
hi : i = 0
hrange : Set.range s.points = {s.points i}
hmonge : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) s.mongePoint
⊢ s.mongePoint = s.points i

Tactic:
rw [hrange, mem_affineSpan_singleton] at hmonge

Premises used: AffineSubspace.mem_affineSpan_singleton
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
s : Simplex ℝ P 0
i : Fin (HAdd.hAdd (α := ℕ) 0 1)
this : Subsingleton (Fin (HAdd.hAdd (α := ℕ) 0 1))
hi : i = 0
hrange : Set.range s.points = {s.points i}
hmonge : s.mongePoint = s.points i
⊢ s.points i -ᵥ s.mongePoint - HSMul.hSMul (α := ℝ) (↑0 : ℝ)⁻¹ (s.points i -ᵥ s.mongePoint) =
    (HSub.hSub (α := ℝ) (↑0 : ℝ) 1 / (↑0 : ℝ)) • (s.points i -ᵥ s.mongePoint)

Tactic:
simp [hmonge]
-- Module: Mathlib.Geometry.Euclidean.NinePointCircle
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
i : Fin (n + 1)
hn : ¬n = 0
⊢ Ne (α := ℝ) (↑n : ℝ) 0

Tactic:
simpa using hn