awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst_8 : FiniteDimensional 𝕜 E
b : OrthonormalBasis
  (↥(Classical.choose (p := fun (x : Finset E) ↦
      ∃ (b : OrthonormalBasis (↥x) 𝕜 E),
        Eq.{u_4 + 1} (α := (a : ↥x) → E) (⇑b : (a : ↥x) → E) (Subtype.val (p := fun (x_1 : E) ↦ x_1 ∈ x)))
      ⋯))
  𝕜 E :=
  Classical.choose (p :=
    fun
      (x :
        OrthonormalBasis
          (↥(Classical.choose (p := fun (x : Finset E) ↦
              ∃ (b : OrthonormalBasis (↥x) 𝕜 E),
                Eq.{u_4 + 1} (α := (a : ↥x) → E) (⇑b : (a : ↥x) → E) (Subtype.val (p := fun (x_1 : E) ↦ x_1 ∈ x)))
              ⋯))
          𝕜 E) ↦
    Eq.{u_4 + 1} (α :=
      (a :
          ↥(Classical.choose (p := fun (x : Finset E) ↦
              ∃ (b : OrthonormalBasis (↥x) 𝕜 E),
                Eq.{u_4 + 1} (α := (a : ↥x) → E) (⇑b : (a : ↥x) → E) (Subtype.val (p := fun (x_1 : E) ↦ x_1 ∈ x)))
              ⋯)) →
        E)
      (⇑x : (a : ↥(Classical.choose ⋯)) → E)
      (Subtype.val (p := fun (x : E) ↦
        x ∈
          Classical.choose (p := fun (x : Finset E) ↦
            ∃ (b : OrthonormalBasis (↥x) 𝕜 E),
              Eq.{u_4 + 1} (α := (a : ↥x) → E) (⇑b : (a : ↥x) → E) (Subtype.val (p := fun (x_1 : E) ↦ x_1 ∈ x)))
            ⋯)))
    ⋯
rw :
  OrthonormalBasis
    (Fin
      (Fintype.card.{u_4}
        ↥(Classical.choose (p := fun (x : Finset E) ↦
            ∃ (b : OrthonormalBasis (↥x) 𝕜 E),
              Eq.{u_4 + 1} (α := (a : ↥x) → E) (⇑b : (a : ↥x) → E) (Subtype.val (p := fun (x_1 : E) ↦ x_1 ∈ x)))
            ⋯)))
    𝕜 E
⊢ OrthonormalBasis (Fin (finrank 𝕜 E)) 𝕜 E

Tactic:
rw [finrank_eq_card_basis b.toBasis]

Premises used: Module.finrank_eq_card_basis, OrthonormalBasis.toBasis
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst_8 : FiniteDimensional 𝕜 E
b : OrthonormalBasis
  (↥(Classical.choose (p := fun (x : Finset E) ↦
      ∃ (b : OrthonormalBasis (↥x) 𝕜 E),
        Eq.{u_4 + 1} (α := (a : ↥x) → E) (⇑b : (a : ↥x) → E) (Subtype.val (p := fun (x_1 : E) ↦ x_1 ∈ x)))
      ⋯))
  𝕜 E :=
  Classical.choose (p :=
    fun
      (x :
        OrthonormalBasis
          (↥(Classical.choose (p := fun (x : Finset E) ↦
              ∃ (b : OrthonormalBasis (↥x) 𝕜 E),
                Eq.{u_4 + 1} (α := (a : ↥x) → E) (⇑b : (a : ↥x) → E) (Subtype.val (p := fun (x_1 : E) ↦ x_1 ∈ x)))
              ⋯))
          𝕜 E) ↦
    Eq.{u_4 + 1} (α :=
      (a :
          ↥(Classical.choose (p := fun (x : Finset E) ↦
              ∃ (b : OrthonormalBasis (↥x) 𝕜 E),
                Eq.{u_4 + 1} (α := (a : ↥x) → E) (⇑b : (a : ↥x) → E) (Subtype.val (p := fun (x_1 : E) ↦ x_1 ∈ x)))
              ⋯)) →
        E)
      (⇑x : (a : ↥(Classical.choose ⋯)) → E)
      (Subtype.val (p := fun (x : E) ↦
        x ∈
          Classical.choose (p := fun (x : Finset E) ↦
            ∃ (b : OrthonormalBasis (↥x) 𝕜 E),
              Eq.{u_4 + 1} (α := (a : ↥x) → E) (⇑b : (a : ↥x) → E) (Subtype.val (p := fun (x_1 : E) ↦ x_1 ∈ x)))
            ⋯)))
    ⋯
⊢ OrthonormalBasis
    (Fin
      (Fintype.card.{u_4}
        ↥(Classical.choose (p := fun (x : Finset E) ↦
            ∃ (b : OrthonormalBasis (↥x) 𝕜 E),
              Eq.{u_4 + 1} (α := (a : ↥x) → E) (⇑b : (a : ↥x) → E) (Subtype.val (p := fun (x_1 : E) ↦ x_1 ∈ x)))
            ⋯)))
    𝕜 E

Tactic:
exact b.reindex (Fintype.equivFinOfCardEq rfl)

Premises used: OrthonormalBasis.reindex, Fintype.equivFinOfCardEq, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
inst : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
have :
  ∀ (this : Unique ι),
    (Eq (α := (a : ι) → ℝ) (⇑b : (a : ι) → ℝ) fun (x : ι) ↦ 1) ∨
      Eq (α := (a : ι) → ℝ) (⇑b : (a : ι) → ℝ) fun (x : ι) ↦ -1
⊢ (Eq (α := (a : ι) → ℝ) (⇑b : (a : ι) → ℝ) fun (x : ι) ↦ 1) ∨ Eq (α := (a : ι) → ℝ) (⇑b : (a : ι) → ℝ) fun (x : ι) ↦ -1

Tactic:
have : Unique ι := b.toBasis.unique
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
inst : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
this : Unique ι
⊢ Norm.norm (E := ℝ) ((b : (a : ι) → ℝ) default : ℝ) = 1

Tactic:
have : ‖b default‖ = 1 := b.orthonormal.1 _
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
inst : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
this_1 : Unique ι
this : Norm.norm (E := ℝ) ((b : (a : ι) → ℝ) default : ℝ) = 1
rwa :
  ∀ (this : Eq (α := ℝ) (|(b : (a : ι) → ℝ) default| : ℝ) (1 : ℝ)),
    Eq (α := ℝ) ((b : (a : ι) → ℝ) default : ℝ) (1 : ℝ) ∨ Eq (α := ℝ) ((b : (a : ι) → ℝ) default : ℝ) (-1 : ℝ)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : Eq (α := ℝ) ((b : (a : ι) → ℝ) default : ℝ) (1 : ℝ) ∨ Eq (α := ℝ) ((b : (a : ι) → ℝ) default : ℝ) (-1 : ℝ)),
    Eq (α := ℝ) ((b : (a : ι) → ℝ) default : ℝ) (1 : ℝ) ∨ Eq (α := ℝ) ((b : (a : ι) → ℝ) default : ℝ) (-1 : ℝ)
⊢ Eq (α := ℝ) ((b : (a : ι) → ℝ) default : ℝ) (1 : ℝ) ∨ Eq (α := ℝ) ((b : (a : ι) → ℝ) default : ℝ) (-1 : ℝ)

Tactic:
rwa [Real.norm_eq_abs, abs_eq (zero_le_one' ℝ)] at this

Premises used: Real, abs_eq, zero_le_one', Real.norm_eq_abs
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
inst : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
this : Unique ι
⊢ Eq (α := ℝ) ((b : (a : ι) → ℝ) default : ℝ) (1 : ℝ) ∨ Eq (α := ℝ) ((b : (a : ι) → ℝ) default : ℝ) (-1 : ℝ)

Tactic:
have : b default = 1 ∨ b default = -1 := by
    have : ‖b default‖ = 1 := b.orthonormal.1 _
    rwa [Real.norm_eq_abs, abs_eq (zero_le_one' ℝ)] at this
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
inst : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
this_1 : Unique ι
this : Eq (α := ℝ) ((b : (a : ι) → ℝ) default : ℝ) (1 : ℝ) ∨ Eq (α := ℝ) ((b : (a : ι) → ℝ) default : ℝ) (-1 : ℝ)
rw :
  (Eq (α := (a : ι) → ℝ) (const ι ((b : (a : ι) → ℝ) default) : ι → ℝ) fun (x : ι) ↦ (1 : ℝ)) ∨
    Eq (α := (a : ι) → ℝ) (const ι ((b : (a : ι) → ℝ) default) : ι → ℝ) fun (x : ι) ↦ (-1 : ℝ)
⊢ (Eq (α := (a : ι) → ℝ) (⇑b : (a : ι) → ℝ) fun (x : ι) ↦ 1) ∨ Eq (α := (a : ι) → ℝ) (⇑b : (a : ι) → ℝ) fun (x : ι) ↦ -1

Tactic:
rw [eq_const_of_unique b]

Premises used: DFunLike.coe, eq_const_of_unique
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
inst : Fintype ι
b : OrthonormalBasis ι ℝ ℝ
this_1 : Unique ι
this : Eq (α := ℝ) ((b : (a : ι) → ℝ) default : ℝ) (1 : ℝ) ∨ Eq (α := ℝ) ((b : (a : ι) → ℝ) default : ℝ) (-1 : ℝ)
⊢ (Eq (α := (a : ι) → ℝ) (const ι ((b : (a : ι) → ℝ) default) : ι → ℝ) fun (x : ι) ↦ (1 : ℝ)) ∨
    Eq (α := (a : ι) → ℝ) (const ι ((b : (a : ι) → ℝ) default) : ι → ℝ) fun (x : ι) ↦ (-1 : ℝ)

Tactic:
grind
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
inst_4 : FiniteDimensional 𝕜 E
n : ℕ
hn : finrank 𝕜 E = n
inst_5 : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
a : Fin n
hV' : OrthogonalFamily.{u_3, u_4, u_1, u_4} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
⊢ Membership.mem (α := E) (V (subordinateOrthonormalBasisIndex hn hV a hV'))
    ((subordinateOrthonormalBasis hn hV hV' : (a : Fin n) → E) a : E)

Tactic:
simpa only [DirectSum.IsInternal.subordinateOrthonormalBasis, OrthonormalBasis.coe_reindex,
    DirectSum.IsInternal.subordinateOrthonormalBasisIndex] using
    hV.collectedOrthonormalBasis_mem hV' (fun i => stdOrthonormalBasis 𝕜 (V i))
      ((hV.sigmaOrthonormalBasisIndexEquiv hn hV').symm a)

Premises used: DirectSum.IsInternal.subordinateOrthonormalBasisIndex, OrthonormalBasis.coe_reindex, Membership.mem, Subtype, DirectSum.IsInternal.collectedOrthonormalBasis_mem, DirectSum.IsInternal.subordinateOrthonormalBasis, Equiv.symm, DirectSum.IsInternal.sigmaOrthonormalBasisIndexEquiv, DFunLike.coe, stdOrthonormalBasis
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
inst_4 : FiniteDimensional 𝕜 E
n : ℕ
hn : finrank 𝕜 E = n
inst_5 : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily.{u_3, u_4, u_1, u_4} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
i : ι
hi : V i ≠ ⊥
⊢ 0 < finrank.{u_3, u_4} 𝕜 ↥(V i)

Tactic:
grind [finrank_eq_zero (S := V i)]

Premises used: Submodule.finrank_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
inst_4 : FiniteDimensional 𝕜 E
n : ℕ
hn : finrank 𝕜 E = n
inst_5 : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily.{u_3, u_4, u_1, u_4} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
i : ι
hi : V i ≠ ⊥
h :
  subordinateOrthonormalBasisIndex hn hV
      ((sigmaOrthonormalBasisIndexEquiv hn hV hV' : (a : (i : ι) × Fin (finrank 𝕜 ↥(V i))) → Fin n)
        (Sigma.mk (β := fun (i : ι) ↦ Fin (finrank.{u_3, u_4} 𝕜 ↥(V i))) i
          (⟨0, ⋯⟩ : Fin (finrank.{u_3, u_4} 𝕜 ↥(V i)))))
      hV' =
    i
⊢ ∃ (a : Fin n), subordinateOrthonormalBasisIndex hn hV a hV' = i

Tactic:
use hV.sigmaOrthonormalBasisIndexEquiv hn hV' ⟨i, ⟨0, by grind [finrank_eq_zero (S := V i)]⟩⟩

Premises used: Fin.mk, Sigma.mk, DirectSum.IsInternal.sigmaOrthonormalBasisIndexEquiv, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
inst_4 : FiniteDimensional 𝕜 E
n : ℕ
hn : finrank 𝕜 E = n
inst_5 : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily.{u_3, u_4, u_1, u_4} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
i : ι
hi : V i ≠ ⊥
⊢ subordinateOrthonormalBasisIndex hn hV
      ((sigmaOrthonormalBasisIndexEquiv hn hV hV' : (a : (i : ι) × Fin (finrank 𝕜 ↥(V i))) → Fin n)
        (Sigma.mk (β := fun (i : ι) ↦ Fin (finrank.{u_3, u_4} 𝕜 ↥(V i))) i
          (⟨0, ⋯⟩ : Fin (finrank.{u_3, u_4} 𝕜 ↥(V i)))))
      hV' =
    i

Tactic:
simp [subordinateOrthonormalBasisIndex_def]

Premises used: DirectSum.IsInternal.subordinateOrthonormalBasisIndex_def
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst_8 : FiniteDimensional 𝕜 E
n : ℕ
hn : finrank 𝕜 E = n
inst_9 : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily.{u_3, u_4, u_1, u_4} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
i : ι
a : { a : Fin n // subordinateOrthonormalBasisIndex hn hV a hV' = i }
rw : finrank.{u_3, u_4} 𝕜 ↥(V (subordinateOrthonormalBasisIndex hn hV (↑a : Fin n) hV')) = finrank.{u_3, u_4} 𝕜 ↥(V i)
rw₁ rw₂ : finrank.{u_3, u_4} 𝕜 ↥(V i) = finrank.{u_3, u_4} 𝕜 ↥(V i)
⊢ finrank.{u_3, u_4} 𝕜
      ↥(V
          (Sigma.fst (β := fun (i : ι) ↦ Fin (finrank.{u_3, u_4} 𝕜 ↥(V i)))
            (((sigmaOrthonormalBasisIndexEquiv hn hV hV').symm : (a : Fin n) → (i : ι) × Fin (finrank 𝕜 ↥(V i)))
              (↑a : Fin n)))) =
    finrank.{u_3, u_4} 𝕜 ↥(V i)

Tactic:
rw [← subordinateOrthonormalBasisIndex_def, a.property]

Premises used: Subtype.property, DirectSum.IsInternal.subordinateOrthonormalBasisIndex_def
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst_8 : FiniteDimensional 𝕜 E
n : ℕ
hn : finrank 𝕜 E = n
inst_9 : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily.{u_3, u_4, u_1, u_4} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
i : ι
b : Fin (finrank.{u_3, u_4} 𝕜 ↥(V i))
⊢ subordinateOrthonormalBasisIndex hn hV
      ((sigmaOrthonormalBasisIndexEquiv hn hV hV' : (a : (i : ι) × Fin (finrank 𝕜 ↥(V i))) → Fin n)
        (Sigma.mk (β := fun (i : ι) ↦ Fin (finrank.{u_3, u_4} 𝕜 ↥(V i))) i b))
      hV' =
    i

Tactic:
simp [subordinateOrthonormalBasisIndex_def]

Premises used: DirectSum.IsInternal.subordinateOrthonormalBasisIndex_def
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst_8 : FiniteDimensional 𝕜 E
n : ℕ
hn : finrank 𝕜 E = n
inst_9 : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily.{u_3, u_4, u_1, u_4} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
i : ι
⊢ LeftInverse
    (fun (b : Fin (finrank.{u_3, u_4} 𝕜 ↥(V i))) ↦
      Subtype.mk (p := fun (a : Fin n) ↦ subordinateOrthonormalBasisIndex hn hV a hV' = i)
        ((sigmaOrthonormalBasisIndexEquiv hn hV hV' : (a : (i : ι) × Fin (finrank 𝕜 ↥(V i))) → Fin n)
          (Sigma.mk (β := fun (i : ι) ↦ Fin (finrank.{u_3, u_4} 𝕜 ↥(V i))) i b))
        ⋯)
    fun (a : { a : Fin n // subordinateOrthonormalBasisIndex hn hV a hV' = i }) ↦
    Fin.cast (n :=
      finrank.{u_3, u_4} 𝕜
        ↥(V
            (Sigma.fst (β := fun (i : ι) ↦ Fin (finrank.{u_3, u_4} 𝕜 ↥(V i)))
              (((sigmaOrthonormalBasisIndexEquiv hn hV hV').symm : (a : Fin n) → (i : ι) × Fin (finrank 𝕜 ↥(V i)))
                (↑a : Fin n)))))
      ⋯
      (Sigma.snd (β := fun (i : ι) ↦ Fin (finrank.{u_3, u_4} 𝕜 ↥(V i)))
          (((sigmaOrthonormalBasisIndexEquiv hn hV hV').symm : (a : Fin n) → (i : ι) × Fin (finrank 𝕜 ↥(V i)))
            (↑a : Fin n)) :
        Fin
          (finrank.{u_3, u_4} 𝕜
            ↥(V
                (Sigma.fst (β := fun (i : ι) ↦ Fin (finrank.{u_3, u_4} 𝕜 ↥(V i)))
                  (((sigmaOrthonormalBasisIndexEquiv hn hV hV').symm : (a : Fin n) → (i : ι) × Fin (finrank 𝕜 ↥(V i)))
                    (↑a : Fin n))))))

Tactic:
grind [subordinateOrthonormalBasisIndex_def, Fin.cast_eq_self]

Premises used: Fin.cast_eq_self, DirectSum.IsInternal.subordinateOrthonormalBasisIndex_def
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
v : Set E
A : ι → Submodule 𝕜 E
inst_8 : FiniteDimensional 𝕜 E
n : ℕ
hn : finrank 𝕜 E = n
inst_9 : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily.{u_3, u_4, u_1, u_4} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
i : ι
⊢ RightInverse
    (fun (b : Fin (finrank.{u_3, u_4} 𝕜 ↥(V i))) ↦
      Subtype.mk (p := fun (a : Fin n) ↦ subordinateOrthonormalBasisIndex hn hV a hV' = i)
        ((sigmaOrthonormalBasisIndexEquiv hn hV hV' : (a : (i : ι) × Fin (finrank 𝕜 ↥(V i))) → Fin n)
          (Sigma.mk (β := fun (i : ι) ↦ Fin (finrank.{u_3, u_4} 𝕜 ↥(V i))) i b))
        ⋯)
    fun (a : { a : Fin n // subordinateOrthonormalBasisIndex hn hV a hV' = i }) ↦
    Fin.cast (n :=
      finrank.{u_3, u_4} 𝕜
        ↥(V
            (Sigma.fst (β := fun (i : ι) ↦ Fin (finrank.{u_3, u_4} 𝕜 ↥(V i)))
              (((sigmaOrthonormalBasisIndexEquiv hn hV hV').symm : (a : Fin n) → (i : ι) × Fin (finrank 𝕜 ↥(V i)))
                (↑a : Fin n)))))
      ⋯
      (Sigma.snd (β := fun (i : ι) ↦ Fin (finrank.{u_3, u_4} 𝕜 ↥(V i)))
          (((sigmaOrthonormalBasisIndexEquiv hn hV hV').symm : (a : Fin n) → (i : ι) × Fin (finrank 𝕜 ↥(V i)))
            (↑a : Fin n)) :
        Fin
          (finrank.{u_3, u_4} 𝕜
            ↥(V
                (Sigma.fst (β := fun (i : ι) ↦ Fin (finrank.{u_3, u_4} 𝕜 ↥(V i)))
                  (((sigmaOrthonormalBasisIndexEquiv hn hV hV').symm : (a : Fin n) → (i : ι) × Fin (finrank 𝕜 ↥(V i)))
                    (↑a : Fin n))))))

Tactic:
grind
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
inst_4 : FiniteDimensional 𝕜 E
n : ℕ
hn : finrank 𝕜 E = n
inst_5 : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily.{u_3, u_4, u_1, u_4} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
i : ι
i₁ : ↥{a : Fin n | subordinateOrthonormalBasisIndex hn hV a hV' = i} ≃ Fin (finrank.{u_3, u_4} 𝕜 ↥(V i))
⊢ Finset.card (α := Fin n) {a : Fin n | subordinateOrthonormalBasisIndex hn hV a hV' = i} = finrank.{u_3, u_4} 𝕜 ↥(V i)

Tactic:
apply Finset.card_eq_of_equiv_fin

Premises used: Finset.card_eq_of_equiv_fin
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
inst_4 : FiniteDimensional 𝕜 E
n : ℕ
hn : finrank 𝕜 E = n
inst_5 : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
hV' : OrthogonalFamily.{u_3, u_4, u_1, u_4} 𝕜 (E := E) (fun (i : ι) ↦ ↥(V i)) fun (i : ι) ↦ (V i).subtypeₗᵢ
i : ι
⊢ ↥{a : Fin n | subordinateOrthonormalBasisIndex hn hV a hV' = i} ≃ Fin (finrank.{u_3, u_4} 𝕜 ↥(V i))

Tactic:
simpa using hV.subordinateOrthonormalBasisIndexFiberEquiv hn hV' i

Premises used: _private.0.DirectSum.IsInternal.subordinateOrthonormalBasisIndexFiberEquiv
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
V : Type u_7
inst_8 : NormedAddCommGroup V
inst_9 : InnerProductSpace 𝕜 V
inst_10 : FiniteDimensional 𝕜 V
S : Submodule 𝕜 V
L_1 L : ↥S →ₗᵢ[𝕜] V
d : ℕ := finrank.{u_3, u_7} 𝕜 ↥Sᗮ
LS : Submodule 𝕜 V := L.range
⊢ finrank.{u_3, u_7} 𝕜 ↥LSᗮ = finrank 𝕜 V - finrank.{u_3, u_7} 𝕜 ↥LS

Tactic:
simp only [← LS.finrank_add_finrank_orthogonal, add_tsub_cancel_left]

Premises used: add_tsub_cancel_left, Submodule.finrank_add_finrank_orthogonal
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
V : Type u_7
inst_8 : NormedAddCommGroup V
inst_9 : InnerProductSpace 𝕜 V
inst_10 : FiniteDimensional 𝕜 V
S : Submodule 𝕜 V
L_1 L : ↥S →ₗᵢ[𝕜] V
d : ℕ := finrank.{u_3, u_7} 𝕜 ↥Sᗮ
LS : Submodule 𝕜 V := L.range
⊢ finrank 𝕜 V - finrank.{u_3, u_7} 𝕜 ↥LS = finrank 𝕜 V - finrank.{u_3, u_7} 𝕜 ↥S

Tactic:
simp only [LS, LinearMap.finrank_range_of_inj L.injective]

Premises used: LinearMap.finrank_range_of_inj, LinearIsometry.injective
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
V : Type u_7
inst_8 : NormedAddCommGroup V
inst_9 : InnerProductSpace 𝕜 V
inst_10 : FiniteDimensional 𝕜 V
S : Submodule 𝕜 V
L_1 L : ↥S →ₗᵢ[𝕜] V
d : ℕ := finrank.{u_3, u_7} 𝕜 ↥Sᗮ
LS : Submodule 𝕜 V := L.range
⊢ finrank 𝕜 V - finrank.{u_3, u_7} 𝕜 ↥S = finrank.{u_3, u_7} 𝕜 ↥Sᗮ

Tactic:
simp only [← S.finrank_add_finrank_orthogonal, add_tsub_cancel_left]

Premises used: add_tsub_cancel_left, Submodule.finrank_add_finrank_orthogonal
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
V : Type u_7
inst_8 : NormedAddCommGroup V
inst_9 : InnerProductSpace 𝕜 V
inst_10 : FiniteDimensional 𝕜 V
S : Submodule 𝕜 V
L_1 L : ↥S →ₗᵢ[𝕜] V
d : ℕ := finrank.{u_3, u_7} 𝕜 ↥Sᗮ
LS : Submodule 𝕜 V := L.range
⊢ finrank.{u_3, u_7} 𝕜 ↥LSᗮ = d

Tactic:
have dim_LS_perp : finrank 𝕜 LSᗮ = d :=
      calc
        finrank 𝕜 LSᗮ = finrank 𝕜 V - finrank 𝕜 LS := by
          simp only [← LS.finrank_add_finrank_orthogonal, add_tsub_cancel_left]
        _ = finrank 𝕜 V - finrank 𝕜 S := by
          simp only [LS, LinearMap.finrank_range_of_inj L.injective]
        _ = finrank 𝕜 Sᗮ := by simp only [← S.finrank_add_finrank_orthogonal, add_tsub_cancel_left]
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
V : Type u_7
inst_8 : NormedAddCommGroup V
inst_9 : InnerProductSpace 𝕜 V
inst_10 : FiniteDimensional 𝕜 V
S : Submodule 𝕜 V
L_1 L : ↥S →ₗᵢ[𝕜] V
d : ℕ := finrank.{u_3, u_7} 𝕜 ↥Sᗮ
LS : Submodule 𝕜 V := L.range
dim_LS_perp : finrank.{u_3, u_7} 𝕜 ↥LSᗮ = d
⊢ ↥Sᗮ ≃ₗᵢ[𝕜] ↥LSᗮ

Tactic:
exact
      (stdOrthonormalBasis 𝕜 Sᗮ).repr.trans
        ((stdOrthonormalBasis 𝕜 LSᗮ).reindex <| finCongr dim_LS_perp).repr.symm

Premises used: LinearIsometryEquiv.symm, LinearIsometryEquiv.trans, OrthonormalBasis.repr, OrthonormalBasis.reindex, finCongr, Membership.mem, Subtype, Submodule.orthogonal, stdOrthonormalBasis
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
V : Type u_7
inst_8 : NormedAddCommGroup V
inst_9 : InnerProductSpace 𝕜 V
inst_10 : FiniteDimensional 𝕜 V
S : Submodule 𝕜 V
L_1 L : ↥S →ₗᵢ[𝕜] V
d : ℕ := finrank.{u_3, u_7} 𝕜 ↥Sᗮ
LS : Submodule 𝕜 V := L.range
have : (E : ↥Sᗮ ≃ₗᵢ[𝕜] ↥LSᗮ) → V →ₗᵢ[𝕜] V
⊢ V →ₗᵢ[𝕜] V

Tactic:
have E : Sᗮ ≃ₗᵢ[𝕜] LSᗮ := by
    have dim_LS_perp : finrank 𝕜 LSᗮ = d :=
      calc
        finrank 𝕜 LSᗮ = finrank 𝕜 V - finrank 𝕜 LS := by
          simp only [← LS.finrank_add_finrank_orthogonal, add_tsub_cancel_left]
        _ = finrank 𝕜 V - finrank 𝕜 S := by
          simp only [LS, LinearMap.finrank_range_of_inj L.injective]
        _ = finrank 𝕜 Sᗮ := by simp only [← S.finrank_add_finrank_orthogonal, add_tsub_cancel_left]
    exact
      (stdOrthonormalBasis 𝕜 Sᗮ).repr.trans
        ((stdOrthonormalBasis 𝕜 LSᗮ).reindex <| finCongr dim_LS_perp).repr.symm