mathlib-initiative/mathlib-tactics huggingface dataset:
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:
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
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₂
⊢ ∠ p₂ p₃ p₁ = Real.arcsin (dist p₁ p₂ / dist p₁ p₃)

Tactic:
@ne_comm _ 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
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₁ -ᵥ p₂ ≠ 0 ∨ p₂ ≠ p₃
⊢ ∠ p₂ p₃ p₁ = Real.arcsin (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
⊢ InnerProductGeometry.angle (p₂ -ᵥ p₃) (p₂ -ᵥ p₃ + (p₁ -ᵥ p₂)) ≤ π / 2

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

Tactic:
@ne_comm _ 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
h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫ = 0
h0 : p₁ -ᵥ p₂ ≠ 0 ∨ p₂ ≠ p₃
⊢ Real.sin (∠ p₂ p₃ p₁) = dist p₁ p₂ / dist p₁ p₃
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)
⊢ ∡ p (↑((orthogonalProjection s) p)) p' = ↑(- -(π / 2)) ∨ ∡ p (↑((orthogonalProjection s) p)) p' = -↑(π / 2)

Tactic:
neg_neg,

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

Tactic:
rw [oangle_rev, neg_eq_iff_eq_neg, neg_eq_iff_eq_neg, or_comm, ← Real.Angle.coe_neg, neg_div,
    neg_neg, ← Real.Angle.coe_neg, ← neg_div]

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
s : AffineSubspace ℝ P
inst✝ : s.direction.HasOrthogonalProjection
hp : p ∉ s
h : p' ∈ s
hp' : p' ≠ ↑((orthogonalProjection s) p)
⊢ ∡ p (↑((orthogonalProjection s) p)) p' = ↑(π / 2) ∨ ∡ p (↑((orthogonalProjection s) p)) p' = ↑(-π / 2)
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)) (-(r • (o.rotation ↑(π / 2)) x)))
      (r⁻¹ • (o.rotation ↑(π / 2)) (-(r • (o.rotation ↑(π / 2)) x))) =
    ↑(Real.arctan r)

Tactic:
o.oangle_add_left_smul_rotation_pi_div_two,

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))
⊢ ↑(Real.arctan r⁻¹⁻¹) = ↑(Real.arctan r)

case neg.h
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))
⊢ -(r • (o.rotation ↑(π / 2)) x) ≠ 0
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
r : ℝ
hr0 : 0 ≤ r
hr : (r + 1) • y = x
⊢ |(o.oangle (y - x) y).toReal| < π / 2

Tactic:
rw [← hr, norm_smul, Real.norm_eq_abs, abs_of_pos (Left.add_pos_of_nonneg_of_pos hr0 one_pos),
      mul_left_eq_self₀, or_iff_left (norm_ne_zero_iff.2 hy), add_eq_right] at h

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
hn : ¬x = y
hy : y ≠ 0
r : ℝ
h : r = 0
hr0 : 0 ≤ r
hr : (r + 1) • 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
h : ∃ r > 0, r • v = w
⊢ signedDist v = signedDist w

Tactic:
obtain ⟨r, _, _⟩ := 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
v w : V
r : ℝ
left✝ : r > 0
right✝ : r • v = w
⊢ signedDist v = signedDist w
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₂, ((p₂ -ᵥ p₁) +ᵥ p₂) -ᵥ p₁⟫ = 0 ↔ ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫ = 0

Tactic:
vadd_vsub_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
c p₁ p₂ : P
⊢ ⟪c -ᵥ p₂, p₂ -ᵥ p₁ + (p₂ -ᵥ p₁)⟫ = 0 ↔ ⟪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₁ ((Equiv.pointReflection p₂) p₁) ↔ ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫ = 0

Tactic:
by
  rw [mem_perpBisector_iff_inner_eq_zero, midpoint_pointReflection_right,
    Equiv.pointReflection_apply, vadd_vsub_assoc, inner_add_right, add_self_eq_zero,
    ← neg_eq_zero, ← inner_neg_right, neg_vsub_eq_vsub_rev]

Goal state after:
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₁ c₂ p₁ p₂ : P
hc₁ : dist p₁ c₁ = dist p₂ c₁
hc₂ : dist p₁ c₂ = dist p₂ c₂
⊢ c₂ -ᵥ c₁ ∈ (ℝ ∙ (p₂ -ᵥ p₁))ᗮ

Tactic:
← direction_perpBisector

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₁ c₂ p₁ p₂ : P
hc₁ : dist p₁ c₁ = dist p₂ c₁
hc₂ : dist p₁ c₂ = dist p₂ c₂
⊢ c₂ -ᵥ c₁ ∈ (perpBisector p₁ p₂).direction
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₄ : P
hp₁₃ : Sbtw ℝ p₁ p p₃
hp₂₄ : Sbtw ℝ p₂ p p₄
⊢ (∡ p₄ p₃ p).sign = (∡ p₁ p₃ p₂).sign

Tactic:
Sbtw.oangle_sign_eq _ hp₂₄.symm,

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₄ : P
hp₁₃ : Sbtw ℝ p₁ p p₃
hp₂₄ : Sbtw ℝ p₂ p p₄
⊢ (∡ p p₃ p₂).sign = (∡ p₁ p₃ p₂).sign
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
r : ℝ
v : V
p₁ p₂ : P
⊢ ⟪(r • v +ᵥ p₁) -ᵥ p₂, (r • v +ᵥ p₁) -ᵥ p₂⟫ = ⟪v, v⟫ * r * r + 2 * ⟪v, p₁ -ᵥ p₂⟫ * r + ⟪p₁ -ᵥ p₂, p₁ -ᵥ p₂⟫

Tactic:
vadd_vsub_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
r : ℝ
v : V
p₁ p₂ : P
⊢ ⟪r • v + (p₁ -ᵥ p₂), r • v + (p₁ -ᵥ p₂)⟫ = ⟪v, v⟫ * r * r + 2 * ⟪v, p₁ -ᵥ p₂⟫ * r + ⟪p₁ -ᵥ p₂, p₁ -ᵥ p₂⟫
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
⊢ ⟪p -ᵥ ↑((orthogonalProjection s) p), ↑Classical.ofNonempty -ᵥ q⟫ = 0

Tactic:
apply s.direction.inner_left_of_mem_orthogonal

Goal state after:
case hu
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
⊢ ↑Classical.ofNonempty -ᵥ q ∈ s.direction

case hv
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
⊢ p -ᵥ ↑((orthogonalProjection s) p) ∈ s.directionᗮ
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₁]
i : Fin 2
⊢ b i ≠ 0

Tactic:
fin_cases i <;> simp [b, hc.symm, hp.symm]

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

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

Tactic:
← hp₁c₁,

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
hc₁s : c₁ ∈ s
hc₂s : c₂ ∈ s
hp₁s : p₁ ∈ s
hp₂s : p₂ ∈ s
r₁ r₂ : ℝ
hc : c₁ ≠ c₂
hp : p₁ ≠ p₂
hp₁c₁ : dist p₁ c₁ = r₁
hp₂c₁ : dist p₂ c₁ = r₁
hp₁c₂ : dist p₁ c₂ = r₂
hp₂c₂ : dist p₂ c₂ = r₂
ho : ⟪c₂ -ᵥ c₁, p₂ -ᵥ p₁⟫ = 0
b : Fin 2 → V := ![c₂ -ᵥ c₁, p₂ -ᵥ p₁]
hb : LinearIndependent ℝ b
hbs : Submodule.span ℝ (Set.range b) = s.direction
hv : ∀ v ∈ s.direction, ∃ t₁ t₂, v = t₁ • (c₂ -ᵥ c₁) + t₂ • (p₂ -ᵥ p₁)
t₁ t₂ : ℝ
hop : t₁ = 0
hps : t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ ∈ s
hpc₁ : dist (t₂ • (p₂ -ᵥ p₁) +ᵥ p₁) c₁ = dist p₁ c₁
hpc₂ : dist (t₂ • (p₂ -ᵥ p₁) +ᵥ p₁) c₂ = r₂
hp' : p₂ -ᵥ p₁ ≠ 0
hp₂ : dist (1 • (p₂ -ᵥ p₁) +ᵥ p₁) c₁ = dist p₁ c₁
⊢ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₁ ∨ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₂
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 : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
o : P := s.center
t : ℝ
hpt : (AffineMap.lineMap p₁ p₂) t = p
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
hne₁ : p ≠ p₁
hne₂ : p ≠ p₂
ht₀' : 0 < t
ht₁' : t < 1
u : V := p₁ -ᵥ o
v : V := p₂ -ᵥ o
hu : ‖u‖ = s.radius
hv : ‖v‖ = s.radius
huv : u ≠ v
⊢ (t • (p₂ -ᵥ p₁) +ᵥ p₁) -ᵥ o = (1 - t) • u + t • v

Tactic:
vadd_vsub_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
p₁ p₂ p : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
o : P := s.center
t : ℝ
hpt : (AffineMap.lineMap p₁ p₂) t = p
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
hne₁ : p ≠ p₁
hne₂ : p ≠ p₂
ht₀' : 0 < t
ht₁' : t < 1
u : V := p₁ -ᵥ o
v : V := p₂ -ᵥ o
hu : ‖u‖ = s.radius
hv : ‖v‖ = s.radius
huv : u ≠ v
⊢ t • (p₂ -ᵥ p₁) + (p₁ -ᵥ o) = (1 - t) • u + t • v
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 : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
o : P := s.center
t : ℝ
hpt : (AffineMap.lineMap p₁ p₂) t = p
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
hne₁ : p ≠ p₁
hne₂ : p ≠ p₂
ht₀' : 0 < t
ht₁' : t < 1
u : V := p₁ -ᵥ o
v : V := p₂ -ᵥ o
hu : ‖u‖ = s.radius
hv : ‖v‖ = s.radius
huv : u ≠ v
hpo : p -ᵥ o = (1 - t) • u + t • v
hmem : (1 - t) • u + t • v ∈ interior (Metric.closedBall 0 s.radius)
⊢ ‖(1 - t) • u + t • v‖ < s.radius

Tactic:
rwa [interior_closedBall _ (fun h : s.radius = 0 => huv <|
      (norm_eq_zero.mp (hu.trans h)).trans (norm_eq_zero.mp (hv.trans h)).symm),
    Metric.mem_ball, dist_zero_right] at hmem

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

Goal state before:
pp: case neg.refine_3
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : Nontrivial V
s₁ s₂ : Sphere P
h : dist s₂.center s₁.center = s₂.radius - s₁.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.center = s₂.center
ha : |s₂.radius - s₁.radius| = s₂.radius - s₁.radius
hr0 : s₂.radius - s₁.radius ≠ 0
⊢ s₂.center = s₁.center ∨
    (AffineMap.lineMap s₂.center s₁.center) (s₂.radius / (s₂.radius - s₁.radius)) ∈
      ⇑(AffineMap.lineMap s₂.center s₁.center) '' Set.Ici 1

Tactic:
simp only [Ne.symm h0, Set.mem_image, Set.mem_Ici, AffineMap.lineMap_eq_lineMap_iff,
          false_or, exists_eq_right]

Goal state after:
case neg.refine_3
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : Nontrivial V
s₁ s₂ : Sphere P
h : dist s₂.center s₁.center = s₂.radius - s₁.radius
h₁ : 0 ≤ s₁.radius
h₂ : 0 ≤ s₂.radius
h0 : ¬s₁.center = s₂.center
ha : |s₂.radius - s₁.radius| = s₂.radius - s₁.radius
hr0 : s₂.radius - s₁.radius ≠ 0
⊢ 1 ≤ s₂.radius / (s₂.radius - 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
p₁ p₂ p₃ : P
s : Sphere P
hd : s.IsDiameter p₁ p₃
o : P := s.center
⊢ ⟪p₁ -ᵥ p₂, p₃ -ᵥ p₂⟫_ℝ = 0 ↔ dist s.center p₂ = s.radius

Tactic:
have h_center : o = midpoint ℝ p₁ p₃ := hd.midpoint_eq_center.symm

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₃
⊢ ⟪p₁ -ᵥ p₂, p₃ -ᵥ p₂⟫_ℝ = 0 ↔ dist s.center p₂ = s.radius
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
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
⊢ (s.reindex e).insphere = s.insphere

Tactic:
simp_rw [insphere, exsphere_reindex]

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
⊢ s.exsphere (Finset.map e.symm.toEmbedding ∅) = s.exsphere ∅
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
i : Fin (n + 1)
⊢ SignType.sign ((s.signedInfDist i) s.incenter) = 1

Tactic:
by
  convert! s.excenterExists_empty.sign_signedInfDist_excenter i
  simp

Goal state after:
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₂
⊢ dist p₁ (midpoint ℝ p₁ p₂) /
      («o».oangle (midpoint ℝ p₁ p₂ -ᵥ p₁)
          ((((∡ p₂ p₁ s.center).tan / 2) • («o».rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂) -ᵥ p₁)).cos =
    dist p₁ (((∡ p₂ p₁ s.center).tan / 2) • («o».rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂)

Tactic:
vadd_vsub_assoc,

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₂
⊢ dist p₁ (midpoint ℝ p₁ p₂) /
      («o».oangle (midpoint ℝ p₁ p₂ -ᵥ p₁)
          (((∡ p₂ p₁ s.center).tan / 2) • («o».rotation ↑(π / 2)) (p₂ -ᵥ p₁) + (midpoint ℝ p₁ p₂ -ᵥ p₁))).cos =
    dist p₁ (((∡ p₂ p₁ s.center).tan / 2) • («o».rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂)
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₁)
          ((∡ p₂ p₁ s.center).tan • («o».rotation ↑(π / 2)) (midpoint ℝ p₁ p₂ -ᵥ p₁) + (midpoint ℝ p₁ p₂ -ᵥ p₁))).cos =
    ‖((∡ p₂ p₁ s.center).tan • («o».rotation ↑(π / 2)) (midpoint ℝ p₁ p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂) -ᵥ p₁‖

Tactic:
vadd_vsub_assoc,

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₁‖ /
      («o».oangle (midpoint ℝ p₁ p₂ -ᵥ p₁)
          ((∡ p₂ p₁ s.center).tan • («o».rotation ↑(π / 2)) (midpoint ℝ p₁ p₂ -ᵥ p₁) + (midpoint ℝ p₁ p₂ -ᵥ p₁))).cos =
    ‖(∡ p₂ p₁ s.center).tan • («o».rotation ↑(π / 2)) (midpoint ℝ p₁ p₂ -ᵥ p₁) + (midpoint ℝ p₁ p₂ -ᵥ p₁)‖
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: case inr
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 y = 0 ∨ o.oangle x y = ↑π
h : o.oangle x (x - y) = o.oangle (y - x) y + ↑π
⊢ ‖x‖ = ‖y‖

Tactic:
simp [h0, hpi] at hs

Goal state after:
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
inst✝¹ : Module.Oriented ℝ V (Fin 2)
inst✝ : Fact (Module.finrank ℝ V = 2)
p₁ p₂ p₃ : P
h21 : p₂ ≠ p₁
h32 : p₃ ≠ p₂
h13 : p₁ ≠ p₃
⊢ ∡ p₁ p₂ p₃ + ∡ p₂ p₃ p₁ + ∡ p₃ p₁ p₂ = ↑π

Tactic:
by
  simpa only [neg_vsub_eq_vsub_rev] using!
    positiveOrientation.oangle_add_cyc3_neg_left (vsub_ne_zero.mpr h21) (vsub_ne_zero.mpr h32)
      (vsub_ne_zero.mpr h13)

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

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
n : ℕ
r : ℝ
s : Simplex ℝ P n
p₁ : P
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₁' : ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter
h : s.points 0 ∈ affineSpan ℝ (Set.range s.points)
⊢ dist s.circumcenter p₁ * dist s.circumcenter p₁ = r * r - s.circumradius * s.circumradius

Tactic:
← h₁ 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
n : ℕ
r : ℝ
s : Simplex ℝ P n
p₁ : P
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₁' : ↑(s.orthogonalProjectionSpan p₁) = s.circumcenter
h : s.points 0 ∈ affineSpan ℝ (Set.range s.points)
⊢ dist s.circumcenter p₁ * dist s.circumcenter p₁ =
    dist (s.points 0) p₁ * dist (s.points 0) p₁ - s.circumradius * s.circumradius
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
fs : Finset (Fin (n + 1))
⊢ ∑ i ∈ fs, centroidWeights ℝ fs i • (s.points i -ᵥ Classical.choice ⋯) +ᵥ Classical.choice ⋯ =
    (∑ i, (if i ∈ fs then (↑(#fs))⁻¹ else 0) • (s.pointsWithCircumcenter (pointIndex i) -ᵥ Classical.choice ⋯) +
        0 • (s.pointsWithCircumcenter circumcenterIndex -ᵥ Classical.choice ⋯)) +ᵥ
      Classical.choice ⋯

Tactic:
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
fs : Finset (Fin (n + 1))
⊢ ∑ i ∈ fs, centroidWeights ℝ fs i • (s.points i -ᵥ Classical.choice ⋯) +ᵥ Classical.choice ⋯ =
    (∑ i, (if i ∈ fs then (↑(#fs))⁻¹ else 0) • (s.points i -ᵥ Classical.choice ⋯) +
        0 • (s.pointsWithCircumcenter circumcenterIndex -ᵥ Classical.choice ⋯)) +ᵥ
      Classical.choice ⋯
Module: Mathlib.Geometry.Euclidean.Circumcenter

Goal state before:
pp: n : ℕ
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
⊢ ∑ x with x = i₁ ∨ x = i₂, 1 + ∑ x with ¬(x = i₁ ∨ x = i₂), 0 + -1 = 1

Tactic:
sum_const,

Goal state after:
n : ℕ
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
⊢ #{x | x = i₁ ∨ x = i₂} • 1 + #{x | ¬(x = i₁ ∨ x = i₂)} • 0 + -1 = 1