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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
X✝ Y✝ : ShortComplex C
p : X✝ ⟶ Y✝
x✝ : Epi p
⊢ NormalEpi p

Tactic:
refine NormalEpi.mk _ (kernel.ι p) (kernel.condition _)
    (isColimitOfIsColimitπ _ ?_ ?_ ?_)

Goal state after:
case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
X✝ Y✝ : ShortComplex C
p : X✝ ⟶ Y✝
x✝ : Epi p
⊢ IsColimit (π₁.mapCocone (CokernelCofork.ofπ p ⋯))

case refine_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
X✝ Y✝ : ShortComplex C
p : X✝ ⟶ Y✝
x✝ : Epi p
⊢ IsColimit (π₂.mapCocone (CokernelCofork.ofπ p ⋯))

case refine_3
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
S : ShortComplex C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
X✝ Y✝ : ShortComplex C
p : X✝ ⟶ Y✝
x✝ : Epi p
⊢ IsColimit (π₃.mapCocone (CokernelCofork.ofπ p ⋯))
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₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂ + φ₃.τ₂ = S₁.g ≫ (h.h₂ + h'.h₂) + (h.h₁ + h'.h₁) ≫ S₂.f + (φ₂.τ₂ + φ₄.τ₂)

Tactic:
h'.comm₂,

Goal state after:
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₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂ + (S₁.g ≫ h'.h₂ + h'.h₁ ≫ S₂.f + φ₄.τ₂) =
    S₁.g ≫ (h.h₂ + h'.h₂) + (h.h₁ + h'.h₁) ≫ S₂.f + (φ₂.τ₂ + φ₄.τ₂)
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 φ₃ φ₄
⊢ (φ₁ + φ₃).τ₃ = h.h₃ + h'.h₃ + (h.h₂ + h'.h₂) ≫ S₂.g + (φ₂ + φ₄).τ₃

Tactic:
rw [add_τ₃, add_τ₃, h.comm₃, h'.comm₃, add_comp]; abel

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₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂ - φ₃.τ₂ = S₁.g ≫ (h.h₂ - h'.h₂) + (h.h₁ - h'.h₁) ≫ S₂.f + (φ₂.τ₂ - φ₄.τ₂)

Tactic:
h'.comm₂,

Goal state after:
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₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂ - (S₁.g ≫ h'.h₂ + h'.h₁ ≫ S₂.f + φ₄.τ₂) =
    S₁.g ≫ (h.h₂ - h'.h₂) + (h.h₁ - h'.h₁) ≫ S₂.f + (φ₂.τ₂ - φ₄.τ₂)
Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P Q : C
i : P ≅ Q
x✝¹ : Projective P
E✝ X✝ : C
f : Q ⟶ X✝
e : E✝ ⟶ X✝
x✝ : Epi e
f' : P ⟶ E✝
hf' : f' ≫ e = i.hom ≫ f
⊢ (i.inv ≫ f') ≫ e = f

Tactic:
by simp [hf']

Goal state after:
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✝ : S.HasHomology
h : S.LeftHomologyData
⊢ Epi h.f' → S.Exact

Tactic:
· intro
    simp only [h.exact_iff, IsZero.iff_id_eq_zero, ← cancel_epi h.π, ← cancel_epi h.f',
      comp_id, h.f'_π, comp_zero]

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

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
f : X ⟶ Y
h : P.Factors f
w : P.factorThru f h ≫ P.arrow = 0 ≫ P.arrow
⊢ f = 0

Tactic:
simpa using w

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
B : C
X Y : Subobject B
h : X ≤ Y
Z : C
f g : Z ⟶ underlying.obj X
w : (f ≫ X.ofLE Y h) ≫ Y.arrow = (g ≫ X.ofLE Y h) ≫ Y.arrow
⊢ f ≫ X.arrow = g ≫ X.arrow

Tactic:
simpa using w

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

Goal state after:
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 A B : C
g : B ⟶ X
hg : Mono g
i : A ≅ B
hf : Mono (i.hom ≫ g)
⊢ Subobject.mk (cokernel.π (i.hom ≫ g)).op = Subobject.mk (cokernel.π g).op
Module: Mathlib.Algebra.Homology.ImageToKernel

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝² : HasKernels V
inst✝¹ : HasImages V
D : V
h : C ⟶ D
inst✝ : Mono h
w : f ≫ g ≫ h = 0
⊢ (f ≫ g) ≫ h = 0 ≫ h

Tactic:
simpa using w

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝² : HasKernels V
inst✝¹ : HasImages V
Z : V
h : Z ⟶ A
inst✝ : Epi h
w : (h ≫ f) ≫ g = 0
⊢ h ≫ f ≫ g = h ≫ 0

Tactic:
simpa using w

Goal state after:
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✝ : HasKernels C
X : C
⊢ ∀ ⦃A B : Cᵒᵖ⦄ (f : A ⟶ op X) (g : B ⟶ op X) [Mono f] [Mono g] (i : A ≅ B),
    i.hom ≫ g = f → Subobject.mk (kernel.ι f.unop) = Subobject.mk (kernel.ι g.unop)

Tactic:
rintro A B f g hf hg i rfl

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f : X✝ ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernels C
X : C
A B : Cᵒᵖ
g : B ⟶ op X
hg : Mono g
i : A ≅ B
hf : Mono (i.hom ≫ g)
⊢ Subobject.mk (kernel.ι (i.hom ≫ g).unop) = Subobject.mk (kernel.ι g.unop)
Module: Mathlib.Algebra.Homology.ImageToKernel

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasEqualizers V
inst✝ : HasImages V
Z : V
i : B ≅ Z
w : (f ≫ i.hom) ≫ i.inv ≫ g = 0
⊢ f ≫ g = 0

Tactic:
simpa using w

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

Goal state before:
pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f : X✝ ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernels C
X : C
A B : Cᵒᵖ
g : B ⟶ op X
hg : Mono g
i : A ≅ B
hf : Mono (i.hom ≫ g)
⊢ ((limit.isLimit (parallelPair (g.unop ≫ i.unop.hom) 0)).conePointUniqueUpToIso
          (isKernelCompMono (limit.isLimit (parallelPair g.unop 0)) i.unop.hom ⋯)).hom ≫
      kernel.ι g.unop =
    kernel.ι (i.hom ≫ g).unop

Tactic:
dsimp
          simp only [← Iso.eq_inv_comp, limit.conePointUniqueUpToIso_inv_comp,
            Fork.ofι_π_app]

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
w✝ : f ≫ g = 0
inst✝¹ : HasKernels V
inst✝ : HasImages V
w : f ≫ g = 0
⊢ factorThruImage f ≫ image.ι f ≫ g = factorThruImage f ≫ 0

Tactic:
simpa using w

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ S.Exact ↔ Epi (imageToKernel' S.f S.g ⋯)

Tactic:
rw [S.exact_iff_epi_kernel_lift]

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ Epi (kernel.lift S.g S.f ⋯) ↔ Epi (imageToKernel' S.f S.g ⋯)
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ f ≤ sSup s

Tactic:
fapply le_of_comm
  · refine eqToHom ?_ ≫ Sigma.ι _ ⟨equivShrink (Subobject A) f, by simpa [Set.mem_image] using hf⟩
      ≫ factorThruImage _ ≫ (underlyingIso _).inv
    exact (congr_arg (fun X : Subobject A => (X : C)) (Equiv.symm_apply_apply _ _).symm)
  · simp [sSup, smallCoproductDesc]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A F G : Cᵒᵖ ⥤ Type v
η : F ⟶ A
μ : G ⟶ A
ε : F ⟶ G
hε : ε ≫ μ = η
X : C
s : yoneda.obj X ⟶ A
u : F.obj (op X)
h : MakesOverArrow η s u
⊢ (ConcreteCategory.hom (η.app (op X))) u = yonedaEquiv s

Tactic:
h.app

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
A F G : Cᵒᵖ ⥤ Type v
η : F ⟶ A
μ : G ⟶ A
ε : F ⟶ G
hε : ε ≫ μ = η
X : C
s : yoneda.obj X ⟶ A
u : F.obj (op X)
h : MakesOverArrow η s u
⊢ yonedaEquiv s = yonedaEquiv s
Module: Mathlib.CategoryTheory.Subobject.Comma

Goal state before:
pp: case i.g
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 : StructuredArrow S T
f : P ⟶ A
hf : Mono f
q : S ⟶ T.obj (Subobject.underlying.obj (projectSubobject (Subobject.mk f)))
hq : q ≫ T.map (projectSubobject (Subobject.mk f)).arrow = A.hom
⊢ (mk q).right ≅ P.right

Tactic:
exact Subobject.underlyingIso _

Goal state after:
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 _ _ (_ | _ | _) <;> cat_disch

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
⊢ IsCoseparator (G ⨯ H) ↔ (ObjectProperty.pair G H).IsCoseparating

Tactic:
refine (isCoseparator_iff_of_isLimit_fan (prodIsProd G H)).trans ?_
  convert! Iff.rfl
  ext X
  simp only [ObjectProperty.pair_iff, ObjectProperty.ofObj_iff]
  constructor
  · rintro (rfl | rfl); exacts [⟨.left, rfl⟩, ⟨.right, rfl⟩]
  · rintro ⟨⟨_ | _⟩, rfl⟩ <;> tauto

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

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c₁ c₂ : α
inst✝ : AddGroup α
h1 : Periodic f c₁
h2 : Periodic f c₂
x : α
⊢ f (x + (c₁ - c₂)) = f x

Tactic:
sub_eq_add_neg,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c₁ c₂ : α
inst✝ : AddGroup α
h1 : Periodic f c₁
h2 : Periodic f c₂
x : α
⊢ f (x + (c₁ + -c₂)) = f x
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : AddSemigroup α
h : Periodic f c
a x : α
⊢ (fun x ↦ f (a + x)) (x + c) = (fun x ↦ f (a + x)) x

Tactic:
by simpa [add_assoc] using h (a + x)

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

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

Tactic:
sub_eq_add_neg,

Goal state after:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝¹ : AddCommGroup α
inst✝ : SubtractionMonoid β
h : Antiperiodic f c
n : ℤ
⊢ f (n • c + -x) = ↑n.negOnePow • f (-x)
Module: Mathlib.Algebra.Ring.Periodic

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddSemigroup α
inst✝ : Neg β
h : Antiperiodic f c
a x : α
⊢ (fun x ↦ f (a + x)) (x + c) = -(fun x ↦ f (a + x)) x

Tactic:
by simpa [add_assoc] using h (a + x)

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

Goal state before:
pp: case inr
n : ℕ
hn : n > 0
⊢ n.divisors.sum φ = n

Tactic:
← sum_div_divisors n φ

Goal state after:
case inr
n : ℕ
hn : n > 0
⊢ ∑ d ∈ n.divisors, φ (n / d) = n
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p ∈ n.primeFactors, ↑p ≠ 0
p : ℕ
hp✝ : p ∈ n.primeFactors
hp : 0 < p
hp' : ↑p ≠ 0
⊢ ↑(p - 1) = ↑p - 1

Tactic:
cast_pred hp

Goal state after:
case neg
n : ℕ
hn : ¬n = 0
hn' : ↑n ≠ 0
hpQ : ∏ p ∈ n.primeFactors, ↑p ≠ 0
p : ℕ
hp✝ : p ∈ n.primeFactors
hp : 0 < p
hp' : ↑p ≠ 0
⊢ ↑p - 1 = ↑p - 1
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: case neg
a : ℕ
ha : ¬a = 0
c : ℕ
h' : φ a = φ (a * c)
hb : ¬a * c = 0
⊢ a = a * c ∨ 2 * a = a * c

Tactic:
suffices a.Coprime c by
    rw [totient_mul this, eq_comm, mul_eq_left (totient_eq_zero.not.mpr ha),
      totient_eq_one_iff] at h'
    obtain rfl | rfl := h'
    · simp
    · simp [mul_comm]

Goal state after:
case neg
a : ℕ
ha : ¬a = 0
c : ℕ
h' : φ a = φ (a * c)
hb : ¬a * c = 0
⊢ a.Coprime c
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 : α
m : ℤ
⊢ toIcoDiv hp a (b - m • p) = toIcoDiv hp a b - m

Tactic:
sub_eq_add_neg,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoDiv hp a (b + -(m • p)) = toIcoDiv hp a b - m
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 : α
m : ℤ
⊢ toIcoDiv hp (a - m • p) b = toIcoDiv hp a b + m

Tactic:
sub_eq_add_neg,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoDiv hp (a + -(m • p)) b = toIcoDiv hp a b + m
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 : α
m : ℤ
⊢ toIocDiv hp a (b - m • p) = toIocDiv hp a b - m

Tactic:
sub_eq_add_neg,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocDiv hp a (b + -(m • p)) = toIocDiv hp a b - m
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 : α
m : ℤ
⊢ toIocDiv hp (a - m • p) b = toIocDiv hp a b + m

Tactic:
sub_eq_add_neg,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocDiv hp (a + -(m • p)) b = toIocDiv hp a b + m
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 : α
m : ℤ
⊢ toIcoMod hp a (b - m • p) = toIcoMod hp a b

Tactic:
sub_eq_add_neg,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoMod hp a (b + -(m • p)) = toIcoMod hp 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 : α
m : ℤ
⊢ toIcoMod hp (a - m • p) b = toIcoMod hp a b - m • p

Tactic:
sub_eq_add_neg,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoMod hp (a + -(m • p)) b = toIcoMod hp a b + -(m • p)
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 : α
m : ℤ
⊢ toIocMod hp a (b - m • p) = toIocMod hp a b

Tactic:
sub_eq_add_neg,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocMod hp a (b + -(m • p)) = toIocMod hp 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 : α
m : ℤ
⊢ toIocMod hp (a - m • p) b = toIocMod hp a b - m • p

Tactic:
sub_eq_add_neg,

Goal state after:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocMod hp (a + -(m • p)) b = toIocMod hp a b + -(m • p)
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
⊢ interior (⋂₀ S) = interior (⋂ s ∈ S, s)

Tactic:
sInter_eq_biInter

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
S : Set (Set X)
⊢ interior (⋂ i ∈ S, i) = interior (⋂ s ∈ S, s)
Module: Mathlib.Topology.Continuous

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ (∀ (x : Set Y), IsOpen[inst✝] xᶜ → IsOpen[inst✝¹] (f ⁻¹' xᶜ)) ↔
    ∀ (s : Set Y), IsClosed[inst✝] s → IsClosed[inst✝¹] (f ⁻¹' s)

Tactic:
simp only [isOpen_compl_iff, preimage_compl]

Goal state after:
Module: Mathlib.Topology.Continuous

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
α : Type u_4
f : α → X
hf : Surjective f
x : X
⊢ x ∈ closure[inst✝] (range f)

Tactic:
by
  simp [hf.range_eq]

Goal state after:
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
h : X ≃ₜ Y
f : Z → X
⊢ IsOpenMap (⇑h ∘ f) ↔ IsOpenMap f

Tactic:
refine ⟨?_, fun hf => h.isOpenMap.comp hf⟩
  intro hf
  rw [← Function.id_comp f, ← h.symm_comp_self, Function.comp_assoc]
  exact h.symm.isOpenMap.comp hf

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
⊢ IsClosedMap f ↔ ∀ {s : Set Y}, comap f (𝓝ˢ s) ≤ 𝓝ˢ (f ⁻¹' s)

Tactic:
by
  simp_rw [Filter.le_def, mem_comap'', ← subset_interior_iff_mem_nhdsSet,
    ← subset_kernImage_iff, isClosedMap_iff_kernImage_interior]
  exact ⟨fun H s t hst ↦ hst.trans H, fun H s ↦ H _ subset_rfl⟩

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
⊢ (map f (F.lift' closure[inst✝¹]) ⊓ pure y).NeBot ↔ (map f (F.lift' closure[inst✝¹] ⊓ comap f (𝓟 {y}))).NeBot

Tactic:
Filter.push_pull,

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 ↔ (map f (F.lift' closure[inst✝¹]) ⊓ 𝓟 {y}).NeBot
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
a : α
h1 : s ∈ 𝓝 a
h2 : t ∈ 𝓝[s] a
⊢ t ∈ 𝓝 a

Tactic:
rcases mem_nhdsWithin_iff_exists_mem_nhds_inter.mp h2 with ⟨_, Hw, hw⟩
  exact (𝓝 a).sets_of_superset ((𝓝 a).inter_sets Hw h1) hw

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
h : ¬AccPt x (𝓟 s)
⊢ ContinuousWithinAt f s x

Tactic:
← continuousWithinAt_sdiff_self

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
x : α
h : ¬AccPt x (𝓟 s)
⊢ ContinuousWithinAt f (s \ {x}) x
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 : IsOpenEmbedding f
hg : IsOpenEmbedding g
h : Injective (Sum.elim f g)
⊢ IsOpenEmbedding (Sum.elim f g)

Tactic:
rw [isOpenEmbedding_iff_continuous_injective_isOpenMap] at hf hg ⊢
  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
δ : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : β × γ → δ
g : α → β
h : α → γ
x : α
s : Set α
y : β × γ
hf : ContinuousAt f (g x, h x)
hg : ContinuousWithinAt g s x
hh : ContinuousWithinAt h s x
e : (g x, h x) = y
⊢ ContinuousWithinAt (fun x ↦ f (g x, h x)) s x

Tactic:
exact hf.comp₂_continuousWithinAt hg hh

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsCoinducing f
s : Set Y
hs : IsOpen[inst✝] s
⊢ IsCoinducing (s.restrictPreimage f)

Tactic:
refine .of_isOpen_preimage_iff_isOpen fun _ ↦ ?_

Goal state after:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsCoinducing f
s : Set Y
hs : IsOpen[inst✝] s
x✝ : Set ↑s
⊢ IsOpen[instTopologicalSpaceSubtype] (s.restrictPreimage f ⁻¹' x✝) ↔ IsOpen[instTopologicalSpaceSubtype] x✝
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t✝ : TopologicalSpace α
B : Set (Set α)
s t : Set α
hB : IsTopologicalBasis B
hs : IsOpen[t✝] s
ht : IsOpen[t✝] t
h : ∀ U ∈ B, U ⊆ s ↔ U ⊆ t
⊢ ⋃₀ {s_1 | s_1 ∈ B ∧ s_1 ⊆ s} = ⋃₀ {s | s ∈ B ∧ s ⊆ t}

Tactic:
exact congr_arg _ (Set.ext fun U ↦ and_congr_right <| h _)

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 γ
f : α → β → γ
sα : Set α
sβ : Set β
a : α
ha : a ∈ sα
h : ContinuousOn (uncurry f) (sα ×ˢ sβ)
⊢ ContinuousOn (f a) sβ

Tactic:
let g : β → γ := f.uncurry ∘ (fun b => (a, b))
  refine ContinuousOn.congr (f := g) ?_ (fun y => by simp [g])
  exact ContinuousOn.comp h (by fun_prop) (by grind [Set.MapsTo])

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: Y : Type v
n : ℕ
A : Fin (n + 1) → Type u_9
inst✝ : (i : Fin (n + 1)) → TopologicalSpace (A i)
f : Y → (j : Fin n) → A j.castSucc
g : Y → A (Fin.last n)
l : Filter Y
x : (j : Fin n) → A j.castSucc
y : A (Fin.last n)
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
j : Fin (n + 1)
⊢ ∀ (i : Fin n), Tendsto (fun i_1 ↦ Fin.snoc (f i_1) (g i_1) i.castSucc) l (𝓝 (Fin.snoc x y i.castSucc))

Tactic:
simpa using tendsto_pi_nhds.1 hf

Goal state after:
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: α : Type u_1
s : ℕ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) s
n : ℕ
⊢ ∃ m, accumulate s n ⊆ s m

Tactic:
induction n with
  | zero => use 0; simp [accumulate_def]
  | succ n hn =>
    obtain ⟨m, hm⟩ := hn
    obtain ⟨k, hk⟩ := hd m (n + 1)
    simp at hk
    exact ⟨k, by simp; grind⟩

Goal state after:
Module: Mathlib.Topology.Constructions

Goal state before:
pp: case intro.refine_1
ι : Type u_5
A : ι → Type u_6
T : (i : ι) → TopologicalSpace (A i)
inst✝ : Finite ι
s : Set ((a : ι) → A a)
val✝ : Fintype ι
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) →
    ∃ u, (∀ (a_2 : ι), IsOpen[T a_2] (u a_2) ∧ a a_2 ∈ u a_2) ∧ univ.pi u ⊆ s

Tactic:
rintro ⟨I, t, ⟨h1, h2⟩⟩
    refine
      ⟨fun i => (h1 i).choose,
        ⟨fun i => (h1 i).choose_spec.2,
          (pi_mono fun i _ => (h1 i).choose_spec.1).trans (Subset.trans ?_ h2)⟩⟩
    rw [← pi_inter_compl (I : Set ι)]
    exact inter_subset_left

Goal state after: