mathlib-initiative/mathlib-tactics huggingface dataset:
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
⊢ (o.oangle (x + y) y).sign = (o.oangle x y).sign

Tactic:
rw [← o.oangle_sign_add_smul_left x y 1, one_smul]

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
⊢ (2 • o.oangle (y - x) y).sign = (↑π - 2 • o.oangle (y - x) y).sign

Tactic:
Real.Angle.sign_pi_sub

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
⊢ (2 • o.oangle (y - x) y).sign = (2 • o.oangle (y - x) y).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 q : P
c₁ c₂ : ℝ
⊢ ((signedDist v) ((AffineMap.lineMap p q) c₁)) ((AffineMap.lineMap p q) c₂) = (c₂ - c₁) * ((signedDist v) p) q

Tactic:
trans c₂ * signedDist v p q + c₁ * signedDist v q 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
v : V
p q : P
c₁ c₂ : ℝ
⊢ ((signedDist v) ((AffineMap.lineMap p q) c₁)) ((AffineMap.lineMap p q) c₂) =
    c₂ * ((signedDist v) p) q + c₁ * ((signedDist v) q) p

V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
v : V
p q : P
c₁ c₂ : ℝ
⊢ c₂ * ((signedDist v) p) q + c₁ * ((signedDist v) q) p = (c₂ - c₁) * ((signedDist v) p) q
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
⊢ discrim ⟪v, v⟫ (2 * ⟪v, p₁ -ᵥ p₂⟫) 0 = 2 * ⟪v, p₁ -ᵥ p₂⟫ * (2 * ⟪v, p₁ -ᵥ p₂⟫)

Tactic:
rw [discrim]

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

Goal state before:
pp: P : Type u_2
inst✝ : MetricSpace P
p₁ p₂ : P
s : Sphere P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
⊢ dist p₁ s.center = dist p₂ s.center

Tactic:
rw [mem_sphere.1 hp₁, mem_sphere.1 hp₂]

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
⊢ f 0 = 0

Tactic:
have hf0' := hf 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
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' : p 0 = f 0 • v +ᵥ p 0
⊢ f 0 = 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
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' : p 0 = f 0 • v +ᵥ p 0
⊢ f 0 = 0

Tactic:
rw [eq_comm, ← @vsub_eq_zero_iff_eq V, vadd_vsub, smul_eq_zero] at hf0'

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 = 0 ∨ v = 0
⊢ f 0 = 0
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
⊢ AffineIndependent ℝ ![t.points i₁, t.points i₂, t.points i₃]

Tactic:
convert!
      t.independent.comp_embedding
        ⟨![i₁, i₂, i₃], by
          intro i j hij
          fin_cases i <;> fin_cases j <;> simp_all⟩

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 : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
p : P
⊢ ![t.points i₁, t.points i₂, t.points i₃] = t.points ∘ ⇑{ toFun := ![i₁, i₂, i₃], inj' := ⋯ }
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:
(t.touchpoint_singleton_sbtw h₁₃ h₁₂ h₂₃.symm).symm.oangle_eq_add_pi_left
        ((t.excenterExists_singleton _).excenter_ne_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
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₃
⊢ ∡ (touchpoint t {i₁} i₃) (t.points i₂) (excenter t {i₁}) + ↑π = ∡ (excenter t {i₁}) (t.points i₂) (t.points i₃) + ↑π
Module: Mathlib.Geometry.Euclidean.Angle.Incenter

Goal state before:
pp: case inr.inr.inl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
signs : Finset (Fin 3)
h : ∡ (excenter t {i₂}) (t.points i₁) (t.points i₃) + ↑π = ∡ (excenter t {i₂}) (t.points i₁) (t.points i₃)
hs : excenter t signs = excenter t {i₂}
⊢ excenter t signs = incenter t ∨ excenter t signs = excenter t {i₁}

Tactic:
simp [Real.Angle.pi_ne_zero] at h

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Incenter

Goal state before:
pp: case inr.inr.inr
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
signs : Finset (Fin 3)
h : -∡ (excenter t {i₃}) (t.points i₁) (t.points i₂) = -(∡ (excenter t {i₃}) (t.points i₁) (t.points i₂) + ↑π)
hs : excenter t signs = excenter t {i₃}
⊢ excenter t signs = incenter t ∨ excenter t signs = excenter t {i₁}

Tactic:
simp [Real.Angle.pi_ne_zero] at h

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Incenter

Goal state before:
pp: case inl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
signs : Finset (Fin 3)
h : ∡ (incenter t) (t.points i₁) (t.points i₃) = ∡ (incenter t) (t.points i₁) (t.points i₃) + ↑π
hs : excenter t signs = incenter t
⊢ excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}

Tactic:
simp [Real.Angle.pi_ne_zero] at h

Goal state after:
Module: Mathlib.Geometry.Euclidean.Angle.Incenter

Goal state before:
pp: case inr.inl
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
signs : Finset (Fin 3)
h : ∡ (excenter t {i₁}) (t.points i₁) (t.points i₃) = ∡ (excenter t {i₁}) (t.points i₁) (t.points i₃) + ↑π
hs : excenter t signs = excenter t {i₁}
⊢ excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}

Tactic:
simp [Real.Angle.pi_ne_zero] at h

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

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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
i : Fin (n + 1)
h : i ∈ signs
⊢ s.excenterWeightsUnnorm signsᶜ i = (-s.excenterWeightsUnnorm signs) i

Tactic:
simp [excenterWeightsUnnorm, h]

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

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
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
i : Fin (n + 1)
h : i ∉ signs
⊢ s.excenterWeightsUnnorm signsᶜ i = (-s.excenterWeightsUnnorm signs) i

Tactic:
simp [excenterWeightsUnnorm, h]

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

Goal state before:
pp: case a
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
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
h : j ≠ i
⊢ s.excenterWeightsUnnorm {i} j = (s.height j)⁻¹

Tactic:
simp [excenterWeightsUnnorm, h]

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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
⊢ ↑((s.restrict S hS).excenter signs) = s.excenter signs

Tactic:
← s.excenterExists_restrict S hS

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))
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
h : (s.restrict S hS).ExcenterExists signs
⊢ ↑((s.restrict S hS).excenter signs) = s.excenter signs
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))
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
h : (s.restrict S hS).ExcenterExists signs
⊢ ↑((s.restrict S hS).excenter signs) = s.excenter signs

Tactic:
have := Nonempty.map (AffineSubspace.inclusion hS) inferInstance

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))
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
h : (s.restrict S hS).ExcenterExists signs
this : Nonempty ↥S
⊢ ↑((s.restrict S hS).excenter signs) = s.excenter signs
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₂
r : ℝ
hr : r • («o».rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = s.center
⊢ ((«o».oangle (midpoint ℝ p₁ p₂ -ᵥ p₁)
              (r • («o».rotation ↑(π / 2)) (2 • (midpoint ℝ p₁ p₂ -ᵥ p₁)) + (midpoint ℝ p₁ p₂ -ᵥ p₁))).tan /
          2) •
        («o».rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ
      midpoint ℝ p₁ p₂ =
    r • («o».rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂

Tactic:
map_smul,

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₂
r : ℝ
hr : r • («o».rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = s.center
⊢ ((«o».oangle (midpoint ℝ p₁ p₂ -ᵥ p₁)
              (r • 2 • («o».rotation ↑(π / 2)) (midpoint ℝ p₁ p₂ -ᵥ p₁) + (midpoint ℝ p₁ p₂ -ᵥ p₁))).tan /
          2) •
        («o».rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ
      midpoint ℝ p₁ p₂ =
    r • («o».rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂
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 ≠ π
h : ⟪x, x - y⟫ * (‖x - y‖ * ‖x‖)⁻¹ = ⟪y, y - x⟫ * (‖x - y‖ * ‖y‖)⁻¹
hxy : ¬x = y
⊢ ‖x‖ = ‖y‖

Tactic:
mul_inv_rev,

Goal state after:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
h : ⟪x, x - y⟫ * (‖x‖⁻¹ * ‖x - y‖⁻¹) = ⟪y, y - x⟫ * (‖x - y‖ * ‖y‖)⁻¹
hxy : ¬x = 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 ≠ π
h : ⟪x, x - y⟫ * (‖x‖⁻¹ * ‖x - y‖⁻¹) = ⟪y, y - x⟫ * (‖x - y‖ * ‖y‖)⁻¹
hxy : ¬x = y
⊢ ‖x‖ = ‖y‖

Tactic:
mul_inv_rev,

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

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

Tactic:
map_smul,

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) • 2 • («o».rotation ↑(π / 2)) (midpoint ℝ p₁ p₂ -ᵥ p₁) +
            (midpoint ℝ p₁ p₂ -ᵥ p₁))).cos =
    dist p₁ (((∡ p₂ p₁ s.center).tan / 2) • 2 • («o».rotation ↑(π / 2)) (midpoint ℝ p₁ p₂ -ᵥ p₁) +ᵥ midpoint ℝ 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
h : ¬Collinear ℝ {p₁, p₂, p₃}
sin_gt_zero : 0 < Real.sin (∠ p₁ p₂ p₃)
⊢ Real.sin (∠ p₁ p₂ p₃) * dist p₁ p₂ = dist p₃ p₁ * Real.sin (∠ p₂ p₃ p₁)

Tactic:
mul_comm (dist 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
h : ¬Collinear ℝ {p₁, p₂, p₃}
sin_gt_zero : 0 < Real.sin (∠ p₁ p₂ p₃)
⊢ Real.sin (∠ p₁ p₂ p₃) * dist p₁ p₂ = Real.sin (∠ p₂ p₃ p₁) * dist p₃ p₁
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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
i : Fin (n + 1)
⊢ ↑((s.restrict S hS).touchpoint signs i) = s.touchpoint signs i

Tactic:
← s.excenterExists_restrict S hS

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

Tactic:
have := Nonempty.map (AffineSubspace.inclusion hS) inferInstance

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))
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
h : (s.restrict S hS).ExcenterExists signs
i : Fin (n + 1)
this : Nonempty ↥S
⊢ ↑((s.restrict S hS).touchpoint signs i) = s.touchpoint signs i
Module: Mathlib.Geometry.Euclidean.Angle.Sphere

Goal state before:
pp: case e'_2.e'_6
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
t' : Triangle ℝ ↥S := Simplex.restrict t S ⋯
hf2 : Fact (finrank ℝ ↥S.direction = 2)
this : Oriented ℝ (↥S.direction) (Fin 2)
⊢ Real.sin (∠ (t.points i₁) (t.points i₂) (t.points i₃)) = |(∡ (t'.points i₁) (t'.points i₂) (t'.points i₃)).sin|

Tactic:
rw [← Real.Angle.sin_toReal,
      Real.abs_sin_eq_sin_abs_of_abs_le_pi (Real.Angle.abs_toReal_le_pi _),
      ← angle_eq_abs_oangle_toReal (t'.independent.injective.ne h₁₂)
        (t'.independent.injective.ne h₂₃.symm)]
    congr

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)
⊢ |(s.signedInfDist i) (s.excenter signs)| = s.exradius signs

Tactic:
h.signedInfDist_excenter,

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)
⊢ |(if i ∈ signs then -1 else 1) * ↑(SignType.sign (∑ j, s.excenterWeightsUnnorm signs j)) * s.exradius signs| =
    s.exradius signs
Module: Mathlib.Geometry.Euclidean.Angle.Sphere

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₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hc : Collinear ℝ {p₁, p₂, p₄}
he : ¬p₁ = p₄
⊢ Cospherical {p₁, p₂, p₃, p₄} ∨ Collinear ℝ {p₁, p₂, p₃, p₄}

Tactic:
have hc' : Collinear ℝ ({p₁, p₃, p₄} : Set P) := by
      rwa [← collinear_iff_of_two_zsmul_oangle_eq h]

Goal state after:
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₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hc : Collinear ℝ {p₁, p₂, p₄}
he : ¬p₁ = p₄
hc' : Collinear ℝ {p₁, p₃, p₄}
⊢ Cospherical {p₁, p₂, p₃, p₄} ∨ Collinear ℝ {p₁, p₂, 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
a b c : P
h : ¬Collinear ℝ {a, b, c}
hsin : Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c
hac : dist a c > 0
hsinabc : Real.sin (∠ a b c) ≥ 0
h1 : ∠ a c b < ∠ a b c
h2 : ∠ a b c ≤ π / 2
⊢ Real.sin (∠ a c b) < Real.sin (∠ a b c)

Tactic:
exact Real.sin_lt_sin_of_lt_of_le_pi_div_two (by linarith [angle_nonneg a c b]) h2 h1

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
a b c : P
h : ¬Collinear ℝ {a, b, c}
hsin : Real.sin (∠ a b c) * dist a b = Real.sin (∠ a c b) * dist a c
hac : dist a c > 0
hsinabc : Real.sin (∠ a b c) ≥ 0
h1 : ∠ a c b < ∠ a b c
h2 : π / 2 < ∠ a b c
w : dist a c ≤ dist a b
w1 : Real.sin (∠ a c b) < Real.sin (∠ a b c)
⊢ Real.sin (∠ a c b) * dist a c < Real.sin (∠ a b c) * dist a b

Tactic:
exact mul_lt_mul w1 w hac hsinabc

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

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

Tactic:
rw [NormedSpace.normalize, real_inner_smul_right, inner_sub_right, real_inner_smul_right,
    real_inner_self_eq_norm_sq, hx, real_inner_comm y, ← sq, mul_smul, ← smul_assoc]

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