awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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')
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 (∠ c' 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 (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}
h_bac' : ¬Collinear ℝ (P := P₂) {b', a', c'}
⊢ ![a, b, c] ≅ ![a', b', c']
have dist_ab_eq : dist a b = dist a' b'
Tactic: have dist_ab_eq : dist a b = dist a' b' := by
    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 (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'
ha₂ : ∠ b c a = ∠ b' c' a'
hd : dist c a = dist c' a'
⊢ ![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'
ha₂ : ∠ b c a = ∠ b' c' a'
hd : dist c a = dist c' a'
ha₃ : ∠ c a b + ∠ a b c + ∠ b c a = Real.pi
⊢ ![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'
ha₂ : ∠ b c a = ∠ b' c' a'
hd : dist c a = dist c' a'
ha₃ : ∠ c a b + ∠ a b c + ∠ b c a = Real.pi
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'
ha₂ : ∠ b c a = ∠ b' c' a'
hd : dist c a = dist c' a'
ha₃ : ∠ c a b + ∠ a b c + ∠ b c a = Real.pi
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 = ∠ 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 (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'
ha₂ : ∠ b c a = ∠ b' c' a'
hd : dist c a = dist 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'
⊢ ¬Collinear ℝ (P := P₁) {b, c, a}
have rwa : ∀ (h : ¬Collinear ℝ (P := P₁) {b, a, c}) (ha₁ : ∠ a b c = ∠ a' b' c') (ha₂ : ∠ b c a = ∠ b' c' a')
  (hd : dist c a = dist 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'), ¬Collinear ℝ (P := P₁) {b, c, a}
Tactic: rwa [Set.insert_comm, Set.pair_comm] at h
Cleared hypotheses: h, ha₁, ha₂, hd, h', ha₃', ha₃
-- 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'
ha₂ : ∠ b c a = ∠ b' c' a'
hd : dist c a = dist 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'
rwa :
  ∀ (h : ¬Collinear ℝ (P := P₁) {b, a, c}) (ha₁ : ∠ a b c = ∠ a' b' c') (ha₂ : ∠ b c a = ∠ b' c' a')
    (hd : dist c a = dist 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'),
    ¬Collinear ℝ (P := P₁) {b, c, a}
⊢ ¬Collinear ℝ (P := P₁) {b, c, a}
have rwa₁ : ∀ (h : ¬Collinear ℝ (P := P₁) {b, c, a}) (ha₁ : ∠ a b c = ∠ a' b' c') (ha₂ : ∠ b c a = ∠ b' c' a')
  (hd : dist c a = dist 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'), ¬Collinear ℝ (P := P₁) {b, c, a}
Tactic: rwa [Set.insert_comm, Set.pair_comm] at h
Cleared hypotheses: h, ha₁, ha₂, hd, h', ha₃', 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'
ha₂ : ∠ b c a = ∠ b' c' a'
hd : dist c a = dist 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_bca : ¬Collinear ℝ (P := P₁) {b, c, a}
Tactic: have h_bca : ¬Collinear ℝ {b, c, a} := by rwa [Set.insert_comm, Set.pair_comm] at 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'
ha₂ : ∠ b c a = ∠ b' c' a'
hd : dist c a = dist 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_bca : ¬Collinear ℝ (P := P₁) {b, c, a}
⊢ ![a, b, c] ≅ ![a', b', c']
have h1 : ![b, c, a] ≅ ![b', c', a']
Tactic: have h1 := angle_side_angle h_bca ha₂ hd ha₃
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Congruence (goal)
Goal:
ι : Type u_1
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₂
v₁ : ι → P₁
v₂ : ι → P₂
h : v₁ ≅ v₂
i j k : ι
⊢ Real.arccos (inner ℝ (v₁ i -ᵥ v₁ j) (v₁ k -ᵥ v₁ j) / (‖v₁ i -ᵥ v₁ j‖ * ‖v₁ k -ᵥ v₁ j‖)) =
    Real.arccos (inner ℝ (v₂ i -ᵥ v₂ j) (v₂ k -ᵥ v₂ j) / (‖v₂ i -ᵥ v₂ j‖ * ‖v₂ k -ᵥ v₂ j‖))
have simp_rw : Real.arccos
    ((‖v₁ i -ᵥ v₁ j‖ * ‖v₁ i -ᵥ v₁ j‖ + ‖v₁ k -ᵥ v₁ j‖ * ‖v₁ k -ᵥ v₁ j‖ -
          ‖v₁ i -ᵥ v₁ j - (v₁ k -ᵥ v₁ j)‖ * ‖v₁ i -ᵥ v₁ j - (v₁ k -ᵥ v₁ j)‖) /
        2 /
      (‖v₁ i -ᵥ v₁ j‖ * ‖v₁ k -ᵥ v₁ j‖)) =
  Real.arccos
    ((‖v₂ i -ᵥ v₂ j‖ * ‖v₂ i -ᵥ v₂ j‖ + ‖v₂ k -ᵥ v₂ j‖ * ‖v₂ k -ᵥ v₂ j‖ -
          ‖v₂ i -ᵥ v₂ j - (v₂ k -ᵥ v₂ j)‖ * ‖v₂ i -ᵥ v₂ j - (v₂ k -ᵥ v₂ j)‖) /
        2 /
      (‖v₂ i -ᵥ v₂ j‖ * ‖v₂ k -ᵥ v₂ j‖))
Tactic: simp_rw [real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two,
    vsub_sub_vsub_cancel_right, ← dist_eq_norm_vsub, h.dist_eq]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Congruence (goal)
Goal:
ι : Type u_1
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₂
v₁ : ι → P₁
v₂ : ι → P₂
h : v₁ ≅ v₂
i j k : ι
simp_rw :
  Real.arccos
      ((‖v₁ i -ᵥ v₁ j‖ * ‖v₁ i -ᵥ v₁ j‖ + ‖v₁ k -ᵥ v₁ j‖ * ‖v₁ k -ᵥ v₁ j‖ -
            ‖v₁ i -ᵥ v₁ j - (v₁ k -ᵥ v₁ j)‖ * ‖v₁ i -ᵥ v₁ j - (v₁ k -ᵥ v₁ j)‖) /
          2 /
        (‖v₁ i -ᵥ v₁ j‖ * ‖v₁ k -ᵥ v₁ j‖)) =
    Real.arccos
      ((‖v₂ i -ᵥ v₂ j‖ * ‖v₂ i -ᵥ v₂ j‖ + ‖v₂ k -ᵥ v₂ j‖ * ‖v₂ k -ᵥ v₂ j‖ -
            ‖v₂ i -ᵥ v₂ j - (v₂ k -ᵥ v₂ j)‖ * ‖v₂ i -ᵥ v₂ j - (v₂ k -ᵥ v₂ j)‖) /
          2 /
        (‖v₂ i -ᵥ v₂ j‖ * ‖v₂ k -ᵥ v₂ j‖))
⊢ Real.arccos (inner ℝ (v₁ i -ᵥ v₁ j) (v₁ k -ᵥ v₁ j) / (‖v₁ i -ᵥ v₁ j‖ * ‖v₁ k -ᵥ v₁ j‖)) =
    Real.arccos (inner ℝ (v₂ i -ᵥ v₂ j) (v₂ k -ᵥ v₂ j) / (‖v₂ i -ᵥ v₂ j‖ * ‖v₂ k -ᵥ v₂ j‖))
have simp_rw₁ : Real.arccos
    ((‖v₁ i -ᵥ v₁ j‖ * ‖v₁ i -ᵥ v₁ j‖ + ‖v₁ k -ᵥ v₁ j‖ * ‖v₁ k -ᵥ v₁ j‖ - ‖v₁ i -ᵥ v₁ k‖ * ‖v₁ i -ᵥ v₁ k‖) / 2 /
      (‖v₁ i -ᵥ v₁ j‖ * ‖v₁ k -ᵥ v₁ j‖)) =
  Real.arccos
    ((‖v₂ i -ᵥ v₂ j‖ * ‖v₂ i -ᵥ v₂ j‖ + ‖v₂ k -ᵥ v₂ j‖ * ‖v₂ k -ᵥ v₂ j‖ - ‖v₂ i -ᵥ v₂ k‖ * ‖v₂ i -ᵥ v₂ k‖) / 2 /
      (‖v₂ i -ᵥ v₂ j‖ * ‖v₂ k -ᵥ v₂ j‖))
Tactic: simp_rw [real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two,
    vsub_sub_vsub_cancel_right, ← dist_eq_norm_vsub, h.dist_eq]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Congruence (goal)
Goal:
ι : Type u_1
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₂
v₁ : ι → P₁
v₂ : ι → P₂
h : v₁ ≅ v₂
i j k : ι
simp_rw :
  Real.arccos
      ((‖v₁ i -ᵥ v₁ j‖ * ‖v₁ i -ᵥ v₁ j‖ + ‖v₁ k -ᵥ v₁ j‖ * ‖v₁ k -ᵥ v₁ j‖ -
            ‖v₁ i -ᵥ v₁ j - (v₁ k -ᵥ v₁ j)‖ * ‖v₁ i -ᵥ v₁ j - (v₁ k -ᵥ v₁ j)‖) /
          2 /
        (‖v₁ i -ᵥ v₁ j‖ * ‖v₁ k -ᵥ v₁ j‖)) =
    Real.arccos
      ((‖v₂ i -ᵥ v₂ j‖ * ‖v₂ i -ᵥ v₂ j‖ + ‖v₂ k -ᵥ v₂ j‖ * ‖v₂ k -ᵥ v₂ j‖ -
            ‖v₂ i -ᵥ v₂ j - (v₂ k -ᵥ v₂ j)‖ * ‖v₂ i -ᵥ v₂ j - (v₂ k -ᵥ v₂ j)‖) /
          2 /
        (‖v₂ i -ᵥ v₂ j‖ * ‖v₂ k -ᵥ v₂ j‖))
simp_rw₁ :
  Real.arccos
      ((‖v₁ i -ᵥ v₁ j‖ * ‖v₁ i -ᵥ v₁ j‖ + ‖v₁ k -ᵥ v₁ j‖ * ‖v₁ k -ᵥ v₁ j‖ - ‖v₁ i -ᵥ v₁ k‖ * ‖v₁ i -ᵥ v₁ k‖) / 2 /
        (‖v₁ i -ᵥ v₁ j‖ * ‖v₁ k -ᵥ v₁ j‖)) =
    Real.arccos
      ((‖v₂ i -ᵥ v₂ j‖ * ‖v₂ i -ᵥ v₂ j‖ + ‖v₂ k -ᵥ v₂ j‖ * ‖v₂ k -ᵥ v₂ j‖ - ‖v₂ i -ᵥ v₂ k‖ * ‖v₂ i -ᵥ v₂ k‖) / 2 /
        (‖v₂ i -ᵥ v₂ j‖ * ‖v₂ k -ᵥ v₂ j‖))
⊢ Real.arccos (inner ℝ (v₁ i -ᵥ v₁ j) (v₁ k -ᵥ v₁ j) / (‖v₁ i -ᵥ v₁ j‖ * ‖v₁ k -ᵥ v₁ j‖)) =
    Real.arccos (inner ℝ (v₂ i -ᵥ v₂ j) (v₂ k -ᵥ v₂ j) / (‖v₂ i -ᵥ v₂ j‖ * ‖v₂ k -ᵥ v₂ j‖))
have simp_rw₂ : Real.arccos
    ((dist (v₁ i) (v₁ j) * dist (v₁ i) (v₁ j) + dist (v₁ k) (v₁ j) * dist (v₁ k) (v₁ j) -
          dist (v₁ i) (v₁ k) * dist (v₁ i) (v₁ k)) /
        2 /
      (dist (v₁ i) (v₁ j) * dist (v₁ k) (v₁ j))) =
  Real.arccos
    ((dist (v₂ i) (v₂ j) * dist (v₂ i) (v₂ j) + dist (v₂ k) (v₂ j) * dist (v₂ k) (v₂ j) -
          dist (v₂ i) (v₂ k) * dist (v₂ i) (v₂ k)) /
        2 /
      (dist (v₂ i) (v₂ j) * dist (v₂ k) (v₂ j)))
Tactic: simp_rw [real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two,
    vsub_sub_vsub_cancel_right, ← dist_eq_norm_vsub, h.dist_eq]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
m n : ℕ
inst_4 : NeZero m
inst_5 : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
signs : Finset (Fin (m + 1))
⊢ (s.reindex e).excenterWeightsUnnorm signs =
    s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs) ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))
have h : ∀ (i : Fin (m + 1)),
  (s.reindex e).excenterWeightsUnnorm signs i =
    (s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs) ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
inst_8 : NeZero n
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
⊢ (s.map f.toAffineMap ⋯).excenterWeightsUnnorm = s.excenterWeightsUnnorm
have h : ∀ (x : Finset (Fin (n + 1))) (x_1 : Fin (n + 1)),
  (s.map f.toAffineMap sorry).excenterWeightsUnnorm x x_1 = s.excenterWeightsUnnorm x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
⊢ excenterWeightsUnnorm.{u_1, u_2} (P := ↥S) (s.restrict S hS) = s.excenterWeightsUnnorm
have h : ∀ (x : Finset (Fin (n + 1))) (x_1 : Fin (n + 1)),
  excenterWeightsUnnorm.{u_1, u_2} (P := ↥S) (s.restrict S hS) x x_1 = s.excenterWeightsUnnorm x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
i : Fin (n + 1)
⊢ (if i ∈ signs then -1 else 1) * (s.height i)⁻¹ ≠ 0
have refine_1 : Ne (α := ℝ) (if i ∈ signs then -1 else 1) 0
Tactic: refine mul_ne_zero ?_ ?_
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
i : Fin (n + 1)
refine_1 : Ne (α := ℝ) (if i ∈ signs then -1 else 1) 0
⊢ (if i ∈ signs then -1 else 1) * (s.height i)⁻¹ ≠ 0
have refine_2 : (s.height i)⁻¹ ≠ 0
Tactic: refine mul_ne_zero ?_ ?_
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
m n : ℕ
inst_4 : NeZero m
inst_5 : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
signs : Finset (Fin (m + 1))
⊢ (s.reindex e).ExcenterExists signs ↔ s.ExcenterExists (Finset.map e.symm.toEmbedding signs)
have simp_rw : Ne (α := ℝ) (∑ i : Fin (m + 1), (s.reindex e).excenterWeightsUnnorm signs i) 0 ↔
  Ne (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs) i) 0
Tactic: simp_rw [ExcenterExists, excenterWeightsUnnorm_reindex, Finset.sum_comp_equiv,
    Finset.map_univ_equiv]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
m n : ℕ
inst_4 : NeZero m
inst_5 : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
signs : Finset (Fin (m + 1))
simp_rw :
  Ne (α := ℝ) (∑ i : Fin (m + 1), (s.reindex e).excenterWeightsUnnorm signs i) 0 ↔
    Ne (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs) i) 0
⊢ (s.reindex e).ExcenterExists signs ↔ s.ExcenterExists (Finset.map e.symm.toEmbedding signs)
have simp_rw₁ : Ne (α := ℝ)
    (∑ x : Fin (m + 1),
      (s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs) ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) x)
    0 ↔
  Ne (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs) i) 0
Tactic: simp_rw [ExcenterExists, excenterWeightsUnnorm_reindex, Finset.sum_comp_equiv,
    Finset.map_univ_equiv]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
m n : ℕ
inst_4 : NeZero m
inst_5 : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
signs : Finset (Fin (m + 1))
simp_rw :
  Ne (α := ℝ) (∑ i : Fin (m + 1), (s.reindex e).excenterWeightsUnnorm signs i) 0 ↔
    Ne (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs) i) 0
simp_rw₁ :
  Ne (α := ℝ)
      (∑ x : Fin (m + 1),
        (s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs) ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) x)
      0 ↔
    Ne (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs) i) 0
⊢ (s.reindex e).ExcenterExists signs ↔ s.ExcenterExists (Finset.map e.symm.toEmbedding signs)
have simp_rw₂ : (Finset.map e.symm.toEmbedding Finset.univ).sum (s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs)) ≠ 0 ↔
  Ne (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs) i) 0
Tactic: simp_rw [ExcenterExists, excenterWeightsUnnorm_reindex, Finset.sum_comp_equiv,
    Finset.map_univ_equiv]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
inst_8 : NeZero n
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
⊢ (s.map f.toAffineMap ⋯).ExcenterExists = s.ExcenterExists
have h : ∀ (x : Finset (Fin (n + 1))), (s.map f.toAffineMap sorry).ExcenterExists x ↔ s.ExcenterExists x
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
⊢ ExcenterExists.{u_1, u_2} (P := ↥S) (s.restrict S hS) = s.ExcenterExists
have h : ∀ (x : Finset (Fin (n + 1))), ExcenterExists.{u_1, u_2} (P := ↥S) (s.restrict S hS) x ↔ s.ExcenterExists x
Tactic: ext
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Incenter (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
m n : ℕ
inst_4 : NeZero m
inst_5 : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
signs : Finset (Fin (m + 1))
⊢ (s.reindex e).excenterWeights signs =
    s.excenterWeights (Finset.map e.symm.toEmbedding signs) ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))
have simp_rw : HSMul.hSMul (α := ℝ) (∑ i : Fin (m + 1), (s.reindex e).excenterWeightsUnnorm signs i)⁻¹
    ((s.reindex e).excenterWeightsUnnorm signs) =
  HSMul.hSMul (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs) i)⁻¹
      (s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs)) ∘
    (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))
Tactic: simp_rw [excenterWeights, excenterWeightsUnnorm_reindex, Finset.sum_comp_equiv,
    Finset.map_univ_equiv, Pi.smul_comp]