awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (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
h : ‖x‖ = ‖y‖
⊢ (o.rotation (o.oangle x y) : (a : V) → V) x = y
have mpr : o.oangle ((o.rotation (o.oangle x y) : (a : V) → V) x) y = 0
Tactic: rw [o.eq_iff_oangle_eq_zero_of_norm_eq]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (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
h : ‖x‖ = ‖y‖
mpr : o.oangle ((o.rotation (o.oangle x y) : (a : V) → V) x) y = 0
⊢ (o.rotation (o.oangle x y) : (a : V) → V) x = y
have mpr₁ : norm (E := V) ((o.rotation (o.oangle x y) : (a : V) → V) x : V) = ‖y‖
Tactic: rw [o.eq_iff_oangle_eq_zero_of_norm_eq]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (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
θ : Real.Angle
⊢ o.oangle x y = θ ↔ y = HSMul.hSMul (β := V) (‖y‖ / ‖x‖) ((o.rotation θ : (a : V) → V) x : V)
have hp : 0 < ‖y‖ / ‖x‖
Tactic: have hp := div_pos (norm_pos_iff.2 hy) (norm_pos_iff.2 hx)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (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
θ : Real.Angle
hp : 0 < ‖y‖ / ‖x‖
⊢ o.oangle x y = θ ↔ y = HSMul.hSMul (β := V) (‖y‖ / ‖x‖) ((o.rotation θ : (a : V) → V) x : V)
have mp : o.oangle x y = θ → y = HSMul.hSMul (β := V) (‖y‖ / ‖x‖) ((o.rotation θ : (a : V) → V) x : V)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (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
θ : Real.Angle
hp : 0 < ‖y‖ / ‖x‖
mp : o.oangle x y = θ → y = HSMul.hSMul (β := V) (‖y‖ / ‖x‖) ((o.rotation θ : (a : V) → V) x : V)
⊢ o.oangle x y = θ ↔ y = HSMul.hSMul (β := V) (‖y‖ / ‖x‖) ((o.rotation θ : (a : V) → V) x : V)
have mpr : y = HSMul.hSMul (β := V) (‖y‖ / ‖x‖) ((o.rotation θ : (a : V) → V) x : V) → o.oangle x y = θ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (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
hp : 0 < ‖y‖ / ‖x‖
⊢ y = HSMul.hSMul (β := V) (‖y‖ / ‖x‖) ((o.rotation (o.oangle x y) : (a : V) → V) x : V)
have mp : y = (o.rotation (o.oangle x y) : (a : V) → V) ((‖y‖ / ‖x‖) • x)
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)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (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
hp : 0 < ‖y‖ / ‖x‖
mp : y = (o.rotation (o.oangle x y) : (a : V) → V) ((‖y‖ / ‖x‖) • x)
⊢ y = HSMul.hSMul (β := V) (‖y‖ / ‖x‖) ((o.rotation (o.oangle x y) : (a : V) → V) x : V)
have mp₁ : y = (o.rotation (o.oangle ((‖y‖ / ‖x‖) • x) y) : (a : V) → V) ((‖y‖ / ‖x‖) • x)
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)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (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
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)
⊢ y = HSMul.hSMul (β := V) (‖y‖ / ‖x‖) ((o.rotation (o.oangle x y) : (a : V) → V) x : V)
have mp₂ : (o.rotation (o.oangle ((‖y‖ / ‖x‖) • x) y) : (a : V) → V) ((‖y‖ / ‖x‖) • x) = y
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)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (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
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
⊢ y = HSMul.hSMul (β := V) (‖y‖ / ‖x‖) ((o.rotation (o.oangle x y) : (a : V) → V) x : V)
have mp₃ : ‖(‖y‖ / ‖x‖) • x‖ = ‖y‖
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)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (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
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‖
⊢ y = HSMul.hSMul (β := V) (‖y‖ / ‖x‖) ((o.rotation (o.oangle x y) : (a : V) → V) x : V)
have mp₄ : ‖‖y‖ / ‖x‖‖ * ‖x‖ = ‖y‖
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)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (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
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‖
⊢ y = HSMul.hSMul (β := V) (‖y‖ / ‖x‖) ((o.rotation (o.oangle x y) : (a : V) → V) x : V)
have mp₅ : ‖y‖ / ‖x‖ * ‖x‖ = ‖y‖
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)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (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
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‖
⊢ y = HSMul.hSMul (β := V) (‖y‖ / ‖x‖) ((o.rotation (o.oangle x y) : (a : V) → V) x : V)
have mp₆ : ‖y‖ = ‖y‖
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)]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (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
θ : Real.Angle
hp : 0 < ‖y‖ / ‖x‖
hye : y = HSMul.hSMul (β := V) (‖y‖ / ‖x‖) ((o.rotation θ : (a : V) → V) x : V)
⊢ o.oangle x y = θ
have mpr : o.oangle x (HSMul.hSMul (β := V) (‖y‖ / ‖x‖) ((o.rotation θ : (a : V) → V) x : V)) = θ
Tactic: rw [hye, o.oangle_smul_right_of_pos _ _ hp, o.oangle_rotation_self_right hx]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (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
θ : 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)) = θ
⊢ o.oangle x y = θ
have mpr₁ : o.oangle x ((o.rotation θ : (a : V) → V) x) = θ
Tactic: rw [hye, o.oangle_smul_right_of_pos _ _ hp, o.oangle_rotation_self_right hx]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (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
θ : 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) = θ
⊢ o.oangle x y = θ
have mpr₂ : θ = θ
Tactic: rw [hye, o.oangle_smul_right_of_pos _ _ hp, o.oangle_rotation_self_right hx]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (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
θ : Real.Angle
⊢ o.oangle x y = θ ↔ ∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) r ((o.rotation θ : (a : V) → V) x : V)
have mp : o.oangle x y = θ → ∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) r ((o.rotation θ : (a : V) → V) x : V)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (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
θ : Real.Angle
mp : o.oangle x y = θ → ∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) r ((o.rotation θ : (a : V) → V) x : V)
⊢ o.oangle x y = θ ↔ ∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) r ((o.rotation θ : (a : V) → V) x : V)
have mpr : (∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) r ((o.rotation θ : (a : V) → V) x : V)) → o.oangle x y = θ
Tactic: constructor
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (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
θ : Real.Angle
h : o.oangle x y = θ
⊢ ∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) r ((o.rotation θ : (a : V) → V) x : V)
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (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 : V
hx : x ≠ 0
θ : Real.Angle
r : ℝ
hr : 0 < r
hy : HSMul.hSMul (β := V) r ((o.rotation θ : (a : V) → V) x : V) ≠ 0
⊢ o.oangle x (HSMul.hSMul (β := V) r ((o.rotation θ : (a : V) → V) x : V)) = θ
have mpr : o.oangle x ((o.rotation θ : (a : V) → V) x) = θ
Tactic: rw [o.oangle_smul_right_of_pos _ _ hr, o.oangle_rotation_self_right hx]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (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 : 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) = θ
⊢ o.oangle x (HSMul.hSMul (β := V) r ((o.rotation θ : (a : V) → V) x : V)) = θ
have mpr₁ : θ = θ
Tactic: rw [o.oangle_smul_right_of_pos _ _ hr, o.oangle_rotation_self_right hx]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (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
θ : Real.Angle
⊢ 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)
have 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)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (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
θ : 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)
⊢ 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)
have 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)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (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
θ : 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)
have 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)
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (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
θ : 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)
⊢ 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)
have 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)
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (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
θ : 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)
have 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)
Tactic: rw [o.oangle_eq_iff_eq_norm_div_norm_smul_rotation_of_ne_zero hx hy]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (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
θ : Real.Angle
⊢ 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)
have 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)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (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
θ : 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)
⊢ 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)
have 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)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (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
θ : 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)
have 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)
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (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
θ : 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)
⊢ 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)
have 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)
Tactic: by_cases hy : y = 0
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (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
θ : 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)
have 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)
Tactic: rw [o.oangle_eq_iff_eq_pos_smul_rotation_of_ne_zero hx hy]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (hypothesis)
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) : ℝ)
⊢ ∃ (θ : Real.Angle), f = o.rotation θ
have this : Nontrivial V
Tactic: haveI : Nontrivial V := nontrivial_of_finrank_eq_succ (@Fact.out (finrank ℝ V = 2) _)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (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 ≃ₗᵢ[ℝ] V
hd : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : V →ₗ[ℝ] V) → ℝ) (↑f.toLinearEquiv : V →ₗ[ℝ] V) : ℝ)
this : Nontrivial V
⊢ ∃ (θ : Real.Angle), f = o.rotation θ
have obtain : ∀ (x : V) (hx : x ≠ 0), ∃ (θ : Real.Angle), f = o.rotation θ
Tactic: obtain ⟨x, hx⟩ : ∃ x, x ≠ (0 : V) := exists_ne (0 : V)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (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 ≃ₗᵢ[ℝ] V
hd : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : V →ₗ[ℝ] V) → ℝ) (↑f.toLinearEquiv : V →ₗ[ℝ] V) : ℝ)
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ ∃ (θ : Real.Angle), f = o.rotation θ
have h : f = o.rotation (o.oangle x ((f : (a : V) → V) x))
Tactic: use o.oangle x (f x)
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (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 ≃ₗᵢ[ℝ] V
hd : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : V →ₗ[ℝ] V) → ℝ) (↑f.toLinearEquiv : V →ₗ[ℝ] V) : ℝ)
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ f = o.rotation (o.oangle x ((f : (a : V) → V) x))
have h : f.toLinearEquiv = (o.rotation (o.oangle x ((f : (a : V) → V) x))).toLinearEquiv
Tactic: apply LinearIsometryEquiv.toLinearEquiv_injective
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (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 ≃ₗᵢ[ℝ] V
hd : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : V →ₗ[ℝ] V) → ℝ) (↑f.toLinearEquiv : V →ₗ[ℝ] V) : ℝ)
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ f.toLinearEquiv = (o.rotation (o.oangle x ((f : (a : V) → V) x))).toLinearEquiv
have h : (↑f.toLinearEquiv : V →ₗ[ℝ] V) = (↑(o.rotation (o.oangle x ((f : (a : V) → V) x))).toLinearEquiv : V →ₗ[ℝ] V)
Tactic: apply LinearEquiv.toLinearMap_injective
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (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 ≃ₗᵢ[ℝ] V
hd : LT.lt (α := ℝ) (0 : ℝ) ((LinearMap.det : (a : V →ₗ[ℝ] V) → ℝ) (↑f.toLinearEquiv : V →ₗ[ℝ] V) : ℝ)
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ (↑f.toLinearEquiv : V →ₗ[ℝ] V) = (↑(o.rotation (o.oangle x ((f : (a : V) → V) x))).toLinearEquiv : V →ₗ[ℝ] V)
have 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)
Tactic: apply (o.basisRightAngleRotation x hx).ext
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (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 ≃ₗᵢ[ℝ] 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
⊢ 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)
have 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)
Tactic: symm