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₂
h_not_col : ¬Collinear ℝ (P := P₁) {a, b, c}
h_not_col' : ¬Collinear ℝ (P := P₂) {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' :
  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_ac_pos : 0 < dist a c
k_dist_a'c' : 0 ≤ k * dist a' c'
hij :
  Ne (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩)
⊢ dist a c = k * dist a' c'

Tactic:
grind [dist_comm]

Premises used: dist_comm
-- 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_not_col : ¬Collinear ℝ (P := P₁) {a, b, c}
h_not_col' : ¬Collinear ℝ (P := P₂) {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' :
  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_ac_pos : 0 < dist a c
k_dist_a'c' : 0 ≤ k * dist a' c'
hij :
  Ne (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
h₁ : dist b a = k * dist b' a'
⊢ dist (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))
      (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ))) =
    k *
      dist (![a', b', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))
        (![a', b', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))

Tactic:
simp
-- 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_not_col : ¬Collinear ℝ (P := P₁) {a, b, c}
h_not_col' : ¬Collinear ℝ (P := P₂) {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' :
  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_ac_pos : 0 < dist a c
k_dist_a'c' : 0 ≤ k * dist a' c'
hij :
  Ne (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
⊢ dist b a = k * dist b' a'

Tactic:
grind [dist_comm]

Premises used: dist_comm
-- 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_not_col : ¬Collinear ℝ (P := P₁) {a, b, c}
h_not_col' : ¬Collinear ℝ (P := P₂) {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' :
  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_ac_pos : 0 < dist a c
k_dist_a'c' : 0 ≤ k * dist a' c'
hij :
  Ne (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩)
h₁ : dist b c = k * dist b' c'
⊢ dist (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))
      (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : Fin (Nat.succ 0).succ.succ))) =
    k *
      dist (![a', b', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))
        (![a', b', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))

Tactic:
simp
-- 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_not_col : ¬Collinear ℝ (P := P₁) {a, b, c}
h_not_col' : ¬Collinear ℝ (P := P₂) {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' :
  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_ac_pos : 0 < dist a c
k_dist_a'c' : 0 ≤ k * dist a' c'
hij :
  Ne (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩)
⊢ dist b c = k * dist b' c'

Tactic:
grind [dist_comm]

Premises used: dist_comm
-- 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_not_col : ¬Collinear ℝ (P := P₁) {a, b, c}
h_not_col' : ¬Collinear ℝ (P := P₂) {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' :
  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_ac_pos : 0 < dist a c
k_dist_a'c' : 0 ≤ k * dist a' c'
hij :
  Ne (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
h₁ : dist c a = k * dist c' a'
⊢ dist (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))
      (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ))) =
    k *
      dist (![a', b', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))
        (![a', b', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))

Tactic:
simp
-- 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_not_col : ¬Collinear ℝ (P := P₁) {a, b, c}
h_not_col' : ¬Collinear ℝ (P := P₂) {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' :
  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_ac_pos : 0 < dist a c
k_dist_a'c' : 0 ≤ k * dist a' c'
hij :
  Ne (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨0, ⋯⟩)
⊢ dist c a = k * dist c' a'

Tactic:
grind [dist_comm]

Premises used: dist_comm
-- 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_not_col : ¬Collinear ℝ (P := P₁) {a, b, c}
h_not_col' : ¬Collinear ℝ (P := P₂) {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' :
  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_ac_pos : 0 < dist a c
k_dist_a'c' : 0 ≤ k * dist a' c'
hij :
  Ne (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
h₁ : dist c b = k * dist c' b'
⊢ dist (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))
      (![a, b, c] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ))) =
    k *
      dist (![a', b', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨2, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))
        (![a', b', c'] ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 0).succ.succ)))

Tactic:
simp
-- 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_not_col : ¬Collinear ℝ (P := P₁) {a, b, c}
h_not_col' : ¬Collinear ℝ (P := P₂) {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' :
  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_ac_pos : 0 < dist a c
k_dist_a'c' : 0 ≤ k * dist a' c'
hij :
  Ne (α := Fin (Nat.succ 0).succ.succ) ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨2, ⋯⟩)
    ((fun (i : Fin (Nat.succ 0).succ.succ) ↦ i) ⟨1, ⋯⟩)
⊢ dist c b = k * dist c' b'

Tactic:
grind [dist_comm]

Premises used: dist_comm
-- 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']
⊢ ∃ (r : ℝ),
    0 < r ∧
      ∀ (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₂)

Tactic:
rw [similar_iff_exists_pos_dist_eq] at h

Premises used: similar_iff_exists_pos_dist_eq
-- 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 :
  ∃ (r : ℝ),
    0 < r ∧
      ∀ (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₂)
rcases :
  ∀ (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₂)),
    ∠ a b c = ∠ a' b' c'
⊢ ∠ a b c = ∠ a' b' c'

Tactic:
rcases h with ⟨r, hr_pos, hdist⟩
-- 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₂)
⊢ dist a b = r * dist a' b'

Tactic:
have h_ab : dist a b = r * dist a' b' := hdist 0 1
-- 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'
⊢ dist c b = r * dist c' b'

Tactic:
have h_cb : dist c b = r * dist c' b' := hdist 2 1
-- 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'
⊢ dist a c = r * dist a' c'

Tactic:
have h_ac : dist a c = r * dist a' c' := hdist 0 2
-- 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'
⊢ dist a c * dist a c = dist a b * dist a b + dist c b * dist c b - 2 * dist a b * dist c b * Real.cos (∠ a b c)

Tactic:
have h_cos := law_cos a b c
-- 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 c * dist a c = dist a b * dist a b + dist c b * dist c b - 2 * dist a b * dist c b * Real.cos (∠ a b c)
⊢ r * dist a' c' * (r * dist a' c') =
    r * dist a' b' * (r * dist a' b') + r * dist c' b' * (r * dist c' b') -
      2 * (r * dist a' b') * (r * dist c' b') * Real.cos (∠ a b c)

Tactic:
rw [h_ab, h_cb, h_ac] at h_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 :
  r * dist a' c' * (r * dist a' c') =
    r * dist a' b' * (r * dist a' b') + r * dist c' b' * (r * dist c' b') -
      2 * (r * dist a' b') * (r * dist c' b') * 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:
field_simp at h_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)
⊢ dist a' c' * dist a' c' =
    dist a' b' * dist a' b' + dist c' b' * dist c' b' - 2 * dist a' b' * dist c' b' * Real.cos (∠ a' b' c')

Tactic:
have h_cos' := law_cos a' b' c'
-- 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)
h_cos' :
  dist a' c' * dist a' c' =
    dist a' b' * dist a' b' + dist c' b' * dist c' b' - 2 * dist a' b' * dist c' b' * 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:
field_simp at h_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)
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 * Real.cos (∠ a' b' c') = dist a' b' * dist c' b' * 2 * Real.cos (∠ a b c)

Tactic:
rw [h_cos', sub_right_inj] at h_cos

Premises used: sub_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 :
  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)
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')
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)
⊢ 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 [h_cos', sub_right_inj] at h_cos

Premises used: sub_right_inj