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

Goal state before:
pp: α : Type ua
β : Type ub
inst✝ : UniformSpace α
p : β → Prop
s : β → SetRel α α
h : (𝓤 α).HasBasis p s
t : SetRel α α
⊢ (∃ i, p i ∧ s i ⊆ t) ↔ ∃ i, p i ∧ ∀ (a b : α), (a, b) ∈ s i → (a, b) ∈ t

Tactic:
by simp only [Prod.forall, subset_def]

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 : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : SetRel.comp t t ⊆ u
this :
  ∀ᶠ (x : (ι × ι) × α × α) in (p ×ˢ p) ×ˢ p' ×ˢ p',
    (f ((x.1.1, x.2.1), x.1.2, x.2.2).1.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 ((x.1.1, x.2.1), x.1.2, x.2.2).1.2) ∈
        t ∧
      (f ((x.1.1, x.2.1), x.1.2, x.2.2).2.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 ((x.1.1, x.2.1), x.1.2, x.2.2).2.2) ∈
        t
⊢ ∀ (a b : ι) (b_1 : α), (f b_1, F a b_1) ∈ t → (f b_1, F b b_1) ∈ t → (F a b_1, F b b_1) ∈ u

Tactic:
intro n1

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
p' : Filter α
hF : TendstoUniformlyOnFilter F f p p'
u : Set (β × β)
hu : u ∈ 𝓤 β
t : Set (β × β)
ht : t ∈ 𝓤 β
htsymm : ∀ {a b : β}, (a, b) ∈ t → (b, a) ∈ t
htmem : SetRel.comp t t ⊆ u
this :
  ∀ᶠ (x : (ι × ι) × α × α) in (p ×ˢ p) ×ˢ p' ×ˢ p',
    (f ((x.1.1, x.2.1), x.1.2, x.2.2).1.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).1.1 ((x.1.1, x.2.1), x.1.2, x.2.2).1.2) ∈
        t ∧
      (f ((x.1.1, x.2.1), x.1.2, x.2.2).2.2, F ((x.1.1, x.2.1), x.1.2, x.2.2).2.1 ((x.1.1, x.2.1), x.1.2, x.2.2).2.2) ∈
        t
n1 : ι
⊢ ∀ (b : ι) (b_1 : α), (f b_1, F n1 b_1) ∈ t → (f b_1, F b b_1) ∈ t → (F n1 b_1, F b b_1) ∈ u
Module: Mathlib.Topology.UniformSpace.Separation

Goal state before:
pp: α : Type u
inst✝¹ : UniformSpace α
β : Type u_1
l : Filter β
inst✝ : l.NeBot
f g : β → α
a b : α
ha : Tendsto f l (𝓝 a)
hb : Tendsto g l (𝓝 b)
⊢ Inseparable a b ↔ Tendsto (fun x ↦ (f x, g x)) l (𝓤 α)

Tactic:
refine ⟨fun h ↦ (ha.prodMk_nhds hb).mono_right h.nhds_le_uniformity, fun h ↦ ?_⟩
  rw [inseparable_iff_clusterPt_uniformity]
  exact (ClusterPt.of_le_nhds (ha.prodMk_nhds hb)).mono h

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

Goal state before:
pp: β : Type v
inst✝¹ : UniformSpace β
α : Type u_1
u : UniformSpace α
inst✝ : IndiscreteTopology β
f : α → β
⊢ Tendsto (fun x ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β)

Tactic:
top_uniformity

Goal state after:
β : Type v
inst✝¹ : UniformSpace β
α : Type u_1
u : UniformSpace α
inst✝ : IndiscreteTopology β
f : α → β
⊢ Tendsto (fun x ↦ (f x.1, f x.2)) (𝓤 α) ⊤
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
⊢ comap (fun x ↦ (f x.1, f x.2)) (𝓤 β) = 𝓤 α ↔
    Tendsto (fun x ↦ (f x.1, f x.2)) (𝓤 α) (𝓤 β) ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α

Tactic:
tendsto_iff_comap,

Goal state after:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
⊢ comap (fun x ↦ (f x.1, f x.2)) (𝓤 β) = 𝓤 α ↔
    𝓤 α ≤ comap (fun x ↦ (f x.1, f x.2)) (𝓤 β) ∧ comap (Prod.map f f) (𝓤 β) ≤ 𝓤 α
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: case mpr
α : Type u
uniformSpace : UniformSpace α
g : Filter α
⊢ (∀ (f : Filter α), f.NeBot → f ≤ g → ∃ c ≤ f, Cauchy c) → g.TotallyBounded

Tactic:
· intro H d hd
    contrapose! H with hd_cover
    set f := ⨅ t : Finset α, g ⊓ 𝓟 (d.preimage t)ᶜ
    have hb : Antitone fun t : Finset α ↦ g ⊓ 𝓟 (d.preimage t)ᶜ :=
      fun s t (h : s ⊆ t) => by beta_reduce; gcongr
    have : Filter.NeBot f :=
      (Filter.iInf_neBot_iff_of_directed' <| hb.directed_ge).mpr fun t =>
        Filter.notMem_iff_inf_principal_compl.mp <| hd_cover t t.finite_toSet
    have : f ≤ g := iInf_le_of_le ∅ (by simp)
    refine ⟨f, ‹_›, ‹_›, fun c hcf hc => ?_⟩
    rcases mem_prod_same_iff.1 (hc.2 hd) with ⟨m, hm, hmd⟩
    rcases hc.1.nonempty_of_mem hm with ⟨y, hym⟩
    have : {x | (x, y) ∈ d}ᶜ ∈ c := by
      simpa [SetRel.preimage] using hcf.trans <| (iInf_le _ {y}).trans inf_le_right
    rcases hc.1.nonempty_of_mem (inter_mem hm this) with ⟨z, hzm, hyz⟩
    exact hyz (hmd ⟨hzm, hym⟩)

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 β
F : ι → α → β
f : α → β
p : Filter ι
⊢ TendstoLocallyUniformly F f p ↔ ∀ (x : α), Tendsto (fun y ↦ (f y.2, F y.1 y.2)) (p ×ˢ 𝓝 x) (𝓤 β)

Tactic:
simp [← tendstoLocallyUniformlyOn_univ, isOpen_univ.tendstoLocallyUniformlyOn_iff_forall_tendsto]

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 β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : α → Set α
t : Finset ↑univ
hU : ∀ᶠ (x : ι) in p, ∀ (i : ↥t), ∀ y ∈ U ↑↑i, (f y, F x y) ∈ V
i : ι
hi : ∀ (i_1 : ↥t), ∀ y ∈ U ↑↑i_1, (f y, F i y) ∈ V
x : α
ht : x ∈ ⋃ x ∈ t, U ↑x
⊢ (f x, F i x) ∈ V

Tactic:
simp only [exists_prop, mem_iUnion, SetCoe.exists, exists_and_right] at ht

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : CompactSpace α
h : TendstoLocallyUniformly F f p
V : Set (β × β)
hV : V ∈ 𝓤 β
U : α → Set α
t : Finset ↑univ
hU : ∀ᶠ (x : ι) in p, ∀ (i : ↥t), ∀ y ∈ U ↑↑i, (f y, F x y) ∈ V
i : ι
hi : ∀ (i_1 : ↥t), ∀ y ∈ U ↑↑i_1, (f y, F i y) ∈ V
x : α
ht : ∃ x_1, (∃ (x : x_1 ∈ univ), ⟨x_1, ⋯⟩ ∈ t) ∧ x ∈ U x_1
⊢ (f x, F i x) ∈ V
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝⁴ : CommMonoid α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : MulLeftReflectLE α
inst✝ : ExistsMulOfLE α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
⊢ Icc a b * Icc c d = Icc (a * c) (b * d)

Tactic:
refine (Icc_mul_Icc_subset' _ _ _ _).antisymm fun x ⟨hacx, hxbd⟩ ↦ ?_
  obtain hxbc | hbcx := le_total x (b * c)
  · obtain ⟨y, hy, rfl⟩ := exists_one_le_mul_of_le hacx
    refine ⟨a * y, ⟨le_mul_of_one_le_right' hy, ?_⟩, c, left_mem_Icc.2 hcd, mul_right_comm ..⟩
    rwa [mul_right_comm, mul_le_mul_iff_right] at hxbc
  · obtain ⟨y, hy, rfl⟩ := exists_one_le_mul_of_le hbcx
    refine ⟨b, right_mem_Icc.2 hab, c * y, ⟨le_mul_of_one_le_right' hy, ?_⟩, (mul_assoc ..).symm⟩
    rwa [mul_assoc, mul_le_mul_iff_left] at hxbd

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

Goal state before:
pp: M : Type u_1
X : Type u_2
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace X
inst✝³ : Group M
inst✝² : IsTopologicalGroup M
inst✝¹ : MulAction M X
inst✝ : DiscreteTopology X
h : ∀ (x : X), IsOpen[inst✝⁵] ↑(MulAction.stabilizer M x)
⊢ Continuous[instTopologicalSpaceProd, inst✝⁴] fun p ↦ p.1 • p.2

Tactic:
continuous_prod_of_discrete_right

Goal state after:
M : Type u_1
X : Type u_2
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace X
inst✝³ : Group M
inst✝² : IsTopologicalGroup M
inst✝¹ : MulAction M X
inst✝ : DiscreteTopology X
h : ∀ (x : X), IsOpen[inst✝⁵] ↑(MulAction.stabilizer M x)
⊢ ∀ (b : X), Continuous[inst✝⁵, inst✝⁴] fun x ↦ (x, b).1 • (x, b).2
Module: Mathlib.Topology.ContinuousMap.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
f : α → β
g : C(↑s, β)
hf : ¬Continuous[instTopologicalSpaceSubtype, inst✝] (s.domRestrict f)
⊢ mkD (s.domRestrict f) g = g

Tactic:
exact mkD_of_not_continuous hf

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
hf : IsQuotientMap ⇑f
g : C(X, Z)
h : FactorsThrough ⇑g ⇑f
a✝ : X
⊢ ((hf.lift g h).comp f) a✝ = g a✝

Tactic:
simpa using h (Function.rightInverse_surjInv _ _)

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

Goal state before:
pp: α : Type u_2
G : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : ContinuousConstSMul G α
x : α
inst✝ : IsPretransitive G α
hx : IsClosed[inst✝⁴] {x}
g : G
⊢ IsClosed[inst✝⁴] (HSMul.hSMul g '' {x})

Tactic:
image_smul

Goal state after:
α : Type u_2
G : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : ContinuousConstSMul G α
x : α
inst✝ : IsPretransitive G α
hx : IsClosed[inst✝⁴] {x}
g : G
⊢ IsClosed[inst✝⁴] (g • {x})
Module: Mathlib.Topology.Algebra.ConstMulAction

Goal state before:
pp: α : Type u_2
G : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : ContinuousConstSMul G α
x : α
inst✝ : IsPretransitive G α
hx : IsOpen[inst✝⁴] {x}
g : G
⊢ IsOpen[inst✝⁴] (HSMul.hSMul g '' {x})

Tactic:
image_smul

Goal state after:
α : Type u_2
G : Type u_4
inst✝⁴ : TopologicalSpace α
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : ContinuousConstSMul G α
x : α
inst✝ : IsPretransitive G α
hx : IsOpen[inst✝⁴] {x}
g : G
⊢ IsOpen[inst✝⁴] (g • {x})
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: case mk
ι : Type u_1
α : Type u_2
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → α → M
x : Filter α
a : ι → M
s : Multiset ι
l : List ι
⊢ (∀ i ∈ Quot.mk (⇑(List.isSetoid ι)) l, Tendsto (f i) x (𝓝 (a i))) →
    Tendsto (fun b ↦ (Multiset.map (fun c ↦ f c b) (Quot.mk (⇑(List.isSetoid ι)) l)).prod) x
      (𝓝 (Multiset.map a (Quot.mk (⇑(List.isSetoid ι)) l)).prod)

Tactic:
simpa using tendsto_list_prod l

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

Goal state before:
pp: G : Type w
H : Type x
α : Type u
β : Type v
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : IsTopologicalGroup G
inst✝ : TopologicalSpace α
f : α → G
s✝ : Set α
x : α
s : Subgroup G
g : G
hg : g ∈ closure[inst✝³] ↑s
⊢ g⁻¹ ∈ closure[inst✝³] ↑s

Tactic:
simpa only [← Set.mem_inv, inv_closure, inv_coe_set] using hg

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

Goal state before:
pp: G : Type w
H : Type x
inst✝⁵ : TopologicalSpace G
inst✝⁴ : Group G
inst✝³ : IsTopologicalGroup G
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : IsTopologicalGroup H
f : G →* H
hf : Continuous[inst✝⁵, inst✝¹] ⇑f
hf' : DenseRange ⇑f
s : Subgroup G
hs : Dense ↑s
⊢ Dense ↑(Subgroup.map f s)

Tactic:
exact hf'.dense_image hf 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
S : Subgroup G
hS : IsDiscrete ↑S
⊢ ∃ U ∈ 𝓝 1, U⁻¹ = U ∧ ∀ g ∈ S, ((fun x ↦ g * x) '' U ∩ U).Nonempty → g = 1

Tactic:
by
  obtain ⟨V, hV⟩ := nhds_inter_eq_singleton_of_mem_discrete hS S.one_mem
  obtain ⟨U, hU, -, hUinv, hUV⟩ := exists_closed_nhds_one_inv_eq_mul_subset hV.1
  refine ⟨U, hU, hUinv, fun g hgS ↦ ?_⟩
  rintro ⟨_, ⟨x, hx, rfl⟩, hgx⟩
  refine hV.2.subset ⟨hUV ?_, hgS⟩
  rw [← hUinv] at hx
  exact ⟨_, hgx, _, hx, by simp⟩

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

Goal state before:
pp: β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
⊢ Tendsto (fun gx ↦ gx.1 * gx.2 * gx.1⁻¹) (comap snd (𝓝 1)) (𝓝 1)

Tactic:
tendsto_iff_comap,

Goal state after:
β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
⊢ comap snd (𝓝 1) ≤ comap (fun gx ↦ gx.1 * gx.2 * gx.1⁻¹) (𝓝 1)
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : 0 < C
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 C)
⊢ Tendsto (fun x ↦ f x * g x) l atTop

Tactic:
refine tendsto_atTop_mono' _ ?_ (hf.atTop_mul_const (half_pos hC))
  filter_upwards [hg.eventually (lt_mem_nhds (half_lt_self hC)), hf.eventually_ge_atTop 0] with x hg
    hf using mul_le_mul_of_nonneg_left hg.le hf

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

Goal state before:
pp: case refine_1
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : OrderTopology α
inst✝ : Countable α
f1 : α → Set α := fun a ↦ Ioi a
⊢ {s | ∃ a, s = Ioi a ∨ s = Iio a}.Countable

Tactic:
let f2 : α → Set α := fun a => Iio a

Goal state after:
case refine_1
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst✝² : Preorder α
inst✝¹ : OrderTopology α
inst✝ : Countable α
f1 : α → Set α := fun a ↦ Ioi a
f2 : α → Set α := fun a ↦ Iio a
⊢ {s | ∃ a, s = Ioi a ∨ s = Iio a}.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
y : γ
hy : y ∈ e'.target
⊢ (↑e.symm ∘ ↑e'.symm) y ∈ e.source

Tactic:
by simp [h, hy]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
⊢ TendstoIxxClass Icc (𝓝 a) (𝓝 a)

Tactic:
simp only [nhds_eq_order, iInf_subtype']

Goal state after:
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
⊢ TendstoIxxClass Icc ((⨅ x, 𝓟 (Ioi ↑x)) ⊓ ⨅ x, 𝓟 (Iio ↑x)) ((⨅ x, 𝓟 (Ioi ↑x)) ⊓ ⨅ x, 𝓟 (Iio ↑x))
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case refine_1
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
b : β
hb : b ∈ Iio (f a)
⊢ ⨅ b ∈ Iio a, 𝓟 (Ioi b) ≤ 𝓟 (f ⁻¹' Ioi b)

Tactic:
by_cases! h : ∃ x, ¬(b < f x)

Goal state after:
case pos
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
b : β
hb : b ∈ Iio (f a)
h : ∃ x, ¬b < f x
⊢ ⨅ b ∈ Iio a, 𝓟 (Ioi b) ≤ 𝓟 (f ⁻¹' Ioi b)

case neg
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
b : β
hb : b ∈ Iio (f a)
h : ∀ (x : α), b < f x
⊢ ⨅ b ∈ Iio a, 𝓟 (Ioi b) ≤ 𝓟 (f ⁻¹' Ioi b)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTop α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
⊢ (𝓝 ⊤).HasBasis (fun a ↦ a < ⊤) fun a ↦ Ioi a

Tactic:
by
  have : ∃ x : α, x < ⊤ := (exists_ne ⊤).imp fun x hx => hx.lt_top
  simpa only [Iic_top, nhdsWithin_univ, Ioc_top] using nhdsLE_basis_of_exists_lt this

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

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

Tactic:
rcases exists_Icc_mem_subset_of_mem_nhdsLE (nhdsWithin_le_nhds hs) with
    ⟨b, hba, hb_nhds, hbs⟩
  rcases exists_Icc_mem_subset_of_mem_nhdsGE (nhdsWithin_le_nhds hs) with
    ⟨c, hac, hc_nhds, hcs⟩
  refine ⟨b, c, ⟨hba, hac⟩, ?_⟩
  rw [← Icc_union_Icc_eq_Icc hba hac, ← nhdsLE_sup_nhdsGE]
  exact ⟨union_mem_sup hb_nhds hc_nhds, union_subset hbs hcs⟩

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)
n : ℕ
h : 0 < ↑n
m : ℕ
hn : m < n
h0 : 0 < m
k : ℕ
hk : k • p = ↑m * (p / ↑n)
⊢ False

Tactic:
rw [mul_div, eq_div_iff h.ne', nsmul_eq_mul, mul_right_comm, ← Nat.cast_mul,
    (mul_left_injective₀ hp.out.ne').eq_iff, Nat.cast_inj, mul_comm] at hk

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
k : ℕ
hk : n * k = m
⊢ False
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
q : ℚ
⊢ addOrderOf ↑(↑q * p) = q.den

Tactic:
have : (↑(q.den : ℤ) : 𝕜) ≠ 0 := by
    norm_cast
    exact q.pos.ne.symm

Goal state after:
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
q : ℚ
this : ↑↑q.den ≠ 0
⊢ addOrderOf ↑(↑q * p) = q.den
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
r : R
g : Y ⟶ Z
⊢ (sum f fun f' s ↦ (r • g).sum fun g' t ↦ single (f' ≫ g') (s * t)) =
    r • sum f fun f' s ↦ sum g fun g' t ↦ single (f' ≫ g') (s * t)

Tactic:
Finsupp.smul_sum

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
C : Type u
inst✝ : Category.{v, u} C
X Y Z : Free R C
f : X ⟶ Y
r : R
g : Y ⟶ Z
⊢ (sum f fun f' s ↦ (r • g).sum fun g' t ↦ single (f' ≫ g') (s * t)) =
    sum f fun a b ↦ sum g fun a_1 b_1 ↦ r • single (a ≫ a_1) (b * b_1)
Module: Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X₁ X₂ : C
inst✝¹ : HasBinaryProduct X₁ X₂
inst✝ : PreservesLimit (pair X₁ X₂) (forget C)
x : ToType X₁ × ToType X₂
⊢ (hom prod.fst) ((prodEquiv X₁ X₂).symm x) = x.1

Tactic:
by
  obtain ⟨y, rfl⟩ := (prodEquiv X₁ X₂).surjective x
  simp

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X₁ X₂ : C
inst✝¹ : HasBinaryProduct X₁ X₂
inst✝ : PreservesLimit (pair X₁ X₂) (forget C)
x : ToType X₁ × ToType X₂
⊢ (hom prod.snd) ((prodEquiv X₁ X₂).symm x) = x.2

Tactic:
by
  obtain ⟨y, rfl⟩ := (prodEquiv X₁ X₂).surjective x
  simp

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 ↔ Function.Exact ⇑(ConcreteCategory.hom S.f) ⇑(ConcreteCategory.hom S.g)

Tactic:
moduleCat_exact_iff_range_eq_ker,

Goal state after:
R : Type u
inst✝ : Ring R
S : ShortComplex (ModuleCat R)
⊢ (ModuleCat.Hom.hom S.f).range = (ModuleCat.Hom.hom S.g).ker ↔
    Function.Exact ⇑(ConcreteCategory.hom S.f) ⇑(ConcreteCategory.hom S.g)
Module: Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
D : SnakeInput C
x₃ : ↑((forget₂ C Ab).obj D.L₀.X₃)
x₂ : ↑((forget₂ C Ab).obj D.L₁.X₂)
x₁ : ↑((forget₂ C Ab).obj D.L₂.X₁)
h₂ : (ConcreteCategory.hom ((forget₂ C Ab).map D.L₁.g)) x₂ = (ConcreteCategory.hom ((forget₂ C Ab).map D.v₀₁.τ₃)) x₃
h₁ : (ConcreteCategory.hom ((forget₂ C Ab).map D.L₂.f)) x₁ = (ConcreteCategory.hom ((forget₂ C Ab).map D.v₁₂.τ₂)) x₂
e : forget₂ C Ab ⋙ forget Ab ≅ forget C
⊢ (ConcreteCategory.hom ((forget₂ C Ab).map D.δ)) x₃ = (ConcreteCategory.hom ((forget₂ C Ab).map D.v₂₃.τ₁)) x₁

Tactic:
apply (ofHom_mono_iff_injective (e.hom.app _)).1 inferInstance

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
D : SnakeInput C
x₃ : ↑((forget₂ C Ab).obj D.L₀.X₃)
x₂ : ↑((forget₂ C Ab).obj D.L₁.X₂)
x₁ : ↑((forget₂ C Ab).obj D.L₂.X₁)
h₂ : (ConcreteCategory.hom ((forget₂ C Ab).map D.L₁.g)) x₂ = (ConcreteCategory.hom ((forget₂ C Ab).map D.v₀₁.τ₃)) x₃
h₁ : (ConcreteCategory.hom ((forget₂ C Ab).map D.L₂.f)) x₁ = (ConcreteCategory.hom ((forget₂ C Ab).map D.v₁₂.τ₂)) x₂
e : forget₂ C Ab ⋙ forget Ab ≅ forget C
⊢ (ConcreteCategory.hom (e.hom.app D.L₃.X₁)) ((ConcreteCategory.hom ((forget₂ C Ab).map D.δ)) x₃) =
    (ConcreteCategory.hom (e.hom.app D.L₃.X₁)) ((ConcreteCategory.hom ((forget₂ C Ab).map D.v₂₃.τ₁)) x₁)
Module: Mathlib.Algebra.Category.ModuleCat.Biproducts

Goal state before:
pp: R : Type u
inst✝ : Ring R
J : Type w
f : J → ModuleCat R
s : Cone (Discrete.functor f)
m : s.pt ⟶ { pt := of R ((j : J) → ↑(f j)), π := Discrete.natTrans fun j ↦ ↟(LinearMap.proj j.as) }.pt
w :
  ∀ (j : Discrete J),
    m ≫ { pt := of R ((j : J) → ↑(f j)), π := Discrete.natTrans fun j ↦ ↟(LinearMap.proj j.as) }.π.app j = s.π.app j
⊢ m = lift f s

Tactic:
ext x j

Goal state after:
R : Type u
inst✝ : Ring R
J : Type w
f : J → ModuleCat R
s : Cone (Discrete.functor f)
m : s.pt ⟶ { pt := of R ((j : J) → ↑(f j)), π := Discrete.natTrans fun j ↦ ↟(LinearMap.proj j.as) }.pt
w :
  ∀ (j : Discrete J),
    m ≫ { pt := of R ((j : J) → ↑(f j)), π := Discrete.natTrans fun j ↦ ↟(LinearMap.proj j.as) }.π.app j = s.π.app j
x : ↑s.pt
j : J
⊢ (Hom.hom m) x j = (Hom.hom (lift f s)) x j
Module: Mathlib.Algebra.Category.ModuleCat.Biproducts

Goal state before:
pp: R : Type u
inst✝ : Ring R
J : Type w
f : J → ModuleCat R
s : Cone (Discrete.functor f)
m : s.pt ⟶ { pt := of R ((j : J) → ↑(f j)), π := Discrete.natTrans fun j ↦ ↟(LinearMap.proj j.as) }.pt
w :
  ∀ (j : Discrete J),
    m ≫ { pt := of R ((j : J) → ↑(f j)), π := Discrete.natTrans fun j ↦ ↟(LinearMap.proj j.as) }.π.app j = s.π.app j
⊢ m = lift f s

Tactic:
by
        ext x j
        exact congr_arg (fun g : s.pt ⟶ f j => (g : s.pt → f j) x) (w ⟨j⟩)

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : HasCoreflexiveEqualizers C
inst✝¹ : F.ReflectsIsomorphisms
inst✝ : PreservesLimitOfIsCoreflexivePair F
this : ∀ (X : adj.toComonad.Coalgebra), IsIso ((comparisonAdjunction adj).counit.app X)
⊢ (comparison adj).IsEquivalence

Tactic:
have : ∀ (Y : C), IsIso ((comparisonAdjunction adj).unit.app Y) := by
      intro Y
      rw [comparisonAdjunction_unit_app]
      change IsIso (IsLimit.conePointUniqueUpToIso _ ?_).inv
      · infer_instance
      have : IsCoreflexivePair (G.map (F.map (adj.unit.app Y)))
          (adj.unit.app (G.obj (F.obj Y))) := by
        apply IsCoreflexivePair.mk' (G.map (adj.counit.app _)) _ _
        · rw [← G.map_comp, ← G.map_id]
          exact congr_arg G.map (adj.left_triangle_components Y)
        · rw [← G.map_id]
          simp
      apply @unitEqualizerOfCoreflectsEqualizer _ _ _ _ _ _ _ _ ?_
      apply reflectsLimit_of_reflectsIsomorphisms

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : HasCoreflexiveEqualizers C
inst✝¹ : F.ReflectsIsomorphisms
inst✝ : PreservesLimitOfIsCoreflexivePair F
this✝ : ∀ (X : adj.toComonad.Coalgebra), IsIso ((comparisonAdjunction adj).counit.app X)
this : ∀ (Y : C), IsIso ((comparisonAdjunction adj).unit.app Y)
⊢ (comparison adj).IsEquivalence