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₃
p : P
h₁ :
  dist p
      (↑(((faceOpposite t i₃).orthogonalProjectionSpan :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₃).points)))
            p) :
        P) =
    dist p
      (↑(((faceOpposite t i₂).orthogonalProjectionSpan :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₂).points)))
            p) :
        P)
h₂ :
  dist p
      (↑(((faceOpposite t i₁).orthogonalProjectionSpan :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₁).points)))
            p) :
        P) =
    dist p
      (↑(((faceOpposite t i₃).orthogonalProjectionSpan :
              (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i₃).points)))
            p) :
        P)
hp : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ (Set.range t.points)) p
hr :
  ∃ (r : ℝ),
    ∀ (i : Fin (HAdd.hAdd (α := ℕ) 2 1)),
      dist p
          (↑(((faceOpposite t i).orthogonalProjectionSpan :
                  (a : P) → ↥(affineSpan ℝ (Set.range (faceOpposite t i).points)))
                p) :
            P) =
        r
⊢ ∃ (signs : Finset (Fin 3)), p = excenter t signs
have obtain : ∀ (signs : Finset (Fin (HAdd.hAdd (α := ℕ) 2 1))) (hp : p = excenter t signs),
  ∃ (signs : Finset (Fin 3)), p = excenter t signs
Tactic: obtain ⟨signs, -, hp⟩ :=
    (t.exists_forall_dist_eq_iff_exists_excenterExists_and_eq_excenter hp).1 hr
-- 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₃)
⊢ excenter t signs = incenter t ∨ excenter t signs = excenter t {i₁}
have hs : 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 hs := t.excenter_eq_incenter_or_excenter_singleton_of_ne signs h₁₂ 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₃)
hs :
  excenter t signs = incenter t ∨
    excenter t signs = excenter t {i₁} ∨ excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}
⊢ excenter t signs = incenter t ∨ excenter t signs = excenter t {i₁}
have inl : ∀ (hs : excenter t signs = incenter t), excenter t signs = incenter t ∨ excenter t signs = excenter t {i₁}
Tactic: rcases hs with hs | hs | hs | hs
Cleared hypotheses: hs
-- 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₃)
hs :
  excenter t signs = incenter t ∨
    excenter t signs = excenter t {i₁} ∨ excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}
inl : ∀ (hs : excenter t signs = incenter t), excenter t signs = incenter t ∨ excenter t signs = excenter t {i₁}
⊢ excenter t signs = incenter t ∨ excenter t signs = excenter t {i₁}
have inr : ∀ (hs : excenter t signs = excenter t {i₁}), excenter t signs = incenter t ∨ excenter t signs = excenter t {i₁}
Tactic: rcases hs with hs | hs | hs | hs
Cleared hypotheses: hs
-- 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₃)
hs :
  excenter t signs = incenter t ∨
    excenter t signs = excenter t {i₁} ∨ excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}
inl : ∀ (hs : excenter t signs = incenter t), excenter t signs = incenter t ∨ excenter t signs = excenter t {i₁}
inr : ∀ (hs : excenter t signs = excenter t {i₁}), excenter t signs = incenter t ∨ excenter t signs = excenter t {i₁}
⊢ excenter t signs = incenter t ∨ excenter t signs = excenter t {i₁}
have inr₁ : ∀ (hs : excenter t signs = excenter t {i₂}), excenter t signs = incenter t ∨ excenter t signs = excenter t {i₁}
Tactic: rcases hs with hs | hs | hs | hs
Cleared hypotheses: hs
-- 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₃)
hs :
  excenter t signs = incenter t ∨
    excenter t signs = excenter t {i₁} ∨ excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}
inl : ∀ (hs : excenter t signs = incenter t), excenter t signs = incenter t ∨ excenter t signs = excenter t {i₁}
inr : ∀ (hs : excenter t signs = excenter t {i₁}), excenter t signs = incenter t ∨ excenter t signs = excenter t {i₁}
inr₁ : ∀ (hs : excenter t signs = excenter t {i₂}), excenter t signs = incenter t ∨ excenter t signs = excenter t {i₁}
⊢ excenter t signs = incenter t ∨ excenter t signs = excenter t {i₁}
have inr₂ : ∀ (hs : excenter t signs = excenter t {i₃}), excenter t signs = incenter t ∨ excenter t signs = excenter t {i₁}
Tactic: rcases hs with hs | hs | hs | hs
Cleared hypotheses: hs
-- 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₃)
hs : excenter t signs = excenter t {i₂}
⊢ excenter t signs = incenter t ∨ excenter t signs = excenter t {i₁}
have h₁ : ∡ (excenter t {i₂}) (t.points i₁) (t.points i₃) + (↑π : Real.Angle) = ∡ (excenter t {i₂}) (t.points i₁) (t.points i₃)
Tactic: rw [hs, t.oangle_excenter_singleton_eq_add_pi h₁₂.symm h₂₃ h₁₃] at h
Cleared hypotheses: h, hs
-- 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₃)
hs : excenter t signs = excenter t {i₃}
⊢ excenter t signs = incenter t ∨ excenter t signs = excenter t {i₁}
have h₁ : -∡ (excenter t {i₃}) (t.points i₁) (t.points i₂) =
  -(∡ (excenter t {i₃}) (t.points i₁) (t.points i₂) + (↑π : Real.Angle))
Tactic: rw [hs, oangle_rev (t.points i₃), t.oangle_excenter_singleton_eq_add_pi h₁₃.symm h₂₃.symm h₁₂,
      oangle_rev] at h
Cleared hypotheses: h, hs
-- 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)
⊢ excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}
have hs : 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 hs := t.excenter_eq_incenter_or_excenter_singleton_of_ne signs h₁₂ 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)
hs :
  excenter t signs = incenter t ∨
    excenter t signs = excenter t {i₁} ∨ excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}
⊢ excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}
have inl : ∀ (hs : excenter t signs = incenter t), excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}
Tactic: rcases hs with hs | hs | hs | hs
Cleared hypotheses: hs
-- 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)
hs :
  excenter t signs = incenter t ∨
    excenter t signs = excenter t {i₁} ∨ excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}
inl : ∀ (hs : excenter t signs = incenter t), excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}
⊢ excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}
have inr : ∀ (hs : excenter t signs = excenter t {i₁}), excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}
Tactic: rcases hs with hs | hs | hs | hs
Cleared hypotheses: hs
-- 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)
hs :
  excenter t signs = incenter t ∨
    excenter t signs = excenter t {i₁} ∨ excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}
inl : ∀ (hs : excenter t signs = incenter t), excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}
inr :
  ∀ (hs : excenter t signs = excenter t {i₁}), excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}
⊢ excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}
have inr₁ : ∀ (hs : excenter t signs = excenter t {i₂}), excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}
Tactic: rcases hs with hs | hs | hs | hs
Cleared hypotheses: hs
-- 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)
hs :
  excenter t signs = incenter t ∨
    excenter t signs = excenter t {i₁} ∨ excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}
inl : ∀ (hs : excenter t signs = incenter t), excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}
inr :
  ∀ (hs : excenter t signs = excenter t {i₁}), excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}
inr₁ :
  ∀ (hs : excenter t signs = excenter t {i₂}), excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}
⊢ excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}
have inr₂ : ∀ (hs : excenter t signs = excenter t {i₃}), excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}
Tactic: rcases hs with hs | hs | hs | hs
Cleared hypotheses: hs
-- 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)
hs : excenter t signs = incenter t
⊢ excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}
have h₁ : ∡ (incenter t) (t.points i₁) (t.points i₃) = ∡ (incenter t) (t.points i₁) (t.points i₃) + (↑π : Real.Angle)
Tactic: rw [hs, t.oangle_incenter_eq h₁₂ h₁₃ h₂₃] at h
Cleared hypotheses: h, hs
-- 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)
hs : excenter t signs = excenter t {i₁}
⊢ excenter t signs = excenter t {i₂} ∨ excenter t signs = excenter t {i₃}
have h₁ : ∡ (excenter t {i₁}) (t.points i₁) (t.points i₃) = ∡ (excenter t {i₁}) (t.points i₁) (t.points i₃) + (↑π : Real.Angle)
Tactic: rw [hs, t.oangle_excenter_singleton_eq h₁₂ h₁₃ h₂₃] at h
Cleared hypotheses: h, hs
-- 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₁)
⊢ 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₁)
⊢ 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₁)
⊢ p = incenter t
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₁)),
  excenter t signs = incenter t
Tactic: obtain ⟨signs, rfl⟩ := t.eq_excenter_of_two_zsmul_oangle_eq h₁₂ h₁₃ h₂₃ (by rw [h₁]) (by rw [h₂])
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₁)
⊢ excenter t signs = incenter t
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₁)
h₁' : excenter t signs = incenter t ∨ excenter t signs = excenter t {i₁}
⊢ excenter t signs = incenter t
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₁₂.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₁)
h₁' : excenter t signs = incenter t ∨ excenter t signs = excenter t {i₁}
h₂' : excenter t signs = incenter t ∨ excenter t signs = excenter t {i₂}
⊢ excenter t signs = incenter t
have inl : ∀ (h₁' : excenter t signs = incenter t), excenter t signs = incenter t
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₁)
h₁' : excenter t signs = incenter t ∨ excenter t signs = excenter t {i₁}
h₂' : excenter t signs = incenter t ∨ excenter t signs = excenter t {i₂}
inl : ∀ (h₁' : excenter t signs = incenter t), excenter t signs = incenter t
⊢ excenter t signs = incenter t
have inr : ∀ (h₁' : excenter t signs = excenter t {i₁}), excenter t signs = incenter t
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₁)
h₂' : excenter t signs = incenter t ∨ excenter t signs = excenter t {i₂}
h₁' : excenter t signs = excenter t {i₁}
⊢ excenter t signs = incenter t
have inr : ∀ (h₂' : excenter t signs = incenter t), excenter t signs = incenter t
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₁)
h₂' : excenter t signs = incenter t ∨ excenter t signs = excenter t {i₂}
h₁' : excenter t signs = excenter t {i₁}
inr : ∀ (h₂' : excenter t signs = incenter t), excenter t signs = incenter t
⊢ excenter t signs = incenter t
have inr₁ : ∀ (h₂' : excenter t signs = excenter t {i₂}), excenter t signs = incenter t
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₁)
h₁' : excenter t signs = excenter t {i₁}
h₂' : excenter t signs = excenter t {i₂}
⊢ excenter t signs = incenter t
have h₂'₁ : excenter t {i₁} = excenter t {i₂}
Tactic: rw [h₁'] at h₂'
Cleared hypotheses: h₂'