mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : CartesianMonoidalCategory C
X : C
⊢ Function.Injective (@toMonObj C inst✝¹ inst✝ X)

Tactic:
intro h₁ h₂ e

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : CartesianMonoidalCategory C
X : C
h₁ h₂ : GrpObj X
e : h₁.toMonObj = h₂.toMonObj
⊢ h₁ = h₂
Module: Mathlib.CategoryTheory.Monoidal.Grp

Goal state before:
pp: case mk
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : CartesianMonoidalCategory C
X : C
h₂ : GrpObj X
toMonObj✝ : MonObj X
inv✝ : X ⟶ X
left_inv✝ : lift inv✝ (𝟙 X) ≫ μ = toUnit X ≫ η
right_inv✝ : lift (𝟙 X) inv✝ ≫ μ = toUnit X ≫ η
e : { toMonObj := toMonObj✝, inv := inv✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toMonObj = h₂.toMonObj
this : ι = ι
⊢ { toMonObj := toMonObj✝, inv := inv✝, left_inv := left_inv✝, right_inv := right_inv✝ } = h₂

Tactic:
congr!

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : ExactPairing X Y
⊢ Y ◁ η_ X Y ⊗≫ ε_ X Y ▷ Y = ⊗𝟙.hom

Tactic:
convert! coevaluation_evaluation X Y

Goal state after:
case e'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : ExactPairing X Y
⊢ Y ◁ η_ X Y ⊗≫ ε_ X Y ▷ Y = Y ◁ η_ X Y ≫ (α_ Y X Y).inv ≫ ε_ X Y ▷ Y

case e'_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y : C
inst✝ : ExactPairing X Y
⊢  ⊗𝟙.hom = (ρ_ Y).hom ≫ (λ_ Y).inv
Module: Mathlib.Data.W.Basic

Goal state before:
pp: case mk
α : Type u_1
β : α → Type u_2
inst✝ : (a : α) → Fintype (β a)
a✝ : α
f✝ : β a✝ → WType β
⊢ 0 < (mk a✝ f✝).depth

Tactic:
apply Nat.succ_pos

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

Goal state before:
pp: case intro
R : Type uR
M : Type uM
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_1
inst✝ : Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ (Dual.eval R M).range = ⊤

Tactic:
rw [← b.toDual_toDual, range_comp, b.toDual_range, Submodule.map_top, toDual_range _]

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_1
M : Type u
M' : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : HasRankNullity.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
f' : M' ⧸ Submodule.map f p →ₗ[R] M' ⧸ f.range := factor ⋯
⊢ Submodule.map (Submodule.map f p).mkQ f.range = f'.ker

Tactic:
rw [ker_mapQ]

Goal state after:
R : Type u_1
M : Type u
M' : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
inst✝ : HasRankNullity.{v, u_1} R
f : M →ₗ[R] M'
p : Submodule R M
f' : M' ⧸ Submodule.map f p →ₗ[R] M' ⧸ f.range := factor ⋯
⊢ Submodule.map (Submodule.map f p).mkQ f.range = Submodule.map (Submodule.map f p).mkQ (comap id f.range)
Module: Mathlib.LinearAlgebra.Dimension.DivisionRing

Goal state before:
pp: K : Type u
V V₁ V₂ V₃ : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module K V₁
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ : ∀ (d : V₂) (e : V₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e
⊢ db.range ⊔ eb.range = ⊤

Tactic:
eq_top_iff

Goal state after:
K : Type u
V V₁ V₂ V₃ : Type v
inst✝⁸ : DivisionRing K
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module K V
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : Module K V₁
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : AddCommGroup V₃
inst✝ : Module K V₃
db : V₂ →ₗ[K] V
eb : V₃ →ₗ[K] V
cd : V₁ →ₗ[K] V₂
ce : V₁ →ₗ[K] V₃
hde : ⊤ ≤ db.range ⊔ eb.range
hgd : cd.ker = ⊥
eq : db ∘ₗ cd = eb ∘ₗ ce
eq₂ : ∀ (d : V₂) (e : V₃), db d = eb e → ∃ c, cd c = d ∧ ce c = e
⊢ ⊤ ≤ db.range ⊔ eb.range
Module: Mathlib.LinearAlgebra.Dimension.RankNullity

Goal state before:
pp: R : Type u_1
M : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : HasRankNullity.{u, u_1} R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
h : finrank R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank R (M ⧸ N)
hs' : LinearIndependent R Subtype.val
⊢ ¬finrank R M ≤ finrank R ↥N

Tactic:
not_le

Goal state after:
R : Type u_1
M : Type u
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : HasRankNullity.{u, u_1} R
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
h : finrank R ↥N < finrank R M
s : Finset (M ⧸ N)
hs : s.card = finrank R (M ⧸ N)
hs' : LinearIndependent R Subtype.val
⊢ finrank R ↥N < finrank R M
Module: Mathlib.LinearAlgebra.FiniteDimensional.Lemmas

Goal state before:
pp: K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
h_contra : ¬∃ k ≤ finrank K V, LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
⊢ False

Tactic:
not_exists,

Goal state after:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
h_contra : ∀ (x : ℕ), ¬(x ≤ finrank K V ∧ LinearMap.ker (f ^ x) = LinearMap.ker (f ^ x.succ))
⊢ False
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Matrix

Goal state before:
pp: R : Type u
S : Type u'
M : Type v
inst✝⁹ : Ring R
inst✝⁸ : Ring S
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Free R M
inst✝⁴ : Module.Finite R M
inst✝³ : StrongRankCondition R
inst✝² : StrongRankCondition S
inst✝¹ : Module R S
inst✝ : SMulCommClass R S S
⊢ finrank S (M →ₗ[R] S) = finrank R M

Tactic:
rw [finrank_linearMap, finrank_self, mul_one]

Goal state after:
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)) (j : Discrete ι),
    (coproductCocone Z).ι.app j ≫ ↟(toModule R ι ↑s.1 fun i ↦ Hom.hom (s.ι.app { as := i })) = s.ι.app j

Tactic:
by
    rintro s ⟨i⟩
    ext (x : Z i)
    simpa only [Discrete.functor_obj_eq_as, coproductCocone, Cofan.mk_pt, Functor.const_obj_obj,
      Cofan.mk_ι_app, hom_comp, LinearMap.coe_comp, Function.comp_apply] using!
      DirectSum.toModule_lof (ι := ι) R (M := fun i ↦ Z i) i x

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
fin : Finite ι ∨ Module.Finite R M
h : Function.Bijective ⇑(dualTensorHom R M N)
⊢ Function.Bijective ⇑(dualTensorHom R M (ι →₀ N))

Tactic:
rw [dualTensorHom_finsupp, coe_comp]

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
fin : Finite ι ∨ Module.Finite R M
h : Function.Bijective ⇑(dualTensorHom R M N)
⊢ Function.Bijective
    (⇑(finsuppLinearMap R) ∘ ⇑(Finsupp.mapRange.linearMap (dualTensorHom R M N) ∘ₗ ↑(finsuppRight R R (Dual R M) N ι)))
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
I I' : R →+* R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
inst✝ : Nontrivial R
v : Basis n R M
h : B.IsOrthoᵢ ⇑v
hB : B.SeparatingLeft
i : n
ho : (B (v i)) (v i) = 0
vi : n →₀ R
⊢ (B (v i)) (v.repr.symm vi) = 0

Tactic:
rw [Basis.repr_symm_apply, Finsupp.linearCombination_apply, Finsupp.sum, map_sum]

Goal state after:
n : Type u_19
R : Type u_20
M : Type u_21
M₁ : Type u_22
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M
inst✝¹ : Module R M₁
I I' : R →+* R
B : M →ₛₗ[I] M →ₛₗ[I'] M₁
inst✝ : Nontrivial R
v : Basis n R M
h : B.IsOrthoᵢ ⇑v
hB : B.SeparatingLeft
i : n
ho : (B (v i)) (v i) = 0
vi : n →₀ R
⊢ ∑ x ∈ vi.support, (B (v i)) (vi x • v x) = 0
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: case inr.inr
R : Type u_1
M : Type u_5
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
x y : M
aux : ∀ (x y : M), 0 ≤ (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
hx : (B x) x = 0
hy : (B y) y = 0
⊢ (B x) y + (B y) x = 0

Tactic:
apply le_antisymm

Goal state after:
case inr.inr.a
R : Type u_1
M : Type u_5
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
x y : M
aux : ∀ (x y : M), 0 ≤ (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
hx : (B x) x = 0
hy : (B y) y = 0
⊢ (B x) y + (B y) x ≤ 0

case a
R : Type u_1
M : Type u_5
inst✝⁴ : CommRing R
inst✝³ : LinearOrder R
inst✝² : IsStrictOrderedRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
hs : ∀ (x : M), 0 ≤ (B x) x
x y : M
aux : ∀ (x y : M), 0 ≤ (B x) x * ((B x) x * (B y) y - (B x) y * (B y) x)
hx : (B x) x = 0
hy : (B y) y = 0
⊢ 0 ≤ (B x) y + (B y) x
Module: Mathlib.Algebra.Category.ModuleCat.Kernels

Goal state before:
pp: R : Type u
inst✝ : Ring R
M N : ModuleCat R
f : M ⟶ N
x y : ↑N
m : ↑M
w : x = y + (ConcreteCategory.hom f) m
⊢ (ConcreteCategory.hom (cokernel.π f)) x = (ConcreteCategory.hom (cokernel.π f)) y

Tactic:
by
  subst w
  simpa only [map_add, add_eq_left] using! cokernel.condition_apply f m

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
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : J ⥤ C
c₁ : Cofan fun f ↦ F.obj f.fst.1
c₂ : Cofan F.obj
s t : c₁.pt ⟶ c₂.pt
hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), c₁.ι.app { as := f } ≫ s = F.map f.snd ≫ c₂.ι.app { as := f.fst.2 }
ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), c₁.ι.app { as := f } ≫ t = c₂.ι.app { as := f.fst.1 }
i : Cofork s t
t₁ : IsColimit c₁
t₂ : IsColimit c₂
hi : IsColimit i
q : Cocone F
⊢ (buildColimit s t hs ht i).pt ⟶ q.pt

Tactic:
refine hi.desc (Cofork.ofπ ?_ ?_)

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : SmallCategory J
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : J ⥤ C
c₁ : Cofan fun f ↦ F.obj f.fst.1
c₂ : Cofan F.obj
s t : c₁.pt ⟶ c₂.pt
hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), c₁.ι.app { as := f } ≫ s = F.map f.snd ≫ c₂.ι.app { as := f.fst.2 }
ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), c₁.ι.app { as := f } ≫ t = c₂.ι.app { as := f.fst.1 }
i : Cofork s t
t₁ : IsColimit c₁
t₂ : IsColimit c₂
hi : IsColimit i
q : Cocone F
⊢ c₂.pt ⟶ q.1

case refine_2
C : Type u
inst✝² : Category.{v, u} C
J : Type w
inst✝¹ : SmallCategory J
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : J ⥤ C
c₁ : Cofan fun f ↦ F.obj f.fst.1
c₂ : Cofan F.obj
s t : c₁.pt ⟶ c₂.pt
hs : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), c₁.ι.app { as := f } ≫ s = F.map f.snd ≫ c₂.ι.app { as := f.fst.2 }
ht : ∀ (f : (p : J × J) × (p.1 ⟶ p.2)), c₁.ι.app { as := f } ≫ t = c₂.ι.app { as := f.fst.1 }
i : Cofork s t
t₁ : IsColimit c₁
t₂ : IsColimit c₂
hi : IsColimit i
q : Cocone F
⊢ s ≫ ?refine_1 = t ≫ ?refine_1
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
inst✝ : IsNormalMonoCategory C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
x✝ : Mono f
⊢ IsRegularMono f

Tactic:
have := normalMonoOfMono f
    infer_instance

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
F : Type u_3
inst✝¹ : Finite ι
inst✝ : Field F
f : ι → α → F
⊢ (map (↑(Finsupp.llift F F F ι)) (span F (Set.range (flip f)))).dualCoannihilator = ⊥ ↔
    (Finsupp.linearCombination F f).ker = ⊥

Tactic:
congr!

Goal state after:
ι : Type u_1
α : Type u_2
F : Type u_3
inst✝¹ : Finite ι
inst✝ : Field F
f : ι → α → F
⊢ (map (↑(Finsupp.llift F F F ι)) (span F (Set.range (flip f)))).dualCoannihilator = (Finsupp.linearCombination F f).ker
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
X Y : Cᵒᵖ
f : X ⟶ Y
m : NormalEpi f.unop
⊢ ∀ {W' : Cᵒᵖ} (g' : W' ⟶ Y) (eq' : g' ≫ NormalEpi.g.op = 0) (m_1 : W' ⟶ X),
    m_1 ≫ f = g' → m_1 = (↑(CokernelCofork.IsColimit.desc' NormalEpi.isColimit g'.unop ⋯)).op

Tactic:
rintro Z' g' w' m' rfl
        apply Quiver.Hom.unop_inj
        apply m.isColimit.uniq (CokernelCofork.ofπ (f.unop ≫ m'.unop) _) m'.unop
        rintro (⟨⟩ | ⟨⟩) <;> simp

Goal state after:
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) := ⋯
hp2 : IsColimit (CokernelCofork.ofπ prod.snd hlp) := ⋯
Z : C
z : cokernel (diag A) ⟶ Z
hz : r A ≫ z = 0
h : prod.lift (𝟙 A) 0 ≫ cokernel.π (diag A) ≫ z = 0
t : (CokernelCofork.ofπ prod.snd hlp).pt ⟶ Z
ht : prod.snd ≫ t = cokernel.π (diag A) ≫ z
htt : t = 0
⊢ cokernel.π (diag A) ≫ z = cokernel.π (diag A) ≫ 0

Tactic:
← ht,

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) :=
  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
Z : C
z : cokernel (diag A) ⟶ Z
hz : r A ≫ z = 0
h : prod.lift (𝟙 A) 0 ≫ cokernel.π (diag A) ≫ z = 0
t : (CokernelCofork.ofπ prod.snd hlp).pt ⟶ Z
ht : prod.snd ≫ t = cokernel.π (diag A) ≫ z
htt : t = 0
⊢ prod.snd ≫ t = cokernel.π (diag A) ≫ 0
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: case e'_2.e'_6
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 : Epi f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
s : CokernelCofork (kernel.ι f)
e_1✝ : (X✝ ⟶ s.pt) = ((parallelPair (kernel.ι f) 0).obj WalkingParallelPair.one ⟶ s.pt)
e_3✝ : X✝ = (parallelPair (kernel.ι f) 0).obj WalkingParallelPair.one
⊢ (f ≫ inv (imageMonoFactorisation f).m) ≫ inv (coimageImageComparison f) =
    colimit.ι (parallelPair (kernel.ι f) 0) WalkingParallelPair.one

Tactic:
IsIso.comp_inv_eq,

Goal state after:
case e'_2.e'_6
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 : Epi f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
s : CokernelCofork (kernel.ι f)
e_1✝ : (X✝ ⟶ s.pt) = ((parallelPair (kernel.ι f) 0).obj WalkingParallelPair.one ⟶ s.pt)
e_3✝ : X✝ = (parallelPair (kernel.ι f) 0).obj WalkingParallelPair.one
⊢ f ≫ inv (imageMonoFactorisation f).m =
    colimit.ι (parallelPair (kernel.ι f) 0) WalkingParallelPair.one ≫ coimageImageComparison f
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: case e'_2.e'_6
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 : Epi f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
s : CokernelCofork (kernel.ι f)
e_1✝ : (X✝ ⟶ s.pt) = ((parallelPair (kernel.ι f) 0).obj WalkingParallelPair.one ⟶ s.pt)
e_3✝ : X✝ = (parallelPair (kernel.ι f) 0).obj WalkingParallelPair.one
⊢ f ≫ inv (imageMonoFactorisation f).m =
    colimit.ι (parallelPair (kernel.ι f) 0) WalkingParallelPair.one ≫ coimageImageComparison f

Tactic:
IsIso.comp_inv_eq,

Goal state after:
case e'_2.e'_6
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 : Epi f
this✝¹ : HasImages C
this✝ : HasEqualizers C
this : HasZeroObject C
s : CokernelCofork (kernel.ι f)
e_1✝ : (X✝ ⟶ s.pt) = ((parallelPair (kernel.ι f) 0).obj WalkingParallelPair.one ⟶ s.pt)
e_3✝ : X✝ = (parallelPair (kernel.ι f) 0).obj WalkingParallelPair.one
⊢ f =
    (colimit.ι (parallelPair (kernel.ι f) 0) WalkingParallelPair.one ≫ coimageImageComparison f) ≫
      (imageMonoFactorisation f).m
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ (coimageIsoImage' f).hom = cokernel.desc (kernel.ι f) (factorThruImage f) ⋯

Tactic:
ext
  simp only [← cancel_mono (Limits.image.ι f), IsImage.isoExt_hom, cokernel.π_desc,
    Category.assoc, IsImage.lift_ι, coimageStrongEpiMonoFactorisation_m,
    Limits.image.fac]

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

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
x : ↑B
hx : x ∈ (Hom.hom f).range
b : ↑B
hb : b ∉ (Hom.hom f).range
r : x * b ∈ (Hom.hom f).range
⊢ b = x⁻¹ * (x * b)

Tactic:
rw [← mul_assoc, inv_mul_cancel, one_mul]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ S₄ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
⊢ ∀ (a b : HomologyMapData φ h₁ h₂), a = b

Tactic:
by
  rintro ⟨left₁, right₁⟩ ⟨left₂, right₂⟩
  simp only [mk.injEq, eq_iff_true_of_subsingleton, and_self]

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
h : S.RightHomologyData
inst✝ : S.HasRightHomology
⊢ h.p ≫ h.opcyclesIso.inv = S.pOpcycles

Tactic:
dsimp [pOpcycles, RightHomologyData.opcyclesIso]
  simp only [p_opcyclesMap', id_τ₂, id_comp]

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
S S₁ S₂ : ShortComplex C
h : S.RightHomologyData
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : h.IsPreservedBy F
this✝ : PreservesColimit (parallelPair S.f 0) F
this : PreservesLimit (parallelPair h.g' 0) F
⊢ F.map S.f ≫ F.map h.p = 0

Tactic:
rw [← F.map_comp, h.wp, F.map_zero]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Injective.Basic

Goal state before:
pp: case h₀
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
P Q : C
inst✝³ : HasZeroMorphisms C
inst✝² : HasBinaryBiproduct P Q
inst✝¹ : Injective P
inst✝ : Injective Q
X✝ Y✝ : C
g : X✝ ⟶ P ⊞ Q
f : X✝ ⟶ Y✝
mono : Mono f
⊢ (f ≫ biprod.lift (factorThru (g ≫ biprod.fst) f) (factorThru (g ≫ biprod.snd) f)) ≫ biprod.fst = g ≫ biprod.fst

Tactic:
simp only [Category.assoc, biprod.lift_fst, comp_factorThru]

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

Goal state before:
pp: case mpr
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ S₂.Exact → S₁.Exact

Tactic:
rintro ⟨h₂, z₂⟩

Goal state after:
case mpr
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
h₂ : S₂.HomologyData
z₂ : IsZero h₂.left.H
⊢ S₁.Exact
Module: Mathlib.Algebra.Homology.ShortComplex.Ab

Goal state before:
pp: S : ShortComplex Ab
hS : S.Exact
inst✝¹ : Finite ↑S.X₁
inst✝ : Finite ↑S.X₃
⊢ Finite ↑S.X₂

Tactic:
have : Finite S.f.hom.range := Set.finite_range _
  have : Finite (S.X₂ ⧸ S.f.hom.range) := by
    rw [hS.ab_range_eq_ker]
    exact .of_equiv _ (QuotientAddGroup.quotientKerEquivRange _).toEquiv.symm
  exact .of_addSubgroup_quotient (H := S.f.hom.range)

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 : ShortComplex C
hS : S.Exact
P : C
f : P ⟶ S.X₂
inst✝ : Projective P
hf : f ≫ S.g = 0
⊢ Projective.factorThru (S.liftCycles f hf) S.toCycles ≫ S.f = f

Tactic:
← toCycles_i,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
S : ShortComplex C
hS : S.Exact
P : C
f : P ⟶ S.X₂
inst✝ : Projective P
hf : f ≫ S.g = 0
⊢ Projective.factorThru (S.liftCycles f hf) S.toCycles ≫ S.toCycles ≫ S.iCycles = f
Module: Mathlib.CategoryTheory.Abelian.Exact

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

Tactic:
apply Limits.kernel.lift_mono

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasPullbacks C
A : C
f₁ f₂ : Subobject A
inst✝ : HasBinaryProduct f₁ f₂
⊢ (f₁ ⨯ f₂) = f₁ ⊓ f₂

Tactic:
apply le_antisymm

Goal state after:
case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasPullbacks C
A : C
f₁ f₂ : Subobject A
inst✝ : HasBinaryProduct f₁ f₂
⊢ (f₁ ⨯ f₂) ≤ f₁ ⊓ f₂

case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasPullbacks C
A : C
f₁ f₂ : Subobject A
inst✝ : HasBinaryProduct f₁ f₂
⊢ f₁ ⊓ f₂ ≤ (f₁ ⨯ f₂)
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✝² : LocallySmall.{w, v₁, u₁} C
inst✝¹ : WellPowered.{w, v₁, u₁} C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
Z✝ : C
u v : Z✝ ⟶ widePullback s
h : u ≫ widePullbackι s = v ≫ widePullbackι s
j : WidePullbackShape ↑(⇑(equivShrink (Subobject A)) '' s)
⊢ u ≫ limit.π (wideCospan s) j = v ≫ limit.π (wideCospan s) j

Tactic:
by
      cases j
      · exact h
      · apply (cancel_mono ((equivShrink (Subobject A)).symm _).arrow).1
        rw [assoc, assoc]
        erw [limit.w (wideCospan s) (WidePullbackShape.Hom.term _)]
        exact h

Goal state after:
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
X : C
Y : Subobject X
W Z : Subobject (underlying.obj Y)
⊢ { toFun := fun Z ↦ ⟨mk (Z.arrow ≫ Y.arrow), ⋯⟩, invFun := fun Z ↦ mk ((↑Z).ofLE Y ⋯), left_inv := ⋯, right_inv := ⋯ }
        W ≤
      { toFun := fun Z ↦ ⟨mk (Z.arrow ≫ Y.arrow), ⋯⟩, invFun := fun Z ↦ mk ((↑Z).ofLE Y ⋯), left_inv := ⋯,
          right_inv := ⋯ }
        Z ↔
    W ≤ Z

Tactic:
dsimp
    constructor
    · intro h
      exact le_of_comm (((underlyingIso _).inv ≫ ofLE _ _ (Subtype.mk_le_mk.mp h) ≫
        (underlyingIso _).hom)) (by cat_disch)
    · intro h
      exact Subtype.mk_le_mk.mpr (le_of_comm
        ((underlyingIso _).hom ≫ ofLE _ _ h ≫ (underlyingIso _).inv) (by simp))

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
⊢ (map₁ η p).yonedaEquivFst = p.yonedaEquivFst

Tactic:
simp only [YonedaCollection.yonedaEquivFst_eq, map₁_fst]

Goal state after: