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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hs : IsGδ s
ht : IsGδ t
⊢ IsGδ (s ∪ t)

Tactic:
rcases hs with ⟨S, Sopen, Scount, rfl⟩

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
t : Set X
ht : IsGδ t
S : Set (Set X)
Sopen : ∀ t ∈ S, IsOpen[inst✝] t
Scount : S.Countable
⊢ IsGδ (⋂₀ S ∪ t)
Module: Mathlib.Topology.GDelta.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
⊢ IsMeagre ∅

Tactic:
rw [IsMeagre, compl_empty]
  exact Filter.univ_mem

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

Goal state before:
pp: case inl
α : Type u
inst✝¹ : TopologicalSpace α
β : Type u_3
inst✝ : TopologicalSpace β
T : Set β
hT : IsDiscrete T
f : α → β
hne : T.Nonempty
hS : IsPreconnected ∅
hc : ContinuousOn f ∅
hTm : MapsTo f ∅ T
⊢ ∃ y ∈ T, EqOn f (const α y) ∅

pp: case inr
α : Type u
inst✝¹ : TopologicalSpace α
S : Set α
hS : IsPreconnected S
β : Type u_3
inst✝ : TopologicalSpace β
T : Set β
hT : IsDiscrete T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
hne : T.Nonempty
x : α
hx : x ∈ S
⊢ ∃ y ∈ T, EqOn f (const α y) S

Tactic:
· exact hne.imp fun _ hy => ⟨hy, eqOn_empty _ _⟩

Goal state after:
case inr
α : Type u
inst✝¹ : TopologicalSpace α
S : Set α
hS : IsPreconnected S
β : Type u_3
inst✝ : TopologicalSpace β
T : Set β
hT : IsDiscrete T
f : α → β
hc : ContinuousOn f S
hTm : MapsTo f S T
hne : T.Nonempty
x : α
hx : x ∈ S
⊢ ∃ y ∈ T, EqOn f (const α y) S
Module: Mathlib.Topology.Baire.Lemmas

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : BaireSpace X
s : Set X
hs : IsOpen[inst✝¹] s
hne : s.Nonempty
h : IsMeagre s
x : X
hx : x ∈ s
hxc : x ∈ sᶜ
⊢ False

Tactic:
exact hxc hx

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
f : X → Y
hf : IsEmbedding f
x : X
⊢ hf.toHomeomorph (hf.toHomeomorph.symm ⟨f x, ⋯⟩) = hf.toHomeomorph x

Tactic:
ext; simp

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

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y
u v : Set α
u_op : IsOpen[inst✝] u
v_op : IsOpen[inst✝] v
hsuv : s ⊆ u ∪ v
x : α
x_in_s : x ∈ s
x_in_u : x ∈ u
H : s ∩ (u ∩ v) = ∅
y : α
y_in_s : y ∈ s
y_in_v : y ∈ v
hy : y ∉ u
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' u)

pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y
u v : Set α
u_op : IsOpen[inst✝] u
v_op : IsOpen[inst✝] v
hsuv : s ⊆ u ∪ v
x : α
x_in_s : x ∈ s
x_in_u : x ∈ u
H : s ∩ (u ∩ v) = ∅
y : α
y_in_s : y ∈ s
y_in_v : y ∈ v
hy : y ∉ u
⊢ IsOpen[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' u)

Tactic:
· rw [preimage_subtype_coe_eq_compl hsuv H]
      exact (v_op.preimage continuous_subtype_val).isClosed_compl

Goal state after:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y
u v : Set α
u_op : IsOpen[inst✝] u
v_op : IsOpen[inst✝] v
hsuv : s ⊆ u ∪ v
x : α
x_in_s : x ∈ s
x_in_u : x ∈ u
H : s ∩ (u ∩ v) = ∅
y : α
y_in_s : y ∈ s
y_in_v : y ∈ v
hy : y ∉ u
⊢ IsOpen[instTopologicalSpaceSubtype] (Subtype.val ⁻¹' u)
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : ∀ (f : α → Bool), ContinuousOn f s → ∀ x ∈ s, ∀ y ∈ s, f x = f y
⊢ IsPreconnected s

Tactic:
by
  unfold IsPreconnected
  by_contra! ⟨u, v, u_op, v_op, hsuv, ⟨x, x_in_s, x_in_u⟩, ⟨y, y_in_s, y_in_v⟩, H⟩
  have hy : y ∉ u := fun y_in_u => eq_empty_iff_forall_notMem.mp H y ⟨y_in_s, ⟨y_in_u, y_in_v⟩⟩
  have : ContinuousOn u.boolIndicator s := by
    apply (continuousOn_boolIndicator_iff_isClopen _ _).mpr ⟨_, _⟩
    · rw [preimage_subtype_coe_eq_compl hsuv H]
      exact (v_op.preimage continuous_subtype_val).isClosed_compl
    · exact u_op.preimage continuous_subtype_val
  simpa [(u.mem_iff_boolIndicator _).mp x_in_u, (u.notMem_iff_boolIndicator _).mp hy] using
    hs _ this x x_in_s y y_in_s

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
s : Set α
U : SetRel α α
hs : Dense s
hU : U ∈ 𝓤 α
y : α
⊢ ∃ i, ∃ (_ : i ∈ s), y ∈ ball i U

Tactic:
rcases hs.inter_nhds_nonempty (mem_nhds_right y hU) with ⟨x, hxs, hxy : (x, y) ∈ U⟩

Goal state after:
α : Type ua
inst✝ : UniformSpace α
s : Set α
U : SetRel α α
hs : Dense s
hU : U ∈ 𝓤 α
y x : α
hxs : x ∈ s
hxy : (x, y) ∈ U
⊢ ∃ i, ∃ (_ : i ∈ s), y ∈ ball i U
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u
inst✝¹ : UniformSpace α
inst✝ : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun x y ↦ (x, y) ∉ V₀
⊢ IsClosed[inst✝¹.toTopologicalSpace] s

Tactic:
rcases comp_symm_mem_uniformity_sets V₀_in with ⟨V₁, V₁_in, V₁_symm, h_comp⟩

Goal state after:
α : Type u
inst✝¹ : UniformSpace α
inst✝ : T0Space α
V₀ : Set (α × α)
V₀_in : V₀ ∈ 𝓤 α
s : Set α
hs : s.Pairwise fun x y ↦ (x, y) ∉ V₀
V₁ : Set (α × α)
V₁_in : V₁ ∈ 𝓤 α
V₁_symm : SetRel.IsSymm V₁
h_comp : SetRel.comp V₁ V₁ ⊆ V₀
⊢ IsClosed[inst✝¹.toTopologicalSpace] s
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
u : SetRel α α
v : SetRel β β
x : α × β
⊢ ball x (entourageProd u v) = ball x.1 u ×ˢ ball x.2 v

Tactic:
ext p; simp only [ball, entourageProd, Set.mem_ofPred_eq, Set.mem_prod, Set.mem_preimage]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
s s' : Set α
p : Filter ι
hf : UniformCauchySeqOnFilter F p (𝓟 s)
hss' : s' ⊆ s
⊢ UniformCauchySeqOnFilter F p (𝓟 s')

Tactic:
exact hf.mono_right (le_principal_iff.mpr <| mem_principal.mpr hss')

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
K : Set α
ι : Sort u_2
U : ι → Set α
hK : IsCompact K
hopen : ∀ (i : ι), IsOpen[inst✝.toTopologicalSpace] (U i)
hcover : K ⊆ ⋃ i, U i
x : α
hx : x ∈ K
i : ι
hi : x ∈ U i
⊢ ∃ i, ∃ V ∈ 𝓤 α, ball x (V ○ V) ⊆ U i

Tactic:
← (hopen i).mem_nhds_iff,

Goal state after:
α : Type ua
inst✝ : UniformSpace α
K : Set α
ι : Sort u_2
U : ι → Set α
hK : IsCompact K
hopen : ∀ (i : ι), IsOpen[inst✝.toTopologicalSpace] (U i)
hcover : K ⊆ ⋃ i, U i
x : α
hx : x ∈ K
i : ι
hi : U i ∈ 𝓝 x
⊢ ∃ i, ∃ V ∈ 𝓤 α, ball x (V ○ V) ⊆ U i
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : CompleteSpace γ
p : α → Prop
e : α → β
f : α → γ
b : β
s : Set α
hf : UniformContinuous fun x ↦ f ↑x
he : IsUniformEmbedding e
hd : ∀ (x : β), x ∈ closure[inst✝².toTopologicalSpace] (range e)
hb : closure[inst✝².toTopologicalSpace] (e '' s) ∈ 𝓝 b
hs : IsClosed[inst✝³.toTopologicalSpace] s
hp : ∀ x ∈ s, p x
de : IsDenseEmbedding e
de' : IsDenseEmbedding (IsDenseEmbedding.subtypeEmb p e)
ue' : IsUniformEmbedding (IsDenseEmbedding.subtypeEmb p e)
this : b ∈ closure[inst✝².toTopologicalSpace] (e '' {x | p x})
c : γ
hc : Tendsto (f ∘ Subtype.val) (comap Subtype.val (comap e (𝓝 b))) (𝓝 c)
⊢ {x | p x} ∈ comap e (𝓝 b)

Tactic:
exact ⟨_, hb, by rwa [← de.isInducing.closure_eq_preimage_closure_image, hs.closure_eq]⟩

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

Goal state before:
pp: X : Type u_1
α : Type u_2
inst✝¹ : One α
inst✝ : TopologicalSpace X
f : X → α
⊢ mulTSupport f = ∅ ↔ f = 1

Tactic:
rw [mulTSupport, closure_empty_iff, mulSupport_eq_empty_iff]

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

Goal state before:
pp: α : Type ua
inst✝¹ : UniformSpace α
inst✝ : CompactSpace α
this : (𝓤 (α × α)).HasBasis (fun U ↦ U ∈ 𝓤 α) fun U ↦ (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U
⊢ 𝓤 α ≤ 𝓝ˢ (diagonal α)

Tactic:
refine (isCompact_diagonal.nhdsSet_basis_uniformity this).ge_iff.2 fun U hU => ?_

Goal state after:
α : Type ua
inst✝¹ : UniformSpace α
inst✝ : CompactSpace α
this : (𝓤 (α × α)).HasBasis (fun U ↦ U ∈ 𝓤 α) fun U ↦ (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ⋃ x ∈ diagonal α, ball x ((fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U) ∈ 𝓤 α
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i ↦ mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := {i ∈ hnf.toFinset | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset | x ∉ U j}
⊢ ∃ is, ∃ n ∈ 𝓝 x, n ⊆ ⋂ i ∈ is, U i ∧ ∀ z ∈ n, (mulSupport fun i ↦ f i z) ⊆ ↑is

Tactic:
refine
      ⟨is, (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i, inter_mem (inter_mem hn ?_) ?_,
        inter_subset_right, fun z hz => ?_⟩

Goal state after:
case refine_1
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i ↦ mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := {i ∈ hnf.toFinset | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset | x ∉ U j}
⊢ ⋂ j ∈ js, (mulTSupport (f j))ᶜ ∈ 𝓝 x

case refine_2
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i ↦ mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := {i ∈ hnf.toFinset | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset | x ∉ U j}
⊢ ⋂ i ∈ is, U i ∈ 𝓝 x

case refine_3
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i ↦ mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := {i ∈ hnf.toFinset | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset | x ∉ U j}
z : X
hz : z ∈ (n ∩ ⋂ j ∈ js, (mulTSupport (f j))ᶜ) ∩ ⋂ i ∈ is, U i
⊢ (mulSupport fun i ↦ f i z) ⊆ ↑is
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
γ : Type u_3
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace β
inst✝ : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace ↑(closure (range sf))
ff : α → ↑(closure (range sf)) := inclusion ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : β → ↑(closure (range sf)) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
key : SeparationQuotient.mk ∘ hg.extend i ∘ fwd = SeparationQuotient.mk
hfu : IsUniformInducing fwd
hrr : range (SeparationQuotient.mk ∘ hid.extend f) ⊆ closure (range (SeparationQuotient.mk ∘ f))
⊢ fwd = inclusion hrr ∘ rangeFactorization (SeparationQuotient.mk ∘ hid.extend f)

Tactic:
refine hid.extend_unique ?_ ?_

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
γ : Type u_3
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace β
inst✝ : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace ↑(closure (range sf))
ff : α → ↑(closure (range sf)) := inclusion ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : β → ↑(closure (range sf)) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
key : SeparationQuotient.mk ∘ hg.extend i ∘ fwd = SeparationQuotient.mk
hfu : IsUniformInducing fwd
hrr : range (SeparationQuotient.mk ∘ hid.extend f) ⊆ closure (range (SeparationQuotient.mk ∘ f))
⊢ ∀ (x : α), (inclusion hrr ∘ rangeFactorization (SeparationQuotient.mk ∘ hid.extend f)) (i x) = ff x

case refine_2
α : Type u_1
β : Type u_2
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
γ : Type u_3
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace β
inst✝ : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
this : CompleteSpace ↑(closure (range sf))
ff : α → ↑(closure (range sf)) := inclusion ⋯ ∘ rangeFactorization sf
hgu : IsUniformInducing ff
hgd : DenseRange ff
hg : IsDenseInducing ff
fwd : β → ↑(closure (range sf)) := hid.extend ff
hfwd : UniformContinuous fwd
hg' : UniformContinuous (hg.extend i)
key : SeparationQuotient.mk ∘ hg.extend i ∘ fwd = SeparationQuotient.mk
hfu : IsUniformInducing fwd
hrr : range (SeparationQuotient.mk ∘ hid.extend f) ⊆ closure (range (SeparationQuotient.mk ∘ f))
⊢ Continuous[inst✝³.toTopologicalSpace, _] (inclusion hrr ∘ rangeFactorization (SeparationQuotient.mk ∘ hid.extend f))
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
⊢ TendstoLocallyUniformlyOn F f p s ↔ TendstoLocallyUniformly (fun i x ↦ F i ↑x) (f ∘ Subtype.val) p

Tactic:
simp only [tendstoLocallyUniformly_iff_forall_tendsto, Subtype.forall', tendsto_map'_iff,
    tendstoLocallyUniformlyOn_iff_forall_tendsto, ← map_nhds_subtype_val, prod_map_right]; rfl

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

Goal state before:
pp: α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
f : α → β
hf : IsUniformEmbedding f
⊢ UniformContinuous (f ∘ (Equiv.ofInjective f ⋯).invFun)

Tactic:
Equiv.invFun_as_coe,

Goal state after:
α : Type u
β : Type u_1
γ : Type u_2
δ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
inst✝ : UniformSpace δ
f : α → β
hf : IsUniformEmbedding f
⊢ UniformContinuous (f ∘ ⇑(Equiv.ofInjective f ⋯).symm)
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: case refine_2
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : δ → γ → ε
n : α → β → δ
m₁ : α → γ → α'
m₂ : β → γ → β'
n' : α' → β' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m₁ a c) (m₂ b c)
s : Set ε
t₁ : Set α'
u : Set α
hu : u ∈ f
w₁ : Set γ
hw₁ : w₁ ∈ h
ht₁ : image2 m₁ u w₁ ⊆ t₁
t₂ : Set β'
hs : image2 n' t₁ t₂ ⊆ s
v : Set β
hv : v ∈ g
w₂ : Set γ
hw₂ : w₂ ∈ h
ht₂ : image2 m₂ v w₂ ⊆ t₂
⊢ image2 m₂ v (w₁ ∩ w₂) ⊆ t₂

Tactic:
· exact (image2_subset_left inter_subset_right).trans ht₂

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

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
n : ℕ
x✝ : n + 2 ≠ 0
⊢ ⊤ ^ (n + 1) * ⊤ = ⊤

Tactic:
top_pow n.succ_ne_zero,

Goal state after:
α : Type u_2
inst✝ : Monoid α
n : ℕ
x✝ : n + 2 ≠ 0
⊢ ⊤ * ⊤ = ⊤
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: K : Type u_2
inst✝⁴ : DivisionSemiring K
inst✝³ : PartialOrder K
inst✝² : PosMulReflectLT K
inst✝¹ : IsOrderedCancelAddMonoid K
inst✝ : ExistsAddOfLE K
a : K
h : 0 < a
b c d : K
⊢ (fun x ↦ x + b) '' (fun x ↦ a * x) '' Ioc c d = Ioc (a * c + b) (a * d + b)

Tactic:
rw [image_mul_left_Ioc h, image_add_const_Ioc]

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

Goal state before:
pp: M : Type u_3
inst✝⁴ : GroupWithZero M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : CompactSpace M
inst✝ : T1Space M
⊢ IsOpen[inst✝³] {0}

Tactic:
obtain ⟨U, hU, h0U, h1U⟩ := t1Space_iff_exists_open.mp ‹_› zero_ne_one
  obtain ⟨W, hW, hW'⟩ := exists_mem_nhds_zero_mul_subset isCompact_univ (hU.mem_nhds h0U)
  by_cases H : ∃ x ≠ 0, x ∈ W
  · obtain ⟨x, hx, hxW⟩ := H
    cases h1U (hW' (by simpa [hx] using Set.mul_mem_mul (Set.mem_univ x⁻¹) hxW))
  · obtain rfl : W = {0} := subset_antisymm
      (by simpa [not_imp_not] using H) (by simpa using mem_of_mem_nhds hW)
    simpa [isOpen_iff_mem_nhds]

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
s : Set G
hs : IsOpen[inst✝²] s
t : Set G
⊢ s * closure[inst✝²] t = s * t

Tactic:
refine (mul_subset_iff.2 fun a ha b hb => ?_).antisymm (mul_subset_mul_left subset_closure)
  rw [mem_closure_iff] at hb
  have hbU : b ∈ s⁻¹ * {a * b} := ⟨a⁻¹, Set.inv_mem_inv.2 ha, a * b, rfl, inv_mul_cancel_left _ _⟩
  obtain ⟨_, ⟨c, hc, d, rfl : d = _, rfl⟩, hcs⟩ := hb _ hs.inv.mul_right hbU
  exact ⟨c⁻¹, hc, _, hcs, inv_mul_cancel_left _ _⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : UniformSpace α
inst✝⁶ : Group α
inst✝⁵ : IsUniformGroup α
hom : Type u_3
inst✝⁴ : UniformSpace β
inst✝³ : Group β
inst✝² : IsUniformGroup β
inst✝¹ : FunLike hom α β
inst✝ : MonoidHomClass hom α β
f : hom
h : Continuous[inst✝⁷.toTopologicalSpace, inst✝⁴.toTopologicalSpace] ⇑f
this : Tendsto (⇑f) (𝓝 1) (𝓝 (f 1))
⊢ Tendsto (⇑f) (𝓝 1) (𝓝 1)

Tactic:
map_one

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁷ : UniformSpace α
inst✝⁶ : Group α
inst✝⁵ : IsUniformGroup α
hom : Type u_3
inst✝⁴ : UniformSpace β
inst✝³ : Group β
inst✝² : IsUniformGroup β
inst✝¹ : FunLike hom α β
inst✝ : MonoidHomClass hom α β
f : hom
h : Continuous[inst✝⁷.toTopologicalSpace, inst✝⁴.toTopologicalSpace] ⇑f
this : Tendsto (⇑f) (𝓝 1) (𝓝 1)
⊢ Tendsto (⇑f) (𝓝 1) (𝓝 1)
Module: Mathlib.Order.Filter.AtTopBot.Field

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
l : Filter β
f : β → α
r : α
inst✝ : l.NeBot
h : Tendsto f l atTop
⊢ Tendsto (fun x ↦ f x / r) l atBot ↔ r < 0

Tactic:
by
  simp [div_eq_mul_inv, tendsto_mul_const_atBot_iff_neg h]

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

Goal state before:
pp: case inl
K✝ : Type u_1
inst✝⁴ : DivisionRing K✝
inst✝³ : TopologicalSpace K✝
α : Type u_2
inst✝² : Field α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalDivisionRing α
K : Subfield α
hx : 0 ∈ closure ↑K
⊢ 0⁻¹ ∈ closure ↑K

Tactic:
rwa [inv_zero]

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

Goal state before:
pp: case inr.inr.h
G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
h : Dense (range fun x ↦ a ^ x)
ha₀ : a ≤ 1
this : ∀ {a : G}, Dense (range fun x ↦ a ^ x) → 1 < a → (range fun x ↦ a ^ x) = univ
hlt : a < 1
H : (range fun x ↦ a⁻¹ ^ x) = range fun x ↦ a ^ x
⊢ Dense (range fun x ↦ a⁻¹ ^ x)

Tactic:
simpa only [H, one_lt_inv']

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

Goal state before:
pp: case inr.inr.ha₀
G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
h : Dense (range fun x ↦ a ^ x)
ha₀ : a ≤ 1
this : ∀ {a : G}, Dense (range fun x ↦ a ^ x) → 1 < a → (range fun x ↦ a ^ x) = univ
hlt : a < 1
H : (range fun x ↦ a⁻¹ ^ x) = range fun x ↦ a ^ x
⊢ 1 < a⁻¹

Tactic:
simpa only [H, one_lt_inv']

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

Goal state before:
pp: G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a : G
⊢ (DenseRange fun x ↦ a ^ x) ↔ Surjective fun x ↦ a ^ x

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ h.denseRange⟩
  wlog! ha₀ : 1 < a generalizing a
  · simp only [← range_eq_univ, DenseRange] at *
    rcases ha₀.eq_or_lt with rfl | hlt
    · simpa only [one_zpow, range_const, dense_iff_closure_eq, closure_singleton] using h
    · have H : range (a⁻¹ ^ · : ℤ → G) = range (a ^ · : ℤ → G) := by
        simpa only [← inv_zpow, zpow_neg, comp_def] using neg_surjective.range_comp (a ^ · : ℤ → G)
      rw [← H]
      apply this <;> simpa only [H, one_lt_inv']
  intro b
  obtain ⟨m, hm, hm'⟩ : ∃ m : ℤ, a ^ m ∈ Ioo b (b * a * a) := by
    have hne : (Ioo b (b * a * a)).Nonempty := ⟨b * a, by simpa⟩
    simpa using h.exists_mem_open isOpen_Ioo hne
  rcases eq_or_ne b (a ^ (m - 1)) with rfl | hne; · simp
  suffices (Ioo (a ^ m) (a ^ (m + 1))).Nonempty by
    rcases h.exists_mem_open isOpen_Ioo this with ⟨l, hl⟩
    have : m < l ∧ l < m + 1 := by simpa [zpow_lt_zpow_iff_right ha₀] using hl
    lia
  rcases hne.lt_or_gt with hlt | hlt
  · refine ⟨b * a * a, hm', ?_⟩
    simpa only [zpow_add, zpow_sub, zpow_one, ← div_eq_mul_inv, lt_div_iff_mul_lt,
      mul_lt_mul_iff_right] using hlt
  · use b * a
    simp only [mem_Ioo, zpow_add, zpow_sub, zpow_one, ← div_eq_mul_inv,
      mul_lt_mul_iff_right] at hlt ⊢
    exact ⟨div_lt_iff_lt_mul.1 hlt, hm⟩

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

Goal state before:
pp: α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
c : Set α
h : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
k : Set (Set α)
k_fin : k.Finite
hk : k ⊆ {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
kl : Set (Set α) := {s | s ∈ k ∧ ∃ a ∈ c, s = Ioi a}
kr : Set (Set α) := {s | s ∈ k ∧ ∃ a ∈ c, s = Iio a}
k_eq : k = kl ∪ kr
this✝ : Finite ↑kl
this : Finite ↑kr
al : ↑kl → α
alc : ∀ (s : ↑kl), al s ∈ c
hal : ∀ (s : ↑kl), ↑s = Ioi (al s)
ar : ↑kr → α
arc : ∀ (s : ↑kr), ar s ∈ c
har : ∀ (s : ↑kr), ↑s = Iio (ar s)
⊢ range al ⊆ c

Tactic:
by simp [range_subset_iff, alc]

Goal state after:
Module: Mathlib.Algebra.Category.Grp.IsFinite

Goal state before:
pp: S : ShortComplex AddCommGrpCat
hS : S.ShortExact
h₁ : Finite ↑S.X₁
h₃ : Finite ↑S.X₃
hg : Function.Surjective ⇑(ConcreteCategory.hom S.g)
s : ↑S.X₃ → ↑S.X₂
hs : Function.RightInverse s ⇑(ConcreteCategory.hom S.g)
x₂ : ↑S.X₂
⊢ (ConcreteCategory.hom S.g) (x₂ - s ((ConcreteCategory.hom S.g) x₂)) = 0

Tactic:
by simp [hs (S.g x₂)]

Goal state after:
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: R : Type uR
inst✝³ : CommRing R
A : Type uA
inst✝² : AddCommGroup A
A' : Type u_1
inst✝¹ : AddCommGroup A'
B : Type uB
inst✝ : AddCommGroup B
a : A
⊢ (LinearMap.toSpanSingleton ℤ A a).ker = Ideal.span {↑(addOrderOf a)}

Tactic:
ext1 x
    rw [Ideal.mem_span_singleton, addOrderOf_dvd_iff_zsmul_eq_zero, LinearMap.mem_ker,
      LinearMap.toSpanSingleton_apply]

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : Field 𝕜
p q r : 𝕜
m : ℕ
⊢ ↑(↑m / q * r) = m • ↑(r / q)

Tactic:
mul_comm_div,

Goal state after:
𝕜 : Type u_1
inst✝ : Field 𝕜
p q r : 𝕜
m : ℕ
⊢ ↑(↑m * (r / q)) = m • ↑(r / q)
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : Field 𝕜
p q r : 𝕜
m : ℤ
⊢ ↑(↑m / q * r) = m • ↑(r / q)

Tactic:
mul_comm_div,

Goal state after:
𝕜 : Type u_1
inst✝ : Field 𝕜
p q r : 𝕜
m : ℤ
⊢ ↑(↑m * (r / q)) = m • ↑(r / q)