mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.Opposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (cokernel.π f.op).unop ≫ f = 0

Tactic:
rw [← f.unop_op, ← unop_comp, f.unop_op]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (f.op ≫ cokernel.π f.op).unop = 0
Module: Mathlib.Algebra.Homology.ShortComplex.PreservesHomology

Goal state before:
pp: case mp
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
F : C ⥤ D
inst✝⁷ : F.PreservesZeroMorphisms
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝⁶ : S₁.HasHomology
inst✝⁵ : S₂.HasHomology
inst✝⁴ : (F.mapShortComplex.obj S₁).HasHomology
inst✝³ : (F.mapShortComplex.obj S₂).HasHomology
inst✝² : F.PreservesLeftHomologyOf S₁
inst✝¹ : F.PreservesLeftHomologyOf S₂
inst✝ : F.ReflectsIsomorphisms
γ : LeftHomologyMapData φ S₁.leftHomologyData S₂.leftHomologyData
a✝ : IsIso (F.map γ.φH)
⊢ IsIso γ.φH

Tactic:
exact isIso_of_reflects_iso _ F

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

Goal state before:
pp: case mp
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
F : C ⥤ D
inst✝⁷ : F.PreservesZeroMorphisms
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝⁶ : S₁.HasHomology
inst✝⁵ : S₂.HasHomology
inst✝⁴ : (F.mapShortComplex.obj S₁).HasHomology
inst✝³ : (F.mapShortComplex.obj S₂).HasHomology
inst✝² : F.PreservesRightHomologyOf S₁
inst✝¹ : F.PreservesRightHomologyOf S₂
inst✝ : F.ReflectsIsomorphisms
γ : RightHomologyMapData φ S₁.rightHomologyData S₂.rightHomologyData
a✝ : IsIso (F.map γ.φH)
⊢ IsIso γ.φH

Tactic:
exact isIso_of_reflects_iso _ F

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

Goal state before:
pp: case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : S.ShortExact
inst✝ : Balanced C
this✝¹ : HasZeroObject C
this✝ : Mono S.f
this : Epi S.g
hf : IsIso S.g
⊢ IsZero S.X₁

Tactic:
simp only [IsZero.iff_id_eq_zero, ← cancel_mono S.f, ← cancel_mono S.g,
      S.zero, zero_comp, assoc, comp_zero]

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

Goal state before:
pp: case mpr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : S.ShortExact
inst✝ : Balanced C
this✝¹ : HasZeroObject C
this✝ : Mono S.f
this : Epi S.g
⊢ IsZero S.X₁ → IsIso S.g

Tactic:
intro hX₁
    have : Mono S.g := (S.exact_iff_mono (hX₁.eq_of_src _ _)).1 hS.exact
    apply isIso_of_mono_of_epi

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

Goal state before:
pp: case mp
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasZeroObject C
⊢ IsZero S.homology → Nonempty (S.homology ≅ 0)

Tactic:
intro h
    exact ⟨h.isoZero⟩

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.Reflective

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
i : D ⥤ C
inst✝ : Reflective i
X : C
⊢ (reflectorAdjunction i).unit.app (i.obj ((reflector i).obj X)) =
    i.map ((reflector i).map ((reflectorAdjunction i).unit.app X))

Tactic:
← cancel_mono (i.map ((reflectorAdjunction i).counit.app ((reflector i).obj X))),

Goal state after:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
i : D ⥤ C
inst✝ : Reflective i
X : C
⊢ (reflectorAdjunction i).unit.app (i.obj ((reflector i).obj X)) ≫
      i.map ((reflectorAdjunction i).counit.app ((reflector i).obj X)) =
    i.map ((reflector i).map ((reflectorAdjunction i).unit.app X)) ≫
      i.map ((reflectorAdjunction i).counit.app ((reflector i).obj X))
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.Exact
inst✝³ : Mono S₁.f
inst✝² : Mono S₂.f
inst✝¹ : Mono φ.τ₁
inst✝ : Mono φ.τ₃
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ φ.τ₂ = 0
⊢ x₂ = 0

Tactic:
obtain ⟨x₁, hx₁⟩ : ∃ x₁, x₁ ≫ S₁.f = x₂ := ⟨_, h₁.lift_f x₂
    (by simp only [← cancel_mono φ.τ₃, assoc, zero_comp, ← φ.comm₂₃, reassoc_of% hx₂])⟩

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.Exact
inst✝³ : Mono S₁.f
inst✝² : Mono S₂.f
inst✝¹ : Mono φ.τ₁
inst✝ : Mono φ.τ₃
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ φ.τ₂ = 0
x₁ : A ⟶ S₁.X₁
hx₁ : x₁ ≫ S₁.f = x₂
⊢ x₂ = 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
inst✝⁴ : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.Exact
inst✝³ : Mono S₁.f
inst✝² : Mono S₂.f
inst✝¹ : Mono φ.τ₁
inst✝ : Mono φ.τ₃
A : C
x₂ : A ⟶ S₁.X₂
hx₂ : x₂ ≫ φ.τ₂ = 0
x₁ : A ⟶ S₁.X₁
hx₁ : x₁ ≫ S₁.f = x₂
this : x₁ = 0
⊢ x₂ = 0

Tactic:
by rw [← hx₁, this, zero_comp]

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✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
⊢ QuasiIso φ ↔ { X₁ := S₁.X₁, X₂ := S₁.X₂, X₃ := S₂.X₂, f := S₁.f, g := φ.τ₂, zero := ⋯ }.Exact ∧ Epi φ.τ₂

Tactic:
rw [← quasiIso_opMap_iff, quasiIso_iff_of_zeros]
  rotate_left
  · dsimp
    rw [hg₂, op_zero]
  · dsimp
    rw [hf₂, op_zero]
  · dsimp
    rw [hg₁, op_zero]
  rw [← exact_unop_iff]
  have : Mono φ.τ₂.op ↔ Epi φ.τ₂ :=
    ⟨fun _ => unop_epi_of_mono φ.τ₂.op, fun _ => op_mono_of_epi _⟩
  tauto

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✝¹ : HasImages V
inst✝ : Epi f
this : Epi (image.ι f)
⊢ Epi ((imageSubobject f).arrow ≫ inv (kernelSubobject 0).arrow)

Tactic:
rw [← imageSubobject_arrow]

Goal state after:
ι : 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✝¹ : HasImages V
inst✝ : Epi f
this : Epi (image.ι f)
⊢ Epi (((imageSubobjectIso f).hom ≫ image.ι f) ≫ inv (kernelSubobject 0).arrow)
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasEqualizers C
⊢ Epi (factorThruImageSubobject f)

Tactic:
dsimp [factorThruImageSubobject]
  apply epi_comp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
⊢ (imageSubobject 0).arrow = 0

Tactic:
rw [← imageSubobject_arrow]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
⊢ (imageSubobjectIso 0).hom ≫ image.ι 0 = 0
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
X : C
⊢ ∀ (a : Subobject X), Quotient.mk'' ⊥ ≤ a

Tactic:
by
    refine Quotient.ind' fun f => ?_
    exact ⟨MonoOver.botLE f⟩

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

Goal state before:
pp: case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : LocallySmall.{w, v₁, u₁} C
inst✝¹ : WellPowered.{w, v₁, u₁} C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ ((underlyingIso (widePullbackι s)).hom ≫
        limit.π (wideCospan s) (some ⟨(equivShrink (Subobject A)) f, ⋯⟩) ≫ eqToHom ⋯) ≫
      f.arrow =
    (sInf s).arrow

Tactic:
· dsimp [sInf]
    simp only [Category.assoc, ← underlyingIso_hom_comp_eq_mk,
      Iso.cancel_iso_hom_left]
    convert! limit.w (wideCospan s) (WidePullbackShape.Hom.term _)
    simp

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

Goal state before:
pp: case mp
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E : D ≌ D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
a✝ : L.HasPointwiseRightKanExtensionAt F Y
⊢ L'.HasPointwiseRightKanExtensionAt F Y'

Tactic:
exact hasPointwiseRightKanExtensionAt_of_equivalence L L' F E eL Y Y' e

Goal state after:
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
G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
p : YonedaCollection F X
⊢ op (CostructuredArrow.mk p.fst) = op (CostructuredArrow.mk (map₁ η p).fst)

Tactic:
YonedaCollection.map₁_fst

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
p : YonedaCollection F X
⊢ op (CostructuredArrow.mk p.fst) = op (CostructuredArrow.mk p.fst)
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
f :
  CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
    (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj E
x✝¹ x✝ : Cᵒᵖ
g : x✝¹ ⟶ x✝
x : P.obj x✝¹
⊢ uliftYoneda.{max w v₂, v₁, u₁}.map g.unop ≫ uliftYonedaEquiv.symm x = uliftYonedaEquiv.symm ((hom (P.map g)) x)

Tactic:
uliftYonedaEquiv_symm_map

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
f :
  CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
    (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj E
x✝¹ x✝ : Cᵒᵖ
g : x✝¹ ⟶ x✝
x : P.obj x✝¹
⊢ uliftYoneda.{max w v₂, v₁, u₁}.map g.unop ≫ uliftYonedaEquiv.symm x =
    uliftYoneda.{max v₂ w, v₁, u₁}.map g.unop ≫ uliftYonedaEquiv.symm x
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
⊢ Function.LeftInverse
    (fun x ↦
      match x with
      | none => Arrow.mk (𝟙 zero)
      | some none => Arrow.mk (𝟙 one)
      | some (some t) => Arrow.mk (line t))
    fun f ↦
    match f.left, f.right, f.hom with
    | zero, .(zero), Hom.id .(zero) => none
    | one, .(one), Hom.id .(one) => some none
    | zero, one, line t => some (some t)

Tactic:
rintro ⟨(_ | _), _, (_ | _)⟩

Goal state after:
case zero.id
J : Type w
⊢ (fun x ↦
        match x with
        | none => Arrow.mk (𝟙 zero)
        | some none => Arrow.mk (𝟙 one)
        | some (some t) => Arrow.mk (line t))
      ((fun f ↦
          match f.left, f.right, f.hom with
          | zero, .(zero), Hom.id .(zero) => none
          | one, .(one), Hom.id .(one) => some none
          | zero, one, line t => some (some t))
        { left := zero, right := zero, hom := Hom.id ((𝟭 (WalkingParallelFamily J)).obj zero) }) =
    { left := zero, right := zero, hom := Hom.id ((𝟭 (WalkingParallelFamily J)).obj zero) }

case zero.line
J : Type w
a✝ : J
⊢ (fun x ↦
        match x with
        | none => Arrow.mk (𝟙 zero)
        | some none => Arrow.mk (𝟙 one)
        | some (some t) => Arrow.mk (line t))
      ((fun f ↦
          match f.left, f.right, f.hom with
          | zero, .(zero), Hom.id .(zero) => none
          | one, .(one), Hom.id .(one) => some none
          | zero, one, line t => some (some t))
        { left := zero, right := one, hom := line a✝ }) =
    { left := zero, right := one, hom := line a✝ }

case one.id
J : Type w
⊢ (fun x ↦
        match x with
        | none => Arrow.mk (𝟙 zero)
        | some none => Arrow.mk (𝟙 one)
        | some (some t) => Arrow.mk (line t))
      ((fun f ↦
          match f.left, f.right, f.hom with
          | zero, .(zero), Hom.id .(zero) => none
          | one, .(one), Hom.id .(one) => some none
          | zero, one, line t => some (some t))
        { left := one, right := one, hom := Hom.id ((𝟭 (WalkingParallelFamily J)).obj one) }) =
    { left := one, right := one, hom := Hom.id ((𝟭 (WalkingParallelFamily J)).obj one) }
Module: Mathlib.GroupTheory.Divisible

Goal state before:
pp: A : Type u_1
inst✝ : AddCommGroup A
H : ∀ {n : ℤ}, n ≠ 0 → n • ⊤ = ⊤
a : A
n : ℤ
hn : ¬n = 0
⊢ a ∈ n • ⊤

Tactic:
H hn

Goal state after:
A : Type u_1
inst✝ : AddCommGroup A
H : ∀ {n : ℤ}, n ≠ 0 → n • ⊤ = ⊤
a : A
n : ℤ
hn : ¬n = 0
⊢ a ∈ ⊤
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)
y : N
z1 : R
z2 : ↥(ideal i f y)
⊢ ↑(extensionOfMax i f).toLinearPMap ⟨↑(z1 • z2) • y, ⋯⟩ =
    (RingHom.id R) z1 • ↑(extensionOfMax i f).toLinearPMap ⟨↑z2 • y, ⋯⟩

Tactic:
simp_rw [← (extensionOfMax i f).toLinearPMap.map_smul]
    congr 2
    apply mul_smul

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
h : Baer R Q
f : M →ₗ[R] N
hf : Function.Injective ⇑f
g : M →ₗ[R] Q
this : Fact (Function.Injective ⇑f)
x y : N
⊢ ↑(extensionOfMax f g).toLinearPMap ⟨x + y, ⋯⟩ =
    ↑(extensionOfMax f g).toLinearPMap ⟨x, ⋯⟩ + ↑(extensionOfMax f g).toLinearPMap ⟨y, ⋯⟩

Tactic:
← LinearPMap.map_add

Goal state after:
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
h : Baer R Q
f : M →ₗ[R] N
hf : Function.Injective ⇑f
g : M →ₗ[R] Q
this : Fact (Function.Injective ⇑f)
x y : N
⊢ ↑(extensionOfMax f g).toLinearPMap ⟨x + y, ⋯⟩ = ↑(extensionOfMax f g).toLinearPMap (⟨x, ⋯⟩ + ⟨y, ⋯⟩)
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝² : Ring R
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module R M
inj : Injective R (ULift.{v', v} M)
X Y : Type v
x✝³ : AddCommGroup X
x✝² : AddCommGroup Y
x✝¹ : Module R X
x✝ : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ⇑f
g : X →ₗ[R] M
eX : ULift.{v', v} X ≃ₗ[R] X := ULift.moduleEquiv
⊢ Function.Injective ⇑(↑ULift.moduleEquiv.symm ∘ₗ f ∘ₗ ↑eX)

Tactic:
by exact ULift.moduleEquiv.symm.injective.comp <| hf.comp eX.injective

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

Goal state before:
pp: case pos
a b : ℕ
h : a ∣ b
h' : φ a = φ b
ha : ¬a = 0
hb : b = 0
⊢ a = b ∨ 2 * a = b

Tactic:
hb,

Goal state after:
case pos
a b : ℕ
h : a ∣ b
h' : φ a = φ 0
ha : ¬a = 0
hb : b = 0
⊢ a = b ∨ 2 * a = b
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
z : ℤ
hz : c - b = z • p
⊢ toIcoMod hp a b = toIcoMod hp a c

Tactic:
rw [sub_eq_iff_eq_add] at hz

Goal state after:
case refine_2
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
z : ℤ
hz : c = z • p + b
⊢ toIcoMod hp a b = toIcoMod hp a c
Module: Mathlib.Order.Filter.Lift

Goal state before:
pp: α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
x : Set α₁
⊢ (fun s ↦ (f₂.lift g₂).lift' fun t ↦ s ×ˢ t) = fun t ↦ f₂.lift fun s ↦ (g₂ s).lift' fun t_1 ↦ t ×ˢ t_1

Tactic:
funext y

Goal state after:
α₁ : Type u_5
α₂ : Type u_6
β₁ : Type u_7
β₂ : Type u_8
f₁ : Filter α₁
f₂ : Filter α₂
g₁ : Set α₁ → Filter β₁
g₂ : Set α₂ → Filter β₂
hg₁ : Monotone g₁
hg₂ : Monotone g₂
x : Set α₁
y : Set β₁
⊢ ((f₂.lift g₂).lift' fun t ↦ y ×ˢ t) = f₂.lift fun s ↦ (g₂ s).lift' fun t ↦ y ×ˢ t
Module: Mathlib.Algebra.Order.ToIntervalMod

Goal state before:
pp: case refine_2
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
z : ℤ
hz : c - b = z • p
⊢ toIocMod hp a b = toIocMod hp a c

Tactic:
rw [sub_eq_iff_eq_add] at hz

Goal state after:
case refine_2
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
z : ℤ
hz : c = z • p + b
⊢ toIocMod hp a b = toIocMod hp a 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 c : α
⊢ toIcoMod hp c a = toIcoMod hp c b ↔ a ≡ b [PMOD p]

Tactic:
rw [toIcoMod_eq_toIcoMod, AddCommGroup.modEq_iff_zsmul']

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
F G : Filter X
⊢ ClusterPt x (F ⊔ G) ↔ ClusterPt x F ∨ ClusterPt x G

Tactic:
by
  simp only [ClusterPt, inf_sup_left, sup_neBot]

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝¹ : TopologicalSpace X
x : X
f : Filter X
H : f ≤ 𝓝 x
inst✝ : f.NeBot
⊢ ClusterPt x f

Tactic:
rwa [ClusterPt, inf_eq_right.mpr H]

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

Tactic:
rw [← neg_sub, toIcoMod_neg, neg_zero]

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

Goal state before:
pp: α : Type u_1
inst✝³ : Field α
inst✝² : LinearOrder α
inst✝¹ : IsStrictOrderedRing α
inst✝ : FloorRing α
b : α
⊢ toIcoDiv ⋯ 0 b = ⌊b⌋

Tactic:
by
  simp [toIcoDiv_eq_floor]

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 Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
hg : IsInducing g
⊢ IsInducing (g ∘ f) ↔ IsInducing f

Tactic:
refine ⟨fun h ↦ ?_, hg.comp⟩

Goal state after:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
hg : IsInducing g
h : IsInducing (g ∘ f)
⊢ IsInducing f
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
a : α
f : Filter α
t : TopologicalSpace α
⊢ t ≤ nhdsAdjoint a f ↔ 𝓝 a ≤ pure a ⊔ f ∧ ∀ (b : α), b ≠ a → IsOpen[t] {b}

Tactic:
simp only [le_nhdsAdjoint_iff', @isOpen_singleton_iff_nhds_eq_pure α t]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
⊢ ContinuousOn f s ↔ Continuous[instTopologicalSpaceSubtype, inst✝] (s.domRestrict f)

Tactic:
rw [ContinuousOn, continuous_iff_continuousAt]; constructor
  · rintro h ⟨x, xs⟩
    exact (continuousWithinAt_iff_continuousAt_domRestrict f xs).mp (h x xs)
  intro h x xs
  exact (continuousWithinAt_iff_continuousAt_domRestrict f xs).mpr (h ⟨x, xs⟩)

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ 𝓝ˢ[univ] s = 𝓝ˢ s

Tactic:
by
  simp [nhdsSetWithin]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ 𝓝ˢ[s] univ = 𝓟 s

Tactic:
by
  simp [nhdsSetWithin]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ 𝓝ˢ[∅] s = ⊥

Tactic:
by
  simp [nhdsSetWithin]

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ 𝓝ˢ[s] ∅ = ⊥

Tactic:
by
  simp [nhdsSetWithin]

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
⊢ IsClosedMap (Sum.elim f g) ↔ IsClosedMap f ∧ IsClosedMap g

Tactic:
simp only [isClosedMap_sum, Sum.elim_inl, Sum.elim_inr]

Goal state after:
Module: Mathlib.Topology.Bases

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

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

Goal state after:
Module: Mathlib.Order.SetAccumulate

Goal state before:
pp: β : Type u_2
s : ℕ → Set β
⊢ accumulate s 0 = s 0

Tactic:
by
  simp [accumulate_def]

Goal state after:
Module: Mathlib.Topology.ContinuousOn

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_5
s : ι → Set α
hf : ∀ (i : ι), ContinuousOn f (s i)
hs : ∀ (i : ι), IsOpen[inst✝¹] (s i)
⊢ ContinuousOn f (⋃ i, s i)

Tactic:
rintro x ⟨si, ⟨i, rfl⟩, hxsi⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_5
s : ι → Set α
hf : ∀ (i : ι), ContinuousOn f (s i)
hs : ∀ (i : ι), IsOpen[inst✝¹] (s i)
x : α
i : ι
hxsi : x ∈ (fun i ↦ s i) i
⊢ ContinuousWithinAt f (⋃ i, s i) x
Module: Mathlib.Topology.Bases

Goal state before:
pp: α : Type u
t : TopologicalSpace α
inst✝ : SecondCountableTopology α
f : α → Set α
hf : ∀ (x : α), f x ∈ 𝓝 x
s : Set α
hsc : s.Countable
hsU : ⋃ i ∈ s, interior (f i) = ⋃ i, interior (f i)
⊢ ∀ (x : α), ∃ i, x ∈ interior (f i)

Tactic:
exact fun x => ⟨x, mem_interior_iff_mem_nhds.2 (hf x)⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
f : α → β
⊢ Tendsto (fun x ↦ f '' x) la.smallSets lb.smallSets ↔ Tendsto f la lb

Tactic:
tendsto_smallSets_iff

Goal state after:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
f : α → β
⊢ (∀ t ∈ lb, ∀ᶠ (x : Set α) in la.smallSets, f '' x ⊆ t) ↔ Tendsto f la lb
Module: Mathlib.Order.Filter.SmallSets

Goal state before:
pp: α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
s t : α → Set β
ht : Tendsto t la lb.smallSets
hst : ∀ᶠ (x : α) in la, s x ⊆ t x
⊢ Tendsto s la lb.smallSets

Tactic:
tendsto_smallSets_iff

Goal state after:
α : Type u_1
β : Type u_2
la : Filter α
lb : Filter β
s t : α → Set β
ht : ∀ t_1 ∈ lb, ∀ᶠ (x : α) in la, t x ⊆ t_1
hst : ∀ᶠ (x : α) in la, s x ⊆ t x
⊢ ∀ t ∈ lb, ∀ᶠ (x : α) in la, s x ⊆ t
Module: Mathlib.Topology.Compactness.SigmaCompact

Goal state before:
pp: case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
K : CompactExhaustion X
s : Set X
hs : IsCompact s
⊢ Directed (fun x1 x2 ↦ x1 ⊆ x2) (interior ∘ ⇑K)

Tactic:
· exact Monotone.directed_le fun _ _ h ↦ interior_mono <| K.subset h

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

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsCompact t
b : Bool
⊢ IsCompact (bif b then s else t)

Tactic:
cases b <;> assumption

Goal state after: