mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Support

Goal state before:
pp: case refine_3
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i ↦ mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := {i ∈ hnf.toFinset | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset | x ∉ U j}
z : X
hzn : z ∈ n
hz : ∀ (i : ι), (mulSupport (f i) ∩ n).Nonempty → x ∉ U i → z ∈ (mulTSupport (f i))ᶜ
i : ι
⊢ (i ∈ mulSupport fun i ↦ f i z) → i ∈ ↑hnf.toFinset

Tactic:
hi

Goal state after:
case refine_3
X : Type u_1
R : Type u_8
ι : Type u_9
inst✝¹ : TopologicalSpace X
U : ι → Set X
inst✝ : One R
f : ι → X → R
hlf : LocallyFinite fun i ↦ mulSupport (f i)
hso : ∀ (i : ι), mulTSupport (f i) ⊆ U i
ho : ∀ (i : ι), IsOpen[inst✝¹] (U i)
x : X
n : Set X
hn : n ∈ 𝓝 x
hnf : {i | ((fun i ↦ mulSupport (f i)) i ∩ n).Nonempty}.Finite
is : Finset ι := {i ∈ hnf.toFinset | x ∈ U i}
js : Finset ι := {j ∈ hnf.toFinset | x ∉ U j}
z : X
hzn : z ∈ n
hz : ∀ (i : ι), (mulSupport (f i) ∩ n).Nonempty → x ∉ U i → z ∈ (mulTSupport (f i))ᶜ
i : ι
hi : i ∈ mulSupport fun i ↦ f i z
⊢ i ∈ ↑hnf.toFinset
Module: Mathlib.Topology.UniformSpace.UniformApproximation

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
x : α
hx : x ∈ s
L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∃ F, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u
u₀ : Set (β × β)
hu₀ : u₀ ∈ 𝓤 β
u₁ : Set (β × β)
h₁ : u₁ ∈ 𝓤 β
u₁₀ : u₁ ○ u₁ ⊆ u₀
u₂ : Set (β × β)
h₂ : u₂ ∈ 𝓤 β
hsymm : ∀ {a b : β}, (a, b) ∈ u₂ → (b, a) ∈ u₂
u₂₁ : u₂ ○ u₂ ⊆ u₁
t : Set α
tx : t ∈ 𝓝[s] x
F : α → β
hFc : ContinuousWithinAt F s x
hF : ∀ y ∈ t, (f y, F y) ∈ u₂
⊢ u₀ ∈ map (fun x_1 ↦ (f x_1, f x)) (𝓝[s] x)

Tactic:
have A : ∀ᶠ y in 𝓝[s] x, (f y, F y) ∈ u₂ := Eventually.mono tx hF

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
f : α → β
s : Set α
x : α
hx : x ∈ s
L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∃ F, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u
u₀ : Set (β × β)
hu₀ : u₀ ∈ 𝓤 β
u₁ : Set (β × β)
h₁ : u₁ ∈ 𝓤 β
u₁₀ : u₁ ○ u₁ ⊆ u₀
u₂ : Set (β × β)
h₂ : u₂ ∈ 𝓤 β
hsymm : ∀ {a b : β}, (a, b) ∈ u₂ → (b, a) ∈ u₂
u₂₁ : u₂ ○ u₂ ⊆ u₁
t : Set α
tx : t ∈ 𝓝[s] x
F : α → β
hFc : ContinuousWithinAt F s x
hF : ∀ y ∈ t, (f y, F y) ∈ u₂
A : ∀ᶠ (y : α) in 𝓝[s] x, (f y, F y) ∈ u₂
⊢ u₀ ∈ map (fun x_1 ↦ (f x_1, f x)) (𝓝[s] x)
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 : β → γ
t : Set β
hg : UniformContinuousOn g t
hf : TendstoLocallyUniformly F f p
hfs : ∀ (x : α), f x ∈ t
hFs : ∀ᶠ (n : ι) in p, ∀ (x : α), F n x ∈ t
⊢ TendstoLocallyUniformly (fun x ↦ g ∘ F x) (g ∘ f) p

Tactic:
by
  rw [← tendstoLocallyUniformlyOn_univ] at *
  apply hg.comp_tendstoLocallyUniformlyOn hf <;> simpa [MapsTo]

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

Goal state before:
pp: ι : Type u_1
α : Type u_6
β : Type u_8
γ : Type u_10
uα : UniformSpace α
uβ : UniformSpace β
uγ : UniformSpace γ
F : ι → β → α
u : α → γ
hu : IsUniformInducing u
this : IsUniformInducing (⇑ofFun ∘ (fun x ↦ u ∘ x) ∘ ⇑toFun)
⊢ UniformEquicontinuous F ↔ UniformEquicontinuous ((fun x ↦ u ∘ x) ∘ F)

Tactic:
simp only [uniformEquicontinuous_iff_uniformContinuous, this.uniformContinuous_iff]

Goal state after:
ι : Type u_1
α : Type u_6
β : Type u_8
γ : Type u_10
uα : UniformSpace α
uβ : UniformSpace β
uγ : UniformSpace γ
F : ι → β → α
u : α → γ
hu : IsUniformInducing u
this : IsUniformInducing (⇑ofFun ∘ (fun x ↦ u ∘ x) ∘ ⇑toFun)
⊢ UniformContinuous ((⇑ofFun ∘ (fun x ↦ u ∘ x) ∘ ⇑toFun) ∘ ⇑ofFun ∘ swap F) ↔
    UniformContinuous (⇑ofFun ∘ swap ((fun x ↦ u ∘ x) ∘ F))
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 ι
F : ι → X → α
f : X → α
s : Set X
x : X
z : α
hF : EquicontinuousAt F x
hf : ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[s] x, f x ∈ {y | (y, z) ∈ id i}
hs : ∀ y ∈ s, Tendsto (fun x ↦ F x y) l (𝓝 (f y))
hx : (𝓝[s] x).NeBot
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVs : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
this : ∀ᶠ (y : X) in 𝓝[s] x, y ∈ s ∧ (∀ (i : ι), (F i x, F i y) ∈ V) ∧ (f y, z) ∈ V
y : X
hys : y ∈ s
hFy : ∀ (i : ι), (F i x, F i y) ∈ V
hfy : (f y, z) ∈ V
i : ι
⊢ i ∈ (fun x ↦ F x y) ⁻¹' ball (f y) V → (F i x, z) ∈ id U

Tactic:
hi

Goal state after:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
l : Filter ι
F : ι → X → α
f : X → α
s : Set X
x : X
z : α
hF : EquicontinuousAt F x
hf : ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[s] x, f x ∈ {y | (y, z) ∈ id i}
hs : ∀ y ∈ s, Tendsto (fun x ↦ F x y) l (𝓝 (f y))
hx : (𝓝[s] x).NeBot
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
hVs : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
this : ∀ᶠ (y : X) in 𝓝[s] x, y ∈ s ∧ (∀ (i : ι), (F i x, F i y) ∈ V) ∧ (f y, z) ∈ V
y : X
hys : y ∈ s
hFy : ∀ (i : ι), (F i x, F i y) ∈ V
hfy : (f y, z) ∈ V
i : ι
hi : i ∈ (fun x ↦ F x y) ⁻¹' ball (f y) V
⊢ (F i x, z) ∈ id U
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: case mp
α : Type u_2
inst✝ : DivisionMonoid α
u : (Filter α)ˣ
a b : α
ha : ↑u = pure a
hb : ↑u⁻¹ = pure b
h : a * b = 1
⊢ pure b * pure a = pure 1

Tactic:
← ha,

Goal state after:
case mp
α : Type u_2
inst✝ : DivisionMonoid α
u : (Filter α)ˣ
a b : α
ha : ↑u = pure a
hb : ↑u⁻¹ = pure b
h : a * b = 1
⊢ pure b * ↑u = pure 1
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: G₀ : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
c a b : G₀
h : 0 < c
⊢ (fun x ↦ x * c) ⁻¹' Ico a b = Ico (a / c) (b / c)

Tactic:
simp [← Ici_inter_Iio, h]

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

Goal state before:
pp: G₀ : Type u_2
inst✝² : CommGroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
c a b : G₀
h : 0 < c
⊢ (fun x ↦ c * x) ⁻¹' Ico a b = Ico (a / c) (b / c)

Tactic:
simp [← Ici_inter_Iio, h]

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

Goal state before:
pp: M : Type u
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
hmul : Tendsto (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 1 ×ˢ 𝓝 1) (𝓝 1)
hleft : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x₀ * x) (𝓝 1)
hright : ∀ (x₀ : M), 𝓝 x₀ = map (fun x ↦ x * x₀) (𝓝 1)
x₀ y₀ : M
key : (fun p ↦ x₀ * p.1 * (p.2 * y₀)) = ((fun x ↦ x₀ * x) ∘ fun x ↦ x * y₀) ∘ uncurry fun x1 x2 ↦ x1 * x2
key₂ : ((fun x ↦ x₀ * x) ∘ fun x ↦ y₀ * x) = fun x ↦ x₀ * y₀ * x
⊢ map (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 (x₀, y₀)) = map (uncurry fun x1 x2 ↦ x1 * x2) (𝓝 x₀ ×ˢ 𝓝 y₀)

Tactic:
rw [nhds_prod_eq]

Goal state after:
Module: Mathlib.Topology.Maps.Proper.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 : X → Y
g : Y → Z
hg : IsProperMap g
hf : IsProperMap f
ℱ : Filter X
x : X
hx : ClusterPt x ℱ
hy : ClusterPt (f x) (map f ℱ)
h : MapClusterPt (g (f x)) (map f ℱ) g
⊢ ∃ x_1, (g ∘ f) x_1 = g (f x) ∧ ClusterPt x_1 ℱ

Tactic:
use x, rfl

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
f_cont : Continuous[inst✝¹, inst✝] f
f_inj : Injective f
h : IsClosedMap f
⊢ IsProperMap f

Tactic:
isProperMap_iff_isClosedMap_and_compact_fibers

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
f_cont : Continuous[inst✝¹, inst✝] f
f_inj : Injective f
h : IsClosedMap f
⊢ Continuous[inst✝¹, inst✝] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})
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
inst✝ : T1Space Y
⊢ (Continuous[inst✝², inst✝¹] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})) ↔
    Continuous[inst✝², inst✝¹] f ∧ IsClosedMap f ∧ Tendsto f (cocompact X) cofinite

Tactic:
Tendsto,

Goal state after:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : T1Space Y
⊢ (Continuous[inst✝², inst✝¹] f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})) ↔
    Continuous[inst✝², inst✝¹] f ∧ IsClosedMap f ∧ map f (cocompact X) ≤ cofinite
Module: Mathlib.Topology.Maps.Proper.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : T1Space Y
y : Y
⊢ (IsProperMap fun x ↦ y) ↔ CompactSpace X

Tactic:
isProperMap_iff_isClosedMap_and_compact_fibers

Goal state after:
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
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
H : Type x
inst✝⁴ : Group G
inst✝³ : Monoid H
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace H
inst✝ : ContinuousInv G
f : G →* Hˣ
hf : Continuous[inst✝², inst✝¹] ⇑((Units.coeHom H).comp f)
⊢ Continuous[inst✝², inferInstance] (⇑(Units.embedProduct H) ∘ ⇑f)

Tactic:
refine continuous_prodMk.mpr ⟨hf, ?_⟩

Goal state after:
G : Type w
H : Type x
inst✝⁴ : Group G
inst✝³ : Monoid H
inst✝² : TopologicalSpace G
inst✝¹ : TopologicalSpace H
inst✝ : ContinuousInv G
f : G →* Hˣ
hf : Continuous[inst✝², inst✝¹] ⇑((Units.coeHom H).comp f)
⊢ Continuous[inst✝², instTopologicalSpaceMulOpposite] fun x ↦ op ↑(f x)⁻¹
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: G : Type w
inst✝ : Group G
t₁ t₂ : TopologicalSpace G
h₁ : IsTopologicalGroup G
h₂ : IsTopologicalGroup G
⊢ IsTopologicalGroup G

Tactic:
by
  rw [inf_eq_iInf]
  refine topologicalGroup_iInf fun b => ?_
  cases b <;> assumption

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝¹² : TopologicalSpace α
inst✝¹¹ : AddCommGroup α
inst✝¹⁰ : IsTopologicalAddGroup α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : AddCommGroup β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : AddCommGroup γ
inst✝⁵ : IsTopologicalAddGroup γ
inst✝⁴ : TopologicalSpace δ
inst✝³ : AddCommGroup δ
inst✝² : UniformSpace G
inst✝¹ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
f : δ →+ γ
df : IsDenseInducing ⇑f
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝².toTopologicalSpace] fun p ↦ (φ p.1) p.2
W' : Set G
W'_nhds : W' ∈ 𝓝 0
inst✝ : IsUniformAddGroup G
x₀ : α
y₀ : γ
ee : β × β → α × α := fun u ↦ (e u.1, e u.2)
ff : δ × δ → γ × γ := fun u ↦ (f u.1, f u.2)
lim_φ : Tendsto (fun p ↦ (φ p.1) p.2) (𝓝 (0, 0)) (𝓝 0)
lim_sub_sub :
  Tendsto (fun p ↦ (p.1.2 - p.1.1, p.2.2 - p.2.1)) (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 0 ×ˢ 𝓝 0)
⊢ Tendsto (fun p ↦ (fun p ↦ (φ p.1) p.2) (p.1.2 - p.1.1, p.2.2 - p.2.1))
    (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 0)

Tactic:
rw [← nhds_prod_eq] at lim_sub_sub

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝¹² : TopologicalSpace α
inst✝¹¹ : AddCommGroup α
inst✝¹⁰ : IsTopologicalAddGroup α
inst✝⁹ : TopologicalSpace β
inst✝⁸ : AddCommGroup β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : AddCommGroup γ
inst✝⁵ : IsTopologicalAddGroup γ
inst✝⁴ : TopologicalSpace δ
inst✝³ : AddCommGroup δ
inst✝² : UniformSpace G
inst✝¹ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
f : δ →+ γ
df : IsDenseInducing ⇑f
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝².toTopologicalSpace] fun p ↦ (φ p.1) p.2
W' : Set G
W'_nhds : W' ∈ 𝓝 0
inst✝ : IsUniformAddGroup G
x₀ : α
y₀ : γ
ee : β × β → α × α := fun u ↦ (e u.1, e u.2)
ff : δ × δ → γ × γ := fun u ↦ (f u.1, f u.2)
lim_φ : Tendsto (fun p ↦ (φ p.1) p.2) (𝓝 (0, 0)) (𝓝 0)
lim_sub_sub :
  Tendsto (fun p ↦ (p.1.2 - p.1.1, p.2.2 - p.2.1)) (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 (0, 0))
⊢ Tendsto (fun p ↦ (fun p ↦ (φ p.1) p.2) (p.1.2 - p.1.1, p.2.2 - p.2.1))
    (comap ee (𝓝 (x₀, x₀)) ×ˢ comap ff (𝓝 (y₀, y₀))) (𝓝 0)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : 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))

Tactic:
refine
    ((hasBasis_iInf_principal_finite _).inf (hasBasis_iInf_principal_finite _)).tendstoIxxClass
      fun s _ => ?_

Goal state after:
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
s : Set (Subtype (Membership.mem (Iio a))) × Set (Subtype (Membership.mem (Ioi a)))
x✝ : s.1.Finite ∧ s.2.Finite
⊢ ∀ x ∈ (⋂ i ∈ s.1, Ioi ↑i) ∩ ⋂ i ∈ s.2, Iio ↑i,
    ∀ y ∈ (⋂ i ∈ s.1, Ioi ↑i) ∩ ⋂ i ∈ s.2, Iio ↑i, Icc x y ⊆ (⋂ i ∈ s.1, Ioi ↑i) ∩ ⋂ i ∈ s.2, Iio ↑i
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ (e.trans (PartialEquiv.refl β)).source = e.source

Tactic:
by simp [trans_source]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set β
⊢ (e.trans ((PartialEquiv.refl β).restr s)).source = (e.restr (↑e ⁻¹' s)).source

Tactic:
by simp [trans_source]

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

Goal state before:
pp: case refine_2
α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
c : Set α
h : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
k : Set (Set α)
k_fin : k.Finite
hk : k ⊆ {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
⊢ ∃ f ⊆ c, ∃ x ⊆ c, f.Finite ∧ x.Finite ∧ ⋂₀ k = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ x, Iio a

Tactic:
let kl := {s ∈ k | ∃ a ∈ c, s = Ioi a}

Goal state after:
case refine_2
α : Type u
ts : TopologicalSpace α
inst✝ : Preorder α
c : Set α
h : ts = generateFrom {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
k : Set (Set α)
k_fin : k.Finite
hk : k ⊆ {s | ∃ a ∈ c, s = Ioi a ∨ s = Iio a}
kl : Set (Set α) := {s | s ∈ k ∧ ∃ a ∈ c, s = Ioi a}
⊢ ∃ f ⊆ c, ∃ x ⊆ c, f.Finite ∧ x.Finite ∧ ⋂₀ k = (⋂ a ∈ f, Ioi a) ∩ ⋂ a ∈ x, Iio a
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
ha : ∃ u, a < u
⊢ 𝓝[≥] a = ⨅ u, ⨅ (_ : a < u), 𝓟 (Ico a u)

Tactic:
by
  simp only [nhdsGE_eq_iInf_inf_principal, biInf_inf ha, inf_principal, Iio_inter_Ici]

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

Goal state before:
pp: A : GrpCat
⊢ CartesianMonoidalCategory.lift (↾fun x ↦ x⁻¹)
        (𝟙 (MonTypeEquivalenceMon.inverse.obj ((forget₂ GrpCat MonCat).obj A)).X) ≫
      μ =
    SemiCartesianMonoidalCategory.toUnit (MonTypeEquivalenceMon.inverse.obj ((forget₂ GrpCat MonCat).obj A)).X ≫ η

Tactic:
by
            ext x
            exact inv_mul_cancel (G := A) x

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

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝⁶ : AddCommGroup 𝕜
p : 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝³ : Archimedean 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
x : AddCircle p
inst✝ : DiscreteTopology ↥(zmultiples p)
⊢ ContinuousOn (fun x ↦ ↑((equivIco p a) x)) {↑a}ᶜ

Tactic:
exact continuousOn_of_forall_continuousAt
      (fun _ ↦ continuousAt_subtype_val.comp ∘ continuousAt_equivIco p a)

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

Goal state before:
pp: case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
⊢ ↑(↑(a.natMod ↑n) / ↑n * p) = ↑k

Tactic:
← ha,

Goal state after:
case refine_2
𝕜 : Type u_1
inst✝² : Field 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
hp : Fact (0 < p)
u : AddCircle p
n : ℕ
h : 0 < n
k : 𝕜
a : ℤ
ha : ↑(a / ↑n) * p + (a % ↑n) • p / ↑n = k
h0 : ↑n ≠ 0
⊢ ↑(↑(a.natMod ↑n) / ↑n * p) = ↑(↑(a / ↑n) * p + (a % ↑n) • p / ↑n)
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝⁶ : AddCommGroup 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝³ : Archimedean 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : TopologicalSpace B
f : 𝕜 → B
hf : f a = f (a + p)
hc : ContinuousOn f (Icc a (a + p))
⊢ Continuous[QuotientAddGroup.instTopologicalSpace (zmultiples p), inst✝] (liftIco p a f)

Tactic:
by
  rw [liftIco_eq_lift_Icc hf]
  refine Continuous.comp ?_ (homeoIccQuot p a).continuous_toFun
  exact continuous_coinduced_dom.mpr (continuousOn_iff_continuous_domRestrict.mp hc)

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

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

Tactic:
simpa only [moduleCat_exact_iff_range_eq_ker] using hS

Goal state after:
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 (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₁)

Tactic:
refine ((ConcreteCategory.congr_hom (e.hom.naturality D.δ) x₃).trans ?_).trans
    (ConcreteCategory.congr_hom (e.hom.naturality D.v₂₃.τ₁).symm x₁)

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₃ ≫ (forget C).map D.δ)) x₃ =
    (ConcreteCategory.hom (e.hom.app D.L₂.X₁ ≫ (forget C).map D.v₂₃.τ₁)) x₁
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

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

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

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

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
⊢ CofreeEqualizer.topMap X ≫ T.cofree.map (T.ε.app X.A) = 𝟙 (T.cofree.obj X.A)

C : Type u₁
inst✝ : Category.{v₁, u₁} C
T : Comonad C
X : T.Coalgebra
⊢ CofreeEqualizer.bottomMap X ≫ T.cofree.map (T.ε.app X.A) = 𝟙 (T.cofree.obj X.A)
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ F G : ComposableArrows C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app ⟨i + 1, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
i j : ℕ
hj : i + 0 = j
hj' : j ≤ n
⊢ F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i j ⋯ hj'

Tactic:
simp only [add_zero] at hj

Goal state after:
case zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ F G : ComposableArrows C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app ⟨i + 1, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
i j : ℕ
hj✝ : i + 0 = j
hj' : j ≤ n
hj : i = j
⊢ F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i j ⋯ hj'
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 1
left : F.obj' 0 homMk₁._proof_4 ⟶ G.obj' 0 homMk₁._proof_4
right : F.obj' 1 homMk₁._proof_5 ⟶ G.obj' 1 homMk₁._proof_5
w : F.map' 0 1 homMk₁._proof_4 homMk₁._proof_5 ≫ right = left ≫ G.map' 0 1 homMk₁._proof_4 homMk₁._proof_5
i : ℕ
⊢ ∀ (hi : i < 1),
    (F.map' i (i + 1) ⋯ hi ≫
        match ⟨i + 1, ⋯⟩ with
        | ⟨0, isLt⟩ => left
        | ⟨1, isLt⟩ => right) =
      (match ⟨i, ⋯⟩ with
        | ⟨0, isLt⟩ => left
        | ⟨1, isLt⟩ => right) ≫
        G.map' i (i + 1) ⋯ hi

Tactic:
hi

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ : ComposableArrows C n
F G : ComposableArrows C 1
left : F.obj' 0 homMk₁._proof_4 ⟶ G.obj' 0 homMk₁._proof_4
right : F.obj' 1 homMk₁._proof_5 ⟶ G.obj' 1 homMk₁._proof_5
w : F.map' 0 1 homMk₁._proof_4 homMk₁._proof_5 ≫ right = left ≫ G.map' 0 1 homMk₁._proof_4 homMk₁._proof_5
i : ℕ
hi : i < 1
⊢ (F.map' i (i + 1) ⋯ hi ≫
      match ⟨i + 1, ⋯⟩ with
      | ⟨0, isLt⟩ => left
      | ⟨1, isLt⟩ => right) =
    (match ⟨i, ⋯⟩ with
      | ⟨0, isLt⟩ => left
      | ⟨1, isLt⟩ => right) ≫
      G.map' i (i + 1) ⋯ hi
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : C
⊢ L.map (h.unit.app X) ≫ h.toComonad.δ.app (L.obj X) = L.map (h.unit.app X) ≫ h.toComonad.map (L.map (h.unit.app X))

Tactic:
dsimp
        rw [← L.map_comp, ← Adjunction.unit_naturality, L.map_comp]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A B✝ : C
f g : A ⟶ B✝
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
B : D
⊢ F.map (adj.unit.app (G.obj B)) ≫ F.map (G.map (adj.counit.app B)) = 𝟙 (F.obj (G.obj ((𝟭 D).obj B)))

Tactic:
by
      rw [← F.map_comp, adj.right_triangle_components]
      apply F.map_id

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

Goal state before:
pp: M : Type u_1
R : Type u_3
inst✝² : Group M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
a : M
S T : Ideal R
⊢ a⁻¹ • a • S ≤ a⁻¹ • T ↔ S ≤ a⁻¹ • T

Tactic:
inv_smul_smul

Goal state after:
M : Type u_1
R : Type u_3
inst✝² : Group M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
a : M
S T : Ideal R
⊢ S ≤ a⁻¹ • T ↔ S ≤ a⁻¹ • T
Module: Mathlib.RingTheory.Ideal.Pointwise

Goal state before:
pp: M : Type u_1
R : Type u_3
inst✝² : Group M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
a : M
S T : Ideal R
⊢ a⁻¹ • S ≤ a⁻¹ • a • T ↔ a⁻¹ • S ≤ T

Tactic:
inv_smul_smul

Goal state after:
M : Type u_1
R : Type u_3
inst✝² : Group M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
a : M
S T : Ideal R
⊢ a⁻¹ • S ≤ T ↔ a⁻¹ • S ≤ T
Module: Mathlib.RingTheory.Ideal.Colon

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N✝ N₁ N₂ : Submodule R M
S✝ S₁ S₂ : Set M
N : Submodule R M
S : Set M
r : R
⊢ ∀ {x : R}, x ∈ {r | r • S ⊆ ↑N} → r • x ∈ {r | r • S ⊆ ↑N}

Tactic:
by
    simp only [Set.mem_ofPred_eq, smul_eq_mul, mul_smul, Set.smul_set_subset_iff]
    intro x hx y hy
    exact N.smul_mem _ (hx hy)

Goal state after: