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)
θ : Real.Angle
x : V
⊢ Eq (α := V) (-(o.rotation θ : (a : V) → V) x : V) ((o.rotation ((↑π : Real.Angle) + θ) : (a : V) → V) x : V)
have rw : Eq (α := V) ((o.rotation (↑π : Real.Angle) : (a : V) → V) ((o.rotation θ : (a : V) → V) x : V) : V)
  ((o.rotation ((↑π : Real.Angle) + θ) : (a : V) → V) x : V)
Tactic: rw [← o.rotation_pi_apply, rotation_rotation]
-- 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)
θ : Real.Angle
x : V
rw :
  Eq (α := V) ((o.rotation (↑π : Real.Angle) : (a : V) → V) ((o.rotation θ : (a : V) → V) x : V) : V)
    ((o.rotation ((↑π : Real.Angle) + θ) : (a : V) → V) x : V)
⊢ Eq (α := V) (-(o.rotation θ : (a : V) → V) x : V) ((o.rotation ((↑π : Real.Angle) + θ) : (a : V) → V) x : V)
have rw₁ : Eq (α := V) ((o.rotation ((↑π : Real.Angle) + θ) : (a : V) → V) x : V)
  ((o.rotation ((↑π : Real.Angle) + θ) : (a : V) → V) x : V)
Tactic: rw [← o.rotation_pi_apply, rotation_rotation]
-- 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
⊢ Eq (α := V) (-(o.rotation (↑(-π / 2) : Real.Angle) : (a : V) → V) x : V)
    ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
have rw : Eq (α := V) ((o.rotation ((↑π : Real.Angle) + (↑(-π / 2) : Real.Angle)) : (a : V) → V) x : V)
  ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
Tactic: rw [neg_rotation, ← Real.Angle.coe_add, neg_div, ← sub_eq_add_neg, sub_half]
-- 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
rw :
  Eq (α := V) ((o.rotation ((↑π : Real.Angle) + (↑(-π / 2) : Real.Angle)) : (a : V) → V) x : V)
    ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
⊢ Eq (α := V) (-(o.rotation (↑(-π / 2) : Real.Angle) : (a : V) → V) x : V)
    ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
have rw₁ : Eq (α := V) ((o.rotation (↑(π + -π / 2) : Real.Angle) : (a : V) → V) x : V)
  ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
Tactic: rw [neg_rotation, ← Real.Angle.coe_add, neg_div, ← sub_eq_add_neg, sub_half]
-- 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
rw :
  Eq (α := V) ((o.rotation ((↑π : Real.Angle) + (↑(-π / 2) : Real.Angle)) : (a : V) → V) x : V)
    ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
rw₁ :
  Eq (α := V) ((o.rotation (↑(π + -π / 2) : Real.Angle) : (a : V) → V) x : V)
    ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
⊢ Eq (α := V) (-(o.rotation (↑(-π / 2) : Real.Angle) : (a : V) → V) x : V)
    ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
have rw₂ : Eq (α := V) ((o.rotation (↑(π + -(π / 2)) : Real.Angle) : (a : V) → V) x : V)
  ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
Tactic: rw [neg_rotation, ← Real.Angle.coe_add, neg_div, ← sub_eq_add_neg, sub_half]
-- 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
rw :
  Eq (α := V) ((o.rotation ((↑π : Real.Angle) + (↑(-π / 2) : Real.Angle)) : (a : V) → V) x : V)
    ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
rw₁ :
  Eq (α := V) ((o.rotation (↑(π + -π / 2) : Real.Angle) : (a : V) → V) x : V)
    ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
rw₂ :
  Eq (α := V) ((o.rotation (↑(π + -(π / 2)) : Real.Angle) : (a : V) → V) x : V)
    ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
⊢ Eq (α := V) (-(o.rotation (↑(-π / 2) : Real.Angle) : (a : V) → V) x : V)
    ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
have rw₃ : Eq (α := V) ((o.rotation (↑(π - π / 2) : Real.Angle) : (a : V) → V) x : V)
  ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
Tactic: rw [neg_rotation, ← Real.Angle.coe_add, neg_div, ← sub_eq_add_neg, sub_half]
-- 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
rw :
  Eq (α := V) ((o.rotation ((↑π : Real.Angle) + (↑(-π / 2) : Real.Angle)) : (a : V) → V) x : V)
    ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
rw₁ :
  Eq (α := V) ((o.rotation (↑(π + -π / 2) : Real.Angle) : (a : V) → V) x : V)
    ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
rw₂ :
  Eq (α := V) ((o.rotation (↑(π + -(π / 2)) : Real.Angle) : (a : V) → V) x : V)
    ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
rw₃ :
  Eq (α := V) ((o.rotation (↑(π - π / 2) : Real.Angle) : (a : V) → V) x : V)
    ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
⊢ Eq (α := V) (-(o.rotation (↑(-π / 2) : Real.Angle) : (a : V) → V) x : V)
    ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
have rw₄ : Eq (α := V) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
  ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
Tactic: rw [neg_rotation, ← Real.Angle.coe_add, neg_div, ← sub_eq_add_neg, sub_half]
-- 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.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) ((o.rotation θ : (a : V) → V) y : V) =
    HMul.hMul (β := ℂ) (↑θ.toCircle : ℂ) ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ)
have simp : HMul.hMul (β := ℂ) (↑θ.cos : ℂ) ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ) +
    (↑θ.sin : ℂ) * HMul.hMul (β := ℂ) I ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ) =
  HMul.hMul (β := ℂ) ((↑θ.cos : ℂ) + (↑θ.sin : ℂ) * I)
    ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ)
Tactic: simp only [o.rotation_apply, map_add, map_smulₛₗ, RingHom.id_apply, real_smul,
    kahler_rightAngleRotation_right, Real.Angle.coe_toCircle]
-- 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 ((o.rotation θ : (a : V) → V) x) y = o.oangle x y - θ
have simp : (↑(HMul.hMul (β := ℂ) (↑(-θ).toCircle : ℂ)
          ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ)).arg :
    Real.Angle) =
  (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) - θ
Tactic: simp only [oangle, o.kahler_rotation_left']
-- 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
⊢ (↑(HMul.hMul (β := ℂ) (↑(-θ).toCircle : ℂ)
            ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ)).arg :
      Real.Angle) =
    (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) - θ
have rw : -θ + (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) =
  (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) - θ
Tactic: rw [Complex.arg_mul_coe_angle, Real.Angle.arg_toCircle]
-- 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
rw :
  -θ + (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) =
    (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) - θ
⊢ (↑(HMul.hMul (β := ℂ) (↑(-θ).toCircle : ℂ)
            ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ)).arg :
      Real.Angle) =
    (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) - θ
have hx₁ : (↑(-θ).toCircle : ℂ) ≠ 0
Tactic: rw [Complex.arg_mul_coe_angle, Real.Angle.arg_toCircle]
-- 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
rw :
  -θ + (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) =
    (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) - θ
hx₁ : (↑(-θ).toCircle : ℂ) ≠ 0
⊢ (↑(HMul.hMul (β := ℂ) (↑(-θ).toCircle : ℂ)
            ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ)).arg :
      Real.Angle) =
    (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) - θ
have hy₁ : Ne (α := ℂ) ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ) (0 : ℂ)
Tactic: rw [Complex.arg_mul_coe_angle, Real.Angle.arg_toCircle]
-- 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 ((o.rotation θ : (a : V) → V) y) = o.oangle x y + θ
have simp : (↑(HMul.hMul (β := ℂ) (↑θ.toCircle : ℂ) ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ)).arg :
    Real.Angle) =
  (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) + θ
Tactic: simp only [oangle, o.kahler_rotation_right]
-- 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
⊢ (↑(HMul.hMul (β := ℂ) (↑θ.toCircle : ℂ)
            ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ)).arg :
      Real.Angle) =
    (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) + θ
have rw : θ + (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) =
  (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) + θ
Tactic: rw [Complex.arg_mul_coe_angle, Real.Angle.arg_toCircle]
-- 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
rw :
  θ + (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) =
    (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) + θ
⊢ (↑(HMul.hMul (β := ℂ) (↑θ.toCircle : ℂ)
            ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ)).arg :
      Real.Angle) =
    (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) + θ
have hx₁ : (↑θ.toCircle : ℂ) ≠ 0
Tactic: rw [Complex.arg_mul_coe_angle, Real.Angle.arg_toCircle]
-- 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
rw :
  θ + (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) =
    (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) + θ
hx₁ : (↑θ.toCircle : ℂ) ≠ 0
⊢ (↑(HMul.hMul (β := ℂ) (↑θ.toCircle : ℂ)
            ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ)).arg :
      Real.Angle) =
    (↑(arg ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y)) : Real.Angle) + θ
have hy₁ : Ne (α := ℂ) ((((o.kahler : (a : V) → V →ₗ[ℝ] ℂ) x : V →ₗ[ℝ] ℂ) : (a : V) → ℂ) y : ℂ) (0 : ℂ)
Tactic: rw [Complex.arg_mul_coe_angle, Real.Angle.arg_toCircle]
-- 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
⊢ o.oangle ((o.rotation (o.oangle x y) : (a : V) → V) x) y = 0
have pos : ∀ (hx : x = 0), o.oangle ((o.rotation (o.oangle x y) : (a : V) → V) x) 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
pos : ∀ (hx : x = 0), o.oangle ((o.rotation (o.oangle x y) : (a : V) → V) x) y = 0
⊢ o.oangle ((o.rotation (o.oangle x y) : (a : V) → V) x) y = 0
have neg : ∀ (hx : ¬x = 0), o.oangle ((o.rotation (o.oangle x y) : (a : V) → V) x) 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
hx : ¬x = 0
⊢ o.oangle ((o.rotation (o.oangle x y) : (a : V) → V) x) y = 0
have pos : ∀ (hy : y = 0), o.oangle ((o.rotation (o.oangle x y) : (a : V) → V) x) 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
hx : ¬x = 0
pos : ∀ (hy : y = 0), o.oangle ((o.rotation (o.oangle x y) : (a : V) → V) x) y = 0
⊢ o.oangle ((o.rotation (o.oangle x y) : (a : V) → V) x) y = 0
have neg : ∀ (hy : ¬y = 0), o.oangle ((o.rotation (o.oangle x y) : (a : V) → V) x) 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
⊢ o.oangle y ((o.rotation (o.oangle x y) : (a : V) → V) x) = 0
have rw : -o.oangle ((o.rotation (o.oangle x y) : (a : V) → V) x) y = 0
Tactic: rw [oangle_rev]
-- 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 ((o.rotation θ : (a : V) → V) x) ((o.rotation θ : (a : V) → V) y) = o.oangle x y
have pos : ∀ (hx : x = 0), o.oangle ((o.rotation θ : (a : V) → V) x) ((o.rotation θ : (a : V) → V) y) = o.oangle x y
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 ((o.rotation θ : (a : V) → V) x) ((o.rotation θ : (a : V) → V) y) = o.oangle x y
⊢ o.oangle ((o.rotation θ : (a : V) → V) x) ((o.rotation θ : (a : V) → V) y) = o.oangle x y
have neg : ∀ (hx : ¬x = 0), o.oangle ((o.rotation θ : (a : V) → V) x) ((o.rotation θ : (a : V) → V) y) = o.oangle x y
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 ((o.rotation θ : (a : V) → V) x) ((o.rotation θ : (a : V) → V) y) = o.oangle x y
have pos : ∀ (hy : y = 0), o.oangle ((o.rotation θ : (a : V) → V) x) ((o.rotation θ : (a : V) → V) y) = o.oangle x y
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 ((o.rotation θ : (a : V) → V) x) ((o.rotation θ : (a : V) → V) y) = o.oangle x y
⊢ o.oangle ((o.rotation θ : (a : V) → V) x) ((o.rotation θ : (a : V) → V) y) = o.oangle x y
have neg : ∀ (hy : ¬y = 0), o.oangle ((o.rotation θ : (a : V) → V) x) ((o.rotation θ : (a : V) → V) y) = o.oangle x y
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
⊢ o.oangle ((o.rotation θ : (a : V) → V) x) ((o.rotation θ : (a : V) → V) y) = o.oangle x y
have pos : ∀ (hy : y = 0), o.oangle ((o.rotation θ : (a : V) → V) x) ((o.rotation θ : (a : V) → V) y) = o.oangle x y
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 ((o.rotation θ : (a : V) → V) x) ((o.rotation θ : (a : V) → V) y) = o.oangle x y
⊢ o.oangle ((o.rotation θ : (a : V) → V) x) ((o.rotation θ : (a : V) → V) y) = o.oangle x y
have neg : ∀ (hy : ¬y = 0), o.oangle ((o.rotation θ : (a : V) → V) x) ((o.rotation θ : (a : V) → V) y) = o.oangle x y
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 : V
hx : x ≠ 0
θ : Real.Angle
⊢ (o.rotation θ : (a : V) → V) x = x ↔ θ = 0
have mp : (o.rotation θ : (a : V) → V) x = x → θ = 0
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 : V
hx : x ≠ 0
θ : Real.Angle
mp : (o.rotation θ : (a : V) → V) x = x → θ = 0
⊢ (o.rotation θ : (a : V) → V) x = x ↔ θ = 0
have mpr : θ = 0 → (o.rotation θ : (a : V) → V) x = x
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 : V
hx : x ≠ 0
θ : Real.Angle
h : (o.rotation θ : (a : V) → V) x = x
⊢ θ = 0
have mp : 0 = θ
Tactic: rw [eq_comm]
-- 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
⊢ x = (o.rotation θ : (a : V) → V) x ↔ θ = 0
have rw : x = (o.rotation θ : (a : V) → V) x ↔ (o.rotation θ : (a : V) → V) x = x
Tactic: rw [← o.rotation_eq_self_iff_angle_eq_zero hx, eq_comm]
-- 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
rw : x = (o.rotation θ : (a : V) → V) x ↔ (o.rotation θ : (a : V) → V) x = x
⊢ x = (o.rotation θ : (a : V) → V) x ↔ θ = 0
have rw₁ : (o.rotation θ : (a : V) → V) x = x ↔ (o.rotation θ : (a : V) → V) x = x
Tactic: rw [← o.rotation_eq_self_iff_angle_eq_zero hx, eq_comm]
-- 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
θ : Real.Angle
⊢ (o.rotation θ : (a : V) → V) x = x ↔ x = 0 ∨ θ = 0
have pos : ∀ (h : x = 0), (o.rotation θ : (a : V) → V) x = x ↔ x = 0 ∨ θ = 0
Tactic: by_cases h : 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 : V
θ : Real.Angle
pos : ∀ (h : x = 0), (o.rotation θ : (a : V) → V) x = x ↔ x = 0 ∨ θ = 0
⊢ (o.rotation θ : (a : V) → V) x = x ↔ x = 0 ∨ θ = 0
have neg : ∀ (h : ¬x = 0), (o.rotation θ : (a : V) → V) x = x ↔ x = 0 ∨ θ = 0
Tactic: by_cases h : 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 : V
θ : Real.Angle
⊢ x = (o.rotation θ : (a : V) → V) x ↔ x = 0 ∨ θ = 0
have rw : x = (o.rotation θ : (a : V) → V) x ↔ (o.rotation θ : (a : V) → V) x = x
Tactic: rw [← rotation_eq_self_iff, eq_comm]
-- 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
θ : Real.Angle
rw : x = (o.rotation θ : (a : V) → V) x ↔ (o.rotation θ : (a : V) → V) x = x
o₁ : Orientation ℝ V (Fin 2)
⊢ x = (o.rotation θ : (a : V) → V) x ↔ x = 0 ∨ θ = 0
have rw₁ : (o.rotation θ : (a : V) → V) x = x ↔ (o.rotation θ : (a : V) → V) x = x
Tactic: rw [← rotation_eq_self_iff, eq_comm]
-- 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
⊢ (o.rotation (o.oangle x y) : (a : V) → V) x = y ↔ ‖x‖ = ‖y‖
have mp : (o.rotation (o.oangle x y) : (a : V) → V) x = y → ‖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
mp : (o.rotation (o.oangle x y) : (a : V) → V) x = y → ‖x‖ = ‖y‖
⊢ (o.rotation (o.oangle x y) : (a : V) → V) x = y ↔ ‖x‖ = ‖y‖
have mpr : ‖x‖ = ‖y‖ → (o.rotation (o.oangle x y) : (a : V) → V) 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
h : (o.rotation (o.oangle x y) : (a : V) → V) x = y
⊢ ‖x‖ = ‖y‖
have mp : ‖x‖ = norm (E := V) ((o.rotation (o.oangle x y) : (a : V) → V) x : V)
Tactic: rw [← h, LinearIsometryEquiv.norm_map]
-- 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 : (o.rotation (o.oangle x y) : (a : V) → V) x = y
mp : ‖x‖ = norm (E := V) ((o.rotation (o.oangle x y) : (a : V) → V) x : V)
⊢ ‖x‖ = ‖y‖
have mp₁ : ‖x‖ = ‖x‖
Tactic: rw [← h, LinearIsometryEquiv.norm_map]