awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (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
s : Simplex ℝ P 1
j : Fin 2
hj : Membership.mem (γ := Set (Fin 2)) Set.univ j
hi : Membership.mem (γ := Set (Fin 2)) Set.univ ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
hij : (fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ ‖HSMul.hSMul (α := ℝ) 1 (s.points ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) -ᵥ s.points 0) -
        HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖ =
    ‖HSMul.hSMul (α := ℝ) 1 (s.points j -ᵥ s.points 0) - HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖
have 0 : ∀ (hj : Membership.mem (γ := Set (Fin 2)) Set.univ ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩))
  (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)),
  ‖HSMul.hSMul (α := ℝ) 1 (s.points ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) -ᵥ s.points 0) -
        HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖ =
    ‖HSMul.hSMul (α := ℝ) 1 (s.points ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) -ᵥ s.points 0) -
        HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖
Tactic: fin_cases j
Cleared hypotheses: j, hj, hij
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (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
s : Simplex ℝ P 1
j : Fin 2
hj : Membership.mem (γ := Set (Fin 2)) Set.univ j
hi : Membership.mem (γ := Set (Fin 2)) Set.univ ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
hij : (fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩ ≠ j
0 :
  ∀ (hj : Membership.mem (γ := Set (Fin 2)) Set.univ ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩))
    (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)),
    ‖HSMul.hSMul (α := ℝ) 1 (s.points ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) -ᵥ s.points 0) -
          HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖ =
      ‖HSMul.hSMul (α := ℝ) 1 (s.points ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) -ᵥ s.points 0) -
          HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖
⊢ ‖HSMul.hSMul (α := ℝ) 1 (s.points ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) -ᵥ s.points 0) -
        HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖ =
    ‖HSMul.hSMul (α := ℝ) 1 (s.points j -ᵥ s.points 0) - HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖
have 0₁ : ∀ (hj : Membership.mem (γ := Set (Fin 2)) Set.univ ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩))
  (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)),
  ‖HSMul.hSMul (α := ℝ) 1 (s.points ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) -ᵥ s.points 0) -
        HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖ =
    ‖HSMul.hSMul (α := ℝ) 1 (s.points ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) -ᵥ s.points 0) -
        HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖
Tactic: fin_cases j
Cleared hypotheses: j, hj, hij
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (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
s : Simplex ℝ P 1
j : Fin 2
hj : Membership.mem (γ := Set (Fin 2)) Set.univ j
hi : Membership.mem (γ := Set (Fin 2)) Set.univ ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
hij : (fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ ‖HSMul.hSMul (α := ℝ) 1 (s.points ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) -ᵥ s.points 0) -
        HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖ =
    ‖HSMul.hSMul (α := ℝ) 1 (s.points j -ᵥ s.points 0) - HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖
have 1 : ∀ (hj : Membership.mem (γ := Set (Fin 2)) Set.univ ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩))
  (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)),
  ‖HSMul.hSMul (α := ℝ) 1 (s.points ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) -ᵥ s.points 0) -
        HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖ =
    ‖HSMul.hSMul (α := ℝ) 1 (s.points ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)) -ᵥ s.points 0) -
        HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖
Tactic: fin_cases j
Cleared hypotheses: j, hj, hij
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (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
s : Simplex ℝ P 1
j : Fin 2
hj : Membership.mem (γ := Set (Fin 2)) Set.univ j
hi : Membership.mem (γ := Set (Fin 2)) Set.univ ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
hij : (fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩ ≠ j
1 :
  ∀ (hj : Membership.mem (γ := Set (Fin 2)) Set.univ ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩))
    (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)),
    ‖HSMul.hSMul (α := ℝ) 1 (s.points ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) -ᵥ s.points 0) -
          HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖ =
      ‖HSMul.hSMul (α := ℝ) 1 (s.points ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) -ᵥ s.points 0) -
          HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖
⊢ ‖HSMul.hSMul (α := ℝ) 1 (s.points ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) -ᵥ s.points 0) -
        HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖ =
    ‖HSMul.hSMul (α := ℝ) 1 (s.points j -ᵥ s.points 0) - HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖
have 1₁ : ∀ (hj : Membership.mem (γ := Set (Fin 2)) Set.univ ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩))
  (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)),
  ‖HSMul.hSMul (α := ℝ) 1 (s.points ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) -ᵥ s.points 0) -
        HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖ =
    ‖HSMul.hSMul (α := ℝ) 1 (s.points ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)) -ᵥ s.points 0) -
        HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖
Tactic: fin_cases j
Cleared hypotheses: j, hj, hij
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (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
s : Simplex ℝ P 1
hi : Membership.mem (γ := Set (Fin 2)) Set.univ ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
hj : Membership.mem (γ := Set (Fin 2)) Set.univ ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ ‖HSMul.hSMul (α := ℝ) 1 (s.points ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) -ᵥ s.points 0) -
        HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖ =
    ‖HSMul.hSMul (α := ℝ) 1 (s.points ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) -ᵥ s.points 0) -
        HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖
have 0 : ‖HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖ = ‖HSub.hSub (α := ℝ) 1 2⁻¹ • (s.points 1 -ᵥ s.points 0)‖
Tactic: simp [-one_smul, ← sub_smul]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (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
s : Simplex ℝ P 1
hi : Membership.mem (γ := Set (Fin 2)) Set.univ ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
hj : Membership.mem (γ := Set (Fin 2)) Set.univ ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
⊢ ‖HSMul.hSMul (α := ℝ) 1 (s.points ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) -ᵥ s.points 0) -
        HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖ =
    ‖HSMul.hSMul (α := ℝ) 1 (s.points ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) -ᵥ s.points 0) -
        HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖
have 1 : ‖HSub.hSub (α := ℝ) 1 2⁻¹ • (s.points 1 -ᵥ s.points 0)‖ = ‖HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖
Tactic: simp [-one_smul, ← sub_smul]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (hypothesis)
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
s : Simplex ℝ P 1
⊢ s.circumcenter = Finset.centroid ℝ univ s.points
have hr : Set.Pairwise Set.univ fun (i j : Fin 2) ↦
  dist (s.points i) (Finset.centroid ℝ univ s.points) = dist (s.points j) (Finset.centroid ℝ univ s.points)
Tactic: have hr :
    Set.Pairwise Set.univ fun i j : Fin 2 =>
      dist (s.points i) (Finset.univ.centroid ℝ s.points) =
        dist (s.points j) (Finset.univ.centroid ℝ s.points) := by
    intro i hi j hj hij
    rw [Finset.centroid_pair_fin, dist_eq_norm_vsub V (s.points i),
      dist_eq_norm_vsub V (s.points j), vsub_vadd_eq_vsub_sub, vsub_vadd_eq_vsub_sub, ←
      one_smul ℝ (s.points i -ᵥ s.points 0), ← one_smul ℝ (s.points j -ᵥ s.points 0)]
    fin_cases i <;> fin_cases j <;> simp [-one_smul, ← sub_smul] <;> norm_num
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (hypothesis)
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
s : Simplex ℝ P 1
hr :
  Set.Pairwise Set.univ fun (i j : Fin 2) ↦
    dist (s.points i) (Finset.centroid ℝ univ s.points) = dist (s.points j) (Finset.centroid ℝ univ s.points)
⊢ s.circumcenter = Finset.centroid ℝ univ s.points
have hr₁ : ∃ (z : ℝ),
  ∀ (x : Fin 2), Membership.mem (γ := Set (Fin 2)) Set.univ x → dist (s.points x) (Finset.centroid ℝ univ s.points) = z
Tactic: rw [Set.pairwise_eq_iff_exists_eq] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (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
s : Simplex ℝ P 1
hr :
  ∃ (z : ℝ),
    ∀ (x : Fin 2),
      Membership.mem (γ := Set (Fin 2)) Set.univ x → dist (s.points x) (Finset.centroid ℝ univ s.points) = z
⊢ s.circumcenter = Finset.centroid ℝ univ s.points
have obtain : ∀ (r : ℝ)
  (hr :
    ∀ (x : Fin 2),
      Membership.mem (γ := Set (Fin 2)) Set.univ x → dist (s.points x) (Finset.centroid ℝ univ s.points) = r),
  s.circumcenter = Finset.centroid ℝ univ s.points
Tactic: obtain ⟨r, hr⟩ := hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (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 : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ (s.reindex e).circumsphere = s.circumsphere
have refine_1 : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) (s.reindex e).circumsphere.center
Tactic: refine s.circumsphere_unique_dist_eq.2 _ ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (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 : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
refine_1 :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) (s.reindex e).circumsphere.center
⊢ (s.reindex e).circumsphere = s.circumsphere
have refine_2 : Set.range s.points ⊆ Metric.sphere (s.reindex e).circumsphere.center (s.reindex e).circumsphere.radius
Tactic: refine s.circumsphere_unique_dist_eq.2 _ ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (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 : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) (s.reindex e).circumsphere.center
have refine_1 : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.reindex e).points))
  (s.reindex e).circumsphere.center
Tactic: rw [← s.reindex_range_points e]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (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 : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ Set.range s.points ⊆ Metric.sphere (s.reindex e).circumsphere.center (s.reindex e).circumsphere.radius
have refine_2 : Set.range (s.reindex e).points ⊆ Metric.sphere (s.reindex e).circumsphere.center (s.reindex e).circumsphere.radius
Tactic: rw [← s.reindex_range_points e]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (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 : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
⊢ (s.map f.toAffineMap ⋯).circumcenter = (f : (a : P) → P₂) s.circumcenter
have rw : (f : (a : P) → P₂) s.circumcenter = (s.map f.toAffineMap sorry).circumcenter
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (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 : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
⊢ (f : (a : P) → P₂) s.circumcenter = (s.map f.toAffineMap ⋯).circumcenter
have refine : Membership.mem (α := P₂) (γ := AffineSubspace ℝ P₂) (affineSpan ℝ (Set.range (s.map f.toAffineMap sorry).points))
  ((f : (a : P) → P₂) s.circumcenter : P₂)
Tactic: refine (s.map f.toAffineMap f.injective).eq_circumcenter_of_dist_eq (r := s.circumradius) ?_
    fun i ↦ by simp
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (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 : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
⊢ Membership.mem (α := P₂) (γ := AffineSubspace ℝ P₂) (affineSpan ℝ (Set.range (s.map f.toAffineMap ⋯).points))
    ((f : (a : P) → P₂) s.circumcenter : P₂)
have rw : Membership.mem (α := P₂) (AffineSubspace.map f.toAffineMap (affineSpan ℝ (Set.range s.points)))
  ((f : (a : P) → P₂) s.circumcenter : P₂)
Tactic: rw [map_points, Set.range_comp, ← AffineSubspace.map_span]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (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 : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
⊢ (s.map f.toAffineMap ⋯).circumradius = s.circumradius
have rw : s.circumradius = (s.map f.toAffineMap sorry).circumradius
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (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 : ℕ
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
⊢ s.circumradius = (s.map f.toAffineMap ⋯).circumradius
have refine : Membership.mem (α := P₂) (γ := AffineSubspace ℝ P₂) (affineSpan ℝ (Set.range (s.map f.toAffineMap sorry).points))
  ((f : (a : P) → P₂) s.circumcenter : P₂)
Tactic: refine (s.map f.toAffineMap f.injective).eq_circumradius_of_dist_eq (p := f s.circumcenter) ?_
    fun i ↦ by simp
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (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 : ℕ
s : Simplex ℝ P n
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
⊢ (↑((s.restrict S hS).circumcenter (n := n)) : P) = s.circumcenter
have rw : s.circumcenter = (↑((s.restrict S hS).circumcenter (n := n)) : P)
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (hypothesis)
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 : ℕ
s : Simplex ℝ P n
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
⊢ s.circumcenter = (↑((s.restrict S hS).circumcenter (n := n)) : P)
have this : Nonempty.{u_2 + 1} ↥S
Tactic: have : Nonempty S := Nonempty.map (AffineSubspace.inclusion hS) inferInstance
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (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 : ℕ
s : Simplex ℝ P n
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
⊢ circumradius.{u_1, u_2} (P := ↥S) (n := n) (s.restrict S hS) = s.circumradius
have rw : s.circumradius = circumradius.{u_1, u_2} (P := ↥S) (n := n) (s.restrict S hS)
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (hypothesis)
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 : ℕ
s : Simplex ℝ P n
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
⊢ s.circumradius = circumradius.{u_1, u_2} (P := ↥S) (n := n) (s.restrict S hS)
have this : Nonempty.{u_2 + 1} ↥S
Tactic: have : Nonempty S := Nonempty.map (AffineSubspace.inclusion hS) inferInstance
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (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 : ℕ
r : ℝ
s : Simplex ℝ P n
p₁ : P
h₁ : ∀ (i : Fin (n + 1)), dist (s.points i) p₁ = r
h₁' : (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P) = s.circumcenter
h : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) (s.points 0)
⊢ dist p₁ s.circumcenter * dist p₁ s.circumcenter = r * r - s.circumradius * s.circumradius
have rw : dist s.circumcenter p₁ * dist s.circumcenter p₁ =
  dist (s.points 0) (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P) *
        dist (s.points 0) (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P) +
      dist p₁ (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P) *
        dist p₁ (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p₁) : P) -
    s.circumradius * s.circumradius
Tactic: rw [dist_comm, ← h₁ 0,
    s.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq p₁ h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (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 : ℕ
s : Simplex ℝ P n
p : P
hr : ∃ (r : ℝ), ∀ (i : Fin (n + 1)), (fun (x : P) ↦ dist x p = r) (s.points i)
⊢ ∃ (r : ℝ), ∀ (a : P), Membership.mem (γ := Set P) (Set.range fun (i : Fin (n + 1)) ↦ s.points i) a → dist a p = r
have obtain : ∀ (r : ℝ) (hr : ∀ (i : Fin (n + 1)), (fun (x : P) ↦ dist x p = r) (s.points i)),
  ∃ (r : ℝ), ∀ (a : P), Membership.mem (γ := Set P) (Set.range fun (i : Fin (n + 1)) ↦ s.points i) a → dist a p = r
Tactic: obtain ⟨r, hr⟩ := hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (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 : ℕ
s : Simplex ℝ P n
p : P
r : ℝ
hr : ∀ (i : Fin (n + 1)), (fun (x : P) ↦ dist x p = r) (s.points i)
⊢ ∃ (r : ℝ), ∀ (a : P), Membership.mem (γ := Set P) (Set.range fun (i : Fin (n + 1)) ↦ s.points i) a → dist a p = r
have h : ∀ (a : P), Membership.mem (γ := Set P) (Set.range fun (i : Fin (n + 1)) ↦ s.points i) a → dist a p = r
Tactic: use r
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (hypothesis)
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 : ℕ
s : Simplex ℝ P n
p : P
hr : ∃ (r : ℝ), ∀ (i : Fin (n + 1)), (fun (x : P) ↦ dist x p = r) (s.points i)
⊢ (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p) : P) = s.circumcenter
have hr₁ : ∃ (r : ℝ), ∀ (a : P), Membership.mem (γ := Set P) (Set.range fun (i : Fin (n + 1)) ↦ s.points i) a → dist a p = r
Tactic: have hr : ∃ (r : ℝ), ∀ (a : P),
      a ∈ Set.range (fun (i : Fin (n + 1)) => s.points i) → dist a p = r := by
    obtain ⟨r, hr⟩ := hr
    use r
    refine Set.forall_mem_range.mpr ?_
    exact hr
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (hypothesis)
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 : ℕ
s : Simplex ℝ P n
p : P
hr_1 : ∃ (r : ℝ), ∀ (i : Fin (n + 1)), (fun (x : P) ↦ dist x p = r) (s.points i)
hr : ∃ (r : ℝ), ∀ (a : P), Membership.mem (γ := Set P) (Set.range fun (i : Fin (n + 1)) ↦ s.points i) a → dist a p = r
⊢ (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p) : P) = s.circumcenter
have hr₁ : ∃ (r : ℝ),
  ∀ (p₁ : P),
    Membership.mem (γ := Set P) (Set.range fun (i : Fin (n + 1)) ↦ s.points i) p₁ →
      dist p₁
          (↑((orthogonalProjection (affineSpan ℝ (Set.range fun (i : Fin (n + 1)) ↦ s.points i)) :
                  (a : P) → ↥(affineSpan ℝ (Set.range fun (i : Fin (n + 1)) ↦ s.points i)))
                p) :
            P) =
        r
Tactic: rw [exists_dist_eq_iff_exists_dist_orthogonalProjection_eq (subset_affineSpan ℝ _) p] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (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 : ℕ
s : Simplex ℝ P n
p : P
hr_1 : ∃ (r : ℝ), ∀ (i : Fin (n + 1)), (fun (x : P) ↦ dist x p = r) (s.points i)
hr :
  ∃ (r : ℝ),
    ∀ (p₁ : P),
      Membership.mem (γ := Set P) (Set.range fun (i : Fin (n + 1)) ↦ s.points i) p₁ →
        dist p₁
            (↑((orthogonalProjection (affineSpan ℝ (Set.range fun (i : Fin (n + 1)) ↦ s.points i)) :
                    (a : P) → ↥(affineSpan ℝ (Set.range fun (i : Fin (n + 1)) ↦ s.points i)))
                  p) :
              P) =
          r
⊢ (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p) : P) = s.circumcenter
have obtain : ∀ (r : ℝ)
  (hr :
    ∀ (p₁ : P),
      Membership.mem (γ := Set P) (Set.range fun (i : Fin (n + 1)) ↦ s.points i) p₁ →
        dist p₁
            (↑((orthogonalProjection (affineSpan ℝ (Set.range fun (i : Fin (n + 1)) ↦ s.points i)) :
                    (a : P) → ↥(affineSpan ℝ (Set.range fun (i : Fin (n + 1)) ↦ s.points i)))
                  p) :
              P) =
          r),
  (↑((s.orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range s.points))) p) : P) = s.circumcenter
Tactic: obtain ⟨r, hr⟩ := hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Circumcenter (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 : ℕ
s : Simplex ℝ P n
fs : Finset (Fin (n + 1))
m : ℕ
h : #fs = m + 1
⊢ ∃ (r : ℝ), ∀ (i : Fin (m + 1)), dist ((s.face h).points i) s.circumcenter = r
have h₁ : ∀ (i : Fin (m + 1)), dist ((s.face h).points i) s.circumcenter = s.circumradius
Tactic: use s.circumradius