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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ AffineSubspace.SSameSide (affineSpan ℝ (Set.range (Simplex.faceOpposite t i₁).points)) (Simplex.excenter t {i₂})
    (t.points i₁)

Tactic:
t.sSameSide_excenter_singleton_point h₁₂

Premises used: Affine.Simplex.sSameSide_excenter_singleton_point
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h : {t.points i₂, t.points i₃} = Set.range (Simplex.faceOpposite t i₁).points
⊢ AffineSubspace.SSameSide (affineSpan ℝ {t.points i₂, t.points i₃}) (Simplex.excenter t {i₂}) (t.points i₁)

Tactic:
convert! t.sSameSide_excenter_singleton_point h₁₂

Premises used: Affine.Simplex.sSameSide_excenter_singleton_point
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ AffineSubspace.SSameSide (affineSpan ℝ (Set.range (Simplex.faceOpposite t i₁).points)) (t.points i₁)
    (Simplex.excenter t {i₂})

Tactic:
t.sSameSide_point_excenter_singleton h₁₂

Premises used: Affine.Simplex.sSameSide_point_excenter_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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h : {t.points i₂, t.points i₃} = Set.range (Simplex.faceOpposite t i₁).points
⊢ AffineSubspace.SSameSide (affineSpan ℝ {t.points i₂, t.points i₃}) (t.points i₁) (Simplex.excenter t {i₂})

Tactic:
convert! t.sSameSide_point_excenter_singleton h₁₂

Premises used: Affine.Simplex.sSameSide_point_excenter_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
t : Triangle ℝ P
inst_4 : Fact (Module.finrank ℝ V = 2)
signs : Finset (Fin 3)
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Eq (α := AffineSubspace ℝ P) (affineSpan ℝ (Set.range (Simplex.faceOpposite t i₁).points))
    ((Simplex.exsphere t signs).orthRadius (Simplex.touchpoint t signs i₁))

Tactic:
(t.excenterExists signs).affineSpan_faceOpposite_eq_orthRadius i₁

Premises used: Affine.Simplex.ExcenterExists.affineSpan_faceOpposite_eq_orthRadius, Affine.Triangle.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
t : Triangle ℝ P
inst_4 : Fact (Module.finrank ℝ V = 2)
signs : Finset (Fin 3)
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h : {t.points i₂, t.points i₃} = Set.range (Simplex.faceOpposite t i₁).points
⊢ Eq (α := AffineSubspace ℝ P) (affineSpan ℝ {t.points i₂, t.points i₃})
    ((Simplex.exsphere t signs).orthRadius (Simplex.touchpoint t signs i₁))

Tactic:
convert! (t.excenterExists signs).affineSpan_faceOpposite_eq_orthRadius i₁

Premises used: Affine.Simplex.ExcenterExists.affineSpan_faceOpposite_eq_orthRadius, Affine.Triangle.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
t : Triangle ℝ P
inst_4 : Fact (Module.finrank ℝ V = 2)
signs : Finset (Fin 3)
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Eq (α := Set (Fin 3)) {i₁}ᶜ {i₂, i₃}

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
t : Triangle ℝ P
inst_4 : Fact (Module.finrank ℝ V = 2)
signs : Finset (Fin 3)
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Eq (α := Set (Fin 3)) {i₁}ᶜ {i₂, i₃}

Tactic:
have hc : {i₁}ᶜ = ({i₂, i₃} : Set (Fin 3)) := by 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
t : Triangle ℝ P
inst_4 : Fact (Module.finrank ℝ V = 2)
signs : Finset (Fin 3)
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hc : Eq (α := Set (Fin 3)) {i₁}ᶜ {i₂, i₃}
⊢ {t.points i₂, t.points i₃} = Set.range (Simplex.faceOpposite t i₁).points

Tactic:
simp [Simplex.range_faceOpposite_points, hc, Set.image_insert_eq]

Premises used: Set.image_insert_eq, 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
t : Triangle ℝ P
inst_4 : Fact (Module.finrank ℝ V = 2)
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Eq (α := AffineSubspace ℝ P) (affineSpan ℝ {t.points i₂, t.points i₃})
    ((Simplex.insphere t).orthRadius (Simplex.touchpoint t ∅ i₁))

Tactic:
t.affineSpan_pair_eq_orthRadius ∅ h₁₂ h₁₃ h₂₃

Premises used: Affine.Triangle.affineSpan_pair_eq_orthRadius, EmptyCollection.emptyCollection, Affine.Simplex.insphere
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
rw : Simplex.touchpoint t ∅ i₂ ∈ (Simplex.face t (fs := {i₁, i₃}) ⋯).interior
⊢ Sbtw ℝ (t.points i₁) (Simplex.touchpoint t ∅ i₂) (t.points i₃)

Tactic:
rw [← t.mem_interior_face_iff_sbtw h₁₃]

Premises used: Affine.Simplex.mem_interior_face_iff_sbtw
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Simplex.touchpoint t ∅ i₂ ∈ (Simplex.faceOpposite t i₂).interior

Tactic:
t.touchpoint_empty_mem_interior_faceOpposite i₂

Premises used: Affine.Simplex.touchpoint_empty_mem_interior_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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h : Simplex.face t (fs := {i₁, i₃}) ⋯ = Simplex.faceOpposite t i₂
⊢ Simplex.touchpoint t ∅ i₂ ∈ (Simplex.face t (fs := {i₁, i₃}) ⋯).interior

Tactic:
convert! t.touchpoint_empty_mem_interior_faceOpposite i₂

Premises used: Affine.Simplex.touchpoint_empty_mem_interior_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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Simplex.face t (fs := {i₁, i₃}) ⋯ = Simplex.face t (fs := {i₁, i₃}) ⋯

Tactic:
rfl

Premises used: rfl
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h : Eq (α := Finset (Fin (HAdd.hAdd (α := ℕ) 2 1))) {i₂}ᶜ {i₁, i₃}
⊢ Simplex.face t (fs := {i₁, i₃}) ⋯ = Simplex.face t ⋯

Tactic:
convert! rfl using 2

Premises used: rfl
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Eq (α := Finset (Fin (HAdd.hAdd (α := ℕ) 2 1))) {i₂}ᶜ {i₁, i₃}

Tactic:
decide +revert
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
rw : Simplex.touchpoint t {i₂} i₂ ∈ (Simplex.face t (fs := {i₁, i₃}) ⋯).interior
⊢ Sbtw ℝ (t.points i₁) (Simplex.touchpoint t {i₂} i₂) (t.points i₃)

Tactic:
rw [← t.mem_interior_face_iff_sbtw h₁₃]

Premises used: Affine.Simplex.mem_interior_face_iff_sbtw
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Simplex.touchpoint t {i₂} i₂ ∈ (Simplex.faceOpposite t i₂).interior

Tactic:
t.touchpoint_singleton_mem_interior_faceOpposite i₂

Premises used: Affine.Simplex.touchpoint_singleton_mem_interior_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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
h : Simplex.face t (fs := {i₁, i₃}) ⋯ = Simplex.faceOpposite t i₂
⊢ Simplex.touchpoint t {i₂} i₂ ∈ (Simplex.face t (fs := {i₁, i₃}) ⋯).interior

Tactic:
convert! t.touchpoint_singleton_mem_interior_faceOpposite i₂

Premises used: Affine.Simplex.touchpoint_singleton_mem_interior_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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
rw :
  Sbtw ℝ
    ((Finset.affineCombination ℝ Finset.univ t.points : (a : Fin (2 + 1) → ℝ) → P)
      (Simplex.touchpointWeights t {i₁} i₂))
    (t.points i₃) (t.points i₁)
⊢ Sbtw ℝ (Simplex.touchpoint t {i₁} i₂) (t.points i₃) (t.points i₁)

Tactic:
rw [← Affine.Simplex.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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Eq (α := ℝ) (∑ j : Fin (2 + 1), Simplex.touchpointWeights t {i₁} i₂ j) 1

Tactic:
have hw := t.sum_touchpointWeights {i₁} 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
⊢ Eq (α := Finset (Fin 3)) Finset.univ {i₁, i₂, i₃}

Tactic:
decide +revert
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hw : Eq (α := ℝ) (∑ j : Fin (2 + 1), Simplex.touchpointWeights t {i₁} i₂ j) 1
⊢ Eq (α := ℝ) (∑ j ∈ {i₁, i₂, i₃}, Simplex.touchpointWeights t {i₁} i₂ j) 1

Tactic:
rw [(by clear hw; decide +revert : (Finset.univ : Finset (Fin 3)) = {i₁, i₂, i₃})] at hw
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hw : Eq (α := ℝ) (∑ j ∈ {i₁, i₂, i₃}, Simplex.touchpointWeights t {i₁} i₂ j) 1
⊢ Simplex.touchpointWeights t {i₁} i₂ i₁ + Simplex.touchpointWeights t {i₁} i₂ i₃ = 1

Tactic:
simp only [Nat.reduceAdd, Finset.mem_insert, h₁₂, Finset.mem_singleton, h₁₃, or_self,
    not_false_eq_true, Finset.sum_insert, h₂₃, Simplex.touchpointWeights_eq_zero,
    Finset.sum_singleton, zero_add] at hw

Premises used: Finset.mem_singleton, Nat.reduceAdd, Finset.mem_insert, zero_add, Finset.sum_singleton, or_self, Affine.Simplex.touchpointWeights_eq_zero, Finset.sum_insert, not_false_eq_true
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hw : Simplex.touchpointWeights t {i₁} i₂ i₁ + Simplex.touchpointWeights t {i₁} i₂ i₃ = 1
h :
  ∀ (i : Fin (HAdd.hAdd (α := ℕ) 2 1)),
    Simplex.touchpointWeights t {i₁} i₂ i =
      Finset.affineCombinationLineMapWeights i₁ i₃ (Simplex.touchpointWeights t {i₁} i₂ i₃) i
⊢ Simplex.touchpointWeights t {i₁} i₂ =
    Finset.affineCombinationLineMapWeights i₁ i₃ (Simplex.touchpointWeights t {i₁} i₂ i₃)

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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
i : Fin (HAdd.hAdd (α := ℕ) 2 1)
⊢ i = i₁ ∨ i = i₂ ∨ i = i₃

Tactic:
decide +revert
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hw : Simplex.touchpointWeights t {i₁} i₂ i₁ + Simplex.touchpointWeights t {i₁} i₂ i₃ = 1
i : Fin (HAdd.hAdd (α := ℕ) 2 1)
⊢ i = i₁ ∨ i = i₂ ∨ i = i₃

Tactic:
have h : i = i₁ ∨ i = i₂ ∨ i = i₃ := by clear hw; decide +revert
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hw : Simplex.touchpointWeights t {i₁} i₂ i₁ + Simplex.touchpointWeights t {i₁} i₂ i₃ = 1
i : Fin (HAdd.hAdd (α := ℕ) 2 1)
h : i = i₁ ∨ i = i₂ ∨ i = i₃
h₁ :
  ∀ (h₁₂ : i ≠ i₂) (h₁₃ : i ≠ i₃)
    (hw : Simplex.touchpointWeights t {i} i₂ i + Simplex.touchpointWeights t {i} i₂ i₃ = 1),
    Simplex.touchpointWeights t {i} i₂ i =
      Finset.affineCombinationLineMapWeights i i₃ (Simplex.touchpointWeights t {i} i₂ i₃) i
h₂ :
  ∀ (h₁₂ : i₁ ≠ i) (h₂₃ : i ≠ i₃)
    (hw : Simplex.touchpointWeights t {i₁} i i₁ + Simplex.touchpointWeights t {i₁} i i₃ = 1),
    Simplex.touchpointWeights t {i₁} i i =
      Finset.affineCombinationLineMapWeights i₁ i₃ (Simplex.touchpointWeights t {i₁} i i₃) i
h₃ :
  ∀ (h₁₃ : i₁ ≠ i) (h₂₃ : i₂ ≠ i)
    (hw : Simplex.touchpointWeights t {i₁} i₂ i₁ + Simplex.touchpointWeights t {i₁} i₂ i = 1),
    Simplex.touchpointWeights t {i₁} i₂ i =
      Finset.affineCombinationLineMapWeights i₁ i (Simplex.touchpointWeights t {i₁} i₂ i) i
⊢ Simplex.touchpointWeights t {i₁} i₂ i =
    Finset.affineCombinationLineMapWeights i₁ i₃ (Simplex.touchpointWeights t {i₁} i₂ i₃) i

Tactic:
rcases h with rfl | rfl | rfl

Premises used: rfl
-- 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
t : Triangle ℝ P
i₂ i₃ : Fin 3
h₂₃ : i₂ ≠ i₃
i : Fin (HAdd.hAdd (α := ℕ) 2 1)
h₁₂ : i ≠ i₂
h₁₃ : i ≠ i₃
hw : Simplex.touchpointWeights t {i} i₂ i + Simplex.touchpointWeights t {i} i₂ i₃ = 1
h : Simplex.touchpointWeights t {i} i₂ i = 1 - Simplex.touchpointWeights t {i} i₂ i₃
⊢ Simplex.touchpointWeights t {i} i₂ i =
    Finset.affineCombinationLineMapWeights i i₃ (Simplex.touchpointWeights t {i} i₂ i₃) i

Tactic:
rw [Finset.affineCombinationLineMapWeights_apply_left h₁₃]

Premises used: Finset.affineCombinationLineMapWeights_apply_left
-- 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
t : Triangle ℝ P
i₂ i₃ : Fin 3
h₂₃ : i₂ ≠ i₃
i : Fin (HAdd.hAdd (α := ℕ) 2 1)
h₁₂ : i ≠ i₂
h₁₃ : i ≠ i₃
hw : Simplex.touchpointWeights t {i} i₂ i + Simplex.touchpointWeights t {i} i₂ i₃ = 1
⊢ Simplex.touchpointWeights t {i} i₂ i = 1 - Simplex.touchpointWeights t {i} i₂ i₃

Tactic:
simp [← hw]
-- 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
t : Triangle ℝ P
i₁ i₃ : Fin 3
h₁₃ : i₁ ≠ i₃
i : Fin (HAdd.hAdd (α := ℕ) 2 1)
h₁₂ : i₁ ≠ i
h₂₃ : i ≠ i₃
hw : Simplex.touchpointWeights t {i₁} i i₁ + Simplex.touchpointWeights t {i₁} i i₃ = 1
⊢ Simplex.touchpointWeights t {i₁} i i =
    Finset.affineCombinationLineMapWeights i₁ i₃ (Simplex.touchpointWeights t {i₁} i i₃) i

Tactic:
simp [h₁₂.symm, h₂₃]

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
t : Triangle ℝ P
i₁ i₂ : Fin 3
h₁₂ : i₁ ≠ i₂
i : Fin (HAdd.hAdd (α := ℕ) 2 1)
h₁₃ : i₁ ≠ i
h₂₃ : i₂ ≠ i
hw : Simplex.touchpointWeights t {i₁} i₂ i₁ + Simplex.touchpointWeights t {i₁} i₂ i = 1
⊢ Simplex.touchpointWeights t {i₁} i₂ i =
    Finset.affineCombinationLineMapWeights i₁ i (Simplex.touchpointWeights t {i₁} i₂ i) i

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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hw : Simplex.touchpointWeights t {i₁} i₂ i₁ + Simplex.touchpointWeights t {i₁} i₂ i₃ = 1
⊢ Simplex.touchpointWeights t {i₁} i₂ =
    Finset.affineCombinationLineMapWeights i₁ i₃ (Simplex.touchpointWeights t {i₁} i₂ i₃)

Tactic:
have h : t.touchpointWeights {i₁} i₂ =
      Finset.affineCombinationLineMapWeights i₁ i₃ (t.touchpointWeights {i₁} i₂ i₃) := by
    ext i
    have h : i = i₁ ∨ i = i₂ ∨ i = i₃ := by clear hw; decide +revert
    rcases h with rfl | rfl | rfl
    · rw [Finset.affineCombinationLineMapWeights_apply_left h₁₃]
      simp [← hw]
    · simp [h₁₂.symm, h₂₃]
    · 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hw : Simplex.touchpointWeights t {i₁} i₂ i₁ + Simplex.touchpointWeights t {i₁} i₂ i₃ = 1
h :
  Simplex.touchpointWeights t {i₁} i₂ =
    Finset.affineCombinationLineMapWeights i₁ i₃ (Simplex.touchpointWeights t {i₁} i₂ i₃)
rw :
  t.points i₁ ≠ t.points i₃ ∧
    Membership.mem.{u_2, u_2} (α := P) (γ := Set P)
      (Set.image (α := ℝ) (⇑(AffineMap.lineMap (t.points i₁) (t.points i₃)) : (a : ℝ) → P) (Set.Ioi 1))
      ((AffineMap.lineMap (t.points i₁) (t.points i₃) : (a : ℝ) → P) (Simplex.touchpointWeights t {i₁} i₂ i₃) : P)
⊢ Sbtw ℝ
    ((Finset.affineCombination ℝ Finset.univ t.points : (a : Fin (2 + 1) → ℝ) → P)
      (Simplex.touchpointWeights t {i₁} i₂))
    (t.points i₃) (t.points i₁)

Tactic:
rw [h, Finset.univ.affineCombination_affineCombinationLineMapWeights _ (Finset.mem_univ _)
    (Finset.mem_univ _), sbtw_iff_right_ne_and_left_mem_image_Ioi]

Premises used: Finset.mem_univ, Finset.univ, sbtw_iff_right_ne_and_left_mem_image_Ioi, Finset.affineCombination_affineCombinationLineMapWeights
-- 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
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
hw : Simplex.touchpointWeights t {i₁} i₂ i₁ + Simplex.touchpointWeights t {i₁} i₂ i₃ = 1
h :
  Simplex.touchpointWeights t {i₁} i₂ =
    Finset.affineCombinationLineMapWeights i₁ i₃ (Simplex.touchpointWeights t {i₁} i₂ i₃)
⊢ t.points i₁ ≠ t.points i₃ ∧
    Membership.mem.{u_2, u_2} (α := P) (γ := Set P)
      (Set.image (α := ℝ) (⇑(AffineMap.lineMap (t.points i₁) (t.points i₃)) : (a : ℝ) → P) (Set.Ioi 1))
      ((AffineMap.lineMap (t.points i₁) (t.points i₃) : (a : ℝ) → P) (Simplex.touchpointWeights t {i₁} i₂ i₃) : P)

Tactic:
simp [t.independent.injective.ne h₁₃, ← hw, t.touchpointWeights_singleton_neg h₁₂]

Premises used: Function.Injective.ne, AffineIndependent.injective, Affine.Simplex.touchpointWeights_singleton_neg, Affine.Simplex.independent
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
⊢ Eq.{u_2 + 1} (α := (c : P) → (R : ℝ) → (x : P) → P) inversion fun (c : P) (R : ℝ) (x : P) ↦
    HPow.hPow (β := ℕ) (R / dist x c) 2 • (x -ᵥ c) +ᵥ c

Tactic:
rfl

Premises used: EuclideanGeometry.inversion, rfl
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
c : P
R : ℝ
x : P
⊢ inversion c R x = (lineMap c x : (a : ℝ) → P) (HPow.hPow (β := ℕ) (R / dist x c) 2)

Tactic:
rfl

Premises used: EuclideanGeometry.inversion, rfl
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
c : P
R : ℝ
x : P
⊢ inversion c R x -ᵥ c = HPow.hPow (β := ℕ) (R / dist x c) 2 • (x -ᵥ c)

Tactic:
vadd_vsub _ _

Premises used: EuclideanGeometry.inversion, vadd_vsub
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
c : P
R : ℝ
⊢ inversion c R c = c

Tactic:
simp [inversion]

Premises used: EuclideanGeometry.inversion
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
c x : P
⊢ inversion c 0 x = c

Tactic:
simp [inversion]

Premises used: EuclideanGeometry.inversion
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
c : P
a R : ℝ
x : P
⊢ inversion c (a * R) x = (homothety c (HPow.hPow (β := ℕ) a 2) : (a : P) → P) (inversion c R x)

Tactic:
simp only [inversion_eq_lineMap, ← homothety_eq_lineMap, ← homothety_mul_apply, mul_div_assoc,
    mul_pow]

Premises used: mul_div_assoc, mul_pow, EuclideanGeometry.inversion_eq_lineMap, AffineMap.homothety_eq_lineMap, AffineMap.homothety_mul_apply
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
c x : P
inl : inversion x (dist x x) x = x
inr : ∀ (hne : x ≠ c), inversion c (dist x c) x = x
⊢ inversion c (dist x c) x = x

Tactic:
rcases eq_or_ne x c with (rfl | hne)

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Geometry.Euclidean.Inversion.Basic
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
x : P
⊢ inversion x (dist x x) x = x

Tactic:
apply inversion_self

Premises used: EuclideanGeometry.inversion_self