mathlib-initiative/mathlib-tactics huggingface dataset:
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✝¹ : StarRing A
inst✝ : CStarRing A
a : 𝓜(𝕜, A)
⊢ ‖a.toProd.2‖ = ‖a‖

Tactic:
by

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)
⊢ ‖star a * a‖₊ = ‖a‖₊ * ‖a‖₊

Tactic:
have hball : (Metric.closedBall (0 : A) 1).Nonempty :=
        Metric.nonempty_closedBall.2 zero_le_one

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
⊢ ‖star a * a‖₊ = ‖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
e : E
he : f e ∈ U
⊢ (if he : f e ∈ U then (↑(H ⟨e, he⟩).1, (H ⟨e, he⟩).2) else (x, Classical.arbitrary I)) ∈ U ×ˢ Set.univ

Tactic:
by

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.1‖₊ * 1 * (‖a.toProd.1‖₊ * 1) ≤ ‖a‖₊ * ‖a‖₊

Tactic:
by

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), ‖x‖₊ ≤ 1 → ‖y‖₊ ≤ 1 → ‖a.toProd.2 (star (a.toProd.1 (star x))) * y‖₊ ≤ ‖a‖₊ * ‖a‖₊

Tactic:
by

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
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
e : E
he : f e ∈ U
⊢ ↑(H.symm
        (if hx : (if he : f e ∈ U then (↑(H ⟨e, he⟩).1, (H ⟨e, he⟩).2) else (x, Classical.arbitrary I)).1 ∈ U then
            ⟨(if he : f e ∈ U then (↑(H ⟨e, he⟩).1, (H ⟨e, he⟩).2) else (x, Classical.arbitrary I)).1, hx⟩
          else ⟨x, hxU⟩,
          (if he : f e ∈ U then (↑(H ⟨e, he⟩).1, (H ⟨e, he⟩).2) else (x, Classical.arbitrary I)).2)) =
    e

Tactic:
by

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
hf : IsLocalHomeomorph f
⊢ IsTopologicalBasis {U | ∃ V, IsOpen[inst✝] V ∧ ∃ s, f ∘ ⇑s = Subtype.val ∧ Set.range ⇑s = U}

Tactic:
by

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
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
xi : X × I
⊢ xi ∈ U ×ˢ Set.univ →
    (if he : f ↑(H.symm (if hx : xi.1 ∈ U then ⟨xi.1, hx⟩ else ⟨x, hxU⟩, xi.2)) ∈ U then
        (↑(H ⟨↑(H.symm (if hx : xi.1 ∈ U then ⟨xi.1, hx⟩ else ⟨x, hxU⟩, xi.2)), he⟩).1,
          (H ⟨↑(H.symm (if hx : xi.1 ∈ U then ⟨xi.1, hx⟩ else ⟨x, hxU⟩, xi.2)), he⟩).2)
      else (x, Classical.arbitrary I)) =
      xi

Tactic:
by

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
hf : IsLocalHomeomorph f
x : X
⊢ f x ∈ (hf.localInverseAt x).source

Tactic:
by

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
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
x✝ : ↑(f ⁻¹' U)
e : E
he : f e ∈ U
⊢ (Prod.map Subtype.val id ∘ ⇑H) ⟨e, he⟩ =
    (f ⁻¹' U).domRestrict (fun e ↦ if he : f e ∈ U then (↑(H ⟨e, he⟩).1, (H ⟨e, he⟩).2) else (x, Classical.arbitrary I))
      ⟨e, he⟩

Tactic:
by

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
hf : IsLocalHomeomorph f
x y : X
x✝ : y ∈ (hf.localInverseAt x).target
⊢ f y = ↑(hf.localInverseAt x).symm y

Tactic:
by

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
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

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
hf : IsLocalHomeomorph f
x : X
⊢ Set.InjOn f (hf.localInverseAt x).target

Tactic:
by

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
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
x✝ : ↑(U ×ˢ Set.univ)
x : X
i : I
hx : (x, i).1 ∈ U
right✝ : (x, i).2 ∈ Set.univ
⊢ ((Subtype.val ∘ ⇑H.symm) ∘ fun ui ↦ (⟨(↑ui).1, ⋯⟩, (↑ui).2)) ⟨(x, i), ⋯⟩ =
    (U ×ˢ Set.univ).domRestrict (fun xi ↦ ↑(H.symm (if hx : xi.1 ∈ U then ⟨xi.1, hx⟩ else ⟨x✝¹, hxU⟩, xi.2)))
      ⟨(x, i), ⋯⟩

Tactic:
by

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
hf : IsLocalHomeomorph f
x : X
y : Y
hx : y ∈ (hf.localInverseAt x).source
⊢ f (↑(hf.localInverseAt x) y) = y

Tactic:
by

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
hf : IsLocalHomeomorph f
x : X
⊢ ↑(hf.localInverseAt x) (f x) ∈ (hf.localInverseAt x).target

Tactic:
by

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
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
e : E
he : f e ∈ U
⊢ (↑{ toFun := fun e ↦ if he : f e ∈ U then (↑(H ⟨e, he⟩).1, (H ⟨e, he⟩).2) else (x, Classical.arbitrary I),
            invFun := fun xi ↦ ↑(H.symm (if hx : xi.1 ∈ U then ⟨xi.1, hx⟩ else ⟨x, hxU⟩, xi.2)), source := f ⁻¹' U,
            target := U ×ˢ Set.univ, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯,
            continuousOn_toFun := ⋯, continuousOn_invFun := ⋯, open_source := hfU, open_target := ⋯ }
        e).1 =
    f e

Tactic:
by

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
inst✝ : Nonempty I
h : IsEvenlyCovered f x I
⊢ Trivialization I f

Tactic:
by

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
I : Type u_3
inst✝¹ : TopologicalSpace I
x : E
inst✝ : Nonempty I
h : IsEvenlyCovered f (f x) I
⊢ h.fiberHomeomorph.symm (↑h.toTrivialization x).2 = h.fiberHomeomorph.symm ⟨x, ⋯⟩

Tactic:
by

Goal state after:
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_4
inst✝¹ : AddGroup G
inst✝ : AddAction G E
hf : IsAddQuotientCoveringMap f G
g : Multiplicative G
⊢ Continuous[inst✝³, inst✝³] fun x ↦ g • x

Tactic:
by

Goal state after:
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_4
inst✝¹ : AddGroup G
inst✝ : AddAction G E
hf : IsAddQuotientCoveringMap f G
e₁ e₂ : E
⊢ f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit (Multiplicative G) e₂

Tactic:
by

Goal state after:
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_4
inst✝¹ : AddGroup G
inst✝ : AddAction G E
hf : IsAddQuotientCoveringMap f G
e : E
U : Set E
hU : U ∈ 𝓝 e
hU' : ∀ (g : G), ((fun x ↦ g +ᵥ x) '' U ∩ U).Nonempty → g = 0
g : Multiplicative G
⊢ ((fun x ↦ g • x) '' U ∩ U).Nonempty → g = 1

Tactic:
by

Goal state after:
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_4
inst✝¹ : AddGroup G
inst✝ : AddAction G E
hf : IsAddQuotientCoveringMap f G
e : E
⊢ ∃ U ∈ 𝓝 e, ∀ (g : Multiplicative G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g = 1

Tactic:
by

Goal state after:
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_4
inst✝¹ : Group G
inst✝ : MulAction G E
hf : IsQuotientCoveringMap f G
g : Additive G
⊢ Continuous[inst✝³, inst✝³] fun x ↦ g +ᵥ x

Tactic:
by

Goal state after:
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_4
inst✝¹ : Group G
inst✝ : MulAction G E
hf : IsQuotientCoveringMap f G
e₁ e₂ : E
⊢ f e₁ = f e₂ ↔ e₁ ∈ AddAction.orbit (Additive G) e₂

Tactic:
by

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
I : Type u_3
inst✝¹ : TopologicalSpace I
J : Type u_4
inst✝ : TopologicalSpace J
g : I ≃ₜ J
x : X
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
x✝ : ↑(f ⁻¹' U)
⊢ ↑((H.trans ((Homeomorph.refl ↑U).prodCongr g)) x✝).1 = f ↑x✝

Tactic:
by

Goal state after:
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_4
inst✝¹ : Group G
inst✝ : MulAction G E
hf : IsQuotientCoveringMap f G
e : E
U : Set E
hU : U ∈ 𝓝 e
hU' : ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g = 1
g : Additive G
⊢ ((fun x ↦ g +ᵥ x) '' U ∩ U).Nonempty → g = 0

Tactic:
by

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
I : Type u_3
inst✝¹ : TopologicalSpace I
inst✝ : DiscreteTopology I
x : X
t : Trivialization I f
hx : x ∈ t.baseSet
xi : ↑t.baseSet × I
⊢ t.invFun (↑xi.1, xi.2) ∈ f ⁻¹' t.baseSet

Tactic:
by

Goal state after:
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_4
inst✝¹ : Group G
inst✝ : MulAction G E
hf : IsQuotientCoveringMap f G
e : E
⊢ ∃ U ∈ 𝓝 e, ∀ (g : Additive G), ((fun x ↦ g +ᵥ x) '' U ∩ U).Nonempty → g = 0

Tactic:
by

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
I : Type u_3
inst✝¹ : TopologicalSpace I
inst✝ : DiscreteTopology I
x : X
t : Trivialization I f
hx : x ∈ t.baseSet
xi : ↑t.baseSet × I
⊢ (fun e ↦ (⟨f ↑e, ⋯⟩, (↑t ↑e).2)) ((fun xi ↦ ⟨t.invFun (↑xi.1, xi.2), ⋯⟩) xi) = xi

Tactic:
by

Goal state after:
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
S S' : Subgroup G
eq : S = S'
⊢ IsQuotientCoveringMap f ↥S ↔ IsQuotientCoveringMap f ↥S'

Tactic:
by

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
I : Type u_3
inst✝¹ : TopologicalSpace I
inst✝ : DiscreteTopology I
x : X
t : Trivialization I f
hx : x ∈ t.baseSet
e : ↑(f ⁻¹' t.baseSet)
⊢ (f ⁻¹' t.baseSet).domRestrict (↑t.toPartialEquiv) e = (Prod.map Subtype.val id ∘ fun e ↦ (⟨f ↑e, ⋯⟩, (↑t ↑e).2)) e

Tactic:
by

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

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
G : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G E
hf : IsQuotientCoveringMap f G
g g' : G
e : E
eq : g • e = g' • e
U : Set E
heU : U ∈ 𝓝 e
hU : ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g = 1
⊢ (fun x ↦ (g'⁻¹ * g) • x) e = e

Tactic:
by

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

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
G : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G E
hf : IsQuotientCoveringMap f G
g g' : G
e : E
eq : g • e = g' • e
⊢ g = g'

Tactic:
by

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
I : Type u_3
inst✝¹ : TopologicalSpace I
inst✝ : DiscreteTopology I
x : X
t : Trivialization I f
hx : x ∈ t.baseSet
x✝ : ↑(f ⁻¹' t.baseSet)
⊢ ↑({ toFun := fun e ↦ (⟨f ↑e, ⋯⟩, (↑t ↑e).2), invFun := fun xi ↦ ⟨t.invFun (↑xi.1, xi.2), ⋯⟩, left_inv := ⋯,
            right_inv := ⋯, continuous_toFun := ⋯, continuous_invFun := ⋯ }
          x✝).1 =
    f ↑x✝

Tactic:
by

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

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace X
f : E → X
G : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G E
hf : IsQuotientCoveringMap f G
Y : Type u_4
inst✝ : TopologicalSpace Y
φ : X ≃ₜ Y
⊢ ∀ {e₁ e₂ : E}, (⇑φ ∘ f) e₁ = (⇑φ ∘ f) e₂ ↔ e₁ ∈ MulAction.orbit G e₂

Tactic:
by

Goal state after:
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
Y : Type u_4
inst✝ : TopologicalSpace Y
φ : X ≃ₜ Y
h : IsQuotientCoveringMap (⇑φ ∘ f) G
⊢ IsQuotientCoveringMap f G

Tactic:
by

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

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

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
G : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G E
hf : IsQuotientCoveringMap f G
x : X
e e' : ↑(f ⁻¹' {x})
g : G
⊢ (hf.fiberEquivGroup e) e' = g ↔ ↑e' = g • ↑e

Tactic:
by

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

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
G : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G E
hf : IsQuotientCoveringMap f G
x : X
⊢ MulAction.IsPretransitive G ↑(f ⁻¹' {x})

Tactic:
by

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
e : ↑(s.restrictPreimage f ⁻¹' Subtype.val ⁻¹' U)
⊢ ⟨↑(H ⟨↑↑e, ⋯⟩).1, ⋯⟩ ∈ Subtype.val ⁻¹' U

Tactic:
by

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

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace X
f : E → X
G : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G E
hf : IsQuotientCoveringMap f G
x : X
e e' : ↑(f ⁻¹' {x})
⊢ ∃ g, ((hf.toPermFiber x) g) e = e'

Tactic:
by

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
x : ↑(Subtype.val ⁻¹' U) × I
⊢ ↑(H.symm (⟨↑↑x.1, ⋯⟩, x.2)) ∈ f ⁻¹' s

Tactic:
by

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
x : ↑(Subtype.val ⁻¹' U) × I
⊢ ⟨↑(H.symm (⟨↑↑x.1, ⋯⟩, x.2)), ⋯⟩ ∈ s.restrictPreimage f ⁻¹' Subtype.val ⁻¹' U

Tactic:
by

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
x✝ : ↑(s.restrictPreimage f ⁻¹' Subtype.val ⁻¹' U)
⊢ (fun x ↦ ⟨⟨↑(H.symm (⟨↑↑x.1, ⋯⟩, x.2)), ⋯⟩, ⋯⟩) ((fun e ↦ (⟨⟨↑(H ⟨↑↑e, ⋯⟩).1, ⋯⟩, ⋯⟩, (H ⟨↑↑e, ⋯⟩).2)) x✝) = x✝

Tactic:
by

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

Goal state before:
pp: E : Type u_1
X : Type u_2
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace X
f : E → X
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulAction G E
hf : IsQuotientMap f
inst✝² : ContinuousConstSMul G E
hfG : ∀ {e₁ e₂ : E}, f e₁ = f e₂ ↔ e₁ ∈ MulAction.orbit G e₂
inst✝¹ : TopologicalSpace G
inst✝ : DiscreteTopology G
U : Set E
open_U : IsOpen[inst✝⁶] U
disjoint : ∀ (g : G), ((fun x ↦ g • x) '' U ∩ U).Nonempty → g = 1
pGE : ∀ (g : G) (e : E), f (g • e) = f e
⊢ f ⁻¹' f '' U = ⋃ g, (fun x ↦ g • x) ⁻¹' U

Tactic:
by

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
x✝ : ↑(Subtype.val ⁻¹' U) × I
⊢ (fun e ↦ (⟨⟨↑(H ⟨↑↑e, ⋯⟩).1, ⋯⟩, ⋯⟩, (H ⟨↑↑e, ⋯⟩).2)) ((fun x ↦ ⟨⟨↑(H.symm (⟨↑↑x.1, ⋯⟩, x.2)), ⋯⟩, ⋯⟩) x✝) = x✝

Tactic:
by

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
x✝ : ↑(s.restrictPreimage f ⁻¹' Subtype.val ⁻¹' U)
⊢ ↑({ toFun := fun e ↦ (⟨⟨↑(H ⟨↑↑e, ⋯⟩).1, ⋯⟩, ⋯⟩, (H ⟨↑↑e, ⋯⟩).2),
            invFun := fun x ↦ ⟨⟨↑(H.symm (⟨↑↑x.1, ⋯⟩, x.2)), ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯,
            continuous_toFun := ⋯, continuous_invFun := ⋯ }
          x✝).1 =
    s.restrictPreimage f ↑x✝

Tactic:
by

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
s : Set X
I : Type u_3
inst✝ : TopologicalSpace I
hs : IsOpen[inst✝¹] s
x : ↑s
f : E → ↑s
h : IsEvenlyCovered f x I
inst : DiscreteTopology I
U : Set ↑s
hxU : x ∈ U
hU : IsOpen[instTopologicalSpaceSubtype] U
hfU : IsOpen[inst✝²] (f ⁻¹' U)
H : ↑(f ⁻¹' U) ≃ₜ ↑U × I
hH : ∀ (x : ↑(f ⁻¹' U)), ↑(H x).1 = f ↑x
⊢ Subtype.val ∘ f ⁻¹' Subtype.val '' U = f ⁻¹' U

Tactic:
by

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
s : Set X
I : Type u_3
inst✝ : TopologicalSpace I
hs : IsOpen[inst✝¹] s
x : ↑s
f : E → ↑s
h : IsEvenlyCovered f x I
inst : DiscreteTopology I
U : Set ↑s
hxU : x ∈ U
hU : IsOpen[instTopologicalSpaceSubtype] U
hfU : IsOpen[inst✝²] (f ⁻¹' U)
H : ↑(f ⁻¹' U) ≃ₜ ↑U × I
hH : ∀ (x : ↑(f ⁻¹' U)), ↑(H x).1 = f ↑x
this : Subtype.val ∘ f ⁻¹' Subtype.val '' U = f ⁻¹' U
⊢ IsOpen[inst✝²] (Subtype.val ∘ f ⁻¹' Subtype.val '' U)

Tactic:
by

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
hs : IsOpen[inst✝¹] s
hfs : IsOpen[inst✝²] (f ⁻¹' s)
x : X
hx : x ∈ s
h : IsEvenlyCovered (fun e ↦ f ↑e) x I
inst : DiscreteTopology I
U : Set X
hxU : x ∈ U
hU : IsOpen[inst✝¹] U
hfU : IsOpen[instTopologicalSpaceSubtype] ((fun e ↦ f ↑e) ⁻¹' U)
H : ↑((fun e ↦ f ↑e) ⁻¹' U) ≃ₜ ↑U × I
hH : ∀ (x : ↑((fun e ↦ f ↑e) ⁻¹' U)), ↑(H x).1 = (fun e ↦ f ↑e) ↑x
x✝ : Nonempty I
y : X
hy : y ∈ U
⊢ y ∈ s

Tactic:
by

Goal state after: