awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormedField 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : TopologicalSpace F
q : SeminormFamily 𝕜₂ F ι
hq : WithSeminorms q
f : E →ₛₗ[σ₁₂] F
this_1 : IsTopologicalAddGroup F
x : TopologicalSpace E := TopologicalSpace.induced.{u_6, u_7} (Y := F) (⇑f : (a : E) → F) inferInstance
this : IsTopologicalAddGroup E
⊢ WithSeminorms (q.comp f)
have rw : Eq.{u_6 + 1} (α := Filter E)
  (⨅ (i : ι), comap (β := F) (⇑f : (a : E) → F) (comap (β := ℝ) (⇑(q i) : (a : F) → ℝ) (𝓝 0)))
  (⨅ (i : ι), comap (β := ℝ) (⇑(q.comp f i) : (a : E) → ℝ) (𝓝 0))
Tactic: rw [(q.comp f).withSeminorms_iff_nhds_eq_iInf, nhds_induced, map_zero,
    q.withSeminorms_iff_nhds_eq_iInf.mp hq, Filter.comap_iInf]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormedField 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : TopologicalSpace F
q : SeminormFamily 𝕜₂ F ι
hq : WithSeminorms q
f : E →ₛₗ[σ₁₂] F
this_1 : IsTopologicalAddGroup F
x : TopologicalSpace E := TopologicalSpace.induced.{u_6, u_7} (Y := F) (⇑f : (a : E) → F) inferInstance
this : IsTopologicalAddGroup E
⊢ Eq.{u_6 + 1} (α := Filter E)
    (⨅ (i : ι), comap (β := F) (⇑f : (a : E) → F) (comap (β := ℝ) (⇑(q i) : (a : F) → ℝ) (𝓝 0)))
    (⨅ (i : ι), comap (β := ℝ) (⇑(q.comp f i) : (a : E) → ℝ) (𝓝 0))
have refine : ∀ (i : ι),
  Eq (α := Filter E) (comap (β := F) (⇑f : (a : E) → F) (comap (β := ℝ) (⇑(q i) : (a : F) → ℝ) (𝓝 0)))
    (comap (β := ℝ) (⇑(q.comp f i) : (a : E) → ℝ) (𝓝 0))
Tactic: refine iInf_congr fun i => ?_
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
𝕜₂ : Type u_3
E : Type u_6
F : Type u_7
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormedField 𝕜₂
inst_4 : AddCommGroup F
inst_5 : Module 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst_6 : RingHomIsometric σ₁₂
inst_7 : TopologicalSpace F
q : SeminormFamily 𝕜₂ F ι
hq : WithSeminorms q
inst_8 : TopologicalSpace E
f : E →ₛₗ[σ₁₂] F
hf : IsInducing.{u_6, u_7} (X := E) (Y := F) (⇑f : (a : E) → F)
⊢ WithSeminorms (q.comp f)
have rw : WithSeminorms (q.comp f)
Tactic: rw [hf.eq_induced]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (hypothesis)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
κ : ι → Type u_11
p : (i : ι) → SeminormFamily.{u_2, u_6, u_11} 𝕜 E (κ i)
t : ι → TopologicalSpace E
hp : ∀ (i : ι), WithSeminorms (p i)
⊢ WithSeminorms (SeminormFamily.sigma (κ := κ) p)
have this : ∀ (i : ι), IsTopologicalAddGroup E
Tactic: have : ∀ i, @IsTopologicalAddGroup E (t i) _ :=
    fun i ↦ @WithSeminorms.topologicalAddGroup _ _ _ _ _ _ (t i) _ (hp i)
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (hypothesis)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
κ : ι → Type u_11
p : (i : ι) → SeminormFamily.{u_2, u_6, u_11} 𝕜 E (κ i)
t : ι → TopologicalSpace E
hp : ∀ (i : ι), WithSeminorms (p i)
this : ∀ (i : ι), IsTopologicalAddGroup E
⊢ WithSeminorms (SeminormFamily.sigma (κ := κ) p)
have this₁ : IsTopologicalAddGroup E
Tactic: have : @IsTopologicalAddGroup E (⨅ i, t i) _ := topologicalAddGroup_iInf inferInstance
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
κ : ι → Type u_11
p : (i : ι) → SeminormFamily.{u_2, u_6, u_11} 𝕜 E (κ i)
t : ι → TopologicalSpace E
hp : ∀ (i : ι), WithSeminorms (p i)
this_1 : ∀ (i : ι), IsTopologicalAddGroup E
this : IsTopologicalAddGroup E
⊢ WithSeminorms (SeminormFamily.sigma (κ := κ) p)
have simp_rw : ∀ (hp : ∀ (i : ι), t i = ⨅ (i_1 : κ i), UniformSpace.toTopologicalSpace),
  Eq.{u_6 + 1} (α := TopologicalSpace E) (⨅ (i : ι), t i) (⨅ (i : (i : ι) × κ i), UniformSpace.toTopologicalSpace)
Tactic: simp_rw [@SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf _ _ _ _ _ _ _ (_)] at hp ⊢
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
κ : ι → Type u_11
p : (i : ι) → SeminormFamily.{u_2, u_6, u_11} 𝕜 E (κ i)
t : ι → TopologicalSpace E
this_1 : ∀ (i : ι), IsTopologicalAddGroup E
this : IsTopologicalAddGroup E
hp : ∀ (i : ι), t i = ⨅ (i_1 : κ i), UniformSpace.toTopologicalSpace
⊢ Eq.{u_6 + 1} (α := TopologicalSpace E) (⨅ (i : ι), t i) (⨅ (i : (i : ι) × κ i), UniformSpace.toTopologicalSpace)
have rw : Eq.{u_6 + 1} (α := TopologicalSpace E) (⨅ (i : ι), t i) (⨅ (i : ι), ⨅ (j : κ i), UniformSpace.toTopologicalSpace)
Tactic: rw [iInf_sigma]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
ts : Set (TopologicalSpace E)
hts : ∀ t ∈ ts, PolynormableSpace 𝕜 E
⊢ PolynormableSpace 𝕜 E
have rw : PolynormableSpace 𝕜 E
Tactic: rw [sInf_eq_iInf']
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
inst : NormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
t₁ t₂ : TopologicalSpace E
ht₁ : PolynormableSpace 𝕜 E
ht₂ : PolynormableSpace 𝕜 E
⊢ PolynormableSpace 𝕜 E
have rw : PolynormableSpace 𝕜 E
Tactic: rw [← sInf_pair]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (hypothesis)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Countable ι
p : SeminormFamily 𝕜 E ι
inst_4 : TopologicalSpace E
hp : WithSeminorms p
⊢ FirstCountableTopology E
have this : IsTopologicalAddGroup E
Tactic: have := hp.topologicalAddGroup
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (hypothesis)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Countable ι
p : SeminormFamily 𝕜 E ι
inst_4 : TopologicalSpace E
hp : WithSeminorms p
this : IsTopologicalAddGroup E
x : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
⊢ FirstCountableTopology E
have this₁ : IsUniformAddGroup E
Tactic: have : IsUniformAddGroup E := isUniformAddGroup_of_addCommGroup
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (goal)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Countable ι
p : SeminormFamily 𝕜 E ι
inst_4 : TopologicalSpace E
hp : WithSeminorms p
this_1 : IsTopologicalAddGroup E
x : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
⊢ IsCountablyGenerated.{u_6} (α := E) (𝓝 0)
have rw : IsCountablyGenerated.{u_6} (α := E) (⨅ (i : ι), comap (β := ℝ) (⇑(p i) : (a : E) → ℝ) (𝓝 0))
Tactic: rw [p.withSeminorms_iff_nhds_eq_iInf.mp hp]
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (hypothesis)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Countable ι
p : SeminormFamily 𝕜 E ι
inst_4 : TopologicalSpace E
hp : WithSeminorms p
this_1 : IsTopologicalAddGroup E
x : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this : IsUniformAddGroup E
⊢ FirstCountableTopology E
have this₁ : IsCountablyGenerated.{u_6} (α := E) (𝓝 0)
Tactic: have : (𝓝 (0 : E)).IsCountablyGenerated := by
    rw [p.withSeminorms_iff_nhds_eq_iInf.mp hp]
    exact Filter.iInf.isCountablyGenerated _
-- Lean 4 proof step from Mathlib.Analysis.LocallyConvex.WithSeminorms (hypothesis)
Goal:
𝕜 : Type u_2
E : Type u_6
ι : Type u_9
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : Countable ι
p : SeminormFamily 𝕜 E ι
inst_4 : TopologicalSpace E
hp : WithSeminorms p
this_1 : IsTopologicalAddGroup E
x : UniformSpace E := IsTopologicalAddGroup.rightUniformSpace E
this_2 : IsUniformAddGroup E
this : IsCountablyGenerated.{u_6} (α := E) (𝓝 0)
⊢ FirstCountableTopology E
have this₁ : (𝓤 E).IsCountablyGenerated
Tactic: have : (uniformity E).IsCountablyGenerated := IsUniformAddGroup.uniformity_countably_generated
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Hermitian (goal)
Goal:
𝕜 : Type u_1
n : Type u_3
A : Matrix n n 𝕜
inst : RCLike 𝕜
h : A.IsHermitian
i : n
⊢ (↑((re : (a : 𝕜) → ℝ) (A i i)) : 𝕜) = A i i
have rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (A i i) = A i i
Tactic: rw [← conj_eq_iff_re, ← star_def, ← conjTranspose_apply, h.eq]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Hermitian (goal)
Goal:
𝕜 : Type u_1
n : Type u_3
A : Matrix n n 𝕜
inst : RCLike 𝕜
h : A.IsHermitian
i : n
rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (A i i) = A i i
⊢ (↑((re : (a : 𝕜) → ℝ) (A i i)) : 𝕜) = A i i
have rw₁ : star (A i i) = A i i
Tactic: rw [← conj_eq_iff_re, ← star_def, ← conjTranspose_apply, h.eq]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Hermitian (goal)
Goal:
𝕜 : Type u_1
n : Type u_3
A : Matrix n n 𝕜
inst : RCLike 𝕜
h : A.IsHermitian
i : n
rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (A i i) = A i i
rw₁ : star (A i i) = A i i
⊢ (↑((re : (a : 𝕜) → ℝ) (A i i)) : 𝕜) = A i i
have rw₂ : Aᴴ i i = A i i
Tactic: rw [← conj_eq_iff_re, ← star_def, ← conjTranspose_apply, h.eq]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Hermitian (goal)
Goal:
𝕜 : Type u_1
n : Type u_3
A : Matrix n n 𝕜
inst : RCLike 𝕜
h : A.IsHermitian
i : n
rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) (A i i) = A i i
rw₁ : star (A i i) = A i i
rw₂ : Aᴴ i i = A i i
⊢ (↑((re : (a : 𝕜) → ℝ) (A i i)) : 𝕜) = A i i
have rw₃ : A i i = A i i
Tactic: rw [← conj_eq_iff_re, ← star_def, ← conjTranspose_apply, h.eq]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Hermitian (hypothesis)
Goal:
𝕜 : Type u_1
n : Type u_3
A : Matrix n n 𝕜
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
E : Type u_4
inst_3 : NormedAddCommGroup E
inst_4 : InnerProductSpace 𝕜 E
b : OrthonormalBasis n 𝕜 E
⊢ LinearMap.IsSymmetric.{u_1, u_4} (𝕜 := 𝕜) (E := E) ((toLin b.toBasis b.toBasis : (a : Matrix n n 𝕜) → E →ₗ[𝕜] E) A) ↔
    A.IsHermitian
have this : FiniteDimensional 𝕜 E
Tactic: have : FiniteDimensional 𝕜 E := b.toBasis.finiteDimensional_of_finite
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Hermitian (goal)
Goal:
𝕜 : Type u_1
n : Type u_3
A : Matrix n n 𝕜
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
E : Type u_4
inst_3 : NormedAddCommGroup E
inst_4 : InnerProductSpace 𝕜 E
b : OrthonormalBasis n 𝕜 E
this : FiniteDimensional 𝕜 E
⊢ LinearMap.IsSymmetric.{u_1, u_4} (𝕜 := 𝕜) (E := E) ((toLin b.toBasis b.toBasis : (a : Matrix n n 𝕜) → E →ₗ[𝕜] E) A) ↔
    A.IsHermitian
have simp_rw : (∀ (x y : E),
    inner 𝕜 ((((toLin b.toBasis b.toBasis : (a : Matrix n n 𝕜) → E →ₗ[𝕜] E) A : E →ₗ[𝕜] E) : (a : E) → E) x) y =
      inner 𝕜 ((((toLin b.toBasis b.toBasis : (a : Matrix n n 𝕜) → E →ₗ[𝕜] E) Aᴴ : E →ₗ[𝕜] E) : (a : E) → E) x) y) ↔
  A.IsHermitian
Tactic: simp_rw [LinearMap.IsSymmetric, ← LinearMap.adjoint_inner_left, ← toLin_conjTranspose]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Hermitian (goal)
Goal:
𝕜 : Type u_1
n : Type u_3
A : Matrix n n 𝕜
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
E : Type u_4
inst_3 : NormedAddCommGroup E
inst_4 : InnerProductSpace 𝕜 E
b : OrthonormalBasis n 𝕜 E
this : FiniteDimensional 𝕜 E
h : A.IsHermitian
x x_1 : E
⊢ inner 𝕜 ((((toLin b.toBasis b.toBasis : (a : Matrix n n 𝕜) → E →ₗ[𝕜] E) A : E →ₗ[𝕜] E) : (a : E) → E) x) x_1 =
    inner 𝕜 ((((toLin b.toBasis b.toBasis : (a : Matrix n n 𝕜) → E →ₗ[𝕜] E) Aᴴ : E →ₗ[𝕜] E) : (a : E) → E) x) x_1
have rw : inner 𝕜 ((((toLin b.toBasis b.toBasis : (a : Matrix n n 𝕜) → E →ₗ[𝕜] E) A : E →ₗ[𝕜] E) : (a : E) → E) x) x_1 =
  inner 𝕜 ((((toLin b.toBasis b.toBasis : (a : Matrix n n 𝕜) → E →ₗ[𝕜] E) A : E →ₗ[𝕜] E) : (a : E) → E) x) x_1
Tactic: rw [h.eq]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Hermitian (goal)
Goal:
𝕜 : Type u_1
n : Type u_3
A : Matrix n n 𝕜
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
E : Type u_4
inst_3 : NormedAddCommGroup E
inst_4 : InnerProductSpace 𝕜 E
b : OrthonormalBasis n 𝕜 E
this : FiniteDimensional 𝕜 E
⊢ (∀ (x y : E),
      inner 𝕜 ((((toLin b.toBasis b.toBasis : (a : Matrix n n 𝕜) → E →ₗ[𝕜] E) A : E →ₗ[𝕜] E) : (a : E) → E) x) y =
        inner 𝕜 ((((toLin b.toBasis b.toBasis : (a : Matrix n n 𝕜) → E →ₗ[𝕜] E) Aᴴ : E →ₗ[𝕜] E) : (a : E) → E) x) y) ↔
    A.IsHermitian
have refine : ∀
  (h :
    ∀ (x y : E),
      inner 𝕜 ((((toLin b.toBasis b.toBasis : (a : Matrix n n 𝕜) → E →ₗ[𝕜] E) A : E →ₗ[𝕜] E) : (a : E) → E) x) y =
        inner 𝕜 ((((toLin b.toBasis b.toBasis : (a : Matrix n n 𝕜) → E →ₗ[𝕜] E) Aᴴ : E →ₗ[𝕜] E) : (a : E) → E) x) y),
  A.IsHermitian
Tactic: refine ⟨fun h ↦ ?_, fun h _ _ ↦ by rw [h.eq]⟩
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Hermitian (goal)
Goal:
n : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : RCLike 𝕜
inst_3 : NormedAddCommGroup E
inst_4 : InnerProductSpace 𝕜 E
f : E →ₗ[𝕜] E
b : OrthonormalBasis n 𝕜 E
⊢ Matrix.IsHermitian.{u_2, u_1} (α := 𝕜) (n := n) ((toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix n n 𝕜) f) ↔
    IsSymmetric.{u_2, u_3} (𝕜 := 𝕜) (E := E) f
have rw : IsSymmetric.{u_2, u_3} (𝕜 := 𝕜) (E := E)
    ((Matrix.toLin b.toBasis b.toBasis : (a : Matrix n n 𝕜) → E →ₗ[𝕜] E)
      ((toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix n n 𝕜) f)) ↔
  IsSymmetric.{u_2, u_3} (𝕜 := 𝕜) (E := E) f
Tactic: rw [← Matrix.isSymmetric_toLin_iff b, Matrix.toLin_toMatrix]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.Hermitian (goal)
Goal:
n : Type u_1
𝕜 : Type u_2
E : Type u_3
inst : Fintype n
inst_1 : DecidableEq n
inst_2 : RCLike 𝕜
inst_3 : NormedAddCommGroup E
inst_4 : InnerProductSpace 𝕜 E
f : E →ₗ[𝕜] E
b : OrthonormalBasis n 𝕜 E
rw :
  IsSymmetric.{u_2, u_3} (𝕜 := 𝕜) (E := E)
      ((Matrix.toLin b.toBasis b.toBasis : (a : Matrix n n 𝕜) → E →ₗ[𝕜] E)
        ((toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix n n 𝕜) f)) ↔
    IsSymmetric.{u_2, u_3} (𝕜 := 𝕜) (E := E) f
⊢ Matrix.IsHermitian.{u_2, u_1} (α := 𝕜) (n := n) ((toMatrix b.toBasis b.toBasis : (a : E →ₗ[𝕜] E) → Matrix n n 𝕜) f) ↔
    IsSymmetric.{u_2, u_3} (𝕜 := 𝕜) (E := E) f
have rw₁ : IsSymmetric.{u_2, u_3} (𝕜 := 𝕜) (E := E) f ↔ IsSymmetric.{u_2, u_3} (𝕜 := 𝕜) (E := E) f
Tactic: rw [← Matrix.isSymmetric_toLin_iff b, Matrix.toLin_toMatrix]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (goal)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f g : C((↑(spectrum ℝ A) : Type), ℝ)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have simp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: simp only [ContinuousMap.coe_mul, ← map_mul, diagonal_mul_diagonal, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (goal)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f g : C((↑(spectrum ℝ A) : Type), ℝ)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have simp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: simp only [ContinuousMap.coe_add, ← map_add, diagonal_add, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (goal)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
r : ℝ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have simp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: simp only [Function.comp_def, algebraMap_apply, smul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (goal)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
r : ℝ
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have rw : ((↑hA.eigenvectorUnitary : Matrix n n 𝕜) * diagonal fun (x : n) ↦ (↑r : 𝕜)) *
    star (↑hA.eigenvectorUnitary : Matrix n n 𝕜) =
  HMul.hMul (β := Matrix n n 𝕜) (↑hA.eigenvectorUnitary : Matrix n n 𝕜)
      ((algebraMap ℝ (Matrix n n 𝕜) : (a : ℝ) → Matrix n n 𝕜) r : Matrix n n 𝕜) *
    star (↑hA.eigenvectorUnitary : Matrix n n 𝕜)
Tactic: rw [← mul_one (algebraMap _ _ _), ← coe_mul_star_self hA.eigenvectorUnitary,
      ← Algebra.left_comm, coe_star, ← mul_assoc, conjStarAlgAut_apply]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (goal)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
f : C((↑(spectrum ℝ A) : Type), ℝ)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have simp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: simp only [star_trivial, ← map_star, star_eq_conjTranspose, diagonal_conjTranspose, Pi.star_def,
      Function.comp_apply, RCLike.star_def, RCLike.conj_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (hypothesis)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
⊢ IsClosedEmbedding (X := C((↑(spectrum ℝ A) : Type), ℝ)) (Y := Matrix n n 𝕜)
    (⇑hA.cfcAux : (a : C((↑(spectrum ℝ A) : Type), ℝ)) → Matrix n n 𝕜)
have h0 : FiniteDimensional ℝ C((↑(spectrum ℝ A) : Type), ℝ)
Tactic: have h0 : FiniteDimensional ℝ C(spectrum ℝ A, ℝ) :=
    FiniteDimensional.of_injective (ContinuousMap.coeFnLinearMap ℝ (M := ℝ)) DFunLike.coe_injective
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (goal)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
h0 : FiniteDimensional ℝ C((↑(spectrum ℝ A) : Type), ℝ)
⊢ IsClosedEmbedding (X := C((↑(spectrum ℝ A) : Type), ℝ)) (Y := Matrix n n 𝕜)
    (⇑hA.cfcAux : (a : C((↑(spectrum ℝ A) : Type), ℝ)) → Matrix n n 𝕜)
have refine : ∀ (f : C((↑(spectrum ℝ A) : Type), ℝ))
  (hf :
    Eq (α := Matrix n n 𝕜)
      (((↑hA.cfcAux :
              [inst_3 :
                  FunLike (C((↑(spectrum ℝ A) : Type), ℝ) →⋆ₐ[ℝ] Matrix n n 𝕜) C((↑(spectrum ℝ A) : Type), ℝ)
                    (Matrix n n 𝕜)] →
                [SemilinearMapClass (C((↑(spectrum ℝ A) : Type), ℝ) →⋆ₐ[ℝ] Matrix n n 𝕜) (RingHom.id ℝ)
                      C((↑(spectrum ℝ A) : Type), ℝ) (Matrix n n 𝕜)] →
                  C((↑(spectrum ℝ A) : Type), ℝ) →ₗ[ℝ] Matrix n n 𝕜) :
            (a : C((↑(spectrum ℝ A) : Type), ℝ)) → Matrix n n 𝕜)
          f :
        Matrix n n 𝕜)
      (0 : Matrix n n 𝕜)),
  f = 0
Tactic: refine LinearMap.isClosedEmbedding_of_injective (𝕜 := ℝ) (E := C(spectrum ℝ A, ℝ))
    (F := Matrix n n 𝕜) (f := hA.cfcAux) <| LinearMap.ker_eq_bot'.mpr fun f hf ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (hypothesis)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
h0 : FiniteDimensional ℝ C((↑(spectrum ℝ A) : Type), ℝ)
f : C((↑(spectrum ℝ A) : Type), ℝ)
hf :
  (↑hA.eigenvectorUnitary : Matrix n n 𝕜) *
        diagonal
          (RCLike.ofReal ∘
            Function.comp (β := (↑(spectrum ℝ A) : Type)) (⇑f : (a : (↑(spectrum ℝ A) : Type)) → ℝ) fun (i : n) ↦
              Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ A) (hA.eigenvalues i) ⋯) *
      star (↑hA.eigenvectorUnitary : Matrix n n 𝕜) =
    0
⊢ Eq (α := Matrix n n 𝕜)
    (diagonal
      (RCLike.ofReal ∘
        Function.comp (β := (↑(spectrum ℝ A) : Type)) (⇑f : (a : (↑(spectrum ℝ A) : Type)) → ℝ) fun (i : n) ↦
          Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ A) (hA.eigenvalues i) ⋯))
    0
have hf₁ : (↑hA.eigenvectorUnitary : Matrix n n 𝕜) *
        diagonal
          (RCLike.ofReal ∘
            Function.comp (β := (↑(spectrum ℝ A) : Type)) (⇑f : (a : (↑(spectrum ℝ A) : Type)) → ℝ) fun (i : n) ↦
              Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ A) (hA.eigenvalues i) sorry) *
      star (↑hA.eigenvectorUnitary : Matrix n n 𝕜) *
    (↑hA.eigenvectorUnitary : Matrix n n 𝕜) =
  0 * (↑hA.eigenvectorUnitary : Matrix n n 𝕜)
Tactic: replace hf := congr($hf * (hA.eigenvectorUnitary : Matrix n n 𝕜))
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (hypothesis)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
h0 : FiniteDimensional ℝ C((↑(spectrum ℝ A) : Type), ℝ)
f : C((↑(spectrum ℝ A) : Type), ℝ)
hf :
  (↑hA.eigenvectorUnitary : Matrix n n 𝕜) *
          diagonal
            (RCLike.ofReal ∘
              Function.comp (β := (↑(spectrum ℝ A) : Type)) (⇑f : (a : (↑(spectrum ℝ A) : Type)) → ℝ) fun (i : n) ↦
                Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ A) (hA.eigenvalues i) ⋯) *
        star (↑hA.eigenvectorUnitary : Matrix n n 𝕜) *
      (↑hA.eigenvectorUnitary : Matrix n n 𝕜) =
    0 * (↑hA.eigenvectorUnitary : Matrix n n 𝕜)
⊢ Eq (α := Matrix n n 𝕜)
    (diagonal
      (RCLike.ofReal ∘
        Function.comp (β := (↑(spectrum ℝ A) : Type)) (⇑f : (a : (↑(spectrum ℝ A) : Type)) → ℝ) fun (i : n) ↦
          Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ A) (hA.eigenvalues i) ⋯))
    0
have hf₁ : (↑hA.eigenvectorUnitary : Matrix n n 𝕜) *
    diagonal
      (RCLike.ofReal ∘
        Function.comp (β := (↑(spectrum ℝ A) : Type)) (⇑f : (a : (↑(spectrum ℝ A) : Type)) → ℝ) fun (i : n) ↦
          Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ A) (hA.eigenvalues i) sorry) =
  0
Tactic: simp only [mul_assoc, SetLike.coe_mem, Unitary.star_mul_self_of_mem, mul_one, zero_mul] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Matrix.HermitianFunctionalCalculus (hypothesis)
Goal:
n : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : Fintype n
inst_2 : DecidableEq n
A : Matrix n n 𝕜
hA : A.IsHermitian
h0 : FiniteDimensional ℝ C((↑(spectrum ℝ A) : Type), ℝ)
f : C((↑(spectrum ℝ A) : Type), ℝ)
hf :
  Eq (α := Matrix n n 𝕜)
    (((↑hA.cfcAux :
            [inst_3 :
                FunLike (C((↑(spectrum ℝ A) : Type), ℝ) →⋆ₐ[ℝ] Matrix n n 𝕜) C((↑(spectrum ℝ A) : Type), ℝ)
                  (Matrix n n 𝕜)] →
              [SemilinearMapClass (C((↑(spectrum ℝ A) : Type), ℝ) →⋆ₐ[ℝ] Matrix n n 𝕜) (RingHom.id ℝ)
                    C((↑(spectrum ℝ A) : Type), ℝ) (Matrix n n 𝕜)] →
                C((↑(spectrum ℝ A) : Type), ℝ) →ₗ[ℝ] Matrix n n 𝕜) :
          (a : C((↑(spectrum ℝ A) : Type), ℝ)) → Matrix n n 𝕜)
        f :
      Matrix n n 𝕜)
    (0 : Matrix n n 𝕜)
⊢ f = 0
have h2 : Eq (α := Matrix n n 𝕜)
  (diagonal
    (RCLike.ofReal ∘
      Function.comp (β := (↑(spectrum ℝ A) : Type)) (⇑f : (a : (↑(spectrum ℝ A) : Type)) → ℝ) fun (i : n) ↦
        Subtype.mk (p := fun (x : ℝ) ↦ x ∈ spectrum ℝ A) (hA.eigenvalues i) sorry))
  0
Tactic: have h2 :
      diagonal (RCLike.ofReal ∘ f ∘ fun i ↦ ⟨hA.eigenvalues i, hA.eigenvalues_mem_spectrum_real i⟩)
        = (0 : Matrix n n 𝕜) := by
    simp only [LinearMap.coe_coe, cfcAux_apply, conjStarAlgAut_apply] at hf
    replace hf := congr($hf * (hA.eigenvectorUnitary : Matrix n n 𝕜))
    simp only [mul_assoc, SetLike.coe_mem, Unitary.star_mul_self_of_mem, mul_one, zero_mul] at hf
    simpa [← mul_assoc] using congr((star hA.eigenvectorUnitary : Matrix n n 𝕜) * $hf)