awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Congruence
Goal:
ι : Type u_1
V₁ : Type u_2
V₂ : Type u_3
P₁ : Type u_4
P₂ : Type u_5
inst : NormedAddCommGroup V₁
inst_1 : NormedAddCommGroup V₂
inst_2 : InnerProductSpace ℝ V₁
inst_3 : InnerProductSpace ℝ V₂
inst_4 : MetricSpace P₁
inst_5 : MetricSpace P₂
inst_6 : NormedAddTorsor V₁ P₁
inst_7 : NormedAddTorsor V₂ P₂
v₁ : ι → P₁
v₂ : ι → P₂
h : v₁ ≅ v₂
i j k : ι
simp_rw :
  Real.arccos
      ((‖v₁ i -ᵥ v₁ j‖ * ‖v₁ i -ᵥ v₁ j‖ + ‖v₁ k -ᵥ v₁ j‖ * ‖v₁ k -ᵥ v₁ j‖ -
            ‖v₁ i -ᵥ v₁ j - (v₁ k -ᵥ v₁ j)‖ * ‖v₁ i -ᵥ v₁ j - (v₁ k -ᵥ v₁ j)‖) /
          2 /
        (‖v₁ i -ᵥ v₁ j‖ * ‖v₁ k -ᵥ v₁ j‖)) =
    Real.arccos
      ((‖v₂ i -ᵥ v₂ j‖ * ‖v₂ i -ᵥ v₂ j‖ + ‖v₂ k -ᵥ v₂ j‖ * ‖v₂ k -ᵥ v₂ j‖ -
            ‖v₂ i -ᵥ v₂ j - (v₂ k -ᵥ v₂ j)‖ * ‖v₂ i -ᵥ v₂ j - (v₂ k -ᵥ v₂ j)‖) /
          2 /
        (‖v₂ i -ᵥ v₂ j‖ * ‖v₂ k -ᵥ v₂ j‖))
simp_rw₁ :
  Real.arccos
      ((‖v₁ i -ᵥ v₁ j‖ * ‖v₁ i -ᵥ v₁ j‖ + ‖v₁ k -ᵥ v₁ j‖ * ‖v₁ k -ᵥ v₁ j‖ - ‖v₁ i -ᵥ v₁ k‖ * ‖v₁ i -ᵥ v₁ k‖) / 2 /
        (‖v₁ i -ᵥ v₁ j‖ * ‖v₁ k -ᵥ v₁ j‖)) =
    Real.arccos
      ((‖v₂ i -ᵥ v₂ j‖ * ‖v₂ i -ᵥ v₂ j‖ + ‖v₂ k -ᵥ v₂ j‖ * ‖v₂ k -ᵥ v₂ j‖ - ‖v₂ i -ᵥ v₂ k‖ * ‖v₂ i -ᵥ v₂ k‖) / 2 /
        (‖v₂ i -ᵥ v₂ j‖ * ‖v₂ k -ᵥ v₂ j‖))
simp_rw₂ :
  Real.arccos
      ((dist (v₁ i) (v₁ j) * dist (v₁ i) (v₁ j) + dist (v₁ k) (v₁ j) * dist (v₁ k) (v₁ j) -
            dist (v₁ i) (v₁ k) * dist (v₁ i) (v₁ k)) /
          2 /
        (dist (v₁ i) (v₁ j) * dist (v₁ k) (v₁ j))) =
    Real.arccos
      ((dist (v₂ i) (v₂ j) * dist (v₂ i) (v₂ j) + dist (v₂ k) (v₂ j) * dist (v₂ k) (v₂ j) -
            dist (v₂ i) (v₂ k) * dist (v₂ i) (v₂ k)) /
          2 /
        (dist (v₂ i) (v₂ j) * dist (v₂ k) (v₂ j)))
⊢ Real.arccos (inner ℝ (v₁ i -ᵥ v₁ j) (v₁ k -ᵥ v₁ j) / (‖v₁ i -ᵥ v₁ j‖ * ‖v₁ k -ᵥ v₁ j‖)) =
    Real.arccos (inner ℝ (v₂ i -ᵥ v₂ j) (v₂ k -ᵥ v₂ j) / (‖v₂ i -ᵥ v₂ j‖ * ‖v₂ k -ᵥ v₂ j‖))

Tactic:
simp_rw [real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two,
    vsub_sub_vsub_cancel_right, ← dist_eq_norm_vsub, h.dist_eq]

Premises used: real_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two, vsub_sub_vsub_cancel_right, dist_eq_norm_vsub, Congruent.dist_eq
-- Module: Mathlib.Geometry.Euclidean.Incenter
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
m n : ℕ
inst_4 : NeZero m
inst_5 : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
signs : Finset (Fin (m + 1))
h :
  ∀ (i : Fin (m + 1)),
    (s.reindex e).excenterWeightsUnnorm signs i =
      (s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs) ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) i
⊢ (s.reindex e).excenterWeightsUnnorm signs =
    s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs) ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))

Tactic:
ext i
-- Module: Mathlib.Geometry.Euclidean.Incenter
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
m n : ℕ
inst_4 : NeZero m
inst_5 : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
signs : Finset (Fin (m + 1))
i : Fin (m + 1)
⊢ (s.reindex e).excenterWeightsUnnorm signs i =
    (s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs) ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) i

Tactic:
simp [excenterWeightsUnnorm]

Premises used: Affine.Simplex.excenterWeightsUnnorm
-- Module: Mathlib.Geometry.Euclidean.Incenter
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
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
inst_8 : NeZero n
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
h :
  ∀ (x : Finset (Fin (n + 1))) (x_1 : Fin (n + 1)),
    (s.map f.toAffineMap ⋯).excenterWeightsUnnorm x x_1 = s.excenterWeightsUnnorm x x_1
⊢ (s.map f.toAffineMap ⋯).excenterWeightsUnnorm = s.excenterWeightsUnnorm

Tactic:
ext
-- Module: Mathlib.Geometry.Euclidean.Incenter
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
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
inst_8 : NeZero n
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
x : Finset (Fin (n + 1))
x_1 : Fin (n + 1)
⊢ (s.map f.toAffineMap ⋯).excenterWeightsUnnorm x x_1 = s.excenterWeightsUnnorm x x_1

Tactic:
simp [excenterWeightsUnnorm]

Premises used: Affine.Simplex.excenterWeightsUnnorm
-- Module: Mathlib.Geometry.Euclidean.Incenter
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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
h :
  ∀ (x : Finset (Fin (n + 1))) (x_1 : Fin (n + 1)),
    excenterWeightsUnnorm.{u_1, u_2} (P := ↥S) (s.restrict S hS) x x_1 = s.excenterWeightsUnnorm x x_1
⊢ excenterWeightsUnnorm.{u_1, u_2} (P := ↥S) (s.restrict S hS) = s.excenterWeightsUnnorm

Tactic:
ext
-- Module: Mathlib.Geometry.Euclidean.Incenter
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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
x : Finset (Fin (n + 1))
x_1 : Fin (n + 1)
⊢ excenterWeightsUnnorm.{u_1, u_2} (P := ↥S) (s.restrict S hS) x x_1 = s.excenterWeightsUnnorm x x_1

Tactic:
simp [excenterWeightsUnnorm]

Premises used: Affine.Simplex.excenterWeightsUnnorm
-- Module: Mathlib.Geometry.Euclidean.Incenter
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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
i : Fin (n + 1)
⊢ s.excenterWeightsUnnorm ∅ i = (s.height i)⁻¹

Tactic:
one_mul _

Premises used: Multiset.zero, Multiset.ofList, Affine.Simplex.excenterWeightsUnnorm, one_mul, ite
-- Module: Mathlib.Geometry.Euclidean.Incenter
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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
i : Fin (n + 1)
⊢ (if i ∈ signs then -1 else 1) * (s.height i)⁻¹ ≠ 0

Tactic:
mul_ne_zero ?_ ?_

Premises used: mul_ne_zero
-- Module: Mathlib.Geometry.Euclidean.Incenter
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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
i : Fin (n + 1)
refine_1 : Ne (α := ℝ) (if i ∈ signs then -1 else 1) 0
refine_2 : (s.height i)⁻¹ ≠ 0
⊢ (if i ∈ signs then -1 else 1) * (s.height i)⁻¹ ≠ 0

Tactic:
refine mul_ne_zero ?_ ?_

Premises used: mul_ne_zero
-- Module: Mathlib.Geometry.Euclidean.Incenter
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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
i : Fin (n + 1)
⊢ Ne (α := ℝ) (if i ∈ signs then -1 else 1) 0

Tactic:
grind
-- Module: Mathlib.Geometry.Euclidean.Incenter
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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
i : Fin (n + 1)
⊢ (s.height i)⁻¹ ≠ 0

Tactic:
simp [(s.height_pos i).ne']

Premises used: Affine.Simplex.height_pos, LT.lt.ne'
-- Module: Mathlib.Geometry.Euclidean.Incenter
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
m n : ℕ
inst_4 : NeZero m
inst_5 : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
signs : Finset (Fin (m + 1))
simp_rw :
  Ne (α := ℝ) (∑ i : Fin (m + 1), (s.reindex e).excenterWeightsUnnorm signs i) 0 ↔
    Ne (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs) i) 0
simp_rw₁ :
  Ne (α := ℝ)
      (∑ x : Fin (m + 1),
        (s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs) ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) x)
      0 ↔
    Ne (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs) i) 0
simp_rw₂ :
  (Finset.map e.symm.toEmbedding Finset.univ).sum (s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs)) ≠ 0 ↔
    Ne (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs) i) 0
⊢ (s.reindex e).ExcenterExists signs ↔ s.ExcenterExists (Finset.map e.symm.toEmbedding signs)

Tactic:
simp_rw [ExcenterExists, excenterWeightsUnnorm_reindex, Finset.sum_comp_equiv,
    Finset.map_univ_equiv]

Premises used: Affine.Simplex.ExcenterExists, Affine.Simplex.excenterWeightsUnnorm_reindex, Finset.map_univ_equiv, Finset.sum_comp_equiv
-- Module: Mathlib.Geometry.Euclidean.Incenter
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
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
inst_8 : NeZero n
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
h : ∀ (x : Finset (Fin (n + 1))), (s.map f.toAffineMap ⋯).ExcenterExists x ↔ s.ExcenterExists x
⊢ (s.map f.toAffineMap ⋯).ExcenterExists = s.ExcenterExists

Tactic:
ext
-- Module: Mathlib.Geometry.Euclidean.Incenter
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
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
inst_8 : NeZero n
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
x : Finset (Fin (n + 1))
⊢ (s.map f.toAffineMap ⋯).ExcenterExists x ↔ s.ExcenterExists x

Tactic:
simp [ExcenterExists]

Premises used: Affine.Simplex.ExcenterExists
-- Module: Mathlib.Geometry.Euclidean.Incenter
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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
h : ∀ (x : Finset (Fin (n + 1))), ExcenterExists.{u_1, u_2} (P := ↥S) (s.restrict S hS) x ↔ s.ExcenterExists x
⊢ ExcenterExists.{u_1, u_2} (P := ↥S) (s.restrict S hS) = s.ExcenterExists

Tactic:
ext
-- Module: Mathlib.Geometry.Euclidean.Incenter
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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
x : Finset (Fin (n + 1))
⊢ ExcenterExists.{u_1, u_2} (P := ↥S) (s.restrict S hS) x ↔ s.ExcenterExists x

Tactic:
simp [ExcenterExists]

Premises used: Affine.Simplex.ExcenterExists
-- Module: Mathlib.Geometry.Euclidean.Incenter
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
m n : ℕ
inst_4 : NeZero m
inst_5 : NeZero n
s : Simplex ℝ P n
e : Fin (n + 1) ≃ Fin (m + 1)
signs : Finset (Fin (m + 1))
simp_rw :
  HSMul.hSMul (α := ℝ) (∑ i : Fin (m + 1), (s.reindex e).excenterWeightsUnnorm signs i)⁻¹
      ((s.reindex e).excenterWeightsUnnorm signs) =
    HSMul.hSMul (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs) i)⁻¹
        (s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs)) ∘
      (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))
simp_rw₁ :
  HSMul.hSMul (α := ℝ) (β := (i : Fin (m + 1)) → ℝ)
      (∑ x : Fin (m + 1),
          (s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs) ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1)))
            x)⁻¹
      (s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs) ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) =
    HSMul.hSMul (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs) i)⁻¹
        (s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs)) ∘
      (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))
simp_rw₂ :
  HSMul.hSMul (β := (i : Fin (m + 1)) → ℝ)
      ((Finset.map e.symm.toEmbedding Finset.univ).sum
          (s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs)))⁻¹
      (s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs) ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) =
    HSMul.hSMul (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs) i)⁻¹
        (s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs)) ∘
      (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))
simp_rw₃ :
  HSMul.hSMul (α := ℝ) (β := (i : Fin (m + 1)) → ℝ)
      (∑ x : Fin (n + 1), s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs) x)⁻¹
      (s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs) ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) =
    HSMul.hSMul (α := ℝ) (∑ x : Fin (n + 1), s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs) x)⁻¹
        (s.excenterWeightsUnnorm (Finset.map e.symm.toEmbedding signs)) ∘
      (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))
⊢ (s.reindex e).excenterWeights signs =
    s.excenterWeights (Finset.map e.symm.toEmbedding signs) ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))

Tactic:
simp_rw [excenterWeights, excenterWeightsUnnorm_reindex, Finset.sum_comp_equiv,
    Finset.map_univ_equiv, Pi.smul_comp]

Premises used: Pi.smul_comp, Affine.Simplex.excenterWeightsUnnorm_reindex, Finset.map_univ_equiv, Affine.Simplex.excenterWeights, Finset.sum_comp_equiv
-- Module: Mathlib.Geometry.Euclidean.Incenter
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
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
inst_8 : NeZero n
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
h :
  ∀ (x : Finset (Fin (n + 1))) (x_1 : Fin (n + 1)),
    (s.map f.toAffineMap ⋯).excenterWeights x x_1 = s.excenterWeights x x_1
⊢ (s.map f.toAffineMap ⋯).excenterWeights = s.excenterWeights

Tactic:
ext
-- Module: Mathlib.Geometry.Euclidean.Incenter
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
V₂ : Type u_3
P₂ : Type u_4
inst_4 : NormedAddCommGroup V₂
inst_5 : InnerProductSpace ℝ V₂
inst_6 : MetricSpace P₂
inst_7 : NormedAddTorsor V₂ P₂
n : ℕ
inst_8 : NeZero n
s : Simplex ℝ P n
f : P →ᵃⁱ[ℝ] P₂
x : Finset (Fin (n + 1))
x_1 : Fin (n + 1)
⊢ (s.map f.toAffineMap ⋯).excenterWeights x x_1 = s.excenterWeights x x_1

Tactic:
simp [excenterWeights]

Premises used: Affine.Simplex.excenterWeights
-- Module: Mathlib.Geometry.Euclidean.Incenter
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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
h :
  ∀ (x : Finset (Fin (n + 1))) (x_1 : Fin (n + 1)),
    excenterWeights.{u_1, u_2} (P := ↥S) (s.restrict S hS) x x_1 = s.excenterWeights x x_1
⊢ excenterWeights.{u_1, u_2} (P := ↥S) (s.restrict S hS) = s.excenterWeights

Tactic:
ext
-- Module: Mathlib.Geometry.Euclidean.Incenter
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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
x : Finset (Fin (n + 1))
x_1 : Fin (n + 1)
⊢ excenterWeights.{u_1, u_2} (P := ↥S) (s.restrict S hS) x x_1 = s.excenterWeights x x_1

Tactic:
simp [excenterWeights]

Premises used: Affine.Simplex.excenterWeights
-- Module: Mathlib.Geometry.Euclidean.Incenter
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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
⊢ HSMul.hSMul (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹ (s.excenterWeightsUnnorm signs) i ≠ 0

Tactic:
mul_ne_zero ?_ (s.excenterWeightsUnnorm_ne_zero _ _)

Premises used: Affine.Simplex.excenterWeightsUnnorm_ne_zero, mul_ne_zero
-- Module: Mathlib.Geometry.Euclidean.Incenter
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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
refine : Ne (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹ 0
⊢ HSMul.hSMul (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹ (s.excenterWeightsUnnorm signs) i ≠ 0

Tactic:
refine mul_ne_zero ?_ (s.excenterWeightsUnnorm_ne_zero _ _)

Premises used: Affine.Simplex.excenterWeightsUnnorm_ne_zero, mul_ne_zero
-- Module: Mathlib.Geometry.Euclidean.Incenter
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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i : Fin (n + 1)
rw :
  ∀ (h : Ne (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i) 0) (i : Fin (n + 1)),
    Ne (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹ 0
⊢ Ne (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹ 0

Tactic:
rw [ExcenterExists] at h

Premises used: Affine.Simplex.ExcenterExists
-- Module: Mathlib.Geometry.Euclidean.Incenter
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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : Ne (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i) 0
i : Fin (n + 1)
⊢ Ne (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹ 0

Tactic:
simp [h]
-- Module: Mathlib.Geometry.Euclidean.Incenter
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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
h : ∀ (i : Fin (n + 1)), s.excenterWeightsUnnorm signsᶜ i = (-s.excenterWeightsUnnorm signs) i
⊢ s.excenterWeightsUnnorm signsᶜ = -s.excenterWeightsUnnorm signs

Tactic:
ext i
-- Module: Mathlib.Geometry.Euclidean.Incenter
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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
i : Fin (n + 1)
pos : ∀ (h : i ∈ signs), s.excenterWeightsUnnorm signsᶜ i = (-s.excenterWeightsUnnorm signs) i
neg : ∀ (h : i ∉ signs), s.excenterWeightsUnnorm signsᶜ i = (-s.excenterWeightsUnnorm signs) i
⊢ s.excenterWeightsUnnorm signsᶜ i = (-s.excenterWeightsUnnorm signs) i

Tactic:
by_cases h : i ∈ signs
-- Module: Mathlib.Geometry.Euclidean.Incenter
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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
i : Fin (n + 1)
h : i ∈ signs
⊢ s.excenterWeightsUnnorm signsᶜ i = (-s.excenterWeightsUnnorm signs) i

Tactic:
simp [excenterWeightsUnnorm, h]

Premises used: Affine.Simplex.excenterWeightsUnnorm
-- Module: Mathlib.Geometry.Euclidean.Incenter
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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
i : Fin (n + 1)
h : i ∉ signs
⊢ s.excenterWeightsUnnorm signsᶜ i = (-s.excenterWeightsUnnorm signs) i

Tactic:
simp [excenterWeightsUnnorm, h]

Premises used: Affine.Simplex.excenterWeightsUnnorm
-- Module: Mathlib.Geometry.Euclidean.Incenter
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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
⊢ s.excenterWeights signsᶜ = s.excenterWeights signs

Tactic:
simp [excenterWeights, inv_neg]

Premises used: inv_neg, Affine.Simplex.excenterWeights
-- Module: Mathlib.Geometry.Euclidean.Incenter
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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
⊢ s.ExcenterExists signsᶜ ↔ s.ExcenterExists signs

Tactic:
simp [ExcenterExists]

Premises used: Affine.Simplex.ExcenterExists
-- Module: Mathlib.Geometry.Euclidean.Incenter
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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
inst_5 : Decidable (s.ExcenterExists signs)
pos :
  ∀ (h : Ne (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i) 0),
    Eq (α := ℝ)
      (∑ x : Fin (n + 1),
        HSMul.hSMul (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹ (s.excenterWeightsUnnorm signs) x)
      1
neg :
  ∀ (h : ¬Ne (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i) 0),
    Eq (α := ℝ)
      (∑ x : Fin (n + 1),
        HSMul.hSMul (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹ (s.excenterWeightsUnnorm signs) x)
      0
⊢ Eq (α := ℝ)
    (∑ x : Fin (n + 1),
      HSMul.hSMul (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹ (s.excenterWeightsUnnorm signs) x)
    (if Ne (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i) 0 then 1 else 0)

Tactic:
split_ifs with h
-- Module: Mathlib.Geometry.Euclidean.Incenter
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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
inst_5 : Decidable (s.ExcenterExists signs)
h : Ne (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i) 0
⊢ Eq (α := ℝ)
    (∑ x : Fin (n + 1),
      HSMul.hSMul (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹ (s.excenterWeightsUnnorm signs) x)
    1

Tactic:
simp [← Finset.mul_sum, h]

Premises used: Finset.mul_sum
-- Module: Mathlib.Geometry.Euclidean.Incenter
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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
inst_5 : Decidable (s.ExcenterExists signs)
h : ¬Ne (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i) 0
⊢ Eq (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i) 0

Tactic:
simp only [ne_eq, not_not] at h

Premises used: Classical.not_not, ne_eq
-- Module: Mathlib.Geometry.Euclidean.Incenter
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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
inst_5 : Decidable (s.ExcenterExists signs)
h : Eq (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i) 0
⊢ Eq (α := ℝ)
    (∑ x : Fin (n + 1),
      HSMul.hSMul (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹ (s.excenterWeightsUnnorm signs) x)
    0

Tactic:
simp [h]
-- Module: Mathlib.Geometry.Euclidean.Incenter
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 : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
signs : Finset (Fin (n + 1))
⊢ Eq (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeights signs i) 1 ↔ s.ExcenterExists signs

Tactic:
simp [sum_excenterWeights]

Premises used: Affine.Simplex.sum_excenterWeights