awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Angle.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
signs : Finset (Fin 3)
h₁ : ∡ (t.points i₂) (t.points i₁) (excenter t signs) = ∡ (excenter t signs) (t.points i₁) (t.points i₃)
h₂ : ∡ (t.points i₃) (t.points i₂) (excenter t signs) = ∡ (excenter t signs) (t.points i₂) (t.points i₁)
h₁' : excenter t signs = excenter t {i₁}
h₂' : excenter t {i₁} = excenter t {i₂}
⊢ False

Tactic:
t.excenter_singleton_injective.ne h₁₂ h₂'

Premises used: Affine.Simplex.excenter_singleton_injective, Function.Injective.ne
-- Module: Mathlib.Geometry.Euclidean.Angle.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
signs : Finset (Fin 3)
h₁ : ∡ (t.points i₂) (t.points i₁) (excenter t signs) = ∡ (excenter t signs) (t.points i₁) (t.points i₃)
h₂ : ∡ (t.points i₃) (t.points i₂) (excenter t signs) = ∡ (excenter t signs) (t.points i₂) (t.points i₁)
h₁' : excenter t signs = excenter t {i₁}
h₂' : excenter t {i₁} = excenter t {i₂}
⊢ False

Tactic:
exact t.excenter_singleton_injective.ne h₁₂ h₂'

Premises used: Affine.Simplex.excenter_singleton_injective, Function.Injective.ne
-- Module: Mathlib.Geometry.Euclidean.Angle.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
p : P
h₁ : ∡ (t.points i₂) (t.points i₁) p = ∡ p (t.points i₁) (t.points i₃)
h₂ : ∡ (t.points i₃) (t.points i₂) p = ∡ p (t.points i₂) (t.points i₁) + (↑π : Real.Angle)
rw rw₁ :
  HSMul.hSMul (α := ℤ) 2 (∡ p (t.points i₁) (t.points i₃)) = HSMul.hSMul (α := ℤ) 2 (∡ p (t.points i₁) (t.points i₃))
⊢ HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₂) (t.points i₁) p) = HSMul.hSMul (α := ℤ) 2 (∡ p (t.points i₁) (t.points i₃))

Tactic:
rw [h₁]
-- Module: Mathlib.Geometry.Euclidean.Angle.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
p : P
h₁ : ∡ (t.points i₂) (t.points i₁) p = ∡ p (t.points i₁) (t.points i₃)
h₂ : ∡ (t.points i₃) (t.points i₂) p = ∡ p (t.points i₂) (t.points i₁) + (↑π : Real.Angle)
rw :
  HSMul.hSMul (α := ℤ) 2 (∡ p (t.points i₂) (t.points i₁) + (↑π : Real.Angle)) =
    HSMul.hSMul (α := ℤ) 2 (∡ p (t.points i₂) (t.points i₁))
⊢ HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₃) (t.points i₂) p) = HSMul.hSMul (α := ℤ) 2 (∡ p (t.points i₂) (t.points i₁))

Tactic:
rw [h₂]
-- Module: Mathlib.Geometry.Euclidean.Angle.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
p : P
h₁ : ∡ (t.points i₂) (t.points i₁) p = ∡ p (t.points i₁) (t.points i₃)
h₂ : ∡ (t.points i₃) (t.points i₂) p = ∡ p (t.points i₂) (t.points i₁) + (↑π : Real.Angle)
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p (t.points i₂) (t.points i₁) + (↑π : Real.Angle)) =
    HSMul.hSMul (α := ℤ) 2 (∡ p (t.points i₂) (t.points i₁))

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Angle.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
p : P
h₁ : ∡ (t.points i₂) (t.points i₁) p = ∡ p (t.points i₁) (t.points i₃)
h₂ : ∡ (t.points i₃) (t.points i₂) p = ∡ p (t.points i₂) (t.points i₁) + (↑π : Real.Angle)
obtain :
  ∀ (signs : Finset (Fin 3))
    (h₁ : ∡ (t.points i₂) (t.points i₁) (excenter t signs) = ∡ (excenter t signs) (t.points i₁) (t.points i₃))
    (h₂ :
      ∡ (t.points i₃) (t.points i₂) (excenter t signs) =
        ∡ (excenter t signs) (t.points i₂) (t.points i₁) + (↑π : Real.Angle)),
    excenter t signs = excenter t {i₁}
⊢ p = excenter t {i₁}

Tactic:
obtain ⟨signs, rfl⟩ := t.eq_excenter_of_two_zsmul_oangle_eq h₁₂ h₁₃ h₂₃ (by rw [h₁])
    (by rw [h₂]; simp)

Premises used: Affine.Triangle.eq_excenter_of_two_zsmul_oangle_eq, rfl
-- Module: Mathlib.Geometry.Euclidean.Angle.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
signs : Finset (Fin 3)
h₁ : ∡ (t.points i₂) (t.points i₁) (excenter t signs) = ∡ (excenter t signs) (t.points i₁) (t.points i₃)
h₂ :
  ∡ (t.points i₃) (t.points i₂) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₂) (t.points i₁) + (↑π : Real.Angle)
⊢ excenter t signs = incenter t ∨ excenter t signs = excenter t {i₁}

Tactic:
have h₁' := t.eq_incenter_or_eq_excenter_singleton_of_oangle_eq h₁₂ h₁₃ h₂₃ h₁
-- Module: Mathlib.Geometry.Euclidean.Angle.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
signs : Finset (Fin 3)
h₁ : ∡ (t.points i₂) (t.points i₁) (excenter t signs) = ∡ (excenter t signs) (t.points i₁) (t.points i₃)
h₂ :
  ∡ (t.points i₃) (t.points i₂) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₂) (t.points i₁) + (↑π : Real.Angle)
h₁' : excenter t signs = incenter t ∨ excenter t signs = excenter t {i₁}
⊢ excenter t signs = excenter t {i₃} ∨ excenter t signs = excenter t {i₁}

Tactic:
have h₂' := t.eq_excenter_singleton_of_oangle_eq_add_pi h₂₃ h₁₂.symm h₁₃.symm h₂
-- Module: Mathlib.Geometry.Euclidean.Angle.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
signs : Finset (Fin 3)
h₁ : ∡ (t.points i₂) (t.points i₁) (excenter t signs) = ∡ (excenter t signs) (t.points i₁) (t.points i₃)
h₂ :
  ∡ (t.points i₃) (t.points i₂) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₂) (t.points i₁) + (↑π : Real.Angle)
h₁' : excenter t signs = incenter t ∨ excenter t signs = excenter t {i₁}
h₂' : excenter t signs = excenter t {i₃} ∨ excenter t signs = excenter t {i₁}
inl : ∀ (h₁' : excenter t signs = incenter t), excenter t signs = excenter t {i₁}
inr : ∀ (h₁' : excenter t signs = excenter t {i₁}), excenter t signs = excenter t {i₁}
⊢ excenter t signs = excenter t {i₁}

Tactic:
rcases h₁' with h₁' | h₁'
-- Module: Mathlib.Geometry.Euclidean.Angle.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
signs : Finset (Fin 3)
h₁ : ∡ (t.points i₂) (t.points i₁) (excenter t signs) = ∡ (excenter t signs) (t.points i₁) (t.points i₃)
h₂ :
  ∡ (t.points i₃) (t.points i₂) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₂) (t.points i₁) + (↑π : Real.Angle)
h₂' : excenter t signs = excenter t {i₃} ∨ excenter t signs = excenter t {i₁}
h₁' : excenter t signs = incenter t
inl : ∀ (h₂' : excenter t signs = excenter t {i₃}), excenter t signs = excenter t {i₁}
inl₁ : ∀ (h₂' : excenter t signs = excenter t {i₁}), excenter t signs = excenter t {i₁}
⊢ excenter t signs = excenter t {i₁}

Tactic:
rcases h₂' with h₂' | h₂'
-- Module: Mathlib.Geometry.Euclidean.Angle.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
signs : Finset (Fin 3)
h₁ : ∡ (t.points i₂) (t.points i₁) (excenter t signs) = ∡ (excenter t signs) (t.points i₁) (t.points i₃)
h₂ :
  ∡ (t.points i₃) (t.points i₂) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₂) (t.points i₁) + (↑π : Real.Angle)
h₁' : excenter t signs = incenter t
h₂' : excenter t signs = excenter t {i₃}
⊢ incenter t = excenter t {i₃}

Tactic:
rw [h₁'] at h₂'
-- Module: Mathlib.Geometry.Euclidean.Angle.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
signs : Finset (Fin 3)
h₁ : ∡ (t.points i₂) (t.points i₁) (excenter t signs) = ∡ (excenter t signs) (t.points i₁) (t.points i₃)
h₂ :
  ∡ (t.points i₃) (t.points i₂) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₂) (t.points i₁) + (↑π : Real.Angle)
h₁' : excenter t signs = incenter t
h₂' : incenter t = excenter t {i₃}
inl : False
⊢ excenter t signs = excenter t {i₁}

Tactic:
exfalso
-- Module: Mathlib.Geometry.Euclidean.Angle.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
signs : Finset (Fin 3)
h₁ : ∡ (t.points i₂) (t.points i₁) (excenter t signs) = ∡ (excenter t signs) (t.points i₁) (t.points i₃)
h₂ :
  ∡ (t.points i₃) (t.points i₂) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₂) (t.points i₁) + (↑π : Real.Angle)
h₁' : excenter t signs = incenter t
h₂' : incenter t = excenter t {i₃}
⊢ False

Tactic:
(t.excenter_singleton_ne_incenter _).symm h₂'

Premises used: Ne.symm, Affine.Simplex.excenter_singleton_ne_incenter
-- Module: Mathlib.Geometry.Euclidean.Angle.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
signs : Finset (Fin 3)
h₁ : ∡ (t.points i₂) (t.points i₁) (excenter t signs) = ∡ (excenter t signs) (t.points i₁) (t.points i₃)
h₂ :
  ∡ (t.points i₃) (t.points i₂) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₂) (t.points i₁) + (↑π : Real.Angle)
h₁' : excenter t signs = incenter t
h₂' : incenter t = excenter t {i₃}
⊢ False

Tactic:
exact (t.excenter_singleton_ne_incenter _).symm h₂'

Premises used: Ne.symm, Affine.Simplex.excenter_singleton_ne_incenter
-- Module: Mathlib.Geometry.Euclidean.Angle.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
signs : Finset (Fin 3)
h₁ : ∡ (t.points i₂) (t.points i₁) (excenter t signs) = ∡ (excenter t signs) (t.points i₁) (t.points i₃)
h₂ :
  ∡ (t.points i₃) (t.points i₂) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₂) (t.points i₁) + (↑π : Real.Angle)
h₁' : excenter t signs = incenter t
h₂' : excenter t signs = excenter t {i₁}
⊢ excenter t signs = excenter t {i₁}

Tactic:
h₂'
-- Module: Mathlib.Geometry.Euclidean.Angle.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
signs : Finset (Fin 3)
h₁ : ∡ (t.points i₂) (t.points i₁) (excenter t signs) = ∡ (excenter t signs) (t.points i₁) (t.points i₃)
h₂ :
  ∡ (t.points i₃) (t.points i₂) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₂) (t.points i₁) + (↑π : Real.Angle)
h₁' : excenter t signs = incenter t
h₂' : excenter t signs = excenter t {i₁}
⊢ excenter t signs = excenter t {i₁}

Tactic:
exact h₂'
-- Module: Mathlib.Geometry.Euclidean.Angle.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
signs : Finset (Fin 3)
h₁ : ∡ (t.points i₂) (t.points i₁) (excenter t signs) = ∡ (excenter t signs) (t.points i₁) (t.points i₃)
h₂ :
  ∡ (t.points i₃) (t.points i₂) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₂) (t.points i₁) + (↑π : Real.Angle)
h₂' : excenter t signs = excenter t {i₃} ∨ excenter t signs = excenter t {i₁}
h₁' : excenter t signs = excenter t {i₁}
⊢ excenter t signs = excenter t {i₁}

Tactic:
h₁'
-- Module: Mathlib.Geometry.Euclidean.Angle.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
signs : Finset (Fin 3)
h₁ : ∡ (t.points i₂) (t.points i₁) (excenter t signs) = ∡ (excenter t signs) (t.points i₁) (t.points i₃)
h₂ :
  ∡ (t.points i₃) (t.points i₂) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₂) (t.points i₁) + (↑π : Real.Angle)
h₂' : excenter t signs = excenter t {i₃} ∨ excenter t signs = excenter t {i₁}
h₁' : excenter t signs = excenter t {i₁}
⊢ excenter t signs = excenter t {i₁}

Tactic:
exact h₁'
-- Module: Mathlib.Geometry.Euclidean.Angle.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
p : P
h₁ : ∡ (t.points i₂) (t.points i₁) p = ∡ p (t.points i₁) (t.points i₃) + (↑π : Real.Angle)
h₂ : ∡ (t.points i₃) (t.points i₂) p = ∡ p (t.points i₂) (t.points i₁) + (↑π : Real.Angle)
rw :
  HSMul.hSMul (α := ℤ) 2 (∡ p (t.points i₁) (t.points i₃) + (↑π : Real.Angle)) =
    HSMul.hSMul (α := ℤ) 2 (∡ p (t.points i₁) (t.points i₃))
⊢ HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₂) (t.points i₁) p) = HSMul.hSMul (α := ℤ) 2 (∡ p (t.points i₁) (t.points i₃))

Tactic:
rw [h₁]
-- Module: Mathlib.Geometry.Euclidean.Angle.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
p : P
h₁ : ∡ (t.points i₂) (t.points i₁) p = ∡ p (t.points i₁) (t.points i₃) + (↑π : Real.Angle)
h₂ : ∡ (t.points i₃) (t.points i₂) p = ∡ p (t.points i₂) (t.points i₁) + (↑π : Real.Angle)
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p (t.points i₁) (t.points i₃) + (↑π : Real.Angle)) =
    HSMul.hSMul (α := ℤ) 2 (∡ p (t.points i₁) (t.points i₃))

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Angle.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
p : P
h₁ : ∡ (t.points i₂) (t.points i₁) p = ∡ p (t.points i₁) (t.points i₃) + (↑π : Real.Angle)
h₂ : ∡ (t.points i₃) (t.points i₂) p = ∡ p (t.points i₂) (t.points i₁) + (↑π : Real.Angle)
rw :
  HSMul.hSMul (α := ℤ) 2 (∡ p (t.points i₂) (t.points i₁) + (↑π : Real.Angle)) =
    HSMul.hSMul (α := ℤ) 2 (∡ p (t.points i₂) (t.points i₁))
⊢ HSMul.hSMul (α := ℤ) 2 (∡ (t.points i₃) (t.points i₂) p) = HSMul.hSMul (α := ℤ) 2 (∡ p (t.points i₂) (t.points i₁))

Tactic:
rw [h₂]
-- Module: Mathlib.Geometry.Euclidean.Angle.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
p : P
h₁ : ∡ (t.points i₂) (t.points i₁) p = ∡ p (t.points i₁) (t.points i₃) + (↑π : Real.Angle)
h₂ : ∡ (t.points i₃) (t.points i₂) p = ∡ p (t.points i₂) (t.points i₁) + (↑π : Real.Angle)
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p (t.points i₂) (t.points i₁) + (↑π : Real.Angle)) =
    HSMul.hSMul (α := ℤ) 2 (∡ p (t.points i₂) (t.points i₁))

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Angle.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
p : P
h₁ : ∡ (t.points i₂) (t.points i₁) p = ∡ p (t.points i₁) (t.points i₃) + (↑π : Real.Angle)
h₂ : ∡ (t.points i₃) (t.points i₂) p = ∡ p (t.points i₂) (t.points i₁) + (↑π : Real.Angle)
obtain :
  ∀ (signs : Finset (Fin 3))
    (h₁ :
      ∡ (t.points i₂) (t.points i₁) (excenter t signs) =
        ∡ (excenter t signs) (t.points i₁) (t.points i₃) + (↑π : Real.Angle))
    (h₂ :
      ∡ (t.points i₃) (t.points i₂) (excenter t signs) =
        ∡ (excenter t signs) (t.points i₂) (t.points i₁) + (↑π : Real.Angle)),
    excenter t signs = excenter t {i₃}
⊢ p = excenter t {i₃}

Tactic:
obtain ⟨signs, rfl⟩ := t.eq_excenter_of_two_zsmul_oangle_eq h₁₂ h₁₃ h₂₃ (by rw [h₁]; simp)
    (by rw [h₂]; simp)

Premises used: Affine.Triangle.eq_excenter_of_two_zsmul_oangle_eq, rfl
-- Module: Mathlib.Geometry.Euclidean.Angle.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
signs : Finset (Fin 3)
h₁ :
  ∡ (t.points i₂) (t.points i₁) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₁) (t.points i₃) + (↑π : Real.Angle)
h₂ :
  ∡ (t.points i₃) (t.points i₂) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₂) (t.points i₁) + (↑π : Real.Angle)
⊢ excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}

Tactic:
have h₁' := t.eq_excenter_singleton_of_oangle_eq_add_pi h₁₂ h₁₃ h₂₃ h₁
-- Module: Mathlib.Geometry.Euclidean.Angle.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
signs : Finset (Fin 3)
h₁ :
  ∡ (t.points i₂) (t.points i₁) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₁) (t.points i₃) + (↑π : Real.Angle)
h₂ :
  ∡ (t.points i₃) (t.points i₂) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₂) (t.points i₁) + (↑π : Real.Angle)
h₁' : excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}
⊢ excenter t signs = excenter t {i₃} ∨ excenter t signs = excenter t {i₁}

Tactic:
have h₂' := t.eq_excenter_singleton_of_oangle_eq_add_pi h₂₃ h₁₂.symm h₁₃.symm h₂
-- Module: Mathlib.Geometry.Euclidean.Angle.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
signs : Finset (Fin 3)
h₁ :
  ∡ (t.points i₂) (t.points i₁) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₁) (t.points i₃) + (↑π : Real.Angle)
h₂ :
  ∡ (t.points i₃) (t.points i₂) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₂) (t.points i₁) + (↑π : Real.Angle)
h₁' : excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}
h₂' : excenter t signs = excenter t {i₃} ∨ excenter t signs = excenter t {i₁}
inl : ∀ (h₁' : excenter t signs = excenter t {i₂}), excenter t signs = excenter t {i₃}
inr : ∀ (h₁' : excenter t signs = excenter t {i₃}), excenter t signs = excenter t {i₃}
⊢ excenter t signs = excenter t {i₃}

Tactic:
rcases h₁' with h₁' | h₁'
-- Module: Mathlib.Geometry.Euclidean.Angle.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
signs : Finset (Fin 3)
h₁ :
  ∡ (t.points i₂) (t.points i₁) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₁) (t.points i₃) + (↑π : Real.Angle)
h₂ :
  ∡ (t.points i₃) (t.points i₂) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₂) (t.points i₁) + (↑π : Real.Angle)
h₂' : excenter t signs = excenter t {i₃} ∨ excenter t signs = excenter t {i₁}
h₁' : excenter t signs = excenter t {i₂}
inl : ∀ (h₂' : excenter t signs = excenter t {i₃}), excenter t signs = excenter t {i₃}
inl₁ : ∀ (h₂' : excenter t signs = excenter t {i₁}), excenter t signs = excenter t {i₃}
⊢ excenter t signs = excenter t {i₃}

Tactic:
rcases h₂' with h₂' | h₂'
-- Module: Mathlib.Geometry.Euclidean.Angle.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
signs : Finset (Fin 3)
h₁ :
  ∡ (t.points i₂) (t.points i₁) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₁) (t.points i₃) + (↑π : Real.Angle)
h₂ :
  ∡ (t.points i₃) (t.points i₂) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₂) (t.points i₁) + (↑π : Real.Angle)
h₁' : excenter t signs = excenter t {i₂}
h₂' : excenter t signs = excenter t {i₃}
⊢ excenter t signs = excenter t {i₃}

Tactic:
h₂'
-- Module: Mathlib.Geometry.Euclidean.Angle.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
signs : Finset (Fin 3)
h₁ :
  ∡ (t.points i₂) (t.points i₁) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₁) (t.points i₃) + (↑π : Real.Angle)
h₂ :
  ∡ (t.points i₃) (t.points i₂) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₂) (t.points i₁) + (↑π : Real.Angle)
h₁' : excenter t signs = excenter t {i₂}
h₂' : excenter t signs = excenter t {i₃}
⊢ excenter t signs = excenter t {i₃}

Tactic:
exact h₂'
-- Module: Mathlib.Geometry.Euclidean.Angle.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
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
t : Triangle ℝ P
i₁ i₂ i₃ : Fin 3
h₁₂ : i₁ ≠ i₂
h₁₃ : i₁ ≠ i₃
h₂₃ : i₂ ≠ i₃
signs : Finset (Fin 3)
h₁ :
  ∡ (t.points i₂) (t.points i₁) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₁) (t.points i₃) + (↑π : Real.Angle)
h₂ :
  ∡ (t.points i₃) (t.points i₂) (excenter t signs) =
    ∡ (excenter t signs) (t.points i₂) (t.points i₁) + (↑π : Real.Angle)
h₁' : excenter t signs = excenter t {i₂}
h₂' : excenter t signs = excenter t {i₁}
⊢ excenter t {i₁} = excenter t {i₂}

Tactic:
rw [h₂'] at h₁'