awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
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
h : Collinear ℝ (P := P) {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hw : Wbtw ℝ p₁' p₁ p₂
neg neg₁ : HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)

Tactic:
rw [hw.symm.oangle_eq_left hp₁p₂]

Premises used: Wbtw.oangle_eq_left, Wbtw.symm
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
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
h : Collinear ℝ (P := P) {p₃, p₂, p₃'}
hp₃p₂ : p₃ ≠ p₂
hp₃'p₂ : p₃' ≠ p₂
rw : HSMul.hSMul (α := ℤ) 2 (-∡ p₃ p₂ p₁) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃')
rw₁ : -HSMul.hSMul (α := ℤ) 2 (∡ p₃ p₂ p₁) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃')
rw₂ : -HSMul.hSMul (α := ℤ) 2 (∡ p₃' p₂ p₁) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃')
rw₃ : HSMul.hSMul (α := ℤ) 2 (-∡ p₃' p₂ p₁) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃')
rw₄ rw₅ : HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃') = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃')
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃')

Tactic:
rw [oangle_rev, smul_neg, h.two_zsmul_oangle_eq_left hp₃p₂ hp₃'p₂, ← smul_neg, ← oangle_rev]

Premises used: EuclideanGeometry.oangle_rev, smul_neg, Collinear.two_zsmul_oangle_eq_left
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
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₂
⊢ dist p₁ p = dist p₂ p ↔
    ∃ (r : ℝ),
      HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) +ᵥ
          midpoint ℝ p₁ p₂ =
        p

Tactic:
⟨fun hd => ?_, fun hr => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
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₂
refine_1 :
  ∀ (hd : dist p₁ p = dist p₂ p),
    ∃ (r : ℝ),
      HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) +ᵥ
          midpoint ℝ p₁ p₂ =
        p
refine_2 :
  ∀
    (hr :
      ∃ (r : ℝ),
        HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) +ᵥ
            midpoint ℝ p₁ p₂ =
          p),
    dist p₁ p = dist p₂ p
⊢ dist p₁ p = dist p₂ p ↔
    ∃ (r : ℝ),
      HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) +ᵥ
          midpoint ℝ p₁ p₂ =
        p

Tactic:
refine ⟨fun hd => ?_, fun hr => ?_⟩
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
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₂
hd : dist p₁ p = dist p₂ p
⊢ ⟪p -ᵥ p₁, p -ᵥ p₁⟫ = ⟪p -ᵥ p₂, p -ᵥ p₂⟫

Tactic:
rw [@dist_eq_norm_vsub' V, @dist_eq_norm_vsub' V, ←
        mul_self_inj (norm_nonneg _) (norm_nonneg _), ← real_inner_self_eq_norm_mul_norm, ←
        real_inner_self_eq_norm_mul_norm] at hd

Premises used: dist_eq_norm_vsub', real_inner_self_eq_norm_mul_norm, norm_nonneg, mul_self_inj
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
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₂
hd : ⟪p -ᵥ p₁, p -ᵥ p₁⟫ = ⟪p -ᵥ p₂, p -ᵥ p₂⟫
simp_rw :
  @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ * ⟪p -ᵥ p₂, p -ᵥ p₂⟫ +
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ * ⟪p -ᵥ p₁, p -ᵥ p₂⟫ -
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ * ⟪p -ᵥ p₁, p -ᵥ p₂⟫ +
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ * ⟪p -ᵥ p₂, p -ᵥ p₂⟫) =
    0
⊢ ⟪p₂ -ᵥ p₁, p -ᵥ midpoint ℝ p₁ p₂⟫ = 0

Tactic:
simp_rw [vsub_midpoint, ← vsub_sub_vsub_cancel_left p₂ p₁ p, inner_sub_left, inner_add_right,
        inner_smul_right, hd, real_inner_comm (p -ᵥ p₁)]

Premises used: vsub_midpoint, VSub.vsub, inner_add_right, inner_sub_left, vsub_sub_vsub_cancel_left, inner_smul_right, real_inner_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
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₂
hd : ⟪p -ᵥ p₁, p -ᵥ p₁⟫ = ⟪p -ᵥ p₂, p -ᵥ p₂⟫
⊢ @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ * ⟪p -ᵥ p₂, p -ᵥ p₂⟫ +
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ * ⟪p -ᵥ p₁, p -ᵥ p₂⟫ -
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ * ⟪p -ᵥ p₁, p -ᵥ p₂⟫ +
        @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ * ⟪p -ᵥ p₂, p -ᵥ p₂⟫) =
    0

Tactic:
abel
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
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₂
hd : dist p₁ p = dist p₂ p
⊢ ⟪p₂ -ᵥ p₁, p -ᵥ midpoint ℝ p₁ p₂⟫ = 0

Tactic:
have hi : ⟪p₂ -ᵥ p₁, p -ᵥ midpoint ℝ p₁ p₂⟫ = 0 := by
      rw [@dist_eq_norm_vsub' V, @dist_eq_norm_vsub' V, ←
        mul_self_inj (norm_nonneg _) (norm_nonneg _), ← real_inner_self_eq_norm_mul_norm, ←
        real_inner_self_eq_norm_mul_norm] at hd
      simp_rw [vsub_midpoint, ← vsub_sub_vsub_cancel_left p₂ p₁ p, inner_sub_left, inner_add_right,
        inner_smul_right, hd, real_inner_comm (p -ᵥ p₁)]
      abel
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
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₂
hd : dist p₁ p = dist p₂ p
hi : ⟪p₂ -ᵥ p₁, p -ᵥ midpoint ℝ p₁ p₂⟫ = 0
⊢ ∃ (r : ℝ),
    HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) =
      p -ᵥ midpoint ℝ p₁ p₂

Tactic:
rw [@Orientation.inner_eq_zero_iff_eq_zero_or_eq_smul_rotation_pi_div_two V _ _ _ o,
      or_iff_right (vsub_ne_zero.2 h.symm)] at hi

Premises used: Iff.mpr, vsub_ne_zero, Ne.symm, Orientation.inner_eq_zero_iff_eq_zero_or_eq_smul_rotation_pi_div_two, or_iff_right, EuclideanGeometry.o
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
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₂
hd : dist p₁ p = dist p₂ p
hi :
  ∃ (r : ℝ),
    HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) =
      p -ᵥ midpoint ℝ p₁ p₂
refine_1 :
  ∀ (r : ℝ)
    (hr :
      HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) =
        p -ᵥ midpoint ℝ p₁ p₂),
    ∃ (r : ℝ),
      HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) +ᵥ
          midpoint ℝ p₁ p₂ =
        p
⊢ ∃ (r : ℝ),
    HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) +ᵥ
        midpoint ℝ p₁ p₂ =
      p

Tactic:
rcases hi with ⟨r, hr⟩
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
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₂
hd : dist p₁ p = dist p₂ p
r : ℝ
hr :
  HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) =
    p -ᵥ midpoint ℝ p₁ p₂
⊢ p =
    HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) +ᵥ
      midpoint ℝ p₁ p₂

Tactic:
rw [eq_comm, ← eq_vadd_iff_vsub_eq] at hr

Premises used: eq_comm, eq_vadd_iff_vsub_eq
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
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₂
hd : dist p₁ p = dist p₂ p
r : ℝ
hr :
  p =
    HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) +ᵥ
      midpoint ℝ p₁ p₂
⊢ ∃ (r : ℝ),
    HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) +ᵥ
        midpoint ℝ p₁ p₂ =
      p

Tactic:
⟨r, hr.symm⟩

Premises used: Exists.intro, Eq.symm
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
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₂
hd : dist p₁ p = dist p₂ p
r : ℝ
hr :
  p =
    HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) +ᵥ
      midpoint ℝ p₁ p₂
⊢ ∃ (r : ℝ),
    HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) +ᵥ
        midpoint ℝ p₁ p₂ =
      p

Tactic:
exact ⟨r, hr.symm⟩
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
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₂
hr :
  ∃ (r : ℝ),
    HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) +ᵥ
        midpoint ℝ p₁ p₂ =
      p
refine_2 :
  ∀ (r : ℝ),
    dist p₁
        (HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) +ᵥ
          midpoint ℝ p₁ p₂) =
      dist p₂
        (HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) +ᵥ
          midpoint ℝ p₁ p₂)
⊢ dist p₁ p = dist p₂ p

Tactic:
rcases hr with ⟨r, rfl⟩

Premises used: rfl
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
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
h : p₁ ≠ p₂
r : ℝ
refine_2 :
  ⟪HSMul.hSMul (α := ℝ) 2⁻¹ (-(p₂ -ᵥ p₁)), HSMul.hSMul (α := ℝ) 2⁻¹ (-(p₂ -ᵥ p₁))⟫ -
          ⟪HSMul.hSMul (α := ℝ) 2⁻¹ (-(p₂ -ᵥ p₁)),
            HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V)⟫ -
        ⟪HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V),
          HSMul.hSMul (α := ℝ) 2⁻¹ (-(p₂ -ᵥ p₁))⟫ +
      ⟪HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V),
        HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V)⟫ =
    ⟪HSMul.hSMul (α := ℝ) 2⁻¹ (p₂ -ᵥ p₁), HSMul.hSMul (α := ℝ) 2⁻¹ (p₂ -ᵥ p₁)⟫ -
          ⟪HSMul.hSMul (α := ℝ) 2⁻¹ (p₂ -ᵥ p₁),
            HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V)⟫ -
        ⟪HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V),
          HSMul.hSMul (α := ℝ) 2⁻¹ (p₂ -ᵥ p₁)⟫ +
      ⟪HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V),
        HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V)⟫
⊢ dist p₁
      (HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) +ᵥ
        midpoint ℝ p₁ p₂) =
    dist p₂
      (HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) +ᵥ
        midpoint ℝ p₁ p₂)

Tactic:
simp_rw [@dist_eq_norm_vsub V, vsub_vadd_eq_vsub_sub, left_vsub_midpoint, right_vsub_midpoint,
      invOf_eq_inv, ← neg_vsub_eq_vsub_rev p₂ p₁, ← mul_self_inj (norm_nonneg _) (norm_nonneg _), ←
      real_inner_self_eq_norm_mul_norm, inner_sub_sub_self]

Premises used: vsub_vadd_eq_vsub_sub, real_inner_self_eq_norm_mul_norm, neg_vsub_eq_vsub_rev, invOf_eq_inv, dist_eq_norm_vsub, right_vsub_midpoint, inner_sub_sub_self, norm_nonneg, mul_self_inj, left_vsub_midpoint
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
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
h : p₁ ≠ p₂
r : ℝ
⊢ ⟪HSMul.hSMul (α := ℝ) 2⁻¹ (-(p₂ -ᵥ p₁)), HSMul.hSMul (α := ℝ) 2⁻¹ (-(p₂ -ᵥ p₁))⟫ -
          ⟪HSMul.hSMul (α := ℝ) 2⁻¹ (-(p₂ -ᵥ p₁)),
            HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V)⟫ -
        ⟪HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V),
          HSMul.hSMul (α := ℝ) 2⁻¹ (-(p₂ -ᵥ p₁))⟫ +
      ⟪HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V),
        HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V)⟫ =
    ⟪HSMul.hSMul (α := ℝ) 2⁻¹ (p₂ -ᵥ p₁), HSMul.hSMul (α := ℝ) 2⁻¹ (p₂ -ᵥ p₁)⟫ -
          ⟪HSMul.hSMul (α := ℝ) 2⁻¹ (p₂ -ᵥ p₁),
            HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V)⟫ -
        ⟪HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V),
          HSMul.hSMul (α := ℝ) 2⁻¹ (p₂ -ᵥ p₁)⟫ +
      ⟪HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V),
        HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V)⟫

Tactic:
simp [-neg_vsub_eq_vsub_rev]

Premises used: neg_vsub_eq_vsub_rev
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
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₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
pos : ∀ (hc₅₁₂ : Collinear ℝ (P := P) {p₅, p₁, p₂}), (∡ p₁ p₅ p₂).sign = (∡ p₃ p₅ p₄).sign
neg : ∀ (hc₅₁₂ : ¬Collinear ℝ (P := P) {p₅, p₁, p₂}), (∡ p₁ p₅ p₂).sign = (∡ p₃ p₅ p₄).sign
⊢ (∡ p₁ p₅ p₂).sign = (∡ p₃ p₅ p₄).sign

Tactic:
by_cases hc₅₁₂ : Collinear ℝ ({p₅, p₁, p₂} : Set P)

Premises used: Real, Collinear, Insert.insert, Singleton.singleton
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
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₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : Collinear ℝ (P := P) {p₅, p₁, p₂}
⊢ Collinear ℝ (P := P) {p₅, p₁, p₂, p₃, p₄}

Tactic:
have hc₅₁₂₃₄ : Collinear ℝ ({p₅, p₁, p₂, p₃, p₄} : Set P) :=
      (hc.collinear_insert_iff_of_ne (Set.mem_insert _ _)
        (Set.mem_insert_of_mem _ (Set.mem_insert _ _)) hp₁p₂).2 hc₅₁₂
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
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₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : Collinear ℝ (P := P) {p₅, p₁, p₂}
hc₅₁₂₃₄ : Collinear ℝ (P := P) {p₅, p₁, p₂, p₃, p₄}
⊢ Collinear ℝ (P := P) {p₅, p₃, p₄}

Tactic:
have hc₅₃₄ : Collinear ℝ ({p₅, p₃, p₄} : Set P) :=
      (hc.collinear_insert_iff_of_ne
        (Set.mem_insert_of_mem _ (Set.mem_insert_of_mem _ (Set.mem_insert _ _)))
        (Set.mem_insert_of_mem _ (Set.mem_insert_of_mem _ (Set.mem_insert_of_mem _
          (Set.mem_singleton _)))) hp₃p₄).1 hc₅₁₂₃₄
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
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₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : Collinear ℝ (P := P) {p₅, p₁, p₂}
hc₅₁₂₃₄ : Collinear ℝ (P := P) {p₅, p₁, p₂, p₃, p₄}
hc₅₃₄ : Collinear ℝ (P := P) {p₅, p₃, p₄}
⊢ Collinear ℝ (P := P) {p₁, p₅, p₂}

Tactic:
rw [Set.insert_comm] at hc₅₁₂ hc₅₃₄

Premises used: Set.insert_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
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₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : Collinear ℝ (P := P) {p₅, p₁, p₂}
hc₅₁₂₃₄ : Collinear ℝ (P := P) {p₅, p₁, p₂, p₃, p₄}
hc₅₃₄ : Collinear ℝ (P := P) {p₅, p₃, p₄}
hc₅₁₃ : Collinear ℝ (P := P) {p₁, p₅, p₂}
⊢ Collinear ℝ (P := P) {p₅, p₁, p₂, p₃, p₄}

Tactic:
rw [Set.insert_comm] at hc₅₁₂ hc₅₃₄

Premises used: Set.insert_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
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₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : Collinear ℝ (P := P) {p₅, p₁, p₂}
hc₅₁₂₃₄ : Collinear ℝ (P := P) {p₅, p₁, p₂, p₃, p₄}
hc₅₃₄ : Collinear ℝ (P := P) {p₅, p₃, p₄}
hc₅₁₃ : Collinear ℝ (P := P) {p₁, p₅, p₂}
hc₅₁₂₃₅ : Collinear ℝ (P := P) {p₅, p₁, p₂, p₃, p₄}
⊢ Collinear ℝ (P := P) {p₃, p₅, p₄}

Tactic:
rw [Set.insert_comm] at hc₅₁₂ hc₅₃₄

Premises used: Set.insert_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
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₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : Collinear ℝ (P := P) {p₁, p₅, p₂}
hc₅₁₂₃₄ : Collinear ℝ (P := P) {p₅, p₁, p₂, p₃, p₄}
hc₅₃₄ : Collinear ℝ (P := P) {p₃, p₅, p₄}
⊢ ∡ p₁ p₅ p₂ = 0 ∨ ∡ p₁ p₅ p₂ = (↑π : Real.Angle)

Tactic:
have hs₁₅₂ := oangle_eq_zero_or_eq_pi_iff_collinear.2 hc₅₁₂
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
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₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : Collinear ℝ (P := P) {p₁, p₅, p₂}
hc₅₁₂₃₄ : Collinear ℝ (P := P) {p₅, p₁, p₂, p₃, p₄}
hc₅₃₄ : Collinear ℝ (P := P) {p₃, p₅, p₄}
hs₁₅₂ : ∡ p₁ p₅ p₂ = 0 ∨ ∡ p₁ p₅ p₂ = (↑π : Real.Angle)
⊢ ∡ p₃ p₅ p₄ = 0 ∨ ∡ p₃ p₅ p₄ = (↑π : Real.Angle)

Tactic:
have hs₃₅₄ := oangle_eq_zero_or_eq_pi_iff_collinear.2 hc₅₃₄
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
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₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : Collinear ℝ (P := P) {p₁, p₅, p₂}
hc₅₁₂₃₄ : Collinear ℝ (P := P) {p₅, p₁, p₂, p₃, p₄}
hc₅₃₄ : Collinear ℝ (P := P) {p₃, p₅, p₄}
hs₁₅₂ : ∡ p₁ p₅ p₂ = 0 ∨ ∡ p₁ p₅ p₂ = (↑π : Real.Angle)
hs₃₅₄ : ∡ p₃ p₅ p₄ = 0 ∨ ∡ p₃ p₅ p₄ = (↑π : Real.Angle)
⊢ (∡ p₁ p₅ p₂).sign = 0

Tactic:
rw [← Real.Angle.sign_eq_zero_iff] at hs₁₅₂ hs₃₅₄

Premises used: Real.Angle.sign_eq_zero_iff
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
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₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : Collinear ℝ (P := P) {p₁, p₅, p₂}
hc₅₁₂₃₄ : Collinear ℝ (P := P) {p₅, p₁, p₂, p₃, p₄}
hc₅₃₄ : Collinear ℝ (P := P) {p₃, p₅, p₄}
hs₁₅₂ : ∡ p₁ p₅ p₂ = 0 ∨ ∡ p₁ p₅ p₂ = (↑π : Real.Angle)
hs₃₅₄ : ∡ p₃ p₅ p₄ = 0 ∨ ∡ p₃ p₅ p₄ = (↑π : Real.Angle)
hs₁₅₃ : (∡ p₁ p₅ p₂).sign = 0
⊢ (∡ p₃ p₅ p₄).sign = 0

Tactic:
rw [← Real.Angle.sign_eq_zero_iff] at hs₁₅₂ hs₃₅₄

Premises used: Real.Angle.sign_eq_zero_iff
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
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₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : Collinear ℝ (P := P) {p₁, p₅, p₂}
hc₅₁₂₃₄ : Collinear ℝ (P := P) {p₅, p₁, p₂, p₃, p₄}
hc₅₃₄ : Collinear ℝ (P := P) {p₃, p₅, p₄}
hs₁₅₂ : (∡ p₁ p₅ p₂).sign = 0
hs₃₅₄ : (∡ p₃ p₅ p₄).sign = 0
pos : 0 = (∡ p₃ p₅ p₄).sign
pos₁ pos₂ : Eq (α := SignType) 0 0
⊢ (∡ p₁ p₅ p₂).sign = (∡ p₃ p₅ p₄).sign

Tactic:
rw [hs₁₅₂, hs₃₅₄]
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
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₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ (P := P) {p₅, p₁, p₂}
s : Set (P × P × P) :=
  (fun (x : Prod.{u_2, u_1} (↥(affineSpan ℝ {p₁, p₂})) V) ↦ ((↑x.1 : P), p₅, x.2 +ᵥ (↑x.1 : P))) ''
    SProd.sprod (α := Set ↥(affineSpan ℝ {p₁, p₂})) (β := Set V) Set.univ {v : V | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
this : ConnectedSpace.{u_2} ↥(affineSpan ℝ {p₁, p₂})
⊢ ContinuousOn (Y := P × P × P)
    (fun (x : Prod.{u_2, u_1} (↥(affineSpan ℝ {p₁, p₂})) V) ↦ ((↑x.1 : P), p₅, x.2 +ᵥ (↑x.1 : P)))
    (SProd.sprod (α := Set ↥(affineSpan ℝ {p₁, p₂})) (β := Set V) Set.univ {y : V | SameRay ℝ (p₂ -ᵥ p₁) y ∧ y ≠ 0})

Tactic:
fun_prop