-- Mathlib/Geometry/Euclidean/Circumcenter.lean
theorem sum_pointsWithCircumcenter {α : Type*} [AddCommMonoid α] {n : ℕ}
    (f : PointsWithCircumcenterIndex n → α) :
    ∑ i, f i = (∑ i : Fin (n + 1), f (pointIndex i)) + f circumcenterIndex

Proof state:
case h.pointIndex
α : Type u_3
inst✝ : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
i : Fin (n + 1)
h : pointIndex i ∈ univ
⊢ pointIndex i ∈ insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)

Tactic:
exact mem_insert_of_mem (mem_map_of_mem _ (mem_univ i))

Result:
no goals

Proof state:
α : Type u_3
inst✝ : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
⊢ ∑ i : PointsWithCircumcenterIndex n, f i = ∑ i : Fin (n + 1), f ((pointIndexEmbedding n) i) + f circumcenterIndex

Tactic:
rw [add_comm, h, ← sum_map, sum_insert]

Result:
α : Type u_3
inst✝ : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
⊢ circumcenterIndex ∉ Finset.map (pointIndexEmbedding n) univ

Proof state:
case h.circumcenterIndex
α : Type u_3
inst✝ : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
h : circumcenterIndex ∈ univ
⊢ circumcenterIndex ∈ insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)

Tactic:
exact mem_insert_self _ _

Result:
no goals

Proof state:
α : Type u_3
inst✝ : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
⊢ ∑ i : PointsWithCircumcenterIndex n, f i = ∑ i : Fin (n + 1), f (pointIndex i) + f circumcenterIndex

Tactic:
change _ = (∑ i, f (pointIndexEmbedding n i)) + _

Result:
α : Type u_3
inst✝ : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
⊢ ∑ i : PointsWithCircumcenterIndex n, f i = ∑ i : Fin (n + 1), f ((pointIndexEmbedding n) i) + f circumcenterIndex

Proof state:
case h
α : Type u_3
inst✝ : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
x : PointsWithCircumcenterIndex n
⊢ x ∈ univ ↔ x ∈ insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)

Tactic:
refine ⟨fun h => ?_, fun _ => mem_univ _⟩

Result:
case h
α : Type u_3
inst✝ : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
x : PointsWithCircumcenterIndex n
h : x ∈ univ
⊢ x ∈ insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)

Proof state:
α : Type u_3
inst✝ : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
⊢ ∀ (x : Fin (n + 1)), ¬(x ∈ univ ∧ (pointIndexEmbedding n) x = circumcenterIndex)

Tactic:
rintro x ⟨_, h⟩

Result:
case intro
α : Type u_3
inst✝ : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
h✝ : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
x : Fin (n + 1)
left✝ : x ∈ univ
h : (pointIndexEmbedding n) x = circumcenterIndex
⊢ False

Proof state:
case intro
α : Type u_3
inst✝ : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
h✝ : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
x : Fin (n + 1)
left✝ : x ∈ univ
h : (pointIndexEmbedding n) x = circumcenterIndex
⊢ False

Tactic:
injection h

Result:
no goals

Proof state:
α : Type u_3
inst✝ : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
⊢ univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)

Tactic:
ext x

Result:
case h
α : Type u_3
inst✝ : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
x : PointsWithCircumcenterIndex n
⊢ x ∈ univ ↔ x ∈ insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)

Proof state:
case h
α : Type u_3
inst✝ : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
x : PointsWithCircumcenterIndex n
h : x ∈ univ
⊢ x ∈ insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)

Tactic:
obtain i | - := x

Result:
case h.pointIndex
α : Type u_3
inst✝ : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
i : Fin (n + 1)
h : pointIndex i ∈ univ
⊢ pointIndex i ∈ insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)

case h.circumcenterIndex
α : Type u_3
inst✝ : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
h : circumcenterIndex ∈ univ
⊢ circumcenterIndex ∈ insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)

Proof state:
α : Type u_3
inst✝ : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
⊢ circumcenterIndex ∉ Finset.map (pointIndexEmbedding n) univ

Tactic:
simp_rw [Finset.mem_map, not_exists]

Result:
α : Type u_3
inst✝ : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
⊢ ∀ (x : Fin (n + 1)), ¬(x ∈ univ ∧ (pointIndexEmbedding n) x = circumcenterIndex)