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

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
x✝ : PartialOrder A := spectralOrder A
⊢ ∀ (x y : A), x ≤ y ↔ ∃ p ∈ AddSubmonoid.closure (Set.range fun s ↦ star s * s), y = x + p

Tactic:
intro x y
      constructor
      · intro h
        obtain ⟨s, hs₁, _, hs₂⟩ :=
          CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts h.1 h.2
        refine ⟨s * s, ?_, by rwa [eq_sub_iff_add_eq', eq_comm] at hs₂⟩
        exact AddSubmonoid.subset_closure ⟨s, by simp [hs₁.star_eq]⟩
      · rintro ⟨p, hp, rfl⟩
        simp +instances only [spectralOrder, add_sub_cancel_left]
        induction hp using AddSubmonoid.closure_induction with
        | mem x hx =>
          obtain ⟨s, rfl⟩ := hx
          refine ⟨IsSelfAdjoint.star_mul_self s, ?_⟩
          rw [quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ,
            SpectrumRestricts.nnreal_iff, Unitization.inr_mul, Unitization.inr_star]
          exact spectrum_star_mul_self_nonneg
        | zero =>
          rw [quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ, SpectrumRestricts.nnreal_iff]
          simp
        | add x y _ _ hx hy =>
          simp +singlePass only [← Unitization.isSelfAdjoint_inr (R := ℂ),
            quasispectrumRestricts_iff_spectrumRestricts_inr' ℂ] at hx hy ⊢
          rw [Unitization.inr_add]
          exact ⟨hx.1.add hy.1, hx.2.nnreal_add hx.1 hy.1 hy.2⟩

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

Goal state before:
pp: A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
x y : ℝ≥0
hx : 0 < x
hy : 0 < y
⊢ cfcₙ (fun x_1 ↦ x_1.nnrpow (x + y)) a = cfcₙ (fun x_1 ↦ x_1.nnrpow x) a * cfcₙ (fun x ↦ x.nnrpow y) a

Tactic:
rw [← cfcₙ_mul _ _ a]

Goal state after:
A : Type u_1
inst✝⁹ : PartialOrder A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : TopologicalSpace A
inst✝⁶ : StarRing A
inst✝⁵ : Module ℝ A
inst✝⁴ : SMulCommClass ℝ A A
inst✝³ : IsScalarTower ℝ A A
inst✝² : StarOrderedRing A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
x y : ℝ≥0
hx : 0 < x
hy : 0 < y
⊢ cfcₙ (fun x_1 ↦ x_1.nnrpow (x + y)) a = cfcₙ (fun x_1 ↦ x_1.nnrpow x * x_1.nnrpow y) a
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: case neg
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
y : ℝ
hy : y ≠ 0
ha : 0 ≤ a
a✝ : Nontrivial A
h : IsUnit (cfc (fun x ↦ x ^ y) a)
hf : ¬ContinuousOn (fun x ↦ x ^ y) (spectrum ℝ≥0 a)
⊢ IsUnit a

Tactic:
rw [cfc_apply_of_not_continuousOn a hf] at h
    exact False.elim <| not_isUnit_zero h

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : A → A
s : Set A
hf : ∀ (x : A), IsSelfAdjoint (f x)
hf₂ : ConvexOn ℝ s (inr ∘ f)
⊢ ConvexOn ℝ s f

Tactic:
refine ⟨hf₂.1, ?_⟩
  intro x hx y hy a b ha hb hab
  rw [← Unitization.inr_le_iff _ _]
  simpa using hf₂.2 hx hy ha hb hab

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

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
f : A → A
s : Set A
hf : ∀ (x : A), IsSelfAdjoint (f x)
hf₂ : ConcaveOn ℝ s (inr ∘ f)
⊢ ConcaveOn ℝ s f

Tactic:
refine ⟨hf₂.1, ?_⟩
  intro x hx y hy a b ha hb hab
  rw [← Unitization.inr_le_iff _ _]
  simpa using hf₂.2 hx hy ha hb hab

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CStarAlgebra A
inst✝ : Nontrivial A
a : A
ha : IsSelfAdjoint a
ha' : SpectrumRestricts a ⇑Complex.reCLM
⊢ (spectralRadius ℝ a).toReal ∈ spectrum ℝ a ∨ -(spectralRadius ℝ a).toReal ∈ spectrum ℝ a

Tactic:
exact Real.spectralRadius_mem_spectrum_or (ha'.image ▸ (spectrum.nonempty a).image _)

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 : 0 ≤ a
n : ℕ
⊢ 0 ≤ cfc (fun x ↦ x ^ n) a

Tactic:
exact cfc_nonneg_of_predicate

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

Goal state before:
pp: A : Type u_1
inst✝¹⁰ : NonUnitalCStarAlgebra A
inst✝⁹ : PartialOrder A
E : Type u_2
F : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : Module ℂ E
inst✝⁶ : SMul A E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : Module ℂ F
inst✝³ : SMul A F
inst✝² : CStarModule A E
inst✝¹ : CStarModule A F
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ ‖x.1‖ + ‖x.2‖ ≤ ↑2 * ‖(linearEquiv ℂ A (E × F)) x‖

Tactic:
simp only [NNReal.coe_ofNat, linearEquiv_apply, two_mul]

Goal state after:
A : Type u_1
inst✝¹⁰ : NonUnitalCStarAlgebra A
inst✝⁹ : PartialOrder A
E : Type u_2
F : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : Module ℂ E
inst✝⁶ : SMul A E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : Module ℂ F
inst✝³ : SMul A F
inst✝² : CStarModule A E
inst✝¹ : CStarModule A F
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ(A, E × F)
⊢ ‖x.1‖ + ‖x.2‖ ≤ ‖(equiv A (E × F)) x‖ + ‖(equiv A (E × F)) x‖
Module: Mathlib.Analysis.Matrix.Normed

Goal state before:
pp: R : Type u_1
l : Type u_2
m : Type u_3
n : Type u_4
α : Type u_5
β : Type u_6
ι : Type u_7
inst✝⁵ : Fintype l
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Unique ι
inst✝¹ : NormedDivisionRing α
inst✝ : NormedAlgebra ℝ α
a : α
⊢ α

Tactic:
exact if a = 0 then 1 else ‖a‖ • a⁻¹

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

Goal state before:
pp: α : Type u_5
inst✝¹ : NormedDivisionRing α
inst✝ : NormedAlgebra ℝ α
a : α
⊢ ‖unitOf a‖₊ = 1

Tactic:
by
  rw [unitOf]
  split_ifs with h
  · simp
  · rw [← nnnorm_eq_zero] at h
    rw [nnnorm_smul, nnnorm_inv, nnnorm_norm, mul_inv_cancel₀ h]

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

Goal state before:
pp: case pos
A : Type u_2
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : Module ℝ A
inst✝⁸ : IsScalarTower ℝ A A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : IsTopologicalRing A
inst✝³ : T2Space A
inst✝² : PartialOrder A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : StarOrderedRing A
a b : A
hb : Commute a b
f : ℝ≥0 → ℝ≥0
ha : 0 ≤ a
⊢ Commute (cfcₙ f a) b

pp: case neg
A : Type u_2
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : Module ℝ A
inst✝⁸ : IsScalarTower ℝ A A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : IsTopologicalRing A
inst✝³ : T2Space A
inst✝² : PartialOrder A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : StarOrderedRing A
a b : A
hb : Commute a b
f : ℝ≥0 → ℝ≥0
ha : ¬0 ≤ a
⊢ Commute (cfcₙ f a) b

Tactic:
· rw [cfcₙ_nnreal_eq_real ..]
    exact hb.cfcₙ_real _

Goal state after:
case neg
A : Type u_2
inst✝¹¹ : NonUnitalRing A
inst✝¹⁰ : StarRing A
inst✝⁹ : Module ℝ A
inst✝⁸ : IsScalarTower ℝ A A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint
inst✝⁴ : IsTopologicalRing A
inst✝³ : T2Space A
inst✝² : PartialOrder A
inst✝¹ : NonnegSpectrumClass ℝ A
inst✝ : StarOrderedRing A
a b : A
hb : Commute a b
f : ℝ≥0 → ℝ≥0
ha : ¬0 ≤ a
⊢ Commute (cfcₙ f a) b
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range

Goal state before:
pp: A : Type u_1
inst✝¹⁴ : NonUnitalRing A
inst✝¹³ : StarRing A
inst✝¹² : Module ℝ A
inst✝¹¹ : IsScalarTower ℝ A A
inst✝¹⁰ : SMulCommClass ℝ A A
inst✝⁹ : TopologicalSpace A
inst✝⁸ : IsTopologicalRing A
inst✝⁷ : T2Space A
inst✝⁶ : PartialOrder A
inst✝⁵ : NonnegSpectrumClass ℝ A
inst✝⁴ : StarOrderedRing A
inst✝³ : StarModule ℝ A
inst✝² : ContinuousStar A
inst✝¹ : ContinuousConstSMul ℝ A
inst✝ : NonUnitalClosedEmbeddingContinuousFunctionalCalculus ℝ A IsSelfAdjoint
a : A
ha : 0 ≤ a
⊢ (Set.range fun x ↦ cfcₙ x a) = {x | x ∈ NonUnitalStarAlgebra.elemental ℝ a ∧ 0 ≤ x}

Tactic:
by
  rw [range_cfcₙ_nnreal_eq_image_cfcₙ_real a ha, Set.ofPred_and, SetLike.setOfPred_mem_eq,
    ← range_cfcₙ _ ha.isSelfAdjoint, Set.inter_comm, ← Set.image_preimage_eq_inter_range]
  refine Set.Subset.antisymm (Set.image_mono (fun _ ↦ cfcₙ_nonneg)) ?_
  rintro _ ⟨f, hf, rfl⟩
  simp only [Set.preimage_ofPred_eq, Set.mem_ofPred_eq, Set.mem_image] at hf ⊢
  obtain (⟨h₁, h₂, h₃⟩ | h | h | h) := by
    simpa only [not_and_or] using
      em (ContinuousOn f (quasispectrum ℝ a) ∧ f 0 = 0 ∧ IsSelfAdjoint a)
  · refine ⟨f, ?_, rfl⟩
    rwa [cfcₙ_nonneg_iff f a] at hf
  · exact ⟨0, by simp, by simp [cfcₙ_apply_of_not_continuousOn a h]⟩
  · exact ⟨0, by simp, by simp [cfcₙ_apply_of_not_map_zero a h]⟩
  · exact ⟨0, by simp, by simp [cfcₙ_apply_of_not_predicate a h]⟩

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 : A
x : f.PreGNS
⊢ f
      (star (f.ofPreGNS ((↑f.toPreGNS ∘ₗ ↑((ContinuousLinearMap.mul ℂ A) a) ∘ₗ ↑f.ofPreGNS) x)) *
        f.ofPreGNS ((↑f.toPreGNS ∘ₗ ↑((ContinuousLinearMap.mul ℂ A) a) ∘ₗ ↑f.ofPreGNS) x)) ≤
    ↑(‖a‖ ^ 2 * ‖x‖ ^ 2)

Tactic:
have : star (f.ofPreGNS x) * star a * (a * f.ofPreGNS x) ≤
        ‖a‖ ^ 2 • star (f.ofPreGNS x) * f.ofPreGNS x := by
      rw [← mul_assoc, mul_assoc _ (star a), sq, ← CStarRing.norm_star_mul_self (x := a),
        smul_mul_assoc]
      exact CStarAlgebra.star_left_conjugate_le_norm_smul

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
f : A →ₚ[ℂ] ℂ
inst✝ : StarOrderedRing A
a : A
x : f.PreGNS
this : star (f.ofPreGNS x) * star a * (a * f.ofPreGNS x) ≤ ‖a‖ ^ 2 • star (f.ofPreGNS x) * f.ofPreGNS x
⊢ f
      (star (f.ofPreGNS ((↑f.toPreGNS ∘ₗ ↑((ContinuousLinearMap.mul ℂ A) a) ∘ₗ ↑f.ofPreGNS) x)) *
        f.ofPreGNS ((↑f.toPreGNS ∘ₗ ↑((ContinuousLinearMap.mul ℂ A) a) ∘ₗ ↑f.ofPreGNS) x)) ≤
    ↑(‖a‖ ^ 2 * ‖x‖ ^ 2)
Module: Mathlib.Analysis.CStarAlgebra.Matrix

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x, ‖U i x‖ ^ 2
diag_eq_norm_sum : (U * Uᴴ) i i = ↑(∑ x, ‖U i x‖ ^ 2)
⊢ RCLike.re ((U * Uᴴ) i i) = ∑ x, ‖U i x‖ ^ 2

Tactic:
RCLike.ext_iff

Goal state after:
𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
U : Matrix n n 𝕜
hU : U ∈ Matrix.unitaryGroup n 𝕜
i j : n
norm_sum : ‖U i j‖ ^ 2 ≤ ∑ x, ‖U i x‖ ^ 2
diag_eq_norm_sum :
  RCLike.re ((U * Uᴴ) i i) = RCLike.re ↑(∑ x, ‖U i x‖ ^ 2) ∧ RCLike.im ((U * Uᴴ) i i) = RCLike.im ↑(∑ x, ‖U i x‖ ^ 2)
⊢ RCLike.re ((U * Uᴴ) i i) = ∑ x, ‖U i x‖ ^ 2
Module: Mathlib.Analysis.Normed.Field.UnitBall

Goal state before:
pp: 𝕜✝ : Type u_1
𝕜 : Type u_2
inst✝² : SeminormedRing 𝕜
inst✝¹ : NormMulClass 𝕜
inst✝ : NormOneClass 𝕜
a✝ b✝ : 𝕜
hx : a✝ ∈ sphere 0 1
hy : b✝ ∈ sphere 0 1
⊢ a✝ * b✝ ∈ sphere 0 1

Tactic:
by
    rw [mem_sphere_zero_iff_norm] at *
    simp [*]

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

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
hs : IsOpen[inst✝¹] s
⊢ (ofSet s hs).trans e = e.restr (e.source ∩ s)

Tactic:
ofSet_trans,

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
hs : IsOpen[inst✝¹] s
⊢ e.restr s = e.restr (e.source ∩ s)
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
U V : Opens X
hU : Nonempty ↥U
hV : Nonempty ↥V
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : Y
hy : y ∈ e.target ∩ ↑e.symm ⁻¹' (U.openPartialHomeomorphSubtypeCoe hU).target
⊢ ↑e.symm y ∈ (V.openPartialHomeomorphSubtypeCoe hV).target

Tactic:
Opens.openPartialHomeomorphSubtypeCoe_target

Goal state after:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
U V : Opens X
hU : Nonempty ↥U
hV : Nonempty ↥V
hUV : U ≤ V
i : ↑↑U → ↑↑V := inclusion hUV
y : Y
hy : y ∈ e.target ∩ ↑e.symm ⁻¹' ↑U
⊢ ↑e.symm y ∈ ↑V
Module: Mathlib.Topology.OpenPartialHomeomorph.Constructions

Goal state before:
pp: case hs
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 e' : OpenPartialHomeomorph X Z
hf : IsOpenEmbedding f
z : Z
x✝ : z ∈ e.target ∩ f ∘ ↑e.symm ⁻¹' f '' e'.source
hx : z ∈ e.target
y : X
hy : y ∈ e'.source
hxy : f y = f (↑e.symm z)
⊢ ↑e.symm z ∈ e'.source

Tactic:
exact (hf.injective hxy) ▸ hy

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

Goal state before:
pp: case left
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
⊢ ((Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j)).source = (Z.trivChange i j).source

pp: case right
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
⊢ EqOn (↑((Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j))) (↑(Z.trivChange i j).toPartialEquiv)
    ((Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j)).source

Tactic:
· ext x
    simp only [mem_localTrivAsPartialEquiv_target, mfld_simps]
    rfl

Goal state after:
case right
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i j : ι
⊢ EqOn (↑((Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j))) (↑(Z.trivChange i j).toPartialEquiv)
    ((Z.localTrivAsPartialEquiv i).symm.trans (Z.localTrivAsPartialEquiv j)).source
Module: Mathlib.Analysis.CStarAlgebra.Multiplier

Goal state before:
pp: case succ
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NonUnitalNormedRing A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : IsScalarTower 𝕜 A A
a : 𝓜(𝕜, A)
k : ℕ
hk : ∀ (x y : A), (a.toProd ^ k).2 x * y = x * (a.toProd ^ k).1 y
x y : A
⊢ (a.toProd ^ (k + 1)).2 x * y = x * (a.toProd ^ (k + 1)).1 y

Tactic:
rw [Prod.pow_snd, Prod.pow_fst] at hk ⊢
        rw [pow_succ' a.snd, mul_apply_eq_comp, a.central, hk, pow_succ a.fst, mul_apply_eq_comp]

Goal state after:
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
h : ∀ x ∈ s, ∃ e, x ∈ e.source ∧ Set.EqOn f (↑e) e.source
x : X
hx✝ : x ∈ s
e : OpenPartialHomeomorph X Y
hx : x ∈ e.source
he : Set.EqOn f (↑e) e.source
_y : Y
hy : _y ∈ e.target
⊢ f (e.invFun _y) = _y

Tactic:
rw [he (e.map_target' hy)]

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
s : Set X
h : ∀ x ∈ s, ∃ e, x ∈ e.source ∧ Set.EqOn f (↑e) e.source
x : X
hx✝ : x ∈ s
e : OpenPartialHomeomorph X Y
hx : x ∈ e.source
he : Set.EqOn f (↑e) e.source
_y : Y
hy : _y ∈ e.target
⊢ ↑e (e.invFun _y) = _y
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: case inr
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
⊢ IsEvenlyCovered f x ↑(f ⁻¹' {x})

Tactic:
let U' := U ∩ ⋂ e : f ⁻¹' {x}, f '' (V' e)

Goal state after:
case inr
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
⊢ IsEvenlyCovered f x ↑(f ⁻¹' {x})
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: ⊢ (nhds 1).HasBasis (fun x ↦ True) fun n ↦ centeredArc (π / 2 ^ (n + 1))

Tactic:
rw [← Circle.exp_zero, ← isLocalHomeomorph_circleExp.map_nhds_eq 0]

Goal state after:
⊢ (Filter.map (⇑exp) (nhds 0)).HasBasis (fun x ↦ True) fun n ↦ centeredArc (π / 2 ^ (n + 1))
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span

Goal state before:
pp: case inr
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
key : a + I • CFC.sqrt (1 - a ^ 2) = cfc (fun x ↦ ↑x.re + I * ↑√(1 - x.re ^ 2)) a
x : ℂ
hx : x ∈ spectrum ℂ a
⊢ ↑1 = 1

pp: case inr
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
key : a + I • CFC.sqrt (1 - a ^ 2) = cfc (fun x ↦ ↑x.re + I * ↑√(1 - x.re ^ 2)) a
x : ℂ
hx : x ∈ spectrum ℂ a
⊢ ‖x.re‖ ≤ 1

Tactic:
Complex.ofReal_one

Goal state after:
case inr
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
key : a + I • CFC.sqrt (1 - a ^ 2) = cfc (fun x ↦ ↑x.re + I * ↑√(1 - x.re ^ 2)) a
x : ℂ
hx : x ∈ spectrum ℂ a
⊢ 1 = 1

case inr
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
key : a + I • CFC.sqrt (1 - a ^ 2) = cfc (fun x ↦ ↑x.re + I * ↑√(1 - x.re ^ 2)) a
x : ℂ
hx : x ∈ spectrum ℂ a
⊢ ‖x.re‖ ≤ 1
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

pp: case mpr
A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
⊢ (∃ l, (List.map expUnitary l).prod = u) → u ∈ pathComponent 1

Tactic:
· revert u
    simp_rw [← Set.mem_range, ← Set.subset_def, pathComponent_eq_connectedComponent]
    refine IsClopen.connectedComponent_subset ?_ ⟨[], by simp⟩
    refine .of_thickening_subset_self zero_lt_two ?_
    intro u hu
    rw [mem_thickening_iff] at hu
    obtain ⟨v, ⟨⟨l, (hlv : (l.map expUnitary).prod = v)⟩, huv⟩⟩ := hu
    refine ⟨argSelfAdjoint (u * star v) :: l, ?_⟩
    simp [hlv, mul_assoc,
      expUnitary_eq_mul_inv u v (by simpa [Subtype.dist_eq, dist_eq_norm] using! huv)]

Goal state after:
case mpr
A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
⊢ (∃ l, (List.map expUnitary l).prod = u) → u ∈ pathComponent 1
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
p : E →L[𝕜] E
⊢ (↑p).IsSymmetricProjection ↔ ∃ (x : (↑p).range.HasOrthogonalProjection), p = (↑p).range.starProjection

Tactic:
LinearMap.isSymmetricProjection_iff_eq_coe_starProjection_range,

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
p : E →L[𝕜] E
⊢ (∃ (x : (↑p).range.HasOrthogonalProjection), ↑p = ↑(↑p).range.starProjection) ↔
    ∃ (x : (↑p).range.HasOrthogonalProjection), p = (↑p).range.starProjection
Module: Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional

Goal state before:
pp: case inr.inr
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s t : Finset V
hs : AffineIndependent k Subtype.val
hst : ↑s ⊆ ↑(affineSpan k ↑t)
hs' : s.Nonempty
ht' : t.Nonempty
this✝ : Nonempty ↥s
this : Nonempty ↑↑t
direction_le : vectorSpan k (Set.range Subtype.val) ≤ vectorSpan k (Set.range Subtype.val)
⊢ #s ≤ #t

Tactic:
have finrank_le := add_le_add_left (Submodule.finrank_mono direction_le) 1

Goal state after:
case inr.inr
k : Type u_1
V : Type u_2
inst✝² : DivisionRing k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s t : Finset V
hs : AffineIndependent k Subtype.val
hst : ↑s ⊆ ↑(affineSpan k ↑t)
hs' : s.Nonempty
ht' : t.Nonempty
this✝ : Nonempty ↥s
this : Nonempty ↑↑t
direction_le : vectorSpan k (Set.range Subtype.val) ≤ vectorSpan k (Set.range Subtype.val)
finrank_le :
  finrank k ↥(vectorSpan k (Set.range Subtype.val)) + 1 ≤ finrank k ↥(vectorSpan k (Set.range Subtype.val)) + 1
⊢ #s ≤ #t
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)
F : α → Type u_5
inst✝ : (i : α) → NormedAddCommGroup (F i)
hp : ∞ ≠ 0
x : ↥(lp E ∞)
y : ↥(lp F ∞)
h : ∀ (i : α), ‖↑x i‖ ≤ ‖↑y i‖
⊢ ‖x‖ ≤ ‖y‖

Tactic:
exact norm_le_of_forall_le (by positivity) fun i ↦ (h i).trans <| norm_apply_le_norm hp y i

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)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
C : ℝ
i : ι
hC : 0 ≤ C
_i : Fact (1 ≤ ∞)
F : ι → ↥(lp E ∞)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : ↥(lp E ∞)
hf : Tendsto (id fun i ↦ ↑(F i)) l (𝓝 ↑f)
hi : ‖F i‖ ≤ C
⊢ ‖f‖ ≤ C

pp: case inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
_i : Fact (1 ≤ p)
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : ↥(lp E p)
hf : Tendsto (id fun i ↦ ↑(F i)) l (𝓝 ↑f)
i : ι
hi : ‖F i‖ ≤ C
hC : 0 ≤ C
hp : p < ∞
⊢ ‖f‖ ≤ C

Tactic:
· apply norm_le_of_forall_le hC
    exact norm_apply_le_of_tendsto hCF hf

Goal state after:
case inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
_i : Fact (1 ≤ p)
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : ↥(lp E p)
hf : Tendsto (id fun i ↦ ↑(F i)) l (𝓝 ↑f)
i : ι
hi : ‖F i‖ ≤ C
hC : 0 ≤ C
hp : p < ∞
⊢ ‖f‖ ≤ C
Module: Mathlib.Analysis.Normed.Lp.lpSpace

Goal state before:
pp: case inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
_i : Fact (1 ≤ p)
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : ↥(lp E p)
hf : Tendsto (id fun i ↦ ↑(F i)) l (𝓝 ↑f)
i : ι
hi : ‖F i‖ ≤ C
hC : 0 ≤ C
hp : p < ∞
⊢ ‖f‖ ≤ C

Tactic:
have : 0 < p := zero_lt_one.trans_le _i.elim

Goal state after:
case inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_5
l : Filter ι
inst✝ : l.NeBot
_i : Fact (1 ≤ p)
C : ℝ
F : ι → ↥(lp E p)
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : ↥(lp E p)
hf : Tendsto (id fun i ↦ ↑(F i)) l (𝓝 ↑f)
i : ι
hi : ‖F i‖ ≤ C
hC : 0 ≤ C
hp : p < ∞
this : 0 < p
⊢ ‖f‖ ≤ C
Module: Mathlib.Analysis.SpecialFunctions.PolynomialExp

Goal state before:
pp: p : ℝ[X]
⊢ Tendsto (fun x ↦ eval x p / rexp x) atTop (𝓝 0)

Tactic:
induction p using Polynomial.induction_on' with

Goal state after: