awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ‖x‖ = ‖y‖
⊢ x = y ↔ o.oangle x y = 0

Tactic:
⟨fun he => ((o.eq_iff_norm_eq_and_oangle_eq_zero x y).1 he).2, fun ha =>
    (o.eq_iff_norm_eq_and_oangle_eq_zero x y).2 ⟨h, ha⟩⟩

Premises used: Iff.mpr, Orientation.eq_iff_norm_eq_and_oangle_eq_zero, And.right, And.intro, Iff.intro, 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 = 0
⊢ x = y ↔ ‖x‖ = ‖y‖

Tactic:
⟨fun he => ((o.eq_iff_norm_eq_and_oangle_eq_zero x y).1 he).1, fun hn =>
    (o.eq_iff_norm_eq_and_oangle_eq_zero x y).2 ⟨hn, h⟩⟩

Premises used: Iff.mpr, Orientation.eq_iff_norm_eq_and_oangle_eq_zero, And.left, And.intro, Iff.intro, 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 z : V
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
rw :
  (↑(HMul.hMul (β := ℂ) (HPow.hPow (β := ℕ) (↑‖y‖ : ℂ) 2)
            ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) z : ℂ)).arg :
      Real.Angle) =
    (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) z)) : Real.Angle)
hx₁ : Ne (α := ℂ) ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ) (0 : ℂ)
hy₁ : Ne (α := ℂ) ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) y : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) z : ℂ) (0 : ℂ)
⊢ (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) +
      (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) y : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) z)) : Real.Angle) =
    (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) z)) : Real.Angle)

Tactic:
rw [← Complex.arg_mul_coe_angle, o.kahler_mul y x z]

Premises used: Orientation.kahler_mul, Complex.arg_mul_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 z : V
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
e_r :
  (HMul.hMul (β := ℂ) (HPow.hPow (β := ℕ) (↑‖y‖ : ℂ) 2)
        ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) z : ℂ)).arg =
    arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) z)
⊢ (↑(HMul.hMul (β := ℂ) (HPow.hPow (β := ℕ) (↑‖y‖ : ℂ) 2)
            ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) z : ℂ)).arg :
      Real.Angle) =
    (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) z)) : Real.Angle)

Tactic:
congr 1
-- 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 z : V
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ 0 < HPow.hPow (β := ℕ) ‖y‖ 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)
x y z : V
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ (HMul.hMul (β := ℂ) (HPow.hPow (β := ℕ) (↑‖y‖ : ℂ) 2)
        ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) z : ℂ)).arg =
    arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) z)

Tactic:
exact mod_cast Complex.arg_real_mul _ (by positivity : 0 < ‖y‖ ^ 2)

Premises used: Complex.arg_real_mul
-- 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 z : V
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 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 z : V
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 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 z : V
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ Ne (α := ℂ) ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) y : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) z : ℂ) (0 : ℂ)

Tactic:
o.kahler_ne_zero hy hz

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 z : V
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ Ne (α := ℂ) ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) y : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) z : ℂ) (0 : ℂ)

Tactic:
exact o.kahler_ne_zero hy hz

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 z : V
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
rw : o.oangle x y + o.oangle y z = o.oangle x z
rw₁ rw₂ : o.oangle x z = o.oangle x z
⊢ o.oangle y z + o.oangle x y = o.oangle x z

Tactic:
rw [add_comm, o.oangle_add hx hy hz]

Premises used: Orientation.oangle_add, add_comm
-- 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 z : V
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
rw : o.oangle x z = o.oangle y z + o.oangle x y
rw₁ rw₂ : o.oangle x z = o.oangle x z
⊢ o.oangle x z - o.oangle x y = o.oangle y z

Tactic:
rw [sub_eq_iff_eq_add, o.oangle_add_swap hx hy hz]

Premises used: Orientation.oangle_add_swap, sub_eq_iff_eq_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 y z : V
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
rw : o.oangle x z = o.oangle x y + o.oangle y z
rw₁ rw₂ : o.oangle x z = o.oangle x z
⊢ o.oangle x z - o.oangle y z = o.oangle x y

Tactic:
rw [sub_eq_iff_eq_add, o.oangle_add hx hy hz]

Premises used: Orientation.oangle_add, sub_eq_iff_eq_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 y z : V
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ o.oangle x y + o.oangle y z + o.oangle z x = 0

Tactic:
simp [hx, hy, hz]
-- 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 z : V
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
⊢ o.oangle x y + (↑π : Real.Angle) + (o.oangle y z + (↑π : Real.Angle)) + (o.oangle z x + (↑π : Real.Angle)) =
    o.oangle x y + o.oangle y z + o.oangle z x + ((↑π : Real.Angle) + (↑π : Real.Angle) + (↑π : Real.Angle))

Tactic:
abel
-- 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 z : V
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
rw : o.oangle x y + (↑π : Real.Angle) + o.oangle (-y) z + o.oangle (-z) x = (↑π : Real.Angle)
rw₁ : o.oangle x y + (↑π : Real.Angle) + (o.oangle y z + (↑π : Real.Angle)) + o.oangle (-z) x = (↑π : Real.Angle)
rw₂ :
  o.oangle x y + (↑π : Real.Angle) + (o.oangle y z + (↑π : Real.Angle)) + (o.oangle z x + (↑π : Real.Angle)) =
    (↑π : Real.Angle)
rw₃ :
  o.oangle x y + o.oangle y z + o.oangle z x + ((↑π : Real.Angle) + (↑π : Real.Angle) + (↑π : Real.Angle)) =
    (↑π : Real.Angle)
rw₄ : 0 + ((↑π : Real.Angle) + (↑π : Real.Angle) + (↑π : Real.Angle)) = (↑π : Real.Angle)
rw₅ : 0 + (0 + (↑π : Real.Angle)) = (↑π : Real.Angle)
rw₆ : 0 + (↑π : Real.Angle) = (↑π : Real.Angle)
rw₇ rw₈ : (↑π : Real.Angle) = (↑π : Real.Angle)
⊢ o.oangle (-x) y + o.oangle (-y) z + o.oangle (-z) x = (↑π : Real.Angle)

Tactic:
rw [o.oangle_neg_left hx hy, o.oangle_neg_left hy hz, o.oangle_neg_left hz hx,
    show o.oangle x y + π + (o.oangle y z + π) + (o.oangle z x + π) =
      o.oangle x y + o.oangle y z + o.oangle z x + (π + π + π : Real.Angle) by abel,
    o.oangle_add_cyc3 hx hy hz, Real.Angle.coe_pi_add_coe_pi, zero_add, zero_add]

Premises used: Orientation.oangle_neg_left, zero_add, Orientation.oangle_add_cyc3, Real.Angle.coe_pi_add_coe_pi
-- 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 z : V
hx : x ≠ 0
hy : y ≠ 0
hz : z ≠ 0
simp_rw : o.oangle (-x) y + o.oangle (-y) z + o.oangle (-z) x = (↑π : Real.Angle)
⊢ o.oangle x (-y) + o.oangle y (-z) + o.oangle z (-x) = (↑π : Real.Angle)

Tactic:
simp_rw [← oangle_neg_left_eq_neg_right, o.oangle_add_cyc3_neg_left hx hy hz]

Premises used: Orientation.oangle_neg_left_eq_neg_right, Orientation.oangle_add_cyc3_neg_left
-- 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 : ‖x‖ = ‖y‖
⊢ o.oangle x (x - y) = o.oangle (y - x) y

Tactic:
simp [oangle, h]

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 y : V
hn : x ≠ y
h : ‖x‖ = ‖y‖
rw : o.oangle y x = (↑π : Real.Angle) - (o.oangle (y - x) y + o.oangle (y - x) y)
⊢ o.oangle y x = (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) y)

Tactic:
rw [two_zsmul]

Premises used: two_zsmul
-- 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
hn : x ≠ y
h : ‖x‖ = ‖y‖
nth_rw : o.oangle y x = (↑π : Real.Angle) - (o.oangle x (x - y) + o.oangle (y - x) y)
⊢ o.oangle y x = (↑π : Real.Angle) - (o.oangle (y - x) y + o.oangle (y - x) y)

Tactic:
nth_rw 1 [← o.oangle_sub_eq_oangle_sub_rev_of_norm_eq h]

Premises used: Orientation.oangle_sub_eq_oangle_sub_rev_of_norm_eq
-- 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
hn : x ≠ y
h : ‖x‖ = ‖y‖
rw : o.oangle (-y) (-x) + o.oangle x (x - y) + o.oangle (y - x) y = (↑π : Real.Angle)
⊢ o.oangle y x = (↑π : Real.Angle) - (o.oangle x (x - y) + o.oangle (y - x) y)

Tactic:
rw [eq_sub_iff_add_eq, ← oangle_neg_neg, ← add_assoc]

Premises used: add_assoc, eq_sub_iff_add_eq, Orientation.oangle_neg_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 : V
hn : x ≠ 0
h : ‖x‖ = norm.{u_1} (E := V) 0
⊢ x = 0

Tactic:
rw [norm_zero, norm_eq_zero] at h

Premises used: norm_eq_zero, norm_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
hn : x ≠ 0
h : x = 0
⊢ False

Tactic:
hn 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
hn : x ≠ 0
h : x = 0
⊢ False

Tactic:
exact hn 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
hn : x ≠ y
h : ‖x‖ = ‖y‖
⊢ y ≠ 0

Tactic:
have hy : y ≠ 0 := by
    rintro rfl
    rw [norm_zero, norm_eq_zero] at h
    exact hn 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
hn : x ≠ y
h : ‖x‖ = ‖y‖
hy : y ≠ 0
⊢ x ≠ 0

Tactic:
have hx : x ≠ 0 := norm_ne_zero_iff.1 (h.symm ▸ norm_ne_zero_iff.2 hy)
-- 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
hn : x ≠ y
h : ‖x‖ = ‖y‖
hy : y ≠ 0
hx : x ≠ 0
⊢ o.oangle (-y) (-x) + o.oangle x (-(y - x)) + o.oangle (y - x) (- -y) = (↑π : Real.Angle)

Tactic:
o.oangle_add_cyc3_neg_right (neg_ne_zero.2 hy) hx (sub_ne_zero_of_ne hn.symm)

Premises used: Iff.mpr, Ne.symm, sub_ne_zero_of_ne, neg_ne_zero, Orientation.oangle_add_cyc3_neg_right
-- 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
hn : x ≠ y
h : ‖x‖ = ‖y‖
hy : y ≠ 0
hx : x ≠ 0
h₁ :
  o.oangle (-y) (-x) + o.oangle x (x - y) + o.oangle (y - x) y =
    o.oangle (-y) (-x) + o.oangle x (-(y - x)) + o.oangle (y - x) (- -y)
⊢ o.oangle (-y) (-x) + o.oangle x (x - y) + o.oangle (y - x) y = (↑π : Real.Angle)

Tactic:
convert! o.oangle_add_cyc3_neg_right (neg_ne_zero.2 hy) hx (sub_ne_zero_of_ne hn.symm) using 1

Premises used: Iff.mpr, Ne.symm, sub_ne_zero_of_ne, neg_ne_zero, Orientation.oangle_add_cyc3_neg_right
-- 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
hn : x ≠ y
h : ‖x‖ = ‖y‖
hy : y ≠ 0
hx : x ≠ 0
⊢ o.oangle (-y) (-x) + o.oangle x (x - y) + o.oangle (y - x) y =
    o.oangle (-y) (-x) + o.oangle x (-(y - x)) + o.oangle (y - x) (- -y)

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
V : Type u_1
V' : Type u_2
inst : NormedAddCommGroup V
inst_1 : NormedAddCommGroup V'
inst_2 : InnerProductSpace ℝ V
inst_3 : InnerProductSpace ℝ V'
inst_4 : Fact (finrank ℝ V = 2)
inst_5 : Fact (finrank ℝ V' = 2)
o : Orientation ℝ V (Fin 2)
x y : V'
f : V ≃ₗᵢ[ℝ] V'
⊢ oangle
      (((map (Fin 2) f.toLinearEquiv : Equiv.{u_1 + 1, u_2 + 1} (Orientation ℝ V (Fin 2)) (Orientation ℝ V' (Fin 2))) :
          (a : Orientation ℝ V (Fin 2)) → Orientation ℝ V' (Fin 2))
        o)
      x y =
    o.oangle ((f.symm : (a : V') → V) x) ((f.symm : (a : V') → V) y)

Tactic:
simp [oangle, o.kahler_map]

Premises used: Orientation.oangle, Orientation.kahler_map
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
Goal:
w z : ℂ
⊢ Complex.orientation.oangle w z = (↑(HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z).arg : Real.Angle)

Tactic:
simp [oangle, mul_comm z]

Premises used: Orientation.oangle, mul_comm
-- 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)
f : V ≃ₗᵢ[ℝ] ℂ
hf :
  ((map (Fin 2) f.toLinearEquiv : Orientation ℝ V (Fin 2) ≃ Orientation ℝ ℂ (Fin 2)) :
        (a : Orientation ℝ V (Fin 2)) → Orientation ℝ ℂ (Fin 2))
      o =
    Complex.orientation
x y : V
rw :
  o.oangle x y =
    o.oangle ((f.symm : (a : ℂ) → V) ((f : (a : V) → ℂ) x : ℂ)) ((f.symm : (a : ℂ) → V) ((f : (a : V) → ℂ) y : ℂ))
⊢ o.oangle x y =
    (↑(HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : V) → ℂ) x : ℂ) : ℂ)
            ((f : (a : V) → ℂ) y : ℂ)).arg :
      Real.Angle)

Tactic:
rw [← Complex.oangle, ← hf, o.oangle_map]

Premises used: Complex.oangle, Orientation.oangle_map
-- 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)
f : V ≃ₗᵢ[ℝ] ℂ
hf :
  ((map (Fin 2) f.toLinearEquiv : Orientation ℝ V (Fin 2) ≃ Orientation ℝ ℂ (Fin 2)) :
        (a : Orientation ℝ V (Fin 2)) → Orientation ℝ ℂ (Fin 2))
      o =
    Complex.orientation
x y : V
rw : o.oangle x y = o.oangle x ((f.symm : (a : ℂ) → V) ((f : (a : V) → ℂ) y : ℂ))
⊢ o.oangle x y =
    o.oangle ((f.symm : (a : ℂ) → V) ((f : (a : V) → ℂ) x : ℂ)) ((f.symm : (a : ℂ) → V) ((f : (a : V) → ℂ) y : ℂ))

Tactic:
rw [LinearIsometryEquiv.symm_apply_apply]

Premises used: LinearIsometryEquiv.symm_apply_apply
-- 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)
f : V ≃ₗᵢ[ℝ] ℂ
hf :
  ((map (Fin 2) f.toLinearEquiv : Orientation ℝ V (Fin 2) ≃ Orientation ℝ ℂ (Fin 2)) :
        (a : Orientation ℝ V (Fin 2)) → Orientation ℝ ℂ (Fin 2))
      o =
    Complex.orientation
x y : V
rw rw₁ : o.oangle x y = o.oangle x y
⊢ o.oangle x y = o.oangle x ((f.symm : (a : ℂ) → V) ((f : (a : V) → ℂ) y : ℂ))

Tactic:
rw [LinearIsometryEquiv.symm_apply_apply]

Premises used: LinearIsometryEquiv.symm_apply_apply
-- 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)
f : V ≃ₗᵢ[ℝ] ℂ
hf :
  ((map (Fin 2) f.toLinearEquiv : Orientation ℝ V (Fin 2) ≃ Orientation ℝ ℂ (Fin 2)) :
        (a : Orientation ℝ V (Fin 2)) → Orientation ℝ ℂ (Fin 2))
      o =
    Complex.orientation
x y : V
iterate iterate₁ iterate₂ iterate₃ : o.oangle x y = o.oangle x ((f.symm : (a : ℂ) → V) ((f : (a : V) → ℂ) y : ℂ))
⊢ o.oangle x y =
    o.oangle ((f.symm : (a : ℂ) → V) ((f : (a : V) → ℂ) x : ℂ)) ((f.symm : (a : ℂ) → V) ((f : (a : V) → ℂ) y : ℂ))

Tactic:
iterate 2 rw [LinearIsometryEquiv.symm_apply_apply]

Premises used: LinearIsometryEquiv.symm_apply_apply
-- 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 x y

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 y : V
pos : ∀ (hx : x = 0), ⟪x, y⟫ = ‖x‖ * ‖y‖ * (o.oangle x y).cos
neg : ∀ (hx : ¬x = 0), ⟪x, y⟫ = ‖x‖ * ‖y‖ * (o.oangle x y).cos
⊢ ⟪x, y⟫ = ‖x‖ * ‖y‖ * (o.oangle x y).cos

Tactic:
by_cases hx : x = 0
-- 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
⊢ ⟪x, y⟫ = ‖x‖ * ‖y‖ * (o.oangle x y).cos

Tactic:
simp [hx]
-- 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
pos : ∀ (hy : y = 0), ⟪x, y⟫ = ‖x‖ * ‖y‖ * (o.oangle x y).cos
neg : ∀ (hy : ¬y = 0), ⟪x, y⟫ = ‖x‖ * ‖y‖ * (o.oangle x y).cos
⊢ ⟪x, y⟫ = ‖x‖ * ‖y‖ * (o.oangle x y).cos

Tactic:
by_cases hy : y = 0
-- 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
⊢ ⟪x, y⟫ = ‖x‖ * ‖y‖ * (o.oangle x y).cos

Tactic:
simp [hy]
-- 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
neg : ⟪x, y⟫ = ‖x‖ * ‖y‖ * (re ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y) / (‖x‖ * ‖y‖))
neg₁ : Ne (α := ℂ) ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ) (0 : ℂ)
⊢ ⟪x, y⟫ = ‖x‖ * ‖y‖ * (o.oangle x y).cos

Tactic:
rw [oangle, Real.Angle.cos_coe, Complex.cos_arg, o.norm_kahler]

Premises used: Orientation.oangle, Real.Angle.cos_coe, Orientation.norm_kahler, Complex.cos_arg
-- 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
neg :
  ⟪x, y⟫ =
    ‖x‖ * ‖y‖ *
      ((⟪x, y⟫ +
          (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : V) → V →ₗ[ℝ] ℝ) x : V →ₗ[ℝ] ℝ) : (a : V) → ℝ) y : ℝ)
              (0 : ℝ) -
            0 * I.im)) /
        (‖x‖ * ‖y‖))
⊢ ⟪x, y⟫ = ‖x‖ * ‖y‖ * (re ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y) / (‖x‖ * ‖y‖))

Tactic:
simp only [kahler_apply_apply, real_smul, add_re, ofReal_re, mul_re, I_re, ofReal_im]

Premises used: Complex.real_smul, Complex.mul_re, Complex.add_re, Complex.I_re, Complex.ofReal_re, Orientation.kahler_apply_apply, Complex.ofReal_im
-- 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
⊢ ⟪x, y⟫ =
    ‖x‖ * ‖y‖ *
      ((⟪x, y⟫ +
          (HMul.hMul (α := ℝ) (β := ℝ) ((((o.areaForm : (a : V) → V →ₗ[ℝ] ℝ) x : V →ₗ[ℝ] ℝ) : (a : V) → ℝ) y : ℝ)
              (0 : ℝ) -
            0 * I.im)) /
        (‖x‖ * ‖y‖))

Tactic:
simp [field]
-- 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
rw : (o.oangle x y).cos = ‖x‖ * ‖y‖ * (o.oangle x y).cos / (‖x‖ * ‖y‖)
⊢ (o.oangle x y).cos = ⟪x, y⟫ / (‖x‖ * ‖y‖)

Tactic:
rw [o.inner_eq_norm_mul_norm_mul_cos_oangle]

Premises used: Orientation.inner_eq_norm_mul_norm_mul_cos_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 y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ (o.oangle x y).cos = ‖x‖ * ‖y‖ * (o.oangle x y).cos / (‖x‖ * ‖y‖)

Tactic:
field
-- 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
rw : ⟪x, y⟫ / (‖x‖ * ‖y‖) = Real.cos (InnerProductGeometry.angle x y)
rw₁ rw₂ : ⟪x, y⟫ / (‖x‖ * ‖y‖) = ⟪x, y⟫ / (‖x‖ * ‖y‖)
⊢ (o.oangle x y).cos = Real.cos (InnerProductGeometry.angle x y)

Tactic:
rw [o.cos_oangle_eq_inner_div_norm_mul_norm hx hy, InnerProductGeometry.cos_angle]

Premises used: InnerProductGeometry.cos_angle, Orientation.cos_oangle_eq_inner_div_norm_mul_norm