awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.OfNorm (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
hI : ¬Eq.{u_1 + 1} (α := 𝕜) I 0
x y : E
hI' : HMul.hMul (α := 𝕜) I I = -1
⊢ 4⁻¹ *
      (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖ : 𝕜)
              ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖ : 𝕜) -
            HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y‖ : 𝕜)
              ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y‖ : 𝕜) +
          HMul.hMul (β := 𝕜) (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖-x + y‖ : 𝕜))
            ((𝓚 : (a : ℝ) → 𝕜) ‖-x + y‖ : 𝕜) -
        HMul.hMul (β := 𝕜) (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖-x - y‖ : 𝕜))
          ((𝓚 : (a : ℝ) → 𝕜) ‖-x - y‖ : 𝕜)) =
    4⁻¹ *
      (-I *
        (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + y‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + y‖ : 𝕜) -
              HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x - y‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x - y‖ : 𝕜) +
            HMul.hMul (β := 𝕜)
              (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜)
                ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖ : 𝕜))
              ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖ : 𝕜) -
          HMul.hMul (β := 𝕜)
            (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y‖ : 𝕜))
            ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y‖ : 𝕜)))
have h₁ : ‖-x - y‖ = ‖x + y‖
Tactic: have h₁ : ‖-x - y‖ = ‖x + y‖ := by rw [← neg_add', norm_neg]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.OfNorm (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
hI : ¬Eq.{u_1 + 1} (α := 𝕜) I 0
x y : E
hI' : HMul.hMul (α := 𝕜) I I = -1
h₁ : ‖-x - y‖ = ‖x + y‖
⊢ ‖-x + y‖ = ‖x - y‖
have rw : ‖-x + y‖ = ‖-(y - x)‖
Tactic: rw [← neg_sub, norm_neg, sub_eq_neg_add]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.OfNorm (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
hI : ¬Eq.{u_1 + 1} (α := 𝕜) I 0
x y : E
hI' : HMul.hMul (α := 𝕜) I I = -1
h₁ : ‖-x - y‖ = ‖x + y‖
rw : ‖-x + y‖ = ‖-(y - x)‖
⊢ ‖-x + y‖ = ‖x - y‖
have rw₁ : ‖-x + y‖ = ‖y - x‖
Tactic: rw [← neg_sub, norm_neg, sub_eq_neg_add]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.OfNorm (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
hI : ¬Eq.{u_1 + 1} (α := 𝕜) I 0
x y : E
hI' : HMul.hMul (α := 𝕜) I I = -1
h₁ : ‖-x - y‖ = ‖x + y‖
rw : ‖-x + y‖ = ‖-(y - x)‖
rw₁ : ‖-x + y‖ = ‖y - x‖
⊢ ‖-x + y‖ = ‖x - y‖
have rw₂ : ‖-x + y‖ = ‖-x + y‖
Tactic: rw [← neg_sub, norm_neg, sub_eq_neg_add]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.OfNorm (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
hI : ¬Eq.{u_1 + 1} (α := 𝕜) I 0
x y : E
hI' : HMul.hMul (α := 𝕜) I I = -1
h₁ : ‖-x - y‖ = ‖x + y‖
⊢ 4⁻¹ *
      (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖ : 𝕜)
              ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖ : 𝕜) -
            HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y‖ : 𝕜)
              ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y‖ : 𝕜) +
          HMul.hMul (β := 𝕜) (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖-x + y‖ : 𝕜))
            ((𝓚 : (a : ℝ) → 𝕜) ‖-x + y‖ : 𝕜) -
        HMul.hMul (β := 𝕜) (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖-x - y‖ : 𝕜))
          ((𝓚 : (a : ℝ) → 𝕜) ‖-x - y‖ : 𝕜)) =
    4⁻¹ *
      (-I *
        (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + y‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + y‖ : 𝕜) -
              HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x - y‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x - y‖ : 𝕜) +
            HMul.hMul (β := 𝕜)
              (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜)
                ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖ : 𝕜))
              ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖ : 𝕜) -
          HMul.hMul (β := 𝕜)
            (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y‖ : 𝕜))
            ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y‖ : 𝕜)))
have h₂ : ‖-x + y‖ = ‖x - y‖
Tactic: have h₂ : ‖-x + y‖ = ‖x - y‖ := by rw [← neg_sub, norm_neg, sub_eq_neg_add]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.OfNorm (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
hI : ¬Eq.{u_1 + 1} (α := 𝕜) I 0
x y : E
hI' : HMul.hMul (α := 𝕜) I I = -1
h₁ : ‖-x - y‖ = ‖x + y‖
h₂ : ‖-x + y‖ = ‖x - y‖
⊢ 4⁻¹ *
      (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖ : 𝕜)
              ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖ : 𝕜) -
            HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y‖ : 𝕜)
              ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y‖ : 𝕜) +
          HMul.hMul (β := 𝕜) (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖-x + y‖ : 𝕜))
            ((𝓚 : (a : ℝ) → 𝕜) ‖-x + y‖ : 𝕜) -
        HMul.hMul (β := 𝕜) (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖-x - y‖ : 𝕜))
          ((𝓚 : (a : ℝ) → 𝕜) ‖-x - y‖ : 𝕜)) =
    4⁻¹ *
      (-I *
        (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + y‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + y‖ : 𝕜) -
              HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x - y‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x - y‖ : 𝕜) +
            HMul.hMul (β := 𝕜)
              (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜)
                ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖ : 𝕜))
              ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖ : 𝕜) -
          HMul.hMul (β := 𝕜)
            (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y‖ : 𝕜))
            ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y‖ : 𝕜)))
have neg : 4⁻¹ *
    (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖ : 𝕜)
            ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖ : 𝕜) -
          HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y‖ : 𝕜)
            ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y‖ : 𝕜) +
        HMul.hMul (β := 𝕜) (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x - y‖ : 𝕜))
          ((𝓚 : (a : ℝ) → 𝕜) ‖x - y‖ : 𝕜) -
      HMul.hMul (β := 𝕜) (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + y‖ : 𝕜))
        ((𝓚 : (a : ℝ) → 𝕜) ‖x + y‖ : 𝕜)) =
  4⁻¹ *
    (-I *
      (HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + y‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x + y‖ : 𝕜) -
            HMul.hMul (α := 𝕜) (β := 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x - y‖ : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖x - y‖ : 𝕜) +
          HMul.hMul (β := 𝕜)
            (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖ : 𝕜))
            ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x + y‖ : 𝕜) -
        HMul.hMul (β := 𝕜)
          (HMul.hMul (α := 𝕜) (β := 𝕜) (I : 𝕜) ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y‖ : 𝕜))
          ((𝓚 : (a : ℝ) → 𝕜) ‖HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) I x - y‖ : 𝕜)))
Tactic: rw [h₁, h₂]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.OfNorm (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
r : 𝕜
x y : E
⊢ inner_ 𝕜 (r • x) y = HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜) (inner_ 𝕜 x y)
have rw : (↑((re : (a : 𝕜) → ℝ) r) : 𝕜) * inner_ 𝕜 x y + (↑((im : (a : 𝕜) → ℝ) r) : 𝕜) * (-I * inner_ 𝕜 x y) =
  ((↑((re : (a : 𝕜) → ℝ) r) : 𝕜) + HMul.hMul (α := 𝕜) (↑((im : (a : 𝕜) → ℝ) r) : 𝕜) (-I)) * inner_ 𝕜 x y
Tactic: rw [← re_add_im r, add_smul, add_left, real_prop _ x, ← smul_smul, real_prop _ _ y, I_prop,
    map_add, map_mul, conj_ofReal, conj_ofReal, conj_I]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.OfNorm (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : InnerProductSpaceable E
inst_4 : NormedSpace ℝ E
⊢ UniformConvexSpace E
have intro : ∀ (val : InnerProductSpace ℝ E), UniformConvexSpace E
Tactic: cases nonempty_innerProductSpace ℝ E
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
inst_3 : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : Eq (α := Orientation ℝ E ι) e.toBasis.orientation f.toBasis.orientation
⊢ Eq (α := ℝ) ((e.toBasis.det : (a : ι → E) → ℝ) (⇑f : (a : ι) → E) : ℝ) (1 : ℝ)
have apply : ¬Eq (α := ℝ) ((e.toBasis.det : (a : ι → E) → ℝ) (⇑f : (a : ι) → E) : ℝ) (-1 : ℝ)
Tactic: apply (e.det_to_matrix_orthonormalBasis_real f).resolve_right
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
inst_3 : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : Eq (α := Orientation ℝ E ι) e.toBasis.orientation f.toBasis.orientation
⊢ LT.lt (α := ℝ) (0 : ℝ) ((e.toBasis.det : (a : ι → E) → ℝ) (⇑f : (a : ι) → E) : ℝ)
have h₁ : LT.lt (α := ℝ) (0 : ℝ) ((e.toBasis.det : (a : ι → E) → ℝ) (⇑f.toBasis : (a : ι) → E) : ℝ)
Tactic: rw [e.toBasis.orientation_eq_iff_det_pos] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
inst_3 : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : Eq (α := Orientation ℝ E ι) e.toBasis.orientation f.toBasis.orientation
⊢ ¬Eq (α := ℝ) ((e.toBasis.det : (a : ι → E) → ℝ) (⇑f : (a : ι) → E) : ℝ) (-1 : ℝ)
have this : LT.lt (α := ℝ) (0 : ℝ) ((e.toBasis.det : (a : ι → E) → ℝ) (⇑f : (a : ι) → E) : ℝ)
Tactic: have : 0 < e.toBasis.det f := by
    rw [e.toBasis.orientation_eq_iff_det_pos] at h
    simpa using h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
inst_3 : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : Eq (α := Orientation ℝ E ι) e.toBasis.orientation f.toBasis.orientation
this : LT.lt (α := ℝ) (0 : ℝ) ((e.toBasis.det : (a : ι → E) → ℝ) (⇑f : (a : ι) → E) : ℝ)
⊢ ¬Eq (α := ℝ) ((e.toBasis.det : (a : ι → E) → ℝ) (⇑f : (a : ι) → E) : ℝ) (-1 : ℝ)
have linarith : Eq (α := ℝ) ((e.toBasis.det : (a : ι → E) → ℝ) (⇑f : (a : ι) → E) : ℝ) (-1 : ℝ) →
  -1 + HSub.hSub (α := ℝ) (β := ℝ) (0 : ℝ) ((e.toBasis.det : (a : ι → E) → ℝ) (⇑f : (a : ι) → E) : ℝ) +
      HSub.hSub (α := ℝ) (β := ℝ) ((e.toBasis.det : (a : ι → E) → ℝ) (⇑f : (a : ι) → E) : ℝ) (-1 : ℝ) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
inst_3 : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : Ne (α := Orientation ℝ E ι) e.toBasis.orientation f.toBasis.orientation
⊢ Eq (α := ℝ) ((e.toBasis.det : (a : ι → E) → ℝ) (⇑f : (a : ι) → E) : ℝ) (-1 : ℝ)
have contrapose! : ∀ (h : Ne (α := ℝ) ((e.toBasis.det : (a : ι → E) → ℝ) (⇑f : (a : ι) → E) : ℝ) (-1 : ℝ)),
  Eq (α := Orientation ℝ E ι) e.toBasis.orientation f.toBasis.orientation
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
inst_3 : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
⊢ e.toBasis.det = f.toBasis.det ↔ Eq (α := Orientation ℝ E ι) e.toBasis.orientation f.toBasis.orientation
have mp : e.toBasis.det = f.toBasis.det → Eq (α := Orientation ℝ E ι) e.toBasis.orientation f.toBasis.orientation
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
inst_3 : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
mp : e.toBasis.det = f.toBasis.det → Eq (α := Orientation ℝ E ι) e.toBasis.orientation f.toBasis.orientation
⊢ e.toBasis.det = f.toBasis.det ↔ Eq (α := Orientation ℝ E ι) e.toBasis.orientation f.toBasis.orientation
have mpr : Eq (α := Orientation ℝ E ι) e.toBasis.orientation f.toBasis.orientation → e.toBasis.det = f.toBasis.det
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
inst_3 : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : Eq (α := Orientation ℝ E ι) e.toBasis.orientation f.toBasis.orientation
⊢ e.toBasis.det = f.toBasis.det
have mpr : HSMul.hSMul (α := ℝ) ((e.toBasis.det : (a : ι → E) → ℝ) (⇑f.toBasis : (a : ι) → E) : ℝ) f.toBasis.det = f.toBasis.det
Tactic: rw [e.toBasis.det.eq_smul_basis_det f.toBasis]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
inst_3 : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : Ne (α := Orientation ℝ E ι) e.toBasis.orientation f.toBasis.orientation
⊢ e.toBasis.det = -f.toBasis.det
have rw : HSMul.hSMul (α := ℝ) ((e.toBasis.det : (a : ι → E) → ℝ) (⇑f.toBasis : (a : ι) → E) : ℝ) f.toBasis.det = -f.toBasis.det
Tactic: rw [e.toBasis.det.eq_smul_basis_det f.toBasis]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
inst_3 : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : Ne (α := Orientation ℝ E ι) e.toBasis.orientation f.toBasis.orientation
⊢ HSMul.hSMul (α := ℝ) ((e.toBasis.det : (a : ι → E) → ℝ) (⇑f.toBasis : (a : ι) → E) : ℝ) f.toBasis.det = -f.toBasis.det
have simp : HSMul.hSMul (α := ℝ) (-1) f.toBasis.det = -f.toBasis.det
Tactic: simp [e.det_to_matrix_orthonormalBasis_of_opposite_orientation f h]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
inst_3 : DecidableEq ι
e : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
inst_4 : Nonempty ι
⊢ Orthonormal.{0, u_1, u_2} ℝ (E := E) (ι := ι) (⇑(e.toBasis.adjustToOrientation x) : (a : ι) → E)
have apply : ∀ (i : ι),
  Eq.{u_1 + 1} (α := E) ((e.toBasis.adjustToOrientation x : (a : ι) → E) i : E) ((e : (a : ι) → E) i : E) ∨
    Eq.{u_1 + 1} (α := E) ((e.toBasis.adjustToOrientation x : (a : ι) → E) i : E) (-(e : (a : ι) → E) i : E)
Tactic: apply e.orthonormal.orthonormal_of_forall_eq_or_eq_neg
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
ι : Type u_2
inst_2 : Fintype ι
inst_3 : DecidableEq ι
e : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
inst_4 : Nonempty ι
⊢ (e.adjustToOrientation x).toBasis.orientation = x
have rw : (e.toBasis.adjustToOrientation x).orientation = x
Tactic: rw [e.toBasis_adjustToOrientation]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
hn : 0 < n
h : finrank ℝ E = n
x : Orientation ℝ E (Fin n)
⊢ OrthonormalBasis (Fin n) ℝ E
have this : Nonempty (Fin n)
Tactic: haveI := Fin.pos_iff_nonempty.1 hn
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
hn : 0 < n
h : finrank ℝ E = n
x : Orientation ℝ E (Fin n)
this : Nonempty (Fin n)
⊢ OrthonormalBasis (Fin n) ℝ E
have this₁ : FiniteDimensional ℝ E
Tactic: haveI : FiniteDimensional ℝ E := .of_finrank_pos <| h.symm ▸ hn
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
hn : 0 < n
h : finrank ℝ E = n
x : Orientation ℝ E (Fin n)
⊢ (Orientation.finOrthonormalBasis hn h x).toBasis.orientation = x
have this : Nonempty (Fin n)
Tactic: haveI := Fin.pos_iff_nonempty.1 hn
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
hn : 0 < n
h : finrank ℝ E = n
x : Orientation ℝ E (Fin n)
this : Nonempty (Fin n)
⊢ (Orientation.finOrthonormalBasis hn h x).toBasis.orientation = x
have this₁ : FiniteDimensional ℝ E
Tactic: haveI : FiniteDimensional ℝ E := .of_finrank_pos <| h.symm ▸ hn
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
⊢ E [⋀^Fin n]→ₗ[ℝ] ℝ
have zero : [_i : Fact (finrank ℝ E = 0)] → (o : Orientation ℝ E (Fin 0)) → E [⋀^Fin 0]→ₗ[ℝ] ℝ
Tactic: cases n with
    | zero =>
      let opos : E [⋀^Fin 0]→ₗ[ℝ] ℝ := .constOfIsEmpty ℝ E (Fin 0) (1 : ℝ)
      exact o.eq_or_eq_neg_of_isEmpty.by_cases (fun _ => opos) fun _ => -opos
    | succ n => exact (o.finOrthonormalBasis n.succ_pos _i.out).toBasis.det
Cleared hypotheses: n, _i, o
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
zero : [_i : Fact (finrank ℝ E = 0)] → (o : Orientation ℝ E (Fin 0)) → E [⋀^Fin 0]→ₗ[ℝ] ℝ
⊢ E [⋀^Fin n]→ₗ[ℝ] ℝ
have succ : (n : ℕ) → [_i : Fact (finrank ℝ E = n + 1)] → (o : Orientation ℝ E (Fin (n + 1))) → E [⋀^Fin (n + 1)]→ₗ[ℝ] ℝ
Tactic: cases n with
    | zero =>
      let opos : E [⋀^Fin 0]→ₗ[ℝ] ℝ := .constOfIsEmpty ℝ E (Fin 0) (1 : ℝ)
      exact o.eq_or_eq_neg_of_isEmpty.by_cases (fun _ => opos) fun _ => -opos
    | succ n => exact (o.finOrthonormalBasis n.succ_pos _i.out).toBasis.det
Cleared hypotheses: n, _i, o
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
⊢ E [⋀^Fin n]→ₗ[ℝ] ℝ
have zero : [_i : Fact (finrank ℝ E = 0)] → (o : Orientation ℝ E (Fin 0)) → E [⋀^Fin 0]→ₗ[ℝ] ℝ
Tactic: classical
    cases n with
    | zero =>
      let opos : E [⋀^Fin 0]→ₗ[ℝ] ℝ := .constOfIsEmpty ℝ E (Fin 0) (1 : ℝ)
      exact o.eq_or_eq_neg_of_isEmpty.by_cases (fun _ => opos) fun _ => -opos
    | succ n => exact (o.finOrthonormalBasis n.succ_pos _i.out).toBasis.det
Cleared hypotheses: n, _i, o
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
zero : [_i : Fact (finrank ℝ E = 0)] → (o : Orientation ℝ E (Fin 0)) → E [⋀^Fin 0]→ₗ[ℝ] ℝ
⊢ E [⋀^Fin n]→ₗ[ℝ] ℝ
have succ : (n : ℕ) → [_i : Fact (finrank ℝ E = n + 1)] → (o : Orientation ℝ E (Fin (n + 1))) → E [⋀^Fin (n + 1)]→ₗ[ℝ] ℝ
Tactic: classical
    cases n with
    | zero =>
      let opos : E [⋀^Fin 0]→ₗ[ℝ] ℝ := .constOfIsEmpty ℝ E (Fin 0) (1 : ℝ)
      exact o.eq_or_eq_neg_of_isEmpty.by_cases (fun _ => opos) fun _ => -opos
    | succ n => exact (o.finOrthonormalBasis n.succ_pos _i.out).toBasis.det
Cleared hypotheses: n, _i, o
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
⊢ Eq.{u_1 + 1} (α := E [⋀^Fin 0]→ₗ[ℝ] ℝ) (volumeForm (-positiveOrientation))
    (-(AlternatingMap.constLinearEquivOfIsEmpty : (a : ℝ) → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 1)
have simp_rw : Eq.{u_1 + 1} (α := E [⋀^Fin 0]→ₗ[ℝ] ℝ)
  (Nat.casesAuxOn (motive := fun (a : ℕ) ↦ (h : 0 = a) → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 0
      (fun (h : Eq (α := ℕ) 0 0) ↦
        if hp :
            Eq.{u_1 + 1} (α := Orientation ℝ E (Fin 0))
              (-rayOfNeZero ℝ ((AlternatingMap.constLinearEquivOfIsEmpty : (a : ℝ) → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 1) sorry :
                Orientation ℝ E (Fin 0))
              (rayOfNeZero ℝ ((AlternatingMap.constLinearEquivOfIsEmpty : (a : ℝ) → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 1) sorry :
                Ray ℝ (E [⋀^Fin 0]→ₗ[ℝ] ℝ)) then
          AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1
        else -AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1)
      (fun (n : ℕ) (h : 0 = n + 1) ↦
        Eq.rec (motive := fun (x : ℕ) (x_1 : n + 1 = x) ↦
          [_i : Fact (finrank ℝ E = x)] → (o : Orientation ℝ E (Fin x)) → E [⋀^Fin x]→ₗ[ℝ] ℝ)
          (fun [Fact (finrank ℝ E = n + 1)] (o : Orientation ℝ E (Fin (n + 1))) ↦
            (Orientation.finOrthonormalBasis sorry sorry o).toBasis.det)
          sorry (-rayOfNeZero ℝ ((AlternatingMap.constLinearEquivOfIsEmpty : (a : ℝ) → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 1) sorry))
      sorry :
    E [⋀^Fin 0]→ₗ[ℝ] ℝ)
  (-(AlternatingMap.constLinearEquivOfIsEmpty : (a : ℝ) → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 1 : E [⋀^Fin 0]→ₗ[ℝ] ℝ)
Tactic: simp_rw [volumeForm, Or.by_cases, positiveOrientation]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Orientation (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
⊢ Eq.{u_1 + 1} (α := E [⋀^Fin 0]→ₗ[ℝ] ℝ)
    (Nat.casesAuxOn (motive := fun (a : ℕ) ↦ (h : 0 = a) → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 0
        (fun (h : Eq (α := ℕ) 0 0) ↦
          if hp :
              Eq.{u_1 + 1} (α := Orientation ℝ E (Fin 0))
                (-rayOfNeZero ℝ ((AlternatingMap.constLinearEquivOfIsEmpty : (a : ℝ) → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 1) ⋯ :
                  Orientation ℝ E (Fin 0))
                (rayOfNeZero ℝ ((AlternatingMap.constLinearEquivOfIsEmpty : (a : ℝ) → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 1) ⋯ :
                  Ray ℝ (E [⋀^Fin 0]→ₗ[ℝ] ℝ)) then
            AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1
          else -AlternatingMap.constOfIsEmpty ℝ E (Fin 0) 1)
        (fun (n : ℕ) (h : 0 = n + 1) ↦
          Eq.rec (motive := fun (x : ℕ) (x_1 : n + 1 = x) ↦
            [_i : Fact (finrank ℝ E = x)] → (o : Orientation ℝ E (Fin x)) → E [⋀^Fin x]→ₗ[ℝ] ℝ)
            (fun [Fact (finrank ℝ E = n + 1)] (o : Orientation ℝ E (Fin (n + 1))) ↦
              (Orientation.finOrthonormalBasis ⋯ ⋯ o).toBasis.det)
            ⋯ (-rayOfNeZero ℝ ((AlternatingMap.constLinearEquivOfIsEmpty : (a : ℝ) → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 1) ⋯))
        ⋯ :
      E [⋀^Fin 0]→ₗ[ℝ] ℝ)
    (-(AlternatingMap.constLinearEquivOfIsEmpty : (a : ℝ) → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 1 : E [⋀^Fin 0]→ₗ[ℝ] ℝ)
have hnc : ¬Eq.{u_1 + 1} (α := Orientation ℝ E (Fin 0))
    (-rayOfNeZero ℝ ((AlternatingMap.constLinearEquivOfIsEmpty : (a : ℝ) → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 1) sorry :
      Orientation ℝ E (Fin 0))
    (rayOfNeZero ℝ ((AlternatingMap.constLinearEquivOfIsEmpty : (a : ℝ) → E [⋀^Fin 0]→ₗ[ℝ] ℝ) 1) sorry :
      Ray ℝ (E [⋀^Fin 0]→ₗ[ℝ] ℝ))
Tactic: apply if_neg