mathlib-initiative/mathlib-tactics huggingface dataset:
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
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
n : ℕ
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
⊢ sx₁.circumradius = sx₂.circumradius

Tactic:
by
  rcases exists_circumradius_eq_of_cospherical_subset h hd hc with ⟨r, hr⟩
  rw [hr sx₁ hsx₁, hr sx₂ hsx₂]

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, c, b}
⊢ ∠ a c b ≤ ∠ a b c ↔ dist a b ≤ dist a c

Tactic:
simpa using

Goal state after:
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, c, b}
⊢ ∠ a c b ≤ ∠ a b c ↔ dist a b ≤ dist a c
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : x = 0
⊢ angle x z ≤ angle x y + angle y z

Tactic:
simpa using

Goal state after:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : x = 0
⊢ 0 ≤ angle y z
Module: Mathlib.Topology.MetricSpace.Congruence

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
P₁ : Type u_3
P₂ : Type u_4
inst✝² : PseudoEMetricSpace P₁
inst✝¹ : PseudoEMetricSpace P₂
E : Type u_7
inst✝ : EquivLike E ι' ι
f : E
v₁ : ι → P₁
v₂ : ι → P₂
h : v₁ ∘ ⇑f ≅ v₂ ∘ ⇑f
i₁ i₂ : ι
⊢ edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)

Tactic:
simpa using

Goal state after:
ι : Type u_1
ι' : Type u_2
P₁ : Type u_3
P₂ : Type u_4
inst✝² : PseudoEMetricSpace P₁
inst✝¹ : PseudoEMetricSpace P₂
E : Type u_7
inst✝ : EquivLike E ι' ι
f : E
v₁ : ι → P₁
v₂ : ι → P₂
h : v₁ ∘ ⇑f ≅ v₂ ∘ ⇑f
i₁ i₂ : ι
⊢ edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ¬x = 0
hy : y = 0
⊢ angle x z ≤ angle x y + angle y z

Tactic:
simpa using

Goal state after:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ¬x = 0
hy : y = 0
⊢ angle x z ≤ π
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ¬x = 0
hy : ¬y = 0
hz : z = 0
⊢ angle x z ≤ angle x y + angle y z

Tactic:
simpa using

Goal state after:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ¬x = 0
hy : ¬y = 0
hz : z = 0
⊢ 0 ≤ angle x y
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 j : Fin (n + 1)
hne : i ≠ j
⊢ 0 < s.touchpointWeights ∅ i j

Tactic:
simpa using

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 j : Fin (n + 1)
hne : i ≠ j
⊢ 0 < s.touchpointWeights ∅ i j
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 z : V
hx : ¬x = 0
hy : ¬y = 0
hz : ¬z = 0
⊢ angle x z ≤ angle x y + angle y z

Tactic:
simpa using

Goal state after:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hx : ¬x = 0
hy : ¬y = 0
hz : ¬z = 0
⊢ angle x z ≤ angle x y + angle y z
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
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
hne : i ≠ j
⊢ 0 < s.touchpointWeights {i} i j

Tactic:
simpa using

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
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
hne : i ≠ j
⊢ 0 < s.touchpointWeights {i} i j
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x z : V
kx kz : ℝ≥0
hy : kx • x + kz • z ≠ 0
hkx : 0 < kx
hkz : 0 < kz
hz : z ≠ 0
⊢ angle x z = angle x (kx • x + kz • z) + angle z (kx • x + kz • z)

Tactic:
simpa using

Goal state after:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x z : V
kx kz : ℝ≥0
hy : kx • x + kz • z ≠ 0
hkx : 0 < kx
hkz : 0 < kz
hz : z ≠ 0
⊢ angle x z = angle x (↑kx • x + ↑kz • z) + angle z (↑kx • x + ↑kz • z)
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x z : V
kx kz : ℝ≥0
hy : kx • x + kz • z ≠ 0
hkx : 0 < kx
hkz : 0 < kz
hz : z = 0
hx : x ≠ 0
⊢ angle z x = angle z (kz • z + kx • x) + angle x (kz • z + kx • x)

Tactic:
simpa using

Goal state after:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x z : V
kx kz : ℝ≥0
hy : kx • x + kz • z ≠ 0
hkx : 0 < kx
hkz : 0 < kz
hz : z = 0
hx : x ≠ 0
⊢ angle z x = angle z (↑kz • z + ↑kx • x) + angle x (↑kz • z + ↑kx • x)
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
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
hne : i ≠ j
⊢ s.touchpointWeights {i} j i < 0

Tactic:
simpa using

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
inst✝ : n.AtLeastTwo
i j : Fin (n + 1)
hne : i ≠ j
⊢ s.touchpointWeights {i} j i < 0
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'
⊢ ¬Collinear ℝ {b, a, c}

Tactic:
simpa using

Goal state after:
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'
⊢ ¬Collinear ℝ {a, b, c}
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}
⊢ ¬Collinear ℝ {b', a', c'}

Tactic:
simpa using

Goal state after:
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}
⊢ ¬Collinear ℝ {a', b', c'}
Module: Mathlib.Geometry.Euclidean.Congruence

Goal state before:
pp: ι : Type u_1
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₂
v₁ : ι → P₁
v₂ : ι → P₂
h : v₁ ≅ v₂
i j k : ι
⊢ Real.arccos (inner ℝ (v₁ i -ᵥ v₁ j) (v₁ k -ᵥ v₁ j) / (‖v₁ i -ᵥ v₁ j‖ * ‖v₁ k -ᵥ v₁ j‖)) =
    Real.arccos (inner ℝ (v₂ i -ᵥ v₂ j) (v₂ k -ᵥ v₂ j) / (‖v₂ i -ᵥ v₂ j‖ * ‖v₂ k -ᵥ v₂ j‖))

Tactic:
simp_rw [real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two,
    vsub_sub_vsub_cancel_right, ← dist_eq_norm_vsub, h.dist_eq]

Goal state after:
Module: Mathlib.Geometry.Euclidean.Inversion.Calculus

Goal state before:
pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
c : F
R : ℝ
x : F
hx : (fun x ↦ c + x) x ≠ c
A : HasFDerivAt (fun x ↦ _root_.id x - c) (ContinuousLinearMap.id ℝ F) (c + x)
⊢ ‖_root_.id (c + x) - c‖ ^ 2 ≠ 0

Tactic:
simpa using

Goal state after:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
c : F
R : ℝ
x : F
hx : (fun x ↦ c + x) x ≠ c
A : HasFDerivAt (fun x ↦ _root_.id x - c) (ContinuousLinearMap.id ℝ F) (c + x)
⊢ ¬x = 0
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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Sbtw ℝ (t.points i₁) (Simplex.touchpoint t ∅ i₂) (t.points i₃)

Tactic:
← t.mem_interior_face_iff_sbtw 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Simplex.touchpoint t ∅ i₂ ∈ (Simplex.face t ⋯).interior
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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Sbtw ℝ (t.points i₁) (Simplex.touchpoint t {i₂} i₂) (t.points i₃)

Tactic:
← t.mem_interior_face_iff_sbtw 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Simplex.touchpoint t {i₂} i₂ ∈ (Simplex.face t ⋯).interior
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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hw : Simplex.touchpointWeights t {i₁} i₂ i₁ + Simplex.touchpointWeights t {i₁} i₂ i₃ = 1
i : Fin (2 + 1)
⊢ Simplex.touchpointWeights t {i₁} i₂ i =
    Finset.affineCombinationLineMapWeights i₁ i₃ (Simplex.touchpointWeights t {i₁} i₂ i₃) i

Tactic:
have h : i = i₁ ∨ i = i₂ ∨ i = i₃ := by clear hw; decide +revert

Goal state after:
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₃
hw : Simplex.touchpointWeights t {i₁} i₂ i₁ + Simplex.touchpointWeights t {i₁} i₂ i₃ = 1
i : Fin (2 + 1)
h : i = i₁ ∨ i = i₂ ∨ i = i₃
⊢ Simplex.touchpointWeights t {i₁} i₂ i =
    Finset.affineCombinationLineMapWeights i₁ i₃ (Simplex.touchpointWeights t {i₁} i₂ i₃) i
Module: Mathlib.Geometry.Euclidean.NinePointCircle

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 : ℕ
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
⊢ n = m

Tactic:
simpa using

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 : ℕ
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
⊢ n = m
Module: Mathlib.Geometry.Euclidean.NinePointCircle

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)
⊢ ↑n ≠ 0

Tactic:
simpa using

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)
⊢ ¬n = 0
Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoEMetricSpace P₁
inst✝ : PseudoEMetricSpace P₂
v₁ : ι → P₁
v₂ : ι → P₂
h : v₁ ≅ v₂
i₁ i₂ : ι
⊢ edist (v₁ i₁) (v₁ i₂) = ↑1 * edist (v₂ i₁) (v₂ i₂)

Tactic:
simpa using

Goal state after:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoEMetricSpace P₁
inst✝ : PseudoEMetricSpace P₂
v₁ : ι → P₁
v₂ : ι → P₂
h : v₁ ≅ v₂
i₁ i₂ : ι
⊢ edist (v₁ i₁) (v₁ i₂) = edist (v₂ i₁) (v₂ i₂)
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)

Tactic:
simpa using

Goal state after:
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.points)
Module: Mathlib.Geometry.Euclidean.NinePointCircle

Goal state before:
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
⊢ ∀ (y : Fin (n + 1)), s.medial.points y ∈ Metric.sphere s.ninePointCircle.center s.ninePointCircle.radius

Tactic:
simpa using

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
⊢ ∀ (y : Fin (n + 1)), s.faceOppositeCentroid y ∈ s.ninePointCircle
Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoEMetricSpace P₁
inst✝ : PseudoEMetricSpace P₂
f : ι' ≃ ι
v₁ : ι → P₁
v₂ : ι → P₂
r : ℝ≥0
hr : r ≠ 0
h : ∀ (i₁ i₂ : ι'), edist ((v₁ ∘ ⇑f) i₁) ((v₁ ∘ ⇑f) i₂) = ↑r * edist ((v₂ ∘ ⇑f) i₁) ((v₂ ∘ ⇑f) i₂)
i₁ i₂ : ι
⊢ edist (v₁ i₁) (v₁ i₂) = ↑r * edist (v₂ i₁) (v₂ i₂)

Tactic:
simpa using

Goal state after:
ι : Type u_1
ι' : Type u_2
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoEMetricSpace P₁
inst✝ : PseudoEMetricSpace P₂
f : ι' ≃ ι
v₁ : ι → P₁
v₂ : ι → P₂
r : ℝ≥0
hr : r ≠ 0
h : ∀ (i₁ i₂ : ι'), edist ((v₁ ∘ ⇑f) i₁) ((v₁ ∘ ⇑f) i₂) = ↑r * edist ((v₂ ∘ ⇑f) i₁) ((v₂ ∘ ⇑f) i₂)
i₁ i₂ : ι
⊢ edist (v₁ i₁) (v₁ i₂) = ↑r * edist (v₂ i₁) (v₂ i₂)
Module: Mathlib.Geometry.Euclidean.NinePointCircle

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 : Fin (n + 1)
hn : ¬n = 0
⊢ ↑n ≠ 0

Tactic:
simpa using

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
i : Fin (n + 1)
hn : ¬n = 0
⊢ ¬n = 0
Module: Mathlib.Geometry.Euclidean.MongePoint

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 : ℕ
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
⊢ n = m

Tactic:
simpa using

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 : ℕ
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
⊢ n = m
Module: Mathlib.Geometry.Euclidean.NinePointCircle

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 : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
hltn : 1 < n
hnsub1 : ↑(n - 1) = ↑n - 1
⊢ ↑n - 1 ≠ 0

Tactic:
simpa using

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 : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
hltn : 1 < n
hnsub1 : ↑(n - 1) = ↑n - 1
⊢ ¬n = 1
Module: Mathlib.Geometry.Euclidean.NinePointCircle

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 : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
hltn : 1 < n
hnsub1 : ↑(n - 1) = ↑n - 1
⊢ ↑n ≠ 0

Tactic:
simpa using

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 : ℕ
hn : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
hn1 : ¬n = 1
hltn : 1 < n
hnsub1 : ↑(n - 1) = ↑n - 1
⊢ ¬n = 0
Module: Mathlib.Geometry.Euclidean.MongePoint

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 : ℕ
s : Simplex ℝ P (n + 2)
e : Fin (n + 3) ≃ Fin (m + 3)
i₁ i₂ : Fin (m + 3)
⊢ n = m

Tactic:
simpa using

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 : ℕ
s : Simplex ℝ P (n + 2)
e : Fin (n + 3) ≃ Fin (m + 3)
i₁ i₂ : Fin (m + 3)
⊢ n = m
Module: Mathlib.Geometry.Euclidean.Sphere.Power

Goal state before:
pp: V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : ∠ p₁ p p₂ = π
hp₃p₄ : ∠ p₃ p p₄ = π
hn : ¬Collinear ℝ {p₁, p, p₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄
hindep : AffineIndependent ℝ ![p₁, p, p₃]
t : Affine.Triangle ℝ P := { points := ![p₁, p, p₃], independent := hindep }
ht : t = { points := ![p₁, p, p₃], independent := hindep }
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
hp₂ : p₂ ∈ S
hp₄ : p₄ ∈ S
s_isom : ↥S →ᵃⁱ[ℝ] P := S.subtypeₐᵢ
p₁' : ↥S := ⟨p₁, ⋯⟩
p' : ↥S := ⟨p, ⋯⟩
p₃' : ↥S := ⟨p₃, ⋯⟩
p₂' : ↥S := ⟨p₂, hp₂⟩
p₄' : ↥S := ⟨p₄, hp₄⟩
⊢ dist p₁' p' * dist p₂' p' = dist p₃' p' * dist p₄' p'

Tactic:
simpa using

Goal state after:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : ∠ p₁ p p₂ = π
hp₃p₄ : ∠ p₃ p p₄ = π
hn : ¬Collinear ℝ {p₁, p, p₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄
hindep : AffineIndependent ℝ ![p₁, p, p₃]
t : Affine.Triangle ℝ P := { points := ![p₁, p, p₃], independent := hindep }
ht : t = { points := ![p₁, p, p₃], independent := hindep }
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
hp₂ : p₂ ∈ S
hp₄ : p₄ ∈ S
s_isom : ↥S →ᵃⁱ[ℝ] P := S.subtypeₐᵢ
p₁' : ↥S := ⟨p₁, ⋯⟩
p' : ↥S := ⟨p, ⋯⟩
p₃' : ↥S := ⟨p₃, ⋯⟩
p₂' : ↥S := ⟨p₂, hp₂⟩
p₄' : ↥S := ⟨p₄, hp₄⟩
⊢ ‖↑p₁' -ᵥ ↑p'‖ * ‖↑p₂' -ᵥ ↑p'‖ = ‖↑p₃' -ᵥ ↑p'‖ * ‖↑p₄' -ᵥ ↑p'‖
Module: Mathlib.Geometry.Euclidean.Sphere.Power

Goal state before:
pp: V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : ∠ p₁ p p₂ = π
hp₃p₄ : ∠ p₃ p p₄ = π
hn : ¬Collinear ℝ {p₁, p, p₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄
hindep : AffineIndependent ℝ ![p₁, p, p₃]
t : Affine.Triangle ℝ P := { points := ![p₁, p, p₃], independent := hindep }
ht : t = { points := ![p₁, p, p₃], independent := hindep }
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
hp₂ : p₂ ∈ S
hp₄ : p₄ ∈ S
s_isom : ↥S →ᵃⁱ[ℝ] P := S.subtypeₐᵢ
p₁' : ↥S := ⟨p₁, ⋯⟩
p' : ↥S := ⟨p, ⋯⟩
p₃' : ↥S := ⟨p₃, ⋯⟩
p₂' : ↥S := ⟨p₂, hp₂⟩
p₄' : ↥S := ⟨p₄, hp₄⟩
h_dist' : dist p₁' p' * dist p₂' p' = dist p₃' p' * dist p₄' p'
hp₁'p₂' : ∠ p₁' p' p₂' = π
hp₃'p₄' : ∠ p₃' p' p₄' = π
h_cospherical' : Cospherical {p₁', p₂', p₃', p₄'}
⊢ Cospherical {p₁, p₂, p₃, p₄}

Tactic:
simpa using

Goal state after:
V : Type u_1
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
P : Type u_2
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ p₄ p : P
h : dist p₁ p * dist p₂ p = dist p₃ p * dist p₄ p
hp₁p₂ : ∠ p₁ p p₂ = π
hp₃p₄ : ∠ p₃ p p₄ = π
hn : ¬Collinear ℝ {p₁, p, p₃}
hp₁p₂_sbtw : Sbtw ℝ p₁ p p₂
hp₃p₄_sbtw : Sbtw ℝ p₃ p p₄
hindep : AffineIndependent ℝ ![p₁, p, p₃]
t : Affine.Triangle ℝ P := { points := ![p₁, p, p₃], independent := hindep }
ht : t = { points := ![p₁, p, p₃], independent := hindep }
S : AffineSubspace ℝ P := affineSpan ℝ (Set.range t.points)
hS : S = affineSpan ℝ (Set.range t.points)
hp₂ : p₂ ∈ S
hp₄ : p₄ ∈ S
s_isom : ↥S →ᵃⁱ[ℝ] P := S.subtypeₐᵢ
p₁' : ↥S := ⟨p₁, ⋯⟩
p' : ↥S := ⟨p, ⋯⟩
p₃' : ↥S := ⟨p₃, ⋯⟩
p₂' : ↥S := ⟨p₂, hp₂⟩
p₄' : ↥S := ⟨p₄, hp₄⟩
h_dist' : dist p₁' p' * dist p₂' p' = dist p₃' p' * dist p₄' p'
hp₁'p₂' : ∠ p₁' p' p₂' = π
hp₃'p₄' : ∠ p₃' p' p₄' = π
h_cospherical' : Cospherical {p₁', p₂', p₃', p₄'}
⊢ Cospherical {p₁, p₂, p₃, p₄}
Module: Mathlib.Geometry.Group.Growth.QuotientInter

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
H : Subgroup G
inst✝¹ : DecidablePred fun x ↦ x ∈ H
inst✝ : H.Normal
A : Finset G
m n : ℕ
π : G →* G ⧸ H := QuotientGroup.mk' H
φ : G ⧸ H → G := invFunOn (⇑π) (↑A ^ m)
hφ : Set.InjOn φ (⇑π '' ↑A ^ m)
a : G ⧸ H
ha : a ∈ ⇑π '' ↑A ^ m
⊢ ∃ a ∈ ?m.112, ?m.113 a = ?m.114

Tactic:
simpa using

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
H : Subgroup G
inst✝¹ : DecidablePred fun x ↦ x ∈ H
inst✝ : H.Normal
A : Finset G
m n : ℕ
π : G →* G ⧸ H := QuotientGroup.mk' H
φ : G ⧸ H → G := invFunOn (⇑π) (↑A ^ m)
hφ : Set.InjOn φ (⇑π '' ↑A ^ m)
a : G ⧸ H
ha : a ∈ ⇑π '' ↑A ^ m
⊢ ∃ a ∈ ?m.112, ?m.113 a = ?m.114