mathlib-initiative/mathlib-tactics huggingface dataset:
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
A : Type u_1
inst✝³ : Semiring A
inst✝² : Module A V
inst✝¹ : SMul K A
inst✝ : IsScalarTower K A V
h : finrank K V = 1
this : Nontrivial V
S : Submodule A V
hn : ¬S = ⊥
⊢ S = ⊤

Tactic:
rw [← restrictScalars_inj K] at hn ⊢

Goal state after:
K : Type u
V : Type v
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
A : Type u_1
inst✝³ : Semiring A
inst✝² : Module A V
inst✝¹ : SMul K A
inst✝ : IsScalarTower K A V
h : finrank K V = 1
this : Nontrivial V
S : Submodule A V
hn : ¬restrictScalars K S = restrictScalars K ⊥
⊢ restrictScalars K S = restrictScalars K ⊤
Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic

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

Tactic:
by
        rw [evaluation_coevaluation'']; monoidal

Goal state after:
Module: Mathlib.LinearAlgebra.Coevaluation

Goal state before:
pp: K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (∑ x, if j = x then (Basis.ofVectorSpace K V) x ⊗ₜ[K] 1 else 0) = (Basis.ofVectorSpace K V) j ⊗ₜ[K] 1

Tactic:
Finset.sum_ite_eq

Goal state after:
K : Type u
inst✝³ : Field K
V : Type v
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)
j : ↑(Basis.ofVectorSpaceIndex K V)
⊢ (if j ∈ Finset.univ then (Basis.ofVectorSpace K V) j ⊗ₜ[K] 1 else 0) = (Basis.ofVectorSpace K V) j ⊗ₜ[K] 1
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
⊢ lift.{v, u_2} (Module.rank K M) < ℵ₀

Tactic:
· rw [lift_lt_aleph0]; have := Module.nontrivial K L; apply Module.rank_lt_aleph0

Goal state after:
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
I : R →+* R
B : M →ₛₗ[I] M →ₗ[R] R
H : B.IsSymm
p : Submodule R M
x✝¹ x✝ : ↥p
⊢ I ((B ↑x✝¹) ↑x✝) = (B ↑x✝) ↑x✝¹

Tactic:
exact H.eq _ _

Goal state after:
Module: Mathlib.LinearAlgebra.Contraction

Goal state before:
pp: case inl
ι : 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
h : Function.Bijective ⇑(dualTensorHom R M N)
h✝ : Finite ι
⊢ Function.Bijective ⇑(finsuppLinearMap R)

pp: case inr
ι : 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
h : Function.Bijective ⇑(dualTensorHom R M N)
h✝ : Module.Finite R M
⊢ Function.Bijective ⇑(finsuppLinearMap R)

Tactic:
· apply finsuppLinearMap_bijective_of_finite

Goal state after:
case inr
ι : 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
h : Function.Bijective ⇑(dualTensorHom R M N)
h✝ : Module.Finite R M
⊢ Function.Bijective ⇑(finsuppLinearMap R)
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
inst✝² : HasCoequalizer f g
inst✝¹ : HasCoequalizer (G.map f) (G.map g)
inst✝ : PreservesColimit (parallelPair f g) G
⊢ coequalizer.π (G.map f) (G.map g) ≫ coequalizerComparison f g G ≫ (PreservesCoequalizer.iso G f g).inv =
    coequalizer.π (G.map f) (G.map g)

Tactic:
← PreservesCoequalizer.iso_hom,

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
f g : X ⟶ Y
inst✝² : HasCoequalizer f g
inst✝¹ : HasCoequalizer (G.map f) (G.map g)
inst✝ : PreservesColimit (parallelPair f g) G
⊢ coequalizer.π (G.map f) (G.map g) ≫ (PreservesCoequalizer.iso G f g).hom ≫ (PreservesCoequalizer.iso G f g).inv =
    coequalizer.π (G.map f) (G.map g)
Module: Mathlib.LinearAlgebra.SesquilinearForm.Basic

Goal state before:
pp: 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
hB : IsSymm B
x y : M
⊢ (B x) y * (B y) x ≤ (B x) x * (B y) y

Tactic:
exact apply_mul_apply_le_of_forall_zero_le B hs x y

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

Goal state before:
pp: 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 ≫ t₂.desc (Cofan.mk q.1 fun j ↦ q.ι.app j) = t ≫ t₂.desc (Cofan.mk q.1 fun j ↦ q.ι.app j)

Tactic:
apply t₁.hom_ext

Goal state after:
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
⊢ ∀ (j : Discrete ((p : J × J) × (p.1 ⟶ p.2))),
    c₁.ι.app j ≫ s ≫ t₂.desc (Cofan.mk q.1 fun j ↦ q.ι.app j) =
      c₁.ι.app j ≫ t ≫ t₂.desc (Cofan.mk q.1 fun j ↦ q.ι.app j)
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
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f ↦ K.obj f.fst.1
⊢ PreservesColimit K G

Tactic:
let s : Q ⟶ P := Sigma.desc fun f => K.map f.2 ≫ colimit.ι (Discrete.functor K.obj) ⟨_⟩

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
inst✝⁷ : SmallCategory J
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasColimitsOfShape (Discrete J) C
inst✝⁴ : HasColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst✝³ : HasCoequalizers C
G : C ⥤ D
inst✝² : PreservesColimitsOfShape WalkingParallelPair G
inst✝¹ : PreservesColimitsOfShape (Discrete J) G
inst✝ : PreservesColimitsOfShape (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : J ⥤ C
P : C := ∐ K.obj
Q : C := ∐ fun f ↦ K.obj f.fst.1
s : Q ⟶ P := Sigma.desc fun f ↦ K.map f.snd ≫ colimit.ι (Discrete.functor K.obj) { as := f.fst.2 }
⊢ PreservesColimit K G
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✝² : HasFiniteProducts C
inst✝¹ : HasKernels C
inst✝ : IsNormalMonoCategory C
X Y : C
f : X ⟶ Y
Z : C
l : IsColimit (CokernelCofork.ofπ 0 ⋯)
Z✝ : C
u v : Y ⟶ Z✝
huv : f ≫ u = f ≫ v
W : C
w : Y ⟶ W
hw : equalizer.ι u v ≫ w = 0
hl : IsLimit (KernelFork.ofι (equalizer.ι u v) hw)
m : X ⟶ equalizer u v
hm : m ≫ equalizer.ι u v = f
⊢ u = v

Tactic:
have hwf : f ≫ w = 0 := by rw [← hm, Category.assoc, hw, comp_zero]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasFiniteProducts C
inst✝¹ : HasKernels C
inst✝ : IsNormalMonoCategory C
X Y : C
f : X ⟶ Y
Z : C
l : IsColimit (CokernelCofork.ofπ 0 ⋯)
Z✝ : C
u v : Y ⟶ Z✝
huv : f ≫ u = f ≫ v
W : C
w : Y ⟶ W
hw : equalizer.ι u v ≫ w = 0
hl : IsLimit (KernelFork.ofι (equalizer.ι u v) hw)
m : X ⟶ equalizer u v
hm : m ≫ equalizer.ι u v = f
hwf : f ≫ w = 0
⊢ u = v
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 : X ⟶ Y
Z : C
l : IsLimit (KernelFork.ofι 0 ⋯)
Z✝ : C
u v : Z✝ ⟶ X
huv : u ≫ f = v ≫ f
W : C
w : W ⟶ X
hw : w ≫ coequalizer.π u v = 0
hl : IsColimit (CokernelCofork.ofπ (coequalizer.π u v) hw)
m : coequalizer u v ⟶ Y
hm : coequalizer.π u v ≫ m = f
reassoced : ∀ {W_1 : C} (h : coequalizer u v ⟶ W_1), w ≫ coequalizer.π u v ≫ h = 0 ≫ h
hwf : w ≫ f = 0
n : W ⟶ (KernelFork.ofι 0 ⋯).pt
hn : 0 = w
this : IsIso (coequalizer.π u v)
⊢ u ≫ coequalizer.π u v = v ≫ coequalizer.π u v

Tactic:
exact coequalizer.condition _ _

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)
⊢ (β⁻¹ * β) • x = x

Tactic:
inv_mul_cancel,

Goal state after:
A B : GrpCat
f : A ⟶ B
β : ↑B
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ 1 • x = x
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:
inv_mul_cancel,

Goal state after:
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 = 1 * b
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 S₁ S₂ S₃ : ShortComplex C
inst✝ : S.HasRightHomology
hg : S.g = 0
⊢ S.opcycles ≅ S.rightHomology

Tactic:
have := S.isIso_rightHomologyι hg

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
inst✝ : S.HasRightHomology
hg : S.g = 0
this : IsIso S.rightHomologyι
⊢ S.opcycles ≅ S.rightHomology
Module: Mathlib.Algebra.Homology.ShortComplex.Homology

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
hg : S.g = 0
inst✝ : S.HasHomology
⊢ IsIso S.homologyι

Tactic:
have := S.isIso_rightHomologyι hg

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
hg : S.g = 0
inst✝ : S.HasHomology
this : IsIso S.rightHomologyι
⊢ IsIso S.homologyι
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), (c.ι.app j).τ₁ ≫ h₁.desc (π₁.mapCocone s) = (s.ι.app j).τ₁
eq₂ : ∀ (j : J), (c.ι.app j).τ₂ ≫ h₂.desc (π₂.mapCocone s) = (s.ι.app j).τ₂
eq₁₂ : ∀ (j : J), (c.ι.app j).τ₁ ≫ c.pt.f = (F.obj j).f ≫ (c.ι.app j).τ₂
eq₁₂' : ∀ (j : J), (s.ι.app j).τ₁ ≫ s.pt.f = (F.obj j).f ≫ (s.ι.app j).τ₂
⊢ (c.ι.app j).τ₁ ≫ h₁.desc (π₁.mapCocone s) ≫ s.pt.f = (c.ι.app j).τ₁ ≫ c.pt.f ≫ h₂.desc (π₂.mapCocone s)

Tactic:
rw [reassoc_of% (eq₁ j), eq₁₂', reassoc_of% eq₁₂, eq₂]

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
Z'✝ : C
k : cokernel S.f ⟶ Z'✝
hk : (kernel.ι S.g ≫ cokernel.π S.f) ≫ k = 0
b : Abelian.coimage S.g ⟶ Z'✝
hb : S.cokernelToAbelianCoimage ≫ b = k
⊢ b = cokernel.desc (kernel.ι S.g) (cokernel.π S.f ≫ k) ⋯

Tactic:
by
      simp only [← cancel_epi S.cokernelToAbelianCoimage, ← cancel_epi (cokernel.π S.f), hb,
        cokernel_π_comp_cokernelToAbelianCoimage_assoc, cokernel.π_desc]

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 : ShortComplex C
hr : S.RightHomologyData
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : S.HasRightHomology
inst✝ : F.PreservesRightHomologyOf S
⊢ rightHomologyMap' (𝟙 (S.map F)) (S.map F).rightHomologyData (S.rightHomologyData.map F) =
    rightHomologyMap' (𝟙 (S.map F)) (S.map F).rightHomologyData (hr.map F) ≫
      F.map (rightHomologyMap' (𝟙 S) hr S.rightHomologyData)

Tactic:
simp only [map_rightHomologyMap', ← rightHomologyMap'_comp, Functor.map_id, comp_id,
    Functor.mapShortComplex_obj]

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

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

Tactic:
← unop_id,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
A B : Cᵒᵖ
g : A ⟶ B
⊢ (kernel.lift f.op (cokernel.π f).op ⋯).unop ≫ cokernel.desc f (kernel.ι f.op).unop ⋯ = (𝟙 (kernel f.op)).unop
Module: Mathlib.CategoryTheory.Abelian.Opposite

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

Tactic:
← unop_id,

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

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 : ShortComplex C
hS : S.ShortExact
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteColimits F
⊢ (S.map F).ShortExact

Tactic:
by
  have := hS.mono_f
  have := hS.epi_g
  exact hS.map F

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.LeftExact

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : HasBinaryBiproducts C
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := ⋯
this : F.Additive
c : Cocone (parallelPair f g)
i : IsColimit c
c' : IsColimit (CokernelCofork.ofπ (Cofork.π c) ⋯) := ⋯
iFc : IsColimit (CokernelCofork.ofπ (F.map (Cofork.π c)) ⋯) := ⋯
⊢ IsColimit (Cofork.ofπ (F.map (Cofork.π c)) ⋯)

Tactic:
let p : parallelPair (F.map (f - g)) 0 ≅ parallelPair (F.map f - F.map g) 0 :=
    parallelPair.ext (Iso.refl _) (Iso.refl _) (by simp) (by simp)

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : HasBinaryBiproducts C
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproducts_of_preservesBinaryCoproducts F
this : F.Additive
c : Cocone (parallelPair f g)
i : IsColimit c
c' : IsColimit (CokernelCofork.ofπ (Cofork.π c) ⋯) :=
  isColimitCokernelCoforkOfCofork (i.ofIsoColimit (Cofork.isoCoforkOfπ c))
iFc : IsColimit (CokernelCofork.ofπ (F.map (Cofork.π c)) ⋯) := isColimitCoforkMapOfIsColimit' F ⋯ c'
p : parallelPair (F.map (f - g)) 0 ≅ parallelPair (F.map f - F.map g) 0 :=
  parallelPair.ext (Iso.refl ((parallelPair (F.map (f - g)) 0).obj WalkingParallelPair.zero))
    (Iso.refl ((parallelPair (F.map (f - g)) 0).obj WalkingParallelPair.one)) ⋯ ⋯
⊢ IsColimit (Cofork.ofπ (F.map (Cofork.π c)) ⋯)
Module: Mathlib.CategoryTheory.Adjunction.Restrict

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
iC : C ⥤ C'
iD : D ⥤ D'
L' : C' ⥤ D'
R' : D' ⥤ C'
adj : L' ⊣ R'
hiC : iC.FullyFaithful
hiD : iD.FullyFaithful
L : C ⥤ D
R : D ⥤ C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
X : C
Y' Y : D
f : L.obj X ⟶ Y'
g : Y' ⟶ Y
⊢ (Trans.trans
        (Trans.trans
          (Trans.trans (Trans.trans hiD.homEquiv ((comm1.symm.app X).homCongr (Iso.refl (iD.obj Y))))
            (adj.homEquiv (iC.obj X) (iD.obj Y)))
          ((Iso.refl (iC.obj X)).homCongr (comm2.app Y)))
        hiC.homEquiv.symm)
      (f ≫ g) =
    (Trans.trans
          (Trans.trans
            (Trans.trans (Trans.trans hiD.homEquiv ((comm1.symm.app X).homCongr (Iso.refl (iD.obj Y'))))
              (adj.homEquiv (iC.obj X) (iD.obj Y')))
            ((Iso.refl (iC.obj X)).homCongr (comm2.app Y')))
          hiC.homEquiv.symm)
        f ≫
      R.map g

Tactic:
by
        apply hiC.map_injective
        suffices R'.map (iD.map g) ≫ comm2.hom.app Y = comm2.hom.app Y' ≫ iC.map (R.map g) by
          simp [Trans.trans, this]
        apply comm2.hom.naturality g

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

Goal state before:
pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
P✝ : Subobject Y
f : X ⟶ Y
P Q : MonoOver Y
h : P ≅ Q
⊢ Q.Factors f → P.Factors f

Tactic:
rintro ⟨i, w⟩
        exact ⟨i ≫ h.inv.hom.left, by rw [Category.assoc, Over.w h.inv.hom, w]⟩

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 : S.Exact
hf : S.f = 0
hg : S.g = 0
⊢ IsZero S.X₂

Tactic:
by
  have := hS.mono_g hf
  rw [IsZero.iff_id_eq_zero, ← cancel_mono S.g, hg, comp_zero, comp_zero]

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
B : C
X Y : Subobject B
f : underlying.obj X ⟶ underlying.obj Y
w : f ≫ Y.arrow = X.arrow
⊢ X ≤ Y

Tactic:
by
  convert! mk_le_mk_of_comm _ w <;> simp

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

Goal state before:
pp: case hf₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
⊢ S₂.g.op = 0

Tactic:
rw [hg₂, op_zero]

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasImages V
D : V
h : C ⟶ D
w : f ≫ g = 0
⊢ f ≫ g ≫ h = 0

Tactic:
simp [reassoc_of% w]

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
B : C
⊢ IsIso ⊤.arrow

Tactic:
← underlyingIso_top_hom

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
B : C
⊢ IsIso (underlyingIso (𝟙 B)).hom
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y : C
g : X ⟶ Y
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (pullback g).obj ((inf.obj (Quotient.mk'' f₁)).obj f₂) =
    (inf.obj ((pullback g).obj (Quotient.mk'' f₁))).obj ((pullback g).obj f₂)

Tactic:
inf_eq_map_pullback',

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y : C
g : X ⟶ Y
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (pullback g).obj ((map f₁.arrow).obj ((pullback f₁.arrow).obj f₂)) =
    (inf.obj ((pullback g).obj (Quotient.mk'' f₁))).obj ((pullback g).obj f₂)
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y : C
g : X ⟶ Y
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (pullback g).obj ((map f₁.arrow).obj ((pullback f₁.arrow).obj f₂)) =
    (inf.obj ((pullback g).obj (Quotient.mk'' f₁))).obj ((pullback g).obj f₂)

Tactic:
inf_eq_map_pullback',

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
X Y : C
g : X ⟶ Y
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (pullback g).obj ((map f₁.arrow).obj ((pullback f₁.arrow).obj f₂)) =
    (map ((MonoOver.pullback g).obj f₁).arrow).obj
      ((pullback ((MonoOver.pullback g).obj f₁).arrow).obj ((pullback g).obj f₂))
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasPullbacks C
X Y : C
g : Y ⟶ X
inst✝ : Mono g
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (map g).obj ((inf.obj (Quotient.mk'' f₁)).obj f₂) = (inf.obj ((map g).obj (Quotient.mk'' f₁))).obj ((map g).obj f₂)

Tactic:
inf_eq_map_pullback',

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasPullbacks C
X Y : C
g : Y ⟶ X
inst✝ : Mono g
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (map g).obj ((map f₁.arrow).obj ((pullback f₁.arrow).obj f₂)) =
    (inf.obj ((map g).obj (Quotient.mk'' f₁))).obj ((map g).obj f₂)
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasPullbacks C
X Y : C
g : Y ⟶ X
inst✝ : Mono g
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (map g).obj ((map f₁.arrow).obj ((pullback f₁.arrow).obj f₂)) =
    (inf.obj ((map g).obj (Quotient.mk'' f₁))).obj ((map g).obj f₂)

Tactic:
inf_eq_map_pullback',

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasPullbacks C
X Y : C
g : Y ⟶ X
inst✝ : Mono g
f₂ : Subobject Y
f₁ : MonoOver Y
⊢ (map g).obj ((map f₁.arrow).obj ((pullback f₁.arrow).obj f₂)) =
    (map ((MonoOver.map g).obj f₁).arrow).obj ((pullback ((MonoOver.map g).obj f₁).arrow).obj ((map g).obj f₂))
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A B : C
inst✝ : HasBinaryProduct A B
⊢ coprod.inl.unop.op = coprod.inl

Tactic:
Quiver.Hom.op_unop

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A B : C
inst✝ : HasBinaryProduct A B
⊢ coprod.inl = coprod.inl
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A B : C
inst✝ : HasBinaryProduct A B
⊢ coprod.inr.unop.op = coprod.inr

Tactic:
Quiver.Hom.op_unop

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A B : C
inst✝ : HasBinaryProduct A B
⊢ coprod.inr = coprod.inr
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Functor

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : C ⥤ D
d : D
⊢ (map (𝟙 d)).toCatHom = 𝟙 (Cat.of (CostructuredArrow T d))

Tactic:
ext
    exact Functor.ext (fun ⟨_, _, _⟩ => by simp [CostructuredArrow.map, Comma.mapRight])

Goal state after: