awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.TensorProduct (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
ι₁ : Type u_6
ι₂ : Type u_7
b₁ : Basis ι₁ 𝕜 E
b₂ : Basis ι₂ 𝕜 F
hb₁ : Orthonormal.{u_1, u_2, u_6} 𝕜 (E := E) (ι := ι₁) (⇑b₁ : (a : ι₁) → E)
hb₂ : Orthonormal.{u_1, u_3, u_7} 𝕜 (E := F) (ι := ι₂) (⇑b₂ : (a : ι₂) → F)
⊢ Orthonormal 𝕜 (E := E ⊗[𝕜] F) (ι := ι₁ × ι₂)
    (⇑(b₁.tensorProduct b₂ : Basis (ι₁ × ι₂) 𝕜 (E ⊗[𝕜] F)) : (a : ι₁ × ι₂) → E ⊗[𝕜] F)
have h : ∀ (x : ι₁ × ι₂),
  Eq (α := E ⊗[𝕜] F) (((b₁.tensorProduct b₂ : Basis (ι₁ × ι₂) 𝕜 (E ⊗[𝕜] F)) : (a : ι₁ × ι₂) → E ⊗[𝕜] F) x : E ⊗[𝕜] F)
    ((b₁ : (a : ι₁) → E) x.1 ⊗ₜ[𝕜] (b₂ : (a : ι₂) → F) x.2 : E ⊗[𝕜] F)
Tactic: convert! hb₁.tmul hb₂
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Trace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype ι
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
b : OrthonormalBasis ι 𝕜 E
⊢ Eq.{u_1 + 1} (α := 𝕜) ((trace 𝕜 E : (a : E →ₗ[𝕜] E) → 𝕜) T : 𝕜)
    (∑ i : ι, inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E) :
      𝕜)
have rw : Eq.{u_1 + 1} (α := 𝕜)
  (Matrix.trace.{u_3, u_1} (n := ι) ((toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix ι ι 𝕜) T))
  (∑ i : ι, inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E))
Tactic: rw [LinearMap.trace_eq_matrix_trace 𝕜 b.toBasis T]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Trace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype ι
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
b : OrthonormalBasis ι 𝕜 E
⊢ Eq.{u_1 + 1} (α := 𝕜)
    (Matrix.trace.{u_3, u_1} (n := ι) ((toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix ι ι 𝕜) T))
    (∑ i : ι, inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E))
have h : ∀ (a : ι),
  Matrix.diag ((toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix ι ι 𝕜) T) a =
    inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) a : E) ((T : (a : E) → E) ((b : (a : ι) → E) a : E) : E)
Tactic: apply Fintype.sum_congr
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Trace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype ι
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
b : OrthonormalBasis ι 𝕜 E
i : ι
⊢ Matrix.diag ((toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix ι ι 𝕜) T) i =
    inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E)
have h : (toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix ι ι 𝕜) T i i =
  inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E)
Tactic: rw [Matrix.diag_apply, T.toMatrix_apply, b.coe_toBasis, b.coe_toBasis_repr_apply,
    b.repr_apply_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Trace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype ι
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
b : OrthonormalBasis ι 𝕜 E
i : ι
h :
  (toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix ι ι 𝕜) T i i =
    inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E)
⊢ Matrix.diag ((toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix ι ι 𝕜) T) i =
    inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E)
have h₁ : (((b.toBasis.repr : (a : E) → ι →₀ 𝕜) ((T : (a : E) → E) ((b.toBasis : (a : ι) → E) i : E)) : ι →₀ 𝕜) : (a : ι) → 𝕜) i =
  inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E)
Tactic: rw [Matrix.diag_apply, T.toMatrix_apply, b.coe_toBasis, b.coe_toBasis_repr_apply,
    b.repr_apply_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Trace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype ι
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
b : OrthonormalBasis ι 𝕜 E
i : ι
h :
  (toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix ι ι 𝕜) T i i =
    inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E)
h₁ :
  (((b.toBasis.repr : (a : E) → ι →₀ 𝕜) ((T : (a : E) → E) ((b.toBasis : (a : ι) → E) i : E)) : ι →₀ 𝕜) : (a : ι) → 𝕜)
      i =
    inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E)
⊢ Matrix.diag ((toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix ι ι 𝕜) T) i =
    inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E)
have h₂ : (((b.toBasis.repr : (a : E) → ι →₀ 𝕜) ((T : (a : E) → E) ((b : (a : ι) → E) i : E)) : ι →₀ 𝕜) : (a : ι) → 𝕜) i =
  inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E)
Tactic: rw [Matrix.diag_apply, T.toMatrix_apply, b.coe_toBasis, b.coe_toBasis_repr_apply,
    b.repr_apply_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Trace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype ι
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
b : OrthonormalBasis ι 𝕜 E
i : ι
h :
  (toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix ι ι 𝕜) T i i =
    inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E)
h₁ :
  (((b.toBasis.repr : (a : E) → ι →₀ 𝕜) ((T : (a : E) → E) ((b.toBasis : (a : ι) → E) i : E)) : ι →₀ 𝕜) : (a : ι) → 𝕜)
      i =
    inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E)
h₂ :
  (((b.toBasis.repr : (a : E) → ι →₀ 𝕜) ((T : (a : E) → E) ((b : (a : ι) → E) i : E)) : ι →₀ 𝕜) : (a : ι) → 𝕜) i =
    inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E)
⊢ Matrix.diag ((toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix ι ι 𝕜) T) i =
    inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E)
have h₃ : WithLp.ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) ((T : (a : E) → E) ((b : (a : ι) → E) i : E))) i =
  inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E)
Tactic: rw [Matrix.diag_apply, T.toMatrix_apply, b.coe_toBasis, b.coe_toBasis_repr_apply,
    b.repr_apply_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Trace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype ι
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
b : OrthonormalBasis ι 𝕜 E
i : ι
h :
  (toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix ι ι 𝕜) T i i =
    inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E)
h₁ :
  (((b.toBasis.repr : (a : E) → ι →₀ 𝕜) ((T : (a : E) → E) ((b.toBasis : (a : ι) → E) i : E)) : ι →₀ 𝕜) : (a : ι) → 𝕜)
      i =
    inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E)
h₂ :
  (((b.toBasis.repr : (a : E) → ι →₀ 𝕜) ((T : (a : E) → E) ((b : (a : ι) → E) i : E)) : ι →₀ 𝕜) : (a : ι) → 𝕜) i =
    inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E)
h₃ :
  WithLp.ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 ι) ((T : (a : E) → E) ((b : (a : ι) → E) i : E))) i =
    inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E)
⊢ Matrix.diag ((toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix ι ι 𝕜) T) i =
    inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E)
have h₄ : inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E) =
  inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E)
Tactic: rw [Matrix.diag_apply, T.toMatrix_apply, b.coe_toBasis, b.coe_toBasis_repr_apply,
    b.repr_apply_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Trace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype ι
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
b : OrthonormalBasis ι 𝕜 E
⊢ Eq.{u_1 + 1} (α := 𝕜) ((trace 𝕜 E : (a : E →ₗ[𝕜] E) → 𝕜) T : 𝕜)
    (∑ i : ι, inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E) :
      𝕜)
have rw : Eq.{u_1 + 1} (α := 𝕜)
  (Matrix.trace.{u_3, u_1} (n := ι) ((toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix ι ι 𝕜) T))
  (∑ i : ι, inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E))
Tactic: classical
  rw [LinearMap.trace_eq_matrix_trace 𝕜 b.toBasis T]
  apply Fintype.sum_congr
  intro i
  rw [Matrix.diag_apply, T.toMatrix_apply, b.coe_toBasis, b.coe_toBasis_repr_apply,
    b.repr_apply_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Trace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst : RCLike 𝕜
inst_1 : Fintype ι
inst_2 : NormedAddCommGroup E
inst_3 : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
b : OrthonormalBasis ι 𝕜 E
rw rw₁ rw₂ :
  Eq.{u_1 + 1} (α := 𝕜)
    (Matrix.trace.{u_3, u_1} (n := ι) ((toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix ι ι 𝕜) T))
    (∑ i : ι, inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E))
⊢ Eq.{u_1 + 1} (α := 𝕜) ((trace 𝕜 E : (a : E →ₗ[𝕜] E) → 𝕜) T : 𝕜)
    (∑ i : ι, inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((T : (a : E) → E) ((b : (a : ι) → E) i : E) : E) :
      𝕜)
have h : ∀ (a : ι),
  Matrix.diag ((toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix ι ι 𝕜) T) a =
    inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) a : E) ((T : (a : E) → E) ((b : (a : ι) → E) a : E) : E)
Tactic: classical
  rw [LinearMap.trace_eq_matrix_trace 𝕜 b.toBasis T]
  apply Fintype.sum_congr
  intro i
  rw [Matrix.diag_apply, T.toMatrix_apply, b.coe_toBasis, b.coe_toBasis_repr_apply,
    b.repr_apply_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Trace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
n : ℕ
hn : Module.finrank 𝕜 E = n
T : E →ₗ[𝕜] E
hT : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) T
⊢ Eq (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) ((trace 𝕜 E : (a : E →ₗ[𝕜] E) → 𝕜) T : 𝕜) : ℝ)
    (∑ i : Fin n, hT.eigenvalues hn i : ℝ)
have rw : Eq (α := ℝ) ((RCLike.re : (a : 𝕜) → ℝ) (↑(∑ i : Fin n, hT.eigenvalues hn i) : 𝕜) : ℝ)
  (∑ i : Fin n, hT.eigenvalues hn i : ℝ)
Tactic: rw [hT.trace_eq_sum_eigenvalues]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Trace (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
x y : E
⊢ (trace 𝕜 E : (a : E →ₗ[𝕜] E) → 𝕜)
      (↑((((rankOne 𝕜 : (a : E) → E →L⋆[𝕜] E →L[𝕜] E) x : E →L⋆[𝕜] E →L[𝕜] E) : (a : E) → E →L[𝕜] E) y) : E →ₗ[𝕜] E) =
    ⟪y, x⟫_𝕜
have rw : (trace 𝕜 𝕜 : (a : 𝕜 →ₗ[𝕜] 𝕜) → 𝕜)
    ((↑(ContinuousLinearMap.toSpanSingleton 𝕜 ((((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) y : E →L[𝕜] 𝕜) : (a : E) → 𝕜) x)) :
        𝕜 →ₗ[𝕜] 𝕜) :
      𝕜 →ₗ[𝕜] 𝕜) =
  ⟪y, x⟫_𝕜
Tactic: rw [rankOne_def', ContinuousLinearMap.coe_comp, trace_comp_comm',
    ← ContinuousLinearMap.coe_comp, ContinuousLinearMap.comp_toSpanSingleton]
-- 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 : E
⊢ Eq (α := ℝ) ((((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ) (0 : ℝ)
have rw : Eq (α := ℝ) ((o.volumeForm : (a : Fin 2 → E) → ℝ) ![x, x] : ℝ) (0 : ℝ)
Tactic: rw [areaForm_to_volumeForm]
-- 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 : E
⊢ Eq (α := ℝ) ((o.volumeForm : (a : Fin 2 → E) → ℝ) ![x, x] : ℝ) (0 : ℝ)
have refine_1 : ![x, x] 0 = ![x, x] 1
Tactic: refine o.volumeForm.map_eq_zero_of_eq ![x, x] ?_ (?_ : (0 : Fin 2) ≠ 1)
-- 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 : E
refine_1 : ![x, x] 0 = ![x, x] 1
⊢ Eq (α := ℝ) ((o.volumeForm : (a : Fin 2 → E) → ℝ) ![x, x] : ℝ) (0 : ℝ)
have refine_2 : Ne (α := Fin 2) 0 1
Tactic: refine o.volumeForm.map_eq_zero_of_eq ![x, x] ?_ (?_ : (0 : Fin 2) ≠ 1)
-- 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.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
    (-(((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) y : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) x : ℝ)
have simp : Eq (α := ℝ) ((o.volumeForm : (a : Fin 2 → E) → ℝ) ![x, y] : ℝ) (-(o.volumeForm : (a : Fin 2 → E) → ℝ) ![y, x] : ℝ)
Tactic: simp only [areaForm_to_volumeForm]
-- 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.volumeForm : (a : Fin 2 → E) → ℝ) ![x, y] : ℝ) (-(o.volumeForm : (a : Fin 2 → E) → ℝ) ![y, x] : ℝ)
have h : ![x, y] = ![y, x] ∘ (⇑(Equiv.swap 0 1) : (a : Fin 2) → Fin 2)
Tactic: convert! o.volumeForm.map_swap ![y, x] (_ : (0 : Fin 2) ≠ 1)
-- 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
h : ![x, y] = ![y, x] ∘ (⇑(Equiv.swap 0 1) : (a : Fin 2) → Fin 2)
⊢ Eq (α := ℝ) ((o.volumeForm : (a : Fin 2 → E) → ℝ) ![x, y] : ℝ) (-(o.volumeForm : (a : Fin 2 → E) → ℝ) ![y, x] : ℝ)
have convert! : Ne (α := Fin 2) 0 1
Tactic: convert! o.volumeForm.map_swap ![y, x] (_ : (0 : Fin 2) ≠ 1)
-- 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, y] = ![y, x] ∘ (⇑(Equiv.swap 0 1) : (a : Fin 2) → Fin 2)
have h : ∀ (i : Fin (Nat.succ 1)), ![x, y] i = (![y, x] ∘ (⇑(Equiv.swap 0 1) : (a : Fin 2) → Fin 2)) i
Tactic: ext i
-- 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
i : Fin (Nat.succ 1)
⊢ ![x, y] i = (![y, x] ∘ (⇑(Equiv.swap 0 1) : (a : Fin 2) → Fin 2)) i
have h : ![x, y] ((fun (i : Fin (Nat.succ 1)) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 1))) =
  Function.comp (α := Fin 2) ![y, x] (⇑(Equiv.swap 0 1) : (a : Fin 2) → Fin 2) ((fun (i : Fin (Nat.succ 1)) ↦ i) ⟨0, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- 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
i : Fin (Nat.succ 1)
h :
  ![x, y] ((fun (i : Fin (Nat.succ 1)) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 1))) =
    Function.comp (α := Fin 2) ![y, x] (⇑(Equiv.swap 0 1) : (a : Fin 2) → Fin 2)
      ((fun (i : Fin (Nat.succ 1)) ↦ i) ⟨0, ⋯⟩)
⊢ ![x, y] i = (![y, x] ∘ (⇑(Equiv.swap 0 1) : (a : Fin 2) → Fin 2)) i
have h₁ : ![x, y] ((fun (i : Fin (Nat.succ 1)) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 1))) =
  Function.comp (α := Fin 2) ![y, x] (⇑(Equiv.swap 0 1) : (a : Fin 2) → Fin 2) ((fun (i : Fin (Nat.succ 1)) ↦ i) ⟨1, sorry⟩)
Tactic: fin_cases i
Cleared hypotheses: i
-- 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)
⊢ (-o).areaForm = -o.areaForm
have h : ∀ (x y : E),
  Eq (α := ℝ) (((((-o).areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
    ((((-o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
Tactic: ext x y
-- 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
h : ⟪x, y⟫ = 0
⊢ |(((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y| = ‖x‖ * ‖y‖
have rw : ∏ i : Fin 2, ‖![x, y] i‖ = ‖x‖ * ‖y‖
Tactic: rw [o.areaForm_to_volumeForm, o.abs_volumeForm_apply_of_pairwise_orthogonal]
-- 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
h : ⟪x, y⟫ = 0
rw : ∏ i : Fin 2, ‖![x, y] i‖ = ‖x‖ * ‖y‖
⊢ |(((o.areaForm : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y| = ‖x‖ * ‖y‖
have rw₁ : Pairwise fun (i j : Fin 2) ↦ ⟪![x, y] i, ![x, y] j⟫ = 0
Tactic: rw [o.areaForm_to_volumeForm, o.abs_volumeForm_apply_of_pairwise_orthogonal]
-- 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
h : ⟪x, y⟫ = 0
i j : Fin 2
hij : i ≠ j
⊢ ⟪![x, y] i, ![x, y] j⟫ = 0
have 0 : ∀ (hij : (fun (i : Fin 2) ↦ i) ⟨0, sorry⟩ ≠ j), ⟪![x, y] ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)), ![x, y] j⟫ = 0
Tactic: fin_cases i
Cleared hypotheses: i, hij
-- 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
h : ⟪x, y⟫ = 0
i j : Fin 2
hij : i ≠ j
0 : ∀ (hij : (fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩ ≠ j), ⟪![x, y] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)), ![x, y] j⟫ = 0
⊢ ⟪![x, y] i, ![x, y] j⟫ = 0
have 1 : ∀ (hij : (fun (i : Fin 2) ↦ i) ⟨1, sorry⟩ ≠ j), ⟪![x, y] ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)), ![x, y] j⟫ = 0
Tactic: fin_cases i
Cleared hypotheses: i, hij
-- 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
h : ⟪x, y⟫ = 0
j : Fin 2
hij : (fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩ ≠ j
⊢ ⟪![x, y] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)), ![x, y] j⟫ = 0
have 0 : ∀ (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)),
  ⟪![x, y] ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)), ![x, y] ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2))⟫ = 0
Tactic: fin_cases j
Cleared hypotheses: j, hij
-- 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
h : ⟪x, y⟫ = 0
j : Fin 2
hij : (fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩ ≠ j
0 :
  ∀ (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)),
    ⟪![x, y] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)), ![x, y] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))⟫ = 0
⊢ ⟪![x, y] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)), ![x, y] j⟫ = 0
have 0₁ : ∀ (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)),
  ⟪![x, y] ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2)), ![x, y] ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2))⟫ = 0
Tactic: fin_cases j
Cleared hypotheses: j, hij
-- 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
h : ⟪x, y⟫ = 0
j : Fin 2
hij : (fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩ ≠ j
⊢ ⟪![x, y] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)), ![x, y] j⟫ = 0
have 1 : ∀ (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)),
  ⟪![x, y] ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)), ![x, y] ((fun (i : Fin 2) ↦ i) (⟨0, sorry⟩ : Fin 2))⟫ = 0
Tactic: fin_cases j
Cleared hypotheses: j, hij
-- 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
h : ⟪x, y⟫ = 0
j : Fin 2
hij : (fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩ ≠ j
1 :
  ∀ (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)),
    ⟪![x, y] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)), ![x, y] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))⟫ = 0
⊢ ⟪![x, y] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)), ![x, y] j⟫ = 0
have 1₁ : ∀ (hij : Ne (α := Fin 2) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)),
  ⟪![x, y] ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2)), ![x, y] ((fun (i : Fin 2) ↦ i) (⟨1, sorry⟩ : Fin 2))⟫ = 0
Tactic: fin_cases j
Cleared hypotheses: j, hij
-- 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 : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
⊢ Eq.{u_1 + 1} (α := Fin (Nat.succ 0).succ → E) ((⇑φ.symm : (a : F) → E) ∘ ![x, y] : Fin (Nat.succ 0).succ → E)
    (![(φ.symm : (a : F) → E) x, (φ.symm : (a : F) → E) y] : Fin (Nat.succ 0).succ → E)
have h : ∀ (i : Fin (Nat.succ 0).succ),
  Eq.{u_1 + 1} (α := E) (((⇑φ.symm : (a : F) → E) ∘ ![x, y]) i : E)
    (![(φ.symm : (a : F) → E) x, (φ.symm : (a : F) → E) y] i : E)
Tactic: ext i
-- 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 : Type u_2
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
hF : Fact (finrank ℝ F = 2)
φ : E ≃ₗᵢ[ℝ] F
x y : F
i : Fin (Nat.succ 0).succ
⊢ Eq.{u_1 + 1} (α := E) (((⇑φ.symm : (a : F) → E) ∘ ![x, y]) i : E)
    (![(φ.symm : (a : F) → E) x, (φ.symm : (a : F) → E) y] i : E)
have h : Eq.{u_1 + 1} (α := E) (((⇑φ.symm : (a : F) → E) ∘ ![x, y]) ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, sorry⟩) : E)
  (Matrix.vecCons (n := Nat.succ 0) ((φ.symm : (a : F) → E) x) ![(φ.symm : (a : F) → E) y]
      ((fun (i : Fin (Nat.succ 0).succ) ↦ i) ⟨0, sorry⟩) :
    E)
Tactic: fin_cases i
Cleared hypotheses: i