awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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
hp : 0 < ‖y‖ / ‖x‖
mp : y = (o.rotation (o.oangle x y) : (a : V) → V) ((‖y‖ / ‖x‖) • x)
mp₁ : y = (o.rotation (o.oangle ((‖y‖ / ‖x‖) • x) y) : (a : V) → V) ((‖y‖ / ‖x‖) • x)
mp₂ : (o.rotation (o.oangle ((‖y‖ / ‖x‖) • x) y) : (a : V) → V) ((‖y‖ / ‖x‖) • x) = y
mp₃ : ‖(‖y‖ / ‖x‖) • x‖ = ‖y‖
mp₄ : ‖‖y‖ / ‖x‖‖ * ‖x‖ = ‖y‖
mp₅ : ‖y‖ / ‖x‖ * ‖x‖ = ‖y‖
mp₆ mp₇ : ‖y‖ = ‖y‖
⊢ y = HSMul.hSMul (β := V) (‖y‖ / ‖x‖) ((o.rotation (o.oangle x y) : (a : V) → V) x : V)

Tactic:
rw [← map_smul, ← o.oangle_smul_left_of_pos x y hp, eq_comm,
      rotation_oangle_eq_iff_norm_eq, norm_smul, Real.norm_of_nonneg hp.le,
      div_mul_cancel₀ _ (norm_ne_zero_iff.2 hx)]

Premises used: Iff.mpr, div_mul_cancel₀, norm_smul, LT.lt.le, eq_comm, norm_ne_zero_iff, Orientation.rotation_oangle_eq_iff_norm_eq, map_smul, Real.norm_of_nonneg, Orientation.oangle_smul_left_of_pos
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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
θ : Real.Angle
hp : 0 < ‖y‖ / ‖x‖
hye : y = HSMul.hSMul (β := V) (‖y‖ / ‖x‖) ((o.rotation θ : (a : V) → V) x : V)
mpr : o.oangle x (HSMul.hSMul (β := V) (‖y‖ / ‖x‖) ((o.rotation θ : (a : V) → V) x : V)) = θ
mpr₁ : o.oangle x ((o.rotation θ : (a : V) → V) x) = θ
mpr₂ mpr₃ : θ = θ
⊢ o.oangle x y = θ

Tactic:
rw [hye, o.oangle_smul_right_of_pos _ _ hp, o.oangle_rotation_self_right hx]

Premises used: Orientation.oangle_rotation_self_right, Orientation.oangle_smul_right_of_pos
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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
θ : Real.Angle
mp : o.oangle x y = θ → ∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) r ((o.rotation θ : (a : V) → V) x : V)
mpr : (∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) r ((o.rotation θ : (a : V) → V) x : V)) → o.oangle x y = θ
⊢ o.oangle x y = θ ↔ ∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) r ((o.rotation θ : (a : V) → V) x : V)

Tactic:
constructor
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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
θ : Real.Angle
h : o.oangle x y = θ
⊢ y = HSMul.hSMul (β := V) (‖y‖ / ‖x‖) ((o.rotation θ : (a : V) → V) x : V)

Tactic:
rw [o.oangle_eq_iff_eq_norm_div_norm_smul_rotation_of_ne_zero hx hy] at h

Premises used: Orientation.oangle_eq_iff_eq_norm_div_norm_smul_rotation_of_ne_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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
θ : Real.Angle
h : y = HSMul.hSMul (β := V) (‖y‖ / ‖x‖) ((o.rotation θ : (a : V) → V) x : V)
⊢ ∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) r ((o.rotation θ : (a : V) → V) x : V)

Tactic:
⟨‖y‖ / ‖x‖, div_pos (norm_pos_iff.2 hy) (norm_pos_iff.2 hx), h⟩

Premises used: Iff.mpr, Norm.norm, norm_pos_iff, HDiv.hDiv, And.intro, Exists.intro, div_pos
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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
θ : Real.Angle
h : y = HSMul.hSMul (β := V) (‖y‖ / ‖x‖) ((o.rotation θ : (a : V) → V) x : V)
⊢ ∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) r ((o.rotation θ : (a : V) → V) x : V)

Tactic:
exact ⟨‖y‖ / ‖x‖, div_pos (norm_pos_iff.2 hy) (norm_pos_iff.2 hx), h⟩
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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
hx : x ≠ 0
θ : Real.Angle
r : ℝ
hr : 0 < r
hy : HSMul.hSMul (β := V) r ((o.rotation θ : (a : V) → V) x : V) ≠ 0
mpr : o.oangle x ((o.rotation θ : (a : V) → V) x) = θ
mpr₁ mpr₂ : θ = θ
⊢ o.oangle x (HSMul.hSMul (β := V) r ((o.rotation θ : (a : V) → V) x : V)) = θ

Tactic:
rw [o.oangle_smul_right_of_pos _ _ hr, o.oangle_rotation_self_right hx]

Premises used: Orientation.oangle_rotation_self_right, Orientation.oangle_smul_right_of_pos
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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
θ : Real.Angle
pos :
  ∀ (hx : x = 0),
    o.oangle x y = θ ↔
      x ≠ 0 ∧ y ≠ 0 ∧ y = HSMul.hSMul (β := V) (‖y‖ / ‖x‖) ((o.rotation θ : (a : V) → V) x : V) ∨
        θ = 0 ∧ (x = 0 ∨ y = 0)
neg :
  ∀ (hx : ¬x = 0),
    o.oangle x y = θ ↔
      x ≠ 0 ∧ y ≠ 0 ∧ y = HSMul.hSMul (β := V) (‖y‖ / ‖x‖) ((o.rotation θ : (a : V) → V) x : V) ∨
        θ = 0 ∧ (x = 0 ∨ y = 0)
⊢ o.oangle x y = θ ↔
    x ≠ 0 ∧ y ≠ 0 ∧ y = HSMul.hSMul (β := V) (‖y‖ / ‖x‖) ((o.rotation θ : (a : V) → V) x : V) ∨ θ = 0 ∧ (x = 0 ∨ y = 0)

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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
θ : Real.Angle
hx : x = 0
⊢ o.oangle x y = θ ↔
    x ≠ 0 ∧ y ≠ 0 ∧ y = HSMul.hSMul (β := V) (‖y‖ / ‖x‖) ((o.rotation θ : (a : V) → V) x : V) ∨ θ = 0 ∧ (x = 0 ∨ y = 0)

Tactic:
simp [hx, eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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
θ : Real.Angle
hx : ¬x = 0
pos :
  ∀ (hy : y = 0),
    o.oangle x y = θ ↔
      x ≠ 0 ∧ y ≠ 0 ∧ y = HSMul.hSMul (β := V) (‖y‖ / ‖x‖) ((o.rotation θ : (a : V) → V) x : V) ∨
        θ = 0 ∧ (x = 0 ∨ y = 0)
neg :
  ∀ (hy : ¬y = 0),
    o.oangle x y = θ ↔
      x ≠ 0 ∧ y ≠ 0 ∧ y = HSMul.hSMul (β := V) (‖y‖ / ‖x‖) ((o.rotation θ : (a : V) → V) x : V) ∨
        θ = 0 ∧ (x = 0 ∨ y = 0)
⊢ o.oangle x y = θ ↔
    x ≠ 0 ∧ y ≠ 0 ∧ y = HSMul.hSMul (β := V) (‖y‖ / ‖x‖) ((o.rotation θ : (a : V) → V) x : V) ∨ θ = 0 ∧ (x = 0 ∨ y = 0)

Tactic:
by_cases hy : y = 0
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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
θ : Real.Angle
hx : ¬x = 0
hy : y = 0
⊢ o.oangle x y = θ ↔
    x ≠ 0 ∧ y ≠ 0 ∧ y = HSMul.hSMul (β := V) (‖y‖ / ‖x‖) ((o.rotation θ : (a : V) → V) x : V) ∨ θ = 0 ∧ (x = 0 ∨ y = 0)

Tactic:
simp [hy, eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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
θ : Real.Angle
hx : ¬x = 0
hy : ¬y = 0
neg :
  y = HSMul.hSMul (β := V) (‖y‖ / ‖x‖) ((o.rotation θ : (a : V) → V) x : V) ↔
    x ≠ 0 ∧ y ≠ 0 ∧ y = HSMul.hSMul (β := V) (‖y‖ / ‖x‖) ((o.rotation θ : (a : V) → V) x : V) ∨ θ = 0 ∧ (x = 0 ∨ y = 0)
⊢ o.oangle x y = θ ↔
    x ≠ 0 ∧ y ≠ 0 ∧ y = HSMul.hSMul (β := V) (‖y‖ / ‖x‖) ((o.rotation θ : (a : V) → V) x : V) ∨ θ = 0 ∧ (x = 0 ∨ y = 0)

Tactic:
rw [o.oangle_eq_iff_eq_norm_div_norm_smul_rotation_of_ne_zero hx hy]

Premises used: Orientation.oangle_eq_iff_eq_norm_div_norm_smul_rotation_of_ne_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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
θ : Real.Angle
hx : ¬x = 0
hy : ¬y = 0
⊢ y = HSMul.hSMul (β := V) (‖y‖ / ‖x‖) ((o.rotation θ : (a : V) → V) x : V) ↔
    x ≠ 0 ∧ y ≠ 0 ∧ y = HSMul.hSMul (β := V) (‖y‖ / ‖x‖) ((o.rotation θ : (a : V) → V) x : V) ∨ θ = 0 ∧ (x = 0 ∨ y = 0)

Tactic:
simp [hx, hy]
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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
θ : Real.Angle
pos :
  ∀ (hx : x = 0),
    o.oangle x y = θ ↔
      (x ≠ 0 ∧ y ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) r ((o.rotation θ : (a : V) → V) x : V)) ∨
        θ = 0 ∧ (x = 0 ∨ y = 0)
neg :
  ∀ (hx : ¬x = 0),
    o.oangle x y = θ ↔
      (x ≠ 0 ∧ y ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) r ((o.rotation θ : (a : V) → V) x : V)) ∨
        θ = 0 ∧ (x = 0 ∨ y = 0)
⊢ o.oangle x y = θ ↔
    (x ≠ 0 ∧ y ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) r ((o.rotation θ : (a : V) → V) x : V)) ∨
      θ = 0 ∧ (x = 0 ∨ y = 0)

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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
θ : Real.Angle
hx : x = 0
⊢ o.oangle x y = θ ↔
    (x ≠ 0 ∧ y ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) r ((o.rotation θ : (a : V) → V) x : V)) ∨
      θ = 0 ∧ (x = 0 ∨ y = 0)

Tactic:
simp [hx, eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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
θ : Real.Angle
hx : ¬x = 0
pos :
  ∀ (hy : y = 0),
    o.oangle x y = θ ↔
      (x ≠ 0 ∧ y ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) r ((o.rotation θ : (a : V) → V) x : V)) ∨
        θ = 0 ∧ (x = 0 ∨ y = 0)
neg :
  ∀ (hy : ¬y = 0),
    o.oangle x y = θ ↔
      (x ≠ 0 ∧ y ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) r ((o.rotation θ : (a : V) → V) x : V)) ∨
        θ = 0 ∧ (x = 0 ∨ y = 0)
⊢ o.oangle x y = θ ↔
    (x ≠ 0 ∧ y ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) r ((o.rotation θ : (a : V) → V) x : V)) ∨
      θ = 0 ∧ (x = 0 ∨ y = 0)

Tactic:
by_cases hy : y = 0
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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
θ : Real.Angle
hx : ¬x = 0
hy : y = 0
⊢ o.oangle x y = θ ↔
    (x ≠ 0 ∧ y ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) r ((o.rotation θ : (a : V) → V) x : V)) ∨
      θ = 0 ∧ (x = 0 ∨ y = 0)

Tactic:
simp [hy, eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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
θ : Real.Angle
hx : ¬x = 0
hy : ¬y = 0
neg :
  (∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) r ((o.rotation θ : (a : V) → V) x : V)) ↔
    (x ≠ 0 ∧ y ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) r ((o.rotation θ : (a : V) → V) x : V)) ∨
      θ = 0 ∧ (x = 0 ∨ y = 0)
⊢ o.oangle x y = θ ↔
    (x ≠ 0 ∧ y ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) r ((o.rotation θ : (a : V) → V) x : V)) ∨
      θ = 0 ∧ (x = 0 ∨ y = 0)

Tactic:
rw [o.oangle_eq_iff_eq_pos_smul_rotation_of_ne_zero hx hy]

Premises used: Orientation.oangle_eq_iff_eq_pos_smul_rotation_of_ne_zero
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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
θ : Real.Angle
hx : ¬x = 0
hy : ¬y = 0
⊢ (∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) r ((o.rotation θ : (a : V) → V) x : V)) ↔
    (x ≠ 0 ∧ y ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) r ((o.rotation θ : (a : V) → V) x : V)) ∨
      θ = 0 ∧ (x = 0 ∨ y = 0)

Tactic:
simp [hx, hy]
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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 ≃ₗᵢ[ℝ] V
hd : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : V →ₗ[ℝ] V) → ℝ) (↑f.toLinearEquiv : V →ₗ[ℝ] V) : ℝ)
⊢ Nontrivial V

Tactic:
haveI : Nontrivial V := nontrivial_of_finrank_eq_succ (@Fact.out (finrank ℝ V = 2) _)
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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 ≃ₗᵢ[ℝ] V
hd : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : V →ₗ[ℝ] V) → ℝ) (↑f.toLinearEquiv : V →ₗ[ℝ] V) : ℝ)
this : Nontrivial V
⊢ ∃ (x : V), x ≠ 0

Tactic:
exists_ne (0 : V)

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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 ≃ₗᵢ[ℝ] V
hd : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : V →ₗ[ℝ] V) → ℝ) (↑f.toLinearEquiv : V →ₗ[ℝ] V) : ℝ)
this : Nontrivial V
obtain : ∀ (x : V) (hx : x ≠ 0), ∃ (θ : Real.Angle), f = o.rotation θ
⊢ ∃ (θ : Real.Angle), f = o.rotation θ

Tactic:
obtain ⟨x, hx⟩ : ∃ x, x ≠ (0 : V) := exists_ne (0 : V)

Premises used: exists_ne, OfNat.ofNat
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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 ≃ₗᵢ[ℝ] V
hd : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : V →ₗ[ℝ] V) → ℝ) (↑f.toLinearEquiv : V →ₗ[ℝ] V) : ℝ)
this : Nontrivial V
x : V
hx : x ≠ 0
h : f = o.rotation (o.oangle x ((f : (a : V) → V) x))
⊢ ∃ (θ : Real.Angle), f = o.rotation θ

Tactic:
use o.oangle x (f x)

Premises used: Orientation.oangle, DFunLike.coe
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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 ≃ₗᵢ[ℝ] V
hd : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : V →ₗ[ℝ] V) → ℝ) (↑f.toLinearEquiv : V →ₗ[ℝ] V) : ℝ)
this : Nontrivial V
x : V
hx : x ≠ 0
h : f.toLinearEquiv = (o.rotation (o.oangle x ((f : (a : V) → V) x))).toLinearEquiv
⊢ f = o.rotation (o.oangle x ((f : (a : V) → V) x))

Tactic:
apply LinearIsometryEquiv.toLinearEquiv_injective

Premises used: LinearIsometryEquiv.toLinearEquiv_injective
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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 ≃ₗᵢ[ℝ] V
hd : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : V →ₗ[ℝ] V) → ℝ) (↑f.toLinearEquiv : V →ₗ[ℝ] V) : ℝ)
this : Nontrivial V
x : V
hx : x ≠ 0
h : (↑f.toLinearEquiv : V →ₗ[ℝ] V) = (↑(o.rotation (o.oangle x ((f : (a : V) → V) x))).toLinearEquiv : V →ₗ[ℝ] V)
⊢ f.toLinearEquiv = (o.rotation (o.oangle x ((f : (a : V) → V) x))).toLinearEquiv

Tactic:
apply LinearEquiv.toLinearMap_injective

Premises used: LinearEquiv.toLinearMap_injective
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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 ≃ₗᵢ[ℝ] V
hd : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : V →ₗ[ℝ] V) → ℝ) (↑f.toLinearEquiv : V →ₗ[ℝ] V) : ℝ)
this : Nontrivial V
x : V
hx : x ≠ 0
h :
  ∀ (i : Fin 2),
    Eq (α := V)
      (((↑f.toLinearEquiv : V →ₗ[ℝ] V) : (a : V) → V) ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) i : V) : V)
      (((↑(o.rotation (o.oangle x ((f : (a : V) → V) x))).toLinearEquiv : V →ₗ[ℝ] V) : (a : V) → V)
          ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) i : V) :
        V)
⊢ (↑f.toLinearEquiv : V →ₗ[ℝ] V) = (↑(o.rotation (o.oangle x ((f : (a : V) → V) x))).toLinearEquiv : V →ₗ[ℝ] V)

Tactic:
apply (o.basisRightAngleRotation x hx).ext

Premises used: Orientation.basisRightAngleRotation, Module.Basis.ext
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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 ≃ₗᵢ[ℝ] V
hd : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : V →ₗ[ℝ] V) → ℝ) (↑f.toLinearEquiv : V →ₗ[ℝ] V) : ℝ)
this : Nontrivial V
x : V
hx : x ≠ 0
i : Fin 2
h :
  Eq (α := V)
    (((↑(o.rotation (o.oangle x ((f : (a : V) → V) x))).toLinearEquiv : V →ₗ[ℝ] V) : (a : V) → V)
        ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) i : V) :
      V)
    (((↑f.toLinearEquiv : V →ₗ[ℝ] V) : (a : V) → V) ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) i : V) : V)
⊢ Eq (α := V)
    (((↑f.toLinearEquiv : V →ₗ[ℝ] V) : (a : V) → V) ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) i : V) : V)
    (((↑(o.rotation (o.oangle x ((f : (a : V) → V) x))).toLinearEquiv : V →ₗ[ℝ] V) : (a : V) → V)
        ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) i : V) :
      V)

Tactic:
symm
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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 ≃ₗᵢ[ℝ] V
hd : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : V →ₗ[ℝ] V) → ℝ) (↑f.toLinearEquiv : V →ₗ[ℝ] V) : ℝ)
this : Nontrivial V
x : V
hx : x ≠ 0
i : Fin 2
h :
  Eq (α := V)
    (((↑(o.rotation (o.oangle x ((f : (a : V) → V) x))).toLinearEquiv : V →ₗ[ℝ] V) : (a : V) → V)
        ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : V) :
      V)
    (((↑f.toLinearEquiv : V →ₗ[ℝ] V) : (a : V) → V)
        ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : V) :
      V)
h₁ :
  Eq (α := V)
    (((↑(o.rotation (o.oangle x ((f : (a : V) → V) x))).toLinearEquiv : V →ₗ[ℝ] V) : (a : V) → V)
        ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : V) :
      V)
    (((↑f.toLinearEquiv : V →ₗ[ℝ] V) : (a : V) → V)
        ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : V) :
      V)
⊢ Eq (α := V)
    (((↑(o.rotation (o.oangle x ((f : (a : V) → V) x))).toLinearEquiv : V →ₗ[ℝ] V) : (a : V) → V)
        ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) i : V) :
      V)
    (((↑f.toLinearEquiv : V →ₗ[ℝ] V) : (a : V) → V) ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) i : V) : V)

Tactic:
fin_cases i
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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 ≃ₗᵢ[ℝ] V
hd : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : V →ₗ[ℝ] V) → ℝ) (↑f.toLinearEquiv : V →ₗ[ℝ] V) : ℝ)
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ Eq (α := V)
    (((↑(o.rotation (o.oangle x ((f : (a : V) → V) x))).toLinearEquiv : V →ₗ[ℝ] V) : (a : V) → V)
        ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : V) :
      V)
    (((↑f.toLinearEquiv : V →ₗ[ℝ] V) : (a : V) → V)
        ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : V) :
      V)

Tactic:
simp
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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 ≃ₗᵢ[ℝ] V
hd : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : V →ₗ[ℝ] V) → ℝ) (↑f.toLinearEquiv : V →ₗ[ℝ] V) : ℝ)
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ o.oangle ((o.rightAngleRotation : (a : V) → V) x) ((f : (a : V) → V) ((o.rightAngleRotation : (a : V) → V) x : V)) =
    o.oangle x ((f : (a : V) → V) x)

Tactic:
simp only [oangle, o.linearIsometryEquiv_comp_rightAngleRotation f hd,
      o.kahler_comp_rightAngleRotation]

Premises used: Orientation.oangle, Orientation.kahler_comp_rightAngleRotation, Orientation.linearIsometryEquiv_comp_rightAngleRotation
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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 ≃ₗᵢ[ℝ] V
hd : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : V →ₗ[ℝ] V) → ℝ) (↑f.toLinearEquiv : V →ₗ[ℝ] V) : ℝ)
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ o.oangle ((o.rightAngleRotation : (a : V) → V) x) ((f : (a : V) → V) ((o.rightAngleRotation : (a : V) → V) x : V)) =
    o.oangle x ((f : (a : V) → V) x)

Tactic:
have : o.oangle (J x) (f (J x)) = o.oangle x (f x) := by
    simp only [oangle, o.linearIsometryEquiv_comp_rightAngleRotation f hd,
      o.kahler_comp_rightAngleRotation]
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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 ≃ₗᵢ[ℝ] V
hd : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : V →ₗ[ℝ] V) → ℝ) (↑f.toLinearEquiv : V →ₗ[ℝ] V) : ℝ)
this_1 : Nontrivial V
x : V
hx : x ≠ 0
this :
  o.oangle ((o.rightAngleRotation : (a : V) → V) x) ((f : (a : V) → V) ((o.rightAngleRotation : (a : V) → V) x : V)) =
    o.oangle x ((f : (a : V) → V) x)
⊢ Eq (α := V)
    (((↑(o.rotation (o.oangle x ((f : (a : V) → V) x))).toLinearEquiv : V →ₗ[ℝ] V) : (a : V) → V)
        ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : V) :
      V)
    (((↑f.toLinearEquiv : V →ₗ[ℝ] V) : (a : V) → V)
        ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : V) :
      V)

Tactic:
simp [← this]
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
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)
θ : Real.Angle
f : V ≃ₗᵢ[ℝ] V'
x : V'
⊢ Eq (α := V')
    ((rotation
            (((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)
            θ :
          (a : V') → V')
        x :
      V')
    ((f : (a : V) → V') ((o.rotation θ : (a : V) → V) ((f.symm : (a : V') → V) x : V) : V) : V')

Tactic:
simp [rotation_apply, o.rightAngleRotation_map]

Premises used: Orientation.rotation_apply, Orientation.rightAngleRotation_map
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
Goal:
θ : Real.Angle
z : ℂ
simp : (↑θ.cos : ℂ) * z + (↑θ.sin : ℂ) * (I * z) = ((↑θ.cos : ℂ) + (↑θ.sin : ℂ) * I) * z
⊢ (Complex.orientation.rotation θ : (a : ℂ) → ℂ) z = (↑θ.toCircle : ℂ) * z

Tactic:
simp only [rotation_apply, Complex.rightAngleRotation, Real.Angle.coe_toCircle, real_smul]

Premises used: Complex.real_smul, Real.Angle.coe_toCircle, Orientation.rotation_apply, Complex.rightAngleRotation
-- Module: Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
Goal:
θ : Real.Angle
z : ℂ
⊢ (↑θ.cos : ℂ) * z + (↑θ.sin : ℂ) * (I * z) = ((↑θ.cos : ℂ) + (↑θ.sin : ℂ) * I) * z

Tactic:
ring