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

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 : P
hs : s.center ∈ s
hsp : p = s.center
⊢ p ∈ s

Tactic:
← hsp

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 : P
hs : p ∈ s
hsp : p = s.center
⊢ p ∈ s
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

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
as : AffineSubspace ℝ P
h : s.IsTangent as
p : P
hp : p ∈ as
⊢ s.radius ≤ dist p s.center

Tactic:
obtain ⟨x, h⟩ := h
  refine le_of_sq_le_sq ?_ dist_nonneg
  rw [h.dist_sq_eq_of_mem hp, le_add_iff_nonneg_right]
  exact sq_nonneg _

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

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
s : Sphere P
p₁ p₂ : P
hp₁ : p₁ ∈ s
hp₂ : dist p₂ s.center < s.radius
h : p₁ = p₂
⊢ 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫

Tactic:
rw [h, mem_sphere] at hp₁

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
s : Sphere P
p₁ p₂ : P
hp₁ : dist p₂ s.center = s.radius
hp₂ : dist p₂ s.center < s.radius
h : p₁ = p₂
⊢ 0 < ⟪p₁ -ᵥ p₂, p₁ -ᵥ s.center⟫
Module: Mathlib.Geometry.Euclidean.Sphere.Tangent

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
as : AffineSubspace ℝ P
inst✝¹ : Nonempty ↥as
inst✝ : as.direction.HasOrthogonalProjection
h : s.IsTangentAt p as
⊢ p = ↑((orthogonalProjection as) s.center)

Tactic:
refine h.eq_of_isTangentAt ?_
  have h' := h.isTangent
  rwa [isTangent_iff_isTangentAt_orthogonalProjection] at h'

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

Goal state before:
pp: case refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s₁ s₂ : Sphere P
h₁ : s₁.center ∈ s₁
h₂ : s₁.center ∈ s₂
⊢ s₁.radius = 0 ∧ s₁.center ∈ s₂

Tactic:
center_mem_iff

Goal state after:
case refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s₁ s₂ : Sphere P
h₁ : s₁.radius = 0
h₂ : s₁.center ∈ s₂
⊢ s₁.radius = 0 ∧ s₁.center ∈ s₂
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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center ≤ s.radius
hpc : p ≠ s.center
v : V
hv : v ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ
hv1 : ‖v‖ = 1
⊢ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) =
    {√(s.radius ^ 2 - dist p s.center ^ 2) • v +ᵥ p, -√(s.radius ^ 2 - dist p s.center ^ 2) • v +ᵥ p}

Tactic:
have hr : 0 ≤ s.radius := dist_nonneg.trans hp

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center ≤ s.radius
hpc : p ≠ s.center
v : V
hv : v ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ
hv1 : ‖v‖ = 1
hr : 0 ≤ s.radius
⊢ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p) =
    {√(s.radius ^ 2 - dist p s.center ^ 2) • v +ᵥ p, -√(s.radius ^ 2 - dist p s.center ^ 2) • v +ᵥ p}
Module: Mathlib.Geometry.Euclidean.Sphere.OrthRadius

Goal state before:
pp: case refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center ≤ s.radius
hpc : p ≠ s.center
v : V
hv : v ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ
hv1 : ‖v‖ = 1
hr : 0 ≤ s.radius
hv0 : v ≠ 0
hf : ∀ (w : ↥(ℝ ∙ (p -ᵥ s.center))ᗮ), ∃ c, c • ⟨v, hv⟩ = w
hvc : ∀ w ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ, ∃ c, c • v = w
hvp : 0 ≤ s.radius ^ 2 - dist p s.center ^ 2
p' : P
h : p' ∈ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p)
⊢ (p' -ᵥ p) +ᵥ p = √(s.radius ^ 2 - dist p s.center ^ 2) • v +ᵥ p ∨
    (p' -ᵥ p) +ᵥ p = -(√(s.radius ^ 2 - dist p s.center ^ 2) • v) +ᵥ p

Tactic:
vadd_right_cancel_iff,

Goal state after:
case refine_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center ≤ s.radius
hpc : p ≠ s.center
v : V
hv : v ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ
hv1 : ‖v‖ = 1
hr : 0 ≤ s.radius
hv0 : v ≠ 0
hf : ∀ (w : ↥(ℝ ∙ (p -ᵥ s.center))ᗮ), ∃ c, c • ⟨v, hv⟩ = w
hvc : ∀ w ∈ (ℝ ∙ (p -ᵥ s.center))ᗮ, ∃ c, c • v = w
hvp : 0 ≤ s.radius ^ 2 - dist p s.center ^ 2
p' : P
h : p' ∈ Metric.sphere s.center s.radius ∩ ↑(s.orthRadius p)
⊢ p' -ᵥ p = √(s.radius ^ 2 - dist p s.center ^ 2) • v ∨
    (p' -ᵥ p) +ᵥ p = -(√(s.radius ^ 2 - dist p s.center ^ 2) • v) +ᵥ p
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
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center < s.radius
hpc : p ≠ s.center
v : ↥(s.orthRadius p).direction
hv : ∀ (w : ↥(s.orthRadius p).direction), ∃ c, c • v = w
hv0 : ↑v ≠ 0
⊢ ¬(√(s.radius ^ 2 - dist p s.center ^ 2) / ‖v‖) • ↑v +ᵥ p = -((√(s.radius ^ 2 - dist p s.center ^ 2) / ‖v‖) • ↑v) +ᵥ p

Tactic:
vadd_right_cancel_iff,

Goal state after:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
hf2 : Fact (Module.finrank ℝ V = 2)
s : Sphere P
p : P
hp : dist p s.center < s.radius
hpc : p ≠ s.center
v : ↥(s.orthRadius p).direction
hv : ∀ (w : ↥(s.orthRadius p).direction), ∃ c, c • v = w
hv0 : ↑v ≠ 0
⊢ ¬(√(s.radius ^ 2 - dist p s.center ^ 2) / ‖v‖) • ↑v = -((√(s.radius ^ 2 - dist p s.center ^ 2) / ‖v‖) • ↑v)
Module: Mathlib.Geometry.Euclidean.Angle.Sphere

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
p₁ p₂ p₃ : P
s : Sphere P
inst✝ : Fact (finrank ℝ V = 2)
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hne₁₂ : p₁ ≠ p₂
hne₂₃ : p₂ ≠ p₃
hangle : ∠ p₁ p₂ p₃ = π / 2
this : FiniteDimensional ℝ V
hne₁₃ : p₁ ≠ p₃
hd : (Sphere.ofDiameter p₁ p₃).IsDiameter p₁ p₃
hne : ¬s = Sphere.ofDiameter p₁ p₃
⊢ False

Tactic:
have := eq_of_mem_sphere_of_mem_sphere_of_finrank_eq_two
      (Fact.out : finrank ℝ V = 2) hne hne₁₃ hp₁ hp₃ hp₂
      hd.left_mem hd.right_mem (angle_eq_pi_div_two_iff_mem_sphere_ofDiameter.mp hangle)

Goal state after:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
p₁ p₂ p₃ : P
s : Sphere P
inst✝ : Fact (finrank ℝ V = 2)
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃ : p₃ ∈ s
hne₁₂ : p₁ ≠ p₂
hne₂₃ : p₂ ≠ p₃
hangle : ∠ p₁ p₂ p₃ = π / 2
this✝ : FiniteDimensional ℝ V
hne₁₃ : p₁ ≠ p₃
hd : (Sphere.ofDiameter p₁ p₃).IsDiameter p₁ p₃
hne : ¬s = Sphere.ofDiameter p₁ p₃
this : p₂ = p₁ ∨ p₂ = p₃
⊢ False
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
hm : s.excenter signs ∈ affineSpan ℝ (Set.range (s.face hfs).points)
⊢ False

Tactic:
rw [range_face_points] at 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 ℝ (s.points '' ↑fs)
⊢ False
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)
⊢ (affineSpan ℝ (Set.range (s.faceOpposite i).points)).SOppSide
      ((Finset.affineCombination ℝ Finset.univ s.points) (s.excenterWeights signs)) (s.points i) ↔
    s.excenterWeights signs i < 0

Tactic:
s.sOppSide_affineSpan_faceOpposite_point_right_iff h.sum_excenterWeights_eq_one

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)
⊢ s.excenterWeights signs i < 0 ↔ s.excenterWeights signs i < 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
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:
rw [← s.excenterExists_restrict S hS] at h
  have := Nonempty.map (AffineSubspace.inclusion hS) inferInstance
  exact (h.touchpoint_map S.subtypeₐᵢ i).symm

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

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hn : ¬Collinear ℝ {p₁, p₂, p₄}
⊢ ¬Collinear ℝ {p₁, p₃, p₄}

Tactic:
← collinear_iff_of_two_zsmul_oangle_eq 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
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
h : 2 • ∡ p₁ p₂ p₄ = 2 • ∡ p₁ p₃ p₄
hn : ¬Collinear ℝ {p₁, p₂, p₄}
⊢ ¬Collinear ℝ {p₁, p₂, p₄}
Module: Mathlib.Geometry.Euclidean.Angle.Sphere

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
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₄
⊢ Collinear ℝ {p₁, p₃, p₄}

Tactic:
← collinear_iff_of_two_zsmul_oangle_eq 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
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₄
⊢ Collinear ℝ {p₁, p₂, p₄}
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}
⊢ ![a, b, c] ≅ ![a', b', c']

Tactic:
have h_bac' : ¬Collinear ℝ {b', a', c'} := by simpa [Set.insert_comm] using h'

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}
h_bac' : ¬Collinear ℝ {b', a', c'}
⊢ ![a, b, c] ≅ ![a', b', c']
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:
by
  simp_rw [similar_iff_exists_pairwise_edist_eq, edist_nndist]
  exact_mod_cast Iff.rfl

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

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₂ i₃ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hr : ∀ (i j : Fin (n + 1)), i ≠ j → dist (s.points i) (s.points j) = 0
⊢ False

Tactic:
replace hr := hr _ _ 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
n : ℕ
s : Simplex ℝ P n
i₁ i₂ i₃ : Fin (n + 1)
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hr : dist (s.points i₁) (s.points i₂) = 0
⊢ False
Module: Mathlib.Geometry.Euclidean.Similarity

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_not_col : ¬Collinear ℝ {a, b, c}
h₁ : ∠ a b c = ∠ a' b' c'
h₂ : ∠ b c a = ∠ b' c' a'
hne_pi_div_two : ∠ a b c ≠ Real.pi / 2 ∨ ∠ b c a ≠ Real.pi / 2
not_all_eq : a' ≠ b' ∨ b' ≠ c' ∨ a' ≠ c'
h_not_col' : ¬Collinear ℝ {a', b', c'}
h_pos1 : 0 < dist a b
h_pos1' : 0 < dist a' b'
h_pos2 : 0 < dist b c
h_pos2' : 0 < dist b' c'
h₃ : ∠ c a b = ∠ c' a' b'
h_sin_ne1 : Real.sin (∠ b c a) ≠ 0
h_sin_ne2 : Real.sin (∠ c a b) ≠ 0
h_sin1 : dist b' c' / dist a' b' = dist b c / dist a b
h_sin1' : Real.sin (∠ c a b) = Real.sin (∠ b c a) * dist b' c' / dist a' b'
⊢ ![a, b, c] ∼ ![a', b', c']

Tactic:
div_eq_div_iff (by positivity) (by positivity),

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_not_col : ¬Collinear ℝ {a, b, c}
h₁ : ∠ a b c = ∠ a' b' c'
h₂ : ∠ b c a = ∠ b' c' a'
hne_pi_div_two : ∠ a b c ≠ Real.pi / 2 ∨ ∠ b c a ≠ Real.pi / 2
not_all_eq : a' ≠ b' ∨ b' ≠ c' ∨ a' ≠ c'
h_not_col' : ¬Collinear ℝ {a', b', c'}
h_pos1 : 0 < dist a b
h_pos1' : 0 < dist a' b'
h_pos2 : 0 < dist b c
h_pos2' : 0 < dist b' c'
h₃ : ∠ c a b = ∠ c' a' b'
h_sin_ne1 : Real.sin (∠ b c a) ≠ 0
h_sin_ne2 : Real.sin (∠ c a b) ≠ 0
h_sin1 : dist b' c' * dist a b = dist b c * dist a' b'
h_sin1' : Real.sin (∠ c a b) = Real.sin (∠ b c a) * dist b' c' / dist a' b'
⊢ ![a, b, c] ∼ ![a', b', c']
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
i : Fin (n + 2 + 1)
⊢ #{i₁, i₂}ᶜ = n + 1

Tactic:
simp [card_compl, Fintype.card_fin, h]

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

Goal state before:
pp: n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
⊢ ∑ x, mongePointWeightsWithCircumcenter n x - ∑ x, centroidWeightsWithCircumcenter {i₁, i₂}ᶜ x = 0

Tactic:
sum_mongePointWeightsWithCircumcenter

Goal state after:
n : ℕ
i₁ i₂ : Fin (n + 3)
h : i₁ ≠ i₂
⊢ 1 - ∑ x, centroidWeightsWithCircumcenter {i₁, i₂}ᶜ x = 0
Module: Mathlib.Geometry.Euclidean.Similarity

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_not_col : ¬Collinear ℝ {a, b, c}
h₁ : ∠ a b c = ∠ a' b' c'
h₂ : ∠ b c a = ∠ b' c' a'
hne_pi_div_two : ∠ a b c ≠ Real.pi / 2 ∨ ∠ b c a ≠ Real.pi / 2
not_all_eq : a' ≠ b' ∨ b' ≠ c' ∨ a' ≠ c'
h_not_col' : ¬Collinear ℝ {a', b', c'}
h_pos1 : 0 < dist a b
h_pos1' : 0 < dist a' b'
h_pos2 : 0 < dist b c
h_pos2' : 0 < dist b' c'
h₃ : ∠ c a b = ∠ c' a' b'
h_sin_ne1 : Real.sin (∠ b c a) ≠ 0
h_sin_ne2 : Real.sin (∠ c a b) ≠ 0
h_sin1 : dist a b * dist b' c' = dist b c * dist a' b'
h_sin1' : Real.sin (∠ c a b) = Real.sin (∠ b c a) * dist b' c' / dist a' b'
h_sin2 : dist c' a' / dist b' c' = dist c a / dist b c
h_sin2' : Real.sin (∠ a b c) = Real.sin (∠ c a b) * dist c' a' / dist b' c'
⊢ ![a, b, c] ∼ ![a', b', c']

Tactic:
div_eq_div_iff (by positivity) (by positivity),

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_not_col : ¬Collinear ℝ {a, b, c}
h₁ : ∠ a b c = ∠ a' b' c'
h₂ : ∠ b c a = ∠ b' c' a'
hne_pi_div_two : ∠ a b c ≠ Real.pi / 2 ∨ ∠ b c a ≠ Real.pi / 2
not_all_eq : a' ≠ b' ∨ b' ≠ c' ∨ a' ≠ c'
h_not_col' : ¬Collinear ℝ {a', b', c'}
h_pos1 : 0 < dist a b
h_pos1' : 0 < dist a' b'
h_pos2 : 0 < dist b c
h_pos2' : 0 < dist b' c'
h₃ : ∠ c a b = ∠ c' a' b'
h_sin_ne1 : Real.sin (∠ b c a) ≠ 0
h_sin_ne2 : Real.sin (∠ c a b) ≠ 0
h_sin1 : dist a b * dist b' c' = dist b c * dist a' b'
h_sin1' : Real.sin (∠ c a b) = Real.sin (∠ b c a) * dist b' c' / dist a' b'
h_sin2 : dist c' a' * dist b c = dist c a * dist b' c'
h_sin2' : Real.sin (∠ a b c) = Real.sin (∠ c a b) * dist c' a' / dist b' c'
⊢ ![a, b, c] ∼ ![a', b', c']
Module: Mathlib.Geometry.Euclidean.Similarity

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_not_col : ¬Collinear ℝ {a, b, c}
h_not_col' : ¬Collinear ℝ {a', b', c'}
h : ∠ a b c = ∠ a' b' c'
hd : dist a b * dist b' c' = dist b c * dist a' b'
dist_a'b' : dist a' b' ≠ 0
dist_b'c' : dist b' c' ≠ 0
⊢ ![a, b, c] ∼ ![a', b', c']

Tactic:
← div_eq_div_iff dist_a'b' dist_b'c'

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_not_col : ¬Collinear ℝ {a, b, c}
h_not_col' : ¬Collinear ℝ {a', b', c'}
h : ∠ a b c = ∠ a' b' c'
hd : dist a b / dist a' b' = dist b c / dist b' c'
dist_a'b' : dist a' b' ≠ 0
dist_b'c' : dist b' c' ≠ 0
⊢ ![a, b, c] ∼ ![a', b', c']
Module: Mathlib.Geometry.Euclidean.Similarity

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_not_col : ¬Collinear ℝ {a, b, c}
h_not_col' : ¬Collinear ℝ {a', b', c'}
h : ∠ a b c = ∠ a' b' c'
dist_a'b' : dist a' b' ≠ 0
dist_b'c' : dist b' c' ≠ 0
k : ℝ := dist a b / dist a' b'
hd : k = dist b c / dist b' c'
hk : k = dist a b / dist a' b'
k_pos : 0 < k
h_ab : dist a b = k * dist a' b'
h_bc : dist b c = k * dist b' c'
hcos : dist c a = k * dist c' a'
hcos' : dist a' c' ^ 2 = dist a' b' ^ 2 + dist c' b' ^ 2 - dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
dist_ac_pos : 0 < dist a c
k_dist_a'c' : 0 ≤ k * dist a' c'
⊢ ∃ r,
    0 < r ∧ Pairwise fun i₁ i₂ ↦ dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)

Tactic:
use k

Goal state after:
case h
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_not_col : ¬Collinear ℝ {a, b, c}
h_not_col' : ¬Collinear ℝ {a', b', c'}
h : ∠ a b c = ∠ a' b' c'
dist_a'b' : dist a' b' ≠ 0
dist_b'c' : dist b' c' ≠ 0
k : ℝ := ⋯
hd : k = dist b c / dist b' c'
hk : k = dist a b / dist a' b'
k_pos : 0 < k
h_ab : dist a b = k * dist a' b'
h_bc : dist b c = k * dist b' c'
hcos : dist c a = k * dist c' a'
hcos' : dist a' c' ^ 2 = dist a' b' ^ 2 + dist c' b' ^ 2 - dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
dist_ac_pos : 0 < dist a c
k_dist_a'c' : 0 ≤ k * dist a' c'
⊢ 0 < k ∧ Pairwise fun i₁ i₂ ↦ dist (![a, b, c] i₁) (![a, b, c] i₂) = k * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
Module: Mathlib.Geometry.Euclidean.MongePoint

Goal state before:
pp: case e'_2.e'_5.e'_9
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 + 2)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ : Fin (n + 3)
⊢ {i₁, i₂}ᶜ = Finset.map e.toEmbedding {e.symm i₁, e.symm i₂}ᶜ

pp: case e'_3.e'_5
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 + 2)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ : Fin (n + 3)
⊢ s.points = (s.points ∘ ⇑e.symm) ∘ ⇑e.toEmbedding

pp: case e'_3.e'_6
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 + 2)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ : Fin (n + 3)
⊢ centroidWeights ℝ {e.symm i₁, e.symm i₂}ᶜ = centroidWeights ℝ {i₁, i₂}ᶜ ∘ ⇑e.toEmbedding

Tactic:
· ext i
    simp

Goal state after:
case e'_3.e'_5
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 + 2)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ : Fin (n + 3)
⊢ s.points = (s.points ∘ ⇑e.symm) ∘ ⇑e.toEmbedding

case e'_3.e'_6
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 + 2)
e : Fin (n + 3) ≃ Fin (n + 3)
i₁ i₂ : Fin (n + 3)
⊢ centroidWeights ℝ {e.symm i₁, e.symm i₂}ᶜ = centroidWeights ℝ {i₁, i₂}ᶜ ∘ ⇑e.toEmbedding