awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) (0 : ℂ)
this : ‖x‖ * ‖y‖ = 0
h : ‖y‖ = 0
⊢ x = 0 ∨ y = 0
have inr : y = 0
Tactic: right
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) (0 : ℂ) ↔ x = 0 ∨ y = 0
have refine : x = 0 ∨ y = 0 → Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) (0 : ℂ)
Tactic: refine ⟨o.eq_zero_or_eq_zero_of_kahler_eq_zero, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
hx : x ≠ 0
hy : y ≠ 0
⊢ Ne (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) (0 : ℂ)
have apply : ¬(x = 0 ∨ y = 0)
Tactic: apply mt o.eq_zero_or_eq_zero_of_kahler_eq_zero
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ Ne (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) (0 : ℂ) ↔ x ≠ 0 ∧ y ≠ 0
have refine : Ne (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) (0 : ℂ) → x ≠ 0 ∧ y ≠ 0
Tactic: refine ⟨?_, fun h => o.kahler_ne_zero h.1 h.2⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ Ne (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) (0 : ℂ) → x ≠ 0 ∧ y ≠ 0
have contrapose : ¬(x ≠ 0 ∧ y ≠ 0) → Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) (0 : ℂ)
Tactic: contrapose
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ¬(x ≠ 0 ∧ y ≠ 0) → Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ) (0 : ℂ)
have simp : x = 0 ∨ y = 0 →
  (↑⟪x, y⟫ : ℂ) + (↑((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y) : ℂ) * Complex.I = 0
Tactic: simp only [not_and_or, Classical.not_not, kahler_apply_apply, Complex.real_smul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
Goal:
w z : ℂ
o : Orientation ℝ ℂ (Fin 2) := Complex.orientation
⊢ (((Complex.orientation.areaForm : (a : ℂ) → ℂ →ₗ[ℝ] ℝ) w : ℂ →ₗ[ℝ] ℝ) : (a : ℂ) → ℝ) z =
    (HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ) z).im
have simp : w.re * z.im - z.re * w.im = w.re * z.im + -w.im * z.re
Tactic: simp only [o, o.areaForm_to_volumeForm,
    o.volumeForm_robust Complex.orthonormalBasisOneI rfl, Basis.det_apply, Matrix.det_fin_two,
    Basis.toMatrix_apply, toBasis_orthonormalBasisOneI, Matrix.cons_val_zero, coe_basisOneI_repr,
    Matrix.cons_val_one, mul_im, conj_re, conj_im]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
Goal:
z : ℂ
⊢ (Complex.orientation.rightAngleRotation : (a : ℂ) → ℂ) z = I * z
have apply : ∀ (v : ℂ), ⟪(Complex.orientation.rightAngleRotation : (a : ℂ) → ℂ) z, v⟫ = ⟪I * z, v⟫
Tactic: apply ext_inner_right ℝ
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
Goal:
z w : ℂ
⊢ ⟪(Complex.orientation.rightAngleRotation : (a : ℂ) → ℂ) z, w⟫ = ⟪I * z, w⟫
have rw : (((Complex.orientation.areaForm : (a : ℂ) → ℂ →ₗ[ℝ] ℝ) z : ℂ →ₗ[ℝ] ℝ) : (a : ℂ) → ℝ) w = ⟪I * z, w⟫
Tactic: rw [Orientation.inner_rightAngleRotation_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
Goal:
z w : ℂ
⊢ (((Complex.orientation.areaForm : (a : ℂ) → ℂ →ₗ[ℝ] ℝ) z : ℂ →ₗ[ℝ] ℝ) : (a : ℂ) → ℝ) w = ⟪I * z, w⟫
have simp : z.re * w.im + -z.im * w.re = w.re * (-0 * z.re - -1 * -z.im) - w.im * (-0 * -z.im + -1 * z.re)
Tactic: simp only [Complex.areaForm, Complex.inner, mul_re, mul_im, conj_re, conj_im, map_mul, conj_I,
    neg_re, neg_im, I_re, I_im]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
Goal:
w z : ℂ
⊢ (↑⟪w, z⟫ : ℂ) +
      HSMul.hSMul (α := ℝ) ((((Complex.orientation.areaForm : (a : ℂ) → ℂ →ₗ[ℝ] ℝ) w : ℂ →ₗ[ℝ] ℝ) : (a : ℂ) → ℝ) z : ℝ)
        I =
    HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ)
have a : ((↑⟪w, z⟫ : ℂ) +
      HSMul.hSMul (α := ℝ) ((((Complex.orientation.areaForm : (a : ℂ) → ℂ →ₗ[ℝ] ℝ) w : ℂ →ₗ[ℝ] ℝ) : (a : ℂ) → ℝ) z : ℝ)
        I).re =
  (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ)).re
Tactic: apply Complex.ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
Goal:
w z : ℂ
a :
  ((↑⟪w, z⟫ : ℂ) +
        HSMul.hSMul (α := ℝ)
          ((((Complex.orientation.areaForm : (a : ℂ) → ℂ →ₗ[ℝ] ℝ) w : ℂ →ₗ[ℝ] ℝ) : (a : ℂ) → ℝ) z : ℝ) I).re =
    (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ)).re
⊢ (↑⟪w, z⟫ : ℂ) +
      HSMul.hSMul (α := ℝ) ((((Complex.orientation.areaForm : (a : ℂ) → ℂ →ₗ[ℝ] ℝ) w : ℂ →ₗ[ℝ] ℝ) : (a : ℂ) → ℝ) z : ℝ)
        I =
    HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ)
have a₁ : ((↑⟪w, z⟫ : ℂ) +
      HSMul.hSMul (α := ℝ) ((((Complex.orientation.areaForm : (a : ℂ) → ℂ →ₗ[ℝ] ℝ) w : ℂ →ₗ[ℝ] ℝ) : (a : ℂ) → ℝ) z : ℝ)
        I).im =
  (HMul.hMul (β := ℂ) z ((starRingEnd ℂ : (a : ℂ) → ℂ) w : ℂ)).im
Tactic: apply Complex.ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf :
  ((map (Fin 2) f.toLinearEquiv : Orientation ℝ E (Fin 2) ≃ Orientation ℝ ℂ (Fin 2)) :
        (a : Orientation ℝ E (Fin 2)) → Orientation ℝ ℂ (Fin 2))
      o =
    Complex.orientation
x y : E
⊢ (((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y =
    (HMul.hMul (α := ℂ) (β := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : E) → ℂ) x : ℂ) : ℂ)
        ((f : (a : E) → ℂ) y : ℂ)).im
have rw : Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
  ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) x : ℂ) : E) : E →ₗ[ℝ] ℝ) :
        (a : E) → ℝ)
      ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) y : ℂ) : E) :
    ℝ)
Tactic: rw [← Complex.areaForm, ← hf, areaForm_map]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf :
  ((map (Fin 2) f.toLinearEquiv : Orientation ℝ E (Fin 2) ≃ Orientation ℝ ℂ (Fin 2)) :
        (a : Orientation ℝ E (Fin 2)) → Orientation ℝ ℂ (Fin 2))
      o =
    Complex.orientation
x y : E
⊢ Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
    ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) x : ℂ) : E) : E →ₗ[ℝ] ℝ) :
          (a : E) → ℝ)
        ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) y : ℂ) : E) :
      ℝ)
have rw : Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
  ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ)
      ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) y : ℂ) : E) :
    ℝ)
Tactic: rw [LinearIsometryEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf :
  ((map (Fin 2) f.toLinearEquiv : Orientation ℝ E (Fin 2) ≃ Orientation ℝ ℂ (Fin 2)) :
        (a : Orientation ℝ E (Fin 2)) → Orientation ℝ ℂ (Fin 2))
      o =
    Complex.orientation
x y : E
⊢ Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
    ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ)
        ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) y : ℂ) : E) :
      ℝ)
have rw : Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
  ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
Tactic: rw [LinearIsometryEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf :
  ((map (Fin 2) f.toLinearEquiv : Orientation ℝ E (Fin 2) ≃ Orientation ℝ ℂ (Fin 2)) :
        (a : Orientation ℝ E (Fin 2)) → Orientation ℝ ℂ (Fin 2))
      o =
    Complex.orientation
x y : E
⊢ Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
    ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) x : ℂ) : E) : E →ₗ[ℝ] ℝ) :
          (a : E) → ℝ)
        ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) y : ℂ) : E) :
      ℝ)
have iterate : Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
  ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ)
      ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) y : ℂ) : E) :
    ℝ)
Tactic: iterate 2 rw [LinearIsometryEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf :
  ((map (Fin 2) f.toLinearEquiv : Orientation ℝ E (Fin 2) ≃ Orientation ℝ ℂ (Fin 2)) :
        (a : Orientation ℝ E (Fin 2)) → Orientation ℝ ℂ (Fin 2))
      o =
    Complex.orientation
x : E
⊢ (f : (a : E) → ℂ) ((o.rightAngleRotation : (a : E) → E) x : E) = HMul.hMul (β := ℂ) I ((f : (a : E) → ℂ) x : ℂ)
have rw : Eq (α := ℂ) ((f : (a : E) → ℂ) ((o.rightAngleRotation : (a : E) → E) x : E) : ℂ)
  ((Complex.orientation.rightAngleRotation : (a : ℂ) → ℂ) ((f : (a : E) → ℂ) x : ℂ) : ℂ)
Tactic: rw [← Complex.rightAngleRotation, ← hf, rightAngleRotation_map,
    LinearIsometryEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf :
  ((map (Fin 2) f.toLinearEquiv : Orientation ℝ E (Fin 2) ≃ Orientation ℝ ℂ (Fin 2)) :
        (a : Orientation ℝ E (Fin 2)) → Orientation ℝ ℂ (Fin 2))
      o =
    Complex.orientation
x : E
rw :
  Eq (α := ℂ) ((f : (a : E) → ℂ) ((o.rightAngleRotation : (a : E) → E) x : E) : ℂ)
    ((Complex.orientation.rightAngleRotation : (a : ℂ) → ℂ) ((f : (a : E) → ℂ) x : ℂ) : ℂ)
⊢ (f : (a : E) → ℂ) ((o.rightAngleRotation : (a : E) → E) x : E) = HMul.hMul (β := ℂ) I ((f : (a : E) → ℂ) x : ℂ)
have rw₁ : Eq (α := ℂ) ((f : (a : E) → ℂ) ((o.rightAngleRotation : (a : E) → E) x : E) : ℂ)
  ((rightAngleRotation
          (((map (Fin 2) f.toLinearEquiv : Orientation ℝ E (Fin 2) ≃ Orientation ℝ ℂ (Fin 2)) :
              (a : Orientation ℝ E (Fin 2)) → Orientation ℝ ℂ (Fin 2))
            o) :
        (a : ℂ) → ℂ)
      ((f : (a : E) → ℂ) x : ℂ) :
    ℂ)
Tactic: rw [← Complex.rightAngleRotation, ← hf, rightAngleRotation_map,
    LinearIsometryEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf :
  ((map (Fin 2) f.toLinearEquiv : Orientation ℝ E (Fin 2) ≃ Orientation ℝ ℂ (Fin 2)) :
        (a : Orientation ℝ E (Fin 2)) → Orientation ℝ ℂ (Fin 2))
      o =
    Complex.orientation
x : E
rw :
  Eq (α := ℂ) ((f : (a : E) → ℂ) ((o.rightAngleRotation : (a : E) → E) x : E) : ℂ)
    ((Complex.orientation.rightAngleRotation : (a : ℂ) → ℂ) ((f : (a : E) → ℂ) x : ℂ) : ℂ)
rw₁ :
  Eq (α := ℂ) ((f : (a : E) → ℂ) ((o.rightAngleRotation : (a : E) → E) x : E) : ℂ)
    ((rightAngleRotation
            (((map (Fin 2) f.toLinearEquiv : Orientation ℝ E (Fin 2) ≃ Orientation ℝ ℂ (Fin 2)) :
                (a : Orientation ℝ E (Fin 2)) → Orientation ℝ ℂ (Fin 2))
              o) :
          (a : ℂ) → ℂ)
        ((f : (a : E) → ℂ) x : ℂ) :
      ℂ)
⊢ (f : (a : E) → ℂ) ((o.rightAngleRotation : (a : E) → E) x : E) = HMul.hMul (β := ℂ) I ((f : (a : E) → ℂ) x : ℂ)
have rw₂ : Eq (α := ℂ) ((f : (a : E) → ℂ) ((o.rightAngleRotation : (a : E) → E) x : E) : ℂ)
  ((f : (a : E) → ℂ) ((o.rightAngleRotation : (a : E) → E) ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) x : ℂ) : E) : E) :
    ℂ)
Tactic: rw [← Complex.rightAngleRotation, ← hf, rightAngleRotation_map,
    LinearIsometryEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf :
  ((map (Fin 2) f.toLinearEquiv : Orientation ℝ E (Fin 2) ≃ Orientation ℝ ℂ (Fin 2)) :
        (a : Orientation ℝ E (Fin 2)) → Orientation ℝ ℂ (Fin 2))
      o =
    Complex.orientation
x : E
rw :
  Eq (α := ℂ) ((f : (a : E) → ℂ) ((o.rightAngleRotation : (a : E) → E) x : E) : ℂ)
    ((Complex.orientation.rightAngleRotation : (a : ℂ) → ℂ) ((f : (a : E) → ℂ) x : ℂ) : ℂ)
rw₁ :
  Eq (α := ℂ) ((f : (a : E) → ℂ) ((o.rightAngleRotation : (a : E) → E) x : E) : ℂ)
    ((rightAngleRotation
            (((map (Fin 2) f.toLinearEquiv : Orientation ℝ E (Fin 2) ≃ Orientation ℝ ℂ (Fin 2)) :
                (a : Orientation ℝ E (Fin 2)) → Orientation ℝ ℂ (Fin 2))
              o) :
          (a : ℂ) → ℂ)
        ((f : (a : E) → ℂ) x : ℂ) :
      ℂ)
rw₂ :
  Eq (α := ℂ) ((f : (a : E) → ℂ) ((o.rightAngleRotation : (a : E) → E) x : E) : ℂ)
    ((f : (a : E) → ℂ)
        ((o.rightAngleRotation : (a : E) → E) ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) x : ℂ) : E) : E) :
      ℂ)
⊢ (f : (a : E) → ℂ) ((o.rightAngleRotation : (a : E) → E) x : E) = HMul.hMul (β := ℂ) I ((f : (a : E) → ℂ) x : ℂ)
have rw₃ : Eq (α := ℂ) ((f : (a : E) → ℂ) ((o.rightAngleRotation : (a : E) → E) x : E) : ℂ)
  ((f : (a : E) → ℂ) ((o.rightAngleRotation : (a : E) → E) x : E) : ℂ)
Tactic: rw [← Complex.rightAngleRotation, ← hf, rightAngleRotation_map,
    LinearIsometryEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf :
  ((map (Fin 2) f.toLinearEquiv : Orientation ℝ E (Fin 2) ≃ Orientation ℝ ℂ (Fin 2)) :
        (a : Orientation ℝ E (Fin 2)) → Orientation ℝ ℂ (Fin 2))
      o =
    Complex.orientation
x y : E
⊢ (((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y =
    HMul.hMul (α := ℂ) (β := ℂ) ((f : (a : E) → ℂ) y : ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : E) → ℂ) x : ℂ) : ℂ)
have rw : Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)
  ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) x : ℂ) : E) : E →ₗ[ℝ] ℂ) : (a : E) → ℂ)
      ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) y : ℂ) : E) :
    ℂ)
Tactic: rw [← Complex.kahler, ← hf, kahler_map]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf :
  ((map (Fin 2) f.toLinearEquiv : Orientation ℝ E (Fin 2) ≃ Orientation ℝ ℂ (Fin 2)) :
        (a : Orientation ℝ E (Fin 2)) → Orientation ℝ ℂ (Fin 2))
      o =
    Complex.orientation
x y : E
⊢ Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)
    ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) x : ℂ) : E) : E →ₗ[ℝ] ℂ) :
          (a : E) → ℂ)
        ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) y : ℂ) : E) :
      ℂ)
have rw : Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)
  ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ)
      ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) y : ℂ) : E) :
    ℂ)
Tactic: rw [LinearIsometryEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf :
  ((map (Fin 2) f.toLinearEquiv : Orientation ℝ E (Fin 2) ≃ Orientation ℝ ℂ (Fin 2)) :
        (a : Orientation ℝ E (Fin 2)) → Orientation ℝ ℂ (Fin 2))
      o =
    Complex.orientation
x y : E
⊢ Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)
    ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ)
        ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) y : ℂ) : E) :
      ℂ)
have rw : Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)
  ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)
Tactic: rw [LinearIsometryEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TwoDim (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
inst_2 : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
f : E ≃ₗᵢ[ℝ] ℂ
hf :
  ((map (Fin 2) f.toLinearEquiv : Orientation ℝ E (Fin 2) ≃ Orientation ℝ ℂ (Fin 2)) :
        (a : Orientation ℝ E (Fin 2)) → Orientation ℝ ℂ (Fin 2))
      o =
    Complex.orientation
x y : E
⊢ Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)
    ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) x : ℂ) : E) : E →ₗ[ℝ] ℂ) :
          (a : E) → ℂ)
        ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) y : ℂ) : E) :
      ℂ)
have iterate : Eq (α := ℂ) ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ) y : ℂ)
  ((((o.kahler : (a : E) → E →ₗ[ℝ] ℂ) x : E →ₗ[ℝ] ℂ) : (a : E) → ℂ)
      ((f.symm : (a : ℂ) → E) ((f : (a : E) → ℂ) y : ℂ) : E) :
    ℂ)
Tactic: iterate 2 rw [LinearIsometryEquiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace 𝕜 F
A B : E →WOT[𝕜] F
h : ∀ (x : E) (y : F), ⟪y, (A : (a : E) → F) x⟫_𝕜 = ⟪y, (B : (a : E) → F) x⟫_𝕜
⊢ A = B
have rw : ∀ (x : E), Eq.{u_3 + 1} (α := F) ((A : (a : E) → F) x : F) ((B : (a : E) → F) x : F)
Tactic: rw [ContinuousLinearMapWOT.ext_iff]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup E
inst_2 : TopologicalSpace E
inst_3 : Module 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : InnerProductSpace 𝕜 F
inst_6 : CompleteSpace F
α : Type u_4
l : Filter α
f : α → E →WOT[𝕜] F
A : E →WOT[𝕜] F
⊢ Tendsto f l (𝓝 A) ↔
    ∀ (x : E) (y : F), Tendsto (fun (a : α) ↦ ⟪y, (f a : (a : E) → F) x⟫_𝕜) l (𝓝 ⟪y, (A : (a : E) → F) x⟫_𝕜)
have simp_rw : (∀ (x : E) (y : StrongDual 𝕜 F),
    Tendsto.{u_4, u_1} (β := 𝕜) (fun (a : α) ↦ ((y : (a : F) → 𝕜) ((f a : (a : E) → F) x : F) : 𝕜)) l
      (𝓝 ((y : (a : F) → 𝕜) ((A : (a : E) → F) x : F)) : Filter 𝕜)) ↔
  ∀ (x : E) (y : F), Tendsto (fun (a : α) ↦ ⟪y, (f a : (a : E) → F) x⟫_𝕜) l (𝓝 ⟪y, (A : (a : E) → F) x⟫_𝕜)
Tactic: simp_rw [tendsto_iff_forall_dual_apply_tendsto]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
G : ι → Type u_4
inst_1 : (i : ι) → NormedAddCommGroup (G i)
inst_2 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
f g : ↥(lp G 2)
⊢ Summable.{u_2, u_1} (α := 𝕜) fun (i : ι) ↦ ⟪(↑f : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫
have refine_1 : (ENNReal.toReal 2).HolderConjugate (ENNReal.toReal 2)
Tactic: refine .of_norm_bounded (lp.summable_mul ?_ f g) ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
G : ι → Type u_4
inst_1 : (i : ι) → NormedAddCommGroup (G i)
inst_2 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
f g : ↥(lp G 2)
refine_1 : (ENNReal.toReal 2).HolderConjugate (ENNReal.toReal 2)
⊢ Summable.{u_2, u_1} (α := 𝕜) fun (i : ι) ↦ ⟪(↑f : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫
have refine_2 : ∀ (i : ι), ‖⟪(↑f : (i : ι) → G i) i, (↑g : (i : ι) → G i) i⟫‖ ≤ ‖(↑f : (i : ι) → G i) i‖ * ‖(↑g : (i : ι) → G i) i‖
Tactic: refine .of_norm_bounded (lp.summable_mul ?_ f g) ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
G : ι → Type u_4
inst_1 : (i : ι) → NormedAddCommGroup (G i)
inst_2 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
f g : ↥(lp G 2)
⊢ (ENNReal.toReal 2).HolderConjugate (ENNReal.toReal 2)
have refine_1 : 1 < ENNReal.toReal 2 ∧ (ENNReal.toReal 2)⁻¹ + (ENNReal.toReal 2)⁻¹ = 1
Tactic: rw [Real.holderConjugate_iff]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
f : ↥(lp G 2)
⊢ HPow.hPow (β := ℕ) ‖f‖ 2 = ‖f‖ ^ ENNReal.toReal 2
have norm_cast : HPow.hPow (β := ℕ) ‖f‖ 2 = HPow.hPow (β := ℕ) ‖f‖ 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
f : ↥(lp G 2)
⊢ Eq (α := ℝ) (∑' (i : ι), ‖(↑f : (i : ι) → G i) i‖ ^ ENNReal.toReal 2)
    (∑' (i : ι), HPow.hPow (β := ℕ) ‖(↑f : (i : ι) → G i) i‖ 2)
have norm_cast : Eq (α := ℝ) (∑' (i : ι), HPow.hPow (β := ℕ) ‖(↑f : (i : ι) → G i) i‖ 2)
  (∑' (i : ι), HPow.hPow (β := ℕ) ‖(↑f : (i : ι) → G i) i‖ 2)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
f : ↥(lp G 2)
⊢ HPow.hPow (β := ℕ) ‖f‖ 2 = (re : (a : 𝕜) → ℝ) (∑' (i : ι), ⟪(↑f : (i : ι) → G i) i, (↑f : (i : ι) → G i) i⟫)
have calc_1 : 0 < ENNReal.toReal 2
Tactic: calc
        ‖f‖ ^ 2 = ‖f‖ ^ (2 : ℝ≥0∞).toReal := by norm_cast
        _ = ∑' i, ‖f i‖ ^ (2 : ℝ≥0∞).toReal := lp.norm_rpow_eq_tsum ?_ f
        _ = ∑' i, ‖f i‖ ^ (2 : ℕ) := by norm_cast
        _ = ∑' i, re ⟪f i, f i⟫ := by simp
        _ = re (∑' i, ⟪f i, f i⟫) := (RCLike.reCLM.map_tsum ?_).symm
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.l2Space (goal)
Goal:
ι : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
G : ι → Type u_4
inst_3 : (i : ι) → NormedAddCommGroup (G i)
inst_4 : (i : ι) → InnerProductSpace.{u_2, u_4} 𝕜 (G i)
f : ↥(lp G 2)
calc_1 : 0 < ENNReal.toReal 2
⊢ HPow.hPow (β := ℕ) ‖f‖ 2 = (re : (a : 𝕜) → ℝ) (∑' (i : ι), ⟪(↑f : (i : ι) → G i) i, (↑f : (i : ι) → G i) i⟫)
have calc_2 : Summable.{u_2, u_1} (α := 𝕜) fun (i : ι) ↦ ⟪(↑f : (i : ι) → G i) i, (↑f : (i : ι) → G i) i⟫
Tactic: calc
        ‖f‖ ^ 2 = ‖f‖ ^ (2 : ℝ≥0∞).toReal := by norm_cast
        _ = ∑' i, ‖f i‖ ^ (2 : ℝ≥0∞).toReal := lp.norm_rpow_eq_tsum ?_ f
        _ = ∑' i, ‖f i‖ ^ (2 : ℕ) := by norm_cast
        _ = ∑' i, re ⟪f i, f i⟫ := by simp
        _ = re (∑' i, ⟪f i, f i⟫) := (RCLike.reCLM.map_tsum ?_).symm