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

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
⊢ o.oangle x (x + r • (o.rotation ↑(π / 2)) x) = ↑(Real.arctan r)

Tactic:
rcases lt_trichotomy r 0 with (hr | rfl | hr)

Goal state after:
case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r < 0
⊢ o.oangle x (x + r • (o.rotation ↑(π / 2)) x) = ↑(Real.arctan r)

case inr.inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
⊢ o.oangle x (x + 0 • (o.rotation ↑(π / 2)) x) = ↑(Real.arctan 0)

case inr.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : 0 < r
⊢ o.oangle x (x + r • (o.rotation ↑(π / 2)) x) = ↑(Real.arctan r)
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p : P
h : p₁ ≠ p₂
hd : dist p₁ p = dist p₂ p
r : ℝ
hr : p = r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂
⊢ ∃ r, r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = p

Tactic:
exact ⟨r, hr.symm⟩

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

Goal state before:
pp: case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r < 0
ha : (-o).oangle x (r • (o.rotation ↑(π / 2)) x) = ↑(π / 2)
⊢ -↑(Real.arctan (‖r‖ * ‖x‖ / ‖x‖)) = ↑(Real.arctan r)

Tactic:
mul_div_assoc,

Goal state after:
case inl
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : r < 0
ha : (-o).oangle x (r • (o.rotation ↑(π / 2)) x) = ↑(π / 2)
⊢ -↑(Real.arctan (‖r‖ * (‖x‖ / ‖x‖))) = ↑(Real.arctan r)
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Goal state before:
pp: case inr.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : 0 < r
ha : o.oangle x (r • (o.rotation ↑(π / 2)) x) = ↑(π / 2)
⊢ ↑(Real.arctan (‖r‖ * ‖x‖ / ‖x‖)) = ↑(Real.arctan r)

Tactic:
mul_div_assoc,

Goal state after:
case inr.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : 0 < r
ha : o.oangle x (r • (o.rotation ↑(π / 2)) x) = ↑(π / 2)
⊢ ↑(Real.arctan (‖r‖ * (‖x‖ / ‖x‖))) = ↑(Real.arctan r)
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

Goal state before:
pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
hx : -x = r⁻¹ • (o.rotation ↑(π / 2)) (r • (o.rotation ↑(π / 2)) x)
⊢ o.oangle (r • (o.rotation ↑(π / 2)) x) (r • (o.rotation ↑(π / 2)) x + -x) = ↑(Real.arctan r⁻¹)

Tactic:
hx,

Goal state after:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : x ≠ 0
r : ℝ
hr : ¬r = 0
hx : -x = r⁻¹ • (o.rotation ↑(π / 2)) (r • (o.rotation ↑(π / 2)) x)
⊢ o.oangle (r • (o.rotation ↑(π / 2)) x)
      (r • (o.rotation ↑(π / 2)) x + r⁻¹ • (o.rotation ↑(π / 2)) (r • (o.rotation ↑(π / 2)) x)) =
    ↑(Real.arctan r⁻¹)
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: case neg.inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
hn : ¬x = y
hs : o.oangle y (y - x) = ↑π
⊢ |(o.oangle (y - x) y).toReal| < π / 2

Tactic:
oangle_eq_pi_iff_sameRay_neg,

Goal state after:
case neg.inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : ‖x‖ = ‖y‖
hn : ¬x = y
hs : y ≠ 0 ∧ y - x ≠ 0 ∧ SameRay ℝ y (-(y - x))
⊢ |(o.oangle (y - x) y).toReal| < π / 2
Module: Mathlib.Geometry.Euclidean.SignedDist

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
v w : V
p q : P
⊢ ((signedDist v) p) (-w +ᵥ w +ᵥ q) = ((signedDist v) p) q

Tactic:
neg_vadd_vadd

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v w : V
p q : P
⊢ ((signedDist v) p) q = ((signedDist v) p) q
Module: Mathlib.Geometry.Euclidean.PerpBisector

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
c p₁ p₂ : P
⊢ ⟪c -ᵥ midpoint ℝ p₁ p₂, p₂ -ᵥ p₁⟫ = 0 ↔ ⟪((c -ᵥ p₁) +ᵥ c) -ᵥ p₂, p₂ -ᵥ p₁⟫ = 0

Tactic:
vsub_midpoint,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c p₁ p₂ : P
⊢ ⟪⅟2 • (c -ᵥ p₁) + ⅟2 • (c -ᵥ p₂), p₂ -ᵥ p₁⟫ = 0 ↔ ⟪((c -ᵥ p₁) +ᵥ c) -ᵥ p₂, p₂ -ᵥ p₁⟫ = 0
Module: Mathlib.Geometry.Euclidean.PerpBisector

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
c p₁ p₂ : P
⊢ c ∈ perpBisector p₁ p₂ ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫

Tactic:
Iff.comm,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c p₁ p₂ : P
⊢ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫ ↔ c ∈ perpBisector p₁ p₂
Module: Mathlib.Geometry.Euclidean.PerpBisector

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
c p₁ p₂ : P
⊢ ⟪c -ᵥ p₁ + (c -ᵥ p₂), p₂ -ᵥ p₁⟫ = 0 ↔ ⟪c -ᵥ midpoint ℝ p₁ p₂, p₂ -ᵥ p₁⟫ = 0

Tactic:
vsub_midpoint,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c p₁ p₂ : P
⊢ ⟪c -ᵥ p₁ + (c -ᵥ p₂), p₂ -ᵥ p₁⟫ = 0 ↔ ⟪⅟2 • (c -ᵥ p₁) + ⅟2 • (c -ᵥ p₂), p₂ -ᵥ p₁⟫ = 0
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
ι₁ : Type u_3
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
p₁ : ι₁ → P
h₁ : ∑ i ∈ s₁, w₁ i = 0
ι₂ : Type u_4
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
p₂ : ι₂ → P
h₂ : ∑ i ∈ s₂, w₂ i = 0
⊢ ⟪(s₁.weightedVSub p₁) w₁, (s₂.weightedVSub p₂) w₂⟫ =
    (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (dist (p₁ i₁) (p₂ i₂) * dist (p₁ i₁) (p₂ i₂))) / 2

Tactic:
Finset.weightedVSub_apply,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
ι₁ : Type u_3
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
p₁ : ι₁ → P
h₁ : ∑ i ∈ s₁, w₁ i = 0
ι₂ : Type u_4
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
p₂ : ι₂ → P
h₂ : ∑ i ∈ s₂, w₂ i = 0
⊢ ⟪∑ i ∈ s₁, w₁ i • (p₁ i -ᵥ Classical.choice ⋯), (s₂.weightedVSub p₂) w₂⟫ =
    (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (dist (p₁ i₁) (p₂ i₂) * dist (p₁ i₁) (p₂ i₂))) / 2
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
ι₁ : Type u_3
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
p₁ : ι₁ → P
h₁ : ∑ i ∈ s₁, w₁ i = 0
ι₂ : Type u_4
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
p₂ : ι₂ → P
h₂ : ∑ i ∈ s₂, w₂ i = 0
⊢ ⟪∑ i ∈ s₁, w₁ i • (p₁ i -ᵥ Classical.choice ⋯), (s₂.weightedVSub p₂) w₂⟫ =
    (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (dist (p₁ i₁) (p₂ i₂) * dist (p₁ i₁) (p₂ i₂))) / 2

Tactic:
Finset.weightedVSub_apply,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
ι₁ : Type u_3
s₁ : Finset ι₁
w₁ : ι₁ → ℝ
p₁ : ι₁ → P
h₁ : ∑ i ∈ s₁, w₁ i = 0
ι₂ : Type u_4
s₂ : Finset ι₂
w₂ : ι₂ → ℝ
p₂ : ι₂ → P
h₂ : ∑ i ∈ s₂, w₂ i = 0
⊢ ⟪∑ i ∈ s₁, w₁ i • (p₁ i -ᵥ Classical.choice ⋯), ∑ i ∈ s₂, w₂ i • (p₂ i -ᵥ Classical.choice ⋯)⟫ =
    (-∑ i₁ ∈ s₁, ∑ i₂ ∈ s₂, w₁ i₁ * w₂ i₂ * (dist (p₁ i₁) (p₂ i₂) * dist (p₁ i₁) (p₂ i₂))) / 2
Module: Mathlib.Geometry.Euclidean.SignedDist

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✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p q : P
h : q ∈ s
⊢ s.signedInfDist p = (signedDist (p -ᵥ ↑((orthogonalProjection s) p))) q

Tactic:
apply signedDist_left_congr
  apply s.direction.inner_left_of_mem_orthogonal
  · exact vsub_mem_direction (SetLike.coe_mem _) h
  · exact vsub_orthogonalProjection_mem_direction_orthogonal s p

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
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
hvi : ⟪v, v⟫ ≠ 0
hd : discrim ⟪v, v⟫ (2 * ⟪v, p₁ -ᵥ p₂⟫) 0 = 2 * ⟪v, p₁ -ᵥ p₂⟫ * (2 * ⟪v, p₁ -ᵥ p₂⟫)
⊢ r = 0 ∨ r = -2 * (2 * ⟪v, p₁ -ᵥ p₂⟫) / (2 * ⟪v, v⟫) ↔ r = 0 ∨ r = -2 * ⟪v, p₁ -ᵥ p₂⟫ / ⟪v, v⟫

Tactic:
mul_div_assoc,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p₁ p₂ : P
hv : v ≠ 0
r : ℝ
hvi : ⟪v, v⟫ ≠ 0
hd : discrim ⟪v, v⟫ (2 * ⟪v, p₁ -ᵥ p₂⟫) 0 = 2 * ⟪v, p₁ -ᵥ p₂⟫ * (2 * ⟪v, p₁ -ᵥ p₂⟫)
⊢ r = 0 ∨ r = -2 * (2 * ⟪v, p₁ -ᵥ p₂⟫ / (2 * ⟪v, v⟫)) ↔ r = 0 ∨ r = -2 * ⟪v, p₁ -ᵥ p₂⟫ / ⟪v, v⟫
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: case refine_1
P : Type u_2
inst✝ : MetricSpace P
ps : Set P
h : Cospherical ps
⊢ ∃ s, ps ⊆ Metric.sphere s.center s.radius

Tactic:
rcases h with ⟨c, r, h⟩

Goal state after:
case refine_1
P : Type u_2
inst✝ : MetricSpace P
ps : Set P
c : P
r : ℝ
h : ∀ p ∈ ps, dist p c = r
⊢ ∃ s, ps ⊆ Metric.sphere s.center s.radius
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ p₃ : P
h₁₂ : s.IsDiameter p₁ p₂
h₁₃ : s.IsDiameter p₁ p₃
⊢ p₂ = p₃

Tactic:
rw [← h₁₂.pointReflection_center_left, ← h₁₃.pointReflection_center_left]

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
s : Sphere P
p x : P
⊢ x ∈ s.orthRadius p ↔ ⟪p -ᵥ s.center, x -ᵥ p⟫ = 0

Tactic:
mem_orthRadius_iff_inner_left,

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 x : P
⊢ ⟪x -ᵥ p, p -ᵥ s.center⟫ = 0 ↔ ⟪p -ᵥ s.center, x -ᵥ p⟫ = 0
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
⊢ s.center ∈ s.orthRadius p ↔ p = s.center

Tactic:
mem_orthRadius_iff_inner_left,

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 : P
⊢ ⟪s.center -ᵥ p, p -ᵥ s.center⟫ = 0 ↔ p = s.center
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

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
s : Sphere P
p q : P
h : s.orthRadius p ≤ s.orthRadius q
⊢ p = q ∨ q = s.center

Tactic:
have h' := direction_le h

Goal state after:
case 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 q : P
h : s.orthRadius p ≤ s.orthRadius q
h' : (s.orthRadius p).direction ≤ (s.orthRadius q).direction
⊢ p = q ∨ q = s.center
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

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
s : Sphere P
p q : P
h : s.orthRadius p ≤ s.orthRadius q
h' : (ℝ ∙ (p -ᵥ s.center))ᗮ ≤ (ℝ ∙ (q -ᵥ s.center))ᗮ
r : ℝ
hr : r • (p -ᵥ s.center) = q -ᵥ s.center
hp : p ∈ s.orthRadius q
⊢ p = q ∨ q = s.center

Tactic:
mem_orthRadius_iff_inner_left,

Goal state after:
case 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 q : P
h : s.orthRadius p ≤ s.orthRadius q
h' : (ℝ ∙ (p -ᵥ s.center))ᗮ ≤ (ℝ ∙ (q -ᵥ s.center))ᗮ
r : ℝ
hr : r • (p -ᵥ s.center) = q -ᵥ s.center
hp : ⟪p -ᵥ q, q -ᵥ s.center⟫ = 0
⊢ p = q ∨ q = s.center
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

Goal state before:
pp: case inr
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 : dist q s.center ^ 2 - dist p s.center ^ 2 = dist q p ^ 2
h0 : s.radius < 0
⊢ q ∈ s ↔ 0 ≤ s.radius ∧ dist q s.center ^ 2 - dist p s.center ^ 2 = s.radius ^ 2 - dist p s.center ^ 2

Tactic:
simp only [h0.not_ge, sub_left_inj, false_and, iff_false]

Goal state after:
case inr
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 : dist q s.center ^ 2 - dist p s.center ^ 2 = dist q p ^ 2
h0 : s.radius < 0
⊢ q ∉ s
Module: Mathlib.Geometry.Euclidean.Sphere.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
p₁ p₂ : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁' : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂' : ‖p₂ -ᵥ s.center‖ = s.radius
hd : s.radius ^ 2 = ‖p₂ -ᵥ p₁‖ ^ 2 + 2 * ⟪p₂ -ᵥ p₁, p₁ -ᵥ s.center⟫ + ‖p₁ -ᵥ s.center‖ ^ 2
⊢ 0 < ⟪p₂ -ᵥ p₁, s.center -ᵥ p₁⟫

Tactic:
hp₁',

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
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
hp₁' : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂' : ‖p₂ -ᵥ s.center‖ = s.radius
hd : s.radius ^ 2 = ‖p₂ -ᵥ p₁‖ ^ 2 + 2 * ⟪p₂ -ᵥ p₁, p₁ -ᵥ s.center⟫ + s.radius ^ 2
⊢ 0 < ⟪p₂ -ᵥ p₁, s.center -ᵥ 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₃
signs : Finset (Fin 3)
h : ∡ (t.points i₂) (t.points i₁) (excenter t signs) = ∡ (excenter t signs) (t.points i₁) (t.points i₃) + ↑π
⊢ excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}

Tactic:
by
  have hs := t.excenter_eq_incenter_or_excenter_singleton_of_ne signs h₁₂ h₁₃ h₂₃
  rcases hs with hs | hs | hs | hs
  · rw [hs, t.oangle_incenter_eq h₁₂ h₁₃ h₂₃] at h
    simp [Real.Angle.pi_ne_zero] at h
  · rw [hs, t.oangle_excenter_singleton_eq h₁₂ h₁₃ h₂₃] at h
    simp [Real.Angle.pi_ne_zero] at h
  · exact .inl hs
  · exact .inr hs

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

Goal state before:
pp: case h.left.right.inr
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)
p₁ : P
hp₁ : p₁ ∈ ps
⊢ dist p₁ { center := cc₂, radius := cr₂ }.center * dist p₁ { center := cc₂, radius := cr₂ }.center =
    cr * cr + ycc₂ * ycc₂

Tactic:
dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq _ (hps hp₁),

Goal state after:
case h.left.right.inr
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)
p₁ : P
hp₁ : p₁ ∈ ps
⊢ dist p₁ ↑((orthogonalProjection s) { center := cc₂, radius := cr₂ }.center) *
        dist p₁ ↑((orthogonalProjection s) { center := cc₂, radius := cr₂ }.center) +
      dist { center := cc₂, radius := cr₂ }.center ↑((orthogonalProjection s) { center := cc₂, radius := cr₂ }.center) *
        dist { center := cc₂, radius := cr₂ }.center
          ↑((orthogonalProjection s) { center := cc₂, radius := cr₂ }.center) =
    cr * cr + ycc₂ * ycc₂
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))
h : s.ExcenterExists signs
fs : Finset (Fin (n + 1))
m : ℕ
hfs : #fs = m + 1
hne : m ≠ n
hm : s.excenter signs ∈ affineSpan ℝ (s.points '' ↑fs)
this : m + 1 ≤ #fs
⊢ #fs < #Finset.univ

Tactic:
fs.subset_univ

Goal state after:
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))
h : s.ExcenterExists signs
fs : Finset (Fin (n + 1))
m : ℕ
hfs : #fs = m + 1
hne : m ≠ n
hm : s.excenter signs ∈ affineSpan ℝ (s.points '' ↑fs)
this : m + 1 ≤ #Finset.univ
⊢ #fs < #Finset.univ
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : -(‖y‖ - ‖x‖) = (‖y‖ - ‖x‖) * ⟪x, y⟫ / (‖x‖ * ‖y‖)
hx0 : ¬x = 0
hy0 : ¬y = 0
⊢ ‖x‖ = ‖y‖

Tactic:
mul_div_assoc,

Goal state after:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : -(‖y‖ - ‖x‖) = (‖y‖ - ‖x‖) * (⟪x, y⟫ / (‖x‖ * ‖y‖))
hx0 : ¬x = 0
hy0 : ¬y = 0
⊢ ‖x‖ = ‖y‖
Module: Mathlib.Geometry.Euclidean.Angle.Sphere

Goal state before:
pp: V : Type u_3
P : Type u_4
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ /
      («o».oangle (midpoint ℝ p₁ p₂ -ᵥ p₁)
          (midpoint ℝ p₁ p₂ -ᵥ p₁ + (∡ p₂ p₁ s.center).tan • («o».rotation ↑(π / 2)) (midpoint ℝ p₁ p₂ -ᵥ p₁))).cos =
    ‖midpoint ℝ p₁ p₂ -ᵥ p₁ + (∡ p₂ p₁ s.center).tan • («o».rotation ↑(π / 2)) (midpoint ℝ p₁ p₂ -ᵥ p₁)‖

Tactic:
o.oangle_add_right_smul_rotation_pi_div_two,

Goal state after:
V : Type u_3
P : Type u_4
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ ‖midpoint ℝ p₁ p₂ -ᵥ p₁‖ / (↑(Real.arctan (∡ p₂ p₁ s.center).tan)).cos =
    ‖midpoint ℝ p₁ p₂ -ᵥ p₁ + (∡ p₂ p₁ s.center).tan • («o».rotation ↑(π / 2)) (midpoint ℝ p₁ p₂ -ᵥ p₁)‖

case h
V : Type u_3
P : Type u_4
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
h : p₁ ≠ p₂
⊢ midpoint ℝ p₁ p₂ -ᵥ p₁ ≠ 0
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)
⊢ s.points i = (affineCombination ℝ univ s.pointsWithCircumcenter) (pointWeightsWithCircumcenter i)

Tactic:
rw [← pointsWithCircumcenter_point]

Goal state after:
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)
⊢ s.pointsWithCircumcenter (pointIndex i) =
    (affineCombination ℝ univ s.pointsWithCircumcenter) (pointWeightsWithCircumcenter i)
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ ‖x‖ * ‖y‖ ≤ 1

Tactic:
hx,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
⊢ 1 * ‖y‖ ≤ 1
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h₁ : ¬x = y
h₂ : ¬x = -y
H1 : ‖x - ⟪y, x⟫ • y‖ ≠ 0
⊢ (1 - ⟪x, y⟫ * ⟪x, y⟫) ^ 2 +
      (‖x‖ ^ 2 - ⟪x, y⟫ * ⟪x, y⟫ - (⟪x, y⟫ * ⟪x, y⟫ - ⟪x, y⟫ * (⟪x, y⟫ * ⟪y, y⟫))) * ⟪x, y⟫ ^ 2 =
    ‖x‖ ^ 2 - ⟪x, y⟫ * ⟪x, y⟫ - (⟪x, y⟫ * ⟪x, y⟫ - ⟪x, y⟫ * (⟪x, y⟫ * ⟪y, y⟫))

Tactic:
hx,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
h₁ : ¬x = y
h₂ : ¬x = -y
H1 : ‖x - ⟪y, x⟫ • y‖ ≠ 0
⊢ (1 - ⟪x, y⟫ * ⟪x, y⟫) ^ 2 + (1 ^ 2 - ⟪x, y⟫ * ⟪x, y⟫ - (⟪x, y⟫ * ⟪x, y⟫ - ⟪x, y⟫ * (⟪x, y⟫ * ⟪y, y⟫))) * ⟪x, y⟫ ^ 2 =
    1 ^ 2 - ⟪x, y⟫ * ⟪x, y⟫ - (⟪x, y⟫ * ⟪x, y⟫ - ⟪x, y⟫ * (⟪x, y⟫ * ⟪y, y⟫))
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
⊢ x = ⟪x, y⟫ • y + (‖x - ⟪y, x⟫ • y‖⁻¹ * (‖x‖ ^ 2 - ⟪y, x⟫ * ⟪x, y⟫)) • ‖x - ⟪y, x⟫ • y‖⁻¹ • (x - ⟪y, x⟫ • y)

Tactic:
hx,

Goal state after:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
hxy : ¬x - ⟪x, y⟫ • y = 0
⊢ x = ⟪x, y⟫ • y + (‖x - ⟪y, x⟫ • y‖⁻¹ * (1 ^ 2 - ⟪y, x⟫ * ⟪x, y⟫)) • ‖x - ⟪y, x⟫ • y‖⁻¹ • (x - ⟪y, x⟫ • y)