mathlib-initiative/mathlib-tactics huggingface dataset:
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
inst✝³ : L.Full
inst✝² : L.Faithful
F : C ⥤ H
inst✝¹ : L.HasPointwiseRightKanExtension F
inst✝ : ∀ (F : C ⥤ H), L.HasRightKanExtension F
⊢ IsIso (L.ranCounit.app F)

Tactic:
infer_instance

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

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

Tactic:
intro

Goal state after:
case mp
C : Type u_1
H : Type u_3
D : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
φ : F' ⟶ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft φ = α'
inst✝ : F'.IsLeftKanExtension α
a✝ : F''.IsLeftKanExtension α'
⊢ IsIso φ
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case mp
C : Type u_1
H : Type u_3
D : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
φ : F' ⟶ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft φ = α'
inst✝ : F'.IsLeftKanExtension α
a✝ : F''.IsLeftKanExtension α'
⊢ IsIso (F'.leftKanExtensionUnique α F'' α').hom

Tactic:
infer_instance

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

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

Tactic:
intro

Goal state after:
case mpr
C : Type u_1
H : Type u_3
D : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
φ : F' ⟶ F''
L : C ⥤ D
F : C ⥤ H
α : F ⟶ L ⋙ F'
α' : F ⟶ L ⋙ F''
comm : α ≫ L.whiskerLeft φ = α'
inst✝ : F'.IsLeftKanExtension α
a✝ : IsIso φ
⊢ F''.IsLeftKanExtension α'
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: case pos
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasCountableCoproducts C
inst✝³ : HasFiniteLimits C
inst✝² : ∀ (J : Type) [inst : Finite J], HasExactColimitsOfShape (Discrete J) C
inst✝¹ : HasExactColimitsOfShape (Discrete ℕ) C
J : Type
inst✝ : Countable J
h : Finite J
⊢ HasExactColimitsOfShape (Discrete J) C

Tactic:
infer_instance

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

Goal state before:
pp: case pos
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasCountableProducts C
inst✝³ : HasFiniteColimits C
inst✝² : ∀ (J : Type) [inst : Finite J], HasExactLimitsOfShape (Discrete J) C
inst✝¹ : HasExactLimitsOfShape (Discrete ℕ) C
J : Type
inst✝ : Countable J
h : Finite J
⊢ HasExactLimitsOfShape (Discrete J) C

Tactic:
infer_instance

Goal state after:
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
P : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{v₁, v₁, u₁} P
inst✝ : LocallySmall.{v₁, v₂, u₂} D
this : P.inverseImage (proj S T) = ObjectProperty.ofObj fun f ↦ mk f.snd
⊢ ObjectProperty.Small.{v₁, v₁, max u₁ v₂} (ObjectProperty.ofObj fun f ↦ mk f.snd)

Tactic:
infer_instance

Goal state after:
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 : C ⥤ D
T : D
P : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{v₁, v₁, u₁} P
inst✝ : LocallySmall.{v₁, v₂, u₂} D
this : P.inverseImage (proj S T) = ObjectProperty.ofObj fun f ↦ mk f.snd
⊢ ObjectProperty.Small.{v₁, v₁, max u₁ v₂} (ObjectProperty.ofObj fun f ↦ mk f.snd)

Tactic:
infer_instance

Goal state after:
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 : ℰᵒᵖ ⥤ Type (max w v₁ v₂)
inst✝ : HasColimitsOfSize.{v₁, max u₁ v₁ v₂ w, v₂, u₂} ℰ
⊢ uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasFiniteProducts C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝¹ : G.PreservesZeroMorphisms
inst✝ : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
this✝¹ : HasKernels C
this✝ : HasCokernels C
X Y : C
f : X ⟶ Y
arrowIso : Arrow.mk (G.map (F.map f)) ≅ Arrow.mk f := ((Functor.mapArrowFunctor C C).mapIso i).app (Arrow.mk f)
this : PreservesColimits G
iso : Arrow.mk (G.map (Abelian.coimageImageComparison (F.map f))) ≅ Arrow.mk (Abelian.coimageImageComparison f) :=
  Abelian.PreservesCoimageImageComparison.iso G (F.map f) ≪≫ Abelian.coimageImageComparisonFunctor.mapIso arrowIso
⊢ IsIso (G.map (Abelian.coimageImageComparison (F.map f)))

Tactic:
infer_instance

Goal state after:
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✝ : ℰᵒᵖ ⥤ Type (max w v₁ v₂)
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst✝ : L.IsLeftKanExtension α
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
X Y : ℰ
f : L.obj P ⟶ X
g : X ⟶ Y
this :
  ∀ {W W' : ℰ}
    (f :
      CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
        (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj W)
    (g : W ⟶ W'),
    (IsColimit.homEquiv (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P)).symm
        (f ≫ (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).map g) =
      (IsColimit.homEquiv (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P)).symm f ≫ g
⊢ ∀ (j : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P),
    ((Functor.LeftExtension.mk L α).coconeAt P).ι.app j ≫
        (restrictedULiftYonedaHomEquiv L α P Y).symm ((restrictedULiftYonedaHomEquiv L α P Y) (f ≫ g)) =
      ((Functor.LeftExtension.mk L α).coconeAt P).ι.app j ≫
        (restrictedULiftYonedaHomEquiv L α P Y).symm
          ((restrictedULiftYonedaHomEquiv L α P X) f ≫ (restrictedULiftYoneda A).map g)

Tactic:
intro

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝² : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P✝ : ℰᵒᵖ ⥤ Type (max w v₁ v₂)
inst✝¹ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
inst✝ : L.IsLeftKanExtension α
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
X Y : ℰ
f : L.obj P ⟶ X
g : X ⟶ Y
this :
  ∀ {W W' : ℰ}
    (f :
      CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
        (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj W)
    (g : W ⟶ W'),
    (IsColimit.homEquiv (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P)).symm
        (f ≫ (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).map g) =
      (IsColimit.homEquiv (Functor.isPointwiseLeftKanExtensionOfIsLeftKanExtension L α P)).symm f ≫ g
j✝ : CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P
⊢ ((Functor.LeftExtension.mk L α).coconeAt P).ι.app j✝ ≫
      (restrictedULiftYonedaHomEquiv L α P Y).symm ((restrictedULiftYonedaHomEquiv L α P Y) (f ≫ g)) =
    ((Functor.LeftExtension.mk L α).coconeAt P).ι.app j✝ ≫
      (restrictedULiftYonedaHomEquiv L α P Y).symm
        ((restrictedULiftYonedaHomEquiv L α P X) f ≫ (restrictedULiftYoneda A).map g)
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝¹ : Category.{v₂, u₂} ℰ
A✝ A : C ⥤ ℰ
inst✝ : HasColimitsOfSize.{v₁, max w u₁ v₁ v₂, v₂, u₂} ℰ
⊢ uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A

Tactic:
infer_instance

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

Goal state before:
pp: case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝¹ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
inst✝ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
⊢ L.IsLeftKanExtension α →
    IsIso α ∧
      PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
          max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
        L

Tactic:
intro

Goal state after:
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝¹ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
inst✝ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
a✝ : L.IsLeftKanExtension α
⊢ IsIso α ∧
    PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
        max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
      L
Module: Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
⊢ HasInitial C

Tactic:
have : ∀ X : C, Unique (wideEqualizer (id : endos → endos) ⟶ X) := by
    intro X
    refine ⟨⟨i ≫ Classical.choice (hT X)⟩, fun a => ?_⟩
    let E := equalizer a (i ≫ Classical.choice (hT _))
    let e : E ⟶ wideEqualizer id := equalizer.ι _ _
    let h : T ⟶ E := Classical.choice (hT E)
    have : ((i ≫ h) ≫ e) ≫ i = i ≫ 𝟙 _ := by
      rw [Category.assoc, Category.assoc]
      apply wideEqualizer.condition (id : endos → endos) (h ≫ e ≫ i)
    rw [Category.comp_id, cancel_mono_id i] at this
    have : IsSplitEpi e := IsSplitEpi.mk' ⟨i ≫ h, this⟩
    rw [← cancel_epi e]
    apply equalizer.condition

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this✝ : Nonempty endos
this : (X : C) → Unique (wideEqualizer id ⟶ X)
⊢ HasInitial C
Module: Mathlib.CategoryTheory.Generator.Basic

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✝¹ : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this✝¹ : HasFiniteLimits C
this✝ : HasProductsOfShape (Subtype P) C
this : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
⊢ HasInitial C

Tactic:
let := completeLatticeOfCompleteSemilatticeInf (Subobject (piObj (Subtype.val : Subtype P → C)))

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this✝² : HasFiniteLimits C
this✝¹ : HasProductsOfShape (Subtype P) C
this✝ : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this : CompleteLattice (Subobject (∏ᶜ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ᶜ Subtype.val))
⊢ HasInitial C
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono

Goal state before:
pp: K : Type u
inst✝⁵ : Category.{v, u} K
C : Type u'
inst✝⁴ : Category.{v', u'} C
D : Type u''
inst✝³ : Category.{v'', u''} D
F G : K ⥤ C
f : F ⟶ G
inst✝² : HasPullbacks C
inst✝¹ : Mono f
H : C ⥤ D
inst✝ : H.PreservesMonomorphisms
X✝ : K
⊢ Mono (H.map (f.app X✝))

Tactic:
infer_instance

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

Goal state before:
pp: K : Type u
inst✝⁴ : Category.{v, u} K
C : Type u'
inst✝³ : Category.{v', u'} C
D : Type u''
inst✝² : Category.{v'', u''} D
F✝ G : K ⥤ C
f✝ : F✝ ⟶ G
inst✝¹ : HasPullbacks C
F : C ⥤ D
inst✝ : F.PreservesMonomorphisms
X✝ Y✝ : K ⥤ C
f : X✝ ⟶ Y✝
x✝ : Mono f
⊢ Mono (whiskerRight f F)

Tactic:
infer_instance

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

Goal state before:
pp: K : Type u
inst✝⁵ : Category.{v, u} K
C : Type u'
inst✝⁴ : Category.{v', u'} C
D : Type u''
inst✝³ : Category.{v'', u''} D
F G : K ⥤ C
f : F ⟶ G
inst✝² : HasPushouts C
inst✝¹ : Epi f
H : C ⥤ D
inst✝ : H.PreservesEpimorphisms
X✝ : K
⊢ Epi (H.map (f.app X✝))

Tactic:
infer_instance

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

Goal state before:
pp: case h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS :
  ∀ (j : J),
    (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).g).ker ≤
      (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).f).range
j : J
y : ToType (S.X₂.obj j)
hx :
  (ConcreteCategory.hom (colimit.ι S.X₃ j)) ((ConcreteCategory.hom (S.g.app j)) y) =
    (AddCommGrpCat.Hom.hom (colimit.ι S.X₃ j)) 0
k : J
e₁ e₂ : j ⟶ k
hk : (ConcreteCategory.hom (S.g.app k)) ((ConcreteCategory.hom (S.X₂.map e₁)) y) = 0
t : ↑(S.map ((evaluation J AddCommGrpCat).obj k)).X₁
ht : (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj k)).f) t = (ConcreteCategory.hom (S.X₂.map e₁)) y
⊢ (AddCommGrpCat.Hom.hom (S.map colim).f) ((ConcreteCategory.hom (colimit.ι S.X₁ k)) t) =
    (ConcreteCategory.hom (colimit.ι S.X₂ j)) y

Tactic:
erw [← ConcreteCategory.comp_apply, colimit.ι_map, ConcreteCategory.comp_apply, ht]

Goal state after:
case h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS :
  ∀ (j : J),
    (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).g).ker ≤
      (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).f).range
j : J
y : ToType (S.X₂.obj j)
hx :
  (ConcreteCategory.hom (colimit.ι S.X₃ j)) ((ConcreteCategory.hom (S.g.app j)) y) =
    (AddCommGrpCat.Hom.hom (colimit.ι S.X₃ j)) 0
k : J
e₁ e₂ : j ⟶ k
hk : (ConcreteCategory.hom (S.g.app k)) ((ConcreteCategory.hom (S.X₂.map e₁)) y) = 0
t : ↑(S.map ((evaluation J AddCommGrpCat).obj k)).X₁
ht : (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj k)).f) t = (ConcreteCategory.hom (S.X₂.map e₁)) y
⊢ (ConcreteCategory.hom (colimit.ι S.X₂ k)) ((ConcreteCategory.hom (S.X₂.map e₁)) y) =
    (ConcreteCategory.hom (colimit.ι S.X₂ j)) y
Module: Mathlib.Algebra.Category.Grp.Adjunctions

Goal state before:
pp: case neg
X Y : Type u
f : X ⟶ Y
x✝ : Mono f
hX : Nonempty X
hf : Function.Injective ⇑(ConcreteCategory.hom f)
g : (fun X ↦ X) Y → (fun X ↦ X) X
hg : Function.LeftInverse g ⇑(ConcreteCategory.hom f)
this : IsSplitMono f
⊢ Mono (free.map f)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.Data.ZMod.IntUnitsPower

Goal state before:
pp: z₁ z₂ : ZMod 2
au : Additive ℤˣ
⊢ Additive.toMul au ^ (z₁.val * z₂.val) = Additive.toMul au ^ (z₂.val * z₁.val)

Tactic:
mul_comm

Goal state after:
z₁ z₂ : ZMod 2
au : Additive ℤˣ
⊢ Additive.toMul au ^ (z₂.val * z₁.val) = Additive.toMul au ^ (z₂.val * z₁.val)
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
⊢ f (Exists.choose ⋯) = (RingHom.id R) r • f (Exists.choose ⋯)

Tactic:
have eq1 : r • _ = (r • x).1 := congr_arg (r • ·) x.2.choose_spec

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 : r • i (Exists.choose ⋯) = ↑(r • x)
⊢ f (Exists.choose ⋯) = (RingHom.id R) r • f (Exists.choose ⋯)
Module: Mathlib.Algebra.Group.Nat.Range

Goal state before:
pp: a : ℕ
s : Finset ℕ
⊢ Disjoint (range a) (map (addLeftEmbedding a) s)

Tactic:
simp_rw [disjoint_left, mem_map, mem_range, addLeftEmbedding_apply]

Goal state after:
a : ℕ
s : Finset ℕ
⊢ ∀ ⦃a_1 : ℕ⦄, a_1 < a → ¬∃ a_3 ∈ s, a + a_3 = a_1
Module: Mathlib.Algebra.Module.Injective

Goal state before:
pp: R : Type u
inst✝⁶ : Ring R
inst✝⁵ : Small.{v, u} R
S : Type u'
inst✝⁴ : Ring S
M : Type v
N : Type v'
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module S N
e₁ : R ≃+* S
e₂ : M ≃ₛₗ[↑e₁] N
inj : Injective R M
⊢ Injective S N

Tactic:
by
  apply Module.Baer.injective (fun I g ↦ ?_)
  let I' := Submodule.map e₁.symm.toSemilinearEquiv.toLinearMap I
  let e : I' ≃ₛₗ[RingHomClass.toRingHom e₁] I := (e₁.symm.toSemilinearEquiv.submoduleMap I).symm
  let f : I' →ₗ[R] M := e₂.symm.toLinearMap.comp (g.comp e.toLinearMap)
  have hf (x) (hx : x ∈ I') : f ⟨x, hx⟩ = e₂.symm (g ⟨e₁ x, by simp_all [I']⟩) := rfl
  obtain ⟨f', hf'⟩ := Module.Baer.of_injective ‹_› I' f
  exact ⟨e₂.toLinearMap ∘ₛₗ f' ∘ₛₗ e₁.toSemilinearEquiv.symm.toLinearMap, by simp_all [I']⟩

Goal state after:
Module: Mathlib.Data.Set.Constructions

Goal state before:
pp: case refine_2
α : Type u_1
S : Set (Set α)
cond : FiniteInter S
F : Finset (Set α)
a : Set α
s : Finset (Set α)
a✝ : a ∉ s
h1 : ↑s ⊆ S → ⋂₀ ↑s ∈ S
h2 : ↑(insert a s) ⊆ S
⊢ a ∩ ⋂₀ ↑s ∈ S

Tactic:
exact
      cond.inter_mem (h2 (Finset.mem_insert_self a s))
        (h1 fun x hx => h2 <| Finset.mem_insert_of_mem hx)

Goal state after:
Module: Mathlib.Data.Set.Constructions

Goal state before:
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.inr
          ⟨Q ∩ R, cond.inter_mem hQ hR, by
            ext x
            constructor <;> simp +contextual⟩

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

Goal state before:
pp: p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x ↦ x * p
h2 : image (fun x ↦ x * p) (range (p ^ n)) ⊆ range (p ^ (n + 1))
⊢ (p - 1) * p ^ n = p ^ n * (p - 1)

Tactic:
mul_comm

Goal state after:
p : ℕ
hp : Prime p
n : ℕ
h1 : Function.Injective fun x ↦ x * p
h2 : image (fun x ↦ x * p) (range (p ^ n)) ⊆ range (p ^ (n + 1))
⊢ p ^ n * (p - 1) = p ^ n * (p - 1)
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ k < n, ∀ (b : ℕ), N k ≤ b → p (n * b + k)
b : ℕ
hb : ((Finset.range n).sup fun x ↦ n * N x) ≤ b
hlt : b % n < n
⊢ N (b % n) * n ≤ b

Tactic:
mul_comm

Goal state after:
p : ℕ → Prop
n : ℕ
hn : n ≠ 0
N : ℕ → ℕ
hN : ∀ k < n, ∀ (b : ℕ), N k ≤ b → p (n * b + k)
b : ℕ
hb : ((Finset.range n).sup fun x ↦ n * N x) ≤ b
hlt : b % n < n
⊢ n * N (b % n) ≤ b
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: p : ℕ → Prop
n : ℕ
hn : n ≠ 0
hp : ∀ k < n, ∀ᶠ (a : ℕ) in atTop, p (n * a + k)
⊢ ∀ᶠ (a : ℕ) in atTop, p a

Tactic:
by
  simp only [eventually_atTop] at hp ⊢
  choose! N hN using hp
  refine ⟨(Finset.range n).sup (n * N ·), fun b hb => ?_⟩
  rw [← Nat.div_add_mod b n]
  have hlt := Nat.mod_lt b hn.bot_lt
  refine hN _ hlt _ ?_
  rw [Nat.le_div_iff_mul_le hn.bot_lt, mul_comm]
  exact (Finset.le_sup (f := (n * N ·)) (Finset.mem_range.2 hlt)).trans hb

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : atTop.IsCountablyGenerated
inst✝¹ : Preorder β
inst✝ : atTop.IsCountablyGenerated
⊢ (atTop ×ˢ atTop).IsCountablyGenerated

Tactic:
infer_instance

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : atBot.IsCountablyGenerated
inst✝¹ : Preorder β
inst✝ : atBot.IsCountablyGenerated
⊢ (atBot ×ˢ atBot).IsCountablyGenerated

Tactic:
infer_instance

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

Goal state before:
pp: n : ℕ
⊢ (∏ p ∈ n.primeFactors, (p - 1)) * (n / ∏ p ∈ n.primeFactors, p) =
    (n / ∏ p ∈ n.primeFactors, p) * ∏ p ∈ n.primeFactors, (p - 1)

pp: n : ℕ
⊢ 0 < ∏ p ∈ n.primeFactors, p

Tactic:
mul_comm

Goal state after:
n : ℕ
⊢ (n / ∏ p ∈ n.primeFactors, p) * ∏ p ∈ n.primeFactors, (p - 1) =
    (n / ∏ p ∈ n.primeFactors, p) * ∏ p ∈ n.primeFactors, (p - 1)

n : ℕ
⊢ 0 < ∏ p ∈ n.primeFactors, p
Module: Mathlib.Order.Filter.AtTopBot.Finite

Goal state before:
pp: a c d : ℕ
⊢ ∀ᶠ (n : ℕ) in atTop, a * c ^ n < (n - d)!

Tactic:
filter_upwards [Nat.eventually_pow_lt_factorial_sub (a * c) d, Filter.eventually_gt_atTop 0]
    with n hn hn0

Goal state after:
a c d n : ℕ
hn : (a * c) ^ n < (n - d)!
hn0 : 0 < n
⊢ a * c ^ n < (n - d)!
Module: Mathlib.Data.Nat.Totient

Goal state before:
pp: a b : ℕ
h : a ∣ b
ha : Even a
h' : φ a = φ b
⊢ a = b

Tactic:
by_cases ha' : a = 0
  · rw [ha', totient_zero, eq_comm, totient_eq_zero] at h'
    rw [h', ha']
  refine (eq_or_eq_of_totient_eq_totient h h').resolve_right fun h ↦ ?_
  rw [← h, totient_mul_of_prime_of_dvd (prime_two) (even_iff_two_dvd.mp ha), eq_comm,
    mul_eq_right (totient_eq_zero.not.mpr ha')] at h'
  lia

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

Goal state before:
pp: case refine_1
α : Type u_1
γ : Type u_3
ι : Sort 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
s : Set γ
t₁ : Set α
ht₁ : t₁ ∈ f.sets
t₂ : Set α
⊢ t₂ ∈ f.sets → ∃ z ∈ f.sets, (g ⁻¹'o fun x1 x2 ↦ x1 ≥ x2) t₁ z ∧ (g ⁻¹'o fun x1 x2 ↦ x1 ≥ x2) t₂ z

Tactic:
ht₂

Goal state after:
case refine_1
α : Type u_1
γ : Type u_3
ι : Sort 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
s : Set γ
t₁ : Set α
ht₁ : t₁ ∈ f.sets
t₂ : Set α
ht₂ : t₂ ∈ f.sets
⊢ ∃ z ∈ f.sets, (g ⁻¹'o fun x1 x2 ↦ x1 ≥ x2) t₁ z ∧ (g ⁻¹'o fun x1 x2 ↦ x1 ≥ x2) t₂ z
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 = z • p + b
⊢ toIcoMod hp a b = toIcoMod hp a c

Tactic:
rw [hz, toIcoMod_zsmul_add]

Goal state after:
Module: Mathlib.Topology.Neighborhoods

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ {x | s ∈ 𝓝 x} = {x | 𝓝 x ≤ 𝓟 s}

Tactic:
by simp only [le_principal_iff]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
x : X
hx : x ∈ s
⊢ x ∈ interior s ↔ x ∉ frontier s

Tactic:
simp [← self_sdiff_frontier, hx]

Goal state after:
Module: Mathlib.Topology.Closure

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
x : X
hx : x ∈ s
⊢ x ∈ frontier s ↔ x ∉ interior s

Tactic:
simp [← self_sdiff_frontier, hx]

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

Goal state before:
pp: case H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b c : α
n : ℤ
a z✝ : α
⊢ ↑(toIcoMod hp a z✝) = ↑z✝

Tactic:
rw [QuotientAddGroup.eq_iff_sub_mem, toIcoMod_sub_self]

Goal state after:
case H
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a✝ b c : α
n : ℤ
a z✝ : α
⊢ -toIcoDiv hp a z✝ • p ∈ AddSubgroup.zmultiples p