mathlib-initiative/mathlib-tactics huggingface dataset:
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
e : E
he : e ∈ f ⁻¹' V
⊢ (if h : f e ∈ V then inv (if he : f e ∈ V then idx e he else Classical.arbitrary ι) ⋯
    else Classical.arbitrary (X → E) (f e)) =
    e

Tactic:
[

Goal state after:
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
e : E
he : e ∈ f ⁻¹' V
⊢ (if h : f e ∈ V then inv (if he : f e ∈ V then idx e he else Classical.arbitrary ι) ⋯
    else Classical.arbitrary (X → E) (f e)) =
    e
Module: Mathlib.Topology.Covering.Quotient

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

Tactic:
[

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

Tactic:
[

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
f : C(α, 𝕜)
a : α
⊢ (exp f) a = { toFun := exp ∘ ⇑f, continuous_toFun := ⋯ } a

Tactic:
[

Goal state after:
𝕜 : Type u_1
α : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
f : C(α, 𝕜)
a : α
⊢ (exp f) a = { toFun := exp ∘ ⇑f, continuous_toFun := ⋯ } a
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
f : C(α, 𝕜)
a : α
h_sum : Summable fun n ↦ (expSeries 𝕜 C(α, 𝕜) n) fun x ↦ f
⊢ (∑' (n : ℕ), (expSeries 𝕜 C(α, 𝕜) n) fun x ↦ f) a = { toFun := exp ∘ ⇑f, continuous_toFun := ⋯ } a

Tactic:
[

Goal state after:
𝕜 : Type u_1
α : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : TopologicalSpace α
inst✝ : CompactSpace α
f : C(α, 𝕜)
a : α
h_sum : Summable fun n ↦ (expSeries 𝕜 C(α, 𝕜) n) fun x ↦ f
⊢ (∑' (n : ℕ), (expSeries 𝕜 C(α, 𝕜) n) fun x ↦ f) a = { toFun := exp ∘ ⇑f, continuous_toFun := ⋯ } 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
⊢ cfc exp a = exp ((cfcHom ha) { toFun := (spectrum 𝕜 a).domRestrict id, continuous_toFun := ⋯ })

Tactic:
[

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
h : Continuous ⇑(cfcHom ha)
x✝ : ContinuousOn exp (spectrum 𝕜 a)
this : Algebra ℚ A
⊢ cfc exp a = exp ((cfcHom ha) { toFun := (spectrum 𝕜 a).domRestrict id, continuous_toFun := ⋯ })
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic

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

Tactic:
[

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

Goal state before:
pp: r : ℝ
hr : r ≤ π
⊢ BijOn (⇑exp) (Ioo (-r) r) (centeredArc r)

Tactic:
[

Goal state after:
r : ℝ
hr : r ≤ π
⊢ BijOn (⇑exp) (Ioo (-r) r) (centeredArc r)
Module: Mathlib.Topology.Covering.Basic

Goal state before:
pp: case refine_3
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
i : ι
⊢ ContinuousOn (fun x ↦ F.invFun (x, i)) {a | (a, i) ∈ F.target}

Tactic:
[

Goal state after:
case refine_3
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
i : ι
⊢ ContinuousOn (fun x ↦ F.invFun (x, i)) {a | (a, i) ∈ F.target}
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: x y : Circle
h : x ≠ y
⊢ ⇑(x.path y) '' insert 0 (insert 1 (Ioo 0 1)) ∩ ⇑(y.path x) '' insert 0 (insert 1 (Ioo 0 1)) = {x, y}

Tactic:
[

Goal state after:
x y : Circle
h : x ≠ y
⊢ ⇑(x.path y) '' insert 0 (insert 1 (Ioo 0 1)) ∩ ⇑(y.path x) '' insert 0 (insert 1 (Ioo 0 1)) = {x, y}
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case inr
x y : Circle
hyx : y ≠ x
hxP : x ∈ range ⇑((-x).path y)
⊢ JoinedIn {x}ᶜ (-x) y

Tactic:
refine ⟨(path y (-x)).symm, ?_⟩

Goal state after:
case inr
x y : Circle
hyx : y ≠ x
hxP : x ∈ range ⇑((-x).path y)
⊢ ∀ (t : ↑unitInterval), (y.path (-x)).symm t ∈ {x}ᶜ
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
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✝¹] s
⊢ f ⁻¹' s ∩ V' e = (φ e).source ∩ ↑(φ e) ⁻¹' s ∩ V ↑e

Tactic:
[

Goal state after:
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✝¹] s
⊢ f ⁻¹' s ∩ V' e = (φ e).source ∩ ↑(φ e) ⁻¹' s ∩ V ↑e
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case h
x✝ : ℝ
⊢ (-↑x✝).toCircle = (↑x✝).toCircle⁻¹

Tactic:
[

Goal state after:
case h
x✝ : ℝ
⊢ (-↑x✝).toCircle = (↑x✝).toCircle⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case inr
T : ℝ
hT : T ≠ 0
x : ℝ
⊢ Circle.exp (2 * π / T * (x + T)) = Circle.exp (2 * π / T * x)

Tactic:
[

Goal state after:
case inr
T : ℝ
hT : T ≠ 0
x : ℝ
⊢ Circle.exp (2 * π / T * (x + T)) = Circle.exp (2 * π / T * x)
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case H.H
T z✝¹ z✝ : ℝ
⊢ (↑z✝¹ + ↑z✝).toCircle = toCircle ↑z✝¹ * toCircle ↑z✝

Tactic:
[

Goal state after:
case H.H
T z✝¹ z✝ : ℝ
⊢ (↑z✝¹ + ↑z✝).toCircle = toCircle ↑z✝¹ * toCircle ↑z✝
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

Goal state before:
pp: case H.H
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : toCircle ↑z✝¹ = toCircle ↑z✝
⊢ ↑z✝¹ = ↑z✝

Tactic:
[

Goal state after:
case H.H
T : ℝ
hT : T ≠ 0
z✝¹ z✝ : ℝ
h : toCircle ↑z✝¹ = toCircle ↑z✝
⊢ ↑z✝¹ = ↑z✝
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✝)
m : ℤ
hm : 2 * π / T * z✝ = 2 * π / T * z✝¹ + ↑m * (2 * π)
⊢ -z✝¹ + z✝ ∈ AddSubgroup.zmultiples T

Tactic:
[

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✝ ∈ AddSubgroup.zmultiples T
Module: Mathlib.Analysis.SpecialFunctions.Complex.Circle

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

Tactic:
[

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

Goal state before:
pp: ⊢ Filter.Tendsto (fun i ↦ π / 2 ^ (i + 1)) Filter.atTop (nhds 0)

Tactic:
[

Goal state after:
⊢ Filter.Tendsto (fun i ↦ π / 2 ^ (i + 1)) Filter.atTop (nhds 0)
Module: Mathlib.Analysis.Normed.Module.Normalize

Goal state before:
pp: case inr.inr
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : NormedSpace ℝ V
r : ℝ
x : V
h_neg : r < 0
⊢ normalize (r • x) = ↑(SignType.sign r) • normalize x

Tactic:
simp [normalize_smul_of_neg, h_neg]

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

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
t : ℝ
ht : t ∈ Set.Icc 0 1
hu : ‖↑u - 1‖ < 2
⊢ ‖t • argSelfAdjoint u‖ ≤ 1 * ‖argSelfAdjoint u‖

Tactic:
[

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
u : ↥(unitary A)
t : ℝ
ht : t ∈ Set.Icc 0 1
hu : ‖↑u - 1‖ < 2
⊢ ‖t • argSelfAdjoint u‖ ≤ 1 * ‖argSelfAdjoint u‖
Module: Mathlib.Analysis.CStarAlgebra.Unitary.Span

Goal state before:
pp: A : Type u_1
inst✝ : CStarAlgebra A
x : A
x✝¹ : (A : Type u_1) → [NonUnitalCStarAlgebra A] → PartialOrder A := spectralOrder
x✝ : ∀ (A : Type u_1) [inst : NonUnitalCStarAlgebra A], StarOrderedRing A := spectralOrderedRing
hx : x ≠ 0
u₁ : ↥(unitary A) := selfAdjoint.unitarySelfAddISMul (ℜ (‖x‖⁻¹ • x)) ⋯
u₂ : ↥(unitary A) := selfAdjoint.unitarySelfAddISMul (ℑ (‖x‖⁻¹ • x)) ⋯
this : x = ‖x‖ • 2⁻¹ • (↑u₁ + ↑(star u₁) + I • (↑u₂ + ↑(star u₂)))
| x

Tactic:
this

Goal state after:
A : Type u_1
inst✝ : CStarAlgebra A
x : A
x✝¹ : (A : Type u_1) → [NonUnitalCStarAlgebra A] → PartialOrder A := spectralOrder
x✝ : ∀ (A : Type u_1) [inst : NonUnitalCStarAlgebra A], StarOrderedRing A := spectralOrderedRing
hx : x ≠ 0
u₁ : ↥(unitary A) := selfAdjoint.unitarySelfAddISMul (ℜ (‖x‖⁻¹ • x)) ⋯
u₂ : ↥(unitary A) := selfAdjoint.unitarySelfAddISMul (ℑ (‖x‖⁻¹ • x)) ⋯
this : x = ‖x‖ • 2⁻¹ • (↑u₁ + ↑(star u₁) + I • (↑u₂ + ↑(star u₂)))
| ‖x‖ • 2⁻¹ • (↑u₁ + ↑(star u₁) + I • (↑u₂ + ↑(star u₂)))
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:
[

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

Goal state before:
pp: case a
𝕜 : 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
x : E
hx : x ∈ (↑T).ker
y : F
⊢ ⟪↑(adjoint T) y, x⟫_𝕜 = 0

Tactic:
simp_all [T.adjoint_inner_left]

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

Goal state before:
pp: f : ℝ → ℝ
s : Set ℝ
hs : UniqueDiffOn ℝ s
⊢ AbsolutelyMonotoneOn f s ↔ ContDiffOn ℝ ∞ f s ∧ ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ iteratedDerivWithin n f s x

Tactic:
by
  refine ⟨fun hf => ⟨hf.contDiffOn, fun n x hx => hf.iteratedDerivWithin_nonneg hs n hx⟩, ?_⟩
  rintro ⟨hcont, hnn⟩
  refine ⟨ftaylorSeriesWithin ℝ f s, hcont.ftaylorSeriesWithin hs, fun n x hx => ?_⟩
  exact iteratedDerivWithin_eq_iteratedFDerivWithin (𝕜 := ℝ) (f := f) (s := s) ▸ hnn n x hx

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

Goal state before:
pp: case hbc
𝕜 : 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
x : E
⊢ ‖(adjoint A ∘SL A) x‖ ≤ ‖adjoint A ∘SL A‖ * ‖x‖

Tactic:
exact le_opNorm _ _

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
x : E
this : re ⟪(adjoint A ∘SL A) x, x⟫_𝕜 ≤ ‖adjoint A ∘SL A‖ * ‖x‖ * ‖x‖
⊢ √(‖adjoint A ∘SL A‖ * ‖x‖ * ‖x‖) = √‖adjoint A ∘SL A‖ * ‖x‖

Tactic:
[

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
A : E →L[𝕜] F
x : E
this : re ⟪(adjoint A ∘SL A) x, x⟫_𝕜 ≤ ‖adjoint A ∘SL A‖ * ‖x‖ * ‖x‖
⊢ √(‖adjoint A ∘SL A‖ * ‖x‖ * ‖x‖) = √‖adjoint A ∘SL A‖ * ‖x‖
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
F : Type u_3
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : CompleteSpace F
E : Type u_5
G : Type u_6
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup G
inst✝¹ : InnerProductSpace 𝕜 G
inst✝ : CompleteSpace G
x : E
y : F
f : G →L[𝕜] F
⊢ ((rankOne 𝕜) x) y ∘SL f = ((rankOne 𝕜) x) ((adjoint f) y)

Tactic:
[

Goal state after:
𝕜 : Type u_1
F : Type u_3
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : InnerProductSpace 𝕜 F
inst✝⁵ : CompleteSpace F
E : Type u_5
G : Type u_6
inst✝⁴ : SeminormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup G
inst✝¹ : InnerProductSpace 𝕜 G
inst✝ : CompleteSpace G
x : E
y : F
f : G →L[𝕜] F
⊢ ((rankOne 𝕜) x) y ∘SL f = ((rankOne 𝕜) x) ((adjoint f) y)
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst✝ : CompleteSpace E
⊢ star T * T - T * star T = 0 ↔ ∀ (v : E), ‖T v‖ = ‖(adjoint T) v‖

Tactic:
[

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst✝ : CompleteSpace E
⊢ star T * T - T * star T = 0 ↔ ∀ (v : E), ‖T v‖ = ‖(adjoint T) v‖
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst✝ : CompleteSpace E
this : (↑(adjoint T * T) - ↑(T * adjoint T)).IsSymmetric
⊢ ↑(star T * T) - ↑(T * star T) = 0 ↔ ∀ (v : E), ‖↑T v‖ = ‖↑(adjoint T) v‖

Tactic:
[

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst✝ : CompleteSpace E
this : (↑(adjoint T * T) - ↑(T * adjoint T)).IsSymmetric
⊢ ↑(star T * T) - ↑(T * star T) = 0 ↔ ∀ (v : E), ‖↑T v‖ = ‖↑(adjoint T) v‖
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst✝ : CompleteSpace E
hT : IsStarNormal T
x : E
⊢ (adjoint T) x = 0 ↔ T x = 0

Tactic:
[

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst✝ : CompleteSpace E
hT : IsStarNormal T
x : E
⊢ (adjoint T) x = 0 ↔ T x = 0
Module: Mathlib.Analysis.InnerProductSpace.Adjoint

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst✝ : CompleteSpace E
hT : IsIdempotentElem T
h : IsStarNormal T
⊢ ∀ (x : E), (T - star T * T) x = 0 x

Tactic:
[

Goal state after:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
inst✝ : CompleteSpace E
hT : IsIdempotentElem T
h : IsStarNormal T
⊢ ∀ (x : E), (T - star T * T) x = 0 x
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
⊢ IsStarProjection p ↔ ∃ (x : (↑p).range.HasOrthogonalProjection), p = (↑p).range.starProjection

Tactic:
[

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
⊢ IsStarProjection p ↔ ∃ (x : (↑p).range.HasOrthogonalProjection), p = (↑p).range.starProjection
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
⊢ (∃ K, ∃ (x : K.HasOrthogonalProjection), p = K.starProjection) → IsStarProjection p

Tactic:
rintro ⟨_, _, rfl⟩; simp

Goal state after: