mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SOppSide p₃ p₄
hp₁p₃ : p₁ ≠ p₃
⊢ (∡ ((AffineEquiv.pointReflection ℝ p₁) p₃) p₂ p₁).sign = -(∡ p₁ p₃ p₂).sign

Tactic:
← oangle_rotate_sign p₁,

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SOppSide p₃ p₄
hp₁p₃ : p₁ ≠ p₃
⊢ (∡ ((AffineEquiv.pointReflection ℝ p₁) p₃) p₂ p₁).sign = -(∡ p₃ p₂ p₁).sign
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: P : Type u_2
inst✝ : MetricSpace P
p₁ p₂ : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
⊢ dist s.center p₁ = dist s.center p₂

Tactic:
by
  rw [mem_sphere'.1 hp₁, mem_sphere'.1 hp₂]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + ↑π
hs : line[ℝ, p₁, p₂].SSameSide p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
ha' : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ ((AffineEquiv.pointReflection ℝ p₂) p₄)
hs' : line[ℝ, p₁, p₂].SOppSide p₄ ((AffineEquiv.pointReflection ℝ p₂) p₄)
h : ∠ p₁ p₂ p₃ = π - (π - ∠ p₁ p₂ p₄) / 2
⊢ ∠ p₁ p₂ p₃ = (∠ p₁ p₂ p₄ + π) / 2

Tactic:
linear_combination h

Goal state after:
Module: Mathlib.Geometry.Euclidean.Basic

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0
hop : ⟪c₂ -ᵥ c₁, p -ᵥ p₁⟫ = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = s.direction
v : V
hr : Set.range b = {c₂ -ᵥ c₁, p₂ -ᵥ p₁}
t₁ : ℝ
v' : V
hv' : v' ∈ ℝ ∙ (p₂ -ᵥ p₁)
hv : v = t₁ • (c₂ -ᵥ c₁) + v'
⊢ ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)

Tactic:
Submodule.mem_span_singleton

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = 2
c₁ c₂ p₁ p₂ p : P
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
hps : p ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hpc₁ : dist p c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
hpc₂ : dist p c₂ = r₂
ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0
hop : ⟪c₂ -ᵥ c₁, p -ᵥ p₁⟫ = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = s.direction
v : V
hr : Set.range b = {c₂ -ᵥ c₁, p₂ -ᵥ p₁}
t₁ : ℝ
v' : V
hv' : ∃ a, a • (p₂ -ᵥ p₁) = v'
hv : v = t₁ • (c₂ -ᵥ c₁) + v'
⊢ ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: case neg.refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
⊢ ‖p₂ -ᵥ s.center‖ ≤ ‖p₁ -ᵥ s.center‖

pp: case neg.refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
⊢ ⟪p₂ -ᵥ s.center, p₁ -ᵥ s.center⟫ ≠ ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖

Tactic:
· rwa [← dist_eq_norm_vsub, ← dist_eq_norm_vsub, hp₁]

Goal state after:
case neg.refine_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
hp₁ : dist p₁ s.center = s.radius
hp₂ : dist p₂ s.center ≤ s.radius
h : ¬p₁ = p₂
⊢ ⟪p₂ -ᵥ s.center, p₁ -ᵥ s.center⟫ ≠ ‖p₁ -ᵥ s.center‖ * ‖p₁ -ᵥ s.center‖
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
hpc : p ≠ s.center
hp : dist p s.center ≠ s.radius
hf : Module.finrank ℝ V = 1
⊢ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = ∅

Tactic:
ext p'
  rw [mem_inter_orthRadius_iff_radius_nonneg_and_vsub_mem_and_norm_sq]
  simp only [Set.mem_empty_iff_false, iff_false, not_and]
  intro hr hpo
  have : FiniteDimensional ℝ V := Module.finite_of_finrank_eq_succ hf
  have ha := (ℝ ∙ (p -ᵥ s.center)).finrank_add_finrank_orthogonal
  simp only [finrank_span_singleton (vsub_ne_zero.2 hpc), hf, Nat.add_eq_left,
    Submodule.finrank_eq_zero, Submodule.orthogonal_eq_bot_iff] at ha
  simp only [ha, Submodule.top_orthogonal_eq_bot, Submodule.mem_bot, vsub_eq_zero_iff_eq] at hpo
  simp only [hpo, vsub_self, norm_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow]
  rw [eq_comm, sub_eq_zero, eq_comm, sq_eq_sq₀ dist_nonneg hr]
  exact hp

Goal state after:
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center ≤ s.radius
hpc : p ≠ s.center
v : V
hv : v ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ
hv1 : ‖v‖ = 1
hr : 0 ≤ s.radius
hv0 : v ≠ 0
hf : Module.finrank ℝ ↥(ℝ ∙ (p -ᵥ s.center))ᗮ = 1
⊢ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) =
    {√(s.radius ^ 2 - dist p s.center ^ 2) • v +ᵥ p, -(√(s.radius ^ 2 - dist p s.center ^ 2) • v) +ᵥ p}

Tactic:
rw [finrank_eq_one_iff_of_nonzero' ⟨v, hv⟩ (by simpa using hv0)] at hf

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center ≤ s.radius
hpc : p ≠ s.center
v : V
hv : v ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ
hv1 : ‖v‖ = 1
hr : 0 ≤ s.radius
hv0 : v ≠ 0
hf : ∀ (w : ↥(ℝ ∙ (p -ᵥ s.center))ᗮ), ∃ c, c • ⟨v, hv⟩ = w
⊢ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) =
    {√(s.radius ^ 2 - dist p s.center ^ 2) • v +ᵥ p, -(√(s.radius ^ 2 - dist p s.center ^ 2) • v) +ᵥ p}
Module: Mathlib.Geometry.Euclidean.Angle.Incenter

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
p : P
h₁ : dist p ↑((faceOpposite t i₃).orthogonalProjectionSpan p) = dist p ↑((faceOpposite t i₂).orthogonalProjectionSpan p)
h₂ : dist p ↑((faceOpposite t i₁).orthogonalProjectionSpan p) = dist p ↑((faceOpposite t i₃).orthogonalProjectionSpan p)
⊢ affineSpan ℝ (Set.range t.points) = ⊤

Tactic:
rw [t.independent.affineSpan_eq_top_iff_card_eq_finrank_add_one]

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
p : P
h₁ : dist p ↑((faceOpposite t i₃).orthogonalProjectionSpan p) = dist p ↑((faceOpposite t i₂).orthogonalProjectionSpan p)
h₂ : dist p ↑((faceOpposite t i₁).orthogonalProjectionSpan p) = dist p ↑((faceOpposite t i₃).orthogonalProjectionSpan p)
⊢ Fintype.card (Fin (2 + 1)) = finrank ℝ V + 1
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : Nontrivial V
s₁ s₂ : Sphere P
⊢ s₁.IsIntTangent s₂ ↔ dist s₁.center s₂.center = s₂.radius - s₁.radius ∧ 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius

Tactic:
by
  refine ⟨fun h ↦ ⟨h.dist_center, ?_⟩, ?_⟩
  · rcases h with ⟨p, h₁, h₂, h⟩
    exact ⟨radius_nonneg_of_mem h₁, radius_nonneg_of_mem h₂⟩
  · rintro ⟨h, h₁, h₂⟩
    by_cases h0 : s₁.center = s₂.center
    · rw [h0, dist_self, eq_comm, sub_eq_zero, eq_comm] at h
      have hs : s₁ = s₂ := by
        ext <;> assumption
      simp [hs, h₂]
    · rw [dist_comm] at h
      have ha : |s₂.radius - s₁.radius| = s₂.radius - s₁.radius := by
        refine abs_of_nonneg ?_
        rw [← h]
        exact dist_nonneg
      have hr0 : s₂.radius - s₁.radius ≠ 0 := by
        intro hr0
        rw [hr0, dist_eq_zero] at h
        exact h0 h.symm
      refine ⟨AffineMap.lineMap s₂.center s₁.center (s₂.radius / (s₂.radius - s₁.radius)),
              ?_, ?_, ?_⟩
      · simp only [mem_sphere, dist_lineMap_right, Real.norm_eq_abs, h, one_sub_div hr0, abs_div,
          sub_sub_cancel_left, abs_neg, abs_of_nonneg h₁, ha]
        field
      · simp only [mem_sphere, dist_lineMap_left, norm_div, Real.norm_eq_abs, h, ha,
          abs_of_nonneg h₂]
        field
      · rw [wbtw_iff_left_eq_or_right_mem_image_Ici]
        simp only [Ne.symm h0, Set.mem_image, Set.mem_Ici, AffineMap.lineMap_eq_lineMap_iff,
          false_or, exists_eq_right]
        rw [one_le_div]
        · linarith
        · rw [← h]
          simp [Ne.symm h0]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Circumcenter

Goal state before:
pp: case h.left.left
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : s.direction.HasOrthogonalProjection
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ ↑s
hp : p ∉ s
this : Nonempty ↥s
cc : P
cr : ℝ
hcccru : ∀ (y : Sphere P), y.center ∈ s ∧ ps ⊆ Metric.sphere y.center y.radius → y = { center := cc, radius := cr }
hcc : cc ∈ s
hcr : ps ⊆ Metric.sphere cc cr
x : ℝ := ⋯
y : ℝ := ⋯
hy0 : y ≠ 0
ycc₂ : ℝ := ⋯
cc₂ : P := ⋯
cr₂ : ℝ := ⋯
hpo : p = 1 • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ ↑((orthogonalProjection s) p)
⊢ { center := cc₂, radius := cr₂ }.center ∈ affineSpan ℝ (insert p ↑s)

pp: case h.left.right
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : s.direction.HasOrthogonalProjection
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ ↑s
hp : p ∉ s
this : Nonempty ↥s
cc : P
cr : ℝ
hcccru : ∀ (y : Sphere P), y.center ∈ s ∧ ps ⊆ Metric.sphere y.center y.radius → y = { center := cc, radius := cr }
hcc : cc ∈ s
hcr : ps ⊆ Metric.sphere cc cr
x : ℝ := ⋯
y : ℝ := ⋯
hy0 : y ≠ 0
ycc₂ : ℝ := ⋯
cc₂ : P := ⋯
cr₂ : ℝ := ⋯
hpo : p = 1 • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ ↑((orthogonalProjection s) p)
⊢ insert p ps ⊆ Metric.sphere { center := cc₂, radius := cr₂ }.center { center := cc₂, radius := cr₂ }.radius

Tactic:
· refine vadd_mem_of_mem_direction ?_ (mem_affineSpan ℝ (Set.mem_insert_of_mem _ hcc))
      rw [direction_affineSpan]
      exact
        Submodule.smul_mem _ _
          (vsub_mem_vectorSpan ℝ (Set.mem_insert _ _)
            (Set.mem_insert_of_mem _ (orthogonalProjection_mem _)))

Goal state after:
case h.left.right
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : s.direction.HasOrthogonalProjection
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ ↑s
hp : p ∉ s
this : Nonempty ↥s
cc : P
cr : ℝ
hcccru : ∀ (y : Sphere P), y.center ∈ s ∧ ps ⊆ Metric.sphere y.center y.radius → y = { center := cc, radius := cr }
hcc : cc ∈ s
hcr : ps ⊆ Metric.sphere cc cr
x : ℝ := ⋯
y : ℝ := ⋯
hy0 : y ≠ 0
ycc₂ : ℝ := ⋯
cc₂ : P := ⋯
cr₂ : ℝ := ⋯
hpo : p = 1 • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ ↑((orthogonalProjection s) p)
⊢ insert p ps ⊆ Metric.sphere { center := cc₂, radius := cr₂ }.center { center := cc₂, radius := cr₂ }.radius
Module: Mathlib.Geometry.Euclidean.Angle.Sphere

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
s : Sphere P
hd : s.IsDiameter p₁ p₃
o : P := s.center
h_center : o = midpoint ℝ p₁ p₃
h_opp : p₁ -ᵥ o = -(p₃ -ᵥ o)
⊢ ⟪p₁ -ᵥ o, p₃ -ᵥ o⟫_ℝ + ⟪p₁ -ᵥ o, o -ᵥ p₂⟫_ℝ + (⟪o -ᵥ p₂, p₃ -ᵥ o⟫_ℝ + ⟪o -ᵥ p₂, o -ᵥ p₂⟫_ℝ) = 0 ↔
    dist s.center p₂ = s.radius

Tactic:
rw [h_opp, inner_neg_left, inner_neg_left, real_inner_comm (p₃ -ᵥ o) (o -ᵥ p₂)]

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
s : Sphere P
hd : s.IsDiameter p₁ p₃
o : P := s.center
h_center : o = midpoint ℝ p₁ p₃
h_opp : p₁ -ᵥ o = -(p₃ -ᵥ o)
⊢ -⟪p₃ -ᵥ o, p₃ -ᵥ o⟫_ℝ + -⟪p₃ -ᵥ o, o -ᵥ p₂⟫_ℝ + (⟪p₃ -ᵥ o, o -ᵥ p₂⟫_ℝ + ⟪o -ᵥ p₂, o -ᵥ p₂⟫_ℝ) = 0 ↔
    dist s.center p₂ = s.radius
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.CrossProduct

Goal state before:
pp: a b : EuclideanSpace ℝ (Fin 3)
this : 0 ≤ sin (angle a b)
⊢ ‖toLp 2 ((crossProduct a.ofLp) b.ofLp)‖ ^ 2 = ‖a‖ ^ 2 * ‖b‖ ^ 2 - ⟪a, b⟫ ^ 2

Tactic:
simp_rw [norm_sq_eq_re_inner (𝕜 := ℝ), EuclideanSpace.inner_eq_star_dotProduct, star_trivial,
      RCLike.re_to_real, cross_dot_cross, dotProduct_comm (ofLp b) (ofLp a), sq]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Sphere

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p q : P
h : ⟪q -ᵥ p, s.center -ᵥ p⟫_ℝ = 0
hp : p ∈ s
hp_mem : p ∈ line[ℝ, p, q]
⊢ ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0

Tactic:
← neg_vsub_eq_vsub_rev p s.center,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p q : P
h : ⟪q -ᵥ p, -(p -ᵥ s.center)⟫_ℝ = 0
hp : p ∈ s
hp_mem : p ∈ line[ℝ, p, q]
⊢ ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0
Module: Mathlib.Geometry.Euclidean.Circumcenter

Goal state before:
pp: case h.right.refl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : s.direction.HasOrthogonalProjection
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ ↑s
hp : p ∉ s
this : Nonempty ↥s
cc : P
cr : ℝ
hcccru : ∀ (y : Sphere P), y.center ∈ s ∧ ps ⊆ Metric.sphere y.center y.radius → y = { center := cc, radius := cr }
hcc : cc ∈ s
hcr : ps ⊆ Metric.sphere cc cr
x : ℝ := dist cc ↑((orthogonalProjection s) p)
y : ℝ := dist p ↑((orthogonalProjection s) p)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo : p = 1 • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ ↑((orthogonalProjection s) p)
cc₃ : P
cr₃ : ℝ
hcc₃ : cc₃ ∈ affineSpan ℝ (insert p ↑s)
t₃ : ℝ
hcc₃' : cc ∈ s
hcc₃'' : cc₃ = t₃ • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc
hcr₃' : ∀ p₁ ∈ ps, dist p₁ ↑⟨cc, hcc₃'⟩ = cr
hcr₃val : cr₃ = √(cr * cr + t₃ * y * (t₃ * y))
hcr₃ : dist p cc₃ = cr₃
⊢ { center := cc₃, radius := cr₃ } = { center := cc₂, radius := cr₂ }

Tactic:
rw [hpo, hcc₃'', hcr₃val, ← mul_self_inj_of_nonneg dist_nonneg (Real.sqrt_nonneg _),
      dist_sq_smul_orthogonal_vadd_smul_orthogonal_vadd (orthogonalProjection_mem p) hcc₃' _ _
        (vsub_orthogonalProjection_mem_direction_orthogonal s p),
      Real.norm_eq_abs, abs_mul_abs_self, dist_comm, ← dist_eq_norm_vsub V p,
      Real.mul_self_sqrt (add_nonneg (mul_self_nonneg _) (mul_self_nonneg _))] at hcr₃

Goal state after:
case h.right.refl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
s : AffineSubspace ℝ P
inst✝ : s.direction.HasOrthogonalProjection
ps : Set P
hnps : ps.Nonempty
p : P
hps : ps ⊆ ↑s
hp : p ∉ s
this : Nonempty ↥s
cc : P
cr : ℝ
hcccru : ∀ (y : Sphere P), y.center ∈ s ∧ ps ⊆ Metric.sphere y.center y.radius → y = { center := cc, radius := cr }
hcc : cc ∈ s
hcr : ps ⊆ Metric.sphere cc cr
x : ℝ := dist cc ↑((orthogonalProjection s) p)
y : ℝ := dist p ↑((orthogonalProjection s) p)
hy0 : y ≠ 0
ycc₂ : ℝ := (x * x + y * y - cr * cr) / (2 * y)
cc₂ : P := (ycc₂ / y) • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc
cr₂ : ℝ := √(cr * cr + ycc₂ * ycc₂)
hpo : p = 1 • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ ↑((orthogonalProjection s) p)
cc₃ : P
cr₃ : ℝ
hcc₃ : cc₃ ∈ affineSpan ℝ (insert p ↑s)
t₃ : ℝ
hcc₃' : cc ∈ s
hcc₃'' : cc₃ = t₃ • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc
hcr₃' : ∀ p₁ ∈ ps, dist p₁ ↑⟨cc, hcc₃'⟩ = cr
hcr₃val : cr₃ = √(cr * cr + t₃ * y * (t₃ * y))
hcr₃ :
  dist cc ↑((orthogonalProjection s) p) * dist cc ↑((orthogonalProjection s) p) +
      (1 - t₃) * (1 - t₃) * (dist p ↑((orthogonalProjection s) p) * dist p ↑((orthogonalProjection s) p)) =
    cr * cr + t₃ * y * (t₃ * y)
⊢ { center := cc₃, radius := cr₃ } = { center := cc₂, radius := cr₂ }
Module: Mathlib.Geometry.Euclidean.Incenter

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
⊢ s.exradius Finset.univ = s.inradius

Tactic:
rw [exradius, exsphere_univ, insphere_radius]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Circumcenter

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
s : Simplex ℝ P n
⊢ ∀ (i : Fin (n + 1)), dist s.circumcenter (s.points i) = s.circumradius

Tactic:
by
  intro i
  rw [dist_comm]
  exact dist_circumcenter_eq_circumradius _ _

Goal state after:
Module: Mathlib.Geometry.Euclidean.Incenter

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
i : Fin (n + 1)
p : P
ht : (s.exsphere signs).IsTangentAt p (affineSpan ℝ (Set.range (s.faceOpposite i).points))
⊢ p = s.touchpoint signs i

Tactic:
by
  rw [ht.eq_orthogonalProjection, touchpoint, orthogonalProjectionSpan, excenter]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Incenter

Goal state before:
pp: case refine_1
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
r : ℝ
h1 : ∑ i, s.excenterWeights signs i = 1
hp : (Finset.affineCombination ℝ Finset.univ s.points) (s.excenterWeights signs) ∈ affineSpan ℝ (Set.range s.points)
h :
  ∀ (i : Fin (n + 1)),
    (s.signedInfDist i) ((Finset.affineCombination ℝ Finset.univ s.points) (s.excenterWeights signs)) =
      (if i ∈ signs then -1 else 1) * r
h' :
  ∀ (i : Fin (n + 1)),
    s.excenterWeights signs i * dist (s.points i) (s.altitudeFoot i) = (if i ∈ signs then -1 else 1) * r
h'' : ∀ (i : Fin (n + 1)), s.excenterWeights signs i = r * s.excenterWeightsUnnorm signs i
⊢ s.ExcenterExists signs ∧
    (Finset.affineCombination ℝ Finset.univ s.points) (s.excenterWeights signs) = s.excenter signs

Tactic:
exact ⟨s.sum_excenterWeights_eq_one_iff.1 h1, rfl⟩

Goal state after:
Module: Mathlib.Geometry.Euclidean.Circumcenter

Goal state before:
pp: case mp
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
c : P
hcr : ∃ radius, ∀ p ∈ ps, dist p c = radius
⊢ ∃ center ∈ s, ∃ radius, ∀ p ∈ ps, dist p center = radius

Tactic:
exists_dist_eq_iff_exists_dist_orthogonalProjection_eq h c

Goal state after:
case mp
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
c : P
hcr : ∃ r, ∀ p₁ ∈ ps, dist p₁ ↑((orthogonalProjection s) c) = r
⊢ ∃ center ∈ s, ∃ radius, ∀ p ∈ ps, dist p center = radius
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : angle x z ≠ π
H0 : angle x z = angle x y + angle y z
H1 : ¬angle x z = 0
Hxz : Real.sin (angle x z) ≠ 0
H2 : ¬angle x y = 0
H3 : ¬angle y z = 0
H4 : angle x y = π
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z

pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : angle x z ≠ π
H0 : angle x z = angle x y + angle y z
H1 : ¬angle x z = 0
Hxz : Real.sin (angle x z) ≠ 0
H2 : ¬angle x y = 0
H3 : ¬angle y z = 0
H4 : ¬angle x y = π
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z

Tactic:
· grind [angle_le_pi, angle_nonneg]

Goal state after:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : angle x z ≠ π
H0 : angle x z = angle x y + angle y z
H1 : ¬angle x z = 0
Hxz : Real.sin (angle x z) ≠ 0
H2 : ¬angle x y = 0
H3 : ¬angle y z = 0
H4 : ¬angle x y = π
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : angle x z ≠ π
H0 : angle x z = angle x y + angle y z
H1 : ¬angle x z = 0
Hxz : Real.sin (angle x z) ≠ 0
H2 : ¬angle x y = 0
H3 : ¬angle y z = 0
H4 : ¬angle x y = π
H5 : angle y z = π
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z

pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : angle x z ≠ π
H0 : angle x z = angle x y + angle y z
H1 : ¬angle x z = 0
Hxz : Real.sin (angle x z) ≠ 0
H2 : ¬angle x y = 0
H3 : ¬angle y z = 0
H4 : ¬angle x y = π
H5 : ¬angle y z = π
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z

Tactic:
· grind [angle_le_pi, angle_nonneg]

Goal state after:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hz : ‖z‖ = 1
H : angle x z ≠ π
H0 : angle x z = angle x y + angle y z
H1 : ¬angle x z = 0
Hxz : Real.sin (angle x z) ≠ 0
H2 : ¬angle x y = 0
H3 : ¬angle y z = 0
H4 : ¬angle x y = π
H5 : ¬angle y z = π
⊢ Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z