-- 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
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
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 : ι))
    (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
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 : ι))
    (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
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 : ι))
    (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
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 : ι))
    (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 : ι))
h :
  ∀ (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})
h₁ :
  ∀ (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})
⊢ ∃! cs : Sphere P,
    Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range p)) cs.center ∧
      Set.range p ⊆ Metric.sphere cs.center cs.radius
have h₂ : ∀ (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})
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
Cleared hypotheses: hm