awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : E
refine_1 : ∀ (h : Eq (α := E) ((K.starProjection : (a : E) → E) v : E) (0 : E)) (w : E) (hw : w ∈ K), ⟪w, v⟫ = 0
refine_2 : ∀ (hv : v ∈ Kᗮ), Eq (α := E) ((K.starProjection : (a : E) → E) v : E) (0 : E)
⊢ Eq (α := E) ((K.starProjection : (a : E) → E) v : E) (0 : E) ↔ v ∈ Kᗮ

Tactic:
refine ⟨fun h w hw => ?_, fun hv => ?_⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : E
h : Eq (α := E) ((K.starProjection : (a : E) → E) v : E) (0 : E)
w : E
hw : w ∈ K
refine_1 : ⟪(K.starProjection : (a : E) → E) w, v⟫ = 0
refine_1₁ : ⟪w, (K.starProjection : (a : E) → E) v⟫ = 0
refine_1₂ : ⟪w, 0⟫ = 0
refine_1₃ refine_1₄ : Eq.{u_1 + 1} (α := 𝕜) 0 0
⊢ ⟪w, v⟫ = 0

Tactic:
rw [← starProjection_eq_self_iff.mpr hw, inner_starProjection_left_eq_right, h,
      inner_zero_right]

Premises used: Iff.mpr, inner_zero_right, Submodule.inner_starProjection_left_eq_right, Submodule.starProjection_eq_self_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : E
hv : v ∈ Kᗮ
⊢ Eq (α := E) ((K.starProjection : (a : E) → E) v : E) (0 : E)

Tactic:
simp [starProjection_apply, orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero hv]

Premises used: Submodule.orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero, Submodule.starProjection_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : E
⊢ HSub.hSub (α := ℝ) 2 1 = 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : E
rw :
  ‖v‖ * ‖v‖ =
    ‖v - (↑((K.orthogonalProjection : (a : E) → ↥K) v) : E)‖ *
        ‖v - (↑((K.orthogonalProjection : (a : E) → ↥K) v) : E)‖ +
      norm.{u_2} (E := E) (↑((K.orthogonalProjection : (a : E) → ↥K) v) : E) *
        norm.{u_2} (E := E) (↑((K.orthogonalProjection : (a : E) → ↥K) v) : E)
⊢ (re : (a : 𝕜) → ℝ) ⟪(K.starProjection : (a : E) → E) v, v⟫ =
    HPow.hPow (β := ℕ) (norm (E := ↥K) ((K.orthogonalProjection : (a : E) → ↥K) v : ↥K)) 2

Tactic:
rw [starProjection_apply,
    re_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two,
    div_eq_iff (NeZero.ne' 2).symm, pow_two, add_sub_assoc, ← eq_sub_iff_add_eq', coe_norm,
    ← mul_sub_one, show (2 : ℝ) - 1 = 1 by norm_num, mul_one, sub_eq_iff_eq_add', norm_sub_rev]

Premises used: add_sub_assoc, eq_sub_iff_add_eq', NeZero.ne', pow_two, re_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two, Submodule.starProjection_apply, Ne.symm, mul_sub_one, div_eq_iff, norm_sub_rev, Submodule.coe_norm, mul_one, OfNat.ofNat, sub_eq_iff_eq_add'
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : E
⊢ ‖v‖ * ‖v‖ =
    ‖v - (↑((K.orthogonalProjection : (a : E) → ↥K) v) : E)‖ *
        ‖v - (↑((K.orthogonalProjection : (a : E) → ↥K) v) : E)‖ +
      norm.{u_2} (E := E) (↑((K.orthogonalProjection : (a : E) → ↥K) v) : E) *
        norm.{u_2} (E := E) (↑((K.orthogonalProjection : (a : E) → ↥K) v) : E)

Tactic:
orthogonalProjectionFn_norm_sq K v

Premises used: Submodule.orthogonalProjectionFn, Set.Mem, Classical.choose, Submodule.orthogonalProjectionFn_norm_sq
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : E
⊢ ‖v‖ * ‖v‖ =
    ‖v - (↑((K.orthogonalProjection : (a : E) → ↥K) v) : E)‖ *
        ‖v - (↑((K.orthogonalProjection : (a : E) → ↥K) v) : E)‖ +
      norm.{u_2} (E := E) (↑((K.orthogonalProjection : (a : E) → ↥K) v) : E) *
        norm.{u_2} (E := E) (↑((K.orthogonalProjection : (a : E) → ↥K) v) : E)

Tactic:
exact orthogonalProjectionFn_norm_sq K v

Premises used: Submodule.orthogonalProjectionFn_norm_sq
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : E
rw : 0 ≤ HPow.hPow (β := ℕ) (norm (E := ↥K) ((K.orthogonalProjection : (a : E) → ↥K) v : ↥K)) 2
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪(K.starProjection : (a : E) → E) v, v⟫ : ℝ)

Tactic:
rw [re_inner_starProjection_eq_normSq K v]

Premises used: Submodule.re_inner_starProjection_eq_normSq
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : E
⊢ 0 ≤ HPow.hPow (β := ℕ) (norm (E := ↥K) ((K.orthogonalProjection : (a : E) → ↥K) v : ↥K)) 2

Tactic:
sq_nonneg ‖K.orthogonalProjection v‖

Premises used: Norm.norm, Submodule.orthogonalProjection, sq_nonneg, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst_3 : K.HasOrthogonalProjection
v : E
⊢ 0 ≤ HPow.hPow (β := ℕ) (norm (E := ↥K) ((K.orthogonalProjection : (a : E) → ↥K) v : ↥K)) 2

Tactic:
exact sq_nonneg ‖K.orthogonalProjection v‖

Premises used: Norm.norm, Submodule.orthogonalProjection, sq_nonneg, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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
⊢ K.topologicalClosure = K

Tactic:
K.closed_of_finiteDimensional.submodule_topologicalClosure_eq

Premises used: IsClosed.submodule_topologicalClosure_eq, Submodule.closed_of_finiteDimensional
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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
pos :
  ∀ (hK : FiniteDimensional.{u_1, u_2} 𝕜 ↥Kᗮ),
    (LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) =
      HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
neg :
  ∀ (hK : ¬FiniteDimensional.{u_1, u_2} 𝕜 ↥Kᗮ),
    (LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] 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ᗮ)

Tactic:
by_cases hK : FiniteDimensional 𝕜 Kᗮ

Premises used: Membership.mem, Subtype, Submodule.orthogonal, FiniteDimensional
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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ᗮ
neg : finrank 𝕜 E = 0
⊢ (LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) =
    HPow.hPow (α := 𝕜) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)

Tactic:
rw [finrank_of_infinite_dimensional hK, pow_zero, LinearMap.det_eq_one_of_finrank_eq_zero]

Premises used: pow_zero, LinearMap.det_eq_one_of_finrank_eq_zero, Module.finrank_of_infinite_dimensional
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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ᗮ
⊢ finrank 𝕜 E = 0

Tactic:
finrank_of_infinite_dimensional fun h ↦ hK (h.finiteDimensional_submodule _)

Premises used: Submodule.orthogonal, FiniteDimensional.finiteDimensional_submodule, Module.finrank_of_infinite_dimensional
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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ᗮ
⊢ finrank 𝕜 E = 0

Tactic:
exact finrank_of_infinite_dimensional fun h ↦ hK (h.finiteDimensional_submodule _)

Premises used: Submodule.orthogonal, FiniteDimensional.finiteDimensional_submodule, Module.finrank_of_infinite_dimensional
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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ᗮ)
val val_1 : Fin (finrank.{u_1, u_2} 𝕜 ↥K)
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((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))
        (Sum.inl val) (Sum.inl val_1) :
      𝕜)
    (Matrix.fromBlocks (m := Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) (o := Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 1 0 0 (-1)
        (Sum.inl val) (Sum.inl val_1) :
      𝕜)

Tactic:
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]

Premises used: Matrix.one_apply, eq_comm, Finsupp.single_apply, Submodule.reflection_mem_subspace_eq_self, LinearMap.toMatrix_apply, Submodule.reflection_mem_subspace_orthogonalComplement_eq_neg
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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ᗮ)
val : Fin (finrank.{u_1, u_2} 𝕜 ↥K)
val_1 : Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((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))
        (Sum.inl val) (Sum.inr val_1) :
      𝕜)
    (Matrix.fromBlocks (l := Fin (finrank.{u_1, u_2} 𝕜 ↥K)) (o := Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) 1 0 0 (-1)
        (Sum.inl val) (Sum.inr val_1) :
      𝕜)

Tactic:
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]

Premises used: Matrix.one_apply, eq_comm, Finsupp.single_apply, Submodule.reflection_mem_subspace_eq_self, LinearMap.toMatrix_apply, Submodule.reflection_mem_subspace_orthogonalComplement_eq_neg
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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ᗮ)
val : Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
val_1 : Fin (finrank.{u_1, u_2} 𝕜 ↥K)
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((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))
        (Sum.inr val) (Sum.inl val_1) :
      𝕜)
    (Matrix.fromBlocks (m := Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) (n := Fin (finrank.{u_1, u_2} 𝕜 ↥K)) 1 0 0 (-1)
        (Sum.inr val) (Sum.inl val_1) :
      𝕜)

Tactic:
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]

Premises used: Matrix.one_apply, eq_comm, Finsupp.single_apply, Submodule.reflection_mem_subspace_eq_self, LinearMap.toMatrix_apply, Submodule.reflection_mem_subspace_orthogonalComplement_eq_neg
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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ᗮ)
val val_1 : Fin (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((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))
        (Sum.inr val) (Sum.inr val_1) :
      𝕜)
    (Matrix.fromBlocks (l := Fin (finrank.{u_1, u_2} 𝕜 ↥K)) (n := Fin (finrank.{u_1, u_2} 𝕜 ↥K)) 1 0 0 (-1)
        (Sum.inr val) (Sum.inr val_1) :
      𝕜)

Tactic:
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]

Premises used: Matrix.one_apply, eq_comm, Finsupp.single_apply, Submodule.reflection_mem_subspace_eq_self, LinearMap.toMatrix_apply, Submodule.reflection_mem_subspace_orthogonalComplement_eq_neg
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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ᗮ)
⊢ 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]
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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
huv :
  (↑((LinearEquiv.det : (a : E ≃ₗ[𝕜] E) → 𝕜ˣ) K.reflection.toLinearEquiv) : 𝕜) =
    (↑(HPow.hPow (α := 𝕜ˣ) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) : 𝕜)
⊢ (LinearEquiv.det : (a : E ≃ₗ[𝕜] E) → 𝕜ˣ) K.reflection.toLinearEquiv =
    HPow.hPow (α := 𝕜ˣ) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)

Tactic:
ext
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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
huv :
  (LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) =
    HPow.hPow (α := 𝕜) (↑(-1) : 𝕜) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)
⊢ (↑((LinearEquiv.det : (a : E ≃ₗ[𝕜] E) → 𝕜ˣ) K.reflection.toLinearEquiv) : 𝕜) =
    (↑(HPow.hPow (α := 𝕜ˣ) (-1) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)) : 𝕜)

Tactic:
rw [LinearEquiv.coe_det, Units.val_pow_eq_pow_val]

Premises used: Units.val_pow_eq_pow_val, LinearEquiv.coe_det
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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
⊢ (LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) =
    HPow.hPow (α := 𝕜) (↑(-1) : 𝕜) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)

Tactic:
K.det_reflection

Premises used: Submodule.det_reflection
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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
⊢ (LinearMap.det : (a : E →ₗ[𝕜] E) → 𝕜) (↑K.reflection.toLinearEquiv : E →ₗ[𝕜] E) =
    HPow.hPow (α := 𝕜) (↑(-1) : 𝕜) (finrank.{u_1, u_2} 𝕜 ↥Kᗮ)

Tactic:
exact K.det_reflection

Premises used: Submodule.det_reflection
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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₂
⊢ FiniteDimensional.{u_1, u_2} 𝕜 ↥K₁

Tactic:
haveI : FiniteDimensional 𝕜 K₁ := Submodule.finiteDimensional_of_le h
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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₁ ⊔ 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₂)
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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₂ + 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

Premises used: Submodule.orthogonal_disjoint, Submodule.sup_orthogonal_inf_of_hasOrthogonalProjection, finrank_bot, inf_assoc, Disjoint.eq_bot, bot_inf_eq
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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₁ + finrank.{u_1, u_2} 𝕜 ↥(K₁ᗮ ⊓ K₂)

Tactic:
rw [add_zero] at hd

Premises used: add_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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₂ = 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₂

Tactic:
hd.symm

Premises used: Set.Mem, Eq.symm
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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₂ = 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₂

Tactic:
exact hd.symm

Premises used: Eq.symm
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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₂
rw : finrank.{u_1, u_2} 𝕜 ↥K₁ + finrank.{u_1, u_2} 𝕜 ↥(K₁ᗮ ⊓ K₂) = finrank.{u_1, u_2} 𝕜 ↥K₁ + n
⊢ finrank.{u_1, u_2} 𝕜 ↥(K₁ᗮ ⊓ K₂) = n

Tactic:
rw [← add_right_inj (finrank 𝕜 K₁)]

Premises used: Membership.mem, Subtype, add_right_inj, Module.finrank
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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₁ + finrank.{u_1, u_2} 𝕜 ↥(K₁ᗮ ⊓ K₂) = finrank.{u_1, u_2} 𝕜 ↥K₁ + n

Tactic:
simp [Submodule.finrank_add_inf_finrank_orthogonal h, h_dim]

Premises used: Submodule.finrank_add_inf_finrank_orthogonal
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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} 𝕜 ↥⊤

Tactic:
Submodule.finrank_add_inf_finrank_orthogonal (le_top : K ≤ ⊤)

Premises used: Submodule.finrank_add_inf_finrank_orthogonal, le_top
-- Module: Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
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ᗮ ⊓ ⊤)
h₁ : finrank 𝕜 E = finrank.{u_1, u_2} 𝕜 ↥⊤
⊢ finrank.{u_1, u_2} 𝕜 ↥K + finrank.{u_1, u_2} 𝕜 ↥Kᗮ = finrank 𝕜 E

Tactic:
convert! Submodule.finrank_add_inf_finrank_orthogonal (le_top : K ≤ ⊤) using 1

Premises used: Submodule.finrank_add_inf_finrank_orthogonal, le_top