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}
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
⊢ (↑(Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) x) p₃ ⋯,
              p₄ -ᵥ p₃).1 :
        P) =
      p₃ ∧
    True ∧
      (Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) x) p₃ ⋯,
              p₄ -ᵥ p₃).2 +ᵥ
          (↑(Subtype.mk (p := fun (x : P) ↦ Membership.mem (γ := AffineSubspace ℝ P) (affineSpan ℝ {p₁, p₂}) x) p₃ ⋯,
                  p₄ -ᵥ p₃).1 :
            P) =
        p₄

Tactic:
simp
-- 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
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

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
-- 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
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
hp₃p₄s : (p₃, p₅, p₄) ∈ s
⊢ (∡ (p₁, p₅, p₂).1 (p₁, p₅, p₂).2.1 (p₁, p₅, p₂).2.2).sign = (∡ (p₃, p₅, p₄).1 (p₃, p₅, p₄).2.1 (p₃, p₅, p₄).2.2).sign

Tactic:
Real.Angle.sign_eq_of_continuousOn hco hf hsp hp₃p₄s hp₁p₂s

Premises used: Real.Angle.sign_eq_of_continuousOn
-- 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
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
hp₃p₄s : (p₃, p₅, p₄) ∈ s
⊢ (∡ p₁ p₅ p₂).sign = (∡ p₃ p₅ p₄).sign

Tactic:
convert! Real.Angle.sign_eq_of_continuousOn hco hf hsp hp₃p₄s hp₁p₂s

Premises used: Real.Angle.sign_eq_of_continuousOn
-- 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
h : Sbtw ℝ p₁ p₂ p₃
⊢ Collinear ℝ (P := P) {p₁, p₂, p₂, p₃}

Tactic:
simpa using h.wbtw.collinear

Premises used: Wbtw.collinear, Sbtw.wbtw
-- 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
h : Wbtw ℝ p₁ p₂ p₃
hne : p₁ ≠ p₂
⊢ Collinear ℝ (P := P) {p₁, p₂, p₁, p₃}

Tactic:
simpa [Set.insert_comm p₂] using h.collinear

Premises used: Wbtw.collinear, Set.insert_comm
-- 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
h : Sbtw ℝ p₁ p₂ p₃
⊢ (∡ p₁ p₄ p₂).sign = (∡ p₁ p₄ p₃).sign

Tactic:
h.wbtw.oangle_sign_eq_of_ne_left _ h.left_ne

Premises used: Wbtw.oangle_sign_eq_of_ne_left, Sbtw.wbtw, Sbtw.left_ne
-- 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
h : Wbtw ℝ p₁ p₂ p₃
hne : p₂ ≠ p₃
simp_rw : (-∡ p₃ p₄ p₂).sign = (-∡ p₃ p₄ p₁).sign
simp_rw₁ : -(∡ p₃ p₄ p₂).sign = -(∡ p₃ p₄ p₁).sign
⊢ (∡ 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]

Premises used: Real.Angle.sign_neg, Wbtw.oangle_sign_eq_of_ne_left, EuclideanGeometry.oangle_rev, Ne.symm, Wbtw.symm
-- 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
h : Sbtw ℝ p₁ p₂ p₃
⊢ (∡ p₂ p₄ p₃).sign = (∡ p₁ p₄ p₃).sign

Tactic:
h.wbtw.oangle_sign_eq_of_ne_right _ h.ne_right

Premises used: Wbtw.oangle_sign_eq_of_ne_right, Sbtw.wbtw, Sbtw.ne_right
-- 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₁₃ : 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
rw₄ rw₅ : (∡ p₁ p₃ p₂).sign = (∡ p₁ p₃ p₂).sign
⊢ (∡ 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]

Premises used: EuclideanGeometry.oangle_rotate_sign, Sbtw.oangle_sign_eq, Sbtw.oangle_eq_right, Sbtw.symm, Sbtw.oangle_eq_left
-- 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₁₃ : 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
rw₄ rw₅ : (∡ p p₃ p₂).sign = (∡ p p₃ p₂).sign
⊢ (∡ 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]

Premises used: EuclideanGeometry.oangle_rotate_sign, Sbtw.oangle_sign_eq_right, Sbtw.oangle_eq_right, Sbtw.symm, Sbtw.oangle_sign_eq_left, Sbtw.oangle_eq_left
-- 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)
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
neg : ∀ (h : ¬p₁ = p₂), (∡ p₁ p₄ p₂).sign = (∡ p₁ p₃ p₂).sign
⊢ (∡ p₁ p₄ p₂).sign = (∡ p₁ p₃ p₂).sign

Tactic:
by_cases h : p₁ = 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)
s : AffineSubspace ℝ P
p₁ p₂ p₃ p₄ : P
hp₁ : p₁ ∈ s
hp₂ : p₂ ∈ s
hp₃p₄ : s.SSameSide p₃ p₄
h : p₁ = p₂
⊢ (∡ p₁ p₄ p₂).sign = (∡ p₁ p₃ p₂).sign

Tactic:
simp [h]
-- 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)
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}
⊢ ContinuousOn (Y := P × P × P) (fun (p : P) ↦ (p₁, p, p₂)) {y : P | s.SSameSide p₃ y}

Tactic:
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)
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}
⊢ IsConnected sp

Tactic:
have hc : IsConnected sp :=
    (isConnected_setOf_sSameSide hp₃p₄.2.1 hp₃p₄.nonempty).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)
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

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)
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
refine_2 : ∀ (p : P × P × P) (hp : p ∈ sp), p.2.2 ≠ p.2.1
⊢ ContinuousOn (Y := Real.Angle) (fun (p : P × P × P) ↦ ∡ p.1 p.2.1 p.2.2) sp

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)
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
⊢ ∃ (x : P), s.SSameSide p₃ x ∧ (p₁, x, p₂) = p

Tactic:
simp_rw [sp, Set.mem_image, Set.mem_setOf] at hp

Premises used: Set.mem_image, 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)
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
refine_1 : ∀ (p' : P) (hp' : s.SSameSide p₃ p'), (p₁, p', p₂).1 ≠ (p₁, p', p₂).2.1
⊢ p.1 ≠ p.2.1

Tactic:
obtain ⟨p', hp', 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)
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'
refine_1 : p₁ ≠ p'
⊢ (p₁, p', p₂).1 ≠ (p₁, p', p₂).2.1

Tactic:
dsimp only
-- 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)
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
refine_2 : ∀ (p' : P) (hp' : s.SSameSide p₃ p'), (p₁, p', p₂).2.2 ≠ (p₁, p', p₂).2.1
⊢ p.2.2 ≠ p.2.1

Tactic:
obtain ⟨p', hp', 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)
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'
refine_2 : p₂ ≠ p'
⊢ (p₁, p', p₂).2.2 ≠ (p₁, p', p₂).2.1

Tactic:
dsimp only
-- 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)
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
hp' : s.SSameSide p₃ p₁
⊢ False

Tactic:
hp'.2.2 hp₁

Premises used: And.right
-- 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)
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
hp' : s.SSameSide p₃ p₁
⊢ False

Tactic:
exact hp'.2.2 hp₁

Premises used: And.right
-- 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)
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
hp' : s.SSameSide p₃ p₂
⊢ False

Tactic:
hp'.2.2 hp₂

Premises used: And.right
-- 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)
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
hp' : s.SSameSide p₃ p₂
⊢ False

Tactic:
exact hp'.2.2 hp₂

Premises used: And.right
-- 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)
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

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₂
-- 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)
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
⊢ ∃ (x : P), s.SSameSide p₃ x ∧ (p₁, x, p₂) = p

Tactic:
simp_rw [sp, Set.mem_image, Set.mem_setOf] at hp

Premises used: Set.mem_image, 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)
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
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)
⊢ ∡ p.1 p.2.1 p.2.2 ≠ 0 ∧ ∡ p.1 p.2.1 p.2.2 ≠ (↑π : Real.Angle)

Tactic:
obtain ⟨p', hp', 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)
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'
dsimp : ∡ p₁ p' p₂ ≠ 0 ∧ ∡ p₁ p' p₂ ≠ (↑π : Real.Angle)
⊢ ∡ (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:
dsimp only
-- 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)
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'
rw : AffineIndependent ℝ ![p₁, p', p₂]
⊢ ∡ p₁ p' p₂ ≠ 0 ∧ ∡ p₁ p' p₂ ≠ (↑π : Real.Angle)

Tactic:
rw [oangle_ne_zero_and_ne_pi_iff_affineIndependent]

Premises used: EuclideanGeometry.oangle_ne_zero_and_ne_pi_iff_affineIndependent
-- 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)
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'
⊢ AffineIndependent ℝ ![p₁, p', p₂]

Tactic:
affineIndependent_of_ne_of_mem_of_notMem_of_mem h hp₁ hp'.2.2 hp₂

Premises used: affineIndependent_of_ne_of_mem_of_notMem_of_mem, And.right
-- 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)
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'
⊢ AffineIndependent ℝ ![p₁, p', p₂]

Tactic:
exact affineIndependent_of_ne_of_mem_of_notMem_of_mem h hp₁ hp'.2.2 hp₂

Premises used: affineIndependent_of_ne_of_mem_of_notMem_of_mem, And.right