awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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}
⊢ (∡ p₁ p₅ p₂).sign = (∡ p₃ p₅ p₄).sign
have hco : 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)
-- 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
⊢ ContinuousOn (Y := Real.Angle) (fun (p : P × P × P) ↦ ∡ p.1 p.2.1 p.2.2) s
have refine_1 : ∀ (p : P × P × P) (hp : p ∈ s), 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)
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
⊢ ContinuousOn (Y := Real.Angle) (fun (p : P × P × P) ↦ ∡ p.1 p.2.1 p.2.2) s
have refine_2 : ∀ (p : P × P × P) (hp : p ∈ s), 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)
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
⊢ p.1 ≠ p.2.1
have 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
Tactic: simp_rw [s, Set.mem_image, Set.mem_prod, Set.mem_univ, true_and, Prod.ext_iff] 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)
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
⊢ p.1 ≠ p.2.1
have 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
Tactic: obtain ⟨q₁, q₅, q₂⟩ := p
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)
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
⊢ (q₁, q₅, q₂).1 ≠ (q₁, q₅, q₂).2.1
have refine_1 : q₁ ≠ q₅
Tactic: dsimp only at 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₅ : 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₂
⊢ q₁ ≠ q₅
have 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₅
Tactic: obtain ⟨⟨⟨q, hq⟩, v⟩, hv, rfl, rfl, rfl⟩ := hp
Cleared hypotheses: q₁, q₅, q₂, 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₅ : 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
⊢ (↑(Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) x) q hq, v).1 :
      P) ≠
    p₅
have refine_1 : q ≠ p₅
Tactic: dsimp only [Subtype.coe_mk, Set.mem_setOf] at hv ⊢
-- 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
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
⊢ q ≠ p₅
have hvr : SameRay ℝ (p₂ -ᵥ p₁) v
Tactic: obtain ⟨hvr, -⟩ := hv
Cleared hypotheses: hv
-- 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
p : P × P × P
hp : p ∈ s
⊢ p.2.2 ≠ p.2.1
have 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
Tactic: simp_rw [s, Set.mem_image, Set.mem_prod, Set.mem_univ, true_and, Prod.ext_iff] 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)
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
⊢ p.2.2 ≠ p.2.1
have 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
Tactic: obtain ⟨q₁, q₅, q₂⟩ := p
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)
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
⊢ (q₁, q₅, q₂).2.2 ≠ (q₁, q₅, q₂).2.1
have refine_2 : q₂ ≠ q₅
Tactic: dsimp only at 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₅ : 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₂
⊢ q₂ ≠ q₅
have 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₅
Tactic: obtain ⟨⟨⟨q, hq⟩, v⟩, hv, rfl, rfl, rfl⟩ := hp
Cleared hypotheses: q₁, q₅, q₂, 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₅ : 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
⊢ (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₅
have refine_2 : v +ᵥ q ≠ p₅
Tactic: dsimp only [Subtype.coe_mk, Set.mem_setOf] at hv ⊢
-- 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
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
⊢ v +ᵥ q ≠ p₅
have hvr : SameRay ℝ (p₂ -ᵥ p₁) v
Tactic: obtain ⟨hvr, -⟩ := hv
Cleared hypotheses: hv
-- 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₁ ≠ 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
have refine_2 : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) (v +ᵥ q)
Tactic: refine hc₅₁₂ ((collinear_insert_iff_of_mem_affineSpan ?_).2 (collinear_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
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)
have refine_2 : Membership.mem (γ := Submodule ℝ V) (direction (P := P) (affineSpan ℝ {p₁, p₂})) v
Tactic: refine vadd_mem_of_mem_direction ?_ hq
-- 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
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 (γ := Submodule ℝ V) (direction (P := P) (affineSpan ℝ {p₁, p₂})) v
have hvr₁ : ∃ (r : ℝ), 0 ≤ r ∧ r • (p₂ -ᵥ p₁) = v
Tactic: rw [← exists_nonneg_left_iff_sameRay (vsub_ne_zero.2 hp₁p₂.symm)] at hvr
Cleared hypotheses: hvr, hc₅₁₂, s, hco
-- 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₁ ≠ 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 : ∃ (r : ℝ), 0 ≤ r ∧ r • (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 (γ := Submodule ℝ V) (direction (P := P) (affineSpan ℝ {p₁, p₂})) v
have refine_2 : ∀ (r : ℝ) (hc₅₁₂ : ¬Collinear ℝ (P := P) {r • (p₂ -ᵥ p₁) +ᵥ q, p₁, p₂}),
  let s : Set (P × P × P) :=
    (fun (x : Prod.{u_2, u_1} (↥(affineSpan ℝ {p₁, p₂})) V) ↦ ((↑x.1 : P), r • (p₂ -ᵥ 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 (γ := Submodule ℝ V) (direction (P := P) (affineSpan ℝ {p₁, p₂})) (r • (p₂ -ᵥ p₁))
Tactic: obtain ⟨r, -, rfl⟩ := hvr
Cleared hypotheses: v, hvr, hc₅₁₂, s, hco
-- 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₁ ≠ p₂
hp₃p₄ : p₃ ≠ p₄
hc : Collinear ℝ (P := P) {p₁, p₂, p₃, p₄}
hr : SameRay ℝ (p₂ -ᵥ p₁) (p₄ -ᵥ p₃)
q : P
hq : Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) q
r : ℝ
hc₅₁₂ : ¬Collinear ℝ (P := P) {r • (p₂ -ᵥ p₁) +ᵥ q, p₁, p₂}
s : Set (P × P × P) :=
  (fun (x : Prod.{u_2, u_1} (↥(affineSpan ℝ {p₁, p₂})) V) ↦ ((↑x.1 : P), r • (p₂ -ᵥ 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 (γ := 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]