-- Mathlib/Geometry/Euclidean/Triangle.lean
theorem dist_mul_of_eq_angle_of_dist_mul (a b c a' b' c' : P) (r : ℝ) (h : ∠ a' b' c' = ∠ a b c)
    (hab : dist a' b' = r * dist a b) (hcb : dist c' b' = r * dist c b) :
    dist a' c' = r * dist a c

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
⊢ r ^ 2 * (dist a b ^ 2 + dist c b ^ 2 - 2 * dist a b * dist c b * Real.cos (∠ a b c)) = (r * dist a c) ^ 2

Tactic:
simp [pow_two, ← law_cos a b c, mul_pow]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
⊢ r * r * (dist a c * dist a c) = r * dist a c * (r * dist a c)

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : dist a' c' ^ 2 = (r * dist a c) ^ 2
hab₁ : a = b
⊢ a' = b'

Tactic:
rw [← dist_eq_zero, hab, dist_eq_zero.mpr hab₁, mul_zero r]

Result:
no goals

Proof state:
case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : dist a' c' ^ 2 = (r * dist a c) ^ 2
hab₁ : ¬a = b
h1 : 0 ≤ r * dist a b
h2 : 0 ≤ r
⊢ dist a' c' = r * dist a c

Tactic:
exact (sq_eq_sq₀ dist_nonneg (mul_nonneg h2 dist_nonneg)).mp h'

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
⊢ (r * dist a b) ^ 2 + (r * dist c b) ^ 2 - 2 * (r * dist a b) * (r * dist c b) * Real.cos (∠ a b c) =
    r ^ 2 * (dist a b ^ 2 + dist c b ^ 2 - 2 * dist a b * dist c b * Real.cos (∠ a b c))

Tactic:
ring

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : dist a' c' ^ 2 = (r * dist a c) ^ 2
hab₁ : ¬a = b
⊢ 0 ≤ r * dist a b

Tactic:
rw [← hab]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : dist a' c' ^ 2 = (r * dist a c) ^ 2
hab₁ : ¬a = b
⊢ 0 ≤ dist a' b'

Proof state:
case pos
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : dist a' c' ^ 2 = (r * dist a c) ^ 2
hab₁ : a = b
hab'₁ : a' = b'
⊢ dist a' c' = r * dist a c

Tactic:
rw [hab₁, hab'₁, dist_comm b' c', dist_comm b c, hcb]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
⊢ dist a' b' ^ 2 + dist c' b' ^ 2 - 2 * dist a' b' * dist c' b' * Real.cos (∠ a' b' c') =
    r ^ 2 * (dist a b ^ 2 + dist c b ^ 2 - 2 * dist a b * dist c b * Real.cos (∠ a b c))

Tactic:
rw [h, hab, hcb]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
⊢ (r * dist a b) ^ 2 + (r * dist c b) ^ 2 - 2 * (r * dist a b) * (r * dist c b) * Real.cos (∠ a b c) =
    r ^ 2 * (dist a b ^ 2 + dist c b ^ 2 - 2 * dist a b * dist c b * Real.cos (∠ a b c))

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : dist a' c' ^ 2 = (r * dist a c) ^ 2
hab₁ : ¬a = b
⊢ 0 ≤ dist a' b'

Tactic:
exact dist_nonneg

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
⊢ r * r * (dist a c * dist a c) = r * dist a c * (r * dist a c)

Tactic:
ring

Result:
no goals

Proof state:
case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : dist a' c' ^ 2 = (r * dist a c) ^ 2
hab₁ : ¬a = b
⊢ dist a' c' = r * dist a c

Tactic:
have h1 : 0 ≤ r * dist a b := by rw [← hab]; exact dist_nonneg

Result:
case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : dist a' c' ^ 2 = (r * dist a c) ^ 2
hab₁ : ¬a = b
h1 : 0 ≤ r * dist a b
⊢ dist a' c' = r * dist a c

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
⊢ dist a' c' = r * dist a c

Tactic:
have h' : dist a' c' ^ 2 = (r * dist a c) ^ 2 := calc
  dist a' c' ^ 2 =
      dist a' b' ^ 2 + dist c' b' ^ 2 - 2 * dist a' b' * dist c' b' * Real.cos (∠ a' b' c') := by
    simp [pow_two, law_cos a' b' c']
  _ = r ^ 2 * (dist a b ^ 2 + dist c b ^ 2 - 2 * dist a b * dist c b * Real.cos (∠ a b c)) := by
    rw [h, hab, hcb]; ring
  _ = (r * dist a c) ^ 2 := by simp [pow_two, ← law_cos a b c, mul_pow]; ring

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : dist a' c' ^ 2 = (r * dist a c) ^ 2
⊢ dist a' c' = r * dist a c

Proof state:
case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : dist a' c' ^ 2 = (r * dist a c) ^ 2
hab₁ : ¬a = b
h1 : 0 ≤ r * dist a b
⊢ dist a' c' = r * dist a c

Tactic:
have h2 : 0 ≤ r := nonneg_of_mul_nonneg_left h1 (dist_pos.mpr hab₁)

Result:
case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
a b c a' b' c' : P
r : ℝ
h : ∠ a' b' c' = ∠ a b c
hab : dist a' b' = r * dist a b
hcb : dist c' b' = r * dist c b
h' : dist a' c' ^ 2 = (r * dist a c) ^ 2
hab₁ : ¬a = b
h1 : 0 ≤ r * dist a b
h2 : 0 ≤ r
⊢ dist a' c' = r * dist a c