awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
η : Type u_7
inst : Fintype η
inst_1 : DecidableEq η
ι : η → Type u_8
inst_2 : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst_3 : RCLike 𝕜
E : η → Type u_10
inst_4 : (i : η) → NormedAddCommGroup (E i)
inst_5 : (i : η) → InnerProductSpace.{u_9, u_10} 𝕜 (E i)
B : (i : η) → OrthonormalBasis.{u_8, u_9, u_10} (ι i) 𝕜 (E i)
j : (i : η) × ι i
k : η
h :
  ∀ (i : η) (j : ι i),
    Eq.{u_10 + 1} (α := E k)
      (ofLp (p := 2)
          ((Pi.orthonormalBasis (ι := ι) (E := E) B : (a : (i : η) × ι i) → PiLp 2 E)
            (Sigma.mk (β := fun (i : η) ↦ ι i) i j))
          k :
        E k)
      (ofLp (p := 2)
          (PiLp.single 2 (β := E) ((Sigma.mk (β := fun (i : η) ↦ ι i) i j).fst (β := fun (i : η) ↦ ι i))
            ((B ((Sigma.mk (β := fun (i : η) ↦ ι i) i j).fst (β := fun (i : η) ↦ ι i)) :
                (a : ι ⟨i, j⟩.fst) → E ⟨i, j⟩.fst)
              ((Sigma.mk (β := fun (i : η) ↦ ι i) i j).snd (β := fun (i : η) ↦ ι i))))
          k :
        E k)
⊢ Eq.{u_10 + 1} (α := E k)
    (ofLp (p := 2) ((Pi.orthonormalBasis (ι := ι) (E := E) B : (a : (i : η) × ι i) → PiLp 2 E) j) k : E k)
    (ofLp (p := 2)
        (PiLp.single 2 (β := E) (j.fst (β := fun (i : η) ↦ ι i))
          ((B (j.fst (β := fun (i : η) ↦ ι i)) : (a : ι j.fst) → E j.fst) (j.snd (β := fun (i : η) ↦ ι i))))
        k :
      E k)

Tactic:
obtain ⟨i, j⟩ := j
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
η : Type u_7
inst : Fintype η
inst_1 : DecidableEq η
ι : η → Type u_8
inst_2 : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst_3 : RCLike 𝕜
E : η → Type u_10
inst_4 : (i : η) → NormedAddCommGroup (E i)
inst_5 : (i : η) → InnerProductSpace.{u_9, u_10} 𝕜 (E i)
B : (i : η) → OrthonormalBasis.{u_8, u_9, u_10} (ι i) 𝕜 (E i)
k i : η
j : ι i
h :
  Eq.{u_10 + 1} (α := E k)
    (((B k).repr.symm : (a : EuclideanSpace 𝕜 (ι k)) → E k)
        (toLp 2 (Pi.single (M := fun (j : η) ↦ (y : ι j) → 𝕜) i (Pi.single (M := fun (x : ι i) ↦ 𝕜) j 1) k)) :
      E k)
    (Pi.single (M := E) i ((B i : (a : ι i) → E i) j) k : E k)
⊢ Eq.{u_10 + 1} (α := E k)
    (ofLp (p := 2)
        ((Pi.orthonormalBasis (ι := ι) (E := E) B : (a : (i : η) × ι i) → PiLp 2 E)
          (Sigma.mk (β := fun (i : η) ↦ ι i) i j))
        k :
      E k)
    (ofLp (p := 2)
        (PiLp.single 2 (β := E) ((Sigma.mk (β := fun (i : η) ↦ ι i) i j).fst (β := fun (i : η) ↦ ι i))
          ((B ((Sigma.mk (β := fun (i : η) ↦ ι i) i j).fst (β := fun (i : η) ↦ ι i)) :
              (a : ι ⟨i, j⟩.fst) → E ⟨i, j⟩.fst)
            ((Sigma.mk (β := fun (i : η) ↦ ι i) i j).snd (β := fun (i : η) ↦ ι i))))
        k :
      E k)

Tactic:
simp only [Pi.orthonormalBasis, coe_ofRepr, LinearIsometryEquiv.symm_trans,
    LinearIsometryEquiv.symm_symm, LinearIsometryEquiv.piLpCongrRight_symm,
    LinearIsometryEquiv.trans_apply, LinearIsometryEquiv.piLpCongrRight_apply,
    LinearIsometryEquiv.piLpCurry_apply, PiLp.ofLp_single, PiLp.toLp_apply,
    Sigma.curry_single (γ := fun _ _ => 𝕜)]

Premises used: LinearIsometryEquiv.piLpCongrRight_symm, PiLp.ofLp_single, LinearIsometryEquiv.piLpCongrRight_apply, OrthonormalBasis.coe_ofRepr, Pi.orthonormalBasis, LinearIsometryEquiv.piLpCurry_apply, Sigma.curry_single, LinearIsometryEquiv.trans_apply, LinearIsometryEquiv.symm_trans, PiLp.toLp_apply, LinearIsometryEquiv.symm_symm
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
η : Type u_7
inst : Fintype η
inst_1 : DecidableEq η
ι : η → Type u_8
inst_2 : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst_3 : RCLike 𝕜
E : η → Type u_10
inst_4 : (i : η) → NormedAddCommGroup (E i)
inst_5 : (i : η) → InnerProductSpace.{u_9, u_10} 𝕜 (E i)
B : (i : η) → OrthonormalBasis.{u_8, u_9, u_10} (ι i) 𝕜 (E i)
k i : η
j : ι i
h :
  Eq.{u_10 + 1} (α := E i)
    (((B i).repr.symm : (a : EuclideanSpace 𝕜 (ι i)) → E i)
        (toLp 2 (Pi.single (M := fun (j : η) ↦ (y : ι j) → 𝕜) i (Pi.single (M := fun (x : ι i) ↦ 𝕜) j 1) i)) :
      E i)
    (Pi.single (M := E) i ((B i : (a : ι i) → E i) j) i : E i)
h₁ :
  ∀ (hi : i ≠ k),
    Eq.{u_10 + 1} (α := E k)
      (((B k).repr.symm : (a : EuclideanSpace 𝕜 (ι k)) → E k)
          (toLp 2 (Pi.single (M := fun (j : η) ↦ (y : ι j) → 𝕜) i (Pi.single (M := fun (x : ι i) ↦ 𝕜) j 1) k)) :
        E k)
      (Pi.single (M := E) i ((B i : (a : ι i) → E i) j) k : E k)
⊢ Eq.{u_10 + 1} (α := E k)
    (((B k).repr.symm : (a : EuclideanSpace 𝕜 (ι k)) → E k)
        (toLp 2 (Pi.single (M := fun (j : η) ↦ (y : ι j) → 𝕜) i (Pi.single (M := fun (x : ι i) ↦ 𝕜) j 1) k)) :
      E k)
    (Pi.single (M := E) i ((B i : (a : ι i) → E i) j) k : E k)

Tactic:
obtain rfl | hi := Decidable.eq_or_ne i k

Premises used: Decidable.eq_or_ne, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
η : Type u_7
inst : Fintype η
inst_1 : DecidableEq η
ι : η → Type u_8
inst_2 : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst_3 : RCLike 𝕜
E : η → Type u_10
inst_4 : (i : η) → NormedAddCommGroup (E i)
inst_5 : (i : η) → InnerProductSpace.{u_9, u_10} 𝕜 (E i)
B : (i : η) → OrthonormalBasis.{u_8, u_9, u_10} (ι i) 𝕜 (E i)
i : η
j : ι i
⊢ Eq.{u_10 + 1} (α := E i)
    (((B i).repr.symm : (a : EuclideanSpace 𝕜 (ι i)) → E i)
        (toLp 2 (Pi.single (M := fun (j : η) ↦ (y : ι j) → 𝕜) i (Pi.single (M := fun (x : ι i) ↦ 𝕜) j 1) i)) :
      E i)
    (Pi.single (M := E) i ((B i : (a : ι i) → E i) j) i : E i)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
η : Type u_7
inst : Fintype η
inst_1 : DecidableEq η
ι : η → Type u_8
inst_2 : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst_3 : RCLike 𝕜
E : η → Type u_10
inst_4 : (i : η) → NormedAddCommGroup (E i)
inst_5 : (i : η) → InnerProductSpace.{u_9, u_10} 𝕜 (E i)
B : (i : η) → OrthonormalBasis.{u_8, u_9, u_10} (ι i) 𝕜 (E i)
k i : η
j : ι i
hi : i ≠ k
⊢ Eq.{u_10 + 1} (α := E k)
    (((B k).repr.symm : (a : EuclideanSpace 𝕜 (ι k)) → E k)
        (toLp 2 (Pi.single (M := fun (j : η) ↦ (y : ι j) → 𝕜) i (Pi.single (M := fun (x : ι i) ↦ 𝕜) j 1) k)) :
      E k)
    (Pi.single (M := E) i ((B i : (a : ι i) → E i) j) k : E k)

Tactic:
simp [hi]
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
η : Type u_7
inst : Fintype η
ι : η → Type u_8
inst_1 : (i : η) → Fintype (ι i)
𝕜 : Type u_9
inst_2 : RCLike 𝕜
E : η → Type u_10
inst_3 : (i : η) → NormedAddCommGroup (E i)
inst_4 : (i : η) → InnerProductSpace.{u_9, u_10} 𝕜 (E i)
B : (i : η) → OrthonormalBasis.{u_8, u_9, u_10} (ι i) 𝕜 (E i)
x : (i : η) → E i
j : (i : η) × ι i
⊢ Eq.{u_9 + 1} (α := (fun (x : (i : η) × ι i) ↦ 𝕜) j)
    (ofLp (p := 2)
      ((repr (Pi.orthonormalBasis (ι := ι) (E := E) B) : (a : PiLp 2 E) → EuclideanSpace 𝕜 ((i : η) × ι i)) (toLp 2 x))
      j)
    (ofLp (p := 2)
      ((repr (B (j.fst (β := fun (i : η) ↦ ι i))) : (a : E j.fst) → EuclideanSpace 𝕜 (ι j.fst))
        (x (j.fst (β := fun (i : η) ↦ ι i))))
      (j.snd (β := fun (i : η) ↦ ι i)))

Tactic:
rfl

Premises used: Sigma.uncurry, rfl
-- 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 : ι → E
hon : Orthonormal 𝕜 v
hsp : LE.le (α := Submodule 𝕜 E) ⊤ (span 𝕜 (range v))
rwa rwa₁ rwa₂ rwa₃ : Orthonormal 𝕜 v
⊢ Orthonormal.{u_3, u_4, u_1} 𝕜 (E := E) (ι := ι) (⇑(Basis.mk ⋯ hsp) : (a : ι) → E)

Tactic:
rwa [Basis.coe_mk]

Premises used: Module.Basis.coe_mk
-- 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 ι
v : ι → E
hon : Orthonormal 𝕜 v
hsp : LE.le (α := Submodule 𝕜 E) ⊤ (span 𝕜 (range v))
rw : (⇑((Basis.mk ⋯ hsp).toOrthonormalBasis ⋯) : (a : ι) → E) = v
rw₁ : (⇑(Basis.mk ⋯ hsp) : (a : ι) → E) = v
rw₂ rw₃ : v = v
⊢ (⇑(OrthonormalBasis.mk hon hsp) : (a : ι) → E) = v

Tactic:
rw [OrthonormalBasis.mk, _root_.Module.Basis.coe_toOrthonormalBasis, Basis.coe_mk]

Premises used: Module.Basis.coe_mk, OrthonormalBasis.mk, Module.Basis.coe_toOrthonormalBasis
-- 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 ι
v : ι → E
hon : Orthonormal 𝕜 v
hsp : LE.le (α := Submodule 𝕜 E) ⊤ (span 𝕜 (range v))
classical : (⇑((Basis.mk ⋯ hsp).toOrthonormalBasis ⋯) : (a : ι) → E) = v
classical₁ : (⇑(Basis.mk ⋯ hsp) : (a : ι) → E) = v
classical₂ classical₃ : v = v
⊢ (⇑(OrthonormalBasis.mk hon hsp) : (a : ι) → E) = v

Tactic:
classical rw [OrthonormalBasis.mk, _root_.Module.Basis.coe_toOrthonormalBasis, Basis.coe_mk]

Premises used: Module.Basis.coe_mk, OrthonormalBasis.mk, Module.Basis.coe_toOrthonormalBasis
-- 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 : ι → E
inst_8 : DecidableEq E
v' : ι' → E
h : Orthonormal 𝕜 v'
s : Finset ι'
e₀' : Basis.{u_2, u_3, u_4} (↥s) 𝕜 ↥(span 𝕜 (range (ι := ↥s) (v' ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)))) :=
  Basis.span ⋯
⊢ Orthonormal.{u_3, u_4, u_2} 𝕜 (E := ↥(span 𝕜 (range (ι := ↥s) (v' ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)))))
    fun (i : ↥s) ↦
    Subtype.mk (p := fun (x : E) ↦
      Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 (range (ι := ↥s) (v' ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)))) x)
      ((v' ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) i) ⋯

Tactic:
orthonormal_span (h.comp ((↑) : s → ι') Subtype.val_injective)

Premises used: Subtype.val_injective, Orthonormal.comp, Subtype.val, orthonormal_span
-- 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 : ι → E
inst_8 : DecidableEq E
v' : ι' → E
h : Orthonormal 𝕜 v'
s : Finset ι'
e₀' : Basis.{u_2, u_3, u_4} (↥s) 𝕜 ↥(span 𝕜 (range (ι := ↥s) (v' ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)))) :=
  Basis.span ⋯
h₁ :
  ∀ (x : ↥s),
    (↑((e₀' : (a : ↥s) → ↥(span 𝕜 (range (v' ∘ Subtype.val)))) x) : E) =
      (v' ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) x
⊢ Orthonormal.{u_3, u_4, u_2} 𝕜 (E := ↥(span 𝕜 (range (ι := ↥s) (v' ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s))))) (ι :=
    ↥s) (⇑e₀' : (a : ↥s) → ↥(span 𝕜 (range (v' ∘ Subtype.val))))

Tactic:
convert! orthonormal_span (h.comp ((↑) : s → ι') Subtype.val_injective)

Premises used: Subtype.val_injective, Orthonormal.comp, Subtype.val, orthonormal_span
-- 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 : ι → E
inst_8 : DecidableEq E
v' : ι' → E
h : Orthonormal 𝕜 v'
s : Finset ι'
e₀' : Basis.{u_2, u_3, u_4} (↥s) 𝕜 ↥(span 𝕜 (range (ι := ↥s) (v' ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)))) :=
  Basis.span ⋯
x : ↥s
⊢ (↑((e₀' : (a : ↥s) → ↥(span 𝕜 (range (v' ∘ Subtype.val)))) x) : E) = (v' ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)) x

Tactic:
simp [e₀', Basis.span_apply]

Premises used: Module.Basis.span_apply
-- 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 : ι → E
inst_8 : DecidableEq E
v' : ι' → E
h : Orthonormal 𝕜 v'
s : Finset ι'
e₀' : Basis.{u_2, u_3, u_4} (↥s) 𝕜 ↥(span 𝕜 (range (ι := ↥s) (v' ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)))) :=
  Basis.span ⋯
e₀ : OrthonormalBasis.{u_2, u_3, u_4} (↥s) 𝕜
  ↥(span 𝕜 (range (ι := ↥s) (v' ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)))) :=
  OrthonormalBasis.mk ⋯ ⋯
rw :
  Eq (α := Submodule 𝕜 E) (span 𝕜 (range fun (x : (↑(↑s : Set ι') : Type u_2)) ↦ v' (↑x : ι')))
    (span 𝕜 (range (ι := ↥s) (v' ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s))))
⊢ Eq (α := Submodule 𝕜 E) (span 𝕜 (↑(Finset.image v' s) : Set E))
    (span 𝕜 (range (ι := ↥s) (v' ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s))))

Tactic:
rw [Finset.coe_image, image_eq_range]

Premises used: Finset.coe_image, Set.image_eq_range
-- 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 : ι → E
inst_8 : DecidableEq E
v' : ι' → E
h : Orthonormal 𝕜 v'
s : Finset ι'
e₀' : Basis.{u_2, u_3, u_4} (↥s) 𝕜 ↥(span 𝕜 (range (ι := ↥s) (v' ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)))) :=
  Basis.span ⋯
e₀ : OrthonormalBasis.{u_2, u_3, u_4} (↥s) 𝕜
  ↥(span 𝕜 (range (ι := ↥s) (v' ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s)))) :=
  OrthonormalBasis.mk ⋯ ⋯
⊢ Eq (α := Submodule 𝕜 E) (span 𝕜 (range fun (x : (↑(↑s : Set ι') : Type u_2)) ↦ v' (↑x : ι')))
    (span 𝕜 (range (ι := ↥s) (v' ∘ Subtype.val (p := fun (x : ι') ↦ x ∈ s))))

Tactic:
rfl
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
Goal:
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : DecidableEq E
v' : ι' → E
h : Orthonormal 𝕜 v'
s : Finset ι'
i : ↥s
⊢ (↑((OrthonormalBasis.span h s : (a : ↥s) → ↥(span 𝕜 (↑(Finset.image v' s) : Set E))) i) : E) = v' (↑i : ι')

Tactic:
simp only [OrthonormalBasis.span, Basis.span_apply, LinearIsometryEquiv.ofEq_symm,
    OrthonormalBasis.map_apply, OrthonormalBasis.coe_mk, LinearIsometryEquiv.coe_ofEq_apply,
    comp_apply]

Premises used: LinearIsometryEquiv.coe_ofEq_apply, Module.Basis.span_apply, OrthonormalBasis.coe_mk, OrthonormalBasis.map_apply, Function.comp_apply, OrthonormalBasis.span, LinearIsometryEquiv.ofEq_symm
-- 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 : ι → E
hon : Orthonormal 𝕜 v
hsp : Eq (α := Submodule 𝕜 E) (span 𝕜 (range v))ᗮ ⊥
⊢ LE.le (α := Submodule 𝕜 E) ⊤ (span 𝕜 (range v))

Tactic:
Eq.ge ?_

Premises used: Eq.ge
-- 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 : ι → E
hon : Orthonormal 𝕜 v
hsp : Eq (α := Submodule 𝕜 E) (span 𝕜 (range v))ᗮ ⊥
refine : Eq (α := Submodule 𝕜 E) (span 𝕜 (range v)) ⊤
⊢ LE.le (α := Submodule 𝕜 E) ⊤ (span 𝕜 (range v))

Tactic:
refine Eq.ge ?_

Premises used: Eq.ge
-- 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 : ι → E
hon : Orthonormal 𝕜 v
hsp : Eq (α := Submodule 𝕜 E) (span 𝕜 (range v))ᗮ ⊥
⊢ FiniteDimensional.{u_3, u_4} 𝕜 ↥(span 𝕜 (range v))

Tactic:
haveI : FiniteDimensional 𝕜 (span 𝕜 (range v)) :=
        FiniteDimensional.span_of_finite 𝕜 (finite_range v)
-- 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 : ι → E
hon : Orthonormal 𝕜 v
hsp : Eq (α := Submodule 𝕜 E) (span 𝕜 (range v))ᗮ ⊥
this : FiniteDimensional.{u_3, u_4} 𝕜 ↥(span 𝕜 (range v))
⊢ CompleteSpace.{u_4} ↥(span 𝕜 (range v))

Tactic:
haveI : CompleteSpace (span 𝕜 (range v)) := FiniteDimensional.complete 𝕜 _
-- 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 : ι → E
hon : Orthonormal 𝕜 v
hsp : Eq (α := Submodule 𝕜 E) (span 𝕜 (range v))ᗮ ⊥
this_1 : FiniteDimensional.{u_3, u_4} 𝕜 ↥(span 𝕜 (range v))
this : CompleteSpace.{u_4} ↥(span 𝕜 (range v))
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (hsp : Eq (α := Submodule 𝕜 E) (span 𝕜 (range v)) ⊤) (this : FiniteDimensional.{u_3, u_4} 𝕜 ↥(span 𝕜 (range v)))
    (this : CompleteSpace.{u_4} ↥(span 𝕜 (range v))), Eq (α := Submodule 𝕜 E) (span 𝕜 (range v)) ⊤
⊢ Eq (α := Submodule 𝕜 E) (span 𝕜 (range v)) ⊤

Tactic:
rwa [orthogonal_eq_bot_iff] at hsp

Premises used: Submodule.orthogonal_eq_bot_iff
-- 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 ι
v : ι → E
hon : Orthonormal 𝕜 v
hsp : Eq (α := Submodule 𝕜 E) (span 𝕜 (range v))ᗮ ⊥
⊢ (⇑(OrthonormalBasis.mkOfOrthogonalEqBot hon hsp) : (a : ι) → E) = v

Tactic:
OrthonormalBasis.coe_mk hon _

Premises used: OrthonormalBasis.coe_mk
-- 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
inst_3 : Fintype ι
inst_4 : Fintype ι'
b : OrthonormalBasis ι 𝕜 E
e : ι ≃ ι'
i' : ι'
dsimp :
  Eq.{u_4 + 1} (α := E) (({ repr := b.repr.trans (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e) } : (a : ι') → E) i' : E)
    ((b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι) : E)
⊢ Eq.{u_4 + 1} (α := E) ((b.reindex e : (a : ι') → E) i' : E) ((b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι) : E)

Tactic:
dsimp [reindex]

Premises used: OrthonormalBasis.reindex
-- 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
inst_3 : Fintype ι
inst_4 : Fintype ι'
b : OrthonormalBasis ι 𝕜 E
e : ι ≃ ι'
i' : ι'
rw :
  Eq.{u_4 + 1} (α := E)
    ((fun (i : ι') ↦
          ((LinearIsometryEquiv.symm (b.repr.trans (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e)) :
                (a : EuclideanSpace 𝕜 ι') → E)
              (EuclideanSpace.single i 1) :
            E))
        i' :
      E)
    ((b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι) : E)
⊢ Eq.{u_4 + 1} (α := E) (({ repr := b.repr.trans (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e) } : (a : ι') → E) i' : E)
    ((b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι) : E)

Tactic:
rw [coe_ofRepr]

Premises used: OrthonormalBasis.coe_ofRepr
-- 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
inst_3 : Fintype ι
inst_4 : Fintype ι'
b : OrthonormalBasis ι 𝕜 E
e : ι ≃ ι'
i' : ι'
dsimp :
  Eq.{u_4 + 1} (α := E)
    ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E)
        ((LinearIsometryEquiv.symm (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e) :
              (a : EuclideanSpace 𝕜 ι') → EuclideanSpace 𝕜 ι)
            (EuclideanSpace.single i' 1) :
          EuclideanSpace 𝕜 ι) :
      E)
    ((b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι) : E)
⊢ Eq.{u_4 + 1} (α := E)
    ((fun (i : ι') ↦
          ((LinearIsometryEquiv.symm (b.repr.trans (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e)) :
                (a : EuclideanSpace 𝕜 ι') → E)
              (EuclideanSpace.single i 1) :
            E))
        i' :
      E)
    ((b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι) : E)

Tactic:
dsimp
-- 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
inst_3 : Fintype ι
inst_4 : Fintype ι'
b : OrthonormalBasis ι 𝕜 E
e : ι ≃ ι'
i' : ι'
rw :
  Eq.{u_4 + 1} (α := E)
    ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E)
        ((LinearIsometryEquiv.symm (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e) :
              (a : EuclideanSpace 𝕜 ι') → EuclideanSpace 𝕜 ι)
            (EuclideanSpace.single i' 1) :
          EuclideanSpace 𝕜 ι) :
      E)
    ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E)
        (EuclideanSpace.single ((e.symm : (a : ι') → ι) i') 1 : EuclideanSpace 𝕜 ι) :
      E)
rw₁ :
  Eq.{u_4 + 1} (α := E)
    ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E)
        ((LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e.symm : (a : EuclideanSpace 𝕜 ι') → EuclideanSpace 𝕜 ι)
            (EuclideanSpace.single i' 1) :
          EuclideanSpace 𝕜 ι) :
      E)
    ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E)
        (EuclideanSpace.single ((e.symm : (a : ι') → ι) i') 1 : EuclideanSpace 𝕜 ι) :
      E)
rw₂ rw₃ :
  Eq.{u_4 + 1} (α := E)
    ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E)
        (EuclideanSpace.single ((e.symm : (a : ι') → ι) i') 1 : EuclideanSpace 𝕜 ι) :
      E)
    ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E)
        (EuclideanSpace.single ((e.symm : (a : ι') → ι) i') 1 : EuclideanSpace 𝕜 ι) :
      E)
⊢ Eq.{u_4 + 1} (α := E)
    ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E)
        ((LinearIsometryEquiv.symm (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e) :
              (a : EuclideanSpace 𝕜 ι') → EuclideanSpace 𝕜 ι)
            (EuclideanSpace.single i' 1) :
          EuclideanSpace 𝕜 ι) :
      E)
    ((b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι) : E)

Tactic:
rw [← b.repr_symm_single, LinearIsometryEquiv.piLpCongrLeft_symm,
      EuclideanSpace.piLpCongrLeft_single]

Premises used: EuclideanSpace.piLpCongrLeft_single, OrthonormalBasis.repr_symm_single, LinearIsometryEquiv.piLpCongrLeft_symm
-- 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
inst_3 : Fintype ι
inst_4 : Fintype ι'
b : OrthonormalBasis ι 𝕜 E
e : ι ≃ ι'
i' : ι'
dsimp :
  Eq.{u_4 + 1} (α := E) (({ repr := b.repr.trans (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e) } : (a : ι') → E) i' : E)
    ((b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι) : E)
dsimp₁ :
  Eq.{u_4 + 1} (α := E)
    ((fun (i : ι') ↦
          ((LinearIsometryEquiv.symm (b.repr.trans (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e)) :
                (a : EuclideanSpace 𝕜 ι') → E)
              (EuclideanSpace.single i 1) :
            E))
        i' :
      E)
    ((b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι) : E)
dsimp₂ :
  Eq.{u_4 + 1} (α := E)
    ((b.repr.symm : (a : EuclideanSpace 𝕜 ι) → E)
        ((LinearIsometryEquiv.symm (LinearIsometryEquiv.piLpCongrLeft 2 𝕜 𝕜 e) :
              (a : EuclideanSpace 𝕜 ι') → EuclideanSpace 𝕜 ι)
            (EuclideanSpace.single i' 1) :
          EuclideanSpace 𝕜 ι) :
      E)
    ((b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι) : E)
⊢ Eq.{u_4 + 1} (α := E) ((b.reindex e : (a : ι') → E) i' : E) ((b : (a : ι) → E) ((e.symm : (a : ι') → ι) i' : ι) : E)

Tactic:
classical
    dsimp [reindex]
    rw [coe_ofRepr]
    dsimp
    rw [← b.repr_symm_single, LinearIsometryEquiv.piLpCongrLeft_symm,
      EuclideanSpace.piLpCongrLeft_single]

Premises used: OrthonormalBasis.reindex, OrthonormalBasis.coe_ofRepr, EuclideanSpace.piLpCongrLeft_single, LinearIsometryEquiv.piLpCongrLeft_symm