awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : FiniteDimensional.{u_1, u_2} 𝕜 ↥K
hK : FiniteDimensional.{u_1, u_2} 𝕜 ↥Kᗮ
e : (↥K × ↥Kᗮ) ≃ₗ[𝕜] E := K.prodEquivOfIsCompl Kᗮ ⋯
b : Basis.{0, u_1, u_2} (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜 (↥K × ↥Kᗮ) :=
  Basis.prod (finBasis 𝕜 ↥K) (finBasis 𝕜 ↥Kᗮ)
⊢ (LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) =
    HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
have this : Eq.{u_1 + 1} (α :=
  Matrix (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ))
    (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜)
  ((LinearMap.toMatrix b b :
        (a : ↥K × ↥Kᗮ →ₗ[𝕜] ↥K × ↥Kᗮ) →
          Matrix (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) 𝕜)
      ((↑e.symm : E →ₗ[𝕜] ↥K × ↥Kᗮ) ∘ₗ (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) ∘ₗ (↑e.symm.symm : ↥K × ↥Kᗮ →ₗ[𝕜] E)) :
    Matrix (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ))
      (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜)
  (Matrix.fromBlocks 1 0 0 (-1) :
    Matrix (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ))
      (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜)
Tactic: have : LinearMap.toMatrix b b (e.symm ∘ₗ K.reflection.toLinearMap ∘ₗ e.symm.symm) =
      Matrix.fromBlocks 1 0 0 (-1) := by
    ext (_ | _) (_ | _) <;>
    simp [LinearMap.toMatrix_apply, b, Matrix.one_apply, Finsupp.single_apply, e, eq_comm,
      reflection_mem_subspace_eq_self, reflection_mem_subspace_orthogonalComplement_eq_neg]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : FiniteDimensional.{u_1, u_2} 𝕜 ↥K
hK : FiniteDimensional.{u_1, u_2} 𝕜 ↥Kᗮ
e : (↥K × ↥Kᗮ) ≃ₗ[𝕜] E := K.prodEquivOfIsCompl Kᗮ ⋯
b : Basis.{0, u_1, u_2} (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜 (↥K × ↥Kᗮ) :=
  Basis.prod (finBasis 𝕜 ↥K) (finBasis 𝕜 ↥Kᗮ)
this :
  Eq.{u_1 + 1} (α :=
    Matrix (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ))
      (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜)
    ((LinearMap.toMatrix b b :
          (a : ↥K × ↥Kᗮ →ₗ[𝕜] ↥K × ↥Kᗮ) →
            Matrix (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) 𝕜)
        ((↑e.symm : E →ₗ[𝕜] ↥K × ↥Kᗮ) ∘ₗ
          (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) ∘ₗ (↑e.symm.symm : ↥K × ↥Kᗮ →ₗ[𝕜] E)) :
      Matrix (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ))
        (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜)
    (Matrix.fromBlocks 1 0 0 (-1) :
      Matrix (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ))
        (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜)
⊢ (LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) =
    HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
have pos : (LinearMap.det : (a : ↥K × ↥Kᗮ →ₗ[𝕜] ↥K × ↥Kᗮ) → 𝕜)
    ((↑e.symm : E →ₗ[𝕜] ↥K × ↥Kᗮ) ∘ₗ (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) ∘ₗ (↑e.symm.symm : ↥K × ↥Kᗮ →ₗ[𝕜] E)) =
  HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
Tactic: rw [← LinearMap.det_conj _ e.symm, ← LinearMap.det_toMatrix b, this, Matrix.det_fromBlocks_zero₂₁,
    Matrix.det_one, one_mul, Matrix.det_neg, Fintype.card_fin, Matrix.det_one, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : FiniteDimensional.{u_1, u_2} 𝕜 ↥K
hK : FiniteDimensional.{u_1, u_2} 𝕜 ↥Kᗮ
e : (↥K × ↥Kᗮ) ≃ₗ[𝕜] E := K.prodEquivOfIsCompl Kᗮ ⋯
b : Basis.{0, u_1, u_2} (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜 (↥K × ↥Kᗮ) :=
  Basis.prod (finBasis 𝕜 ↥K) (finBasis 𝕜 ↥Kᗮ)
this :
  Eq.{u_1 + 1} (α :=
    Matrix (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ))
      (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜)
    ((LinearMap.toMatrix b b :
          (a : ↥K × ↥Kᗮ →ₗ[𝕜] ↥K × ↥Kᗮ) →
            Matrix (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) 𝕜)
        ((↑e.symm : E →ₗ[𝕜] ↥K × ↥Kᗮ) ∘ₗ
          (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) ∘ₗ (↑e.symm.symm : ↥K × ↥Kᗮ →ₗ[𝕜] E)) :
      Matrix (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ))
        (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜)
    (Matrix.fromBlocks 1 0 0 (-1) :
      Matrix (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ))
        (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜)
pos :
  (LinearMap.det : (a : ↥K × ↥Kᗮ →ₗ[𝕜] ↥K × ↥Kᗮ) → 𝕜)
      ((↑e.symm : E →ₗ[𝕜] ↥K × ↥Kᗮ) ∘ₗ (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) ∘ₗ (↑e.symm.symm : ↥K × ↥Kᗮ →ₗ[𝕜] E)) =
    HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
⊢ (LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) =
    HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
have pos₁ : Matrix.det (n := Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ))
    ((LinearMap.toMatrix b b :
        (a : ↥K × ↥Kᗮ →ₗ[𝕜] ↥K × ↥Kᗮ) →
          Matrix (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) 𝕜)
      ((↑e.symm : E →ₗ[𝕜] ↥K × ↥Kᗮ) ∘ₗ
        (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) ∘ₗ (↑e.symm.symm : ↥K × ↥Kᗮ →ₗ[𝕜] E))) =
  HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
Tactic: rw [← LinearMap.det_conj _ e.symm, ← LinearMap.det_toMatrix b, this, Matrix.det_fromBlocks_zero₂₁,
    Matrix.det_one, one_mul, Matrix.det_neg, Fintype.card_fin, Matrix.det_one, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : FiniteDimensional.{u_1, u_2} 𝕜 ↥K
hK : FiniteDimensional.{u_1, u_2} 𝕜 ↥Kᗮ
e : (↥K × ↥Kᗮ) ≃ₗ[𝕜] E := K.prodEquivOfIsCompl Kᗮ ⋯
b : Basis.{0, u_1, u_2} (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜 (↥K × ↥Kᗮ) :=
  Basis.prod (finBasis 𝕜 ↥K) (finBasis 𝕜 ↥Kᗮ)
this :
  Eq.{u_1 + 1} (α :=
    Matrix (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ))
      (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜)
    ((LinearMap.toMatrix b b :
          (a : ↥K × ↥Kᗮ →ₗ[𝕜] ↥K × ↥Kᗮ) →
            Matrix (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) 𝕜)
        ((↑e.symm : E →ₗ[𝕜] ↥K × ↥Kᗮ) ∘ₗ
          (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) ∘ₗ (↑e.symm.symm : ↥K × ↥Kᗮ →ₗ[𝕜] E)) :
      Matrix (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ))
        (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜)
    (Matrix.fromBlocks 1 0 0 (-1) :
      Matrix (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ))
        (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜)
pos :
  (LinearMap.det : (a : ↥K × ↥Kᗮ →ₗ[𝕜] ↥K × ↥Kᗮ) → 𝕜)
      ((↑e.symm : E →ₗ[𝕜] ↥K × ↥Kᗮ) ∘ₗ (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) ∘ₗ (↑e.symm.symm : ↥K × ↥Kᗮ →ₗ[𝕜] E)) =
    HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
pos₁ :
  Matrix.det (n := Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ))
      ((LinearMap.toMatrix b b :
          (a : ↥K × ↥Kᗮ →ₗ[𝕜] ↥K × ↥Kᗮ) →
            Matrix (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) 𝕜)
        ((↑e.symm : E →ₗ[𝕜] ↥K × ↥Kᗮ) ∘ₗ
          (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) ∘ₗ (↑e.symm.symm : ↥K × ↥Kᗮ →ₗ[𝕜] E))) =
    HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
⊢ (LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) =
    HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
have pos₂ : Matrix.det (n := Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) (Matrix.fromBlocks 1 0 0 (-1)) =
  HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
Tactic: rw [← LinearMap.det_conj _ e.symm, ← LinearMap.det_toMatrix b, this, Matrix.det_fromBlocks_zero₂₁,
    Matrix.det_one, one_mul, Matrix.det_neg, Fintype.card_fin, Matrix.det_one, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : FiniteDimensional.{u_1, u_2} 𝕜 ↥K
hK : FiniteDimensional.{u_1, u_2} 𝕜 ↥Kᗮ
e : (↥K × ↥Kᗮ) ≃ₗ[𝕜] E := K.prodEquivOfIsCompl Kᗮ ⋯
b : Basis.{0, u_1, u_2} (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜 (↥K × ↥Kᗮ) :=
  Basis.prod (finBasis 𝕜 ↥K) (finBasis 𝕜 ↥Kᗮ)
this :
  Eq.{u_1 + 1} (α :=
    Matrix (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ))
      (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜)
    ((LinearMap.toMatrix b b :
          (a : ↥K × ↥Kᗮ →ₗ[𝕜] ↥K × ↥Kᗮ) →
            Matrix (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) 𝕜)
        ((↑e.symm : E →ₗ[𝕜] ↥K × ↥Kᗮ) ∘ₗ
          (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) ∘ₗ (↑e.symm.symm : ↥K × ↥Kᗮ →ₗ[𝕜] E)) :
      Matrix (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ))
        (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜)
    (Matrix.fromBlocks 1 0 0 (-1) :
      Matrix (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ))
        (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜)
pos :
  (LinearMap.det : (a : ↥K × ↥Kᗮ →ₗ[𝕜] ↥K × ↥Kᗮ) → 𝕜)
      ((↑e.symm : E →ₗ[𝕜] ↥K × ↥Kᗮ) ∘ₗ (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) ∘ₗ (↑e.symm.symm : ↥K × ↥Kᗮ →ₗ[𝕜] E)) =
    HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
pos₁ :
  Matrix.det (n := Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ))
      ((LinearMap.toMatrix b b :
          (a : ↥K × ↥Kᗮ →ₗ[𝕜] ↥K × ↥Kᗮ) →
            Matrix (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) 𝕜)
        ((↑e.symm : E →ₗ[𝕜] ↥K × ↥Kᗮ) ∘ₗ
          (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) ∘ₗ (↑e.symm.symm : ↥K × ↥Kᗮ →ₗ[𝕜] E))) =
    HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
pos₂ :
  Matrix.det (n := Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) (Matrix.fromBlocks 1 0 0 (-1)) =
    HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
⊢ (LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) =
    HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
have pos₃ : HMul.hMul (α := 𝕜) (Matrix.det (n := Fin (finrank.{u_1, u_2} 𝕜 ↥K)) 1)
    (Matrix.det (n := Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) (-1)) =
  HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
Tactic: rw [← LinearMap.det_conj _ e.symm, ← LinearMap.det_toMatrix b, this, Matrix.det_fromBlocks_zero₂₁,
    Matrix.det_one, one_mul, Matrix.det_neg, Fintype.card_fin, Matrix.det_one, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : FiniteDimensional.{u_1, u_2} 𝕜 ↥K
hK : FiniteDimensional.{u_1, u_2} 𝕜 ↥Kᗮ
e : (↥K × ↥Kᗮ) ≃ₗ[𝕜] E := K.prodEquivOfIsCompl Kᗮ ⋯
b : Basis.{0, u_1, u_2} (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜 (↥K × ↥Kᗮ) :=
  Basis.prod (finBasis 𝕜 ↥K) (finBasis 𝕜 ↥Kᗮ)
this :
  Eq.{u_1 + 1} (α :=
    Matrix (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ))
      (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜)
    ((LinearMap.toMatrix b b :
          (a : ↥K × ↥Kᗮ →ₗ[𝕜] ↥K × ↥Kᗮ) →
            Matrix (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) 𝕜)
        ((↑e.symm : E →ₗ[𝕜] ↥K × ↥Kᗮ) ∘ₗ
          (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) ∘ₗ (↑e.symm.symm : ↥K × ↥Kᗮ →ₗ[𝕜] E)) :
      Matrix (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ))
        (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜)
    (Matrix.fromBlocks 1 0 0 (-1) :
      Matrix (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ))
        (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜)
pos :
  (LinearMap.det : (a : ↥K × ↥Kᗮ →ₗ[𝕜] ↥K × ↥Kᗮ) → 𝕜)
      ((↑e.symm : E →ₗ[𝕜] ↥K × ↥Kᗮ) ∘ₗ (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) ∘ₗ (↑e.symm.symm : ↥K × ↥Kᗮ →ₗ[𝕜] E)) =
    HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
pos₁ :
  Matrix.det (n := Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ))
      ((LinearMap.toMatrix b b :
          (a : ↥K × ↥Kᗮ →ₗ[𝕜] ↥K × ↥Kᗮ) →
            Matrix (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) 𝕜)
        ((↑e.symm : E →ₗ[𝕜] ↥K × ↥Kᗮ) ∘ₗ
          (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) ∘ₗ (↑e.symm.symm : ↥K × ↥Kᗮ →ₗ[𝕜] E))) =
    HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
pos₂ :
  Matrix.det (n := Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) (Matrix.fromBlocks 1 0 0 (-1)) =
    HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
pos₃ :
  HMul.hMul (α := 𝕜) (Matrix.det (n := Fin (finrank.{u_1, u_2} 𝕜 ↥K)) 1)
      (Matrix.det (n := Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) (-1)) =
    HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
⊢ (LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) =
    HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
have pos₄ : HMul.hMul (α := 𝕜) 1 (Matrix.det (n := Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) (-1)) =
  HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
Tactic: rw [← LinearMap.det_conj _ e.symm, ← LinearMap.det_toMatrix b, this, Matrix.det_fromBlocks_zero₂₁,
    Matrix.det_one, one_mul, Matrix.det_neg, Fintype.card_fin, Matrix.det_one, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : FiniteDimensional.{u_1, u_2} 𝕜 ↥K
hK : FiniteDimensional.{u_1, u_2} 𝕜 ↥Kᗮ
e : (↥K × ↥Kᗮ) ≃ₗ[𝕜] E := K.prodEquivOfIsCompl Kᗮ ⋯
b : Basis.{0, u_1, u_2} (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜 (↥K × ↥Kᗮ) :=
  Basis.prod (finBasis 𝕜 ↥K) (finBasis 𝕜 ↥Kᗮ)
this :
  Eq.{u_1 + 1} (α :=
    Matrix (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ))
      (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜)
    ((LinearMap.toMatrix b b :
          (a : ↥K × ↥Kᗮ →ₗ[𝕜] ↥K × ↥Kᗮ) →
            Matrix (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) 𝕜)
        ((↑e.symm : E →ₗ[𝕜] ↥K × ↥Kᗮ) ∘ₗ
          (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) ∘ₗ (↑e.symm.symm : ↥K × ↥Kᗮ →ₗ[𝕜] E)) :
      Matrix (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ))
        (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜)
    (Matrix.fromBlocks 1 0 0 (-1) :
      Matrix (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ))
        (Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 𝕜)
pos :
  (LinearMap.det : (a : ↥K × ↥Kᗮ →ₗ[𝕜] ↥K × ↥Kᗮ) → 𝕜)
      ((↑e.symm : E →ₗ[𝕜] ↥K × ↥Kᗮ) ∘ₗ (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) ∘ₗ (↑e.symm.symm : ↥K × ↥Kᗮ →ₗ[𝕜] E)) =
    HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
pos₁ :
  Matrix.det (n := Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ))
      ((LinearMap.toMatrix b b :
          (a : ↥K × ↥Kᗮ →ₗ[𝕜] ↥K × ↥Kᗮ) →
            Matrix (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) (Fin (finrank 𝕜 ↥K) ⊕ Fin (finrank 𝕜 ↥Kᗮ)) 𝕜)
        ((↑e.symm : E →ₗ[𝕜] ↥K × ↥Kᗮ) ∘ₗ
          (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) ∘ₗ (↑e.symm.symm : ↥K × ↥Kᗮ →ₗ[𝕜] E))) =
    HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
pos₂ :
  Matrix.det (n := Fin (finrank.{u_1, u_2} 𝕜 ↥K) ⊕ Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) (Matrix.fromBlocks 1 0 0 (-1)) =
    HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
pos₃ :
  HMul.hMul (α := 𝕜) (Matrix.det (n := Fin (finrank.{u_1, u_2} 𝕜 ↥K)) 1)
      (Matrix.det (n := Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) (-1)) =
    HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
pos₄ :
  HMul.hMul (α := 𝕜) 1 (Matrix.det (n := Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) (-1)) =
    HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
⊢ (LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) =
    HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
have pos₅ : Matrix.det (n := Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) (-1) = HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
Tactic: rw [← LinearMap.det_conj _ e.symm, ← LinearMap.det_toMatrix b, this, Matrix.det_fromBlocks_zero₂₁,
    Matrix.det_one, one_mul, Matrix.det_neg, Fintype.card_fin, Matrix.det_one, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : FiniteDimensional.{u_1, u_2} 𝕜 ↥K
⊢ (LinearEquiv.det : (a : E ≃ₗ[𝕜] E) → 𝕜ˣ) K.reflection.toLinearEquiv =
    HPow.hPow (α := 𝕜ˣ) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
have huv : (↑((LinearEquiv.det : (a : E ≃ₗ[𝕜] E) → 𝕜ˣ) K.reflection.toLinearEquiv) : 𝕜) =
  (↑(HPow.hPow (α := 𝕜ˣ) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) : 𝕜)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : FiniteDimensional.{u_1, u_2} 𝕜 ↥K
⊢ (↑((LinearEquiv.det : (a : E ≃ₗ[𝕜] E) → 𝕜ˣ) K.reflection.toLinearEquiv) : 𝕜) =
    (↑(HPow.hPow (α := 𝕜ˣ) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) : 𝕜)
have huv : (LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) =
  HPow.hPow (α := 𝕜) (↑(-1) : 𝕜) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
Tactic: rw [LinearEquiv.coe_det, Units.val_pow_eq_pow_val]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
inst_3 : FiniteDimensional.{u_1, u_2} 𝕜 ↥K₂
h : K₁ ≤ K₂
⊢ finrank.{u_1, u_2} 𝕜 ↥K₁ + finrank.{u_1, u_2} 𝕜 ↥(K₁ᗮ ⊓ K₂) = finrank.{u_1, u_2} 𝕜 ↥K₂
have this : FiniteDimensional.{u_1, u_2} 𝕜 ↥K₁
Tactic: haveI : FiniteDimensional 𝕜 K₁ := Submodule.finiteDimensional_of_le h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
inst_3 : FiniteDimensional.{u_1, u_2} 𝕜 ↥K₂
h : K₁ ≤ K₂
this : FiniteDimensional.{u_1, u_2} 𝕜 ↥K₁
⊢ finrank.{u_1, u_2} 𝕜 ↥K₁ + finrank.{u_1, u_2} 𝕜 ↥(K₁ᗮ ⊓ K₂) = finrank.{u_1, u_2} 𝕜 ↥K₂
have hd : finrank.{u_1, u_2} 𝕜 ↥(K₁ ⊔ K₁ᗮ ⊓ K₂) + finrank.{u_1, u_2} 𝕜 ↥(K₁ ⊓ (K₁ᗮ ⊓ K₂)) =
  finrank.{u_1, u_2} 𝕜 ↥K₁ + finrank.{u_1, u_2} 𝕜 ↥(K₁ᗮ ⊓ K₂)
Tactic: have hd := Submodule.finrank_sup_add_finrank_inf_eq K₁ (K₁ᗮ ⊓ K₂)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
inst_3 : FiniteDimensional.{u_1, u_2} 𝕜 ↥K₂
h : K₁ ≤ K₂
this : FiniteDimensional.{u_1, u_2} 𝕜 ↥K₁
hd :
  finrank.{u_1, u_2} 𝕜 ↥(K₁ ⊔ K₁ᗮ ⊓ K₂) + finrank.{u_1, u_2} 𝕜 ↥(K₁ ⊓ (K₁ᗮ ⊓ K₂)) =
    finrank.{u_1, u_2} 𝕜 ↥K₁ + finrank.{u_1, u_2} 𝕜 ↥(K₁ᗮ ⊓ K₂)
⊢ finrank.{u_1, u_2} 𝕜 ↥K₁ + finrank.{u_1, u_2} 𝕜 ↥(K₁ᗮ ⊓ K₂) = finrank.{u_1, u_2} 𝕜 ↥K₂
have hd₁ : finrank.{u_1, u_2} 𝕜 ↥K₂ + 0 = finrank.{u_1, u_2} 𝕜 ↥K₁ + finrank.{u_1, u_2} 𝕜 ↥(K₁ᗮ ⊓ K₂)
Tactic: rw [← inf_assoc, (Submodule.orthogonal_disjoint K₁).eq_bot, bot_inf_eq, finrank_bot,
    Submodule.sup_orthogonal_inf_of_hasOrthogonalProjection h] at hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
inst_3 : FiniteDimensional.{u_1, u_2} 𝕜 ↥K₂
h : K₁ ≤ K₂
this : FiniteDimensional.{u_1, u_2} 𝕜 ↥K₁
hd : finrank.{u_1, u_2} 𝕜 ↥K₂ + 0 = finrank.{u_1, u_2} 𝕜 ↥K₁ + finrank.{u_1, u_2} 𝕜 ↥(K₁ᗮ ⊓ K₂)
⊢ finrank.{u_1, u_2} 𝕜 ↥K₁ + finrank.{u_1, u_2} 𝕜 ↥(K₁ᗮ ⊓ K₂) = finrank.{u_1, u_2} 𝕜 ↥K₂
have hd₁ : finrank.{u_1, u_2} 𝕜 ↥K₂ = finrank.{u_1, u_2} 𝕜 ↥K₁ + finrank.{u_1, u_2} 𝕜 ↥(K₁ᗮ ⊓ K₂)
Tactic: rw [add_zero] at hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K₁ K₂ : Submodule 𝕜 E
inst_3 : FiniteDimensional.{u_1, u_2} 𝕜 ↥K₂
h : K₁ ≤ K₂
n : ℕ
h_dim : finrank.{u_1, u_2} 𝕜 ↥K₁ + n = finrank.{u_1, u_2} 𝕜 ↥K₂
⊢ finrank.{u_1, u_2} 𝕜 ↥(K₁ᗮ ⊓ K₂) = n
have rw : finrank.{u_1, u_2} 𝕜 ↥K₁ + finrank.{u_1, u_2} 𝕜 ↥(K₁ᗮ ⊓ K₂) = finrank.{u_1, u_2} 𝕜 ↥K₁ + n
Tactic: rw [← add_right_inj (finrank 𝕜 K₁)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
K : Submodule 𝕜 E
⊢ finrank.{u_1, u_2} 𝕜 ↥K + finrank.{u_1, u_2} 𝕜 ↥Kᗮ = finrank 𝕜 E
have h : finrank.{u_1, u_2} 𝕜 ↥K + finrank.{u_1, u_2} 𝕜 ↥Kᗮ = finrank.{u_1, u_2} 𝕜 ↥K + finrank.{u_1, u_2} 𝕜 ↥(Kᗮ ⊓ ⊤)
Tactic: convert! Submodule.finrank_add_inf_finrank_orthogonal (le_top : K ≤ ⊤) using 1
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
K : Submodule 𝕜 E
h : finrank.{u_1, u_2} 𝕜 ↥K + finrank.{u_1, u_2} 𝕜 ↥Kᗮ = finrank.{u_1, u_2} 𝕜 ↥K + finrank.{u_1, u_2} 𝕜 ↥(Kᗮ ⊓ ⊤)
⊢ finrank.{u_1, u_2} 𝕜 ↥K + finrank.{u_1, u_2} 𝕜 ↥Kᗮ = finrank 𝕜 E
have h₁ : finrank 𝕜 E = finrank.{u_1, u_2} 𝕜 ↥⊤
Tactic: convert! Submodule.finrank_add_inf_finrank_orthogonal (le_top : K ≤ ⊤) using 1
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
K : Submodule 𝕜 E
⊢ finrank.{u_1, u_2} 𝕜 ↥K + finrank.{u_1, u_2} 𝕜 ↥Kᗮ = finrank.{u_1, u_2} 𝕜 ↥K + finrank.{u_1, u_2} 𝕜 ↥(Kᗮ ⊓ ⊤)
have h : finrank.{u_1, u_2} 𝕜 ↥K + finrank.{u_1, u_2} 𝕜 ↥Kᗮ = finrank.{u_1, u_2} 𝕜 ↥K + finrank.{u_1, u_2} 𝕜 ↥Kᗮ
Tactic: rw [inf_top_eq]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
K : Submodule 𝕜 E
n : ℕ
h_dim : finrank.{u_1, u_2} 𝕜 ↥K + n = finrank 𝕜 E
⊢ finrank.{u_1, u_2} 𝕜 ↥Kᗮ = n
have rw : finrank.{u_1, u_2} 𝕜 ↥K + finrank.{u_1, u_2} 𝕜 ↥Kᗮ = finrank.{u_1, u_2} 𝕜 ↥K + n
Tactic: rw [← add_right_inj (finrank 𝕜 K)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
n : ℕ
_i : Fact (finrank 𝕜 E = n + 1)
v : E
hv : v ≠ 0
⊢ finrank.{u_1, u_2} 𝕜 ↥(𝕜 ∙ v)ᗮ = n
have this : FiniteDimensional 𝕜 E
Tactic: haveI : FiniteDimensional 𝕜 E := .of_fact_finrank_eq_succ n