awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
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 :
      Real.Angle) =
    (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) z)) : Real.Angle)
have 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)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
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 y z + o.oangle x y = o.oangle x z
have rw : o.oangle x y + o.oangle y z = o.oangle x z
Tactic: rw [add_comm, o.oangle_add hx hy hz]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
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
⊢ o.oangle y z + o.oangle x y = o.oangle x z
have rw₁ : o.oangle x z = o.oangle x z
Tactic: rw [add_comm, o.oangle_add hx hy hz]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
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 z - o.oangle x y = o.oangle y z
have rw : o.oangle x z = o.oangle y z + o.oangle x y
Tactic: rw [sub_eq_iff_eq_add, o.oangle_add_swap hx hy hz]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
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
⊢ o.oangle x z - o.oangle x y = o.oangle y z
have rw₁ : o.oangle x z = o.oangle x z
Tactic: rw [sub_eq_iff_eq_add, o.oangle_add_swap hx hy hz]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
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 z - o.oangle y z = o.oangle x y
have rw : o.oangle x z = o.oangle x y + o.oangle y z
Tactic: rw [sub_eq_iff_eq_add, o.oangle_add hx hy hz]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
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
⊢ o.oangle x z - o.oangle y z = o.oangle x y
have rw₁ : o.oangle x z = o.oangle x z
Tactic: rw [sub_eq_iff_eq_add, o.oangle_add hx hy hz]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
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 = (↑π : Real.Angle)
have rw : o.oangle x y + (↑π : Real.Angle) + 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
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)
⊢ o.oangle (-x) y + o.oangle (-y) z + o.oangle (-z) x = (↑π : Real.Angle)
have rw₁ : o.oangle x y + (↑π : Real.Angle) + (o.oangle y z + (↑π : Real.Angle)) + 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
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)
⊢ o.oangle (-x) y + o.oangle (-y) z + o.oangle (-z) x = (↑π : Real.Angle)
have rw₂ : o.oangle x y + (↑π : Real.Angle) + (o.oangle y z + (↑π : Real.Angle)) + (o.oangle z x + (↑π : Real.Angle)) =
  (↑π : 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
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)
⊢ o.oangle (-x) y + o.oangle (-y) z + o.oangle (-z) x = (↑π : Real.Angle)
have rw₃ : o.oangle x y + o.oangle y z + o.oangle z x + ((↑π : Real.Angle) + (↑π : Real.Angle) + (↑π : Real.Angle)) =
  (↑π : 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
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)
⊢ o.oangle (-x) y + o.oangle (-y) z + o.oangle (-z) x = (↑π : Real.Angle)
have rw₄ : 0 + ((↑π : Real.Angle) + (↑π : Real.Angle) + (↑π : Real.Angle)) = (↑π : 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
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)
⊢ o.oangle (-x) y + o.oangle (-y) z + o.oangle (-z) x = (↑π : Real.Angle)
have rw₅ : 0 + (0 + (↑π : Real.Angle)) = (↑π : 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
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)
⊢ o.oangle (-x) y + o.oangle (-y) z + o.oangle (-z) x = (↑π : Real.Angle)
have rw₆ : 0 + (↑π : Real.Angle) = (↑π : 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
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)
⊢ o.oangle (-x) y + o.oangle (-y) z + o.oangle (-z) x = (↑π : Real.Angle)
have rw₇ : (↑π : Real.Angle) = (↑π : 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
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) = (↑π : Real.Angle)
have simp_rw : 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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
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‖
⊢ o.oangle y x = (↑π : Real.Angle) - HSMul.hSMul (α := ℤ) 2 (o.oangle (y - x) y)
have rw : o.oangle y x = (↑π : Real.Angle) - (o.oangle (y - x) y + o.oangle (y - x) y)
Tactic: rw [two_zsmul]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
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‖
⊢ o.oangle y x = (↑π : Real.Angle) - (o.oangle (y - x) y + o.oangle (y - x) y)
have nth_rw : o.oangle y x = (↑π : Real.Angle) - (o.oangle x (x - y) + o.oangle (y - x) y)
Tactic: nth_rw 1 [← o.oangle_sub_eq_oangle_sub_rev_of_norm_eq h]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
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‖
⊢ o.oangle y x = (↑π : Real.Angle) - (o.oangle x (x - y) + o.oangle (y - x) y)
have rw : o.oangle (-y) (-x) + o.oangle x (x - y) + o.oangle (y - x) y = (↑π : Real.Angle)
Tactic: rw [eq_sub_iff_add_eq, ← oangle_neg_neg, ← add_assoc]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (hypothesis)
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
⊢ False
have h₁ : x = 0
Tactic: rw [norm_zero, norm_eq_zero] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (hypothesis)
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‖
⊢ o.oangle (-y) (-x) + o.oangle x (x - y) + o.oangle (y - x) y = (↑π : Real.Angle)
have hy : y ≠ 0
Tactic: have hy : y ≠ 0 := by
    rintro rfl
    rw [norm_zero, norm_eq_zero] at h
    exact hn h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (hypothesis)
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
⊢ o.oangle (-y) (-x) + o.oangle x (x - y) + o.oangle (y - x) y = (↑π : Real.Angle)
have hx : x ≠ 0
Tactic: have hx : x ≠ 0 := norm_ne_zero_iff.1 (h.symm ▸ norm_ne_zero_iff.2 hy)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
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 = (↑π : Real.Angle)
have 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)
Tactic: convert! o.oangle_add_cyc3_neg_right (neg_ne_zero.2 hy) hx (sub_ne_zero_of_ne hn.symm) using 1
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
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
⊢ o.oangle x y =
    (↑(HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : V) → ℂ) x : ℂ) : ℂ)
            ((f : (a : V) → ℂ) y : ℂ)).arg :
      Real.Angle)
have rw : o.oangle x y =
  o.oangle ((f.symm : (a : ℂ) → V) ((f : (a : V) → ℂ) x : ℂ)) ((f.symm : (a : ℂ) → V) ((f : (a : V) → ℂ) y : ℂ))
Tactic: rw [← Complex.oangle, ← hf, o.oangle_map]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
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
⊢ o.oangle x y =
    o.oangle ((f.symm : (a : ℂ) → V) ((f : (a : V) → ℂ) x : ℂ)) ((f.symm : (a : ℂ) → V) ((f : (a : V) → ℂ) y : ℂ))
have rw : o.oangle x y = o.oangle x ((f.symm : (a : ℂ) → V) ((f : (a : V) → ℂ) y : ℂ))
Tactic: rw [LinearIsometryEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
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
⊢ o.oangle x y = o.oangle x ((f.symm : (a : ℂ) → V) ((f : (a : V) → ℂ) y : ℂ))
have rw : o.oangle x y = o.oangle x y
Tactic: rw [LinearIsometryEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
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
⊢ o.oangle x y =
    o.oangle ((f.symm : (a : ℂ) → V) ((f : (a : V) → ℂ) x : ℂ)) ((f.symm : (a : ℂ) → V) ((f : (a : V) → ℂ) y : ℂ))
have iterate : o.oangle x y = o.oangle x ((f.symm : (a : ℂ) → V) ((f : (a : V) → ℂ) y : ℂ))
Tactic: iterate 2 rw [LinearIsometryEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
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
⊢ ⟪x, y⟫ = ‖x‖ * ‖y‖ * (o.oangle x y).cos
have pos : ∀ (hx : x = 0), ⟪x, y⟫ = ‖x‖ * ‖y‖ * (o.oangle x y).cos
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
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
⊢ ⟪x, y⟫ = ‖x‖ * ‖y‖ * (o.oangle x y).cos
have neg : ∀ (hx : ¬x = 0), ⟪x, y⟫ = ‖x‖ * ‖y‖ * (o.oangle x y).cos
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
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
have pos : ∀ (hy : y = 0), ⟪x, y⟫ = ‖x‖ * ‖y‖ * (o.oangle x y).cos
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
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
⊢ ⟪x, y⟫ = ‖x‖ * ‖y‖ * (o.oangle x y).cos
have neg : ∀ (hy : ¬y = 0), ⟪x, y⟫ = ‖x‖ * ‖y‖ * (o.oangle x y).cos
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
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
have neg : ⟪x, y⟫ = ‖x‖ * ‖y‖ * (re ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y) / (‖x‖ * ‖y‖))
Tactic: rw [oangle, Real.Angle.cos_coe, Complex.cos_arg, o.norm_kahler]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
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‖))
⊢ ⟪x, y⟫ = ‖x‖ * ‖y‖ * (o.oangle x y).cos
have neg₁ : Ne (α := ℂ) ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ) (0 : ℂ)
Tactic: rw [oangle, Real.Angle.cos_coe, Complex.cos_arg, o.norm_kahler]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
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‖ * (re ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y) / (‖x‖ * ‖y‖))
have 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‖))
Tactic: simp only [kahler_apply_apply, real_smul, add_re, ofReal_re, mul_re, I_re, ofReal_im]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
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⟫ / (‖x‖ * ‖y‖)
have rw : (o.oangle x y).cos = ‖x‖ * ‖y‖ * (o.oangle x y).cos / (‖x‖ * ‖y‖)
Tactic: rw [o.inner_eq_norm_mul_norm_mul_cos_oangle]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
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 = Real.cos (InnerProductGeometry.angle x y)
have rw : ⟪x, y⟫ / (‖x‖ * ‖y‖) = Real.cos (InnerProductGeometry.angle x y)
Tactic: rw [o.cos_oangle_eq_inner_div_norm_mul_norm hx hy, InnerProductGeometry.cos_angle]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (goal)
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)
⊢ (o.oangle x y).cos = Real.cos (InnerProductGeometry.angle x y)
have rw₁ : ⟪x, y⟫ / (‖x‖ * ‖y‖) = ⟪x, y⟫ / (‖x‖ * ‖y‖)
Tactic: rw [o.cos_oangle_eq_inner_div_norm_mul_norm hx hy, InnerProductGeometry.cos_angle]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Basic (hypothesis)
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
⊢ InnerProductGeometry.angle x y = |(o.oangle x y).toReal|
have h0 : 0 ≤ InnerProductGeometry.angle x y
Tactic: have h0 := InnerProductGeometry.angle_nonneg x y