mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁶ : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝⁵ : HasCokernel f
inst✝⁴ : HasCokernel (G.map f)
inst✝³ : PreservesColimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasCokernel g
inst✝¹ : HasCokernel (G.map g)
inst✝ : PreservesColimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯ ≫ cokernelComparison g G =
    (PreservesCokernel.iso G f).inv ≫ G.map (cokernel.map f g p q hpq)

Tactic:
cokernel_map_comp_cokernelComparison,

Goal state after:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁶ : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝⁵ : HasCokernel f
inst✝⁴ : HasCokernel (G.map f)
inst✝³ : PreservesColimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasCokernel g
inst✝¹ : HasCokernel (G.map g)
inst✝ : PreservesColimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ cokernelComparison f G ≫ G.map (cokernel.map f g p q ?hpq) =
    (PreservesCokernel.iso G f).inv ≫ G.map (cokernel.map f g p q hpq)

case hpq
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁶ : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝⁵ : HasCokernel f
inst✝⁴ : HasCokernel (G.map f)
inst✝³ : PreservesColimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasCokernel g
inst✝¹ : HasCokernel (G.map g)
inst✝ : PreservesColimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ f ≫ q = p ≫ g
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hlp : prod.lift (𝟙 A) 0 ≫ prod.snd = 0
hp1 : IsLimit (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) :=
  Fork.IsLimit.mk (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) (fun s ↦ s.ι ≫ prod.fst) ⋯ ⋯
hp2 : IsColimit (CokernelCofork.ofπ prod.snd hlp) := epiIsCokernelOfKernel (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) hp1
⊢ Epi (r A)

Tactic:
apply NormalMonoCategory.epi_of_zero_cancel

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
A : C
hlp : prod.lift (𝟙 A) 0 ≫ prod.snd = 0
hp1 : IsLimit (KernelFork.ofι (prod.lift (𝟙 A) 0) hlp) := ⋯
hp2 : IsColimit (CokernelCofork.ofπ prod.snd hlp) := ⋯
⊢ ∀ (Z : C) (g : cokernel (diag A) ⟶ Z), r A ≫ g = 0 → g = 0
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c d : X ⟶ Y
⊢ a - c - (b - d) = a - b - (c - d)

Tactic:
rw [sub_def, ← lift_sub_lift, sub_def, Category.assoc, σ_comp, prod.lift_map_assoc]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c d : X ⟶ Y
⊢ prod.lift (prod.lift a b ≫ σ) (prod.lift c d ≫ σ) ≫ σ = a - b - (c - d)
Module: Mathlib.CategoryTheory.Abelian.NonPreadditive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ -a - b = -b - a

Tactic:
by
  conv_lhs => rw [neg_def, ← sub_zero b, sub_sub_sub, sub_zero, ← neg_def]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ a - - -b = a - b

Tactic:
neg_neg

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b : X ⟶ Y
⊢ a - b = a - b
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteCoproducts C
inst✝¹ : HasCokernels C
inst✝ : IsNormalEpiCategory C
X Y : C
f g : X ⟶ Y
huv : pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) = pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)
hvu :
  f ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) =
    g ≫ pushout.inr (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)
huu :
  f ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g) =
    g ≫ pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)
s : Cofork f g
⊢ (Cofork.ofπ (pushout.inl (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)) huu).π ≫ pushout.desc s.π s.π ⋯ = s.π

Tactic:
simp only [pushout.inl_desc, Cofork.π_ofπ]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c : X ⟶ Y
⊢ a + (- -b + c) = a + (b + c)

Tactic:
neg_neg

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y : C
a b c : X ⟶ Y
⊢ a + (b + c) = a + (b + c)
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasKernels C
inst✝² : HasCokernels C
inst✝¹ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (coimageImageComparison f)
inst✝ : HasFiniteProducts C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
m : Mono f
⊢ IsLimit (KernelFork.ofι f ⋯)

Tactic:
haveI : Limits.HasImages C := hasImages
        haveI : HasEqualizers C := Preadditive.hasEqualizers_of_hasKernels
        haveI : HasZeroObject C := Limits.hasZeroObject_of_hasFiniteBiproducts _
        have aux (s : KernelFork (cokernel.π f)) :
            (limit.lift (parallelPair (cokernel.π f) 0) s ≫ inv (imageMonoFactorisation f).e) ≫
            Fork.ι (KernelFork.ofι _ (cokernel.condition f)) = Fork.ι s := ?_
        · refine isLimitAux _ (fun A => limit.lift _ _ ≫ inv (imageMonoFactorisation f).e) aux ?_
          intro A g hg
          rw [KernelFork.ι_ofι] at hg
          rw [← cancel_mono f, hg, ← aux, KernelFork.ι_ofι]
        · simp only [KernelFork.ι_ofι, Category.assoc]
          convert! limit.lift_π s WalkingParallelPair.zero using 2
          rw [IsIso.inv_comp_eq, eq_comm]
          exact (imageMonoFactorisation f).fac

Goal state after:
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
⊢ (Equiv.symm τ) ∞ = fromCoset ⟨↑(Hom.hom f).range, ⋯⟩

Tactic:
rw [tau, Equiv.symm_swap, Equiv.swap_apply_right]

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

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
eq₂ : ∀ (j : J), (π₂.mapCocone c).ι.app j ≫ h₂.desc (π₂.mapCocone s) = (π₂.mapCocone s).ι.app j
eq₃ : ∀ (j : J), (π₃.mapCocone c).ι.app j ≫ h₃.desc (π₃.mapCocone s) = (π₃.mapCocone s).ι.app j
eq₂₃ : ∀ (j : J), (c.ι.app j).τ₂ ≫ (((const J).obj c.pt).obj j).g = (F.obj j).g ≫ (c.ι.app j).τ₃
⊢ (π₂.mapCocone c).ι.app j ≫ h₂.desc (π₂.mapCocone s) ≫ s.pt.g =
    (π₂.mapCocone c).ι.app j ≫ c.pt.g ≫ h₃.desc (π₃.mapCocone s)

Tactic:
have eq₂₃' := fun j => (s.ι.app j).comm₂₃

Goal state after:
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
eq₂ : ∀ (j : J), (π₂.mapCocone c).ι.app j ≫ h₂.desc (π₂.mapCocone s) = (π₂.mapCocone s).ι.app j
eq₃ : ∀ (j : J), (π₃.mapCocone c).ι.app j ≫ h₃.desc (π₃.mapCocone s) = (π₃.mapCocone s).ι.app j
eq₂₃ : ∀ (j : J), (c.ι.app j).τ₂ ≫ (((const J).obj c.pt).obj j).g = (F.obj j).g ≫ (c.ι.app j).τ₃
eq₂₃' : ∀ (j : J), (s.ι.app j).τ₂ ≫ (((const J).obj s.pt).obj j).g = (F.obj j).g ≫ (s.ι.app j).τ₃
⊢ (π₂.mapCocone c).ι.app j ≫ h₂.desc (π₂.mapCocone s) ≫ s.pt.g =
    (π₂.mapCocone c).ι.app j ≫ c.pt.g ≫ h₃.desc (π₃.mapCocone s)
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₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ homologyMap (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) = 0

Tactic:
by
  apply homologyMap'_nullHomotopic

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 : ShortComplex C
inst✝ : S.HasLeftHomology
A : C
k k' : A ⟶ S.X₂
hk : k ≫ S.g = 0
hk' : k' ≫ S.g = 0
⊢ S.liftCycles k hk - S.liftCycles k' hk' = S.liftCycles (k - k') ⋯

Tactic:
by
  simp only [← cancel_mono S.iCycles, liftCycles_i, sub_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✝¹ : Preadditive C
S : ShortComplex C
hS : IsColimit (CokernelCofork.ofπ S.g ⋯)
inst✝ : S.HasHomology
⊢ S.fromOpcycles ≫ hS.desc (CokernelCofork.ofπ S.pOpcycles ⋯) = 𝟙 S.opcycles

Tactic:
rw [← cancel_epi S.pOpcycles, p_fromOpcycles_assoc, comp_id]
          exact Cofork.IsColimit.π_desc hS

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
x : Subobject X
⊢ (pullback f).obj x = mk (pullback.snd x.arrow f)

Tactic:
obtain ⟨Z, i, _, rfl⟩ := mk_surjective x

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y : C
f : Y ⟶ X
Z : C
i : Z ⟶ X
w✝ : Mono i
⊢ (pullback f).obj (mk i) = mk (pullback.snd (mk i).arrow f)
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
this✝ : HasBinaryBiproducts C
this : HasEqualizers C
⊢ F.map (𝟙 0) = 0

Tactic:
id_zero,

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
this : HasEqualizers C
⊢ F.map 0 = 0
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✝¹ : HasFiniteCoproducts C
inst✝ : HasCokernels C
this✝¹ : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
this✝ : HasBinaryBiproducts C
this : HasCoequalizers C
⊢ F.map (𝟙 0) = 0

Tactic:
id_zero,

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✝¹ : HasFiniteCoproducts C
inst✝ : HasCokernels C
this✝¹ : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
this✝ : HasBinaryBiproducts C
this : HasCoequalizers C
⊢ F.map 0 = 0
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
α : Type w
inst✝² : HasFiniteCoproducts C
inst✝¹ : HasColimitsOfShape (Finset (Discrete α)) C
inst✝ : HasColimitsOfShape (Discrete α) C
X✝ Y✝ : Discrete α ⥤ C
β : X✝ ⟶ Y✝
⊢ (liftToFinset C α ⋙ colim).map β ≫ (colimit.isoColimitCocone (liftToFinsetColimitCocone Y✝)).symm.hom =
    (colimit.isoColimitCocone (liftToFinsetColimitCocone X✝)).symm.hom ≫ colim.map β

Tactic:
simp only [Functor.comp_obj, colim_obj, Functor.comp_map, colim_map, Iso.symm_hom]
      ext J
      simp only [liftToFinset_obj_obj]
      ext j
      simp [liftToFinset, liftToFinsetColimIso_aux, liftToFinsetColimIso_aux_assoc]

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

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
L : C ⥤ D
H : Type u_3
inst✝³ : Category.{v_3, u_3} H
G : C ⥤ H
inst✝² : L.HasPointwiseLeftKanExtension G
inst✝¹ : HasColimitsOfShape D H
inst✝ : HasColimitsOfShape C H
X : Grothendieck (CostructuredArrow.functor L)
⊢ colimit.ι (CostructuredArrow.grothendieckProj L ⋙ G) X ≫ (L.colimitIsoColimitGrothendieck G).inv =
    colimit.ι G ((CostructuredArrow.proj L X.base).obj X.fiber)

Tactic:
simp [colimitIsoColimitGrothendieck]

Goal state after:
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' : D ⥤ H
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
inst✝² : F'.IsLeftKanExtension α
inst✝¹ : HasColimit F
inst✝ : HasColimit F'
i : C
⊢ colimit.ι F i ≫ (F'.colimitIsoOfIsLeftKanExtension α).inv = α.app i ≫ colimit.ι F' (L.obj i)

Tactic:
rw [Iso.comp_inv_eq, assoc, ι_colimitIsoOfIsLeftKanExtension_hom]

Goal state after:
Module: Mathlib.Algebra.Category.Grp.AB

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS : S.Exact
⊢ (S.map colim).Exact

Tactic:
replace hS := fun j => hS.map ((evaluation _ _).obj j)

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS : ∀ (j : J), (S.map ((evaluation J AddCommGrpCat).obj j)).Exact
⊢ (S.map colim).Exact
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
c : CofanTypes F
hc : Functor.CoconeTypes.IsColimit c
i₁ i₂ : C
y₁ : F i₁
y₂ : F i₂
x✝ : ∃ (h : i₁ = i₂), y₂ = cast ⋯ y₁
h₁ : i₁ = i₂
h₂ : y₂ = cast ⋯ y₁
⊢ c.inj i₁ y₁ = c.inj i₂ y₂

Tactic:
by subst h₁ h₂; rfl

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

Goal state before:
pp: case neg
n₁ n₂ : ℤ
h₂ : Odd n₂
⊢ Odd n₁ ↔ (Even n₁ ↔ Even n₂)

Tactic:
← Int.not_odd_iff_even,

Goal state after:
case neg
n₁ n₂ : ℤ
h₂ : Odd n₂
⊢ Odd n₁ ↔ (¬Odd n₁ ↔ Even n₂)
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: case ofNat
R : Type u_1
inst✝ : Ring R
n : ℕ
⊢ ↑↑(ofNat n).negOnePow = (-1) ^ (ofNat n).natAbs

Tactic:
| ofNat n =>

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

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

Tactic:
simpa only [sub_eq_neg_add] using h (-x)

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

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

Tactic:
simpa only [sub_eq_neg_add] using h (-x)

Goal state after:
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁷ : Ring R
Q : Type v
inst✝⁶ : AddCommGroup Q
inst✝⁵ : Module R Q
M : Type u_1
N : Type u_2
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
r : R
x : ↥i.range
eq1 : i (r • Exists.choose ⋯) = i (Exists.choose ⋯)
⊢ f (r • Exists.choose ⋯) = r • f (Exists.choose ⋯)

Tactic:
map_smul

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
i : M →ₗ[R] N
f : M →ₗ[R] Q
inst✝ : Fact (Function.Injective ⇑i)
r : R
x : ↥i.range
eq1 : i (r • Exists.choose ⋯) = i (Exists.choose ⋯)
⊢ r • f (Exists.choose ⋯) = r • f (Exists.choose ⋯)
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
⊢ 1 < b

Tactic:
have : a * b ^ m < a * b ^ (m + 1) := hx.1.1.trans_lt hx.1.2

Goal state after:
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedMonoid α
a b : α
m n : ℤ
hmn : m ≠ n
x : α
hx : x ∈ Ico (a * b ^ m) (a * b ^ (m + 1)) ∩ Ico (a * b ^ n) (a * b ^ (n + 1))
this : a * b ^ m < a * b ^ (m + 1)
⊢ 1 < b
Module: Mathlib.Data.Nat.Factorization.Induction

Goal state before:
pp: a✝ b m n p : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a : ℕ
⊢ (p n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)

Tactic:
p

Goal state after:
a✝ b m n p✝ : ℕ
motive : ℕ → Sort u_1
prime_pow : (p n : ℕ) → Prime p → 0 < n → motive (p ^ n)
zero : motive 0
one : motive 1
coprime : (a b : ℕ) → 1 < a → 1 < b → a.Coprime b → motive a → motive b → motive (a * b)
a p : ℕ
⊢ (n : ℕ) → Prime p → ¬p ∣ a → 0 < n → motive a → motive (p ^ n * a)
Module: Mathlib.Data.Nat.Count

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
a k : ℕ
h : 0 < count (fun k ↦ p (a + k)) (k + 1)
t : ℕ
ht : t < k + 1
hp : p (a + t)
⊢ ∃ x, (a ≤ x ∧ x < a + k + 1) ∧ p x

Tactic:
exact ⟨a + t, by grind⟩

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Prod

Goal state before:
pp: α : Type u_3
γ : Type u_5
inst✝¹ : Preorder α
inst✝ : Preorder γ
f g : α → γ
hf : Tendsto f atTop atTop
hg : Tendsto g atTop atTop
⊢ Tendsto (Prod.map f g) atTop atTop

Tactic:
rw [← prod_atTop_atTop_eq]
  exact hf.prod_map_prod_atTop hg

Goal state after:
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: c d : ℕ
⊢ ∀ (b : ℕ), 2 * (c ^ 2 + d + 1) ≤ b → c ^ b < (b - d)!

Tactic:
intro n

Goal state after:
c d n : ℕ
⊢ 2 * (c ^ 2 + d + 1) ≤ n → c ^ n < (n - d)!
Module: Mathlib.Order.Filter.AtTopBot.CountablyGenerated

Goal state before:
pp: α : Type u_1
f : Filter α
inst✝¹ : f.IsCountablyGenerated
inst✝ : f.NeBot
⊢ ∃ x, Tendsto x atTop f

Tactic:
obtain ⟨B, h⟩ := f.exists_antitone_basis

Goal state after:
α : Type u_1
f : Filter α
inst✝¹ : f.IsCountablyGenerated
inst✝ : f.NeBot
B : ℕ → Set α
h : f.HasAntitoneBasis B
⊢ ∃ x, Tendsto x atTop f
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: a c d n : ℕ
hn : (a * c) ^ n < (n - d)!
hn0 : 0 < n
⊢ a * c ^ n < (n - d)!

Tactic:
mul_pow

Goal state after:
a c d n : ℕ
hn : a ^ n * c ^ n < (n - d)!
hn0 : 0 < n
⊢ a * c ^ n < (n - d)!
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 : α
⊢ b - toIocMod hp a b = toIocDiv hp a b • p

Tactic:
rw [toIocMod, sub_sub_cancel]

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

Goal state before:
pp: α : Type u_1
γ : Type u_3
ι : Type u_6
p : ι → Prop
s : ι → Set α
f : Filter α
hf : f.HasBasis p s
β : ι → Type u_5
pg : (i : ι) → β i → Prop
sg : (i : ι) → β i → Set γ
g : Set α → Filter γ
hg : ∀ (i : ι), (g (s i)).HasBasis (pg i) (sg i)
gm : Monotone g
⊢ (f.lift g).HasBasis (fun i ↦ p i.fst ∧ pg i.fst i.snd) fun i ↦ sg i.fst i.snd

Tactic:
refine ⟨fun t => (hf.mem_lift_iff hg gm).trans ?_⟩
  simp [Sigma.exists, and_assoc, exists_and_left]

Goal state after:
Module: Mathlib.Topology.Basic

Goal state before:
pp: X : Type u
α : Type u_1
inst✝ : TopologicalSpace X
s : Set α
f : α → Set X
hs : s.Finite
h : ∀ i ∈ s, IsClosed[inst✝] (f i)
⊢ IsClosed[inst✝] (⋃ i ∈ s, f i)

Tactic:
simp only [← isOpen_compl_iff, compl_iUnion] at *
  exact hs.isOpen_biInter h

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClosed (frontier s)

Tactic:
rw [frontier_eq_closure_inter_closure]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ IsClosed (closure s ∩ closure sᶜ)
Module: Mathlib.Topology.Continuous

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
α : Type u_4
f : α → X
s : Set X
hf : DenseRange f
hs : IsOpen[inst✝] s
⊢ s ⊆ closure[inst✝] (f '' f ⁻¹' s)

Tactic:
by
  rw [image_preimage_eq_inter_range]
  exact hf.open_subset_closure_inter hs

Goal state after:
Module: Mathlib.Topology.ClusterPt

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x : X
F : Filter X
⊢ AccPt x F ↔ ClusterPt x (𝓟 {x}ᶜ ⊓ F)

Tactic:
rw [AccPt, nhdsWithin, ClusterPt, inf_assoc]

Goal state after:
Module: Mathlib.Topology.NhdsSet

Goal state before:
pp: X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
⊢ t ⊆ (closure[inst✝] s)ᶜ ↔ Disjoint (closure[inst✝] s) t

Tactic:
subset_compl_iff_disjoint_left

Goal state after:
X : Type u_2
inst✝ : TopologicalSpace X
s t : Set X
⊢ Disjoint (closure[inst✝] s) t ↔ Disjoint (closure[inst✝] s) t
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace β
s : Set α
f : α → β
⊢ IsClosed[TopologicalSpace.induced f t] s ↔ ∃ t_1, IsClosed[t] t_1 ∧ f ⁻¹' t_1 = s

Tactic:
let := t.induced f

Goal state after:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
s : Set α
f : α → β
this : TopologicalSpace α := TopologicalSpace.induced f t
⊢ IsClosed[TopologicalSpace.induced f t] s ↔ ∃ t_1, IsClosed[t] t_1 ∧ f ⁻¹' t_1 = s
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
t : TopologicalSpace β
f : α → β
s : Set α
⊢ IsClosed[induced f t] s ↔ ∀ (a : α), f a ∈ closure[t] (f '' s) → a ∈ s

Tactic:
by
  simp only [← closure_subset_iff_isClosed, subset_def, closure_induced]

Goal state after:
Module: Mathlib.Topology.Order

Goal state before:
pp: α : Type u
s : Set α
T : Set (TopologicalSpace α)
⊢ IsClosed[sSup T] s ↔ ∀ t ∈ T, IsClosed s

Tactic:
simp +instances only [sSup_eq_iSup, isClosed_iSup_iff]

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 → Y → Z
x : X
y : Y
s : Set X
t : Set Y
u : Set Z
hf : Continuous[instTopologicalSpaceProd, inst✝] (uncurry f)
hx : x ∈ closure[inst✝²] s
hy : y ∈ closure[inst✝¹] t
h : ∀ a ∈ s, ∀ b ∈ t, f a b ∈ u
⊢ (x, y) ∈ closure[instTopologicalSpaceProd] (s ×ˢ t)

Tactic:
by simpa only [closure_prod_eq] using mk_mem_prod hx hy

Goal state after:
Module: Mathlib.Topology.NhdsWithin

Goal state before:
pp: α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s u : Set α
⊢ u ∈ 𝓝ˢ s ↔ ∃ v ∈ 𝓝ˢ (f '' s), f ⁻¹' v ⊆ u

Tactic:
let := t.induced f

Goal state after:
α : Type u_5
β : Type u_6
t : TopologicalSpace β
f : α → β
s u : Set α
this : TopologicalSpace α := TopologicalSpace.induced f t
⊢ u ∈ 𝓝ˢ s ↔ ∃ v ∈ 𝓝ˢ (f '' s), f ⁻¹' v ⊆ u
Module: Mathlib.Topology.Constructions

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hst : s ⊆ t
⊢ t ⊆ closure[inst✝] ↑(range (inclusion hst)) ↔ t ⊆ closure[inst✝] s

Tactic:
← range_comp,

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hst : s ⊆ t
⊢ t ⊆ closure[inst✝] (range (Subtype.val ∘ inclusion hst)) ↔ t ⊆ closure[inst✝] s
Module: Mathlib.Topology.Constructions.SumProd

Goal state before:
pp: case e'_3
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 : IsInducing f
hg : IsInducing g
hFg : Disjoint (𝓟 (range f)) (𝓝ˢ (range g))
hfG : Disjoint (𝓝ˢ (range f)) (𝓟 (range g))
x : X
⊢ Disjoint (𝓝 (f x)) (𝓟 (range g))

Tactic:
exact hfG.mono_left (nhds_le_nhdsSet (mem_range_self x))

Goal state after:
Module: Mathlib.Topology.Bornology.Basic

Goal state before:
pp: α : Type u_2
x✝ : Bornology α
s : Set α
h : ¬IsBounded s
⊢ s.Nonempty

Tactic:
rw [nonempty_iff_ne_empty]

Goal state after:
α : Type u_2
x✝ : Bornology α
s : Set α
h : ¬IsBounded s
⊢ s ≠ ∅