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)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SSameSide p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun (p : P) ↦ (p₁, p, p₂)) '' {p : P | s.SSameSide p₃ p}
hc : IsConnected sp
p' : P
hp' : s.SSameSide p₃ p'
⊢ (p₁, p', p₂).1 ≠ (p₁, p', p₂).2.1
have refine_1 : p₁ ≠ p'
Tactic: dsimp only
-- 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)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SSameSide p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun (p : P) ↦ (p₁, p, p₂)) '' {p : P | s.SSameSide p₃ p}
hc : IsConnected sp
p : P × P × P
hp : p ∈ sp
⊢ p.2.2 ≠ p.2.1
have hp₃ : ∃ (x : P), s.SSameSide p₃ x ∧ (p₁, x, p₂) = p
Tactic: simp_rw [sp, Set.mem_image, Set.mem_setOf] at hp
Cleared hypotheses: hp
-- 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)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SSameSide p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun (p : P) ↦ (p₁, p, p₂)) '' {p : P | s.SSameSide p₃ p}
hc : IsConnected sp
p : P × P × P
hp : ∃ (x : P), s.SSameSide p₃ x ∧ (p₁, x, p₂) = p
⊢ p.2.2 ≠ p.2.1
have refine_2 : ∀ (p' : P) (hp' : s.SSameSide p₃ p'), (p₁, p', p₂).2.2 ≠ (p₁, p', p₂).2.1
Tactic: obtain ⟨p', hp', rfl⟩ := hp
Cleared hypotheses: p, hp
-- 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)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SSameSide p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun (p : P) ↦ (p₁, p, p₂)) '' {p : P | s.SSameSide p₃ p}
hc : IsConnected sp
p' : P
hp' : s.SSameSide p₃ p'
⊢ (p₁, p', p₂).2.2 ≠ (p₁, p', p₂).2.1
have refine_2 : p₂ ≠ p'
Tactic: dsimp only
-- 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)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SSameSide p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun (p : P) ↦ (p₁, p, p₂)) '' {p : P | s.SSameSide p₃ p}
hc : IsConnected sp
⊢ (∡ p₁ p₄ p₂).sign = (∡ p₁ p₃ p₂).sign
have hf : ContinuousOn (Y := Real.Angle) (fun (p : P × P × P) ↦ ∡ p.1 p.2.1 p.2.2) sp
Tactic: have hf : ContinuousOn (fun p : P × P × P => ∡ p.1 p.2.1 p.2.2) sp := by
    refine continuousOn_of_forall_continuousAt fun p hp => continuousAt_oangle ?_ ?_
    all_goals
      simp_rw [sp, Set.mem_image, Set.mem_setOf] at hp
      obtain ⟨p', hp', rfl⟩ := hp
      dsimp only
      rintro rfl
    · exact hp'.2.2 hp₁
    · exact hp'.2.2 hp₂
-- 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)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SSameSide p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun (p : P) ↦ (p₁, p, p₂)) '' {p : P | s.SSameSide p₃ p}
hc : IsConnected sp
hf : ContinuousOn (Y := Real.Angle) (fun (p : P × P × P) ↦ ∡ p.1 p.2.1 p.2.2) sp
p : P × P × P
hp : p ∈ sp
⊢ ∡ p.1 p.2.1 p.2.2 ≠ 0 ∧ ∡ p.1 p.2.1 p.2.2 ≠ (↑π : Real.Angle)
have hp₃ : ∃ (x : P), s.SSameSide p₃ x ∧ (p₁, x, p₂) = p
Tactic: simp_rw [sp, Set.mem_image, Set.mem_setOf] at hp
Cleared hypotheses: hp
-- 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)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SSameSide p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun (p : P) ↦ (p₁, p, p₂)) '' {p : P | s.SSameSide p₃ p}
hc : IsConnected sp
hf : ContinuousOn (Y := Real.Angle) (fun (p : P × P × P) ↦ ∡ p.1 p.2.1 p.2.2) sp
p : P × P × P
hp : ∃ (x : P), s.SSameSide p₃ x ∧ (p₁, x, p₂) = p
⊢ ∡ p.1 p.2.1 p.2.2 ≠ 0 ∧ ∡ p.1 p.2.1 p.2.2 ≠ (↑π : Real.Angle)
have obtain : ∀ (p' : P) (hp' : s.SSameSide p₃ p'),
  ∡ (p₁, p', p₂).1 (p₁, p', p₂).2.1 (p₁, p', p₂).2.2 ≠ 0 ∧
    ∡ (p₁, p', p₂).1 (p₁, p', p₂).2.1 (p₁, p', p₂).2.2 ≠ (↑π : Real.Angle)
Tactic: obtain ⟨p', hp', rfl⟩ := hp
Cleared hypotheses: p, hp
-- 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)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SSameSide p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun (p : P) ↦ (p₁, p, p₂)) '' {p : P | s.SSameSide p₃ p}
hc : IsConnected sp
hf : ContinuousOn (Y := Real.Angle) (fun (p : P × P × P) ↦ ∡ p.1 p.2.1 p.2.2) sp
p' : P
hp' : s.SSameSide p₃ p'
⊢ ∡ (p₁, p', p₂).1 (p₁, p', p₂).2.1 (p₁, p', p₂).2.2 ≠ 0 ∧
    ∡ (p₁, p', p₂).1 (p₁, p', p₂).2.1 (p₁, p', p₂).2.2 ≠ (↑π : Real.Angle)
have dsimp : ∡ p₁ p' p₂ ≠ 0 ∧ ∡ p₁ p' p₂ ≠ (↑π : Real.Angle)
Tactic: dsimp only
-- 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)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SSameSide p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun (p : P) ↦ (p₁, p, p₂)) '' {p : P | s.SSameSide p₃ p}
hc : IsConnected sp
hf : ContinuousOn (Y := Real.Angle) (fun (p : P × P × P) ↦ ∡ p.1 p.2.1 p.2.2) sp
p' : P
hp' : s.SSameSide p₃ p'
⊢ ∡ p₁ p' p₂ ≠ 0 ∧ ∡ p₁ p' p₂ ≠ (↑π : Real.Angle)
have rw : AffineIndependent ℝ ![p₁, p', p₂]
Tactic: rw [oangle_ne_zero_and_ne_pi_iff_affineIndependent]
-- 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)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SSameSide p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun (p : P) ↦ (p₁, p, p₂)) '' {p : P | s.SSameSide p₃ p}
hc : IsConnected sp
hf : ContinuousOn (Y := Real.Angle) (fun (p : P × P × P) ↦ ∡ p.1 p.2.1 p.2.2) sp
⊢ (∡ p₁ p₄ p₂).sign = (∡ p₁ p₃ p₂).sign
have hsp : ∀ p ∈ sp, ∡ p.1 p.2.1 p.2.2 ≠ 0 ∧ ∡ p.1 p.2.1 p.2.2 ≠ (↑π : Real.Angle)
Tactic: have hsp : ∀ p : P × P × P, p ∈ sp → ∡ p.1 p.2.1 p.2.2 ≠ 0 ∧ ∡ p.1 p.2.1 p.2.2 ≠ π := by
    intro p hp
    simp_rw [sp, Set.mem_image, Set.mem_setOf] at hp
    obtain ⟨p', hp', rfl⟩ := hp
    dsimp only
    rw [oangle_ne_zero_and_ne_pi_iff_affineIndependent]
    exact affineIndependent_of_ne_of_mem_of_notMem_of_mem h hp₁ hp'.2.2 hp₂
-- 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)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SSameSide p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun (p : P) ↦ (p₁, p, p₂)) '' {p : P | s.SSameSide p₃ p}
hc : IsConnected sp
hf : ContinuousOn (Y := Real.Angle) (fun (p : P × P × P) ↦ ∡ p.1 p.2.1 p.2.2) sp
hsp : ∀ p ∈ sp, ∡ p.1 p.2.1 p.2.2 ≠ 0 ∧ ∡ p.1 p.2.1 p.2.2 ≠ (↑π : Real.Angle)
⊢ (∡ p₁ p₄ p₂).sign = (∡ p₁ p₃ p₂).sign
have hp₃ : (p₁, p₃, p₂) ∈ sp
Tactic: have hp₃ : (p₁, p₃, p₂) ∈ sp :=
    Set.mem_image_of_mem _ (sSameSide_self_iff.2 ⟨hp₃p₄.nonempty, hp₃p₄.2.1⟩)
-- 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)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SSameSide p₃ p₄
h : ¬p₁ = p₂
sp : Set (P × P × P) := (fun (p : P) ↦ (p₁, p, p₂)) '' {p : P | s.SSameSide p₃ p}
hc : IsConnected sp
hf : ContinuousOn (Y := Real.Angle) (fun (p : P × P × P) ↦ ∡ p.1 p.2.1 p.2.2) sp
hsp : ∀ p ∈ sp, ∡ p.1 p.2.1 p.2.2 ≠ 0 ∧ ∡ p.1 p.2.1 p.2.2 ≠ (↑π : Real.Angle)
hp₃ : (p₁, p₃, p₂) ∈ sp
⊢ (∡ p₁ p₄ p₂).sign = (∡ p₁ p₃ p₂).sign
have hp₄ : (p₁, p₄, p₂) ∈ sp
Tactic: have hp₄ : (p₁, p₄, p₂) ∈ sp := Set.mem_image_of_mem _ hp₃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)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SOppSide p₃ p₄
⊢ (∡ p₁ p₄ p₂).sign = -(∡ p₁ p₃ p₂).sign
have hp₁p₃ : p₁ ≠ p₃
Tactic: have hp₁p₃ : p₁ ≠ p₃ := by rintro rfl; exact hp₃p₄.left_notMem hp₁
-- 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)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SOppSide p₃ p₄
hp₁p₃ : p₁ ≠ p₃
⊢ (∡ p₁ p₄ p₂).sign = -(∡ p₁ p₃ p₂).sign
have rw : (∡ p₁ ((AffineEquiv.pointReflection ℝ p₁ : (a : P) → P) p₃) p₂).sign = -(∡ p₁ p₃ p₂).sign
Tactic: rw [← (hp₃p₄.symm.trans (sOppSide_pointReflection hp₁ hp₃p₄.left_notMem)).oangle_sign_eq hp₁ hp₂,
    ← oangle_rotate_sign p₁, ← oangle_rotate_sign p₁, oangle_swap₁₃_sign,
    (sbtw_pointReflection_of_ne ℝ hp₁p₃).symm.oangle_sign_eq _]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SOppSide p₃ p₄
hp₁p₃ : p₁ ≠ p₃
rw : (∡ p₁ ((AffineEquiv.pointReflection ℝ p₁ : (a : P) → P) p₃) p₂).sign = -(∡ p₁ p₃ p₂).sign
⊢ (∡ p₁ p₄ p₂).sign = -(∡ p₁ p₃ p₂).sign
have rw₁ : (∡ ((AffineEquiv.pointReflection ℝ p₁ : (a : P) → P) p₃) p₂ p₁).sign = -(∡ p₁ p₃ p₂).sign
Tactic: rw [← (hp₃p₄.symm.trans (sOppSide_pointReflection hp₁ hp₃p₄.left_notMem)).oangle_sign_eq hp₁ hp₂,
    ← oangle_rotate_sign p₁, ← oangle_rotate_sign p₁, oangle_swap₁₃_sign,
    (sbtw_pointReflection_of_ne ℝ hp₁p₃).symm.oangle_sign_eq _]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SOppSide p₃ p₄
hp₁p₃ : p₁ ≠ p₃
rw : (∡ p₁ ((AffineEquiv.pointReflection ℝ p₁ : (a : P) → P) p₃) p₂).sign = -(∡ p₁ p₃ p₂).sign
rw₁ : (∡ ((AffineEquiv.pointReflection ℝ p₁ : (a : P) → P) p₃) p₂ p₁).sign = -(∡ p₁ p₃ p₂).sign
⊢ (∡ p₁ p₄ p₂).sign = -(∡ p₁ p₃ p₂).sign
have rw₂ : (∡ ((AffineEquiv.pointReflection ℝ p₁ : (a : P) → P) p₃) p₂ p₁).sign = -(∡ p₃ p₂ p₁).sign
Tactic: rw [← (hp₃p₄.symm.trans (sOppSide_pointReflection hp₁ hp₃p₄.left_notMem)).oangle_sign_eq hp₁ hp₂,
    ← oangle_rotate_sign p₁, ← oangle_rotate_sign p₁, oangle_swap₁₃_sign,
    (sbtw_pointReflection_of_ne ℝ hp₁p₃).symm.oangle_sign_eq _]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SOppSide p₃ p₄
hp₁p₃ : p₁ ≠ p₃
rw : (∡ p₁ ((AffineEquiv.pointReflection ℝ p₁ : (a : P) → P) p₃) p₂).sign = -(∡ p₁ p₃ p₂).sign
rw₁ : (∡ ((AffineEquiv.pointReflection ℝ p₁ : (a : P) → P) p₃) p₂ p₁).sign = -(∡ p₁ p₃ p₂).sign
rw₂ : (∡ ((AffineEquiv.pointReflection ℝ p₁ : (a : P) → P) p₃) p₂ p₁).sign = -(∡ p₃ p₂ p₁).sign
⊢ (∡ p₁ p₄ p₂).sign = -(∡ p₁ p₃ p₂).sign
have rw₃ : (∡ ((AffineEquiv.pointReflection ℝ p₁ : (a : P) → P) p₃) p₂ p₁).sign = (∡ p₁ p₂ p₃).sign
Tactic: rw [← (hp₃p₄.symm.trans (sOppSide_pointReflection hp₁ hp₃p₄.left_notMem)).oangle_sign_eq hp₁ hp₂,
    ← oangle_rotate_sign p₁, ← oangle_rotate_sign p₁, oangle_swap₁₃_sign,
    (sbtw_pointReflection_of_ne ℝ hp₁p₃).symm.oangle_sign_eq _]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SOppSide p₃ p₄
hp₁p₃ : p₁ ≠ p₃
rw : (∡ p₁ ((AffineEquiv.pointReflection ℝ p₁ : (a : P) → P) p₃) p₂).sign = -(∡ p₁ p₃ p₂).sign
rw₁ : (∡ ((AffineEquiv.pointReflection ℝ p₁ : (a : P) → P) p₃) p₂ p₁).sign = -(∡ p₁ p₃ p₂).sign
rw₂ : (∡ ((AffineEquiv.pointReflection ℝ p₁ : (a : P) → P) p₃) p₂ p₁).sign = -(∡ p₃ p₂ p₁).sign
rw₃ : (∡ ((AffineEquiv.pointReflection ℝ p₁ : (a : P) → P) p₃) p₂ p₁).sign = (∡ p₁ p₂ p₃).sign
⊢ (∡ p₁ p₄ p₂).sign = -(∡ p₁ p₃ p₂).sign
have rw₄ : (∡ p₁ p₂ p₃).sign = (∡ p₁ p₂ p₃).sign
Tactic: rw [← (hp₃p₄.symm.trans (sOppSide_pointReflection hp₁ hp₃p₄.left_notMem)).oangle_sign_eq hp₁ hp₂,
    ← oangle_rotate_sign p₁, ← oangle_rotate_sign p₁, oangle_swap₁₃_sign,
    (sbtw_pointReflection_of_ne ℝ hp₁p₃).symm.oangle_sign_eq _]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Affine (goal)
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ≠ p₂
hp₄ : p₄ ≠ p₂
⊢ ∠ p₁ p₂ p₃ = ∠ p₃ p₂ p₄ ↔ ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ ∨ Wbtw ℝ p₂ p₁ p₄ ∨ Wbtw ℝ p₂ p₄ p₁
have simp_rw : Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = Orientation.oangle o (p₃ -ᵥ p₂) (p₄ -ᵥ p₂) ∨
    SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂) ↔
  Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = Orientation.oangle o (p₃ -ᵥ p₂) (p₄ -ᵥ p₂) ∨
    Wbtw ℝ p₂ p₁ p₄ ∨ Wbtw ℝ p₂ p₄ p₁
Tactic: simp_rw [angle, oangle,
    o.angle_eq_iff_oangle_eq_or_sameRay (vsub_ne_zero.2 hp₁) (vsub_ne_zero.2 hp₄)]
-- 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
hp₁ : p₁ ≠ p₂
hp₄ : p₄ ≠ p₂
⊢ Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = Orientation.oangle o (p₃ -ᵥ p₂) (p₄ -ᵥ p₂) ∨
      SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂) ↔
    Orientation.oangle o (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = Orientation.oangle o (p₃ -ᵥ p₂) (p₄ -ᵥ p₂) ∨
      Wbtw ℝ p₂ p₁ p₄ ∨ Wbtw ℝ p₂ p₄ p₁
have h : SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂) ↔ Wbtw ℝ p₂ p₁ p₄ ∨ Wbtw ℝ p₂ p₄ p₁
Tactic: apply or_congr_right
-- 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
hp₁ : p₁ ≠ p₂
hp₄ : p₄ ≠ p₂
⊢ SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂) ↔ Wbtw ℝ p₂ p₁ p₄ ∨ Wbtw ℝ p₂ p₄ p₁
have h : ∀ (h : SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂)), Wbtw ℝ p₂ p₁ p₄ ∨ Wbtw ℝ p₂ p₄ p₁
Tactic: refine ⟨fun h ↦ ?_, fun 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
hp₁ : p₁ ≠ p₂
hp₄ : p₄ ≠ p₂
h : ∀ (h : SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂)), Wbtw ℝ p₂ p₁ p₄ ∨ Wbtw ℝ p₂ p₄ p₁
⊢ SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂) ↔ Wbtw ℝ p₂ p₁ p₄ ∨ Wbtw ℝ p₂ p₄ p₁
have h₁ : ∀ (h : Wbtw ℝ p₂ p₁ p₄ ∨ Wbtw ℝ p₂ p₄ p₁), SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂)
Tactic: refine ⟨fun h ↦ ?_, fun 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
hp₁ : p₁ ≠ p₂
hp₄ : p₄ ≠ p₂
h : SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂)
⊢ Wbtw ℝ p₂ p₁ p₄ ∨ Wbtw ℝ p₂ p₄ p₁
have h₁ : ∀ (r : ℝ) (hr : 0 < r) (he : r • (p₁ -ᵥ p₂) = p₄ -ᵥ p₂), Wbtw ℝ p₂ p₁ p₄ ∨ Wbtw ℝ p₂ p₄ p₁
Tactic: obtain ⟨r, hr, he⟩ := h.exists_pos_left (vsub_ne_zero.2 hp₁) (vsub_ne_zero.2 hp₄)
-- 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
hp₁ : p₁ ≠ p₂
hp₄ : p₄ ≠ p₂
h : SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂)
r : ℝ
hr : 0 < r
he : r • (p₁ -ᵥ p₂) = p₄ -ᵥ p₂
⊢ Wbtw ℝ p₂ p₁ p₄ ∨ Wbtw ℝ p₂ p₄ p₁
have h₁ : Wbtw ℝ p₂ ((p₁ -ᵥ p₂) +ᵥ p₂) (r • (p₁ -ᵥ p₂) +ᵥ p₂) ∨ Wbtw ℝ p₂ (r • (p₁ -ᵥ p₂) +ᵥ p₂) ((p₁ -ᵥ p₂) +ᵥ p₂)
Tactic: rw [← vsub_vadd p₁ p₂, ← vsub_vadd p₄ p₂, ← he]
-- 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
hp₁ : p₁ ≠ p₂
hp₄ : p₄ ≠ p₂
h : SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂)
r : ℝ
hr : 0 < r
he : r • (p₁ -ᵥ p₂) = p₄ -ᵥ p₂
⊢ Wbtw ℝ p₂ ((p₁ -ᵥ p₂) +ᵥ p₂) (r • (p₁ -ᵥ p₂) +ᵥ p₂) ∨ Wbtw ℝ p₂ (r • (p₁ -ᵥ p₂) +ᵥ p₂) ((p₁ -ᵥ p₂) +ᵥ p₂)
have h₁ : Wbtw ℝ p₂ (HSMul.hSMul (α := ℝ) 1 (p₁ -ᵥ p₂) +ᵥ p₂) (r • (p₁ -ᵥ p₂) +ᵥ p₂) ∨
  Wbtw ℝ p₂ (r • (p₁ -ᵥ p₂) +ᵥ p₂) (HSMul.hSMul (α := ℝ) 1 (p₁ -ᵥ p₂) +ᵥ p₂)
Tactic: nth_rw 1 4 [← one_smul ℝ (p₁ -ᵥ 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
hp₁ : p₁ ≠ p₂
hp₄ : p₄ ≠ p₂
h : Wbtw ℝ p₂ p₁ p₄ ∨ Wbtw ℝ p₂ p₄ p₁
⊢ SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂)
have h₁ : ∀ (h : Wbtw ℝ p₂ p₁ p₄), SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂)
Tactic: rcases h with h | h
Cleared hypotheses: 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
hp₁ : p₁ ≠ p₂
hp₄ : p₄ ≠ p₂
h : Wbtw ℝ p₂ p₁ p₄ ∨ Wbtw ℝ p₂ p₄ p₁
h₁ : ∀ (h : Wbtw ℝ p₂ p₁ p₄), SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂)
⊢ SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂)
have h₂ : ∀ (h : Wbtw ℝ p₂ p₄ p₁), SameRay ℝ (p₁ -ᵥ p₂) (p₄ -ᵥ p₂)
Tactic: rcases h with h | 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₄
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₄
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₄
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
this : ((∡ p₁ p₂ p₃).toReal + (∡ p₃ p₂ p₄).toReal) / 2 = (∡ p₁ p₂ p₄).toReal / 2
⊢ ∠ p₁ p₂ p₃ = ∠ p₁ p₂ p₄ / 2
have this₁ : (∡ p₁ p₂ p₃).toReal = (∡ p₁ p₂ p₄).toReal / 2
Tactic: rw [← ha, add_self_div_two] at this
Cleared hypotheses: this
-- 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₂
this : (∡ p₁ p₂ p₃).toReal = (∡ p₁ p₂ p₄).toReal / 2
⊢ ∠ p₁ p₂ p₃ = ∠ p₁ p₂ p₄ / 2
have rw : |(∡ p₁ p₂ p₄).toReal| / |2| = |(∡ p₁ p₂ p₄).toReal| / 2
Tactic: rw [angle_eq_abs_oangle_toReal h₁₂ h₃₂, angle_eq_abs_oangle_toReal h₁₂ h₄₂, this, abs_div]
-- 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₂
⊢ ∠ p₁ p₂ p₃ = ∠ p₁ p₂ p₄ / 2
have suffices : ((∡ p₁ p₂ p₃).toReal + (∡ p₃ p₂ p₄).toReal) / 2 = (∡ p₁ p₂ p₄).toReal / 2
Tactic: suffices ((∡ p₁ p₂ p₃).toReal + (∡ p₃ p₂ p₄).toReal) / 2 = (∡ p₁ p₂ p₄).toReal / 2 by
    rw [← ha, add_self_div_two] at this
    rw [angle_eq_abs_oangle_toReal h₁₂ h₃₂, angle_eq_abs_oangle_toReal h₁₂ h₄₂, this, abs_div]
    simp
-- 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₂
⊢ ((∡ p₁ p₂ p₃).toReal + (∡ p₃ p₂ p₄).toReal) / 2 = (∡ p₁ p₂ p₄).toReal / 2
have hadd : ∡ p₁ p₂ p₃ + ∡ p₃ p₂ p₄ = ∡ p₁ p₂ p₄
Tactic: have hadd := oangle_add h₁₂ h₃₂ h₄₂