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 y : V
h : o.oangle x y = ↑(π / 2)
⊢ o.oangle (x - y) x = ↑(Real.arcsin (‖y‖ / ‖x - y‖))

Tactic:
← neg_inj,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : -o.oangle x y = -↑(π / 2)
⊢ -o.oangle (x - y) x = -↑(Real.arcsin (‖y‖ / ‖x - y‖))
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 y : V
h : o.oangle x y = ↑(π / 2)
⊢ o.oangle (x - y) x = ↑(Real.arctan (‖y‖ / ‖x‖))

Tactic:
← neg_inj,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : -o.oangle x y = -↑(π / 2)
⊢ -o.oangle (x - y) x = -↑(Real.arctan (‖y‖ / ‖x‖))
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 y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle (x - y) x).cos = ‖x‖ / ‖x - y‖

Tactic:
← neg_inj,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : -o.oangle x y = -↑(π / 2)
⊢ -(o.oangle (x - y) x).cos = -(‖x‖ / ‖x - y‖)
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 y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle (x - y) x).sin = ‖y‖ / ‖x - y‖

Tactic:
← neg_inj,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : -o.oangle x y = -↑(π / 2)
⊢ -(o.oangle (x - y) x).sin = -(‖y‖ / ‖x - y‖)
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 : Sbtw ℝ p₃ p₂ p₃'
hp₁p₂ : p₁ ≠ p₂
⊢ ∡ p₁ p₂ p₃ = ∡ p₁ p₂ p₃' + ∡ p₃' p₂ p₃

Tactic:
oangle_add hp₁p₂ h.right_ne h.left_ne

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)
p₁ p₂ p₃ p₃' : P
h : Sbtw ℝ p₃ p₂ p₃'
hp₁p₂ : p₁ ≠ p₂
⊢ ∡ p₁ p₂ p₃ = ∡ p₁ p₂ p₃
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 y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle (x - y) x).tan = ‖y‖ / ‖x‖

Tactic:
← neg_inj,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : -o.oangle x y = -↑(π / 2)
⊢ -(o.oangle (x - y) x).tan = -(‖y‖ / ‖x‖)
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 y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle (x - y) x).cos * ‖x - y‖ = ‖x‖

Tactic:
← neg_inj,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : -o.oangle x y = -↑(π / 2)
⊢ -((o.oangle (x - y) x).cos * ‖x - y‖) = -‖x‖
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 y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle (x - y) x).sin * ‖x - y‖ = ‖y‖

Tactic:
← neg_inj,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : -o.oangle x y = -↑(π / 2)
⊢ -((o.oangle (x - y) x).sin * ‖x - y‖) = -‖y‖
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 y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle (x - y) x).tan * ‖x‖ = ‖y‖

Tactic:
← neg_inj,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : -o.oangle x y = -↑(π / 2)
⊢ -((o.oangle (x - y) x).tan * ‖x‖) = -‖y‖
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 y : V
h : o.oangle x y = ↑(π / 2)
⊢ ‖x‖ / (o.oangle (x - y) x).cos = ‖x - y‖

Tactic:
← neg_inj,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : -o.oangle x y = -↑(π / 2)
⊢ -(‖x‖ / (o.oangle (x - y) x).cos) = -‖x - y‖
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 y : V
h : o.oangle x y = ↑(π / 2)
⊢ ‖y‖ / (o.oangle (x - y) x).sin = ‖x - y‖

Tactic:
← neg_inj,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : -o.oangle x y = -↑(π / 2)
⊢ -(‖y‖ / (o.oangle (x - y) x).sin) = -‖x - y‖
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Projection

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
s : AffineSubspace ℝ P
inst✝ : s.direction.HasOrthogonalProjection
hp : p ∉ s
h : p' ∈ s
hp' : p' ≠ ↑((orthogonalProjection s) p)
this : Nonempty ↥s
hpne : p ≠ ↑((orthogonalProjection s) p)
ha : ∡ p (↑((orthogonalProjection s) p)) p' = ↑(π / 2) ∨ ∡ p (↑((orthogonalProjection s) p)) p' = -↑(π / 2)
⊢ ∡ p (↑((orthogonalProjection s) p)) p' = ↑(π / 2) ∨ ∡ p (↑((orthogonalProjection s) p)) p' = ↑(-π / 2)

Tactic:
rwa [neg_div]

Goal state after:
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 y : V
h : o.oangle x y = ↑(π / 2)
⊢ ‖y‖ / (o.oangle (x - y) x).tan = ‖x‖

Tactic:
← neg_inj,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : -o.oangle x y = -↑(π / 2)
⊢ -(‖y‖ / (o.oangle (x - y) x).tan) = -‖x‖
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)
⊢ o.oangle x (x + r • (o.rotation ↑(π / 2)) x) = ↑(Real.arctan r)

Tactic:
← neg_inj,

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)
⊢ o.oangle x (x + r • (o.rotation ↑(π / 2)) x) = ↑(Real.arctan r)
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)
⊢ o.oangle x (x + r • (o.rotation ↑(π / 2)) x) = ↑(Real.arctan r)

Tactic:
← neg_inj,

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)
⊢ -o.oangle x (x + r • (o.rotation ↑(π / 2)) 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
⊢ o.oangle (x + r • (o.rotation ↑(π / 2)) x) (r • (o.rotation ↑(π / 2)) x) = ↑(Real.arctan r⁻¹)

Tactic:
← neg_inj,

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
⊢ -o.oangle (x + r • (o.rotation ↑(π / 2)) x) (r • (o.rotation ↑(π / 2)) x) = -↑(Real.arctan r⁻¹)
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r₁ r₂ : ℝ
⊢ (o.oangle x (r₁ • x + r₂ • y)).sign = SignType.sign r₂ * (o.oangle x y).sign

Tactic:
by
  simp

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

Goal state before:
pp: 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
| (o.oangle (y - x) y).sign

Tactic:
rw [oangle_sign_sub_left_swap]

Goal state after:
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
| (o.oangle y x).sign
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
hy : y ≠ 0
hr : SameRay ℝ y (x - y)
⊢ |(o.oangle (y - x) y).toReal| < π / 2

Tactic:
rw [← exists_nonneg_left_iff_sameRay hy] at hr

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
hy : y ≠ 0
hr : ∃ r, 0 ≤ r ∧ r • y = x - y
⊢ |(o.oangle (y - x) y).toReal| < π / 2
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle

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
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ (∡ p₂ p₃ p₁).tan = dist p₁ p₂ / dist p₃ p₂

Tactic:
have hs : (∡ p₂ p₃ p₁).sign = 1 := by rw [oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]
  rw [oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
    tan_angle_of_angle_eq_pi_div_two (angle_eq_pi_div_two_of_oangle_eq_pi_div_two h)]

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

Goal state before:
pp: case hp₁
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
i : Fin (n + 1)
w : Fin (n + 1) → ℝ
h : ∑ i, w i = 1
⊢ ∀ i_1 ∈ Finset.univ \ {i}, (⇑↑(s.signedInfDist i) ∘ s.points) i_1 = 0

Tactic:
simp only [Finset.mem_sdiff, Finset.mem_univ, Finset.mem_singleton, true_and,
      Function.comp_apply]
    intro j hj
    exact s.signedInfDist_apply_of_ne hj

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

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 : 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
⊢ Submodule.span ℝ (Set.range b) ≤ s.direction

Tactic:
Submodule.span_le,

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 : 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
⊢ Set.range b ⊆ ↑s.direction
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

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 : Sphere P
p q : P
h : Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = {q}
hq : q ∈ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p)
hr : 0 ≤ s.radius
h' : ∀ (q' : P), q' -ᵥ p ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ ∧ ‖q' -ᵥ p‖ ^ 2 = s.radius ^ 2 - dist p s.center ^ 2 ↔ q' = q
hq' : q -ᵥ p ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ ∧ ‖q -ᵥ p‖ ^ 2 = s.radius ^ 2 - dist p s.center ^ 2
hq'' : (-(q -ᵥ p) +ᵥ p) -ᵥ p ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ ∧ ‖(-(q -ᵥ p) +ᵥ p) -ᵥ p‖ ^ 2 = s.radius ^ 2 - dist p s.center ^ 2
hqq : q -ᵥ p = -(q -ᵥ p)
⊢ q = p ∧ dist p s.center = s.radius

Tactic:
eq_neg_iff_add_eq_zero,

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 : Sphere P
p q : P
h : Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) = {q}
hq : q ∈ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p)
hr : 0 ≤ s.radius
h' : ∀ (q' : P), q' -ᵥ p ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ ∧ ‖q' -ᵥ p‖ ^ 2 = s.radius ^ 2 - dist p s.center ^ 2 ↔ q' = q
hq' : q -ᵥ p ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ ∧ ‖q -ᵥ p‖ ^ 2 = s.radius ^ 2 - dist p s.center ^ 2
hq'' : (-(q -ᵥ p) +ᵥ p) -ᵥ p ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ ∧ ‖(-(q -ᵥ p) +ᵥ p) -ᵥ p‖ ^ 2 = s.radius ^ 2 - dist p s.center ^ 2
hqq : q -ᵥ p + (q -ᵥ p) = 0
⊢ q = p ∧ dist p s.center = s.radius
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: case h₂
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
x✝ : p₁ ∈ s ∧ p₂ ∈ s ∧ dist p₁ p₂ = 2 * s.radius
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
hr : dist p₁ p₂ = 2 * s.radius
⊢ 2 * s.radius = s.radius + s.radius

Tactic:
two_mul

Goal state after:
case h₂
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
x✝ : p₁ ∈ s ∧ p₂ ∈ s ∧ dist p₁ p₂ = 2 * s.radius
h₁ : p₁ ∈ s
h₂ : p₂ ∈ s
hr : dist p₁ p₂ = 2 * s.radius
⊢ s.radius + s.radius = s.radius + s.radius
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
⊢ dist p ↑((faceOpposite t i₃).orthogonalProjectionSpan p) = dist p ↑((faceOpposite t i₂).orthogonalProjectionSpan p) ↔
    2 • ∡ (t.points i₂) (t.points i₁) p = 2 • ∡ p (t.points i₁) (t.points i₃)

Tactic:
by
  have ha : AffineIndependent ℝ ![t.points i₁, t.points i₂, t.points i₃] := by
    convert!
      t.independent.comp_embedding
        ⟨![i₁, i₂, i₃], by
          intro i j hij
          fin_cases i <;> fin_cases j <;> simp_all⟩
    ext i
    fin_cases i <;> rfl
  rw [orthogonalProjectionSpan, orthogonalProjectionSpan,
    ← dist_orthogonalProjection_line_eq_iff_two_zsmul_oangle_eq ha]
  simp only [range_faceOpposite_points]
  simp_rw [(by grind : ({i₃}ᶜ : Set (Fin 3)) = {i₁, i₂}),
    (by grind : ({i₂}ᶜ : Set (Fin 3)) = {i₁, i₃}), Set.image_insert_eq, Set.image_singleton]

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
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:
h_opp,

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₂⟫_ℝ + (⟪o -ᵥ p₂, p₃ -ᵥ o⟫_ℝ + ⟪o -ᵥ p₂, o -ᵥ p₂⟫_ℝ) = 0 ↔
    dist s.center p₂ = s.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
s : Sphere P
p q : P
h : ∠ q p s.center = π / 2
hp✝ : p ∈ s
hp_mem : p ∈ line[ℝ, p, q]
h_ortho : ⟪q -ᵥ p, p -ᵥ s.center⟫_ℝ = 0
hq : q ∈ s.orthRadius p
hp : p ∈ s.orthRadius p
⊢ p ∈ ↑(s.orthRadius p) ∧ q ∈ ↑(s.orthRadius p)

Tactic:
exact ⟨hp, hq⟩

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))
h : s.ExcenterExists signs
fs : Finset (Fin (n + 1))
m : ℕ
hfs : #fs = m + 1
hne : m ≠ n
hm : (Finset.affineCombination ℝ Finset.univ s.points) (s.excenterWeights signs) ∈ affineSpan ℝ (s.points '' ↑fs)
i : Fin (n + 1)
hi : i ∉ ↑fs
⊢ False

Tactic:
exact h.excenterWeights_ne_zero i (s.independent.eq_zero_of_affineCombination_mem_affineSpan
    h.sum_excenterWeights_eq_one hm (Finset.mem_univ i) hi)

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))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ n - 1 ≠ n

Tactic:
have := NeZero.ne n

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
i : Fin (n + 1)
this : n ≠ 0
⊢ n - 1 ≠ n
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h✝ : ↑(angle x y) = ↑(angle x (x + y) + angle y (x + y))
n : ℤ
this : -1 < n
h : 2 * π ≤ angle x (x + y) + angle y (x + y)
hn : 1 ≤ n
⊢ False

Tactic:
two_mul

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h✝ : ↑(angle x y) = ↑(angle x (x + y) + angle y (x + y))
n : ℤ
this : -1 < n
h : π + π ≤ angle x (x + y) + angle y (x + y)
hn : 1 ≤ n
⊢ False
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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
t₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h₁ : t₁.points i₁ = t₂.points i₁
h₃ : t₁.points i₃ = t₂.points i₃
h₂ : 2 • ∡ (t₁.points i₁) (t₁.points i₂) (t₁.points i₃) = 2 • ∡ (t₂.points i₁) (t₂.points i₂) (t₂.points i₃)
⊢ {
      center :=
        ((∡ (t₂.points i₁) (t₂.points i₂) (t₂.points i₃)).tan⁻¹ / 2) •
            («o».rotation ↑(π / 2)) (t₁.points i₃ -ᵥ t₁.points i₁) +ᵥ
          midpoint ℝ (t₁.points i₁) (t₁.points i₃),
      radius := dist (t₁.points i₁) (t₁.points i₃) / |(∡ (t₁.points i₁) (t₁.points i₂) (t₁.points i₃)).sin| / 2 } =
    {
      center :=
        ((∡ (t₂.points i₁) (t₂.points i₂) (t₂.points i₃)).tan⁻¹ / 2) •
            («o».rotation ↑(π / 2)) (t₂.points i₃ -ᵥ t₂.points i₁) +ᵥ
          midpoint ℝ (t₂.points i₁) (t₂.points i₃),
      radius := dist (t₂.points i₁) (t₂.points i₃) / |(∡ (t₂.points i₁) (t₂.points i₂) (t₂.points i₃)).sin| / 2 }

Tactic:
Real.Angle.abs_sin_eq_of_two_zsmul_eq h₂,

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₁ t₂ : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h₁ : t₁.points i₁ = t₂.points i₁
h₃ : t₁.points i₃ = t₂.points i₃
h₂ : 2 • ∡ (t₁.points i₁) (t₁.points i₂) (t₁.points i₃) = 2 • ∡ (t₂.points i₁) (t₂.points i₂) (t₂.points i₃)
⊢ {
      center :=
        ((∡ (t₂.points i₁) (t₂.points i₂) (t₂.points i₃)).tan⁻¹ / 2) •
            («o».rotation ↑(π / 2)) (t₁.points i₃ -ᵥ t₁.points i₁) +ᵥ
          midpoint ℝ (t₁.points i₁) (t₁.points i₃),
      radius := dist (t₁.points i₁) (t₁.points i₃) / |(∡ (t₂.points i₁) (t₂.points i₂) (t₂.points i₃)).sin| / 2 } =
    {
      center :=
        ((∡ (t₂.points i₁) (t₂.points i₂) (t₂.points i₃)).tan⁻¹ / 2) •
            («o».rotation ↑(π / 2)) (t₂.points i₃ -ᵥ t₂.points i₁) +ᵥ
          midpoint ℝ (t₂.points i₁) (t₂.points i₃),
      radius := dist (t₂.points i₁) (t₂.points i₃) / |(∡ (t₂.points i₁) (t₂.points i₂) (t₂.points i₃)).sin| / 2 }
Module: Mathlib.Geometry.Euclidean.Triangle

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
⊢ Real.sin (∠ p₁ p₂ p₃) * dist p₂ p₃ = Real.sin (∠ p₃ p₁ p₂) * dist p₃ p₁

Tactic:
simp only [dist_comm p₂ p₃, angle]

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
⊢ Real.sin (InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)) * dist p₃ p₂ =
    Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁)) * dist p₃ p₁
Module: Mathlib.Geometry.Euclidean.Triangle

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
⊢ Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₁ -ᵥ p₂)) =
    Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₂ -ᵥ p₁))

Tactic:
← neg_vsub_eq_vsub_rev p₁ 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
⊢ Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (p₁ -ᵥ p₂)) =
    Real.sin (InnerProductGeometry.angle (p₃ -ᵥ p₁) (-(p₁ -ᵥ p₂)))