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
i : Fin (n + 1)
hn : ¬n = 0
rw : HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑n : ℝ) - HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) = HSub.hSub (α := ℝ) 1 (↑n : ℝ)⁻¹
rw₁ : 1 - HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) = HSub.hSub (α := ℝ) 1 (↑n : ℝ)⁻¹
rw₂ rw₃ : HSub.hSub (α := ℝ) 1 (↑n : ℝ)⁻¹ = HSub.hSub (α := ℝ) 1 (↑n : ℝ)⁻¹
⊢ HSub.hSub (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ) = HSub.hSub (α := ℝ) 1 (↑n : ℝ)⁻¹

Tactic:
rw [sub_div, div_self (by simpa using hn), one_div]

Premises used: sub_div, one_div, div_self
-- 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
⊢ HSub.hSub (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ) = HSub.hSub (α := ℝ) 1 (↑n : ℝ)⁻¹

Tactic:
have : ((n - 1) / n : ℝ) = 1 - (n : ℝ)⁻¹ := by
    rw [sub_div, div_self (by simpa using hn), one_div]
-- 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
this : HSub.hSub (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ) = HSub.hSub (α := ℝ) 1 (↑n : ℝ)⁻¹
neg :
  s.points i -ᵥ s.mongePoint - HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.points i -ᵥ s.mongePoint) =
    HSub.hSub (α := ℝ) 1 (↑n : ℝ)⁻¹ • (s.points i -ᵥ s.mongePoint)
neg₁ :
  s.points i -ᵥ s.mongePoint - HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.points i -ᵥ s.mongePoint) =
    HSMul.hSMul (α := ℝ) 1 (s.points i -ᵥ s.mongePoint) - HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.points i -ᵥ s.mongePoint)
neg₂ neg₃ :
  s.points i -ᵥ s.mongePoint - HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.points i -ᵥ s.mongePoint) =
    s.points i -ᵥ s.mongePoint - HSMul.hSMul (α := ℝ) (↑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:
rw [this, sub_smul, one_smul]

Premises used: sub_smul, one_smul
-- 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 : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
apply :
  midpoint ℝ (s.faceOppositeCentroid i) (s.eulerPoint i) -ᵥ s.circumcenter = s.ninePointCircle.center -ᵥ s.circumcenter
⊢ midpoint ℝ (s.faceOppositeCentroid i) (s.eulerPoint i) = s.ninePointCircle.center

Tactic:
apply vsub_left_cancel (p := s.circumcenter)

Premises used: vsub_left_cancel
-- 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 : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
rw :
  HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        (s.faceOppositeCentroid i -ᵥ s.circumcenter) +
      HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        ((HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
              (s.points i -ᵥ
                (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (s.centroid -ᵥ s.circumcenter) +ᵥ
                  s.circumcenter)) +ᵥ
            HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter) -ᵥ
          s.circumcenter) =
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
⊢ midpoint ℝ (s.faceOppositeCentroid i) (s.eulerPoint i) -ᵥ s.circumcenter = s.ninePointCircle.center -ᵥ s.circumcenter

Tactic:
rw [ninePointCircle_center, midpoint_vsub, vadd_vsub, eulerPoint,
    mongePoint_eq_smul_vsub_vadd_circumcenter, ← centroid]

Premises used: Affine.Simplex.eulerPoint, Affine.Simplex.mongePoint_eq_smul_vsub_vadd_circumcenter, Affine.Simplex.centroid, vadd_vsub, midpoint_vsub, 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 : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
pos :
  ∀ (hn1 : n = 1),
    HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
          (s.faceOppositeCentroid i -ᵥ s.circumcenter) +
        HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
          ((HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                (s.points i -ᵥ
                  (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (s.centroid -ᵥ s.circumcenter) +ᵥ
                    s.circumcenter)) +ᵥ
              HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter) -ᵥ
            s.circumcenter) =
      (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
neg :
  ∀ (hn1 : ¬n = 1),
    HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
          (s.faceOppositeCentroid i -ᵥ s.circumcenter) +
        HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
          ((HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
                (s.points i -ᵥ
                  (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (s.centroid -ᵥ s.circumcenter) +ᵥ
                    s.circumcenter)) +ᵥ
              HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter) -ᵥ
            s.circumcenter) =
      (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
⊢ HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        (s.faceOppositeCentroid i -ᵥ s.circumcenter) +
      HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        ((HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
              (s.points i -ᵥ
                (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (s.centroid -ᵥ s.circumcenter) +ᵥ
                  s.circumcenter)) +ᵥ
            HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter) -ᵥ
          s.circumcenter) =
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)

Tactic:
by_cases hn1 : n = 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
n : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : n = 1
pos :
  ∀ [hn : NeZero (R := ℕ) 1] (s : Simplex ℝ P 1) (i : Fin (HAdd.hAdd (α := ℕ) 1 1)),
    HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
          (s.faceOppositeCentroid i -ᵥ s.circumcenter) +
        HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
          ((HSMul.hSMul (α := ℝ) (↑1 : ℝ)⁻¹
                (s.points i -ᵥ
                  (HDiv.hDiv (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1) : ℝ) (↑(HSub.hSub (α := ℕ) 1 1) : ℝ) •
                      (s.centroid -ᵥ s.circumcenter) +ᵥ
                    s.circumcenter)) +ᵥ
              HDiv.hDiv (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1) : ℝ) (↑(HSub.hSub (α := ℕ) 1 1) : ℝ) •
                  (s.centroid -ᵥ s.circumcenter) +ᵥ
                s.circumcenter) -ᵥ
            s.circumcenter) =
      (HAdd.hAdd (α := ℝ) (↑1 : ℝ) 1 / (↑1 : ℝ)) • (s.centroid -ᵥ s.circumcenter)
⊢ HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        (s.faceOppositeCentroid i -ᵥ s.circumcenter) +
      HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        ((HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹
              (s.points i -ᵥ
                (HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (s.centroid -ᵥ s.circumcenter) +ᵥ
                  s.circumcenter)) +ᵥ
            HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑(n - 1) : ℝ) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter) -ᵥ
          s.circumcenter) =
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)

Tactic:
obtain rfl := hn1

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
hn : NeZero (R := ℕ) 1
s : Simplex ℝ P 1
i : Fin (HAdd.hAdd (α := ℕ) 1 1)
this :
  HSMul.hSMul (α := ℝ) 2⁻¹ (s.faceOppositeCentroid i -ᵥ s.centroid) +
      HSMul.hSMul (α := ℝ) 2⁻¹ (s.points i -ᵥ s.centroid) =
    0
⊢ HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        (s.faceOppositeCentroid i -ᵥ s.circumcenter) +
      HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        ((HSMul.hSMul (α := ℝ) (↑1 : ℝ)⁻¹
              (s.points i -ᵥ
                (HDiv.hDiv (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1) : ℝ) (↑(HSub.hSub (α := ℕ) 1 1) : ℝ) •
                    (s.centroid -ᵥ s.circumcenter) +ᵥ
                  s.circumcenter)) +ᵥ
            HDiv.hDiv (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1) : ℝ) (↑(HSub.hSub (α := ℕ) 1 1) : ℝ) •
                (s.centroid -ᵥ s.circumcenter) +ᵥ
              s.circumcenter) -ᵥ
          s.circumcenter) =
    (HAdd.hAdd (α := ℝ) (↑1 : ℝ) 1 / (↑1 : ℝ)) • (s.centroid -ᵥ s.circumcenter)

Tactic:
simpa [circumcenter_eq_centroid, centroid]

Premises used: Affine.Simplex.centroid, Affine.Simplex.circumcenter_eq_centroid
-- 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
hn : NeZero (R := ℕ) 1
s : Simplex ℝ P 1
i : Fin (HAdd.hAdd (α := ℕ) 1 1)
pos :
  HSMul.hSMul (α := ℝ) 2⁻¹ (s.faceOppositeCentroid i -ᵥ s.centroid) +
      HSMul.hSMul (α := ℝ) 2⁻¹ (s.points i -ᵥ s.centroid) =
    0
⊢ HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        (s.faceOppositeCentroid i -ᵥ s.circumcenter) +
      HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        ((HSMul.hSMul (α := ℝ) (↑1 : ℝ)⁻¹
              (s.points i -ᵥ
                (HDiv.hDiv (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1) : ℝ) (↑(HSub.hSub (α := ℕ) 1 1) : ℝ) •
                    (s.centroid -ᵥ s.circumcenter) +ᵥ
                  s.circumcenter)) +ᵥ
            HDiv.hDiv (α := ℝ) (↑(HAdd.hAdd (α := ℕ) 1 1) : ℝ) (↑(HSub.hSub (α := ℕ) 1 1) : ℝ) •
                (s.centroid -ᵥ s.circumcenter) +ᵥ
              s.circumcenter) -ᵥ
          s.circumcenter) =
    (HAdd.hAdd (α := ℝ) (↑1 : ℝ) 1 / (↑1 : ℝ)) • (s.centroid -ᵥ s.circumcenter)

Tactic:
suffices (2⁻¹ : ℝ) • (s.faceOppositeCentroid i -ᵥ s.centroid) +
        (2⁻¹ : ℝ) • (s.points i -ᵥ s.centroid) = 0 by
      simpa [circumcenter_eq_centroid, centroid]
-- 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
hn : NeZero (R := ℕ) 1
s : Simplex ℝ P 1
i : Fin (HAdd.hAdd (α := ℕ) 1 1)
pos :
  HSMul.hSMul (α := ℝ) 2⁻¹ (HSMul.hSMul (α := ℝ) (↑1 : ℝ)⁻¹ (s.centroid -ᵥ s.points i) + (s.points i -ᵥ s.centroid)) = 0
⊢ HSMul.hSMul (α := ℝ) 2⁻¹ (s.faceOppositeCentroid i -ᵥ s.centroid) +
      HSMul.hSMul (α := ℝ) 2⁻¹ (s.points i -ᵥ s.centroid) =
    0

Tactic:
rw [faceOppositeCentroid_vsub_centroid_eq_smul_vsub, ← smul_add]

Premises used: Affine.Simplex.faceOppositeCentroid_vsub_centroid_eq_smul_vsub, smul_add
-- 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
hn : NeZero (R := ℕ) 1
s : Simplex ℝ P 1
i : Fin (HAdd.hAdd (α := ℕ) 1 1)
⊢ HSMul.hSMul (α := ℝ) (↑1 : ℝ)⁻¹ (s.centroid -ᵥ s.points i) + (s.points i -ᵥ s.centroid) = 0

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
hn : NeZero (R := ℕ) 1
s : Simplex ℝ P 1
i : Fin (HAdd.hAdd (α := ℕ) 1 1)
⊢ HSMul.hSMul (α := ℝ) 2⁻¹ (HSMul.hSMul (α := ℝ) (↑1 : ℝ)⁻¹ (s.centroid -ᵥ s.points i) + (s.points i -ᵥ s.centroid)) = 0

Tactic:
exact (smul_eq_zero_of_right _ (by simp))

Premises used: smul_eq_zero_of_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 : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
⊢ n ≠ 0

Tactic:
have _ := hn.out
-- 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 : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
h : n ≠ 0
⊢ 1 < n

Tactic:
lia
-- 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 : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
⊢ 1 < n

Tactic:
have hltn : 1 < n := by
    have _ := hn.out
    lia
-- 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 : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
hltn : 1 < n
push_cast : HSub.hSub (α := ℝ) (↑n : ℝ) 1 = HSub.hSub (α := ℝ) (↑n : ℝ) 1
⊢ (↑(n - 1) : ℝ) = HSub.hSub (α := ℝ) (↑n : ℝ) 1

Tactic:
push_cast [hltn]
-- 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 : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
hltn : 1 < n
⊢ HSub.hSub (α := ℝ) (↑n : ℝ) 1 = HSub.hSub (α := ℝ) (↑n : ℝ) 1

Tactic:
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
n : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
hltn : 1 < n
⊢ (↑(n - 1) : ℝ) = HSub.hSub (α := ℝ) (↑n : ℝ) 1

Tactic:
have hnsub1 : (n - 1 : ℕ) = (n : ℝ) - 1 := by
    push_cast [hltn]
    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
n : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
hltn : 1 < n
hnsub1 : (↑(n - 1) : ℝ) = HSub.hSub (α := ℝ) (↑n : ℝ) 1
⊢ HSub.hSub (α := ℝ) (↑n : ℝ)⁻¹ 1 = -HSub.hSub (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)

Tactic:
field [hn.out]

Premises used: NeZero.out
-- 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 : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
hltn : 1 < n
hnsub1 : (↑(n - 1) : ℝ) = HSub.hSub (α := ℝ) (↑n : ℝ) 1
⊢ HSub.hSub (α := ℝ) (↑n : ℝ) 1 ≠ 0

Tactic:
simpa [sub_eq_zero] using hn1

Premises used: sub_eq_zero
-- 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 : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
hltn : 1 < n
hnsub1 : (↑(n - 1) : ℝ) = HSub.hSub (α := ℝ) (↑n : ℝ) 1
neg :
  HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) +
        (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)) =
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
⊢ HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) +
        HDiv.hDiv (α := ℝ) (↑(n + 1) : ℝ) (↑n : ℝ) • (s.centroid -ᵥ s.circumcenter)) =
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)

Tactic:
push_cast
-- 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 : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
hltn : 1 < n
hnsub1 : (↑(n - 1) : ℝ) = HSub.hSub (α := ℝ) (↑n : ℝ) 1
⊢ Ne (α := ℝ) (↑n : ℝ) 0

Tactic:
simpa using hn.out

Premises used: NeZero.out
-- 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 : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
hltn : 1 < n
hnsub1 : (↑(n - 1) : ℝ) = HSub.hSub (α := ℝ) (↑n : ℝ) 1
rw :
  HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
    (HAdd.hAdd (α := ℝ) 1 (↑n : ℝ) / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
rw₁ :
  HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
    (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) + HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
rw₂ :
  HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
    (HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) + 1) • (s.centroid -ᵥ s.circumcenter)
rw₃ :
  HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
    HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) • (s.centroid -ᵥ s.circumcenter) +
      HSMul.hSMul (α := ℝ) 1 (s.centroid -ᵥ s.circumcenter)
rw₄ :
  HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
    HDiv.hDiv (α := ℝ) 1 (↑n : ℝ) • (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter)
rw₅ rw₆ :
  HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
    HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter)
⊢ HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)

Tactic:
rw [add_comm (n : ℝ) 1, add_div, div_self (by simpa using hn.out), add_smul, one_smul, one_div]

Premises used: Nat.cast, add_comm, one_smul, add_smul, one_div, OfNat.ofNat, div_self, add_div
-- 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 : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
hltn : 1 < n
hnsub1 : (↑(n - 1) : ℝ) = HSub.hSub (α := ℝ) (↑n : ℝ) 1
⊢ HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)

Tactic:
have : (n : ℝ)⁻¹ • (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
      (((n + 1) / n : ℝ)) • (s.centroid -ᵥ s.circumcenter) := by
    rw [add_comm (n : ℝ) 1, add_div, div_self (by simpa using hn.out), add_smul, one_smul, one_div]
-- 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 : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
hltn : 1 < n
hnsub1 : (↑(n - 1) : ℝ) = HSub.hSub (α := ℝ) (↑n : ℝ) 1
this :
  HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
neg :
  HMul.hMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) 2 •
      (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter) =
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
⊢ HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) +
        (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)) =
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)

Tactic:
rw [this, ← two_smul ℝ, smul_smul]

Premises used: Real, two_smul, smul_smul
-- 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 : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
hltn : 1 < n
hnsub1 : (↑(n - 1) : ℝ) = HSub.hSub (α := ℝ) (↑n : ℝ) 1
this :
  HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (s.centroid -ᵥ s.circumcenter) + (s.centroid -ᵥ s.circumcenter) =
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)
⊢ HMul.hMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) 2 •
      (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter) =
    (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 / (↑n : ℝ)) • (s.centroid -ᵥ s.circumcenter)

Tactic:
norm_num
-- 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)
⊢ s.eulerPoint i ∈ s.ninePointCircle

Tactic:
(s.isDiameter_ninePointCircle i).right_mem

Premises used: EuclideanGeometry.Sphere.IsDiameter.right_mem, Affine.Simplex.isDiameter_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
s : Triangle ℝ P
i : Fin 3
apply : s.points i -ᵥ Simplex.eulerPoint s i = s.points i -ᵥ midpoint ℝ s.orthocenter (s.points i)
⊢ Simplex.eulerPoint s i = midpoint ℝ s.orthocenter (s.points i)

Tactic:
apply vsub_right_cancel (p := s.points i)

Premises used: vsub_right_cancel
-- 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 : Triangle ℝ P
i : Fin 3
rw :
  (HSub.hSub (α := ℝ) (↑2 : ℝ) 1 / (↑2 : ℝ)) • (s.points i -ᵥ Simplex.mongePoint s) =
    HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        (s.points i -ᵥ Simplex.mongePoint s) +
      HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (s.points i -ᵥ s.points i)
⊢ s.points i -ᵥ Simplex.eulerPoint s i = s.points i -ᵥ midpoint ℝ s.orthocenter (s.points i)

Tactic:
rw [orthocenter_eq_mongePoint, Simplex.points_vsub_eulerPoint, vsub_midpoint]

Premises used: vsub_midpoint, Affine.Triangle.orthocenter_eq_mongePoint, Affine.Simplex.points_vsub_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
s : Triangle ℝ P
i : Fin 3
⊢ (HSub.hSub (α := ℝ) (↑2 : ℝ) 1 / (↑2 : ℝ)) • (s.points i -ᵥ Simplex.mongePoint s) =
    HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        (s.points i -ᵥ Simplex.mongePoint s) +
      HSMul.hSMul (α := ℝ) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _) (s.points i -ᵥ s.points i)

Tactic:
norm_num