mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: case mpr.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h₁ : { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ }.Exact
h₂ : Mono φ.τ₂
⊢ h₁.lift S₂.iCycles ⋯ ≫ S₂.liftCycles φ.τ₂ ⋯ ≫ S₂.iCycles = 𝟙 S₂.cycles ≫ S₂.iCycles

Tactic:
liftCycles_i,

Goal state after:
case mpr.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h₁ : { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ }.Exact
h₂ : Mono φ.τ₂
⊢ h₁.lift S₂.iCycles ⋯ ≫ φ.τ₂ = 𝟙 S₂.cycles ≫ S₂.iCycles
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : F.Faithful
S : ShortComplex C
hS : kernel.ι (F.map S.g) ≫ cokernel.π (F.map S.f) = 0
k : F.obj (Limits.kernel S.g) ⟶ Limits.kernel (F.map S.g)
hk : k ≫ kernel.ι (F.map S.g) = F.map (kernel.ι S.g)
l : cokernel (F.map S.f) ⟶ F.obj (cokernel S.f)
hl : cokernel.π (F.map S.f) ≫ l = F.map (cokernel.π S.f)
⊢ F.map (kernel.ι S.g) ≫ F.map (cokernel.π S.f) = 0

Tactic:
← hl,

Goal state after:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : F.Faithful
S : ShortComplex C
hS : kernel.ι (F.map S.g) ≫ cokernel.π (F.map S.f) = 0
k : F.obj (Limits.kernel S.g) ⟶ Limits.kernel (F.map S.g)
hk : k ≫ kernel.ι (F.map S.g) = F.map (kernel.ι S.g)
l : cokernel (F.map S.f) ⟶ F.obj (cokernel S.f)
hl : cokernel.π (F.map S.f) ≫ l = F.map (cokernel.π S.f)
⊢ F.map (kernel.ι S.g) ≫ cokernel.π (F.map S.f) ≫ l = 0
Module: Mathlib.CategoryTheory.Abelian.FunctorCategory

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
| α.app X

Tactic:
← coimage_image_factorisation α

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
| (coimage.π α ≫ coimageImageComparison α ≫ image.ι α).app X
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
Y₁ Y₂ : D
e : Y₁ ≅ Y₂
inst✝ : L.HasPointwiseLeftKanExtensionAt F Y₁
⊢ L.HasPointwiseLeftKanExtensionAt F Y₂

Tactic:
change HasColimit ((CostructuredArrow.mapIso e.symm).functor ⋙ CostructuredArrow.proj L Y₁ ⋙ F)

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
Y₁ Y₂ : D
e : Y₁ ≅ Y₂
inst✝ : L.HasPointwiseLeftKanExtensionAt F Y₁
⊢ HasColimit ((CostructuredArrow.mapIso e.symm).functor ⋙ CostructuredArrow.proj L Y₁ ⋙ F)
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X Y : C
f : X ⟶ Y
p : YonedaCollection F Y
⊢ op (CostructuredArrow.mk (yoneda.map f ≫ p.fst)) = op (CostructuredArrow.mk (map₂ F f p).fst)

Tactic:
by rw [YonedaCollection.map₂_fst f]

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsFiltered J
d : J
⊢ IsConnected (StructuredArrow d (sequentialFunctor J))

Tactic:
obtain ⟨n, (g : d ≤ (sequentialFunctor J).obj n)⟩ := sequentialFunctor_final_aux J d

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
J : Type u_2
inst✝² : Countable J
inst✝¹ : Preorder J
inst✝ : IsFiltered J
d : J
n : ℕ
g : d ≤ (sequentialFunctor J).obj n
⊢ IsConnected (StructuredArrow d (sequentialFunctor J))
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u_1
inst✝³ : Category.{v_1, u_1} J
D : Type u_2
inst✝² : Category.{v_2, u_2} D
e : C ≌ D
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
this : HasLimitsOfShape J D
x✝² : Type
x✝¹ : SmallCategory x✝²
x✝ : FinCategory x✝²
K : x✝² ⥤ J ⥤ D
⊢ PreservesColimit K lim

Tactic:
refine preservesColimit_of_natIso K (?_ : e.congrRight.inverse ⋙ lim ⋙ e.functor ≅ lim)

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
J : Type u_1
inst✝³ : Category.{v_1, u_1} J
D : Type u_2
inst✝² : Category.{v_2, u_2} D
e : C ≌ D
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasExactLimitsOfShape J C
this : HasLimitsOfShape J D
x✝² : Type
x✝¹ : SmallCategory x✝²
x✝ : FinCategory x✝²
K : x✝² ⥤ J ⥤ D
⊢ e.congrRight.inverse ⋙ lim ⋙ e.functor ≅ lim
Module: Mathlib.CategoryTheory.Abelian.Transfer

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasFiniteProducts C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝¹ : G.PreservesZeroMorphisms
inst✝ : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
this✝¹ : HasKernels C
this✝ : HasCokernels C
X Y : C
f : X ⟶ Y
arrowIso : Arrow.mk (G.map (F.map f)) ≅ Arrow.mk f := ((Functor.mapArrowFunctor C C).mapIso i).app (Arrow.mk f)
this : PreservesColimits G
iso : Arrow.mk (G.map (Abelian.coimageImageComparison (F.map f))) ≅ Arrow.mk (Abelian.coimageImageComparison f) :=
  Abelian.PreservesCoimageImageComparison.iso G (F.map f) ≪≫ Abelian.coimageImageComparisonFunctor.mapIso arrowIso
⊢ IsIso (Abelian.coimageImageComparison f)

Tactic:
Arrow.isIso_iff_isIso_of_isIso iso.inv

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasFiniteProducts C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝¹ : G.PreservesZeroMorphisms
inst✝ : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
this✝¹ : HasKernels C
this✝ : HasCokernels C
X Y : C
f : X ⟶ Y
arrowIso : Arrow.mk (G.map (F.map f)) ≅ Arrow.mk f := ((Functor.mapArrowFunctor C C).mapIso i).app (Arrow.mk f)
this : PreservesColimits G
iso : Arrow.mk (G.map (Abelian.coimageImageComparison (F.map f))) ≅ Arrow.mk (Abelian.coimageImageComparison f) :=
  Abelian.PreservesCoimageImageComparison.iso G (F.map f) ≪≫ Abelian.coimageImageComparisonFunctor.mapIso arrowIso
⊢ IsIso (G.map (Abelian.coimageImageComparison (F.map f)))
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
j₁ j₂ : J
t : Trident f
⊢ t.π.app one = t.ι ≫ f j₂

Tactic:
t.app_zero

Goal state after:
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
j₁ j₂ : J
t : Trident f
⊢ t.π.app one = t.π.app one
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C
h : IsSeparator G
α : C ≌ D
⊢ IsSeparator (α.functor.obj G)

Tactic:
by
  simpa using! ObjectProperty.IsSeparating.of_equivalence h α

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Zero

Goal state before:
pp: case refine_1
G : GrpCat
inst✝ : Subsingleton ↑G
X : GrpCat
f : G ⟶ X
x : ↑G
this : x = 1
⊢ (Hom.hom f) x = (Hom.hom default) x

Tactic:
rw [this, map_one, map_one]

Goal state after:
Module: Mathlib.Algebra.Category.Grp.Zero

Goal state before:
pp: case refine_1
G : CommGrpCat
inst✝ : Subsingleton ↑G
X : CommGrpCat
f : G ⟶ X
x : ↑G
this : x = 1
⊢ (Hom.hom f) x = (Hom.hom default) x

Tactic:
rw [this, map_one, map_one]

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
this : Mono (ModuleCat.ofHom f)
⊢ ∃ h, ∀ (x : X), h (f x) = g x

Tactic:
obtain ⟨l, h⟩ := inj.factors (ModuleCat.ofHom g) (ModuleCat.ofHom f)

Goal state after:
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
this : Mono (ModuleCat.ofHom f)
l : ModuleCat.of R Y ⟶ ModuleCat.of R M
h : ModuleCat.ofHom f ≫ l = ModuleCat.ofHom g
⊢ ∃ h, ∀ (x : X), h (f x) = g x
Module: Mathlib.Algebra.Category.Grp.Injective

Goal state before:
pp: case inl
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
g : ↥(ℤ ∙ 0) →ₗ[ℤ] A
n : ℤ
hn : n ∈ ℤ ∙ 0
⊢ 0 n = g ⟨n, hn⟩

Tactic:
Submodule.span_zero_singleton

Goal state after:
case inl
A : Type u
inst✝¹ : AddCommGroup A
inst✝ : DivisibleBy A ℤ
g : ↥(ℤ ∙ 0) →ₗ[ℤ] A
n : ℤ
hn✝ : n ∈ ℤ ∙ 0
hn : n ∈ ⊥
⊢ 0 n = g ⟨n, hn✝⟩
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: n : ℤ
⊢ (-1) ^ (-n) = (-1) ^ n

Tactic:
simp only [zpow_neg, ← inv_zpow, inv_neg, inv_one]

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

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
⊢ count p n = #({x ∈ range n | p x})

Tactic:
rw [count, List.countP_eq_length_filter]
  rfl

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
inst✝ : Fact (Function.Injective ⇑i)
h : Baer R Q
y : N
x : ↥(extensionOfMax i f).domain
x' : ↥(extensionOfMaxAdjoin i f h y).domain
EQ : ↑x = ↑x'
⊢ ↑x' = ↑x + 0 • y

Tactic:
simp [EQ]

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

Goal state before:
pp: case zero
a k n : ℕ
a_ne_zero : a ≠ 0
⊢ #({x ∈ Ico k (k + (n % a + a * 0)) | a.Coprime x}) ≤ φ a * (0 + 1)

Tactic:
rw [← filter_coprime_Ico_eq_totient a k]

Goal state after:
case zero
a k n : ℕ
a_ne_zero : a ≠ 0
⊢ #({x ∈ Ico k (k + (n % a + a * 0)) | a.Coprime x}) ≤ #({x ∈ Ico k (k + a) | a.Coprime x}) * (0 + 1)
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: case inr.hac
c d d' : ℕ
hn : 2 * (c ^ 2 + d + 1) ≤ 2 * (c ^ 2 + d + 1) + d'
c0 : c > 0
⊢ 1 ≤ (c ^ 2)!

Tactic:
exact Nat.one_le_of_lt (Nat.factorial_pos _)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
m : Filter β
p : α × β → Prop
⊢ (∀ᶠ (x : α × β) in l.curry m, ¬p x) ↔ ∀ᶠ (x : α) in l, ¬¬∀ᶠ (x_1 : β) in m, ¬p (x, x_1)

Tactic:
not_not,

Goal state after:
α : Type u_1
β : Type u_2
l : Filter α
m : Filter β
p : α × β → Prop
⊢ (∀ᶠ (x : α × β) in l.curry m, ¬p x) ↔ ∀ᶠ (x : α) in l, ∀ᶠ (x_1 : β) in m, ¬p (x, x_1)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ a.gcd b * (a * b) / ((∏ p ∈ (a.gcd b).primeFactors, p) * ∏ p ∈ (a * b).primeFactors, p) *
      ((∏ p ∈ (a.gcd b).primeFactors, (p - 1)) * ∏ p ∈ (a * b).primeFactors, (p - 1)) =
    ((a / ∏ p ∈ a.primeFactors, p) * ∏ p ∈ a.primeFactors, (p - 1)) *
        ((b / ∏ p ∈ b.primeFactors, p) * ∏ p ∈ b.primeFactors, (p - 1)) *
      a.gcd b

pp: case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p ∈ (a.gcd b).primeFactors, p ∣ a.gcd b

pp: case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p ∈ (a * b).primeFactors, p ∣ a * b

Tactic:
shuffle

Goal state after:
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ a.gcd b * (a * b) / ((∏ p ∈ (a.gcd b).primeFactors, p) * ∏ p ∈ (a * b).primeFactors, p) *
      ((∏ p ∈ (a.gcd b).primeFactors, (p - 1)) * ∏ p ∈ (a * b).primeFactors, (p - 1)) =
    a * b / ((∏ p ∈ a.primeFactors, p) * ∏ p ∈ b.primeFactors, p) *
        ((∏ p ∈ a.primeFactors, (p - 1)) * ∏ p ∈ b.primeFactors, (p - 1)) *
      a.gcd b

case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p ∈ a.primeFactors, p ∣ a

case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p ∈ b.primeFactors, p ∣ b

case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p ∈ (a.gcd b).primeFactors, p ∣ a.gcd b

case a
a b : ℕ
shuffle : ∀ (a1 a2 b1 b2 c1 c2 : ℕ), b1 ∣ a1 → b2 ∣ a2 → a1 / b1 * c1 * (a2 / b2 * c2) = a1 * a2 / (b1 * b2) * (c1 * c2)
⊢ ∏ p ∈ (a * b).primeFactors, p ∣ a * b
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p n : ℕ
hp : Prime p
h : ¬p ∣ n
⊢ φ (p * n) = (p - 1) * φ n

Tactic:
totient_mul _,

Goal state after:
p n : ℕ
hp : Prime p
h : ¬p ∣ n
⊢ φ p * φ n = (p - 1) * φ n

p n : ℕ
hp : Prime p
h : ¬p ∣ n
⊢ p.Coprime n
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 b : α
⊢ toIocDiv hp a b • p + toIocMod hp a b = b

Tactic:
by
  rw [add_comm, toIocMod_add_toIocDiv_zsmul]

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 b : α
⊢ toIcoDiv hp (a + p) b = toIcoDiv hp a b - 1

Tactic:
simpa only [one_zsmul] using toIcoDiv_add_zsmul' hp a b 1

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
T : Set (Set X)
empty_mem : ∅ ∈ T
sInter_mem : ∀ A ⊆ T, ⋂₀ A ∈ T
union_mem : ∀ A ∈ T, ∀ B ∈ T, A ∪ B ∈ T
s : Set (Set X)
hs : ∀ t ∈ s, tᶜ ∈ T
⊢ (⋃₀ s)ᶜ ∈ T

Tactic:
simp only [Set.compl_sUnion]

Goal state after:
X : Type u
T : Set (Set X)
empty_mem : ∅ ∈ T
sInter_mem : ∀ A ⊆ T, ⋂₀ A ∈ T
union_mem : ∀ A ∈ T, ∀ B ∈ T, A ∪ B ∈ T
s : Set (Set X)
hs : ∀ t ∈ s, tᶜ ∈ T
⊢ ⋂₀ (compl '' s) ∈ T
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
g : Set α → Filter β
m : γ → β
l : Filter γ
⊢ Tendsto m l (f.lift g) ↔ ∀ s ∈ f, Tendsto m l (g s)

Tactic:
simp only [Filter.lift, tendsto_iInf]

Goal state after:
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : Dense s
ht : IsOpen[inst✝] t
⊢ t = t ∩ univ

Tactic:
inter_univ

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : Dense s
ht : IsOpen[inst✝] t
⊢ t = t
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ frontier s = (interior s)ᶜ ∩ (interior sᶜ)ᶜ

Tactic:
rw [← frontier_compl, ← closure_compl, ← sdiff_eq, closure_sdiff_interior]

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ ClusterPt x (F.lift' closure[inst✝]) ↔ ClusterPt x F

Tactic:
by
  simp [clusterPt_iff_lift'_closure, lift'_lift'_assoc (monotone_closure X) (monotone_closure X)]

Goal state after:
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
m : ℤ
⊢ toIcoMod hp a (b + ↑m * p) = toIcoMod hp a b

Tactic:
simpa using toIcoMod_add_zsmul hp a b m

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
⊢ SeparatedNhds s t ↔ Disjoint (𝓝ˢ s) (𝓝ˢ t)

Tactic:
by
  simp only [(hasBasis_nhdsSet s).disjoint_iff (hasBasis_nhdsSet t), SeparatedNhds, ←
    exists_and_left, and_assoc, and_comm, and_left_comm]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace α
b : Set (Set β)
f : α → β
h : ∀ a ∈ b, IsOpen[t] (f ⁻¹' a)
⊢ t ≤ induced f (generateFrom b)

Tactic:
induced_generateFrom_eq

Goal state after:
α : Type u_1
β : Type u_2
t : TopologicalSpace α
b : Set (Set β)
f : α → β
h : ∀ a ∈ b, IsOpen[t] (f ⁻¹' a)
⊢ t ≤ generateFrom (preimage f '' b)
Module: Mathlib.Topology.WithTopology

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
s : Set (WithTopology X t)
⊢ IsClosed s ↔ IsClosed[t] (toTopology t ⁻¹' s)

Tactic:
by
  simp [← isOpen_compl_iff, isOpen_iff]

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
F : Filter X
f_closed : IsClosedMap f
f_cont : Continuous[inst✝¹, inst✝] f
y : Y
⊢ ClusterPt y (map f F) ↔ (F.lift' closure[inst✝¹] ⊓ 𝓟 (f ⁻¹' {y})).NeBot

Tactic:
clusterPt_iff_lift'_closure',

Goal state after:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
F : Filter X
f_closed : IsClosedMap f
f_cont : Continuous[inst✝¹, inst✝] f
y : Y
⊢ ((map f F).lift' closure[inst✝] ⊓ pure y).NeBot ↔ (F.lift' closure[inst✝¹] ⊓ 𝓟 (f ⁻¹' {y})).NeBot
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: ι : Type u_5
α : ι → Type u_6
inst✝ : (i : ι) → TopologicalSpace (α i)
s : (i : ι) → Set (α i)
I : Set ι
hs : ∀ i ∈ I, Dense (s i)
⊢ Dense (I.pi s)

Tactic:
simp only [dense_iff_closure_eq, closure_pi_set, pi_congr rfl fun i hi => (hs i hi).closure_eq,
    pi_univ]

Goal state after:
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : IsOpenMap f
hg : IsOpenMap g
⊢ IsOpenMap (Prod.map f g)

Tactic:
rw [isOpenMap_iff_nhds_le]

Goal state after:
X : Type u
Y : Type v
W : Type u_1
Z : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace W
f : X → Y
g : Z → W
hf : IsOpenMap f
hg : IsOpenMap g
⊢ ∀ (x : X × Z), 𝓝 (Prod.map f g x) ≤ map (Prod.map f g) (𝓝 x)
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
f : X → Bool
b : Bool
⊢ Continuous[inst✝, _] f ↔ IsClopen (f ⁻¹' {b})

Tactic:
rw [continuous_discrete_rng, Bool.forall_bool' b, IsClopen, ← isOpen_compl_iff, ← preimage_compl,
    Bool.compl_singleton, and_comm]

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : SeparableSpace β
f : α → β
h : IsOpenMap f
h' : IsInducing f
⊢ SeparableSpace α

Tactic:
by
  cases isEmpty_or_nonempty α
  · infer_instance
  obtain ⟨s, s_cnt, s_dense⟩ := exists_countable_dense β
  refine ⟨f.invFun '' s, s_cnt.image _, ?_⟩
  simp_rw [h'.dense_iff, mem_closure_iff]
  intro x U hU hx
  obtain ⟨-, ⟨hx'U, x', rfl⟩, hx's⟩ :=
    s_dense.inter_open_nonempty (U ∩ range f) (hU.inter h.isOpen_range) ⟨f x, hx, mem_range_self _⟩
  refine ⟨f <| f.invFun <| f x', ?_, mem_image_of_mem _ <| mem_image_of_mem _ hx's⟩
  rwa [Function.apply_invFun_apply (f := f)]

Goal state after:
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: case h₂
α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
x : α
⊢ ⋃ y, ⋃ (_ : y ≤ x), s y ⊆ ⋃ y, ⋃ (_ : y ≤ x), accumulate s y

Tactic:
· exact iUnion₂_mono fun y _ => subset_accumulate

Goal state after:
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
β : Type u_2
s : α → Set β
inst✝ : Preorder α
hs : Pairwise (Disjoint on s)
i j : α
hij : i < j
x : β
k : α
hk : k ≤ i
hx : x ∈ s k
⊢ x ∉ s j

Tactic:
exact disjoint_left.1 (hs (hk.trans_lt hij).ne) hx

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t : Set α
f : α → β
hfs : ContinuousOn f s
hft : ContinuousOn f t
hs : IsClosed[inst✝¹] s
ht : IsClosed[inst✝¹] t
x : α
hx✝ : x ∈ s ∪ t
hx : x ∉ s
⊢ x ∉ closure[inst✝¹] s

Tactic:
rwa [hs.closure_eq]

Goal state after:
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)
inst✝ : Finite ι
f : (i : ι) → A i → B i
hf : ∀ (i : ι), IsOpenEmbedding (f i)
⊢ IsOpen[Pi.topologicalSpace] (range (Pi.map f))

Tactic:
by simpa using isOpen_set_pi Set.finite_univ fun i _ ↦ (hf i).2

Goal state after:
Module: Mathlib.Order.Filter.Ultrafilter.Defs

Goal state before:
pp: α : Type u
f : Ultrafilter α
g : Filter α
⊢ Disjoint (↑f) g ↔ ¬¬↑f ⊓ g = ⊥

Tactic:
not_not,

Goal state after:
α : Type u
f : Ultrafilter α
g : Filter α
⊢ Disjoint (↑f) g ↔ ↑f ⊓ g = ⊥
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace β
inst✝ : SecondCountableTopology β
f : α → β
b : Set (Set β)
hb : b.Countable
eq : t = generateFrom b
this : TopologicalSpace α := induced f t
⊢ induced f (generateFrom b) = generateFrom (preimage f '' b)

Tactic:
induced_generateFrom_eq

Goal state after:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
inst✝ : SecondCountableTopology β
f : α → β
b : Set (Set β)
hb : b.Countable
eq : t = generateFrom b
this : TopologicalSpace α := induced f t
⊢ generateFrom (preimage f '' b) = generateFrom (preimage f '' b)
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t✝] u
a : α → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
x : α
hx : x ∈ u
⊢ IsOpen[t✝] (a ↑⟨x, hx⟩)

Tactic:
exact ht.isOpen (hat x hx)

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
inst✝ : SecondCountableTopology α
t : Set (Set α)
ht : IsTopologicalBasis t
u : Set α
hu : IsOpen[t✝] u
a : α → Set α
hat : ∀ x ∈ u, a x ∈ t
xa : ∀ x ∈ u, x ∈ a x
au : ∀ x ∈ u, a x ⊆ u
⊢ ∃ T, T.Countable ∧ ⋃ i ∈ T, a ↑i = ⋃ i, a ↑i

Tactic:
by
    apply isOpen_iUnion_countable _
    rintro ⟨x, hx⟩
    exact ht.isOpen (hat x hx)

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

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsCompact s
hf : ContinuousOn f s
⊢ IsCompact (f '' s)

Tactic:
by
  intro l lne ls
  have : NeBot (l.comap f ⊓ 𝓟 s) :=
    comap_inf_principal_neBot_of_image_mem lne (le_principal_iff.1 ls)
  obtain ⟨x, hxs, hx⟩ : ∃ x ∈ s, ClusterPt x (l.comap f ⊓ 𝓟 s) := @hs _ this inf_le_right
  have := hx.neBot
  use f x, mem_image_of_mem f hxs
  have : Tendsto f (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)) (𝓝 (f x) ⊓ l) := by
    convert! (hf x hxs).inf (@tendsto_comap _ _ f l) using 1
    rw [nhdsWithin]
    ac_rfl
  exact this.neBot

Goal state after:
Module: Mathlib.Topology.DiscreteSubset

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
⊢ (x ∉ S → ¬¬Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → 𝓝[≠] x ⊓ 𝓟 S = ⊥) ↔ Disjoint (𝓝[≠] x) (𝓟 S)

Tactic:
not_not,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
S : Set X
x : X
⊢ (x ∉ S → Disjoint (𝓝 x) (𝓟 S)) ∧ (x ∈ S → 𝓝[≠] x ⊓ 𝓟 S = ⊥) ↔ Disjoint (𝓝[≠] x) (𝓟 S)