awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h : Collinear ℝ (P := P) {p₁, p₂, p₁'}
hp₁p₂ : p₁ ≠ p₂
hp₁'p₂ : p₁' ≠ p₂
hp₃p₂ : ¬p₃ = p₂
hw : Wbtw ℝ p₁' p₁ p₂
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)
have neg : HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁' p₂ p₃)
Tactic: rw [hw.symm.oangle_eq_left hp₁p₂]
-- 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
h : Collinear ℝ (P := P) {p₃, p₂, p₃'}
hp₃p₂ : p₃ ≠ p₂
hp₃'p₂ : p₃' ≠ p₂
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃')
have rw : 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]
-- 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
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₃')
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃')
have rw₁ : -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]
-- 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
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₃')
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃')
have rw₂ : -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]
-- 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
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₃')
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃')
have rw₃ : 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]
-- 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
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₃')
⊢ HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃) = HSMul.hSMul (α := ℤ) 2 (∡ p₁ p₂ p₃')
have rw₄ : 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]
-- 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₂
⊢ 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
have 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
Tactic: refine ⟨fun hd => ?_, fun hr => ?_⟩
-- 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₂
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
⊢ 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
have 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
Tactic: refine ⟨fun hd => ?_, fun hr => ?_⟩
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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)
p₁ p₂ p : P
h : p₁ ≠ p₂
hd : dist p₁ p = dist p₂ p
⊢ ⟪p₂ -ᵥ p₁, p -ᵥ midpoint ℝ p₁ p₂⟫ = 0
have hd₁ : ⟪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
Cleared hypotheses: hd
-- 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₂
hd : ⟪p -ᵥ p₁, p -ᵥ p₁⟫ = ⟪p -ᵥ p₂, p -ᵥ p₂⟫
⊢ ⟪p₂ -ᵥ p₁, p -ᵥ midpoint ℝ p₁ p₂⟫ = 0
have 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
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₁)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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)
p₁ p₂ p : P
h : p₁ ≠ p₂
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
have hi : ⟪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
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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)
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) +ᵥ
        midpoint ℝ p₁ p₂ =
      p
have hi₁ : ∃ (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
Cleared hypotheses: hi
-- 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₂
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₂
⊢ ∃ (r : ℝ),
    HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) +ᵥ
        midpoint ℝ p₁ p₂ =
      p
have 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
Tactic: rcases hi with ⟨r, hr⟩
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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)
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₂
⊢ ∃ (r : ℝ),
    HSMul.hSMul (β := V) r ((Orientation.rotation o (↑(π / 2) : Real.Angle) : (a : V) → V) (p₂ -ᵥ p₁) : V) +ᵥ
        midpoint ℝ p₁ p₂ =
      p
have hr₁ : 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
Cleared hypotheses: hr
-- 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₂
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
have 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₂)
Tactic: rcases hr with ⟨r, rfl⟩
Cleared hypotheses: p, hr
-- 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
h : p₁ ≠ p₂
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₂)
have 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)⟫
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]
-- 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₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
⊢ (∡ p₁ p₅ p₂).sign = (∡ p₃ p₅ p₄).sign
have pos : ∀ (hc₅₁₂ : Collinear ℝ (P := P) {p₅, p₁, p₂}), (∡ p₁ p₅ p₂).sign = (∡ p₃ p₅ p₄).sign
Tactic: by_cases hc₅₁₂ : Collinear ℝ ({p₅, p₁, p₂} : Set P)
-- 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₅ : 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
⊢ (∡ p₁ p₅ p₂).sign = (∡ p₃ p₅ p₄).sign
have neg : ∀ (hc₅₁₂ : ¬Collinear ℝ (P := P) {p₅, p₁, p₂}), (∡ p₁ p₅ p₂).sign = (∡ p₃ p₅ p₄).sign
Tactic: by_cases hc₅₁₂ : Collinear ℝ ({p₅, p₁, p₂} : Set P)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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)
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₂}
⊢ (∡ p₁ p₅ p₂).sign = (∡ p₃ p₅ p₄).sign
have hc₅₁₂₃₄ : 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₅₁₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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)
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₄}
⊢ (∡ p₁ p₅ p₂).sign = (∡ p₃ p₅ p₄).sign
have hc₅₃₄ : 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₅₁₂₃₄
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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)
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₂).sign = (∡ p₃ p₅ p₄).sign
have hc₅₁₃ : Collinear ℝ (P := P) {p₁, p₅, p₂}
Tactic: rw [Set.insert_comm] at hc₅₁₂ hc₅₃₄
Cleared hypotheses: hc₅₁₂, hc₅₁₂₃₄, hc₅₃₄
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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)
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₄}
⊢ (∡ p₁ p₅ p₂).sign = (∡ p₃ p₅ p₄).sign
have hc₅₃₅ : Collinear ℝ (P := P) {p₃, p₅, p₄}
Tactic: rw [Set.insert_comm] at hc₅₁₂ hc₅₃₄
Cleared hypotheses: hc₅₁₂, hc₅₁₂₃₄, hc₅₃₄
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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)
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₂).sign = (∡ p₃ p₅ p₄).sign
have hs₁₅₂ : ∡ p₁ p₅ p₂ = 0 ∨ ∡ p₁ p₅ p₂ = (↑π : Real.Angle)
Tactic: have hs₁₅₂ := oangle_eq_zero_or_eq_pi_iff_collinear.2 hc₅₁₂
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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)
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₂).sign = (∡ p₃ p₅ p₄).sign
have hs₃₅₄ : ∡ p₃ p₅ p₄ = 0 ∨ ∡ p₃ p₅ p₄ = (↑π : Real.Angle)
Tactic: have hs₃₅₄ := oangle_eq_zero_or_eq_pi_iff_collinear.2 hc₅₃₄
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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)
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 = (∡ p₃ p₅ p₄).sign
have hs₁₅₃ : (∡ p₁ p₅ p₂).sign = 0
Tactic: rw [← Real.Angle.sign_eq_zero_iff] at hs₁₅₂ hs₃₅₄
Cleared hypotheses: hs₁₅₂, hs₃₅₄
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (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)
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 = (∡ p₃ p₅ p₄).sign
have hs₃₅₅ : (∡ p₃ p₅ p₄).sign = 0
Tactic: rw [← Real.Angle.sign_eq_zero_iff] at hs₁₅₂ hs₃₅₄
Cleared hypotheses: hs₁₅₂, hs₃₅₄
-- 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₅ : 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
⊢ (∡ p₁ p₅ p₂).sign = (∡ p₃ p₅ p₄).sign
have pos : 0 = (∡ p₃ p₅ p₄).sign
Tactic: rw [hs₁₅₂, hs₃₅₄]
-- 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₅ : 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
⊢ (∡ p₁ p₅ p₂).sign = (∡ p₃ p₅ p₄).sign
have pos₁ : Eq (α := SignType) 0 0
Tactic: rw [hs₁₅₂, hs₃₅₄]