mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.Euclidean.Projection

Goal state before:
pp: case mpr
𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace 𝕜 V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst✝¹ : Nonempty ↥s
inst✝ : s.direction.HasOrthogonalProjection
p : P
⊢ p ∈ s → ↑((orthogonalProjection s) p) = p

Tactic:
intro h
    have hp : p ∈ (s : Set P) ∩ mk' p s.directionᗮ := ⟨h, self_mem_mk' p _⟩
    rw [inter_eq_singleton_orthogonalProjection p] at hp
    symm
    exact hp

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

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
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ ↑(↑(-θ).toCircle * (o.kahler x) y).arg = ↑((o.kahler x) y).arg - θ

Tactic:
rw [Complex.arg_mul_coe_angle, Real.Angle.arg_toCircle]

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
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ -θ + ↑((o.kahler x) y).arg = ↑((o.kahler x) y).arg - θ

case hx
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ ↑(-θ).toCircle ≠ 0

case hy
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ (o.kahler x) y ≠ 0
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation

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
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ ↑(↑θ.toCircle * (o.kahler x) y).arg = ↑((o.kahler x) y).arg + θ

Tactic:
rw [Complex.arg_mul_coe_angle, Real.Angle.arg_toCircle]

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
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ θ + ↑((o.kahler x) y).arg = ↑((o.kahler x) y).arg + θ

case hx
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ ↑θ.toCircle ≠ 0

case hy
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
θ : Real.Angle
⊢ (o.kahler x) y ≠ 0
Module: Mathlib.Geometry.Euclidean.Altitude

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 : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
i : Fin (n + 1)
⊢ ↑((s.restrict S hS).altitudeFoot i) = s.altitudeFoot i

Tactic:
rw [eq_comm]
  convert! (s.restrict S hS).altitudeFoot_map S.subtypeₐᵢ i

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

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₂ : Type u_3
P₂ : Type u_4
inst✝³ : NormedAddCommGroup V₂
inst✝² : InnerProductSpace ℝ V₂
inst✝¹ : MetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
i j : Fin (n + 1)
h : i ≠ j
⊢ NeZero n

Tactic:
grind [neZero_iff]

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

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 j : Fin (n + 1)
h : i ≠ j
⊢ NeZero n

Tactic:
grind [neZero_iff]

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

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
P : Type u_3
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace 𝕜 V
inst✝⁵ : MetricSpace P
inst✝⁴ : NormedAddTorsor V P
s : AffineSubspace 𝕜 P
inst✝³ : Nonempty ↥s
s' : AffineSubspace 𝕜 ↥s
inst✝² : Nonempty ↥s'
inst✝¹ : s'.direction.HasOrthogonalProjection
inst✝ : (map s.subtype s').direction.HasOrthogonalProjection
p : ↥s
this : (map s.subtypeₐᵢ.toAffineMap s').direction.HasOrthogonalProjection
⊢ ↑((orthogonalProjection (map s.subtype s')) ↑p) = ↑↑((orthogonalProjection s') p)

Tactic:
convert! orthogonalProjection_map s' s.subtypeₐᵢ p

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

Goal state before:
pp: case mpr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ ‖x‖ = ‖y‖ ∧ SameRay ℝ x y → x = y

Tactic:
· rcases eq_or_ne y 0 with (rfl | hy)
    · simp
    rintro ⟨h₁, h₂⟩
    obtain ⟨r, hr, rfl⟩ := h₂.exists_nonneg_right hy
    have : ‖y‖ ≠ 0 := by simpa using hy
    obtain rfl : r = 1 := by
      apply mul_right_cancel₀ this
      simpa [norm_smul, abs_of_nonneg hr] using h₁
    simp

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

Goal state before:
pp: case refine_2
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
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr : r < 0
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
⊢ p₂ ≠ p₃

Tactic:
ne_comm,

Goal state after:
case refine_2
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
hp₁p₂ : p₁ -ᵥ p₂ ≠ 0
r : ℝ
hr : r < 0
hp₃p₂ : p₃ -ᵥ p₂ = r • (p₁ -ᵥ p₂)
⊢ p₃ ≠ p₂
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic

Goal state before:
pp: case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : ¬y = 0
⊢ ⟪x, y⟫ = ‖x‖ * ‖y‖ * (((o.kahler x) y).re / (‖x‖ * ‖y‖))

Tactic:
simp only [kahler_apply_apply, real_smul, add_re, ofReal_re, mul_re, I_re, ofReal_im]

Goal state after:
case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : ¬y = 0
⊢ ⟪x, y⟫ = ‖x‖ * ‖y‖ * ((⟪x, y⟫ + ((o.areaForm x) y * 0 - 0 * I.im)) / (‖x‖ * ‖y‖))
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0 ∨ y ≠ 0
⊢ Real.sin (angle x (x + y)) = ‖y‖ / ‖x + y‖

Tactic:
angle_add_eq_arcsin_of_inner_eq_zero h h0,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : x ≠ 0 ∨ y ≠ 0
⊢ Real.sin (Real.arcsin (‖y‖ / ‖x + y‖)) = ‖y‖ / ‖x + y‖
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: case neg.h.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
h0 : ¬y = 0
⊢ 0 < ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖

Tactic:
· exact Left.add_pos_of_nonneg_of_pos (mul_self_nonneg _) (mul_self_pos.2 (norm_ne_zero_iff.2 h0))

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

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
h0 : x ≠ 0 ∨ -y ≠ 0
⊢ angle x (x + -y) = Real.arcsin (‖y‖ / ‖x + -y‖)

Tactic:
angle_add_eq_arcsin_of_inner_eq_zero h h0,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
h0 : x ≠ 0 ∨ -y ≠ 0
⊢ Real.arcsin (‖-y‖ / ‖x + -y‖) = Real.arcsin (‖y‖ / ‖x + -y‖)
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, y⟫ = 0
⊢ angle x (x - y) ≤ π / 2

Tactic:
rw [← neg_eq_zero, ← inner_neg_right] at h
  rw [sub_eq_add_neg]
  exact angle_add_le_pi_div_two_of_inner_eq_zero h

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

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : ⟪x, -y⟫ = 0
⊢ Real.cos (angle x (x - y)) * ‖x - y‖ = ‖x‖

Tactic:
rw [sub_eq_add_neg, cos_angle_add_mul_norm_of_inner_eq_zero h]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₃ ≠ p₂
⊢ ∠ p₂ p₃ p₁ = Real.arctan (dist p₁ p₂ / dist p₃ p₂)

Tactic:
ne_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
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₂ ≠ p₃
⊢ ∠ p₂ p₃ p₁ = Real.arctan (dist p₁ p₂ / dist p₃ p₂)
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₃ ≠ p₂
⊢ ∠ p₂ p₃ p₁ < π / 2

Tactic:
ne_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
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₂ ≠ p₃
⊢ ∠ p₂ p₃ p₁ < π / 2
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
⊢ (o.oangle (p₁ -ᵥ p₂) (p₁ -ᵥ p₃)).sign = -(o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)).sign

Tactic:
←
    vsub_sub_vsub_cancel_left p₁ 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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ (o.oangle (p₁ -ᵥ p₂) (p₂ -ᵥ p₃ - (p₂ -ᵥ p₁))).sign = -(o.oangle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)).sign
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₁ = p₂ ∨ p₃ ≠ p₂
⊢ Real.tan (∠ p₂ p₃ p₁) * dist p₃ p₂ = dist p₁ p₂

Tactic:
ne_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
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₁ = p₂ ∨ p₂ ≠ p₃
⊢ Real.tan (∠ p₂ p₃ p₁) * dist p₃ p₂ = dist p₁ p₂
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₁ = p₂ ∨ p₃ ≠ p₂
⊢ dist p₃ p₂ / Real.cos (∠ p₂ p₃ p₁) = dist p₁ p₃

Tactic:
ne_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
p₁ p₂ p₃ : P
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₁ = p₂ ∨ p₂ ≠ p₃
⊢ dist p₃ p₂ / Real.cos (∠ p₂ p₃ p₁) = dist p₁ p₃
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
pp: case pos
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₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : Collinear ℝ {p₁, p₅, p₂}
hc₅₁₂₃₄ : Collinear ℝ {p₅, p₁, p₂, p₃, p₄}
hc₅₃₄ : Collinear ℝ {p₃, p₅, p₄}
hs₁₅₂ : (∡ p₁ p₅ p₂).sign = 0
hs₃₅₄ : (∡ p₃ p₅ p₄).sign = 0
⊢ (∡ p₁ p₅ p₂).sign = (∡ p₃ p₅ p₄).sign

Tactic:
hs₁₅₂,

Goal state after:
case pos
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₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : Collinear ℝ {p₁, p₅, p₂}
hc₅₁₂₃₄ : Collinear ℝ {p₅, p₁, p₂, p₃, p₄}
hc₅₃₄ : Collinear ℝ {p₃, p₅, p₄}
hs₁₅₂ : (∡ p₁ p₅ p₂).sign = 0
hs₃₅₄ : (∡ p₃ p₅ p₄).sign = 0
⊢ 0 = (∡ p₃ p₅ p₄).sign
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 : V
p : P
⊢ (↑((signedDist v) p)).linear = (innerₗ V) (NormedSpace.normalize v)

Tactic:
change (innerₗ V (normalize v)).comp (LinearMap.id - 0) = _

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
⊢ (innerₗ V) (NormedSpace.normalize v) ∘ₗ (LinearMap.id - 0) = (innerₗ V) (NormedSpace.normalize v)
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 : P
⊢ (s.signedInfDist p) p = ‖p -ᵥ ↑((orthogonalProjection s) p)‖

Tactic:
rw [signedInfDist_eq_signedDist_orthogonalProjection, signedDist_vsub_self, dist_eq_norm_vsub']

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₂⟫)
⊢ ⟪v, v⟫ * (r * r) + 2 * ⟪v, p₁ -ᵥ p₂⟫ * r + 0 = 0 ↔ r = 0 ∨ r = -2 * ⟪v, p₁ -ᵥ p₂⟫ / ⟪v, v⟫

Tactic:
rw [quadratic_eq_zero_iff hvi hd, neg_add_cancel, zero_div, neg_mul_eq_neg_mul, ←
    mul_sub_right_distrib, sub_eq_add_neg, ← mul_two, mul_assoc, mul_div_assoc, mul_div_mul_left,
    mul_div_assoc]

Goal state after:
case hc
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₂⟫)
⊢ 2 ≠ 0
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₂
⊢ 0 < ⟪p₂ -ᵥ p₁, s.center -ᵥ p₁⟫

Tactic:
have hp₁' : ‖p₁ -ᵥ s.center‖ = s.radius := norm_vsub_center_eq_radius 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
⊢ 0 < ⟪p₂ -ᵥ p₁, s.center -ᵥ p₁⟫
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
s : Sphere P
as : AffineSubspace ℝ P
p : P
hpar : as ∥ s.orthRadius p
hp : p ∈ s
q : P
hqs : q ∈ s
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius ≠ 0
⊢ as.direction = (s.orthRadius q).direction

Tactic:
rw [hpar.direction_eq, direction_orthRadius, direction_orthRadius]

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
as : AffineSubspace ℝ P
p : P
hpar : as ∥ s.orthRadius p
hp : p ∈ s
q : P
hqs : q ∈ s
hqas : q ∈ as
hqo : as ≤ s.orthRadius q
r : ℝ
hr : q -ᵥ s.center = r • (p -ᵥ s.center)
hrad : s.radius ≠ 0
⊢ (ℝ ∙ (p -ᵥ s.center))ᗮ = (ℝ ∙ (q -ᵥ s.center))ᗮ
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₃
⊢ ∡ (t.points i₁) (t.points i₂) (excenter t {i₁}) = ∡ (excenter t {i₁}) (t.points i₂) (t.points i₃) + ↑π

Tactic:
rw [(t.touchpoint_singleton_sbtw h₁₃ h₁₂ h₂₃.symm).symm.oangle_eq_add_pi_left
        ((t.excenterExists_singleton _).excenter_ne_point _),
    ← (t.sbtw_touchpoint_singleton h₁₂.symm h₂₃ h₁₃).oangle_eq_right, add_left_inj]
  have hd := (t.excenterExists_singleton i₁).dist_excenter_eq_dist_excenter i₃ i₁
  simp_rw [touchpoint, orthogonalProjectionSpan] at hd ⊢
  refine oangle_eq_of_dist_orthogonalProjection_eq (mem_affineSpan _ ?_) (mem_affineSpan _ ?_)
    ((t.excenterExists_singleton i₁).touchpoint_injective.ne h₁₃.symm) hd
  · simp
    grind
  · simp
    grind

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

Goal state before:
pp: case h.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 : ℝ := 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)
hcr₃ : insert p ps ⊆ Metric.sphere cc₃ cr₃
t₃ : ℝ
cc₃' : P
hcc₃' : cc₃' ∈ s
hcc₃'' : cc₃ = t₃ • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc₃'
hcr₃' : ∃ r, ∀ p₁ ∈ ps, dist p₁ cc₃ = r
⊢ { center := cc₃, radius := cr₃ } = { center := cc₂, radius := cr₂ }

Tactic:
rw [exists_dist_eq_iff_exists_dist_orthogonalProjection_eq hps cc₃, hcc₃'',
      orthogonalProjection_vadd_smul_vsub_orthogonalProjection _ _ hcc₃'] at hcr₃'

Goal state after:
case h.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 : ℝ := 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)
hcr₃ : insert p ps ⊆ Metric.sphere cc₃ cr₃
t₃ : ℝ
cc₃' : P
hcc₃' : cc₃' ∈ s
hcc₃'' : cc₃ = t₃ • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ cc₃'
hcr₃' : ∃ r, ∀ p₁ ∈ ps, dist p₁ ↑⟨cc₃', hcc₃'⟩ = r
⊢ { center := cc₃, radius := cr₃ } = { center := cc₂, radius := cr₂ }
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 : ‖x‖ * ‖x‖ * ‖x‖⁻¹ - ⟪x, y⟫ * ‖x‖⁻¹ = ‖y‖ * ‖y‖ * ‖y‖⁻¹ - ⟪x, y⟫ * ‖y‖⁻¹
⊢ ‖x‖ = ‖y‖

Tactic:
mul_self_mul_inv,

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 : ‖x‖ - ⟪x, y⟫ * ‖x‖⁻¹ = ‖y‖ * ‖y‖ * ‖y‖⁻¹ - ⟪x, y⟫ * ‖y‖⁻¹
⊢ ‖x‖ = ‖y‖
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 : ‖x‖ - ⟪x, y⟫ * ‖x‖⁻¹ = ‖y‖ * ‖y‖ * ‖y‖⁻¹ - ⟪x, y⟫ * ‖y‖⁻¹
⊢ ‖x‖ = ‖y‖

Tactic:
mul_self_mul_inv,

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 : ‖x‖ - ⟪x, y⟫ * ‖x‖⁻¹ = ‖y‖ - ⟪x, y⟫ * ‖y‖⁻¹
⊢ ‖x‖ = ‖y‖
Module: Mathlib.Geometry.Euclidean.Circumcenter

Goal state before:
pp: case intro.succ.succ
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
ι : Type u_3
hne : Nonempty ι
inst✝ : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
val✝ : Fintype ι
m : ℕ
hn : Fintype.card ι = m + 1 + 1
i : ι
ι2 : Type (max 0 u_3) := { x // x ≠ i }
hc : Fintype.card ι2 = m + 1
this : Nonempty ι2
ha2 : AffineIndependent ℝ fun i2 ↦ p ↑i2
hm :
  ∃! cs,
    cs.center ∈ affineSpan ℝ (Set.range fun i2 ↦ p ↑i2) ∧ (Set.range fun i2 ↦ p ↑i2) ⊆ Metric.sphere cs.center cs.radius
hr : Set.range p = insert (p i) (Set.range fun i2 ↦ p ↑i2)
⊢ ∃! cs,
    cs.center ∈ affineSpan ℝ (insert (p i) ↑(affineSpan ℝ (Set.range fun i2 ↦ p ↑i2))) ∧
      insert (p i) (Set.range fun i2 ↦ p ↑i2) ⊆ Metric.sphere cs.center cs.radius

Tactic:
refine existsUnique_dist_eq_of_insert (Set.range_nonempty _) (subset_affineSpan ℝ _) ?_ hm

Goal state after:
case intro.succ.succ
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
ι : Type u_3
hne : Nonempty ι
inst✝ : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
val✝ : Fintype ι
m : ℕ
hn : Fintype.card ι = m + 1 + 1
i : ι
ι2 : Type (max 0 u_3) := { x // x ≠ i }
hc : Fintype.card ι2 = m + 1
this : Nonempty ι2
ha2 : AffineIndependent ℝ fun i2 ↦ p ↑i2
hm :
  ∃! cs,
    cs.center ∈ affineSpan ℝ (Set.range fun i2 ↦ p ↑i2) ∧ (Set.range fun i2 ↦ p ↑i2) ⊆ Metric.sphere cs.center cs.radius
hr : Set.range p = insert (p i) (Set.range fun i2 ↦ p ↑i2)
⊢ p i ∉ affineSpan ℝ (Set.range fun i2 ↦ p ↑i2)
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: case inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h0 : o.oangle x y ≠ 0
hpi : o.oangle x y ≠ ↑π
hs : (o.oangle x (x - y)).sign = (o.oangle (y - x) y).sign
h : o.oangle x (x - y) = o.oangle (y - x) y
⊢ ‖x‖ = ‖y‖

Tactic:
← o.angle_eq_iff_oangle_eq_of_sign_eq (o.left_ne_zero_of_oangle_ne_zero h0)
      (sub_ne_zero_of_ne (o.ne_of_oangle_ne_zero h0))
      (sub_ne_zero_of_ne (o.ne_of_oangle_ne_zero h0).symm)
      (o.right_ne_zero_of_oangle_ne_zero h0) hs,

Goal state after:
case inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h0 : o.oangle x y ≠ 0
hpi : o.oangle x y ≠ ↑π
hs : (o.oangle x (x - y)).sign = (o.oangle (y - x) y).sign
h : angle x (x - y) = angle (y - x) y
⊢ ‖x‖ = ‖y‖