mathlib-initiative/mathlib-tactics huggingface dataset:
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₂.op.f = 0

pp: case hg₁
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₂.op.g = 0

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₁.op.f = 0

pp: 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
⊢ { X₁ := S₂.op.X₂, X₂ := S₁.op.X₂, X₃ := S₁.op.X₃, f := (opMap φ).τ₂, g := S₁.op.g, zero := ⋯ }.Exact ∧
      Mono (opMap φ).τ₂ ↔
    { X₁ := S₁.X₁, X₂ := S₁.X₂, X₃ := S₂.X₂, f := S₁.f, g := φ.τ₂, zero := ⋯ }.Exact ∧ Epi φ.τ₂

Tactic:
· dsimp
    rw [hg₂, op_zero]

Goal state after:
case hg₁
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₂.op.g = 0

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₁.op.f = 0

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
⊢ { X₁ := S₂.op.X₂, X₂ := S₁.op.X₂, X₃ := S₁.op.X₃, f := (opMap φ).τ₂, g := S₁.op.g, zero := ⋯ }.Exact ∧
      Mono (opMap φ).τ₂ ↔
    { X₁ := S₁.X₁, X₂ := S₁.X₂, X₃ := S₂.X₂, f := S₁.f, g := φ.τ₂, zero := ⋯ }.Exact ∧ Epi φ.τ₂
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f : X✝ ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernels C
X : C
⊢ ∀ ⦃A B : Cᵒᵖ⦄ (f : A ⟶ op X) (g : B ⟶ op X) [Mono f] [Mono g] (i : A ≅ B),
    i.hom ≫ g = f → Subobject.mk (kernel.ι f.unop) = Subobject.mk (kernel.ι g.unop)

Tactic:
rintro A B f g hf hg i rfl
        refine Subobject.mk_eq_mk_of_comm _ _ ?_ ?_
        · exact
            IsLimit.conePointUniqueUpToIso (limit.isLimit _)
              (isKernelCompMono (limit.isLimit (parallelPair g.unop 0)) i.unop.hom rfl)
        · dsimp
          simp only [← Iso.eq_inv_comp, limit.conePointUniqueUpToIso_inv_comp,
            Fork.ofι_π_app]

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
inst✝¹ : HasImages C
inst✝ : HasBinaryCoproducts C
A : C
f g : MonoOver A
⊢ f ⟶ (sup.obj f).obj g

Tactic:
by
  refine homMk (coprod.inl ≫ factorThruImage _) ?_
  erw [Category.assoc, image.fac, coprod.inl_desc]
  rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
x : β
⊢ x ∈ ⇑e '' s → e.symm x ∈ s

Tactic:
rintro ⟨a, m, rfl⟩
    simpa using m

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: case left
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst✝ : HasBinaryProduct A B
this : HasProduct fun x ↦ WalkingPair.casesOn x A B
⊢ WalkingPair.rec (op A) (op B) WalkingPair.left = op (WalkingPair.rec A B WalkingPair.left)

pp: case right
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst✝ : HasBinaryProduct A B
this : HasProduct fun x ↦ WalkingPair.casesOn x A B
⊢ WalkingPair.rec (op A) (op B) WalkingPair.right = op (WalkingPair.rec A B WalkingPair.right)

Tactic:
<;>

Goal state after:
case left
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst✝ : HasBinaryProduct A B
this : HasProduct fun x ↦ WalkingPair.casesOn x A B
⊢ WalkingPair.rec (op A) (op B) WalkingPair.left = op (WalkingPair.rec A B WalkingPair.left)

case right
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst✝ : HasBinaryProduct A B
this : HasProduct fun x ↦ WalkingPair.casesOn x A B
⊢ WalkingPair.rec (op A) (op B) WalkingPair.right = op (WalkingPair.rec A B WalkingPair.right)
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: case h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst✝ : HasBinaryProduct A B
⊢ ((prod.lift coprod.inl.unop coprod.inr.unop).op ≫ coprod.desc prod.fst.op prod.snd.op).unop ≫ prod.fst =
    (𝟙 (op (A ⨯ B))).unop ≫ prod.fst

pp: case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst✝ : HasBinaryProduct A B
⊢ ((prod.lift coprod.inl.unop coprod.inr.unop).op ≫ coprod.desc prod.fst.op prod.snd.op).unop ≫ prod.snd =
    (𝟙 (op (A ⨯ B))).unop ≫ prod.snd

Tactic:
<;>

Goal state after:
case h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst✝ : HasBinaryProduct A B
⊢ ((prod.lift coprod.inl.unop coprod.inr.unop).op ≫ coprod.desc prod.fst.op prod.snd.op).unop ≫ prod.fst =
    (𝟙 (op (A ⨯ B))).unop ≫ prod.fst

case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst✝ : HasBinaryProduct A B
⊢ ((prod.lift coprod.inl.unop coprod.inr.unop).op ≫ coprod.desc prod.fst.op prod.snd.op).unop ≫ prod.snd =
    (𝟙 (op (A ⨯ B))).unop ≫ prod.snd
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: case h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst✝ : HasBinaryProduct A B
⊢ coprod.inl ≫ coprod.desc prod.fst.op prod.snd.op ≫ (prod.lift coprod.inl.unop coprod.inr.unop).op =
    coprod.inl ≫ 𝟙 (op A ⨿ op B)

pp: case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst✝ : HasBinaryProduct A B
⊢ coprod.inr ≫ coprod.desc prod.fst.op prod.snd.op ≫ (prod.lift coprod.inl.unop coprod.inr.unop).op =
    coprod.inr ≫ 𝟙 (op A ⨿ op B)

Tactic:
<;>

Goal state after:
case h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst✝ : HasBinaryProduct A B
⊢ coprod.inl ≫ coprod.desc prod.fst.op prod.snd.op ≫ (prod.lift coprod.inl.unop coprod.inr.unop).op =
    coprod.inl ≫ 𝟙 (op A ⨿ op B)

case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst✝ : HasBinaryProduct A B
⊢ coprod.inr ≫ coprod.desc prod.fst.op prod.snd.op ≫ (prod.lift coprod.inl.unop coprod.inr.unop).op =
    coprod.inr ≫ 𝟙 (op A ⨿ op B)
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasFiniteBiproducts C
inst✝² : HasFiniteColimits C
inst✝¹ : HasCountableProducts C
inst✝ : HasExactLimitsOfShape (Discrete ℕ) C
⊢ CountableAB4Star C

Tactic:
apply +allowSynthFailures CountableAB4Star.of_hasExactLimitsOfShape_nat_and_finite

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasFiniteBiproducts C
inst✝² : HasFiniteColimits C
inst✝¹ : HasCountableProducts C
inst✝ : HasExactLimitsOfShape (Discrete ℕ) C
⊢ ∀ (J : Type) [inst : Finite J], HasExactLimitsOfShape (Discrete J) C
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case none
J : Type w
⊢ (fun f ↦
        match f.left, f.right, f.hom with
        | zero, .(zero), Hom.id .(zero) => none
        | one, .(one), Hom.id .(one) => some none
        | zero, one, line t => some (some t))
      ((fun x ↦
          match x with
          | none => Arrow.mk (𝟙 zero)
          | some none => Arrow.mk (𝟙 one)
          | some (some t) => Arrow.mk (line t))
        none) =
    none

pp: case some.none
J : Type w
⊢ (fun f ↦
        match f.left, f.right, f.hom with
        | zero, .(zero), Hom.id .(zero) => none
        | one, .(one), Hom.id .(one) => some none
        | zero, one, line t => some (some t))
      ((fun x ↦
          match x with
          | none => Arrow.mk (𝟙 zero)
          | some none => Arrow.mk (𝟙 one)
          | some (some t) => Arrow.mk (line t))
        (some none)) =
    some none

pp: case some.some
J : Type w
val✝ : J
⊢ (fun f ↦
        match f.left, f.right, f.hom with
        | zero, .(zero), Hom.id .(zero) => none
        | one, .(one), Hom.id .(one) => some none
        | zero, one, line t => some (some t))
      ((fun x ↦
          match x with
          | none => Arrow.mk (𝟙 zero)
          | some none => Arrow.mk (𝟙 one)
          | some (some t) => Arrow.mk (line t))
        (some (some val✝))) =
    some (some val✝)

Tactic:
<;>

Goal state after:
case none
J : Type w
⊢ (fun f ↦
        match f.left, f.right, f.hom with
        | zero, .(zero), Hom.id .(zero) => none
        | one, .(one), Hom.id .(one) => some none
        | zero, one, line t => some (some t))
      ((fun x ↦
          match x with
          | none => Arrow.mk (𝟙 zero)
          | some none => Arrow.mk (𝟙 one)
          | some (some t) => Arrow.mk (line t))
        none) =
    none

case some.none
J : Type w
⊢ (fun f ↦
        match f.left, f.right, f.hom with
        | zero, .(zero), Hom.id .(zero) => none
        | one, .(one), Hom.id .(one) => some none
        | zero, one, line t => some (some t))
      ((fun x ↦
          match x with
          | none => Arrow.mk (𝟙 zero)
          | some none => Arrow.mk (𝟙 one)
          | some (some t) => Arrow.mk (line t))
        (some none)) =
    some none

case some.some
J : Type w
val✝ : J
⊢ (fun f ↦
        match f.left, f.right, f.hom with
        | zero, .(zero), Hom.id .(zero) => none
        | one, .(one), Hom.id .(one) => some none
        | zero, one, line t => some (some t))
      ((fun x ↦
          match x with
          | none => Arrow.mk (𝟙 zero)
          | some none => Arrow.mk (𝟙 one)
          | some (some t) => Arrow.mk (line t))
        (some (some val✝))) =
    some (some val✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
⊢ F.obj zero = (parallelFamily fun j ↦ F.map (line j)).obj zero

pp: case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
⊢ F.obj one = (parallelFamily fun j ↦ F.map (line j)).obj one

Tactic:
<;>

Goal state after:
case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
⊢ F.obj zero = (parallelFamily fun j ↦ F.map (line j)).obj zero

case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
⊢ F.obj one = (parallelFamily fun j ↦ F.map (line j)).obj one
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
X✝ : WalkingParallelFamily J
⊢ F.map (Hom.id X✝) ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (parallelFamily fun j ↦ F.map (line j)).map (Hom.id X✝)

pp: case line
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
a✝ : J
⊢ F.map (line a✝) ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (parallelFamily fun j ↦ F.map (line j)).map (line a✝)

Tactic:
<;>

Goal state after:
case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
X✝ : WalkingParallelFamily J
⊢ F.map (Hom.id X✝) ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (parallelFamily fun j ↦ F.map (line j)).map (Hom.id X✝)

case line
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
a✝ : J
⊢ F.map (line a✝) ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (parallelFamily fun j ↦ F.map (line j)).map (line a✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (𝟭 (WalkingParallelFamily (ULift.{w, 0} Bool))).obj zero =
    ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
          parallelPair (line { down := true }) (line { down := false })).obj
      zero

pp: case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (𝟭 (WalkingParallelFamily (ULift.{w, 0} Bool))).obj one =
    ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
          parallelPair (line { down := true }) (line { down := false })).obj
      one

Tactic:
<;>

Goal state after:
case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (𝟭 (WalkingParallelFamily (ULift.{w, 0} Bool))).obj zero =
    ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
          parallelPair (line { down := true }) (line { down := false })).obj
      zero

case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (𝟭 (WalkingParallelFamily (ULift.{w, 0} Bool))).obj one =
    ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
          parallelPair (line { down := true }) (line { down := false })).obj
      one
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
X✝ : WalkingParallelFamily (ULift.{w, 0} Bool)
⊢ (𝟭 (WalkingParallelFamily (ULift.{w, 0} Bool))).map (Hom.id X✝) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫
      ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
            parallelPair (line { down := true }) (line { down := false })).map
        (Hom.id X✝)

pp: case line.false
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (𝟭 (WalkingParallelFamily (ULift.{w, 0} Bool))).map (line { down := false }) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫
      ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
            parallelPair (line { down := true }) (line { down := false })).map
        (line { down := false })

pp: case line.true
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (𝟭 (WalkingParallelFamily (ULift.{w, 0} Bool))).map (line { down := true }) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫
      ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
            parallelPair (line { down := true }) (line { down := false })).map
        (line { down := true })

Tactic:
<;>

Goal state after:
case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
X✝ : WalkingParallelFamily (ULift.{w, 0} Bool)
⊢ (𝟭 (WalkingParallelFamily (ULift.{w, 0} Bool))).map (Hom.id X✝) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫
      ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
            parallelPair (line { down := true }) (line { down := false })).map
        (Hom.id X✝)

case line.false
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (𝟭 (WalkingParallelFamily (ULift.{w, 0} Bool))).map (line { down := false }) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫
      ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
            parallelPair (line { down := true }) (line { down := false })).map
        (line { down := false })

case line.true
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (𝟭 (WalkingParallelFamily (ULift.{w, 0} Bool))).map (line { down := true }) ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫
      ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right) ⋙
            parallelPair (line { down := true }) (line { down := false })).map
        (line { down := true })
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (parallelPair (line { down := true }) (line { down := false }) ⋙
          parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
      WalkingParallelPair.zero =
    (𝟭 WalkingParallelPair).obj WalkingParallelPair.zero

pp: case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (parallelPair (line { down := true }) (line { down := false }) ⋙
          parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
      WalkingParallelPair.one =
    (𝟭 WalkingParallelPair).obj WalkingParallelPair.one

Tactic:
<;>

Goal state after:
case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (parallelPair (line { down := true }) (line { down := false }) ⋙
          parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
      WalkingParallelPair.zero =
    (𝟭 WalkingParallelPair).obj WalkingParallelPair.zero

case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (parallelPair (line { down := true }) (line { down := false }) ⋙
          parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
      WalkingParallelPair.one =
    (𝟭 WalkingParallelPair).obj WalkingParallelPair.one
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: case left
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (parallelPair (line { down := true }) (line { down := false }) ⋙
            parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).map
        WalkingParallelPairHom.left ≫
      (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPair).map WalkingParallelPairHom.left

pp: case right
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (parallelPair (line { down := true }) (line { down := false }) ⋙
            parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).map
        WalkingParallelPairHom.right ≫
      (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPair).map WalkingParallelPairHom.right

pp: case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
X✝ : WalkingParallelPair
⊢ (parallelPair (line { down := true }) (line { down := false }) ⋙
            parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).map
        (WalkingParallelPairHom.id X✝) ≫
      (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPair).map (WalkingParallelPairHom.id X✝)

Tactic:
<;>

Goal state after:
case left
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (parallelPair (line { down := true }) (line { down := false }) ⋙
            parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).map
        WalkingParallelPairHom.left ≫
      (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPair).map WalkingParallelPairHom.left

case right
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (parallelPair (line { down := true }) (line { down := false }) ⋙
            parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).map
        WalkingParallelPairHom.right ≫
      (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPair).map WalkingParallelPairHom.right

case id
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
X✝ : WalkingParallelPair
⊢ (parallelPair (line { down := true }) (line { down := false }) ⋙
            parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).map
        (WalkingParallelPairHom.id X✝) ≫
      (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPair).map (WalkingParallelPairHom.id X✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ ∀ {X Y : WalkingParallelPair} (f : X ⟶ Y),
    (parallelPair (line { down := true }) (line { down := false }) ⋙
              parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).map
          f ≫
        (eqToIso ⋯).hom =
      (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPair).map f

Tactic:
by
    rintro _ _ (_ | _ | _) <;> cat_disch

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

Goal state before:
pp: case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).map
        ((NatIso.ofComponents (fun X ↦ eqToIso ⋯) @walkingParallelFamilyEquivWalkingParallelPair._proof_3).hom.app
          zero) ≫
      (NatIso.ofComponents (fun X ↦ eqToIso ⋯) @walkingParallelFamilyEquivWalkingParallelPair._proof_6).hom.app
        ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
          zero) =
    𝟙 ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj zero)

pp: case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).map
        ((NatIso.ofComponents (fun X ↦ eqToIso ⋯) @walkingParallelFamilyEquivWalkingParallelPair._proof_3).hom.app
          one) ≫
      (NatIso.ofComponents (fun X ↦ eqToIso ⋯) @walkingParallelFamilyEquivWalkingParallelPair._proof_6).hom.app
        ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
          one) =
    𝟙 ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj one)

Tactic:
<;>

Goal state after:
case zero
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).map
        ((NatIso.ofComponents (fun X ↦ eqToIso ⋯) @walkingParallelFamilyEquivWalkingParallelPair._proof_3).hom.app
          zero) ≫
      (NatIso.ofComponents (fun X ↦ eqToIso ⋯) @walkingParallelFamilyEquivWalkingParallelPair._proof_6).hom.app
        ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
          zero) =
    𝟙 ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj zero)

case one
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
⊢ (parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).map
        ((NatIso.ofComponents (fun X ↦ eqToIso ⋯) @walkingParallelFamilyEquivWalkingParallelPair._proof_3).hom.app
          one) ≫
      (NatIso.ofComponents (fun X ↦ eqToIso ⋯) @walkingParallelFamilyEquivWalkingParallelPair._proof_6).hom.app
        ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj
          one) =
    𝟙 ((parallelFamily fun p ↦ bif p.down then WalkingParallelPairHom.left else WalkingParallelPairHom.right).obj one)