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₅ : 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}
hco : IsConnected s
hf : ContinuousOn (Y := Real.Angle) (fun (p : P × P × P) ↦ ∡ p.1 p.2.1 p.2.2) s
q : P
r : ℝ
hv0 : r • (p₂ -ᵥ p₁) ≠ 0
hq : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) q
⊢ Membership.mem (γ := Submodule ℝ V) (direction (P := P) (affineSpan ℝ {p₁, p₂})) (r • (p₂ -ᵥ p₁))
have refine_2 : Membership.mem (γ := Submodule ℝ V) (vectorSpan ℝ (P := P) {p₁, p₂}) (r • (p₂ -ᵥ p₁))
Tactic: rw [direction_affineSpan]
-- 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₂}
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}
hco : IsConnected s
hf : ContinuousOn (Y := Real.Angle) (fun (p : P × P × P) ↦ ∡ p.1 p.2.1 p.2.2) s
⊢ (∡ p₁ p₅ p₂).sign = (∡ p₃ p₅ p₄).sign
have hsp : ∀ p ∈ s, ∡ 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 ∈ s → ∡ p.1 p.2.1 p.2.2 ≠ 0 ∧ ∡ p.1 p.2.1 p.2.2 ≠ π := by
      intro p hp
      simp_rw [s, Set.mem_image, Set.mem_prod, Set.mem_setOf, Set.mem_univ, true_and,
        Prod.ext_iff] at hp
      obtain ⟨q₁, q₅, q₂⟩ := p
      dsimp only at hp ⊢
      obtain ⟨⟨⟨q, hq⟩, v⟩, hv, rfl, rfl, rfl⟩ := hp
      dsimp only [Subtype.coe_mk, Set.mem_setOf] at hv ⊢
      obtain ⟨hvr, hv0⟩ := hv
      rw [← exists_nonneg_left_iff_sameRay (vsub_ne_zero.2 hp₁p₂.symm)] at hvr
      obtain ⟨r, -, rfl⟩ := hvr
      change q ∈ line[ℝ, p₁, p₂] at hq
      rw [oangle_ne_zero_and_ne_pi_iff_affineIndependent]
      refine affineIndependent_of_ne_of_mem_of_notMem_of_mem ?_ hq
          (fun h => hc₅₁₂ ((collinear_insert_iff_of_mem_affineSpan h).2 (collinear_pair _ _ _))) ?_
      · rwa [← @vsub_ne_zero V, vsub_vadd_eq_vsub_sub, vsub_self, zero_sub, neg_ne_zero]
      · refine vadd_mem_of_mem_direction ?_ hq
        rw [direction_affineSpan]
        exact smul_vsub_rev_mem_vectorSpan_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₅ : 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}
hco : IsConnected s
hf : ContinuousOn (Y := Real.Angle) (fun (p : P × P × P) ↦ ∡ p.1 p.2.1 p.2.2) s
hsp : ∀ p ∈ s, ∡ p.1 p.2.1 p.2.2 ≠ 0 ∧ ∡ p.1 p.2.1 p.2.2 ≠ (↑π : Real.Angle)
⊢ (p₁, p₅, p₂) ∈ s
have simp_rw : ∃ (x : Prod.{u_2, u_1} (↥(affineSpan ℝ {p₁, p₂})) V),
  (SameRay ℝ (p₂ -ᵥ p₁) x.2 ∧ x.2 ≠ 0) ∧ (↑x.1 : P) = p₁ ∧ True ∧ x.2 +ᵥ (↑x.1 : P) = p₂
Tactic: simp_rw [s, Set.mem_image, Set.mem_prod, Set.mem_setOf, Set.mem_univ, true_and,
        Prod.ext_iff]
-- 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₂}
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}
hco : IsConnected s
hf : ContinuousOn (Y := Real.Angle) (fun (p : P × P × P) ↦ ∡ p.1 p.2.1 p.2.2) s
hsp : ∀ p ∈ s, ∡ p.1 p.2.1 p.2.2 ≠ 0 ∧ ∡ p.1 p.2.1 p.2.2 ≠ (↑π : Real.Angle)
⊢ ∃ (x : Prod.{u_2, u_1} (↥(affineSpan ℝ {p₁, p₂})) V),
    (SameRay ℝ (p₂ -ᵥ p₁) x.2 ∧ x.2 ≠ 0) ∧ (↑x.1 : P) = p₁ ∧ True ∧ x.2 +ᵥ (↑x.1 : P) = p₂
have refine : (↑(Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) x) p₁ sorry,
            p₂ -ᵥ p₁).1 :
      P) =
    p₁ ∧
  True ∧
    (Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) x) p₁ sorry,
            p₂ -ᵥ p₁).2 +ᵥ
        (↑(Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) x) p₁ sorry,
                p₂ -ᵥ p₁).1 :
          P) =
      p₂
Tactic: refine ⟨⟨⟨p₁, left_mem_affineSpan_pair ℝ _ _⟩, p₂ -ᵥ p₁⟩,
        ⟨SameRay.rfl, vsub_ne_zero.2 hp₁p₂.symm⟩, ?_⟩
-- 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₂}
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}
hco : IsConnected s
hf : ContinuousOn (Y := Real.Angle) (fun (p : P × P × P) ↦ ∡ p.1 p.2.1 p.2.2) s
hsp : ∀ p ∈ s, ∡ 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₂s : (p₁, p₅, p₂) ∈ s
Tactic: have hp₁p₂s : (p₁, p₅, p₂) ∈ s := by
      simp_rw [s, Set.mem_image, Set.mem_prod, Set.mem_setOf, Set.mem_univ, true_and,
        Prod.ext_iff]
      refine ⟨⟨⟨p₁, left_mem_affineSpan_pair ℝ _ _⟩, p₂ -ᵥ p₁⟩,
        ⟨SameRay.rfl, vsub_ne_zero.2 hp₁p₂.symm⟩, ?_⟩
      simp
-- 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₂}
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}
hco : IsConnected s
hf : ContinuousOn (Y := Real.Angle) (fun (p : P × P × P) ↦ ∡ p.1 p.2.1 p.2.2) s
hsp : ∀ p ∈ s, ∡ p.1 p.2.1 p.2.2 ≠ 0 ∧ ∡ p.1 p.2.1 p.2.2 ≠ (↑π : Real.Angle)
hp₁p₂s : (p₁, p₅, p₂) ∈ s
⊢ (p₃, p₅, p₄) ∈ s
have simp_rw : ∃ (x : Prod.{u_2, u_1} (↥(affineSpan ℝ {p₁, p₂})) V),
  (SameRay ℝ (p₂ -ᵥ p₁) x.2 ∧ x.2 ≠ 0) ∧ (↑x.1 : P) = p₃ ∧ True ∧ x.2 +ᵥ (↑x.1 : P) = p₄
Tactic: simp_rw [s, Set.mem_image, Set.mem_prod, Set.mem_setOf, Set.mem_univ, true_and,
        Prod.ext_iff]
-- 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₂}
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}
hco : IsConnected s
hf : ContinuousOn (Y := Real.Angle) (fun (p : P × P × P) ↦ ∡ p.1 p.2.1 p.2.2) s
hsp : ∀ p ∈ s, ∡ p.1 p.2.1 p.2.2 ≠ 0 ∧ ∡ p.1 p.2.1 p.2.2 ≠ (↑π : Real.Angle)
hp₁p₂s : (p₁, p₅, p₂) ∈ s
⊢ ∃ (x : Prod.{u_2, u_1} (↥(affineSpan ℝ {p₁, p₂})) V),
    (SameRay ℝ (p₂ -ᵥ p₁) x.2 ∧ x.2 ≠ 0) ∧ (↑x.1 : P) = p₃ ∧ True ∧ x.2 +ᵥ (↑x.1 : P) = p₄
have refine : (↑(Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) x) p₃ sorry,
            p₄ -ᵥ p₃).1 :
      P) =
    p₃ ∧
  True ∧
    (Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) x) p₃ sorry,
            p₄ -ᵥ p₃).2 +ᵥ
        (↑(Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) x) p₃ sorry,
                p₄ -ᵥ p₃).1 :
          P) =
      p₄
Tactic: refine ⟨⟨⟨p₃, hc.mem_affineSpan_of_mem_of_ne (Set.mem_insert _ _)
        (Set.mem_insert_of_mem _ (Set.mem_insert _ _))
        (Set.mem_insert_of_mem _ (Set.mem_insert_of_mem _ (Set.mem_insert _ _))) hp₁p₂⟩, p₄ -ᵥ p₃⟩,
        ⟨hr, vsub_ne_zero.2 hp₃p₄.symm⟩, ?_⟩
-- 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₂}
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}
hco : IsConnected s
hf : ContinuousOn (Y := Real.Angle) (fun (p : P × P × P) ↦ ∡ p.1 p.2.1 p.2.2) s
hsp : ∀ p ∈ s, ∡ p.1 p.2.1 p.2.2 ≠ 0 ∧ ∡ p.1 p.2.1 p.2.2 ≠ (↑π : Real.Angle)
hp₁p₂s : (p₁, p₅, p₂) ∈ s
⊢ (∡ p₁ p₅ p₂).sign = (∡ p₃ p₅ p₄).sign
have hp₃p₄s : (p₃, p₅, p₄) ∈ s
Tactic: have hp₃p₄s : (p₃, p₅, p₄) ∈ s := by
      simp_rw [s, Set.mem_image, Set.mem_prod, Set.mem_setOf, Set.mem_univ, true_and,
        Prod.ext_iff]
      refine ⟨⟨⟨p₃, hc.mem_affineSpan_of_mem_of_ne (Set.mem_insert _ _)
        (Set.mem_insert_of_mem _ (Set.mem_insert _ _))
        (Set.mem_insert_of_mem _ (Set.mem_insert_of_mem _ (Set.mem_insert _ _))) hp₁p₂⟩, p₄ -ᵥ p₃⟩,
        ⟨hr, vsub_ne_zero.2 hp₃p₄.symm⟩, ?_⟩
      simp
-- 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 : Wbtw ℝ p₁ p₂ p₃
hne : p₂ ≠ p₃
⊢ (∡ p₂ p₄ p₃).sign = (∡ p₁ p₄ p₃).sign
have simp_rw : (-∡ p₃ p₄ p₂).sign = (-∡ p₃ p₄ p₁).sign
Tactic: simp_rw [oangle_rev p₃, Real.Angle.sign_neg, h.symm.oangle_sign_eq_of_ne_left _ hne.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 : Wbtw ℝ p₁ p₂ p₃
hne : p₂ ≠ p₃
simp_rw : (-∡ p₃ p₄ p₂).sign = (-∡ p₃ p₄ p₁).sign
⊢ (∡ p₂ p₄ p₃).sign = (∡ p₁ p₄ p₃).sign
have simp_rw₁ : -(∡ p₃ p₄ p₂).sign = -(∡ p₃ p₄ p₁).sign
Tactic: simp_rw [oangle_rev p₃, Real.Angle.sign_neg, h.symm.oangle_sign_eq_of_ne_left _ hne.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₄ : P
hp₁₃ : Sbtw ℝ p₁ p p₃
hp₂₄ : Sbtw ℝ p₂ p p₄
⊢ (∡ p₁ p₄ p₂).sign = (∡ p₁ p₃ p₂).sign
have rw : (∡ p₁ p₄ p).sign = (∡ p₁ p₃ p₂).sign
Tactic: rw [← Sbtw.oangle_eq_right hp₂₄.symm, Sbtw.oangle_sign_eq _ hp₁₃, ← oangle_rotate_sign,
    Sbtw.oangle_sign_eq _ hp₂₄.symm, Sbtw.oangle_eq_left hp₁₃.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₄ : P
hp₁₃ : Sbtw ℝ p₁ p p₃
hp₂₄ : Sbtw ℝ p₂ p p₄
rw : (∡ 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 [← Sbtw.oangle_eq_right hp₂₄.symm, Sbtw.oangle_sign_eq _ hp₁₃, ← oangle_rotate_sign,
    Sbtw.oangle_sign_eq _ hp₂₄.symm, Sbtw.oangle_eq_left hp₁₃.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₄ : P
hp₁₃ : Sbtw ℝ p₁ p p₃
hp₂₄ : Sbtw ℝ p₂ p p₄
rw : (∡ p₁ p₄ p).sign = (∡ p₁ p₃ p₂).sign
rw₁ : (∡ 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 [← Sbtw.oangle_eq_right hp₂₄.symm, Sbtw.oangle_sign_eq _ hp₁₃, ← oangle_rotate_sign,
    Sbtw.oangle_sign_eq _ hp₂₄.symm, Sbtw.oangle_eq_left hp₁₃.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₄ : P
hp₁₃ : Sbtw ℝ p₁ p p₃
hp₂₄ : Sbtw ℝ p₂ p p₄
rw : (∡ p₁ p₄ p).sign = (∡ p₁ p₃ p₂).sign
rw₁ : (∡ p p₄ p₃).sign = (∡ p₁ p₃ p₂).sign
rw₂ : (∡ 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 [← Sbtw.oangle_eq_right hp₂₄.symm, Sbtw.oangle_sign_eq _ hp₁₃, ← oangle_rotate_sign,
    Sbtw.oangle_sign_eq _ hp₂₄.symm, Sbtw.oangle_eq_left hp₁₃.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₄ : P
hp₁₃ : Sbtw ℝ p₁ p p₃
hp₂₄ : Sbtw ℝ p₂ p p₄
rw : (∡ p₁ p₄ p).sign = (∡ p₁ p₃ p₂).sign
rw₁ : (∡ p p₄ p₃).sign = (∡ p₁ p₃ p₂).sign
rw₂ : (∡ p₄ p₃ p).sign = (∡ p₁ p₃ p₂).sign
rw₃ : (∡ 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 [← Sbtw.oangle_eq_right hp₂₄.symm, Sbtw.oangle_sign_eq _ hp₁₃, ← oangle_rotate_sign,
    Sbtw.oangle_sign_eq _ hp₂₄.symm, Sbtw.oangle_eq_left hp₁₃.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₄ : P
hp₁₃ : Sbtw ℝ p p₁ p₃
hp₂₄ : Sbtw ℝ p p₂ p₄
⊢ (∡ p₁ p₄ p₂).sign = (∡ p₁ p₃ p₂).sign
have rw : (∡ p₁ p₄ p).sign = (∡ p₁ p₃ p₂).sign
Tactic: rw [Sbtw.oangle_eq_right hp₂₄.symm, Sbtw.oangle_sign_eq_right _ hp₁₃.symm, oangle_rotate_sign,
    ← Sbtw.oangle_sign_eq_left p₃ hp₂₄, Sbtw.oangle_eq_left hp₁₃.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₄ : P
hp₁₃ : Sbtw ℝ p p₁ p₃
hp₂₄ : Sbtw ℝ p p₂ p₄
rw : (∡ 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 [Sbtw.oangle_eq_right hp₂₄.symm, Sbtw.oangle_sign_eq_right _ hp₁₃.symm, oangle_rotate_sign,
    ← Sbtw.oangle_sign_eq_left p₃ hp₂₄, Sbtw.oangle_eq_left hp₁₃.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₄ : P
hp₁₃ : Sbtw ℝ p p₁ p₃
hp₂₄ : Sbtw ℝ p p₂ p₄
rw : (∡ p₁ p₄ p).sign = (∡ p₁ p₃ p₂).sign
rw₁ : (∡ 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 [Sbtw.oangle_eq_right hp₂₄.symm, Sbtw.oangle_sign_eq_right _ hp₁₃.symm, oangle_rotate_sign,
    ← Sbtw.oangle_sign_eq_left p₃ hp₂₄, Sbtw.oangle_eq_left hp₁₃.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₄ : P
hp₁₃ : Sbtw ℝ p p₁ p₃
hp₂₄ : Sbtw ℝ p p₂ p₄
rw : (∡ p₁ p₄ p).sign = (∡ p₁ p₃ p₂).sign
rw₁ : (∡ p₃ p₄ p).sign = (∡ p₁ p₃ p₂).sign
rw₂ : (∡ 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 [Sbtw.oangle_eq_right hp₂₄.symm, Sbtw.oangle_sign_eq_right _ hp₁₃.symm, oangle_rotate_sign,
    ← Sbtw.oangle_sign_eq_left p₃ hp₂₄, Sbtw.oangle_eq_left hp₁₃.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₄ : P
hp₁₃ : Sbtw ℝ p p₁ p₃
hp₂₄ : Sbtw ℝ p p₂ p₄
rw : (∡ p₁ p₄ p).sign = (∡ p₁ p₃ p₂).sign
rw₁ : (∡ p₃ p₄ p).sign = (∡ p₁ p₃ p₂).sign
rw₂ : (∡ p p₃ p₄).sign = (∡ p₁ p₃ p₂).sign
rw₃ : (∡ 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 [Sbtw.oangle_eq_right hp₂₄.symm, Sbtw.oangle_sign_eq_right _ hp₁₃.symm, oangle_rotate_sign,
    ← Sbtw.oangle_sign_eq_left p₃ hp₂₄, Sbtw.oangle_eq_left hp₁₃.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)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SSameSide p₃ p₄
⊢ (∡ p₁ p₄ p₂).sign = (∡ p₁ p₃ p₂).sign
have pos : ∀ (h : p₁ = p₂), (∡ p₁ p₄ p₂).sign = (∡ p₁ p₃ p₂).sign
Tactic: by_cases h : 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)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SSameSide p₃ p₄
pos : ∀ (h : p₁ = p₂), (∡ p₁ p₄ p₂).sign = (∡ p₁ p₃ p₂).sign
⊢ (∡ p₁ p₄ p₂).sign = (∡ p₁ p₃ p₂).sign
have neg : ∀ (h : ¬p₁ = p₂), (∡ p₁ p₄ p₂).sign = (∡ p₁ p₃ p₂).sign
Tactic: by_cases h : 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)
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}
⊢ (∡ p₁ p₄ p₂).sign = (∡ p₁ p₃ p₂).sign
have hc : IsConnected sp
Tactic: have hc : IsConnected sp :=
    (isConnected_setOf_sSameSide hp₃p₄.2.1 hp₃p₄.nonempty).image _ (by fun_prop)
-- 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
⊢ ContinuousOn (Y := Real.Angle) (fun (p : P × P × P) ↦ ∡ p.1 p.2.1 p.2.2) sp
have refine_1 : ∀ (p : P × P × P) (hp : p ∈ sp), p.1 ≠ p.2.1
Tactic: refine continuousOn_of_forall_continuousAt fun p hp => continuousAt_oangle ?_ ?_
-- 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
refine_1 : ∀ (p : P × P × P) (hp : p ∈ sp), p.1 ≠ p.2.1
⊢ ContinuousOn (Y := Real.Angle) (fun (p : P × P × P) ↦ ∡ p.1 p.2.1 p.2.2) sp
have refine_2 : ∀ (p : P × P × P) (hp : p ∈ sp), p.2.2 ≠ p.2.1
Tactic: refine continuousOn_of_forall_continuousAt fun p hp => continuousAt_oangle ?_ ?_
-- 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.1 ≠ 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.1 ≠ p.2.1
have refine_1 : ∀ (p' : P) (hp' : s.SSameSide p₃ p'), (p₁, p', p₂).1 ≠ (p₁, p', p₂).2.1
Tactic: obtain ⟨p', hp', rfl⟩ := hp
Cleared hypotheses: p, hp