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)
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)
    (((↑(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)
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) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) : V) :
    V)
  (((↑f.toLinearEquiv : V →ₗ[ℝ] V) : (a : V) → V)
      ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) : V) :
    V)
Tactic: fin_cases i
Cleared hypotheses: i
-- 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
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)
⊢ 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)
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) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) : V) :
    V)
  (((↑f.toLinearEquiv : V →ₗ[ℝ] V) : (a : V) → V)
      ((o.basisRightAngleRotation x hx : (a : Fin 2) → V) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) : V) :
    V)
Tactic: fin_cases i
Cleared hypotheses: i
-- 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) : ℝ)
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) ⟨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)
have 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)
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]
-- Lean 4 proof step from Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation (goal)
Goal:
θ : Real.Angle
z : ℂ
⊢ (Complex.orientation.rotation θ : (a : ℂ) → ℂ) z = (↑θ.toCircle : ℂ) * z
have simp : (↑θ.cos : ℂ) * z + (↑θ.sin : ℂ) * (I * z) = ((↑θ.cos : ℂ) + (↑θ.sin : ℂ) * I) * z
Tactic: simp only [rotation_apply, Complex.rightAngleRotation, Real.Angle.coe_toCircle, real_smul]
-- 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
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 : V
⊢ (f : (a : V) → ℂ) ((o.rotation θ : (a : V) → V) x : V) =
    HMul.hMul (β := ℂ) (↑θ.toCircle : ℂ) ((f : (a : V) → ℂ) x : ℂ)
have rw : Eq (α := ℂ) ((f : (a : V) → ℂ) ((o.rotation θ : (a : V) → V) x : V) : ℂ)
  ((Complex.orientation.rotation θ : (a : ℂ) → ℂ) ((f : (a : V) → ℂ) x : ℂ) : ℂ)
Tactic: rw [← Complex.rotation, ← hf, o.rotation_map, LinearIsometryEquiv.symm_apply_apply]
-- 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
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 : V
rw :
  Eq (α := ℂ) ((f : (a : V) → ℂ) ((o.rotation θ : (a : V) → V) x : V) : ℂ)
    ((Complex.orientation.rotation θ : (a : ℂ) → ℂ) ((f : (a : V) → ℂ) x : ℂ) : ℂ)
⊢ (f : (a : V) → ℂ) ((o.rotation θ : (a : V) → V) x : V) =
    HMul.hMul (β := ℂ) (↑θ.toCircle : ℂ) ((f : (a : V) → ℂ) x : ℂ)
have rw₁ : Eq (α := ℂ) ((f : (a : V) → ℂ) ((o.rotation θ : (a : V) → V) x : V) : ℂ)
  ((rotation
          (((map (Fin 2) f.toLinearEquiv : Orientation ℝ V (Fin 2) ≃ Orientation ℝ ℂ (Fin 2)) :
              (a : Orientation ℝ V (Fin 2)) → Orientation ℝ ℂ (Fin 2))
            o)
          θ :
        (a : ℂ) → ℂ)
      ((f : (a : V) → ℂ) x : ℂ) :
    ℂ)
Tactic: rw [← Complex.rotation, ← hf, o.rotation_map, LinearIsometryEquiv.symm_apply_apply]
-- 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
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 : V
rw :
  Eq (α := ℂ) ((f : (a : V) → ℂ) ((o.rotation θ : (a : V) → V) x : V) : ℂ)
    ((Complex.orientation.rotation θ : (a : ℂ) → ℂ) ((f : (a : V) → ℂ) x : ℂ) : ℂ)
rw₁ :
  Eq (α := ℂ) ((f : (a : V) → ℂ) ((o.rotation θ : (a : V) → V) x : V) : ℂ)
    ((rotation
            (((map (Fin 2) f.toLinearEquiv : Orientation ℝ V (Fin 2) ≃ Orientation ℝ ℂ (Fin 2)) :
                (a : Orientation ℝ V (Fin 2)) → Orientation ℝ ℂ (Fin 2))
              o)
            θ :
          (a : ℂ) → ℂ)
        ((f : (a : V) → ℂ) x : ℂ) :
      ℂ)
⊢ (f : (a : V) → ℂ) ((o.rotation θ : (a : V) → V) x : V) =
    HMul.hMul (β := ℂ) (↑θ.toCircle : ℂ) ((f : (a : V) → ℂ) x : ℂ)
have rw₂ : Eq (α := ℂ) ((f : (a : V) → ℂ) ((o.rotation θ : (a : V) → V) x : V) : ℂ)
  ((f : (a : V) → ℂ) ((o.rotation θ : (a : V) → V) ((f.symm : (a : ℂ) → V) ((f : (a : V) → ℂ) x : ℂ) : V) : V) : ℂ)
Tactic: rw [← Complex.rotation, ← hf, o.rotation_map, LinearIsometryEquiv.symm_apply_apply]
-- 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
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 : V
rw :
  Eq (α := ℂ) ((f : (a : V) → ℂ) ((o.rotation θ : (a : V) → V) x : V) : ℂ)
    ((Complex.orientation.rotation θ : (a : ℂ) → ℂ) ((f : (a : V) → ℂ) x : ℂ) : ℂ)
rw₁ :
  Eq (α := ℂ) ((f : (a : V) → ℂ) ((o.rotation θ : (a : V) → V) x : V) : ℂ)
    ((rotation
            (((map (Fin 2) f.toLinearEquiv : Orientation ℝ V (Fin 2) ≃ Orientation ℝ ℂ (Fin 2)) :
                (a : Orientation ℝ V (Fin 2)) → Orientation ℝ ℂ (Fin 2))
              o)
            θ :
          (a : ℂ) → ℂ)
        ((f : (a : V) → ℂ) x : ℂ) :
      ℂ)
rw₂ :
  Eq (α := ℂ) ((f : (a : V) → ℂ) ((o.rotation θ : (a : V) → V) x : V) : ℂ)
    ((f : (a : V) → ℂ) ((o.rotation θ : (a : V) → V) ((f.symm : (a : ℂ) → V) ((f : (a : V) → ℂ) x : ℂ) : V) : V) : ℂ)
⊢ (f : (a : V) → ℂ) ((o.rotation θ : (a : V) → V) x : V) =
    HMul.hMul (β := ℂ) (↑θ.toCircle : ℂ) ((f : (a : V) → ℂ) x : ℂ)
have rw₃ : Eq (α := ℂ) ((f : (a : V) → ℂ) ((o.rotation θ : (a : V) → V) x : V) : ℂ)
  ((f : (a : V) → ℂ) ((o.rotation θ : (a : V) → V) x : V) : ℂ)
Tactic: rw [← Complex.rotation, ← hf, o.rotation_map, LinearIsometryEquiv.symm_apply_apply]
-- 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
⊢ ⟪(o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x, x⟫ = 0
have rw : ⟪(o.rightAngleRotation : (a : V) → V) x, x⟫ = 0
Tactic: rw [rotation_pi_div_two, inner_rightAngleRotation_self]
-- 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 : ⟪(o.rightAngleRotation : (a : V) → V) x, x⟫ = 0
⊢ ⟪(o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x, x⟫ = 0
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [rotation_pi_div_two, inner_rightAngleRotation_self]
-- 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
⊢ ⟪x, (o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x⟫ = 0
have rw : ⟪(o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x, x⟫ = 0
Tactic: rw [real_inner_comm, inner_rotation_pi_div_two_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 : V
rw : ⟪(o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x, x⟫ = 0
⊢ ⟪x, (o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x⟫ = 0
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [real_inner_comm, inner_rotation_pi_div_two_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 : V
r : ℝ
⊢ ⟪HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V), x⟫ = 0
have rw : HMul.hMul (α := ℝ) ((starRingEnd ℝ : (a : ℝ) → ℝ) r : ℝ) ⟪(o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x, x⟫ = 0
Tactic: rw [inner_smul_left, inner_rotation_pi_div_two_left, mul_zero]
-- 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
r : ℝ
rw :
  HMul.hMul (α := ℝ) ((starRingEnd ℝ : (a : ℝ) → ℝ) r : ℝ) ⟪(o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x, x⟫ = 0
⊢ ⟪HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V), x⟫ = 0
have rw₁ : HMul.hMul (α := ℝ) (β := ℝ) ((starRingEnd ℝ : (a : ℝ) → ℝ) r : ℝ) (0 : ℝ) = 0
Tactic: rw [inner_smul_left, inner_rotation_pi_div_two_left, mul_zero]
-- 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
r : ℝ
rw :
  HMul.hMul (α := ℝ) ((starRingEnd ℝ : (a : ℝ) → ℝ) r : ℝ) ⟪(o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x, x⟫ = 0
rw₁ : HMul.hMul (α := ℝ) (β := ℝ) ((starRingEnd ℝ : (a : ℝ) → ℝ) r : ℝ) (0 : ℝ) = 0
⊢ ⟪HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V), x⟫ = 0
have rw₂ : Eq (α := ℝ) 0 0
Tactic: rw [inner_smul_left, inner_rotation_pi_div_two_left, mul_zero]
-- 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
r : ℝ
⊢ ⟪x, HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)⟫ = 0
have rw : ⟪HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V), x⟫ = 0
Tactic: rw [real_inner_comm, inner_smul_rotation_pi_div_two_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 : V
r : ℝ
rw : ⟪HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V), x⟫ = 0
⊢ ⟪x, HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)⟫ = 0
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [real_inner_comm, inner_smul_rotation_pi_div_two_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 : V
r : ℝ
⊢ ⟪(o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x, r • x⟫ = 0
have rw : r * ⟪(o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x, x⟫ = 0
Tactic: rw [inner_smul_right, inner_rotation_pi_div_two_left, mul_zero]
-- 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
r : ℝ
rw : r * ⟪(o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x, x⟫ = 0
⊢ ⟪(o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x, r • x⟫ = 0
have rw₁ : r * 0 = 0
Tactic: rw [inner_smul_right, inner_rotation_pi_div_two_left, mul_zero]
-- 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
r : ℝ
rw : r * ⟪(o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x, x⟫ = 0
rw₁ : r * 0 = 0
⊢ ⟪(o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x, r • x⟫ = 0
have rw₂ : Eq (α := ℝ) 0 0
Tactic: rw [inner_smul_right, inner_rotation_pi_div_two_left, mul_zero]
-- 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
r : ℝ
⊢ ⟪r • x, (o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x⟫ = 0
have rw : ⟪(o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x, r • x⟫ = 0
Tactic: rw [real_inner_comm, inner_rotation_pi_div_two_left_smul]
-- 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
r : ℝ
rw : ⟪(o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x, r • x⟫ = 0
⊢ ⟪r • x, (o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x⟫ = 0
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [real_inner_comm, inner_rotation_pi_div_two_left_smul]
-- 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
r₁ r₂ : ℝ
⊢ ⟪HSMul.hSMul (β := V) r₁ ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V), r₂ • x⟫ = 0
have rw : r₂ * ⟪HSMul.hSMul (β := V) r₁ ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V), x⟫ = 0
Tactic: rw [inner_smul_right, inner_smul_rotation_pi_div_two_left, mul_zero]
-- 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
r₁ r₂ : ℝ
rw : r₂ * ⟪HSMul.hSMul (β := V) r₁ ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V), x⟫ = 0
⊢ ⟪HSMul.hSMul (β := V) r₁ ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V), r₂ • x⟫ = 0
have rw₁ : r₂ * 0 = 0
Tactic: rw [inner_smul_right, inner_smul_rotation_pi_div_two_left, mul_zero]
-- 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
r₁ r₂ : ℝ
rw : r₂ * ⟪HSMul.hSMul (β := V) r₁ ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V), x⟫ = 0
rw₁ : r₂ * 0 = 0
⊢ ⟪HSMul.hSMul (β := V) r₁ ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V), r₂ • x⟫ = 0
have rw₂ : Eq (α := ℝ) 0 0
Tactic: rw [inner_smul_right, inner_smul_rotation_pi_div_two_left, mul_zero]
-- 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
r₁ r₂ : ℝ
⊢ ⟪r₂ • x, HSMul.hSMul (β := V) r₁ ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)⟫ = 0
have rw : ⟪HSMul.hSMul (β := V) r₁ ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V), r₂ • x⟫ = 0
Tactic: rw [real_inner_comm, inner_smul_rotation_pi_div_two_smul_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 : V
r₁ r₂ : ℝ
rw : ⟪HSMul.hSMul (β := V) r₁ ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V), r₂ • x⟫ = 0
⊢ ⟪r₂ • x, HSMul.hSMul (β := V) r₁ ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)⟫ = 0
have rw₁ : Eq (α := ℝ) 0 0
Tactic: rw [real_inner_comm, inner_smul_rotation_pi_div_two_smul_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
⊢ ⟪x, y⟫ = 0 ↔ x = 0 ∨ ∃ (r : ℝ), HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) = y
have pos : ∀ (H : x = 0 ∨ y = 0),
  ⟪x, y⟫ = 0 ↔ x = 0 ∨ ∃ (r : ℝ), HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) = y
Tactic: by_cases! +distrib H : x = 0 ∨ 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
pos :
  ∀ (H : x = 0 ∨ y = 0),
    ⟪x, y⟫ = 0 ↔
      x = 0 ∨ ∃ (r : ℝ), HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) = y
⊢ ⟪x, y⟫ = 0 ↔ x = 0 ∨ ∃ (r : ℝ), HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) = y
have neg : ∀ (H : x ≠ 0 ∧ y ≠ 0),
  ⟪x, y⟫ = 0 ↔ x = 0 ∨ ∃ (r : ℝ), HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) = y
Tactic: by_cases! +distrib H : x = 0 ∨ 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
H : x = 0 ∨ y = 0
⊢ ⟪x, y⟫ = 0 ↔ x = 0 ∨ ∃ (r : ℝ), HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) = y
have pos : ⟪0, y⟫ = 0 ↔
  Eq.{u_1 + 1} (α := V) 0 0 ∨
    ∃ (r : ℝ), HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) 0 : V) = y
Tactic: rcases H with (rfl | rfl)
Cleared hypotheses: x, 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 y : V
H : x = 0 ∨ y = 0
pos :
  ⟪0, y⟫ = 0 ↔
    Eq.{u_1 + 1} (α := V) 0 0 ∨
      ∃ (r : ℝ), HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) 0 : V) = y
⊢ ⟪x, y⟫ = 0 ↔ x = 0 ∨ ∃ (r : ℝ), HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) = y
have pos₁ : ⟪x, 0⟫ = 0 ↔ x = 0 ∨ ∃ (r : ℝ), HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) = 0
Tactic: rcases H with (rfl | rfl)
Cleared hypotheses: y, 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 y : V
H : x ≠ 0 ∧ y ≠ 0
⊢ ⟪x, y⟫ = 0 ↔ x = 0 ∨ ∃ (r : ℝ), HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) = y
have neg : ((∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) ∨
    ∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) (-r) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) ↔
  ∃ (r : ℝ), HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) = y
Tactic: simp only [← o.eq_zero_or_oangle_eq_iff_inner_eq_zero, H, ← neg_smul, false_or,
    o.oangle_eq_iff_eq_pos_smul_rotation_of_ne_zero H.1 H.2, ← o.neg_rotation_pi_div_two, smul_neg]
-- 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 ≠ 0 ∧ y ≠ 0
⊢ ((∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) ∨
      ∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) (-r) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) ↔
    ∃ (r : ℝ), HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) = y
have neg : ((∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) ∨
    ∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) (-r) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) →
  ∃ (r : ℝ), HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) = 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 : x ≠ 0 ∧ y ≠ 0
neg :
  ((∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) ∨
      ∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) (-r) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) →
    ∃ (r : ℝ), HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) = y
⊢ ((∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) ∨
      ∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) (-r) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) ↔
    ∃ (r : ℝ), HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) = y
have neg₁ : (∃ (r : ℝ), HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V) = y) →
  (∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) r ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)) ∨
    ∃ (r : ℝ), 0 < r ∧ y = HSMul.hSMul (β := V) (-r) ((o.rotation (↑(π / 2) : Real.Angle) : (a : V) → V) x : V)
Tactic: constructor