mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
E : L.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
f₁ f₂ : G ⟶ E
Y : D
X : StructuredArrow Y L
eq₁ :
  (((whiskeringLeft C D H).obj L).map f₁.left ≫ CostructuredArrow.hom E).app X.right =
    (CostructuredArrow.hom G).app X.right
⊢ f₁.left.app Y ≫ (E.coneAt Y).π.app X = f₂.left.app Y ≫ (E.coneAt Y).π.app X

Tactic:
have eq₂ := congr_app (CostructuredArrow.w f₂) X.right

Goal state after:
C : Type u_1
D : Type u_2
H : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
E : L.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
f₁ f₂ : G ⟶ E
Y : D
X : StructuredArrow Y L
eq₁ :
  (((whiskeringLeft C D H).obj L).map f₁.left ≫ CostructuredArrow.hom E).app X.right =
    (CostructuredArrow.hom G).app X.right
eq₂ :
  (((whiskeringLeft C D H).obj L).map f₂.left ≫ CostructuredArrow.hom E).app X.right =
    (CostructuredArrow.hom G).app X.right
⊢ f₁.left.app Y ≫ (E.coneAt Y).π.app X = f₂.left.app Y ≫ (E.coneAt Y).π.app X
Module: Mathlib.CategoryTheory.Limits.Shapes.Countable

Goal state before:
pp: J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsFiltered J
j : J
m : ℕ
h : ⋯.choose m = j
⊢ j ≤ sequentialFunctor_obj J (m + 1)

Tactic:
simpa only [h] using! leOfHom (IsFilteredOrEmpty.cocone_objs ((exists_surjective_nat _).choose m)
    (sequentialFunctor_obj J m)).choose_spec.choose

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
x✝² : C
x✝¹ x✝ : F x✝²
h : (sigma F).inj x✝² x✝¹ = (sigma F).inj x✝² x✝
⊢ x✝¹ = x✝

Tactic:
rw [Sigma.ext_iff] at h; simpa using h

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
u v : F.Elementsᵒᵖ
g : u ⟶ v
X : C
x : unop ((CategoryOfElements.π F).op.obj u) ⟶ X
⊢ (ConcreteCategory.hom
          ((((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.flip).map g ≫
                { app := fun X ↦ (coconeπOpCompShrinkYonedaObj F X).ι.app v, naturality := ⋯ }).app
            X)).toFun
      (shrinkYonedaObjObjEquiv.symm x) =
    (ConcreteCategory.hom
          (({ app := fun X ↦ (coconeπOpCompShrinkYonedaObj F X).ι.app u, naturality := ⋯ } ≫
                ((const F.Elementsᵒᵖ).obj F).map g).app
            X)).toFun
      (shrinkYonedaObjObjEquiv.symm x)

Tactic:
simp [← shrinkYonedaObjObjEquiv_symm_comp.{w}]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
inj : CategoryTheory.Injective (ModuleCat.of R M)
X Y : Type v
x✝³ : AddCommGroup X
x✝² : AddCommGroup Y
x✝¹ : Module R X
x✝ : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ⇑f
g : X →ₗ[R] M
⊢ ∃ h, ∀ (x : X), h (f x) = g x

Tactic:
have : CategoryTheory.Mono (ModuleCat.ofHom f) := (ModuleCat.mono_iff_injective _).mpr hf
    obtain ⟨l, h⟩ := inj.factors (ModuleCat.ofHom g) (ModuleCat.ofHom f)
    obtain rfl := ModuleCat.hom_ext_iff.mp h
    exact ⟨l.hom, fun _ => rfl⟩

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: case h
M : Type u_1
inst✝² : AddCommGroup M
R : Type u
inst✝¹ : CommRing R
inst✝ : Module R M
h : ∀ (I : Ideal R), Function.Surjective ⇑(LinearMap.lcomp R M (Submodule.subtype I))
I : Ideal R
g : ↥I →ₗ[R] M
g' : R →ₗ[R] M
hg' : (LinearMap.lcomp R M (Submodule.subtype I)) g' = g
x : R
hx : x ∈ I
⊢ g' x = g ⟨x, hx⟩

Tactic:
simp [← hg']

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
Q : Type v
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
c : Set (ExtensionOf i f)
hchain : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
hnonempty : c.Nonempty
⊢ i.range ≤ (LinearPMap.sSup ((fun x ↦ x.toLinearPMap) '' c) ⋯).domain

Tactic:
by
      refine le_trans hnonempty.some.le <|
        (LinearPMap.le_sSup _ <|
            (Set.mem_image _ _ _).mpr ⟨hnonempty.some, hnonempty.choose_spec, rfl⟩).1

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
Q : Type v
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M : Type u_1
N : Type u_2
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
c : Set (ExtensionOf i f)
hchain : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
hnonempty : c.Nonempty
m : M
⊢ f m = ↑(LinearPMap.sSup ((fun x ↦ x.toLinearPMap) '' c) ⋯) ⟨i m, ⋯⟩

Tactic:
by
      refine Eq.trans (hnonempty.some.is_extension m) ?_
      symm
      generalize_proofs _ _ h1
      exact
        LinearPMap.sSup_apply (IsChain.directedOn <| chain_linearPMap_of_chain_extensionOf hchain)
          ((Set.mem_image _ _ _).mpr ⟨hnonempty.some, hnonempty.choose_spec, rfl⟩) ⟨i m, h1⟩

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
inst✝⁵ : Small.{v, u} R
S : Type u'
inst✝⁴ : Ring S
M : Type v
N : Type v'
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module S N
e₁ : R ≃+* S
e₂ : M ≃ₛₗ[↑e₁] N
inj : Injective R M
I : Ideal S
g : ↥I →ₗ[S] N
I' : Submodule R R := Submodule.map (↑e₁.symm.toSemilinearEquiv) I
e : ↥I' ≃ₛₗ[↑e₁] ↥I := (e₁.symm.toSemilinearEquiv.submoduleMap I).symm
f : ↥I' →ₗ[R] M := ↑e₂.symm ∘ₛₗ g ∘ₛₗ ↑e
x : R
hx : x ∈ I'
⊢ e₁ x ∈ I

Tactic:
simp_all [I']

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
inst✝⁵ : Small.{v, u} R
S : Type u'
inst✝⁴ : Ring S
M : Type v
N : Type v'
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module S N
e₁ : R ≃+* S
e₂ : M ≃ₛₗ[↑e₁] N
inj : Injective R M
I : Ideal S
g : ↥I →ₗ[S] N
I' : Submodule R R := Submodule.map (↑e₁.symm.toSemilinearEquiv) I
e : ↥I' ≃ₛₗ[↑e₁] ↥I := (e₁.symm.toSemilinearEquiv.submoduleMap I).symm
f : ↥I' →ₗ[R] M := ↑e₂.symm ∘ₛₗ g ∘ₛₗ ↑e
hf : ∀ (x : R) (hx : x ∈ I'), f ⟨x, hx⟩ = e₂.symm (g ⟨e₁ x, ⋯⟩)
f' : R →ₗ[R] M
hf' : ∀ (x : R) (mem : x ∈ I'), f' x = f ⟨x, mem⟩
⊢ ∀ (x : S) (mem : x ∈ I), (↑e₂ ∘ₛₗ f' ∘ₛₗ ↑e₁.toSemilinearEquiv.symm) x = g ⟨x, mem⟩

Tactic:
simp_all [I']

Goal state after:
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
⊢ ∀ {n : ℕ}, n ≠ 0 → f n = n.factorization.prod fun p k ↦ f (p ^ k)

Tactic:
by
  apply Nat.recOnPosPrimePosCoprime
  · rintro p k hp - -
    simp [Prime.factorization_pow hp, Finsupp.prod_single_index _, hf]
  · simp
  · rintro -
    rw [factorization_one, hf]
    simp
  · intro a b _ _ hab ha hb hab_pos
    rw [h_mult a b hab, ha (left_ne_zero_of_mul hab_pos), hb (right_ne_zero_of_mul hab_pos),
      factorization_mul_of_coprime hab, ← prod_add_index_of_disjoint]
    exact hab.disjoint_primeFactors

Goal state after:
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
hn : 2 < n
this : Fact (1 < n)
⊢ Even (φ n)

Tactic:
have : NeZero n := NeZero.of_gt hn

Goal state after:
n : ℕ
hn : 2 < n
this✝ : Fact (1 < n)
this : NeZero n
⊢ Even (φ n)
Module: Mathlib.Data.Set.Constructions

Goal state before:
pp: case inter
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T1 T2 : Set α
a✝¹ : finiteInterClosure (insert A S) T1
a✝ : finiteInterClosure (insert A S) T2
h1 : T1 ∈ S ∨ ∃ Q ∈ S, T1 = A ∩ Q
h2 : T2 ∈ S ∨ ∃ Q ∈ S, T2 = A ∩ Q
⊢ T1 ∩ T2 ∈ S ∨ ∃ Q ∈ S, T1 ∩ T2 = A ∩ Q

Tactic:
| @inter T1 T2 _ _ h1 h2 =>

Goal state after:
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p k : ℕ
hp : Prime p
hk : 0 < k
h : p ^ (k - 1) ≤ k * (p ^ (k - 1) * (p - 1))
⊢ p ^ (k * (p ^ (k - 1) * (p - 1)) - p ^ (k - 1)) = p ^ (p ^ (k - 1) * (p * k - k - 1))

Tactic:
Nat.mul_sub,

Goal state after:
p k : ℕ
hp : Prime p
hk : 0 < k
h : p ^ (k - 1) ≤ k * (p ^ (k - 1) * (p - 1))
⊢ p ^ (k * (p ^ (k - 1) * p) - k * (p ^ (k - 1) * 1) - p ^ (k - 1)) =
    p ^ (p ^ (k - 1) * (p * k) - p ^ (k - 1) * k - p ^ (k - 1) * 1)
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
α : Type u_1
inst✝ : TopologicalSpace X
hX : Nonempty X
f : Filter α
g : α → X
h : ¬∃ x, map g f ≤ 𝓝 x
⊢ f.limUnder g = Classical.choice hX

Tactic:
simp_rw [limUnder, lim, Classical.epsilon, Classical.strongIndefiniteDescription, dif_neg h]

Goal state after:
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
f : Filter X
⊢ f ≤ 𝓝 x ↔ ∀ (s : Set X), x ∈ s → IsOpen[inst✝] s → s ∈ f

Tactic:
by simp [nhds_def]

Goal state after:
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
α : Type u_1
x✝ : X
f : α → X
l : Filter α
s : Set α
h : ∀ a ∉ s, f a = x✝
U : Set α
t : Set X
ht : t ∈ 𝓝 x✝
htU : f ⁻¹' t ⊆ U
x : α
hx : x ∈ sᶜ
this : f x ∈ t
⊢ x ∈ U

Tactic:
exact htU this

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a x✝ : α
⊢ (¬∀ (z : ℤ), x✝ - z • p ∉ Set.Ioo a (a + p)) ↔ ∃ i, x✝ - i • p ∈ Set.Ioo a (a + p)

Tactic:
not_forall,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a x✝ : α
⊢ (∃ x, ¬x✝ - x • p ∉ Set.Ioo a (a + p)) ↔ ∃ i, x✝ - i • p ∈ Set.Ioo a (a + p)
Module: Mathlib.Topology.Continuous

Goal state before:
pp: Y : Type u_2
Z : Type u_3
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
α : Type u_4
g : Y → Z
f : α → Y
hg : DenseRange g
hf : DenseRange f
cg : Continuous[inst✝¹, inst✝] g
⊢ Dense (range (g ∘ f))

Tactic:
range_comp

Goal state after:
Y : Type u_2
Z : Type u_3
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
α : Type u_4
g : Y → Z
f : α → Y
hg : DenseRange g
hf : DenseRange f
cg : Continuous[inst✝¹, inst✝] g
⊢ Dense (g '' range f)
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : LinearOrder R
inst✝¹ : IsOrderedAddMonoid R
inst✝ : Archimedean R
p : R
hp : 0 < p
a b : R
⊢ b - ↑(toIocDiv hp a b) * p = toIocMod hp a b

Tactic:
simpa using self_sub_toIocDiv_zsmul hp a b

Goal state after:
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ b - toIocDiv hp a b • p = a + p - Int.fract ((a + p - b) / p) * p

Tactic:
toIocDiv_eq_neg_floor,

Goal state after:
α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
p : α
hp : 0 < p
a b : α
⊢ b - -⌊(a + p - b) / p⌋ • p = a + p - Int.fract ((a + p - b) / p) * p
Module: Mathlib.Topology.Maps.OpenQuotient

Goal state before:
pp: case mpr
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
U : Set C
⊢ (∃ x, IsOpen[inst✝¹] (q ⁻¹' q '' x) ∧ g ⁻¹' q '' x = U) → ∃ t, IsOpen[inst✝¹] t ∧ f ⁻¹' t = p ⁻¹' U

Tactic:
rintro ⟨V, hV, rfl⟩

Goal state after:
case mpr
A : Type u_4
B : Type u_5
C : Type u_6
D : Type u_7
inst✝² : TopologicalSpace A
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace D
f : A → B
g : C → D
p : A → C
q : B → D
h : g ∘ p = q ∘ f
hf : IsInducing f
hp : Surjective p
hq : IsOpenQuotientMap q
hg : Injective g
H : q ⁻¹' q '' range f ⊆ range f
V : Set B
hV : IsOpen[inst✝¹] (q ⁻¹' q '' V)
⊢ ∃ t, IsOpen[inst✝¹] t ∧ f ⁻¹' t = p ⁻¹' g ⁻¹' q '' V
Module: Mathlib.Topology.Separation.SeparatedNhds

Goal state before:
pp: case mpr
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
⊢ SeparatedNhds s t → HasSeparatingCover s t ∧ HasSeparatingCover t s

Tactic:
rintro ⟨U, V, U_open, V_open, h_sub_U, k_sub_V, UV_dis⟩

Goal state after:
case mpr
X : Type u_1
inst✝ : TopologicalSpace X
s t U V : Set X
U_open : IsOpen[inst✝] U
V_open : IsOpen[inst✝] V
h_sub_U : s ⊆ U
k_sub_V : t ⊆ V
UV_dis : Disjoint U V
⊢ HasSeparatingCover s t ∧ HasSeparatingCover t s
Module: Mathlib.Topology.Order

Goal state before:
pp: β : Type u_2
α : Type u_3
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : DiscreteTopology β
f : α → β
h : ∀ (b : β), IsOpen[inst✝²] (f ⁻¹' {b})
s : Set β
x✝ : IsOpen[inst✝¹] s
⊢ IsOpen[inst✝²] (f ⁻¹' s)

Tactic:
by
    rw [← biUnion_of_singleton s, preimage_iUnion₂]
    exact isOpen_biUnion fun _ _ => h _

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
ι : Sort v
t : ι → TopologicalSpace α
s : Set α
⊢ s ∈ {s | IsOpen[iSup t] s} ↔ s ∈ {x | ∀ (i : ι), IsOpen[t i] x}

Tactic:
simp [setOfPred_isOpen_iSup]

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : ∀ (x : X) (l : Filter Y), ClusterPt (f x) l → ClusterPt x (comap f l)
x : X
s : Set X
hs : ClusterPt (f x) (𝓟 (f '' s)ᶜ)
⊢ comap f (𝓟 (f '' s)ᶜ) ≤ 𝓟 sᶜ

Tactic:
simp [subset_preimage_image]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s u : Set α
t v : Set β
a : α
b : β
hu : u ∈ 𝓝[s] a
hv : v ∈ 𝓝[t] b
⊢ u ×ˢ v ∈ 𝓝[s ×ˢ t] (a, b)

Tactic:
rw [nhdsWithin_prod_eq]

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s u : Set α
t v : Set β
a : α
b : β
hu : u ∈ 𝓝[s] a
hv : v ∈ 𝓝[t] b
⊢ u ×ˢ v ∈ 𝓝[s] a ×ˢ 𝓝[t] b
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
T : (i : ι) → TopologicalSpace (A i)
inst✝ : (i : ι) → TopologicalSpace (B i)
f : (i : ι) → A i → B i
hfo : ∀ (i : ι), IsOpenMap (f i)
hsurj : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
x : (i : ι) → A i
⊢ 𝓝 (Pi.map f x) ≤ map (Pi.map f) (𝓝 x)

Tactic:
nhds_pi,

Goal state after:
ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
T : (i : ι) → TopologicalSpace (A i)
inst✝ : (i : ι) → TopologicalSpace (B i)
f : (i : ι) → A i → B i
hfo : ∀ (i : ι), IsOpenMap (f i)
hsurj : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
x : (i : ι) → A i
⊢ (Filter.pi fun i ↦ 𝓝 (Pi.map f x i)) ≤ map (Pi.map f) (𝓝 x)
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
T : (i : ι) → TopologicalSpace (A i)
inst✝ : (i : ι) → TopologicalSpace (B i)
f : (i : ι) → A i → B i
hfo : ∀ (i : ι), IsOpenMap (f i)
hsurj : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
x : (i : ι) → A i
⊢ (Filter.pi fun i ↦ 𝓝 (Pi.map f x i)) ≤ map (Pi.map f) (𝓝 x)

Tactic:
nhds_pi,

Goal state after:
ι : Type u_5
A : ι → Type u_6
B : ι → Type u_7
T : (i : ι) → TopologicalSpace (A i)
inst✝ : (i : ι) → TopologicalSpace (B i)
f : (i : ι) → A i → B i
hfo : ∀ (i : ι), IsOpenMap (f i)
hsurj : ∀ᶠ (i : ι) in cofinite, Surjective (f i)
x : (i : ι) → A i
⊢ (Filter.pi fun i ↦ 𝓝 (Pi.map f x i)) ≤ map (Pi.map f) (Filter.pi fun i ↦ 𝓝 (x i))
Module: Mathlib.Topology.Constructions

Goal state before:
pp: Y : Type v
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
f : Y → (i : ι) → A i
g : (i : ι) → A i
u : Filter Y
⊢ Tendsto f u (𝓝 g) ↔ ∀ (x : ι), Tendsto (fun i ↦ f i x) u (𝓝 (g x))

Tactic:
nhds_pi,

Goal state after:
Y : Type v
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
f : Y → (i : ι) → A i
g : (i : ι) → A i
u : Filter Y
⊢ Tendsto f u (Filter.pi fun i ↦ 𝓝 (g i)) ↔ ∀ (x : ι), Tendsto (fun i ↦ f i x) u (𝓝 (g x))
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
⊢ (∀ x ∈ s, s ∈ 𝓝 x) ↔ ∀ f ∈ s, ∃ I u, (∀ a ∈ I, IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ (↑I).pi u ⊆ s

Tactic:
nhds_pi,

Goal state after:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
⊢ (∀ x ∈ s, s ∈ Filter.pi fun i ↦ 𝓝 (x i)) ↔ ∀ f ∈ s, ∃ I u, (∀ a ∈ I, IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ (↑I).pi u ⊆ s
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : LE α
x : α
z : β
⊢ z ∈ accumulate s x ↔ ∃ y ≤ x, z ∈ s y

Tactic:
accumulate_def,

Goal state after:
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : LE α
x : α
z : β
⊢ z ∈ ⋃ y, ⋃ (_ : y ≤ x), s y ↔ ∃ y ≤ x, z ∈ s y
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
f : ℕ → Set α
⊢ ⇑(partialSups f) = accumulate f

Tactic:
by
  ext n
  simp [partialSups_eq_sup_range, accumulate, Nat.lt_succ_iff]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case refine_1
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
x✝ : a ∈ s
⊢ (∃ I t, (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1) ∧ (↑I).pi t ⊆ s) →
    ∃ I u, (∀ a_2 ∈ I, IsOpen[T a_2] (u a_2) ∧ a a_2 ∈ u a_2) ∧ (↑I).pi u ⊆ s

pp: case refine_2
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
x✝ : a ∈ s
⊢ (∃ I u, (∀ a_1 ∈ I, IsOpen[T a_1] (u a_1) ∧ a a_1 ∈ u a_1) ∧ (↑I).pi u ⊆ s) →
    ∃ I t, (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1) ∧ (↑I).pi t ⊆ s

Tactic:
· rintro ⟨I, t, ⟨h1, h2⟩⟩
    refine ⟨I, fun a => eval a '' (I : Set ι).pi fun a => (h1 a).choose, fun i hi => ?_, ?_⟩
    · simp_rw [eval_image_pi (Finset.mem_coe.mpr hi)
          (pi_nonempty_iff.mpr fun i => ⟨_, fun _ => (h1 i).choose_spec.2.2⟩)]
      exact (h1 i).choose_spec.2
    · exact Subset.trans
        (pi_mono fun i hi => (eval_image_pi_subset hi).trans (h1 i).choose_spec.1) h2

Goal state after:
case refine_2
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
s : Set ((a : ι) → A a)
a : (a : ι) → A a
x✝ : a ∈ s
⊢ (∃ I u, (∀ a_1 ∈ I, IsOpen[T a_1] (u a_1) ∧ a a_1 ∈ u a_1) ∧ (↑I).pi u ⊆ s) →
    ∃ I t, (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ a i ∈ t_1) ∧ (↑I).pi t ⊆ s
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t✝ : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), SeparableSpace (X i)
inst✝ : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), (t x).Countable
htd : ∀ (x : ι), Dense (t x)
this : ∀ (i : ι), Countable ↑(t i)
a✝ : Nontrivial ((i : ι) → X i)
inhabited_h : Inhabited ((i : ι) → X i)
f : (I : Finset ι) × ((i : ↥I) → ↑(t ↑i)) → (i : ι) → X i :=
  fun x i ↦
    match x with
    | ⟨I, g⟩ => if hi : i ∈ I then ↑(g ⟨i, hi⟩) else default i
U : Set ((i : ι) → X i)
hU : IsOpen[Pi.topologicalSpace] U
x✝ : U.Nonempty
g : (i : ι) → X i
hg : g ∈ U
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen[inst✝² a] (u a) ∧ g a ∈ u a
huU : (↑I).pi u ⊆ U
⊢ (U ∩ range f).Nonempty

Tactic:
have : ∀ i : I, ∃ y ∈ t i, y ∈ u i := fun i ↦
      (htd i).exists_mem_open (huo i i.2).1 ⟨_, (huo i i.2).2⟩

Goal state after:
α : Type u
β : Type u_1
t✝ : TopologicalSpace α
B : Set (Set α)
s : Set α
ι : Type u_2
X : ι → Type u_3
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), SeparableSpace (X i)
inst✝ : Countable ι
t : (x : ι) → Set (X x)
htc : ∀ (x : ι), (t x).Countable
htd : ∀ (x : ι), Dense (t x)
this✝ : ∀ (i : ι), Countable ↑(t i)
a✝ : Nontrivial ((i : ι) → X i)
inhabited_h : Inhabited ((i : ι) → X i)
f : (I : Finset ι) × ((i : ↥I) → ↑(t ↑i)) → (i : ι) → X i :=
  fun x i ↦
    match x with
    | ⟨I, g⟩ => if hi : i ∈ I then ↑(g ⟨i, hi⟩) else default i
U : Set ((i : ι) → X i)
hU : IsOpen[Pi.topologicalSpace] U
x✝ : U.Nonempty
g : (i : ι) → X i
hg : g ∈ U
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen[inst✝² a] (u a) ∧ g a ∈ u a
huU : (↑I).pi u ⊆ U
this : ∀ (i : ↥I), ∃ y ∈ t ↑i, y ∈ u ↑i
⊢ (U ∩ range f).Nonempty
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case intro
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst✝ : Finite ι
s : Set ((a : ι) → A a)
val✝ : Fintype ι
⊢ (∀ x ∈ s, s ∈ 𝓝 x) ↔ ∀ f ∈ s, ∃ u, (∀ (a : ι), IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ univ.pi u ⊆ s

Tactic:
nhds_pi,

Goal state after:
case intro
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst✝ : Finite ι
s : Set ((a : ι) → A a)
val✝ : Fintype ι
⊢ (∀ x ∈ s, s ∈ Filter.pi fun i ↦ 𝓝 (x i)) ↔ ∀ f ∈ s, ∃ u, (∀ (a : ι), IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ univ.pi u ⊆ s
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (A i)
a : (i : ι) → A i
⊢ I.pi s ∈ 𝓝 a ↔ ∀ i ∈ I, s i ∈ 𝓝 (a i)

Tactic:
nhds_pi,

Goal state after:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (A i)
a : (i : ι) → A i
⊢ (I.pi s ∈ Filter.pi fun i ↦ 𝓝 (a i)) ↔ ∀ i ∈ I, s i ∈ 𝓝 (a i)
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter γ
m : α → β
n : β → γ
inj₀ : Injective n
large₀ : range n ∈ f
inj₁ : Injective m
large₁ : range m ∈ f.comap inj₀ large₀
inj₂ : optParam (Injective (n ∘ m)) ⋯
⊢ range (n ∘ m) ∈ f

Tactic:
range_comp

Goal state after:
α : Type u
β : Type v
γ : Type u_1
f✝ g : Ultrafilter α
s t : Set α
p q : α → Prop
f : Ultrafilter γ
m : α → β
n : β → γ
inj₀ : Injective n
large₀ : range n ∈ f
inj₁ : Injective m
large₁ : range m ∈ f.comap inj₀ large₀
inj₂ : optParam (Injective (n ∘ m)) ⋯
⊢ n '' range m ∈ f
Module: Mathlib.Topology.Compactness.LocallyCompact

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s t✝ : Set X✝
X : ι → Type u_4
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), LocallyCompactSpace (X i)
inst✝ : Finite ι
t : (i : ι) → X i
n : Set ((i : ι) → X i)
hn : n ∈ 𝓝 t
⊢ ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s

Tactic:
nhds_pi,

Goal state after:
X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s t✝ : Set X✝
X : ι → Type u_4
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), LocallyCompactSpace (X i)
inst✝ : Finite ι
t : (i : ι) → X i
n : Set ((i : ι) → X i)
hn : n ∈ Filter.pi fun i ↦ 𝓝 (t i)
⊢ ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s
Module: Mathlib.Topology.Compactness.LocallyCompact

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s t✝ : Set X✝
X : ι → Type u_4
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), LocallyCompactSpace (X i)
inst✝ : ∀ (i : ι), CompactSpace (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
hn : n ∈ 𝓝 t
⊢ ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s

Tactic:
nhds_pi,

Goal state after:
X✝ : Type u_1
Y : Type u_2
ι : Type u_3
inst✝⁴ : TopologicalSpace X✝
inst✝³ : TopologicalSpace Y
s t✝ : Set X✝
X : ι → Type u_4
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), LocallyCompactSpace (X i)
inst✝ : ∀ (i : ι), CompactSpace (X i)
t : (i : ι) → X i
n : Set ((i : ι) → X i)
hn : n ∈ Filter.pi fun i ↦ 𝓝 (t i)
⊢ ∃ s ∈ 𝓝 t, s ⊆ n ∧ IsCompact s
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
x : X
⊢ ∃ n, K n ∈ 𝓝 x

Tactic:
by
  rcases K.exists_mem x with ⟨n, hn⟩
  exact ⟨n + 1, mem_interior_iff_mem_nhds.mp <| K.subset_interior_succ n hn⟩

Goal state after:
Module: Mathlib.Topology.Compactness.Compact

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsCompact s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst✝] (t i)
hst : s ∩ ⋂ i, t i = ∅
⊢ s ∩ ⋂ i, ⋂ i_1 ∈ i, t i_1 = ∅

Tactic:
← iInter_eq_iInter_finset

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
ι : Type v
hs : IsCompact s
t : ι → Set X
htc : ∀ (i : ι), IsClosed[inst✝] (t i)
hst : s ∩ ⋂ i, t i = ∅
⊢ s ∩ ⋂ i, t i = ∅