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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ IsPreirreducible s ↔ ∀ (z₁ z₂ : Set X), IsClosed[inst✝] z₁ → IsClosed[inst✝] z₂ → s ⊆ z₁ ∪ z₂ → s ⊆ z₁ ∨ s ⊆ z₂

Tactic:
by
  refine compl_surjective.forall.trans <| forall_congr' fun z₁ => compl_surjective.forall.trans <|
    forall_congr' fun z₂ => ?_
  simp only [isOpen_compl_iff, ← compl_union, inter_compl_nonempty_iff]
  refine forall₂_congr fun _ _ => ?_
  rw [← and_imp, ← not_or, not_imp_not]

Goal state after:
Module: Mathlib.Topology.Irreducible

Goal state before:
pp: case h
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
h : ∀ (U : Set X), IsOpen[inst✝] U → (S ∩ U).Nonempty → S ⊆ closure[inst✝] (S ∩ U)
a b : Set X
ha : IsOpen[inst✝] a
hb : IsOpen[inst✝] b
p : X
pS : p ∈ S
pa : p ∈ a
bS : (S ∩ b).Nonempty
h0 : S ∩ (a ∩ b) = ∅
⊢ IsClosed[inst✝] aᶜ ∧ S ∩ b ⊆ aᶜ ∧ p ∉ aᶜ

Tactic:
grind [isClosed_compl_iff, subset_compl_iff_disjoint_left, disjoint_iff_inter_eq_empty]

Goal state after:
Module: Mathlib.Topology.Order.LeftRight

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
a : α
⊢ 𝓝[Iic a ∪ Ioi a] a = 𝓝 a

Tactic:
Iic_union_Ioi,

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
a : α
⊢ 𝓝[univ] a = 𝓝 a
Module: Mathlib.Topology.Order.LeftRight

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
s : Set α
a : α
⊢ 𝓝[s ∩ (Iic a ∪ Ioi a)] a = 𝓝[s] a

Tactic:
Iic_union_Ioi,

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrder α
s : Set α
a : α
⊢ 𝓝[s ∩ univ] a = 𝓝[s] a
Module: Mathlib.Topology.Separation.Basic

Goal state before:
pp: case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
h : ∀ ⦃x y : SeparationQuotient X⦄, x ⤳ y → x = y
x y : X
xspecy : x ⤳ y
⊢ y ⤳ x

Tactic:
rw [← IsInducing.specializes_iff isInducing_mk, h xspecy] at *

Goal state after:
Module: Mathlib.Topology.Order.OrderClosed

Goal state before:
pp: α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderClosedTopology α
f g : β → α
inst✝ : TopologicalSpace β
hf : Continuous[inst✝, inst✝³] f
hg : Continuous[inst✝, inst✝³] g
⊢ frontier {b | f b < g b} ⊆ {b | f b = g b}

Tactic:
simpa only [← not_lt, ← compl_ofPred, frontier_compl, eq_comm] using frontier_le_subset_eq hg hf

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

Goal state before:
pp: case mp
α : Type u
inst✝ : TopologicalSpace α
h : ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen[inst✝] V ∧ x ∈ V ∧ IsConnected V
x : α
U : Set α
hxU : U ∈ 𝓝 x
V : Set α
hVU : V ⊆ U
hV₁ : IsOpen[inst✝] V
hxV : x ∈ V
hV₂ : IsConnected V
⊢ ∃ V ∈ 𝓝 x, IsPreconnected V ∧ V ⊆ U

Tactic:
exact ⟨V, hV₁.mem_nhds hxV, hV₂.isPreconnected, hVU⟩

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

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝¹ : CountableInterFilter l✝
l : Filter β
inst✝ : CountableInterFilter l
f : α → β
S : Set (Set α)
hSc : S.Countable
t : Set α → Set β
htl : ∀ s ∈ S, t s ∈ l
ht : ∀ s ∈ S, f ⁻¹' t s ⊆ s
⊢ ⋂₀ S ∈ comap f l

Tactic:
have : (⋂ s ∈ S, t s) ∈ l := (countable_bInter_mem hSc).2 htl

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
l✝ : Filter α
inst✝¹ : CountableInterFilter l✝
l : Filter β
inst✝ : CountableInterFilter l
f : α → β
S : Set (Set α)
hSc : S.Countable
t : Set α → Set β
htl : ∀ s ∈ S, t s ∈ l
ht : ∀ s ∈ S, f ⁻¹' t s ⊆ s
this : ⋂ s ∈ S, t s ∈ l
⊢ ⋂₀ S ∈ comap f l
Module: Mathlib.Topology.Connected.Basic

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s u : Set α
hs : IsPreconnected s
hu : IsOpen[inst✝] u
h'u : (s ∩ u).Nonempty
h : closure[inst✝] u ∩ s ⊆ u
A : s ⊆ u ∪ (closure[inst✝] u)ᶜ
⊢ s ⊆ u

Tactic:
apply hs.subset_left_of_subset_union hu isClosed_closure.isOpen_compl _ A h'u

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s u : Set α
hs : IsPreconnected s
hu : IsOpen[inst✝] u
h'u : (s ∩ u).Nonempty
h : closure[inst✝] u ∩ s ⊆ u
A : s ⊆ u ∪ (closure[inst✝] u)ᶜ
⊢ Disjoint u (closure[inst✝] u)ᶜ
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: case insert
X : Type u_1
inst✝ : TopologicalSpace X
S : Set (Set X)
a✝¹ : Set X
s✝ : Set (Set X)
a✝ : a✝¹ ∉ s✝
hs✝ : s✝.Finite
ih : (∀ s ∈ s✝, IsGδ s) → IsGδ (⋃₀ s✝)
h : IsGδ a✝¹ ∧ ∀ x ∈ s✝, IsGδ x
⊢ IsGδ (a✝¹ ∪ ⋃₀ s✝)

Tactic:
exact h.1.union (ih h.2)

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

Goal state before:
pp: α : Type u
β : Type v
ι : Type u_1
X : ι → Type u_2
inst✝¹ : TopologicalSpace α
s t u v : Set α
inst✝ : PreconnectedSpace α
⊢ Subsingleton (ConnectedComponents α)

Tactic:
refine ⟨fun x y ↦ ?_⟩
  obtain ⟨x, rfl⟩ := surjective_coe x
  obtain ⟨y, rfl⟩ := surjective_coe y
  simp_rw [coe_eq_coe, PreconnectedSpace.connectedComponent_eq_univ, ]

Goal state after:
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
ι : Sort u_3
inst✝³ : TopologicalSpace X
inst✝² : BaireSpace X
inst✝¹ : Nonempty X
inst✝ : Countable ι
f : ι → Set X
hc : ∀ (i : ι), IsClosed[inst✝³] (f i)
hU : ⋃ i, f i = univ
⊢ ∃ i, (interior (f i)).Nonempty

Tactic:
by
  simpa using (dense_iUnion_interior_of_closed hc hU).nonempty

Goal state after:
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
h : X ≃ₜ Y
⊢ IsConnected (⇑h ⁻¹' s) ↔ IsConnected s

Tactic:
by
  rw [← image_symm, isConnected_image]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : Monoid M
inst✝¹ : TopologicalSpace N
inst✝ : Monoid N
f : M →* N
hf_inj : Function.Injective ⇑f
hf : IsOpenMap ⇑f
U : Set (M × Mᵐᵒᵖ)
hU : IsOpen[inferInstance] U
hg_openMap : IsOpenMap (Prod.map (⇑f) (⇑opHomeomorph ∘ ⇑f ∘ ⇑opHomeomorph.symm))
y : Nˣ
⊢ (∃ a a_1, (a, op a_1) ∈ U ∧ f a = ↑y ∧ (⇑opHomeomorph ∘ ⇑f ∘ ⇑opHomeomorph.symm) (op a_1) = op ↑y⁻¹) ↔
    ∃ x, (↑x, op ↑x⁻¹) ∈ U ∧ (map f) x = y

Tactic:
refine ⟨fun ⟨a, b, h, ha, hb⟩ ↦ ⟨⟨a, b, hf_inj ?_, hf_inj ?_⟩, ?_⟩,
    fun ⟨x, hxV, hx⟩ ↦ ⟨x, x.inv, by simp [hxV, ← hx]⟩⟩

Goal state after:
case refine_1
M : Type u_1
N : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : Monoid M
inst✝¹ : TopologicalSpace N
inst✝ : Monoid N
f : M →* N
hf_inj : Function.Injective ⇑f
hf : IsOpenMap ⇑f
U : Set (M × Mᵐᵒᵖ)
hU : IsOpen[inferInstance] U
hg_openMap : IsOpenMap (Prod.map (⇑f) (⇑opHomeomorph ∘ ⇑f ∘ ⇑opHomeomorph.symm))
y : Nˣ
x✝ : ∃ a a_1, (a, op a_1) ∈ U ∧ f a = ↑y ∧ (⇑opHomeomorph ∘ ⇑f ∘ ⇑opHomeomorph.symm) (op a_1) = op ↑y⁻¹
a b : M
h : (a, op b) ∈ U
ha : f a = ↑y
hb : (⇑opHomeomorph ∘ ⇑f ∘ ⇑opHomeomorph.symm) (op b) = op ↑y⁻¹
⊢ f (a * b) = f 1

case refine_2
M : Type u_1
N : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : Monoid M
inst✝¹ : TopologicalSpace N
inst✝ : Monoid N
f : M →* N
hf_inj : Function.Injective ⇑f
hf : IsOpenMap ⇑f
U : Set (M × Mᵐᵒᵖ)
hU : IsOpen[inferInstance] U
hg_openMap : IsOpenMap (Prod.map (⇑f) (⇑opHomeomorph ∘ ⇑f ∘ ⇑opHomeomorph.symm))
y : Nˣ
x✝ : ∃ a a_1, (a, op a_1) ∈ U ∧ f a = ↑y ∧ (⇑opHomeomorph ∘ ⇑f ∘ ⇑opHomeomorph.symm) (op a_1) = op ↑y⁻¹
a b : M
h : (a, op b) ∈ U
ha : f a = ↑y
hb : (⇑opHomeomorph ∘ ⇑f ∘ ⇑opHomeomorph.symm) (op b) = op ↑y⁻¹
⊢ f (b * a) = f 1

case refine_3
M : Type u_1
N : Type u_2
inst✝³ : TopologicalSpace M
inst✝² : Monoid M
inst✝¹ : TopologicalSpace N
inst✝ : Monoid N
f : M →* N
hf_inj : Function.Injective ⇑f
hf : IsOpenMap ⇑f
U : Set (M × Mᵐᵒᵖ)
hU : IsOpen[inferInstance] U
hg_openMap : IsOpenMap (Prod.map (⇑f) (⇑opHomeomorph ∘ ⇑f ∘ ⇑opHomeomorph.symm))
y : Nˣ
x✝ : ∃ a a_1, (a, op a_1) ∈ U ∧ f a = ↑y ∧ (⇑opHomeomorph ∘ ⇑f ∘ ⇑opHomeomorph.symm) (op a_1) = op ↑y⁻¹
a b : M
h : (a, op b) ∈ U
ha : f a = ↑y
hb : (⇑opHomeomorph ∘ ⇑f ∘ ⇑opHomeomorph.symm) (op b) = op ↑y⁻¹
⊢ (↑{ val := a, inv := b, val_inv := ⋯, inv_val := ⋯ }, op ↑{ val := a, inv := b, val_inv := ⋯, inv_val := ⋯ }⁻¹) ∈ U ∧
    (map f) { val := a, inv := b, val_inv := ⋯, inv_val := ⋯ } = y
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: β : Type ub
V : SetRel β β
inst✝ : V.IsSymm
x : β
⊢ ball x V = {y | (y, x) ∈ V}

Tactic:
by
  ext y
  rw [mem_ball_symmetry]
  exact Iff.rfl

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
inst✝ : DiscreteUniformity α
f : Filter α
f_ne_bot : f.NeBot
x : α
hS hT : {x} ∈ f
H : {x} ×ˢ {x} ⊆ SetRel.id
⊢ ∃ x, f = pure x

Tactic:
exact ⟨x, f_ne_bot.le_pure_iff.mp <| le_pure_iff.mpr hS⟩

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
f : Filter α
h : f.TotallyBounded
⊢ TotallyBounded {x | ClusterPt x f}

Tactic:
refine uniformity_hasBasis_closed.totallyBounded_iff.2 fun V hV => ?_
  obtain ⟨t, htf, hst⟩ := h V hV.1
  refine ⟨t, htf, fun x hx => ?_⟩
  rw [← SetRel.preimage_eq_biUnion, id, ← (hV.2.relPreimage_of_finite htf).closure_eq]
  exact hx.mem_closure_of_mem _ hst

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

Goal state before:
pp: α : Type u
inst✝¹ : UniformSpace α
ι : Type u_1
inst✝ : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
f : ι → α
hf : Pairwise fun x y ↦ (f x, f y) ∉ V₀
x y : ι
h : f x ≠ f y
⊢ (f x, f y) ∉ V₀

Tactic:
exact hf (ne_of_apply_ne f h)

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

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
f g : Filter α
⊢ (f ⊔ g).TotallyBounded ↔ f.TotallyBounded ∧ g.TotallyBounded

Tactic:
sup_eq_iSup,

Goal state after:
α : Type u
uniformSpace : UniformSpace α
f g : Filter α
⊢ (⨆ b, bif b then f else g).TotallyBounded ↔ f.TotallyBounded ∧ g.TotallyBounded
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
m : α → β
s : Set α
hm : IsUniformInducing m
fact1 : SurjOn (map m) (Iic (𝓟 s)) (Iic (𝓟 (m '' s)))
fact2 : MapsTo (map m) (Iic (𝓟 s)) (Iic (𝓟 (m '' s)))
⊢ (∀ f ∈ Iic (𝓟 (m '' s)), Cauchy f → ∃ x ∈ m '' s, f ≤ 𝓝 x) ↔ ∀ f ∈ Iic (𝓟 s), Cauchy f → ∃ x ∈ s, f ≤ 𝓝 x

Tactic:
fact1.forall fact2,

Goal state after:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
m : α → β
s : Set α
hm : IsUniformInducing m
fact1 : SurjOn (map m) (Iic (𝓟 s)) (Iic (𝓟 (m '' s)))
fact2 : MapsTo (map m) (Iic (𝓟 s)) (Iic (𝓟 (m '' s)))
⊢ (∀ x ∈ Iic (𝓟 s), Cauchy (map m x) → ∃ x_1 ∈ m '' s, map m x ≤ 𝓝 x_1) ↔ ∀ f ∈ Iic (𝓟 s), Cauchy f → ∃ x ∈ s, f ≤ 𝓝 x
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: 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

Tactic:
exact inter_subset_left (seq_pair_mem hf Hmem hm hn)

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

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h✝ :
  ∀ x ∈ s,
    ∀ u ∈ 𝓤 β,
      ∃ pa,
        (∀ᶠ (x : ι) in p, pa x) ∧
          ∃ pb, (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
pa : ι → Prop
hpa : ∀ᶠ (x : ι) in p, pa x
pb : α → Prop
hpb : ∀ᶠ (y : α) in 𝓝[s] x, pb y
h : ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

Tactic:
exact ⟨{a | pb a}, hpb, eventually_of_mem hpa fun i hi y hy => h hi hy⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s✝ : Set α
p : Filter ι
inst✝ : UniformSpace β
𝔖 : Set (Set α)
𝔗 : Set (Set γ)
e : γ ≃ α
he : 𝔗 ⊆ image ⇑e ⁻¹' 𝔖
he' : 𝔖 ⊆ preimage ⇑e ⁻¹' 𝔗
s : Set α
hs : s ∈ 𝔖
⊢ (fun x ↦ ⇑e.symm '' x) s ∈ 𝔗

Tactic:
change e.symm '' s ∈ 𝔗
      rw [Equiv.image_symm_eq_preimage]
      exact he' hs

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : TopologicalSpace α
f : α →ᵤ[𝔖] β
x : α
h𝔖 : ∃ V ∈ 𝔖, V ∈ 𝓝 x
hc : ContinuousAt ((toFun 𝔖) f) x
U : Set (β × β)
hU : U ∈ 𝓤 β
⊢ ∀ᶠ (a : (α →ᵤ[𝔖] β) × α) in 𝓝 (f, x),
    (Prod.mk ((toFun 𝔖) (f, x).1 (f, x).2) ∘ fun fx ↦ (toFun 𝔖) fx.1 fx.2) a ∈ SetRel.comp U U

Tactic:
rcases h𝔖 with ⟨V, hV, hVx⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : TopologicalSpace α
f : α →ᵤ[𝔖] β
x : α
hc : ContinuousAt ((toFun 𝔖) f) x
U : Set (β × β)
hU : U ∈ 𝓤 β
V : Set α
hV : V ∈ 𝔖
hVx : V ∈ 𝓝 x
⊢ ∀ᶠ (a : (α →ᵤ[𝔖] β) × α) in 𝓝 (f, x),
    (Prod.mk ((toFun 𝔖) (f, x).1 (f, x).2) ∘ fun fx ↦ (toFun 𝔖) fx.1 fx.2) a ∈ SetRel.comp U U
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: case refine_2
α : Type u_2
inst✝ : DivisionMonoid α
a b : α
h : a * b = 1
⊢ pure a * pure b = 1

Tactic:
rw [pure_mul_pure, h, pure_one]

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

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : Group α
f g : Filter α
h : 1 ≤ f / g
hfg : Disjoint f g
s : Set α
hs : s ∈ f
t : Set α
ht : t ∈ g
hst : ∅ = s ∩ t
⊢ False

Tactic:
exact Set.one_mem_div_iff.1 (h <| div_mem_div hs ht) (disjoint_iff.2 hst.symm)

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

Goal state before:
pp: R : Type u_5
α : Type u_6
β : Type u_7
F : Type u_8
inst✝⁸ : FunLike F α β
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid α
inst✝⁵ : AddCommMonoid β
inst✝⁴ : Module R α
inst✝³ : Module R β
inst✝² : TopologicalSpace R
inst✝¹ : LinearMapClass F R α β
tβ : TopologicalSpace β
inst✝ : ContinuousSMul R β
f : F
⊢ ContinuousSMul R α

Tactic:
let tα := tβ.induced f

Goal state after:
R : Type u_5
α : Type u_6
β : Type u_7
F : Type u_8
inst✝⁸ : FunLike F α β
inst✝⁷ : Semiring R
inst✝⁶ : AddCommMonoid α
inst✝⁵ : AddCommMonoid β
inst✝⁴ : Module R α
inst✝³ : Module R β
inst✝² : TopologicalSpace R
inst✝¹ : LinearMapClass F R α β
tβ : TopologicalSpace β
inst✝ : ContinuousSMul R β
f : F
tα : TopologicalSpace α := TopologicalSpace.induced (⇑f) tβ
⊢ ContinuousSMul R α
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: α : Type u_6
β : Type u_7
F : Type u_8
inst✝⁴ : FunLike F α β
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : MulHomClass F α β
tβ : TopologicalSpace β
inst✝ : ContinuousMul β
f : F
⊢ ContinuousMul α

Tactic:
let tα := tβ.induced f

Goal state after:
α : Type u_6
β : Type u_7
F : Type u_8
inst✝⁴ : FunLike F α β
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : MulHomClass F α β
tβ : TopologicalSpace β
inst✝ : ContinuousMul β
f : F
tα : TopologicalSpace α := TopologicalSpace.induced (⇑f) tβ
⊢ ContinuousMul α
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u
inst✝¹ : CommMonoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
⊢ ContinuousMul M

Tactic:
apply ContinuousMul.of_nhds_one hmul hleft
  intro x₀
  simp_rw [mul_comm, hleft x₀]

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

Goal state before:
pp: M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
l : Filter (M × M)
hl : Disjoint l (cocompact (M × M))
this : (𝓝 0).coprod (𝓝 0) ⊓ l ≤ 𝓝 0 ×ˢ map Prod.snd l ⊔ map Prod.fst l ×ˢ 𝓝 0
⊢ Tendsto (fun x ↦ x.1 * x.2) ((𝓝 0).coprod (𝓝 0) ⊓ l) (𝓝 0)

Tactic:
apply (Tendsto.sup _ _).mono_left this

Goal state after:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
l : Filter (M × M)
hl : Disjoint l (cocompact (M × M))
this : (𝓝 0).coprod (𝓝 0) ⊓ l ≤ 𝓝 0 ×ˢ map Prod.snd l ⊔ map Prod.fst l ×ˢ 𝓝 0
⊢ Tendsto (fun x ↦ x.1 * x.2) (𝓝 0 ×ˢ map Prod.snd l) (𝓝 0)

M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
l : Filter (M × M)
hl : Disjoint l (cocompact (M × M))
this : (𝓝 0).coprod (𝓝 0) ⊓ l ≤ 𝓝 0 ×ˢ map Prod.snd l ⊔ map Prod.fst l ×ˢ 𝓝 0
⊢ Tendsto (fun x ↦ x.1 * x.2) (map Prod.fst l ×ˢ 𝓝 0) (𝓝 0)
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space Y
y : Y
h : ∀ (y_1 : Y), IsCompact ((fun x ↦ y) ⁻¹' {y_1})
⊢ IsCompact univ

Tactic:
by simpa using h y

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
t : Set G
ht : IsOpen[inst✝²] t
s : Set G
⊢ closure[inst✝²] s * t = s * t

Tactic:
by
  rw [← inv_inv (closure s * t), mul_inv_rev, inv_closure, ht.inv.mul_closure, mul_inv_rev, inv_inv,
    inv_inv]

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

Goal state before:
pp: A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : ContinuousMul A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen[inst✝⁵] U
⊢ IsOpen[inst✝²] (⇑φ '' U)

Tactic:
← hφ.isOpen_preimage

Goal state after:
A : Type u_1
inst✝⁶ : Group A
inst✝⁵ : TopologicalSpace A
inst✝⁴ : ContinuousMul A
B : Type u_2
inst✝³ : Group B
inst✝² : TopologicalSpace B
F : Type u_3
inst✝¹ : FunLike F A B
inst✝ : MonoidHomClass F A B
φ : F
hφ : IsQuotientMap ⇑φ
U : Set A
hU : IsOpen[inst✝⁵] U
⊢ IsOpen[inst✝⁵] (⇑φ ⁻¹' ⇑φ '' U)
Module: Mathlib.Order.Filter.AtTopBot.Group

Goal state before:
pp: G : Type u_2
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
⊢ ∀ (i' : G × G), True ∧ True → ∃ i, True ∧ mabs ⁻¹' Ici i ⊆ Iic i'.1 ∪ Ici i'.2

Tactic:
rintro ⟨a, b⟩ -

Goal state after:
G : Type u_2
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
⊢ ∃ i, True ∧ mabs ⁻¹' Ici i ⊆ Iic (a, b).1 ∪ Ici (a, b).2
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: α : Type u
G : Type u_1
inst✝² : GroupWithZero G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousDiv G
b : G
hb : b ≠ 0
c : G
f : α → G
l : Filter α
⊢ Tendsto (fun x ↦ f x / b) l (𝓝 (c / b)) ↔ Tendsto f l (𝓝 c)

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ Filter.Tendsto.div_const' h b⟩

Goal state after:
α : Type u
G : Type u_1
inst✝² : GroupWithZero G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousDiv G
b : G
hb : b ≠ 0
c : G
f : α → G
l : Filter α
h : Tendsto (fun x ↦ f x / b) l (𝓝 (c / b))
⊢ Tendsto f l (𝓝 c)
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: α : Type u
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousDiv G
b c : G
f : α → G
l : Filter α
⊢ Tendsto (fun x ↦ f x / b) l (𝓝 (c / b)) ↔ Tendsto f l (𝓝 c)

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ Filter.Tendsto.div_const' h b⟩

Goal state after:
α : Type u
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : ContinuousDiv G
b c : G
f : α → G
l : Filter α
h : Tendsto (fun x ↦ f x / b) l (𝓝 (c / b))
⊢ Tendsto f l (𝓝 c)
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
α : Type u_1
l : Filter α
x : G
u : α → G
A : Tendsto (fun x_1 ↦ x) l (𝓝 x)
h : Tendsto u l (𝓝 x)
⊢ Tendsto (fun x_1 ↦ u x_1 / x) l (𝓝 1)

Tactic:
simpa using h.div' A

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
S : Subgroup G
hS : Tendsto (⇑S.subtype) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
this : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun p ↦ (p.1⁻¹, p.2)
H : (Subtype.val ⁻¹' (fun a ↦ a.1⁻¹ * a.2) '' K ×ˢ L).Finite
⊢ (⇑S.equivOp ⁻¹' {γ | ((fun x ↦ γ • x) '' K ∩ L).Nonempty}).Finite

Tactic:
convert! H using 1

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
S : Subgroup G
hS : Tendsto (⇑S.subtype) cofinite (cocompact G)
K L : Set G
hK : IsCompact K
hL : IsCompact L
this : Continuous[instTopologicalSpaceProd, instTopologicalSpaceProd] fun p ↦ (p.1⁻¹, p.2)
H : (Subtype.val ⁻¹' (fun a ↦ a.1⁻¹ * a.2) '' K ×ˢ L).Finite
⊢ ⇑S.equivOp ⁻¹' {γ | ((fun x ↦ γ • x) '' K ∩ L).Nonempty} = Subtype.val ⁻¹' (fun a ↦ a.1⁻¹ * a.2) '' K ×ˢ L
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
s : Set α
hs : TotallyBounded s
⊢ TotallyBounded s⁻¹

Tactic:
by
  simpa using hs.image uniformContinuous_inv

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

Goal state before:
pp: case refine_2
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
h : x ∈ univ.pi fun i_1 ↦ Icc (update f i a i_1) (update f i b i_1)
⊢ x i ∈ Icc a b

pp: case refine_3
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
h : x ∈ univ.pi fun i_1 ↦ Icc (update f i a i_1) (update f i b i_1)
⊢ update f i (x i) = x

Tactic:
· simpa only [Function.update_self] using! h i (mem_univ i)

Goal state after:
case refine_3
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
x : (a : ι) → α a
h : x ∈ univ.pi fun i_1 ↦ Icc (update f i a i_1) (update f i b i_1)
⊢ update f i (x i) = x
Module: Mathlib.Order.Interval.Set.Pi

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

Tactic:
simpa using image_update_uIcc f i a (f i)

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

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝¹⁴ : TopologicalSpace α
inst✝¹³ : AddCommGroup α
inst✝¹² : IsTopologicalAddGroup α
inst✝¹¹ : TopologicalSpace β
inst✝¹⁰ : AddCommGroup β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : AddCommGroup γ
inst✝⁷ : IsTopologicalAddGroup γ
inst✝⁶ : TopologicalSpace δ
inst✝⁵ : AddCommGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
f : δ →+ γ
df : IsDenseInducing ⇑f
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝⁴.toTopologicalSpace] fun p ↦ (φ p.1) p.2
inst✝² : IsUniformAddGroup G
inst✝¹ : T0Space G
inst✝ : CompleteSpace G
x₀ : α
y₀ : γ
W' : Set G
W'_nhds : W' ∈ 𝓝 0
U : Set β
V : Set δ
V_nhds : V ∈ comap (⇑f) (𝓝 y₀)
h : ∀ x ∈ U, ∀ x' ∈ U, ∀ y ∈ V, ∀ y' ∈ V, (fun p ↦ (φ p.1) p.2) (x', y') - (fun p ↦ (φ p.1) p.2) (x, y) ∈ W'
U' : Set α
U'_nhds : U' ∈ 𝓝 x₀
U'_sub : ⇑e ⁻¹' U' ⊆ U
⊢ W' ∈
    map (fun p ↦ (fun p ↦ (φ p.1) p.2) p.2 - (fun p ↦ (φ p.1) p.2) p.1)
      (comap (fun p ↦ ((e p.1.1, f p.1.2), e p.2.1, f p.2.2)) (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀)))

Tactic:
rw [mem_comap] at V_nhds

Goal state after:
case right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝¹⁴ : TopologicalSpace α
inst✝¹³ : AddCommGroup α
inst✝¹² : IsTopologicalAddGroup α
inst✝¹¹ : TopologicalSpace β
inst✝¹⁰ : AddCommGroup β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : AddCommGroup γ
inst✝⁷ : IsTopologicalAddGroup γ
inst✝⁶ : TopologicalSpace δ
inst✝⁵ : AddCommGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
f : δ →+ γ
df : IsDenseInducing ⇑f
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝⁴.toTopologicalSpace] fun p ↦ (φ p.1) p.2
inst✝² : IsUniformAddGroup G
inst✝¹ : T0Space G
inst✝ : CompleteSpace G
x₀ : α
y₀ : γ
W' : Set G
W'_nhds : W' ∈ 𝓝 0
U : Set β
V : Set δ
V_nhds : ∃ t ∈ 𝓝 y₀, ⇑f ⁻¹' t ⊆ V
h : ∀ x ∈ U, ∀ x' ∈ U, ∀ y ∈ V, ∀ y' ∈ V, (fun p ↦ (φ p.1) p.2) (x', y') - (fun p ↦ (φ p.1) p.2) (x, y) ∈ W'
U' : Set α
U'_nhds : U' ∈ 𝓝 x₀
U'_sub : ⇑e ⁻¹' U' ⊆ U
⊢ W' ∈
    map (fun p ↦ (fun p ↦ (φ p.1) p.2) p.2 - (fun p ↦ (φ p.1) p.2) p.1)
      (comap (fun p ↦ ((e p.1.1, f p.1.2), e p.2.1, f p.2.2)) (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀)))