mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u_1
inst✝³ : Category.{v_1, u_1} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : G.Full
inst✝¹ : G.Faithful
I : D
hI : Injective (G.obj I)
X Y : D
f : X ⟶ I
g : X ⟶ Y
inst✝ : Mono g
this : PreservesLimitsOfSize.{0, 0, v_1, v₁, u_1, u₁} G
⊢ ∃ h, g ≫ h = f

Tactic:
rcases hI.factors (G.map f) (G.map g) with ⟨w,h⟩

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u_1
inst✝³ : Category.{v_1, u_1} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : G.Full
inst✝¹ : G.Faithful
I : D
hI : Injective (G.obj I)
X Y : D
f : X ⟶ I
g : X ⟶ Y
inst✝ : Mono g
this : PreservesLimitsOfSize.{0, 0, v_1, v₁, u_1, u₁} G
w : G.obj Y ⟶ G.obj I
h : G.map g ≫ w = G.map f
⊢ ∃ h, g ≫ h = f
Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
h : Retract X Y
i : Injective Y
A B : C
f : A ⟶ X
e : A ⟶ B
x✝ : Mono e
g : B ⟶ Y
hg : e ≫ g = f ≫ h.i
⊢ ∃ h, e ≫ h = f

Tactic:
use g ≫ h.r

Goal state after:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
h : Retract X Y
i : Injective Y
A B : C
f : A ⟶ X
e : A ⟶ B
x✝ : Mono e
g : B ⟶ Y
hg : e ≫ g = f ≫ h.i
⊢ e ≫ g ≫ h.r = f
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
e : S₁ ≅ S₂
h : S₁.Exact
⊢ S₂.Exact

Tactic:
obtain ⟨⟨h, z⟩⟩ := h

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
e : S₁ ≅ S₂
h : S₁.HomologyData
z : IsZero h.left.H
⊢ S₂.Exact
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.s = s'.s
this : Mono S.f
eq : s.r ≫ S.f + S.g ≫ s.s = 𝟙 S.X₂
⊢ s = s'

Tactic:
rw [← s'.id, h, add_left_inj, cancel_mono S.f] at eq

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.s = s'.s
this : Mono S.f
eq : s.r = s'.r
⊢ s = s'
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive C
inst✝ : Preadditive D
S S₁ S₂ : ShortComplex C
s : S₁.Splitting
e : S₁ ≅ S₂
⊢ S₂.f ≫ e.inv.τ₂ ≫ s.r ≫ e.hom.τ₁ = 𝟙 S₂.X₁

Tactic:
← e.inv.comm₁₂_assoc,

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive C
inst✝ : Preadditive D
S S₁ S₂ : ShortComplex C
s : S₁.Splitting
e : S₁ ≅ S₂
⊢ e.inv.τ₁ ≫ S₁.f ≫ s.r ≫ e.hom.τ₁ = 𝟙 S₂.X₁
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
p : Subobject X → Subobject X → Prop
h : ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [inst : Mono f] [inst_1 : Mono g], p (mk f) (mk g)
P Q : Subobject X
⊢ p P Q

Tactic:
induction P, Q using Quotient.inductionOn₂' with

Goal state after:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
p : Subobject X → Subobject X → Prop
h : ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [inst : Mono f] [inst_1 : Mono g], p (mk f) (mk g)
a b : MonoOver X
⊢ p (Quotient.mk'' a) (Quotient.mk'' b)
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: case mpr
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : Balanced C
inst✝ : S.HasHomology
⊢ Nonempty (IsColimit (CokernelCofork.ofπ S.g ⋯)) → S.Exact ∧ Epi S.g

Tactic:
· intro ⟨hS⟩
    exact ⟨S.exact_of_g_is_cokernel hS, epi_of_isColimit_cofork hS⟩

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type u₃
inst✝¹ : Category.{v₃, u₃} J
inst✝ : HasLimitsOfShape J (Over X)
⊢ HasLimitsOfShape J (Subobject X)

Tactic:
by
  apply hasLimitsOfShape_thinSkeleton

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

Goal state before:
pp: case hg₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
⊢ S₂.op.g = 0

pp: case hf₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
⊢ S₁.op.f = 0

pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
⊢ { X₁ := S₂.op.X₂, X₂ := S₁.op.X₂, X₃ := S₁.op.X₃, f := (opMap φ).τ₂, g := S₁.op.g, zero := ⋯ }.Exact ∧
      Mono (opMap φ).τ₂ ↔
    { X₁ := S₁.X₁, X₂ := S₁.X₂, X₃ := S₂.X₂, f := S₁.f, g := φ.τ₂, zero := ⋯ }.Exact ∧ Epi φ.τ₂

Tactic:
· dsimp
    rw [hf₂, op_zero]

Goal state after:
case hf₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
⊢ S₁.op.f = 0

C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
⊢ { X₁ := S₂.op.X₂, X₂ := S₁.op.X₂, X₃ := S₁.op.X₃, f := (opMap φ).τ₂, g := S₁.op.g, zero := ⋯ }.Exact ∧
      Mono (opMap φ).τ₂ ↔
    { X₁ := S₁.X₁, X₂ := S₁.X₂, X₃ := S₂.X₂, f := S₁.f, g := φ.τ₂, zero := ⋯ }.Exact ∧ Epi φ.τ₂
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
I : Type u_1
A B : C
s : Finset I
P : I → Subobject B
f : A ⟶ B
⊢ (s.inf P).Factors f ↔ ∀ i ∈ s, (P i).Factors f

Tactic:
induction s using Finset.induction_on with
  | empty => simp [top_factors]
  | insert _ _ _ ih => simp [ih]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan Z
f : Fan fun x ↦ op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
j : α
⊢ (c'.inj j ≫ (opCoproductIsoProduct' hc' hf).inv.unop ≫ (opCoproductIsoProduct' hc hf).hom.unop).op =
    (c.ι.app { as := j }).op

Tactic:
simp only [op_comp, op_unop, Quiver.Hom.op_unop, Category.assoc,
    opCoproductIsoProduct'_inv_comp_inj]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
c c' : Cofan Z
f : Fan fun x ↦ op (Z x)
hc : IsColimit c
hc' : IsColimit c'
hf : IsLimit f
j : α
⊢ (opCoproductIsoProduct' hc hf).hom ≫ f.proj j = (c.ι.app { as := j }).op
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
H : Type u_3
D : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
φ : F'' ⟶ F'
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : L.whiskerLeft φ ≫ α = α'
inst✝ : F'.IsRightKanExtension α
⊢ F''.IsRightKanExtension α' ↔ IsIso φ

Tactic:
constructor
  · intro
    rw [F'.hom_ext_of_isRightKanExtension α φ (rightKanExtensionUnique _ α' _ α).hom
      (by simp [comm])]
    infer_instance
  · intro
    rw [isRightKanExtension_iff_of_iso (asIso φ) α' α comm]
    infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
β : Type w
f : β → C
hf : (ObjectProperty.ofObj f).IsCoseparating
c : Fan f
hc : IsLimit c
⊢ IsCoseparator c.pt

Tactic:
rw [isCoseparator_def]
  refine fun _ _ _ _ huv ↦ hf _ _ (fun _ h g ↦ ?_)
  obtain ⟨b⟩ := h
  classical simpa using huv (hc.lift (Fan.mk _ (Pi.single b g))) =≫ c.proj b

Goal state after:
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
h : (coyoneda.obj (op G)).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
⊢ IsIso f

Tactic:
suffices IsIso ((coyoneda.obj (op G)).map f) by
      exact @isIso_of_reflects_iso _ _ _ _ _ _ _ (coyoneda.obj (op G)) _ h

Goal state after:
case refine_2
C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
h : (coyoneda.obj (op G)).ReflectsIsomorphisms
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
⊢ IsIso ((coyoneda.obj (op G)).map f)
Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal

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

Tactic:
apply Prod.ext

Goal state after:
case fst
G H : GrpCat
p : ↑G
q : ↑H
⊢ ((hom (Functor.LaxMonoidal.μ (forget GrpCat) G H)) (p, q)).1 = (p, q).1

case snd
G H : GrpCat
p : ↑G
q : ↑H
⊢ ((hom (Functor.LaxMonoidal.μ (forget GrpCat) G H)) (p, q)).2 = (p, q).2
Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal

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

Tactic:
apply Prod.ext

Goal state after:
case fst
G H : AddGrpCat
p : ↑G
q : ↑H
⊢ ((hom (Functor.LaxMonoidal.μ (forget AddGrpCat) G H)) (p, q)).1 = (p, q).1

case snd
G H : AddGrpCat
p : ↑G
q : ↑H
⊢ ((hom (Functor.LaxMonoidal.μ (forget AddGrpCat) G H)) (p, q)).2 = (p, q).2
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:
apply Prod.ext

Goal state after:
case fst
G H : CommGrpCat
p : ↑G
q : ↑H
⊢ ((hom (Functor.LaxMonoidal.μ (forget CommGrpCat) G H)) (p, q)).1 = (p, q).1

case snd
G H : CommGrpCat
p : ↑G
q : ↑H
⊢ ((hom (Functor.LaxMonoidal.μ (forget CommGrpCat) G H)) (p, q)).2 = (p, q).2
Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal

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

Tactic:
apply Prod.ext

Goal state after:
case fst
G H : AddCommGrpCat
p : ↑G
q : ↑H
⊢ ((hom (Functor.LaxMonoidal.μ (forget AddCommGrpCat) G H)) (p, q)).1 = (p, q).1

case snd
G H : AddCommGrpCat
p : ↑G
q : ↑H
⊢ ((hom (Functor.LaxMonoidal.μ (forget AddCommGrpCat) G H)) (p, q)).2 = (p, q).2
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 : Injective R M
X✝ Y✝ : ModuleCat R
g : X✝ ⟶ ModuleCat.of R M
f : X✝ ⟶ Y✝
m : Mono f
l : ↑Y✝ →ₗ[R] M
h : ∀ (x : ↑X✝), l ((ModuleCat.Hom.hom f) x) = (ModuleCat.Hom.hom g) x
⊢ f ≫ ModuleCat.ofHom l = g

Tactic:
by ext x; simpa using h x

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddGroup α
h : Periodic f c
x : α
⊢ f (x - c) = f x

Tactic:
simpa only [sub_add_cancel] using (h (x - c)).symm

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

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
a b : α
⊢ b - a ∈ Icc 0 b ↔ a ∈ Icc 0 b

Tactic:
by
  simp only [sub_mem_Icc_iff_right, sub_self, sub_zero]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : NonAssocRing α
inst✝ : NonAssocRing β
h : Antiperiodic f c
n : ℤ
⊢ f (x - ↑n * c) = ↑↑n.negOnePow * f x

Tactic:
by
  simpa only [zsmul_eq_mul] using h.sub_zsmul_eq n

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

Goal state before:
pp: case coprime
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
a b : ℕ
a✝¹ : 1 < a
a✝ : 1 < b
hab : a.Coprime b
⊢ (a ≠ 0 → f a = a.factorization.prod fun p k ↦ f (p ^ k)) →
    (b ≠ 0 → f b = b.factorization.prod fun p k ↦ f (p ^ k)) →
      a * b ≠ 0 → f (a * b) = (a * b).factorization.prod fun p k ↦ f (p ^ k)

Tactic:
ha

Goal state after:
case coprime
β : Type u_1
inst✝ : CommMonoid β
f : ℕ → β
h_mult : ∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y
hf : f 1 = 1
a b : ℕ
a✝¹ : 1 < a
a✝ : 1 < b
hab : a.Coprime b
ha : a ≠ 0 → f a = a.factorization.prod fun p k ↦ f (p ^ k)
⊢ (b ≠ 0 → f b = b.factorization.prod fun p k ↦ f (p ^ k)) →
    a * b ≠ 0 → f (a * b) = (a * b).factorization.prod fun p k ↦ f (p ^ k)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: p : ℕ
hp : Prime p
n a : ℕ
⊢ a < p ^ (n + 1) → (¬p ∣ a ↔ ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = a))

Tactic:
ha

Goal state after:
p : ℕ
hp : Prime p
n a : ℕ
ha : a < p ^ (n + 1)
⊢ ¬p ∣ a ↔ ∀ (x : ℕ), ¬(x < p ^ n ∧ x * p = a)
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: n : ℕ
this : 3 ≤ n + 3
⊢ n + 3 = 2 → φ (n + 3) = 1

Tactic:
by rintro ⟨⟩

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

Goal state before:
pp: case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p ∈ n.primeFactors, ↑p ≠ 0
⊢ ∏ i ∈ n.primeFactors, ↑(i - 1) = ∏ x ∈ n.primeFactors, (1 - (↑x)⁻¹) * ↑x

Tactic:
refine prod_congr rfl fun p hp => ?_

Goal state after:
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p ∈ n.primeFactors, ↑p ≠ 0
p : ℕ
hp : p ∈ n.primeFactors
⊢ ↑(p - 1) = (1 - (↑p)⁻¹) * ↑p
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: ι : Type u_3
l : Filter ι
p : ι → Prop
inst✝ : l.IsCountablyGenerated
⊢ (∃ᶠ (n : ι) in l, p n) ↔ ∃ x, Tendsto x atTop l ∧ ∃ᶠ (n : ℕ) in atTop, p (x n)

Tactic:
simp only [Filter.Frequently, eventually_iff_seq_eventually (l := l)]
  push Not; rfl

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

Goal state before:
pp: case inr.inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
hab' : a.primeFactors ⊆ b.primeFactors
⊢ (a.factorization.prod fun p k ↦ p ^ (k - 1) * (p - 1)) ∣ b.factorization.prod fun p k ↦ p ^ (k - 1) * (p - 1)

Tactic:
refine Finsupp.prod_dvd_prod_of_subset_of_dvd hab' fun p _ => mul_dvd_mul ?_ dvd_rfl

Goal state after:
case inr.inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
hab' : a.primeFactors ⊆ b.primeFactors
p : ℕ
x✝ : p ∈ a.factorization.support
⊢ p ^ (a.factorization p - 1) ∣ p ^ (b.factorization p - 1)
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
ι : Sort u_4
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
hg' : g univ = ⊤
h✝ : IsEmpty ι
⊢ (iInf f).lift g = ⨅ i, (f i).lift g

pp: case inr
α : Type u_1
β : Type u_2
ι : Sort u_4
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
hg' : g univ = ⊤
h✝ : Nonempty ι
⊢ (iInf f).lift g = ⨅ i, (f i).lift g

Tactic:
· simp [iInf_of_empty, hg']

Goal state after:
case inr
α : Type u_1
β : Type u_2
ι : Sort u_4
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
hg' : g univ = ⊤
h✝ : Nonempty ι
⊢ (iInf f).lift g = ⨅ i, (f i).lift g
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 : 𝓟 sᶜ ≤ comap f (𝓝 x)
h' : l ⊓ 𝓟 s ≤ comap f (𝓝 x)
this : (l ⊔ 𝓟 sᶜ) ⊓ (𝓟 s ⊔ 𝓟 sᶜ) ≤ comap f (𝓝 x)
⊢ l ≤ comap f (𝓝 x)

Tactic:
sup_principal,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
α : Type u_1
x : X
f : α → X
l : Filter α
s : Set α
h : 𝓟 sᶜ ≤ comap f (𝓝 x)
h' : l ⊓ 𝓟 s ≤ comap f (𝓝 x)
this : (l ⊔ 𝓟 sᶜ) ⊓ 𝓟 (s ∪ sᶜ) ≤ comap f (𝓝 x)
⊢ l ≤ comap f (𝓝 x)
Module: Mathlib.Topology.Defs.Induced

Goal state before:
pp: X : Type u_1
Y : Type u_2
f : X → Y
t : TopologicalSpace Y
⊢ ∀ (s t_1 : Set X),
    (∃ t_2, IsOpen[t] t_2 ∧ f ⁻¹' t_2 = s) →
      (∃ t_2, IsOpen[t] t_2 ∧ f ⁻¹' t_2 = t_1) → ∃ t_2, IsOpen[t] t_2 ∧ f ⁻¹' t_2 = s ∩ t_1

Tactic:
by
    rintro s₁ s₂ ⟨s'₁, hs₁, rfl⟩ ⟨s'₂, hs₂, rfl⟩
    exact ⟨s'₁ ∩ s'₂, hs₁.inter hs₂, preimage_inter⟩

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

Goal state before:
pp: α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a < b - toIocDiv hp a b • p
hr : b - toIocDiv hp a b • p ≤ a + p
⊢ b ≤ a + (toIocDiv hp a b + 1) • p

Tactic:
rw [add_smul, one_smul, ← add_assoc]

Goal state after:
α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a < b - toIocDiv hp a b • p
hr : b - toIocDiv hp a b • p ≤ a + p
⊢ b ≤ a + toIocDiv hp a b • p + p
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a ≤ b - toIcoDiv hp a b • p
hr : b - toIcoDiv hp a b • p < a + p
⊢ b < a + (toIcoDiv hp a b + 1) • p

Tactic:
rw [add_smul, one_smul, ← add_assoc]

Goal state after:
α : Type u_1
inst✝³ : AddCommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedAddMonoid α
inst✝ : Archimedean α
p : α
hp : 0 < p
a b : α
hl : a ≤ b - toIcoDiv hp a b • p
hr : b - toIcoDiv hp a b • p < a + p
⊢ b < a + toIcoDiv hp a b • p + p
Module: Mathlib.Topology.Order

Goal state before:
pp: case a
α : Type u
n : α → Filter α
ι : α → Sort u_1
p : (a : α) → ι a → Prop
s : (a : α) → ι a → Set α
hb : ∀ (a : α), (n a).HasBasis (p a) (s a)
hopen : ∀ (a : α) (i : ι a), p a i → ∀ᶠ (x : α) in n a, s a i ∈ n x
a : α
t : TopologicalSpace α := TopologicalSpace.mkOfNhds n
U : Set α
hU : U ∈ n a
hpure : pure ≤ n
x : α
hx : x ∈ {x | U ∈ n x}
i : ι x
hpi : p x i
hi : s x i ⊆ U
⊢ {x | U ∈ n x} ∈ n x

Tactic:
exact (hopen x i hpi).mono fun y ↦ by gcongr

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
ι : Sort v
t : ι → TopologicalSpace α
s : Set α
⊢ IsClosed[⨆ i, t i] s ↔ ∀ (i : ι), IsClosed[t i] s

Tactic:
simp only [← @isOpen_compl_iff _ _ (⨆ i, t i), ← @isOpen_compl_iff _ _ (t _), isOpen_iSup_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
hf : IsOpenMap f
s : Set Y
⊢ f ⁻¹' closure[inst✝] s ⊆ closure[inst✝¹] (f ⁻¹' s)

Tactic:
by
  rw [← compl_subset_compl]
  simp only [← interior_compl, ← preimage_compl, hf.interior_preimage_subset_preimage_interior]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝 a ⊓ 𝓟 (s ∪ t) = 𝓝 a ⊓ 𝓟 s ⊔ 𝓝 a ⊓ 𝓟 t

Tactic:
← inf_sup_left,

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝 a ⊓ 𝓟 (s ∪ t) = 𝓝 a ⊓ (𝓟 s ⊔ 𝓟 t)
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
x : α
s t : Set α
hst : s =ᶠ[𝓝 x] t
h : x ∈ interior s
⊢ x ∈ interior t

Tactic:
rw [← nhdsWithin_eq_iff_eventuallyEq] at hst
  simpa [mem_interior_iff_mem_nhds, ← nhdsWithin_eq_nhds, hst] using h

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

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
hf : Continuous[inst✝², inst✝] f ∧ Injective f ∧ IsOpenMap f
hg : Continuous[inst✝¹, inst✝] g ∧ Injective g ∧ IsOpenMap g
h : Injective (Sum.elim f g)
⊢ Continuous[instTopologicalSpaceSum, inst✝] (Sum.elim f g) ∧ Injective (Sum.elim f g) ∧ IsOpenMap (Sum.elim f g)

Tactic:
exact ⟨hf.1.sumElim hg.1, h, hf.2.2.sumElim hg.2.2⟩

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

Goal state before:
pp: X : Type u
Y : Type v
Z : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : X → Z
g : Y → Z
hf : Continuous[inst✝², inst✝] f ∧ Injective f ∧ IsClosedMap f
hg : Continuous[inst✝¹, inst✝] g ∧ Injective g ∧ IsClosedMap g
h : Injective (Sum.elim f g)
⊢ Continuous[instTopologicalSpaceSum, inst✝] (Sum.elim f g) ∧ Injective (Sum.elim f g) ∧ IsClosedMap (Sum.elim f g)

Tactic:
exact ⟨hf.1.sumElim hg.1, h, hf.2.2.sumElim hg.2.2⟩

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 : α × β → γ
s : Set (α × β)
⊢ ContinuousOn f s ↔ ∀ (b : β), ContinuousOn (fun x ↦ f (x, b)) {a | (a, b) ∈ s}

Tactic:
by
  simp_rw [ContinuousOn, Prod.forall, continuousWithinAt_prod_of_discrete_right]; apply forall_comm

Goal state after:
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
β : Type u_1
t : TopologicalSpace α
inst✝ : TopologicalSpace β
B : Set (Set α)
hB : IsTopologicalBasis B
f : α → β
hf : ∀ s ∈ B, IsOpen[inst✝] (f '' s)
o : Set α
ho : IsOpen[t] o
⊢ IsOpen[inst✝] (f '' o)

Tactic:
hB.open_eq_sUnion' ho,

Goal state after:
α : Type u
β : Type u_1
t : TopologicalSpace α
inst✝ : TopologicalSpace β
B : Set (Set α)
hB : IsTopologicalBasis B
f : α → β
hf : ∀ s ∈ B, IsOpen[inst✝] (f '' s)
o : Set α
ho : IsOpen[t] o
⊢ IsOpen[inst✝] (f '' ⋃₀ {s | s ∈ B ∧ s ⊆ o})
Module: Mathlib.Topology.Bases

Goal state before:
pp: case refine_2
α : Type u
t : TopologicalSpace α
ι : Sort u_2
U : ι → Set α
Uo : ∀ (i : ι), IsOpen[t] (U i)
Uc : ⋃ i, U i = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
a : α
u : Set α
⊢ a ∈ u → IsOpen[t] u → ∃ v ∈ ⋃ i, image Subtype.val '' b i, a ∈ v ∧ v ⊆ u

Tactic:
ha

Goal state after:
case refine_2
α : Type u
t : TopologicalSpace α
ι : Sort u_2
U : ι → Set α
Uo : ∀ (i : ι), IsOpen[t] (U i)
Uc : ⋃ i, U i = univ
b : (i : ι) → Set (Set ↑(U i))
hb : ∀ (i : ι), IsTopologicalBasis (b i)
a : α
u : Set α
ha : a ∈ u
⊢ IsOpen[t] u → ∃ v ∈ ⋃ i, image Subtype.val '' b i, a ∈ v ∧ v ⊆ u
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, ∃ I t, (∀ (i : ι), ∃ t_1 ⊆ t i, IsOpen[T i] t_1 ∧ x i ∈ t_1) ∧ (↑I).pi t ⊆ s) ↔
    ∀ f ∈ s, ∃ I u, (∀ a ∈ I, IsOpen[T a] (u a) ∧ f a ∈ u a) ∧ (↑I).pi u ⊆ s

Tactic:
refine forall₂_congr fun a _ => ⟨?_, ?_⟩

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

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.Order.SetAccumulate

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

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

Goal state after:
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)
⊢ SeparableSpace ((i : ι) → X i)

Tactic:
set f : (Σ I : Finset ι, ∀ i : I, t i) → ∀ i, X i := fun ⟨I, g⟩ i ↦
      if hi : i ∈ I then g ⟨i, hi⟩ else (default : ∀ i, X i) i

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
⊢ SeparableSpace ((i : ι) → X i)