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

Goal state before:
pp: case neg.inr
A : Type u_1
inst✝¹³ : NonUnitalCStarAlgebra A
R : Type u_2
inst✝¹² : Semifield R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalSemiring R
inst✝⁸ : ContinuousStar R
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : Algebra R ℂ
inst✝³ : IsScalarTower R ℂ A
p : A → Prop
p' : Unitization ℂ A → Prop
inst✝² : NonUnitalContinuousFunctionalCalculus R A p
inst✝¹ : ContinuousFunctionalCalculus R (Unitization ℂ A) p'
inst✝ : ContinuousMapZero.UniqueHom R (Unitization ℂ A)
hp : ∀ {a : A}, p' ↑a ↔ p a
a : A
f : R → R
hf₀ : f 0 = 0
h : ¬(ContinuousOn f (σₙ R a) ∧ p a)
ha : ¬p a
⊢ ↑(cfcₙ f a) = cfc f ↑a

Tactic:
· rw [cfcₙ_apply_of_not_predicate a ha, inr_zero,
        cfc_apply_of_not_predicate _ (not_iff_not.mpr hp |>.mpr ha)]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : Ring A
inst✝⁷ : StarRing A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Algebra ℝ A
inst✝³ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : IsSemitopologicalRing A
inst✝ : T2Space A
a : A
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
ha : 0 ≤ a
⊢ (a ^ x) ^ y = a ^ (x * y)

Tactic:
by
  simp only [rpow_def]
  rw [← cfc_comp _ _ a]
  refine cfc_congr fun _ _ => ?_
  simp [NNReal.rpow_mul]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: A : Type u_1
inst✝⁷ : PartialOrder A
inst✝⁶ : Ring A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : StarOrderedRing A
inst✝² : Algebra ℝ A
inst✝¹ : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : Aˣ
n : ℤ
ha : 0 ≤ ↑a
⊢ ↑a ^ ↑n = ↑(a ^ n)

Tactic:
rw [← cfc_zpow (R := ℝ≥0) a n, rpow_def]
  refine cfc_congr fun _ _ => ?_
  simp

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

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : Aˣ
ha : IsStrictlyPositive ↑a
⊢ ↑a ^ (-(1 / 2)) * ↑a * ↑a ^ (-(1 / 2)) = 1

Tactic:
nth_rw 2 [← rpow_one (a : A)]

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : Aˣ
ha : IsStrictlyPositive ↑a
⊢ ↑a ^ (-(1 / 2)) * ↑a ^ 1 * ↑a ^ (-(1 / 2)) = 1
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : a ≤ b
h : IsStrictlyPositive a
a✝ : Nontrivial A
⊢ IsUnit b

Tactic:
rw [← spectrum.zero_notMem_iff ℝ]

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a b : A
hab : a ≤ b
h : IsStrictlyPositive a
a✝ : Nontrivial A
⊢ 0 ∉ spectrum ℝ b
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity

Goal state before:
pp: A : Type u_2
inst✝⁹ : NormedRing A
inst✝⁸ : StarRing A
inst✝⁷ : NormedAlgebra ℝ A
inst✝⁶ : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁵ : ContinuousStar A
inst✝⁴ : PartialOrder A
inst✝³ : StarOrderedRing A
inst✝² : NonnegSpectrumClass ℝ A
inst✝¹ : T2Space A
inst✝ : IsSemitopologicalRing A
s : Set ℝ≥0
hs : IsCompact s
f : ℝ≥0 → ℝ≥0
hf : ContinuousOn f s
⊢ ContinuousOn (cfc f) {a | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}

Tactic:
by
  have : {a : A | 0 ≤ a ∧ spectrum ℝ≥0 a ⊆ s}.EqOn (cfc f) (cfc (fun x : ℝ ↦ f x.toNNReal)) :=
    fun a ha ↦ cfc_nnreal_eq_real _ _ ha.1
  refine ContinuousOn.congr ?_ this
  replace hf : ContinuousOn (fun x ↦ f x.toNNReal : ℝ → ℝ) (NNReal.toReal '' s) := by
    apply hf.ofReal_map_toNNReal
    rw [Set.mapsTo_image_iff]
    intro x hx
    simpa
  refine continuousOn_cfc A (hs.image NNReal.continuous_coe) _ hf |>.mono fun a ha ↦ ?_
  simp only [Set.mem_ofPred_eq, nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts] at ha ⊢
  rw [← SpectrumRestricts] at ha
  refine ⟨ha.1.1, ?_⟩
  rw [← ha.1.2.algebraMap_image]
  exact Set.image_mono ha.2

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
l : Filter A
h : ∀ (m : A), 0 ≤ m → ‖m‖ < 1 → Tendsto (fun x ↦ x * m) l (𝓝 m)
m : A
⊢ Tendsto (fun x ↦ x * m) l (𝓝 m)

Tactic:
by
  have : m ∈ span ℂ ({x | 0 ≤ x} ∩ ball 0 1) := by simp [span_nonneg_inter_unitBall]
  obtain ⟨n, c, x, rfl⟩ := mem_span_set'.mp this
  simp_rw [Finset.mul_sum]
  refine tendsto_finsetSum _ fun i _ ↦ ?_
  simp_rw [mul_smul_comm]
  exact tendsto_const_nhds.smul <| h (x i) (x i).2.1 <| by simpa using (x i).2.2

Goal state after:
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: n : Type u_4
α : Type u_5
inst✝² : Fintype n
inst✝¹ : SeminormedAddCommGroup α
inst✝ : DecidableEq n
v : n → α
s : Finset (n × n) := Finset.map { toFun := fun i ↦ (i, i), inj' := ⋯ } Finset.univ
i : n × n
_hi : i ∈ Finset.univ
his : i ∉ s
⊢ ‖diagonal v i.1 i.2‖₊ ^ 2 = 0

Tactic:
suffices i.1 ≠ i.2 by rw [diagonal_apply_ne _ this, nnnorm_zero, NNReal.zero_rpow two_ne_zero]
    intro h
    exact Finset.mem_map.not.mp his ⟨i.1, Finset.mem_univ _, Prod.ext rfl h⟩

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
inst✝ : Fintype n
x✝¹ y✝ : CStarMatrix n n A
x✝ : C⋆ᵐᵒᵈ(A, n → A)
i✝ : n
⊢ (toCLM (x✝¹ * y✝)) x✝ i✝ = (toCLM y✝ * toCLM x✝¹) x✝ i✝

Tactic:
simp [toCLM]

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✝⁵ : NormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : ContinuousFunctionalCalculus 𝕜 A p
inst✝¹ : CompleteSpace A
inst✝ : NormedSpace ℝ A
f : X → 𝕜 → 𝕜
a : A
hf₁ : ∀ᵐ (x : X) ∂μ, ContinuousOn (f x) (spectrum 𝕜 a)
hf₂ : Integrable (fun x ↦ mkD ((spectrum 𝕜 a).domRestrict (f x)) 0) μ
ha : p a
⊢ cfc (fun z ↦ ∫ (x : X), f x z ∂μ) a = ∫ (x : X), cfc (f x) a ∂μ

Tactic:
have key₁ (z : spectrum 𝕜 a) :
      ∫ x, f x z ∂μ = (∫ x, mkD ((spectrum 𝕜 a).domRestrict (f x)) 0 ∂μ) z := by
    rw [integral_apply hf₂]
    refine integral_congr_ae ?_
    filter_upwards [hf₁] with x cont_x
    rw [mkD_apply_of_continuousOn cont_x]
  have key₂ (z : spectrum 𝕜 a) :
      ∫ x, f x z ∂μ = mkD ((spectrum 𝕜 a).domRestrict (fun z ↦ ∫ x, f x z ∂μ)) 0 z := by
    rw [mkD_apply_of_continuousOn]
    rw [continuousOn_iff_continuous_domRestrict]
    refine continuous_congr key₁ |>.mpr ?_
    exact map_continuous (∫ x, mkD ((spectrum 𝕜 a).domRestrict (f x)) 0 ∂μ)
  simp_rw [cfc_eq_cfcL_mkD _ a, cfcL_integral a _ hf₂ ha]
  congr
  ext z
  rw [← key₁, key₂]

Goal state after:
Module: Mathlib.Analysis.Convex.Extreme

Goal state before:
pp: case mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
A : Set E
x : E
hA : Convex 𝕜 A
hxA : x ∈ A
hAx : ∀ ⦃x_1 : E⦄, x_1 ∈ A \ {x} → ∀ ⦃y : E⦄, y ∈ A \ {x} → [x_1 -[𝕜] y] ⊆ A \ {x}
x₁ : E
hx₁ : x₁ ∈ A
x₂ : E
hx₂ : x₂ ∈ A
hx : x ∈ [x₁ -[𝕜] x₂]
⊢ x₁ = x ∨ x₂ = x

Tactic:
by_contra! h

Goal state after:
case mpr
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : Ring 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : DenselyOrdered 𝕜
inst✝ : IsTorsionFree 𝕜 E
A : Set E
x : E
hA : Convex 𝕜 A
hxA : x ∈ A
hAx : ∀ ⦃x_1 : E⦄, x_1 ∈ A \ {x} → ∀ ⦃y : E⦄, y ∈ A \ {x} → [x_1 -[𝕜] y] ⊆ A \ {x}
x₁ : E
hx₁ : x₁ ∈ A
x₂ : E
hx₂ : x₂ ∈ A
hx : x ∈ [x₁ -[𝕜] x₂]
h : x₁ ≠ x ∧ x₂ ≠ x
⊢ False
Module: Mathlib.Topology.FiberBundle.Basic

Goal state before:
pp: ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
⊢ ∀ ⦃x : B × F⦄,
    x ∈ (Z.baseSet i ∩ Z.baseSet j) ×ˢ univ →
      ((x.1, Z.coordChange j i x.1 x.2).1,
          Z.coordChange i j (x.1, Z.coordChange j i x.1 x.2).1 (x.1, Z.coordChange j i x.1 x.2).2) =
        x

Tactic:
rintro ⟨x, v⟩ hx
    simp only [prodMk_mem_set_prod_eq, mem_inter_iff, and_true, mem_univ] at hx
    dsimp only
    rw [Z.coordChange_comp, Z.coordChange_self]
    · exact hx.2
    · simp [hx]

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

Goal state before:
pp: ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
x : B
v : F
hx : (x, v) ∈ Z.baseSet i ×ˢ univ
⊢ ({ proj := (x, v).1, snd := Z.coordChange i (Z.indexAt (x, v).1) (x, v).1 (x, v).2 }.proj,
      Z.coordChange (Z.indexAt { proj := (x, v).1, snd := Z.coordChange i (Z.indexAt (x, v).1) (x, v).1 (x, v).2 }.proj)
        i { proj := (x, v).1, snd := Z.coordChange i (Z.indexAt (x, v).1) (x, v).1 (x, v).2 }.proj
        { proj := (x, v).1, snd := Z.coordChange i (Z.indexAt (x, v).1) (x, v).1 (x, v).2 }.snd) =
    (x, v)

Tactic:
simp only [prodMk_mem_set_prod_eq, and_true, mem_univ] at hx

Goal state after:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
x : B
v : F
hx : x ∈ Z.baseSet i
⊢ ({ proj := (x, v).1, snd := Z.coordChange i (Z.indexAt (x, v).1) (x, v).1 (x, v).2 }.proj,
      Z.coordChange (Z.indexAt { proj := (x, v).1, snd := Z.coordChange i (Z.indexAt (x, v).1) (x, v).1 (x, v).2 }.proj)
        i { proj := (x, v).1, snd := Z.coordChange i (Z.indexAt (x, v).1) (x, v).1 (x, v).2 }.proj
        { proj := (x, v).1, snd := Z.coordChange i (Z.indexAt (x, v).1) (x, v).1 (x, v).2 }.snd) =
    (x, v)
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
e : Pretrivialization F fun z ↦ proj ↑z
inst✝ : Nonempty (Z → F)
⊢ Subtype.val '' e.source = proj ⁻¹' e.baseSet

Tactic:
by ext z; simpa [e.source_eq] using
    (e.proj_symm_apply' · ▸ (e.invFun (proj z, Classical.arbitrary (Z → F) z)).2)

Goal state after:
Module: Mathlib.Topology.SeparatedMap

Goal state before:
pp: X : Type u_1
Y : Sort u_2
A : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
f : X → Y
sep : IsClosed[instTopologicalSpaceSubtype] (Function.pullbackDiagonal f)
g : A → X
cont : Continuous[inst✝, inst✝¹] g
inj : Function.Injective g
⊢ IsClosed[instTopologicalSpaceSubtype] (Function.pullbackDiagonal (f ∘ g))

Tactic:
rw [← inj.preimage_pullbackDiagonal]

Goal state after:
X : Type u_1
Y : Sort u_2
A : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
f : X → Y
sep : IsClosed[instTopologicalSpaceSubtype] (Function.pullbackDiagonal f)
g : A → X
cont : Continuous[inst✝, inst✝¹] g
inj : Function.Injective g
⊢ IsClosed[instTopologicalSpaceSubtype] (Function.mapPullback g id g ⋯ ⋯ ⁻¹' Function.pullbackDiagonal f)
Module: Mathlib.Topology.SeparatedMap

Goal state before:
pp: X : Type u_1
Y : Sort u_2
A : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
f : X → Y
sep : IsSeparatedMap f
g : A → X
cont : Continuous[inst✝, inst✝¹] g
inj : Function.Injective g
⊢ IsSeparatedMap (f ∘ g)

Tactic:
by
  rw [isSeparatedMap_iff_isClosed_diagonal] at sep ⊢
  rw [← inj.preimage_pullbackDiagonal]
  exact sep.preimage (cont.mapPullback cont)

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
inst✝³ : TopologicalSpace Z
inst✝² : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F proj
x✝ : Z
e'✝ : Trivialization F TotalSpace.proj
b : B
y : E b
inst✝¹ : LinearOrder B
inst✝ : OrderTopology B
e e' : Trivialization F proj
x : B
He : x ∈ e.baseSet
He' : x ∈ e'.baseSet
Heq : ∀ (p : Z), proj p = x → ↑e p = ↑e' p
hx : x ∈ frontier (Iic x)
⊢ x ∈ e.baseSet ↔ x ∈ e'.baseSet

Tactic:
simp [He, He']

Goal state after:
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
hs : IsOpen[inst✝¹] s
hX : ∀ (a : ↑s), IsOpen[instTopologicalSpaceSubtype] {a}
x : X
hx : x ∈ s
e : OpenPartialHomeomorph X Y
hxe : x ∈ e.source
h : IsLocalHomeomorphOn (↑e) s
⊢ IsOpen[inst✝¹] {x}

Tactic:
simpa using hs.isOpenMap_subtype_val _ (hX ⟨x, hx⟩)

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
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace F E)
e✝ : Trivialization F proj
x : Z
e'✝ : Trivialization F TotalSpace.proj
b : B
y : E b
e e' : Trivialization F proj
H : Disjoint e.baseSet e'.baseSet
⊢ Disjoint e.target e'.target

Tactic:
by
        rw [e.target_eq, e'.target_eq, disjoint_iff_inf_le]
        intro x hx
        exact H.le_bot ⟨hx.1.1, hx.2.1⟩

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

Goal state before:
pp: case e'_3
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CStarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h : ∀ (b : A), ‖f b‖₊ ^ 2 ≤ C * ‖f b‖₊ * ‖b‖₊
h1 : ∀ (b : A), C * ‖f b‖₊ * ‖b‖₊ ≤ C * ‖f‖₊ * ‖b‖₊ ^ 2
this : ‖f‖₊ / sqrt ‖f‖₊ ≤ sqrt C
⊢ ‖f‖₊ = (‖f‖₊ / sqrt ‖f‖₊) ^ 2

pp: case e'_4
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CStarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h : ∀ (b : A), ‖f b‖₊ ^ 2 ≤ C * ‖f b‖₊ * ‖b‖₊
h1 : ∀ (b : A), C * ‖f b‖₊ * ‖b‖₊ ≤ C * ‖f‖₊ * ‖b‖₊ ^ 2
this : ‖f‖₊ / sqrt ‖f‖₊ ≤ sqrt C
⊢ C = sqrt C ^ 2

Tactic:
· simp only [NNReal.rpow_two, div_pow, sq_sqrt]
      simp only [sq, mul_self_div_self]

Goal state after:
case e'_4
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : NormedSpace 𝕜 A
inst✝³ : SMulCommClass 𝕜 A A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : StarRing A
inst✝ : CStarRing A
a : 𝓜(𝕜, A)
f : A →L[𝕜] A
C : ℝ≥0
h : ∀ (b : A), ‖f b‖₊ ^ 2 ≤ C * ‖f b‖₊ * ‖b‖₊
h1 : ∀ (b : A), C * ‖f b‖₊ * ‖b‖₊ ≤ C * ‖f‖₊ * ‖b‖₊ ^ 2
this : ‖f‖₊ / sqrt ‖f‖₊ ≤ sqrt C
⊢ C = sqrt C ^ 2
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
I : Type u_3
inst✝ : TopologicalSpace I
hs : IsOpen[inst✝¹] s
hfs : IsOpen[inst✝²] (f ⁻¹' s)
x✝¹ : X
hx : x✝¹ ∈ s
h : IsEvenlyCovered (fun e ↦ f ↑e) x✝¹ I
inst : DiscreteTopology I
U : Set X
hxU : x✝¹ ∈ U
hU : IsOpen[inst✝¹] U
hfU : IsOpen[instTopologicalSpaceSubtype] ((fun e ↦ f ↑e) ⁻¹' U)
H : ↑((fun e ↦ f ↑e) ⁻¹' U) ≃ₜ ↑U × I
hH : ∀ (x : ↑((fun e ↦ f ↑e) ⁻¹' U)), ↑(H x).1 = (fun e ↦ f ↑e) ↑x
x✝ : Nonempty I
hUs : U ⊆ s
this : Subtype.val '' (fun e ↦ f ↑e) ⁻¹' U = f ⁻¹' U
x : ↑(f ⁻¹' U)
⊢ (⋯.homeomorphImage ((fun e ↦ f ↑e) ⁻¹' U)).symm ((Homeomorph.setCongr this).symm x) = ⟨⟨↑x, ⋯⟩, ⋯⟩

Tactic:
Homeomorph.symm_apply_eq

Goal state after:
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst✝ : TopologicalSpace I
hs : IsOpen[inst✝¹] s
hfs : IsOpen[inst✝²] (f ⁻¹' s)
x✝¹ : X
hx : x✝¹ ∈ s
h : IsEvenlyCovered (fun e ↦ f ↑e) x✝¹ I
inst : DiscreteTopology I
U : Set X
hxU : x✝¹ ∈ U
hU : IsOpen[inst✝¹] U
hfU : IsOpen[instTopologicalSpaceSubtype] ((fun e ↦ f ↑e) ⁻¹' U)
H : ↑((fun e ↦ f ↑e) ⁻¹' U) ≃ₜ ↑U × I
hH : ∀ (x : ↑((fun e ↦ f ↑e) ⁻¹' U)), ↑(H x).1 = (fun e ↦ f ↑e) ↑x
x✝ : Nonempty I
hUs : U ⊆ s
this : Subtype.val '' (fun e ↦ f ↑e) ⁻¹' U = f ⁻¹' U
x : ↑(f ⁻¹' U)
⊢ (Homeomorph.setCongr this).symm x = (⋯.homeomorphImage ((fun e ↦ f ↑e) ⁻¹' U)) ⟨⟨↑x, ⋯⟩, ⋯⟩
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
hf : IsQuotientMap f
inst✝ : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
disjoint : ∀ (e : E), ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g • e = e
this✝ : TopologicalSpace G := ⊥
this : DiscreteTopology G
⊢ ∀ x ∈ f '' {e | MulAction.stabilizer G e = ⊥}, ∃ t, x ∈ t.baseSet

Tactic:
rintro x ⟨e, he, rfl⟩

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
hf : IsQuotientMap f
inst✝ : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
disjoint : ∀ (e : E), ∃ U ∈ 𝓝 e, ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g • e = e
this✝ : TopologicalSpace G := ⊥
this : DiscreteTopology G
e : E
he : e ∈ {e | MulAction.stabilizer G e = ⊥}
⊢ ∃ t, f e ∈ t.baseSet
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
h : x ≠ y
⊢ range ⇑(x.path y) ∪ range ⇑(y.path x) = univ

Tactic:
rw [range_path, range_path, ← image_union, Icc_union_Icc_angleDiff_add_arg h,
    periodic_exp.image_Icc two_pi_pos]
  exact exp_surjective.range_eq

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 : RCLike.re z ≤ -‖z‖
hz_norm : ‖z‖ = 1
⊢ -1 ∈ spectrum ℂ u

Tactic:
RCLike.re_le_neg_norm_iff_eq_neg_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 = -↑‖z‖
hz_norm : ‖z‖ = 1
⊢ -1 ∈ spectrum ℂ u
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: case inr.refine_2
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
inst✝ : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h✝¹ : ∀ e ∈ f ⁻¹' {x}, ∃ φ, e ∈ φ.source ∧ ↑φ = f
this✝³ : DiscreteTopology ↑(f ⁻¹' {x})
φ : ↑(f ⁻¹' {x}) → OpenPartialHomeomorph E X
hφ : ∀ (e : ↑(f ⁻¹' {x})), ↑e ∈ (φ e).source ∧ ↑(φ e) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst✝²] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : ↑(f ⁻¹' {x}) → Set E := fun e ↦ V ↑e ∩ (φ e).source
hV' : ∀ (e : ↑(f ⁻¹' {x})), IsOpen[inst✝²] (V' e)
this✝² : ⋃ e, V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ e, V' e
h✝ : Nonempty ↑(f ⁻¹' {x})
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst✝¹] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ e, f '' V' e
this✝¹ : Finite ↑(f ⁻¹' {x})
hU' : IsOpen[inst✝¹] U'
hUV : ∀ (e : ↑(f ⁻¹' {x})), U' ⊆ f '' V' e
this✝ : Nonempty E
e : ↑(f ⁻¹' {x})
s : Set X
hs : s ⊆ U'
h : IsOpen[inst✝²] (f ⁻¹' s ∩ V' e)
this : s ⊆ (φ e).target
⊢ IsOpen[inst✝²] (↑(φ e).symm '' s)

Tactic:
(φ e).symm_image_eq_source_inter_preimage this,

Goal state after:
case inr.refine_2
E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
inst✝ : T2Space E
x : X
hf : IsClosedMap f
fin : (f ⁻¹' {x}).Finite
h✝¹ : ∀ e ∈ f ⁻¹' {x}, ∃ φ, e ∈ φ.source ∧ ↑φ = f
this✝³ : DiscreteTopology ↑(f ⁻¹' {x})
φ : ↑(f ⁻¹' {x}) → OpenPartialHomeomorph E X
hφ : ∀ (e : ↑(f ⁻¹' {x})), ↑e ∈ (φ e).source ∧ ↑(φ e) = f
V : E → Set E
hV : ∀ (x : E), x ∈ V x ∧ IsOpen[inst✝²] (V x)
disj : (f ⁻¹' {x}).PairwiseDisjoint V
V' : ↑(f ⁻¹' {x}) → Set E := fun e ↦ V ↑e ∩ (φ e).source
hV' : ∀ (e : ↑(f ⁻¹' {x})), IsOpen[inst✝²] (V' e)
this✝² : ⋃ e, V' e ∈ 𝓝ˢ (f ⁻¹' {x})
W : Set X
hWx : W ∈ 𝓝 x
hWV : f ⁻¹' W ⊆ ⋃ e, V' e
h✝ : Nonempty ↑(f ⁻¹' {x})
U : Set X
hUW : U ⊆ W
hU : IsOpen[inst✝¹] U
hxU : x ∈ U
U' : Set X := U ∩ ⋂ e, f '' V' e
this✝¹ : Finite ↑(f ⁻¹' {x})
hU' : IsOpen[inst✝¹] U'
hUV : ∀ (e : ↑(f ⁻¹' {x})), U' ⊆ f '' V' e
this✝ : Nonempty E
e : ↑(f ⁻¹' {x})
s : Set X
hs : s ⊆ U'
h : IsOpen[inst✝²] (f ⁻¹' s ∩ V' e)
this : s ⊆ (φ e).target
⊢ IsOpen[inst✝²] ((φ e).source ∩ ↑(φ e) ⁻¹' s)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case H.H
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : Circle.exp (2 * π / T * z✝¹) = Circle.exp (2 * π / T * z✝)
⊢ ↑z✝¹ = ↑z✝

Tactic:
obtain ⟨m, hm⟩ := Circle.exp_eq_exp.mp h.symm

Goal state after:
case H.H
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : Circle.exp (2 * π / T * z✝¹) = Circle.exp (2 * π / T * z✝)
m : ℤ
hm : 2 * π / T * z✝ = 2 * π / T * z✝¹ + ↑m * (2 * π)
⊢ ↑z✝¹ = ↑z✝
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: z : Circle
hz : ∀ n > 0, z ^ n ∈ centeredArc (π / 2)
⊢ z ∈ centeredArc (π / 2)

Tactic:
simpa using hz 1

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
A : E →L[𝕜] F
⊢ ‖adjointAux A‖ = ‖A‖

Tactic:
by
  refine le_antisymm ?_ ?_
  · refine ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg _) fun x => ?_
    rw [adjointAux_apply, LinearIsometryEquiv.norm_map]
    exact toSesqForm_apply_norm_le
  · nth_rw 1 [← adjointAux_adjointAux A]
    refine ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg _) fun x => ?_
    rw [adjointAux_apply, LinearIsometryEquiv.norm_map]
    exact toSesqForm_apply_norm_le

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
hu : dist u 1 < 2
ε : ℝ
huε : dist u 1 ^ 2 < ε
hε2 : ε < 2 ^ 2
hε : 0 < ε
huε' : dist u 1 < √ε
v : ↥(unitary A)
hv : v ∈ closedBall 1 √ε
z : ℂ
hz : z ∈ spectrum ℂ ↑v
⊢ ‖↑v - 1‖ ^ 2 ≤ ε

Tactic:
refine Real.le_sqrt (by positivity) (by positivity) |>.mp ?_
      simpa [Subtype.dist_eq, dist_eq_norm] using hv

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

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

Tactic:
obtain ⟨u, c, rfl, h⟩ := CStarAlgebra.exists_sum_four_unitary x

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
u : Fin 4 → ↥(unitary A)
c : Fin 4 → ℂ
h : ∀ (i : Fin 4), ‖c i‖ ≤ ‖∑ i, c i • ↑(u i)‖ / 2
⊢ ∑ i, c i • ↑(u i) ∈ span ℂ ↑(unitary A)
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Connected

Goal state before:
pp: case mp
A : Type u_1
inst✝ : CStarAlgebra A
⊢ ∀ {u : ↥(unitary A)}, u ∈ pathComponent 1 → ∃ l, (List.map expUnitary l).prod = u

Tactic:
simp_rw [← Set.mem_range, ← Set.subset_def, pathComponent_eq_connectedComponent]

Goal state after:
case mp
A : Type u_1
inst✝ : CStarAlgebra A
⊢ connectedComponent 1 ⊆ Set.range fun y ↦ (List.map expUnitary y).prod
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
⊢ (↑(adjoint T ∘SL T)).ker = ⊥ ↔ (↑T).ker = ⊥

Tactic:
ker_adjoint_comp_self

Goal state after:
𝕜 : 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).ker = ⊥ ↔ (↑T).ker = ⊥