awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : 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}
⊢ IsConnected s

Tactic:
have hco : IsConnected s :=
      haveI : ConnectedSpace line[ℝ, p₁, p₂] := AddTorsor.connectedSpace _ _
      (isConnected_univ.prod (isConnected_setOf_sameRay_and_ne_zero
        (vsub_ne_zero.2 hp₁p₂.symm))).image _ (by fun_prop)
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ (P := P) {p₅, p₁, p₂}
s : Set (P × P × P) :=
  (fun (x : Prod.{u_2, u_1} (↥(affineSpan ℝ {p₁, p₂})) V) ↦ ((↑x.1 : P), p₅, x.2 +ᵥ (↑x.1 : P))) ''
    SProd.sprod (α := Set ↥(affineSpan ℝ {p₁, p₂})) (β := Set V) Set.univ {v : V | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
⊢ ContinuousOn (Y := Real.Angle) (fun (p : P × P × P) ↦ ∡ p.1 p.2.1 p.2.2) s

Tactic:
continuousOn_of_forall_continuousAt fun p hp => continuousAt_oangle ?_ ?_

Premises used: continuousOn_of_forall_continuousAt, EuclideanGeometry.continuousAt_oangle
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ (P := P) {p₅, p₁, p₂}
s : Set (P × P × P) :=
  (fun (x : Prod.{u_2, u_1} (↥(affineSpan ℝ {p₁, p₂})) V) ↦ ((↑x.1 : P), p₅, x.2 +ᵥ (↑x.1 : P))) ''
    SProd.sprod (α := Set ↥(affineSpan ℝ {p₁, p₂})) (β := Set V) Set.univ {v : V | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
refine_1 : ∀ (p : P × P × P) (hp : p ∈ s), p.1 ≠ p.2.1
refine_2 : ∀ (p : P × P × P) (hp : p ∈ s), p.2.2 ≠ p.2.1
⊢ ContinuousOn (Y := Real.Angle) (fun (p : P × P × P) ↦ ∡ p.1 p.2.1 p.2.2) s

Tactic:
refine continuousOn_of_forall_continuousAt fun p hp => continuousAt_oangle ?_ ?_

Premises used: continuousOn_of_forall_continuousAt, EuclideanGeometry.continuousAt_oangle
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ (P := P) {p₅, p₁, p₂}
s : Set (P × P × P) :=
  (fun (x : Prod.{u_2, u_1} (↥(affineSpan ℝ {p₁, p₂})) V) ↦ ((↑x.1 : P), p₅, x.2 +ᵥ (↑x.1 : P))) ''
    SProd.sprod (α := Set ↥(affineSpan ℝ {p₁, p₂})) (β := Set V) Set.univ {v : V | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
p : P × P × P
hp : p ∈ s
⊢ ∃ (x : Prod.{u_2, u_1} (↥(affineSpan ℝ {p₁, p₂})) V),
    Membership.mem (γ := Set V) {v : V | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0} x.2 ∧
      (↑x.1 : P) = p.1 ∧ p₅ = p.2.1 ∧ x.2 +ᵥ (↑x.1 : P) = p.2.2

Tactic:
simp_rw [s, Set.mem_image, Set.mem_prod, Set.mem_univ, true_and, Prod.ext_iff] at hp

Premises used: Set.mem_image, Prod.ext_iff, Set.mem_prod, Set.mem_univ, true_and
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ (P := P) {p₅, p₁, p₂}
s : Set (P × P × P) :=
  (fun (x : Prod.{u_2, u_1} (↥(affineSpan ℝ {p₁, p₂})) V) ↦ ((↑x.1 : P), p₅, x.2 +ᵥ (↑x.1 : P))) ''
    SProd.sprod (α := Set ↥(affineSpan ℝ {p₁, p₂})) (β := Set V) Set.univ {v : V | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
p : P × P × P
hp :
  ∃ (x : Prod.{u_2, u_1} (↥(affineSpan ℝ {p₁, p₂})) V),
    Membership.mem (γ := Set V) {v : V | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0} x.2 ∧
      (↑x.1 : P) = p.1 ∧ p₅ = p.2.1 ∧ x.2 +ᵥ (↑x.1 : P) = p.2.2
refine_1 :
  ∀ (q₁ q₅ q₂ : P)
    (hp :
      ∃ (x : Prod.{u_2, u_1} (↥(affineSpan ℝ {p₁, p₂})) V),
        Membership.mem (γ := Set V) {v : V | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0} x.2 ∧
          (↑x.1 : P) = (q₁, q₅, q₂).1 ∧ p₅ = (q₁, q₅, q₂).2.1 ∧ x.2 +ᵥ (↑x.1 : P) = (q₁, q₅, q₂).2.2),
    (q₁, q₅, q₂).1 ≠ (q₁, q₅, q₂).2.1
⊢ p.1 ≠ p.2.1

Tactic:
obtain ⟨q₁, q₅, q₂⟩ := p
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ (P := P) {p₅, p₁, p₂}
s : Set (P × P × P) :=
  (fun (x : Prod.{u_2, u_1} (↥(affineSpan ℝ {p₁, p₂})) V) ↦ ((↑x.1 : P), p₅, x.2 +ᵥ (↑x.1 : P))) ''
    SProd.sprod (α := Set ↥(affineSpan ℝ {p₁, p₂})) (β := Set V) Set.univ {v : V | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
q₁ q₅ q₂ : P
hp :
  ∃ (x : Prod.{u_2, u_1} (↥(affineSpan ℝ {p₁, p₂})) V),
    Membership.mem (γ := Set V) {v : V | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0} x.2 ∧
      (↑x.1 : P) = (q₁, q₅, q₂).1 ∧ p₅ = (q₁, q₅, q₂).2.1 ∧ x.2 +ᵥ (↑x.1 : P) = (q₁, q₅, q₂).2.2
refine_1 : q₁ ≠ q₅
⊢ (q₁, q₅, q₂).1 ≠ (q₁, q₅, q₂).2.1

Tactic:
dsimp only at hp ⊢
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ (P := P) {p₅, p₁, p₂}
s : Set (P × P × P) :=
  (fun (x : Prod.{u_2, u_1} (↥(affineSpan ℝ {p₁, p₂})) V) ↦ ((↑x.1 : P), p₅, x.2 +ᵥ (↑x.1 : P))) ''
    SProd.sprod (α := Set ↥(affineSpan ℝ {p₁, p₂})) (β := Set V) Set.univ {v : V | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
q₁ q₅ q₂ : P
hp :
  ∃ (x : Prod.{u_2, u_1} (↥(affineSpan ℝ {p₁, p₂})) V),
    Membership.mem (γ := Set V) {v : V | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0} x.2 ∧
      (↑x.1 : P) = q₁ ∧ p₅ = q₅ ∧ x.2 +ᵥ (↑x.1 : P) = q₂
refine_1 :
  ∀ (v : V) (q : P) (hq : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) q)
    (hv :
      Membership.mem (γ := Set V) {v : V | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
        (Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) x) q hq, v).2),
    (↑(Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) x) q hq, v).1 :
        P) ≠
      p₅
⊢ q₁ ≠ q₅

Tactic:
obtain ⟨⟨⟨q, hq⟩, v⟩, hv, rfl, rfl, rfl⟩ := hp

Premises used: rfl
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ 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
v : V
q : P
hq : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) q
hv :
  Membership.mem (γ := Set V) {v : V | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
    (Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) x) q hq, v).2
refine_1 : q ≠ p₅
⊢ (↑(Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) x) q hq, v).1 :
      P) ≠
    p₅

Tactic:
dsimp only [Subtype.coe_mk, Set.mem_setOf] at hv ⊢

Premises used: Subtype.coe_mk, Set.mem_setOf
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ (P := P) {p₅, p₁, p₂}
s : Set (P × P × P) :=
  (fun (x : Prod.{u_2, u_1} (↥(affineSpan ℝ {p₁, p₂})) V) ↦ ((↑x.1 : P), p₅, x.2 +ᵥ (↑x.1 : P))) ''
    SProd.sprod (α := Set ↥(affineSpan ℝ {p₁, p₂})) (β := Set V) Set.univ {v : V | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
v : V
q : P
hq : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) q
hv : Membership.mem (γ := Set V) {v : V | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0} v
⊢ SameRay ℝ (p₂ -ᵥ p₁) v

Tactic:
obtain ⟨hvr, -⟩ := hv
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
v : V
q : P
hq : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) q
hvr : SameRay ℝ (p₂ -ᵥ p₁) v
hc₅₁₂ : ¬Collinear ℝ (P := P) {q, p₁, p₂}
s : Set (P × P × P) :=
  (fun (x : Prod.{u_2, u_1} (↥(affineSpan ℝ {p₁, p₂})) V) ↦ ((↑x.1 : P), q, 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
⊢ False

Tactic:
hc₅₁₂ ((collinear_insert_iff_of_mem_affineSpan ?_).2 (collinear_pair _ _ _))

Premises used: Iff.mpr, collinear_pair, collinear_insert_iff_of_mem_affineSpan
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
v : V
q : P
hq : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) q
hvr : SameRay ℝ (p₂ -ᵥ p₁) v
hc₅₁₂ : ¬Collinear ℝ (P := P) {q, p₁, p₂}
s : Set (P × P × P) :=
  (fun (x : Prod.{u_2, u_1} (↥(affineSpan ℝ {p₁, p₂})) V) ↦ ((↑x.1 : P), q, 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
refine_1 : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) q
⊢ False

Tactic:
refine hc₅₁₂ ((collinear_insert_iff_of_mem_affineSpan ?_).2 (collinear_pair _ _ _))

Premises used: Iff.mpr, collinear_pair, collinear_insert_iff_of_mem_affineSpan
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ (P := P) {p₅, p₁, p₂}
s : Set (P × P × P) :=
  (fun (x : Prod.{u_2, u_1} (↥(affineSpan ℝ {p₁, p₂})) V) ↦ ((↑x.1 : P), p₅, x.2 +ᵥ (↑x.1 : P))) ''
    SProd.sprod (α := Set ↥(affineSpan ℝ {p₁, p₂})) (β := Set V) Set.univ {v : V | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
p : P × P × P
hp :
  ∃ (x : Prod.{u_2, u_1} (↥(affineSpan ℝ {p₁, p₂})) V),
    Membership.mem (γ := Set V) {v : V | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0} x.2 ∧
      (↑x.1 : P) = p.1 ∧ p₅ = p.2.1 ∧ x.2 +ᵥ (↑x.1 : P) = p.2.2
refine_2 :
  ∀ (q₁ q₅ q₂ : P)
    (hp :
      ∃ (x : Prod.{u_2, u_1} (↥(affineSpan ℝ {p₁, p₂})) V),
        Membership.mem (γ := Set V) {v : V | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0} x.2 ∧
          (↑x.1 : P) = (q₁, q₅, q₂).1 ∧ p₅ = (q₁, q₅, q₂).2.1 ∧ x.2 +ᵥ (↑x.1 : P) = (q₁, q₅, q₂).2.2),
    (q₁, q₅, q₂).2.2 ≠ (q₁, q₅, q₂).2.1
⊢ p.2.2 ≠ p.2.1

Tactic:
obtain ⟨q₁, q₅, q₂⟩ := p
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ (P := P) {p₅, p₁, p₂}
s : Set (P × P × P) :=
  (fun (x : Prod.{u_2, u_1} (↥(affineSpan ℝ {p₁, p₂})) V) ↦ ((↑x.1 : P), p₅, x.2 +ᵥ (↑x.1 : P))) ''
    SProd.sprod (α := Set ↥(affineSpan ℝ {p₁, p₂})) (β := Set V) Set.univ {v : V | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
q₁ q₅ q₂ : P
hp :
  ∃ (x : Prod.{u_2, u_1} (↥(affineSpan ℝ {p₁, p₂})) V),
    Membership.mem (γ := Set V) {v : V | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0} x.2 ∧
      (↑x.1 : P) = (q₁, q₅, q₂).1 ∧ p₅ = (q₁, q₅, q₂).2.1 ∧ x.2 +ᵥ (↑x.1 : P) = (q₁, q₅, q₂).2.2
refine_2 : q₂ ≠ q₅
⊢ (q₁, q₅, q₂).2.2 ≠ (q₁, q₅, q₂).2.1

Tactic:
dsimp only at hp ⊢
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ p₅ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
hc₅₁₂ : ¬Collinear ℝ (P := P) {p₅, p₁, p₂}
s : Set (P × P × P) :=
  (fun (x : Prod.{u_2, u_1} (↥(affineSpan ℝ {p₁, p₂})) V) ↦ ((↑x.1 : P), p₅, x.2 +ᵥ (↑x.1 : P))) ''
    SProd.sprod (α := Set ↥(affineSpan ℝ {p₁, p₂})) (β := Set V) Set.univ {v : V | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
hco : IsConnected s
q₁ q₅ q₂ : P
hp :
  ∃ (x : Prod.{u_2, u_1} (↥(affineSpan ℝ {p₁, p₂})) V),
    Membership.mem (γ := Set V) {v : V | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0} x.2 ∧
      (↑x.1 : P) = q₁ ∧ p₅ = q₅ ∧ x.2 +ᵥ (↑x.1 : P) = q₂
refine_2 :
  ∀ (v : V) (q : P) (hq : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) q)
    (hv :
      Membership.mem (γ := Set V) {v : V | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
        (Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) x) q hq, v).2),
    (Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) x) q hq, v).2 +ᵥ
        (↑(Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) x) q hq,
                v).1 :
          P) ≠
      p₅
⊢ q₂ ≠ q₅

Tactic:
obtain ⟨⟨⟨q, hq⟩, v⟩, hv, rfl, rfl, rfl⟩ := hp

Premises used: rfl
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ 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
v : V
q : P
hq : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) q
hv :
  Membership.mem (γ := Set V) {v : V | SameRay ℝ (p₂ -ᵥ p₁) v ∧ v ≠ 0}
    (Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) x) q hq, v).2
refine_2 : v +ᵥ q ≠ p₅
⊢ (Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) x) q hq, v).2 +ᵥ
      (↑(Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) x) q hq, v).1 :
        P) ≠
    p₅

Tactic:
dsimp only [Subtype.coe_mk, Set.mem_setOf] at hv ⊢

Premises used: Subtype.coe_mk, Set.mem_setOf
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
v : V
q : P
hq : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) q
hvr : SameRay ℝ (p₂ -ᵥ p₁) v
hc₅₁₂ : ¬Collinear ℝ (P := P) {v +ᵥ q, p₁, p₂}
s : Set (P × P × P) :=
  (fun (x : Prod.{u_2, u_1} (↥(affineSpan ℝ {p₁, p₂})) V) ↦ ((↑x.1 : P), v +ᵥ q, 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
⊢ False

Tactic:
hc₅₁₂ ((collinear_insert_iff_of_mem_affineSpan ?_).2 (collinear_pair _ _ _))

Premises used: Iff.mpr, collinear_pair, collinear_insert_iff_of_mem_affineSpan
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
v : V
q : P
hq : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) q
hvr : SameRay ℝ (p₂ -ᵥ p₁) v
hc₅₁₂ : ¬Collinear ℝ (P := P) {v +ᵥ q, p₁, p₂}
s : Set (P × P × P) :=
  (fun (x : Prod.{u_2, u_1} (↥(affineSpan ℝ {p₁, p₂})) V) ↦ ((↑x.1 : P), v +ᵥ q, 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
refine_2 : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) (v +ᵥ q)
⊢ False

Tactic:
refine hc₅₁₂ ((collinear_insert_iff_of_mem_affineSpan ?_).2 (collinear_pair _ _ _))

Premises used: Iff.mpr, collinear_pair, collinear_insert_iff_of_mem_affineSpan
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
v : V
q : P
hq : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) q
hvr : SameRay ℝ (p₂ -ᵥ p₁) v
hc₅₁₂ : ¬Collinear ℝ (P := P) {q, p₁, p₂}
s : Set (P × P × P) :=
  (fun (x : Prod.{u_2, u_1} (↥(affineSpan ℝ {p₁, p₂})) V) ↦ ((↑x.1 : P), q, 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
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) q

Tactic:
hq

Premises used: Set.Mem
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
v : V
q : P
hq : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) q
hvr : SameRay ℝ (p₂ -ᵥ p₁) v
hc₅₁₂ : ¬Collinear ℝ (P := P) {q, p₁, p₂}
s : Set (P × P × P) :=
  (fun (x : Prod.{u_2, u_1} (↥(affineSpan ℝ {p₁, p₂})) V) ↦ ((↑x.1 : P), q, 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
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) q

Tactic:
exact hq
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
v : V
q : P
hq : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) q
hvr : SameRay ℝ (p₂ -ᵥ p₁) v
hc₅₁₂ : ¬Collinear ℝ (P := P) {v +ᵥ q, p₁, p₂}
s : Set (P × P × P) :=
  (fun (x : Prod.{u_2, u_1} (↥(affineSpan ℝ {p₁, p₂})) V) ↦ ((↑x.1 : P), v +ᵥ q, 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
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) (v +ᵥ q)

Tactic:
vadd_mem_of_mem_direction ?_ hq

Premises used: AffineSubspace.vadd_mem_of_mem_direction
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
v : V
q : P
hq : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) q
hvr : SameRay ℝ (p₂ -ᵥ p₁) v
hc₅₁₂ : ¬Collinear ℝ (P := P) {v +ᵥ q, p₁, p₂}
s : Set (P × P × P) :=
  (fun (x : Prod.{u_2, u_1} (↥(affineSpan ℝ {p₁, p₂})) V) ↦ ((↑x.1 : P), v +ᵥ q, 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
refine_2 : Membership.mem (γ := Submodule ℝ V) (direction (P := P) (affineSpan ℝ {p₁, p₂})) v
⊢ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) (v +ᵥ q)

Tactic:
refine vadd_mem_of_mem_direction ?_ hq

Premises used: AffineSubspace.vadd_mem_of_mem_direction
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
Goal:
V : Type u_1
P : Type u_2
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : MetricSpace P
inst_3 : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst_4 : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ p₄ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
v : V
q : P
hq : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) q
hvr : SameRay ℝ (p₂ -ᵥ p₁) v
hc₅₁₂ : ¬Collinear ℝ (P := P) {v +ᵥ q, p₁, p₂}
s : Set (P × P × P) :=
  (fun (x : Prod.{u_2, u_1} (↥(affineSpan ℝ {p₁, p₂})) V) ↦ ((↑x.1 : P), v +ᵥ q, 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
⊢ ∃ (r : ℝ), 0 ≤ r ∧ r • (p₂ -ᵥ p₁) = v

Tactic:
rw [← exists_nonneg_left_iff_sameRay (vsub_ne_zero.2 hp₁p₂.symm)] at hvr

Premises used: Iff.mpr, exists_nonneg_left_iff_sameRay, vsub_ne_zero, Ne.symm