awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 j : Fin (n + 1)
hne : i ≠ j
rw :
  Eq (α := SignType)
    ((SignType.sign : (a : ℝ) → SignType) ((s.signedInfDist j : (a : P) → ℝ) (s.touchpoint signs i) : ℝ) : SignType)
    ((SignType.sign : (a : ℝ) → SignType)
        ((s.signedInfDist j : (a : P) → ℝ)
            ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i) : (a : ℝ) → P) 1 : P) :
          ℝ) :
      SignType)
⊢ Eq (α := SignType)
    ((SignType.sign : (a : ℝ) → SignType) ((s.signedInfDist j : (a : P) → ℝ) (s.touchpoint signs i) : ℝ) : SignType)
    ((SignType.sign : (a : ℝ) → SignType) ((s.signedInfDist j : (a : P) → ℝ) (s.excenter signs) : ℝ) : SignType)

Tactic:
rw [← h.sign_signedInfDist_lineMap_excenter_touchpoint hne (r := 1) ⟨zero_le_one, le_rfl⟩]

Premises used: le_rfl, Affine.Simplex.ExcenterExists.sign_signedInfDist_lineMap_excenter_touchpoint, zero_le_one, And.intro
-- 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 j : Fin (n + 1)
hne : i ≠ j
⊢ Eq (α := SignType)
    ((SignType.sign : (a : ℝ) → SignType) ((s.signedInfDist j : (a : P) → ℝ) (s.touchpoint signs i) : ℝ) : SignType)
    ((SignType.sign : (a : ℝ) → SignType)
        ((s.signedInfDist j : (a : P) → ℝ)
            ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i) : (a : ℝ) → P) 1 : P) :
          ℝ) :
      SignType)

Tactic:
simp
-- 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 j : Fin (n + 1)
hne : i ≠ j
⊢ Eq (α := SignType)
    ((SignType.sign : (a : ℝ) → SignType) ((s.signedInfDist j : (a : P) → ℝ) (s.touchpoint ∅ i) : ℝ) : SignType)
    ((SignType.sign : (a : ℝ) → SignType) ((s.signedInfDist j : (a : P) → ℝ) s.incenter : ℝ) : SignType)

Tactic:
s.excenterExists_empty.sign_signedInfDist_touchpoint hne

Premises used: Affine.Simplex.incenter, Affine.Simplex.ExcenterExists.sign_signedInfDist_touchpoint, Affine.Simplex.excenterExists_empty
-- 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)
⊢ Eq (α := ℝ) (∑ j : Fin (n + 1), s.touchpointWeights signs i j) 1

Tactic:
(eq_affineCombination_of_mem_affineSpan_of_fintype
    (s.touchpoint_mem_affineSpan_simplex signs i)).choose_spec.1

Premises used: Exists.choose_spec, eq_affineCombination_of_mem_affineSpan_of_fintype, And.left, Affine.Simplex.touchpointWeights, Affine.Simplex.touchpoint_mem_affineSpan_simplex
-- 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)
⊢ (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) (s.touchpointWeights signs i) =
    s.touchpoint signs i

Tactic:
(eq_affineCombination_of_mem_affineSpan_of_fintype
    (s.touchpoint_mem_affineSpan_simplex signs i)).choose_spec.2.symm

Premises used: Exists.choose_spec, eq_affineCombination_of_mem_affineSpan_of_fintype, And.right, Affine.Simplex.touchpointWeights, Affine.Simplex.touchpoint_mem_affineSpan_simplex, Eq.symm
-- 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)
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ j : Fin (n + 1), w j) 1
mp :
  (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w = s.touchpoint signs i →
    w = s.touchpointWeights signs i
mpr :
  w = s.touchpointWeights signs i →
    (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w = s.touchpoint signs i
⊢ (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w = s.touchpoint signs i ↔
    w = s.touchpointWeights signs i

Tactic:
constructor
-- 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)
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ j : Fin (n + 1), w j) 1
mp :
  Eq.{u_2 + 1} (α := P) ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P)
      ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) (s.touchpointWeights signs i) :
        P) →
    w = s.touchpointWeights signs i
⊢ (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w = s.touchpoint signs i →
    w = s.touchpointWeights signs i

Tactic:
rw [← s.affineCombination_touchpointWeights]

Premises used: Affine.Simplex.affineCombination_touchpointWeights
-- 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)
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ j : Fin (n + 1), w j) 1
⊢ Eq.{u_2 + 1} (α := P) ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P)
      ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) (s.touchpointWeights signs i) :
        P) →
    w = s.touchpointWeights signs i

Tactic:
fun h ↦ (affineIndependent_iff_eq_of_fintype_affineCombination_eq ℝ s.points).1
      s.independent _ _ hw (s.sum_touchpointWeights _ _) h

Premises used: Affine.Simplex.points, Real, affineIndependent_iff_eq_of_fintype_affineCombination_eq, Iff.mp, Affine.Simplex.sum_touchpointWeights, Affine.Simplex.independent, Affine.Simplex.touchpointWeights
-- 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)
w : Fin (n + 1) → ℝ
hw : Eq (α := ℝ) (∑ j : Fin (n + 1), w j) 1
⊢ Eq.{u_2 + 1} (α := P) ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) w : P)
      ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) (s.touchpointWeights signs i) :
        P) →
    w = s.touchpointWeights signs i

Tactic:
exact fun h ↦ (affineIndependent_iff_eq_of_fintype_affineCombination_eq ℝ s.points).1
      s.independent _ _ hw (s.sum_touchpointWeights _ _) h

Premises used: Affine.Simplex.points, Real, affineIndependent_iff_eq_of_fintype_affineCombination_eq, Iff.mp, Affine.Simplex.sum_touchpointWeights, Affine.Simplex.independent, Affine.Simplex.touchpointWeights
-- 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)
hw : Eq (α := ℝ) (∑ j : Fin (n + 1), s.touchpointWeights signs i j) 1
⊢ (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) (s.touchpointWeights signs i) =
    s.touchpoint signs i

Tactic:
simp
-- 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)
rw :
  (Finset.affineCombination ℝ Finset.univ (s.reindex e).points : (a : Fin (m + 1) → ℝ) → P)
      (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i) ∘
        (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) =
    (s.reindex e).touchpoint signs i
rw₁ :
  Eq (α := ℝ)
    (∑ j : Fin (m + 1),
      (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i) ∘
          (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1)))
        j)
    1
⊢ (s.reindex e).touchpointWeights signs i =
    s.touchpointWeights (Finset.map e.symm.toEmbedding signs) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i) ∘
      (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))

Tactic:
rw [eq_comm, ← affineCombination_eq_touchpoint_iff]

Premises used: eq_comm, Affine.Simplex.affineCombination_eq_touchpoint_iff
-- 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)
rw :
  Eq.{u_2 + 1} (α := P)
    ((Finset.affineCombination ℝ Finset.univ
            { points := s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1)), independent := ⋯ :
                Simplex ℝ P m }.points :
          (a : Fin (m + 1) → ℝ) → P)
        (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i) ∘
          (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) :
      P)
    ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P)
        (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i)) :
      P)
⊢ (Finset.affineCombination ℝ Finset.univ (s.reindex e).points : (a : Fin (m + 1) → ℝ) → P)
      (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i) ∘
        (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) =
    (s.reindex e).touchpoint signs i

Tactic:
rw [touchpoint_reindex, ← affineCombination_touchpointWeights, reindex]

Premises used: Affine.Simplex.reindex, Affine.Simplex.touchpoint_reindex, Affine.Simplex.affineCombination_touchpointWeights
-- 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)
dsimp :
  Eq.{u_2 + 1} (α := P)
    ((Finset.affineCombination ℝ Finset.univ (s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) :
          (a : Fin (m + 1) → ℝ) → P)
        (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i) ∘
          (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) :
      P)
    ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P)
        (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i)) :
      P)
⊢ Eq.{u_2 + 1} (α := P)
    ((Finset.affineCombination ℝ Finset.univ
            { points := s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1)), independent := ⋯ :
                Simplex ℝ P m }.points :
          (a : Fin (m + 1) → ℝ) → P)
        (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i) ∘
          (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) :
      P)
    ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P)
        (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i)) :
      P)

Tactic:
dsimp only
-- 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)
rw :
  Eq.{u_2 + 1} (α := P)
    ((Finset.affineCombination ℝ (Finset.map e.symm.toEmbedding Finset.univ) s.points : (a : Fin (n + 1) → ℝ) → P)
        (s.touchpointWeights (Finset.map e.symm.toEmbedding signs)
          ((e.symm.toEmbedding : (a : Fin (m + 1)) → Fin (n + 1)) i)) :
      P)
    ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P)
        (s.touchpointWeights (Finset.map e.symm.toEmbedding signs)
          ((e.symm.toEmbedding : (a : Fin (m + 1)) → Fin (n + 1)) i)) :
      P)
⊢ Eq.{u_2 + 1} (α := P)
    ((Finset.affineCombination ℝ Finset.univ (s.points ∘ (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) :
          (a : Fin (m + 1) → ℝ) → P)
        (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i) ∘
          (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1))) :
      P)
    ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P)
        (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i)) :
      P)

Tactic:
rw [← Equiv.coe_toEmbedding, ← Finset.affineCombination_map]

Premises used: Equiv.coe_toEmbedding, Finset.affineCombination_map
-- 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)
⊢ Eq.{u_2 + 1} (α := P)
    ((Finset.affineCombination ℝ (Finset.map e.symm.toEmbedding Finset.univ) s.points : (a : Fin (n + 1) → ℝ) → P)
        (s.touchpointWeights (Finset.map e.symm.toEmbedding signs)
          ((e.symm.toEmbedding : (a : Fin (m + 1)) → Fin (n + 1)) i)) :
      P)
    ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P)
        (s.touchpointWeights (Finset.map e.symm.toEmbedding signs)
          ((e.symm.toEmbedding : (a : Fin (m + 1)) → Fin (n + 1)) i)) :
      P)

Tactic:
simp
-- 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)
rw :
  (Finset.map e.symm.toEmbedding Finset.univ).sum
      (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i)) =
    1
⊢ Eq (α := ℝ)
    (∑ j : Fin (m + 1),
      (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i) ∘
          (⇑e.symm : (a : Fin (m + 1)) → Fin (n + 1)))
        j)
    1

Tactic:
rw [Finset.sum_comp_equiv]

Premises used: 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
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)
⊢ (Finset.map e.symm.toEmbedding Finset.univ).sum
      (s.touchpointWeights (Finset.map e.symm.toEmbedding signs) ((e.symm : (a : Fin (m + 1)) → Fin (n + 1)) i)) =
    1

Tactic:
simp
-- 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
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
f : P →ᵃⁱ[ℝ] P₂
h₁ : ∀ (i : Fin (n + 1)), (s.map f.toAffineMap ⋯).touchpointWeights signs i = s.touchpointWeights signs i
⊢ (s.map f.toAffineMap ⋯).touchpointWeights signs = s.touchpointWeights signs

Tactic:
ext i : 1
-- 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
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
f : P →ᵃⁱ[ℝ] P₂
i : Fin (n + 1)
h₁ :
  (Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P)
      ((s.map f.toAffineMap ⋯).touchpointWeights signs i) =
    s.touchpoint signs i
⊢ (s.map f.toAffineMap ⋯).touchpointWeights signs i = s.touchpointWeights signs i

Tactic:
rw [← affineCombination_eq_touchpoint_iff
    ((s.map f.toAffineMap f.injective).sum_touchpointWeights _ _)]

Premises used: Affine.Simplex.affineCombination_eq_touchpoint_iff, Affine.Simplex.map, AffineIsometry.toAffineMap, Affine.Simplex.sum_touchpointWeights, AffineIsometry.injective
-- 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
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
f : P →ᵃⁱ[ℝ] P₂
i : Fin (n + 1)
⊢ (Finset.affineCombination ℝ Finset.univ (s.map f.toAffineMap ⋯).points : (a : Fin (n + 1) → ℝ) → P₂)
      ((s.map f.toAffineMap ⋯).touchpointWeights signs i) =
    (s.map f.toAffineMap ⋯).touchpoint signs i

Tactic:
have hc := (s.map f.toAffineMap f.injective).affineCombination_touchpointWeights signs 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))
S : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
h : ExcenterExists.{u_1, u_2} (P := ↥S) (s.restrict S hS) signs
this : Nonempty.{u_2 + 1} ↥S
⊢ touchpointWeights.{u_1, u_2} (P := ↥S) (s.restrict S hS) signs = s.touchpointWeights signs

Tactic:
(h.touchpointWeights_map S.subtypeₐᵢ).symm

Premises used: Affine.Simplex.map, Affine.Simplex.ExcenterExists.touchpointWeights_map, AffineSubspace.subtypeₐᵢ, Eq.symm
-- 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 : AffineSubspace ℝ P
hS : affineSpan ℝ (Set.range s.points) ≤ S
h : ExcenterExists.{u_1, u_2} (P := ↥S) (s.restrict S hS) signs
this : Nonempty.{u_2 + 1} ↥S
⊢ touchpointWeights.{u_1, u_2} (P := ↥S) (s.restrict S hS) signs = s.touchpointWeights signs

Tactic:
exact (h.touchpointWeights_map S.subtypeₐᵢ).symm

Premises used: Affine.Simplex.ExcenterExists.touchpointWeights_map, AffineSubspace.subtypeₐᵢ, Eq.symm
-- 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 j : Fin (n + 1)
hne : i ≠ j
⊢ Eq (α := SignType)
    ((SignType.sign : (a : ℝ) → SignType) ((s.signedInfDist j : (a : P) → ℝ) (s.touchpoint signs i) : ℝ) : SignType)
    ((SignType.sign : (a : ℝ) → SignType) ((s.signedInfDist j : (a : P) → ℝ) (s.excenter signs) : ℝ) : SignType)

Tactic:
have hs := h.sign_signedInfDist_touchpoint hne
-- 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 j : Fin (n + 1)
hne : i ≠ j
hs :
  Eq (α := SignType)
    ((SignType.sign : (a : ℝ) → SignType)
        ((s.signedInfDist j : (a : P) → ℝ)
            ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P)
                (s.touchpointWeights signs i) :
              P) :
          ℝ) :
      SignType)
    ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeights signs j) : SignType)
⊢ Eq (α := ℝ) (∑ i_1 : Fin (n + 1), s.touchpointWeights signs i i_1) 1

Tactic:
simp
-- 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 j : Fin (n + 1)
hne : i ≠ j
hs :
  Eq (α := SignType)
    ((SignType.sign : (a : ℝ) → SignType) ((s.signedInfDist j : (a : P) → ℝ) (s.touchpoint signs i) : ℝ) : SignType)
    ((SignType.sign : (a : ℝ) → SignType) ((s.signedInfDist j : (a : P) → ℝ) (s.excenter signs) : ℝ) : SignType)
⊢ Eq (α := SignType)
    ((SignType.sign : (a : ℝ) → SignType)
        (s.touchpointWeights signs i j *
          ‖s.points j -ᵥ
              (↑(((s.faceOpposite j).orthogonalProjectionSpan :
                      (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite j).points)))
                    (s.points j)) :
                P)‖) :
      SignType)
    ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeights signs j) : SignType)

Tactic:
rw [← s.affineCombination_touchpointWeights signs i, h.sign_signedInfDist_excenter,
    s.signedInfDist_affineCombination j (by simp)] at hs

Premises used: Affine.Simplex.affineCombination_touchpointWeights, Affine.Simplex.ExcenterExists.sign_signedInfDist_excenter, Affine.Simplex.signedInfDist_affineCombination
-- 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 j : Fin (n + 1)
hne : i ≠ j
hs :
  Eq (α := SignType)
    ((SignType.sign : (a : ℝ) → SignType)
        (s.touchpointWeights signs i j *
          ‖s.points j -ᵥ
              (↑(((s.faceOpposite j).orthogonalProjectionSpan :
                      (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite j).points)))
                    (s.points j)) :
                P)‖) :
      SignType)
    ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeights signs j) : SignType)
rw :
  (SignType.sign : (a : ℝ) → SignType) (s.touchpointWeights signs i j) =
    HMul.hMul (α := SignType) (β := SignType)
      ((SignType.sign : (a : ℝ) → SignType) (s.touchpointWeights signs i j) : SignType)
      ((SignType.sign : (a : ℝ) → SignType)
          ‖s.points j -ᵥ
              (↑(((s.faceOpposite j).orthogonalProjectionSpan :
                      (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite j).points)))
                    (s.points j)) :
                P)‖ :
        SignType)
⊢ Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (s.touchpointWeights signs i j) : SignType)
    ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeights signs j) : SignType)

Tactic:
rw [← hs, sign_mul]

Premises used: sign_mul