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

Goal state before:
pp: case «0»
P₁ : Type u_4
P₂ : Type u_5
inst✝¹ : MetricSpace P₁
inst✝ : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
j : Fin 3
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a, b, c] j) = dist (![a', b', c'] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a', b', c'] j)

Tactic:
fin_cases j

Goal state after:
case «0».«0»
P₁ : Type u_4
P₂ : Type u_5
inst✝¹ : MetricSpace P₁
inst✝ : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨0, ⋯⟩)) =
    dist (![a', b', c'] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨0, ⋯⟩))

case «0».«1»
P₁ : Type u_4
P₂ : Type u_5
inst✝¹ : MetricSpace P₁
inst✝ : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨1, ⋯⟩)) =
    dist (![a', b', c'] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨1, ⋯⟩))

case «0».«2»
P₁ : Type u_4
P₂ : Type u_5
inst✝¹ : MetricSpace P₁
inst✝ : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨2, ⋯⟩)) =
    dist (![a', b', c'] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨2, ⋯⟩))
Module: Mathlib.Geometry.Euclidean.Congruence

Goal state before:
pp: case «1»
P₁ : Type u_4
P₂ : Type u_5
inst✝¹ : MetricSpace P₁
inst✝ : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
j : Fin 3
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a, b, c] j) = dist (![a', b', c'] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a', b', c'] j)

Tactic:
fin_cases j

Goal state after:
case «1».«0»
P₁ : Type u_4
P₂ : Type u_5
inst✝¹ : MetricSpace P₁
inst✝ : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨0, ⋯⟩)) =
    dist (![a', b', c'] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨0, ⋯⟩))

case «1».«1»
P₁ : Type u_4
P₂ : Type u_5
inst✝¹ : MetricSpace P₁
inst✝ : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨1, ⋯⟩)) =
    dist (![a', b', c'] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨1, ⋯⟩))

case «1».«2»
P₁ : Type u_4
P₂ : Type u_5
inst✝¹ : MetricSpace P₁
inst✝ : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨2, ⋯⟩)) =
    dist (![a', b', c'] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨2, ⋯⟩))
Module: Mathlib.Geometry.Euclidean.Congruence

Goal state before:
pp: case «2»
P₁ : Type u_4
P₂ : Type u_5
inst✝¹ : MetricSpace P₁
inst✝ : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
j : Fin 3
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a, b, c] j) = dist (![a', b', c'] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a', b', c'] j)

Tactic:
fin_cases j

Goal state after:
case «2».«0»
P₁ : Type u_4
P₂ : Type u_5
inst✝¹ : MetricSpace P₁
inst✝ : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨0, ⋯⟩)) =
    dist (![a', b', c'] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨0, ⋯⟩))

case «2».«1»
P₁ : Type u_4
P₂ : Type u_5
inst✝¹ : MetricSpace P₁
inst✝ : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨1, ⋯⟩)) =
    dist (![a', b', c'] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨1, ⋯⟩))

case «2».«2»
P₁ : Type u_4
P₂ : Type u_5
inst✝¹ : MetricSpace P₁
inst✝ : MetricSpace P₂
a b c : P₁
a' b' c' : P₂
hd₁ : dist a b = dist a' b'
hd₂ : dist b c = dist b' c'
hd₃ : dist c a = dist c' a'
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨2, ⋯⟩)) =
    dist (![a', b', c'] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨2, ⋯⟩))
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 : Fin (n + 1)
⊢ s.touchpoint {i} i ∈ (s.faceOpposite i).interior

Tactic:
by
  rw [faceOpposite, ← affineCombination_touchpointWeights,
    s.affineCombination_mem_interior_face_iff_pos _ (s.sum_touchpointWeights _ _)]
  simp only [Finset.mem_compl, Finset.mem_singleton, Decidable.not_not, forall_eq,
    touchpointWeights_eq_zero, and_true]
  intro j hj
  exact s.touchpointWeights_singleton_pos (Ne.symm hj)

Goal state after:
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
hy : y ≠ 0
h : angle x z = angle x y + angle y z
hxz₁ : ¬angle x z = π
hxz₂ : angle x z = 0
⊢ y ∈ Submodule.span ℝ≥0 {x, z}

pp: case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hy : y ≠ 0
h : angle x z = angle x y + angle y z
hxz₁ : ¬angle x z = π
hxz₂ : ¬angle x z = 0
⊢ y ∈ Submodule.span ℝ≥0 {x, z}

Tactic:
· have hxy : angle x y = 0 := by grind [angle_nonneg]
      rw [angle_eq_zero_iff] at hxy hxz₂
      obtain ⟨_, ⟨r2, ⟨hr2, rfl⟩⟩⟩ := hxy
      lift r2 to ℝ≥0 using hr2.le
      exact Submodule.smul_mem _ _ (Submodule.mem_span_of_mem (by simp))

Goal state after:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hy : y ≠ 0
h : angle x z = angle x y + angle y z
hxz₁ : ¬angle x z = π
hxz₂ : ¬angle x z = 0
⊢ y ∈ Submodule.span ℝ≥0 {x, 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
signs : Finset (Fin (n + 1))
h : ∑ i, s.excenterWeightsUnnorm signs i ≠ 0
i j : Fin (n + 1)
he : Pi.single j 1 = s.touchpointWeights signs i
this : 1 < n
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
he' : (if k ∈ signs then -1 else 1) * (s.height k)⁻¹ = 0
⊢ False

Tactic:
by_cases hk : k ∈ signs

Goal state after:
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
inst✝ : n.AtLeastTwo
signs : Finset (Fin (n + 1))
h : ∑ i, s.excenterWeightsUnnorm signs i ≠ 0
i j : Fin (n + 1)
he : Pi.single j 1 = s.touchpointWeights signs i
this : 1 < n
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
he' : (if k ∈ signs then -1 else 1) * (s.height k)⁻¹ = 0
hk : k ∈ signs
⊢ False

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
inst✝ : n.AtLeastTwo
signs : Finset (Fin (n + 1))
h : ∑ i, s.excenterWeightsUnnorm signs i ≠ 0
i j : Fin (n + 1)
he : Pi.single j 1 = s.touchpointWeights signs i
this : 1 < n
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
he' : (if k ∈ signs then -1 else 1) * (s.height k)⁻¹ = 0
hk : k ∉ signs
⊢ False
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:
[

Goal state after:
ι : 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‖))
Module: Mathlib.Geometry.Euclidean.Angle.Unoriented.TriangleInequality

Goal state before:
pp: case mpr.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y z : V
hy : y ≠ 0
h : y ∈ Submodule.span ℝ≥0 {x, z}
⊢ angle x z = angle x y + angle y z

Tactic:
exact angle_eq_angle_add_add_angle_add_of_mem_span hy h

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
⊢ HasFDerivAt (fun x ↦ (R / dist x c) ^ 2 • (x -ᵥ c) +ᵥ c) ?refine_1 (c + x)

Tactic:
[

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
⊢ HasFDerivAt (fun x ↦ (R / dist x c) ^ 2 • (x -ᵥ c) +ᵥ c) ?refine_1 (c + x)
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)
⊢ dist (s.faceOppositeCentroid i) (((↑n + 1) / ↑n) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter) =
    dist s.circumcenter (s.points i) / ↑n

Tactic:
[

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)
⊢ dist (s.faceOppositeCentroid i) (((↑n + 1) / ↑n) • (s.centroid -ᵥ s.circumcenter) +ᵥ s.circumcenter) =
    dist s.circumcenter (s.points i) / ↑n
Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
⊢ Similar v₁ v₂ ↔ ∃ r, r ≠ 0 ∧ Pairwise fun i₁ i₂ ↦ nndist (v₁ i₁) (v₁ i₂) = r * nndist (v₂ i₁) (v₂ i₂)

Tactic:
[

Goal state after:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
⊢ Similar v₁ v₂ ↔ ∃ r, r ≠ 0 ∧ Pairwise fun i₁ i₂ ↦ nndist (v₁ i₁) (v₁ i₂) = r * nndist (v₂ i₁) (v₂ i₂)
Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
⊢ Similar v₁ v₂ ↔ ∃ r, r ≠ 0 ∧ Pairwise fun i₁ i₂ ↦ dist (v₁ i₁) (v₁ i₂) = ↑r * dist (v₂ i₁) (v₂ i₂)

Tactic:
[

Goal state after:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
⊢ Similar v₁ v₂ ↔ ∃ r, r ≠ 0 ∧ Pairwise fun i₁ i₂ ↦ dist (v₁ i₁) (v₁ i₂) = ↑r * dist (v₂ i₁) (v₂ i₂)
Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
⊢ (∃ r, r ≠ 0 ∧ ∀ (i₁ i₂ : ι), dist (v₁ i₁) (v₁ i₂) = ↑r * dist (v₂ i₁) (v₂ i₂)) ↔
    ∃ r, 0 < r ∧ ∀ (i₁ i₂ : ι), dist (v₁ i₁) (v₁ i₂) = r * dist (v₂ i₁) (v₂ i₂)

Tactic:
[

Goal state after:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
⊢ (∃ r, r ≠ 0 ∧ ∀ (i₁ i₂ : ι), dist (v₁ i₁) (v₁ i₂) = ↑r * dist (v₂ i₁) (v₂ i₂)) ↔
    ∃ r, 0 < r ∧ ∀ (i₁ i₂ : ι), dist (v₁ i₁) (v₁ i₂) = r * dist (v₂ i₁) (v₂ i₂)
Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
⊢ Similar v₁ v₂ ↔ ∃ r, 0 < r ∧ Pairwise fun i₁ i₂ ↦ dist (v₁ i₁) (v₁ i₂) = r * dist (v₂ i₁) (v₂ i₂)

Tactic:
[

Goal state after:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
⊢ Similar v₁ v₂ ↔ ∃ r, 0 < r ∧ Pairwise fun i₁ i₂ ↦ dist (v₁ i₁) (v₁ i₂) = r * dist (v₂ i₁) (v₂ i₂)
Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
⊢ (∃ r, r ≠ 0 ∧ Pairwise fun i₁ i₂ ↦ dist (v₁ i₁) (v₁ i₂) = ↑r * dist (v₂ i₁) (v₂ i₂)) ↔
    ∃ r, 0 < r ∧ Pairwise fun i₁ i₂ ↦ dist (v₁ i₁) (v₁ i₂) = r * dist (v₂ i₁) (v₂ i₂)

Tactic:
[

Goal state after:
ι : Type u_1
P₁ : Type u_3
P₂ : Type u_4
v₁ : ι → P₁
v₂ : ι → P₂
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
⊢ (∃ r, r ≠ 0 ∧ Pairwise fun i₁ i₂ ↦ dist (v₁ i₁) (v₁ i₂) = ↑r * dist (v₂ i₁) (v₂ i₂)) ↔
    ∃ r, 0 < r ∧ Pairwise fun i₁ i₂ ↦ dist (v₁ i₁) (v₁ i₂) = r * dist (v₂ i₁) (v₂ i₂)
Module: Mathlib.Geometry.Euclidean.NinePointCircle

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
hn : NeZero 1
s : Simplex ℝ P 1
i : Fin (1 + 1)
⊢ 2⁻¹ • ((↑1)⁻¹ • (s.centroid -ᵥ s.points i) + (s.points i -ᵥ s.centroid)) = 0

Tactic:
exact (smul_eq_zero_of_right _ (by simp))

Goal state after:
Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: case h.«0»
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := dist a b / dist a' b'
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
j : Fin (Nat.succ 0).succ.succ
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a, b, c] j) =
    r * dist (![a', b', c'] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a', b', c'] j)

Tactic:
fin_cases j

Goal state after:
case h.«0».«0»
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := dist a b / dist a' b'
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨0, ⋯⟩)) =
    r * dist (![a', b', c'] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨0, ⋯⟩))

case h.«0».«1»
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := dist a b / dist a' b'
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨1, ⋯⟩)) =
    r * dist (![a', b', c'] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨1, ⋯⟩))

case h.«0».«2»
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := dist a b / dist a' b'
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
hij : (fun i ↦ i) ⟨0, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨2, ⋯⟩)) =
    r * dist (![a', b', c'] ((fun i ↦ i) ⟨0, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨2, ⋯⟩))
Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: case h.«1»
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := dist a b / dist a' b'
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
j : Fin (Nat.succ 0).succ.succ
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a, b, c] j) =
    r * dist (![a', b', c'] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a', b', c'] j)

Tactic:
fin_cases j

Goal state after:
case h.«1».«0»
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := dist a b / dist a' b'
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨0, ⋯⟩)) =
    r * dist (![a', b', c'] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨0, ⋯⟩))

case h.«1».«1»
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := dist a b / dist a' b'
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨1, ⋯⟩)) =
    r * dist (![a', b', c'] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨1, ⋯⟩))

case h.«1».«2»
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := dist a b / dist a' b'
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
hij : (fun i ↦ i) ⟨1, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨2, ⋯⟩)) =
    r * dist (![a', b', c'] ((fun i ↦ i) ⟨1, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨2, ⋯⟩))
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)
⊢ (s.reindex e).mongePoint = s.mongePoint

Tactic:
[

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)
⊢ (s.reindex e).mongePoint = s.mongePoint
Module: Mathlib.Topology.MetricSpace.Similarity

Goal state before:
pp: case h.«2»
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := dist a b / dist a' b'
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
j : Fin (Nat.succ 0).succ.succ
hij : (fun i ↦ i) ⟨2, ⋯⟩ ≠ j
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a, b, c] j) =
    r * dist (![a', b', c'] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a', b', c'] j)

Tactic:
fin_cases j

Goal state after:
case h.«2».«0»
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := dist a b / dist a' b'
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
hij : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨0, ⋯⟩
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨0, ⋯⟩)) =
    r * dist (![a', b', c'] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨0, ⋯⟩))

case h.«2».«1»
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := dist a b / dist a' b'
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
hij : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨1, ⋯⟩
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨1, ⋯⟩)) =
    r * dist (![a', b', c'] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨1, ⋯⟩))

case h.«2».«2»
P₁ : Type u_3
P₂ : Type u_4
inst✝¹ : PseudoMetricSpace P₁
inst✝ : PseudoMetricSpace P₂
a b c : P₁
a' b' c' : P₂
h_ne : dist a b ≠ 0
h_ne' : dist a' b' ≠ 0
heq1 : dist a b * dist b' c' = dist b c * dist a' b'
heq2 : dist a b * dist c' a' = dist c a * dist a' b'
r : ℝ := dist a b / dist a' b'
hr : r = dist a b / dist a' b'
hr_pos : 0 < r
hij : (fun i ↦ i) ⟨2, ⋯⟩ ≠ (fun i ↦ i) ⟨2, ⋯⟩
⊢ dist (![a, b, c] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a, b, c] ((fun i ↦ i) ⟨2, ⋯⟩)) =
    r * dist (![a', b', c'] ((fun i ↦ i) ⟨2, ⋯⟩)) (![a', b', c'] ((fun i ↦ i) ⟨2, ⋯⟩))
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
V₂ : Type u_3
P₂ : Type u_4
inst✝³ : NormedAddCommGroup V₂
inst✝² : InnerProductSpace ℝ V₂
inst✝¹ : MetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
⊢ (s.map f.toAffineMap ⋯).mongePoint = f s.mongePoint

Tactic:
[

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₂ : Type u_3
P₂ : Type u_4
inst✝³ : NormedAddCommGroup V₂
inst✝² : InnerProductSpace ℝ V₂
inst✝¹ : MetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
n : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
⊢ (s.map f.toAffineMap ⋯).mongePoint = f s.mongePoint
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
n : ℕ
s : Simplex ℝ P n
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
this : Nonempty ↥S
⊢ ↑(s.restrict S hS).mongePoint = s.mongePoint

Tactic:
[

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
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
this : Nonempty ↥S
⊢ ↑(s.restrict S hS).mongePoint = s.mongePoint
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
n : ℕ
s₁ s₂ : Simplex ℝ P n
h : Set.range s₁.points = Set.range s₂.points
⊢ s₁.mongePoint = s₂.mongePoint

Tactic:
[

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₁ s₂ : Simplex ℝ P n
h : Set.range s₁.points = Set.range s₂.points
⊢ s₁.mongePoint = s₂.mongePoint
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: n : ℕ
⊢ ∑ i, mongePointWeightsWithCircumcenter n i = 1

Tactic:
[

Goal state after:
n : ℕ
⊢ ∑ i, mongePointWeightsWithCircumcenter n i = 1