mathlib-initiative/mathlib-tactics huggingface dataset:
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 (im '' spectrum ℂ a)
ha : IsStarNormal a
⊢ ContinuousOn re ((fun x ↦ ↑x.im) '' spectrum ℂ a)

Tactic:
by fun_prop

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

Goal state before:
pp: A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ A IsStarNormal
u : A
hu : IsStarNormal u
⊢ (∀ x ∈ spectrum ℂ u, star (id x) * id x = 1) ↔ ∀ x ∈ spectrum ℂ u, x ∈ ↑(unitary ℂ)

Tactic:
simp only [id_eq, RCLike.star_def, SetLike.mem_coe, Unitary.mem_iff_star_mul_self]

Goal state after:
Module: Mathlib.Analysis.Normed.Group.NullSubmodule

Goal state before:
pp: M : Type u_1
inst✝ : SeminormedCommGroup M
x y : M
hx : ‖x‖ = 0
hy : ‖y‖ = 0
⊢ 0 + 0 = 0

Tactic:
add_zero

Goal state after:
M : Type u_1
inst✝ : SeminormedCommGroup M
x y : M
hx : ‖x‖ = 0
hy : ‖y‖ = 0
⊢ 0 = 0
Module: Mathlib.Analysis.InnerProductSpace.Completion

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : Completion E
⊢ Continuous fun a ↦ ‖a‖ ^ 2

Tactic:
by fun_prop

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x : Completion E
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by fun_prop

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : Completion E
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by fun_prop

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y z : Completion E
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by fun_prop

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : Completion E
c : 𝕜
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
by fun_prop

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

Goal state before:
pp: x y : Circle
⊢ Continuous fun t ↦ cexp (↑t * I)

Tactic:
by fun_prop

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

Goal state before:
pp: 𝕜 : Type u_1
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : Fintype n
inst✝ : DecidableEq n
v : n → 𝕜
T : EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n := toEuclideanCLM (diagonal v)
x : EuclideanSpace 𝕜 n
i : n
x✝ : i ∈ Finset.univ
⊢ (‖v i‖ * ‖x.ofLp i‖) ^ 2 ≤ ?m.78 i

Tactic:
by grw [mul_pow, norm_le_pi_norm v i]

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

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
hs' : IsOpen[inst✝] (↑e '' s)
hs'' : s ⊆ e.source
⊢ e.target ∩ ↑e.symm ⁻¹' s ∩ ↑e.symm ⁻¹' e'.source = e.target ∩ ↑e '' s ∩ ↑e.symm ⁻¹' e'.source

Tactic:
congr 1

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

Goal state before:
pp: X : Type u_1
X' : Type u_2
Y : Type u_3
Y' : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace X'
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Y'
eX eX' : OpenPartialHomeomorph X X'
eY eY' : OpenPartialHomeomorph Y Y'
h : (eX'.prod eY').source.Nonempty
⊢ eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'

Tactic:
by
  rw [eq_comm, prod_eq_prod_of_nonempty h, eq_comm, @eq_comm _ eY']

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

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
ht : IsOpen[inst✝] (e'.target ∩ ↑e'.symm ⁻¹' s)
⊢ ↑e'.symm ⁻¹' e.source ∩ (e'.target ∩ ↑e'.symm ⁻¹' s) =
    ↑e'.symm ⁻¹' e.source ∩ (e'.target ∩ interior (e'.target ∩ ↑e'.symm ⁻¹' s))

Tactic:
congr 1

Goal state after:
case e_a
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : OpenPartialHomeomorph X Y
s : Set X
e' : OpenPartialHomeomorph X Y
hs : IsOpen[inst✝¹] s
ht : IsOpen[inst✝] (e'.target ∩ ↑e'.symm ⁻¹' s)
⊢ e'.target ∩ ↑e'.symm ⁻¹' s = e'.target ∩ interior (e'.target ∩ ↑e'.symm ⁻¹' s)
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
e : Pretrivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] (Prod.map Subtype.val id)

Tactic:
by fun_prop

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

Goal state before:
pp: B : Type u_2
F : Type u_3
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
⊢ ContinuousOn (↑e.symm) e.target

Tactic:
refine fun z H U h => preimage_nhdsWithin_coinduced' H (le_def.1 (nhds_mono ?_) U h)

Goal state after:
B : Type u_2
F : Type u_3
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
z : B × F
H : z ∈ e.target
U : Set (TotalSpace F E)
h : U ∈ 𝓝 (↑e.symm z)
⊢ coinduced (fun x ↦ ↑e.symm ↑x) inferInstance ≤ a.totalSpaceTopology
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 : Trivialization F proj
b : B
v : F
hb : b ∈ e.baseSet
⊢ ContinuousAt (fun x ↦ (x, v)) b

Tactic:
by fun_prop

Goal state after:
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₂ e₃ : Trivialization F proj
b : B
h₁ : b ∈ e₁.baseSet
h₂ : b ∈ e₂.baseSet
x : F
⊢ ↑e₁.symm (b, x) ∈ e₂.source

Tactic:
e₂.mem_source,

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₂ 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 refine_3
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
⊢ ↑e₁.symm (b, x) ∈ e₂.source

Tactic:
e₂.mem_source,

Goal state after:
case refine_3
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.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:
← 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.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 : Trivialization F proj
s : Set B
inst✝ : Nonempty (↑s → F → ↑(proj ⁻¹' s))
⊢ Continuous[instTopologicalSpaceSubtype, inst✝²] Subtype.val

Tactic:
by fun_prop

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
g₁ g₂ : A → X
h₁ : Continuous[inst✝, inst✝¹] g₁
h₂ : Continuous[inst✝, inst✝¹] g₂
sep : IsSeparatedMap f
he : f ∘ g₁ = f ∘ g₂
g : A → Function.Pullback f f := fun a ↦ ⟨(g₁ a, g₂ a), ⋯⟩
⊢ Continuous[inst✝, instTopologicalSpaceSubtype] g

Tactic:
by fun_prop

Goal state after:
Module: Mathlib.Topology.SeparatedMap

Goal state before:
pp: X : Type u_1
Y : Type u_2
A : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace A
f : X → Y
g₁ g₂ : A → X
h₁ : Continuous[inst✝, inst✝¹] g₁
h₂ : Continuous[inst✝, inst✝¹] g₂
inj : IsLocallyInjective f
he : f ∘ g₁ = f ∘ g₂
g : A → Function.Pullback f f := fun a ↦ ⟨(g₁ a, g₂ a), ⋯⟩
⊢ Continuous[inst✝, instTopologicalSpaceSubtype] g

Tactic:
by fun_prop

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
f : X → Y
h : IsLocalHomeomorphOn f s
x : X
hx : x ∈ s
⊢ ∃ U ∈ 𝓝 x, IsOpenEmbedding (U.domRestrict f)

Tactic:
obtain ⟨e, hxe, rfl⟩ := h x hx
    exact ⟨e.source, e.open_source.mem_nhds hxe, e.isOpenEmbedding_restrict⟩

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : CompleteSpace A
x y : A
⊢ Continuous fun x_1 ↦ (unop x_1.2) x * y

Tactic:
by fun_prop

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NonUnitalNormedRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : CompleteSpace A
x y : A
⊢ Continuous fun x_1 ↦ x * x_1.1 y

Tactic:
by fun_prop

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✝
T✝ : Trivialization F proj
z : Z
b : B
T : Trivialization F proj
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] fun x ↦ T.lift ↑x.1 ↑x.2

Tactic:
refine T.continuousOn_invFun.comp_continuous ?_ (by simp [mem_target])

Goal state after:
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✝
T✝ : Trivialization F proj
z : Z
b : B
T : Trivialization F proj
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun x ↦ (↑x.2, (↑T ↑x.1).2)
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✝
T✝ : Trivialization F proj
z : Z
b : B
T : Trivialization F proj
⊢ Continuous[instTopologicalSpaceProd, inst✝³] fun x ↦ ↑x.2

Tactic:
by fun_prop

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✝
T✝ : Trivialization F proj
z : Z
b : B
T : Trivialization F proj
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] fun x ↦ ↑x.1

Tactic:
by fun_prop

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✝
T✝ : Trivialization F proj
z : Z
b : B
ι : Type u_5
inst✝² : TopologicalSpace ι
inst✝¹ : LocallyCompactPair ι ↑T✝.baseSet
γ : C(ι, ↑T✝.baseSet)
i : ι
e : ↑T✝.source
T : Trivialization F proj
inst✝ : LocallyCompactPair ι ↑T.baseSet
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun eγt ↦ (eγt.1.2, eγt.2)

Tactic:
by fun_prop

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✝
T✝ : Trivialization F proj
z : Z
b : B
ι : Type u_5
inst✝² : TopologicalSpace ι
inst✝¹ : LocallyCompactPair ι ↑T✝.baseSet
γ : C(ι, ↑T✝.baseSet)
i : ι
e : ↑T✝.source
T : Trivialization F proj
inst✝ : LocallyCompactPair ι ↑T.baseSet
Ψ : C((↑T.source × C(ι, ↑T.baseSet)) × ι, C(ι, ↑T.baseSet) × ι) :=
  { toFun := fun eγt ↦ (eγt.1.2, eγt.2), continuous_toFun := ⋯ }
⊢ Continuous[instTopologicalSpaceProd, instTopologicalSpaceSubtype] fun x ↦ x.1.1

Tactic:
by fun_prop

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

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst✝ : TopologicalSpace I
x : X
h✝ : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst✝¹] U
hfU : IsOpen[inst✝²] (f ⁻¹' U)
H : ↑(f ⁻¹' U) ≃ₜ ↑U × I
hH : ∀ (x : ↑(f ⁻¹' U)), ↑(H x).1 = f ↑x
⊢ Continuous[inst✝, instTopologicalSpaceSubtype] fun i ↦ ⟨↑(H.symm (⟨x, hxU⟩, i)), ⋯⟩

Tactic:
by fun_prop

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

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst✝ : TopologicalSpace I
x : X
h✝ : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst✝¹] U
hfU : IsOpen[inst✝²] (f ⁻¹' U)
H : ↑(f ⁻¹' U) ≃ₜ ↑U × I
hH : ∀ (x : ↑(f ⁻¹' U)), ↑(H x).1 = f ↑x
⊢ Continuous[instTopologicalSpaceSubtype, inst✝] fun e ↦ (H ⟨↑e, ⋯⟩).2

Tactic:
by fun_prop

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CStarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : (Metric.closedBall 0 1).Nonempty
x y : A
hx : ‖x‖₊ ≤ 1
hy : ‖y‖₊ ≤ 1
⊢ ‖a.toProd.2 (star (a.toProd.1 (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊

Tactic:
a.central

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁸ : DenselyNormedField 𝕜
inst✝⁷ : StarRing 𝕜
inst✝⁶ : NonUnitalNormedRing A
inst✝⁵ : StarRing A
inst✝⁴ : CStarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : SMulCommClass 𝕜 A A
inst✝¹ : IsScalarTower 𝕜 A A
inst✝ : StarModule 𝕜 A
a : 𝓜(𝕜, A)
hball : (Metric.closedBall 0 1).Nonempty
x y : A
hx : ‖x‖₊ ≤ 1
hy : ‖y‖₊ ≤ 1
⊢ ‖star (a.toProd.1 (star x)) * a.toProd.1 y‖₊ ≤ ‖a‖₊ * ‖a‖₊
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
x : X
inst✝ : Nonempty I
h✝ : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst✝²] U
hfU : IsOpen[inst✝³] (f ⁻¹' U)
H : ↑(f ⁻¹' U) ≃ₜ ↑U × I
hH : ∀ (x : ↑(f ⁻¹' U)), ↑(H x).1 = f ↑x
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceProd] fun ui ↦ (⟨(↑ui).1, ⋯⟩, (↑ui).2)

Tactic:
by fun_prop

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

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝² : TopologicalSpace E
inst✝¹ : TopologicalSpace X
f : E → X
s : Set X
I : Type u_3
inst✝ : TopologicalSpace I
x : X
hxs : x ∈ s
h : IsEvenlyCovered f x I
inst : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst✝¹] U
hfU : IsOpen[inst✝²] (f ⁻¹' U)
H : ↑(f ⁻¹' U) ≃ₜ ↑U × I
hH : ∀ (x : ↑(f ⁻¹' U)), ↑(H x).1 = f ↑x
⊢ Continuous[instTopologicalSpaceSubtype, inst✝¹] Subtype.val

Tactic:
by fun_prop

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

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
f : E → X
s : Set X
hf : IsCoveringMapOn f s
x : E
hx : x ∈ f ⁻¹' s
this : Nonempty ↑(f ⁻¹' {f x})
e : Trivialization (↑(f ⁻¹' {f x})) f := ⋯.toTrivialization
h : f x ∈ ⋯.toTrivialization.baseSet
he : x ∈ e.source := (Trivialization.mem_source e).mpr h
⊢ ContinuousOn (fun p ↦ (p, ⟨x, ⋯⟩)) e.baseSet

Tactic:
by fun_prop

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

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
f : E → X
e₁ : E
hf : IsEvenlyCovered f (f e₁) ↑(f ⁻¹' {f e₁})
e₂ : E
he : f e₁ = f e₂
hne : e₁ ≠ e₂
this✝ : Nonempty ↑(f ⁻¹' {f e₁})
t : Trivialization (↑(f ⁻¹' {f e₁})) f := hf.toTrivialization
this : DiscreteTopology ↑(f ⁻¹' {f e₁})
he₁ : f e₁ ∈ hf.toTrivialization.baseSet
⊢ ∃ s₁ s₂, IsOpen[inst✝¹] s₁ ∧ IsOpen[inst✝¹] s₂ ∧ e₁ ∈ s₁ ∧ e₂ ∈ s₂ ∧ Disjoint s₁ s₂

Tactic:
have he₂ := he₁

Goal state after:
E : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalSpace X
f : E → X
e₁ : E
hf : IsEvenlyCovered f (f e₁) ↑(f ⁻¹' {f e₁})
e₂ : E
he : f e₁ = f e₂
hne : e₁ ≠ e₂
this✝ : Nonempty ↑(f ⁻¹' {f e₁})
t : Trivialization (↑(f ⁻¹' {f e₁})) f := hf.toTrivialization
this : DiscreteTopology ↑(f ⁻¹' {f e₁})
he₁ he₂ : f e₁ ∈ hf.toTrivialization.baseSet
⊢ ∃ s₁ s₂, IsOpen[inst✝¹] s₁ ∧ IsOpen[inst✝¹] s₂ ∧ e₁ ∈ s₁ ∧ e₂ ∈ s₂ ∧ Disjoint s₁ s₂
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
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpaceSubtype] (Prod.snd ∘ ⇑H)

Tactic:
by fun_prop

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

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : RCLike 𝕜
p : A → Prop
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : ContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
| exp a

Tactic:
← cfc_id 𝕜 a ha,

Goal state after:
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : RCLike 𝕜
p : A → Prop
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : ContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
| exp (cfc id a)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic

Goal state before:
pp: 𝕜 : Type u_1
A : Type u_2
inst✝⁴ : RCLike 𝕜
p : A → Prop
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : ContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
h : Continuous ⇑(cfcHom ha)
x✝ : ContinuousOn exp (spectrum 𝕜 a)
this : Algebra ℚ A
⊢ (cfcHom ha) { toFun := (spectrum 𝕜 a).domRestrict exp, continuous_toFun := ⋯ } =
    (cfcHom ha) (exp { toFun := (spectrum 𝕜 a).domRestrict id, continuous_toFun := ⋯ })

Tactic:
congr 1

Goal state after:
case e_6
𝕜 : Type u_1
A : Type u_2
inst✝⁴ : RCLike 𝕜
p : A → Prop
inst✝³ : NormedRing A
inst✝² : StarRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : ContinuousFunctionalCalculus 𝕜 A p
a : A
ha : p a
h : Continuous ⇑(cfcHom ha)
x✝ : ContinuousOn exp (spectrum 𝕜 a)
this : Algebra ℚ A
⊢ { toFun := (spectrum 𝕜 a).domRestrict exp, continuous_toFun := ⋯ } =
    exp { toFun := (spectrum 𝕜 a).domRestrict id, continuous_toFun := ⋯ }
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: r s : ℝ
⊢ exp r = exp s ↔ r ≡ s [PMOD 2 * π]

Tactic:
by
  simp [AddCommGroup.modEq_iff_zsmul', ← exp_eq_one, div_eq_one, eq_comm (a := exp r)]

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
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : IsStrictlyPositive a
ha₂ : ∀ x ∈ spectrum ℝ a, x ≠ 0
⊢ ContinuousOn Real.exp (Real.log '' spectrum ℝ a)

Tactic:
by fun_prop

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

Goal state before:
pp: z : Circle
s : ℝ
n : ℕ
hs : s ≤ π
h1 : |(↑z).arg| < π / ↑n
h2 : |(↑(z ^ n)).arg| < s
hs0 : 0 < s
hn0 : n ≠ 0
hn : 1 ≤ ↑n
⊢ ↑n * |(↑z).arg| < s

Tactic:
coe_pow,

Goal state after:
z : Circle
s : ℝ
n : ℕ
hs : s ≤ π
h1 : |(↑z).arg| < π / ↑n
h2 : |(↑z ^ n).arg| < s
hs0 : 0 < s
hn0 : n ≠ 0
hn : 1 ≤ ↑n
⊢ ↑n * |(↑z).arg| < s
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
⊢ exp (x.angleDiff y) * x = y

Tactic:
rw [← exp_arg x, ← exp_add, angleDiff]

Goal state after:
x y : Circle
⊢ exp
      ((if (↑(exp (↑x).arg)).arg ≤ (↑y).arg then (↑y).arg - (↑(exp (↑x).arg)).arg
        else 2 * π + (↑y).arg - (↑(exp (↑x).arg)).arg) +
        (↑x).arg) =
    y
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: T : ℝ
⊢ Continuous (HMul.hMul (2 * π / T))

Tactic:
by fun_prop

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
a✝ : Nontrivial A
this : spectrum ℂ ↑(expUnitary x) ⊆ slitPlane
| ↑x

Tactic:
rw [← cfc_id' ℂ (x : A)]

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
x : ↥(selfAdjoint A)
hx : ‖x‖ < π
a✝ : Nontrivial A
this : spectrum ℂ ↑(expUnitary x) ⊆ slitPlane
| cfc (fun x ↦ x) ↑x