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 ι
hm :
  ∀ {ι : Type u_3} [hne : Nonempty ι] [Finite ι] {p : ι → P} (ha : AffineIndependent ℝ p) (val : Fintype ι)
    (hn : Fintype.card ι = 0),
    ∃! cs : Sphere P,
      Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
        Set.range p ⊆ Metric.sphere cs.center cs.radius
i : ι
hi : ∀ (y : ι), y = i
this : Unique ι
h : p i = p default ∧ {p default} ⊆ Metric.sphere (p i) 0
⊢ (p i = p default ∧ {p default} ⊆ Metric.sphere (p i) 0) ∧
    ∀ (y : Sphere P),
      y.center = p default ∧ {p default} ⊆ Metric.sphere y.center y.radius → y = { center := p i, radius := 0 }
have h₁ : ∀ (y : Sphere P),
  y.center = p default ∧ {p default} ⊆ Metric.sphere y.center y.radius → y = { center := p i, radius := 0 }
Tactic: constructor
-- 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 ι
hm :
  ∀ {ι : Type u_3} [hne : Nonempty ι] [Finite ι] {p : ι → P} (ha : AffineIndependent ℝ p) (val : Fintype ι)
    (hn : Fintype.card ι = 0),
    ∃! cs : Sphere P,
      Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
        Set.range p ⊆ Metric.sphere cs.center cs.radius
i : ι
hi : ∀ (y : ι), y = i
this : Unique ι
⊢ p i = p default ∧ {p default} ⊆ Metric.sphere (p i) 0
have h : True ∧ p i ∈ Metric.sphere (p i) 0
Tactic: simp_rw [hi default, Set.singleton_subset_iff]
-- 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
ι : Type u_3
hne : Nonempty ι
inst_4 : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
val : Fintype ι
hm :
  ∀ {ι : Type u_3} [hne : Nonempty ι] [Finite ι] {p : ι → P} (ha : AffineIndependent ℝ p) (val : Fintype ι)
    (hn : Fintype.card ι = 0),
    ∃! cs : Sphere P,
      Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
        Set.range p ⊆ Metric.sphere cs.center cs.radius
i : ι
hi : ∀ (y : ι), y = i
this : Unique ι
cr : ℝ
hdist :
  {p default} ⊆
    Metric.sphere (Sphere.center { center := p default, radius := cr : Sphere P })
      (Sphere.radius { center := p default, radius := cr : Sphere P })
⊢ Eq (α := Sphere P) { center := p default, radius := cr } { center := p i, radius := 0 }
have hdist₁ : 0 = cr
Tactic: replace hdist : 0 = cr := by simpa using hdist
Cleared hypotheses: hdist
-- 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 ι
hm :
  ∀ {ι : Type u_3} [hne : Nonempty ι] [Finite ι] {p : ι → P} (ha : AffineIndependent ℝ p) (val : Fintype ι)
    (hn : Fintype.card ι = 0),
    ∃! cs : Sphere P,
      Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
        Set.range p ⊆ Metric.sphere cs.center cs.radius
i : ι
hi : ∀ (y : ι), y = i
this : Unique ι
cr : ℝ
hdist : 0 = cr
⊢ Eq (α := Sphere P) { center := p default, radius := cr } { center := p i, radius := 0 }
have h : Eq (α := Sphere P) { center := p i, radius := cr } { center := p i, radius := 0 }
Tactic: rw [hi default, hdist]
-- 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 ι
hm :
  ∀ {ι : Type u_3} [hne : Nonempty ι] [Finite ι] {p : ι → P} (ha : AffineIndependent ℝ p) (val : Fintype ι)
    (hn : Fintype.card ι = 0),
    ∃! cs : Sphere P,
      Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
        Set.range p ⊆ Metric.sphere cs.center cs.radius
i : ι
hi : ∀ (y : ι), y = i
this : Unique ι
cr : ℝ
hdist : 0 = cr
h : Eq (α := Sphere P) { center := p i, radius := cr } { center := p i, radius := 0 }
⊢ Eq (α := Sphere P) { center := p default, radius := cr } { center := p i, radius := 0 }
have h₁ : Eq (α := Sphere P) { center := p i, radius := cr } { center := p i, radius := cr }
Tactic: rw [hi default, hdist]
-- 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
⊢ ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
      Set.range p ⊆ Metric.sphere cs.center cs.radius
have intro : ∀ (i : ι),
  ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
      Set.range p ⊆ Metric.sphere cs.center cs.radius
Tactic: have i := hne.some
-- 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 }
⊢ Fintype.card ι2 = m + 1
have rw : Finset.card.{u_3} (α := ι) {x : ι | x ≠ i} = m + 1
Tactic: rw [Fintype.card_of_subtype {x | x ≠ i}]
-- 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 }
rw : Finset.card.{u_3} (α := ι) {x : ι | x ≠ i} = m + 1
⊢ Fintype.card ι2 = m + 1
have H : ∀ (x : ι), Membership.mem (γ := Finset ι) {x : ι | x ≠ i} x ↔ x ≠ i
Tactic: rw [Fintype.card_of_subtype {x | x ≠ i}]
-- 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 }
⊢ Finset.card.{u_3} (α := ι) {x : ι | x ≠ i} = m + 1
have rw : m + 1 + 1 - Finset.card (α := ι) ({i} ∩ Finset.univ) = m + 1
Tactic: rw [Finset.filter_not, Finset.filter_eq' _ i, if_pos (Finset.mem_univ _),
            Finset.card_sdiff, Finset.card_univ, hn]
-- 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
ι : 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 hc : Fintype.card ι2 = m + 1
Tactic: 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
-- 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
ι : 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 }
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 this : Nonempty ι2
Tactic: haveI : Nonempty ι2 := Fintype.card_pos_iff.1 (hc.symm ▸ Nat.zero_lt_succ _)
-- 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
ι : 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 }
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
have ha2 : AffineIndependent.{0, u_1, u_2, u_3} ℝ (P := P) fun (i2 : ι2) ↦ p (↑i2 : ι)
Tactic: have ha2 : AffineIndependent ℝ fun i2 : ι2 => p i2 := ha.subtype _
-- 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
ι : 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 }
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
have hm₁ : ∃! cs : Sphere P,
  Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι))) cs.center ∧
    (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι)) ⊆ Metric.sphere cs.center cs.radius
Tactic: replace hm := hm ha2 _ hc
Cleared hypotheses: hm
-- 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 : ℕ
hn : Fintype.card ι = m + 1 + 1
i : ι
ι2 : Type (max 0 u_3) := { x : ι // x ≠ i }
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 : ι)
hm :
  ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι))) cs.center ∧
      (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι)) ⊆ Metric.sphere cs.center cs.radius
⊢ Set.range p = insert (p i) (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι))
have change : Set.range p = insert (p i) (Set.range fun (i2 : (↑{x : ι | x ≠ i} : Type u_3)) ↦ p (↑i2 : ι))
Tactic: change _ = insert _ (Set.range fun i2 : { x | x ≠ i } => p i2)
-- 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 : ℕ
hn : Fintype.card ι = m + 1 + 1
i : ι
ι2 : Type (max 0 u_3) := { x : ι // x ≠ i }
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 : ι)
hm :
  ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι))) cs.center ∧
      (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι)) ⊆ Metric.sphere cs.center cs.radius
⊢ Set.range p = insert (p i) (Set.range fun (i2 : (↑{x : ι | x ≠ i} : Type u_3)) ↦ p (↑i2 : ι))
have rw : p '' Set.univ = p '' insert i {x : ι | x ≠ i}
Tactic: rw [← Set.image_eq_range, ← Set.image_univ, ← Set.image_insert_eq]
-- 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 : ℕ
hn : Fintype.card ι = m + 1 + 1
i : ι
ι2 : Type (max 0 u_3) := { x : ι // x ≠ i }
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 : ι)
hm :
  ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι))) cs.center ∧
      (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι)) ⊆ Metric.sphere cs.center cs.radius
⊢ p '' Set.univ = p '' insert i {x : ι | x ≠ i}
have e_s : ∀ (j : ι), Membership.mem (γ := Set ι) Set.univ j ↔ Membership.mem (γ := Set ι) (insert i {x : ι | x ≠ i}) j
Tactic: congr with j
-- 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
ι : Type u_3
hne : Nonempty ι
inst_4 : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
val : Fintype ι
m : ℕ
hn : Fintype.card ι = m + 1 + 1
i : ι
ι2 : Type (max 0 u_3) := { x : ι // x ≠ i }
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 : ι)
hm :
  ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι))) cs.center ∧
      (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι)) ⊆ 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 hr : Set.range p = insert (p i) (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι))
Tactic: 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]
-- 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 : ℕ
hn : Fintype.card ι = m + 1 + 1
i : ι
ι2 : Type (max 0 u_3) := { x : ι // x ≠ i }
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 : ι)
hm :
  ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι))) cs.center ∧
      (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι)) ⊆ Metric.sphere cs.center cs.radius
hr : Set.range p = insert (p i) (Set.range 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
have intro : ∃! cs : Sphere P,
  Membership.mem (γ := AffineSubspace ℝ P)
      (affineSpan ℝ (insert (p i) (↑(affineSpan ℝ (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι))) : Set P))) cs.center ∧
    insert (p i) (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι)) ⊆ Metric.sphere cs.center cs.radius
Tactic: rw [hr, ← affineSpan_insert_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
ι : Type u_3
hne : Nonempty ι
inst_4 : Finite ι
p : ι → P
ha : AffineIndependent ℝ p
val : Fintype ι
m : ℕ
hn : Fintype.card ι = m + 1 + 1
i : ι
ι2 : Type (max 0 u_3) := { x : ι // x ≠ i }
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 : ι)
hm :
  ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι))) cs.center ∧
      (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι)) ⊆ Metric.sphere cs.center cs.radius
hr : Set.range p = insert (p i) (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι))
⊢ ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P)
        (affineSpan ℝ (insert (p i) (↑(affineSpan ℝ (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι))) : Set P))) cs.center ∧
      insert (p i) (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι)) ⊆ Metric.sphere cs.center cs.radius
have intro : p i ∉ affineSpan ℝ (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι))
Tactic: refine existsUnique_dist_eq_of_insert (Set.range_nonempty _) (subset_affineSpan ℝ _) ?_ hm
-- 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 : ℕ
hn : Fintype.card ι = m + 1 + 1
i : ι
ι2 : Type (max 0 u_3) := { x : ι // x ≠ i }
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 : ι)
hm :
  ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι))) cs.center ∧
      (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι)) ⊆ Metric.sphere cs.center cs.radius
hr : Set.range p = insert (p i) (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι))
⊢ p i ∉ affineSpan ℝ (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι))
have h : (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι)) = p '' (Set.univ \ {i})
Tactic: convert! ha.notMem_affineSpan_diff i Set.univ
-- 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 : ℕ
hn : Fintype.card ι = m + 1 + 1
i : ι
ι2 : Type (max 0 u_3) := { x : ι // x ≠ i }
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 : ι)
hm :
  ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι))) cs.center ∧
      (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι)) ⊆ Metric.sphere cs.center cs.radius
hr : Set.range p = insert (p i) (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι))
⊢ (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι)) = p '' (Set.univ \ {i})
have h : (Set.range fun (i2 : (↑{x : ι | x ≠ i} : Type u_3)) ↦ p (↑i2 : ι)) = p '' (Set.univ \ {i})
Tactic: change (Set.range fun i2 : { x | x ≠ i } => p i2) = _
-- 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 : ℕ
hn : Fintype.card ι = m + 1 + 1
i : ι
ι2 : Type (max 0 u_3) := { x : ι // x ≠ i }
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 : ι)
hm :
  ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι))) cs.center ∧
      (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι)) ⊆ Metric.sphere cs.center cs.radius
hr : Set.range p = insert (p i) (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι))
⊢ (Set.range fun (i2 : (↑{x : ι | x ≠ i} : Type u_3)) ↦ p (↑i2 : ι)) = p '' (Set.univ \ {i})
have h : p '' {x : ι | x ≠ i} = p '' (Set.univ \ {i})
Tactic: rw [← Set.image_eq_range]
-- 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 : ℕ
hn : Fintype.card ι = m + 1 + 1
i : ι
ι2 : Type (max 0 u_3) := { x : ι // x ≠ i }
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 : ι)
hm :
  ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι))) cs.center ∧
      (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι)) ⊆ Metric.sphere cs.center cs.radius
hr : Set.range p = insert (p i) (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι))
⊢ p '' {x : ι | x ≠ i} = p '' (Set.univ \ {i})
have h : ∀ (j : ι), Membership.mem (γ := Set ι) {x : ι | x ≠ i} j ↔ Membership.mem (γ := Set ι) (Set.univ \ {i}) j
Tactic: congr 1 with j