awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Incenter (goal)
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₂}
⊢ excenter t signs = incenter t
have inr : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Incenter (goal)
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 (∡ (t.points i₂) (t.points i₁) p) = HSMul.hSMul (α := ℤ) 2 (∡ p (t.points i₁) (t.points i₃))
have rw : HSMul.hSMul (α := ℤ) 2 (∡ p (t.points i₁) (t.points i₃)) = HSMul.hSMul (α := ℤ) 2 (∡ p (t.points i₁) (t.points i₃))
Tactic: rw [h₁]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Incenter (goal)
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 (∡ (t.points i₃) (t.points i₂) p) = HSMul.hSMul (α := ℤ) 2 (∡ p (t.points i₂) (t.points i₁))
have rw : HSMul.hSMul (α := ℤ) 2 (∡ p (t.points i₂) (t.points i₁) + (↑π : Real.Angle)) =
  HSMul.hSMul (α := ℤ) 2 (∡ p (t.points i₂) (t.points i₁))
Tactic: rw [h₂]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Incenter (goal)
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)
⊢ p = excenter t {i₁}
have 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₁}
Tactic: obtain ⟨signs, rfl⟩ := t.eq_excenter_of_two_zsmul_oangle_eq h₁₂ h₁₃ h₂₃ (by rw [h₁])
    (by rw [h₂]; simp)
Cleared hypotheses: p, h₁, h₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Incenter (hypothesis)
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 = excenter t {i₁}
have h₁' : 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₁
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Incenter (hypothesis)
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₁}
have h₂' : 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₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Incenter (goal)
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₁}
⊢ excenter t signs = excenter t {i₁}
have inl : ∀ (h₁' : excenter t signs = incenter t), excenter t signs = excenter t {i₁}
Tactic: rcases h₁' with h₁' | h₁'
Cleared hypotheses: h₁'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Incenter (goal)
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₁}
⊢ excenter t signs = excenter t {i₁}
have inr : ∀ (h₁' : excenter t signs = excenter t {i₁}), excenter t signs = excenter t {i₁}
Tactic: rcases h₁' with h₁' | h₁'
Cleared hypotheses: h₁'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Incenter (goal)
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
⊢ excenter t signs = excenter t {i₁}
have inl : ∀ (h₂' : excenter t signs = excenter t {i₃}), excenter t signs = excenter t {i₁}
Tactic: rcases h₂' with h₂' | h₂'
Cleared hypotheses: h₂'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Incenter (goal)
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₁}
⊢ excenter t signs = excenter t {i₁}
have inl₁ : ∀ (h₂' : excenter t signs = excenter t {i₁}), excenter t signs = excenter t {i₁}
Tactic: rcases h₂' with h₂' | h₂'
Cleared hypotheses: h₂'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Incenter (hypothesis)
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₁}
have h₂'₁ : incenter t = excenter t {i₃}
Tactic: rw [h₁'] at h₂'
Cleared hypotheses: h₂'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Incenter (goal)
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₃}
⊢ excenter t signs = excenter t {i₁}
have inl : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Incenter (goal)
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 (∡ (t.points i₂) (t.points i₁) p) = HSMul.hSMul (α := ℤ) 2 (∡ p (t.points i₁) (t.points i₃))
have rw : HSMul.hSMul (α := ℤ) 2 (∡ p (t.points i₁) (t.points i₃) + (↑π : Real.Angle)) =
  HSMul.hSMul (α := ℤ) 2 (∡ p (t.points i₁) (t.points i₃))
Tactic: rw [h₁]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Incenter (goal)
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 (∡ (t.points i₃) (t.points i₂) p) = HSMul.hSMul (α := ℤ) 2 (∡ p (t.points i₂) (t.points i₁))
have rw : HSMul.hSMul (α := ℤ) 2 (∡ p (t.points i₂) (t.points i₁) + (↑π : Real.Angle)) =
  HSMul.hSMul (α := ℤ) 2 (∡ p (t.points i₂) (t.points i₁))
Tactic: rw [h₂]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Incenter (goal)
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)
⊢ p = excenter t {i₃}
have 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₃}
Tactic: obtain ⟨signs, rfl⟩ := t.eq_excenter_of_two_zsmul_oangle_eq h₁₂ h₁₃ h₂₃ (by rw [h₁]; simp)
    (by rw [h₂]; simp)
Cleared hypotheses: p, h₁, h₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Incenter (hypothesis)
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₃}
have h₁' : 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₁
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Incenter (hypothesis)
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₃}
have h₂' : 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₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Incenter (goal)
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₁}
⊢ excenter t signs = excenter t {i₃}
have inl : ∀ (h₁' : excenter t signs = excenter t {i₂}), excenter t signs = excenter t {i₃}
Tactic: rcases h₁' with h₁' | h₁'
Cleared hypotheses: h₁'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Incenter (goal)
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₃}
⊢ excenter t signs = excenter t {i₃}
have inr : ∀ (h₁' : excenter t signs = excenter t {i₃}), excenter t signs = excenter t {i₃}
Tactic: rcases h₁' with h₁' | h₁'
Cleared hypotheses: h₁'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Incenter (goal)
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₃}
have inl : ∀ (h₂' : excenter t signs = excenter t {i₃}), excenter t signs = excenter t {i₃}
Tactic: rcases h₂' with h₂' | h₂'
Cleared hypotheses: h₂'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Incenter (goal)
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₃}
⊢ excenter t signs = excenter t {i₃}
have inl₁ : ∀ (h₂' : excenter t signs = excenter t {i₁}), excenter t signs = excenter t {i₃}
Tactic: rcases h₂' with h₂' | h₂'
Cleared hypotheses: h₂'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Incenter (hypothesis)
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₃}
have h₁'₁ : excenter t {i₁} = excenter t {i₂}
Tactic: rw [h₂'] at h₁'
Cleared hypotheses: h₁', h₂'
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Incenter (goal)
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 {i₁} = excenter t {i₂}
h₂' : excenter t signs = excenter t {i₁}
⊢ excenter t signs = excenter t {i₃}
have inl : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (goal)
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)
x : P × P × P
hx12 : x.1 ≠ x.2.1
hx32 : x.2.2 ≠ x.2.1
⊢ ContinuousAt (Y := Real.Angle) (fun (y : P × P × P) ↦ Orientation.oangle o (y.1 -ᵥ y.2.1) (y.2.2 -ᵥ y.2.1)) x
have funProp : (x.1 -ᵥ x.2.1, x.2.2 -ᵥ x.2.1).1 ≠ 0
Tactic: fun_prop (disch := simp [*])
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (goal)
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)
x : P × P × P
hx12 : x.1 ≠ x.2.1
hx32 : x.2.2 ≠ x.2.1
funProp : (x.1 -ᵥ x.2.1, x.2.2 -ᵥ x.2.1).1 ≠ 0
⊢ ContinuousAt (Y := Real.Angle) (fun (y : P × P × P) ↦ Orientation.oangle o (y.1 -ᵥ y.2.1) (y.2.2 -ᵥ y.2.1)) x
have funProp₁ : (x.1 -ᵥ x.2.1, x.2.2 -ᵥ x.2.1).2 ≠ 0
Tactic: fun_prop (disch := simp [*])
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (goal)
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)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ ≠ 0
⊢ p₁ ≠ p₂
have rw : p₁ -ᵥ p₂ ≠ 0
Tactic: rw [← @vsub_ne_zero V]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (goal)
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)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ ≠ 0
⊢ p₃ ≠ p₂
have rw : p₃ -ᵥ p₂ ≠ 0
Tactic: rw [← @vsub_ne_zero V]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (goal)
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)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ ≠ 0
⊢ p₁ ≠ p₃
have rw : p₁ -ᵥ p₂ ≠ p₃ -ᵥ p₂
Tactic: rw [← (vsub_left_injective p₂).ne_iff]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (goal)
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)
p p₁ p₂ p₃ : P
r : ℝ
h : r ≠ 0
⊢ ∡ (P := P) ((AffineMap.homothety p r : (a : P) → P) p₁ : P) ((AffineMap.homothety p r : (a : P) → P) p₂ : P)
      ((AffineMap.homothety p r : (a : P) → P) p₃ : P) =
    ∡ p₁ p₂ p₃
have simp_rw : Orientation.oangle o (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂)) = Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)
Tactic: simp_rw [oangle, ← AffineMap.linearMap_vsub, AffineMap.homothety_linear, LinearMap.smul_apply,
    LinearMap.id_coe, id_eq]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (goal)
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)
p p₁ p₂ p₃ : P
r : ℝ
h : r ≠ 0
⊢ Orientation.oangle o (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂)) = Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)
have inl : ∀ (hlt : r < 0), Orientation.oangle o (r • (p₁ -ᵥ p₂)) (r • (p₃ -ᵥ p₂)) = Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂)
Tactic: rcases h.lt_or_gt with hlt | hlt