mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case inl
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht'✝ : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
T₂_v : f ⁻¹' T₂ = f ⁻¹' t ∩ v
hT₁ : IsClosed[inst✝] T₁
hT₂ : IsClosed[inst✝] T₂
t' : β
ht' : t' ∈ t
htu : f ⁻¹' {t'} ⊆ u
⊢ t' ∈ T₁ ∨ t' ∈ T₂

pp: case inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht'✝ : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
T₂_v : f ⁻¹' T₂ = f ⁻¹' t ∩ v
hT₁ : IsClosed[inst✝] T₁
hT₂ : IsClosed[inst✝] T₂
t' : β
ht' : t' ∈ t
htv : f ⁻¹' {t'} ⊆ v
⊢ t' ∈ T₁ ∨ t' ∈ T₂

Tactic:
· left; exact ⟨ht', htu⟩

Goal state after:
case inr
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
connected_fibers : ∀ (t : β), IsConnected (f ⁻¹' {t})
hcl : IsCoinducing f
t : Set β
ht : IsClosed[inst✝] t
ht'✝ : IsConnected t
hf : Surjective f
hT : IsClosed[inst✝¹] (f ⁻¹' t)
u v : Set α
hu : IsClosed[inst✝¹] u
hv : IsClosed[inst✝¹] v
huv : f ⁻¹' t ⊆ u ∪ v
uv_disj : Disjoint u v
T₁ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ u}
T₂ : Set β := {t' | t' ∈ t ∧ f ⁻¹' {t'} ⊆ v}
fiber_decomp : ∀ t' ∈ t, f ⁻¹' {t'} ⊆ u ∨ f ⁻¹' {t'} ⊆ v
T₁_u : f ⁻¹' T₁ = f ⁻¹' t ∩ u
T₂_v : f ⁻¹' T₂ = f ⁻¹' t ∩ v
hT₁ : IsClosed[inst✝] T₁
hT₂ : IsClosed[inst✝] T₂
t' : β
ht' : t' ∈ t
htv : f ⁻¹' {t'} ⊆ v
⊢ t' ∈ T₁ ∨ t' ∈ T₂
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: case h₁
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
Y : Type u_4
inst✝ : TopologicalSpace Y
p : Y → X
hp : IsOpenEmbedding p
f : ℕ → Set Y
hof : ∀ (n : ℕ), IsOpen[inst✝] (f n)
hdf : ∀ (n : ℕ), Dense (f n)
s : Set X := ⋯
c : ℕ → Set X := ⋯
c_open : ∀ (n : ℕ), IsOpen[inst✝²] (c n)
n : ℕ
⊢ interior (closure[inst✝²] s) ⊆ closure[inst✝²] s

Tactic:
exact interior_subset

Goal state after:
Module: Mathlib.Topology.Separation.Regular

Goal state before:
pp: case neg
X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
x : X
hs : IsClosed[inst✝²] (⋂ s, ↑s)
a b : Set X
ha : IsClosed[inst✝²] a
hb : IsClosed[inst✝²] b
hab : ⋂ s, ↑s ⊆ a ∪ b
ab_disj : Disjoint a b
u v : Set X
hu : IsOpen[inst✝²] u
hv : IsOpen[inst✝²] v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
s : Set X
H : IsClopen s ∧ x ∈ s ∧ s ⊆ v ∪ u
H1 : IsClopen (s ∩ u)
H2 : IsClopen (s ∩ v)
hxu : x ∉ u
h1 : x ∈ v
⊢ ⋂ s, ↑s ⊆ s ∩ v

Tactic:
exact iInter_subset (fun s : { s : Set X // IsClopen s ∧ x ∈ s } => s.1)
          ⟨s ∩ v, H2, mem_inter H.2.1 h1⟩

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

Goal state before:
pp: M : Type u_4
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x | IsUnit x}
hf : ∀ (u : Mˣ), f ↑u = ↑u⁻¹
⊢ IsEmbedding val

Tactic:
by
  refine ⟨⟨?_⟩, val_injective⟩
  rw [topology_eq_inf, inf_eq_left, ← continuous_iff_le_induced,
    @continuous_iff_continuousAt _ _ (.induced _ _)]
  intro u s hs
  simp only [← hf, nhds_induced, Filter.mem_map] at hs ⊢
  exact ⟨_, mem_inf_principal.1 (hc u u.isUnit hs), fun u' hu' ↦ hu' u'.isUnit⟩

Goal state after:
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: case inr.succ.succ.cons
α : Type u
inst✝¹ : TopologicalSpace α
inst✝ : Infinite (ConnectedComponents α)
h✝ : Nonempty α
n : ℕ
i : Fin (n + 1)
s : Set α
U : Fin n → Set α
h₁ : ∀ (i_1 : Fin (n + 1)), IsClopen ((Equiv.piCongrLeft (fun x ↦ Set α) (Equiv.swap 0 i)).symm (Fin.cons s U) i_1)
h₂ : ∀ (i_1 : Fin (n + 1)), ((Equiv.piCongrLeft (fun x ↦ Set α) (Equiv.swap 0 i)).symm (Fin.cons s U) i_1).Nonempty
h₃ : Pairwise (Disjoint on (Equiv.piCongrLeft (fun x ↦ Set α) (Equiv.swap 0 i)).symm (Fin.cons s U))
h₄ : ⋃ i_1, (Equiv.piCongrLeft (fun x ↦ Set α) (Equiv.swap 0 i)).symm (Fin.cons s U) i_1 = univ
hi : ¬IsConnected ((Equiv.piCongrLeft (fun x ↦ Set α) (Equiv.swap 0 i)).symm (Fin.cons s U) i)
⊢ ∃ U,
    (∀ (i : Fin (n + 1 + 1)), IsClopen (U i)) ∧
      (∀ (i : Fin (n + 1 + 1)), (U i).Nonempty) ∧ Pairwise (Disjoint on U) ∧ ⋃ i, U i = univ

Tactic:
simp only [Equiv.piCongrLeft_symm_apply, Equiv.swap_apply_right, Fin.cons_zero] at *
    obtain ⟨a, b, ha, hb, ha', hb', hab, rfl⟩ := (show IsClopen s by simpa using h₁ i)
      |>.not_isPreconnected_iff.mp (mt (⟨by simpa using h₂ i, ·⟩) hi)
    refine ⟨Fin.cons a (Fin.cons b U), ?_, ?_, ?_, ?_⟩
    · simpa [Fin.forall_iff_succ, *] using fun x ↦ h₁ (Equiv.swap 0 i (.succ x))
    · simpa [Fin.forall_iff_succ, *] using fun x ↦ h₂ (Equiv.swap 0 i (.succ x))
    · have h₃' (j : _) : Disjoint (U j) a ∧ Disjoint (U j) b := by
        simpa [onFun] using h₃ ((Equiv.swap 0 i).injective.ne (Fin.succ_ne_zero j))
      simpa [Pairwise, Fin.forall_iff_succ, onFun, hab, disjoint_comm (a := a),
        disjoint_comm (a := b), h₃'] using
        h₃.comp_of_injective ((Equiv.swap 0 i).injective.comp (Fin.succ_injective _))
    · simpa [← union_assoc, (Equiv.surjective _).iUnion_comp] using h₄

Goal state after:
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
x y : α
⊢ y ∈ ConnectedComponents.mk ⁻¹' {ConnectedComponents.mk x} ↔ y ∈ connectedComponent x

Tactic:
mem_preimage,

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
x y : α
⊢ ConnectedComponents.mk y ∈ {ConnectedComponents.mk x} ↔ y ∈ connectedComponent x
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
h : TendstoUniformly F f p
⊢ TendstoUniformlyOnFilter F f p ⊤

Tactic:
by rwa [← tendstoUniformly_iff_tendstoUniformlyOnFilter]

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ {p | p.2 = x → p.1 ∈ s} ∈ 𝓤 α

Tactic:
uniformity_eq_symm,

Goal state after:
α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ {p | p.2 = x → p.1 ∈ s} ∈ map Prod.swap (𝓤 α)
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
ι' : Type u_5
α' : Type u_6
β' : Type u_7
inst✝ : UniformSpace β'
F' : ι' → α' → β'
f' : α' → β'
p' : Filter ι'
h : TendstoUniformly F f p
h' : TendstoUniformly F' f' p'
⊢ TendstoUniformly (fun i ↦ Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p')

Tactic:
by
  rw [← tendstoUniformlyOn_univ, ← univ_prod_univ] at *
  exact h.prodMap h'

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

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
x : α
⊢ 𝓝 x = comap (Prod.mk x) ⊤

Tactic:
by simp only [nhds_top, comap_top]

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

Goal state before:
pp: α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : Subsingleton α
u : UniformSpace α
⊢ SetRel.id ∈ (fun u ↦ 𝓤 α) u

Tactic:
rw [SetRel.id, ← diagonal, diagonal_eq_univ]

Goal state after:
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort u_1
inst✝ : Subsingleton α
u : UniformSpace α
⊢ univ ∈ (fun u ↦ 𝓤 α) u
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u
inst✝ : UniformSpace α
⊢ T0Space α ↔ (𝓤 α).ker = diagonal α

Tactic:
by
  simp_rw [t0Space_iff_uniformity, subset_antisymm_iff, diagonal_subset_iff, subset_def,
    Prod.forall, Filter.mem_ker, mem_diagonal_iff, iff_self_and]
  exact fun _ x s hs ↦ refl_mem_uniformity hs

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
f : Filter α
h : f.TotallyBounded
V : SetRel α α
hV : V ∈ 𝓤 α ∧ IsClosed[instTopologicalSpaceProd] V
t : Set α
htf : t.Finite
hst : V.preimage t ∈ f
x : α
hx : x ∈ {x | ClusterPt x f}
⊢ x ∈ ⋃ y ∈ t, {x | (x, y) ∈ id V}

Tactic:
← SetRel.preimage_eq_biUnion,

Goal state after:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
h : f.TotallyBounded
V : SetRel α α
hV : V ∈ 𝓤 α ∧ IsClosed[instTopologicalSpaceProd] V
t : Set α
htf : t.Finite
hst : V.preimage t ∈ f
x : α
hx : x ∈ {x | ClusterPt x f}
⊢ x ∈ (id V).preimage t
Module: Mathlib.Topology.UniformSpace.Compact

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
K : Set α
ι' : Sort u_2
p : ι' → Prop
V : ι' → Set (α × α)
U : α → Set α
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
hU : ∀ x ∈ K, U x ∈ 𝓝[K] x
⊢ ∃ i, p i ∧ ∀ x ∈ K, ∃ y, ball x (V i) ∩ K ⊆ U y

Tactic:
refine (hbasis.exists_iff ?_).1 (lebesgue_number_lemma_nhdsWithin hK hU)
  exact fun s t hst ht x hx ↦ (ht x hx).imp
    fun y hy ↦ Subset.trans (Set.inter_subset_inter_left K (ball_mono hst _)) hy

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, Tendsto u atTop (𝓝 a)
U' : ℕ → Set (α × α)
hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ i, U' i ⊆ s
Hmem : ∀ (n : ℕ), U n ∩ U' n ∈ 𝓤 α
⊢ CompleteSpace α

Tactic:
refine ⟨fun hf => (HU (seq hf Hmem) fun N m n hm hn => ?_).imp <|
    le_nhds_of_seq_tendsto_nhds _ _ fun s hs => ?_⟩

Goal state after:
case refine_1
α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, Tendsto u atTop (𝓝 a)
U' : ℕ → Set (α × α)
hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ i, U' i ⊆ s
Hmem : ∀ (n : ℕ), U n ∩ U' n ∈ 𝓤 α
f✝ : Filter α
hf : Cauchy f✝
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
⊢ (SequentiallyComplete.seq hf Hmem m, SequentiallyComplete.seq hf Hmem n) ∈ U N

case refine_2
α : Type u
uniformSpace : UniformSpace α
inst✝ : (𝓤 α).IsCountablyGenerated
U : ℕ → SetRel α α
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
HU : ∀ (u : ℕ → α), (∀ (N m n : ℕ), N ≤ m → N ≤ n → (u m, u n) ∈ U N) → ∃ a, Tendsto u atTop (𝓝 a)
U' : ℕ → Set (α × α)
hU' : ∀ {s : Set (α × α)}, s ∈ 𝓤 α ↔ ∃ i, U' i ⊆ s
Hmem : ∀ (n : ℕ), U n ∩ U' n ∈ 𝓤 α
f✝ : Filter α
hf : Cauchy f✝
s : Set (α × α)
hs : s ∈ 𝓤 α
⊢ ∃ n, U n ∩ U' n ⊆ s
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: α : Type u_2
γ : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : One γ
f : α → γ
inst✝ : TopologicalSpace γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
v : α
hv : v ∈ (mulTSupport f)ᶜ
⊢ v ∈ f ⁻¹' N

Tactic:
mem_preimage,

Goal state after:
α : Type u_2
γ : Type u_5
inst✝² : TopologicalSpace α
inst✝¹ : One γ
f : α → γ
inst✝ : TopologicalSpace γ
h : HasCompactMulSupport f
N : Set γ
hN : N ∈ 𝓝 1
v : α
hv : v ∈ (mulTSupport f)ᶜ
⊢ f v ∈ N
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
κ : Type u_2
X : Type u_3
α' : Type u_7
tX : TopologicalSpace X
u : κ → UniformSpace α'
F : ι → X → α'
S : Set X
x₀ : X
⊢ Tendsto (⇑ofFun ∘ swap F) (𝓝[S] x₀) (𝓝 ((⇑ofFun ∘ swap F) x₀)) ↔
    ∀ (k : κ), Tendsto (⇑ofFun ∘ swap F) (𝓝[S] x₀) (𝓝 ((⇑ofFun ∘ swap F) x₀))

Tactic:
toTopologicalSpace_iInf,

Goal state after:
ι : Type u_1
κ : Type u_2
X : Type u_3
α' : Type u_7
tX : TopologicalSpace X
u : κ → UniformSpace α'
F : ι → X → α'
S : Set X
x₀ : X
⊢ Tendsto (⇑ofFun ∘ swap F) (𝓝[S] x₀) (𝓝 ((⇑ofFun ∘ swap F) x₀)) ↔
    ∀ (k : κ), Tendsto (⇑ofFun ∘ swap F) (𝓝[S] x₀) (𝓝 ((⇑ofFun ∘ swap F) x₀))
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
κ : Type u_2
X : Type u_3
α' : Type u_7
tX : TopologicalSpace X
u : κ → UniformSpace α'
F : ι → X → α'
⊢ Continuous[tX, inferInstance] (⇑ofFun ∘ swap F) ↔ ∀ (k : κ), Continuous[tX, inferInstance] (⇑ofFun ∘ swap F)

Tactic:
toTopologicalSpace_iInf,

Goal state after:
ι : Type u_1
κ : Type u_2
X : Type u_3
α' : Type u_7
tX : TopologicalSpace X
u : κ → UniformSpace α'
F : ι → X → α'
⊢ Continuous[tX, inferInstance] (⇑ofFun ∘ swap F) ↔ ∀ (k : κ), Continuous[tX, inferInstance] (⇑ofFun ∘ swap F)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
𝔖 : Set (Set α)
h : 𝔖.Nonempty
h' : DirectedOn (fun x1 x2 ↦ x1 ⊆ x2) 𝔖
p : ι → Prop
s : ι → Set (β × β)
hb : (𝓤 β).HasBasis p s
⊢ (𝓤 (α →ᵤ[𝔖] β)).HasBasis (fun Si ↦ Si.1 ∈ 𝔖 ∧ p Si.2) fun Si ↦ UniformOnFun.gen 𝔖 Si.1 (s Si.2)

Tactic:
simp only [iInf_uniformity]
  exact
    hasBasis_biInf_of_directed h (fun S => UniformOnFun.gen 𝔖 S ∘ s) _
      (fun S _hS => UniformOnFun.hasBasis_uniformity_of_basis_aux₁ α β 𝔖 hb S)
      (UniformOnFun.hasBasis_uniformity_of_basis_aux₂ α β 𝔖 h' hb)

Goal state after:
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
g : Filter β
s : Set β
hs : s ∈ 0
a : β
⊢ a ∈ (fun x ↦ 0 • x) ⁻¹' s

Tactic:
mem_preimage,

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
g : Filter β
s : Set β
hs : s ∈ 0
a : β
⊢ 0 • a ∈ s
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: case right
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
u : Set M
hu : u ∈ 𝓝 1
W : Set M
W1 : W ∈ 𝓝 1
h : ∀ v ∈ W, ∀ w ∈ W, v * w ∈ u
V : Set M
V1 : V ∈ 𝓝 1
h' : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ W
⊢ ∀ {v w s t : M}, v ∈ V → w ∈ V → s ∈ V → t ∈ V → v * w * s * t ∈ u

Tactic:
intro v w s t v_in w_in s_in t_in

Goal state after:
case right
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
u : Set M
hu : u ∈ 𝓝 1
W : Set M
W1 : W ∈ 𝓝 1
h : ∀ v ∈ W, ∀ w ∈ W, v * w ∈ u
V : Set M
V1 : V ∈ 𝓝 1
h' : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ W
v w s t : M
v_in : v ∈ V
w_in : w ∈ V
s_in : s ∈ V
t_in : t ∈ V
⊢ v * w * s * t ∈ u
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u_3
ι' : Sort u_6
inst✝ : Mul M
ts : ι' → TopologicalSpace M
h' : ∀ (i : ι'), ContinuousMul M
⊢ ContinuousMul M

Tactic:
by
  rw [← sInf_range]
  exact continuousMul_sInf (Set.forall_mem_range.mpr h')

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
g h : G
hg : g ∈ connectedComponent 1
hh : h ∈ connectedComponent 1
⊢ g ∈ connectedComponent (g * h)

Tactic:
apply Continuous.image_connectedComponent_subset (continuous_const_mul g)

Goal state after:
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
g h : G
hg : g ∈ connectedComponent 1
hh : h ∈ connectedComponent 1
⊢ g ∈ (fun x ↦ g * x) '' connectedComponent h
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : IsDiscrete ↑S
V : Set G
hV : V ∈ 𝓝 1 ∧ V ∩ ↑S = {1}
U : Set G
hU : U ∈ 𝓝 1
hUinv : U⁻¹ = U
hUV : U * U ⊆ V
g : G
hgS : g ∈ S
⊢ ((fun x ↦ g * x) '' U ∩ U).Nonempty → g = 1

Tactic:
rintro ⟨_, ⟨x, hx, rfl⟩, hgx⟩

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : IsDiscrete ↑S
V : Set G
hV : V ∈ 𝓝 1 ∧ V ∩ ↑S = {1}
U : Set G
hU : U ∈ 𝓝 1
hUinv : U⁻¹ = U
hUV : U * U ⊆ V
g : G
hgS : g ∈ S
x : G
hx : x ∈ U
hgx : (fun x ↦ g * x) x ∈ U
⊢ g = 1
Module: Mathlib.Order.Filter.AtTopBot.Group

Goal state before:
pp: G : Type u_2
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b x : G
hx : x ∈ mabs ⁻¹' Ici (max a⁻¹ b)
⊢ x ∈ Iic (a, b).1 ∪ Ici (a, b).2

Tactic:
mem_preimage,

Goal state after:
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b x : G
hx : |x|ₘ ∈ Ici (max a⁻¹ b)
⊢ x ∈ Iic (a, b).1 ∪ Ici (a, b).2
Module: Mathlib.Order.Filter.AtTopBot.Field

Goal state before:
pp: α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k : α
hk : 0 < k
a b : α
x✝ : 1 ≤ b
⊢ a / k ≤ b ↔ a ≤ k * b

Tactic:
by rw [div_le_iff₀' hk]

Goal state after:
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
U : Set G
H : U ∈ 𝓝 1
V : Set G
V_nhds : V ∈ 𝓝 1
V_mul : ∀ v ∈ V, ∀ w ∈ V, v * w ∈ U
x y z : G
hz₁ : (x, z) ∈ (fun p ↦ p.2 * p.1⁻¹) ⁻¹' V
hz₂ : (z, y) ∈ (fun p ↦ p.2 * p.1⁻¹) ⁻¹' V
⊢ (x, y) ∈ (fun p ↦ p.2 * p.1⁻¹) ⁻¹' U

Tactic:
simpa using V_mul _ hz₂ _ hz₁

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
g₀ : G
hg₀ : g₀ ∈ interior V
g : G
x✝ : g ∈ K
⊢ g ∈ (fun x ↦ g₀ * g⁻¹ * x) ⁻¹' interior V

Tactic:
mem_preimage,

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
g₀ : G
hg₀ : g₀ ∈ interior V
g : G
x✝ : g ∈ K
⊢ g₀ * g⁻¹ * g ∈ interior V
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
G : Type u_3
inst✝¹ : Group G
u : UniformSpace G
inst✝ : IsTopologicalGroup G
F : ι → α → G
p : Filter ι
s : Set α
hu : rightUniformSpace G = u
⊢ UniformCauchySeqOn F p s ↔ ∀ u_1 ∈ 𝓝 1, ∀ᶠ (m : ι × ι) in p ×ˢ p, ∀ a ∈ s, F m.2 a / F m.1 a ∈ u_1

Tactic:
by
  simp only [div_eq_mul_inv]
  exact hu ▸ ⟨fun h u hu ↦ h _ ⟨u, hu, fun _ ↦ id⟩,
    fun h _ ⟨u, hu, hv⟩ => mem_of_superset (h u hu) fun _ hi a ha => hv (hi a ha)⟩

Goal state after:
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a : α i
⊢ update f i '' Ioc a (f i) = Ioc (update f i a) f

Tactic:
by simpa using image_update_Ioc f i a (f i)

Goal state after:
Module: Mathlib.Order.Filter.Interval

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
l : Filter α
inst✝ : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ l.smallSets
t : Set α
htl : t ∈ l
hts : ∀ p ∈ t ×ˢ t, Icc p.1 p.2 ∈ s
p : α × α
hp : p ∈ t ×ˢ t
h : p.1 ≤ p.2
⊢ p ∈ (fun p ↦ [[p.1, p.2]]) ⁻¹' s

Tactic:
mem_preimage,

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
l : Filter α
inst✝ : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ l.smallSets
t : Set α
htl : t ∈ l
hts : ∀ p ∈ t ×ˢ t, Icc p.1 p.2 ∈ s
p : α × α
hp : p ∈ t ×ˢ t
h : p.1 ≤ p.2
⊢ [[p.1, p.2]] ∈ s
Module: Mathlib.Order.Filter.Interval

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
l : Filter α
inst✝ : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ l.smallSets
t : Set α
htl : t ∈ l
hts : ∀ p ∈ t ×ˢ t, Icc p.1 p.2 ∈ s
p : α × α
hp : p ∈ t ×ˢ t
h : p.2 ≤ p.1
⊢ p ∈ (fun p ↦ [[p.1, p.2]]) ⁻¹' s

Tactic:
mem_preimage,

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
l : Filter α
inst✝ : TendstoIxxClass Icc l l
s : Set (Set α)
hs : s ∈ l.smallSets
t : Set α
htl : t ∈ l
hts : ∀ p ∈ t ×ˢ t, Icc p.1 p.2 ∈ s
p : α × α
hp : p ∈ t ×ˢ t
h : p.2 ≤ p.1
⊢ [[p.1, p.2]] ∈ s
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
t : Set α := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
y : α → α
hy : ∀ x ∈ t, y x > x
h'y : ∀ x ∈ t, s ∩ Ioo x (y x) = ∅
a : α
ha : a ∈ t
b : α
hb : b ∈ t
⊢ a ≠ b → Disjoint (Ioo a (y a)) (Ioo b (y b))

Tactic:
hab

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
t : Set α := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
y : α → α
hy : ∀ x ∈ t, y x > x
h'y : ∀ x ∈ t, s ∩ Ioo x (y x) = ∅
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : a ≠ b
⊢ Disjoint (Ioo a (y a)) (Ioo b (y b))
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: case hfh
𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hf : ∀ᶠ (x : α) in l, |f x| ≤ C
hg : Tendsto g l (𝓝 0)
hC : Tendsto (fun x ↦ |C * g x|) l (𝓝 0)
⊢ ∀ᶠ (b : α) in l, (abs ∘ fun x ↦ f x * g x) b ≤ |C * g b|

Tactic:
· filter_upwards [hf] with x hx
    simp only [comp_apply, abs_mul]
    exact mul_le_mul_of_nonneg_right (hx.trans (le_abs_self C)) (abs_nonneg _)

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
e : PartialEquiv α β
e' : PartialEquiv α γ
x : α
he : x ∈ e.source
he' : x ∈ e'.source
⊢ ↑e x ∈ ↑e.symm.symm.symm ⁻¹' e'.source

Tactic:
mem_preimage,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
e : PartialEquiv α β
e' : PartialEquiv α γ
x : α
he : x ∈ e.source
he' : x ∈ e'.source
⊢ ↑e.symm.symm.symm (↑e x) ∈ e'.source
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case inl
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst✝³] a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
z : α → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
x : α
xt : x ∈ t
x' : α
x't : x' ∈ t
hxx' : x ≠ x'
h' : x < x'
⊢ (Disjoint on fun x ↦ Ioc (z x) x) x x'

Tactic:
refine disjoint_left.2 fun u ux ux' => xt.2.2.1 ?_

Goal state after:
case inl
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst✝³] a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
z : α → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
x : α
xt : x ∈ t
x' : α
x't : x' ∈ t
hxx' : x ≠ x'
h' : x < x'
u : α
ux : u ∈ (fun x ↦ Ioc (z x) x) x
ux' : u ∈ (fun x ↦ Ioc (z x) x) x'
⊢ y x ∈ a
Module: Mathlib.Algebra.Category.Grp.LargeColimits

Goal state before:
pp: case h
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
χ : CharacterModule (Colimits.Quot F)
c' : Cocone F :=
  { pt := of (ULift.{w, 0} (AddCircle 1)),
    ι := { app := fun j ↦ ofHom ((AddEquiv.ulift.symm.toAddMonoidHom.comp χ).comp (Quot.ι F j)), naturality := ⋯ } }
j : J
x : ↑(F.obj j)
⊢ AddEquiv.ulift ((Hom.hom (hc.desc c')) ((Quot.desc F c) ((Quot.ι F j) x))) = χ ((Quot.ι F j) x)

Tactic:
rw [Quot.ι_desc]

Goal state after:
case h
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrpCat
c : Cocone F
inst✝ : DecidableEq J
x✝ : Nonempty (IsColimit c)
hc : IsColimit c
χ : CharacterModule (Colimits.Quot F)
c' : Cocone F :=
  { pt := of (ULift.{w, 0} (AddCircle 1)),
    ι := { app := fun j ↦ ofHom ((AddEquiv.ulift.symm.toAddMonoidHom.comp χ).comp (Quot.ι F j)), naturality := ⋯ } }
j : J
x : ↑(F.obj j)
⊢ AddEquiv.ulift ((Hom.hom (hc.desc c')) ((ConcreteCategory.hom (c.ι.app j)) x)) = χ ((Quot.ι F j) x)
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < ↑n
m : ℕ
hn : m < n
h0 : 0 < m
⊢ ¬↑(↑m * (p / ↑n)) = 0

Tactic:
rw [coe_eq_zero_of_pos_iff p hp.out (mul_pos (Nat.cast_pos.2 h0) <| div_pos hp.out h)]

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
h : 0 < ↑n
m : ℕ
hn : m < n
h0 : 0 < m
⊢ ¬∃ n_1, n_1 • p = ↑m * (p / ↑n)