mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: case inl
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
f : X → α
⊢ Tendsto (⇑UniformFun.ofFun ∘ F) ⊥ (𝓝 (UniformFun.ofFun f)) ↔ Tendsto F ⊥ (𝓝 f)

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
H : Tendsto F ℱ (𝓝 f)
S : Set (X → α) := closure[Pi.topologicalSpace] (range F)
𝒢 : Filter ↑S := comap Subtype.val (map F ℱ)
hS : S.Equicontinuous
ind : IsInducing (⇑UniformFun.ofFun ∘ Subtype.val)
f_mem : f ∈ S
h𝒢ℱ : map Subtype.val 𝒢 = map F ℱ
⊢ Tendsto id 𝒢 (𝓝 ⟨f, f_mem⟩)

Tactic:
tendsto_id',

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
H : Tendsto F ℱ (𝓝 f)
S : Set (X → α) := closure[Pi.topologicalSpace] (range F)
𝒢 : Filter ↑S := comap Subtype.val (map F ℱ)
hS : S.Equicontinuous
ind : IsInducing (⇑UniformFun.ofFun ∘ Subtype.val)
f_mem : f ∈ S
h𝒢ℱ : map Subtype.val 𝒢 = map F ℱ
⊢ 𝒢 ≤ 𝓝 ⟨f, f_mem⟩
Module: Mathlib.Topology.Algebra.Group.CompactOpen

Goal state before:
pp: X : Type u_7
Y : Type u_8
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group X
inst✝⁶ : IsTopologicalGroup X
inst✝⁵ : UniformSpace Y
inst✝⁴ : CommGroup Y
inst✝³ : IsUniformGroup Y
inst✝² : T0Space Y
inst✝¹ : CompactSpace Y
inst✝ : LocallyCompactSpace X
V : ℕ → Set Y
hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)
hVo : (𝓝 1).HasBasis (fun x ↦ True) V
U0 : Set X
hU0c : IsCompact U0
hU0o : U0 ∈ 𝓝 1
U_aux : ℕ → ↑{S | S ∈ 𝓝 1} :=
  fun t ↦
    Nat.rec ⟨U0, hU0o⟩
      (fun x S ↦
        let h := ⋯;
        ⟨Classical.choose h, ⋯⟩)
      t
U : ℕ → Set X := fun n ↦ ↑(U_aux n)
hU1 : ∀ (n : ℕ), U n ∈ 𝓝 1
hU2 : ∀ (n : ℕ), U (n + 1) * U (n + 1) ⊆ U n
hU3 : ∀ (n : ℕ), U (n + 1) ⊆ U n
f : X →* Y
⊢ Set.MapsTo (⇑f) (U 0) (V 0) → ∀ (n : ℕ), Set.MapsTo (⇑f) (U n) (V n)

Tactic:
hf

Goal state after:
X : Type u_7
Y : Type u_8
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group X
inst✝⁶ : IsTopologicalGroup X
inst✝⁵ : UniformSpace Y
inst✝⁴ : CommGroup Y
inst✝³ : IsUniformGroup Y
inst✝² : T0Space Y
inst✝¹ : CompactSpace Y
inst✝ : LocallyCompactSpace X
V : ℕ → Set Y
hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)
hVo : (𝓝 1).HasBasis (fun x ↦ True) V
U0 : Set X
hU0c : IsCompact U0
hU0o : U0 ∈ 𝓝 1
U_aux : ℕ → ↑{S | S ∈ 𝓝 1} :=
  fun t ↦
    Nat.rec ⟨U0, hU0o⟩
      (fun x S ↦
        let h := ⋯;
        ⟨Classical.choose h, ⋯⟩)
      t
U : ℕ → Set X := fun n ↦ ↑(U_aux n)
hU1 : ∀ (n : ℕ), U n ∈ 𝓝 1
hU2 : ∀ (n : ℕ), U (n + 1) * U (n + 1) ⊆ U n
hU3 : ∀ (n : ℕ), U (n + 1) ⊆ U n
f : X →* Y
hf : Set.MapsTo (⇑f) (U 0) (V 0)
⊢ ∀ (n : ℕ), Set.MapsTo (⇑f) (U n) (V n)
Module: Mathlib.Topology.Algebra.Group.OpenMapping

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
U : Set G
hU : U ∈ 𝓝 1
x : X
V : Set G
V_mem : V ∈ 𝓝 1
V_closed : IsClosed[inst✝⁹] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : ⋃ g ∈ s, g • V = univ
K : ℕ → Set G := compactCovering G
F : ℕ × ↑s → Set X := fun p ↦ (K p.1 ∩ ↑p.2 • V) • {x}
n : ℕ
g : G
hg : g ∈ s
hi : (interior (F (n, ⟨g, hg⟩))).Nonempty
I : (interior ((g • V) • {x})).Nonempty
⊢ (interior (V • {x})).Nonempty

Tactic:
by
    rw [smul_assoc, interior_smul] at I
    exact smul_set_nonempty.1 I

Goal state after:
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: G : GrpCat
P : ProfiniteGrp.{u}
f : completion G ⟶ P
⊢ eta G ≫
      (forget₂ ProfiniteGrp.{u} GrpCat).map
        ((fun f ↦ lift f) ((fun f ↦ eta G ≫ (forget₂ ProfiniteGrp.{u} GrpCat).map f) f)) =
    eta G ≫ (forget₂ ProfiniteGrp.{u} GrpCat).map f

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: G : GrpCat
P : ProfiniteGrp.{u}
f : G ⟶ GrpCat.of ↑P.toProfinite.toTop
⊢ (fun f ↦ eta G ≫ (forget₂ ProfiniteGrp.{u} GrpCat).map f) ((fun f ↦ lift f) f) = f

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.IsOpenUnits

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ ⊥.jacobson
s : Set R
hs : s ∈ Filter.map (⇑(Units.coeHom R)) (Filter.comap (⇑(Units.embedProduct R)) (𝓝 1 ×ˢ 𝓝 1))
H✝ : (𝓝 1).HasBasis (fun _n ↦ True) fun n ↦ (fun y ↦ 1 + y) '' ↑(I ^ n)
this :
  (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ True) fun i ↦
    ((fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.1)) ×ˢ (⇑MulOpposite.opHomeomorph.symm ⁻¹' (fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.2))
n₁ n₂ : ℕ
H : ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n₁ → -1 + ↑u⁻¹ ∈ I ^ n₂ → ↑u ∈ s
⊢ max (max n₁ n₂) 1 ≠ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.IsOpenUnits

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ ⊥.jacobson
s : Set R
hs : s ∈ Filter.map (⇑(Units.coeHom R)) (Filter.comap (⇑(Units.embedProduct R)) (𝓝 1 ×ˢ 𝓝 1))
H✝ : (𝓝 1).HasBasis (fun _n ↦ True) fun n ↦ (fun y ↦ 1 + y) '' ↑(I ^ n)
this :
  (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ True) fun i ↦
    ((fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.1)) ×ˢ (⇑MulOpposite.opHomeomorph.symm ⁻¹' (fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.2))
n₁ n₂ : ℕ
H : ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n₁ → -1 + ↑u⁻¹ ∈ I ^ n₂ → ↑u ∈ s
u : Rˣ
h₁ : -1 + ↑u ∈ I ^ max (max n₁ n₂) 1
h₂ : -1 + ↑u⁻¹ ∈ I ^ max (max n₁ n₂) 1
⊢ n₁ ≤ max (max n₁ n₂) 1

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.Module.IsWeak

Goal state before:
pp: 𝕜 : Type u_2
E : Type u_3
F : Type u_4
E' : Type u_5
F' : Type u_6
inst✝¹⁰ : CommSemiring 𝕜
inst✝⁹ : TopologicalSpace 𝕜
inst✝⁸ : AddCommMonoid E
inst✝⁷ : Module 𝕜 E
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module 𝕜 F
inst : TopologicalSpace E
inst✝⁴ : AddCommMonoid E'
inst✝³ : Module 𝕜 E'
inst✝² : AddCommMonoid F'
inst✝¹ : Module 𝕜 F'
inst✝ : TopologicalSpace E'
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
B' : E' →ₗ[𝕜] F' →ₗ[𝕜] 𝕜
e : E ≃L[𝕜] E'
f : F ≃ₗ[𝕜] F'
hBB' : ((↑e).arrowCongr (f.arrowCongr (LinearEquiv.refl 𝕜 𝕜))) B = B'
hB : B.IsWeak
⊢ ∀ (x : F),
    TopologicalSpace.induced (fun x_1 ↦ ((((↑e).arrowCongr (f.arrowCongr (LinearEquiv.refl 𝕜 𝕜))) B) x_1) (f.toEquiv x))
        inferInstance =
      TopologicalSpace.induced (fun x_1 ↦ ((fun x1 x2 ↦ (B x1) x2) ∘ ⇑e.symm) x_1 x) inferInstance

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.IsOpenUnits

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ ⊥.jacobson
s : Set R
hs : s ∈ Filter.map (⇑(Units.coeHom R)) (Filter.comap (⇑(Units.embedProduct R)) (𝓝 1 ×ˢ 𝓝 1))
H✝ : (𝓝 1).HasBasis (fun _n ↦ True) fun n ↦ (fun y ↦ 1 + y) '' ↑(I ^ n)
this :
  (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ True) fun i ↦
    ((fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.1)) ×ˢ (⇑MulOpposite.opHomeomorph.symm ⁻¹' (fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.2))
n₁ n₂ : ℕ
H : ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n₁ → -1 + ↑u⁻¹ ∈ I ^ n₂ → ↑u ∈ s
u : Rˣ
h₁ : -1 + ↑u ∈ I ^ max (max n₁ n₂) 1
h₂ : -1 + ↑u⁻¹ ∈ I ^ max (max n₁ n₂) 1
⊢ n₂ ≤ max (max n₁ n₂) 1

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.Module.IsWeak

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
E' : Type u_5
F' : Type u_6
inst✝⁷ : CommSemiring 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommMonoid F
inst✝² : Module 𝕜 F
inst : TopologicalSpace E
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
inst✝¹ : ContinuousAdd 𝕜
inst✝ : ContinuousConstSMul 𝕜 𝕜
x✝² x✝¹ : F
x✝ : E
⊢ { toLinearMap := B.flip (x✝² + x✝¹), cont := ⋯ } x✝ =
    ({ toLinearMap := B.flip x✝², cont := ⋯ } + { toLinearMap := B.flip x✝¹, cont := ⋯ }) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.Module.IsWeak

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
E' : Type u_5
F' : Type u_6
inst✝⁷ : CommSemiring 𝕜
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : AddCommMonoid E
inst✝⁴ : Module 𝕜 E
inst✝³ : AddCommMonoid F
inst✝² : Module 𝕜 F
inst : TopologicalSpace E
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
hB : B.IsWeak
inst✝¹ : ContinuousAdd 𝕜
inst✝ : ContinuousConstSMul 𝕜 𝕜
x✝² : 𝕜
x✝¹ : F
x✝ : E
⊢ { toLinearMap := B.flip (x✝² • x✝¹), cont := ⋯ } x✝ =
    ((RingHom.id 𝕜) x✝² • { toLinearMap := B.flip x✝¹, cont := ⋯ }) x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.IsOpenUnits

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
I : Ideal R
hR : IsAdic I
hI : I ≤ ⊥.jacobson
s : Set R
hs : s ∈ Filter.map (⇑(Units.coeHom R)) (Filter.comap (⇑(Units.embedProduct R)) (𝓝 1 ×ˢ 𝓝 1))
H : (𝓝 1).HasBasis (fun _n ↦ True) fun n ↦ (fun y ↦ 1 + y) '' ↑(I ^ n)
this✝¹ :
  (𝓝 1 ×ˢ 𝓝 1).HasBasis (fun i ↦ True) fun i ↦
    ((fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.1)) ×ˢ (⇑MulOpposite.opHomeomorph.symm ⁻¹' (fun x ↦ -1 + x) ⁻¹' ↑(I ^ i.2))
this✝ : ∃ n₁ n₂, ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n₁ → -1 + ↑u⁻¹ ∈ I ^ n₂ → ↑u ∈ s
n : ℕ
hn : n ≠ 0
hn' : ∀ (u : Rˣ), -1 + ↑u ∈ I ^ n → -1 + ↑u⁻¹ ∈ I ^ n → ↑u ∈ s
x : R
hx : x ∈ ↑(I ^ n)
this : IsUnit (1 + x)
⊢ ↑this.unit⁻¹ * (-(1 + x) + 1) = -↑this.unit⁻¹ * x

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected

Goal state before:
pp: G : Type u_1
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : NonarchimedeanGroup G
inst✝ : T2Space G
x : G
x✝¹ : x ∈ Set.univ
y : G
x✝ : y ∈ Set.univ
hxy : x ≠ y
V : OpenSubgroup G
dxy : Disjoint (x • ↑V) (y • ↑V)
⊢ Set.univ ⊆ x • ↑V ∪ (x • ↑V)ᶜ

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.ProperAction.Torsor

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : Group V
inst✝³ : Torsor V P
inst✝² : TopologicalSpace V
inst✝¹ : TopologicalSpace P
inst✝ : IsTopologicalTorsor P
x✝ : V × P
⊢ (fun pq ↦ (pq.1 /ₛ pq.2, pq.2)) ((fun vp ↦ (vp.1 • vp.2, vp.2)) x✝) = x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.ProperAction.Torsor

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : Group V
inst✝³ : Torsor V P
inst✝² : TopologicalSpace V
inst✝¹ : TopologicalSpace P
inst✝ : IsTopologicalTorsor P
x✝ : P × P
⊢ (fun vp ↦ (vp.1 • vp.2, vp.2)) ((fun pq ↦ (pq.1 /ₛ pq.2, pq.2)) x✝) = x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.Ring.Compact

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : IsTopologicalRing R
inst✝² : CompactSpace R
inst✝¹ : T2Space R
inst✝ : IsArtinianRing R
n : ℕ
hn : ⊥.jacobson ^ n = 0
I : Ideal R
hI : I ∈ {I | I.IsMaximal}
⊢ { asIdeal := I, isPrime := ⋯ } ∈ Finset.univ

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.Ring.Compact

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : IsTopologicalRing R
inst✝² : CompactSpace R
inst✝¹ : T2Space R
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
⊢ (Function.mulSupport fun v ↦ v.maxPowDividing I) ⊆ ↑(Set.Finite.toFinset ⋯)

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹³ : Semiring R
inst✝¹² : InvolutiveStar R
inst✝¹¹ : AddCommMonoid E
inst✝¹⁰ : Module R E
inst✝⁹ : StarAddMonoid E
inst✝⁸ : StarModule R E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : Module R F
inst✝⁵ : StarAddMonoid F
inst✝⁴ : StarModule R F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousStar E
inst✝ : ContinuousStar F
x : WithConv (E →L[R] F)
x✝ : E
⊢ (star (star x)).ofConv x✝ = x.ofConv x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁴ : Semiring R
inst✝¹³ : InvolutiveStar R
inst✝¹² : AddCommMonoid E
inst✝¹¹ : Module R E
inst✝¹⁰ : StarAddMonoid E
inst✝⁹ : StarModule R E
inst✝⁸ : AddCommMonoid F
inst✝⁷ : Module R F
inst✝⁶ : StarAddMonoid F
inst✝⁵ : StarModule R F
inst✝⁴ : TopologicalSpace E
inst✝³ : TopologicalSpace F
inst✝² : ContinuousStar E
inst✝¹ : ContinuousStar F
inst✝ : ContinuousAdd F
x y : WithConv (E →L[R] F)
x✝ : E
⊢ (star (x + y)).ofConv x✝ = (star x + star y).ofConv x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁹ : Semiring R
inst✝¹⁸ : InvolutiveStar R
inst✝¹⁷ : AddCommMonoid E
inst✝¹⁶ : Module R E
inst✝¹⁵ : StarAddMonoid E
inst✝¹⁴ : StarModule R E
inst✝¹³ : AddCommMonoid F
inst✝¹² : Module R F
inst✝¹¹ : StarAddMonoid F
inst✝¹⁰ : StarModule R F
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalSpace F
inst✝⁷ : ContinuousStar E
inst✝⁶ : ContinuousStar F
G : Type u_4
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : StarAddMonoid G
inst✝² : StarModule R G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousStar G
f : WithConv (E →L[R] F)
g : WithConv (G →L[R] E)
x✝ : G
⊢ (star (toConv (f.ofConv ∘SL g.ofConv))).ofConv x✝ = (toConv ((star f).ofConv ∘SL (star g).ofConv)).ofConv x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁹ : Semiring R
inst✝¹⁸ : InvolutiveStar R
inst✝¹⁷ : AddCommMonoid E
inst✝¹⁶ : Module R E
inst✝¹⁵ : StarAddMonoid E
inst✝¹⁴ : StarModule R E
inst✝¹³ : AddCommMonoid F
inst✝¹² : Module R F
inst✝¹¹ : StarAddMonoid F
inst✝¹⁰ : StarModule R F
inst✝⁹ : TopologicalSpace E
inst✝⁸ : TopologicalSpace F
inst✝⁷ : ContinuousStar E
inst✝⁶ : ContinuousStar F
G : Type u_4
inst✝⁵ : AddCommMonoid G
inst✝⁴ : Module R G
inst✝³ : StarAddMonoid G
inst✝² : StarModule R G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousStar G
f : E →L[R] F
g : G →L[R] E
x✝ : G
⊢ (star (toConv (f ∘SL g))).ofConv x✝ = (toConv ((star (toConv f)).ofConv ∘SL (star (toConv g)).ofConv)).ofConv x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : InvolutiveStar R
inst✝⁵ : AddCommMonoid E
inst✝⁴ : Module R E
inst✝³ : StarAddMonoid E
inst✝² : StarModule R E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousStar E
x✝ : E
⊢ (star (toConv (ContinuousLinearMap.id R E))).ofConv x✝ = (toConv (ContinuousLinearMap.id R E)).ofConv x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹³ : Semiring R
inst✝¹² : InvolutiveStar R
inst✝¹¹ : AddCommMonoid E
inst✝¹⁰ : Module R E
inst✝⁹ : StarAddMonoid E
inst✝⁸ : StarModule R E
inst✝⁷ : AddCommMonoid F
inst✝⁶ : Module R F
inst✝⁵ : StarAddMonoid F
inst✝⁴ : StarModule R F
inst✝³ : TopologicalSpace E
inst✝² : TopologicalSpace F
inst✝¹ : ContinuousStar E
inst✝ : ContinuousStar F
x✝ : E
⊢ (star (toConv 0)).ofConv x✝ = (toConv 0).ofConv x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.Star.LinearMap

Goal state before:
pp: E : Type u_2
inst✝¹¹ : AddCommMonoid E
inst✝¹⁰ : StarAddMonoid E
inst✝⁹ : TopologicalSpace E
inst✝⁸ : ContinuousStar E
S : Type u_4
inst✝⁷ : Semiring S
inst✝⁶ : StarAddMonoid S
inst✝⁵ : StarModule S S
inst✝⁴ : Module S E
inst✝³ : StarModule S E
inst✝² : TopologicalSpace S
inst✝¹ : ContinuousStar S
inst✝ : ContinuousSMul S E
a : E
⊢ (star (toConv (toSpanSingleton S a))).ofConv 1 = (toConv (toSpanSingleton S (star a))).ofConv 1

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.Star.LinearMap

Goal state before:
pp: E : Type u_2
F : Type u_3
inst✝¹⁷ : AddCommMonoid E
inst✝¹⁶ : StarAddMonoid E
inst✝¹⁵ : AddCommMonoid F
inst✝¹⁴ : StarAddMonoid F
inst✝¹³ : TopologicalSpace E
inst✝¹² : TopologicalSpace F
inst✝¹¹ : ContinuousStar E
inst✝¹⁰ : ContinuousStar F
S : Type u_4
inst✝⁹ : Semiring S
inst✝⁸ : StarAddMonoid S
inst✝⁷ : StarModule S S
inst✝⁶ : Module S E
inst✝⁵ : StarModule S E
inst✝⁴ : TopologicalSpace S
inst✝³ : ContinuousStar S
inst✝² : Module S F
inst✝¹ : StarModule S F
inst✝ : ContinuousSMul S F
f : WithConv (E →L[S] S)
x : F
x✝ : E
⊢ (star (toConv (f.ofConv.smulRight x))).ofConv x✝ = (toConv ((star f).ofConv.smulRight (star x))).ofConv x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.Star.LinearMap

Goal state before:
pp: R : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁵ : Semiring R
inst✝¹⁴ : InvolutiveStar R
inst✝¹³ : AddCommMonoid E
inst✝¹² : Module R E
inst✝¹¹ : StarAddMonoid E
inst✝¹⁰ : StarModule R E
inst✝⁹ : AddCommMonoid F
inst✝⁸ : Module R F
inst✝⁷ : StarAddMonoid F
inst✝⁶ : StarModule R F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : ContinuousStar E
inst✝² : ContinuousStar F
inst✝¹ : SMulCommClass R R F
inst✝ : ContinuousConstSMul R F
x✝² : R
x✝¹ : WithConv (E →L[R] F)
x✝ : E
⊢ (star (x✝² • x✝¹)).ofConv x✝ = (star x✝² • star x✝¹).ofConv x✝

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.WithZeroMulInt

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Valued R (WithZero (Multiplicative ℤ))
x : R
hx : v x ≤ exp (-1)
⊢ -1 < 0

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.WithZeroMulInt

Goal state before:
pp: R : Type u_1
inst✝¹ : Ring R
inst✝ : Valued R (WithZero (Multiplicative ℤ))
x : R
hx : v x ≤ exp (-1)
γ : (WithZero (Multiplicative ℤ))ˣ
⊢ -1 < 0

Tactic:
simp

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Finite

Goal state before:
pp: case h
X✝ : Type u_1
inst✝² : TopologicalSpace X✝
C✝ D✝ : Set X✝
inst✝¹ : RelCWComplex C✝ D✝
X : Type u
inst✝ : TopologicalSpace X
C D : Set X
cell : ℕ → Type u
map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X
finite_cell : ∀ (n : ℕ), _root_.Finite (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target
pairwiseDisjoint' : univ.PairwiseDisjoint fun ni ↦ ↑(map ni.fst ni.snd) '' ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint (↑(map n i) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n), MapsTo (↑(map n i)) (sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' closedBall 0 1)
closed' :
  ∀ A ⊆ C,
    (∀ (n : ℕ) (j : cell n), IsClosed[inst✝] (A ∩ ↑(map n j) '' closedBall 0 1)) ∧ IsClosed[inst✝] (A ∩ D) →
      IsClosed[inst✝] A
isClosedBase : IsClosed[inst✝] D
union' : D ∪ ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = C
n : ℕ
i : cell n
⊢ MapsTo (↑(map n i)) (sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j ∈ (fun m ↦ ⋯.toFinset) m, ↑(map m j) '' closedBall 0 1)

Tactic:
simp only [Finite.mem_toFinset, mem_univ, iUnion_true]

Goal state after:
case h
X✝ : Type u_1
inst✝² : TopologicalSpace X✝
C✝ D✝ : Set X✝
inst✝¹ : RelCWComplex C✝ D✝
X : Type u
inst✝ : TopologicalSpace X
C D : Set X
cell : ℕ → Type u
map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X
finite_cell : ∀ (n : ℕ), _root_.Finite (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target
pairwiseDisjoint' : univ.PairwiseDisjoint fun ni ↦ ↑(map ni.fst ni.snd) '' ball 0 1
disjointBase' : ∀ (n : ℕ) (i : cell n), Disjoint (↑(map n i) '' ball 0 1) D
mapsTo :
  ∀ (n : ℕ) (i : cell n), MapsTo (↑(map n i)) (sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' closedBall 0 1)
closed' :
  ∀ A ⊆ C,
    (∀ (n : ℕ) (j : cell n), IsClosed[inst✝] (A ∩ ↑(map n j) '' closedBall 0 1)) ∧ IsClosed[inst✝] (A ∩ D) →
      IsClosed[inst✝] A
isClosedBase : IsClosed[inst✝] D
union' : D ∪ ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = C
n : ℕ
i : cell n
⊢ MapsTo (↑(map n i)) (sphere 0 1) (D ∪ ⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' closedBall 0 1)
Module: Mathlib.Topology.CWComplex.Classical.Graph

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
e : cell C 1
x y : cell C 0
⊢ cellFrontier 1 e = closedCell 0 x ∪ closedCell 0 y ↔ cellFrontier 1 e = {↑(map 0 x) ![], ↑(map 0 y) ![]}

Tactic:
closedCell_zero_eq_singleton,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
e : cell C 1
x y : cell C 0
⊢ cellFrontier 1 e = {↑(map 0 x) ![]} ∪ closedCell 0 y ↔ cellFrontier 1 e = {↑(map 0 x) ![], ↑(map 0 y) ![]}
Module: Mathlib.Topology.CWComplex.Classical.Graph

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
e : cell C 1
x y : cell C 0
⊢ cellFrontier 1 e = {↑(map 0 x) ![]} ∪ closedCell 0 y ↔ cellFrontier 1 e = {↑(map 0 x) ![], ↑(map 0 y) ![]}

Tactic:
closedCell_zero_eq_singleton,

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
e : cell C 1
x y : cell C 0
⊢ cellFrontier 1 e = {↑(map 0 x) ![]} ∪ {↑(map 0 y) ![]} ↔ cellFrontier 1 e = {↑(map 0 x) ![], ↑(map 0 y) ![]}
Module: Mathlib.Topology.CWComplex.Classical.Graph

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
C : Set X
inst✝ : CWComplex C
e : cell C 1
x y : cell C 0
⊢ (OneSkeletonGraph C).IsLink e x y ↔ cellFrontier 1 e = {↑(map 0 x) ![], ↑(map 0 y) ![]}

Tactic:
by
  rw [OneSkeletonGraph_isLink, closedCell_zero_eq_singleton, closedCell_zero_eq_singleton,
    singleton_union]

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Finite

Goal state before:
pp: case h
X✝ : Type u_1
inst✝² : TopologicalSpace X✝
C✝ D : Set X✝
inst✝¹ : RelCWComplex C✝ D
X : Type u
inst✝ : TopologicalSpace X
C : Set X
cell : ℕ → Type u
map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X
finite_cell : ∀ (n : ℕ), _root_.Finite (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target
pairwiseDisjoint' : univ.PairwiseDisjoint fun ni ↦ ↑(map ni.fst ni.snd) '' ball 0 1
mapsTo :
  ∀ (n : ℕ) (i : cell n), MapsTo (↑(map n i)) (sphere 0 1) (⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' closedBall 0 1)
closed' : ∀ A ⊆ C, (∀ (n : ℕ) (j : cell n), IsClosed[inst✝] (A ∩ ↑(map n j) '' closedBall 0 1)) → IsClosed[inst✝] A
union' : ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = C
n : ℕ
i : cell n
⊢ MapsTo (↑(map n i)) (sphere 0 1) (⋃ m, ⋃ (_ : m < n), ⋃ j ∈ (fun m ↦ ⋯.toFinset) m, ↑(map m j) '' closedBall 0 1)

Tactic:
simp only [Finite.mem_toFinset, mem_univ, iUnion_true]

Goal state after:
case h
X✝ : Type u_1
inst✝² : TopologicalSpace X✝
C✝ D : Set X✝
inst✝¹ : RelCWComplex C✝ D
X : Type u
inst✝ : TopologicalSpace X
C : Set X
cell : ℕ → Type u
map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X
finite_cell : ∀ (n : ℕ), _root_.Finite (cell n)
source_eq : ∀ (n : ℕ) (i : cell n), (map n i).source = ball 0 1
continuousOn : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (closedBall 0 1)
continuousOn_symm : ∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target
pairwiseDisjoint' : univ.PairwiseDisjoint fun ni ↦ ↑(map ni.fst ni.snd) '' ball 0 1
mapsTo :
  ∀ (n : ℕ) (i : cell n), MapsTo (↑(map n i)) (sphere 0 1) (⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' closedBall 0 1)
closed' : ∀ A ⊆ C, (∀ (n : ℕ) (j : cell n), IsClosed[inst✝] (A ∩ ↑(map n j) '' closedBall 0 1)) → IsClosed[inst✝] A
union' : ⋃ n, ⋃ j, ↑(map n j) '' closedBall 0 1 = C
n : ℕ
i : cell n
⊢ MapsTo (↑(map n i)) (sphere 0 1) (⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' closedBall 0 1)