mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : Fintype l
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalSeminormedRing α
A : Matrix l m α
B : Matrix m n α
⊢ (Finset.univ.sup fun i ↦ ∑ y, ∑ x, ‖A i y‖₊ * ‖B y x‖₊) = Finset.univ.sup fun i ↦ ∑ j, ‖A i j‖₊ * ∑ k, ‖B j k‖₊

Tactic:
Finset.mul_sum

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

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁷ : RCLike 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : IsScalarTower 𝕜 A A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : ContinuousStar A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
a : X → A
a₀ : A
l : Filter X
ha_tendsto : Tendsto a l (𝓝 a₀)
ha : ∀ᶠ (x : X) in l, quasispectrum 𝕜 (a x) ⊆ s
ha' : ∀ᶠ (x : X) in l, p (a x)
ha₀ : quasispectrum 𝕜 a₀ ⊆ s
ha₀' : p a₀
hf : ContinuousOn f s
hf0 : f 0 = 0
⊢ Tendsto (fun x ↦ cfcₙ f (a x)) l (𝓝 (cfcₙ f a₀))

Tactic:
apply continuousOn_cfcₙ A hs f |>.continuousWithinAt ⟨ha₀', ha₀⟩ |>.tendsto.comp
  rw [tendsto_nhdsWithin_iff]
  exact ⟨ha_tendsto, ha'.and ha⟩

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

Goal state before:
pp: case h
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
hx : 0 ≤ x ∧ ‖x‖ < 1
⊢ (0 ≤ x ∧ ‖x‖ < 1) ∧ ∀ ⦃x_1 : A⦄, x_1 ∈ {x_2 | x ≤ x_2} ∩ closedBall 0 1 → IsSelfAdjoint x_1

Tactic:
exact ⟨hx, fun y hy ↦ (hx.1.trans hy.1).isSelfAdjoint⟩

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

Goal state before:
pp: X : Type u_1
𝕜 : Type u_2
A : Type u_3
p : A → Prop
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NonUnitalNormedRing A
inst✝⁶ : StarRing A
inst✝⁵ : NormedSpace 𝕜 A
inst✝⁴ : IsScalarTower 𝕜 A A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : ContinuousStar A
inst✝¹ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
inst✝ : TopologicalSpace X
s : Set 𝕜
hs : IsCompact s
f : 𝕜 → 𝕜
a : X → A
ha_cont : Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] a
ha : ∀ (x : X), quasispectrum 𝕜 (a x) ⊆ s
hf : ContinuousOn f s
hf0 : f 0 = 0
ha' : ∀ (x : X), p (a x)
⊢ Continuous[inst✝, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ cfcₙ f (a x)

Tactic:
by
  rw [← continuousOn_univ] at ha_cont ⊢
  exact ha_cont.cfcₙ' hs f (fun x _ ↦ ha x) (fun x _ ↦ ha' x)

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

Goal state before:
pp: X : Type u_1
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
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
a : X → A
a₀ : A
l : Filter X
ha_tendsto : Tendsto a l (𝓝 a₀)
ha : ∀ᶠ (x : X) in l, quasispectrum ℝ≥0 (a x) ⊆ s
ha' : ∀ᶠ (x : X) in l, 0 ≤ a x
ha₀ : quasispectrum ℝ≥0 a₀ ⊆ s
ha₀' : 0 ≤ a₀
hf : ContinuousOn f s
hf0 : f 0 = 0
⊢ Tendsto (fun x ↦ cfcₙ f (a x)) l (𝓝 (cfcₙ f a₀))

Tactic:
apply continuousOn_cfcₙ_nnreal A hs f |>.continuousWithinAt ⟨ha₀', ha₀⟩ |>.tendsto.comp

Goal state after:
X : Type u_1
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
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
a : X → A
a₀ : A
l : Filter X
ha_tendsto : Tendsto a l (𝓝 a₀)
ha : ∀ᶠ (x : X) in l, quasispectrum ℝ≥0 (a x) ⊆ s
ha' : ∀ᶠ (x : X) in l, 0 ≤ a x
ha₀ : quasispectrum ℝ≥0 a₀ ⊆ s
ha₀' : 0 ≤ a₀
hf : ContinuousOn f s
hf0 : f 0 = 0
⊢ Tendsto a l (𝓝[{a | 0 ≤ a ∧ quasispectrum ℝ≥0 a ⊆ s}] a₀)
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
inst✝ : NormedSpace ℝ A
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (quasispectrum 𝕜 a)
hf₂ : ∀ᵐ (x : X) ∂μ, f x 0 = 0
hf₃ : Integrable (fun x ↦ mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) μ
ha : p a
key₁ :
  ∀ (z : ↑(quasispectrum 𝕜 a)), ∫ (x : X), f x ↑z ∂μ = (∫ (x : X), mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0 ∂μ) z
key₂ :
  ∀ (z : ↑(quasispectrum 𝕜 a)),
    ∫ (x : X), f x ↑z ∂μ = (mkD ((quasispectrum 𝕜 a).domRestrict fun z ↦ ∫ (x : X), f x z ∂μ) 0) z
⊢ cfcₙ (fun z ↦ ∫ (x : X), f x z ∂μ) a = ∫ (x : X), cfcₙ (f x) a ∂μ

Tactic:
simp_rw [cfcₙ_eq_cfcₙL_mkD _ a, cfcₙL_integral a _ hf₃ ha]

Goal state after:
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
inst✝ : NormedSpace ℝ A
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (quasispectrum 𝕜 a)
hf₂ : ∀ᵐ (x : X) ∂μ, f x 0 = 0
hf₃ : Integrable (fun x ↦ mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0) μ
ha : p a
key₁ :
  ∀ (z : ↑(quasispectrum 𝕜 a)), ∫ (x : X), f x ↑z ∂μ = (∫ (x : X), mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0 ∂μ) z
key₂ :
  ∀ (z : ↑(quasispectrum 𝕜 a)),
    ∫ (x : X), f x ↑z ∂μ = (mkD ((quasispectrum 𝕜 a).domRestrict fun z ↦ ∫ (x : X), f x z ∂μ) 0) z
⊢ (cfcₙL ha) (mkD ((quasispectrum 𝕜 a).domRestrict fun z ↦ ∫ (x : X), f x z ∂μ) 0) =
    (cfcₙL ha) (∫ (x : X), mkD ((quasispectrum 𝕜 a).domRestrict (f x)) 0 ∂μ)
Module: Mathlib.Analysis.CStarAlgebra.Extreme

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
e : A
x✝ :
  (0 ≤ e ∧ ‖e‖ ≤ 1) ∧ ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
h1 : 0 ≤ e
h2 : ‖e‖ ≤ 1
h3 : ∀ (x₁ : A), 0 ≤ x₁ → ‖x₁‖ ≤ 1 → ∀ (x₂ : A), 0 ≤ x₂ → ‖x₂‖ ≤ 1 → e ∈ openSegment ℝ x₁ x₂ → x₁ = e
this : ↑e ≤ 1
⊢ Commute (↑e) (2 - ↑e)

Tactic:
simp [commute_iff_eq, mul_sub, sub_mul, mul_two, two_mul]

Goal state after:
Module: Mathlib.Data.Bundle

Goal state before:
pp: case h₂
B : Type u_1
F : Type u_2
E : B → Type u_3
proj✝ : B
x : E proj✝
⊢ { proj := proj✝, snd := x } ∈ range (mk { proj := proj✝, snd := x }.proj)

Tactic:
exact ⟨x, rfl⟩

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)
x✝ : B × F
⊢ x✝ ∈ Prod.map Subtype.val id '' e.target →
    (if h : x✝.1 ∈ s then e.invFun (⟨x✝.1, h⟩, x✝.2) else Classical.arbitrary (B → F → Z) x✝.1 x✝.2) ∈ e.source

Tactic:
rintro ⟨x, hx, rfl⟩; simpa using e.map_target hx

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

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G E
hf : IsQuotientCoveringMap f G
e : E
⊢ ∃ U ∈ 𝓝 e, ∀ (g : Additive G), ((fun x ↦ g +ᵥ x) '' U ∩ U).Nonempty → g = 0

Tactic:
obtain ⟨U, hU, hU'⟩ := hf.disjoint e
    exact ⟨U, hU, fun g ↦ by simpa using hU' (Additive.ofMul.symm g)⟩

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

Goal state before:
pp: case refine_2
E : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace X
f : E → X
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G E
hf : IsQuotientMap f
inst✝² : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst✝¹ : TopologicalSpace G
inst✝ : DiscreteTopology G
U : Set E
open_U : IsOpen[inst✝⁶] U
disjoint : ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
preim_im : f ⁻¹' f '' U = ⋃ g, (fun x ↦ g • x) ⁻¹' U
this : Nonempty (X → E)
g : G
W : Set X
hWU : W ⊆ f '' U
isOpen : IsOpen[inst✝⁶] (f ⁻¹' W ∩ (fun x ↦ g • x) ⁻¹' U)
⊢ IsOpen[inst✝⁶] (f ⁻¹' W)

Tactic:
convert! isOpen_iUnion fun g : G ↦ isOpen.preimage (continuous_const_smul g)
    ext e; refine ⟨fun hW ↦ ?_, ?_⟩
    · have ⟨e', he', hfe⟩ := hWU hW
      obtain ⟨g', rfl⟩ := hfG.mp hfe
      refine ⟨_, ⟨g⁻¹ * g', rfl⟩, ?_, ?_⟩
      · apply Set.mem_of_eq_of_mem (pGE _ e) hW
      · apply Set.mem_of_eq_of_mem _ he'; simp_rw [mul_smul, smul_inv_smul]
    · rintro ⟨_, ⟨g, rfl⟩, hW, -⟩; apply Set.mem_of_eq_of_mem (pGE _ e).symm hW

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

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
G : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G E
h :
  IsCoveringMap f ∧
    Function.Surjective f ∧
      ContinuousConstSMul G E ∧ IsCancelSMul G E ∧ ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
e : E
left✝ : DiscreteTopology ↑(f ⁻¹' {f e})
U : Set X
heU : f e ∈ U
hU : IsOpen[inst✝²] U
hfU : IsOpen[inst✝³] (f ⁻¹' U)
H : ↑(f ⁻¹' U) ≃ₜ ↑U × ↑(f ⁻¹' {f e})
hH : ∀ (x : ↑(f ⁻¹' U)), ↑(H x).1 = f ↑x
g : G
x : { x // x ∈ f ⁻¹' U }
hx : x ∈ Prod.snd ∘ ⇑H ⁻¹' {(H ⟨e, heU⟩).2}
y : { x // x ∈ f ⁻¹' U }
hy : y ∈ Prod.snd ∘ ⇑H ⁻¹' {(H ⟨e, heU⟩).2}
eq : ↑y = (fun x ↦ g • x) ↑x
this : IsCancelSMul G E
⊢ g • ↑x = 1 • ↑x

Tactic:
simp_rw [← eq, one_smul]

Goal state after:
E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
G : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G E
h :
  IsCoveringMap f ∧
    Function.Surjective f ∧
      ContinuousConstSMul G E ∧ IsCancelSMul G E ∧ ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
e : E
left✝ : DiscreteTopology ↑(f ⁻¹' {f e})
U : Set X
heU : f e ∈ U
hU : IsOpen[inst✝²] U
hfU : IsOpen[inst✝³] (f ⁻¹' U)
H : ↑(f ⁻¹' U) ≃ₜ ↑U × ↑(f ⁻¹' {f e})
hH : ∀ (x : ↑(f ⁻¹' U)), ↑(H x).1 = f ↑x
g : G
x : { x // x ∈ f ⁻¹' U }
hx : x ∈ Prod.snd ∘ ⇑H ⁻¹' {(H ⟨e, heU⟩).2}
y : { x // x ∈ f ⁻¹' U }
hy : y ∈ Prod.snd ∘ ⇑H ⁻¹' {(H ⟨e, heU⟩).2}
eq : ↑y = (fun x ↦ g • x) ↑x
this : IsCancelSMul G E
⊢ ↑y = ↑x
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic

Goal state before:
pp: A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
r : ℝ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
hr : r ≠ 0
ha₁ : IsSelfAdjoint a
⊢ cfc (Real.log ∘ fun x ↦ r • x) a = (algebraMap ℝ A) (Real.log r) + log a

Tactic:
log

Goal state after:
A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
r : ℝ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
hr : r ≠ 0
ha₁ : IsSelfAdjoint a
⊢ cfc (Real.log ∘ fun x ↦ r • x) a = (algebraMap ℝ A) (Real.log r) + cfc Real.log a
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x : ℝ
h₁ : -π < x
h₂ : x ≤ π
⊢ (Complex.cos ↑x + Complex.sin ↑x * I).arg = x

Tactic:
arg_cos_add_sin_mul_I ⟨h₁, h₂⟩

Goal state after:
x : ℝ
h₁ : -π < x
h₂ : x ≤ π
⊢ x = x
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic

Goal state before:
pp: A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
n : ℕ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
ha₁ : IsSelfAdjoint a
ha₂' : ContinuousOn Real.log (spectrum ℝ a)
ha₂'' : ContinuousOn Real.log ((fun x ↦ x ^ n) '' spectrum ℝ a)
⊢ cfc (fun x ↦ Real.log (x ^ n)) a = n • log a

Tactic:
log

Goal state after:
A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
n : ℕ
a : A
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
ha₁ : IsSelfAdjoint a
ha₂' : ContinuousOn Real.log (spectrum ℝ a)
ha₂'' : ContinuousOn Real.log ((fun x ↦ x ^ n) '' spectrum ℝ a)
⊢ cfc (fun x ↦ Real.log (x ^ n)) a = n • cfc Real.log a
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic

Goal state before:
pp: A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
hcont : ContinuousOn Real.log (Real.exp '' spectrum ℝ a)
⊢ cfc Real.log (exp a) = a

Tactic:
← real_exp_eq_normedSpace_exp,

Goal state after:
A : Type u_1
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : IsSelfAdjoint a
hcont : ContinuousOn Real.log (Real.exp '' spectrum ℝ a)
⊢ cfc Real.log (cfc Real.exp a) = a
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
h : x ≠ y
⊢ ⇑exp '' ⇑(Path.segment (↑x).arg (x.angleDiff y + (↑x).arg)) '' Ioc 0 1 =
    ⇑exp '' Ioc (↑x).arg (x.angleDiff y + (↑x).arg)

Tactic:
segment_image_Ioc (by simp [angleDiff_pos h])

Goal state after:
x y : Circle
h : x ≠ y
⊢ ⇑exp '' Ioc (↑x).arg (x.angleDiff y + (↑x).arg) = ⇑exp '' Ioc (↑x).arg (x.angleDiff y + (↑x).arg)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
h : x ≠ y
⊢ Disjoint (⇑(x.path y) '' Ioo 0 1) (⇑(y.path x) '' Ioo 0 1)

Tactic:
refine (disjoint_path_image_Ioc h).mono ?_ ?_

Goal state after:
case refine_1
x y : Circle
h : x ≠ y
⊢ ⇑(x.path y) '' Ioo 0 1 ⊆ ⇑(x.path y) '' Ioc 0 1

case refine_2
x y : Circle
h : x ≠ y
⊢ ⇑(y.path x) '' Ioo 0 1 ⊆ ⇑(y.path x) '' Ioc 0 1
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.re ≤ -‖z‖
hz_norm : ‖z‖ = 1
⊢ -1 ∈ spectrum ℂ u

Tactic:
← RCLike.re_eq_complex_re,

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 : RCLike.re z ≤ -‖z‖
hz_norm : ‖z‖ = 1
⊢ -1 ∈ spectrum ℂ u
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h✝ : Nontrivial A
⊢ a + I • cfcₙ Real.sqrt (1 - a ^ 2) = a + I • cfc (fun x ↦ √(1 - x ^ 2)) a

Tactic:
cfcₙ_eq_cfc,

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : IsSelfAdjoint a
ha_norm : ‖a‖ ≤ 1
h✝ : Nontrivial A
⊢ a + I • cfc Real.sqrt (1 - a ^ 2) = a + I • cfc (fun x ↦ √(1 - x ^ 2)) a
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
⊢ span ℂ ↑(unitary A) = ⊤

Tactic:
rw [eq_top_iff]

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
⊢ ⊤ ≤ span ℂ ↑(unitary A)
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: case refine_2
𝕜 : 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
A : E →L[𝕜] F
⊢ ‖A‖ ^ 2 ≤ ‖adjoint A ∘SL A‖

Tactic:
← Real.sqrt_le_sqrt_iff (norm_nonneg _),

Goal state after:
case refine_2
𝕜 : 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
A : E →L[𝕜] F
⊢ √(‖A‖ ^ 2) ≤ √‖adjoint A ∘SL A‖
Module: Mathlib.Analysis.Calculus.BumpFunction.Basic

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup X
inst✝¹ : NormedSpace ℝ X
inst✝ : HasContDiffBump E
n : ℕ∞
c g : X → E
f : (x : X) → ContDiffBump (c x)
hc : ContDiff ℝ (↑n) c
hr : ContDiff ℝ ↑n fun x ↦ (f x).rIn
hR : ContDiff ℝ ↑n fun x ↦ (f x).rOut
hg : ContDiff ℝ (↑n) g
⊢ ContDiff ℝ ↑n fun x ↦ ↑(f x) (g x)

Tactic:
by
  rw [contDiff_iff_contDiffAt] at *
  exact fun x => (hc x).contDiffBump (hr x) (hR x) (hg x)

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

Goal state before:
pp: case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
g : α → ℝ
hfg : ∀ (i : α), ‖f i‖ ≤ ‖g i‖
hg : {i | 0 < ‖g i‖}.Finite
⊢ {i | 0 < ‖f i‖}.Finite

Tactic:
refine hg.subset fun i hi ↦ hi.trans_le <| hfg i

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

Goal state before:
pp: α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
p q : ℝ≥0∞
f : (i : α) → E i
hfq : Memℓp f q
hpq : q ≤ p
⊢ Memℓp f p

Tactic:
by
  rcases ENNReal.trichotomy₂ hpq with
    (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ | ⟨rfl, hp⟩ | ⟨rfl, rfl⟩ | ⟨hq, rfl⟩ | ⟨hq, _, hpq'⟩)
  · exact hfq
  · apply memℓp_infty
    obtain ⟨C, hC⟩ := (hfq.finite_dsupport.image fun i => ‖f i‖).bddAbove
    use max 0 C
    rintro x ⟨i, rfl⟩
    by_cases hi : f i = 0
    · simp [hi]
    · exact (hC ⟨i, hi, rfl⟩).trans (le_max_right _ _)
  · apply memℓp_gen
    have : ∀ i ∉ hfq.finite_dsupport.toFinset, ‖f i‖ ^ p.toReal = 0 := by
      intro i hi
      have : f i = 0 := by simpa using hi
      simp [this, Real.zero_rpow hp.ne']
    exact summable_of_ne_finset_zero this
  · exact hfq
  · apply memℓp_infty
    obtain ⟨A, hA⟩ := (hfq.summable hq).tendsto_cofinite_zero.bddAbove_range_of_cofinite
    use A ^ q.toReal⁻¹
    rintro x ⟨i, rfl⟩
    have : 0 ≤ ‖f i‖ ^ q.toReal := by positivity
    simpa [← Real.rpow_mul, mul_inv_cancel₀ hq.ne'] using
      Real.rpow_le_rpow this (hA ⟨i, rfl⟩) (inv_nonneg.mpr hq.le)
  · apply memℓp_gen
    have hf' := hfq.summable hq
    refine .of_norm_bounded_eventually hf' (@Set.Finite.subset _ { i | 1 ≤ ‖f i‖ } ?_ _ ?_)
    · have H : { x : α | 1 ≤ ‖f x‖ ^ q.toReal }.Finite := by
        simpa using hf'.tendsto_cofinite_zero.eventually_lt_const (by simp)
      exact H.subset fun i hi => Real.one_le_rpow hi hq.le
    · change ∀ i, ¬|‖f i‖ ^ p.toReal| ≤ ‖f i‖ ^ q.toReal → 1 ≤ ‖f i‖
      intro i hi
      have : 0 ≤ ‖f i‖ ^ p.toReal := by positivity
      simp only [abs_of_nonneg, this] at hi
      contrapose! hi
      exact Real.rpow_le_rpow_of_exponent_ge' (norm_nonneg _) hi.le hq.le hpq'

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
t : Set 𝕜
y₀ y : 𝕜
hu : Summable u
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
h't : IsPreconnected t
hg : ∀ (n : α), ∀ y ∈ t, HasDerivAt (g n) (g' n y) y
hg' : ∀ (n : α), ∀ y ∈ t, ‖g' n y‖ ≤ u n
hy₀ : y₀ ∈ t
hg0 : Summable fun x ↦ g x y₀
hy : y ∈ t
⊢ Summable fun n ↦ g n y

Tactic:
hasDerivAt_iff_hasFDerivAt

Goal state after:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
t : Set 𝕜
y₀ y : 𝕜
hu : Summable u
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
h't : IsPreconnected t
hg' : ∀ (n : α), ∀ y ∈ t, ‖g' n y‖ ≤ u n
hy₀ : y₀ ∈ t
hg0 : Summable fun x ↦ g x y₀
hy : y ∈ t
hg : ∀ (n : α), ∀ y ∈ t, HasFDerivAt (g n) (ContinuousLinearMap.toSpanSingleton 𝕜 (g' n y)) y
⊢ Summable fun n ↦ g n y
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
t : Set 𝕜
y₀ y : 𝕜
hu : Summable u
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
h't : IsPreconnected t
hg : ∀ (n : α), ∀ y ∈ t, HasDerivAt (g n) (g' n y) y
hg' : ∀ (n : α), ∀ y ∈ t, ‖g' n y‖ ≤ u n
hy₀ : y₀ ∈ t
hg0 : Summable fun n ↦ g n y₀
hy : y ∈ t
⊢ HasDerivAt (fun z ↦ ∑' (n : α), g n z) (∑' (n : α), g' n y) y

Tactic:
hasDerivAt_iff_hasFDerivAt

Goal state after:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
t : Set 𝕜
y₀ y : 𝕜
hu : Summable u
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
h't : IsPreconnected t
hg' : ∀ (n : α), ∀ y ∈ t, ‖g' n y‖ ≤ u n
hy₀ : y₀ ∈ t
hg0 : Summable fun n ↦ g n y₀
hy : y ∈ t
hg : ∀ (n : α), ∀ y ∈ t, HasFDerivAt (g n) (ContinuousLinearMap.toSpanSingleton 𝕜 (g' n y)) y
⊢ HasFDerivAt (fun z ↦ ∑' (n : α), g n z) (ContinuousLinearMap.toSpanSingleton 𝕜 (∑' (n : α), g' n y)) y
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
y₀ : 𝕜
hu : Summable u
hg : ∀ (n : α) (y : 𝕜), HasDerivAt (g n) (g' n y) y
hg' : ∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n
hg0 : Summable fun n ↦ g n y₀
y : 𝕜
⊢ Summable fun n ↦ g n y

Tactic:
exact summable_of_summable_hasDerivAt_of_isPreconnected hu isOpen_univ isPreconnected_univ
    (fun n x _ => hg n x) (fun n x _ => hg' n x) (mem_univ _) hg0 (mem_univ _)

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 : ↥(lp E p)
hp : 0 < p.toReal
⊢ ‖-f‖ = ‖f‖

Tactic:
suffices ‖-f‖ ^ p.toReal = ‖f‖ ^ p.toReal by
      exact Real.rpow_left_injOn hp.ne' (norm_nonneg' _) (norm_nonneg' _) this

Goal state after:
case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : ↥(lp E p)
hp : 0 < p.toReal
⊢ ‖-f‖ ^ p.toReal = ‖f‖ ^ p.toReal
Module: Mathlib.Analysis.Calculus.SmoothSeries

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
hu : Summable u
hg : ∀ (n : α) (y : 𝕜), HasDerivAt (g n) (g' n y) y
hg' : ∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n
⊢ Differentiable 𝕜 fun z ↦ ∑' (n : α), g n z

Tactic:
hasDerivAt_iff_hasFDerivAt

Goal state after:
α : Type u_1
𝕜 : Type u_3
F : Type u_5
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : NormedSpace 𝕜 F
g g' : α → 𝕜 → F
hu : Summable u
hg' : ∀ (n : α) (y : 𝕜), ‖g' n y‖ ≤ u n
hg : ∀ (n : α) (y : 𝕜), HasFDerivAt (g n) (ContinuousLinearMap.toSpanSingleton 𝕜 (g' n y)) y
⊢ Differentiable 𝕜 fun z ↦ ∑' (n : α), g n z