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₄ + (↑π : Real.Angle)
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₄ + (↑π : Real.Angle)
hs : SOppSide (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 : SOppSide (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 : SOppSide (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 : SOppSide (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 : SOppSide (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 : SOppSide (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_angle_div_two_of_oangle_eq_of_sSameSide h₁₂ ha' (hs.trans hs')

Premises used: 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₄ + (↑π : Real.Angle)
hs : SOppSide (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 : SOppSide (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:
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₄ + (↑π : Real.Angle)
hs : SOppSide (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:
exact h
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V × V
hx1 : x.1 ≠ 0
hx2 : x.2 ≠ 0
⊢ ContinuousAt (Y := Real.Angle) (fun (y : V × V) ↦ o.oangle y.1 y.2) x

Tactic:
(Complex.continuousAt_arg_coe_angle ?_).comp ?_

Premises used: Orientation.oangle, Real.Angle.coe, Complex.continuousAt_arg_coe_angle, ContinuousAt.comp
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V × V
hx1 : x.1 ≠ 0
hx2 : x.2 ≠ 0
refine_1 : Ne (α := ℂ) ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x.1 : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) x.2 : ℂ) (0 : ℂ)
refine_2 :
  ContinuousAt (Y := ℂ) (fun (y : V × V) ↦ (((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) y.1 : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y.2) x
⊢ ContinuousAt (Y := Real.Angle) (fun (y : V × V) ↦ o.oangle y.1 y.2) x

Tactic:
refine (Complex.continuousAt_arg_coe_angle ?_).comp ?_

Premises used: Complex.continuousAt_arg_coe_angle, ContinuousAt.comp
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V × V
hx1 : x.1 ≠ 0
hx2 : x.2 ≠ 0
⊢ Ne (α := ℂ) ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x.1 : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) x.2 : ℂ) (0 : ℂ)

Tactic:
o.kahler_ne_zero hx1 hx2

Premises used: Orientation.kahler_ne_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V × V
hx1 : x.1 ≠ 0
hx2 : x.2 ≠ 0
⊢ Ne (α := ℂ) ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x.1 : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) x.2 : ℂ) (0 : ℂ)

Tactic:
exact o.kahler_ne_zero hx1 hx2

Premises used: Orientation.kahler_ne_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V × V
hx1 : x.1 ≠ 0
hx2 : x.2 ≠ 0
⊢ ContinuousAt (Y := ℂ) (fun (y : V × V) ↦ (((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) y.1 : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y.2) x

Tactic:
((continuous_ofReal.comp continuous_inner).add
    ((continuous_ofReal.comp o.areaForm'.continuous₂).mul continuous_const)).continuousAt

Premises used: ContinuousLinearMap.continuous₂, Continuous.comp, continuous_const, Orientation.areaForm', Continuous.continuousAt, continuous_inner, Continuous.mul, Complex.continuous_ofReal, Continuous.add
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V × V
hx1 : x.1 ≠ 0
hx2 : x.2 ≠ 0
⊢ ContinuousAt (Y := ℂ) (fun (y : V × V) ↦ (((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) y.1 : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y.2) x

Tactic:
exact ((continuous_ofReal.comp continuous_inner).add
    ((continuous_ofReal.comp o.areaForm'.continuous₂).mul continuous_const)).continuousAt

Premises used: ContinuousLinearMap.continuous₂, Continuous.comp, continuous_const, Orientation.areaForm', Continuous.continuousAt, continuous_inner, Continuous.mul, Complex.continuous_ofReal, Continuous.add
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
⊢ o.oangle 0 x = 0

Tactic:
simp [oangle]

Premises used: Orientation.oangle
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
⊢ o.oangle x 0 = 0

Tactic:
simp [oangle]

Premises used: Orientation.oangle
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
rw : (↑(↑(HPow.hPow (β := ℕ) ‖x‖ 2) : ℂ).arg : Real.Angle) = 0
⊢ o.oangle x x = 0

Tactic:
rw [oangle, kahler_apply_self, ← ofReal_pow]

Premises used: Orientation.oangle, Orientation.kahler_apply_self, Complex.ofReal_pow
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
⊢ Eq (α := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples (2 * π)))
    (↑0 : ℝ ⧸ AddSubgroup.zmultiples (2 * π)) 0

Tactic:
QuotientAddGroup.mk_zero (AddSubgroup.zmultiples (2 * π))

Premises used: Real.pi, HMul.hMul, QuotientAddGroup.mk_zero, AddSubgroup.zmultiples, OfNat.ofNat
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h :
  Real.Angle = HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples (2 * π)) →
    (↑(HPow.hPow (β := ℕ) ‖x‖ 2) : ℂ).arg = 0
⊢ (↑(↑(HPow.hPow (β := ℕ) ‖x‖ 2) : ℂ).arg : Real.Angle) = 0

Tactic:
convert! QuotientAddGroup.mk_zero (AddSubgroup.zmultiples (2 * π))

Premises used: Real.pi, HMul.hMul, QuotientAddGroup.mk_zero, AddSubgroup.zmultiples, OfNat.ofNat
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
e_1 : Real.Angle = HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples (2 * π))
h : 0 ≤ HPow.hPow (β := ℕ) ‖x‖ 2
⊢ (↑(HPow.hPow (β := ℕ) ‖x‖ 2) : ℂ).arg = 0

Tactic:
apply arg_ofReal_of_nonneg

Premises used: Complex.arg_ofReal_of_nonneg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
e_1 : Real.Angle = HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples (2 * π))
⊢ 0 ≤ HPow.hPow (β := ℕ) ‖x‖ 2

Tactic:
positivity
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
y : V
h : o.oangle 0 y ≠ 0
⊢ False

Tactic:
simp at h
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : o.oangle x 0 ≠ 0
⊢ False

Tactic:
simp at h
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
h : o.oangle x x ≠ 0
⊢ False

Tactic:
simp at h
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑π : Real.Angle)
⊢ x ≠ 0

Tactic:
o.left_ne_zero_of_oangle_ne_zero (h.symm ▸ Real.Angle.pi_ne_zero : o.oangle x y ≠ 0)

Premises used: Orientation.left_ne_zero_of_oangle_ne_zero, Eq.rec, Real.Angle.pi_ne_zero, Eq.symm
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑π : Real.Angle)
⊢ y ≠ 0

Tactic:
o.right_ne_zero_of_oangle_ne_zero (h.symm ▸ Real.Angle.pi_ne_zero : o.oangle x y ≠ 0)

Premises used: Eq.rec, Orientation.right_ne_zero_of_oangle_ne_zero, Real.Angle.pi_ne_zero, Eq.symm
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑π : Real.Angle)
⊢ x ≠ y

Tactic:
o.ne_of_oangle_ne_zero (h.symm ▸ Real.Angle.pi_ne_zero : o.oangle x y ≠ 0)

Premises used: Eq.rec, Orientation.ne_of_oangle_ne_zero, Real.Angle.pi_ne_zero, Eq.symm
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
⊢ x ≠ 0

Tactic:
o.left_ne_zero_of_oangle_ne_zero (h.symm ▸ Real.Angle.pi_div_two_ne_zero : o.oangle x y ≠ 0)

Premises used: Orientation.left_ne_zero_of_oangle_ne_zero, Real.Angle.pi_div_two_ne_zero, Eq.rec, Eq.symm
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
⊢ y ≠ 0

Tactic:
o.right_ne_zero_of_oangle_ne_zero (h.symm ▸ Real.Angle.pi_div_two_ne_zero : o.oangle x y ≠ 0)

Premises used: Real.Angle.pi_div_two_ne_zero, Eq.rec, Orientation.right_ne_zero_of_oangle_ne_zero, Eq.symm
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(π / 2) : Real.Angle)
⊢ x ≠ y

Tactic:
o.ne_of_oangle_ne_zero (h.symm ▸ Real.Angle.pi_div_two_ne_zero : o.oangle x y ≠ 0)

Premises used: Real.Angle.pi_div_two_ne_zero, Eq.rec, Orientation.ne_of_oangle_ne_zero, Eq.symm
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(-π / 2) : Real.Angle)
⊢ x ≠ 0

Tactic:
o.left_ne_zero_of_oangle_ne_zero (h.symm ▸ Real.Angle.neg_pi_div_two_ne_zero : o.oangle x y ≠ 0)

Premises used: Orientation.left_ne_zero_of_oangle_ne_zero, Real.Angle.neg_pi_div_two_ne_zero, Eq.rec, Eq.symm
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(-π / 2) : Real.Angle)
⊢ y ≠ 0

Tactic:
o.right_ne_zero_of_oangle_ne_zero (h.symm ▸ Real.Angle.neg_pi_div_two_ne_zero : o.oangle x y ≠ 0)

Premises used: Real.Angle.neg_pi_div_two_ne_zero, Eq.rec, Orientation.right_ne_zero_of_oangle_ne_zero, Eq.symm
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = (↑(-π / 2) : Real.Angle)
⊢ x ≠ y

Tactic:
o.ne_of_oangle_ne_zero (h.symm ▸ Real.Angle.neg_pi_div_two_ne_zero : o.oangle x y ≠ 0)

Premises used: Real.Angle.neg_pi_div_two_ne_zero, Eq.rec, Orientation.ne_of_oangle_ne_zero, Eq.symm
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (o.oangle x y).sign ≠ 0
⊢ x ≠ 0

Tactic:
o.left_ne_zero_of_oangle_ne_zero (Real.Angle.sign_ne_zero_iff.1 h).1

Premises used: Orientation.left_ne_zero_of_oangle_ne_zero, And.left, Real.Angle.sign_ne_zero_iff, Iff.mp
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (o.oangle x y).sign ≠ 0
⊢ y ≠ 0

Tactic:
o.right_ne_zero_of_oangle_ne_zero (Real.Angle.sign_ne_zero_iff.1 h).1

Premises used: Orientation.right_ne_zero_of_oangle_ne_zero, And.left, Real.Angle.sign_ne_zero_iff, Iff.mp
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (o.oangle x y).sign ≠ 0
⊢ x ≠ y

Tactic:
o.ne_of_oangle_ne_zero (Real.Angle.sign_ne_zero_iff.1 h).1

Premises used: Orientation.ne_of_oangle_ne_zero, And.left, Real.Angle.sign_ne_zero_iff, Iff.mp
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (o.oangle x y).sign = 1
⊢ Ne (α := SignType) 1 0

Tactic:
decide
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (o.oangle x y).sign = -1
⊢ Ne (α := SignType) (-1) 0

Tactic:
decide
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ o.oangle y x = -o.oangle x y

Tactic:
simp only [oangle, o.kahler_swap y x, Complex.arg_conj_coe_angle]

Premises used: Orientation.oangle, Orientation.kahler_swap, Complex.arg_conj_coe_angle
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ o.oangle x y + o.oangle y x = 0

Tactic:
simp [o.oangle_rev y x]

Premises used: Orientation.oangle_rev
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
simp :
  (↑(arg (((-(o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) =
    (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) + (↑π : Real.Angle)
⊢ o.oangle (-x) y = o.oangle x y + (↑π : Real.Angle)

Tactic:
simp only [oangle, map_neg]

Premises used: Orientation.oangle, map_neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ (↑(arg (-(((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) =
    (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) + (↑π : Real.Angle)

Tactic:
Complex.arg_neg_coe_angle _

Premises used: Complex.arg_neg_coe_angle
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
convert_2 : Ne (α := ℂ) ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ) (0 : ℂ)
⊢ (↑(arg (((-(o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) =
    (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) + (↑π : Real.Angle)

Tactic:
convert! Complex.arg_neg_coe_angle _

Premises used: Complex.arg_neg_coe_angle
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ Ne (α := ℂ) ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ) (0 : ℂ)

Tactic:
o.kahler_ne_zero hx hy

Premises used: Orientation.kahler_ne_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ Ne (α := ℂ) ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ) (0 : ℂ)

Tactic:
exact o.kahler_ne_zero hx hy

Premises used: Orientation.kahler_ne_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
simp :
  (↑(arg (-(((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) =
    (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) + (↑π : Real.Angle)
⊢ o.oangle x (-y) = o.oangle x y + (↑π : Real.Angle)

Tactic:
simp only [oangle, map_neg]

Premises used: Orientation.oangle, map_neg
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : InnerProductSpace ℝ V
inst_2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
convert_2 : Ne (α := ℂ) ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ) (0 : ℂ)
⊢ (↑(arg (-(((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) =
    (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) + (↑π : Real.Angle)

Tactic:
convert! Complex.arg_neg_coe_angle _

Premises used: Complex.arg_neg_coe_angle