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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : IsLimit (KernelFork.ofι S.f ⋯)
inst✝ : S.HasHomology
⊢ hS.lift (KernelFork.ofι S.iCycles ⋯) ≫ S.f = S.iCycles

Tactic:
exact Fork.IsLimit.lift_ι hS

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
s : S.Splitting
⊢ s.s ≫ s.r = 0

Tactic:
have := s.epi_g

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
s : S.Splitting
this : Epi S.g
⊢ s.s ≫ s.r = 0
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
s s' : S.Splitting
h : s.r = s'.r
⊢ s = s'

Tactic:
have := s.epi_g

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
s s' : S.Splitting
h : s.r = s'.r
this : Epi S.g
⊢ s = s'
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f : X✝ ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasCokernels C
X : C
⊢ ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [Mono f] [Mono g] (i : A ≅ B),
    i.hom ≫ g = f → Subobject.mk (cokernel.π f).op = Subobject.mk (cokernel.π g).op

Tactic:
rintro A B f g hf hg i rfl
        refine Subobject.mk_eq_mk_of_comm _ _ (Iso.op ?_) (Quiver.Hom.unop_inj ?_)
        · exact (IsColimit.coconePointUniqueUpToIso (colimit.isColimit _)
            (isCokernelEpiComp (colimit.isColimit _) i.hom rfl)).symm
        · simp only [Iso.comp_inv_eq, Iso.op_hom, Iso.symm_hom, unop_comp, Quiver.Hom.unop_op,
            colimit.comp_coconePointUniqueUpToIso_hom, Cofork.ofπ_ι_app,
            coequalizer.cofork_π]

Goal state after:
Module: Mathlib.Algebra.Homology.ImageToKernel

Goal state before:
pp: V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
inst✝¹ : HasImage f
g : B ⟶ C
inst✝ : HasKernel g
w : f ≫ g = 0
⊢ imageToKernel f g w ≫ (kernelSubobject g).arrow = (imageSubobject f).arrow

Tactic:
simp [imageToKernel]

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: case refine_1
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g h : MonoOver A
k₁ : f ⟶ h
k₂ : g ⟶ h
⊢ ((sup.obj f).obj g).obj.left ⟶ h.obj.left

Tactic:
apply image.lift ⟨_, h.arrow, coprod.desc k₁.hom.left k₂.hom.left, _⟩
    ext
    · simp [w k₁]
    · simp [w k₂]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
inst✝² : HasImage f
g : Y ⟶ Z
inst✝¹ : HasImage g
sq : Arrow.mk f ⟶ Arrow.mk g
inst✝ : HasImageMap sq
⊢ imageSubobjectMap sq ≫ (imageSubobject g).arrow = (imageSubobject f).arrow ≫ Arrow.Hom.right sq

Tactic:
by
  simp only [imageSubobjectMap, Category.assoc, Arrow.mk_left, Arrow.mk_right,
    Arrow.mk_hom, imageSubobject_arrow']
  rw [dsimp% image.map_ι sq]
  simp

Goal state after:
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
⊢ coimageImageComparison (α.app X) = (coimageObjIso α X).inv ≫ (coimageImageComparison α).app X ≫ (imageObjIso α X).hom

Tactic:
by
  ext
  dsimp
  dsimp [imageObjIso, coimageObjIso, cokernel.map]
  simp only [coimage_image_factorisation, PreservesKernel.iso_hom, Category.assoc,
    kernel.lift_ι, Category.comp_id, PreservesCokernel.iso_inv,
    cokernel.π_desc_assoc, Category.id_comp]
  erw [kernelComparison_comp_ι _ ((evaluation C D).obj X)]
  erw [π_comp_cokernelComparison_assoc _ ((evaluation C D).obj X)]
  conv_lhs => rw [← coimage_image_factorisation α]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
inst✝¹ : Small.{w, u₁} C
inst✝ : LocallySmall.{w, v₂, u₂} D
f : StructuredArrow S T
⊢ ∃ a, (fun f ↦ mk f.snd) a = f

Tactic:
obtain ⟨X, f, rfl⟩ := f.mk_surjective

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
inst✝¹ : Small.{w, u₁} C
inst✝ : LocallySmall.{w, v₂, u₂} D
X : C
f : S ⟶ T.obj X
⊢ ∃ a, (fun f ↦ mk f.snd) a = mk f
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : Small.{w, u₁} C
inst✝ : LocallySmall.{w, v₂, u₂} D
f : CostructuredArrow S T
⊢ ∃ a, (fun f ↦ mk f.snd) a = f

Tactic:
obtain ⟨X, f, rfl⟩ := f.mk_surjective

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : Small.{w, u₁} C
inst✝ : LocallySmall.{w, v₂, u₂} D
X : C
f : S.obj X ⟶ T
⊢ ∃ a, (fun f ↦ mk f.snd) a = mk f
Module: Mathlib.CategoryTheory.Subobject.Comma

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits T
A P Q : StructuredArrow S T
f : P ⟶ A
g : Q ⟶ A
hf : Mono f
hg : Mono g
i : P ≅ Q
⊢ i.hom ≫ g = f → Subobject.mk (Hom.right f) = Subobject.mk (Hom.right g)

Tactic:
hi

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits T
A P Q : StructuredArrow S T
f : P ⟶ A
g : Q ⟶ A
hf : Mono f
hg : Mono g
i : P ≅ Q
hi : i.hom ≫ g = f
⊢ Subobject.mk (Hom.right f) = Subobject.mk (Hom.right g)
Module: Mathlib.CategoryTheory.Subobject.Comma

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
hf : Mono f
hg : Mono g
i : P ≅ Q
⊢ i.hom ≫ g = f → Subobject.mk f.unop.left.op = Subobject.mk g.unop.left.op

Tactic:
hi

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
hf : Mono f
hg : Mono g
i : P ≅ Q
hi : i.hom ≫ g = f
⊢ Subobject.mk f.unop.left.op = Subobject.mk g.unop.left.op
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)
F : WalkingParallelFamily J ⥤ C
t : Cotrident fun j ↦ F.map (line j)
j j' : WalkingParallelFamily J
g : j ⟶ j'
⊢ F.map g ≫ eqToHom ⋯ ≫ t.ι.app j' =
    (eqToHom ⋯ ≫ t.ι.app j) ≫ ((Functor.const (WalkingParallelFamily J)).obj t.pt).map g

Tactic:
by cases g <;> simp [Cotrident.app_one t]

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝³ : Category.{v₂, u₂} ℰ
A✝ A : C ⥤ ℰ
inst✝² : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
f : P ⟶ Q
eq :
  (𝟭 (Cᵒᵖ ⥤ Type (max w v₁ v₂))).map f ≫ F.op.lanUnit.app Q =
    F.op.lanUnit.app P ≫ (F.op.lan ⋙ (Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ (Type (max w v₁ v₂))).obj F.op).map f
⊢ F.op.lanUnit.app P ≫
      F.op.whiskerLeft
        (F.op.lan.map f ≫ (F.op.lan.obj Q).descOfIsLeftKanExtension (F.op.lanUnit.app Q) (G.obj Q) (presheafHom φ Q)) =
    F.op.lanUnit.app P ≫
      F.op.whiskerLeft
        ((F.op.lan.obj P).descOfIsLeftKanExtension (F.op.lanUnit.app P) (G.obj P) (presheafHom φ P) ≫ G.map f)

Tactic:
dsimp at eq ⊢

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝³ : Category.{v₂, u₂} ℰ
A✝ A : C ⥤ ℰ
inst✝² : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
f : P ⟶ Q
eq : f ≫ F.op.lanUnit.app Q = F.op.lanUnit.app P ≫ F.op.whiskerLeft (F.op.lan.map f)
⊢ F.op.lanUnit.app P ≫
      F.op.whiskerLeft (F.op.lan.map f) ≫
        F.op.whiskerLeft ((F.op.lan.obj Q).descOfIsLeftKanExtension (F.op.lanUnit.app Q) (G.obj Q) (presheafHom φ Q)) =
    F.op.lanUnit.app P ≫
      F.op.whiskerLeft ((F.op.lan.obj P).descOfIsLeftKanExtension (F.op.lanUnit.app P) (G.obj P) (presheafHom φ P)) ≫
        F.op.whiskerLeft (G.map f)
Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal

Goal state before:
pp: G H : CommGrpCat
p : ↑G
q : ↑H
⊢ (hom (Functor.LaxMonoidal.μ (forget CommGrpCat) G H)) (p, q) = (p, q)

Tactic:
by
  apply Prod.ext
  · exact congr_hom (CC := fun X ↦ X) (Functor.Monoidal.μ_fst (forget CommGrpCat.{u}) G H) (p, q)
  · exact congr_hom (CC := fun X ↦ X) (Functor.Monoidal.μ_snd (forget CommGrpCat.{u}) G H) (p, q)

Goal state after:
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
c : α
inst✝¹ : Add α
inst✝ : MulOneClass β
l : List (α → β)
hl : ∀ f ∈ l, Periodic f c
⊢ Periodic l.prod c

Tactic:
induction l with

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

Goal state before:
pp: p✝ : ℕ → Prop
inst✝¹ : DecidablePred p✝
p : ℕ → Prop
inst✝ : DecidablePred p
m n : ℕ
hm : p m
hn : p n
heq : count p m = count p n
h : m ≠ n
hmn : m < n
⊢ False

Tactic:
· simpa [heq] using count_strict_mono hm hmn

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'
⊢ ExtensionOfMaxAdjoin.extensionToFun i f h x' = ↑(extensionOfMax i f).toLinearPMap x

Tactic:
rw [ExtensionOfMaxAdjoin.extensionToFun_wd i f h x' x 0 (by simp [EQ]), map_zero,
      add_zero]

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

Goal state before:
pp: n : ℕ
⊢ Odd (φ n) ↔ n = 1 ∨ n = 2

Tactic:
rcases n with _ | _ | _ | _

Goal state after:
case zero
⊢ Odd (φ 0) ↔ 0 = 1 ∨ 0 = 2

case succ.zero
⊢ Odd (φ (0 + 1)) ↔ 0 + 1 = 1 ∨ 0 + 1 = 2

case succ.succ.zero
⊢ Odd (φ (0 + 1 + 1)) ↔ 0 + 1 + 1 = 1 ∨ 0 + 1 + 1 = 2

case succ.succ.succ
n✝ : ℕ
⊢ Odd (φ (n✝ + 1 + 1 + 1)) ↔ n✝ + 1 + 1 + 1 = 1 ∨ n✝ + 1 + 1 + 1 = 2
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case inl
han : 0 < 1
ha : φ 1 ≤ 1
⊢ 1 ∣ 2

Tactic:
norm_num

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

Goal state before:
pp: case inr
han : 0 < 2
ha : φ 2 ≤ 1
⊢ 2 ∣ 2

Tactic:
norm_num

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

Goal state before:
pp: n : ℕ
⊢ φ n * ∏ p ∈ n.primeFactors, p = n * ∏ p ∈ n.primeFactors, (p - 1)

Tactic:
by_cases hn : n = 0; · simp [hn]
  rw [totient_eq_prod_factorization hn]
  nth_rw 3 [← prod_factorization_pow_eq_self hn]
  simp only [prod_primeFactors_prod_factorization, ← Finsupp.prod_mul]
  refine Finsupp.prod_congr (M := ℕ) (N := ℕ) fun p hp => ?_
  rw [Finsupp.mem_support_iff, ← zero_lt_iff] at hp
  rw [mul_comm, ← mul_assoc, ← pow_succ', Nat.sub_one, Nat.succ_pred_eq_of_pos hp]

Goal state after:
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.primeFactors, p) * ∏ p ∈ b.primeFactors, p) *
      ((∏ p ∈ a.primeFactors, (p - 1)) * ∏ p ∈ 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

Tactic:
rw [eq_comm, mul_comm, ← mul_assoc, ← Nat.mul_div_assoc]

Goal state after:
case H
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) * ∏ p ∈ b.primeFactors, p ∣ a * b
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 : α
⊢ toIocMod hp 0 (-(b - a)) = p - toIcoMod hp 0 (b - a)

Tactic:
toIocMod_neg,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ p - toIcoMod hp (-0) (b - a) = p - toIcoMod hp 0 (b - a)
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ : α
⊢ toIcoMod hp 0 (x₂ - x₁) ≤ toIocMod hp 0 (-(x₁ - x₃)) ↔ toIcoMod hp 0 (x₂ - x₁) + toIcoMod hp 0 (x₁ - x₃) ≤ p

Tactic:
toIocMod_neg,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ : α
⊢ toIcoMod hp 0 (x₂ - x₁) ≤ p - toIcoMod hp (-0) (x₁ - x₃) ↔ toIcoMod hp 0 (x₂ - x₁) + toIcoMod hp 0 (x₁ - x₃) ≤ p
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 : ℤ
⊢ toIcoDiv hp a (↑m * p + b) = m + toIcoDiv hp a b

Tactic:
simpa using toIcoDiv_zsmul_add hp a b m

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

Goal state before:
pp: α : Type u_1
inst✝³ : Ring α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : Archimedean α
⊢ ⋃ n, Ico (↑n) (↑n + 1) = univ

Tactic:
simpa only [zero_add] using iUnion_Ico_add_intCast (0 : α)

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

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hst' : IsOpen[inst✝] (s ∪ t)ᶜ
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
⊢ sᶜᶜ = ((s ∪ t)ᶜ ∪ v)ᶜ

Tactic:
Set.compl_union,

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
hst' : IsOpen[inst✝] (s ∪ t)ᶜ
u v : Set X
hu : IsOpen[inst✝] u
hv : IsOpen[inst✝] v
hsu : s ⊆ u
htv : t ⊆ v
huv : Disjoint u v
⊢ sᶜᶜ = (s ∪ t)ᶜᶜ ∩ vᶜ
Module: Mathlib.Topology.Maps.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenEmbedding f
l : Filter Z
x : X
⊢ Tendsto (g ∘ f) (𝓝 x) l ↔ Tendsto g (𝓝 (f x)) l

Tactic:
Tendsto,

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenEmbedding f
l : Filter Z
x : X
⊢ map (g ∘ f) (𝓝 x) ≤ l ↔ Tendsto g (𝓝 (f x)) l
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ιX : Type u_5
ιY : Type u_6
px : ιX → Prop
py : ιY → Prop
sx : ιX → Set X
sy : ιY → Set Y
x : X
y : Y
hx : (𝓝 x).HasBasis px sx
hy : (𝓝 y).HasBasis py sy
⊢ (𝓝 (x, y)).HasBasis (fun i ↦ px i.1 ∧ py i.2) fun i ↦ sx i.1 ×ˢ sy i.2

Tactic:
rw [nhds_prod_eq]

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ιX : Type u_5
ιY : Type u_6
px : ιX → Prop
py : ιY → Prop
sx : ιX → Set X
sy : ιY → Set Y
x : X
y : Y
hx : (𝓝 x).HasBasis px sx
hy : (𝓝 y).HasBasis py sy
⊢ (𝓝 x ×ˢ 𝓝 y).HasBasis (fun i ↦ px i.1 ∧ py i.2) fun i ↦ sx i.1 ×ˢ sy i.2
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
α : Type u_5
β : Type u_6
f₁ f₂ : X → α
g₁ g₂ : Y → β
x : X
y : Y
hf : f₁ =ᶠ[𝓝 x] f₂
hg : g₁ =ᶠ[𝓝 y] g₂
⊢ Prod.map f₁ g₁ =ᶠ[𝓝 (x, y)] Prod.map f₂ g₂

Tactic:
rw [nhds_prod_eq]

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
α : Type u_5
β : Type u_6
f₁ f₂ : X → α
g₁ g₂ : Y → β
x : X
y : Y
hf : f₁ =ᶠ[𝓝 x] f₂
hg : g₁ =ᶠ[𝓝 y] g₂
⊢ Prod.map f₁ g₁ =ᶠ[𝓝 x ×ˢ 𝓝 y] Prod.map f₂ g₂
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
f₁ f₂ : X → α
g₁ g₂ : Y → β
x : X
y : Y
hf : f₁ ≤ᶠ[𝓝 x] f₂
hg : g₁ ≤ᶠ[𝓝 y] g₂
⊢ Prod.map f₁ g₁ ≤ᶠ[𝓝 (x, y)] Prod.map f₂ g₂

Tactic:
rw [nhds_prod_eq]

Goal state after:
X : Type u
Y : Type v
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
α : Type u_5
β : Type u_6
inst✝¹ : LE α
inst✝ : LE β
f₁ f₂ : X → α
g₁ g₂ : Y → β
x : X
y : Y
hf : f₁ ≤ᶠ[𝓝 x] f₂
hg : g₁ ≤ᶠ[𝓝 y] g₂
⊢ Prod.map f₁ g₁ ≤ᶠ[𝓝 x ×ˢ 𝓝 y] Prod.map f₂ g₂
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
γ : Type u_5
x : X
y : Y
f : Filter γ
mx : γ → X
my : γ → Y
hx : Tendsto mx f (𝓝 x)
hy : Tendsto my f (𝓝 y)
⊢ Tendsto (fun c ↦ (mx c, my c)) f (𝓝 (x, y))

Tactic:
rw [nhds_prod_eq]

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
γ : Type u_5
x : X
y : Y
f : Filter γ
mx : γ → X
my : γ → Y
hx : Tendsto mx f (𝓝 x)
hy : Tendsto my f (𝓝 y)
⊢ Tendsto (fun c ↦ (mx c, my c)) f (𝓝 x ×ˢ 𝓝 y)
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
x : α
y : β
s t : Set β
h : ContinuousWithinAt f (f ⁻¹' s) x
ht : t ∈ 𝓝[s] f x
hxy : y = f x
⊢ f ⁻¹' t ∈ 𝓝[f ⁻¹' s] x

Tactic:
exact h.preimage_mem_nhdsWithin' (nhdsWithin_mono _ (image_preimage_subset f s) ht)

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
a : ↑s
t : Set ↑s
⊢ t ∈ 𝓝 a ↔ Subtype.val '' t ∈ 𝓝[s] ↑a

Tactic:
by
  rw [← map_nhds_subtype_val, image_mem_map_iff Subtype.val_injective]

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case mpr
X : Type u
x : CofiniteTopology X
U : Set (CofiniteTopology X)
⊢ U ∈ pure x ⊔ cofinite → ∃ t ⊆ U, (t.Nonempty → tᶜ.Finite) ∧ x ∈ t

Tactic:
· rintro ⟨hU : x ∈ U, hU' : Uᶜ.Finite⟩
    exact ⟨U, Subset.rfl, fun _ => hU', hU⟩

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
α : Type u_5
β : Type u_6
f : α → X
g : β → Y
la : Filter α
lb : Filter β
x : X
y : Y
hf : ∀ s ∈ 𝓝 x, ∃ᶠ (a : α) in la, f a ∈ s
hg : ∀ s ∈ 𝓝 y, ∃ᶠ (a : β) in lb, g a ∈ s
s : Set X
t : Set Y
hs : (s, t).1 ∈ 𝓝 x
ht : (s, t).2 ∈ 𝓝 y
⊢ ∃ᶠ (a : α × β) in la.curry lb, Prod.map f g a ∈ id (s, t).1 ×ˢ id (s, t).2

Tactic:
frequently_curry_iff

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
α : Type u_5
β : Type u_6
f : α → X
g : β → Y
la : Filter α
lb : Filter β
x : X
y : Y
hf : ∀ s ∈ 𝓝 x, ∃ᶠ (a : α) in la, f a ∈ s
hg : ∀ s ∈ 𝓝 y, ∃ᶠ (a : β) in lb, g a ∈ s
s : Set X
t : Set Y
hs : (s, t).1 ∈ 𝓝 x
ht : (s, t).2 ∈ 𝓝 y
⊢ ∃ᶠ (x : α) in la, ∃ᶠ (y : β) in lb, Prod.map f g (x, y) ∈ id (s, t).1 ×ˢ id (s, t).2
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case refine_2
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : ∀ (U : Set X), IsOpen[inst✝] U → U.Nonempty → (U ∩ s).Nonempty
v : Set X
hv1 : IsOpen[inst✝] v
t : Set X
ht : IsOpen[inst✝] t
ht' : t.Nonempty
hud : ∀ (U : Set ↑s), IsOpen[instTopologicalSpaceSubtype] U → U.Nonempty → (U ∩ Subtype.val ⁻¹' v).Nonempty
x : X
hx : x ∈ t ∩ s
⊢ (s ↓∩ t).Nonempty

Tactic:
simpa using ⟨⟨x, hx.2⟩, hx.1⟩

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : Dense s
u : Set ↑s
huo : IsOpen[instTopologicalSpaceSubtype] u
hud : Dense u
⊢ ∃ v, IsOpen[inst✝] v ∧ Dense v ∧ Subtype.val ⁻¹' v = u

Tactic:
choose v hv1 hv2 using huo
  refine ⟨v, hv1, ?_, hv2⟩
  rw [dense_iff_inter_open] at *
  intro t ht ht'
  subst hv2
  refine nonempty_of_nonempty_preimage (f := (Subtype.val : s → X)) (hud (Subtype.val ⁻¹' t) ?_ ?_)
  · exact IsOpen.preimage_val ht
  · obtain ⟨x, hx⟩ := hs t ht ht'
    simpa using ⟨⟨x, hx.2⟩, hx.1⟩

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : DiscreteTopology α
f : α × β → γ
⊢ IsOpenMap f ↔ ∀ (a : α), IsOpenMap fun x ↦ f (a, x)

Tactic:
by
  simp_rw [isOpenMap_iff_nhds_le, Prod.forall, nhds_prod_eq, nhds_discrete, pure_prod, map_map]
  rfl

Goal state after:
Module: Mathlib.Order.ZornAtoms

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderTop α
h : ∀ (c : Set α), IsChain (fun x1 x2 ↦ x1 ≤ x2) c → c.Nonempty → ⊤ ∉ c → ∃ x, x ≠ ⊤ ∧ x ∈ upperBounds c
x : α
hx : x < ⊤
y : α
hxy : x ≤ y
hmax : Maximal (fun x_1 ↦ x_1 ∈ Ico x ⊤) y
z : α
hyz : y < z
hz : z < ⊤
⊢ False

Tactic:
exact hyz.ne <| hmax.eq_of_le ⟨hxy.trans hyz.le, hz⟩ hyz.le

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
i : Set ι
s : (a : ι) → Set (A a)
x : (a : ι) → A a
hi : i.Finite
hs : ∀ a ∈ i, s a ∈ 𝓝 (x a)
⊢ ⋂ a ∈ i, eval a ⁻¹' s a ∈ 𝓝 x

Tactic:
biInter_mem hi

Goal state after:
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
i : Set ι
s : (a : ι) → Set (A a)
x : (a : ι) → A a
hi : i.Finite
hs : ∀ a ∈ i, s a ∈ 𝓝 (x a)
⊢ ∀ i_1 ∈ i, eval i_1 ⁻¹' s i_1 ∈ 𝓝 x
Module: Mathlib.Topology.Bases

Goal state before:
pp: ι : Type u_2
inst✝¹ : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst✝ : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure[inst✝ i] (c i)
this : ∀ (i : ι), Countable ↑(c i)
g : (I : Finset ι) × ((i : ↥I) → ↑(c ↑i)) → (i : ι) → X i :=
  fun x i ↦
    match x with
    | ⟨I, f⟩ => if hi : i ∈ I then ↑(f ⟨i, hi⟩) else f₀ i
f : (i : ι) → X i
hf : f ∈ univ.pi s
o : Set ((i : ι) → X i)
ho : IsOpen[Pi.topologicalSpace] o
hfo : f ∈ o
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen[inst✝ a] (u a) ∧ f a ∈ u a
hI : (↑I).pi u ⊆ o
i : ι
⊢ i ∈ I → (u i ∩ c i).Nonempty

Tactic:
hi

Goal state after:
ι : Type u_2
inst✝¹ : Countable ι
X : ι → Type u_3
s : (i : ι) → Set (X i)
inst✝ : (i : ι) → TopologicalSpace (X i)
f₀ : (i : ι) → X i
c : (i : ι) → Set (X i)
c_count : ∀ (i : ι), (c i).Countable
hc : ∀ (i : ι), s i ⊆ closure[inst✝ i] (c i)
this : ∀ (i : ι), Countable ↑(c i)
g : (I : Finset ι) × ((i : ↥I) → ↑(c ↑i)) → (i : ι) → X i :=
  fun x i ↦
    match x with
    | ⟨I, f⟩ => if hi : i ∈ I then ↑(f ⟨i, hi⟩) else f₀ i
f : (i : ι) → X i
hf : f ∈ univ.pi s
o : Set ((i : ι) → X i)
ho : IsOpen[Pi.topologicalSpace] o
hfo : f ∈ o
I : Finset ι
u : (a : ι) → Set (X a)
huo : ∀ a ∈ I, IsOpen[inst✝ a] (u a) ∧ f a ∈ u a
hI : (↑I).pi u ⊆ o
i : ι
hi : i ∈ I
⊢ (u i ∩ c i).Nonempty
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
s : Set α
hs : Dense s
⊢ (∃ c, c.Countable ∧ s ⊆ closure[t] c) ↔ ∃ s, s.Countable ∧ closure[t] s = univ

Tactic:
← univ_subset_iff,

Goal state after:
α : Type u
t : TopologicalSpace α
s : Set α
hs : Dense s
⊢ (∃ c, c.Countable ∧ s ⊆ closure[t] c) ↔ ∃ s, s.Countable ∧ univ ⊆ closure[t] s
Module: Mathlib.Order.Filter.Ultrafilter.Defs

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

Tactic:
← inf_neBot_iff,

Goal state after:
α : Type u
f : Ultrafilter α
g : Filter α
⊢ Disjoint (↑f) g ↔ ¬(↑f ⊓ g).NeBot