awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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
intro :
  ∀ (i : ι),
    ∃! 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

Tactic:
have i := hne.some
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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
H : ∀ (x : ι), Membership.mem (γ := Finset ι) {x : ι | x ≠ i} x ↔ x ≠ i
⊢ Fintype.card ι2 = m + 1

Tactic:
rw [Fintype.card_of_subtype {x | x ≠ i}]

Premises used: Finset.univ, Ne, Fintype.card_of_subtype, Finset.filter
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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 : m + 1 + 1 - Finset.card (α := ι) ({i} ∩ Finset.univ) = m + 1
⊢ Finset.card.{u_3} (α := ι) {x : ι | x ≠ i} = m + 1

Tactic:
rw [Finset.filter_not, Finset.filter_eq' _ i, if_pos (Finset.mem_univ _),
            Finset.card_sdiff, Finset.card_univ, hn]

Premises used: Finset.mem_univ, Finset.card_univ, Finset.card_sdiff, Finset.filter_eq', if_pos, Finset.filter_not
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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 }
⊢ m + 1 + 1 - Finset.card (α := ι) ({i} ∩ Finset.univ) = m + 1

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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 }
⊢ ∀ (x : ι), Membership.mem (γ := Finset ι) {x : ι | x ≠ i} x ↔ x ≠ i

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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

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
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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
⊢ Nonempty ι2

Tactic:
haveI : Nonempty ι2 := Fintype.card_pos_iff.1 (hc.symm ▸ Nat.zero_lt_succ _)
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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
⊢ 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 _
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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 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
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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
change : Set.range p = insert (p i) (Set.range fun (i2 : (↑{x : ι | x ≠ i} : Type u_3)) ↦ p (↑i2 : ι))
⊢ Set.range p = insert (p i) (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι))

Tactic:
change _ = insert _ (Set.range fun i2 : { x | x ≠ i } => p i2)

Premises used: Insert.insert, Set.range, Subtype.val
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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
rw : p '' Set.univ = p '' insert i {x : ι | x ≠ i}
⊢ Set.range p = insert (p i) (Set.range fun (i2 : (↑{x : ι | x ≠ i} : Type u_3)) ↦ p (↑i2 : ι))

Tactic:
rw [← Set.image_eq_range, ← Set.image_univ, ← Set.image_insert_eq]

Premises used: Set.image_univ, Set.image_eq_range, Set.image_insert_eq
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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
e_s : ∀ (j : ι), Membership.mem (γ := Set ι) Set.univ j ↔ Membership.mem (γ := Set ι) (insert i {x : ι | x ≠ i}) j
⊢ p '' Set.univ = p '' insert i {x : ι | x ≠ i}

Tactic:
congr with j
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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
j : ι
⊢ Membership.mem (γ := Set ι) Set.univ j ↔ Membership.mem (γ := Set ι) (insert i {x : ι | x ≠ i}) j

Tactic:
simp [Classical.em]

Premises used: Classical.em
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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 : ι))

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]
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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 : ι))
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
⊢ ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
      Set.range p ⊆ Metric.sphere cs.center cs.radius

Tactic:
rw [hr, ← affineSpan_insert_affineSpan]

Premises used: affineSpan_insert_affineSpan
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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

Tactic:
existsUnique_dist_eq_of_insert (Set.range_nonempty _) (subset_affineSpan ℝ _) ?_ hm

Premises used: Real, subset_affineSpan, Set.range_nonempty, EuclideanGeometry.existsUnique_dist_eq_of_insert
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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 : ι))
intro : p i ∉ affineSpan ℝ (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

Tactic:
refine existsUnique_dist_eq_of_insert (Set.range_nonempty _) (subset_affineSpan ℝ _) ?_ hm

Premises used: Real, subset_affineSpan, Set.range_nonempty, EuclideanGeometry.existsUnique_dist_eq_of_insert
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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 ℝ (p '' (Set.univ \ {i}))

Tactic:
ha.notMem_affineSpan_diff i Set.univ

Premises used: Set.univ, AffineIndependent.notMem_affineSpan_diff
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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 : ι))
h : (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι)) = p '' (Set.univ \ {i})
⊢ p i ∉ affineSpan ℝ (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι))

Tactic:
convert! ha.notMem_affineSpan_diff i Set.univ

Premises used: Set.univ, AffineIndependent.notMem_affineSpan_diff
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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 : ι))
h : (Set.range fun (i2 : (↑{x : ι | x ≠ i} : Type u_3)) ↦ p (↑i2 : ι)) = p '' (Set.univ \ {i})
⊢ (Set.range fun (i2 : ι2) ↦ p (↑i2 : ι)) = p '' (Set.univ \ {i})

Tactic:
change (Set.range fun i2 : { x | x ≠ i } => p i2) = _

Premises used: Set.range, Subtype.val
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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 : ι))
h : p '' {x : ι | x ≠ i} = p '' (Set.univ \ {i})
⊢ (Set.range fun (i2 : (↑{x : ι | x ≠ i} : Type u_3)) ↦ p (↑i2 : ι)) = p '' (Set.univ \ {i})

Tactic:
rw [← Set.image_eq_range]

Premises used: Set.image_eq_range
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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 : ι))
h : ∀ (j : ι), Membership.mem (γ := Set ι) {x : ι | x ≠ i} j ↔ Membership.mem (γ := Set ι) (Set.univ \ {i}) j
⊢ p '' {x : ι | x ≠ i} = p '' (Set.univ \ {i})

Tactic:
congr 1 with j
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
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 : ι))
j : ι
⊢ Membership.mem (γ := Set ι) {x : ι | x ≠ i} j ↔ Membership.mem (γ := Set ι) (Set.univ \ {i}) j

Tactic:
simp