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

Goal state before:
pp: α : Type ua
ι : Sort u_1
inst✝ : UniformSpace α
p : ι → Prop
s : ι → SetRel α α
h : (𝓤 α).HasBasis p s
x : α
⊢ (𝓝 x).HasBasis p fun i ↦ ball x (s i)

Tactic:
by
  rw [nhds_eq_comap_uniformity]
  exact h.comap (Prod.mk x)

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 : α → β
x : α
p : Filter ι
⊢ TendstoUniformlyOn F f p {x} ↔ Tendsto (fun n ↦ F n x) p (𝓝 (f x))

Tactic:
tendstoUniformlyOn_iff_tendsto,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
x : α
p : Filter ι
⊢ Tendsto (fun q ↦ (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 {x}) (𝓤 β) ↔ Tendsto (fun n ↦ F n x) p (𝓝 (f x))
Module: Mathlib.Topology.UniformSpace.UniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
X : Type u_5
ιβ : Type u_8
F : X → α → β
f : α → β
l : Filter X
s : Set α
pβ : ιβ → Prop
sβ : ιβ → Set (β × β)
hβ : (𝓤 β).HasBasis pβ sβ
⊢ TendstoUniformlyOn F f l s ↔ ∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ x ∈ s, (f x, F n x) ∈ sβ i

Tactic:
tendstoUniformlyOn_iff_tendsto,

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
X : Type u_5
ιβ : Type u_8
F : X → α → β
f : α → β
l : Filter X
s : Set α
pβ : ιβ → Prop
sβ : ιβ → Set (β × β)
hβ : (𝓤 β).HasBasis pβ sβ
⊢ Tendsto (fun q ↦ (f q.2, F q.1 q.2)) (l ×ˢ 𝓟 s) (𝓤 β) ↔
    ∀ (i : ιβ), pβ i → ∀ᶠ (n : X) in l, ∀ x ∈ s, (f x, F n x) ∈ sβ i
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
x : α
| Filter.comap mk (𝓝 (mk x))

Tactic:
rw [comap_mk_nhds_mk, nhds_eq_comap_uniformity, ← comap_map_mk_uniformity]

Goal state after:
α : Type u
β : Type v
γ : Type w
inst✝² : UniformSpace α
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
x : α
| Filter.comap (Prod.mk x) (Filter.comap (Prod.map mk mk) (map (Prod.map mk mk) (𝓤 α)))
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
S : Set (Set α)
hS : S.Finite
⊢ TotallyBounded (⋃₀ S) ↔ ∀ s ∈ S, TotallyBounded s

Tactic:
by
  rw [sUnion_eq_biUnion, totallyBounded_biUnion hS]

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 : α → β
s : Set α
l : Filter ι
inst✝ : l.IsCountablyGenerated
h : ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun n ↦ F (u n)) f atTop s
⊢ TendstoUniformlyOn F f l s

Tactic:
tendstoUniformlyOn_iff_tendsto,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
l : Filter ι
inst✝ : l.IsCountablyGenerated
h : ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun n ↦ F (u n)) f atTop s
⊢ Tendsto (fun q ↦ (f q.2, F q.1 q.2)) (l ×ˢ 𝓟 s) (𝓤 β)
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
hf : IsUniformInducing f
hsurj : Surjective f
⊢ IsComplete univ ↔ CompleteSpace β

Tactic:
completeSpace_iff_isComplete_univ

Goal state after:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
hf : IsUniformInducing f
hsurj : Surjective f
⊢ IsComplete univ ↔ IsComplete univ
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: case refine_2
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
⊢ ∀ (a : α) (u : Set α),
    a ∈ u → IsOpen[uniformSpace.toTopologicalSpace] u → ∃ v ∈ ⋃ x ∈ s, range fun k ↦ ball x (t k), a ∈ v ∧ v ⊆ u

Tactic:
intro x V hxV hVo

Goal state after:
case refine_2
α : Type u
β : Type v
uniformSpace : UniformSpace α
inst✝¹ : (𝓤 α).IsCountablyGenerated
inst✝ : SeparableSpace α
s : Set α
hsc : s.Countable
hsd : Dense s
t : ℕ → SetRel α α
h_basis : (𝓤 α).HasAntitoneBasis t
ht_mem : ∀ (i : ℕ), t i ∈ (𝓤 α).sets
hto : ∀ (i : ℕ), IsOpen[instTopologicalSpaceProd] (t i)
hts : ∀ (i : ℕ), (t i).IsSymm
x : α
V : Set α
hxV : x ∈ V
hVo : IsOpen[uniformSpace.toTopologicalSpace] V
⊢ ∃ v ∈ ⋃ x ∈ s, range fun k ↦ ball x (t k), x ∈ v ∧ v ⊆ V
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:
rw [isCompact_iff_compactSpace] at hs

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.Algebra.Order.Group.MinMax

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ max c d - max a b ≤ max |a - c| |b - d|

Tactic:
abs_sub_comm a c,

Goal state after:
case refine_2
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c d : α
⊢ max c d - max a b ≤ max |c - a| |b - d|
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
ε : Type u_9
ε' : Type u_10
f : Filter α
g : Filter β
m : δ → γ → ε
n : α → β → δ
m' : α → ε' → ε
n' : β → γ → ε'
h : Filter γ
h_assoc : ∀ (a : α) (b : β) (c : γ), m (n a b) c = m' a (n' b c)
⊢ map₂ m (map₂ n f g) h = map₂ m' f (map₂ n' g h)

Tactic:
rw [← map_prod_eq_map₂ n, ← map_prod_eq_map₂ n', map₂_map_left, map₂_map_right,
    ← map_prod_eq_map₂, ← map_prod_eq_map₂, ← prod_assoc, map_map]
  simp only [h_assoc, Function.comp_def, Equiv.prodAssoc_apply]

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ε : Type u_6
inst✝² : Monoid α
inst✝¹ : Monoid β
inst✝ : MulDistribMulAction α β
x✝ : α
⊢ {x✝ • 1} = 1

Tactic:
rw [smul_one, singleton_one]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : Monoid γ
inst✝ : MulAction γ β
m : α → β
c : γ
f : Filter α
g : Filter β
hc : IsUnit c
⊢ Tendsto (c • m) f (c • g) ↔ Tendsto m f g

Tactic:
rcases hc.exists_left_inv with ⟨d, hd⟩
  refine ⟨fun H ↦ ?_, fun H ↦ tendsto_map.comp H⟩
  simpa [Function.comp_def, smul_smul, hd] using (tendsto_map (f := (d • ·))).comp 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
inst✝¹ : UniformSpace β
inst✝ : UniformSpace γ
p : Filter ι
s : Set β
F : ι → α → β
f : α → β
g : β → γ
hF✝ : ∀ᶠ (i : ι) in p, ∀ (x : α), F i x ∈ s
hf : ∀ (x : α), f x ∈ s
hg : UniformContinuousOn g s
h : TendstoUniformly F f p
s' : Set ι
hs' : s' ∈ p
hs : ∀ y ∈ s', ∀ (x : α), F y x ∈ s
F' : ι → α → β := fun i x ↦ if i ∈ s' then F i x else f x
hF : F =ᶠ[p] F'
⊢ TendstoUniformly F' f p

Tactic:
rwa [tendstoUniformly_congr hF] at h

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

Goal state before:
pp: case inl
G₀ : Type u_4
inst✝⁵ : GroupWithZero G₀
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
s : Set E
⊢ closure[inst✝²] (0 • s) = 0 • closure[inst✝²] s

pp: case inr
G₀ : Type u_4
inst✝⁵ : GroupWithZero G₀
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
c : G₀
s : Set E
hc : c ≠ 0
⊢ closure[inst✝²] (c • s) = c • closure[inst✝²] s

Tactic:
· rcases eq_empty_or_nonempty s with (rfl | hs)
    · simp
    · rw [zero_smul_set hs, zero_smul_set hs.closure]
      exact closure_singleton

Goal state after:
case inr
G₀ : Type u_4
inst✝⁵ : GroupWithZero G₀
E : Type u_5
inst✝⁴ : Zero E
inst✝³ : MulActionWithZero G₀ E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : ContinuousConstSMul G₀ E
c : G₀
s : Set E
hc : c ≠ 0
⊢ closure[inst✝²] (c • s) = c • closure[inst✝²] s
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
x✝ : Continuous[inst✝¹, inst✝] f
⊢ (∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ) ↔
    ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x

Tactic:
constructor <;> intro H

Goal state after:
case mp
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
x✝ : Continuous[inst✝¹, inst✝] f
H : ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ
⊢ ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x

case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
x✝ : Continuous[inst✝¹, inst✝] f
H : ∀ ⦃𝒰 : Ultrafilter X⦄ ⦃y : Y⦄, Tendsto f (↑𝒰) (𝓝 y) → ∃ x, f x = y ∧ ↑𝒰 ≤ 𝓝 x
⊢ ∀ ⦃ℱ : Filter X⦄ ⦃y : Y⦄, MapClusterPt y ℱ f → ∃ x, f x = y ∧ ClusterPt x ℱ
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : SeparatelyContinuousMul M
a b : M
ha : b * a = 1
⊢ Tendsto (fun x ↦ a * x) (cocompact M) (cocompact M)

Tactic:
by
  refine Filter.Tendsto.of_tendsto_comp ?_ (Filter.comap_cocompact_le (continuous_const_mul b))
  convert! Filter.tendsto_id
  ext x
  simp [← mul_assoc, ha]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsProperMap f ↔ Continuous[inst✝¹, inst✝] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})

Tactic:
constructor <;> intro H

Goal state after:
case mp
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : IsProperMap f
⊢ Continuous[inst✝¹, inst✝] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})

case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous[inst✝¹, inst✝] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
⊢ IsProperMap f
Module: Mathlib.Topology.Algebra.Group.Basic

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

Tactic:
refine ⟨?_, Tendsto.mul_const b⟩

Goal state after:
G : Type w
α : Type u
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
b c : G
f : α → G
l : Filter α
⊢ Tendsto (fun x ↦ f x * b) l (𝓝 (c * b)) → Tendsto f l (𝓝 c)
Module: Mathlib.Topology.Algebra.Group.Quotient

Goal state before:
pp: G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
H : Subgroup G
hH : IsCompact ↑H
t : Set G
ht : IsClosed[inst✝²] t
⊢ IsClosed[instTopologicalSpace H] (mk '' t)

Tactic:
rw [← (isQuotientMap_mk H).isClosed_preimage, preimage_image_mk_eq_mul]

Goal state after:
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
H : Subgroup G
hH : IsCompact ↑H
t : Set G
ht : IsClosed[inst✝²] t
⊢ IsClosed[inst✝²] (t * ↑H)
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case right
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
x k : A
hk : φ k = 1
hx : x ∈ (fun h ↦ (fun x ↦ x * k) ⁻¹' U) hk
⊢ φ (x * k) = φ x

Tactic:
map_mul,

Goal state after:
case right
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
x k : A
hk : φ k = 1
hx : x ∈ (fun h ↦ (fun x ↦ x * k) ⁻¹' U) hk
⊢ φ x * φ k = φ x
Module: Mathlib.Topology.Algebra.Group.Basic

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

Tactic:
by
            rw [show (fun x => x₀ * x * x₀⁻¹) = (fun x => x * x₀⁻¹) ∘ fun x => x₀ * x from rfl, ←
              map_map, ← hleft, hright, map_map]
            simp

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
H : (⇑S.subtype ⁻¹' (fun p ↦ p.1 / p.2) '' L ×ˢ K).Finite
x : ↥S
⊢ (x • K ∩ L).Nonempty ↔ ∃ a b, (a, b) ∈ L ×ˢ K ∧ a / b = ↑x

Tactic:
exact Set.smul_inter_nonempty_iff'

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝⁸ : UniformSpace α
inst✝⁷ : Group α
inst✝⁶ : IsUniformGroup α
hom : Type u_3
inst✝⁵ : UniformSpace β
inst✝⁴ : DiscreteTopology β
inst✝³ : Group β
inst✝² : IsUniformGroup β
inst✝¹ : FunLike hom α β
inst✝ : MonoidHomClass hom α β
f : hom
hf : IsOpen[inst✝⁸.toTopologicalSpace] ↑(↑f).ker
⊢ UniformContinuous ⇑f

Tactic:
apply uniformContinuous_of_continuousAt_one

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝⁸ : UniformSpace α
inst✝⁷ : Group α
inst✝⁶ : IsUniformGroup α
hom : Type u_3
inst✝⁵ : UniformSpace β
inst✝⁴ : DiscreteTopology β
inst✝³ : Group β
inst✝² : IsUniformGroup β
inst✝¹ : FunLike hom α β
inst✝ : MonoidHomClass hom α β
f : hom
hf : IsOpen[inst✝⁸.toTopologicalSpace] ↑(↑f).ker
⊢ ContinuousAt (⇑f) 1
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

pp: case inr
K✝ : Type u_1
inst✝⁴ : DivisionRing K✝
inst✝³ : TopologicalSpace K✝
α : Type u_2
inst✝² : Field α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalDivisionRing α
K : Subfield α
x : α
hx : x ∈ closure ↑K
h : x ≠ 0
⊢ x⁻¹ ∈ closure ↑K

Tactic:
· rwa [inv_zero]

Goal state after:
case inr
K✝ : Type u_1
inst✝⁴ : DivisionRing K✝
inst✝³ : TopologicalSpace K✝
α : Type u_2
inst✝² : Field α
inst✝¹ : TopologicalSpace α
inst✝ : IsTopologicalDivisionRing α
K : Subfield α
x : α
hx : x ∈ closure ↑K
h : x ≠ 0
⊢ x⁻¹ ∈ closure ↑K
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: case refine_1
𝕜 : Type u_1
α : Type u_2
inst✝⁵ : Semifield 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
inst✝ : ContinuousMul 𝕜
x : 𝕜
hx : x < 1
⊢ ∀ᶠ (b : 𝕜) in 𝓝 1, x < b⁻¹

pp: case refine_2
𝕜 : Type u_1
α : Type u_2
inst✝⁵ : Semifield 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
inst✝ : ContinuousMul 𝕜
x : 𝕜
hx : x > 1
⊢ ∀ᶠ (b : 𝕜) in 𝓝 1, b⁻¹ < x

Tactic:
· obtain ⟨x', h₀, hxx', h₁⟩ : ∃ x', 0 < x' ∧ x ≤ x' ∧ x' < 1 :=
      ⟨max x (1 / 2), one_half_pos.trans_le (le_max_right _ _), le_max_left _ _,
        max_lt hx one_half_lt_one⟩
    filter_upwards [Ioo_mem_nhds one_pos ((one_lt_inv₀ h₀).2 h₁)] with y hy
    exact hxx'.trans_lt <| lt_inv_of_lt_inv₀ hy.1 hy.2

Goal state after:
case refine_2
𝕜 : Type u_1
α : Type u_2
inst✝⁵ : Semifield 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
inst✝ : ContinuousMul 𝕜
x : 𝕜
hx : x > 1
⊢ ∀ᶠ (b : 𝕜) in 𝓝 1, b⁻¹ < x
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s

Tactic:
by
  rcases (em (IsMax a)).imp_right not_isMax_iff.mp with (ha | ha)
  · use a
    simpa [ha.Ici_eq] using hs
  · rcases (nhdsGE_basis_of_exists_gt ha).mem_iff.mp hs with ⟨b, hab, hbs⟩
    rcases eq_empty_or_nonempty (Ioo a b) with (H | ⟨c, hc⟩)
    · have : Ico a b = Icc a a := by rw [← Icc_union_Ioo_eq_Ico le_rfl hab, H, union_empty]
      exact ⟨a, le_rfl, this ▸ ⟨Ico_mem_nhdsGE hab, hbs⟩⟩
    · exact ⟨c, hc.1.le, Icc_mem_nhdsGE hc.1, (Icc_subset_Ico_right hc.2).trans hbs⟩

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ (∀ᶠ (x_1 : 𝕜) in 𝓝[<] x, toIcoDiv hp a x_1 = toIcoDiv hp a x) ∧
    ∀ᶠ (x_1 : 𝕜) in 𝓝[≥] x, toIcoDiv hp a x_1 = toIcoDiv hp a x

Tactic:
refine ⟨?_, eventuallyEq_toIcoDiv_nhdsGE hp a x⟩

Goal state after:
𝕜 : Type u_1
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsOrderedAddMonoid 𝕜
inst✝² : Archimedean 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
p : 𝕜
hp : 0 < p
a x : 𝕜
hx : ¬x ≡ a [PMOD p]
⊢ ∀ᶠ (x_1 : 𝕜) in 𝓝[<] x, toIcoDiv hp a x_1 = toIcoDiv hp a x
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
⊢ n.gcd m ∣ n

Tactic:
exact n.gcd_dvd_left m

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
⊢ Mono (homologyMap φ) ↔
    ∀ ⦃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

Tactic:
refine ⟨fun h A x₂ hx₂ y₁ fac ↦ ?_, fun h ↦ ?_⟩
  · suffices S₁.liftCycles x₂ hx₂ ≫ S₁.homologyπ = 0 by
      rwa [← S₁.liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements]
    simp only [← cancel_mono (homologyMap φ), zero_comp, assoc,
      homologyπ_naturality, liftCycles_comp_cyclesMap_assoc,
      S₂.liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements]
    exact ⟨A, 𝟙 A, inferInstance, y₁, by simpa using fac⟩
  · rw [Preadditive.mono_iff_cancel_zero]
    intro A γ hγ
    obtain ⟨A₁, π₁, hπ₁, z, hz, fac⟩ := S₁.eq_liftCycles_homologyπ_up_to_refinements γ
    rw [← cancel_epi π₁, fac, comp_zero]
    replace hγ := π₁ ≫= hγ
    simp only [reassoc_of% fac, homologyπ_naturality, liftCycles_comp_cyclesMap_assoc,
      comp_zero, comp_homologyπ_eq_zero_iff_up_to_refinements] at hγ
    obtain ⟨A₂, π₂, hπ₂, y, hy⟩ := hγ
    replace hy := hy =≫ S₂.iCycles
    simp only [assoc, liftCycles_i, toCycles_i] at hy
    obtain ⟨A₃, π₃, hπ₃, x₁, hx₁⟩ :=
      h (π₂ ≫ z) (by rw [assoc, hz, comp_zero]) y (by simpa)
    rw [liftCycles_comp_homologyπ_eq_zero_iff_up_to_refinements]
    exact ⟨A₃, π₃ ≫ π₂, epi_comp _ _, x₁, by simpa⟩

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 : SnakeInput C
⊢ (Iso.refl S.L₂'.op.X₂).hom ≫ S.op.L₁'.g = S.L₂'.op.g ≫ (Iso.refl S.L₂'.op.X₃).hom

Tactic:
by dsimp; simp only [id_comp, comp_id, S.op_δ]

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

Goal state before:
pp: R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
⊢ S.Exact ↔ (ModuleCat.Hom.hom S.f).range = (ModuleCat.Hom.hom S.g).ker

Tactic:
by
  rw [moduleCat_exact_iff_ker_sub_range]
  aesop

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

Goal state before:
pp: J : MultispanShape
a b : J.R
⊢ Subsingleton (right a ⟶ right b)

Tactic:
by
  by_cases h : a = b
  · subst h
    infer_instance
  · have : IsEmpty (right a ⟶ right b) := ⟨by rintro ⟨⟩; simp at h⟩
    infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Equalizer

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
⊢ IsCoreflexivePair (CofreeEqualizer.topMap X) (CofreeEqualizer.bottomMap X)

Tactic:
apply IsCoreflexivePair.mk' _ _ _

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
⊢ T.cofree.obj (T.obj X.A) ⟶ T.cofree.obj X.A

C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
⊢ CofreeEqualizer.topMap X ≫ ?m.21 = 𝟙 (T.cofree.obj X.A)

C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
⊢ CofreeEqualizer.bottomMap X ≫ ?m.21 = 𝟙 (T.cofree.obj X.A)
Module: Mathlib.CategoryTheory.Monad.Equalizer

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
⊢ T.cofree.obj (T.obj X.A) ⟶ T.cofree.obj X.A

Tactic:
apply (cofree T).map (T.ε.app X.A)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
hK : IsLimit K
T : C
f g : T ⟶ K.pt
h : ∀ (a : J.L), f ≫ K.ι a = g ≫ K.ι a
⊢ f = g

Tactic:
apply hK.hom_ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
hK : IsLimit K
T : C
f g : T ⟶ K.pt
h : ∀ (a : J.L), f ≫ K.ι a = g ≫ K.ι a
⊢ ∀ (j : WalkingMulticospan J), f ≫ K.π.app j = g ≫ K.π.app j
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
hK : IsColimit K
T : C
f g : K.pt ⟶ T
h : ∀ (a : J.R), K.π a ≫ f = K.π a ≫ g
⊢ f = g

Tactic:
apply hK.hom_ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
hK : IsColimit K
T : C
f g : K.pt ⟶ T
h : ∀ (a : J.R), K.π a ≫ f = K.π a ≫ g
⊢ ∀ (j : WalkingMultispan J), K.ι.app j ≫ f = K.ι.app j ≫ g
Module: Mathlib.RingTheory.Ideal.Pointwise

Goal state before:
pp: M : Type u_1
N✝ : Type u_2
R✝ : Type u_3
inst✝⁷ : Group M
inst✝⁶ : Semiring R✝
inst✝⁵ : MulSemiringAction M R✝
N : Type u_4
inst✝⁴ : Group N
inst✝³ : MulSemiringAction N R✝
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
x✝ : M
⊢ x✝ ∈ inertia M I ↔ ↑e x✝ ∈ inertia N I

Tactic:
by simp [he]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Semiring R
I : Ideal R
inst✝ : I.IsTwoSided
⊢ colon I Set.univ = I

Tactic:
simp_rw [SetLike.ext_iff, mem_colon, smul_eq_mul]
  exact fun x ↦ ⟨fun h ↦ mul_one x ▸ h 1 trivial, fun h _ _ ↦ I.mul_mem_right _ h⟩

Goal state after:
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' M'' : Submodule R M
x : N
i : M
hi : i ∈ M'
s : ↥p
hs : IsLocalizedModule.mk' f i s = x
j : M
hj : j ∈ M''
t : ↥p
ht : IsLocalizedModule.mk' f j t = x
k : ↥p
hk : k • t • i = k • s • j
⊢ IsLocalizedModule.mk' f ((k * t) • i) (k * s * t) = x

Tactic:
rwa [mul_smul, hk, smul_smul, IsLocalizedModule.mk'_cancel_left]

Goal state after: