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
ι : Type u_3
hne : Nonempty ι
inst_4 : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
val : Fintype ι
m : ℕ
hm :
  ∀ {ι : Type u_3} [hne : Nonempty ι] [Finite ι] {p : ι → P} (ha : AffineIndependent ℝ p) (val : Fintype ι)
    (hn : Fintype.card ι = m + 1),
    ∃! cs : Sphere P,
      Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
        Set.range p ⊆ Metric.sphere cs.center cs.radius
hn : Fintype.card ι = m + 1 + 1
i : ι
ι2 : Type (max 0 u_3) := { x : ι // x ≠ i }
⊢ ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
      Set.range p ⊆ Metric.sphere cs.center cs.radius
have have : Fintype.card ι2 = m + 1
Tactic: classical
      have hc : Fintype.card ι2 = m + 1 := by
        rw [Fintype.card_of_subtype {x | x ≠ i}]
        · rw [Finset.filter_not, Finset.filter_eq' _ i, if_pos (Finset.mem_univ _),
            Finset.card_sdiff, Finset.card_univ, hn]
          simp
        · simp
      haveI : Nonempty ι2 := Fintype.card_pos_iff.1 (hc.symm ▸ Nat.zero_lt_succ _)
      have ha2 : AffineIndependent ℝ fun i2 : ι2 => p i2 := ha.subtype _
      replace hm := hm ha2 _ hc
      have hr : Set.range p = insert (p i) (Set.range fun i2 : ι2 => p i2) := by
        change _ = insert _ (Set.range fun i2 : { x | x ≠ i } => p i2)
        rw [← Set.image_eq_range, ← Set.image_univ, ← Set.image_insert_eq]
        congr with j
        simp [Classical.em]
      rw [hr, ← affineSpan_insert_affineSpan]
      refine existsUnique_dist_eq_of_insert (Set.range_nonempty _) (subset_affineSpan ℝ _) ?_ hm
      convert! ha.notMem_affineSpan_diff i Set.univ
      change (Set.range fun i2 : { x | x ≠ i } => p i2) = _
      rw [← Set.image_eq_range]
      congr 1 with j
      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
ι : Type u_3
hne : Nonempty ι
inst_4 : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
val : Fintype ι
m : ℕ
hm :
  ∀ {ι : Type u_3} [hne : Nonempty ι] [Finite ι] {p : ι → P} (ha : AffineIndependent ℝ p) (val : Fintype ι)
    (hn : Fintype.card ι = m + 1),
    ∃! cs : Sphere P,
      Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
        Set.range p ⊆ Metric.sphere cs.center cs.radius
hn : Fintype.card ι = m + 1 + 1
i : ι
ι2 : Type (max 0 u_3) := { x : ι // x ≠ i }
have : Fintype.card ι2 = m + 1
⊢ ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
      Set.range p ⊆ Metric.sphere cs.center cs.radius
have intro : ∀ (hc : Fintype.card ι2 = m + 1),
  ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
      Set.range p ⊆ Metric.sphere cs.center cs.radius
Tactic: classical
      have hc : Fintype.card ι2 = m + 1 := by
        rw [Fintype.card_of_subtype {x | x ≠ i}]
        · rw [Finset.filter_not, Finset.filter_eq' _ i, if_pos (Finset.mem_univ _),
            Finset.card_sdiff, Finset.card_univ, hn]
          simp
        · simp
      haveI : Nonempty ι2 := Fintype.card_pos_iff.1 (hc.symm ▸ Nat.zero_lt_succ _)
      have ha2 : AffineIndependent ℝ fun i2 : ι2 => p i2 := ha.subtype _
      replace hm := hm ha2 _ hc
      have hr : Set.range p = insert (p i) (Set.range fun i2 : ι2 => p i2) := by
        change _ = insert _ (Set.range fun i2 : { x | x ≠ i } => p i2)
        rw [← Set.image_eq_range, ← Set.image_univ, ← Set.image_insert_eq]
        congr with j
        simp [Classical.em]
      rw [hr, ← affineSpan_insert_affineSpan]
      refine existsUnique_dist_eq_of_insert (Set.range_nonempty _) (subset_affineSpan ℝ _) ?_ hm
      convert! ha.notMem_affineSpan_diff i Set.univ
      change (Set.range fun i2 : { x | x ≠ i } => p i2) = _
      rw [← Set.image_eq_range]
      congr 1 with j
      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
ι : Type u_3
hne : Nonempty ι
inst_4 : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
val : Fintype ι
m : ℕ
hm :
  ∀ {ι : Type u_3} [hne : Nonempty ι] [Finite ι] {p : ι → P} (ha : AffineIndependent ℝ p) (val : Fintype ι)
    (hn : Fintype.card ι = m + 1),
    ∃! cs : Sphere P,
      Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
        Set.range p ⊆ Metric.sphere cs.center cs.radius
hn : Fintype.card ι = m + 1 + 1
i : ι
ι2 : Type (max 0 u_3) := { x : ι // x ≠ i }
have : Fintype.card ι2 = m + 1
intro :
  ∀ (hc : Fintype.card ι2 = m + 1),
    ∃! cs : Sphere P,
      Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
        Set.range p ⊆ Metric.sphere cs.center cs.radius
have₁ : Fintype.card ι2 = m + 1
intro₁ intro₂ :
  ∀ (hc : Fintype.card ι2 = m + 1),
    ∃! cs : Sphere P,
      Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
        Set.range p ⊆ Metric.sphere cs.center cs.radius
⊢ ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
      Set.range p ⊆ Metric.sphere cs.center cs.radius
have intro₃ : ∀ (hc : Fintype.card ι2 = m + 1) (this : Nonempty ι2),
  ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
      Set.range p ⊆ Metric.sphere cs.center cs.radius
Tactic: classical
      have hc : Fintype.card ι2 = m + 1 := by
        rw [Fintype.card_of_subtype {x | x ≠ i}]
        · rw [Finset.filter_not, Finset.filter_eq' _ i, if_pos (Finset.mem_univ _),
            Finset.card_sdiff, Finset.card_univ, hn]
          simp
        · simp
      haveI : Nonempty ι2 := Fintype.card_pos_iff.1 (hc.symm ▸ Nat.zero_lt_succ _)
      have ha2 : AffineIndependent ℝ fun i2 : ι2 => p i2 := ha.subtype _
      replace hm := hm ha2 _ hc
      have hr : Set.range p = insert (p i) (Set.range fun i2 : ι2 => p i2) := by
        change _ = insert _ (Set.range fun i2 : { x | x ≠ i } => p i2)
        rw [← Set.image_eq_range, ← Set.image_univ, ← Set.image_insert_eq]
        congr with j
        simp [Classical.em]
      rw [hr, ← affineSpan_insert_affineSpan]
      refine existsUnique_dist_eq_of_insert (Set.range_nonempty _) (subset_affineSpan ℝ _) ?_ hm
      convert! ha.notMem_affineSpan_diff i Set.univ
      change (Set.range fun i2 : { x | x ≠ i } => p i2) = _
      rw [← Set.image_eq_range]
      congr 1 with j
      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
ι : Type u_3
hne : Nonempty ι
inst_4 : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
val : Fintype ι
m : ℕ
hm :
  ∀ {ι : Type u_3} [hne : Nonempty ι] [Finite ι] {p : ι → P} (ha : AffineIndependent ℝ p) (val : Fintype ι)
    (hn : Fintype.card ι = m + 1),
    ∃! cs : Sphere P,
      Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
        Set.range p ⊆ Metric.sphere cs.center cs.radius
hn : Fintype.card ι = m + 1 + 1
i : ι
ι2 : Type (max 0 u_3) := { x : ι // x ≠ i }
have : Fintype.card ι2 = m + 1
intro :
  ∀ (hc : Fintype.card ι2 = m + 1),
    ∃! cs : Sphere P,
      Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
        Set.range p ⊆ Metric.sphere cs.center cs.radius
have₁ : Fintype.card ι2 = m + 1
intro₁ intro₂ :
  ∀ (hc : Fintype.card ι2 = m + 1),
    ∃! cs : Sphere P,
      Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
        Set.range p ⊆ Metric.sphere cs.center cs.radius
intro₃ :
  ∀ (hc : Fintype.card ι2 = m + 1) (this : Nonempty ι2),
    ∃! cs : Sphere P,
      Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
        Set.range p ⊆ Metric.sphere cs.center cs.radius
⊢ ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
      Set.range p ⊆ Metric.sphere cs.center cs.radius
have intro₄ : ∀ (hc : Fintype.card ι2 = m + 1) (this : Nonempty ι2)
  (ha2 : AffineIndependent.{0, u_1, u_2, u_3} ℝ (P := P) fun (i2 : ι2) ↦ p (↑i2 : ι)),
  ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
      Set.range p ⊆ Metric.sphere cs.center cs.radius
Tactic: classical
      have hc : Fintype.card ι2 = m + 1 := by
        rw [Fintype.card_of_subtype {x | x ≠ i}]
        · rw [Finset.filter_not, Finset.filter_eq' _ i, if_pos (Finset.mem_univ _),
            Finset.card_sdiff, Finset.card_univ, hn]
          simp
        · simp
      haveI : Nonempty ι2 := Fintype.card_pos_iff.1 (hc.symm ▸ Nat.zero_lt_succ _)
      have ha2 : AffineIndependent ℝ fun i2 : ι2 => p i2 := ha.subtype _
      replace hm := hm ha2 _ hc
      have hr : Set.range p = insert (p i) (Set.range fun i2 : ι2 => p i2) := by
        change _ = insert _ (Set.range fun i2 : { x | x ≠ i } => p i2)
        rw [← Set.image_eq_range, ← Set.image_univ, ← Set.image_insert_eq]
        congr with j
        simp [Classical.em]
      rw [hr, ← affineSpan_insert_affineSpan]
      refine existsUnique_dist_eq_of_insert (Set.range_nonempty _) (subset_affineSpan ℝ _) ?_ hm
      convert! ha.notMem_affineSpan_diff i Set.univ
      change (Set.range fun i2 : { x | x ≠ i } => p i2) = _
      rw [← Set.image_eq_range]
      congr 1 with j
      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
ι : Type u_3
hne : Nonempty ι
inst_4 : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
val : Fintype ι
⊢ ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
      Set.range p ⊆ Metric.sphere cs.center cs.radius
have intro : ∀ (x : ℕ) (hn : Fintype.card ι = x),
  ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
      Set.range p ⊆ Metric.sphere cs.center cs.radius
Tactic: induction hn : Fintype.card ι generalizing ι with
  | zero =>
    exfalso
    have h := Fintype.card_pos_iff.2 hne
    lia
  | succ m hm =>
    rcases m with - | m
    · rw [Fintype.card_eq_one_iff] at hn
      obtain ⟨i, hi⟩ := hn
      haveI : Unique ι := ⟨⟨i⟩, hi⟩
      use ⟨p i, 0⟩
      simp only [Set.range_unique, AffineSubspace.mem_affineSpan_singleton]
      constructor
      · simp_rw [hi default, Set.singleton_subset_iff]
        exact ⟨⟨⟩, by simp only [Metric.sphere_zero, Set.mem_singleton_iff]⟩
      · rintro ⟨cc, cr⟩
        rintro ⟨rfl, hdist⟩
        replace hdist : 0 = cr := by simpa using hdist
        rw [hi default, hdist]
    · have i := hne.some
      let ι2 := { x // x ≠ i }
      classical
      have hc : Fintype.card ι2 = m + 1 := by
        rw [Fintype.card_of_subtype {x | x ≠ i}]
        · rw [Finset.filter_not, Finset.filter_eq' _ i, if_pos (Finset.mem_univ _),
            Finset.card_sdiff, Finset.card_univ, hn]
          simp
        · simp
      haveI : Nonempty ι2 := Fintype.card_pos_iff.1 (hc.symm ▸ Nat.zero_lt_succ _)
      have ha2 : AffineIndependent ℝ fun i2 : ι2 => p i2 := ha.subtype _
      replace hm := hm ha2 _ hc
      have hr : Set.range p = insert (p i) (Set.range fun i2 : ι2 => p i2) := by
        change _ = insert _ (Set.range fun i2 : { x | x ≠ i } => p i2)
        rw [← Set.image_eq_range, ← Set.image_univ, ← Set.image_insert_eq]
        congr with j
        simp [Classical.em]
      rw [hr, ← affineSpan_insert_affineSpan]
      refine existsUnique_dist_eq_of_insert (Set.range_nonempty _) (subset_affineSpan ℝ _) ?_ hm
      convert! ha.notMem_affineSpan_diff i Set.univ
      change (Set.range fun i2 : { x | x ≠ i } => p i2) = _
      rw [← Set.image_eq_range]
      congr 1 with j
      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
i : Fin (n + 1)
⊢ dist s.circumcenter (s.points i) = s.circumradius
have rw : dist (s.points i) s.circumcenter = s.circumradius
Tactic: rw [dist_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
p : P
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p
r : ℝ
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p = r
⊢ p = s.circumcenter
have h : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
      (Sphere.center { center := p, radius := r : Sphere P }) ∧
    Set.range s.points ⊆
      Metric.sphere (Sphere.center { center := p, radius := r }) (Sphere.radius { center := p, radius := r }) →
  { center := p, radius := r } = s.circumsphere
Tactic: have h := s.circumsphere_unique_dist_eq.2 ⟨p, 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
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p
r : ℝ
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p = r
h :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
        (Sphere.center { center := p, radius := r : Sphere P }) ∧
      Set.range s.points ⊆
        Metric.sphere (Sphere.center { center := p, radius := r }) (Sphere.radius { center := p, radius := r }) →
    { center := p, radius := r } = s.circumsphere
⊢ p = s.circumcenter
have h₁ : p = s.circumsphere.center ∧ r = s.circumsphere.radius
Tactic: simp only [hp, hr, forall_const, subset_sphere (s := ⟨p, r⟩), Sphere.ext_iff,
    Set.forall_mem_range, mem_sphere, true_and] at h
Cleared hypotheses: h
-- 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
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p
r : ℝ
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p = r
⊢ r = s.circumradius
have h : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
      (Sphere.center { center := p, radius := r : Sphere P }) ∧
    Set.range s.points ⊆
      Metric.sphere (Sphere.center { center := p, radius := r }) (Sphere.radius { center := p, radius := r }) →
  { center := p, radius := r } = s.circumsphere
Tactic: have h := s.circumsphere_unique_dist_eq.2 ⟨p, 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
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) p
r : ℝ
hr : ∀ (i : Fin (n + 1)), dist (s.points i) p = r
h :
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
        (Sphere.center { center := p, radius := r : Sphere P }) ∧
      Set.range s.points ⊆
        Metric.sphere (Sphere.center { center := p, radius := r }) (Sphere.radius { center := p, radius := r }) →
    { center := p, radius := r } = s.circumsphere
⊢ r = s.circumradius
have h₁ : p = s.circumsphere.center ∧ r = s.circumsphere.radius
Tactic: simp only [hp, hr, forall_const, subset_sphere (s := ⟨p, r⟩), Sphere.ext_iff,
    Set.forall_mem_range, mem_sphere, true_and] at h
Cleared hypotheses: 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 + 1)
⊢ 0 < s.circumradius
have refine : 0 ≠ s.circumradius
Tactic: refine lt_of_le_of_ne s.circumradius_nonneg ?_
-- 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 + 1)
h : 0 = s.circumradius
⊢ False
have hr : ∀ (i : Fin (n + 1 + 1)), dist (s.points i) s.circumcenter = s.circumradius
Tactic: have hr := s.dist_circumcenter_eq_circumradius
-- 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 + 1)
h : 0 = s.circumradius
hr : ∀ (i : Fin (n + 1 + 1)), dist (s.points i) s.circumcenter = s.circumradius
⊢ False
have hr₁ : ∀ (i : Fin (n + 1 + 1)), s.points i = s.circumcenter
Tactic: simp_rw [← h, dist_eq_zero] at hr
Cleared hypotheses: 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 + 1)
h : 0 = s.circumradius
hr : ∀ (i : Fin (n + 1 + 1)), s.points i = s.circumcenter
⊢ False
have h01 : s.points 0 ≠ s.points 1
Tactic: have h01 := s.independent.injective.ne (by simp : (0 : Fin (n + 2)) ≠ 1)
-- 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 0
i : Fin 1
⊢ s.circumcenter = s.points i
have h : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) s.circumcenter
Tactic: have h := s.circumcenter_mem_affineSpan
-- 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 0
i : Fin 1
h : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) s.circumcenter
⊢ s.circumcenter = s.points i
have have : ∀ (this : Unique (Fin 1)), s.circumcenter = s.points i
Tactic: have : Unique (Fin 1) := ⟨⟨0, by decide⟩, fun a => by simp only [Fin.eq_zero]⟩
-- 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 0
i : Fin 1
h : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points)) s.circumcenter
this : Unique (Fin 1)
⊢ s.circumcenter = s.points i
have h₁ : s.circumcenter = s.points default
Tactic: simp only [Set.range_unique, AffineSubspace.mem_affineSpan_singleton] at h
Cleared hypotheses: 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
s : Simplex ℝ P 0
i : Fin 1
this : Unique (Fin 1)
h : s.circumcenter = s.points default
⊢ s.circumcenter = s.points i
have rw : s.points default = s.points i
Tactic: rw [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
s : Simplex ℝ P 0
i : Fin 1
this : Unique (Fin 1)
h : s.circumcenter = s.points default
⊢ s.points default = s.points i
have e_a : default = i
Tactic: congr
-- 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 + 1)
i : Fin (n + 2)
⊢ s.circumcenter ≠ s.points i
have rw : s.circumradius ≠ 0
Tactic: rw [← dist_ne_zero, dist_circumcenter_eq_circumradius']
-- 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
i : Fin 2
hi : Membership.mem (γ := Set (Fin 2)) Set.univ i
j : Fin 2
hj : Membership.mem (γ := Set (Fin 2)) Set.univ j
hij : i ≠ j
⊢ dist (s.points i) (Finset.centroid ℝ univ s.points) = dist (s.points j) (Finset.centroid ℝ univ s.points)
have rw : ‖HSMul.hSMul (α := ℝ) 1 (s.points i -ᵥ 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)‖
Tactic: 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)]
-- 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
i : Fin 2
hi : Membership.mem (γ := Set (Fin 2)) Set.univ i
j : Fin 2
hj : Membership.mem (γ := Set (Fin 2)) Set.univ j
hij : i ≠ j
⊢ ‖HSMul.hSMul (α := ℝ) 1 (s.points i -ᵥ 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 : ∀ (hi : Membership.mem (γ := Set (Fin 2)) Set.univ ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩))
  (hij : (fun (i : Fin 2) ↦ i) ⟨0, sorry⟩ ≠ j),
  ‖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 j -ᵥ s.points 0) - HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖
Tactic: fin_cases i
Cleared hypotheses: i, hi, 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
i : Fin 2
hi : Membership.mem (γ := Set (Fin 2)) Set.univ i
j : Fin 2
hj : Membership.mem (γ := Set (Fin 2)) Set.univ j
hij : i ≠ j
0 :
  ∀ (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)‖
⊢ ‖HSMul.hSMul (α := ℝ) 1 (s.points i -ᵥ 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 : ∀ (hi : Membership.mem (γ := Set (Fin 2)) Set.univ ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩))
  (hij : (fun (i : Fin 2) ↦ i) ⟨1, sorry⟩ ≠ j),
  ‖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 j -ᵥ s.points 0) - HSMul.hSMul (α := ℝ) 2⁻¹ (s.points 1 -ᵥ s.points 0)‖
Tactic: fin_cases i
Cleared hypotheses: i, hi, hij