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

Goal state before:
pp: X : Type u_1
ι : Sort u_3
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed[inst✝²] (f i)
hU : s ⊆ ⋃ i, f i
g : ι → Set X := fun i ↦ (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen[inst✝²] (g i)
⊢ Dense (⋂ i, g i)

Tactic:
refine dense_iInter_of_isOpen hgo fun i x => ?_

Goal state after:
X : Type u_1
ι : Sort u_3
inst✝² : TopologicalSpace X
inst✝¹ : BaireSpace X
inst✝ : Countable ι
s : Set X
hs : IsGδ s
hd : Dense s
f : ι → Set X
hc : ∀ (i : ι), IsClosed[inst✝²] (f i)
hU : s ⊆ ⋃ i, f i
g : ι → Set X := fun i ↦ (frontier (f i))ᶜ
hgo : ∀ (i : ι), IsOpen[inst✝²] (g i)
i : ι
x : X
⊢ x ∈ closure[inst✝²] (g i)
Module: Mathlib.Topology.Homeomorph.Lemmas

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : X ≃ Y
⊢ IsHomeomorph ⇑e ↔ Continuous[inst✝¹, inst✝] ⇑e ∧ Continuous[inst✝, inst✝¹] ⇑e.symm

Tactic:
e.continuous_symm_iff

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : X ≃ Y
⊢ IsHomeomorph ⇑e ↔ Continuous[inst✝¹, inst✝] ⇑e ∧ IsOpenMap ⇑e
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
l : Filter α
h : Cauchy l
⊢ Cauchy ↑(Ultrafilter.of l)

Tactic:
have := h.1
  have := Ultrafilter.of_le l
  exact ⟨Ultrafilter.neBot _, (Filter.prod_mono this this).trans h.2⟩

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

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
⊢ 𝓤 α ≤ map Prod.swap (𝓤 α)

Tactic:
rw [map_swap_eq_comap_swap]

Goal state after:
α : Type ua
inst✝ : UniformSpace α
⊢ 𝓤 α ≤ comap Prod.swap (𝓤 α)
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
V : SetRel α α
h : V ∈ 𝓤 α
⊢ V.symmetrize ∈ 𝓤 α

Tactic:
apply (𝓤 α).inter_sets h
  rw [← comap_swap_uniformity]
  exact preimage_mem_comap h

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

Goal state before:
pp: case h
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h✝ : ∀ V ∈ 𝓤 α, ∃ N, ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
V : Set (α × α)
mV : V ∈ 𝓤 α
N : ℕ
h : ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
⊢ ∀ k_1 ≥ N + k, ∀ l ≥ N + k, (u k_1, u l) ∈ V

Tactic:
intro a ha b hb

Goal state after:
case h
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
k : ℕ
h✝ : ∀ V ∈ 𝓤 α, ∃ N, ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
V : Set (α × α)
mV : V ∈ 𝓤 α
N : ℕ
h : ∀ k_1 ≥ N, ∀ l ≥ N, (u (k_1 + k), u (l + k)) ∈ V
a : ℕ
ha : a ≥ N + k
b : ℕ
hb : b ≥ N + k
⊢ (u a, u b) ∈ V
Module: Mathlib.Topology.UniformSpace.Defs

Goal state before:
pp: α : Type ua
inst✝ : UniformSpace α
x : α
V : SetRel α α
V_in : V ∈ 𝓤 α
⊢ ball x V ∈ 𝓝 x

Tactic:
rw [UniformSpace.mem_nhds_iff]
  exact ⟨V, V_in, Subset.rfl⟩

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

Goal state before:
pp: α : Type ua
β : Type ub
f : α → β
u₁ : UniformSpace α
u₂ : Set (UniformSpace β)
⊢ UniformContinuous f ↔ ∀ u ∈ u₂, UniformContinuous f

Tactic:
by
  delta UniformContinuous
  rw [sInf_eq_iInf', iInf_uniformity, tendsto_iInf, SetCoe.forall]

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

Goal state before:
pp: case neg
α : Type u
β : Type v
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : T0Space β
f : α → β
hf : ¬UniformContinuous f
⊢ UniformContinuous (lift' f)

Tactic:
rw [lift', dif_neg hf]
    exact uniformContinuous_of_const fun a _ => rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : UniformCauchySeqOnFilter F p p'
hF' : ∀ᶠ (x : α) in p', Tendsto (fun n ↦ F n x) p (𝓝 (f x))
⊢ TendstoUniformlyOnFilter F f p p'

Tactic:
rcases p.eq_or_neBot with rfl | _
  · simp only [TendstoUniformlyOnFilter, bot_prod, eventually_bot, implies_true]
  -- Proof idea: |f_n(x) - f(x)| ≤ |f_n(x) - f_m(x)| + |f_m(x) - f(x)|. We choose `n`
  -- so that |f_n(x) - f_m(x)| is uniformly small across `s` whenever `m ≥ n`. Then for
  -- a fixed `x`, we choose `m` sufficiently large such that |f_m(x) - f(x)| is small.
  intro u hu
  rcases comp_symm_of_uniformity hu with ⟨t, ht, htsymm, htmem⟩
  -- We will choose n, x, and m simultaneously. n and x come from hF. m comes from hF'
  -- But we need to promote hF' to the full product filter to use it
  have hmc : ∀ᶠ x in (p ×ˢ p) ×ˢ p', Tendsto (fun n : ι => F n x.snd) p (𝓝 (f x.snd)) := by
    rw [eventually_prod_iff]
    exact ⟨fun _ => True, by simp, _, hF', by simp⟩
  -- To apply filter operations we'll need to do some order manipulation
  rw [Filter.eventually_swap_iff]
  have := tendsto_prodAssoc.eventually (tendsto_prod_swap.eventually ((hF t ht).and hmc))
  apply this.curry.mono
  simp only [Equiv.prodAssoc_apply, eventually_and, eventually_const, Prod.snd_swap, Prod.fst_swap,
    and_imp, Prod.forall]
  -- Complete the proof
  intro x n hx hm'
  refine Set.mem_of_mem_of_subset ?_ htmem
  rw [Uniform.tendsto_nhds_right] at hm'
  have := hx.and (hm' ht)
  obtain ⟨m, hm⟩ := this.exists
  exact ⟨F m x, ⟨hm.2, htsymm hm.1⟩⟩

Goal state after:
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)))
⊢ IsComplete (m '' s) ↔ IsComplete s

Tactic:
have fact2 : MapsTo (map m) (Iic <| 𝓟 s) (Iic <| 𝓟 <| m '' s) := mapsTo_image .. |>.filter_map_Iic

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)))
⊢ IsComplete (m '' s) ↔ IsComplete s
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
ind : (x : α) → x ∈ K → ι
W : (x : α) → x ∈ K → Set (α × α)
hW : ∀ (x : α) (a : x ∈ K), W x a ∈ 𝓤 α
hWU : ∀ (x : α) (a : x ∈ K), ball x (W x a ○ W x a) ⊆ U (ind x a)
t : Finset ↑K
ht : K ⊆ ⋃ x ∈ t, ball (↑x) (W ↑x ⋯)
x : α
hx : x ∈ K
y : ↑K
hyt : y ∈ t
hxy : x ∈ ball (↑y) (W ↑y ⋯)
⊢ ∃ i, ball x (⋂ x ∈ t, W ↑x ⋯) ⊆ U i

Tactic:
exact ⟨ind y y.2, fun z hz ↦ hWU _ _ ⟨x, hxy, mem_iInter₂.1 hz _ hyt⟩⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : UniformSpace α
inst✝² : UniformSpace β
inst✝¹ : UniformSpace γ
e : β → α
h_e : IsUniformInducing e
h_dense : DenseRange e
f : β → γ
h_f : UniformContinuous f
inst✝ : CompleteSpace γ
a : α
⊢ Tendsto f (comap e (𝓝 a)) (𝓝 (⋯.extend f a))

Tactic:
simpa only [IsDenseInducing.extend] using
    tendsto_nhds_limUnder (uniformly_extend_exists h_e ‹_› h_f _)

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 → α
⊢ range f ⊆ insert 1 (f '' mulSupport f)

Tactic:
exact range_subset_insert_image_mulSupport f

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u
U : (i : ι) → UniformSpace (α i)
𝔖 : Set (Set ι)
⊢ UniformSpace.comap (⋃₀ 𝔖).domRestrict (uniformSpace fun i ↦ α ↑i) =
    ⨅ S ∈ 𝔖, UniformSpace.comap S.domRestrict (uniformSpace fun i ↦ α ↑i)

Tactic:
by
  simp_rw [Pi.uniformSpace_comap_restrict α, iInf_sUnion]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set α
f : α → β
hs : IsCompact s
hf : ContinuousOn f s
⊢ UniformContinuous (s.domRestrict f)

Tactic:
isCompact_iff_compactSpace

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set α
f : α → β
hs : CompactSpace ↑s
hf : ContinuousOn f s
⊢ UniformContinuous (s.domRestrict f)
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
δ : ι → Type u_6
φ : (i : ι) → δ i → α
h_cover : ∃ I, I.Finite ∧ ⋃ i ∈ I, range (φ i) = univ
⊢ uniformSpace α β = ⨅ i, UniformSpace.comap (⇑ofFun ∘ (fun x ↦ x ∘ φ i) ∘ ⇑toFun) (uniformSpace (δ i) β)

Tactic:
ext : 1
  simp_rw [iInf_uniformity, uniformity_comap]
  refine le_antisymm (le_iInf fun i ↦ tendsto_iff_comap.mp UniformFun.precomp_uniformContinuous) ?_
  rcases h_cover with ⟨I, I_finite, I_cover⟩
  refine HasBasis.iInf (fun i : ι ↦ UniformFun.hasBasis_uniformity (δ i) β |>.comap _)
      |>.le_basis_iff (UniformFun.hasBasis_uniformity α β) |>.mpr fun U hU ↦
    ⟨⟨I, fun _ ↦ U⟩, ⟨I_finite, fun _ ↦ hU⟩, fun ⟨f, g⟩ hfg x ↦ ?_⟩
  rcases mem_iUnion₂.mp <| I_cover.ge <| mem_univ x with ⟨i, hi, y, rfl⟩
  exact mem_iInter.mp hfg ⟨i, hi⟩ y

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
⊢ UniformContinuous fun f ↦ (ofFun 𝔖) (UniformFun.toFun f)

Tactic:
simp only [UniformContinuous, UniformOnFun.uniformity_eq, tendsto_iInf, tendsto_principal,
    (UniformFun.hasBasis_uniformity _ _).eventually_iff]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
⊢ ∀ i ∈ 𝔖,
    ∀ i_2 ∈ 𝓤 β,
      ∃ i_4 ∈ 𝓤 β,
        ∀ ⦃x : (α →ᵤ β) × (α →ᵤ β)⦄,
          x ∈ UniformFun.gen α β i_4 →
            ((ofFun 𝔖) (UniformFun.toFun x.1), (ofFun 𝔖) (UniformFun.toFun x.2)) ∈ UniformOnFun.gen 𝔖 i i_2
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: Y : Type u_5
α : Type u_6
β : Type u_8
tY : TopologicalSpace Y
uα : UniformSpace α
uβ : UniformSpace β
A : Set Y
u : Y → β → α
S : Set β
hA : UniformEquicontinuousOn (u ∘ Subtype.val) S
hu : Continuous[tY, Pi.topologicalSpace] (S.domRestrict ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
⊢ ∀ᶠ (xy : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S),
    ∀ (i : ↑(closure[tY] A)), ((u ∘ Subtype.val) i xy.1, (u ∘ Subtype.val) i xy.2) ∈ U

Tactic:
filter_upwards [hA V hV, mem_inf_of_right (mem_principal_self _)]

Goal state after:
Y : Type u_5
α : Type u_6
β : Type u_8
tY : TopologicalSpace Y
uα : UniformSpace α
uβ : UniformSpace β
A : Set Y
u : Y → β → α
S : Set β
hA : UniformEquicontinuousOn (u ∘ Subtype.val) S
hu : Continuous[tY, Pi.topologicalSpace] (S.domRestrict ∘ u)
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVclosed : IsClosed[instTopologicalSpaceProd] V
hVU : V ⊆ U
⊢ ∀ (a : β × β),
    (∀ (i : ↑A), ((u ∘ Subtype.val) i a.1, (u ∘ Subtype.val) i a.2) ∈ V) →
      a ∈ S ×ˢ S → ∀ (i : ↑(closure[tY] A)), ((u ∘ Subtype.val) i a.1, (u ∘ Subtype.val) i a.2) ∈ U
Module: Mathlib.Order.Filter.Pointwise

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

Tactic:
zero_smul,

Goal state after:
α : Type u_2
β : Type u_3
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
g : Filter β
hg : g.NeBot
s : Set β
hs : s ∈ g
⊢ (fun a ↦ 0) '' s ∈ 0
Module: Mathlib.Topology.Algebra.ConstMulAction

Goal state before:
pp: Γ : Type u_4
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : SMul Γ T
inst✝³ : ProperlyDiscontinuousSMul Γ T
inst✝² : T2Space T
inst✝¹ : LocallyCompactSpace T
inst✝ : ContinuousConstSMul Γ T
x : T
V : Set T
V_cpt : IsCompact V
V_nhd : V ∈ 𝓝 x
Γ₀ : Set Γ := {γ | ((fun x ↦ γ • x) '' V ∩ V).Nonempty ∧ γ • x ≠ x}
this : Finite ↑Γ₀
u v : ↑Γ₀ → Set T
hu : ∀ (γ : ↑Γ₀), u γ ∈ 𝓝 (↑γ • x)
hv : ∀ (γ : ↑Γ₀), v γ ∈ 𝓝 x
u_v_disjoint : ∀ (γ : ↑Γ₀), Disjoint (u γ) (v γ)
γ : Γ
z : T
hz : z ∈ V ∧ ∀ (i : ↑Γ₀), z ∈ (fun x ↦ ↑i • x) ⁻¹' u i ∩ v i
hγz : (fun x ↦ γ • x) z ∈ V ∧ ∀ (i : ↑Γ₀), (fun x ↦ γ • x) z ∈ (fun x ↦ ↑i • x) ⁻¹' u i ∩ v i
h : ¬γ • x = x
⊢ False

Tactic:
let γ : Γ₀ := ⟨γ, ⟨_, ⟨z, hz.1, rfl⟩, hγz.1⟩, h⟩

Goal state after:
Γ : Type u_4
T : Type u_5
inst✝⁵ : TopologicalSpace T
inst✝⁴ : SMul Γ T
inst✝³ : ProperlyDiscontinuousSMul Γ T
inst✝² : T2Space T
inst✝¹ : LocallyCompactSpace T
inst✝ : ContinuousConstSMul Γ T
x : T
V : Set T
V_cpt : IsCompact V
V_nhd : V ∈ 𝓝 x
Γ₀ : Set Γ := {γ | ((fun x ↦ γ • x) '' V ∩ V).Nonempty ∧ γ • x ≠ x}
this : Finite ↑Γ₀
u v : ↑Γ₀ → Set T
hu : ∀ (γ : ↑Γ₀), u γ ∈ 𝓝 (↑γ • x)
hv : ∀ (γ : ↑Γ₀), v γ ∈ 𝓝 x
u_v_disjoint : ∀ (γ : ↑Γ₀), Disjoint (u γ) (v γ)
γ✝ : Γ
z : T
hz : z ∈ V ∧ ∀ (i : ↑Γ₀), z ∈ (fun x ↦ ↑i • x) ⁻¹' u i ∩ v i
hγz : (fun x ↦ γ✝ • x) z ∈ V ∧ ∀ (i : ↑Γ₀), (fun x ↦ γ✝ • x) z ∈ (fun x ↦ ↑i • x) ⁻¹' u i ∩ v i
h : ¬γ✝ • x = x
γ : ↑Γ₀ := ⟨γ✝, ⋯⟩
⊢ False
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
⊢ ∃ U ∈ 𝓝 1, U⁻¹ = U ∧ ∀ g ∈ S, ((fun x ↦ x * g) '' U ∩ U).Nonempty → g = 1

Tactic:
have ⟨U, hU, hUinv, h⟩ := hS.exists_nhds_eq_one_of_image_mulLeft_inter_nonempty
  refine ⟨U, hU, hUinv, fun g hgS hgU ↦ inv_eq_one.mp (h _ (S.inv_mem hgS) ?_)⟩
  rwa [Set.nonempty_image_mulLeft_inv_inter_iff, hUinv]

Goal state after:
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
f : α → G
p : Filter ι
hu : rightUniformSpace G = u
⊢ TendstoUniformly F f p ↔ ∀ u_1 ∈ 𝓝 1, ∀ᶠ (i : ι) in p, ∀ (a : α), F i a / f a ∈ u_1

Tactic:
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 => hv (hi a)⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
δ : Type u_4
G : Type u_5
inst✝⁸ : TopologicalSpace α
inst✝⁷ : AddCommGroup α
inst✝⁶ : IsTopologicalAddGroup α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : AddCommGroup β
inst✝³ : TopologicalSpace δ
inst✝² : AddCommGroup δ
inst✝¹ : UniformSpace G
inst✝ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝¹.toTopologicalSpace] fun p ↦ (φ p.1) p.2
W' : Set G
W'_nhds : W' ∈ 𝓝 0
x₀ : α
y₁ : δ
Nx : Filter α := 𝓝 x₀
ee : β × β → α × α := fun u ↦ (e u.1, e u.2)
this : Tendsto (fun x ↦ (x.2 - x.1, y₁)) (comap (fun p ↦ (e p.1, e p.2)) (𝓝 (x₀, x₀))) (𝓝 0 ×ˢ 𝓝 y₁)
⊢ Tendsto (fun a ↦ (a.2 - a.1, y₁)) (comap (⇑e) Nx ×ˢ comap (⇑e) Nx) (𝓝 0 ×ˢ 𝓝 y₁)

Tactic:
prod_comap_comap_eq,

Goal state after:
α : Type u_1
β : Type u_2
δ : Type u_4
G : Type u_5
inst✝⁸ : TopologicalSpace α
inst✝⁷ : AddCommGroup α
inst✝⁶ : IsTopologicalAddGroup α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : AddCommGroup β
inst✝³ : TopologicalSpace δ
inst✝² : AddCommGroup δ
inst✝¹ : UniformSpace G
inst✝ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝¹.toTopologicalSpace] fun p ↦ (φ p.1) p.2
W' : Set G
W'_nhds : W' ∈ 𝓝 0
x₀ : α
y₁ : δ
Nx : Filter α := 𝓝 x₀
ee : β × β → α × α := fun u ↦ (e u.1, e u.2)
this : Tendsto (fun x ↦ (x.2 - x.1, y₁)) (comap (fun p ↦ (e p.1, e p.2)) (𝓝 (x₀, x₀))) (𝓝 0 ×ˢ 𝓝 y₁)
⊢ Tendsto (fun a ↦ (a.2 - a.1, y₁)) (comap (fun p ↦ (e p.1, e p.2)) (Nx ×ˢ Nx)) (𝓝 0 ×ˢ 𝓝 y₁)
Module: Mathlib.Order.Filter.AtTopBot.CompleteLattice

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝² : Preorder β
inst✝¹ : ConditionallyCompleteLattice γ
l : Filter α
inst✝ : l.NeBot
f : β → γ
hf : Monotone f
hb : BddAbove (range f)
g : α → β
hg : Tendsto g l atTop
⊢ ⨆ a, f (g a) = ⨆ b, f b

Tactic:
have : Nonempty α := nonempty_of_neBot l
  have : Nonempty β := .map g ‹_›
  rw [← csInf_upperBounds_range, ← csInf_upperBounds_range,
    ← hf.upperBounds_range_comp_tendsto_atTop hg, Function.comp_def]
  exacts [hb, hb.mono <| range_comp_subset_range _ _]

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

Goal state before:
pp: K : Type u_2
inst✝⁴ : DivisionRing K
inst✝³ : TopologicalSpace K
inst✝² : IsTopologicalRing K
inst✝¹ : CompactSpace K
inst✝ : T2Space K
this : DiscreteTopology K
⊢ Finite K

Tactic:
exact finite_of_compact_of_discrete

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMaxOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
⊢ s ∈ 𝓝[>] a ↔ ∃ u ∈ Ioi a, Ioc a u ⊆ s

Tactic:
rw [mem_nhdsGT_iff_exists_Ioo_subset]

Goal state after:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMaxOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
⊢ (∃ u ∈ Ioi a, Ioo a u ⊆ s) ↔ ∃ u ∈ Ioi a, Ioc a u ⊆ s
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atTop
a✝ : Nontrivial α
⊢ Tendsto (fun x ↦ f x * g x) l atTop

Tactic:
obtain ⟨C', hC'⟩ : ∃ C', C' < C := exists_lt C

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : OrderTopology α
l : Filter β
f g : β → α
C : α
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atTop
a✝ : Nontrivial α
C' : α
hC' : C' < C
⊢ Tendsto (fun x ↦ f x * g x) l atTop
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n m : ℕ
hn : 0 < n
⊢ m.gcd n * addOrderOf ↑(↑m / ↑n * p) = n

Tactic:
by
  rw [natCast_div_mul_eq_nsmul, IsOfFinAddOrder.addOrderOf_nsmul]
  · rw [addOrderOf_period_div hn, Nat.gcd_comm, Nat.mul_div_cancel']
    exact n.gcd_dvd_left m
  · rwa [← addOrderOf_pos_iff, addOrderOf_period_div hn]

Goal state after:
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)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : n • ↑k = 0
⊢ ∃ m < n, ↑(↑m / ↑n * p) = ↑k

Tactic:
rw [← coe_nsmul, coe_eq_zero_iff] at hk

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
hk : ∃ n_1, n_1 • p = n • k
⊢ ∃ m < n, ↑(↑m / ↑n * p) = ↑k
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case refine_1.refine_1
𝕜 : Type u_1
B : Type u_2
inst✝² : Field 𝕜
p q : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
m₁ m₂ : ↑{m | m < n ∧ m.gcd n = 1}
h : ↑m₁ • ↑(p / ↑n) = ↑m₂ • ↑(p / ↑n)
⊢ ↑m₁ ∈ Iio n

pp: case refine_1.refine_2
𝕜 : Type u_1
B : Type u_2
inst✝² : Field 𝕜
p q : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
m₁ m₂ : ↑{m | m < n ∧ m.gcd n = 1}
h : ↑m₁ • ↑(p / ↑n) = ↑m₂ • ↑(p / ↑n)
⊢ ↑m₂ ∈ Iio n

Tactic:
exacts [m₁.2.1, m₂.2.1]

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

Goal state before:
pp: case left
𝕜 : Type u_1
B : Type u_2
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
⊢ ContinuousWithinAt (fun x ↦ ⟨toIocMod ⋯ a x, ⋯⟩) (Iic x) x

Tactic:
IsInducing.subtypeVal.continuousWithinAt_iff

Goal state after:
case left
𝕜 : Type u_1
B : Type u_2
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
⊢ ContinuousWithinAt (Subtype.val ∘ fun x ↦ ⟨toIocMod ⋯ a x, ⋯⟩) (Iic x) x
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case right
𝕜 : Type u_1
B : Type u_2
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
⊢ ContinuousWithinAt (fun x ↦ ⟨toIcoMod ⋯ a x, ⋯⟩) (Ici x) x

Tactic:
IsInducing.subtypeVal.continuousWithinAt_iff

Goal state after:
case right
𝕜 : Type u_1
B : Type u_2
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
x : 𝕜
⊢ ContinuousWithinAt (Subtype.val ∘ fun x ↦ ⟨toIcoMod ⋯ a x, ⋯⟩) (Ici x) x
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
⊢ (mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact ∧ S.δ₀.Exact → S.Exact

Tactic:
rintro ⟨h, h₀⟩

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : (mk₂ (S.map' 0 1 isComplex₂_iff._proof_2 ⋯) (S.map' 1 2 isComplex₂_iff._proof_4 ⋯)).Exact
h₀ : S.δ₀.Exact
⊢ S.Exact
Module: Mathlib.Algebra.Homology.ExactSequence

Goal state before:
pp: case mp.right
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C (n + 2)
h : S.Exact
⊢ (mk₂ (S.map' n (n + 1) ⋯ ⋯) (S.map' (n + 1) (n + 2) ⋯ ⋯)).Exact

Tactic:
rw [exact₂_iff]; swap
      · rw [isComplex₂_iff]
        exact h.toIsComplex.zero n
      exact h.exact n (by lia)

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : SnakeInput C
f : S₁ ⟶ S₂
⊢ S₁.φ₁ ≫ (f.f₂ ≫ S₂.v₂₃).τ₁ = pullback.snd S₁.L₁.g S₁.v₀₁.τ₃ ≫ f.f₀.τ₃ ≫ S₂.δ

Tactic:
comp_τ₁,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : SnakeInput C
f : S₁ ⟶ S₂
⊢ S₁.φ₁ ≫ f.f₂.τ₁ ≫ S₂.v₂₃.τ₁ = pullback.snd S₁.L₁.g S₁.v₀₁.τ₃ ≫ f.f₀.τ₃ ≫ S₂.δ
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: J : MultispanShape
l : J.L
val✝ : Unit
T₁ : Type := { u // J.fst l = J.snd l }
T₂ : Type := { u // J.snd l = J.snd l }
x✝ : T₂
⊢ left l ⟶ right (J.snd l)

Tactic:
exact Hom.snd l

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.ChangeOfRingsExact

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
R' : Type u'
inst✝ : CommRing R'
f : R →+* R'
⊢ Limits.PreservesFiniteColimits (ModuleCat.restrictScalars f)

Tactic:
have := ((CategoryTheory.Functor.exact_tfae (ModuleCat.restrictScalars.{v} f)).out 1 3).mp
    (ModuleCat.restrictScalars_map_exact f)
  exact this.2

Goal state after: