mathlib-initiative/mathlib-tactics huggingface dataset:
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
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
r₁ r₂ : 𝕜
v : V
hv : v ∈ s.directionᗮ
⊢ ‖(r₁ • v +ᵥ p₁) -ᵥ (r₂ • v +ᵥ p₂)‖ * ‖(r₁ • v +ᵥ p₁) -ᵥ (r₂ • v +ᵥ p₂)‖ =
    ‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖ * ‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖

Tactic:
vsub_vadd_eq_vsub_sub,

Goal state after:
𝕜 : 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
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
r₁ r₂ : 𝕜
v : V
hv : v ∈ s.directionᗮ
⊢ ‖(r₁ • v +ᵥ p₁) -ᵥ p₂ - r₂ • v‖ * ‖(r₁ • v +ᵥ p₁) -ᵥ p₂ - r₂ • v‖ =
    ‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖ * ‖p₁ -ᵥ p₂ + (r₁ - r₂) • v‖
Module: Mathlib.Geometry.Euclidean.Projection

Goal state before:
pp: case mp
𝕜 : 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₁ s₂ : AffineSubspace 𝕜 P
inst✝³ : Nonempty ↥s₁
inst✝² : Nonempty ↥s₂
inst✝¹ : s₁.direction.HasOrthogonalProjection
inst✝ : s₂.direction.HasOrthogonalProjection
p : P
h :
  (↑((orthogonalProjection s₁) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s₁) p) =
    (↑((orthogonalProjection s₂) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s₂) p)
⊢ ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection s₂) p)

Tactic:
← @vsub_eq_zero_iff_eq V,

Goal state after:
case mp
𝕜 : 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₁ s₂ : AffineSubspace 𝕜 P
inst✝³ : Nonempty ↥s₁
inst✝² : Nonempty ↥s₂
inst✝¹ : s₁.direction.HasOrthogonalProjection
inst✝ : s₂.direction.HasOrthogonalProjection
p : P
h :
  ((↑((orthogonalProjection s₁) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s₁) p)) -ᵥ
      ((↑((orthogonalProjection s₂) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s₂) p)) =
    0
⊢ ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection s₂) p)
Module: Mathlib.Geometry.Euclidean.Projection

Goal state before:
pp: case mp
𝕜 : 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₁ s₂ : AffineSubspace 𝕜 P
inst✝³ : Nonempty ↥s₁
inst✝² : Nonempty ↥s₂
inst✝¹ : s₁.direction.HasOrthogonalProjection
inst✝ : s₂.direction.HasOrthogonalProjection
p : P
h :
  ((↑((orthogonalProjection s₁) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s₁) p)) -ᵥ
      ((↑((orthogonalProjection s₂) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s₂) p)) =
    0
⊢ ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection s₂) p)

Tactic:
vsub_vadd_eq_vsub_sub,

Goal state after:
case mp
𝕜 : 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₁ s₂ : AffineSubspace 𝕜 P
inst✝³ : Nonempty ↥s₁
inst✝² : Nonempty ↥s₂
inst✝¹ : s₁.direction.HasOrthogonalProjection
inst✝ : s₂.direction.HasOrthogonalProjection
p : P
h :
  ((↑((orthogonalProjection s₁) p) -ᵥ p) +ᵥ ↑((orthogonalProjection s₁) p)) -ᵥ ↑((orthogonalProjection s₂) p) -
      (↑((orthogonalProjection s₂) p) -ᵥ p) =
    0
⊢ ↑((orthogonalProjection s₁) p) = ↑((orthogonalProjection s₂) p)
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
⊢ o.oangle x ((o.rotation θ) y) = o.oangle x y + θ

Tactic:
by
  simp only [oangle, o.kahler_rotation_right]
  rw [Complex.arg_mul_coe_angle, Real.Angle.arg_toCircle]
  · abel
  · exact Circle.coe_ne_zero _
  · exact o.kahler_ne_zero hx hy

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 : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ line[ℝ, s.altitudeFoot i, s.points i] = s.altitude i

Tactic:
rw [affineSpan_pair_eq_altitude_iff]

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
i : Fin (n + 1)
⊢ s.altitudeFoot i ≠ s.points i ∧
    s.altitudeFoot i ∈ affineSpan ℝ (Set.range s.points) ∧
      s.altitudeFoot i -ᵥ s.points i ∈ (affineSpan ℝ (s.points '' {i}ᶜ)).directionᗮ
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 : V
r : ℝ
hx : ¬x = 0
hr : r < 0
⊢ SameRay ℝ x (r • x) ∨ x ≠ 0 ∧ r • x ≠ 0 ∧ SameRay ℝ x (-(r • x))

Tactic:
rw [← neg_smul]
      exact Or.inr ⟨hx, smul_ne_zero hr.ne hx,
        SameRay.sameRay_pos_smul_right x (Left.neg_pos_iff.2 hr)⟩

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
r : ℝ
hp₂ : (AffineMap.lineMap p₁ p₃) r = p₂
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hr0' : r ≠ 0
hr1' : r ≠ 1
hr0 : 0 < r
hr1 : r < 1
⊢ p₃ -ᵥ (r • (p₃ -ᵥ p₁) +ᵥ p₁) = (-(1 - r) / r) • (p₁ -ᵥ (r • (p₃ -ᵥ p₁) +ᵥ p₁))

Tactic:
vsub_vadd_eq_vsub_sub,

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
r : ℝ
hp₂ : (AffineMap.lineMap p₁ p₃) r = p₂
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hr0' : r ≠ 0
hr1' : r ≠ 1
hr0 : 0 < r
hr1 : r < 1
⊢ p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • (p₁ -ᵥ (r • (p₃ -ᵥ p₁) +ᵥ p₁))
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.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
p₁ p₂ p₃ : P
r : ℝ
hp₂ : (AffineMap.lineMap p₁ p₃) r = p₂
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hr0' : r ≠ 0
hr1' : r ≠ 1
hr0 : 0 < r
hr1 : r < 1
⊢ p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • (p₁ -ᵥ (r • (p₃ -ᵥ p₁) +ᵥ p₁))

Tactic:
vsub_vadd_eq_vsub_sub,

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
r : ℝ
hp₂ : (AffineMap.lineMap p₁ p₃) r = p₂
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
hr0' : r ≠ 0
hr1' : r ≠ 1
hr0 : 0 < r
hr1 : r < 1
⊢ p₃ -ᵥ p₁ - r • (p₃ -ᵥ p₁) = (-(1 - r) / r) • (p₁ -ᵥ p₁ - r • (p₃ -ᵥ p₁))
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 z : V
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ (↑‖y‖ ^ 2 * (o.kahler x) z).arg = ((o.kahler x) z).arg

Tactic:
exact mod_cast Complex.arg_real_mul _ (by positivity : 0 < ‖y‖ ^ 2)

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₂ ≠ 0 ∨ p₂ = p₃
⊢ 0 < ∠ p₂ p₃ p₁

Tactic:
← @vsub_eq_zero_iff_eq V,

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₂ ≠ 0 ∨ p₂ -ᵥ p₃ = 0
⊢ 0 < ∠ p₂ p₃ p₁
Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

Goal state before:
pp: case neg
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₁ p₂ (midpoint ℝ p₃ p₂) = ∡ p₁ p₂ p₃

Tactic:
exact (sbtw_midpoint_of_ne ℝ h).symm.oangle_eq_right

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

Tactic:
← @vsub_eq_zero_iff_eq V,

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₂ = 0 ∨ p₂ -ᵥ p₃ ≠ 0
⊢ 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₃ ≠ 0
⊢ dist p₃ p₂ / Real.cos (∠ p₂ p₃ p₁) = dist p₁ p₃

Tactic:
← @vsub_eq_zero_iff_eq V,

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₂ = 0 ∨ p₂ -ᵥ p₃ ≠ 0
⊢ dist p₃ p₂ / Real.cos (∠ p₂ 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₂ ≠ 0 ∨ p₂ = p₃
⊢ dist p₁ p₂ / Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₃

Tactic:
← @vsub_eq_zero_iff_eq V,

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₂ ≠ 0 ∨ p₂ -ᵥ p₃ = 0
⊢ dist p₁ p₂ / Real.sin (∠ p₂ p₃ p₁) = dist 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)
hs : (o.oangle y (y - x)).sign = 1
⊢ ‖y‖ / (o.oangle y (y - x)).cos = ‖y - x‖

Tactic:
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.cos_coe,
    InnerProductGeometry.norm_div_cos_angle_sub_of_inner_eq_zero
      (o.inner_rev_eq_zero_of_oangle_eq_pi_div_two h)
      (Or.inl (o.right_ne_zero_of_oangle_eq_pi_div_two h))]

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)
⊢ ‖x‖ / (o.oangle (x - y) x).cos = ‖x - y‖

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢
  exact (-o).norm_div_cos_oangle_sub_right_of_oangle_eq_pi_div_two 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₂ ≠ 0 ∨ p₂ = p₃
⊢ dist p₁ p₂ / Real.tan (∠ p₂ p₃ p₁) = dist p₃ p₂

Tactic:
← @vsub_eq_zero_iff_eq V,

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₂ ≠ 0 ∨ p₂ -ᵥ p₃ = 0
⊢ dist p₁ p₂ / Real.tan (∠ p₂ p₃ p₁) = dist p₃ p₂
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
hi : ⟪p₂ -ᵥ p₁, p -ᵥ midpoint ℝ p₁ p₂⟫ = 0
⊢ ∃ r, r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = p

Tactic:
@Orientation.inner_eq_zero_iff_eq_zero_or_eq_smul_rotation_pi_div_two V _ _ _ o,

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

Tactic:
vsub_vadd_eq_vsub_sub,

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ : P
h : p₁ ≠ p₂
r : ℝ
⊢ ‖p₁ -ᵥ midpoint ℝ p₁ p₂ - r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁)‖ =
    ‖p₂ -ᵥ midpoint ℝ p₁ p₂ - r • (o.rotation ↑(π / 2)) (p₂ -ᵥ p₁)‖
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) + x) (r⁻¹ • (o.rotation ↑(π / 2)) (-(r • (o.rotation ↑(π / 2)) x))) =
    ↑(Real.arctan r)

Tactic:
nth_rw 2 [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)) (-(r • (o.rotation ↑(π / 2)) x)))
      (r⁻¹ • (o.rotation ↑(π / 2)) (-(r • (o.rotation ↑(π / 2)) x))) =
    ↑(Real.arctan r)
Module: Mathlib.Geometry.Euclidean.Angle.Bisector

Goal state before:
pp: case refine_2.inr
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₁ s₂ : AffineSubspace ℝ P
inst✝¹ : s₁.direction.HasOrthogonalProjection
inst✝ : s₂.direction.HasOrthogonalProjection
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
h' : p ∈ s₁
this✝ : Nonempty ↥s₁
this : Nonempty ↥s₂
h : ∠ p p' p = ∠ p p' ↑((orthogonalProjection s₂) p)
hpp' : p ≠ p'
⊢ p ∈ s₂

Tactic:
· by_contra hn
      rw [angle_self_of_ne hpp', angle_comm,
        angle_eq_arcsin_of_angle_eq_pi_div_two (angle_self_orthogonalProjection p hp'₂),
        Real.zero_eq_arcsin_iff, div_eq_zero_iff] at h
      · simp only [dist_eq_zero, hpp', or_false] at h
        rw [eq_comm] at h
        simp [orthogonalProjection_eq_self_iff, hn] at h
      · exact .inl (Ne.symm (orthogonalProjection_eq_self_iff.symm.not.1 hn))

Goal state after:
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₄ 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₂}
s : Set (P × P × P) := (fun x ↦ (↑x.1, p₅, x.2 +ᵥ ↑x.1)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p ↦ ∡ p.1 p.2.1 p.2.2) s
q : P
r : ℝ
hv0 : r • (p₂ -ᵥ p₁) ≠ 0
hq : q ∈ line[ℝ, p₁, p₂]
⊢ q -ᵥ (r • (p₂ -ᵥ p₁) +ᵥ q) ≠ 0

Tactic:
vsub_vadd_eq_vsub_sub,

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
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₂}
s : Set (P × P × P) := (fun x ↦ (↑x.1, p₅, x.2 +ᵥ ↑x.1)) '' Set.univ ×ˢ {v | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
hf : ContinuousOn (fun p ↦ ∡ p.1 p.2.1 p.2.2) s
q : P
r : ℝ
hv0 : r • (p₂ -ᵥ p₁) ≠ 0
hq : q ∈ line[ℝ, p₁, p₂]
⊢ q -ᵥ q - r • (p₂ -ᵥ p₁) ≠ 0
Module: Mathlib.Geometry.Euclidean.Angle.Bisector

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✝¹ : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p p' : P
s₁ s₂ : AffineSubspace ℝ P
hp'₁ : p' ∈ s₁
hp'₂ : p' ∈ s₂
hp₁ : ↑((orthogonalProjection s₁) p) ≠ p'
hp₂ : ↑((orthogonalProjection s₂) p) ≠ p'
h : ∡ (↑((orthogonalProjection s₁) p)) p' p = ∡ p p' ↑((orthogonalProjection s₂) p)
⊢ ∡ (↑((orthogonalProjection s₁) p)) p' p = ∡ p p' ↑((orthogonalProjection s₂) p) ∨
    Wbtw ℝ p' ↑((orthogonalProjection s₁) p) ↑((orthogonalProjection s₂) p) ∨
      Wbtw ℝ p' ↑((orthogonalProjection s₂) p) ↑((orthogonalProjection s₁) p)

Tactic:
exact .inl h

Goal state after:
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₄ : P
hp₁ : p₁ ≠ p₂
hp₄ : p₄ ≠ p₂
h : SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂)
r : ℝ
hr : 0 < r
he : r • (p₁ -ᵥ p₂) = p₄ -ᵥ p₂
⊢ Wbtw ℝ p₂ p₁ p₄ ∨ Wbtw ℝ p₂ p₄ p₁

Tactic:
rw [← vsub_vadd p₁ p₂, ← vsub_vadd p₄ p₂, ← he]

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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ≠ p₂
hp₄ : p₄ ≠ p₂
h : SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂)
r : ℝ
hr : 0 < r
he : r • (p₁ -ᵥ p₂) = p₄ -ᵥ p₂
⊢ Wbtw ℝ p₂ ((p₁ -ᵥ p₂) +ᵥ p₂) (r • (p₁ -ᵥ p₂) +ᵥ p₂) ∨ Wbtw ℝ p₂ (r • (p₁ -ᵥ p₂) +ᵥ p₂) ((p₁ -ᵥ p₂) +ᵥ p₂)
Module: Mathlib.Geometry.Euclidean.Basic

Goal state before:
pp: case refine_2.«1».«0»
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₁]
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ ⟪b ((fun i ↦ i) ⟨1, ⋯⟩), b ((fun i ↦ i) ⟨0, ⋯⟩)⟫ = 0

Tactic:
rw [real_inner_comm]
        exact ho

Goal state after:
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
s : Set P
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv0 : v ≠ 0
c : P
r : ℝ
hs : ∀ p ∈ s, dist p c = r
hs' : ∀ (i : Fin 3), dist (p i) c = r
f : Fin 3 → ℝ
hf : ∀ (i : Fin 3), p i = f i • v +ᵥ p 0
hsd : ∀ (i : Fin 3), dist (f i • v +ᵥ p 0) c = r
hf0' : f 0 • v +ᵥ p 0 = p 0
⊢ f 0 = 0

Tactic:
← @vsub_eq_zero_iff_eq V,

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 : Set P
p : Fin 3 → P
hps : Set.range p ⊆ s
hpi : Function.Injective p
v : V
hv0 : v ≠ 0
c : P
r : ℝ
hs : ∀ p ∈ s, dist p c = r
hs' : ∀ (i : Fin 3), dist (p i) c = r
f : Fin 3 → ℝ
hf : ∀ (i : Fin 3), p i = f i • v +ᵥ p 0
hsd : ∀ (i : Fin 3), dist (f i • v +ᵥ p 0) c = r
hf0' : (f 0 • v +ᵥ p 0) -ᵥ p 0 = 0
⊢ f 0 = 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
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
hv : v ∈ Submodule.span ℝ (Set.range b)
hr : Set.range b = {c₂ -ᵥ c₁, p₂ -ᵥ p₁}
⊢ ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)

Tactic:
hr,

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
hv : v ∈ Submodule.span ℝ {c₂ -ᵥ c₁, p₂ -ᵥ p₁}
hr : Set.range b = {c₂ -ᵥ c₁, p₂ -ᵥ p₁}
⊢ ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

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
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
hr0 : r ≠ 0
⊢ ℝ ∙ (p -ᵥ s.center) = ℝ ∙ (q -ᵥ s.center)

Tactic:
hr,

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
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
hr0 : r ≠ 0
⊢ ℝ ∙ (p -ᵥ s.center) = ℝ ∙ r • (p -ᵥ s.center)
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
⊢ dist p₁ p₂ = s.radius + s.radius

Tactic:
hr,

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
⊢ 2 * s.radius = s.radius + s.radius