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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
⊢ S₁.homologyπ ≫ S₁.leftHomologyIso.inv ≫ leftHomologyMap φ = cyclesMap φ ≫ S₂.leftHomologyπ

Tactic:
simp only [homologyπ, assoc, Iso.hom_inv_id_assoc, leftHomologyπ_naturality]

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasLeftHomology
inst✝ : S₂.HasLeftHomology
⊢ (leftHomologyMap' φ S₁.leftHomologyData S₂.leftHomologyData).op =
    rightHomologyMap' (𝟙 S₂.op) S₂.leftHomologyData.op S₂.op.rightHomologyData ≫
      rightHomologyMap' (opMap φ) S₂.op.rightHomologyData S₁.op.rightHomologyData ≫
        rightHomologyMap' (𝟙 S₁.op) S₁.op.rightHomologyData S₁.leftHomologyData.op

Tactic:
simp only [← rightHomologyMap'_comp, comp_id, id_comp, leftHomologyMap'_op]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ (φ₁ - φ₃).τ₁ = S₁.f ≫ (h.h₁ - h'.h₁) + (h.h₀ - h'.h₀) + (φ₂ - φ₄).τ₁

Tactic:
by rw [sub_τ₁, sub_τ₁, h.comm₁, h'.comm₁, comp_sub]; abel

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

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✝⁸ : HasZeroMorphisms C
inst✝⁷ : HasZeroMorphisms D
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁶ : F.PreservesZeroMorphisms
inst✝⁵ : S₁.HasHomology
inst✝⁴ : S₂.HasHomology
inst✝³ : (S₁.map F).HasHomology
inst✝² : (S₂.map F).HasHomology
inst✝¹ : F.PreservesLeftHomologyOf S₁
inst✝ : F.PreservesLeftHomologyOf S₂
⊢ homologyMap (F.mapShortComplex.map φ) ≫ (S₂.mapHomologyIso F).hom = (S₁.mapHomologyIso F).hom ≫ F.map (homologyMap φ)

Tactic:
dsimp only [homologyMap, homologyMap', mapHomologyIso, LeftHomologyData.homologyIso,
    LeftHomologyData.leftHomologyIso, leftHomologyMapIso', leftHomologyIso,
    Iso.symm, Iso.trans, Iso.refl]
  simp only [LeftHomologyData.map_leftHomologyMap', ← leftHomologyMap'_comp, comp_id, id_comp]

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝² : Mono f
A✝¹ : C
f✝¹ : A✝¹ ⟶ X
inst✝¹ : Mono f✝¹
A✝ : C
f✝ : A✝ ⟶ X
inst✝ : Mono f✝
h : mk (f✝¹ ≫ f) = mk (f✝ ≫ f)
⊢ (isoOfMkEqMk (f✝¹ ≫ f) (f✝ ≫ f) h).hom ≫ f✝ = f✝¹

Tactic:
by simp [← cancel_mono f]

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

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
F : C ⥤ D
inst✝⁴ : F.Additive
inst✝³ : F.PreservesHomology
inst✝² : HasZeroObject C
inst✝¹ : HasFiniteProducts C
inst✝ : HasKernels C
this : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
⊢ PreservesFiniteLimits F

Tactic:
have : HasBinaryBiproducts C := HasBinaryBiproducts.of_hasBinaryProducts

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
F : C ⥤ D
inst✝⁴ : F.Additive
inst✝³ : F.PreservesHomology
inst✝² : HasZeroObject C
inst✝¹ : HasFiniteProducts C
inst✝ : HasKernels C
this✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
this : HasBinaryBiproducts C
⊢ PreservesFiniteLimits 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 : C
p q : YonedaCollection F X
h : p.fst = q.fst
h' : (ConcreteCategory.hom (F.map (eqToHom ⋯))) q.snd = p.snd
⊢ p = q

Tactic:
rcases p with ⟨p, p'⟩
  rcases q with ⟨q, q'⟩
  obtain rfl : p = q := yonedaEquiv.symm.injective h
  exact Sigma.ext rfl (by simpa [snd] using! h'.symm)

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
A F : Cᵒᵖ ⥤ Type v
η : F ⟶ A
X : C
p : YonedaCollection (restrictedYonedaObj η) X
⊢ OverArrows.val ((ConcreteCategory.hom ((restrictedYonedaObj η).map (eqToHom ⋯))) (id p).snd) =
    OverArrows.val ((unitBackward η X ∘ unitForward η X) p).snd

Tactic:
· simp [unitForward, unitBackward]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u₃
inst✝² : Category.{v₃, u₃} E
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : HasLimitsOfShape J D
F : C ⥤ E
K : J ⥤ E ⥤ D
c : Cone K
hc : IsLimit c
Y : C
⊢ IsLimit (((evaluation E D).obj (F.obj Y)).mapCone c)

Tactic:
exact isLimitOfPreserves _ hc

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory

Goal state before:
pp: C✝ : Type u₁
inst✝⁸ : Category.{v₁, u₁} C✝
D✝ : Type u₂
inst✝⁷ : Category.{v₂, u₂} D✝
E✝ : Type u₃
inst✝⁶ : Category.{v₃, u₃} E✝
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : Type u_4
inst✝² : Category.{v_4, u_4} J
inst✝¹ : HasLimitsOfShape J D
F : D ⥤ E
inst✝ : PreservesLimitsOfShape J F
K : J ⥤ C ⥤ D
c : Cone K
hc : IsLimit c
k : C
⊢ IsLimit (((evaluation C D).obj k ⋙ F).mapCone c)

Tactic:
exact isLimitOfPreserves _ hc

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
D : Type u₃
inst✝³ : Category.{v₃, u₃} D
inst✝² : HasLimitsOfShape J C
inst✝¹ : HasColimitsOfShape K C
inst✝ : PreservesLimitsOfShape J colim
d : D
F G : K ⥤ D ⥤ C
η : F ⟶ G
j : K
⊢ (colimit.ι F j).app d ≫
      (colim ⋙ (evaluation D C).obj d).map η ≫
        (colimitObjIsoColimitCompEvaluation G d ≪≫
            HasColimit.isoOfNatIso (Iso.refl (G ⋙ (evaluation D C).obj d)) ≪≫
              (colimitObjIsoColimitCompEvaluation ((whiskeringRight K (D ⥤ C) C).obj ((evaluation D C).obj d)).flip
                  G).symm).hom =
    (colimit.ι F j).app d ≫
      (colimitObjIsoColimitCompEvaluation F d ≪≫
            HasColimit.isoOfNatIso (Iso.refl (F ⋙ (evaluation D C).obj d)) ≪≫
              (colimitObjIsoColimitCompEvaluation ((whiskeringRight K (D ⥤ C) C).obj ((evaluation D C).obj d)).flip
                  F).symm).hom ≫
        (colimit ((whiskeringRight K (D ⥤ C) C).obj ((evaluation D C).obj d)).flip).map η

Tactic:
simp [← NatTrans.comp_app_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
D : Type u₃
inst✝³ : Category.{v₃, u₃} D
inst✝² : HasColimitsOfShape J C
inst✝¹ : HasLimitsOfShape K C
inst✝ : PreservesColimitsOfShape J lim
d : D
X : K ⥤ D ⥤ C
⊢ limit (X ⋙ (evaluation D C).obj d) ≅
    limit (((whiskeringRight K (D ⥤ C) C).obj ((evaluation D C).obj d)).flip ⋙ (evaluation (K ⥤ D ⥤ C) C).obj X)

Tactic:
exact HasLimit.isoOfNatIso (Iso.refl _)

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal b
this : (y : (L ⋙ L').LeftExtension F₀) → Unique ((precomp₂ L' α).obj b ⟶ y) :=
  fun y ↦
    let u :=
      mk (StructuredArrow.right y)
        (hα.desc
          (mk (L' ⋙ StructuredArrow.right y)
            (StructuredArrow.hom y ≫ (L.associator L' (StructuredArrow.right y)).hom)));
    { default := StructuredArrow.homMk (hb.desc u) ⋯, uniq := ⋯ }
⊢ StructuredArrow.IsUniversal ((precomp₂ L' α).obj b)

Tactic:
apply IsInitial.ofUnique

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
inst✝ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal ((precomp₂ L' α).obj b)
this : (y : L'.LeftExtension F₁) → Unique (b ⟶ y) :=
  fun y ↦
    let u := IsInitial.to hb ((precomp₂ L' α).obj y);
    { default := StructuredArrow.homMk (StructuredArrow.Hom.right u) ⋯, uniq := ⋯ }
⊢ StructuredArrow.IsUniversal b

Tactic:
apply IsInitial.ofUnique

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝⁷ : F.Full
inst✝⁶ : F.Faithful
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : HasLimitsOfShape J C
inst✝³ : HasLimitsOfShape J D
inst✝² : HasExactLimitsOfShape J D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits G
K : Type
x✝¹ : SmallCategory K
x✝ : FinCategory K
H : K ⥤ J ⥤ C
this : PreservesLimitsOfSize.{v', u', v'', v, u'', u} G
⊢ PreservesColimit H lim

Tactic:
have : PreservesColimitsOfSize.{0, 0} F := adj.leftAdjoint_preservesColimits

Goal state after:
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u''
inst✝⁸ : Category.{v'', u''} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝⁷ : F.Full
inst✝⁶ : F.Faithful
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : HasLimitsOfShape J C
inst✝³ : HasLimitsOfShape J D
inst✝² : HasExactLimitsOfShape J D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits G
K : Type
x✝¹ : SmallCategory K
x✝ : FinCategory K
H : K ⥤ J ⥤ C
this✝ : PreservesLimitsOfSize.{v', u', v'', v, u'', u} G
this : PreservesColimitsOfSize.{0, 0, v, v'', u, u''} F
⊢ PreservesColimit H lim
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✝¹ : EssentiallySmall.{w, v₁, u₁} C
inst✝ : LocallySmall.{w, v₂, u₂} D
⊢ EssentiallySmall.{w, v₁, max u₁ v₂} (StructuredArrow S T)

Tactic:
rw [← essentiallySmall_congr
    (StructuredArrow.pre S (equivSmallModel.{w} C).inverse T).asEquivalence]

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✝¹ : EssentiallySmall.{w, v₁, u₁} C
inst✝ : LocallySmall.{w, v₂, u₂} D
⊢ EssentiallySmall.{w, w, max v₂ w} (StructuredArrow S ((equivSmallModel C).inverse ⋙ T))
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
inst✝ : Balanced C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
⊢ IsIso f

Tactic:
refine
    (isIso_iff_mono_and_epi _).2 ⟨⟨fun g h hgh => hP _ _ fun G hG i => ?_⟩, ⟨fun g h hgh => ?_⟩⟩

Goal state after:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
inst✝ : Balanced C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
Z✝ : C
g h : Z✝ ⟶ X
hgh : g ≫ f = h ≫ f
G : C
hG : P G
i : G ⟶ Z✝
⊢ i ≫ g = i ≫ h

case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
inst✝ : Balanced C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
Z✝ : C
g h : Y ⟶ Z✝
hgh : f ≫ g = f ≫ h
⊢ g = h
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
inst✝ : Balanced C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
Z✝ : C
g h : Z✝ ⟶ X
hgh : g ≫ f = h ≫ f
G : C
hG : P G
i : G ⟶ Z✝
⊢ i ≫ g = i ≫ h

Tactic:
obtain ⟨t, -, ht⟩ := hf G hG (i ≫ g ≫ f)

Goal state after:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
inst✝ : Balanced C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
Z✝ : C
g h : Z✝ ⟶ X
hgh : g ≫ f = h ≫ f
G : C
hG : P G
i : G ⟶ Z✝
t : G ⟶ X
ht : ∀ (y : G ⟶ X), (fun h' ↦ h' ≫ f = i ≫ g ≫ f) y → y = t
⊢ i ≫ g = i ≫ h
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)
⊢ ∀ {X Y : WalkingParallelPair} (f : X ⟶ Y),
    (parallelPair (line { down := true }) (line { down := false }) ⋙
              parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).map
          f ≫
        (eqToIso ⋯).hom =
      (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPair).map f

Tactic:
rintro _ _ (_ | _ | _)

Goal state after:
case left
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (parallelPair (line { down := true }) (line { down := false }) ⋙
            parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).map
        WalkingParallelPairHom.left ≫
      (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPair).map WalkingParallelPairHom.left

case right
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (parallelPair (line { down := true }) (line { down := false }) ⋙
            parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).map
        WalkingParallelPairHom.right ≫
      (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPair).map WalkingParallelPairHom.right

case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
X✝ : WalkingParallelPair
⊢ (parallelPair (line { down := true }) (line { down := false }) ⋙
            parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).map
        (WalkingParallelPairHom.id X✝) ≫
      (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPair).map (WalkingParallelPairHom.id X✝)
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
X Y : Type u
f : X ⟶ Y
inst✝ : Mono f
⊢ IsCompl (Set.range ⇑(ConcreteCategory.hom (BinaryCofan.mk f (↾Subtype.val)).inr))
    (Set.range ⇑(ConcreteCategory.hom (BinaryCofan.mk f (↾Subtype.val)).inl))

Tactic:
← eq_compl_iff_isCompl

Goal state after:
C : Type u
F : C → Type v
X Y : Type u
f : X ⟶ Y
inst✝ : Mono f
⊢ Set.range ⇑(ConcreteCategory.hom (BinaryCofan.mk f (↾Subtype.val)).inr) =
    (Set.range ⇑(ConcreteCategory.hom (BinaryCofan.mk f (↾Subtype.val)).inl))ᶜ
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: n : ℤ
⊢ n.negOnePow = 1 ↔ Even n

Tactic:
constructor
  · intro h
    rw [← Int.not_odd_iff_even]
    intro h'
    simp only [negOnePow_odd _ h'] at h
    contradiction
  · exact negOnePow_even n

Goal state after:
Module: Mathlib.Algebra.Group.Nat.Range

Goal state before:
pp: a : ℕ
s : Finset ℕ
⊢ ∀ ⦃a_1 : ℕ⦄, a_1 ∈ range a → ¬∃ a_3 ∈ s, (addLeftEmbedding a) a_3 = a_1

Tactic:
mem_range,

Goal state after:
a : ℕ
s : Finset ℕ
⊢ ∀ ⦃a_1 : ℕ⦄, a_1 < a → ¬∃ a_3 ∈ s, (addLeftEmbedding a) a_3 = a_1
Module: Mathlib.Data.Set.Constructions

Goal state before:
pp: case inter.inl.inl
α : 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
h : T1 ∈ S
i : T2 ∈ S
⊢ T1 ∩ T2 ∈ S ∨ ∃ Q ∈ S, T1 ∩ T2 = A ∩ Q

pp: case inter.inl.inr
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T1 : Set α
a✝¹ : finiteInterClosure (insert A S) T1
h : T1 ∈ S
R : Set α
hR : R ∈ S
a✝ : finiteInterClosure (insert A S) (A ∩ R)
⊢ T1 ∩ (A ∩ R) ∈ S ∨ ∃ Q ∈ S, T1 ∩ (A ∩ R) = A ∩ Q

pp: case inter.inr.inl
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T2 : Set α
a✝¹ : finiteInterClosure (insert A S) T2
Q : Set α
hQ : Q ∈ S
a✝ : finiteInterClosure (insert A S) (A ∩ Q)
i : T2 ∈ S
⊢ A ∩ Q ∩ T2 ∈ S ∨ ∃ Q_1 ∈ S, A ∩ Q ∩ T2 = A ∩ Q_1

pp: case inter.inr.inr
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P Q : Set α
hQ : Q ∈ S
a✝¹ : finiteInterClosure (insert A S) (A ∩ Q)
R : Set α
hR : R ∈ S
a✝ : finiteInterClosure (insert A S) (A ∩ R)
⊢ A ∩ Q ∩ (A ∩ R) ∈ S ∨ ∃ Q_1 ∈ S, A ∩ Q ∩ (A ∩ R) = A ∩ Q_1

Tactic:
· exact Or.inl (cond.inter_mem h i)

Goal state after:
case inter.inl.inr
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T1 : Set α
a✝¹ : finiteInterClosure (insert A S) T1
h : T1 ∈ S
R : Set α
hR : R ∈ S
a✝ : finiteInterClosure (insert A S) (A ∩ R)
⊢ T1 ∩ (A ∩ R) ∈ S ∨ ∃ Q ∈ S, T1 ∩ (A ∩ R) = A ∩ Q

case inter.inr.inl
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P T2 : Set α
a✝¹ : finiteInterClosure (insert A S) T2
Q : Set α
hQ : Q ∈ S
a✝ : finiteInterClosure (insert A S) (A ∩ Q)
i : T2 ∈ S
⊢ A ∩ Q ∩ T2 ∈ S ∨ ∃ Q_1 ∈ S, A ∩ Q ∩ T2 = A ∩ Q_1

case inter.inr.inr
α : Type u_1
S : Set (Set α)
A : Set α
cond : FiniteInter S
P Q : Set α
hQ : Q ∈ S
a✝¹ : finiteInterClosure (insert A S) (A ∩ Q)
R : Set α
hR : R ∈ S
a✝ : finiteInterClosure (insert A S) (A ∩ R)
⊢ A ∩ Q ∩ (A ∩ R) ∈ S ∨ ∃ Q_1 ∈ S, A ∩ Q ∩ (A ∩ R) = A ∩ Q_1
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case mp
m n : ℕ
⊢ ¬Odd (φ m) ∧ ¬Odd (φ n) → ¬(φ m).Coprime (φ n)

Tactic:
not_odd_iff_even,

Goal state after:
case mp
m n : ℕ
⊢ Even (φ m) ∧ Even (φ n) → ¬(φ m).Coprime (φ n)
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Preorder α
inst✝ : Preorder β
p : α × β → Prop
hp : ∀ᶠ (x : α × β) in atTop ×ˢ atTop, p x
⊢ ∀ᶠ (k : α) in atTop, ∀ᶠ (l : β) in atTop, p (k, l)

Tactic:
exact hp.curry

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
α : Type u_1
s : Set X
inst✝ : TopologicalSpace X
f : α → Set X
ho : ∀ (i : α), IsOpen[inst✝] (f i)
hU : ⋃ i, f i = univ
⊢ IsOpen[inst✝] s ↔ ∀ (i : α), IsOpen[inst✝] (f i ∩ s)

Tactic:
refine ⟨fun h i ↦ (ho i).inter h, fun h ↦ ?_⟩

Goal state after:
X : Type u
α : Type u_1
s : Set X
inst✝ : TopologicalSpace X
f : α → Set X
ho : ∀ (i : α), IsOpen[inst✝] (f i)
hU : ⋃ i, f i = univ
h : ∀ (i : α), IsOpen[inst✝] (f i ∩ s)
⊢ IsOpen[inst✝] s
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
⊢ (iInf f).lift g = ⨅ i, (f i).lift g

Tactic:
refine lift_iInf_le.antisymm fun s => ?_

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝ : Nonempty ι
f : ι → Filter α
g : Set α → Filter β
hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t
s : Set β
⊢ s ∈ (iInf f).lift g → s ∈ ⨅ i, (f i).lift g
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : Dense s
⊢ Dense sᶜᶜ

Tactic:
rwa [compl_compl]

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 : α
this : toIocDiv hp a b = toIcoDiv hp a b ∨ toIocDiv hp a b + 1 = toIcoDiv hp a b
⊢ toIocDiv hp a b ⩿ toIcoDiv hp a b

Tactic:
by
    rwa [wcovBy_iff_eq_or_covBy, ← Order.succ_eq_iff_covBy]

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 : α
⊢ toIocDiv hp a b = toIocDiv hp 0 (b - a)

Tactic:
rw [toIocDiv_sub_eq_toIocDiv_add, zero_add]

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

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

Tactic:
have hIoc₁₃ : toIocMod hp x₁ x₃' = x₃' - p := by
    apply (toIocMod_eq_iff hp).2
    exact ⟨⟨lt_sub_iff_add_lt.2 h₁₃, le_of_lt (h₃₂.trans h₂₁)⟩, 1, by simp⟩

Goal state after:
case inr
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
x₁ x₂ x₃ : α
h✝ : toIcoMod hp x₁ x₂ ≤ toIocMod hp x₁ x₃
x₂' : α := toIcoMod hp x₁ x₂
x₃' : α := toIcoMod hp x₂' x₃
h : x₂' ≤ toIocMod hp x₁ x₃'
h₂₁ : x₂' < x₁ + p
h₃₂ : x₃' - p < x₂'
h₁₃ : x₁ + p < x₃'
hIoc₁₃ : toIocMod hp x₁ x₃' = x₃' - p
⊢ x₃' ≤ toIocMod hp x₂' x₁
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
⊢ s ⊆ interior t ↔ t ∈ 𝓝ˢ s

Tactic:
simp_rw [mem_nhdsSet_iff_forall, subset_interior_iff_nhds]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
a : α
f : Filter α
t : TopologicalSpace α
⊢ nhdsAdjoint a f ≤ t ↔ f ≤ (fun t ↦ 𝓝 a) t

Tactic:
rw [le_nhds_iff]

Goal state after:
α : Type u
a : α
f : Filter α
t : TopologicalSpace α
⊢ nhdsAdjoint a f ≤ t ↔ ∀ (s : Set α), a ∈ s → IsOpen[t] s → s ∈ f
Module: Mathlib.Topology.Homeomorph.Defs

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : X ≃ₜ Y
f : Y → Z
h : IsOpenQuotientMap (f ∘ ⇑e)
⊢ IsOpenQuotientMap f

Tactic:
simpa [Function.comp_assoc] using h.comp e.symm.isOpenQuotientMap

Goal state after:
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
inst✝ : TopologicalSpace Z
hf : Continuous[inst✝², inst✝¹] f
f_surj : Surjective f
h : IsOpenMap (g ∘ f)
s : Set Y
hs : IsOpen[inst✝¹] s
⊢ IsOpen[inst✝] (g '' f '' f ⁻¹' s)

Tactic:
← image_comp

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
inst✝ : TopologicalSpace Z
hf : Continuous[inst✝², inst✝¹] f
f_surj : Surjective f
h : IsOpenMap (g ∘ f)
s : Set Y
hs : IsOpen[inst✝¹] s
⊢ IsOpen[inst✝] (g ∘ f '' f ⁻¹' s)
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:
rw [← compl_subset_compl]
  simp only [← interior_compl, ← preimage_compl, hf.interior_preimage_subset_preimage_interior]

Goal state after:
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
inst✝ : TopologicalSpace Z
hf : Surjective f
hf' : Continuous[inst✝², inst✝¹] f
hfg : IsClosedMap (g ∘ f)
K : Set Y
hK : IsClosed[inst✝¹] K
⊢ IsClosed[inst✝] (g '' f '' f ⁻¹' K)

Tactic:
← image_comp

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
inst✝ : TopologicalSpace Z
hf : Surjective f
hf' : Continuous[inst✝², inst✝¹] f
hfg : IsClosedMap (g ∘ f)
K : Set Y
hK : IsClosed[inst✝¹] K
⊢ IsClosed[inst✝] (g ∘ f '' f ⁻¹' K)
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set (X × Y)
hs : IsClosed[instTopologicalSpaceProd] s
⊢ IsClosed[instTopologicalSpaceProd] (Prod.swap ⁻¹' s)

Tactic:
exact hs.preimage continuous_swap

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
a : α
s : Set α
⊢ 𝓝[s] a ≤ 𝓝 a

Tactic:
rw [← nhdsWithin_univ]
  apply nhdsWithin_le_of_mem
  exact univ_mem

Goal state after: