-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem Orthonormal.exists_orthonormalBasis_extension_of_card_eq {ι : Type*} [Fintype ι]
    (card_ι : finrank 𝕜 E = Fintype.card ι) {v : ι → E} {s : Set ι}
    (hv : Orthonormal 𝕜 (s.restrict v)) : ∃ b : OrthonormalBasis ι 𝕜 E, ∀ i ∈ s, b i = v i

Proof state:
case intro.intro.intro
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_7
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (s.restrict v)
hsv : Injective (s.restrict v)
hX✝ : Orthonormal 𝕜 Subtype.val
Y : Finset E
b₀ : OrthonormalBasis { x // x ∈ Y } 𝕜 E
hX : range (s.restrict v) ⊆ ↑Y
hb₀ : ⇑b₀ = Subtype.val
⊢ ∃ b, ∀ i ∈ s, b i = v i

Tactic:
have hιY : Fintype.card ι = Y.card := by
  refine card_ι.symm.trans ?_
  exact Module.finrank_eq_card_finset_basis b₀.toBasis

Result:
case intro.intro.intro
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_7
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (s.restrict v)
hsv : Injective (s.restrict v)
hX✝ : Orthonormal 𝕜 Subtype.val
Y : Finset E
b₀ : OrthonormalBasis { x // x ∈ Y } 𝕜 E
hX : range (s.restrict v) ⊆ ↑Y
hb₀ : ⇑b₀ = Subtype.val
hιY : Fintype.card ι = Y.card
⊢ ∃ b, ∀ i ∈ s, b i = v i

Proof state:
case intro.intro.intro
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_7
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (s.restrict v)
hsv : Injective (s.restrict v)
hX✝ : Orthonormal 𝕜 Subtype.val
Y : Finset E
b₀ : OrthonormalBasis { x // x ∈ Y } 𝕜 E
hX : range (s.restrict v) ⊆ ↑Y
hb₀ : ⇑b₀ = Subtype.val
hιY : Fintype.card ι = Y.card
⊢ ∃ b, ∀ i ∈ s, b i = v i

Tactic:
have hvsY : s.MapsTo v Y := (s.mapsTo_image v).mono_right (by rwa [← range_restrict])

Result:
case intro.intro.intro
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_7
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (s.restrict v)
hsv : Injective (s.restrict v)
hX✝ : Orthonormal 𝕜 Subtype.val
Y : Finset E
b₀ : OrthonormalBasis { x // x ∈ Y } 𝕜 E
hX : range (s.restrict v) ⊆ ↑Y
hb₀ : ⇑b₀ = Subtype.val
hιY : Fintype.card ι = Y.card
hvsY : MapsTo v s ↑Y
⊢ ∃ b, ∀ i ∈ s, b i = v i

Proof state:
case h
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_7
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (s.restrict v)
hsv : Injective (s.restrict v)
hX✝ : Orthonormal 𝕜 Subtype.val
Y : Finset E
b₀ : OrthonormalBasis { x // x ∈ Y } 𝕜 E
hX : range (s.restrict v) ⊆ ↑Y
hb₀ : ⇑b₀ = Subtype.val
hιY : Fintype.card ι = Y.card
hvsY : MapsTo v s ↑Y
hsv' : InjOn v s
g : ι ≃ { x // x ∈ Y }
hg : ∀ i ∈ s, ↑(g i) = v i
i : ι
hi : i ∈ s
⊢ (b₀.reindex g.symm) i = v i

Tactic:
simp [hb₀, hg i hi]

Result:
no goals

Proof state:
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_7
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (s.restrict v)
hsv : Injective (s.restrict v)
hX✝ : Orthonormal 𝕜 Subtype.val
Y : Finset E
b₀ : OrthonormalBasis { x // x ∈ Y } 𝕜 E
hX : range (s.restrict v) ⊆ ↑Y
hb₀ : ⇑b₀ = Subtype.val
hιY : Fintype.card ι = Y.card
⊢ v '' s ⊆ ↑Y

Tactic:
rwa [← range_restrict]

Result:
no goals

Proof state:
case intro.intro.intro
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_7
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (s.restrict v)
hsv : Injective (s.restrict v)
hX✝ : Orthonormal 𝕜 Subtype.val
Y : Finset E
b₀ : OrthonormalBasis { x // x ∈ Y } 𝕜 E
hX : range (s.restrict v) ⊆ ↑Y
hb₀ : ⇑b₀ = Subtype.val
hιY : Fintype.card ι = Y.card
hvsY : MapsTo v s ↑Y
⊢ ∃ b, ∀ i ∈ s, b i = v i

Tactic:
have hsv' : Set.InjOn v s := by
  rw [Set.injOn_iff_injective]
  exact hsv

Result:
case intro.intro.intro
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_7
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (s.restrict v)
hsv : Injective (s.restrict v)
hX✝ : Orthonormal 𝕜 Subtype.val
Y : Finset E
b₀ : OrthonormalBasis { x // x ∈ Y } 𝕜 E
hX : range (s.restrict v) ⊆ ↑Y
hb₀ : ⇑b₀ = Subtype.val
hιY : Fintype.card ι = Y.card
hvsY : MapsTo v s ↑Y
hsv' : InjOn v s
⊢ ∃ b, ∀ i ∈ s, b i = v i

Proof state:
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_7
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (s.restrict v)
hsv : Injective (s.restrict v)
⊢ ∃ b, ∀ i ∈ s, b i = v i

Tactic:
have hX : Orthonormal 𝕜 ((↑) : Set.range (s.restrict v) → E) := by
  rwa [orthonormal_subtype_range hsv]

Result:
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_7
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (s.restrict v)
hsv : Injective (s.restrict v)
hX : Orthonormal 𝕜 Subtype.val
⊢ ∃ b, ∀ i ∈ s, b i = v i

Proof state:
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_7
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (s.restrict v)
hsv : Injective (s.restrict v)
hX✝ : Orthonormal 𝕜 Subtype.val
Y : Finset E
b₀ : OrthonormalBasis { x // x ∈ Y } 𝕜 E
hX : range (s.restrict v) ⊆ ↑Y
hb₀ : ⇑b₀ = Subtype.val
hιY : Fintype.card ι = Y.card
hvsY : MapsTo v s ↑Y
⊢ Injective (s.restrict v)

Tactic:
exact hsv

Result:
no goals

Proof state:
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_7
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (s.restrict v)
hsv : Injective (s.restrict v)
hX : Orthonormal 𝕜 Subtype.val
⊢ ∃ b, ∀ i ∈ s, b i = v i

Tactic:
obtain ⟨Y, b₀, hX, hb₀⟩ := hX.exists_orthonormalBasis_extension

Result:
case intro.intro.intro
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : FiniteDimensional 𝕜 E
ι : Type u_7
inst✝ : Fintype ι
card_ι : finrank 𝕜 E = Fintype.card ι
v : ι → E
s : Set ι
hv : Orthonormal 𝕜 (s.restrict v)
hsv : Injective (s.restrict v)
hX✝ : Orthonormal 𝕜 Subtype.val
Y : Finset E
b₀ : OrthonormalBasis { x // x ∈ Y } 𝕜 E
hX : range (s.restrict v) ⊆ ↑Y
hb₀ : ⇑b₀ = Subtype.val
⊢ ∃ b, ∀ i ∈ s, b i = v i