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

Goal state before:
pp: case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
x✝ : ∃ x, (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed[inst✝] x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x
S : Set (Set X)
hS : ∀ ⦃x : Set X⦄, x ∈ S → IsClosed[inst✝] x ∧ IsNowhereDense x
hc : (compl '' S).Countable
hsub : s ⊆ ⋃₀ S
⊢ S.Countable

Tactic:
rw [← compl_compl_image S]

Goal state after:
case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
x✝ : ∃ x, (∀ ⦃x_1 : Set X⦄, x_1 ∈ x → IsClosed[inst✝] x_1 ∧ IsNowhereDense x_1) ∧ (compl '' x).Countable ∧ s ⊆ ⋃₀ x
S : Set (Set X)
hS : ∀ ⦃x : Set X⦄, x ∈ S → IsClosed[inst✝] x ∧ IsNowhereDense x
hc : (compl '' S).Countable
hsub : s ⊆ ⋃₀ S
⊢ (compl '' compl '' S).Countable
Module: Mathlib.Topology.Connected.Clopen

Goal state before:
pp: α : Type u
inst✝ : TopologicalSpace α
h : ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
f : α → Bool
hf : Continuous[inst✝, _] f
x y : α
this : f ⁻¹' {false} = (f ⁻¹' {true})ᶜ
⊢ f x = f y

Tactic:
obtain (h | h) := h _ ((isClopen_discrete {true}).preimage hf)

Goal state after:
case inl
α : Type u
inst✝ : TopologicalSpace α
h✝ : ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
f : α → Bool
hf : Continuous[inst✝, _] f
x y : α
this : f ⁻¹' {false} = (f ⁻¹' {true})ᶜ
h : f ⁻¹' {true} = ∅
⊢ f x = f y

case inr
α : Type u
inst✝ : TopologicalSpace α
h✝ : ∀ (s : Set α), IsClopen s → s = ∅ ∨ s = univ
f : α → Bool
hf : Continuous[inst✝, _] f
x y : α
this : f ⁻¹' {false} = (f ⁻¹' {true})ᶜ
h : f ⁻¹' {true} = univ
⊢ f x = f y
Module: Mathlib.Topology.UniformSpace.Basic

Goal state before:
pp: α : Type ua
β : Type ub
f : α → β
U : SetRel β β
x : α
⊢ UniformSpace.ball x (Prod.map f f ⁻¹' U) = f ⁻¹' UniformSpace.ball (f x) U

Tactic:
ext : 1
  simp only [UniformSpace.ball, mem_preimage, Prod.map_apply]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : UniformSpace β
x : α
inst✝¹ : UniformSpace α
inst✝ : UniformSpace γ
U : Set α
hU : U ∈ 𝓝 x
F : α → β → γ
hF : UniformContinuousOn (↿F) (U ×ˢ univ)
⊢ TendstoUniformly F (F x) (𝓝 x)

Tactic:
by
  simpa only [tendstoUniformlyOn_univ, nhdsWithin_eq_nhds.2 hU]
    using hF.tendstoUniformlyOn (mem_of_mem_nhds hU)

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

Goal state before:
pp: α : Type u_2
x✝ : UniformSpace α
⊢ 𝓤 α = 𝓤 α

Tactic:
uniformity_comap,

Goal state after:
α : Type u_2
x✝ : UniformSpace α
⊢ comap (Prod.map id id) (𝓤 α) = 𝓤 α
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
l : Filter ι
h : TendstoUniformlyOn F f l s
u : ℕ → ι
hu : Tendsto u atTop l
⊢ TendstoUniformlyOn (fun n ↦ F (u n)) f atTop s

Tactic:
rw [tendstoUniformlyOn_iff_tendsto] at h ⊢
  exact h.comp ((hu.comp tendsto_fst).prodMk tendsto_snd)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
s : Set α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen[inst✝²] s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K
tfae_2_to_3 : (∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K) → ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v
h : ∀ x ∈ s, ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (g y, G n y) ∈ u

Tactic:
by
    obtain ⟨v, hv1, hv2⟩ := h x hx
    exact ⟨v, hv1, hv2 u hu⟩

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

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
inst✝ : Finite ι
F : ι → X → α
S : Set X
⊢ EquicontinuousOn F S ↔ ∀ (i : ι), ContinuousOn (F i) S

Tactic:
simp only [EquicontinuousOn, equicontinuousWithinAt_finite, ContinuousOn, @forall_comm ι]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
ι : Sort u_5
p : ι → Prop
V : ι → Set (β × β)
h : (𝓤 β).HasBasis p V
⊢ ⨅ i ∈ 𝔖, 𝓤 (α →ᵤ[𝔖] β) = ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i))

Tactic:
uniformity_comap,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
ι : Sort u_5
p : ι → Prop
V : ι → Set (β × β)
h : (𝓤 β).HasBasis p V
⊢ ⨅ i ∈ 𝔖,
      comap (Prod.map (⇑UniformFun.ofFun ∘ i.domRestrict ∘ ⇑(toFun 𝔖)) (⇑UniformFun.ofFun ∘ i.domRestrict ∘ ⇑(toFun 𝔖)))
        (𝓤 (↑i →ᵤ β)) =
    ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), 𝓟 (UniformOnFun.gen 𝔖 s (V i))
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set (β × β)
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → β → α
hβ : (𝓤 β).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ Tendsto (fun x ↦ ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2)) (𝓤 β) (𝓤 (ι →ᵤ α)) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂

Tactic:
hβ.tendsto_iff (UniformFun.hasBasis_uniformity_of_basis ι α hα)

Goal state after:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set (β × β)
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → β → α
hβ : (𝓤 β).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ (∀ (ib : κ₂),
      p₂ ib →
        ∃ ia, p₁ ia ∧ ∀ x ∈ s₁ ia, ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2) ∈ (UniformFun.gen ι α ∘ s₂) ib) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 𝔗 : Set (Set α)
h : ∀ s ∈ 𝔖, ∃ T ⊆ 𝔗, T.Finite ∧ s ⊆ ⋃₀ T
V : Set (β × β)
hV : V ∈ 𝓤 β
⊢ Tendsto (fun x ↦ ((⇑(ofFun 𝔗) ∘ ⇑(toFun 𝔖)) x.1, (⇑(ofFun 𝔗) ∘ ⇑(toFun 𝔖)) x.2))
    (⨅ i₁ ∈ 𝔗, 𝓟 (UniformOnFun.gen 𝔗 i₁ V)) (⨅ i₁ ∈ 𝔖, 𝓟 (UniformOnFun.gen 𝔖 i₁ V))

Tactic:
simp only [tendsto_iInf, tendsto_principal, Filter.Eventually, mem_biInf_principal]

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 𝔗 : Set (Set α)
h : ∀ s ∈ 𝔖, ∃ T ⊆ 𝔗, T.Finite ∧ s ⊆ ⋃₀ T
V : Set (β × β)
hV : V ∈ 𝓤 β
⊢ ∀ i ∈ 𝔖,
    ∃ I,
      I.Finite ∧
        (∀ i ∈ I, i ∈ 𝔗) ∧
          ⋂ i ∈ I, UniformOnFun.gen 𝔗 i V ⊆
            {x | ((⇑(ofFun 𝔗) ∘ ⇑(toFun 𝔖)) x.1, (⇑(ofFun 𝔗) ∘ ⇑(toFun 𝔖)) x.2) ∈ UniformOnFun.gen 𝔖 i V}
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set (β × β)
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → β → α
S : Set β
hβ : (𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ Tendsto (fun x ↦ ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2)) (𝓤 β ⊓ 𝓟 (S ×ˢ S)) (𝓤 (ι →ᵤ α)) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂

Tactic:
hβ.tendsto_iff (UniformFun.hasBasis_uniformity_of_basis ι α hα)

Goal state after:
ι : Type u_1
α : Type u_6
β : Type u_8
uα : UniformSpace α
uβ : UniformSpace β
κ₁ : Type u_11
κ₂ : Type u_12
p₁ : κ₁ → Prop
s₁ : κ₁ → Set (β × β)
p₂ : κ₂ → Prop
s₂ : κ₂ → Set (α × α)
F : ι → β → α
S : Set β
hβ : (𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p₁ s₁
hα : (𝓤 α).HasBasis p₂ s₂
⊢ (∀ (ib : κ₂),
      p₂ ib →
        ∃ ia, p₁ ia ∧ ∀ x ∈ s₁ ia, ((⇑ofFun ∘ swap F) x.1, (⇑ofFun ∘ swap F) x.2) ∈ (UniformFun.gen ι α ∘ s₂) ib) ↔
    ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂
Module: Mathlib.Topology.UniformSpace.Equicontinuity

Goal state before:
pp: ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
inst✝ : l.NeBot
F : ι → X → α
f : X → α
x₀ : X
h₁ : Tendsto F l (𝓝 f)
h₂ : EquicontinuousAt F x₀
⊢ ContinuousAt f x₀

Tactic:
by
  rw [← continuousWithinAt_univ, ← equicontinuousWithinAt_univ, tendsto_pi_nhds] at *
  exact continuousWithinAt_of_equicontinuousWithinAt (fun x _ ↦ h₁ x) (h₁ x₀) h₂

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 α)
inst✝ : UniformSpace γ
H : 𝓤 (α →ᵤ[𝔖] β × γ) = 𝓤 (α →ᵤ[𝔖] β × γ)
⊢ comap
        ((fun p ↦ (p.1.1, p.2.1)) ∘ fun x ↦
          (((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.1,
            ((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.2))
        (𝓤 (α →ᵤ[𝔖] β)) ⊓
      comap
        ((fun p ↦ (p.1.2, p.2.2)) ∘ fun x ↦
          (((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.1,
            ((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.2))
        (𝓤 (α →ᵤ[𝔖] γ)) =
    𝓤 (α →ᵤ[𝔖] β × γ) ⊓ 𝓤 (α →ᵤ[𝔖] β × γ)

Tactic:
uniformity_comap,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
s : Set α
p : Filter ι
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : UniformSpace γ
H : 𝓤 (α →ᵤ[𝔖] β × γ) = 𝓤 (α →ᵤ[𝔖] β × γ)
⊢ comap
        ((fun p ↦ (p.1.1, p.2.1)) ∘ fun x ↦
          (((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.1,
            ((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.2))
        (𝓤 (α →ᵤ[𝔖] β)) ⊓
      comap
        ((fun p ↦ (p.1.2, p.2.2)) ∘ fun x ↦
          (((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.1,
            ((ofFun 𝔖).symm.trans
                ((Equiv.arrowProdEquivProdArrow α (fun a ↦ β) fun a ↦ γ).trans ((ofFun 𝔖).prodCongr (ofFun 𝔖))))
              x.2))
        (𝓤 (α →ᵤ[𝔖] γ)) =
    comap (Prod.map (fun x ↦ Prod.fst ∘ x) fun x ↦ Prod.fst ∘ x) (𝓤 (α → β)) ⊓ 𝓤 (α →ᵤ[𝔖] β × γ)
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : DivisionMonoid α
f g : Filter α
hfg✝ : f * g = 1
t₁ : Set α
h₁ : t₁ ∈ f
t₂ : Set α
h₂ : t₂ ∈ g
h : t₁ * t₂ ⊆ 1
hfg : (f * g).NeBot
⊢ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1

Tactic:
(hfg.nonempty_of_mem <| mul_mem_mul h₁ h₂).subset_one_iff,

Goal state after:
case refine_1
α : Type u_2
inst✝ : DivisionMonoid α
f g : Filter α
hfg✝ : f * g = 1
t₁ : Set α
h₁ : t₁ ∈ f
t₂ : Set α
h₂ : t₂ ∈ g
h : t₁ * t₂ = 1
hfg : (f * g).NeBot
⊢ ∃ a b, f = pure a ∧ g = pure b ∧ a * b = 1
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
δ₁ : Type u_5
δ₂ : Type u_6
φ₁ : δ₁ → α
φ₂ : δ₂ → α
𝔗₁ : Set (Set δ₁)
𝔗₂ : Set (Set δ₂)
h_image₁ : MapsTo (fun x ↦ φ₁ '' x) 𝔗₁ 𝔖
h_image₂ : MapsTo (fun x ↦ φ₂ '' x) 𝔗₂ 𝔖
h_preimage₁ : MapsTo (fun x ↦ φ₁ ⁻¹' x) 𝔖 𝔗₁
h_preimage₂ : MapsTo (fun x ↦ φ₂ ⁻¹' x) 𝔖 𝔗₂
h_cover : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂
ψ₁ : (S : Set α) → ↑(φ₁ ⁻¹' S) → ↑S := fun S ↦ S.restrictPreimage φ₁
ψ₂ : (S : Set α) → ↑(φ₂ ⁻¹' S) → ↑S := fun S ↦ S.restrictPreimage φ₂
this :
  ∀ S ∈ 𝔖,
    UniformFun.uniformSpace (↑S) β =
      UniformSpace.comap (fun x ↦ x ∘ ψ₁ S) (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S)) β) ⊓
        UniformSpace.comap (fun x ↦ x ∘ ψ₂ S) (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S)) β)
S : Set α
hS : S ∈ 𝔖
⊢ (⨅ i ∈ 𝔗₁,
        UniformSpace.comap
          ((⇑UniformFun.ofFun ∘ i.domRestrict ∘ ⇑(toFun 𝔗₁)) ∘ ⇑(ofFun 𝔗₁) ∘ (fun x ↦ x ∘ φ₁) ∘ ⇑(toFun 𝔖))
          (UniformFun.uniformSpace (↑i) β)) ⊓
      ⨅ i ∈ 𝔗₂,
        UniformSpace.comap
          ((⇑UniformFun.ofFun ∘ i.domRestrict ∘ ⇑(toFun 𝔗₂)) ∘ ⇑(ofFun 𝔗₂) ∘ (fun x ↦ x ∘ φ₂) ∘ ⇑(toFun 𝔖))
          (UniformFun.uniformSpace (↑i) β) ≤
    UniformSpace.comap ((fun x ↦ x ∘ ψ₁ S) ∘ ⇑UniformFun.ofFun ∘ S.domRestrict ∘ ⇑(toFun 𝔖))
        (UniformFun.uniformSpace (↑(φ₁ ⁻¹' S)) β) ⊓
      UniformSpace.comap ((fun x ↦ x ∘ ψ₂ S) ∘ ⇑UniformFun.ofFun ∘ S.domRestrict ∘ ⇑(toFun 𝔖))
        (UniformFun.uniformSpace (↑(φ₂ ⁻¹' S)) β)

Tactic:
exact inf_le_inf
      (iInf₂_le_of_le _ (h_preimage₁ hS) le_rfl)
      (iInf₂_le_of_le _ (h_preimage₂ hS) le_rfl)

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
ha : a < 0
x : α
h : x ∈ Iio a⁻¹
h' : x < 0
⊢ x ∈ (Ioo a 0)⁻¹

Tactic:
exact ⟨(lt_inv_of_neg ha h').2 h, inv_neg''.2 h'⟩

Goal state after:
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: case mp
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space Y
y : Y
⊢ ((Continuous[inst✝², inst✝¹] fun x ↦ y) ∧ (IsClosedMap fun x ↦ y) ∧ ∀ (y_1 : Y), IsCompact ((fun x ↦ y) ⁻¹' {y_1})) →
    CompactSpace X

pp: case mpr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space Y
y : Y
⊢ CompactSpace X →
    (Continuous[inst✝², inst✝¹] fun x ↦ y) ∧ (IsClosedMap fun x ↦ y) ∧ ∀ (y_1 : Y), IsCompact ((fun x ↦ y) ⁻¹' {y_1})

Tactic:
· rintro ⟨-, -, h⟩
    exact ⟨by simpa using h y⟩

Goal state after:
case mpr
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space Y
y : Y
⊢ CompactSpace X →
    (Continuous[inst✝², inst✝¹] fun x ↦ y) ∧ (IsClosedMap fun x ↦ y) ∧ ∀ (y_1 : Y), IsCompact ((fun x ↦ y) ⁻¹' {y_1})
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s t : Set G
hs : IsOpen[inst✝²] s
⊢ IsOpen[inst✝²] (s / t)

Tactic:
by
  rw [← iUnion_div_right_image]
  exact isOpen_biUnion fun a _ => isOpenMap_div_right a s hs

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
U : Set G
hU : U ∈ 𝓝 1
x : G
hx : ∀ t ∈ 𝓝 x, (t ∩ U).Nonempty
⊢ x ∈ U * U

Tactic:
have hkey : (fun y => x / y) ⁻¹' U ∈ 𝓝 x :=
    ContinuousAt.preimage_mem_nhds (by fun_prop) (by simpa)

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
U : Set G
hU : U ∈ 𝓝 1
x : G
hx : ∀ t ∈ 𝓝 x, (t ∩ U).Nonempty
hkey : (fun y ↦ x / y) ⁻¹' U ∈ 𝓝 x
⊢ x ∈ U * U
Module: Mathlib.Order.Filter.AtTopBot.Field

Goal state before:
pp: case hb
α : Type u_1
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
k : α
hk : 0 < k
b : α
x✝ : 1 ≤ b
⊢ k ≠ 0

Tactic:
exact ne_of_gt hk

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

Goal state before:
pp: α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : IsUniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : (𝓝 1).HasBasis p U
⊢ (𝓤 α).HasBasis p fun i ↦ {x | x.1 / x.2 ∈ U i}

Tactic:
rw [uniformity_eq_comap_nhds_one_swapped]
  exact h.comap _

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

Goal state before:
pp: G : Type w
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
c a : G
⊢ map (fun x ↦ x / c) (𝓝 a) = 𝓝 (a / c)

Tactic:
convert! (Homeomorph.divRight c).map_nhds_eq .. using 2

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

Goal state before:
pp: case refine_1
G : Type w
H : Type x
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : IsTopologicalGroup G
inst✝¹ : SeparableSpace G
inst✝ : WeaklyLocallyCompactSpace G
L : Set G
hLc : IsCompact L
hL1 : L ∈ 𝓝 1
⊢ ∀ (n : ℕ), IsCompact ((fun n ↦ (fun x ↦ x * denseSeq G n) ⁻¹' L) n)

pp: case refine_2
G : Type w
H : Type x
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : IsTopologicalGroup G
inst✝¹ : SeparableSpace G
inst✝ : WeaklyLocallyCompactSpace G
L : Set G
hLc : IsCompact L
hL1 : L ∈ 𝓝 1
⊢ ⋃ n, (fun n ↦ (fun x ↦ x * denseSeq G n) ⁻¹' L) n = univ

Tactic:
· intro n
    exact (Homeomorph.mulRight _).isCompact_preimage.mpr hLc

Goal state after:
case refine_2
G : Type w
H : Type x
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace G
inst✝³ : Group G
inst✝² : IsTopologicalGroup G
inst✝¹ : SeparableSpace G
inst✝ : WeaklyLocallyCompactSpace G
L : Set G
hLc : IsCompact L
hL1 : L ∈ 𝓝 1
⊢ ⋃ n, (fun n ↦ (fun x ↦ x * denseSeq G n) ⁻¹' L) n = univ
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
this : Nonempty α
⊢ ⨆ a, f (g a) = ⨆ b, f b

Tactic:
have : Nonempty β := .map g ‹_›

Goal state after:
α : 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
this✝ : Nonempty α
this : Nonempty β
⊢ ⨆ a, f (g a) = ⨆ b, f b
Module: Mathlib.Topology.Algebra.Field

Goal state before:
pp: K : Type u_1
inst✝⁴ : DivisionRing K
inst✝³ : TopologicalSpace K
𝕜 : Type u_2
inst✝² : Field 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : IsTopologicalRing 𝕜
a b : 𝕜
h : a ≠ 0
x : 𝕜
⊢ (fun y ↦ (y - b) / a) ((fun x ↦ a * x + b) x) = x

Tactic:
simp only [add_sub_cancel_right]

Goal state after:
K : Type u_1
inst✝⁴ : DivisionRing K
inst✝³ : TopologicalSpace K
𝕜 : Type u_2
inst✝² : Field 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : IsTopologicalRing 𝕜
a b : 𝕜
h : a ≠ 0
x : 𝕜
⊢ a * x / a = 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 b : α i
⊢ Icc (update f i (a ⊓ b)) (update f i (a ⊔ b)) = uIcc (update f i a) (update f i b)

Tactic:
by simp_rw [uIcc, update_sup, update_inf]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y x' y' : (i : ι) → α i
⊢ (Icc x y \ univ.pi fun i ↦ Ioo (x' i) (y' i)) ⊆ (⋃ i, Icc x (update y i (x' i))) ∪ ⋃ i, Icc (update x i (y' i)) y

Tactic:
by
  rintro a ⟨⟨hxa, hay⟩, ha'⟩
  simp only [mem_pi, mem_univ, mem_Ioo, true_implies, not_forall] at ha'
  simp only [le_update_iff, update_le_iff, mem_union, mem_iUnion, mem_Icc,
    hxa, hay _, hxa _, hay, ← exists_or]
  rcases ha' with ⟨w, hw⟩
  apply Exists.intro w
  cases lt_or_ge (x' w) (a w) <;> simp_all

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℤ
hn : n < 0
⊢ Tendsto (fun x ↦ x ^ n) atTop (𝓝 0)

Tactic:
lift -n to ℕ using le_of_lt (neg_pos.mpr hn) with N h

Goal state after:
𝕜 : Type u_1
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℤ
hn : n < 0
N : ℕ
h : ↑N = -n
⊢ Tendsto (fun x ↦ x ^ n) atTop (𝓝 0)
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
⊢ 𝓝[<] a = ⊥ ↔ IsBot a ∨ ∃ b, b ⋖ a

Tactic:
by
  convert! (config := { preTransparency := .default })
    nhdsGT_eq_bot_iff (a := OrderDual.toDual a) using 4
  exact ofDual_covBy_ofDual_iff

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
⊢ e.symm ≈ e'.symm

Tactic:
refine ⟨target_eq h, eqOn_of_leftInvOn_of_rightInvOn e.leftInvOn ?_ ?_⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
⊢ RightInvOn (↑e'.symm) (↑e) e.symm.source

case refine_2
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
⊢ MapsTo (↑e'.symm) e.symm.source e.source
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:
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)
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
    x₂ ≫ S₁.g = 0 → ∀ (y₁ : A ⟶ S₂.X₁), x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S₁.f
⊢ Mono (homologyMap φ)

Tactic:
rw [Preadditive.mono_iff_cancel_zero]

Goal state after:
case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ S₁.X₂),
    x₂ ≫ S₁.g = 0 → ∀ (y₁ : A ⟶ S₂.X₁), x₂ ≫ φ.τ₂ = y₁ ≫ S₂.f → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S₁.f
⊢ ∀ (P : C) (g : P ⟶ S₁.homology), g ≫ homologyMap φ = 0 → g = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: J : MultispanShape
a b : J.L
h : ¬a = b
⊢ ∀ (a : left a ⟶ left b), False

Tactic:
by rintro ⟨⟩; simp at h

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: J : MultispanShape
a b : J.R
h : ¬a = b
⊢ ∀ (a : right a ⟶ right b), False

Tactic:
by rintro ⟨⟩; simp at h

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
i : Fin (n + 1 + 1)
⊢ map F f i i ⋯ = 𝟙 (obj F X i)

Tactic:
obtain ⟨_ | _, hi⟩ := i <;> simp

Goal state after:
Module: Mathlib.RingTheory.Ideal.Pointwise

Goal state before:
pp: M : Type u_1
inst✝⁴ : Group M
N : Type u_4
inst✝³ : Group N
R : Type u_5
inst✝² : Ring R
inst✝¹ : MulSemiringAction M R
inst✝ : MulSemiringAction N R
I : Ideal R
e : M ≃* N
he : ∀ (m : M) (x : R), e m • x = m • x
n : ↥(inertia N I)
x : R
⊢ (I.inertiaEquiv e he).symm ((I.inertiaEquiv e he) ((I.inertiaEquiv e he).symm n)) • x =
    (I.inertiaEquiv e he) ((I.inertiaEquiv e he).symm n) • x

Tactic:
inertiaEquiv_apply_smul,

Goal state after:
M : Type u_1
inst✝⁴ : Group M
N : Type u_4
inst✝³ : Group N
R : Type u_5
inst✝² : Ring R
inst✝¹ : MulSemiringAction M R
inst✝ : MulSemiringAction N R
I : Ideal R
e : M ≃* N
he : ∀ (m : M) (x : R), e m • x = m • x
n : ↥(inertia N I)
x : R
⊢ (I.inertiaEquiv e he).symm ((I.inertiaEquiv e he) ((I.inertiaEquiv e he).symm n)) • x =
    (I.inertiaEquiv e he).symm n • x
Module: Mathlib.Algebra.Ring.Action.Pointwise.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Ring α
inst✝¹ : AddCommGroup β
inst✝ : Module α β
a : α
t : Set β
⊢ (fun x ↦ -a • x) '' t = (fun x ↦ -(a • x)) '' t

Tactic:
neg_smul

Goal state after:
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
⊢ p ∈ {p | I.radical.IsMinimalPrime p} ↔ p ∈ {p | I.IsMinimalPrime p}

Tactic:
refine ⟨?_, ?_⟩ <;> rintro ⟨⟨a, ha⟩, b⟩

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
b : ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I.radical ≤ q) y → y ≤ p → p ≤ y
a : p.IsPrime
ha : I.radical ≤ p
⊢ p ∈ {p | I.IsMinimalPrime p}

case refine_2
R : Type u_1
inst✝ : CommSemiring R
I p : Ideal R
b : ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
a : p.IsPrime
ha : I ≤ p
⊢ p ∈ {p | I.radical.IsMinimalPrime p}