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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
f : α → β → γ
uas : Set (UniformSpace α)
ubs : Set (UniformSpace β)
ua : UniformSpace α
ub : UniformSpace β
uc : UniformSpace γ
ha : ua ∈ uas
hb : ub ∈ ubs
hf : UniformContinuous fun p ↦ f p.1 p.2
⊢ UniformContinuous fun p ↦ f p.1 p.2

Tactic:
have ha := uniformContinuous_sInf_dom ha uniformContinuous_id
  have hb := uniformContinuous_sInf_dom hb uniformContinuous_id
  have h_unif_cont_id := @UniformContinuous.prodMap _ _ _ _ (sInf uas) (sInf ubs) ua ub _ _ ha hb
  exact @UniformContinuous.comp _ _ _ (id _) (id _) _ _ _ hf h_unif_cont_id

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
ι : Sort u_1
ι' : Sort u_2
p : ι → Prop
p' : ι' → Prop
s : ι → Set (α × α)
s' : ι' → Set (β × β)
h : (𝓤 α).HasBasis p s
h' : (𝓤 β).HasBasis p' s'
f : α → β
⊢ IsUniformEmbedding f ↔
    Injective f ∧
      (∀ (i : ι'), p' i → ∃ j, p j ∧ ∀ (x y : α), (x, y) ∈ s j → (f x, f y) ∈ s' i) ∧
        ∀ (j : ι), p j → ∃ i, p' i ∧ ∀ (x y : α), (f x, f y) ∈ s' i → (x, y) ∈ s j

Tactic:
rw [isUniformEmbedding_iff, and_comm, h.isUniformInducing_iff h']

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 γ
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)
⊢ e ⁻¹' closure[inst✝².toTopologicalSpace] (e '' s) ⊆ {x | p x}

Tactic:
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
M : Type u_7
R : Type u_8
ι : Type u_9
inst✝² : TopologicalSpace X
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
f : ι → X → M
h✝ : LocallyFinite fun i ↦ support (f i)
s : ι → X → R
i : ι
x : X
h : f i x = 0
⊢ (s i • f i) x = 0

Tactic:
rw [Pi.smul_apply', h, smul_zero]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : UniformSpace γ
G : ι → α → γ
g : α → γ
hF : TendstoLocallyUniformlyOn F f p univ
hG : TendstoLocallyUniformlyOn G g p univ
⊢ TendstoLocallyUniformlyOn (fun n x ↦ (F n x, G n x)) (fun x ↦ (f x, g x)) p univ

Tactic:
exact hF.prodMk hG

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

Goal state before:
pp: case hnhds
α : Type u_4
β : Type u_5
E : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
u' : Set (E × E)
u'_mem : u' ∈ 𝓤 E
u'_symm : ∀ {a b : E}, (a, b) ∈ u' → (b, a) ∈ u'
hu' : SetRel.comp u' u' ⊆ u
x : β
hx : x ∈ k
v : Set α
hv : v ∈ 𝓝[s] q
w : Set β
hw : w ∈ 𝓝[k] x
hvw : v ×ˢ w ⊆ Function.uncurry f ⁻¹' {z | (f q x, z) ∈ u'}
p : α
hp : p ∈ v
y : β
hy : y ∈ w
A : (f q x, f p y) ∈ u'
⊢ (f p y, f q y) ∈ u

Tactic:
have B : (f q x, f q y) ∈ u' := hvw (⟨mem_of_mem_nhdsWithin hq hv, hy⟩ : (q, y) ∈ v ×ˢ w)

Goal state after:
case hnhds
α : Type u_4
β : Type u_5
E : Type u_6
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : UniformSpace E
f : α → β → E
s : Set α
k : Set β
q : α
u : Set (E × E)
hk : IsCompact k
hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)
hq : q ∈ s
hu : u ∈ 𝓤 E
u' : Set (E × E)
u'_mem : u' ∈ 𝓤 E
u'_symm : ∀ {a b : E}, (a, b) ∈ u' → (b, a) ∈ u'
hu' : SetRel.comp u' u' ⊆ u
x : β
hx : x ∈ k
v : Set α
hv : v ∈ 𝓝[s] q
w : Set β
hw : w ∈ 𝓝[k] x
hvw : v ×ˢ w ⊆ Function.uncurry f ⁻¹' {z | (f q x, z) ∈ u'}
p : α
hp : p ∈ v
y : β
hy : y ∈ w
A : (f q x, f p y) ∈ u'
B : (f q x, f q y) ∈ u'
⊢ (f p y, f q y) ∈ u
Module: Mathlib.Topology.UniformSpace.UniformConvergenceTopology

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
inst✝ : UniformSpace β
𝔖 : Set (Set α)
hs : s ∈ 𝔖
V : Set (β × β)
hV : V ∈ 𝓤 β
⊢ UniformOnFun.gen 𝔖 s V ∈ 𝓤 (α →ᵤ[𝔖] β)

Tactic:
rw [UniformOnFun.uniformity_eq]
  apply_rules [mem_iInf_of_mem, mem_principal_self]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ (fun x ↦ x / a) ⁻¹' Ici b = Ici (b * a)

Tactic:
simp [div_eq_mul_inv]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ (fun x ↦ x / a) ⁻¹' Ioi b = Ioi (b * a)

Tactic:
simp [div_eq_mul_inv]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ (fun x ↦ x / a) ⁻¹' Iic b = Iic (b * a)

Tactic:
simp [div_eq_mul_inv]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ (fun x ↦ x / a) ⁻¹' Iio b = Iio (b * a)

Tactic:
simp [div_eq_mul_inv]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ x / a) ⁻¹' Icc b c = Icc (b * a) (c * a)

Tactic:
simp [div_eq_mul_inv]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ x / a) ⁻¹' Ico b c = Ico (b * a) (c * a)

Tactic:
simp [div_eq_mul_inv]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ x / a) ⁻¹' Ioc b c = Ioc (b * a) (c * a)

Tactic:
simp [div_eq_mul_inv]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ x / a) ⁻¹' Ioo b c = Ioo (b * a) (c * a)

Tactic:
simp [div_eq_mul_inv]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ (fun x ↦ x / a) '' Ici b = Ici (b / a)

Tactic:
simp [div_eq_mul_inv]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ (fun x ↦ x / a) '' Iic b = Iic (b / a)

Tactic:
simp [div_eq_mul_inv]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ (fun x ↦ x / a) '' Ioi b = Ioi (b / a)

Tactic:
simp [div_eq_mul_inv]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
⊢ (fun x ↦ x / a) '' Iio b = Iio (b / a)

Tactic:
simp [div_eq_mul_inv]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ x / a) '' Icc b c = Icc (b / a) (c / a)

Tactic:
simp [div_eq_mul_inv]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ x / a) '' Ico b c = Ico (b / a) (c / a)

Tactic:
simp [div_eq_mul_inv]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ x / a) '' Ioc b c = Ioc (b / a) (c / a)

Tactic:
simp [div_eq_mul_inv]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b c : α
⊢ (fun x ↦ x / a) '' Ioo b c = Ioo (b / a) (c / a)

Tactic:
simp [div_eq_mul_inv]

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✝ : MulAction α β
f : Filter β
⊢ map (fun x2 ↦ 1 • x2) f = f

Tactic:
by simp_rw [one_smul, map_id']

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

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
h : c < 0
⊢ (fun x ↦ c * x) ⁻¹' Ioc a b = Ico (b / c) (a / c)

Tactic:
simpa only [mul_comm] using preimage_mul_const_Ioc_of_neg a b h

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

Goal state before:
pp: α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
hb : a ≠ 0
U V : Set α
hU : U ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}
hV : V = (fun x ↦ a * x) ⁻¹' U
⊢ V ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}

Tactic:
obtain ⟨aU, (haU | haU)⟩ := hU

Goal state after:
case inl
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
hb : a ≠ 0
U V : Set α
hV : V = (fun x ↦ a * x) ⁻¹' U
aU : α
haU : U = Ioi aU
⊢ V ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}

case inr
α : Type u_1
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
hb : a ≠ 0
U V : Set α
hV : V = (fun x ↦ a * x) ⁻¹' U
aU : α
haU : U = Iio aU
⊢ V ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: case neg
M : Type u_3
inst✝⁴ : GroupWithZero M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousMul M
inst✝¹ : CompactSpace M
inst✝ : T1Space M
U : Set M
hU : IsOpen[inst✝³] U
h0U : 0 ∈ U
h1U : 1 ∉ U
hW : {0} ∈ 𝓝 0
hW' : univ * {0} ⊆ U
H : ¬∃ x, x ≠ 0 ∧ x ∈ {0}
⊢ IsOpen[inst✝³] {0}

Tactic:
simpa [isOpen_iff_mem_nhds]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
hc : ∀ (i : ι), Continuous[inst✝³, inst✝²] (f i)
hf : LocallyFinite fun i ↦ mulSupport (f i)
⊢ Continuous[inst✝³, inst✝²] fun x ↦ ∏ᶠ (i : ι), f i x

Tactic:
refine continuous_iff_continuousAt.2 fun x => ?_
  rcases finprod_eventually_eq_prod hf x with ⟨s, hs⟩
  refine ContinuousAt.congr ?_ (EventuallyEq.symm hs)
  exact tendsto_finsetProd _ fun i _ => (hc i).continuousAt

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

Goal state before:
pp: M : Type u_1
s : Set M
inst✝³ : Mul M
inst✝² : TopologicalSpace M
inst✝¹ : SeparatelyContinuousMul M
inst✝ : T2Space M
⊢ IsClosed[inst✝²] s.centralizer

Tactic:
rw [centralizer, ofPred_forall]
  refine isClosed_sInter ?_
  rintro - ⟨m, ht, rfl⟩
  refine isClosed_imp (by simp) <| isClosed_eq ?_ ?_
  all_goals fun_prop

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

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Group α
inst✝ : ContinuousConstSMul αᵐᵒᵖ α
s t : Set α
hs : IsOpen[inst✝²] s
⊢ IsOpen[inst✝²] (s * t)

Tactic:
by
  rw [← image_op_smul]
  exact hs.smul_left

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

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : SeparatelyContinuousMul G
s s' : Set G
hs₀ : s ∈ 𝓝 1
h_symm : ∀ x ∈ s, x⁻¹ ∈ s
y : G
hy : y ∈ closure[inst✝²] s'
⊢ (fun x ↦ x * y) '' s ∈ 𝓝 y

Tactic:
simpa using (isOpenMap_mul_right y).image_mem_nhds hs₀

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

Goal state before:
pp: G : Type u_1
inst✝¹ : MulOneClass G
inst✝ : TopologicalSpace G
s : Set G
⊢ s ⊆ s * closure[inst✝] {1}

Tactic:
have : s ⊆ s * ({1} : Set G) := by simp
  exact this.trans (smul_subset_smul_left subset_closure)

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
n : ℕ
⊢ Continuous[inst✝², inst✝²] fun a ↦ a ^ Int.ofNat n

Tactic:
simpa using continuous_pow n

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
x y : G
⊢ Inseparable ((Homeomorph.mulRight y⁻¹) x) ((Homeomorph.mulRight y⁻¹) y) ↔ Inseparable (x / y) 1

Tactic:
simp [div_eq_mul_inv]

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
H : Type u_1
inst✝⁴ : Group H
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup H
F : Type u_2
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
hf : 𝓝 1 = comap (⇑f) (𝓝 1)
x : G
⊢ 𝓝 x = comap (⇑f) (𝓝 (f x))

Tactic:
← nhds_translation_mul_inv,

Goal state after:
G : Type w
inst✝⁷ : TopologicalSpace G
inst✝⁶ : Group G
inst✝⁵ : IsTopologicalGroup G
H : Type u_1
inst✝⁴ : Group H
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup H
F : Type u_2
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
hf : 𝓝 1 = comap (⇑f) (𝓝 1)
x : G
⊢ comap (fun x_1 ↦ x_1 * x⁻¹) (𝓝 1) = comap (⇑f) (𝓝 (f x))
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case e'_3.e'_4
G : Type w
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
c a : G
⊢ {a / c}ᶜ = ⇑(Homeomorph.divRight c) '' {a}ᶜ

Tactic:
simp [div_eq_mul_inv]

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
K V : Set G
hK : IsCompact K
hV : (interior V).Nonempty
⊢ K ⊆ ⋃ i, interior ((fun x ↦ i * x) ⁻¹' V)

Tactic:
obtain ⟨g₀, hg₀⟩ := hV

Goal state after:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K V : Set G
hK : IsCompact K
g₀ : G
hg₀ : g₀ ∈ interior V
⊢ K ⊆ ⋃ i, interior ((fun x ↦ i * x) ⁻¹' V)
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: G✝ : Type u_1
inst✝⁵ : Group G✝
inst✝⁴ : TopologicalSpace G✝
inst✝³ : IsTopologicalGroup G✝
G : Type u_2
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
⊢ G ≃ᵤ Gᵐᵒᵖ

Tactic:
letI : UniformSpace Gᵐᵒᵖ := IsTopologicalGroup.leftUniformSpace Gᵐᵒᵖ

Goal state after:
G✝ : Type u_1
inst✝⁵ : Group G✝
inst✝⁴ : TopologicalSpace G✝
inst✝³ : IsTopologicalGroup G✝
G : Type u_2
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this✝ : UniformSpace G := IsTopologicalGroup.rightUniformSpace G
this : UniformSpace Gᵐᵒᵖ := IsTopologicalGroup.leftUniformSpace Gᵐᵒᵖ
⊢ G ≃ᵤ Gᵐᵒᵖ
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
t : Set α := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
⊢ {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥}.Countable

Tactic:
suffices H : t.Countable by
    have : { x ∈ s | 𝓝[s ∩ Ioi x] x = ⊥ } ⊆ t ∪ {x | IsTop x} := by
      intro x hx
      by_cases h'x : IsTop x
      · simp [h'x]
      · simpa [-sep_and, t, h'x]
    apply Countable.mono this
    simp [H, (subsingleton_isTop α).countable]

Goal state after:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
s : Set α
t : Set α := {x | x ∈ s ∧ 𝓝[s ∩ Ioi x] x = ⊥ ∧ ¬IsTop x}
⊢ t.Countable
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e'✝ e' : PartialEquiv β γ
h : e.target = e'.source
x : α
hx : x ∈ e.source
⊢ (↑e' ∘ ↑e) x ∈ e'.target

Tactic:
by simp [← h, hx]

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

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

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

Tactic:
· use a
    simpa [ha.Ici_eq] using hs

Goal state after:
case inr
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
hs : s ∈ 𝓝[≥] a
ha : ∃ b, a < b
⊢ ∃ b, a ≤ b ∧ Icc a b ∈ 𝓝[≥] a ∧ Icc a b ⊆ s
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
y : 𝕜
hx✝ : ↑y ∈ {x | n • x = 0}
hx : n • ↑y = 0
⊢ ∃ k y_1, ↑y_1 = ↑⟨↑y, hx✝⟩ ∧ n • y_1 = ↑k • p

Tactic:
← mk_nsmul,

Goal state after:
𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
h0 : n ≠ 0
hn : IsSMulRegular 𝕜 n
y : 𝕜
hx✝ : ↑y ∈ {x | n • x = 0}
hx : ↑(n • y) = 0
⊢ ∃ k y_1, ↑y_1 = ↑⟨↑y, hx✝⟩ ∧ n • y_1 = ↑k • p
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial α
s : Set α := {x | ∃ y, x ⋖ y}
y : α → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst✝³] a
t : Set α := {x | x ∈ s ∧ x ∈ a ∧ y x ∉ a ∧ ¬IsBot x}
z : α → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
this : t.PairwiseDisjoint fun x ↦ Ioc (z x) x
x : α
hx : x ∈ t
⊢ Ioc (z x) x = Ioo (z x) (y x)

Tactic:
apply (Ioc_subset_Ioo_right (hy x hx.1).lt).antisymm

Goal state after:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
a✝ : Nontrivial α
s : Set α := ⋯
y : α → α
hy : ∀ x ∈ s, x ⋖ y x
Hy : ∀ (x z : α), x ∈ s → z < y x → z ≤ x
a : Set α
ha : IsOpen[inst✝³] a
t : Set α := ⋯
z : α → α
hz : ∀ x ∈ t, z x < x
h'z : ∀ x ∈ t, Ioc (z x) x ⊆ a
this : t.PairwiseDisjoint fun x ↦ Ioc (z x) x
x : α
hx : x ∈ t
⊢ Ioo (z x) (y x) ⊆ Ioc (z x) x
Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic

Goal state before:
pp: A : Type u
inst✝ : MonObj A
x y z : A
⊢ x * y * z = x * (y * z)

Tactic:
convert! congr_hom (CC := fun X ↦ X) (mul_assoc A) ((x, y), z)

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic

Goal state before:
pp: A : Type u
inst✝¹ : MonObj A
inst✝ : IsCommMonObj A
x y : A
⊢ x * y = y * x

Tactic:
convert! congr_hom (CC := fun X ↦ X) (IsCommMonObj.mul_comm A) (y, x)

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

Goal state before:
pp: case inl
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SeparableSpace α
h : {x | IsTop x} = ∅
s : Set α
s_count : s.Countable
hs : Dense s
this : atTop = generate (Ici '' s)
⊢ (generate (Ici '' s)).IsCountablyGenerated

Tactic:
exact ⟨_, s_count.image _, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_

Goal state before:
pp: A : Type u
inst✝¹ : GrpObj A
inst✝ : IsCommMonObj A
x y : A
⊢ x * y = y * x

Tactic:
convert! congr_hom (CC := fun X ↦ X) (IsCommMonObj.mul_comm A) (y, x)

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

Goal state before:
pp: case 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
u : ↑{u | addOrderOf u = n}
m : ℕ
hmn : m < n
hg : m.gcd n = 1
he : ↑(↑m / ↑n * p) = ↑u
⊢ ∃ a, (fun m ↦ ⟨↑(↑↑m / ↑n * p), ⋯⟩) a = u

Tactic:
exact ⟨⟨m, hmn, hg⟩, Subtype.ext he⟩

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
⊢ (Hom.hom (↟(Finsupp.lsingle PUnit.unit))) ((Finsupp.single PUnit.unit 1) PUnit.unit) = Finsupp.single PUnit.unit 1

Tactic:
Finsupp.lsingle_apply

Goal state after:
R : Type u
inst✝ : CommRing R
⊢ Finsupp.single PUnit.unit ((Finsupp.single PUnit.unit 1) PUnit.unit) = Finsupp.single PUnit.unit 1
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
S : ComposableArrows C 2
⊢ S.map' 0 1 isComplex₂_iff._proof_2 isComplex₂_iff._proof_4 ≫
        S.map' 1 2 isComplex₂_iff._proof_4 isComplex₂_iff._proof_5 =
      0 →
    S.IsComplex

Tactic:
intro h
    refine IsComplex.mk (fun i hi => ?_)
    obtain rfl : i = 0 := by lia
    exact h

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:
by
  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.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ : ComposableArrows C n
F G : ComposableArrows C (n + 1)
α : F.obj' 0 ⋯ ⟶ G.obj' 0 ⋯
β : F.δ₀ ⟶ G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ ≫ app' β 0 ⋯ = α ≫ G.map' 0 1 homMk₁._proof_4 ⋯
i : ℕ
hi : i < n + 1
⊢ (F.map' i (i + 1) ⋯ hi ≫
      match ⟨i + 1, ⋯⟩ with
      | ⟨0, isLt⟩ => α
      | ⟨i.succ, hi⟩ => app' β i ⋯) =
    (match ⟨i, ⋯⟩ with
      | ⟨0, isLt⟩ => α
      | ⟨i.succ, hi⟩ => app' β i ⋯) ≫
      G.map' i (i + 1) ⋯ hi

Tactic:
obtain _ | i := i
      · exact w
      · exact naturality' β i (i + 1)

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} D✝
J : Type u
inst✝³ : Category.{v, u} J
T : Comonad C
D : J ⥤ T.Coalgebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
inst✝² : PreservesLimit (D ⋙ T.forget) T.toFunctor
inst✝¹ : PreservesLimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cone D
j : J
⊢ s.pt.a ≫ T.map ((T.forget.mapCone s).π.app j) = (T.forget.mapCone s).π.app j ≫ (D.obj j).a

Tactic:
exact (s.π.app j).h

Goal state after: