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
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)
⊢ (SignType.sign : (a : ℝ) → SignType) (s.touchpointWeights signs i j) =
    HMul.hMul (α := SignType) (β := SignType)
      ((SignType.sign : (a : ℝ) → SignType) (s.touchpointWeights signs i j) : SignType) (1 : SignType)

Tactic:
(mul_one _).symm

Premises used: mul_one, 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
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)
h₁ :
  Eq (α := 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)
    (1 : SignType)
⊢ (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)

Tactic:
convert! (mul_one _).symm

Premises used: mul_one, 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
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)
h₁ :
  0 <
    dist (s.points j)
      (↑(((s.faceOpposite j).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite j).points)))
            (s.points j)) :
        P)
⊢ Eq (α := 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)
    (1 : SignType)

Tactic:
rw [sign_eq_one_iff, ← dist_eq_norm_vsub]

Premises used: dist_eq_norm_vsub, sign_eq_one_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
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)
⊢ 0 <
    dist (s.points j)
      (↑(((s.faceOpposite j).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite j).points)))
            (s.points j)) :
        P)

Tactic:
s.height_pos _

Premises used: Affine.Simplex.height, Affine.Simplex.height_pos, Affine.Simplex.altitudeFoot
-- 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)
⊢ 0 <
    dist (s.points j)
      (↑(((s.faceOpposite j).orthogonalProjectionSpan : (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite j).points)))
            (s.points j)) :
        P)

Tactic:
exact s.height_pos _

Premises used: Affine.Simplex.height_pos
-- 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
rw : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeights ∅ j) : SignType) (1 : SignType)
⊢ Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (s.touchpointWeights ∅ i j) : SignType) (1 : SignType)

Tactic:
rw [s.excenterExists_empty.sign_touchpointWeights hne]

Premises used: Affine.Simplex.ExcenterExists.sign_touchpointWeights, 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
i j : Fin (n + 1)
hne : i ≠ j
⊢ Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeights ∅ j) : SignType) (1 : 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
signs : Finset (Fin (n + 1))
i : Fin (n + 1)
⊢ s.touchpointWeights signs i i = 0

Tactic:
s.independent.eq_zero_of_affineCombination_mem_affineSpan
    (s.sum_touchpointWeights signs i) ?_ (Finset.mem_univ _)
    (Set.notMem_compl_iff.2 (Set.mem_singleton _))

Premises used: Iff.mpr, Finset.mem_univ, Set.mem_singleton, Set.notMem_compl_iff, Affine.Simplex.sum_touchpointWeights, Affine.Simplex.independent, AffineIndependent.eq_zero_of_affineCombination_mem_affineSpan
-- 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 :
  Membership.mem (α := P) (γ := AffineSubspace ℝ P) (affineSpan ℝ (s.points '' {i}ᶜ))
    ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) (s.touchpointWeights signs i) : P)
⊢ s.touchpointWeights signs i i = 0

Tactic:
refine s.independent.eq_zero_of_affineCombination_mem_affineSpan
    (s.sum_touchpointWeights signs i) ?_ (Finset.mem_univ _)
    (Set.notMem_compl_iff.2 (Set.mem_singleton _))

Premises used: Iff.mpr, Finset.mem_univ, Set.mem_singleton, Set.notMem_compl_iff, Affine.Simplex.sum_touchpointWeights, Affine.Simplex.independent, AffineIndependent.eq_zero_of_affineCombination_mem_affineSpan
-- 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)
rw : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (s.points '' {i}ᶜ)) (s.touchpoint signs i)
⊢ Membership.mem (α := P) (γ := AffineSubspace ℝ P) (affineSpan ℝ (s.points '' {i}ᶜ))
    ((Finset.affineCombination ℝ Finset.univ s.points : (a : Fin (n + 1) → ℝ) → P) (s.touchpointWeights signs i) : P)

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)
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite i).points)) (s.touchpoint signs i)

Tactic:
s.touchpoint_mem_affineSpan _ _

Premises used: Affine.Simplex.touchpoint_mem_affineSpan
-- 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 : s.points '' {i}ᶜ = Set.range (s.faceOpposite i).points
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (s.points '' {i}ᶜ)) (s.touchpoint signs i)

Tactic:
convert! s.touchpoint_mem_affineSpan _ _

Premises used: Affine.Simplex.touchpoint_mem_affineSpan
-- 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.points '' {i}ᶜ = Set.range (s.faceOpposite i).points

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
⊢ 0 < s.touchpointWeights ∅ i j

Tactic:
simpa [sign_eq_one_iff] using s.sign_touchpointWeights_empty hne

Premises used: Affine.Simplex.sign_touchpointWeights_empty, sign_eq_one_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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
inst_5 : n.AtLeastTwo
i : Fin (n + 1)
rw :
  (∀ (i_1 : Fin (n + 1)), Membership.mem (γ := Finset (Fin (n + 1))) {i}ᶜ i_1 → 0 < s.touchpointWeights ∅ i i_1) ∧
    ∀ i_1 ∉ {i}ᶜ, s.touchpointWeights ∅ i i_1 = 0
⊢ s.touchpoint ∅ i ∈ (s.faceOpposite i).interior

Tactic:
rw [faceOpposite, ← affineCombination_touchpointWeights,
    s.affineCombination_mem_interior_face_iff_pos _ (s.sum_touchpointWeights _ _)]

Premises used: Affine.Simplex.affineCombination_mem_interior_face_iff_pos, Affine.Simplex.affineCombination_touchpointWeights, Affine.Simplex.sum_touchpointWeights, Affine.Simplex.faceOpposite
-- 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
inst_5 : n.AtLeastTwo
i : Fin (n + 1)
simp : ∀ (i_1 : Fin (n + 1)), ¬i_1 = i → 0 < s.touchpointWeights ∅ i i_1
⊢ (∀ (i_1 : Fin (n + 1)), Membership.mem (γ := Finset (Fin (n + 1))) {i}ᶜ i_1 → 0 < s.touchpointWeights ∅ i i_1) ∧
    ∀ i_1 ∉ {i}ᶜ, s.touchpointWeights ∅ i i_1 = 0

Tactic:
simp only [Finset.mem_compl, Finset.mem_singleton, Decidable.not_not, forall_eq,
    touchpointWeights_eq_zero, and_true]

Premises used: Finset.mem_singleton, and_true, forall_eq, Finset.mem_compl, Affine.Simplex.touchpointWeights_eq_zero, Decidable.not_not
-- 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
inst_5 : n.AtLeastTwo
i j : Fin (n + 1)
hj : ¬j = i
⊢ 0 < s.touchpointWeights ∅ i j

Tactic:
s.touchpointWeights_empty_pos (Ne.symm hj)

Premises used: Affine.Simplex.touchpointWeights_empty_pos, Ne.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
inst_5 : n.AtLeastTwo
i j : Fin (n + 1)
hj : ¬j = i
⊢ 0 < s.touchpointWeights ∅ i j

Tactic:
exact s.touchpointWeights_empty_pos (Ne.symm hj)

Premises used: Affine.Simplex.touchpointWeights_empty_pos, Ne.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
inst_5 : n.AtLeastTwo
i j : Fin (n + 1)
hne : i ≠ j
rw : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeights {i} j) : SignType) (1 : SignType)
rw₁ rw₂ : Eq (α := SignType) 1 1
⊢ Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (s.touchpointWeights {i} i j) : SignType) (1 : SignType)

Tactic:
rw [(s.excenterExists_singleton i).sign_touchpointWeights hne,
    s.sign_excenterWeights_singleton_pos hne]

Premises used: Affine.Simplex.sign_excenterWeights_singleton_pos, Affine.Simplex.ExcenterExists.sign_touchpointWeights, Affine.Simplex.excenterExists_singleton
-- 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
inst_5 : n.AtLeastTwo
i j : Fin (n + 1)
hne : i ≠ j
⊢ 0 < s.touchpointWeights {i} i j

Tactic:
simpa [sign_eq_one_iff] using s.sign_touchpointWeights_singleton_pos hne

Premises used: Affine.Simplex.sign_touchpointWeights_singleton_pos, sign_eq_one_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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
inst_5 : n.AtLeastTwo
i : Fin (n + 1)
rw :
  (∀ (i_1 : Fin (n + 1)), Membership.mem (γ := Finset (Fin (n + 1))) {i}ᶜ i_1 → 0 < s.touchpointWeights {i} i i_1) ∧
    ∀ i_1 ∉ {i}ᶜ, s.touchpointWeights {i} i i_1 = 0
⊢ s.touchpoint {i} i ∈ (s.faceOpposite i).interior

Tactic:
rw [faceOpposite, ← affineCombination_touchpointWeights,
    s.affineCombination_mem_interior_face_iff_pos _ (s.sum_touchpointWeights _ _)]

Premises used: Affine.Simplex.affineCombination_mem_interior_face_iff_pos, Affine.Simplex.affineCombination_touchpointWeights, Affine.Simplex.sum_touchpointWeights, Affine.Simplex.faceOpposite
-- 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
inst_5 : n.AtLeastTwo
i : Fin (n + 1)
simp : ∀ (i_1 : Fin (n + 1)), ¬i_1 = i → 0 < s.touchpointWeights {i} i i_1
⊢ (∀ (i_1 : Fin (n + 1)), Membership.mem (γ := Finset (Fin (n + 1))) {i}ᶜ i_1 → 0 < s.touchpointWeights {i} i i_1) ∧
    ∀ i_1 ∉ {i}ᶜ, s.touchpointWeights {i} i i_1 = 0

Tactic:
simp only [Finset.mem_compl, Finset.mem_singleton, Decidable.not_not, forall_eq,
    touchpointWeights_eq_zero, and_true]

Premises used: Finset.mem_singleton, and_true, forall_eq, Finset.mem_compl, Affine.Simplex.touchpointWeights_eq_zero, Decidable.not_not
-- 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
inst_5 : n.AtLeastTwo
i j : Fin (n + 1)
hj : ¬j = i
⊢ 0 < s.touchpointWeights {i} i j

Tactic:
s.touchpointWeights_singleton_pos (Ne.symm hj)

Premises used: Ne.symm, Affine.Simplex.touchpointWeights_singleton_pos
-- 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
inst_5 : n.AtLeastTwo
i j : Fin (n + 1)
hj : ¬j = i
⊢ 0 < s.touchpointWeights {i} i j

Tactic:
exact s.touchpointWeights_singleton_pos (Ne.symm hj)

Premises used: Ne.symm, Affine.Simplex.touchpointWeights_singleton_pos
-- 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
inst_5 : n.AtLeastTwo
i j : Fin (n + 1)
hne : i ≠ j
rw : Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (s.excenterWeights {i} i) : SignType) (-1 : SignType)
rw₁ rw₂ : Eq (α := SignType) (-1) (-1)
⊢ Eq (α := SignType) ((SignType.sign : (a : ℝ) → SignType) (s.touchpointWeights {i} j i) : SignType) (-1 : SignType)

Tactic:
rw [(s.excenterExists_singleton i).sign_touchpointWeights hne.symm,
    s.sign_excenterWeights_singleton_neg]

Premises used: Affine.Simplex.sign_excenterWeights_singleton_neg, Ne.symm, Affine.Simplex.ExcenterExists.sign_touchpointWeights, Affine.Simplex.excenterExists_singleton
-- 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
inst_5 : n.AtLeastTwo
i j : Fin (n + 1)
hne : i ≠ j
⊢ s.touchpointWeights {i} j i < 0

Tactic:
simpa [sign_eq_neg_one_iff] using s.sign_touchpointWeights_singleton_neg hne

Premises used: Affine.Simplex.sign_touchpointWeights_singleton_neg, sign_eq_neg_one_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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
inst_5 : n.AtLeastTwo
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
he : s.touchpoint signs i = s.points j
⊢ Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) j 1 = s.touchpointWeights signs i

Tactic:
rw [eq_comm, ← Finset.univ.affineCombination_piSingle ℝ s.points (Finset.mem_univ _),
    affineCombination_eq_touchpoint_iff (Fintype.sum_pi_single' _ _)] at he

Premises used: Finset.mem_univ, Affine.Simplex.points, Real, Finset.univ, eq_comm, Affine.Simplex.affineCombination_eq_touchpoint_iff, Finset.affineCombination_piSingle, Fintype.sum_pi_single'
-- 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
inst_5 : n.AtLeastTwo
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
he : Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) j 1 = s.touchpointWeights signs i
⊢ 1 < n

Tactic:
have : 1 < n := Nat.AtLeastTwo.one_lt
-- 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
inst_5 : n.AtLeastTwo
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
he : Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) j 1 = s.touchpointWeights signs i
this : 1 < n
⊢ 2 < n + 1

Tactic:
lia
-- 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
inst_5 : n.AtLeastTwo
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
he : Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) j 1 = s.touchpointWeights signs i
this : 1 < n
obtain : ∀ (k : Fin (n + 1)) (hki : k ≠ i) (hkj : k ≠ j), False
⊢ False

Tactic:
obtain ⟨k, hki, hkj⟩ : ∃ k, k ≠ i ∧ k ≠ j := Fin.exists_ne_and_ne_of_two_lt i j (by lia)

Premises used: Fin.exists_ne_and_ne_of_two_lt
-- 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
inst_5 : n.AtLeastTwo
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
he : Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) j 1 = s.touchpointWeights signs i
this : 1 < n
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
⊢ Eq (α := SignType)
    ((SignType.sign : (a : ℝ) → SignType) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) j 1 k : ℝ) : SignType)
    ((SignType.sign : (a : ℝ) → SignType) (s.touchpointWeights signs i k) : SignType)

Tactic:
have he' := congr(SignType.sign ($he k))
-- 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
inst_5 : n.AtLeastTwo
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
he : Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) j 1 = s.touchpointWeights signs i
this : 1 < n
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
he' :
  Eq (α := SignType)
    ((SignType.sign : (a : ℝ) → SignType) (Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) j 1 k : ℝ) : SignType)
    ((SignType.sign : (a : ℝ) → SignType) (s.touchpointWeights signs i k) : SignType)
⊢ HSMul.hSMul (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹ (s.excenterWeightsUnnorm signs) k = 0

Tactic:
rw [Pi.single_eq_of_ne hkj, sign_zero, eq_comm, h.sign_touchpointWeights hki.symm,
    sign_eq_zero_iff, excenterWeights] at he'

Premises used: sign_zero, Pi.single_eq_of_ne, Ne.symm, eq_comm, Affine.Simplex.ExcenterExists.sign_touchpointWeights, Affine.Simplex.excenterWeights, sign_eq_zero_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
n : ℕ
inst_4 : NeZero n
s : Simplex ℝ P n
inst_5 : n.AtLeastTwo
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
he : Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) j 1 = s.touchpointWeights signs i
this : 1 < n
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
he' : HSMul.hSMul (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹ (s.excenterWeightsUnnorm signs) k = 0
rw :
  ∀ (h : Ne (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i) 0) (i j : Fin (n + 1))
    (he : Pi.single (M := fun (a : Fin (n + 1)) ↦ ℝ) j 1 = s.touchpointWeights signs i) (this : 1 < n) (k : Fin (n + 1))
    (hki : k ≠ i) (hkj : k ≠ j)
    (he' :
      HSMul.hSMul (α := ℝ) (∑ i : Fin (n + 1), s.excenterWeightsUnnorm signs i)⁻¹ (s.excenterWeightsUnnorm signs) k =
        0),
    False
⊢ False

Tactic:
rw [ExcenterExists] at h

Premises used: Affine.Simplex.ExcenterExists