-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem inner_eq_norm_mul_norm_mul_cos_oangle (x y : V) :
    ⟪x, y⟫ = ‖x‖ * ‖y‖ * Real.Angle.cos (o.oangle x y)

Proof state:
case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : ¬y = 0
⊢ (o.kahler x) y ≠ 0

Tactic:
exact o.kahler_ne_zero hx hy

Result:
no goals

Proof state:
case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
⊢ inner x y = ‖x‖ * ‖y‖ * (o.oangle x y).cos

Tactic:
by_cases hy : y = 0

Result:
case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : y = 0
⊢ inner x y = ‖x‖ * ‖y‖ * (o.oangle x y).cos

case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : ¬y = 0
⊢ inner x y = ‖x‖ * ‖y‖ * (o.oangle x y).cos

Proof state:
case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : ¬y = 0
⊢ inner x y = ‖x‖ * ‖y‖ * (((o.kahler x) y).re / (‖x‖ * ‖y‖))

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

Result:
case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : ¬y = 0
⊢ inner x y = ‖x‖ * ‖y‖ * ((inner x y + ((o.areaForm x) y * 0 - 0 * I.im)) / (‖x‖ * ‖y‖))

Proof state:
case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x = 0
⊢ inner x y = ‖x‖ * ‖y‖ * (o.oangle x y).cos

Tactic:
simp [hx]

Result:
no goals

Proof state:
case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : ¬y = 0
⊢ inner x y = ‖x‖ * ‖y‖ * ((inner x y + ((o.areaForm x) y * 0 - 0 * I.im)) / (‖x‖ * ‖y‖))

Tactic:
simp (disch := field_simp_discharge) only [mul_zero, I_im, mul_one, sub_self, add_zero,
  mul_div_assoc', mul_div_cancel_left₀]

Result:
no goals

Proof state:
case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : ¬y = 0
⊢ inner x y = ‖x‖ * ‖y‖ * (o.oangle x y).cos

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

Result:
case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : ¬y = 0
⊢ inner x y = ‖x‖ * ‖y‖ * (((o.kahler x) y).re / (‖x‖ * ‖y‖))

case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : ¬y = 0
⊢ (o.kahler x) y ≠ 0

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
⊢ inner x y = ‖x‖ * ‖y‖ * (o.oangle x y).cos

Tactic:
by_cases hx : x = 0

Result:
case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x = 0
⊢ inner x y = ‖x‖ * ‖y‖ * (o.oangle x y).cos

case neg
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
⊢ inner x y = ‖x‖ * ‖y‖ * (o.oangle x y).cos

Proof state:
case pos
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : ¬x = 0
hy : y = 0
⊢ inner x y = ‖x‖ * ‖y‖ * (o.oangle x y).cos

Tactic:
simp [hy]

Result:
no goals