mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u_1
inst✝⁸ : CommRing R
C : Type u
inst✝⁷ : Category.{v, u} C
D : Type u
inst✝⁶ : Category.{v, u} D
inst✝⁵ : Preadditive D
inst✝⁴ : Linear R D
F G : Free R C ⥤ D
inst✝³ : F.Additive
inst✝² : Functor.Linear R F
inst✝¹ : G.Additive
inst✝ : Functor.Linear R G
α : embedding R C ⋙ F ≅ embedding R C ⋙ G
⊢ ∀ {X Y : Free R C} (f : X ⟶ Y), F.map f ≫ (α.app Y).hom = (α.app X).hom ≫ G.map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: X Y Z : Type u
X' Y' Z' : Type v
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
⊢ (↾fun p ↦ (↑p).1) ≫ f = (↾fun p ↦ (↑p).2) ≫ g

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: X Y Z : Type u
X' Y' Z' : Type v
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
f : X ⟶ Z
g : Y ⟶ Z
⊢ ∀ (s : PullbackCone f g), (↾fun x ↦ ⟨((hom s.fst) x, (hom s.snd) x), ⋯⟩) ≫ (pullbackCone f g).fst = s.fst

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: X Y Z : Type u
X' Y' Z' : Type v
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
f : X ⟶ Z
g : Y ⟶ Z
⊢ ∀ (s : PullbackCone f g), (↾fun x ↦ ⟨((hom s.fst) x, (hom s.snd) x), ⋯⟩) ≫ (pullbackCone f g).snd = s.snd

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: X Y S : Type v
f : X ⟶ S
g : Y ⟶ S
c : PullbackCone f g
hc : IsLimit c
x : Types.PullbackObj f g
⊢ (hom c.fst) ((equivPullbackObj hc).symm x) = (↑x).1

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: X Y S : Type v
f : X ⟶ S
g : Y ⟶ S
c : PullbackCone f g
hc : IsLimit c
x : Types.PullbackObj f g
⊢ (hom c.snd) ((equivPullbackObj hc).symm x) = (↑x).2

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: X Y S : Type v
f : X ⟶ S
g : Y ⟶ S
c : PullbackCone f g
hc : IsLimit c
x y : c.pt
h₁ : (hom c.fst) x = (hom c.fst) y
h₂ : (hom c.snd) x = (hom c.snd) y
⊢ (equivPullbackObj hc) x = (equivPullbackObj hc) y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: X Y Z : Type u
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackIsoPullback f g).inv ≫ pullback.fst f g = ↾fun p ↦ (↑p).1

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: X Y Z : Type u
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackIsoPullback f g).inv ≫ pullback.snd f g = ↾fun p ↦ (↑p).2

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max w v)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
F : J → C
inst✝¹ : HasProduct F
inst✝ : PreservesLimit (Discrete.functor F) (forget C)
x : (j : J) → ToType (F j)
j : J
⊢ (hom (Pi.π F j)) ((productEquiv F).symm x) = x j

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
J : Type w
f : J → C
inst✝⁷ : HasProduct f
D : Type t
inst✝⁶ : Category.{r, t} D
FD : D → D → Type u_1
DD : D → Type (max w r)
inst✝⁵ : (X Y : D) → FunLike (FD X Y) (DD X) (DD Y)
inst✝⁴ : ConcreteCategory D FD
F : C ⥤ D
inst✝³ : PreservesLimit (Discrete.functor f) F
inst✝² : HasProduct fun j ↦ F.obj (f j)
inst✝¹ : PreservesLimitsOfShape WalkingCospan (forget D)
inst✝ : PreservesLimit (Discrete.functor fun b ↦ F.obj (f b)) (forget D)
x y : ToType (F.obj (∏ᶜ f))
h : ∀ (i : J), (hom (F.map (Pi.π f i))) x = (hom (F.map (Pi.π f i))) y
⊢ x = y

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
inst✝ : PreservesColimit (Functor.empty C) (forget C)
X : C
h : Nonempty (IsInitial X)
⊢ IsEmpty (ToType X)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
inst✝¹ : PreservesColimit (Functor.empty C) (forget C)
inst✝ : ReflectsColimit (Functor.empty C) (forget C)
X : C
⊢ Nonempty (IsInitial X) ↔ IsEmpty (ToType X)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X₁ X₂ : C
inst✝¹ : HasBinaryProduct X₁ X₂
inst✝ : PreservesLimit (pair X₁ X₂) (forget C)
x : ToType (X₁ ⨯ X₂)
⊢ ((prodEquiv X₁ X₂) x).1 = (hom prod.fst) x

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X₁ X₂ : C
inst✝¹ : HasBinaryProduct X₁ X₂
inst✝ : PreservesLimit (pair X₁ X₂) (forget C)
x : ToType (X₁ ⨯ X₂)
⊢ ((prodEquiv X₁ X₂) x).2 = (hom prod.snd) x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
e : P ≅ PullbackObj f g := h.isoPullback ≪≫ pullbackIsoPullback f g
p : (fun X ↦ X) P
this : (hom fst) p = (hom (pullback.fst f g)) ((hom h.isoPullback.hom) p)
⊢ (hom fst) p = (_root_.Prod.fst ∘ Subtype.val ∘ ⇑(hom e.hom)) p

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X₁ X₂ : C
inst✝¹ : HasBinaryProduct X₁ X₂
inst✝ : PreservesLimit (pair X₁ X₂) (forget C)
x : ToType X₁ × ToType X₂
⊢ (hom prod.fst) ((prodEquiv X₁ X₂).symm x) = x.1

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X₁ X₂ : C
inst✝¹ : HasBinaryProduct X₁ X₂
inst✝ : PreservesLimit (pair X₁ X₂) (forget C)
x : ToType X₁ × ToType X₂
⊢ (hom prod.snd) ((prodEquiv X₁ X₂).symm x) = x.2

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
e : P ≅ PullbackObj f g := h.isoPullback ≪≫ pullbackIsoPullback f g
⊢ ⇑(hom fst) = _root_.Prod.fst ∘ Subtype.val ∘ ⇑(hom e.hom)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
X₁ X₂ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
inst✝¹ : HasPullback f₁ f₂
inst✝ : PreservesLimit (cospan f₁ f₂) (forget C)
x : ToType (pullback f₁ f₂)
⊢ ∃ x₁ x₂, ∃ (h : (hom f₁) x₁ = (hom f₂) x₂), x = pullbackMk f₁ f₂ x₁ x₂ h

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
⊢ Set.range ⇑(hom fst) = ⇑(hom f) ⁻¹' Set.range ⇑(hom g)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
⊢ Set.range ⇑(hom snd) = ⇑(hom g) ⁻¹' Set.range ⇑(hom f)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max v w)
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
B : C
ι : Type w
X : ι → C
f : (j : ι) → X j ⟶ B
inst✝¹ : HasWidePullback B X f
inst✝ : PreservesLimit (wideCospan B X f) (forget C)
x y : ToType (widePullback B X f)
h₀ : (hom (base f)) x = (hom (base f)) y
h : ∀ (j : ι), (hom (π f j)) x = (hom (π f j)) y
⊢ x = y

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type (max v w)
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
B : C
ι : Type w
inst✝² : Nonempty ι
X : ι → C
f : (j : ι) → X j ⟶ B
inst✝¹ : HasWidePullback B X f
inst✝ : PreservesLimit (wideCospan B X f) (forget C)
x y : ToType (widePullback B X f)
h : ∀ (j : ι), (hom (π f j)) x = (hom (π f j)) y
⊢ x = y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPullback t l r b
x₁ y₁ : X₁
h₁ : (hom t) x₁ = (hom t) y₁
h₂ : (hom l) x₁ = (hom l) y₁
⊢ (h.isLimit.conePointUniqueUpToIso (pullbackLimitCone r b).isLimit).toEquiv x₁ =
    (h.isLimit.conePointUniqueUpToIso (pullbackLimitCone r b).isLimit).toEquiv y₁

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPullback t l r b
x₂ : X₂
x₃ : X₃
hx : (hom r) x₂ = (hom b) x₃
⊢ ∃ x₁, (hom t) x₁ = x₂ ∧ (hom l) x₁ = x₃

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
inst✝¹ : HasMultiequalizer I
inst✝ : PreservesLimit I.multicospan (forget C)
x y : ToType (multiequalizer I)
h : ∀ (t : J.L), (hom (Multiequalizer.ι I t)) x = (hom (Multiequalizer.ι I t)) y
⊢ x = y

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
x : ↑(I.multicospan ⋙ forget C).sections
i : J.R
⊢ (hom (I.fst i)) ((fun x_1 ↦ ↑x (WalkingMulticospan.left x_1)) (J.fst i)) =
    (hom (I.snd i)) ((fun x_1 ↦ ↑x (WalkingMulticospan.left x_1)) (J.snd i))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
w : t ≫ r = l ≫ b
h₁ : ∀ (x₁ y₁ : (fun X ↦ X) X₁), (hom t) x₁ = (hom t) y₁ ∧ (hom l) x₁ = (hom l) y₁ → x₁ = y₁
h₂ : ∀ (x₂ : (fun X ↦ X) X₂) (x₃ : (fun X ↦ X) X₃), (hom r) x₂ = (hom b) x₃ → ∃ x₁, (hom t) x₁ = x₂ ∧ (hom l) x₁ = x₃
φ : X₁ ⟶ PullbackObj r b := ↾fun x₁ ↦ ⟨((hom t) x₁, (hom l) x₁), ⋯⟩
x : PullbackObj r b
⊢ (hom r) (↑x).1 = (hom b) (↑x).2

Tactic:
by

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

Goal state before:
pp: ⊢ (decide False, decide True) ∈ {x | x.1 < x.2}

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
x : { x // ∀ (i : J.R), (hom (I.fst i)) (x (J.fst i)) = (hom (I.snd i)) (x (J.snd i)) }
⊢ (fun j ↦
      match j with
      | WalkingMulticospan.left a => ↑x a
      | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b))) ∈
    (I.multicospan ⋙ forget C).sections

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
w : t ≫ r = l ≫ b
h₁ : ∀ (x₁ y₁ : (fun X ↦ X) X₁), (hom t) x₁ = (hom t) y₁ ∧ (hom l) x₁ = (hom l) y₁ → x₁ = y₁
h₂ : ∀ (x₂ : (fun X ↦ X) X₂) (x₃ : (fun X ↦ X) X₃), (hom r) x₂ = (hom b) x₃ → ∃ x₁, (hom t) x₁ = x₂ ∧ (hom l) x₁ = x₃
φ : X₁ ⟶ PullbackObj r b := ↾fun x₁ ↦ ⟨((hom t) x₁, (hom l) x₁), ⋯⟩
⊢ IsIso φ

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (a : (MultispanShape.ofLinearOrder Bool).L),
    a = ⟨(decide False, decide True), instUniqueLOfLinearOrderBool._proof_1⟩

Tactic:
by

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

Goal state before:
pp: J : MulticospanShape
⊢ ∀ {X Y : WalkingMulticospan J} (f : X.Hom Y), (Hom.id X).comp f = f

Tactic:
by

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

Goal state before:
pp: J : MulticospanShape
⊢ ∀ {X Y : WalkingMulticospan J} (f : X.Hom Y), f.comp (Hom.id Y) = f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks

Goal state before:
pp: X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
⊢ IsPullback t l r b ↔
    t ≫ r = l ≫ b ∧
      (∀ (x₁ y₁ : (fun X ↦ X) X₁), (hom t) x₁ = (hom t) y₁ ∧ (hom l) x₁ = (hom l) y₁ → x₁ = y₁) ∧
        ∀ (x₂ : (fun X ↦ X) X₂) (x₃ : (fun X ↦ X) X₃), (hom r) x₂ = (hom b) x₃ → ∃ x₁, (hom t) x₁ = x₂ ∧ (hom l) x₁ = x₃

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
⊢ Function.LeftInverse
    (fun x ↦
      ⟨fun j ↦
        match j with
        | WalkingMulticospan.left a => ↑x a
        | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)),
        ⋯⟩)
    fun x ↦ ⟨fun x_1 ↦ ↑x (WalkingMulticospan.left x_1), ⋯⟩

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
inst✝² : HasForget₂ C Ab
inst✝¹ : HasZeroMorphisms C
inst✝ : (forget₂ C Ab).PreservesZeroMorphisms
S : ShortComplex C
x : ↑((forget₂ C Ab).obj S.X₁)
⊢ (ConcreteCategory.hom ((forget₂ C Ab).map S.g)) ((ConcreteCategory.hom ((forget₂ C Ab).map S.f)) x) = 0

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
⊢ Mono f ↔ Function.Injective ⇑(ConcreteCategory.hom ((forget₂ C Ab).map f))

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type s
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
J : MulticospanShape
I : MulticospanIndex J C
⊢ Function.RightInverse
    (fun x ↦
      ⟨fun j ↦
        match j with
        | WalkingMulticospan.left a => ↑x a
        | WalkingMulticospan.right b => (hom (I.fst b)) (↑x (J.fst b)),
        ⋯⟩)
    fun x ↦ ⟨fun x_1 ↦ ↑x (WalkingMulticospan.left x_1), ⋯⟩

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
⊢ Mono f ↔ Function.Injective ⇑(ConcreteCategory.hom f)

Tactic:
by

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

Goal state before:
pp: J : MulticospanShape
⊢ ∀ {W X Y Z : WalkingMulticospan J} (f : W.Hom X) (g : X.Hom Y) (h : Y.Hom Z), (f.comp g).comp h = f.comp (g.comp h)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
x : ToType (widePushout B X f)
⊢ (∃ y, (hom (head f)) y = x) ∨ ∃ i y, (hom (ι f i)) y = x

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁴ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝³ : ConcreteCategory C FC
B : C
α : Type v
inst✝² : Nonempty α
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
x : ToType (widePushout B X f)
⊢ ∃ i y, (hom (ι f i)) y = x

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
FC : C → C → Type u_2
CC : C → Type u_3
inst✝² : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝¹ : ConcreteCategory C FC
M N K : C
f : M ⟶ N
inst✝ : HasCokernel f
g h : cokernel f ⟶ K
w : ∀ (n : ToType N), (hom g) ((hom (cokernel.π f)) n) = (hom h) ((hom (cokernel.π f)) n)
⊢ g = h

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
⊢ Epi f ↔ Function.Surjective ⇑(ConcreteCategory.hom ((forget₂ C Ab).map f))

Tactic:
by

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

Goal state before:
pp: J : MulticospanShape
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : WalkingMulticospan J ⥤ C
left : (i : J.L) → F.obj (WalkingMulticospan.left i) ≅ G.obj (WalkingMulticospan.left i)
right : (i : J.R) → F.obj (WalkingMulticospan.right i) ≅ G.obj (WalkingMulticospan.right i)
wl : ∀ (i : J.R), F.map (Hom.fst i) ≫ (right i).hom = (left (J.fst i)).hom ≫ G.map (Hom.fst i)
wr : ∀ (i : J.R), F.map (Hom.snd i) ≫ (right i).hom = (left (J.snd i)).hom ≫ G.map (Hom.snd i)
⊢ ∀ {X Y : WalkingMulticospan J} (f : X ⟶ Y),
    F.map f ≫
        (match Y with
          | WalkingMulticospan.left i => left i
          | WalkingMulticospan.right i => right i).hom =
      (match X with
          | WalkingMulticospan.left i => left i
          | WalkingMulticospan.right i => right i).hom ≫
        G.map f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
inst✝ : HasZeroObject C
X Y : C
f : X ⟶ Y
⊢ Epi f ↔ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
by

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

Goal state before:
pp: J : MulticospanShape
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : WalkingMulticospan J ⥤ C
left : ∀ (i : J.L), F.obj (WalkingMulticospan.left i) = G.obj (WalkingMulticospan.left i)
right : ∀ (i : J.R), F.obj (WalkingMulticospan.right i) = G.obj (WalkingMulticospan.right i)
wl : ∀ (i : J.R), F.map (Hom.fst i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ G.map (Hom.fst i)
wr : ∀ (i : J.R), F.map (Hom.snd i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ G.map (Hom.snd i)
⊢ ∀ (X : WalkingMulticospan J), F.obj X = G.obj X

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
S : ShortComplex C
inst✝ : S.HasHomology
⊢ S.Exact ↔
    ∀ (x₂ : ↑((forget₂ C Ab).obj S.X₂)),
      (ConcreteCategory.hom ((forget₂ C Ab).map S.g)) x₂ = 0 →
        ∃ x₁, (ConcreteCategory.hom ((forget₂ C Ab).map S.f)) x₁ = x₂

Tactic:
by

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

Goal state before:
pp: J : MulticospanShape
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : WalkingMulticospan J ⥤ C
left : ∀ (i : J.L), F.obj (WalkingMulticospan.left i) = G.obj (WalkingMulticospan.left i)
right : ∀ (i : J.R), F.obj (WalkingMulticospan.right i) = G.obj (WalkingMulticospan.right i)
wl : ∀ (i : J.R), F.map (Hom.fst i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ G.map (Hom.fst i)
wr : ∀ (i : J.R), F.map (Hom.snd i) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ G.map (Hom.snd i)
⊢ ∀ (X : WalkingMulticospan J), (functorExt (fun x ↦ eqToIso ⋯) (fun x ↦ eqToIso ⋯) wl wr).hom.app X = eqToHom ⋯

Tactic:
by

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

Goal state before:
pp: J : MultispanShape
inst✝¹ : Small.{t, w} J.L
inst✝ : Small.{t, w'} J.R
⊢ Function.Surjective (Sum.elim left right)

Tactic:
by

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

Goal state before:
pp: J : MultispanShape
⊢ ∀ {X Y : WalkingMultispan J} (f : X.Hom Y), (Hom.id X).comp f = f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
S : ShortComplex C
inst✝ : HasZeroObject C
hS : S.ShortExact
⊢ Function.Injective ⇑(ConcreteCategory.hom ((forget₂ C Ab).map S.f))

Tactic:
by

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

Goal state before:
pp: J : MultispanShape
⊢ ∀ {X Y : WalkingMultispan J} (f : X.Hom Y), f.comp (Hom.id Y) = f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
S : ShortComplex C
inst✝ : HasZeroObject C
hS : S.ShortExact
⊢ Function.Surjective ⇑(ConcreteCategory.hom ((forget₂ C Ab).map S.g))

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝⁶ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁵ : ConcreteCategory C FC
inst✝⁴ : HasForget₂ C Ab
inst✝³ : Preadditive C
inst✝² : (forget₂ C Ab).Additive
inst✝¹ : (forget₂ C Ab).PreservesHomology
S : ShortComplex C
inst✝ : S.HasHomology
x₂ : ↑((forget₂ C Ab).obj S.X₂)
hx₂ : (ConcreteCategory.hom ((forget₂ C Ab).map S.g)) x₂ = 0
⊢ (ConcreteCategory.hom ((forget₂ C Ab).map S.iCycles)) (S.cyclesMk x₂ hx₂) = x₂

Tactic:
by

Goal state after: