awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
⊢ Eq.{u_2 + 1} (α := E →ₗ[𝕜] E) ((adjoint : (a : E →ₗ[𝕜] E) → E →ₗ[𝕜] E) id : E →ₗ[𝕜] E) (id : E →ₗ[𝕜] E)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
⊢ Eq.{u_2 + 1} (α := E →ₗ[𝕜] E) ((adjoint : (a : E →ₗ[𝕜] E) → E →ₗ[𝕜] E) 1 : E →ₗ[𝕜] E) (1 : E →ₗ[𝕜] E)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
⊢ CompleteSpace E

Tactic:
haveI := FiniteDimensional.complete 𝕜 E
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
this : CompleteSpace E
⊢ CompleteSpace F

Tactic:
haveI := FiniteDimensional.complete 𝕜 F
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
this_1 : CompleteSpace E
this : CompleteSpace F
⊢ A.kerᗮ =
    range.{u_1, u_1, u_3, u_2} (R := 𝕜) (M := F) (τ₁₂ := RingHom.id 𝕜) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A)

Tactic:
simpa using A.toContinuousLinearMap.orthogonal_ker

Premises used: DFunLike.coe, LinearMap.toContinuousLinearMap, ContinuousLinearMap.orthogonal_ker
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
this_1 : CompleteSpace E
this : CompleteSpace F
⊢ A.rangeᗮ =
    ker.{u_1, u_1, u_3, u_2} (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A)

Tactic:
simpa using A.toContinuousLinearMap.orthogonal_range

Premises used: ContinuousLinearMap.orthogonal_range, DFunLike.coe, LinearMap.toContinuousLinearMap
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
this_1 : CompleteSpace E
this : CompleteSpace F
⊢ ker (M₂ := E) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A ∘ₗ A) = A.ker

Tactic:
simpa using A.toContinuousLinearMap.ker_adjoint_comp_self

Premises used: ContinuousLinearMap.ker_adjoint_comp_self, DFunLike.coe, LinearMap.toContinuousLinearMap
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
⊢ Eq (α := Submodule 𝕜 F) (ker (A ∘ₗ (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A))
    (ker.{u_1, u_1, u_3, u_2} (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A))

Tactic:
simpa using A.adjoint.ker_adjoint_comp_self

Premises used: LinearMap.ker_adjoint_comp_self, DFunLike.coe, LinearMap.adjoint
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
rw :
  Function.Injective (α := E) (β := E) (⇑((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A ∘ₗ A) : (a : E) → E) ↔
    Function.Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑A : (a : E) → F)
rw₁ :
  ker (M₂ := E) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A ∘ₗ A) = ⊥ ↔
    Function.Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑A : (a : E) → F)
rw₂ : ker (M₂ := E) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A ∘ₗ A) = ⊥ ↔ A.ker = ⊥
rw₃ rw₄ : A.ker = ⊥ ↔ A.ker = ⊥
⊢ Function.Injective.{u_2 + 1, u_2 + 1} (α := E) (β := E)
      (Function.comp.{u_2 + 1, u_3 + 1, u_2 + 1} (β := F)
        (⇑((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A : F →ₗ[𝕜] E) : (a : F) → E) (⇑A : (a : E) → F)) ↔
    Function.Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑A : (a : E) → F)

Tactic:
rw [← coe_comp, ← ker_eq_bot, ← ker_eq_bot, ker_adjoint_comp_self]

Premises used: LinearMap.ker_adjoint_comp_self, LinearMap.ker_eq_bot, LinearMap.coe_comp
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
⊢ Function.Injective.{u_3 + 1, u_3 + 1} (α := F) (β := F)
      (Function.comp.{u_3 + 1, u_2 + 1, u_3 + 1} (β := E) (⇑A : (a : E) → F)
        (⇑((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A : F →ₗ[𝕜] E) : (a : F) → E)) ↔
    Function.Injective.{u_3 + 1, u_2 + 1} (α := F) (β := E)
      (⇑((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A : F →ₗ[𝕜] E) : (a : F) → E)

Tactic:
simpa using A.adjoint.adjoint_comp_self_injective_iff

Premises used: LinearMap.adjoint_comp_self_injective_iff, DFunLike.coe, LinearMap.adjoint
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
⊢ range ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A ∘ₗ A) =
    (ker (M₂ := E) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A ∘ₗ A))ᗮ

Tactic:
simp [orthogonal_ker]

Premises used: LinearMap.orthogonal_ker
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
rw :
  A.kerᗮ =
    range.{u_1, u_1, u_3, u_2} (R := 𝕜) (M := F) (τ₁₂ := RingHom.id 𝕜) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A)
rw₁ rw₂ :
  Eq.{u_2 + 1} (α := Submodule 𝕜 E)
    (range.{u_1, u_1, u_3, u_2} (R := 𝕜) (M := F) (τ₁₂ := RingHom.id 𝕜) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A))
    (range.{u_1, u_1, u_3, u_2} (R := 𝕜) (M := F) (τ₁₂ := RingHom.id 𝕜) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A))
⊢ (ker (M₂ := E) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A ∘ₗ A))ᗮ =
    range.{u_1, u_1, u_3, u_2} (R := 𝕜) (M := F) (τ₁₂ := RingHom.id 𝕜) ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A)

Tactic:
rw [ker_adjoint_comp_self, orthogonal_ker]

Premises used: LinearMap.orthogonal_ker, LinearMap.ker_adjoint_comp_self
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
⊢ range (M := F) (A ∘ₗ (adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A) = A.range

Tactic:
simpa using A.adjoint.range_adjoint_comp_self

Premises used: LinearMap.range_adjoint_comp_self, DFunLike.coe, LinearMap.adjoint
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
⊢ finrank.{u_1, u_2} 𝕜
      ↥(range.{u_1, u_1, u_3, u_2} (R := 𝕜) (M := F) (τ₁₂ := RingHom.id 𝕜)
          ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A)) =
    finrank 𝕜 F -
      finrank.{u_1, u_3} 𝕜
        ↥(ker.{u_1, u_1, u_3, u_2} (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
            ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A))

Tactic:
simp [← A.adjoint.finrank_range_add_finrank_ker]

Premises used: DFunLike.coe, LinearMap.finrank_range_add_finrank_ker, LinearMap.adjoint
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
rw :
  finrank.{u_1, u_3} 𝕜
          ↥(ker.{u_1, u_1, u_3, u_2} (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
              ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A)) +
        finrank.{u_1, u_3} 𝕜 ↥A.range -
      finrank.{u_1, u_3} 𝕜
        ↥(ker.{u_1, u_1, u_3, u_2} (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
            ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A)) =
    finrank.{u_1, u_3} 𝕜 ↥A.range
⊢ finrank 𝕜 F -
      finrank.{u_1, u_3} 𝕜
        ↥(ker.{u_1, u_1, u_3, u_2} (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
            ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A)) =
    finrank.{u_1, u_3} 𝕜 ↥A.range

Tactic:
rw [← A.adjoint.ker.finrank_add_finrank_orthogonal,
    orthogonal_ker, adjoint_adjoint]

Premises used: LinearMap.adjoint_adjoint, LinearMap.orthogonal_ker, LinearMap.ker, Submodule.finrank_add_finrank_orthogonal, DFunLike.coe, LinearMap.adjoint
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
A : E →ₗ[𝕜] F
⊢ finrank.{u_1, u_3} 𝕜
          ↥(ker.{u_1, u_1, u_3, u_2} (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
              ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A)) +
        finrank.{u_1, u_3} 𝕜 ↥A.range -
      finrank.{u_1, u_3} 𝕜
        ↥(ker.{u_1, u_1, u_3, u_2} (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
            ((adjoint : (a : E →ₗ[𝕜] F) → F →ₗ[𝕜] E) A)) =
    finrank.{u_1, u_3} 𝕜 ↥A.range

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
ι₁ : Type u_5
ι₂ : Type u_6
b₁ : Basis ι₁ 𝕜 E
b₂ : Basis ι₂ 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : A = (adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B
x : ι₁
y : ι₂
rw :
  inner.{u_1, u_3} 𝕜 (E := F)
      ((((adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B : E →ₗ[𝕜] F) : (a : E) → F) ((b₁ : (a : ι₁) → E) x : E) : F)
      ((b₂ : (a : ι₂) → F) y : F) =
    inner.{u_1, u_2} 𝕜 (E := E) ((b₁ : (a : ι₁) → E) x : E) ((B : (a : F) → E) ((b₂ : (a : ι₂) → F) y : F) : E)
rw₁ rw₂ :
  inner.{u_1, u_2} 𝕜 (E := E) ((b₁ : (a : ι₁) → E) x : E) ((B : (a : F) → E) ((b₂ : (a : ι₂) → F) y : F) : E) =
    inner.{u_1, u_2} 𝕜 (E := E) ((b₁ : (a : ι₁) → E) x : E) ((B : (a : F) → E) ((b₂ : (a : ι₂) → F) y : F) : E)
⊢ inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) ((b₁ : (a : ι₁) → E) x : E) : F) ((b₂ : (a : ι₂) → F) y : F) =
    inner.{u_1, u_2} 𝕜 (E := E) ((b₁ : (a : ι₁) → E) x : E) ((B : (a : F) → E) ((b₂ : (a : ι₂) → F) y : F) : E)

Tactic:
rw [h, adjoint_inner_left]

Premises used: LinearMap.adjoint_inner_left
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
ι₁ : Type u_5
ι₂ : Type u_6
b₁ : Basis ι₁ 𝕜 E
b₂ : Basis ι₂ 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
refine :
  ∀
    (h :
      ∀ (i₁ : ι₁) (i₂ : ι₂),
        inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) ((b₁ : (a : ι₁) → E) i₁ : E) : F) ((b₂ : (a : ι₂) → F) i₂ : F) =
          inner.{u_1, u_2} 𝕜 (E := E) ((b₁ : (a : ι₁) → E) i₁ : E)
            ((B : (a : F) → E) ((b₂ : (a : ι₂) → F) i₂ : F) : E)),
    A = (adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B
⊢ A = (adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B ↔
    ∀ (i₁ : ι₁) (i₂ : ι₂),
      inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) ((b₁ : (a : ι₁) → E) i₁ : E) : F) ((b₂ : (a : ι₂) → F) i₂ : F) =
        inner.{u_1, u_2} 𝕜 (E := E) ((b₁ : (a : ι₁) → E) i₁ : E) ((B : (a : F) → E) ((b₂ : (a : ι₂) → F) i₂ : F) : E)

Tactic:
refine ⟨fun h x y => by rw [h, adjoint_inner_left], fun h => ?_⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
ι₁ : Type u_5
ι₂ : Type u_6
b₁ : Basis ι₁ 𝕜 E
b₂ : Basis ι₂ 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h :
  ∀ (i₁ : ι₁) (i₂ : ι₂),
    inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) ((b₁ : (a : ι₁) → E) i₁ : E) : F) ((b₂ : (a : ι₂) → F) i₂ : F) =
      inner.{u_1, u_2} 𝕜 (E := E) ((b₁ : (a : ι₁) → E) i₁ : E) ((B : (a : F) → E) ((b₂ : (a : ι₂) → F) i₂ : F) : E)
⊢ A = (adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B

Tactic:
Basis.ext b₁ fun i₁ => ?_

Premises used: Module.Basis.ext
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
ι₁ : Type u_5
ι₂ : Type u_6
b₁ : Basis ι₁ 𝕜 E
b₂ : Basis ι₂ 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h :
  ∀ (i₁ : ι₁) (i₂ : ι₂),
    inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) ((b₁ : (a : ι₁) → E) i₁ : E) : F) ((b₂ : (a : ι₂) → F) i₂ : F) =
      inner.{u_1, u_2} 𝕜 (E := E) ((b₁ : (a : ι₁) → E) i₁ : E) ((B : (a : F) → E) ((b₂ : (a : ι₂) → F) i₂ : F) : E)
refine :
  ∀ (i₁ : ι₁),
    Eq.{u_3 + 1} (α := F) ((A : (a : E) → F) ((b₁ : (a : ι₁) → E) i₁ : E) : F)
      ((((adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B : E →ₗ[𝕜] F) : (a : E) → F) ((b₁ : (a : ι₁) → E) i₁ : E) : F)
⊢ A = (adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B

Tactic:
refine Basis.ext b₁ fun i₁ => ?_

Premises used: Module.Basis.ext
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
ι₁ : Type u_5
ι₂ : Type u_6
b₁ : Basis ι₁ 𝕜 E
b₂ : Basis ι₂ 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h :
  ∀ (i₁ : ι₁) (i₂ : ι₂),
    inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) ((b₁ : (a : ι₁) → E) i₁ : E) : F) ((b₂ : (a : ι₂) → F) i₂ : F) =
      inner.{u_1, u_2} 𝕜 (E := E) ((b₁ : (a : ι₁) → E) i₁ : E) ((B : (a : F) → E) ((b₂ : (a : ι₂) → F) i₂ : F) : E)
i₁ : ι₁
i₂ : ι₂
⊢ inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) ((b₁ : (a : ι₁) → E) i₁ : E) : F) ((b₂ : (a : ι₂) → F) i₂ : F) =
    inner.{u_1, u_3} 𝕜 (E := F)
      ((((adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B : E →ₗ[𝕜] F) : (a : E) → F) ((b₁ : (a : ι₁) → E) i₁ : E) : F)
      ((b₂ : (a : ι₂) → F) i₂ : F)

Tactic:
simp only [adjoint_inner_left, h i₁ i₂]

Premises used: LinearMap.adjoint_inner_left
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
ι₁ : Type u_5
ι₂ : Type u_6
b₁ : Basis ι₁ 𝕜 E
b₂ : Basis ι₂ 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h :
  ∀ (i₁ : ι₁) (i₂ : ι₂),
    inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) ((b₁ : (a : ι₁) → E) i₁ : E) : F) ((b₂ : (a : ι₂) → F) i₂ : F) =
      inner.{u_1, u_2} 𝕜 (E := E) ((b₁ : (a : ι₁) → E) i₁ : E) ((B : (a : F) → E) ((b₂ : (a : ι₂) → F) i₂ : F) : E)
i₁ : ι₁
⊢ Eq.{u_3 + 1} (α := F) ((A : (a : E) → F) ((b₁ : (a : ι₁) → E) i₁ : E) : F)
    ((((adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B : E →ₗ[𝕜] F) : (a : E) → F) ((b₁ : (a : ι₁) → E) i₁ : E) : F)

Tactic:
exact ext_inner_right_basis b₂ fun i₂ => by simp only [adjoint_inner_left, h i₁ i₂]

Premises used: InnerProductSpace.ext_inner_right_basis
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
ι : Type u_5
b : Basis ι 𝕜 E
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : A = (adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B
x : ι
y : F
rw :
  ⟪(((adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B : E →ₗ[𝕜] F) : (a : E) → F) ((b : (a : ι) → E) x : E), y⟫_𝕜 =
    inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) x : E) ((B : (a : F) → E) y : E)
rw₁ rw₂ :
  inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) x : E) ((B : (a : F) → E) y : E) =
    inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) x : E) ((B : (a : F) → E) y : E)
⊢ ⟪(A : (a : E) → F) ((b : (a : ι) → E) x : E), y⟫_𝕜 =
    inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) x : E) ((B : (a : F) → E) y : E)

Tactic:
rw [h, adjoint_inner_left]

Premises used: LinearMap.adjoint_inner_left
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
ι : Type u_5
b : Basis ι 𝕜 E
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
refine :
  ∀
    (h :
      ∀ (i : ι) (y : F),
        ⟪(A : (a : E) → F) ((b : (a : ι) → E) i : E), y⟫_𝕜 =
          inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((B : (a : F) → E) y : E))
    (i : ι),
    Eq.{u_3 + 1} (α := F) ((A : (a : E) → F) ((b : (a : ι) → E) i : E) : F)
      ((((adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B : E →ₗ[𝕜] F) : (a : E) → F) ((b : (a : ι) → E) i : E) : F)
⊢ A = (adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B ↔
    ∀ (i : ι) (y : F),
      ⟪(A : (a : E) → F) ((b : (a : ι) → E) i : E), y⟫_𝕜 =
        inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((B : (a : F) → E) y : E)

Tactic:
refine ⟨fun h x y => by rw [h, adjoint_inner_left], fun h => Basis.ext b fun i => ?_⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
ι : Type u_5
b : Basis ι 𝕜 E
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h :
  ∀ (i : ι) (y : F),
    ⟪(A : (a : E) → F) ((b : (a : ι) → E) i : E), y⟫_𝕜 =
      inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((B : (a : F) → E) y : E)
i : ι
y : F
⊢ ⟪(A : (a : E) → F) ((b : (a : ι) → E) i : E), y⟫_𝕜 =
    ⟪(((adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B : E →ₗ[𝕜] F) : (a : E) → F) ((b : (a : ι) → E) i : E), y⟫_𝕜

Tactic:
simp only [h i, adjoint_inner_left]

Premises used: LinearMap.adjoint_inner_left
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
ι : Type u_5
b : Basis ι 𝕜 E
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h :
  ∀ (i : ι) (y : F),
    ⟪(A : (a : E) → F) ((b : (a : ι) → E) i : E), y⟫_𝕜 =
      inner.{u_1, u_2} 𝕜 (E := E) ((b : (a : ι) → E) i : E) ((B : (a : F) → E) y : E)
i : ι
⊢ Eq.{u_3 + 1} (α := F) ((A : (a : E) → F) ((b : (a : ι) → E) i : E) : F)
    ((((adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B : E →ₗ[𝕜] F) : (a : E) → F) ((b : (a : ι) → E) i : E) : F)

Tactic:
exact ext_inner_right 𝕜 fun y => by simp only [h i, adjoint_inner_left]

Premises used: ext_inner_right
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
ι : Type u_5
b : Basis ι 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : A = (adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B
x : ι
y : E
rw :
  inner.{u_1, u_3} 𝕜 (E := F) ((((adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B : E →ₗ[𝕜] F) : (a : E) → F) y : F)
      ((b : (a : ι) → F) x : F) =
    ⟪y, (B : (a : F) → E) ((b : (a : ι) → F) x : F)⟫_𝕜
rw₁ rw₂ : ⟪y, (B : (a : F) → E) ((b : (a : ι) → F) x : F)⟫_𝕜 = ⟪y, (B : (a : F) → E) ((b : (a : ι) → F) x : F)⟫_𝕜
⊢ inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) y : F) ((b : (a : ι) → F) x : F) =
    ⟪y, (B : (a : F) → E) ((b : (a : ι) → F) x : F)⟫_𝕜

Tactic:
rw [h, adjoint_inner_left]

Premises used: LinearMap.adjoint_inner_left
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
ι : Type u_5
b : Basis ι 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
refine :
  ∀
    (h :
      ∀ (i : ι) (x : E),
        inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) x : F) ((b : (a : ι) → F) i : F) =
          ⟪x, (B : (a : F) → E) ((b : (a : ι) → F) i : F)⟫_𝕜),
    A = (adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B
⊢ A = (adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B ↔
    ∀ (i : ι) (x : E),
      inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) x : F) ((b : (a : ι) → F) i : F) =
        ⟪x, (B : (a : F) → E) ((b : (a : ι) → F) i : F)⟫_𝕜

Tactic:
refine ⟨fun h x y => by rw [h, adjoint_inner_left], fun h => ?_⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
ι : Type u_5
b : Basis ι 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h :
  ∀ (i : ι) (x : E),
    inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) x : F) ((b : (a : ι) → F) i : F) =
      ⟪x, (B : (a : F) → E) ((b : (a : ι) → F) i : F)⟫_𝕜
h₁ :
  ∀ (x : E),
    Eq.{u_3 + 1} (α := F) ((A : (a : E) → F) x : F)
      ((((adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B : E →ₗ[𝕜] F) : (a : E) → F) x : F)
⊢ A = (adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B

Tactic:
ext x
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : FiniteDimensional 𝕜 E
inst_6 : FiniteDimensional 𝕜 F
ι : Type u_5
b : Basis ι 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h :
  ∀ (i : ι) (x : E),
    inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) x : F) ((b : (a : ι) → F) i : F) =
      ⟪x, (B : (a : F) → E) ((b : (a : ι) → F) i : F)⟫_𝕜
x : E
i : ι
⊢ inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) x : F) ((b : (a : ι) → F) i : F) =
    inner.{u_1, u_3} 𝕜 (E := F) ((((adjoint : (a : F →ₗ[𝕜] E) → E →ₗ[𝕜] F) B : E →ₗ[𝕜] F) : (a : E) → F) x : F)
      ((b : (a : ι) → F) i : F)

Tactic:
simp only [h i, adjoint_inner_left]

Premises used: LinearMap.adjoint_inner_left