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₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
hadd : ∡ p₁ p₂ p₃ + ∡ p₃ p₂ p₄ = ∡ p₁ p₂ p₄
⊢ ((∡ p₁ p₂ p₃).toReal + (∡ p₃ p₂ p₄).toReal) / 2 = (∡ p₁ p₂ p₄).toReal / 2
have rw : (∡ p₁ p₂ p₃).toReal + (∡ p₃ p₂ p₄).toReal = (∡ p₁ p₂ p₃ + ∡ p₃ p₂ p₄).toReal
Tactic: rw [div_left_inj' (by norm_num), ← hadd]
-- 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
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
hadd : ∡ p₁ p₂ p₃ + ∡ p₃ p₂ p₄ = ∡ p₁ p₂ p₄
⊢ (∡ p₁ p₂ p₃).toReal + (∡ p₃ p₂ p₄).toReal = (∡ p₁ p₂ p₃ + ∡ p₃ p₂ p₄).toReal
have h : ∡ p₁ p₂ p₃ ≠ (↑π : Real.Angle)
Tactic: have h : ∡ p₁ p₂ p₃ ≠ π := fun h ↦ hs.left_notMem ((oangle_eq_zero_or_eq_pi_iff_collinear.1
    (.inr h)).mem_affineSpan_of_mem_of_ne (by grind) (by grind) (by grind) h₁₂)
-- 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₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
hadd : ∡ p₁ p₂ p₃ + ∡ p₃ p₂ p₄ = ∡ p₁ p₂ p₄
h : ∡ p₁ p₂ p₃ ≠ (↑π : Real.Angle)
⊢ (∡ p₁ p₂ p₃).toReal + (∡ p₃ p₂ p₄).toReal = (∡ p₁ p₂ p₃ + ∡ p₃ p₂ p₄).toReal
have refine : (∡ p₁ p₂ p₃).sign = (∡ p₁ p₂ p₃ + ∡ p₃ p₂ p₄).sign
Tactic: refine (Real.Angle.toReal_add_eq_toReal_add_toReal h (ha ▸ h) (.inr ?_)).symm
-- 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₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
hadd : ∡ p₁ p₂ p₃ + ∡ p₃ p₂ p₄ = ∡ p₁ p₂ p₄
h : ∡ p₁ p₂ p₃ ≠ (↑π : Real.Angle)
⊢ (∡ p₁ p₂ p₃).sign = (∡ p₁ p₂ p₃ + ∡ p₃ p₂ p₄).sign
have rw : (∡ p₁ p₄ p₂).sign = (∡ p₁ p₃ p₂).sign
Tactic: rw [hadd, ← oangle_swap₂₃_sign p₁ p₃ p₂, ← oangle_swap₂₃_sign p₁ p₄ p₂, neg_inj, eq_comm]
-- 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
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SOppSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
⊢ ∠ p₁ p₂ p₃ = π - ∠ p₁ p₂ p₄ / 2
have h₃₂ : p₃ ≠ p₂
Tactic: have h₃₂ : p₃ ≠ p₂ := by
    rintro rfl
    exact hs.left_notMem (right_mem_affineSpan_pair _ _ _)
-- 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
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SOppSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
⊢ ∠ p₁ p₂ p₃ = π - ∠ p₁ p₂ p₄ / 2
have h₄₂ : p₄ ≠ p₂
Tactic: have h₄₂ : p₄ ≠ p₂ := by
    rintro rfl
    exact hs.right_notMem (right_mem_affineSpan_pair _ _ _)
-- 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₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SOppSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
⊢ ∡ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) =
    ∡ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) p₂ p₄
have rw : ∡ p₁ p₂ p₃ + (↑π : Real.Angle) = ∡ p₃ p₂ p₄ + (↑π : Real.Angle)
Tactic: rw [oangle_pointReflection_left h₃₂ h₄₂, oangle_pointReflection_right h₁₂ h₃₂]
-- 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
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SOppSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
⊢ ∠ p₁ p₂ p₃ = π - ∠ p₁ p₂ p₄ / 2
have ha' : ∡ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) =
  ∡ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) p₂ p₄
Tactic: have ha' : ∡ p₁ p₂ (AffineEquiv.pointReflection ℝ p₂ p₃) =
      ∡ (AffineEquiv.pointReflection ℝ p₂ p₃) p₂ p₄ := by
    rw [oangle_pointReflection_left h₃₂ h₄₂, oangle_pointReflection_right h₁₂ h₃₂]
    simpa using ha
-- 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
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SOppSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
ha' :
  ∡ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) =
    ∡ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) p₂ p₄
⊢ ∠ p₁ p₂ p₃ = π - ∠ p₁ p₂ p₄ / 2
have hs' : SOppSide (affineSpan ℝ {p₁, p₂}) p₃ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃)
Tactic: have hs' : line[ℝ, p₁, p₂].SOppSide p₃ (AffineEquiv.pointReflection ℝ p₂ p₃) :=
    AffineSubspace.sOppSide_pointReflection (right_mem_affineSpan_pair _ _ _) (hs.left_notMem)
-- 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
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SOppSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
ha' :
  ∡ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) =
    ∡ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) p₂ p₄
hs' : SOppSide (affineSpan ℝ {p₁, p₂}) p₃ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃)
⊢ ∠ p₁ p₂ p₃ = π - ∠ p₁ p₂ p₄ / 2
have h : ∠ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) = ∠ p₁ p₂ p₄ / 2
Tactic: obtain h := angle_eq_angle_div_two_of_oangle_eq_of_sSameSide h₁₂ ha' (hs'.symm.trans 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
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SOppSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
ha' :
  ∡ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) =
    ∡ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) p₂ p₄
hs' : SOppSide (affineSpan ℝ {p₁, p₂}) p₃ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃)
h : ∠ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) = ∠ p₁ p₂ p₄ / 2
⊢ ∠ p₁ p₂ p₃ = π - ∠ p₁ p₂ p₄ / 2
have h₁ : π - ∠ p₁ p₂ p₃ = ∠ p₁ p₂ p₄ / 2
Tactic: rw [angle_pointReflection_right] at h
Cleared hypotheses: h
-- 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
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + (↑π : Real.Angle)
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
⊢ ∠ p₁ p₂ p₃ = (∠ p₁ p₂ p₄ + π) / 2
have h₃₂ : p₃ ≠ p₂
Tactic: have h₃₂ : p₃ ≠ p₂ := by
    rintro rfl
    exact hs.left_notMem (right_mem_affineSpan_pair _ _ _)
-- 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
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + (↑π : Real.Angle)
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
⊢ ∠ p₁ p₂ p₃ = (∠ p₁ p₂ p₄ + π) / 2
have h₄₂ : p₄ ≠ p₂
Tactic: have h₄₂ : p₄ ≠ p₂ := by
    rintro rfl
    exact hs.right_notMem (right_mem_affineSpan_pair _ _ _)
-- 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
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + (↑π : Real.Angle)
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
⊢ ∠ p₁ p₂ p₃ = (∠ p₁ p₂ p₄ + π) / 2
have ha' : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₄)
Tactic: have ha' : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ (AffineEquiv.pointReflection ℝ p₂ p₄) := by
    rw [oangle_pointReflection_right h₃₂ h₄₂]
    exact ha
-- 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
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + (↑π : Real.Angle)
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
ha' : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₄)
⊢ ∠ p₁ p₂ p₃ = (∠ p₁ p₂ p₄ + π) / 2
have hs' : SOppSide (affineSpan ℝ {p₁, p₂}) p₄ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₄)
Tactic: have hs' : line[ℝ, p₁, p₂].SOppSide p₄ (AffineEquiv.pointReflection ℝ p₂ p₄) :=
    AffineSubspace.sOppSide_pointReflection (right_mem_affineSpan_pair _ _ _) (hs.right_notMem)
-- 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
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + (↑π : Real.Angle)
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
ha' : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₄)
hs' : SOppSide (affineSpan ℝ {p₁, p₂}) p₄ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₄)
⊢ ∠ p₁ p₂ p₃ = (∠ p₁ p₂ p₄ + π) / 2
have h : ∠ p₁ p₂ p₃ = π - ∠ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₄) / 2
Tactic: obtain h := angle_eq_pi_sub_angle_div_two_of_oangle_eq_of_sOppSide h₁₂ ha' (hs.trans_sOppSide 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
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + (↑π : Real.Angle)
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
ha' : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₄)
hs' : SOppSide (affineSpan ℝ {p₁, p₂}) p₄ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₄)
h : ∠ p₁ p₂ p₃ = π - ∠ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₄) / 2
⊢ ∠ p₁ p₂ p₃ = (∠ p₁ p₂ p₄ + π) / 2
have h₁ : ∠ p₁ p₂ p₃ = π - (π - ∠ p₁ p₂ p₄) / 2
Tactic: rw [angle_pointReflection_right] at h
Cleared hypotheses: h
-- 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
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + (↑π : Real.Angle)
hs : SOppSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
⊢ ∠ p₁ p₂ p₃ = (π - ∠ p₁ p₂ p₄) / 2
have h₃₂ : p₃ ≠ p₂
Tactic: have h₃₂ : p₃ ≠ p₂ := by
    rintro rfl
    exact hs.left_notMem (right_mem_affineSpan_pair _ _ _)
-- 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
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + (↑π : Real.Angle)
hs : SOppSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
⊢ ∠ p₁ p₂ p₃ = (π - ∠ p₁ p₂ p₄) / 2
have h₄₂ : p₄ ≠ p₂
Tactic: have h₄₂ : p₄ ≠ p₂ := by
    rintro rfl
    exact hs.right_notMem (right_mem_affineSpan_pair _ _ _)
-- 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
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + (↑π : Real.Angle)
hs : SOppSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
⊢ ∠ p₁ p₂ p₃ = (π - ∠ p₁ p₂ p₄) / 2
have ha' : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₄)
Tactic: have ha' : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ (AffineEquiv.pointReflection ℝ p₂ p₄) := by
    rw [oangle_pointReflection_right h₃₂ h₄₂]
    exact ha
-- 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
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + (↑π : Real.Angle)
hs : SOppSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
ha' : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₄)
⊢ ∠ p₁ p₂ p₃ = (π - ∠ p₁ p₂ p₄) / 2
have hs' : SOppSide (affineSpan ℝ {p₁, p₂}) p₄ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₄)
Tactic: have hs' : line[ℝ, p₁, p₂].SOppSide p₄ (AffineEquiv.pointReflection ℝ p₂ p₄) :=
    AffineSubspace.sOppSide_pointReflection (right_mem_affineSpan_pair _ _ _) (hs.right_notMem)
-- 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
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + (↑π : Real.Angle)
hs : SOppSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
ha' : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₄)
hs' : SOppSide (affineSpan ℝ {p₁, p₂}) p₄ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₄)
⊢ ∠ p₁ p₂ p₃ = (π - ∠ p₁ p₂ p₄) / 2
have h : ∠ p₁ p₂ p₃ = ∠ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₄) / 2
Tactic: obtain h := angle_eq_angle_div_two_of_oangle_eq_of_sSameSide h₁₂ ha' (hs.trans hs')
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V × V
hx1 : x.1 ≠ 0
hx2 : x.2 ≠ 0
⊢ ContinuousAt (Y := Real.Angle) (fun (y : V × V) ↦ o.oangle y.1 y.2) x
have refine_1 : Ne (α := ℂ) ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x.1 : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) x.2 : ℂ) (0 : ℂ)
Tactic: refine (Complex.continuousAt_arg_coe_angle ?_).comp ?_
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V × V
hx1 : x.1 ≠ 0
hx2 : x.2 ≠ 0
refine_1 : Ne (α := ℂ) ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x.1 : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) x.2 : ℂ) (0 : ℂ)
⊢ ContinuousAt (Y := Real.Angle) (fun (y : V × V) ↦ o.oangle y.1 y.2) x
have refine_2 : ContinuousAt (Y := ℂ) (fun (y : V × V) ↦ (((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) y.1 : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y.2) x
Tactic: refine (Complex.continuousAt_arg_coe_angle ?_).comp ?_
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
⊢ o.oangle x x = 0
have rw : (↑(↑(HPow.hPow (β := ℕ) ‖x‖ 2) : ℂ).arg : Real.Angle) = 0
Tactic: rw [oangle, kahler_apply_self, ← ofReal_pow]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
⊢ (↑(↑(HPow.hPow (β := ℕ) ‖x‖ 2) : ℂ).arg : Real.Angle) = 0
have h : Real.Angle = HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples (2 * π)) →
  (↑(HPow.hPow (β := ℕ) ‖x‖ 2) : ℂ).arg = 0
Tactic: convert! QuotientAddGroup.mk_zero (AddSubgroup.zmultiples (2 * π))
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
e_1 : Real.Angle = HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples (2 * π))
⊢ (↑(HPow.hPow (β := ℕ) ‖x‖ 2) : ℂ).arg = 0
have h : 0 ≤ HPow.hPow (β := ℕ) ‖x‖ 2
Tactic: apply arg_ofReal_of_nonneg
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ o.oangle (-x) y = o.oangle x y + (↑π : Real.Angle)
have simp : (↑(arg (((-(o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) =
  (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) + (↑π : Real.Angle)
Tactic: simp only [oangle, map_neg]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ (↑(arg (((-(o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) =
    (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) + (↑π : Real.Angle)
have convert_2 : Ne (α := ℂ) ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ) (0 : ℂ)
Tactic: convert! Complex.arg_neg_coe_angle _
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ o.oangle x (-y) = o.oangle x y + (↑π : Real.Angle)
have simp : (↑(arg (-(((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) =
  (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) + (↑π : Real.Angle)
Tactic: simp only [oangle, map_neg]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ (↑(arg (-(((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) =
    (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) + (↑π : Real.Angle)
have convert_2 : Ne (α := ℂ) ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ) (0 : ℂ)
Tactic: convert! Complex.arg_neg_coe_angle _
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle (-x) y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
have pos : ∀ (hx : x = 0), HSMul.hSMul (α := ℤ) 2 (o.oangle (-x) y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
pos : ∀ (hx : x = 0), HSMul.hSMul (α := ℤ) 2 (o.oangle (-x) y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle (-x) y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
have neg : ∀ (hx : ¬x = 0), HSMul.hSMul (α := ℤ) 2 (o.oangle (-x) y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle (-x) y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
have pos : ∀ (hy : y = 0), HSMul.hSMul (α := ℤ) 2 (o.oangle (-x) y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
pos : ∀ (hy : y = 0), HSMul.hSMul (α := ℤ) 2 (o.oangle (-x) y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle (-x) y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
have neg : ∀ (hy : ¬y = 0), HSMul.hSMul (α := ℤ) 2 (o.oangle (-x) y) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle x (-y)) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
have pos : ∀ (hx : x = 0), HSMul.hSMul (α := ℤ) 2 (o.oangle x (-y)) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
pos : ∀ (hx : x = 0), HSMul.hSMul (α := ℤ) 2 (o.oangle x (-y)) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle x (-y)) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
have neg : ∀ (hx : ¬x = 0), HSMul.hSMul (α := ℤ) 2 (o.oangle x (-y)) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
⊢ HSMul.hSMul (α := ℤ) 2 (o.oangle x (-y)) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
have pos : ∀ (hy : y = 0), HSMul.hSMul (α := ℤ) 2 (o.oangle x (-y)) = HSMul.hSMul (α := ℤ) 2 (o.oangle x y)
Tactic: by_cases hy : y = 0