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
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
hadd : ∡ p₁ p₂ p₃ + ∡ p₃ p₂ p₄ = ∡ p₁ p₂ p₄
⊢ ∡ p₁ p₂ p₃ ≠ (↑π : Real.Angle)

Tactic:
have h : ∡ p₁ p₂ p₃ ≠ π := fun h ↦ hs.left_notMem ((oangle_eq_zero_or_eq_pi_iff_collinear.1
    (.inr h)).mem_affineSpan_of_mem_of_ne (by grind) (by grind) (by grind) 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)
p₁ p₂ p₃ p₄ : P
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
hadd : ∡ p₁ p₂ p₃ + ∡ p₃ p₂ p₄ = ∡ p₁ p₂ p₄
h : ∡ p₁ p₂ p₃ ≠ (↑π : Real.Angle)
⊢ (∡ p₁ p₂ p₃).toReal + (∡ p₃ p₂ p₄).toReal = (∡ p₁ p₂ p₃ + ∡ p₃ p₂ p₄).toReal

Tactic:
(Real.Angle.toReal_add_eq_toReal_add_toReal h (ha ▸ h) (.inr ?_)).symm

Premises used: Real.Angle.toReal_add_eq_toReal_add_toReal, Eq.symm, Or.inr
-- 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₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
hadd : ∡ p₁ p₂ p₃ + ∡ p₃ p₂ p₄ = ∡ p₁ p₂ p₄
h : ∡ p₁ p₂ p₃ ≠ (↑π : Real.Angle)
refine : (∡ p₁ p₂ p₃).sign = (∡ p₁ p₂ p₃ + ∡ p₃ p₂ p₄).sign
⊢ (∡ p₁ p₂ p₃).toReal + (∡ p₃ p₂ p₄).toReal = (∡ p₁ p₂ p₃ + ∡ p₃ p₂ p₄).toReal

Tactic:
refine (Real.Angle.toReal_add_eq_toReal_add_toReal h (ha ▸ h) (.inr ?_)).symm

Premises used: Real.Angle.toReal_add_eq_toReal_add_toReal, Eq.symm, Or.inr
-- 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₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
hadd : ∡ p₁ p₂ p₃ + ∡ p₃ p₂ p₄ = ∡ p₁ p₂ p₄
h : ∡ p₁ p₂ p₃ ≠ (↑π : Real.Angle)
rw : (∡ p₁ p₄ p₂).sign = (∡ p₁ p₃ p₂).sign
⊢ (∡ p₁ p₂ p₃).sign = (∡ p₁ p₂ p₃ + ∡ p₃ p₂ p₄).sign

Tactic:
rw [hadd, ← oangle_swap₂₃_sign p₁ p₃ p₂, ← oangle_swap₂₃_sign p₁ p₄ p₂, neg_inj, eq_comm]

Premises used: eq_comm, EuclideanGeometry.oangle_swap₂₃_sign, neg_inj
-- 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₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
hadd : ∡ p₁ p₂ p₃ + ∡ p₃ p₂ p₄ = ∡ p₁ p₂ p₄
h : ∡ p₁ p₂ p₃ ≠ (↑π : Real.Angle)
⊢ (∡ p₁ p₄ p₂).sign = (∡ p₁ p₃ p₂).sign

Tactic:
hs.oangle_sign_eq (left_mem_affineSpan_pair _ _ _) (right_mem_affineSpan_pair _ _ _)

Premises used: right_mem_affineSpan_pair, AffineSubspace.SSameSide.oangle_sign_eq, left_mem_affineSpan_pair
-- 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₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
hadd : ∡ p₁ p₂ p₃ + ∡ p₃ p₂ p₄ = ∡ p₁ p₂ p₄
h : ∡ p₁ p₂ p₃ ≠ (↑π : Real.Angle)
⊢ (∡ p₁ p₄ p₂).sign = (∡ p₁ p₃ p₂).sign

Tactic:
exact hs.oangle_sign_eq (left_mem_affineSpan_pair _ _ _) (right_mem_affineSpan_pair _ _ _)

Premises used: right_mem_affineSpan_pair, AffineSubspace.SSameSide.oangle_sign_eq, left_mem_affineSpan_pair
-- 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
h₁₂ : p₁ ≠ p₃
ha : ∡ p₁ p₃ p₃ = ∡ p₃ p₃ p₄
hs : SOppSide (affineSpan ℝ {p₁, p₃}) p₃ p₄
⊢ False

Tactic:
hs.left_notMem (right_mem_affineSpan_pair _ _ _)

Premises used: right_mem_affineSpan_pair, AffineSubspace.SOppSide.left_notMem
-- 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
h₁₂ : p₁ ≠ p₃
ha : ∡ p₁ p₃ p₃ = ∡ p₃ p₃ p₄
hs : SOppSide (affineSpan ℝ {p₁, p₃}) p₃ p₄
⊢ False

Tactic:
exact hs.left_notMem (right_mem_affineSpan_pair _ _ _)

Premises used: right_mem_affineSpan_pair, AffineSubspace.SOppSide.left_notMem
-- 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₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SOppSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
⊢ p₃ ≠ p₂

Tactic:
have h₃₂ : p₃ ≠ p₂ := by
    rintro rfl
    exact hs.left_notMem (right_mem_affineSpan_pair _ _ _)
-- 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
h₁₂ : p₁ ≠ p₄
ha : ∡ p₁ p₄ p₃ = ∡ p₃ p₄ p₄
hs : SOppSide (affineSpan ℝ {p₁, p₄}) p₃ p₄
h₃₂ : p₃ ≠ p₄
⊢ False

Tactic:
hs.right_notMem (right_mem_affineSpan_pair _ _ _)

Premises used: AffineSubspace.SOppSide.right_notMem, right_mem_affineSpan_pair
-- 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
h₁₂ : p₁ ≠ p₄
ha : ∡ p₁ p₄ p₃ = ∡ p₃ p₄ p₄
hs : SOppSide (affineSpan ℝ {p₁, p₄}) p₃ p₄
h₃₂ : p₃ ≠ p₄
⊢ False

Tactic:
exact hs.right_notMem (right_mem_affineSpan_pair _ _ _)

Premises used: AffineSubspace.SOppSide.right_notMem, right_mem_affineSpan_pair
-- 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₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SOppSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
⊢ p₄ ≠ p₂

Tactic:
have h₄₂ : p₄ ≠ p₂ := by
    rintro rfl
    exact hs.right_notMem (right_mem_affineSpan_pair _ _ _)
-- 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₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SOppSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
rw : ∡ p₁ p₂ p₃ + (↑π : Real.Angle) = ∡ p₃ p₂ p₄ + (↑π : Real.Angle)
⊢ ∡ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) =
    ∡ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) p₂ p₄

Tactic:
rw [oangle_pointReflection_left h₃₂ h₄₂, oangle_pointReflection_right h₁₂ h₃₂]

Premises used: EuclideanGeometry.oangle_pointReflection_left, EuclideanGeometry.oangle_pointReflection_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
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SOppSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
⊢ ∡ p₁ p₂ p₃ + (↑π : Real.Angle) = ∡ p₃ p₂ p₄ + (↑π : Real.Angle)

Tactic:
simpa using ha
-- 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₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SOppSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
⊢ ∡ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) =
    ∡ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) p₂ p₄

Tactic:
have ha' : ∡ p₁ p₂ (AffineEquiv.pointReflection ℝ p₂ p₃) =
      ∡ (AffineEquiv.pointReflection ℝ p₂ p₃) p₂ p₄ := by
    rw [oangle_pointReflection_left h₃₂ h₄₂, oangle_pointReflection_right h₁₂ h₃₂]
    simpa using ha
-- 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₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SOppSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
ha' :
  ∡ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) =
    ∡ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) p₂ p₄
⊢ SOppSide (affineSpan ℝ {p₁, p₂}) p₃ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃)

Tactic:
have hs' : line[ℝ, p₁, p₂].SOppSide p₃ (AffineEquiv.pointReflection ℝ p₂ p₃) :=
    AffineSubspace.sOppSide_pointReflection (right_mem_affineSpan_pair _ _ _) (hs.left_notMem)
-- 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₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SOppSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
ha' :
  ∡ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) =
    ∡ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) p₂ p₄
hs' : SOppSide (affineSpan ℝ {p₁, p₂}) p₃ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃)
⊢ ∠ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) = ∠ p₁ p₂ p₄ / 2

Tactic:
obtain h := angle_eq_angle_div_two_of_oangle_eq_of_sSameSide h₁₂ ha' (hs'.symm.trans hs)

Premises used: AffineSubspace.SOppSide.symm, AffineSubspace.SOppSide.trans, EuclideanGeometry.angle_eq_angle_div_two_of_oangle_eq_of_sSameSide
-- 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₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SOppSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
ha' :
  ∡ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) =
    ∡ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) p₂ p₄
hs' : SOppSide (affineSpan ℝ {p₁, p₂}) p₃ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃)
h : ∠ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) = ∠ p₁ p₂ p₄ / 2
⊢ π - ∠ p₁ p₂ p₃ = ∠ p₁ p₂ p₄ / 2

Tactic:
rw [angle_pointReflection_right] at h

Premises used: EuclideanGeometry.angle_pointReflection_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
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄
hs : SOppSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
ha' :
  ∡ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) =
    ∡ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃) p₂ p₄
hs' : SOppSide (affineSpan ℝ {p₁, p₂}) p₃ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₃)
h : π - ∠ p₁ p₂ p₃ = ∠ p₁ p₂ p₄ / 2
⊢ ∠ p₁ p₂ p₃ = π - ∠ p₁ p₂ p₄ / 2

Tactic:
linear_combination -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)
p₁ p₃ p₄ : P
h₁₂ : p₁ ≠ p₃
ha : ∡ p₁ p₃ p₃ = ∡ p₃ p₃ p₄ + (↑π : Real.Angle)
hs : SSameSide (affineSpan ℝ {p₁, p₃}) p₃ p₄
⊢ False

Tactic:
hs.left_notMem (right_mem_affineSpan_pair _ _ _)

Premises used: right_mem_affineSpan_pair, AffineSubspace.SSameSide.left_notMem
-- 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
h₁₂ : p₁ ≠ p₃
ha : ∡ p₁ p₃ p₃ = ∡ p₃ p₃ p₄ + (↑π : Real.Angle)
hs : SSameSide (affineSpan ℝ {p₁, p₃}) p₃ p₄
⊢ False

Tactic:
exact hs.left_notMem (right_mem_affineSpan_pair _ _ _)

Premises used: right_mem_affineSpan_pair, AffineSubspace.SSameSide.left_notMem
-- 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₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + (↑π : Real.Angle)
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
⊢ p₃ ≠ p₂

Tactic:
have h₃₂ : p₃ ≠ p₂ := by
    rintro rfl
    exact hs.left_notMem (right_mem_affineSpan_pair _ _ _)
-- 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
h₁₂ : p₁ ≠ p₄
ha : ∡ p₁ p₄ p₃ = ∡ p₃ p₄ p₄ + (↑π : Real.Angle)
hs : SSameSide (affineSpan ℝ {p₁, p₄}) p₃ p₄
h₃₂ : p₃ ≠ p₄
⊢ False

Tactic:
hs.right_notMem (right_mem_affineSpan_pair _ _ _)

Premises used: AffineSubspace.SSameSide.right_notMem, right_mem_affineSpan_pair
-- 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
h₁₂ : p₁ ≠ p₄
ha : ∡ p₁ p₄ p₃ = ∡ p₃ p₄ p₄ + (↑π : Real.Angle)
hs : SSameSide (affineSpan ℝ {p₁, p₄}) p₃ p₄
h₃₂ : p₃ ≠ p₄
⊢ False

Tactic:
exact hs.right_notMem (right_mem_affineSpan_pair _ _ _)

Premises used: AffineSubspace.SSameSide.right_notMem, right_mem_affineSpan_pair
-- 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₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + (↑π : Real.Angle)
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
⊢ p₄ ≠ p₂

Tactic:
have h₄₂ : p₄ ≠ p₂ := by
    rintro rfl
    exact hs.right_notMem (right_mem_affineSpan_pair _ _ _)
-- 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₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + (↑π : Real.Angle)
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
rw : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + (↑π : Real.Angle)
⊢ ∡ p₁ p₂ p₃ = ∡ p₃ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₄)

Tactic:
rw [oangle_pointReflection_right h₃₂ h₄₂]

Premises used: EuclideanGeometry.oangle_pointReflection_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
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + (↑π : Real.Angle)
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
⊢ ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + (↑π : Real.Angle)

Tactic:
ha
-- 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₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + (↑π : Real.Angle)
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
⊢ ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + (↑π : Real.Angle)

Tactic:
exact ha
-- 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₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + (↑π : Real.Angle)
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
⊢ ∡ p₁ p₂ p₃ = ∡ p₃ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₄)

Tactic:
have ha' : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ (AffineEquiv.pointReflection ℝ p₂ p₄) := by
    rw [oangle_pointReflection_right h₃₂ h₄₂]
    exact ha
-- 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₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + (↑π : Real.Angle)
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
ha' : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₄)
⊢ SOppSide (affineSpan ℝ {p₁, p₂}) p₄ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₄)

Tactic:
have hs' : line[ℝ, p₁, p₂].SOppSide p₄ (AffineEquiv.pointReflection ℝ p₂ p₄) :=
    AffineSubspace.sOppSide_pointReflection (right_mem_affineSpan_pair _ _ _) (hs.right_notMem)
-- 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₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + (↑π : Real.Angle)
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
ha' : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₄)
hs' : SOppSide (affineSpan ℝ {p₁, p₂}) p₄ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₄)
⊢ ∠ p₁ p₂ p₃ = π - ∠ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₄) / 2

Tactic:
obtain h := angle_eq_pi_sub_angle_div_two_of_oangle_eq_of_sOppSide h₁₂ ha' (hs.trans_sOppSide hs')

Premises used: AffineSubspace.SSameSide.trans_sOppSide, EuclideanGeometry.angle_eq_pi_sub_angle_div_two_of_oangle_eq_of_sOppSide
-- 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₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + (↑π : Real.Angle)
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
ha' : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₄)
hs' : SOppSide (affineSpan ℝ {p₁, p₂}) p₄ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₄)
h : ∠ p₁ p₂ p₃ = π - ∠ p₁ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₄) / 2
⊢ ∠ p₁ p₂ p₃ = π - (π - ∠ p₁ p₂ p₄) / 2

Tactic:
rw [angle_pointReflection_right] at h

Premises used: EuclideanGeometry.angle_pointReflection_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
h₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + (↑π : Real.Angle)
hs : SSameSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
h₃₂ : p₃ ≠ p₂
h₄₂ : p₄ ≠ p₂
ha' : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₄)
hs' : SOppSide (affineSpan ℝ {p₁, p₂}) p₄ ((AffineEquiv.pointReflection ℝ p₂ : (a : P) → P) p₄)
h : ∠ p₁ p₂ p₃ = π - (π - ∠ p₁ p₂ p₄) / 2
⊢ ∠ p₁ p₂ p₃ = (∠ p₁ p₂ p₄ + π) / 2

Tactic:
linear_combination 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)
p₁ p₃ p₄ : P
h₁₂ : p₁ ≠ p₃
ha : ∡ p₁ p₃ p₃ = ∡ p₃ p₃ p₄ + (↑π : Real.Angle)
hs : SOppSide (affineSpan ℝ {p₁, p₃}) p₃ p₄
⊢ False

Tactic:
hs.left_notMem (right_mem_affineSpan_pair _ _ _)

Premises used: right_mem_affineSpan_pair, AffineSubspace.SOppSide.left_notMem
-- 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
h₁₂ : p₁ ≠ p₃
ha : ∡ p₁ p₃ p₃ = ∡ p₃ p₃ p₄ + (↑π : Real.Angle)
hs : SOppSide (affineSpan ℝ {p₁, p₃}) p₃ p₄
⊢ False

Tactic:
exact hs.left_notMem (right_mem_affineSpan_pair _ _ _)

Premises used: right_mem_affineSpan_pair, AffineSubspace.SOppSide.left_notMem
-- 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₁₂ : p₁ ≠ p₂
ha : ∡ p₁ p₂ p₃ = ∡ p₃ p₂ p₄ + (↑π : Real.Angle)
hs : SOppSide (affineSpan ℝ {p₁, p₂}) p₃ p₄
⊢ p₃ ≠ p₂

Tactic:
have h₃₂ : p₃ ≠ p₂ := by
    rintro rfl
    exact hs.left_notMem (right_mem_affineSpan_pair _ _ _)
-- 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
h₁₂ : p₁ ≠ p₄
ha : ∡ p₁ p₄ p₃ = ∡ p₃ p₄ p₄ + (↑π : Real.Angle)
hs : SOppSide (affineSpan ℝ {p₁, p₄}) p₃ p₄
h₃₂ : p₃ ≠ p₄
⊢ False

Tactic:
hs.right_notMem (right_mem_affineSpan_pair _ _ _)

Premises used: AffineSubspace.SOppSide.right_notMem, right_mem_affineSpan_pair
-- 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
h₁₂ : p₁ ≠ p₄
ha : ∡ p₁ p₄ p₃ = ∡ p₃ p₄ p₄ + (↑π : Real.Angle)
hs : SOppSide (affineSpan ℝ {p₁, p₄}) p₃ p₄
h₃₂ : p₃ ≠ p₄
⊢ False

Tactic:
exact hs.right_notMem (right_mem_affineSpan_pair _ _ _)

Premises used: AffineSubspace.SOppSide.right_notMem, right_mem_affineSpan_pair