awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Similarity
Goal:
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
inst_2 : InnerProductSpace ℝ V₁
inst_3 : InnerProductSpace ℝ V₂
inst_4 : MetricSpace P₁
inst_5 : MetricSpace P₂
inst_6 : NormedAddTorsor V₁ P₁
inst_7 : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos : dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c') = dist a' b' * dist c' b' * 2 * Real.cos (∠ a b c)
h_cos' :
  HPow.hPow (β := ℕ) (dist a' c') 2 =
    HPow.hPow (β := ℕ) (dist a' b') 2 + HPow.hPow (β := ℕ) (dist c' b') 2 -
      dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
pos : ∀ (heq : dist a' b' * dist c' b' * 2 = 0), ∠ a b c = ∠ a' b' c'
neg : ∀ (heq : ¬dist a' b' * dist c' b' * 2 = 0), ∠ a b c = ∠ a' b' c'
⊢ ∠ a b c = ∠ a' b' c'

Tactic:
by_cases heq : dist a' b' * dist c' b' * 2 = 0

Premises used: Dist.dist
-- Module: Mathlib.Geometry.Euclidean.Similarity
Goal:
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
inst_2 : InnerProductSpace ℝ V₁
inst_3 : InnerProductSpace ℝ V₂
inst_4 : MetricSpace P₁
inst_5 : MetricSpace P₂
inst_6 : NormedAddTorsor V₁ P₁
inst_7 : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos : dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c') = dist a' b' * dist c' b' * 2 * Real.cos (∠ a b c)
h_cos' :
  HPow.hPow (β := ℕ) (dist a' c') 2 =
    HPow.hPow (β := ℕ) (dist a' b') 2 + HPow.hPow (β := ℕ) (dist c' b') 2 -
      dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
heq : dist a' b' * dist c' b' * 2 = 0
⊢ Ne (α := ℝ) 2 0

Tactic:
norm_num
-- Module: Mathlib.Geometry.Euclidean.Similarity
Goal:
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
inst_2 : InnerProductSpace ℝ V₁
inst_3 : InnerProductSpace ℝ V₂
inst_4 : MetricSpace P₁
inst_5 : MetricSpace P₂
inst_6 : NormedAddTorsor V₁ P₁
inst_7 : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos : dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c') = dist a' b' * dist c' b' * 2 * Real.cos (∠ a b c)
h_cos' :
  HPow.hPow (β := ℕ) (dist a' c') 2 =
    HPow.hPow (β := ℕ) (dist a' b') 2 + HPow.hPow (β := ℕ) (dist c' b') 2 -
      dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
heq : dist a' b' * dist c' b' * 2 = 0
⊢ dist a' b' = 0 ∨ dist c' b' = 0

Tactic:
rw [mul_eq_zero_iff_right (by norm_num), mul_eq_zero] at heq

Premises used: mul_eq_zero, mul_eq_zero_iff_right
-- Module: Mathlib.Geometry.Euclidean.Similarity
Goal:
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
inst_2 : InnerProductSpace ℝ V₁
inst_3 : InnerProductSpace ℝ V₂
inst_4 : MetricSpace P₁
inst_5 : MetricSpace P₂
inst_6 : NormedAddTorsor V₁ P₁
inst_7 : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos : dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c') = dist a' b' * dist c' b' * 2 * Real.cos (∠ a b c)
h_cos' :
  HPow.hPow (β := ℕ) (dist a' c') 2 =
    HPow.hPow (β := ℕ) (dist a' b') 2 + HPow.hPow (β := ℕ) (dist c' b') 2 -
      dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
heq : dist a' b' = 0 ∨ dist c' b' = 0
pos : ∀ (h1 : dist a' b' = 0), ∠ a b c = ∠ a' b' c'
pos₁ : ∀ (h2 : dist c' b' = 0), ∠ a b c = ∠ a' b' c'
⊢ ∠ a b c = ∠ a' b' c'

Tactic:
rcases heq with h1 | h2
-- Module: Mathlib.Geometry.Euclidean.Similarity
Goal:
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
inst_2 : InnerProductSpace ℝ V₁
inst_3 : InnerProductSpace ℝ V₂
inst_4 : MetricSpace P₁
inst_5 : MetricSpace P₂
inst_6 : NormedAddTorsor V₁ P₁
inst_7 : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos : dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c') = dist a' b' * dist c' b' * 2 * Real.cos (∠ a b c)
h_cos' :
  HPow.hPow (β := ℕ) (dist a' c') 2 =
    HPow.hPow (β := ℕ) (dist a' b') 2 + HPow.hPow (β := ℕ) (dist c' b') 2 -
      dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
h1 : dist a' b' = 0
⊢ dist a b = 0

Tactic:
grind
-- Module: Mathlib.Geometry.Euclidean.Similarity
Goal:
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
inst_2 : InnerProductSpace ℝ V₁
inst_3 : InnerProductSpace ℝ V₂
inst_4 : MetricSpace P₁
inst_5 : MetricSpace P₂
inst_6 : NormedAddTorsor V₁ P₁
inst_7 : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos : dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c') = dist a' b' * dist c' b' * 2 * Real.cos (∠ a b c)
h_cos' :
  HPow.hPow (β := ℕ) (dist a' c') 2 =
    HPow.hPow (β := ℕ) (dist a' b') 2 + HPow.hPow (β := ℕ) (dist c' b') 2 -
      dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
h1 : dist a' b' = 0
⊢ dist a b = 0

Tactic:
have h_dist_ab : dist a b = 0 := by grind
-- Module: Mathlib.Geometry.Euclidean.Similarity
Goal:
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
inst_2 : InnerProductSpace ℝ V₁
inst_3 : InnerProductSpace ℝ V₂
inst_4 : MetricSpace P₁
inst_5 : MetricSpace P₂
inst_6 : NormedAddTorsor V₁ P₁
inst_7 : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos : dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c') = dist a' b' * dist c' b' * 2 * Real.cos (∠ a b c)
h_cos' :
  HPow.hPow (β := ℕ) (dist a' c') 2 =
    HPow.hPow (β := ℕ) (dist a' b') 2 + HPow.hPow (β := ℕ) (dist c' b') 2 -
      dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
h1 : dist a' b' = 0
h_dist_ab : dist a b = 0
⊢ a' = b'

Tactic:
rw [dist_eq_zero] at h_dist_ab h1

Premises used: dist_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Similarity
Goal:
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
inst_2 : InnerProductSpace ℝ V₁
inst_3 : InnerProductSpace ℝ V₂
inst_4 : MetricSpace P₁
inst_5 : MetricSpace P₂
inst_6 : NormedAddTorsor V₁ P₁
inst_7 : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos : dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c') = dist a' b' * dist c' b' * 2 * Real.cos (∠ a b c)
h_cos' :
  HPow.hPow (β := ℕ) (dist a' c') 2 =
    HPow.hPow (β := ℕ) (dist a' b') 2 + HPow.hPow (β := ℕ) (dist c' b') 2 -
      dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
h1 : dist a' b' = 0
h_dist_ab : dist a b = 0
h1₁ : a' = b'
⊢ a = b

Tactic:
rw [dist_eq_zero] at h_dist_ab h1

Premises used: dist_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Similarity
Goal:
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
inst_2 : InnerProductSpace ℝ V₁
inst_3 : InnerProductSpace ℝ V₂
inst_4 : MetricSpace P₁
inst_5 : MetricSpace P₂
inst_6 : NormedAddTorsor V₁ P₁
inst_7 : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos : dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c') = dist a' b' * dist c' b' * 2 * Real.cos (∠ a b c)
h_cos' :
  HPow.hPow (β := ℕ) (dist a' c') 2 =
    HPow.hPow (β := ℕ) (dist a' b') 2 + HPow.hPow (β := ℕ) (dist c' b') 2 -
      dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
h1 : a' = b'
h_dist_ab : a = b
pos : ∠ b b c = ∠ a' b' c'
pos₁ : ∠ b b c = ∠ b' b' c'
⊢ ∠ a b c = ∠ a' b' c'

Tactic:
simp_rw [h_dist_ab, h1, angle_self_left]

Premises used: EuclideanGeometry.angle_self_left
-- Module: Mathlib.Geometry.Euclidean.Similarity
Goal:
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
inst_2 : InnerProductSpace ℝ V₁
inst_3 : InnerProductSpace ℝ V₂
inst_4 : MetricSpace P₁
inst_5 : MetricSpace P₂
inst_6 : NormedAddTorsor V₁ P₁
inst_7 : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos : dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c') = dist a' b' * dist c' b' * 2 * Real.cos (∠ a b c)
h_cos' :
  HPow.hPow (β := ℕ) (dist a' c') 2 =
    HPow.hPow (β := ℕ) (dist a' b') 2 + HPow.hPow (β := ℕ) (dist c' b') 2 -
      dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
h2 : dist c' b' = 0
⊢ dist c b = 0

Tactic:
grind
-- Module: Mathlib.Geometry.Euclidean.Similarity
Goal:
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
inst_2 : InnerProductSpace ℝ V₁
inst_3 : InnerProductSpace ℝ V₂
inst_4 : MetricSpace P₁
inst_5 : MetricSpace P₂
inst_6 : NormedAddTorsor V₁ P₁
inst_7 : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos : dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c') = dist a' b' * dist c' b' * 2 * Real.cos (∠ a b c)
h_cos' :
  HPow.hPow (β := ℕ) (dist a' c') 2 =
    HPow.hPow (β := ℕ) (dist a' b') 2 + HPow.hPow (β := ℕ) (dist c' b') 2 -
      dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
h2 : dist c' b' = 0
⊢ dist c b = 0

Tactic:
have h_dist_cb : dist c b = 0 := by grind
-- Module: Mathlib.Geometry.Euclidean.Similarity
Goal:
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
inst_2 : InnerProductSpace ℝ V₁
inst_3 : InnerProductSpace ℝ V₂
inst_4 : MetricSpace P₁
inst_5 : MetricSpace P₂
inst_6 : NormedAddTorsor V₁ P₁
inst_7 : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos : dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c') = dist a' b' * dist c' b' * 2 * Real.cos (∠ a b c)
h_cos' :
  HPow.hPow (β := ℕ) (dist a' c') 2 =
    HPow.hPow (β := ℕ) (dist a' b') 2 + HPow.hPow (β := ℕ) (dist c' b') 2 -
      dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
h2 : dist c' b' = 0
h_dist_cb : dist c b = 0
⊢ c' = b'

Tactic:
rw [dist_eq_zero] at h_dist_cb h2

Premises used: dist_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Similarity
Goal:
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
inst_2 : InnerProductSpace ℝ V₁
inst_3 : InnerProductSpace ℝ V₂
inst_4 : MetricSpace P₁
inst_5 : MetricSpace P₂
inst_6 : NormedAddTorsor V₁ P₁
inst_7 : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos : dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c') = dist a' b' * dist c' b' * 2 * Real.cos (∠ a b c)
h_cos' :
  HPow.hPow (β := ℕ) (dist a' c') 2 =
    HPow.hPow (β := ℕ) (dist a' b') 2 + HPow.hPow (β := ℕ) (dist c' b') 2 -
      dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
h2 : dist c' b' = 0
h_dist_cb : dist c b = 0
h2₁ : c' = b'
⊢ c = b

Tactic:
rw [dist_eq_zero] at h_dist_cb h2

Premises used: dist_eq_zero
-- Module: Mathlib.Geometry.Euclidean.Similarity
Goal:
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
inst_2 : InnerProductSpace ℝ V₁
inst_3 : InnerProductSpace ℝ V₂
inst_4 : MetricSpace P₁
inst_5 : MetricSpace P₂
inst_6 : NormedAddTorsor V₁ P₁
inst_7 : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos : dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c') = dist a' b' * dist c' b' * 2 * Real.cos (∠ a b c)
h_cos' :
  HPow.hPow (β := ℕ) (dist a' c') 2 =
    HPow.hPow (β := ℕ) (dist a' b') 2 + HPow.hPow (β := ℕ) (dist c' b') 2 -
      dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
h2 : c' = b'
h_dist_cb : c = b
pos : ∠ a b b = ∠ a' b' c'
pos₁ : ∠ a b b = ∠ a' b' b'
⊢ ∠ a b c = ∠ a' b' c'

Tactic:
simp_rw [h_dist_cb, h2, angle_self_right]

Premises used: EuclideanGeometry.angle_self_right
-- Module: Mathlib.Geometry.Euclidean.Similarity
Goal:
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
inst_2 : InnerProductSpace ℝ V₁
inst_3 : InnerProductSpace ℝ V₂
inst_4 : MetricSpace P₁
inst_5 : MetricSpace P₂
inst_6 : NormedAddTorsor V₁ P₁
inst_7 : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos : dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c') = dist a' b' * dist c' b' * 2 * Real.cos (∠ a b c)
h_cos' :
  HPow.hPow (β := ℕ) (dist a' c') 2 =
    HPow.hPow (β := ℕ) (dist a' b') 2 + HPow.hPow (β := ℕ) (dist c' b') 2 -
      dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
heq : ¬dist a' b' * dist c' b' * 2 = 0
⊢ Real.cos (∠ a' b' c') = Real.cos (∠ a b c)

Tactic:
rw [mul_right_inj' heq] at h_cos

Premises used: mul_right_inj'
-- Module: Mathlib.Geometry.Euclidean.Similarity
Goal:
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
inst_2 : InnerProductSpace ℝ V₁
inst_3 : InnerProductSpace ℝ V₂
inst_4 : MetricSpace P₁
inst_5 : MetricSpace P₂
inst_6 : NormedAddTorsor V₁ P₁
inst_7 : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos : dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c') = dist a' b' * dist c' b' * 2 * Real.cos (∠ a b c)
h_cos' :
  HPow.hPow (β := ℕ) (dist a' c') 2 =
    HPow.hPow (β := ℕ) (dist a' b') 2 + HPow.hPow (β := ℕ) (dist c' b') 2 -
      dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
heq : ¬dist a' b' * dist c' b' * 2 = 0
h_cos₁ : Real.cos (∠ a' b' c') = Real.cos (∠ a b c)
⊢ HPow.hPow (β := ℕ) (dist a' c') 2 =
    HPow.hPow (β := ℕ) (dist a' b') 2 + HPow.hPow (β := ℕ) (dist c' b') 2 -
      dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')

Tactic:
rw [mul_right_inj' heq] at h_cos

Premises used: mul_right_inj'
-- Module: Mathlib.Geometry.Euclidean.Similarity
Goal:
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
inst_2 : InnerProductSpace ℝ V₁
inst_3 : InnerProductSpace ℝ V₂
inst_4 : MetricSpace P₁
inst_5 : MetricSpace P₂
inst_6 : NormedAddTorsor V₁ P₁
inst_7 : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos : dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c') = dist a' b' * dist c' b' * 2 * Real.cos (∠ a b c)
h_cos' :
  HPow.hPow (β := ℕ) (dist a' c') 2 =
    HPow.hPow (β := ℕ) (dist a' b') 2 + HPow.hPow (β := ℕ) (dist c' b') 2 -
      dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
heq : ¬dist a' b' * dist c' b' * 2 = 0
h_cos₁ : Real.cos (∠ a' b' c') = Real.cos (∠ a b c)
h_cos'₁ :
  HPow.hPow (β := ℕ) (dist a' c') 2 =
    HPow.hPow (β := ℕ) (dist a' b') 2 + HPow.hPow (β := ℕ) (dist c' b') 2 -
      dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
⊢ ¬dist a' b' * dist c' b' * 2 = 0

Tactic:
rw [mul_right_inj' heq] at h_cos

Premises used: mul_right_inj'
-- Module: Mathlib.Geometry.Euclidean.Similarity
Goal:
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
inst_2 : InnerProductSpace ℝ V₁
inst_3 : InnerProductSpace ℝ V₂
inst_4 : MetricSpace P₁
inst_5 : MetricSpace P₂
inst_6 : NormedAddTorsor V₁ P₁
inst_7 : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos : Real.cos (∠ a' b' c') = Real.cos (∠ a b c)
h_cos' :
  HPow.hPow (β := ℕ) (dist a' c') 2 =
    HPow.hPow (β := ℕ) (dist a' b') 2 + HPow.hPow (β := ℕ) (dist c' b') 2 -
      dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
heq : ¬dist a' b' * dist c' b' * 2 = 0
neg : ∀ (h_cos : ∠ a' b' c' = ∠ a b c), ∠ a b c = ∠ a' b' c'
a₁ : ∠ a' b' c' ∈ Set.Icc 0 Real.pi
a₂ : ∠ a b c ∈ Set.Icc 0 Real.pi
⊢ ∠ a b c = ∠ a' b' c'

Tactic:
apply Real.injOn_cos at h_cos

Premises used: Real.injOn_cos
-- Module: Mathlib.Geometry.Euclidean.Similarity
Goal:
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
inst_2 : InnerProductSpace ℝ V₁
inst_3 : InnerProductSpace ℝ V₂
inst_4 : MetricSpace P₁
inst_5 : MetricSpace P₂
inst_6 : NormedAddTorsor V₁ P₁
inst_7 : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos' :
  HPow.hPow (β := ℕ) (dist a' c') 2 =
    HPow.hPow (β := ℕ) (dist a' b') 2 + HPow.hPow (β := ℕ) (dist c' b') 2 -
      dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
heq : ¬dist a' b' * dist c' b' * 2 = 0
h_cos : ∠ a' b' c' = ∠ a b c
⊢ ∠ a b c = ∠ a' b' c'

Tactic:
grind [angle_nonneg, angle_le_pi]

Premises used: EuclideanGeometry.angle_le_pi, EuclideanGeometry.angle_nonneg
-- Module: Mathlib.Geometry.Euclidean.Similarity
Goal:
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
inst_2 : InnerProductSpace ℝ V₁
inst_3 : InnerProductSpace ℝ V₂
inst_4 : MetricSpace P₁
inst_5 : MetricSpace P₂
inst_6 : NormedAddTorsor V₁ P₁
inst_7 : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos : Real.cos (∠ a' b' c') = Real.cos (∠ a b c)
h_cos' :
  HPow.hPow (β := ℕ) (dist a' c') 2 =
    HPow.hPow (β := ℕ) (dist a' b') 2 + HPow.hPow (β := ℕ) (dist c' b') 2 -
      dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
heq : ¬dist a' b' * dist c' b' * 2 = 0
⊢ ∠ a' b' c' ∈ Set.Icc 0 Real.pi

Tactic:
grind [angle_nonneg, angle_le_pi]

Premises used: EuclideanGeometry.angle_le_pi, EuclideanGeometry.angle_nonneg
-- Module: Mathlib.Geometry.Euclidean.Similarity
Goal:
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
inst_2 : InnerProductSpace ℝ V₁
inst_3 : InnerProductSpace ℝ V₂
inst_4 : MetricSpace P₁
inst_5 : MetricSpace P₂
inst_6 : NormedAddTorsor V₁ P₁
inst_7 : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos : Real.cos (∠ a' b' c') = Real.cos (∠ a b c)
h_cos' :
  HPow.hPow (β := ℕ) (dist a' c') 2 =
    HPow.hPow (β := ℕ) (dist a' b') 2 + HPow.hPow (β := ℕ) (dist c' b') 2 -
      dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
heq : ¬dist a' b' * dist c' b' * 2 = 0
⊢ ∠ a b c ∈ Set.Icc 0 Real.pi

Tactic:
grind [angle_nonneg, angle_le_pi]

Premises used: EuclideanGeometry.angle_le_pi, EuclideanGeometry.angle_nonneg
-- Module: Mathlib.Geometry.Euclidean.Similarity
Goal:
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
inst_2 : InnerProductSpace ℝ V₁
inst_3 : InnerProductSpace ℝ V₂
inst_4 : MetricSpace P₁
inst_5 : MetricSpace P₂
inst_6 : NormedAddTorsor V₁ P₁
inst_7 : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
r : ℝ
hr_pos : 0 < r
hdist :
  ∀ (i₁ i₂ : Fin (Nat.succ 0).succ.succ),
    dist (![a, b, c] i₁) (![a, b, c] i₂) = r * dist (![a', b', c'] i₁) (![a', b', c'] i₂)
h_ab : dist a b = r * dist a' b'
h_cb : dist c b = r * dist c' b'
h_ac : dist a c = r * dist a' c'
h_cos' :
  HPow.hPow (β := ℕ) (dist a' c') 2 =
    HPow.hPow (β := ℕ) (dist a' b') 2 + HPow.hPow (β := ℕ) (dist c' b') 2 -
      dist a' b' * dist c' b' * 2 * Real.cos (∠ a' b' c')
heq : ¬dist a' b' * dist c' b' * 2 = 0
h_cos : ∠ a' b' c' = ∠ a b c
⊢ ∠ a b c = ∠ a' b' c'

Tactic:
repeat grind [angle_nonneg, angle_le_pi]

Premises used: EuclideanGeometry.angle_le_pi, EuclideanGeometry.angle_nonneg
-- Module: Mathlib.Geometry.Euclidean.Similarity
Goal:
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
inst_2 : InnerProductSpace ℝ V₁
inst_3 : InnerProductSpace ℝ V₂
inst_4 : MetricSpace P₁
inst_5 : MetricSpace P₂
inst_6 : NormedAddTorsor V₁ P₁
inst_7 : NormedAddTorsor V₂ P₂
a b c : P₁
a' b' c' : P₂
h : ![a, b, c] ∼ ![a', b', c']
⊢ ∠ a b c = ∠ a' b' c' ∧ ∠ b c a = ∠ b' c' a' ∧ ∠ c a b = ∠ c' a' b'

Tactic:
⟨h.angle_eq, h.comm_left.comm_right.angle_eq, h.comm_right.comm_left.angle_eq⟩

Premises used: Similar.angle_eq, Similar.comm_right, And.intro, Similar.comm_left