awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Congruence (hypothesis)
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 : ¬Collinear ℝ (P := P₁) {a, b, c}
ha₁ : ∠ a b c = ∠ a' b' c'
hd : dist b c = dist b' c'
ha₂ : ∠ b c a = ∠ b' c' a'
⊢ ![a, b, c] ≅ ![a', b', c']
have h' : ¬Collinear ℝ (P := P₂) {a', b', c'}
Tactic: have h' : ¬Collinear ℝ {a', b', c'} := by
    grind only [collinear_iff_eq_or_eq_or_angle_eq_zero_or_angle_eq_pi, angle_self_right,
      angle_self_left, dist_eq_zero, Set.insert_comm, Set.pair_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Congruence (hypothesis)
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 : ¬Collinear ℝ (P := P₁) {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 ℝ (P := P₂) {a', b', c'}
⊢ ![a, b, c] ≅ ![a', b', c']
have ha₃ : ∠ c a b + ∠ a b c + ∠ b c a = Real.pi
Tactic: have ha₃ := angle_add_angle_add_angle_eq_pi b (ne₁₃_of_not_collinear h)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Congruence (hypothesis)
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 : ¬Collinear ℝ (P := P₁) {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 ℝ (P := P₂) {a', b', c'}
ha₃ : ∠ c a b + ∠ a b c + ∠ b c a = Real.pi
⊢ ![a, b, c] ≅ ![a', b', c']
have ha₃' : ∠ c' a' b' + ∠ a' b' c' + ∠ b' c' a' = Real.pi
Tactic: have ha₃' := angle_add_angle_add_angle_eq_pi b' (ne₁₃_of_not_collinear h')
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Congruence (hypothesis)
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 : ¬Collinear ℝ (P := P₁) {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 ℝ (P := P₂) {a', b', c'}
ha₃ : ∠ c a b + ∠ a b c + ∠ b c a = Real.pi
ha₃' : ∠ c' a' b' + ∠ a' b' c' + ∠ b' c' a' = Real.pi
⊢ ![a, b, c] ≅ ![a', b', c']
have ha₄ : ∠ c a b = ∠ c' a' b'
Tactic: simp only [← ha₃', ha₁, ha₂, angle_comm b' c' a', add_right_cancel_iff] at ha₃
Cleared hypotheses: ha₃
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Congruence (hypothesis)
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 : ¬Collinear ℝ (P := P₁) {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 ℝ (P := P₂) {a', b', c'}
ha₃' : ∠ c' a' b' + ∠ a' b' c' + ∠ b' c' a' = Real.pi
ha₃ : ∠ c a b = ∠ c' a' b'
⊢ ![a, b, c] ≅ ![a', b', c']
have h_bac : ¬Collinear ℝ (P := P₁) {b, a, c}
Tactic: have h_bac : ¬Collinear ℝ {b, a, c} := by simpa [Set.insert_comm] using h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Congruence (hypothesis)
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 : ¬Collinear ℝ (P := P₁) {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 ℝ (P := P₂) {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 ℝ (P := P₁) {b, a, c}
⊢ ![a, b, c] ≅ ![a', b', c']
have h_bac' : ¬Collinear ℝ (P := P₂) {b', a', c'}
Tactic: have h_bac' : ¬Collinear ℝ {b', a', c'} := by simpa [Set.insert_comm] using h'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Congruence (goal)
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 : ¬Collinear ℝ (P := P₁) {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 ℝ (P := P₂) {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 ℝ (P := P₁) {b, a, c}
h_bac' : ¬Collinear ℝ (P := P₂) {b', a', c'}
⊢ dist a b = dist a' b'
have rw : dist b a = dist a' b'
Tactic: rw [dist_comm a b, dist_comm a' b', dist_eq_dist_mul_sin_angle_div_sin_angle h_bac,
      dist_eq_dist_mul_sin_angle_div_sin_angle h_bac', dist_comm c b, dist_comm c' b', hd,
      angle_comm, ha₂, angle_comm b' c' a', angle_comm b a c, ha₃, angle_comm b' a' c']
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Congruence (goal)
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 : ¬Collinear ℝ (P := P₁) {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 ℝ (P := P₂) {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 ℝ (P := P₁) {b, a, c}
h_bac' : ¬Collinear ℝ (P := P₂) {b', a', c'}
rw : dist b a = dist a' b'
⊢ dist a b = dist a' b'
have rw₁ : dist b a = dist b' a'
Tactic: rw [dist_comm a b, dist_comm a' b', dist_eq_dist_mul_sin_angle_div_sin_angle h_bac,
      dist_eq_dist_mul_sin_angle_div_sin_angle h_bac', dist_comm c b, dist_comm c' b', hd,
      angle_comm, ha₂, angle_comm b' c' a', angle_comm b a c, ha₃, angle_comm b' a' c']
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Congruence (goal)
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 : ¬Collinear ℝ (P := P₁) {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 ℝ (P := P₂) {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 ℝ (P := P₁) {b, a, c}
h_bac' : ¬Collinear ℝ (P := P₂) {b', a', c'}
rw : dist b a = dist a' b'
rw₁ : dist b a = dist b' a'
⊢ dist a b = dist a' b'
have rw₂ : dist c b * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist b' a'
Tactic: rw [dist_comm a b, dist_comm a' b', dist_eq_dist_mul_sin_angle_div_sin_angle h_bac,
      dist_eq_dist_mul_sin_angle_div_sin_angle h_bac', dist_comm c b, dist_comm c' b', hd,
      angle_comm, ha₂, angle_comm b' c' a', angle_comm b a c, ha₃, angle_comm b' a' c']
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Congruence (goal)
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 : ¬Collinear ℝ (P := P₁) {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 ℝ (P := P₂) {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 ℝ (P := P₁) {b, a, c}
h_bac' : ¬Collinear ℝ (P := P₂) {b', a', c'}
rw : dist b a = dist a' b'
rw₁ : dist b a = dist b' a'
rw₂ : dist c b * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist b' a'
⊢ dist a b = dist a' b'
have rw₃ : dist c b * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist c' b' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
Tactic: rw [dist_comm a b, dist_comm a' b', dist_eq_dist_mul_sin_angle_div_sin_angle h_bac,
      dist_eq_dist_mul_sin_angle_div_sin_angle h_bac', dist_comm c b, dist_comm c' b', hd,
      angle_comm, ha₂, angle_comm b' c' a', angle_comm b a c, ha₃, angle_comm b' a' c']
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Congruence (goal)
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 : ¬Collinear ℝ (P := P₁) {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 ℝ (P := P₂) {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 ℝ (P := P₁) {b, a, c}
h_bac' : ¬Collinear ℝ (P := P₂) {b', a', c'}
rw : dist b a = dist a' b'
rw₁ : dist b a = dist b' a'
rw₂ : dist c b * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist b' a'
rw₃ : dist c b * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist c' b' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
⊢ dist a b = dist a' b'
have rw₄ : dist b c * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist c' b' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
Tactic: rw [dist_comm a b, dist_comm a' b', dist_eq_dist_mul_sin_angle_div_sin_angle h_bac,
      dist_eq_dist_mul_sin_angle_div_sin_angle h_bac', dist_comm c b, dist_comm c' b', hd,
      angle_comm, ha₂, angle_comm b' c' a', angle_comm b a c, ha₃, angle_comm b' a' c']
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Congruence (goal)
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 : ¬Collinear ℝ (P := P₁) {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 ℝ (P := P₂) {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 ℝ (P := P₁) {b, a, c}
h_bac' : ¬Collinear ℝ (P := P₂) {b', a', c'}
rw : dist b a = dist a' b'
rw₁ : dist b a = dist b' a'
rw₂ : dist c b * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist b' a'
rw₃ : dist c b * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist c' b' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
rw₄ : dist b c * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist c' b' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
⊢ dist a b = dist a' b'
have rw₅ : dist b c * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
Tactic: rw [dist_comm a b, dist_comm a' b', dist_eq_dist_mul_sin_angle_div_sin_angle h_bac,
      dist_eq_dist_mul_sin_angle_div_sin_angle h_bac', dist_comm c b, dist_comm c' b', hd,
      angle_comm, ha₂, angle_comm b' c' a', angle_comm b a c, ha₃, angle_comm b' a' c']
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Congruence (goal)
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 : ¬Collinear ℝ (P := P₁) {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 ℝ (P := P₂) {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 ℝ (P := P₁) {b, a, c}
h_bac' : ¬Collinear ℝ (P := P₂) {b', a', c'}
rw : dist b a = dist a' b'
rw₁ : dist b a = dist b' a'
rw₂ : dist c b * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist b' a'
rw₃ : dist c b * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist c' b' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
rw₄ : dist b c * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist c' b' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
rw₅ : dist b c * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
⊢ dist a b = dist a' b'
have rw₆ : dist b' c' * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
Tactic: rw [dist_comm a b, dist_comm a' b', dist_eq_dist_mul_sin_angle_div_sin_angle h_bac,
      dist_eq_dist_mul_sin_angle_div_sin_angle h_bac', dist_comm c b, dist_comm c' b', hd,
      angle_comm, ha₂, angle_comm b' c' a', angle_comm b a c, ha₃, angle_comm b' a' c']
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Congruence (goal)
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 : ¬Collinear ℝ (P := P₁) {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 ℝ (P := P₂) {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 ℝ (P := P₁) {b, a, c}
h_bac' : ¬Collinear ℝ (P := P₂) {b', a', c'}
rw : dist b a = dist a' b'
rw₁ : dist b a = dist b' a'
rw₂ : dist c b * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist b' a'
rw₃ : dist c b * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist c' b' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
rw₄ : dist b c * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist c' b' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
rw₅ : dist b c * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
rw₆ : dist b' c' * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
⊢ dist a b = dist a' b'
have rw₇ : dist b' c' * Real.sin (∠ b c a) / Real.sin (∠ b a c) = dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
Tactic: rw [dist_comm a b, dist_comm a' b', dist_eq_dist_mul_sin_angle_div_sin_angle h_bac,
      dist_eq_dist_mul_sin_angle_div_sin_angle h_bac', dist_comm c b, dist_comm c' b', hd,
      angle_comm, ha₂, angle_comm b' c' a', angle_comm b a c, ha₃, angle_comm b' a' c']
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Congruence (goal)
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 : ¬Collinear ℝ (P := P₁) {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 ℝ (P := P₂) {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 ℝ (P := P₁) {b, a, c}
h_bac' : ¬Collinear ℝ (P := P₂) {b', a', c'}
rw : dist b a = dist a' b'
rw₁ : dist b a = dist b' a'
rw₂ : dist c b * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist b' a'
rw₃ : dist c b * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist c' b' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
rw₄ : dist b c * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist c' b' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
rw₅ : dist b c * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
rw₆ : dist b' c' * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
rw₇ : dist b' c' * Real.sin (∠ b c a) / Real.sin (∠ b a c) = dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
⊢ dist a b = dist a' b'
have rw₈ : dist b' c' * Real.sin (∠ b' c' a') / Real.sin (∠ b a c) = dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
Tactic: rw [dist_comm a b, dist_comm a' b', dist_eq_dist_mul_sin_angle_div_sin_angle h_bac,
      dist_eq_dist_mul_sin_angle_div_sin_angle h_bac', dist_comm c b, dist_comm c' b', hd,
      angle_comm, ha₂, angle_comm b' c' a', angle_comm b a c, ha₃, angle_comm b' a' c']
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Congruence (goal)
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 : ¬Collinear ℝ (P := P₁) {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 ℝ (P := P₂) {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 ℝ (P := P₁) {b, a, c}
h_bac' : ¬Collinear ℝ (P := P₂) {b', a', c'}
rw : dist b a = dist a' b'
rw₁ : dist b a = dist b' a'
rw₂ : dist c b * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist b' a'
rw₃ : dist c b * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist c' b' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
rw₄ : dist b c * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist c' b' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
rw₅ : dist b c * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
rw₆ : dist b' c' * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
rw₇ : dist b' c' * Real.sin (∠ b c a) / Real.sin (∠ b a c) = dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
rw₈ :
  dist b' c' * Real.sin (∠ b' c' a') / Real.sin (∠ b a c) = dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
⊢ dist a b = dist a' b'
have rw₉ : dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b a c) = dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
Tactic: rw [dist_comm a b, dist_comm a' b', dist_eq_dist_mul_sin_angle_div_sin_angle h_bac,
      dist_eq_dist_mul_sin_angle_div_sin_angle h_bac', dist_comm c b, dist_comm c' b', hd,
      angle_comm, ha₂, angle_comm b' c' a', angle_comm b a c, ha₃, angle_comm b' a' c']
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Congruence (goal)
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 : ¬Collinear ℝ (P := P₁) {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 ℝ (P := P₂) {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 ℝ (P := P₁) {b, a, c}
h_bac' : ¬Collinear ℝ (P := P₂) {b', a', c'}
rw : dist b a = dist a' b'
rw₁ : dist b a = dist b' a'
rw₂ : dist c b * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist b' a'
rw₃ : dist c b * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist c' b' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
rw₄ : dist b c * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist c' b' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
rw₅ : dist b c * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
rw₆ : dist b' c' * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
rw₇ : dist b' c' * Real.sin (∠ b c a) / Real.sin (∠ b a c) = dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
rw₈ :
  dist b' c' * Real.sin (∠ b' c' a') / Real.sin (∠ b a c) = dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
rw₉ :
  dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b a c) = dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
⊢ dist a b = dist a' b'
have rw₁₀ : dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ c a b) = dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
Tactic: rw [dist_comm a b, dist_comm a' b', dist_eq_dist_mul_sin_angle_div_sin_angle h_bac,
      dist_eq_dist_mul_sin_angle_div_sin_angle h_bac', dist_comm c b, dist_comm c' b', hd,
      angle_comm, ha₂, angle_comm b' c' a', angle_comm b a c, ha₃, angle_comm b' a' c']
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Congruence (goal)
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 : ¬Collinear ℝ (P := P₁) {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 ℝ (P := P₂) {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 ℝ (P := P₁) {b, a, c}
h_bac' : ¬Collinear ℝ (P := P₂) {b', a', c'}
rw : dist b a = dist a' b'
rw₁ : dist b a = dist b' a'
rw₂ : dist c b * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist b' a'
rw₃ : dist c b * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist c' b' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
rw₄ : dist b c * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist c' b' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
rw₅ : dist b c * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
rw₆ : dist b' c' * Real.sin (∠ a c b) / Real.sin (∠ b a c) = dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
rw₇ : dist b' c' * Real.sin (∠ b c a) / Real.sin (∠ b a c) = dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
rw₈ :
  dist b' c' * Real.sin (∠ b' c' a') / Real.sin (∠ b a c) = dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
rw₉ :
  dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b a c) = dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
rw₁₀ :
  dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ c a b) = dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
⊢ dist a b = dist a' b'
have rw₁₁ : dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ c' a' b') = dist b' c' * Real.sin (∠ a' c' b') / Real.sin (∠ b' a' c')
Tactic: rw [dist_comm a b, dist_comm a' b', dist_eq_dist_mul_sin_angle_div_sin_angle h_bac,
      dist_eq_dist_mul_sin_angle_div_sin_angle h_bac', dist_comm c b, dist_comm c' b', hd,
      angle_comm, ha₂, angle_comm b' c' a', angle_comm b a c, ha₃, angle_comm b' a' c']