awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
α : Type u_3
inst : AddCommMonoid α
n : ℕ
f : PointsWithCircumcenterIndex n → α
have : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
have₁ :
  ∀ (h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)),
    ∑ i : PointsWithCircumcenterIndex n, f i = ∑ i : Fin (n + 1), f (pointIndex i) + f circumcenterIndex
have₂ : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)
have₃ have₄ :
  ∀ (h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)),
    ∑ i : PointsWithCircumcenterIndex n, f i = ∑ i : Fin (n + 1), f (pointIndex i) + f circumcenterIndex
have₅ :
  ∀ (h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)),
    ∑ i : PointsWithCircumcenterIndex n, f i =
      ∑ i : Fin (n + 1), f ((pointIndexEmbedding n : (a : Fin (n + 1)) → PointsWithCircumcenterIndex n) i) +
        f circumcenterIndex
have₆ :
  ∀ (h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)),
    circumcenterIndex ∉ Finset.map (pointIndexEmbedding n) univ
have₇ :
  ∀ (h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)) (x : Fin (n + 1)),
    ¬(Membership.mem (γ := Finset (Fin (n + 1))) univ x ∧
        Eq (α := PointsWithCircumcenterIndex n)
          ((pointIndexEmbedding n : (a : Fin (n + 1)) → PointsWithCircumcenterIndex n) x :
            PointsWithCircumcenterIndex n)
          (circumcenterIndex : PointsWithCircumcenterIndex n))
have₈ :
  ∀ (h : univ = insert circumcenterIndex (Finset.map (pointIndexEmbedding n) univ)) (x : Fin (n + 1)),
    Membership.mem (γ := Finset (Fin (n + 1))) univ x →
      ∀
        (h :
          Eq (α := PointsWithCircumcenterIndex n)
            ((pointIndexEmbedding n : (a : Fin (n + 1)) → PointsWithCircumcenterIndex n) x :
              PointsWithCircumcenterIndex n)
            (circumcenterIndex : PointsWithCircumcenterIndex n)),
        False
⊢ ∑ i : PointsWithCircumcenterIndex n, f i = ∑ i : Fin (n + 1), f (pointIndex i) + f circumcenterIndex

Tactic:
classical
  have h : univ = insert circumcenterIndex (univ.map (pointIndexEmbedding n)) := by
    ext x
    refine ⟨fun h => ?_, fun _ => mem_univ _⟩
    obtain i | - := x
    · exact mem_insert_of_mem (mem_map_of_mem _ (mem_univ i))
    · exact mem_insert_self _ _
  change _ = (∑ i, f (pointIndexEmbedding n i)) + _
  rw [add_comm, h, ← sum_map, sum_insert]
  simp_rw [Finset.mem_map, not_exists]
  rintro x ⟨_, h⟩
  injection h

Premises used: Finset.univ, Finset.sum_map, not_exists, Affine.Simplex.pointIndexEmbedding, add_comm, Finset.mem_map, Finset.sum_insert, DFunLike.coe, Finset.sum
-- 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
n : ℕ
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ s.pointsWithCircumcenter (pointIndex i) = s.points i

Tactic:
rfl

Premises used: Affine.Simplex.pointsWithCircumcenter, rfl
-- 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
n : ℕ
s : Simplex ℝ P n
⊢ s.pointsWithCircumcenter circumcenterIndex = s.circumcenter

Tactic:
rfl

Premises used: Affine.Simplex.pointsWithCircumcenter, rfl
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
n : ℕ
i : Fin (n + 1)
⊢ Eq (α := ℝ)
    (∑ x : PointsWithCircumcenterIndex n,
      if x = pointIndex i then Function.const (PointsWithCircumcenterIndex n) 1 x else 0)
    (if Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ (pointIndex i) then
      Function.const (PointsWithCircumcenterIndex n) 1 (pointIndex i)
    else 0)

Tactic:
sum_ite_eq' univ (pointIndex i) (Function.const _ (1 : ℝ))

Premises used: Finset.univ, Finset.sum_ite_eq', Affine.Simplex.PointsWithCircumcenterIndex.pointIndex, Function.const, OfNat.ofNat
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
n : ℕ
i : Fin (n + 1)
h :
  ∀ (j : PointsWithCircumcenterIndex n),
    Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ j →
      pointWeightsWithCircumcenter i j =
        if j = pointIndex i then Function.const (PointsWithCircumcenterIndex n) 1 j else 0
h₁ :
  Eq (α := ℝ) 1
    (if Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ (pointIndex i) then
      Function.const (PointsWithCircumcenterIndex n) 1 (pointIndex i)
    else 0)
⊢ Eq (α := ℝ) (∑ j : PointsWithCircumcenterIndex n, pointWeightsWithCircumcenter i j) 1

Tactic:
convert! sum_ite_eq' univ (pointIndex i) (Function.const _ (1 : ℝ)) with j

Premises used: Finset.univ, Finset.sum_ite_eq', Affine.Simplex.PointsWithCircumcenterIndex.pointIndex, Function.const, OfNat.ofNat
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
n : ℕ
i : Fin (n + 1)
j : PointsWithCircumcenterIndex n
h_1 : Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ j
h :
  ∀ (a : Fin (n + 1)),
    Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ (pointIndex a) →
      pointWeightsWithCircumcenter i (pointIndex a) =
        if pointIndex a = pointIndex i then Function.const (PointsWithCircumcenterIndex n) 1 (pointIndex a) else 0
h₁ :
  Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ circumcenterIndex →
    pointWeightsWithCircumcenter i circumcenterIndex =
      if circumcenterIndex = pointIndex i then Function.const (PointsWithCircumcenterIndex n) 1 circumcenterIndex else 0
⊢ pointWeightsWithCircumcenter i j = if j = pointIndex i then Function.const (PointsWithCircumcenterIndex n) 1 j else 0

Tactic:
cases j
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
n : ℕ
i a : Fin (n + 1)
h : Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ (pointIndex a)
⊢ pointWeightsWithCircumcenter i (pointIndex a) =
    if pointIndex a = pointIndex i then Function.const (PointsWithCircumcenterIndex n) 1 (pointIndex a) else 0

Tactic:
simp [pointWeightsWithCircumcenter]

Premises used: Affine.Simplex.pointWeightsWithCircumcenter
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
n : ℕ
i : Fin (n + 1)
h : Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ circumcenterIndex
⊢ pointWeightsWithCircumcenter i circumcenterIndex =
    if circumcenterIndex = pointIndex i then Function.const (PointsWithCircumcenterIndex n) 1 circumcenterIndex else 0

Tactic:
simp [pointWeightsWithCircumcenter]

Premises used: Affine.Simplex.pointWeightsWithCircumcenter
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
n : ℕ
i : Fin (n + 1)
⊢ Eq (α := ℝ) 1
    (if Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ (pointIndex i) then
      Function.const (PointsWithCircumcenterIndex n) 1 (pointIndex i)
    else 0)

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
n : ℕ
i : Fin (n + 1)
h :
  ∀ (j : PointsWithCircumcenterIndex n),
    Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ j →
      pointWeightsWithCircumcenter i j =
        if j = pointIndex i then Function.const (PointsWithCircumcenterIndex n) 1 j else 0
h₁ h₂ :
  Eq (α := ℝ) 1
    (if Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ (pointIndex i) then
      Function.const (PointsWithCircumcenterIndex n) 1 (pointIndex i)
    else 0)
⊢ Eq (α := ℝ) (∑ j : PointsWithCircumcenterIndex n, pointWeightsWithCircumcenter i j) 1

Tactic:
classical
  convert! sum_ite_eq' univ (pointIndex i) (Function.const _ (1 : ℝ)) with j
  · cases j <;> simp [pointWeightsWithCircumcenter]
  · simp

Premises used: Affine.Simplex.pointWeightsWithCircumcenter
-- 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
n : ℕ
s : Simplex ℝ P n
i : Fin (n + 1)
rw :
  s.pointsWithCircumcenter (pointIndex i) =
    (affineCombination ℝ univ s.pointsWithCircumcenter : (a : PointsWithCircumcenterIndex n → ℝ) → P)
      (pointWeightsWithCircumcenter i)
⊢ s.points i =
    (affineCombination ℝ univ s.pointsWithCircumcenter : (a : PointsWithCircumcenterIndex n → ℝ) → P)
      (pointWeightsWithCircumcenter i)

Tactic:
rw [← pointsWithCircumcenter_point]

Premises used: Affine.Simplex.pointsWithCircumcenter_point
-- 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
n : ℕ
s : Simplex ℝ P n
i : Fin (n + 1)
symm :
  (affineCombination ℝ univ s.pointsWithCircumcenter : (a : PointsWithCircumcenterIndex n → ℝ) → P)
      (pointWeightsWithCircumcenter i) =
    s.pointsWithCircumcenter (pointIndex i)
⊢ s.pointsWithCircumcenter (pointIndex i) =
    (affineCombination ℝ univ s.pointsWithCircumcenter : (a : PointsWithCircumcenterIndex n → ℝ) → P)
      (pointWeightsWithCircumcenter i)

Tactic:
symm
-- 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
n : ℕ
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ pointWeightsWithCircumcenter i (pointIndex i) = 1

Tactic:
simp [pointWeightsWithCircumcenter]

Premises used: Affine.Simplex.pointWeightsWithCircumcenter
-- 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
n : ℕ
s : Simplex ℝ P n
i : Fin (n + 1)
affineCombination_of_eq_one_of_eq_zero :
  ∀ (i2 : PointsWithCircumcenterIndex n),
    Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ i2 →
      i2 ≠ pointIndex i → pointWeightsWithCircumcenter i i2 = 0
⊢ (affineCombination ℝ univ s.pointsWithCircumcenter : (a : PointsWithCircumcenterIndex n → ℝ) → P)
      (pointWeightsWithCircumcenter i) =
    s.pointsWithCircumcenter (pointIndex i)

Tactic:
refine
    affineCombination_of_eq_one_of_eq_zero _ _ _ (mem_univ _)
      (by simp [pointWeightsWithCircumcenter]) ?_

Premises used: Finset.mem_univ, Finset.affineCombination_of_eq_one_of_eq_zero
-- 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
n : ℕ
s : Simplex ℝ P n
i_1 : Fin (n + 1)
i : PointsWithCircumcenterIndex n
hi : Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ i
hn : i ≠ PointsWithCircumcenterIndex.pointIndex i_1
pointIndex :
  ∀ (a : Fin (n + 1))
    (hi : Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ (PointsWithCircumcenterIndex.pointIndex a))
    (hn : PointsWithCircumcenterIndex.pointIndex a ≠ PointsWithCircumcenterIndex.pointIndex i_1),
    pointWeightsWithCircumcenter i_1 (PointsWithCircumcenterIndex.pointIndex a) = 0
circumcenterIndex :
  ∀
    (hi :
      Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ PointsWithCircumcenterIndex.circumcenterIndex)
    (hn : PointsWithCircumcenterIndex.circumcenterIndex ≠ PointsWithCircumcenterIndex.pointIndex i_1),
    pointWeightsWithCircumcenter i_1 PointsWithCircumcenterIndex.circumcenterIndex = 0
⊢ pointWeightsWithCircumcenter i_1 i = 0

Tactic:
cases i
-- 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
n : ℕ
s : Simplex ℝ P n
i a : Fin (n + 1)
hi : Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ (pointIndex a)
hn : pointIndex a ≠ pointIndex i
⊢ a ≠ i

Tactic:
have h : _ ≠ i := fun h => hn (h ▸ rfl)
-- 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
n : ℕ
s : Simplex ℝ P n
i a : Fin (n + 1)
hi : Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ (pointIndex a)
hn : pointIndex a ≠ pointIndex i
h : a ≠ i
⊢ pointWeightsWithCircumcenter i (pointIndex a) = 0

Tactic:
simp [pointWeightsWithCircumcenter, h]

Premises used: Affine.Simplex.pointWeightsWithCircumcenter
-- 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
n : ℕ
s : Simplex ℝ P n
i : Fin (n + 1)
hi : Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ circumcenterIndex
hn : circumcenterIndex ≠ pointIndex i
⊢ pointWeightsWithCircumcenter i circumcenterIndex = 0

Tactic:
rfl
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
n : ℕ
fs : Finset (Fin (n + 1))
h : fs.Nonempty
simp_rw :
  Eq (α := ℝ) (∑ x : Fin (n + 1), if x ∈ fs then (↑(#fs) : ℝ)⁻¹ else 0)
    (∑ i : Fin (n + 1), (↑fs : Set (Fin (n + 1))).indicator (centroidWeights ℝ fs) i)
⊢ Eq (α := ℝ) (∑ i : PointsWithCircumcenterIndex n, centroidWeightsWithCircumcenter fs i) 1

Tactic:
simp_rw [sum_pointsWithCircumcenter, centroidWeightsWithCircumcenter, add_zero, ←
    fs.sum_centroidWeights_eq_one_of_nonempty ℝ h, ← sum_indicator_subset _ fs.subset_univ]

Premises used: Real, Affine.Simplex.centroidWeightsWithCircumcenter, Finset.sum_indicator_subset, Finset.sum_centroidWeights_eq_one_of_nonempty, Affine.Simplex.sum_pointsWithCircumcenter, add_zero, Finset.subset_univ
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
n : ℕ
fs : Finset (Fin (n + 1))
h : fs.Nonempty
⊢ Eq (α := ℝ) (∑ x : Fin (n + 1), if x ∈ fs then (↑(#fs) : ℝ)⁻¹ else 0)
    (∑ i : Fin (n + 1), (↑fs : Set (Fin (n + 1))).indicator (centroidWeights ℝ fs) i)

Tactic:
rcongr
-- 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
n : ℕ
s : Simplex ℝ P n
fs : Finset (Fin (n + 1))
simp_rw :
  HVAdd.hVAdd.{u_1, u_2, u_2} (α := V) (β := P)
      (∑ x : Fin (n + 1),
        HSMul.hSMul (α := ℝ)
          (if x ∈ (↑fs : Set (Fin (n + 1))) then Function.const (Fin (n + 1)) (↑(#fs) : ℝ)⁻¹ x else 0)
          (s.points x -ᵥ Classical.choice ⋯))
      (Classical.choice ⋯) =
    HVAdd.hVAdd.{u_1, u_2, u_2} (α := V) (β := P)
      (∑ x : Fin (n + 1),
        HSMul.hSMul (α := ℝ) (if x ∈ fs then (↑(#fs) : ℝ)⁻¹ else 0) (s.points x -ᵥ Classical.choice ⋯))
      (Classical.choice ⋯)
⊢ Finset.centroid ℝ fs s.points =
    (affineCombination ℝ univ s.pointsWithCircumcenter : (a : PointsWithCircumcenterIndex n → ℝ) → P)
      (centroidWeightsWithCircumcenter fs)

Tactic:
simp_rw [centroid_def, affineCombination_apply, weightedVSubOfPoint_apply,
    sum_pointsWithCircumcenter, centroidWeightsWithCircumcenter,
    pointsWithCircumcenter_point, zero_smul, add_zero, centroidWeights,
    ← sum_indicator_subset_of_eq_zero (Function.const (Fin (n + 1)) (#fs : ℝ)⁻¹)
      (fun i wi => wi • (s.points i -ᵥ Classical.choice AddTorsor.nonempty)) fs.subset_univ fun _ =>
      zero_smul ℝ _,
    Set.indicator_apply]

Premises used: Finset.weightedVSubOfPoint_apply, Affine.Simplex.points, Real, Set.indicator_apply, Classical.choice, Affine.Simplex.centroidWeightsWithCircumcenter, AddTorsor.nonempty, Finset.sum_indicator_subset_of_eq_zero, Nat.cast, Finset.affineCombination_apply, VSub.vsub, Affine.Simplex.pointsWithCircumcenter_point, zero_smul, Inv.inv, HAdd.hAdd, Finset.card, Function.const, HSMul.hSMul, Affine.Simplex.sum_pointsWithCircumcenter, Finset.centroidWeights, add_zero, OfNat.ofNat, Fin, Finset.centroid_def, Finset.subset_univ
-- 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
n : ℕ
s : Simplex ℝ P n
fs : Finset (Fin (n + 1))
⊢ HVAdd.hVAdd.{u_1, u_2, u_2} (α := V) (β := P)
      (∑ x : Fin (n + 1),
        HSMul.hSMul (α := ℝ)
          (if x ∈ (↑fs : Set (Fin (n + 1))) then Function.const (Fin (n + 1)) (↑(#fs) : ℝ)⁻¹ x else 0)
          (s.points x -ᵥ Classical.choice ⋯))
      (Classical.choice ⋯) =
    HVAdd.hVAdd.{u_1, u_2, u_2} (α := V) (β := P)
      (∑ x : Fin (n + 1),
        HSMul.hSMul (α := ℝ) (if x ∈ fs then (↑(#fs) : ℝ)⁻¹ else 0) (s.points x -ᵥ Classical.choice ⋯))
      (Classical.choice ⋯)

Tactic:
congr
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
n : ℕ
⊢ Eq (α := ℝ)
    (∑ x : PointsWithCircumcenterIndex n,
      if x = circumcenterIndex then Function.const (PointsWithCircumcenterIndex n) 1 x else 0)
    (if Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ circumcenterIndex then
      Function.const (PointsWithCircumcenterIndex n) 1 circumcenterIndex
    else 0)

Tactic:
sum_ite_eq' univ circumcenterIndex (Function.const _ (1 : ℝ))

Premises used: Finset.univ, Finset.sum_ite_eq', Function.const, OfNat.ofNat, Affine.Simplex.PointsWithCircumcenterIndex.circumcenterIndex
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
n : ℕ
h :
  ∀ (j : PointsWithCircumcenterIndex n),
    Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ j →
      circumcenterWeightsWithCircumcenter n j =
        if j = circumcenterIndex then Function.const (PointsWithCircumcenterIndex n) 1 j else 0
h₁ :
  Eq (α := ℝ) 1
    (if Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ circumcenterIndex then
      Function.const (PointsWithCircumcenterIndex n) 1 circumcenterIndex
    else 0)
⊢ Eq (α := ℝ) (∑ i : PointsWithCircumcenterIndex n, circumcenterWeightsWithCircumcenter n i) 1

Tactic:
convert! sum_ite_eq' univ circumcenterIndex (Function.const _ (1 : ℝ)) with j

Premises used: Finset.univ, Finset.sum_ite_eq', Function.const, OfNat.ofNat, Affine.Simplex.PointsWithCircumcenterIndex.circumcenterIndex
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
n : ℕ
j : PointsWithCircumcenterIndex n
h_1 : Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ j
h :
  ∀ (a : Fin (n + 1)),
    Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ (pointIndex a) →
      circumcenterWeightsWithCircumcenter n (pointIndex a) =
        if pointIndex a = circumcenterIndex then Function.const (PointsWithCircumcenterIndex n) 1 (pointIndex a) else 0
h₁ :
  Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ circumcenterIndex →
    circumcenterWeightsWithCircumcenter n circumcenterIndex =
      if Eq (α := PointsWithCircumcenterIndex n) circumcenterIndex circumcenterIndex then
        Function.const (PointsWithCircumcenterIndex n) 1 circumcenterIndex
      else 0
⊢ circumcenterWeightsWithCircumcenter n j =
    if j = circumcenterIndex then Function.const (PointsWithCircumcenterIndex n) 1 j else 0

Tactic:
cases j
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
n : ℕ
a : Fin (n + 1)
h : Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ (pointIndex a)
⊢ circumcenterWeightsWithCircumcenter n (pointIndex a) =
    if pointIndex a = circumcenterIndex then Function.const (PointsWithCircumcenterIndex n) 1 (pointIndex a) else 0

Tactic:
simp [circumcenterWeightsWithCircumcenter]

Premises used: Affine.Simplex.circumcenterWeightsWithCircumcenter
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
n : ℕ
h : Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ circumcenterIndex
⊢ circumcenterWeightsWithCircumcenter n circumcenterIndex =
    if Eq (α := PointsWithCircumcenterIndex n) circumcenterIndex circumcenterIndex then
      Function.const (PointsWithCircumcenterIndex n) 1 circumcenterIndex
    else 0

Tactic:
simp [circumcenterWeightsWithCircumcenter]

Premises used: Affine.Simplex.circumcenterWeightsWithCircumcenter
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
n : ℕ
⊢ Eq (α := ℝ) 1
    (if Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ circumcenterIndex then
      Function.const (PointsWithCircumcenterIndex n) 1 circumcenterIndex
    else 0)

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Circumcenter
Goal:
n : ℕ
h :
  ∀ (j : PointsWithCircumcenterIndex n),
    Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ j →
      circumcenterWeightsWithCircumcenter n j =
        if j = circumcenterIndex then Function.const (PointsWithCircumcenterIndex n) 1 j else 0
h₁ h₂ :
  Eq (α := ℝ) 1
    (if Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ circumcenterIndex then
      Function.const (PointsWithCircumcenterIndex n) 1 circumcenterIndex
    else 0)
⊢ Eq (α := ℝ) (∑ i : PointsWithCircumcenterIndex n, circumcenterWeightsWithCircumcenter n i) 1

Tactic:
classical
  convert! sum_ite_eq' univ circumcenterIndex (Function.const _ (1 : ℝ)) with j
  · cases j <;> simp [circumcenterWeightsWithCircumcenter]
  · simp

Premises used: Affine.Simplex.circumcenterWeightsWithCircumcenter
-- 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
n : ℕ
s : Simplex ℝ P n
rw :
  s.pointsWithCircumcenter circumcenterIndex =
    (affineCombination ℝ univ s.pointsWithCircumcenter : (a : PointsWithCircumcenterIndex n → ℝ) → P)
      (circumcenterWeightsWithCircumcenter n)
⊢ s.circumcenter =
    (affineCombination ℝ univ s.pointsWithCircumcenter : (a : PointsWithCircumcenterIndex n → ℝ) → P)
      (circumcenterWeightsWithCircumcenter n)

Tactic:
rw [← pointsWithCircumcenter_eq_circumcenter]

Premises used: Affine.Simplex.pointsWithCircumcenter_eq_circumcenter
-- 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
n : ℕ
s : Simplex ℝ P n
symm :
  (affineCombination ℝ univ s.pointsWithCircumcenter : (a : PointsWithCircumcenterIndex n → ℝ) → P)
      (circumcenterWeightsWithCircumcenter n) =
    s.pointsWithCircumcenter circumcenterIndex
⊢ s.pointsWithCircumcenter circumcenterIndex =
    (affineCombination ℝ univ s.pointsWithCircumcenter : (a : PointsWithCircumcenterIndex n → ℝ) → P)
      (circumcenterWeightsWithCircumcenter n)

Tactic:
symm
-- 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
n : ℕ
s : Simplex ℝ P n
⊢ (affineCombination ℝ univ s.pointsWithCircumcenter : (a : PointsWithCircumcenterIndex n → ℝ) → P)
      (circumcenterWeightsWithCircumcenter n) =
    s.pointsWithCircumcenter circumcenterIndex

Tactic:
affineCombination_of_eq_one_of_eq_zero _ _ _ (mem_univ _) rfl ?_

Premises used: Finset.mem_univ, Finset.affineCombination_of_eq_one_of_eq_zero, rfl
-- 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
n : ℕ
s : Simplex ℝ P n
refine :
  ∀ (i2 : PointsWithCircumcenterIndex n),
    Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ i2 →
      i2 ≠ circumcenterIndex → circumcenterWeightsWithCircumcenter n i2 = 0
⊢ (affineCombination ℝ univ s.pointsWithCircumcenter : (a : PointsWithCircumcenterIndex n → ℝ) → P)
      (circumcenterWeightsWithCircumcenter n) =
    s.pointsWithCircumcenter circumcenterIndex

Tactic:
refine affineCombination_of_eq_one_of_eq_zero _ _ _ (mem_univ _) rfl ?_

Premises used: Finset.mem_univ, Finset.affineCombination_of_eq_one_of_eq_zero, rfl
-- 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
n : ℕ
s : Simplex ℝ P n
i : Fin (n + 1)
h : Membership.mem (γ := Finset (PointsWithCircumcenterIndex n)) univ (pointIndex i)
hn : pointIndex i ≠ circumcenterIndex
⊢ circumcenterWeightsWithCircumcenter n (pointIndex i) = 0

Tactic:
tauto