mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.MetricSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace β
inst✝ : TopologicalSpace α
⊢ Isometry (⇑ofFun ∘ DFunLike.coe)

Tactic:
by
  simp [Isometry, edist_def, edist_eq_iSup]

Goal state after:
Module: Mathlib.Topology.MetricSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : PseudoEMetricSpace γ
𝔖 𝔗 : Set (Set α)
inst✝² : Finite ↑𝔖
inst✝¹ : PseudoMetricSpace β
inst✝ : BoundedSpace β
f g : α →ᵤ[𝔖] β
h✝ : Nonempty ↑(⋃₀ 𝔖)
⊢ BddAbove (Set.range fun x ↦ dist ((toFun 𝔖) f ↑x) ((toFun 𝔖) g ↑x))

Tactic:
use (Metric.ediam (.univ : Set β)).toReal

Goal state after:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : PseudoEMetricSpace γ
𝔖 𝔗 : Set (Set α)
inst✝² : Finite ↑𝔖
inst✝¹ : PseudoMetricSpace β
inst✝ : BoundedSpace β
f g : α →ᵤ[𝔖] β
h✝ : Nonempty ↑(⋃₀ 𝔖)
⊢ (Metric.ediam Set.univ).toReal ∈ upperBounds (Set.range fun x ↦ dist ((toFun 𝔖) f ↑x) ((toFun 𝔖) g ↑x))
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a : A
ha : IsStarNormal a
f : C(↑(σₙ ℂ a), ℂ)₀
⊢ ‖(cfcₙHom ha) f‖ = ‖f‖

Tactic:
rw [← norm_inr (𝕜 := ℂ), ← inrNonUnitalStarAlgHom_apply, ← NonUnitalStarAlgHom.comp_apply,
      inr_comp_cfcₙHom_eq_cfcₙAux a, cfcₙAux]

Goal state after:
A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
a : A
ha : IsStarNormal a
f : C(↑(σₙ ℂ a), ℂ)₀
⊢ ‖(((↑(cfcHom ⋯)).comp ↑(Homeomorph.compStarAlgEquiv' ℂ ℂ (Homeomorph.setCongr ⋯))).comp toContinuousMapHom) f‖ = ‖f‖
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
⊢ sqrt 0 = 0

Tactic:
simp [sqrt]

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

Goal state before:
pp: R : Type u_2
A : Type u_3
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : MetricSpace A
inst✝¹ : Algebra R A
inst✝ : IsometricContinuousFunctionalCalculus R A p
a : A
s : Set R
hs : spectrum R a ⊆ s
h₁ :
  LipschitzOnWith 1 (fun f ↦ cfc ((toFun {spectrum R a}) f) a)
    {f | ContinuousOn ((toFun {spectrum R a}) f) (spectrum R a)}
h₂ : LipschitzWith 1 (⇑(ofFun {spectrum R a}) ∘ ⇑(toFun {s}))
⊢ LipschitzOnWith 1 (fun f ↦ cfc ((toFun {s}) f) a) {f | ContinuousOn ((toFun {s}) f) s}

Tactic:
have h₃ := h₂.lipschitzOnWith (s := {f | ContinuousOn (toFun {s} f) (s)})

Goal state after:
R : Type u_2
A : Type u_3
p : A → Prop
inst✝⁹ : CommSemiring R
inst✝⁸ : StarRing R
inst✝⁷ : MetricSpace R
inst✝⁶ : IsTopologicalSemiring R
inst✝⁵ : ContinuousStar R
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : MetricSpace A
inst✝¹ : Algebra R A
inst✝ : IsometricContinuousFunctionalCalculus R A p
a : A
s : Set R
hs : spectrum R a ⊆ s
h₁ :
  LipschitzOnWith 1 (fun f ↦ cfc ((toFun {spectrum R a}) f) a)
    {f | ContinuousOn ((toFun {spectrum R a}) f) (spectrum R a)}
h₂ : LipschitzWith 1 (⇑(ofFun {spectrum R a}) ∘ ⇑(toFun {s}))
h₃ : LipschitzOnWith 1 (⇑(ofFun {spectrum R a}) ∘ ⇑(toFun {s})) {f | ContinuousOn ((toFun {s}) f) s}
⊢ LipschitzOnWith 1 (fun f ↦ cfc ((toFun {s}) f) a) {f | ContinuousOn ((toFun {s}) f) s}
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

Goal state before:
pp: ι : Type u_2
C : ι → Type u_3
inst✝¹² : (i : ι) → PartialOrder (C i)
inst✝¹¹ : (i : ι) → Ring (C i)
inst✝¹⁰ : (i : ι) → StarRing (C i)
inst✝⁹ : (i : ι) → TopologicalSpace (C i)
inst✝⁸ : ∀ (i : ι), StarOrderedRing (C i)
inst✝⁷ : StarOrderedRing ((i : ι) → C i)
inst✝⁶ : (i : ι) → Algebra ℝ (C i)
inst✝⁵ : ∀ (i : ι), ContinuousFunctionalCalculus ℝ (C i) IsSelfAdjoint
inst✝⁴ : ContinuousFunctionalCalculus ℝ ((i : ι) → C i) IsSelfAdjoint
inst✝³ : ∀ (i : ι), IsSemitopologicalRing (C i)
inst✝² : ∀ (i : ι), T2Space (C i)
inst✝¹ : NonnegSpectrumClass ℝ ((i : ι) → C i)
inst✝ : ∀ (i : ι), NonnegSpectrumClass ℝ (C i)
c : (i : ι) → C i
x : ℝ
hc : ∀ (i : ι), IsUnit (c i)
hc' : ∀ (i : ι), 0 ≤ c i
⊢ rpow c x = fun i ↦ c i ^ x

Tactic:
by
  have hc'' : ∀ i, 0 ∉ spectrum ℝ≥0 (c i) := fun i => spectrum.zero_notMem _ (hc i)
  simp only [rpow_def]
  unfold rpow
  exact cfc_map_pi (S := ℝ) _ c

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

Goal state before:
pp: A : Type u_1
E : Type u_2
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℂ E
inst✝³ : SMul A E
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarOrderedRing A
x y : E
⊢ 0 ≤ ⟪x, y⟫_A * star ⟪x, y⟫_A

Tactic:
exact mul_star_self_nonneg ⟪x, y⟫_A

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

Goal state before:
pp: case pos
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : Nontrivial R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : IsScalarTower R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (quasispectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (quasispectrum R a)
hF0 : ∀ᶠ (x : X) in l, F x 0 = 0
hl : l.NeBot
hf : ContinuousOn f (quasispectrum R a)
hf0 : f 0 = 0
ha : p a
s : Set X := {x | ContinuousOn (F x) (quasispectrum R a) ∧ F x 0 = 0}
hs : s ∈ l
⊢ Tendsto
    (fun x ↦ (cfcₙHom ha) { toFun := (quasispectrum R a).domRestrict (F ↑x), continuous_toFun := ⋯, map_zero' := ⋯ })
    (comap Subtype.val l) (𝓝 (cfcₙ f a))

Tactic:
cfcₙ_apply ..

Goal state after:
case pos
X : Type u_1
R : Type u_2
A : Type u_3
p : A → Prop
inst✝¹² : CommSemiring R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : Nontrivial R
inst✝⁸ : IsTopologicalSemiring R
inst✝⁷ : ContinuousStar R
inst✝⁶ : NonUnitalRing A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : Module R A
inst✝² : SMulCommClass R A A
inst✝¹ : IsScalarTower R A A
inst✝ : NonUnitalContinuousFunctionalCalculus R A p
l : Filter X
F : X → R → R
f : R → R
a : A
h_tendsto : TendstoUniformlyOn F f l (quasispectrum R a)
hF : ∀ᶠ (x : X) in l, ContinuousOn (F x) (quasispectrum R a)
hF0 : ∀ᶠ (x : X) in l, F x 0 = 0
hl : l.NeBot
hf : ContinuousOn f (quasispectrum R a)
hf0 : f 0 = 0
ha : p a
s : Set X := {x | ContinuousOn (F x) (quasispectrum R a) ∧ F x 0 = 0}
hs : s ∈ l
⊢ Tendsto
    (fun x ↦ (cfcₙHom ha) { toFun := (quasispectrum R a).domRestrict (F ↑x), continuous_toFun := ⋯, map_zero' := ⋯ })
    (comap Subtype.val l)
    (𝓝 ((cfcₙHom ha) { toFun := (quasispectrum R a).domRestrict f, continuous_toFun := ⋯, map_zero' := ⋯ }))
Module: Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Goal state before:
pp: A : Type u_1
inst✝ : NonUnitalCStarAlgebra A
l : Filter A
hl : ∀ᶠ (x : A) in l, IsSelfAdjoint x
⊢ (∀ (m : A), Tendsto (fun x ↦ m * x) l (𝓝 m)) ↔ ∀ (m : A), Tendsto (fun x ↦ x * m) l (𝓝 m)

Tactic:
by
  refine ⟨fun h m ↦ ?_, fun h m ↦ ?_⟩
  all_goals
    apply (star_star m ▸ (continuous_star.tendsto _ |>.comp <| h (star m))).congr'
    filter_upwards [hl] with x hx
    simp [hx.star_eq]

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
x y z : A
hx₀ : 0 ≤ x
hxy : x ≤ y
hy₁ : ‖y‖ ≤ 1
c : ℝ
hc : 0 ≤ c
h : ‖star ↑z * (1 - ↑x) * ↑z‖ ≤ c ^ 2
⊢ ‖↑z - ↑(y * z)‖ ≤ c

Tactic:
inr_mul

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x y z : A
hx₀ : 0 ≤ x
hxy : x ≤ y
hy₁ : ‖y‖ ≤ 1
c : ℝ
hc : 0 ≤ c
h : ‖star ↑z * (1 - ↑x) * ↑z‖ ≤ c ^ 2
⊢ ‖↑z - ↑y * ↑z‖ ≤ c
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 → α
⊢ ‖diagonal v‖₊ = ‖v‖₊

Tactic:
by
  simp_rw [nnnorm_def, Pi.nnnorm_def]
  congr 1 with i : 1
  refine le_antisymm (Finset.sup_le fun j hj => ?_) ?_
  · obtain rfl | hij := eq_or_ne i j
    · rw [diagonal_apply_eq]
    · simp [hij]
  · refine Eq.trans_le ?_ (Finset.le_sup (Finset.mem_univ i))
    rw [diagonal_apply_eq]

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
m✝ m : A
hm₁ : 0 ≤ ↑m
hm₂ : ‖↑m‖ < 1
ε : ℝ≥0
hε : 0 < ε
x : A
hx₁ : cfc (fun y ↦ 1 - (1 + y)⁻¹) (ε⁻¹ ^ 2 • ↑m) ≤ ↑x
hx₂ : ‖↑x‖ ≤ 1
hx₀ : 0 ≤ ↑x
⊢ ‖↑m - ↑(x * m)‖₊ ≤ ε

Tactic:
inr_mul

Goal state after:
A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
m✝ m : A
hm₁ : 0 ≤ ↑m
hm₂ : ‖↑m‖ < 1
ε : ℝ≥0
hε : 0 < ε
x : A
hx₁ : cfc (fun y ↦ 1 - (1 + y)⁻¹) (ε⁻¹ ^ 2 • ↑m) ≤ ↑x
hx₂ : ‖↑x‖ ≤ 1
hx₀ : 0 ≤ ↑x
⊢ ‖↑m - ↑x * ↑m‖₊ ≤ ε
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
⊢ (∑ x, ‖diagonal v x.1 x.2‖₊ ^ 2) ^ (1 / 2) = NNReal.sqrt (∑ x, ‖v x‖₊ ^ 2)

Tactic:
← Finset.sum_subset (Finset.subset_univ s) fun i _hi his => ?_

Goal state after:
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
⊢ (∑ x ∈ s, ‖diagonal v x.1 x.2‖₊ ^ 2) ^ (1 / 2) = NNReal.sqrt (∑ x, ‖v x‖₊ ^ 2)

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
Module: Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Range

Goal state before:
pp: case inl
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
f : ℝ → ℝ
hf : 0 ≤ cfcₙ f a
h₁ : ContinuousOn f (quasispectrum ℝ a)
h₂ : f 0 = 0
h₃ : IsSelfAdjoint a
⊢ ∀ x ∈ quasispectrum ℝ a, 0 ≤ f x

Tactic:
rwa [cfcₙ_nonneg_iff f a] at hf

Goal state after:
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
f : ℝ → ℝ
hf : 0 ≤ cfcₙ f a
h : ¬ContinuousOn f (quasispectrum ℝ a)
⊢ cfcₙ 0 a = cfcₙ f a

Tactic:
simp [cfcₙ_apply_of_not_continuousOn a h]

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
this : ContinuousOn (fun x ↦ ↑(f x.re)) ((fun x ↦ ↑x.im) '' spectrum ℂ a)
⊢ cfc (fun x ↦ ↑(f x.im)) a = cfc f ↑(ℑ a)

Tactic:
conv_rhs =>
    rw [cfc_real_eq_complex, ← cfc_im_id a, ← cfc_comp' ..]
    simp

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

Goal state before:
pp: F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CStarAlgebra A
inst✝³ : CStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : AlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
a : A
ha : IsSelfAdjoint a
φ : F
hφ : Function.Injective ⇑φ
h_spec : spectrum ℝ ((StarAlgHom.restrictScalars ℝ ↑φ) a) ⊆ spectrum ℝ a
⊢ spectrum ℝ (φ a) = spectrum ℝ a

Tactic:
refine Set.eq_of_subset_of_subset h_spec fun x hx ↦ ?_

Goal state after:
F : Type u_1
A : Type u_2
B : Type u_3
inst✝⁴ : CStarAlgebra A
inst✝³ : CStarAlgebra B
inst✝² : FunLike F A B
inst✝¹ : AlgHomClass F ℂ A B
inst✝ : StarHomClass F A B
a : A
ha : IsSelfAdjoint a
φ : F
hφ : Function.Injective ⇑φ
h_spec : spectrum ℝ ((StarAlgHom.restrictScalars ℝ ↑φ) a) ⊆ spectrum ℝ a
x : ℝ
hx : x ∈ spectrum ℝ a
⊢ x ∈ spectrum ℝ (φ a)
Module: Mathlib.Analysis.CStarAlgebra.Projection

Goal state before:
pp: A : Type u_1
inst✝⁶ : TopologicalSpace A
inst✝⁵ : NonUnitalRing A
inst✝⁴ : StarRing A
inst✝³ : Module ℂ A
inst✝² : IsScalarTower ℂ A A
inst✝¹ : SMulCommClass ℂ A A
inst✝ : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal
p : A
hp : IsIdempotentElem p
h : IsStarNormal p
x : ℂ
hx : x ∈ quasispectrum ℂ p
⊢ x = ↑x.re

Tactic:
rcases hp.quasispectrum_subset _ hx with (hx | hx) <;> simp [Set.mem_singleton_iff.mp hx]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : NormedDivisionRing 𝕜
x y : ↑(sphere 0 1)
⊢ ‖↑x / ↑y‖ = 1

Tactic:
by
    rw [norm_div, mem_sphere_zero_iff_norm.1 x.2, mem_sphere_zero_iff_norm.1 y.coe_prop, div_one]

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

Goal state before:
pp: x y : ℝ
⊢ ↑(exp (x + y)) = ↑(exp x * exp y)

Tactic:
by
    simp only [coe_exp, ofReal_add, add_mul, Complex.exp_add, coe_mul]

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 : ι
p : Z.TotalSpace
hp : p ∈ Z.proj ⁻¹' Z.baseSet i
⊢ (p.proj, Z.coordChange (Z.indexAt p.proj) i p.proj p.snd) ∈ Z.baseSet i ×ˢ univ

Tactic:
by
    simpa only [Set.mem_preimage, and_true, Set.mem_univ, Set.prodMk_mem_set_prod_eq] using hp

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✝ : ι
b : B
a : F
i : ι
s : Set (B × F)
⊢ IsOpen[instTopologicalSpaceProd] s →
    IsOpen ((Z.localTrivAsPartialEquiv i).source ∩ ↑(Z.localTrivAsPartialEquiv i) ⁻¹' s)

Tactic:
s_open

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✝ : ι
b : B
a : F
i : ι
s : Set (B × F)
s_open : IsOpen[instTopologicalSpaceProd] s
⊢ IsOpen ((Z.localTrivAsPartialEquiv i).source ∩ ↑(Z.localTrivAsPartialEquiv i) ⁻¹' s)
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
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
x✝ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
s : Set (B × F)
hs : IsOpen[instTopologicalSpaceProd] s
e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
⊢ IsOpen[coinduced e'.setSymm instTopologicalSpaceSubtype] (↑e ⁻¹' s ∩ e.source)

Tactic:
isOpen_coinduced,

Goal state after:
ι : Type u_1
B : Type u_2
F : Type u_3
X : Type u_4
inst✝³ : TopologicalSpace X
E : B → Type u_5
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
inst✝ : (x : B) → TopologicalSpace (E x)
a : FiberPrebundle F E
e : Pretrivialization F TotalSpace.proj
he : e ∈ a.pretrivializationAtlas
x✝ : TopologicalSpace (TotalSpace F E) := a.totalSpaceTopology
s : Set (B × F)
hs : IsOpen[instTopologicalSpaceProd] s
e' : Pretrivialization F TotalSpace.proj
he' : e' ∈ a.pretrivializationAtlas
⊢ IsOpen[instTopologicalSpaceSubtype] (e'.setSymm ⁻¹' (↑e ⁻¹' s ∩ e.source))
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ (b, e₁.coordChange e₂ b x).1 = (↑e₁ (↑e₁.symm (b, x))).1

pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ proj (↑e₁.symm (b, x)) ∈ e₁.baseSet

pp: B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ proj (↑e₁.symm (b, x)) ∈ e₂.baseSet

Tactic:
e₁.apply_symm_apply' h₁

Goal state after:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ (b, e₁.coordChange e₂ b x).1 = (b, x).1

B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ proj (↑e₁.symm (b, x)) ∈ e₁.baseSet

B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e₁ e₂ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ proj (↑e₁.symm (b, x)) ∈ e₂.baseSet
Module: Mathlib.Topology.FiberBundle.Trivialization

Goal state before:
pp: case fst
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 : Trivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
z : { x // x ∈ proj ⁻¹' s }
hz : z ∈ fun x ↦ e.source ↑x
⊢ ((Prod.map Subtype.val id ∘ ↑(e.toPretrivialization.restrictPreimage' s).toPartialEquiv) z).1 =
    ((↑e.toPartialEquiv ∘ Subtype.val) z).1

pp: case snd
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 : Trivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
z : { x // x ∈ proj ⁻¹' s }
hz : z ∈ fun x ↦ e.source ↑x
⊢ ((Prod.map Subtype.val id ∘ ↑(e.toPretrivialization.restrictPreimage' s).toPartialEquiv) z).2 =
    ((↑e.toPartialEquiv ∘ Subtype.val) z).2

Tactic:
exacts [(e.proj_toFun _ hz).symm, rfl]

Goal state after:
Module: Mathlib.Topology.IsLocalHomeomorph

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
s : Set X
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
g : OpenPartialHomeomorph Y Z
hxg : f x ∈ g.source
hgf✝ : IsLocalHomeomorphOn (↑g ∘ f) s
hg : IsLocalHomeomorphOn (↑g) (f '' s)
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : ↑g ∘ f = ↑gf
y : X
hy : y ∈ ((gf.restr (f ⁻¹' g.source)).trans g.symm).source
this : f y ∈ g.source
⊢ ↑g (f y) = (↑g ∘ f) y

Tactic:
Function.comp_apply

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Y
s : Set X
cont : ∀ x ∈ s, ContinuousAt f x
x : X
hx : x ∈ s
g : OpenPartialHomeomorph Y Z
hxg : f x ∈ g.source
hgf✝ : IsLocalHomeomorphOn (↑g ∘ f) s
hg : IsLocalHomeomorphOn (↑g) (f '' s)
gf : OpenPartialHomeomorph X Z
hgf : x ∈ gf.source
he : ↑g ∘ f = ↑gf
y : X
hy : y ∈ ((gf.restr (f ⁻¹' g.source)).trans g.symm).source
this : f y ∈ g.source
⊢ ↑g (f y) = ↑g (f y)
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
inst✝³ : Nonempty (X → E)
ι : Type ?u.20
inst✝² : Nonempty ι
inst✝¹ : TopologicalSpace ι
inst✝ : DiscreteTopology ι
U : ι → Set E
V : Set X
open_V : IsOpen[inst✝⁴] V
open_iff : ∀ (i : ι) {W : Set X}, W ⊆ V → (IsOpen[inst✝⁴] W ↔ IsOpen[inst✝⁵] (f ⁻¹' W ∩ U i))
inj : ∀ (i : ι), Set.InjOn f (U i)
disjoint : Pairwise (Disjoint on U)
exhaustive' : f ⁻¹' V ⊆ ⋃ i, U i
idx : (x : E) → x ∈ f ⁻¹' V → ι
idx_U : ∀ (x : E) (a : x ∈ f ⁻¹' V), x ∈ U (idx x a)
inv : ι → ⦃a : X⦄ → a ∈ V → E
inv_U : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), inv i a_1 ∈ U i
f_inv : ∀ (i : ι) ⦃a : X⦄ (a_1 : a ∈ V), f (inv i a_1) = a
F : PartialEquiv E (X × ι) :=
  { toFun := fun e ↦ (f e, if he : f e ∈ V then idx e he else Classical.arbitrary ι),
    invFun := fun x ↦ if hx : x.1 ∈ V then inv x.2 hx else Classical.arbitrary (X → E) x.1, source := f ⁻¹' V,
    target := V ×ˢ Set.univ, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯ }
open_preim : ∀ {W : Set X}, W ⊆ V → IsOpen[inst✝⁴] W → IsOpen[inst✝⁵] (f ⁻¹' W)
open_source : IsOpen[inst✝⁵] F.source
cont_f : ContinuousOn f F.source
e : E
he : e ∈ F.source
e' : E
he' : e' ∈ U (idx e he) ∩ F.source
h : e' ∉ {x | (fun x ↦ (fun x ↦ idx e he) x = (fun x ↦ if he : f x ∈ V then idx x he else Classical.arbitrary ι) x) x}
⊢ f e' ∈ V

Tactic:
exact he'.2

Goal state after:
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
⊢ log (a ^ n) = n • log a

Tactic:
have ha₂' : ContinuousOn Real.log (spectrum ℝ a) := by fun_prop

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)
⊢ log (a ^ n) = n • log a
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case refine_1
x y : Circle
h : x ≠ y
hdisj : Disjoint (Ioc (↑x).arg (x.angleDiff y + (↑x).arg)) (Ioc (↑y).arg (y.angleDiff x + (↑y).arg))
a : ℝ
ha : a ∈ Ioc (↑x).arg (x.angleDiff y + (↑x).arg)
b : ℝ
hb : b ∈ Ioc (↑y).arg (y.angleDiff x + (↑y).arg)
⊢ a ∈ Ioc (min (↑x).arg (↑y).arg) (min (↑x).arg (↑y).arg + 2 * π)

Tactic:
rw [← Ioc_union_Ioc_angleDiff_add_arg h]
    tauto

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

Goal state before:
pp: case refine_2
x y : Circle
h : x ≠ y
hdisj : Disjoint (Ioc (↑x).arg (x.angleDiff y + (↑x).arg)) (Ioc (↑y).arg (y.angleDiff x + (↑y).arg))
a : ℝ
ha : a ∈ Ioc (↑x).arg (x.angleDiff y + (↑x).arg)
b : ℝ
hb : b ∈ Ioc (↑y).arg (y.angleDiff x + (↑y).arg)
⊢ b ∈ Ioc (min (↑x).arg (↑y).arg) (min (↑x).arg (↑y).arg + 2 * π)

Tactic:
rw [← Ioc_union_Ioc_angleDiff_add_arg h]
    tauto

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

Goal state before:
pp: case refine_4
x y : Circle
hxy : x ≠ y
⊢ ¬{x, y} ∪ range ⇑(y.path x) = univ

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

Goal state after:
case refine_4
x y : Circle
hxy : x ≠ y
⊢ ¬range ⇑(y.path x) = univ