[GOAL]
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : IsMaximal I
a : A
ha : a ∈ I
⊢ ↑(toCharacterSpace I) a = 0
[PROOFSTEP]
unfold Ideal.toCharacterSpace
[GOAL]
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : IsMaximal I
a : A
ha : a ∈ I
⊢ ↑(↑CharacterSpace.equivAlgHom.symm
          (AlgHom.comp (↑(AlgEquiv.symm (NormedRing.algEquivComplexOfComplete (_ : ∀ {a : A ⧸ I}, IsUnit a ↔ a ≠ 0))))
            (Quotient.mkₐ ℂ I)))
      a =
    0
[PROOFSTEP]
simp only [CharacterSpace.equivAlgHom_symm_coe, AlgHom.coe_comp, AlgHom.coe_coe, Quotient.mkₐ_eq_mk,
  Function.comp_apply, NormedRing.algEquivComplexOfComplete_symm_apply]
[GOAL]
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : IsMaximal I
a : A
ha : a ∈ I
⊢ Set.Nonempty.some (_ : Set.Nonempty (spectrum ℂ (↑(Quotient.mk I) a))) = 0
[PROOFSTEP]
simp_rw [Quotient.eq_zero_iff_mem.mpr ha, spectrum.zero_eq]
[GOAL]
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : IsMaximal I
a : A
ha : a ∈ I
⊢ Set.Nonempty.some (_ : Set.Nonempty {0}) = 0
[PROOFSTEP]
exact Set.eq_of_mem_singleton (Set.singleton_nonempty (0 : ℂ)).some_mem
[GOAL]
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : IsMaximal I
a : A
ha : ¬IsUnit a
⊢ ∃ f, ↑f a = 0
[PROOFSTEP]
obtain ⟨M, hM, haM⟩ := (span { a }).exists_le_maximal (span_singleton_ne_top ha)
[GOAL]
case intro.intro
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : IsMaximal I
a : A
ha : ¬IsUnit a
M : Ideal A
hM : IsMaximal M
haM : span {a} ≤ M
⊢ ∃ f, ↑f a = 0
[PROOFSTEP]
exact ⟨M.toCharacterSpace, M.toCharacterSpace_apply_eq_zero_of_mem (haM (mem_span_singleton.mpr ⟨1, (mul_one a).symm⟩))⟩
[GOAL]
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : IsMaximal I
a : A
z : ℂ
⊢ z ∈ spectrum ℂ a ↔ ∃ f, ↑f a = z
[PROOFSTEP]
refine' ⟨fun hz => _, _⟩
[GOAL]
case refine'_1
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : IsMaximal I
a : A
z : ℂ
hz : z ∈ spectrum ℂ a
⊢ ∃ f, ↑f a = z
[PROOFSTEP]
obtain ⟨f, hf⟩ := WeakDual.CharacterSpace.exists_apply_eq_zero hz
[GOAL]
case refine'_1.intro
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : IsMaximal I
a : A
z : ℂ
hz : z ∈ spectrum ℂ a
f : ↑(characterSpace ℂ ((fun x => A) z))
hf : ↑f (↑(algebraMap ℂ A) z - a) = 0
⊢ ∃ f, ↑f a = z
[PROOFSTEP]
simp only [map_sub, sub_eq_zero, AlgHomClass.commutes, Algebra.id.map_eq_id, RingHom.id_apply] at hf
[GOAL]
case refine'_1.intro
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : IsMaximal I
a : A
z : ℂ
hz : z ∈ spectrum ℂ a
f : ↑(characterSpace ℂ ((fun x => A) z))
hf : ↑f (↑(algebraMap ℂ A) z) = ↑f a
⊢ ∃ f, ↑f a = z
[PROOFSTEP]
refine ⟨f, ?_⟩
[GOAL]
case refine'_1.intro
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : IsMaximal I
a : A
z : ℂ
hz : z ∈ spectrum ℂ a
f : ↑(characterSpace ℂ ((fun x => A) z))
hf : ↑f (↑(algebraMap ℂ A) z) = ↑f a
⊢ ↑f a = z
[PROOFSTEP]
rw [AlgHomClass.commutes, Algebra.id.map_eq_id, RingHom.id_apply] at hf
[GOAL]
case refine'_1.intro
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : IsMaximal I
a : A
z : ℂ
hz : z ∈ spectrum ℂ a
f : ↑(characterSpace ℂ ((fun x => A) z))
hf : z = ↑f a
⊢ ↑f a = z
[PROOFSTEP]
exact hf.symm
[GOAL]
case refine'_2
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : IsMaximal I
a : A
z : ℂ
⊢ (∃ f, ↑f a = z) → z ∈ spectrum ℂ a
[PROOFSTEP]
rintro ⟨f, rfl⟩
[GOAL]
case refine'_2.intro
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : IsMaximal I
a : A
f : ↑(characterSpace ℂ A)
⊢ ↑f a ∈ spectrum ℂ a
[PROOFSTEP]
exact AlgHom.apply_mem_spectrum f a
[GOAL]
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : IsMaximal I
a : A
⊢ spectrum ℂ (↑(gelfandTransform ℂ A) a) = spectrum ℂ a
[PROOFSTEP]
ext z
[GOAL]
case h
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : IsMaximal I
a : A
z : ℂ
⊢ z ∈ spectrum ℂ (↑(gelfandTransform ℂ A) a) ↔ z ∈ spectrum ℂ a
[PROOFSTEP]
rw [ContinuousMap.spectrum_eq_range, WeakDual.CharacterSpace.mem_spectrum_iff_exists]
[GOAL]
case h
A : Type u_1
inst✝³ : NormedCommRing A
inst✝² : NormedAlgebra ℂ A
inst✝¹ : CompleteSpace A
I : Ideal A
inst✝ : IsMaximal I
a : A
z : ℂ
⊢ z ∈ Set.range ↑(↑(gelfandTransform ℂ A) a) ↔ ∃ f, ↑f a = z
[PROOFSTEP]
exact Iff.rfl
[GOAL]
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
⊢ Isometry ↑(gelfandTransform ℂ A)
[PROOFSTEP]
nontriviality A
[GOAL]
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
✝ : Nontrivial A
⊢ Isometry ↑(gelfandTransform ℂ A)
[PROOFSTEP]
refine'
  AddMonoidHomClass.isometry_of_norm (gelfandTransform ℂ A) fun a =>
    _
      /- By `spectrum.gelfandTransform_eq`, the spectra of `star a * a` and its
          `gelfandTransform` coincide. Therefore, so do their spectral radii, and since they are
          self-adjoint, so also do their norms. Applying the C⋆-property of the norm and taking square
          roots shows that the norm is preserved. -/
[GOAL]
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
✝ : Nontrivial A
a : A
⊢ ‖↑(gelfandTransform ℂ A) a‖ = ‖a‖
[PROOFSTEP]
have : spectralRadius ℂ (gelfandTransform ℂ A (star a * a)) = spectralRadius ℂ (star a * a) := by unfold spectralRadius;
  rw [spectrum.gelfandTransform_eq]
[GOAL]
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
✝ : Nontrivial A
a : A
⊢ spectralRadius ℂ (↑(gelfandTransform ℂ A) (star a * a)) = spectralRadius ℂ (star a * a)
[PROOFSTEP]
unfold spectralRadius
[GOAL]
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
✝ : Nontrivial A
a : A
⊢ ⨆ (k : ℂ) (_ : k ∈ spectrum ℂ (↑(gelfandTransform ℂ A) (star a * a))), ↑‖k‖₊ =
    ⨆ (k : ℂ) (_ : k ∈ spectrum ℂ (star a * a)), ↑‖k‖₊
[PROOFSTEP]
rw [spectrum.gelfandTransform_eq]
[GOAL]
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
✝ : Nontrivial A
a : A
this : spectralRadius ℂ (↑(gelfandTransform ℂ A) (star a * a)) = spectralRadius ℂ (star a * a)
⊢ ‖↑(gelfandTransform ℂ A) a‖ = ‖a‖
[PROOFSTEP]
rw [map_mul, (IsSelfAdjoint.star_mul_self _).spectralRadius_eq_nnnorm, gelfandTransform_map_star,
  (IsSelfAdjoint.star_mul_self (gelfandTransform ℂ A a)).spectralRadius_eq_nnnorm] at this
[GOAL]
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
✝ : Nontrivial A
a : A
this : ↑‖star (↑(gelfandTransform ℂ A) a) * ↑(gelfandTransform ℂ A) a‖₊ = ↑‖star a * a‖₊
⊢ ‖↑(gelfandTransform ℂ A) a‖ = ‖a‖
[PROOFSTEP]
simp only [ENNReal.coe_eq_coe, CstarRing.nnnorm_star_mul_self, ← sq] at this
[GOAL]
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
✝ : Nontrivial A
a : A
this : ‖↑(gelfandTransform ℂ A) a‖₊ ^ 2 = ‖a‖₊ ^ 2
⊢ ‖↑(gelfandTransform ℂ A) a‖ = ‖a‖
[PROOFSTEP]
simpa only [Function.comp_apply, NNReal.sqrt_sq] using congr_arg (((↑) : ℝ≥0 → ℝ) ∘ ⇑NNReal.sqrt) this
[GOAL]
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
⊢ Function.Bijective ↑(gelfandTransform ℂ A)
[PROOFSTEP]
refine'
  ⟨(gelfandTransform_isometry A).injective, _⟩
    /- The range of `gelfandTransform ℂ A` is actually a `StarSubalgebra`. The key lemma below may be
        hard to spot; it's `map_star` coming from `WeakDual.Complex.instStarHomClass`, which is a
        nontrivial result. -/
[GOAL]
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
⊢ Function.Surjective ↑(gelfandTransform ℂ A)
[PROOFSTEP]
let rng : StarSubalgebra ℂ C(characterSpace ℂ A, ℂ) :=
  { toSubalgebra := (gelfandTransform ℂ A).range
    star_mem' := by
      rintro - ⟨a, rfl⟩
      use star a
      ext1 φ
      simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, gelfandTransform_apply_apply, map_star, IsROrC.star_def,
        ContinuousMap.star_apply] }
[GOAL]
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
⊢ ∀ {a : C(↑(characterSpace ℂ A), ℂ)},
    a ∈ (AlgHom.range (gelfandTransform ℂ A)).toSubsemiring.toSubmonoid.toSubsemigroup.carrier →
      star a ∈ (AlgHom.range (gelfandTransform ℂ A)).toSubsemiring.toSubmonoid.toSubsemigroup.carrier
[PROOFSTEP]
rintro - ⟨a, rfl⟩
[GOAL]
case intro
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
a : A
⊢ star (↑↑(gelfandTransform ℂ A) a) ∈
    (AlgHom.range (gelfandTransform ℂ A)).toSubsemiring.toSubmonoid.toSubsemigroup.carrier
[PROOFSTEP]
use star a
[GOAL]
case h
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
a : A
⊢ ↑↑(gelfandTransform ℂ A) (star a) = star (↑↑(gelfandTransform ℂ A) a)
[PROOFSTEP]
ext1 φ
[GOAL]
case h.h
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
a : A
φ : ↑(characterSpace ℂ A)
⊢ ↑(↑↑(gelfandTransform ℂ A) (star a)) φ = ↑(star (↑↑(gelfandTransform ℂ A) a)) φ
[PROOFSTEP]
simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe, gelfandTransform_apply_apply, map_star, IsROrC.star_def,
  ContinuousMap.star_apply]
[GOAL]
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
rng : StarSubalgebra ℂ C(↑(characterSpace ℂ A), ℂ) :=
  { toSubalgebra := AlgHom.range (gelfandTransform ℂ A),
    star_mem' :=
      (_ :
        ∀ {a : C(↑(characterSpace ℂ A), ℂ)},
          a ∈ (AlgHom.range (gelfandTransform ℂ A)).toSubsemiring.toSubmonoid.toSubsemigroup.carrier →
            star a ∈ (AlgHom.range (gelfandTransform ℂ A)).toSubsemiring.toSubmonoid.toSubsemigroup.carrier) }
⊢ Function.Surjective ↑(gelfandTransform ℂ A)
[PROOFSTEP]
suffices rng = ⊤ from fun x => show x ∈ rng from this.symm ▸ StarSubalgebra.mem_top
[GOAL]
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
rng : StarSubalgebra ℂ C(↑(characterSpace ℂ A), ℂ) :=
  { toSubalgebra := AlgHom.range (gelfandTransform ℂ A),
    star_mem' :=
      (_ :
        ∀ {a : C(↑(characterSpace ℂ A), ℂ)},
          a ∈ (AlgHom.range (gelfandTransform ℂ A)).toSubsemiring.toSubmonoid.toSubsemigroup.carrier →
            star a ∈ (AlgHom.range (gelfandTransform ℂ A)).toSubsemiring.toSubmonoid.toSubsemigroup.carrier) }
⊢ rng = ⊤
[PROOFSTEP]
have h : rng.topologicalClosure = rng :=
  le_antisymm
    (StarSubalgebra.topologicalClosure_minimal le_rfl (gelfandTransform_isometry A).closedEmbedding.closed_range)
    (StarSubalgebra.le_topologicalClosure _)
[GOAL]
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
rng : StarSubalgebra ℂ C(↑(characterSpace ℂ A), ℂ) :=
  { toSubalgebra := AlgHom.range (gelfandTransform ℂ A),
    star_mem' :=
      (_ :
        ∀ {a : C(↑(characterSpace ℂ A), ℂ)},
          a ∈ (AlgHom.range (gelfandTransform ℂ A)).toSubsemiring.toSubmonoid.toSubsemigroup.carrier →
            star a ∈ (AlgHom.range (gelfandTransform ℂ A)).toSubsemiring.toSubmonoid.toSubsemigroup.carrier) }
h : StarSubalgebra.topologicalClosure rng = rng
⊢ rng = ⊤
[PROOFSTEP]
refine'
  h ▸
    ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints _
      (fun _ _ => _)
        /- Separating points just means that elements of the `characterSpace` which agree at all points
            of `A` are the same functional, which is just extensionality. -/
[GOAL]
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
rng : StarSubalgebra ℂ C(↑(characterSpace ℂ A), ℂ) :=
  { toSubalgebra := AlgHom.range (gelfandTransform ℂ A),
    star_mem' :=
      (_ :
        ∀ {a : C(↑(characterSpace ℂ A), ℂ)},
          a ∈ (AlgHom.range (gelfandTransform ℂ A)).toSubsemiring.toSubmonoid.toSubsemigroup.carrier →
            star a ∈ (AlgHom.range (gelfandTransform ℂ A)).toSubsemiring.toSubmonoid.toSubsemigroup.carrier) }
h : StarSubalgebra.topologicalClosure rng = rng
x✝¹ x✝ : ↑(characterSpace ℂ A)
⊢ x✝¹ ≠ x✝ → ∃ f, f ∈ (fun f => ↑f) '' ↑rng.toSubalgebra ∧ f x✝¹ ≠ f x✝
[PROOFSTEP]
contrapose!
[GOAL]
A : Type u_1
inst✝⁵ : NormedCommRing A
inst✝⁴ : NormedAlgebra ℂ A
inst✝³ : CompleteSpace A
inst✝² : StarRing A
inst✝¹ : CstarRing A
inst✝ : StarModule ℂ A
rng : StarSubalgebra ℂ C(↑(characterSpace ℂ A), ℂ) :=
  { toSubalgebra := AlgHom.range (gelfandTransform ℂ A),
    star_mem' :=
      (_ :
        ∀ {a : C(↑(characterSpace ℂ A), ℂ)},
          a ∈ (AlgHom.range (gelfandTransform ℂ A)).toSubsemiring.toSubmonoid.toSubsemigroup.carrier →
            star a ∈ (AlgHom.range (gelfandTransform ℂ A)).toSubsemiring.toSubmonoid.toSubsemigroup.carrier) }
h : StarSubalgebra.topologicalClosure rng = rng
x✝¹ x✝ : ↑(characterSpace ℂ A)
⊢ (∀ (f : ↑(characterSpace ℂ A) → ℂ), f ∈ (fun a => ↑a) '' ↑rng.toSubalgebra → f x✝¹ = f x✝) → x✝¹ = x✝
[PROOFSTEP]
exact fun h =>
  Subtype.ext (ContinuousLinearMap.ext fun a => h (gelfandTransform ℂ A a) ⟨gelfandTransform ℂ A a, ⟨a, rfl⟩, rfl⟩)


[GOAL]
⊢ ConcreteCategory SemiNormedGroupCat
[PROOFSTEP]
dsimp [SemiNormedGroupCat]
[GOAL]
⊢ ConcreteCategory (Bundled SeminormedAddCommGroup)
[PROOFSTEP]
infer_instance
[GOAL]
V W : SemiNormedGroupCat
f g : V ⟶ W
h : (forget SemiNormedGroupCat).map f = (forget SemiNormedGroupCat).map g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
V W : SemiNormedGroupCat
g : V ⟶ W
toFun✝ : ↑V → ↑W
map_add'✝ : ∀ (v₁ v₂ : ↑V), toFun✝ (v₁ + v₂) = toFun✝ v₁ + toFun✝ v₂
bound'✝ : ∃ C, ∀ (v : ↑V), ‖toFun✝ v‖ ≤ C * ‖v‖
h :
  (forget SemiNormedGroupCat).map { toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ } =
    (forget SemiNormedGroupCat).map g
⊢ { toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
V W : SemiNormedGroupCat
toFun✝¹ : ↑V → ↑W
map_add'✝¹ : ∀ (v₁ v₂ : ↑V), toFun✝¹ (v₁ + v₂) = toFun✝¹ v₁ + toFun✝¹ v₂
bound'✝¹ : ∃ C, ∀ (v : ↑V), ‖toFun✝¹ v‖ ≤ C * ‖v‖
toFun✝ : ↑V → ↑W
map_add'✝ : ∀ (v₁ v₂ : ↑V), toFun✝ (v₁ + v₂) = toFun✝ v₁ + toFun✝ v₂
bound'✝ : ∃ C, ∀ (v : ↑V), ‖toFun✝ v‖ ≤ C * ‖v‖
h :
  (forget SemiNormedGroupCat).map { toFun := toFun✝¹, map_add' := map_add'✝¹, bound' := bound'✝¹ } =
    (forget SemiNormedGroupCat).map { toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ }
⊢ { toFun := toFun✝¹, map_add' := map_add'✝¹, bound' := bound'✝¹ } =
    { toFun := toFun✝, map_add' := map_add'✝, bound' := bound'✝ }
[PROOFSTEP]
congr
[GOAL]
V : SemiNormedGroupCat
inst✝ : Subsingleton ↑V
⊢ Limits.IsZero V
[PROOFSTEP]
refine' ⟨fun X => ⟨⟨⟨0⟩, fun f => _⟩⟩, fun X => ⟨⟨⟨0⟩, fun f => _⟩⟩⟩
[GOAL]
case refine'_1
V : SemiNormedGroupCat
inst✝ : Subsingleton ↑V
X : SemiNormedGroupCat
f : V ⟶ X
⊢ f = default
[PROOFSTEP]
ext x
[GOAL]
case refine'_1.h
V : SemiNormedGroupCat
inst✝ : Subsingleton ↑V
X : SemiNormedGroupCat
f : V ⟶ X
x : ↑V
⊢ ↑f x = ↑default x
[PROOFSTEP]
have : x = 0 := Subsingleton.elim _ _
[GOAL]
case refine'_1.h
V : SemiNormedGroupCat
inst✝ : Subsingleton ↑V
X : SemiNormedGroupCat
f : V ⟶ X
x : ↑V
this : x = 0
⊢ ↑f x = ↑default x
[PROOFSTEP]
simp only [this, map_zero]
[GOAL]
case refine'_2
V : SemiNormedGroupCat
inst✝ : Subsingleton ↑V
X : SemiNormedGroupCat
f : X ⟶ V
⊢ f = default
[PROOFSTEP]
ext
[GOAL]
case refine'_2.h
V : SemiNormedGroupCat
inst✝ : Subsingleton ↑V
X : SemiNormedGroupCat
f : X ⟶ V
x✝ : ↑X
⊢ ↑f x✝ = ↑default x✝
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
V W : SemiNormedGroupCat
i : V ≅ W
h1 : NormedAddGroupHom.NormNoninc i.hom
h2 : NormedAddGroupHom.NormNoninc i.inv
⊢ Isometry ↑i.hom
[PROOFSTEP]
apply AddMonoidHomClass.isometry_of_norm
[GOAL]
case a
V W : SemiNormedGroupCat
i : V ≅ W
h1 : NormedAddGroupHom.NormNoninc i.hom
h2 : NormedAddGroupHom.NormNoninc i.inv
⊢ ∀ (x : ↑V), ‖↑i.hom x‖ = ‖x‖
[PROOFSTEP]
intro v
[GOAL]
case a
V W : SemiNormedGroupCat
i : V ≅ W
h1 : NormedAddGroupHom.NormNoninc i.hom
h2 : NormedAddGroupHom.NormNoninc i.inv
v : ↑V
⊢ ‖↑i.hom v‖ = ‖v‖
[PROOFSTEP]
apply le_antisymm (h1 v)
[GOAL]
case a
V W : SemiNormedGroupCat
i : V ≅ W
h1 : NormedAddGroupHom.NormNoninc i.hom
h2 : NormedAddGroupHom.NormNoninc i.inv
v : ↑V
⊢ ‖v‖ ≤ ‖↑i.hom v‖
[PROOFSTEP]
calc
  ‖v‖ = ‖i.inv (i.hom v)‖ := by rw [Iso.hom_inv_id_apply]
  _ ≤ ‖i.hom v‖ := h2 _
[GOAL]
V W : SemiNormedGroupCat
i : V ≅ W
h1 : NormedAddGroupHom.NormNoninc i.hom
h2 : NormedAddGroupHom.NormNoninc i.inv
v : ↑V
⊢ ‖v‖ = ‖↑i.inv (↑i.hom v)‖
[PROOFSTEP]
rw [Iso.hom_inv_id_apply]
[GOAL]
M N : SemiNormedGroupCat
f : M ≅ N
i : NormedAddGroupHom.NormNoninc f.hom
i' : NormedAddGroupHom.NormNoninc f.inv
⊢ mkHom f.hom i ≫ mkHom f.inv i' = 𝟙 (of ↑M)
[PROOFSTEP]
apply Subtype.eq
[GOAL]
case a
M N : SemiNormedGroupCat
f : M ≅ N
i : NormedAddGroupHom.NormNoninc f.hom
i' : NormedAddGroupHom.NormNoninc f.inv
⊢ ↑(mkHom f.hom i ≫ mkHom f.inv i') = ↑(𝟙 (of ↑M))
[PROOFSTEP]
exact f.hom_inv_id
[GOAL]
M N : SemiNormedGroupCat
f : M ≅ N
i : NormedAddGroupHom.NormNoninc f.hom
i' : NormedAddGroupHom.NormNoninc f.inv
⊢ mkHom f.inv i' ≫ mkHom f.hom i = 𝟙 (of ↑N)
[PROOFSTEP]
apply Subtype.eq
[GOAL]
case a
M N : SemiNormedGroupCat
f : M ≅ N
i : NormedAddGroupHom.NormNoninc f.hom
i' : NormedAddGroupHom.NormNoninc f.inv
⊢ ↑(mkHom f.inv i' ≫ mkHom f.hom i) = ↑(𝟙 (of ↑N))
[PROOFSTEP]
exact f.inv_hom_id
[GOAL]
V : SemiNormedGroupCat₁
inst✝ : Subsingleton ↑V
⊢ Limits.IsZero V
[PROOFSTEP]
refine' ⟨fun X => ⟨⟨⟨0⟩, fun f => _⟩⟩, fun X => ⟨⟨⟨0⟩, fun f => _⟩⟩⟩
[GOAL]
case refine'_1
V : SemiNormedGroupCat₁
inst✝ : Subsingleton ↑V
X : SemiNormedGroupCat₁
f : V ⟶ X
⊢ f = default
[PROOFSTEP]
ext x
[GOAL]
case refine'_1.w.h
V : SemiNormedGroupCat₁
inst✝ : Subsingleton ↑V
X : SemiNormedGroupCat₁
f : V ⟶ X
x : ↑V
⊢ ↑f x = ↑default x
[PROOFSTEP]
have : x = 0 := Subsingleton.elim _ _
[GOAL]
case refine'_1.w.h
V : SemiNormedGroupCat₁
inst✝ : Subsingleton ↑V
X : SemiNormedGroupCat₁
f : V ⟶ X
x : ↑V
this : x = 0
⊢ ↑f x = ↑default x
[PROOFSTEP]
simp only [this, map_zero]
[GOAL]
case refine'_2
V : SemiNormedGroupCat₁
inst✝ : Subsingleton ↑V
X : SemiNormedGroupCat₁
f : X ⟶ V
⊢ f = default
[PROOFSTEP]
ext
[GOAL]
case refine'_2.w.h
V : SemiNormedGroupCat₁
inst✝ : Subsingleton ↑V
X : SemiNormedGroupCat₁
f : X ⟶ V
x✝ : ↑X
⊢ ↑f x✝ = ↑default x✝
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
V W : SemiNormedGroupCat₁
i : V ≅ W
⊢ Isometry ↑i.hom
[PROOFSTEP]
change Isometry (⟨⟨i.hom, map_zero _⟩, fun _ _ => map_add _ _ _⟩ : V →+ W)
[GOAL]
V W : SemiNormedGroupCat₁
i : V ≅ W
⊢ Isometry
    ↑{ toZeroHom := { toFun := ↑i.hom, map_zero' := (_ : ↑i.hom 0 = 0) },
        map_add' := (_ : ∀ (x x_1 : ↑V), ↑i.hom (x + x_1) = ↑i.hom x + ↑i.hom x_1) }
[PROOFSTEP]
refine' AddMonoidHomClass.isometry_of_norm _ _
[GOAL]
V W : SemiNormedGroupCat₁
i : V ≅ W
⊢ ∀ (x : ↑V),
    ‖↑{ toZeroHom := { toFun := ↑i.hom, map_zero' := (_ : ↑i.hom 0 = 0) },
              map_add' := (_ : ∀ (x x_1 : ↑V), ↑i.hom (x + x_1) = ↑i.hom x + ↑i.hom x_1) }
          x‖ =
      ‖x‖
[PROOFSTEP]
intro v
[GOAL]
V W : SemiNormedGroupCat₁
i : V ≅ W
v : ↑V
⊢ ‖↑{ toZeroHom := { toFun := ↑i.hom, map_zero' := (_ : ↑i.hom 0 = 0) },
            map_add' := (_ : ∀ (x x_1 : ↑V), ↑i.hom (x + x_1) = ↑i.hom x + ↑i.hom x_1) }
        v‖ =
    ‖v‖
[PROOFSTEP]
apply le_antisymm (i.hom.2 v)
[GOAL]
V W : SemiNormedGroupCat₁
i : V ≅ W
v : ↑V
⊢ ‖v‖ ≤ ‖↑↑i.hom v‖
[PROOFSTEP]
calc
  ‖v‖ = ‖i.inv (i.hom v)‖ := by rw [Iso.hom_inv_id_apply]
  _ ≤ ‖i.hom v‖ := i.inv.2 _
[GOAL]
V W : SemiNormedGroupCat₁
i : V ≅ W
v : ↑V
⊢ ‖v‖ = ‖↑i.inv (↑i.hom v)‖
[PROOFSTEP]
rw [Iso.hom_inv_id_apply]


[GOAL]
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
G' : Type u_5
inst✝⁵ : NormedAddCommGroup G'
inst✝⁴ : NormedSpace 𝕜 G'
f✝ f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
𝕜' : Type u_6
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : E → 𝕜'
c' : E →L[𝕜] 𝕜'
hc : HasStrictFDerivAt c c' x
f : F
⊢ HasStrictFDerivAt (fun y => c y • f) (smulRight c' f) x
[PROOFSTEP]
simpa only [smul_zero, zero_add] using hc.smul (hasStrictFDerivAt_const f x)
[GOAL]
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
G' : Type u_5
inst✝⁵ : NormedAddCommGroup G'
inst✝⁴ : NormedSpace 𝕜 G'
f✝ f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
𝕜' : Type u_6
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : E → 𝕜'
c' : E →L[𝕜] 𝕜'
hc : HasFDerivWithinAt c c' s x
f : F
⊢ HasFDerivWithinAt (fun y => c y • f) (smulRight c' f) s x
[PROOFSTEP]
simpa only [smul_zero, zero_add] using hc.smul (hasFDerivWithinAt_const f x s)
[GOAL]
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
G' : Type u_5
inst✝⁵ : NormedAddCommGroup G'
inst✝⁴ : NormedSpace 𝕜 G'
f✝ f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
𝕜' : Type u_6
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : E → 𝕜'
c' : E →L[𝕜] 𝕜'
hc : HasFDerivAt c c' x
f : F
⊢ HasFDerivAt (fun y => c y • f) (smulRight c' f) x
[PROOFSTEP]
simpa only [smul_zero, zero_add] using hc.smul (hasFDerivAt_const f x)
[GOAL]
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
G' : Type u_5
inst✝⁵ : NormedAddCommGroup G'
inst✝⁴ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
𝔸 : Type u_6
𝔸' : Type u_7
inst✝³ : NormedRing 𝔸
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸'
a b : E → 𝔸
a' b' : E →L[𝕜] 𝔸
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasStrictFDerivAt c c' x
hd : HasStrictFDerivAt d d' x
⊢ HasStrictFDerivAt (fun y => c y * d y) (c x • d' + d x • c') x
[PROOFSTEP]
convert hc.mul' hd
[GOAL]
case h.e'_10.h.e'_6
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
G' : Type u_5
inst✝⁵ : NormedAddCommGroup G'
inst✝⁴ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
𝔸 : Type u_6
𝔸' : Type u_7
inst✝³ : NormedRing 𝔸
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸'
a b : E → 𝔸
a' b' : E →L[𝕜] 𝔸
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasStrictFDerivAt c c' x
hd : HasStrictFDerivAt d d' x
⊢ d x • c' = smulRight c' (d x)
[PROOFSTEP]
ext z
[GOAL]
case h.e'_10.h.e'_6.h
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
G' : Type u_5
inst✝⁵ : NormedAddCommGroup G'
inst✝⁴ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
𝔸 : Type u_6
𝔸' : Type u_7
inst✝³ : NormedRing 𝔸
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸'
a b : E → 𝔸
a' b' : E →L[𝕜] 𝔸
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasStrictFDerivAt c c' x
hd : HasStrictFDerivAt d d' x
z : E
⊢ ↑(d x • c') z = ↑(smulRight c' (d x)) z
[PROOFSTEP]
apply mul_comm
[GOAL]
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
G' : Type u_5
inst✝⁵ : NormedAddCommGroup G'
inst✝⁴ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
𝔸 : Type u_6
𝔸' : Type u_7
inst✝³ : NormedRing 𝔸
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸'
a b : E → 𝔸
a' b' : E →L[𝕜] 𝔸
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivWithinAt c c' s x
hd : HasFDerivWithinAt d d' s x
⊢ HasFDerivWithinAt (fun y => c y * d y) (c x • d' + d x • c') s x
[PROOFSTEP]
convert hc.mul' hd
[GOAL]
case h.e'_10.h.e'_6
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
G' : Type u_5
inst✝⁵ : NormedAddCommGroup G'
inst✝⁴ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
𝔸 : Type u_6
𝔸' : Type u_7
inst✝³ : NormedRing 𝔸
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸'
a b : E → 𝔸
a' b' : E →L[𝕜] 𝔸
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivWithinAt c c' s x
hd : HasFDerivWithinAt d d' s x
⊢ d x • c' = smulRight c' (d x)
[PROOFSTEP]
ext z
[GOAL]
case h.e'_10.h.e'_6.h
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
G' : Type u_5
inst✝⁵ : NormedAddCommGroup G'
inst✝⁴ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
𝔸 : Type u_6
𝔸' : Type u_7
inst✝³ : NormedRing 𝔸
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸'
a b : E → 𝔸
a' b' : E →L[𝕜] 𝔸
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivWithinAt c c' s x
hd : HasFDerivWithinAt d d' s x
z : E
⊢ ↑(d x • c') z = ↑(smulRight c' (d x)) z
[PROOFSTEP]
apply mul_comm
[GOAL]
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
G' : Type u_5
inst✝⁵ : NormedAddCommGroup G'
inst✝⁴ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
𝔸 : Type u_6
𝔸' : Type u_7
inst✝³ : NormedRing 𝔸
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸'
a b : E → 𝔸
a' b' : E →L[𝕜] 𝔸
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivAt c c' x
hd : HasFDerivAt d d' x
⊢ HasFDerivAt (fun y => c y * d y) (c x • d' + d x • c') x
[PROOFSTEP]
convert hc.mul' hd
[GOAL]
case h.e'_10.h.e'_6
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
G' : Type u_5
inst✝⁵ : NormedAddCommGroup G'
inst✝⁴ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
𝔸 : Type u_6
𝔸' : Type u_7
inst✝³ : NormedRing 𝔸
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸'
a b : E → 𝔸
a' b' : E →L[𝕜] 𝔸
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivAt c c' x
hd : HasFDerivAt d d' x
⊢ d x • c' = smulRight c' (d x)
[PROOFSTEP]
ext z
[GOAL]
case h.e'_10.h.e'_6.h
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
G' : Type u_5
inst✝⁵ : NormedAddCommGroup G'
inst✝⁴ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
𝔸 : Type u_6
𝔸' : Type u_7
inst✝³ : NormedRing 𝔸
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸'
a b : E → 𝔸
a' b' : E →L[𝕜] 𝔸
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivAt c c' x
hd : HasFDerivAt d d' x
z : E
⊢ ↑(d x • c') z = ↑(smulRight c' (d x)) z
[PROOFSTEP]
apply mul_comm
[GOAL]
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
G' : Type u_5
inst✝⁵ : NormedAddCommGroup G'
inst✝⁴ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
𝔸 : Type u_6
𝔸' : Type u_7
inst✝³ : NormedRing 𝔸
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸'
a b : E → 𝔸
a' b' : E →L[𝕜] 𝔸
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
ha : DifferentiableWithinAt 𝕜 a s x
⊢ DifferentiableWithinAt 𝕜 (fun x => a x ^ 0) s x
[PROOFSTEP]
simp only [pow_zero, differentiableWithinAt_const]
[GOAL]
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
G' : Type u_5
inst✝⁵ : NormedAddCommGroup G'
inst✝⁴ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
𝔸 : Type u_6
𝔸' : Type u_7
inst✝³ : NormedRing 𝔸
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸'
a b : E → 𝔸
a' b' : E →L[𝕜] 𝔸
c d : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
ha : DifferentiableWithinAt 𝕜 a s x
n : ℕ
⊢ DifferentiableWithinAt 𝕜 (fun x => a x ^ (n + 1)) s x
[PROOFSTEP]
simp only [pow_succ, DifferentiableWithinAt.pow ha n, ha.mul]
[GOAL]
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
G' : Type u_5
inst✝⁵ : NormedAddCommGroup G'
inst✝⁴ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
𝔸 : Type u_6
𝔸' : Type u_7
inst✝³ : NormedRing 𝔸
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸'
a b : E → 𝔸
a' b' : E →L[𝕜] 𝔸
c d✝ : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasStrictFDerivAt c c' x
d : 𝔸'
⊢ HasStrictFDerivAt (fun y => c y * d) (d • c') x
[PROOFSTEP]
convert hc.mul_const' d
[GOAL]
case h.e'_10
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
G' : Type u_5
inst✝⁵ : NormedAddCommGroup G'
inst✝⁴ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
𝔸 : Type u_6
𝔸' : Type u_7
inst✝³ : NormedRing 𝔸
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸'
a b : E → 𝔸
a' b' : E →L[𝕜] 𝔸
c d✝ : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasStrictFDerivAt c c' x
d : 𝔸'
⊢ d • c' = smulRight c' d
[PROOFSTEP]
ext z
[GOAL]
case h.e'_10.h
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
G' : Type u_5
inst✝⁵ : NormedAddCommGroup G'
inst✝⁴ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
𝔸 : Type u_6
𝔸' : Type u_7
inst✝³ : NormedRing 𝔸
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸'
a b : E → 𝔸
a' b' : E →L[𝕜] 𝔸
c d✝ : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasStrictFDerivAt c c' x
d : 𝔸'
z : E
⊢ ↑(d • c') z = ↑(smulRight c' d) z
[PROOFSTEP]
apply mul_comm
[GOAL]
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
G' : Type u_5
inst✝⁵ : NormedAddCommGroup G'
inst✝⁴ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
𝔸 : Type u_6
𝔸' : Type u_7
inst✝³ : NormedRing 𝔸
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸'
a b : E → 𝔸
a' b' : E →L[𝕜] 𝔸
c d✝ : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivWithinAt c c' s x
d : 𝔸'
⊢ HasFDerivWithinAt (fun y => c y * d) (d • c') s x
[PROOFSTEP]
convert hc.mul_const' d
[GOAL]
case h.e'_10
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
G' : Type u_5
inst✝⁵ : NormedAddCommGroup G'
inst✝⁴ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
𝔸 : Type u_6
𝔸' : Type u_7
inst✝³ : NormedRing 𝔸
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸'
a b : E → 𝔸
a' b' : E →L[𝕜] 𝔸
c d✝ : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivWithinAt c c' s x
d : 𝔸'
⊢ d • c' = smulRight c' d
[PROOFSTEP]
ext z
[GOAL]
case h.e'_10.h
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
G' : Type u_5
inst✝⁵ : NormedAddCommGroup G'
inst✝⁴ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
𝔸 : Type u_6
𝔸' : Type u_7
inst✝³ : NormedRing 𝔸
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸'
a b : E → 𝔸
a' b' : E →L[𝕜] 𝔸
c d✝ : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivWithinAt c c' s x
d : 𝔸'
z : E
⊢ ↑(d • c') z = ↑(smulRight c' d) z
[PROOFSTEP]
apply mul_comm
[GOAL]
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
G' : Type u_5
inst✝⁵ : NormedAddCommGroup G'
inst✝⁴ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
𝔸 : Type u_6
𝔸' : Type u_7
inst✝³ : NormedRing 𝔸
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸'
a b : E → 𝔸
a' b' : E →L[𝕜] 𝔸
c d✝ : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivAt c c' x
d : 𝔸'
⊢ HasFDerivAt (fun y => c y * d) (d • c') x
[PROOFSTEP]
convert hc.mul_const' d
[GOAL]
case h.e'_10
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
G' : Type u_5
inst✝⁵ : NormedAddCommGroup G'
inst✝⁴ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
𝔸 : Type u_6
𝔸' : Type u_7
inst✝³ : NormedRing 𝔸
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸'
a b : E → 𝔸
a' b' : E →L[𝕜] 𝔸
c d✝ : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivAt c c' x
d : 𝔸'
⊢ d • c' = smulRight c' d
[PROOFSTEP]
ext z
[GOAL]
case h.e'_10.h
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁷ : NormedAddCommGroup G
inst✝⁶ : NormedSpace 𝕜 G
G' : Type u_5
inst✝⁵ : NormedAddCommGroup G'
inst✝⁴ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
𝔸 : Type u_6
𝔸' : Type u_7
inst✝³ : NormedRing 𝔸
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸'
a b : E → 𝔸
a' b' : E →L[𝕜] 𝔸
c d✝ : E → 𝔸'
c' d' : E →L[𝕜] 𝔸'
hc : HasFDerivAt c c' x
d : 𝔸'
z : E
⊢ ↑(d • c') z = ↑(smulRight c' d) z
[PROOFSTEP]
apply mul_comm
[GOAL]
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
G' : Type u_5
inst✝⁴ : NormedAddCommGroup G'
inst✝³ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x✝ : E
s t : Set E
L L₁ L₂ : Filter E
R : Type u_6
inst✝² : NormedRing R
inst✝¹ : NormedAlgebra 𝕜 R
inst✝ : CompleteSpace R
x : Rˣ
this : (fun t => Ring.inverse (↑x + t) - ↑x⁻¹ + ↑x⁻¹ * t * ↑x⁻¹) =o[𝓝 0] _root_.id
⊢ HasFDerivAt Ring.inverse (-↑(↑(mulLeftRight 𝕜 R) ↑x⁻¹) ↑x⁻¹) ↑x
[PROOFSTEP]
simpa [hasFDerivAt_iff_isLittleO_nhds_zero] using this
[GOAL]
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
G' : Type u_5
inst✝⁴ : NormedAddCommGroup G'
inst✝³ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x✝ : E
s t : Set E
L L₁ L₂ : Filter E
R : Type u_6
inst✝² : NormedDivisionRing R
inst✝¹ : NormedAlgebra 𝕜 R
inst✝ : CompleteSpace R
x : R
hx : x ≠ 0
⊢ HasFDerivAt Inv.inv (-↑(↑(mulLeftRight 𝕜 R) x⁻¹) x⁻¹) x
[PROOFSTEP]
simpa using hasFDerivAt_ring_inverse (Units.mk0 _ hx)
[GOAL]
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
G' : Type u_5
inst✝⁴ : NormedAddCommGroup G'
inst✝³ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x✝ : E
s✝ t : Set E
L L₁ L₂ : Filter E
R : Type u_6
inst✝² : NormedDivisionRing R
inst✝¹ : NormedAlgebra 𝕜 R
inst✝ : CompleteSpace R
s : Set R
x : R
hx : x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderivWithin 𝕜 (fun x => x⁻¹) s x = -↑(↑(mulLeftRight 𝕜 R) x⁻¹) x⁻¹
[PROOFSTEP]
rw [DifferentiableAt.fderivWithin (differentiableAt_inv' hx) hxs]
[GOAL]
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁸ : NormedAddCommGroup F
inst✝⁷ : NormedSpace 𝕜 F
G : Type u_4
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
G' : Type u_5
inst✝⁴ : NormedAddCommGroup G'
inst✝³ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x✝ : E
s✝ t : Set E
L L₁ L₂ : Filter E
R : Type u_6
inst✝² : NormedDivisionRing R
inst✝¹ : NormedAlgebra 𝕜 R
inst✝ : CompleteSpace R
s : Set R
x : R
hx : x ≠ 0
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ fderiv 𝕜 Inv.inv x = -↑(↑(mulLeftRight 𝕜 R) x⁻¹) x⁻¹
[PROOFSTEP]
exact fderiv_inv' hx