mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.FinitePresentation

Goal state before:
pp: case zero
P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_1 : CommRing S] → (R →+* S) → Prop
Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_1 : CommRing S] → (R →+* S) → Prop
polynomial : ∀ (R : Type u) [inst : CommRing R], P R R[X] C
fg_ker :
  ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] (f : R →+* S),
    Surjective ⇑f → (ker f).FG → Q R S f
comp :
  ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_1 : CommRing S] (T : Type v) [inst_2 : CommRing T] (f : R →+* S)
    (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
g' : MvPolynomial (Fin 0) R →+* S
hg : Surjective ⇑g'
hg' : (ker g').FG
this : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
⊢ Q R S (g'.comp MvPolynomial.C)

Tactic:
refine fg_ker _ _ _ (hg.comp (MvPolynomial.C_surjective (Fin 0))) ?_

Goal state after:
case zero
P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_1 : CommRing S] → (R →+* S) → Prop
Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_1 : CommRing S] → (R →+* S) → Prop
polynomial : ∀ (R : Type u) [inst : CommRing R], P R R[X] C
fg_ker :
  ∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] (f : R →+* S),
    Surjective ⇑f → (ker f).FG → Q R S f
comp :
  ∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_1 : CommRing S] (T : Type v) [inst_2 : CommRing T] (f : R →+* S)
    (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
g' : MvPolynomial (Fin 0) R →+* S
hg : Surjective ⇑g'
hg' : (ker g').FG
this : Algebra R S := (g'.comp MvPolynomial.C).toAlgebra
⊢ (ker (g'.comp MvPolynomial.C)).FG
Module: Mathlib.CategoryTheory.Limits.Shapes.RegularMono

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
X B : C
f : X ⟶ B
inst✝¹ : HasPullback f f
inst✝ : Epi f
h : ∀ ⦃Z : C⦄ ⦃g : X ⟶ Z⦄, pullback.fst f f ≫ g = pullback.snd f f ≫ g → ∃ u, f ≫ u = g
⊢ IsRegularEpi f

Tactic:
by
  refine ⟨⟨regularEpiOfKernelPair _ <| Cofork.IsColimit.mk' _ fun s ↦ ?_⟩⟩
  choose g hg using h s.condition
  refine ⟨g, hg, fun hm ↦ ?_⟩
  rwa [← cancel_epi f, hg]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst✝ : HasPullback f f
H : IsIso (diagonal f)
Z✝ : C
x✝¹ x✝ : Z✝ ⟶ X
e : x✝¹ ≫ f = x✝ ≫ f
⊢ x✝¹ = x✝

Tactic:
← lift_fst _ _ e,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst✝ : HasPullback f f
H : IsIso (diagonal f)
Z✝ : C
x✝¹ x✝ : Z✝ ⟶ X
e : x✝¹ ≫ f = x✝ ≫ f
⊢ lift x✝¹ x✝ e ≫ fst f f = x✝
Module: Mathlib.RingTheory.RingHomProperties

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
e₁ : R' ≃+* Localization.Away r := (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r)).toRingEquiv
e₂ : Localization.Away (f r) ≃+* S' :=
  (IsLocalization.algEquiv (Submonoid.powers (f r)) (Localization.Away (f r)) S').toRingEquiv
⊢ P
      ((CommRingCat.Hom.hom e₂.toCommRingCatIso.hom).comp
        (CommRingCat.Hom.hom
          (CommRingCat.ofHom
            {
              toFun := fun x ↦
                (CommRingCat.Hom.hom
                    (CommRingCat.ofHom
                      {
                        toFun :=
                          (↑((IsLocalization.toLocalizationMap (Submonoid.powers r) (Localization.Away r)).lift₀
                                ((algebraMap S (Localization.Away (f r))).comp f).toMonoidWithZeroHom ⋯)).toFun,
                        map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }))
                  ((CommRingCat.Hom.hom e₁.toCommRingCatIso.hom) x),
              map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }))) ↔
    P (IsLocalization.Away.map R' S' f r)

Tactic:
rw [← eq_iff_iff]

Goal state after:
P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hP : RespectsIso P
R S R' S' : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing R'
inst✝⁴ : CommRing S'
inst✝³ : Algebra R R'
inst✝² : Algebra S S'
f : R →+* S
r : R
inst✝¹ : IsLocalization.Away r R'
inst✝ : IsLocalization.Away (f r) S'
e₁ : R' ≃+* Localization.Away r := (IsLocalization.algEquiv (Submonoid.powers r) R' (Localization.Away r)).toRingEquiv
e₂ : Localization.Away (f r) ≃+* S' :=
  (IsLocalization.algEquiv (Submonoid.powers (f r)) (Localization.Away (f r)) S').toRingEquiv
⊢ P
      ((CommRingCat.Hom.hom e₂.toCommRingCatIso.hom).comp
        (CommRingCat.Hom.hom
          (CommRingCat.ofHom
            {
              toFun := fun x ↦
                (CommRingCat.Hom.hom
                    (CommRingCat.ofHom
                      {
                        toFun :=
                          (↑((IsLocalization.toLocalizationMap (Submonoid.powers r) (Localization.Away r)).lift₀
                                ((algebraMap S (Localization.Away (f r))).comp f).toMonoidWithZeroHom ⋯)).toFun,
                        map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }))
                  ((CommRingCat.Hom.hom e₁.toCommRingCatIso.hom) x),
              map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }))) =
    P (IsLocalization.Away.map R' S' f r)
Module: Mathlib.Algebra.Category.CommAlgCat.FiniteType

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommRing R
f : FGAlgCatSkeleton R → Skeleton (FGAlgCat R) := toSkeleton ∘ (FGAlgCat.uliftFunctor R).obj ∘ FGAlgCatSkeleton.eval R
A : Skeleton (FGAlgCat R)
P : FGAlgCatSkeleton R
e : ↑((fromSkeleton (FGAlgCat R)).obj A).obj ≃ₐ[R] ↑(FGAlgCatSkeleton.eval R P).obj
⊢ ∃ a, Nonempty ((FGAlgCat.uliftFunctor R).obj (FGAlgCatSkeleton.eval R a) ≅ (fromSkeleton (FGAlgCat R)).obj A)

Tactic:
exact ⟨P, ⟨ObjectProperty.isoMk _ (CommAlgCat.isoMk <| ULift.algEquiv.trans e.symm)⟩⟩

Goal state after:
Module: Mathlib.Algebra.Category.CommAlgCat.FiniteType

Goal state before:
pp: case refine_1
R : Type u
inst✝ : CommRing R
⊢ Small.{u, max (u + 1) (v + 1)} (Skeleton (FGAlgCat R))

pp: case refine_2
R : Type u
inst✝ : CommRing R
⊢ LocallySmall.{u, max u v, max (u + 1) (v + 1)} (FGAlgCat R)

Tactic:
· let f := toSkeleton ∘ (FGAlgCat.uliftFunctor R).obj ∘ FGAlgCatSkeleton.eval R
    refine small_of_surjective (f := f) fun A ↦ ?_
    simp only [Function.comp_apply, f, toSkeleton_eq_iff]
    obtain ⟨P, ⟨e⟩⟩ := Algebra.FiniteType.exists_fgAlgCatSkeleton R
      ((fromSkeleton (FGAlgCat R)).obj A).obj
    exact ⟨P, ⟨ObjectProperty.isoMk _ (CommAlgCat.isoMk <| ULift.algEquiv.trans e.symm)⟩⟩

Goal state after:
case refine_2
R : Type u
inst✝ : CommRing R
⊢ LocallySmall.{u, max u v, max (u + 1) (v + 1)} (FGAlgCat R)
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
X✝ Y✝ Z : C
inst✝¹ : HasPullbacks C
X Y S X' Y' S' : C
f : X ⟶ S
g : Y ⟶ S
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ (fst (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (fst f' g') i₁) ≫ f =
    (snd (fst (fst f' g') i₁) (fst (snd f' g') i₂) ≫ snd (snd f' g') i₂) ≫ g

Tactic:
rw [← cancel_mono i₃, Category.assoc, Category.assoc, Category.assoc, Category.assoc, e₁,
          e₂, ← pullback.condition_assoc, pullback.condition_assoc, pullback.condition,
          pullback.condition_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Diagonal

Goal state before:
pp: case refine_1.refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasPullbacks C
X Y Z S : C
f : X ⟶ S
g : Y ⟶ S
h : Z ⟶ S
c : PullbackCone (fst g h) (snd f g)
⊢ (c.snd ≫ fst f g) ≫ f = (c.fst ≫ snd g h) ≫ h

Tactic:
simp [pullback.condition, ← c.condition_assoc]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasPullbacks C
P : MorphismProperty C
inst✝¹ : P.IsStableUnderBaseChange
inst✝ : P.RespectsIso
⊢ ∀ (X Y S : C) (f : X ⟶ S) (g : Y ⟶ S) [inst : HasPullback f g], P.diagonal g → P.diagonal (pullback.fst f g)

Tactic:
by
      introv h
      rw [diagonal_iff, diagonal_pullback_fst, P.cancel_left_of_respectsIso,
        P.cancel_right_of_respectsIso]
      exact P.overPullbackMap f _ (by simpa)

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

Goal state before:
pp: C✝ : Type u
inst✝⁴ : Category.{v, u} C✝
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderLimitsOfShape (Discrete WalkingPair)
x✝¹ : P.FullSubcategory
x✝ : x✝¹ ⟶ 𝟙_ P.FullSubcategory
⊢ x✝ = ObjectProperty.homMk (toUnit x✝¹.obj)

Tactic:
by ext; apply toUnit_unique

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
x y : C
inst✝¹ : Closed x
inst✝ : Closed y
⊢ (ihom.ev x).app y ≫ (ρ_ y).inv ≫ y ◁ id y ≫ uncurry (𝟙 ((ihom y).obj y)) = uncurry (𝟙 ((ihom x).obj y))

Tactic:
← uncurry_natural_left

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
x y : C
inst✝¹ : Closed x
inst✝ : Closed y
⊢ (ihom.ev x).app y ≫ (ρ_ y).inv ≫ uncurry (id y ≫ 𝟙 ((ihom y).obj y)) = uncurry (𝟙 ((ihom x).obj y))
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: case inr
K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this✝¹ : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun i ↦ bK i.1 i.2)
hLK : #↥L < #K
this✝ : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)
ιL : Type u
bL : Module.Basis ιL (↥L)ᵐᵒᵖ K
card_ιL : ℵ₀ ≤ #ιL
e : ℕ ↪ ιL
c : ιK →₀ K
s : Finset ιK
rep_e : ∑ a ∈ s, c a • bK a = ⇑bL ∘ ⇑e
f : ℕ → ↥s → ↥L := fun i j ↦ ⟨bK (↑j) i, ⋯⟩
this : ¬LinearIndependent (↥L)ᵐᵒᵖ f
t : Finset ℕ
g : ℕ → (↥L)ᵐᵒᵖ
eq0 : ∑ i ∈ t, g i • f i = 0
i : ℕ
hi : i ∈ t
hgi : g i ≠ 0
⊢ ∑ i ∈ t, g i • (⇑bL ∘ ⇑e) i = 0

Tactic:
← rep_e,

Goal state after:
case inr
K : Type u
inst✝ : DivisionRing K
aleph0_le : ℵ₀ ≤ Module.rank K (ℕ → K)
card_K : ℵ₀ < #K
this✝¹ : Module.rank K (ℕ → K) < #K
ιK : Type u
bK : Module.Basis ιK K (ℕ → K)
L : Subfield K := Subfield.closure (Set.range fun i ↦ bK i.1 i.2)
hLK : #↥L < #K
this✝ : Module (↥L)ᵐᵒᵖ K := Module.compHom K (RingHom.op L.subtype)
ιL : Type u
bL : Module.Basis ιL (↥L)ᵐᵒᵖ K
card_ιL : ℵ₀ ≤ #ιL
e : ℕ ↪ ιL
c : ιK →₀ K
s : Finset ιK
rep_e : ∑ a ∈ s, c a • bK a = ⇑bL ∘ ⇑e
f : ℕ → ↥s → ↥L := fun i j ↦ ⟨bK (↑j) i, ⋯⟩
this : ¬LinearIndependent (↥L)ᵐᵒᵖ f
t : Finset ℕ
g : ℕ → (↥L)ᵐᵒᵖ
eq0 : ∑ i ∈ t, g i • f i = 0
i : ℕ
hi : i ∈ t
hgi : g i ≠ 0
⊢ ∑ x ∈ t, g x • (∑ a ∈ s, c a • bK a) x = 0
Module: Mathlib.LinearAlgebra.Dimension.ErdosKaplansky

Goal state before:
pp: K V : Type u
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
h : ℵ₀ ≤ Module.rank K V
⊢ Module.rank K V < Module.rank K (V →ₗ[K] K)

Tactic:
by
  convert! lift_rank_lt_rank_dual h; rw [lift_id]

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix

Goal state before:
pp: case e'_4
K : Type u_1
M : Type u_2
L : Type v
inst✝⁷ : CommRing K
inst✝⁶ : Ring M
inst✝⁵ : Algebra K M
inst✝⁴ : Module.Free K M
inst✝³ : Module.Finite K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
⊢ lift.{v, u_2} (Module.rank K M) = lift.{max u_2 v, max u_2 v} (Module.rank L (M →ₗ[K] L))

Tactic:
have := Module.nontrivial K L

Goal state after:
case e'_4
K : Type u_1
M : Type u_2
L : Type v
inst✝⁷ : CommRing K
inst✝⁶ : Ring M
inst✝⁵ : Algebra K M
inst✝⁴ : Module.Free K M
inst✝³ : Module.Finite K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
this : Nontrivial K
⊢ lift.{v, u_2} (Module.rank K M) = lift.{max u_2 v, max u_2 v} (Module.rank L (M →ₗ[K] L))
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix

Goal state before:
pp: K : Type u_1
M : Type u_2
L : Type v
inst✝⁷ : CommRing K
inst✝⁶ : Ring M
inst✝⁵ : Algebra K M
inst✝⁴ : Module.Free K M
inst✝³ : Module.Finite K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
⊢ Module.rank K M < ℵ₀

Tactic:
have := Module.nontrivial K L

Goal state after:
K : Type u_1
M : Type u_2
L : Type v
inst✝⁷ : CommRing K
inst✝⁶ : Ring M
inst✝⁵ : Algebra K M
inst✝⁴ : Module.Free K M
inst✝³ : Module.Finite K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
this : Nontrivial K
⊢ Module.rank K M < ℵ₀
Module: Mathlib.Algebra.Category.ModuleCat.Products

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
ι : Type v
Z : ι → ModuleCat R
inst✝ : DecidableEq ι
⊢ ∀ (s : Cocone (Discrete.functor Z)) (m : (coproductCocone Z).pt ⟶ s.pt),
    (∀ (j : Discrete ι), (coproductCocone Z).ι.app j ≫ m = s.ι.app j) →
      m = ↟(toModule R ι ↑s.1 fun i ↦ Hom.hom (s.ι.app { as := i }))

Tactic:
rintro s f h
    ext : 1
    refine DirectSum.linearMap_ext _ fun i ↦ ?_
    ext x
    simpa only [LinearMap.coe_comp, Function.comp_apply, hom_ofHom, toModule_lof] using!
      congr($(h ⟨i⟩) x)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryProducts C
inst✝ : HasPullbacks C
F : WalkingParallelPair ⥤ C
⊢ ∀ (s : Cone F) (j : WalkingParallelPair),
    pullback.lift (s.π.app WalkingParallelPair.zero) (s.π.app WalkingParallelPair.zero) ⋯ ≫ (equalizerCone F).π.app j =
      s.π.app j

Tactic:
by rintro c (_ | _) <;> simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Equalizers

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
G : C ⥤ D
inst✝¹ : HasBinaryCoproducts C
inst✝ : HasPushouts C
F : WalkingParallelPair ⥤ C
⊢ ∀ (s : Cocone F) (j : WalkingParallelPair),
    (coequalizerCocone F).ι.app j ≫ pushout.desc (s.ι.app WalkingParallelPair.one) (s.ι.app WalkingParallelPair.one) ⋯ =
      s.ι.app j

Tactic:
by rintro c (_ | _) <;> simp

Goal state after:
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: R : Type u_3
M : Type u_4
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
x : M
hx : x ∉ p
hp' : Projective R (M ⧸ p)
⊢ ∃ f, f x ≠ 0 ∧ map f p = ⊥

Tactic:
by
  suffices ∃ f : Dual R (M ⧸ p), f (p.mkQ x) ≠ 0 by
    obtain ⟨f, hf⟩ := this; exact ⟨f.comp p.mkQ, hf, by simp [Submodule.map_comp]⟩
  rw [← Submodule.Quotient.mk_eq_zero, ← Submodule.mkQ_apply] at hx
  exact Projective.exists_dual_ne_zero R hx

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
F : J ⥤ C
c₁ : Fan F.obj
c₂ : Fan fun f ↦ F.obj f.fst.2
s t : c₁.pt ⟶ c₂.pt
hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), s ≫ c₂.π.app { as := f } = c₁.π.app { as := f.fst.1 } ≫ F.map f.snd
ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), t ≫ c₂.π.app { as := f } = c₁.π.app { as := f.fst.2 }
i : Fork s t
j₁ j₂ : J
f : j₁ ⟶ j₂
⊢ i.ι ≫ c₁.π.app { as := j₂ } = i.ι ≫ c₁.π.app { as := j₁ } ≫ F.map f

Tactic:
← hs ⟨⟨_, _⟩, f⟩,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : Type w
inst✝ : SmallCategory J
F : J ⥤ C
c₁ : Fan F.obj
c₂ : Fan fun f ↦ F.obj f.fst.2
s t : c₁.pt ⟶ c₂.pt
hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), s ≫ c₂.π.app { as := f } = c₁.π.app { as := f.fst.1 } ≫ F.map f.snd
ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), t ≫ c₂.π.app { as := f } = c₁.π.app { as := f.fst.2 }
i : Fork s t
j₁ j₂ : J
f : j₁ ⟶ j₂
⊢ i.ι ≫ c₁.π.app { as := j₂ } = i.ι ≫ s ≫ c₂.π.app { as := ⟨(j₁, j₂), f⟩ }
Module: Mathlib.Algebra.Category.FGModuleCat.Colimits

Goal state before:
pp: J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
k : Type u
inst✝ : Ring k
F : J ⥤ FGModuleCat k
⊢ ModuleCat.isFG k (colimit (F ⋙ forget₂ (FGModuleCat k) (ModuleCat k)))

Tactic:
rw [ModuleCat.isFG_iff]

Goal state after:
J : Type
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
k : Type u
inst✝ : Ring k
F : J ⥤ FGModuleCat k
⊢ Module.Finite k ↑(colimit (F ⋙ forget₂ (FGModuleCat k) (ModuleCat k)))
Module: Mathlib.Algebra.Category.FGModuleCat.Limits

Goal state before:
pp: J : Type
inst✝³ : SmallCategory J
inst✝² : FinCategory J
k : Type u
inst✝¹ : Ring k
inst✝ : IsNoetherianRing k
F : J ⥤ FGModuleCat k
⊢ ModuleCat.isFG k (limit (F ⋙ forget₂ (FGModuleCat k) (ModuleCat k)))

Tactic:
rw [ModuleCat.isFG_iff]

Goal state after:
J : Type
inst✝³ : SmallCategory J
inst✝² : FinCategory J
k : Type u
inst✝¹ : Ring k
inst✝ : IsNoetherianRing k
F : J ⥤ FGModuleCat k
⊢ Module.Finite k ↑(limit (F ⋙ forget₂ (FGModuleCat k) (ModuleCat k)))
Module: Mathlib.LinearAlgebra.Dual.Lemmas

Goal state before:
pp: K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst✝ : IsReflexive K V₂
⊢ B.dualMap.range = (B.dualMap ∘ₗ ↑(evalEquiv K V₂)).range

Tactic:
range_comp_of_range_eq_top _ (LinearEquiv.range _)

Goal state after:
K : Type u_1
V₁ : Type u_2
V₂ : Type u_3
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
B : V₁ →ₗ[K] V₂ →ₗ[K] K
inst✝ : IsReflexive K V₂
⊢ B.dualMap.range = B.dualMap.range
Module: Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
X✝ Y✝ : C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₁, u₂} D
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.IsEquivalence
X Y : C
f : X ⟶ Y
hf : NormalMono (F.map f)
⊢ F.map (f ≫ F.preimage (NormalMono.g ≫ (F.objObjPreimageIso (NormalMono.Z (F.map f))).inv)) = F.map 0

Tactic:
have reassoc' {W : D} (h : hf.Z ⟶ W) : F.map f ≫ hf.g ≫ h = 0 ≫ h := by
      rw [← Category.assoc, eq_whisker hf.w]
    simp [reassoc']

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

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
β : ↑B
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (fun x ↦ β⁻¹ • x) ((fun x ↦ β • x) x) = x

Tactic:
dsimp only
        rw [← mul_smul, inv_mul_cancel, one_smul]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono g
R : C
e : R ⟶ Y
h : e ≫ pushout.inl f g = 0
⊢ e = 0

Tactic:
let u := biprod.lift e (0 : R ⟶ Z)

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPushouts C
W X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝ : Mono g
R : C
e : R ⟶ Y
h : e ≫ pushout.inl f g = 0
u : R ⟶ Y ⊞ Z := biprod.lift e 0
⊢ e = 0
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : CommGrpCat
f : A ⟶ B
⊢ (Hom.hom f).range = ⊤ ↔ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
MonoidHom.range_eq_top

Goal state after:
A B : CommGrpCat
f : A ⟶ B
⊢ Function.Surjective ⇑(Hom.hom f) ↔ Function.Surjective ⇑(ConcreteCategory.hom f)
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ S.leftHomologyData.homologyIso = S.leftHomologyIso.symm

Tactic:
by
  ext
  dsimp [homologyIso, leftHomologyIso, ShortComplex.leftHomologyIso]
  rw [← leftHomologyMap'_comp, comp_id]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
hg : S.g = 0
c : CokernelCofork S.f
hc : IsColimit c
⊢ (ofIsColimitCokernelCofork S hg c hc).g' = 0

Tactic:
← cancel_epi (ofIsColimitCokernelCofork S hg c hc).p,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
hg : S.g = 0
c : CokernelCofork S.f
hc : IsColimit c
⊢ (ofIsColimitCokernelCofork S hg c hc).p ≫ (ofIsColimitCokernelCofork S hg c hc).g' =
    (ofIsColimitCokernelCofork S hg c hc).p ≫ 0
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

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

Tactic:
by
  dsimp only [homologyπ]
  simp only [assoc, Iso.hom_inv_id, comp_id]

Goal state after:
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
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst✝¹ : Epi π
inst✝ : Mono ι
⊢ IsLimit (KernelFork.ofι ι ⋯)

Tactic:
by
    refine (IsLimit.equivOfNatIsoOfIso ?_ _ _ ?_).2 S.homologyIsKernel
    · exact parallelPair.ext (S.isoOpcyclesOfIsColimit hcc) (Iso.refl _)
    · exact Fork.ext (isoHomology S hkf hcc fac) (by simp [Fork.ι])

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 φ₁ φ₂
⊢ (opMap φ₁).τ₂.unop = (S₂.op.g ≫ h.h₁.op + h.h₂.op ≫ S₁.op.f + (opMap φ₂).τ₂).unop

Tactic:
by dsimp; rw [h.comm₂]; 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₂✝
S₁ S₂ : ShortComplex Cᵒᵖ
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ (unopMap φ₁).τ₂.op = (S₂.unop.g ≫ h.h₁.unop + h.h₂.unop ≫ S₁.unop.f + (unopMap φ₂).τ₂).op

Tactic:
by dsimp; rw [h.comm₂]; abel

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
S : ShortComplex C
hg : S.g = 0
inst✝ : PreservesColimit (parallelPair S.f 0) F
h : S.LeftHomologyData
this : IsIso h.i
e : parallelPair h.f' 0 ≅ parallelPair S.f 0 :=
  parallelPair.ext (Iso.refl ((parallelPair h.f' 0).obj WalkingParallelPair.zero)) (asIso h.i) ⋯ ⋯
⊢ PreservesColimit (parallelPair h.f' 0) F

Tactic:
exact Limits.preservesColimit_of_iso_diagram F e.symm

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₀ : 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
⊢ (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃).τ₁ = S₁.f ≫ h₁ + h₀ + Hom.τ₁ 0

Tactic:
rw [nullHomotopic_τ₁, zero_τ₁, add_zero]

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₀ : 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
⊢ h₀ + S₁.f ≫ h₁ = S₁.f ≫ h₁ + h₀
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

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.Exact
a✝ : Mono S.g
⊢ S.f ≫ S.g = 0 ≫ S.g

Tactic:
zero,

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
a✝ : Mono S.g
⊢ 0 = 0 ≫ S.g
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

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.Exact
a✝ : Epi S.f
⊢ S.f ≫ S.g = S.f ≫ 0

Tactic:
zero,

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
a✝ : Epi S.f
⊢ 0 = S.f ≫ 0