mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.CStarAlgebra.PositiveLinearMap

Goal state before:
pp: B₁ : Type u_3
B₂ : Type u_4
inst✝⁵ : CStarAlgebra B₁
inst✝⁴ : CStarAlgebra B₂
inst✝³ : PartialOrder B₁
inst✝² : PartialOrder B₂
inst✝¹ : StarOrderedRing B₁
inst✝ : StarOrderedRing B₂
f : B₁ →ₚ[ℂ] B₂
x : B₁
hx : 0 ≤ x
h : ‖‖x‖‖ = ‖x‖
⊢ ‖f x‖ ≤ ‖‖x‖‖ * ‖f 1‖

Tactic:
← norm_smul ‖x‖ (f 1)

Goal state after:
B₁ : Type u_3
B₂ : Type u_4
inst✝⁵ : CStarAlgebra B₁
inst✝⁴ : CStarAlgebra B₂
inst✝³ : PartialOrder B₁
inst✝² : PartialOrder B₂
inst✝¹ : StarOrderedRing B₁
inst✝ : StarOrderedRing B₂
f : B₁ →ₚ[ℂ] B₂
x : B₁
hx : 0 ≤ x
h : ‖‖x‖‖ = ‖x‖
⊢ ‖f x‖ ≤ ‖‖x‖ • f 1‖
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: A : Type u_2
inst✝¹² : NonUnitalNormedRing A
inst✝¹¹ : StarRing A
inst✝¹⁰ : NormedSpace ℝ A
inst✝⁹ : IsScalarTower ℝ A A
inst✝⁸ : SMulCommClass ℝ A A
inst✝⁷ : ContinuousStar A
inst✝⁶ : NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : PartialOrder A
inst✝⁴ : StarOrderedRing A
inst✝³ : NonnegSpectrumClass ℝ A
inst✝² : T2Space A
inst✝¹ : IsSemitopologicalRing A
inst✝ : CompleteSpace A
s : Set ℝ≥0
⊢ ContinuousOn (fun fa ↦ cfcₙ ((toFun {s}) fa.1) fa.2)
    ({f | ContinuousOn ((toFun {t | IsCompact t ∧ t ⊆ s}) f) s ∧ f 0 = 0} ×ˢ {a | 0 ≤ a ∧ s ∈ 𝓝ˢ (quasispectrum ℝ≥0 a)})

Tactic:
refine continuousOn_of_locally_continuousOn fun (f, a) ⟨hf, ha, has⟩ ↦ ?_
  have hs := NonUnitalContinuousFunctionalCalculus.isCompact_quasispectrum (R := ℝ≥0) a
  obtain ⟨k, ⟨hka, hk⟩, hks⟩ := hs.nhdsSet_basis_isCompact.mem_iff.mp has
  have := (upperHemicontinuous_quasispectrum_nnreal A).isOpen k
  refine ⟨Set.univ ×ˢ {x | k ∈ 𝓝ˢ (quasispectrum ℝ≥0 x)}, isOpen_univ.prod this, by simpa, ?_⟩
  conv in cfcₙ _ =>
    equals cfcₙ (toFun {k} (ofFun {k} (toFun {t | IsCompact t ∧ t ⊆ s} fa.1))) => rfl
  refine continuousOn_cfcₙ_nnreal_setProd hk |>.comp'
    (uniformContinuous_ofFun_toFun_of_mem _ {t | IsCompact t ∧ t ⊆ s} _ ⟨hk, hks⟩ |>.prodMap
      uniformContinuous_id).continuous.continuousOn ?_
  intro (f, a) ⟨⟨hf, ha⟩, ⟨_, ha'⟩⟩
  exact ⟨⟨hf.1.mono hks, hf.2⟩, ha.1, subset_of_mem_nhdsSet ha'⟩

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Type u_5
B : Type u_6
inst✝¹ : Fintype m
inst✝ : NonUnitalCStarAlgebra A
M₁ M₂ : CStarMatrix m n A
⊢ { toFun := ⇑(WithCStarModule.equivL ℂ).symm ∘ (fun v ↦ v ᵥ* (M₁ + M₂)) ∘ ⇑(WithCStarModule.equivL ℂ), map_add' := ⋯,
      map_smul' := ⋯, cont := ⋯ } =
    { toFun := ⇑(WithCStarModule.equivL ℂ).symm ∘ (fun v ↦ v ᵥ* M₁) ∘ ⇑(WithCStarModule.equivL ℂ), map_add' := ⋯,
        map_smul' := ⋯, cont := ⋯ } +
      { toFun := ⇑(WithCStarModule.equivL ℂ).symm ∘ (fun v ↦ v ᵥ* M₂) ∘ ⇑(WithCStarModule.equivL ℂ), map_add' := ⋯,
        map_smul' := ⋯, cont := ⋯ }

Tactic:
by
    ext
    simp only [ContinuousLinearMap.coe_mk', LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply,
      WithCStarModule.equivL_apply, WithCStarModule.equivL_symm_apply,
      WithCStarModule.equiv_symm_pi_apply, _root_.add_apply, WithCStarModule.add_apply]
    rw [Matrix.vecMul_add, Pi.add_apply]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: m : Type u_1
n : Type u_2
A : Type u_5
inst✝⁴ : Fintype m
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype n
M₁ M₂ : CStarMatrix m n A
⊢ ‖M₁ + M₂‖ ≤ ‖M₁‖ + ‖M₂‖

Tactic:
simpa [← map_add] using! norm_add_le (toCLM M₁) (toCLM M₂)

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.CStarMatrix

Goal state before:
pp: case refine_2
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
⊢ Filter.comap (⇑ofMatrix.symm) (cobounded (Matrix m n A)) ≤ cobounded (CStarMatrix m n A)

Tactic:
exact lipschitzWith_toMatrixAux.comap_cobounded_le

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁸ : RCLike 𝕜
inst✝⁷ : MeasurableSpace X
μ : Measure X
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : IsScalarTower 𝕜 A A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus 𝕜 A p
inst✝ : CompleteSpace A
f : X → 𝕜 → 𝕜
a : A
hf : Integrable (fun x ↦ mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) μ
ha : p a
⊢ Integrable (fun x ↦ cfcₙ (f x) a) μ

Tactic:
conv in cfcₙ _ _ => rw [cfcₙ_eq_cfcₙL_mkD _ a]
  exact cfcₙL_integrable _ _ hf ha

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart

Goal state before:
pp: A : Type u_1
inst✝⁷ : TopologicalSpace A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : Algebra ℂ A
inst✝³ : StarModule ℂ A
inst✝² : ContinuousFunctionalCalculus ℂ A IsStarNormal
inst✝¹ : ContinuousMap.UniqueHom ℂ A
inst✝ : T2Space A
f : ℝ → ℝ
a : A
hf : ContinuousOn f (spectrum ℝ ↑(ℑ a))
ha : IsStarNormal a
⊢ cfc (fun x ↦ ↑(f x.im)) a = cfc f ↑(ℑ a)

Tactic:
by
  have : ContinuousOn (fun x ↦ (f x.re) : ℂ → ℂ) ((im · : ℂ → ℂ) '' spectrum ℂ a) := by
    rw [spectrum_imaginaryPart' a] at hf
    refine continuous_ofReal.comp_continuousOn <| hf.comp (by fun_prop) ?_
    simpa [Set.mapsTo_image_iff, Function.comp_def] using Set.mapsTo_image ..
  conv_rhs =>
    rw [cfc_real_eq_complex, ← cfc_im_id a, ← cfc_comp' ..]
    simp

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal

Goal state before:
pp: A : Type u_2
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : A →ₚ[ℂ] ℂ
b : f.GNS
⊢ (f.gnsNonUnitalStarAlgHom 1) b = 1 b

Tactic:
induction b using induction_on with

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal

Goal state before:
pp: A✝ : Type u_1
inst✝⁵ : NonUnitalCStarAlgebra A✝
inst✝⁴ : PartialOrder A✝
f✝ : A✝ →ₚ[ℂ] ℂ
inst✝³ : StarOrderedRing A✝
A : Type u_2
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : A →ₚ[ℂ] ℂ
r : ℂ
⊢ f.gnsNonUnitalStarAlgHom.toFun ((algebraMap ℂ A) r) = (algebraMap ℂ (f.GNS →L[ℂ] f.GNS)) r

Tactic:
by simp [Algebra.algebraMap_eq_smul_one]

Goal state after:
Module: Mathlib.Analysis.Normed.Field.UnitBall

Goal state before:
pp: 𝕜✝ : Type u_1
𝕜 : Type u_2
inst✝ : NonUnitalSeminormedRing 𝕜
a✝ b✝ : 𝕜
hx : a✝ ∈ closedBall 0 1
hy : b✝ ∈ closedBall 0 1
⊢ a✝ * b✝ ∈ closedBall 0 1

Tactic:
rw [mem_closedBall_zero_iff] at *
    exact (norm_mul_le _ _).trans (mul_le_one₀ hx (norm_nonneg _) hy)

Goal state after:
Module: Mathlib.Data.Bundle

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
x x' : B
h : x = x'
b : E x
⊢ mk' F x' (cast ⋯ b) = { proj := x, snd := b }

Tactic:
by subst h; rfl

Goal state after:
Module: Mathlib.Topology.OpenPartialHomeomorph.Composition

Goal state before:
pp: case refine_1.e_a
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
hs' : IsOpen[inst✝] (↑e '' s)
hs'' : s ⊆ e.source
x : X
hx : x ∈ s
y : X
hy : y ∈ e.source
h : ↑e x = ↑e y
⊢ x = ↑e.symm (↑e y)

Tactic:
← left_inv e (hs'' hx),

Goal state after:
case refine_1.e_a
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
hs' : IsOpen[inst✝] (↑e '' s)
hs'' : s ⊆ e.source
x : X
hx : x ∈ s
y : X
hy : y ∈ e.source
h : ↑e x = ↑e y
⊢ ↑e.symm (↑e x) = ↑e.symm (↑e y)
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: X✝ : Type u_1
X'✝ : Type u_2
Y : Type u_3
Y' : Type u_4
Z✝ : Type u_5
Z' : Type u_6
inst✝⁹ : TopologicalSpace X✝
inst✝⁸ : TopologicalSpace X'✝
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : TopologicalSpace Y'
inst✝⁵ : TopologicalSpace Z✝
inst✝⁴ : TopologicalSpace Z'
e✝ : OpenPartialHomeomorph X✝ Y
X : Type u_7
X' : Type u_8
Z : Type u_9
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Z
inst✝ : Nonempty Z
f : X → X'
e : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
⊢ ContinuousOn (extend f ↑e fun x ↦ Classical.arbitrary Z) (f '' e.source)

Tactic:
by
    by_cases Nonempty X; swap
    · intro x hx; simp_all
    set F := (extend f e (fun _ ↦ (Classical.arbitrary Z))) with F_eq
    have heq : EqOn F (e ∘ (hf.toOpenPartialHomeomorph).symm) (f '' e.source) := by
      intro x ⟨x₀, hx₀, hxx₀⟩
      rw [← hxx₀, F_eq, hf.injective.extend_apply e, comp_apply,
        hf.toOpenPartialHomeomorph_left_inv]
    have : ContinuousOn (e ∘ (hf.toOpenPartialHomeomorph).symm) (f '' e.source) := by
      apply e.continuousOn_toFun.comp; swap
      · intro x' ⟨x, hx, hx'x⟩
        rw [← hx'x, hf.toOpenPartialHomeomorph_left_inv]; exact hx
      have : ContinuousOn (hf.toOpenPartialHomeomorph).symm (f '' univ) :=
        (hf.toOpenPartialHomeomorph).continuousOn_invFun
      exact this.mono <| image_mono <| subset_univ _
    exact ContinuousOn.congr this heq

Goal state after:
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj✝ : Z → B
e✝ : Pretrivialization F proj✝
x : Z
e' : Pretrivialization F TotalSpace.proj
b : B
y : E b
s : Set B
hs : IsOpen[inst✝²] s
proj : Z → ↑s
e : Pretrivialization F proj
inst✝ : Nonempty (B → F → Z)
z : Z
hz : z ∈ e.source
⊢ (if h : (↑(↑e z).1, (↑e z).2).1 ∈ s then e.invFun (⟨(↑(↑e z).1, (↑e z).2).1, h⟩, (↑(↑e z).1, (↑e z).2).2)
    else Classical.arbitrary (B → F → Z) (↑(↑e z).1, (↑e z).2).1 (↑(↑e z).1, (↑e z).2).2) =
    z

Tactic:
simpa using e.left_inv hz

Goal state after:
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
f : E → X
s : Set X
hf : IsCoveringMapOn f s
⊢ IsLocalHomeomorphOn f (f ⁻¹' s)

Tactic:
by
  refine IsLocalHomeomorphOn.mk f (f ⁻¹' s) fun x hx ↦ ?_
  have : Nonempty (f ⁻¹' {f x}) := ⟨⟨x, rfl⟩⟩
  let e := (hf (f x) hx).toTrivialization
  have h := (hf (f x) hx).mem_toTrivialization_baseSet
  let he := e.mem_source.2 h
  refine
    ⟨e.toOpenPartialHomeomorph.trans
        { toFun := fun p => p.1
          invFun := fun p => ⟨p, x, rfl⟩
          source := e.baseSet ×ˢ ({⟨x, rfl⟩} : Set (f ⁻¹' {f x}))
          target := e.baseSet
          open_source :=
            e.open_baseSet.prod (discreteTopology_iff_isOpen_singleton.1 (hf (f x) hx).1 ⟨x, rfl⟩)
          open_target := e.open_baseSet
          map_source' := fun p => And.left
          map_target' := fun p hp => ⟨hp, rfl⟩
          left_inv' := fun p hp => Prod.ext rfl hp.2.symm
          right_inv' := fun p _ => rfl
          continuousOn_toFun := continuousOn_fst
          continuousOn_invFun := by fun_prop },
      ⟨he, by rwa [e.toOpenPartialHomeomorph.symm_symm, e.proj_toFun x he],
        (hf (f x) hx).toTrivialization_apply⟩,
      fun p h => (e.proj_toFun p h.1).symm⟩

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: s : Set ℝ
hs : ∀ x ∈ s, ∀ y ∈ s, x - y ∈ Ioo (-2 * π) (2 * π)
t₁ : ℝ
ht₁ : t₁ ∈ s
t₂ : ℝ
ht₂ : t₂ ∈ s
h1 : -(2 * π) < t₁ - t₂
h2 : t₁ - t₂ < 2 * π
heq : cexp ((↑t₁ - ↑t₂) * I) = 1
⊢ (cexp (↑(t₁ - t₂) * I)).re = 1

Tactic:
← ofReal_sub,

Goal state after:
s : Set ℝ
hs : ∀ x ∈ s, ∀ y ∈ s, x - y ∈ Ioo (-2 * π) (2 * π)
t₁ : ℝ
ht₁ : t₁ ∈ s
t₂ : ℝ
ht₂ : t₂ ∈ s
h1 : -(2 * π) < t₁ - t₂
h2 : t₁ - t₂ < 2 * π
heq : cexp (↑(t₁ - t₂) * I) = 1
⊢ (cexp (↑(t₁ - t₂) * I)).re = 1
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: z : Circle
s : ℝ
n : ℕ
hs : s ≤ π
h1 : z ∈ centeredArc (π / ↑n)
h2 : z ^ n ∈ centeredArc s
⊢ z ∈ centeredArc (s / ↑n)

Tactic:
have hs0 : 0 < s := by
    contrapose! h2
    simp [centeredArc_eq_empty h2]
  have hn0 : n ≠ 0 := by
    contrapose! h1
    simp [h1]
  have hn : 1 ≤ (n : ℝ) := by simpa [Nat.one_le_iff_ne_zero]
  rw [mem_centeredArc ((div_le_self hs0.le hn).trans hs),
    lt_div_iff₀' (one_pos.trans_le hn)]
  rw [mem_centeredArc (div_le_self pi_nonneg hn)] at h1
  rwa [mem_centeredArc hs, coe_pow, ← arg_coe_angle_toReal_eq_arg, arg_pow_coe_angle,
    (Angle.nsmul_toReal_eq_mul hn0).mpr (mem_Ioc_of_Ioo ?_), abs_mul, Nat.abs_cast,
    arg_coe_angle_toReal_eq_arg] at h2
  rwa [neg_div, mem_Ioo, ← abs_lt, arg_coe_angle_toReal_eq_arg]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
hxy : x ≠ y
⊢ {x, y} ⊆ range ⇑(x.path y)

Tactic:
simp only [pair_subset_iff,
      (path x y).source_mem_range, (path x y).target_mem_range, and_self]

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: case mpr
A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
a✝ : Nontrivial A
z : ℂ
hz : z ∈ spectrum ℂ u
hx : IsLeast (re '' spectrum ℂ u) z.re
key : z = -↑‖z‖
hz_norm : ‖z‖ = 1
⊢ -1 ∈ spectrum ℂ u

Tactic:
hz_norm

Goal state after:
case mpr
A : Type u_1
inst✝ : CStarAlgebra A
u : A
hu : u ∈ unitary A
a✝ : Nontrivial A
z : ℂ
hz : z ∈ spectrum ℂ u
hx : IsLeast (re '' spectrum ℂ u) z.re
key : z = -↑1
hz_norm : ‖z‖ = 1
⊢ -1 ∈ spectrum ℂ u
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case H
T : ℝ
hT : T ≠ 0
z✝ : ℝ
⊢ homeomorphCircle' ((homeomorphAddCircle T (2 * π) hT homeomorphCircle._proof_1) ↑z✝) = toCircle ↑z✝

Tactic:
homeomorphAddCircle_apply_mk,

Goal state after:
case H
T : ℝ
hT : T ≠ 0
z✝ : ℝ
⊢ homeomorphCircle' ↑(z✝ * (T⁻¹ * (2 * π))) = toCircle ↑z✝
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : ‖↑u - 1‖ < 2
⊢ expUnitary (argSelfAdjoint u) = u

Tactic:
ext
  have : ContinuousOn arg (spectrum ℂ (u : A)) :=
    continuousOn_arg.mono <| (spectrum_subset_slitPlane_iff_norm_lt_two u.2).mpr hu
  rw [expUnitary_coe, argSelfAdjoint_coe, ← CFC.exp_eq_normedSpace_exp (𝕜 := ℂ),
    ← cfc_comp_smul .., ← cfc_comp' ..]
  conv_rhs => rw [← cfc_id' ℂ (u : A)]
  refine cfc_congr fun y hy ↦ ?_
  have hy₁ : ‖y‖ = 1 := spectrum.norm_eq_one_of_unitary u.2 hy
  have : I * y.arg = log y :=
    Complex.ext (by simp [log_re, spectrum.norm_eq_one_of_unitary u.2 hy]) (by simp [log_im])
  simpa [← exp_eq_exp_ℂ, this] using exp_log (by aesop)

Goal state after:
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
⊢ ContinuousOn (fun x ↦ cfc (fun x ↦ ↑x.arg) ↑x) (ball 1 2)

Tactic:
isOpen_ball.continuousOn_iff

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
⊢ ∀ ⦃a : ↥(unitary A)⦄, a ∈ ball 1 2 → ContinuousAt (fun x ↦ cfc (fun x ↦ ↑x.arg) ↑x) a
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] F
⊢ (↑T).rangeᗮ = (↑(adjoint T)).ker

Tactic:
rw [← T†.ker.orthogonal_orthogonal, T†.orthogonal_ker]
  simp

Goal state after:
Module: Mathlib.Analysis.Calculus.AbsolutelyMonotone

Goal state before:
pp: f : ℝ → ℝ
s : Set ℝ
hs : UniqueDiffOn ℝ s
hcont : ContDiffOn ℝ ∞ f s
hnn : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ iteratedDerivWithin n f s x
n : ℕ
x : ℝ
hx : x ∈ s
⊢ 0 ≤ (ftaylorSeriesWithin ℝ f s x n) fun x ↦ 1

Tactic:
exact iteratedDerivWithin_eq_iteratedFDerivWithin (𝕜 := ℝ) (f := f) (s := s) ▸ hnn n x hx

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
x : F
f : E →L[𝕜] F
⊢ (innerSL 𝕜) x ∘SL f = (innerSL 𝕜) ((adjoint f) x)

Tactic:
ext; simp [adjoint_inner_left]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
ι : Type u_5
b : Basis ι 𝕜 E
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : ∀ (i : ι) (y : F), ⟪A (b i), y⟫_𝕜 = ⟪b i, B y⟫_𝕜
i : ι
y : F
⊢ ⟪A (b i), y⟫_𝕜 = ⟪(adjoint B) (b i), y⟫_𝕜

Tactic:
simp only [h i, adjoint_inner_left]

Goal state after:
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : FiniteDimensional 𝕜 E
inst✝ : FiniteDimensional 𝕜 F
ι : Type u_5
b : Basis ι 𝕜 F
A : E →ₗ[𝕜] F
B : F →ₗ[𝕜] E
h : ∀ (i : ι) (x : E), ⟪A x, b i⟫_𝕜 = ⟪x, B (b i)⟫_𝕜
x : E
i : ι
⊢ ⟪A x, b i⟫_𝕜 = ⟪(adjoint B) x, b i⟫_𝕜

Tactic:
simp only [h i, adjoint_inner_left]

Goal state after:
Module: Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid

Goal state before:
pp: k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ s.faceOppositeCentroid i -ᵥ s.points i = (↑n + 1) • (s.faceOppositeCentroid i -ᵥ s.centroid)

Tactic:
rw [← vsub_sub_vsub_cancel_right _ (s.centroid) (s.points i),
    faceOppositeCentroid_vsub_point_eq_smul_sum_vsub, centroid_vsub_eq,
    ← sub_smul, smul_smul]

Goal state after:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁵ : DivisionRing k
inst✝⁴ : AddCommGroup V
inst✝³ : Module k V
inst✝² : AffineSpace V P
n : ℕ
inst✝¹ : NeZero n
inst✝ : CharZero k
s : Simplex k P n
i : Fin (n + 1)
⊢ (↑n)⁻¹ • ∑ x, (s.points x -ᵥ s.points i) = ((↑n + 1) * ((↑n)⁻¹ - (↑n + 1)⁻¹)) • ∑ x, (s.points x -ᵥ s.points i)
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: case mp
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₀ : P
h : p₀ ∈ s
⊢ (∃ v₀, ∀ v ∈ vectorSpan k s, ∃ r, r • v₀ = v) → ∃ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀

pp: case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₀ : P
h : p₀ ∈ s
⊢ (∃ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀) → ∃ v₀, ∀ v ∈ vectorSpan k s, ∃ r, r • v₀ = v

Tactic:
· rintro ⟨v₀, hv⟩
    use v₀
    intro p hp
    obtain ⟨r, hr⟩ := hv (p -ᵥ p₀) (vsub_mem_vectorSpan k hp h)
    use r
    rw [eq_vadd_iff_vsub_eq]
    exact hr.symm

Goal state after:
case mpr
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p₀ : P
h : p₀ ∈ s
⊢ (∃ v, ∀ p ∈ s, ∃ r, p = r • v +ᵥ p₀) → ∃ v₀, ∀ v ∈ vectorSpan k s, ∃ r, r • v₀ = v
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: case inl
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
⊢ Collinear k ∅ ↔ ∃ p₀ v, ∀ p ∈ ∅, ∃ r, p = r • v +ᵥ p₀

Tactic:
simp [collinear_empty]

Goal state after:
Module: Mathlib.Analysis.Normed.Affine.AddTorsorBases

Goal state before:
pp: V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
t : Set V
hts : t ⊆ s
b : AffineBasis ↑t ℝ V
hb : ⇑b = Subtype.val
this : (interior ((convexHull ℝ) (range ⇑b))).Nonempty
⊢ (interior ((convexHull ℝ) s)).Nonempty

Tactic:
hb,

Goal state after:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
t : Set V
hts : t ⊆ s
b : AffineBasis ↑t ℝ V
hb : ⇑b = Subtype.val
this : (interior ((convexHull ℝ) (range Subtype.val))).Nonempty
⊢ (interior ((convexHull ℝ) s)).Nonempty
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
⊢ Memℓp 0 ∞

Tactic:
apply memℓp_infty
    simp only [norm_zero, Pi.zero_apply]
    exact bddAbove_singleton.mono Set.range_const_subset

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
g : α → ℝ
hg : Summable fun i ↦ ‖g i‖ ^ p.toReal
hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖
hp : 0 < p.toReal
⊢ Summable fun i ↦ ‖f i‖ ^ p.toReal

Tactic:
apply hg.of_norm_bounded fun i ↦ ?_

Goal state after:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
g : α → ℝ
hg : Summable fun i ↦ ‖g i‖ ^ p.toReal
hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖
hp : 0 < p.toReal
i : α
⊢ ‖‖f i‖ ^ p.toReal‖ ≤ ‖g i‖ ^ p.toReal
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E ∞)
C : ℝ
hC : 0 ≤ C
hCf : ∀ (i : α), ‖↑f i‖ ≤ C
h✝ : Nonempty α
⊢ ‖f‖ ≤ C

Tactic:
exact norm_le_of_forall_le' C hCf

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inl
𝕜 : Type u_1
α : Type u_3
E : α → Type u_4
inst✝³ : (i : α) → NormedAddCommGroup (E i)
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), IsBoundedSMul 𝕜 (E i)
c : 𝕜
hp : 0 ≠ 0
f : ↥(lp E 0)
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖

Tactic:
exact absurd rfl hp

Goal state after:
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr.inl
𝕜 : Type u_1
𝕜' : Type u_2
α : Type u_3
E : α → Type u_4
q : ℝ≥0∞
inst✝² : (i : α) → NormedAddCommGroup (E i)
inst✝¹ : (i : α) → StarAddMonoid (E i)
inst✝ : ∀ (i : α), NormedStarGroup (E i)
hp : Fact (1 ≤ ∞)
f : ↥(lp E ∞)
⊢ ‖star f‖ = ‖f‖

Tactic:
simp only [lp.norm_eq_ciSup, lp.star_apply, norm_star]

Goal state after:
Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph

Goal state before:
pp: E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ (univBall c r).source = univ

Tactic:
unfold univBall

Goal state after:
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ (if h : 0 < r then univUnitBall.trans' (unitBallBall c r h) ⋯
      else (IsometryEquiv.vaddConst c).toHomeomorph.toOpenPartialHomeomorph).source =
    univ
Module: Mathlib.Analysis.Normed.Module.Ball.Homeomorph

Goal state before:
pp: E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ ↑(univBall c r) 0 = c

Tactic:
unfold univBall

Goal state after:
E : Type u_1
inst✝³ : SeminormedAddCommGroup E
inst✝² : NormedSpace ℝ E
P : Type u_2
inst✝¹ : PseudoMetricSpace P
inst✝ : NormedAddTorsor E P
c : P
r : ℝ
⊢ ↑(if h : 0 < r then univUnitBall.trans' (unitBallBall c r h) ⋯
        else (IsometryEquiv.vaddConst c).toHomeomorph.toOpenPartialHomeomorph)
      0 =
    c
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
_i : Fact (1 ≤ p)
F : ℕ → ↥(lp E p)
hF : CauchySeq F
f : ↥(lp E p)
hf : Tendsto (id fun i ↦ ↑(F i)) atTop (𝓝 ↑f)
⊢ Tendsto F atTop (𝓝 f)

Tactic:
by
  rw [Metric.nhds_basis_closedBall.tendsto_right_iff]
  intro ε hε
  have hε' : { p : lp E p × lp E p | ‖p.1 - p.2‖ < ε } ∈ uniformity (lp E p) :=
    NormedAddCommGroup.uniformity_basis_dist.mem_of_mem hε
  refine (hF.eventually_eventually hε').mono ?_
  rintro n (hn : ∀ᶠ l in atTop, ‖(fun f => F n - f) (F l)‖ < ε)
  rw [mem_closedBall_iff_norm]
  refine norm_le_of_tendsto (hn.mono fun k hk => hk.le) ?_
  rw [tendsto_pi_nhds]
  intro a
  exact (hf.apply_nhds a).const_sub (F n a)

Goal state after: