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

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 : 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₂
hp' : p₂ -ᵥ p₁ ≠ 0
hp₂ : 1 = -2 * ⟪p₂ -ᵥ p₁, p₁ -ᵥ c₁⟫ / ⟪p₂ -ᵥ p₁, p₂ -ᵥ p₁⟫
hpc₁ : t₂ = 1
⊢ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₁ ∨ t₂ • (p₂ -ᵥ p₁) +ᵥ p₁ = p₂

Tactic:
simp [hpc₁]

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

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
p q : P
h : dist q s.center ^ 2 - dist p s.center ^ 2 = dist q p ^ 2
h0 : s.radius < 0
⊢ q ∉ s

Tactic:
intro hm

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
p q : P
h : dist q s.center ^ 2 - dist p s.center ^ 2 = dist q p ^ 2
h0 : s.radius < 0
hm : q ∈ s
⊢ False
Module: Mathlib.Geometry.Euclidean.Sphere.Basic

Goal state before:
pp: case inr.refine_2
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
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₁p₂ : p₁ ≠ p₂
h : s.center ∈ line[ℝ, p₁, p₂]
⊢ dist s.center s.center ≤ s.radius

Tactic:
· simpa using radius_nonneg_of_mem hp₁

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

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p : P
hpc : p ≠ s.center
hp : dist p s.center ≠ s.radius
hf : Module.finrank ℝ V = 1
p' : P
hr : 0 ≤ s.radius
this : FiniteDimensional ℝ V
ha : ℝ ∙ (p -ᵥ s.center) = ⊤
hpo : p' = p
⊢ ¬dist p s.center = s.radius

Tactic:
exact hp

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

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
h : dist s.center s.center < s.radius
hs : Nontrivial V
v : V
hv : ‖v‖ = s.radius
⊢ v +ᵥ s.center ∈ Metric.sphere s.center s.radius

Tactic:
by simp [hv]

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

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
s₁ s₂ : Sphere P
⊢ dist s₁.center s₂.center = s₁.radius + s₂.radius ∧ 0 ≤ s₁.radius ∧ 0 ≤ s₂.radius → s₁.IsExtTangent s₂

Tactic:
· rintro ⟨h, h₁, h₂⟩
    refine ⟨AffineMap.lineMap s₁.center s₂.center (s₁.radius / (s₁.radius + s₂.radius)), ?_⟩
    by_cases h0 : s₁.radius + s₂.radius = 0
    · simp only [h0, div_zero, AffineMap.lineMap_apply_zero, isExtTangentAt_center_iff, mem_sphere]
      exact ⟨by linarith, by linarith⟩
    · refine ⟨?_, ?_, ?_⟩
      · simp only [mem_sphere, dist_lineMap_left, norm_div, Real.norm_eq_abs, h, abs_of_nonneg h₁,
          abs_of_nonneg (add_nonneg h₁ h₂)]
        field
      · simp only [mem_sphere, dist_lineMap_right, Real.norm_eq_abs, h]
        rw [one_sub_div h0, add_sub_cancel_left, abs_div, abs_of_nonneg h₂,
          abs_of_nonneg (add_nonneg h₁ h₂)]
        field
      · simp only [wbtw_lineMap_iff]
        refine .inr ⟨?_, ?_⟩
        · positivity
        · rw [div_le_one (by positivity)]
          linarith

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₃ : P
hp₁ : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂ : ‖p₂ -ᵥ s.center‖ = s.radius
hp₃ : ‖p₃ -ᵥ s.center‖ = s.radius
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ ∡ p₁ s.center p₃ = 2 • ∡ p₁ p₂ p₃

Tactic:
oangle,

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₃ : P
hp₁ : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂ : ‖p₂ -ᵥ s.center‖ = s.radius
hp₃ : ‖p₃ -ᵥ s.center‖ = s.radius
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ «o».oangle (p₁ -ᵥ s.center) (p₃ -ᵥ s.center) = 2 • ∡ p₁ 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₃ : P
hp₁ : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂ : ‖p₂ -ᵥ s.center‖ = s.radius
hp₃ : ‖p₃ -ᵥ s.center‖ = s.radius
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ «o».oangle (p₁ -ᵥ s.center) (p₃ -ᵥ s.center) = 2 • ∡ p₁ p₂ p₃

Tactic:
oangle,

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₃ : P
hp₁ : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂ : ‖p₂ -ᵥ s.center‖ = s.radius
hp₃ : ‖p₃ -ᵥ s.center‖ = s.radius
hp₂p₁ : p₂ ≠ p₁
hp₂p₃ : p₂ ≠ p₃
⊢ «o».oangle (p₁ -ᵥ s.center) (p₃ -ᵥ s.center) = 2 • «o».oangle (p₁ -ᵥ p₂) (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₃ p₄ : P
hp₁ : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂ : ‖p₂ -ᵥ s.center‖ = s.radius
hp₃ : ‖p₃ -ᵥ s.center‖ = s.radius
hp₄ : ‖p₄ -ᵥ s.center‖ = s.radius
hp₂p₁ : p₂ ≠ p₁
hp₂p₄ : p₂ ≠ p₄
hp₃p₁ : p₃ ≠ p₁
hp₃p₄ : p₃ ≠ p₄
⊢ 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄

Tactic:
oangle,

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₃ p₄ : P
hp₁ : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂ : ‖p₂ -ᵥ s.center‖ = s.radius
hp₃ : ‖p₃ -ᵥ s.center‖ = s.radius
hp₄ : ‖p₄ -ᵥ s.center‖ = s.radius
hp₂p₁ : p₂ ≠ p₁
hp₂p₄ : p₂ ≠ p₄
hp₃p₁ : p₃ ≠ p₁
hp₃p₄ : p₃ ≠ p₄
⊢ 2 • «o».oangle (p₁ -ᵥ p₂) (p₄ -ᵥ p₂) = 2 • ∡ p₁ 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₃ p₄ : P
hp₁ : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂ : ‖p₂ -ᵥ s.center‖ = s.radius
hp₃ : ‖p₃ -ᵥ s.center‖ = s.radius
hp₄ : ‖p₄ -ᵥ s.center‖ = s.radius
hp₂p₁ : p₂ ≠ p₁
hp₂p₄ : p₂ ≠ p₄
hp₃p₁ : p₃ ≠ p₁
hp₃p₄ : p₃ ≠ p₄
⊢ 2 • «o».oangle (p₁ -ᵥ p₂) (p₄ -ᵥ p₂) = 2 • ∡ p₁ p₃ p₄

Tactic:
oangle,

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₃ p₄ : P
hp₁ : ‖p₁ -ᵥ s.center‖ = s.radius
hp₂ : ‖p₂ -ᵥ s.center‖ = s.radius
hp₃ : ‖p₃ -ᵥ s.center‖ = s.radius
hp₄ : ‖p₄ -ᵥ s.center‖ = s.radius
hp₂p₁ : p₂ ≠ p₁
hp₂p₄ : p₂ ≠ p₄
hp₃p₁ : p₃ ≠ p₁
hp₃p₄ : p₃ ≠ p₄
⊢ 2 • «o».oangle (p₁ -ᵥ p₂) (p₄ -ᵥ p₂) = 2 • «o».oangle (p₁ -ᵥ p₃) (p₄ -ᵥ p₃)
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - 2 * ‖x‖ * ‖y‖ * Real.cos (angle x y)

Tactic:
rw [show 2 * ‖x‖ * ‖y‖ * Real.cos (angle x y) = 2 * (Real.cos (angle x y) * (‖x‖ * ‖y‖)) by ring,
    cos_angle_mul_norm_mul_norm, ← real_inner_self_eq_norm_mul_norm, ←
    real_inner_self_eq_norm_mul_norm, ← real_inner_self_eq_norm_mul_norm, real_inner_sub_sub_self,
    sub_add_eq_add_sub]

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
m n : ℕ
inst✝¹ : NeZero m
inst✝ : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
signs : Finset (Fin (m + 1))
⊢ {
      center :=
        (Finset.affineCombination ℝ Finset.univ (s.points ∘ ⇑e.symm))
          (s.excenterWeights (Finset.map e.symm.toEmbedding signs) ∘ ⇑e.symm),
      radius :=
        |((Finset.map e.symm.toEmbedding Finset.univ).sum
              (s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs)))⁻¹| } =
    {
      center :=
        (Finset.affineCombination ℝ Finset.univ s.points) (s.excenterWeights (Finset.map e.symm.toEmbedding signs)),
      radius := |(∑ i, s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs) i)⁻¹| }

Tactic:
← Equiv.coe_toEmbedding,

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)
signs : Finset (Fin (m + 1))
⊢ {
      center :=
        (Finset.affineCombination ℝ Finset.univ (s.points ∘ ⇑e.symm.toEmbedding))
          (s.excenterWeights (Finset.map e.symm.toEmbedding signs) ∘ ⇑e.symm.toEmbedding),
      radius :=
        |((Finset.map e.symm.toEmbedding Finset.univ).sum
              (s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs)))⁻¹| } =
    {
      center :=
        (Finset.affineCombination ℝ Finset.univ s.points) (s.excenterWeights (Finset.map e.symm.toEmbedding signs)),
      radius := |(∑ i, s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs) i)⁻¹| }
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
⊢ ((∡ (midpoint ℝ p₁ p₂) p₁ (r • («o».rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂)).tan / 2) •
        («o».rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ
      midpoint ℝ p₁ p₂ =
    r • («o».rotation ↑(π / 2)) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂

Tactic:
oangle,

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

Tactic:
oangle,

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.Incenter

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
n : ℕ
inst✝ : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
fs : Finset (Fin (n + 1))
m : ℕ
hfs : #fs = m + 1
hne : m ≠ n
⊢ s.excenter signs ∉ affineSpan ℝ (Set.range (s.face hfs).points)

Tactic:
intro hm

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
fs : Finset (Fin (n + 1))
m : ℕ
hfs : #fs = m + 1
hne : m ≠ n
hm : s.excenter signs ∈ affineSpan ℝ (Set.range (s.face hfs).points)
⊢ False
Module: Mathlib.Geometry.Euclidean.Triangle

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

Tactic:
← angle_nonneg,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h✝ : ↑(angle x y) = ↑(angle x (x + y) + angle y (x + y))
n : ℤ
h : n ≤ -1
⊢ π + -(2 * π) < 0 + angle y (x + y)
Module: Mathlib.Geometry.Euclidean.Triangle

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h : ↑(angle x y) = ↑(angle x (x + y) + angle y (x + y))
n : ℤ
this : -1 < n
hn : 1 ≤ n
hxy : x + y ≠ 0
r₁ : ℝ
r₁_pos : r₁ < 0
hr₁ : x = r₁ • (x + y)
r₂ : ℝ
r₂_pos : r₂ < 0
hr₂ : y = r₂ • (x + y)
⊢ False

Tactic:
have : (r₁ + r₂ - 1) • (x + y) = 0 := by
      rw [sub_smul, add_smul, one_smul, ← hr₁, ← hr₂, sub_eq_zero]

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hy : y ≠ 0
hx : x ≠ 0
h : ↑(angle x y) = ↑(angle x (x + y) + angle y (x + y))
n : ℤ
this✝ : -1 < n
hn : 1 ≤ n
hxy : x + y ≠ 0
r₁ : ℝ
r₁_pos : r₁ < 0
hr₁ : x = r₁ • (x + y)
r₂ : ℝ
r₂_pos : r₂ < 0
hr₂ : y = r₂ • (x + y)
this : (r₁ + r₂ - 1) • (x + y) = 0
⊢ False
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 : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = InnerProductGeometry.angle (p₁ -ᵥ p₃) (p₂ -ᵥ p₃)
hpi : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₁ -ᵥ p₃) ≠ π
⊢ ‖p₁ -ᵥ p₂‖ = ‖p₁ -ᵥ p₃‖

Tactic:
rw [← vsub_sub_vsub_cancel_left p₃ p₂ p₁, ← vsub_sub_vsub_cancel_left p₂ p₃ p₁] at 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
p₁ p₂ p₃ : P
h :
  InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₁ -ᵥ p₂ - (p₁ -ᵥ p₃)) =
    InnerProductGeometry.angle (p₁ -ᵥ p₃) (p₁ -ᵥ p₃ - (p₁ -ᵥ p₂))
hpi : InnerProductGeometry.angle (p₁ -ᵥ p₂) (p₁ -ᵥ p₃) ≠ π
⊢ ‖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 : P
hb : a ≠ b
hc : a ≠ c
hp : Wbtw ℝ b p c
⊢ ∠ b a p + ∠ p a c = ∠ b a c

Tactic:
by
  by_cases pb : p = b; · simpa [pb] using angle_self_of_ne hb.symm
  by_cases pc : p = c; · simpa [pc] using angle_self_of_ne hc.symm
  have ea := angle_add_angle_add_angle_eq_pi c hb
  have eb := angle_add_angle_add_angle_eq_pi p hb
  have ec := angle_add_angle_add_angle_eq_pi p hc.symm
  replace hp : ∠ b p c = π := angle_eq_pi_iff_sbtw.mpr ⟨hp, pb, pc⟩
  have hp' : ∠ c p b = π := by rwa [angle_comm] at hp
  rw [angle_comm p b a, angle_eq_angle_of_angle_eq_pi a hp, angle_comm a b c] at eb
  rw [angle_eq_angle_of_angle_eq_pi a hp', angle_comm c p a] at ec
  have ep := angle_add_angle_eq_pi_of_angle_eq_pi a hp
  linarith only [ea, eb, ec, ep]

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

Goal state before:
pp: n : ℕ
fs : Finset (Fin (n + 1))
h : fs.Nonempty
⊢ ∑ i, centroidWeightsWithCircumcenter fs i = 1

Tactic:
simp_rw [sum_pointsWithCircumcenter, centroidWeightsWithCircumcenter, add_zero, ←
    fs.sum_centroidWeights_eq_one_of_nonempty ℝ h, ← sum_indicator_subset _ fs.subset_univ]
  rcongr

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 : ℕ
s : Simplex ℝ P n
i₁ i₂ : Fin (n + 1)
h : i₁ ≠ i₂
hc : #{i₁, i₂} = 2
W : AffineSubspace ℝ P := ⋯
⊢ W = affineSpan ℝ (Set.range (s.face hc).points)

Tactic:
simp [W]

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

Goal state before:
pp: V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
H : ⟪x, NormedSpace.normalize (ortho y x)⟫ ^ 2 = Real.sin (angle x y) ^ 2
⊢ ⟪x, NormedSpace.normalize (ortho y x)⟫ = Real.sin (angle x y)

Tactic:
sq_eq_sq_iff_abs_eq_abs,

Goal state after:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hx : ‖x‖ = 1
hy : ‖y‖ = 1
H : |⟪x, NormedSpace.normalize (ortho y x)⟫| = |Real.sin (angle x y)|
⊢ ⟪x, NormedSpace.normalize (ortho y x)⟫ = Real.sin (angle x y)
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
inst✝ : NeZero 1
s : Simplex ℝ P 1
signs : Finset (Fin (1 + 1))
h : s.ExcenterExists signs
i j : Fin (1 + 1)
hij : s.points i.rev = s.points j.rev
hne : ¬i = j
⊢ s.points i = s.points j

Tactic:
convert! hij.symm

Goal state after:
case e'_2
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : NeZero 1
s : Simplex ℝ P 1
signs : Finset (Fin (1 + 1))
h : s.ExcenterExists signs
i j : Fin (1 + 1)
hij : s.points i.rev = s.points j.rev
hne : ¬i = j
⊢ i = j.rev

case e'_3
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : NeZero 1
s : Simplex ℝ P 1
signs : Finset (Fin (1 + 1))
h : s.ExcenterExists signs
i j : Fin (1 + 1)
hij : s.points i.rev = s.points j.rev
hne : ¬i = j
⊢ j = i.rev
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)
signs : Finset (Fin (m + 1))
i : Fin (m + 1)
⊢ (Finset.affineCombination ℝ Finset.univ (s.points ∘ ⇑e.symm))
      (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) (e.symm i) ∘ ⇑e.symm) =
    (Finset.affineCombination ℝ Finset.univ s.points)
      (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) (e.symm i))

Tactic:
← Equiv.coe_toEmbedding,

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)
signs : Finset (Fin (m + 1))
i : Fin (m + 1)
⊢ (Finset.affineCombination ℝ Finset.univ (s.points ∘ ⇑e.symm.toEmbedding))
      (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) (e.symm.toEmbedding i) ∘ ⇑e.symm.toEmbedding) =
    (Finset.affineCombination ℝ Finset.univ s.points)
      (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) (e.symm.toEmbedding i))
Module: Mathlib.Geometry.Euclidean.Congruence

Goal state before:
pp: V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst✝⁷ : NormedAddCommGroup V₁
inst✝⁶ : NormedAddCommGroup V₂
inst✝⁵ : InnerProductSpace ℝ V₁
inst✝⁴ : InnerProductSpace ℝ V₂
inst✝³ : MetricSpace P₁
inst✝² : MetricSpace P₂
inst✝¹ : NormedAddTorsor V₁ P₁
inst✝ : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
h : ¬Collinear ℝ {a, b, c}
ha₁ : ∠ a b c = ∠ a' b' c'
hd : dist b c = dist b' c'
ha₂ : ∠ b c a = ∠ b' c' a'
h' : ¬Collinear ℝ {a', b', c'}
ha₃' : ∠ c' a' b' + ∠ a' b' c' + ∠ b' c' a' = Real.pi
ha₃ : ∠ c a b = ∠ c' a' b'
h_bac : ¬Collinear ℝ {b, a, c}
h_bac' : ¬Collinear ℝ {b', a', c'}
⊢ dist a b = dist a' b'

Tactic:
rw [dist_comm a b, dist_comm a' b', dist_eq_dist_mul_sin_angle_div_sin_angle h_bac,
      dist_eq_dist_mul_sin_angle_div_sin_angle h_bac', dist_comm c b, dist_comm c' b', hd,
      angle_comm, ha₂, angle_comm b' c' a', angle_comm b a c, ha₃, angle_comm b' a' c']

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

Goal state before:
pp: case left
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.ninePointCircle.center ∈ affineSpan ℝ (Set.range s.medial.points)

pp: case right
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
⊢ Set.range s.medial.points ⊆ Metric.sphere s.ninePointCircle.center s.ninePointCircle.radius

Tactic:
· simpa using s.ninePointCircle_center_mem_affineSpan

Goal state after:
case right
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
⊢ Set.range s.medial.points ⊆ Metric.sphere s.ninePointCircle.center s.ninePointCircle.radius
Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
P₃ : Type u_5
v₁ : ι → P₁
v₂ : ι → P₂
v₃ : ι → P₃
inst✝² : PseudoEMetricSpace P₁
inst✝¹ : PseudoEMetricSpace P₂
inst✝ : PseudoEMetricSpace P₃
r₁ : ℝ≥0
hr₁ : r₁ ≠ 0
h₁ : ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = ↑r₁ * edist (v₂ i₁) (v₂ i₂)
r₂ : ℝ≥0
hr₂ : r₂ ≠ 0
h₂ : ∀ (i₁ i₂ : ι), edist (v₂ i₁) (v₂ i₂) = ↑r₂ * edist (v₃ i₁) (v₃ i₂)
x✝¹ x✝ : ι
⊢ edist (v₁ x✝¹) (v₁ x✝) = ↑(r₁ * r₂) * edist (v₃ x✝¹) (v₃ x✝)

Tactic:
ENNReal.coe_mul,

Goal state after:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
P₃ : Type u_5
v₁ : ι → P₁
v₂ : ι → P₂
v₃ : ι → P₃
inst✝² : PseudoEMetricSpace P₁
inst✝¹ : PseudoEMetricSpace P₂
inst✝ : PseudoEMetricSpace P₃
r₁ : ℝ≥0
hr₁ : r₁ ≠ 0
h₁ : ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = ↑r₁ * edist (v₂ i₁) (v₂ i₂)
r₂ : ℝ≥0
hr₂ : r₂ ≠ 0
h₂ : ∀ (i₁ i₂ : ι), edist (v₂ i₁) (v₂ i₂) = ↑r₂ * edist (v₃ i₁) (v₃ i₂)
x✝¹ x✝ : ι
⊢ edist (v₁ x✝¹) (v₁ x✝) = ↑r₁ * ↑r₂ * edist (v₃ x✝¹) (v₃ x✝)