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)
hij : s.touchpoint signs i = s.touchpoint signs j
hne : ¬i = j
hn1 : ¬n = 1
this :
  Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))ᗮ (s.excenter signs -ᵥ s.touchpoint signs i)
h' : Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points)) (s.excenter signs -ᵥ s.touchpoint signs i)
h0 : s.excenter signs -ᵥ s.touchpoint signs i = 0
⊢ s.exradius signs = 0

Tactic:
rw [← norm_eq_zero, ← dist_eq_norm_vsub, h.dist_excenter] at h0

Premises used: norm_eq_zero, Affine.Simplex.ExcenterExists.dist_excenter, dist_eq_norm_vsub
-- 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)
hij : s.touchpoint signs i = s.touchpoint signs j
hne : ¬i = j
hn1 : ¬n = 1
this :
  Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))ᗮ (s.excenter signs -ᵥ s.touchpoint signs i)
h' : Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points)) (s.excenter signs -ᵥ s.touchpoint signs i)
h0 : s.exradius signs = 0
⊢ False

Tactic:
h.exradius_pos.ne' h0

Premises used: LT.lt.ne', Affine.Simplex.ExcenterExists.exradius_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
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hij : s.touchpoint signs i = s.touchpoint signs j
hne : ¬i = j
hn1 : ¬n = 1
this :
  Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))ᗮ (s.excenter signs -ᵥ s.touchpoint signs i)
h' : Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points)) (s.excenter signs -ᵥ s.touchpoint signs i)
h0 : s.exradius signs = 0
⊢ False

Tactic:
exact h.exradius_pos.ne' h0

Premises used: LT.lt.ne', Affine.Simplex.ExcenterExists.exradius_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
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hij : s.touchpoint signs i = s.touchpoint signs j
hne : ¬i = j
hn1 : ¬n = 1
neg :
  Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))ᗮ (s.excenter signs -ᵥ s.touchpoint signs i)
⊢ False

Tactic:
suffices s.excenter signs -ᵥ s.touchpoint signs i ∈ (vectorSpan ℝ (Set.range s.points))ᗮ by
      have h' : s.excenter signs -ᵥ s.touchpoint signs i ∈ (vectorSpan ℝ (Set.range s.points)) := by
        rw [← direction_affineSpan]
        exact AffineSubspace.vsub_mem_direction h.excenter_mem_affineSpan_range
          (s.touchpoint_mem_affineSpan_simplex _ _)
      have h0 : s.excenter signs -ᵥ s.touchpoint signs i = 0 := by
        rw [← Submodule.mem_bot ℝ,
          ← Submodule.inf_orthogonal_eq_bot (vectorSpan ℝ (Set.range s.points))]
        exact ⟨h', this⟩
      rw [← norm_eq_zero, ← dist_eq_norm_vsub, h.dist_excenter] at h0
      exact h.exradius_pos.ne' h0
-- 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)
hij : s.touchpoint signs i = s.touchpoint signs j
hne : ¬i = j
hn1 : ¬n = 1
⊢ 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
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hij : s.touchpoint signs i = s.touchpoint signs j
hne : ¬i = j
hn1 : ¬n = 1
neg :
  ∀ (k : Fin (n + 1)) (hki : k ≠ i) (hkj : k ≠ j),
    Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))ᗮ (s.excenter signs -ᵥ s.touchpoint signs i)
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))ᗮ (s.excenter signs -ᵥ s.touchpoint signs i)

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
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hij : s.touchpoint signs i = s.touchpoint signs j
hne : ¬i = j
hn1 : ¬n = 1
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
simp : Set.range s.points = s.points '' ({i} ∩ {j})ᶜ
⊢ Set.range s.points = Set.range (s.faceOpposite i).points ∪ Set.range (s.faceOpposite j).points

Tactic:
simp only [range_faceOpposite_points, ← Set.image_union, ← Set.compl_inter]

Premises used: Set.compl_inter, Affine.Simplex.range_faceOpposite_points, Set.image_union
-- 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)
hij : s.touchpoint signs i = s.touchpoint signs j
hne : ¬i = j
hn1 : ¬n = 1
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
⊢ Set.range s.points = s.points '' Set.univ

Tactic:
Set.image_univ.symm

Premises used: Set.image_univ, 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)
hij : s.touchpoint signs i = s.touchpoint signs j
hne : ¬i = j
hn1 : ¬n = 1
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
h₁ : Eq (α := Set (Fin (n + 1))) ({i} ∩ {j})ᶜ Set.univ
⊢ Set.range s.points = s.points '' ({i} ∩ {j})ᶜ

Tactic:
convert! Set.image_univ.symm

Premises used: Set.image_univ, 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)
hij : s.touchpoint signs i = s.touchpoint signs j
hne : ¬i = j
hn1 : ¬n = 1
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
⊢ Eq (α := Set (Fin (n + 1))) ({i} ∩ {j})ᶜ Set.univ

Tactic:
simp [Ne.symm hne]

Premises used: 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
signs : Finset (Fin (n + 1))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hij : s.touchpoint signs i = s.touchpoint signs j
hne : ¬i = j
hn1 : ¬n = 1
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
⊢ Set.range s.points = Set.range (s.faceOpposite i).points ∪ Set.range (s.faceOpposite j).points

Tactic:
have hu : Set.range s.points =
        Set.range (s.faceOpposite i).points ∪ Set.range (s.faceOpposite j).points := by
      simp only [range_faceOpposite_points, ← Set.image_union, ← Set.compl_inter]
      convert! Set.image_univ.symm
      simp [Ne.symm 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)
hij : s.touchpoint signs i = s.touchpoint signs j
hne : ¬i = j
hn1 : ¬n = 1
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
hu : Set.range s.points = Set.range (s.faceOpposite i).points ∪ Set.range (s.faceOpposite j).points
⊢ Membership.mem (γ := Set (Fin (n + 1))) {i}ᶜ k

Tactic:
simp [hki]
-- 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)
hij : s.touchpoint signs i = s.touchpoint signs j
hne : ¬i = j
hn1 : ¬n = 1
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
hu : Set.range s.points = Set.range (s.faceOpposite i).points ∪ Set.range (s.faceOpposite j).points
⊢ Membership.mem (γ := Set (Fin (n + 1))) {j}ᶜ k

Tactic:
simp [hkj]
-- 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)
hij : s.touchpoint signs i = s.touchpoint signs j
hne : ¬i = j
hn1 : ¬n = 1
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
hu : Set.range s.points = Set.range (s.faceOpposite i).points ∪ Set.range (s.faceOpposite j).points
neg :
  Membership.mem (γ := Submodule ℝ V) ((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ (vectorSpan ℝ (s.points '' {j}ᶜ))ᗮ)
    (s.excenter signs -ᵥ s.touchpoint signs i)
⊢ Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (Set.range s.points))ᗮ (s.excenter signs -ᵥ s.touchpoint signs i)

Tactic:
rw [hu, range_faceOpposite_points, range_faceOpposite_points,
      AffineSubspace.vectorSpan_union_of_mem_of_mem ℝ (p := s.points k)
        (Set.mem_image_of_mem _ (by simp [hki])) (Set.mem_image_of_mem _ (by simp [hkj])),
      ← Submodule.inf_orthogonal]

Premises used: Real, AffineSubspace.vectorSpan_union_of_mem_of_mem, Submodule.inf_orthogonal, Set.mem_image_of_mem, Affine.Simplex.range_faceOpposite_points
-- 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)
hij : s.touchpoint signs i = s.touchpoint signs j
hne : ¬i = j
hn1 : ¬n = 1
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
hu : Set.range s.points = Set.range (s.faceOpposite i).points ∪ Set.range (s.faceOpposite j).points
⊢ Membership.mem (γ := Submodule ℝ V) ((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ (vectorSpan ℝ (s.points '' {j}ᶜ))ᗮ)
    (s.excenter signs -ᵥ s.touchpoint signs i)

Tactic:
⟨?_, ?_⟩

Premises used: Set.Mem, setOf, Set.inter, 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)
hij : s.touchpoint signs i = s.touchpoint signs j
hne : ¬i = j
hn1 : ¬n = 1
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
hu : Set.range s.points = Set.range (s.faceOpposite i).points ∪ Set.range (s.faceOpposite j).points
neg : s.excenter signs -ᵥ s.touchpoint signs i ∈ (↑(vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ : Set V)
neg₁ : s.excenter signs -ᵥ s.touchpoint signs i ∈ (↑(vectorSpan ℝ (s.points '' {j}ᶜ))ᗮ : Set V)
⊢ Membership.mem (γ := Submodule ℝ V) ((vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ (vectorSpan ℝ (s.points '' {j}ᶜ))ᗮ)
    (s.excenter signs -ᵥ s.touchpoint signs i)

Tactic:
refine ⟨?_, ?_⟩
-- 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)
hij : s.touchpoint signs i = s.touchpoint signs j
hne : ¬i = j
hn1 : ¬n = 1
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
hu : Set.range s.points = Set.range (s.faceOpposite i).points ∪ Set.range (s.faceOpposite j).points
neg :
  s.excenter signs -ᵥ s.touchpoint signs i ∈
    (↑(AffineSubspace.direction (affineSpan ℝ (Set.range (s.faceOpposite i).points)))ᗮ : Set V)
⊢ s.excenter signs -ᵥ s.touchpoint signs i ∈ (↑(vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ : Set V)

Tactic:
rw [← direction_affineSpan, ← range_faceOpposite_points]

Premises used: direction_affineSpan, Affine.Simplex.range_faceOpposite_points
-- 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)
hij : s.touchpoint signs i = s.touchpoint signs j
hne : ¬i = j
hn1 : ¬n = 1
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
hu : Set.range s.points = Set.range (s.faceOpposite i).points ∪ Set.range (s.faceOpposite j).points
⊢ s.excenter signs -ᵥ s.touchpoint signs i ∈
    (↑(AffineSubspace.direction (affineSpan ℝ (Set.range (s.faceOpposite i).points)))ᗮ : Set V)

Tactic:
vsub_orthogonalProjection_mem_direction_orthogonal _ _

Premises used: EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal, Set.Mem, setOf, Affine.Simplex.touchpoint
-- 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)
hij : s.touchpoint signs i = s.touchpoint signs j
hne : ¬i = j
hn1 : ¬n = 1
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
hu : Set.range s.points = Set.range (s.faceOpposite i).points ∪ Set.range (s.faceOpposite j).points
⊢ s.excenter signs -ᵥ s.touchpoint signs i ∈
    (↑(AffineSubspace.direction (affineSpan ℝ (Set.range (s.faceOpposite i).points)))ᗮ : Set V)

Tactic:
exact vsub_orthogonalProjection_mem_direction_orthogonal _ _

Premises used: EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal
-- 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)
hij : s.touchpoint signs i = s.touchpoint signs j
hne : ¬i = j
hn1 : ¬n = 1
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
hu : Set.range s.points = Set.range (s.faceOpposite i).points ∪ Set.range (s.faceOpposite j).points
neg :
  s.excenter signs -ᵥ s.touchpoint signs j ∈
    (↑(AffineSubspace.direction (affineSpan ℝ (Set.range (s.faceOpposite j).points)))ᗮ : Set V)
⊢ s.excenter signs -ᵥ s.touchpoint signs i ∈ (↑(vectorSpan ℝ (s.points '' {j}ᶜ))ᗮ : Set V)

Tactic:
rw [hij, ← direction_affineSpan, ← range_faceOpposite_points]

Premises used: direction_affineSpan, Affine.Simplex.range_faceOpposite_points
-- 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)
hij : s.touchpoint signs i = s.touchpoint signs j
hne : ¬i = j
hn1 : ¬n = 1
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
hu : Set.range s.points = Set.range (s.faceOpposite i).points ∪ Set.range (s.faceOpposite j).points
⊢ s.excenter signs -ᵥ s.touchpoint signs j ∈
    (↑(AffineSubspace.direction (affineSpan ℝ (Set.range (s.faceOpposite j).points)))ᗮ : Set V)

Tactic:
vsub_orthogonalProjection_mem_direction_orthogonal _ _

Premises used: EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal, Set.Mem, setOf, Affine.Simplex.touchpoint
-- 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)
hij : s.touchpoint signs i = s.touchpoint signs j
hne : ¬i = j
hn1 : ¬n = 1
k : Fin (n + 1)
hki : k ≠ i
hkj : k ≠ j
hu : Set.range s.points = Set.range (s.faceOpposite i).points ∪ Set.range (s.faceOpposite j).points
⊢ s.excenter signs -ᵥ s.touchpoint signs j ∈
    (↑(AffineSubspace.direction (affineSpan ℝ (Set.range (s.faceOpposite j).points)))ᗮ : Set V)

Tactic:
exact vsub_orthogonalProjection_mem_direction_orthogonal _ _

Premises used: EuclideanGeometry.vsub_orthogonalProjection_mem_direction_orthogonal
-- 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
⊢ Function.Injective (s.touchpoint ∅)

Tactic:
s.excenterExists_empty.touchpoint_injective

Premises used: Affine.Simplex.ExcenterExists.touchpoint_injective, 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))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hne : i ≠ j
⊢ s.touchpoint signs i ∉ affineSpan ℝ (Set.range (s.faceOpposite j).points)

Tactic:
fun hm ↦ h.touchpoint_injective.ne hne
    ((h.isTangentAt_touchpoint j).eq_of_mem_of_mem (h.touchpoint_mem_exsphere i) hm)

Premises used: EuclideanGeometry.Sphere.IsTangentAt.eq_of_mem_of_mem, Affine.Simplex.ExcenterExists.isTangentAt_touchpoint, Function.Injective.ne, Affine.Simplex.ExcenterExists.touchpoint_mem_exsphere, Affine.Simplex.ExcenterExists.touchpoint_injective, 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
i j : Fin (n + 1)
hne : i ≠ j
⊢ s.touchpoint ∅ i ∉ affineSpan ℝ (Set.range (s.faceOpposite j).points)

Tactic:
s.excenterExists_empty.touchpoint_notMem_affineSpan_of_ne hne

Premises used: Affine.Simplex.ExcenterExists.touchpoint_notMem_affineSpan_of_ne, 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))
h : s.ExcenterExists signs
i j : Fin (n + 1)
hne : i ≠ j
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) r
⊢ ContinuousOn (Y := SignType)
    (fun (t : ℝ) ↦
      (SignType.sign : (a : ℝ) → SignType)
        ((s.signedInfDist j : (a : P) → ℝ)
            ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i) : (a : ℝ) → P) t : P) :
          ℝ))
    (Set.Icc 0 1)

Tactic:
continuousOn_of_forall_continuousAt
      fun t ht ↦ ((continuousAt_sign_of_ne_zero ?_).comp
        (((s.signedInfDist j).cont.comp ?_).continuousAt))

Premises used: continuousOn_of_forall_continuousAt, Continuous.comp, Continuous.continuousAt, Affine.Simplex.signedInfDist, ContinuousAt.comp, continuousAt_sign_of_ne_zero, ContinuousAffineMap.cont
-- 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
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) r
refine_1 :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t),
    Ne (α := ℝ)
      ((s.signedInfDist j : (a : P) → ℝ)
          ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i) : (a : ℝ) → P) t : P) :
        ℝ)
      (0 : ℝ)
refine_2 :
  ∀ (t : ℝ) (ht : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t),
    Continuous.{0, u_2} (X := ℝ) (Y := P) (⇑(AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i)) : (a : ℝ) → P)
⊢ ContinuousOn (Y := SignType)
    (fun (t : ℝ) ↦
      (SignType.sign : (a : ℝ) → SignType)
        ((s.signedInfDist j : (a : P) → ℝ)
            ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i) : (a : ℝ) → P) t : P) :
          ℝ))
    (Set.Icc 0 1)

Tactic:
refine continuousOn_of_forall_continuousAt
      fun t ht ↦ ((continuousAt_sign_of_ne_zero ?_).comp
        (((s.signedInfDist j).cont.comp ?_).continuousAt))

Premises used: continuousOn_of_forall_continuousAt, Continuous.comp, Continuous.continuousAt, Affine.Simplex.signedInfDist, ContinuousAt.comp, continuousAt_sign_of_ne_zero, ContinuousAffineMap.cont
-- 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
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) r
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t
h0 :
  Eq (α := ℝ)
    ((s.signedInfDist j : (a : P) → ℝ)
        ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i) : (a : ℝ) → P) t : P) :
      ℝ)
    (0 : ℝ)
refine_1 :
  ∀
    (h0 :
      dist.{u_2} (α := P) ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i) : (a : ℝ) → P) t : P)
          ((↑(((s.faceOpposite j).orthogonalProjectionSpan :
                    (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite j).points)))
                  ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i) : (a : ℝ) → P) t)) :
              P) :
            P) =
        0),
    False
refine_1₁ :
  ∀
    (h0 :
      Eq (α := ℝ)
        (|(s.signedInfDist j : (a : P) → ℝ)
              ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i) : (a : ℝ) → P) t : P)| :
          ℝ)
        (0 : ℝ)),
    Membership.mem (α := P) (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range s.points))
      ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i) : (a : ℝ) → P) t : P)
⊢ False

Tactic:
rw [← abs_eq_zero, abs_signedInfDist_eq_dist_of_mem_affineSpan_range] at h0

Premises used: abs_eq_zero, Affine.Simplex.abs_signedInfDist_eq_dist_of_mem_affineSpan_range
-- 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
r : ℝ
hr : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) r
t : ℝ
ht : Membership.mem (γ := Set ℝ) (Set.Icc 0 1) t
h0 :
  dist.{u_2} (α := P) ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i) : (a : ℝ) → P) t : P)
      ((↑(((s.faceOpposite j).orthogonalProjectionSpan :
                (a : P) → ↥(affineSpan ℝ (Set.range (s.faceOpposite j).points)))
              ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i) : (a : ℝ) → P) t)) :
          P) :
        P) =
    0
⊢ Membership.mem (α := P) (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (s.faceOpposite j).points))
    ((AffineMap.lineMap (s.excenter signs) (s.touchpoint signs i) : (a : ℝ) → P) t : P)

Tactic:
rw [orthogonalProjectionSpan, dist_orthogonalProjection_eq_zero_iff] at h0

Premises used: Affine.Simplex.orthogonalProjectionSpan, EuclideanGeometry.dist_orthogonalProjection_eq_zero_iff