awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.GradedObject.Unitor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D : Type u_4
I₁ : Type u_5
I₂ : Type u_6
I₃ : Type u_7
J : Type u_8
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} D
inst_4 : Zero I₂
inst_5 : DecidableEq I₂
inst_6 : HasInitial.{v_2, u_2} C₂
F₁ : C₁ ⥤ Functor.{v_2, v_1, u_2, u_1} C₂ C₁
F₂ : C₂ ⥤ Functor.{v_3, v_3, u_3, u_3} C₃ C₃
G : C₁ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ D
associator : bifunctorComp₁₂ F₁ G ≅ bifunctorComp₂₃ G F₂
X₂ : C₂
e₁ : F₁.flip.obj X₂ ≅ 𝟭 C₁
e₂ : F₂.obj X₂ ≅ 𝟭 C₃
inst_7 : ∀ (X₁ : C₁), PreservesColimit (Functor.empty C₂) (F₁.obj X₁)
inst_8 : ∀ (X₃ : C₃), PreservesColimit (Functor.empty C₂) (F₂.flip.obj X₃)
r : I₁ × I₂ × I₃ → J
π : I₁ × I₃ → J
τ : TriangleIndexData r π
X₁ : GradedObject I₁ C₁
X₃ : GradedObject I₃ C₃
inst_9 : (((mapBifunctor F₁ I₁ I₂).obj X₁).obj (Functor.obj (single₀ I₂) X₂)).HasMap τ.p₁₂
inst_10 : (((mapBifunctor G I₁ I₃).obj (mapBifunctorMapObj F₁ τ.p₁₂ X₁ (Functor.obj (single₀ I₂) X₂))).obj X₃).HasMap π
inst_11 : (((mapBifunctor F₂ I₂ I₃).obj (Functor.obj (single₀ I₂) X₂)).obj X₃).HasMap τ.p₂₃
inst_12 : (((mapBifunctor G I₁ I₃).obj X₁).obj (mapBifunctorMapObj F₂ τ.p₂₃ (Functor.obj (single₀ I₂) X₂) X₃)).HasMap π
inst_13 : HasGoodTrifunctor₁₂Obj F₁ G τ.ρ₁₂ X₁ (Functor.obj (single₀ I₂) X₂) X₃
inst_14 : HasGoodTrifunctor₂₃Obj G F₂ τ.ρ₂₃ X₁ (Functor.obj (single₀ I₂) X₂) X₃
inst_15 : (((mapBifunctor G I₁ I₃).obj X₁).obj X₃).HasMap π
triangle :
  ∀ (X₁ : C₁) (X₃ : C₃),
    ((associator.hom.app X₁).app X₂).app X₃ ≫ (G.obj X₁).map (e₂.hom.app X₃) = (G.map (e₁.hom.app X₁)).app X₃
j : J
i₁ : I₁
i₃ : I₃
hj : π (i₁, i₃) = j
⊢ Eq (α :=
    (G.obj ((F₁.obj (X₁ i₁)).obj (Functor.obj (single₀ I₂) X₂ 0))).obj (X₃ i₃) ⟶
      (G.obj (X₁ i₁)).obj ((F₂.obj X₂).obj (X₃ i₃)))
    (NatTrans.app (G.map ((F₁.obj (X₁ i₁)).map (Iso.hom (singleObjApplyIso 0 X₂)))) (X₃ i₃) ≫
      NatTrans.app (NatTrans.app (associator.hom.app (X₁ i₁)) X₂) (X₃ i₃))
    (NatTrans.app (NatTrans.app (associator.hom.app (X₁ i₁)) (Functor.obj (single₀ I₂) X₂ 0)) (X₃ i₃) ≫
      (G.obj (X₁ i₁)).map (NatTrans.app (F₂.map (Iso.hom (singleObjApplyIso 0 X₂))) (X₃ i₃)))

Tactic:
apply NatTrans.naturality_app (associator.hom.app (X₁ i₁))

Premises used: CategoryTheory.NatTrans.naturality_app, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
⊢ Membership.mem (γ := Set (Bool × Bool)) {x : Bool × Bool | x.1 < x.2} (decide False, decide True)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
property : Membership.mem (γ := Set (Bool × Bool)) {x : Bool × Bool | x.1 < x.2} (false, false)
⊢ Subtype.mk (p := fun (x : Bool × Bool) ↦ Membership.mem (γ := Set (Bool × Bool)) {x : Bool × Bool | x.1 < x.2} x)
      (false, false) property =
    Subtype.mk (p := fun (x : Bool × Bool) ↦ Membership.mem (γ := Set (Bool × Bool)) {x : Bool × Bool | x.1 < x.2} x)
      (decide False, decide True) instUniqueLOfLinearOrderBool._proof_1

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
property : Membership.mem (γ := Set (Bool × Bool)) {x : Bool × Bool | x.1 < x.2} (false, true)
⊢ Subtype.mk (p := fun (x : Bool × Bool) ↦ Membership.mem (γ := Set (Bool × Bool)) {x : Bool × Bool | x.1 < x.2} x)
      (false, true) property =
    Subtype.mk (p := fun (x : Bool × Bool) ↦ Membership.mem (γ := Set (Bool × Bool)) {x : Bool × Bool | x.1 < x.2} x)
      (decide False, decide True) instUniqueLOfLinearOrderBool._proof_1

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
property : Membership.mem (γ := Set (Bool × Bool)) {x : Bool × Bool | x.1 < x.2} (true, false)
⊢ Subtype.mk (p := fun (x : Bool × Bool) ↦ Membership.mem (γ := Set (Bool × Bool)) {x : Bool × Bool | x.1 < x.2} x)
      (true, false) property =
    Subtype.mk (p := fun (x : Bool × Bool) ↦ Membership.mem (γ := Set (Bool × Bool)) {x : Bool × Bool | x.1 < x.2} x)
      (decide False, decide True) instUniqueLOfLinearOrderBool._proof_1

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
property : Membership.mem (γ := Set (Bool × Bool)) {x : Bool × Bool | x.1 < x.2} (true, true)
⊢ Subtype.mk (p := fun (x : Bool × Bool) ↦ Membership.mem (γ := Set (Bool × Bool)) {x : Bool × Bool | x.1 < x.2} x)
      (true, true) property =
    Subtype.mk (p := fun (x : Bool × Bool) ↦ Membership.mem (γ := Set (Bool × Bool)) {x : Bool × Bool | x.1 < x.2} x)
      (decide False, decide True) instUniqueLOfLinearOrderBool._proof_1

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MulticospanShape
a : J.L
⊢ (Hom.id (left a)).comp (Hom.id (left a)) = Hom.id (left a)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MulticospanShape
a : J.R
⊢ (Hom.id (left (J.fst a))).comp (Hom.fst a) = Hom.fst a

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MulticospanShape
a : J.R
⊢ (Hom.id (left (J.snd a))).comp (Hom.snd a) = Hom.snd a

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MulticospanShape
a : J.R
⊢ (Hom.id (right a)).comp (Hom.id (right a)) = Hom.id (right a)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MulticospanShape
a : J.R
⊢ (Hom.fst a).comp (Hom.id (right a)) = Hom.fst a

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MulticospanShape
a : J.R
⊢ (Hom.snd a).comp (Hom.id (right a)) = Hom.snd a

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MulticospanShape
a : J.L
⊢ ((Hom.id (left a)).comp (Hom.id (left a))).comp (Hom.id (left a)) =
    (Hom.id (left a)).comp ((Hom.id (left a)).comp (Hom.id (left a)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MulticospanShape
a : J.R
⊢ ((Hom.id (left (J.fst a))).comp (Hom.id (left (J.fst a)))).comp (Hom.fst a) =
    (Hom.id (left (J.fst a))).comp ((Hom.id (left (J.fst a))).comp (Hom.fst a))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MulticospanShape
a : J.R
⊢ ((Hom.id (left (J.snd a))).comp (Hom.id (left (J.snd a)))).comp (Hom.snd a) =
    (Hom.id (left (J.snd a))).comp ((Hom.id (left (J.snd a))).comp (Hom.snd a))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MulticospanShape
a : J.R
⊢ ((Hom.id (left (J.fst a))).comp (Hom.fst a)).comp (Hom.id (right a)) =
    (Hom.id (left (J.fst a))).comp ((Hom.fst a).comp (Hom.id (right a)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MulticospanShape
a : J.R
⊢ ((Hom.id (left (J.snd a))).comp (Hom.snd a)).comp (Hom.id (right a)) =
    (Hom.id (left (J.snd a))).comp ((Hom.snd a).comp (Hom.id (right a)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MulticospanShape
a : J.R
⊢ ((Hom.fst a).comp (Hom.id (right a))).comp (Hom.id (right a)) =
    (Hom.fst a).comp ((Hom.id (right a)).comp (Hom.id (right a)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MulticospanShape
a : J.R
⊢ ((Hom.snd a).comp (Hom.id (right a))).comp (Hom.id (right a)) =
    (Hom.snd a).comp ((Hom.id (right a)).comp (Hom.id (right a)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MulticospanShape
a : J.R
⊢ ((Hom.id (right a)).comp (Hom.id (right a))).comp (Hom.id (right a)) =
    (Hom.id (right a)).comp ((Hom.id (right a)).comp (Hom.id (right a)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MulticospanShape
X : WalkingMulticospan J
⊢ id X = 𝟙 X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MulticospanShape
X Y Z : WalkingMulticospan J
f : X ⟶ Y
g : Y ⟶ Z
⊢ comp f g = f ≫ g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
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 = Iso.hom (left (J.fst i)) ≫ G.map (Hom.fst i)
wr : ∀ (i : J.R), F.map (Hom.snd i) ≫ (right i).hom = Iso.hom (left (J.snd i)) ≫ G.map (Hom.snd i)
X : WalkingMulticospan J
⊢ F.map (Hom.id X) ≫
      Iso.hom
        ((fun (j : WalkingMulticospan J) ↦
            (match (motive := (j : WalkingMulticospan J) → F.obj j ≅ G.obj j) j with
              | WalkingMulticospan.left i => left i
              | WalkingMulticospan.right i => right i :
              F.obj j ≅ G.obj j))
          X) =
    Iso.hom
        ((fun (j : WalkingMulticospan J) ↦
            (match (motive := (j : WalkingMulticospan J) → F.obj j ≅ G.obj j) j with
              | WalkingMulticospan.left i => left i
              | WalkingMulticospan.right i => right i :
              F.obj j ≅ G.obj j))
          X) ≫
      G.map (Hom.id X)

Tactic:
simp [wl, wr]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
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 = Iso.hom (left (J.fst i)) ≫ G.map (Hom.fst i)
wr : ∀ (i : J.R), F.map (Hom.snd i) ≫ (right i).hom = Iso.hom (left (J.snd i)) ≫ G.map (Hom.snd i)
b : J.R
⊢ F.map (Hom.fst b) ≫
      Iso.hom
        ((fun (j : WalkingMulticospan J) ↦
            (match (motive := (j : WalkingMulticospan J) → F.obj j ≅ G.obj j) j with
              | WalkingMulticospan.left i => left i
              | WalkingMulticospan.right i => right i :
              F.obj j ≅ G.obj j))
          (WalkingMulticospan.right b)) =
    Iso.hom
        ((fun (j : WalkingMulticospan J) ↦
            (match (motive := (j : WalkingMulticospan J) → F.obj j ≅ G.obj j) j with
              | WalkingMulticospan.left i => left i
              | WalkingMulticospan.right i => right i :
              F.obj j ≅ G.obj j))
          (WalkingMulticospan.left (J.fst b))) ≫
      G.map (Hom.fst b)

Tactic:
simp [wl, wr]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
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 = Iso.hom (left (J.fst i)) ≫ G.map (Hom.fst i)
wr : ∀ (i : J.R), F.map (Hom.snd i) ≫ (right i).hom = Iso.hom (left (J.snd i)) ≫ G.map (Hom.snd i)
b : J.R
⊢ F.map (Hom.snd b) ≫
      Iso.hom
        ((fun (j : WalkingMulticospan J) ↦
            (match (motive := (j : WalkingMulticospan J) → F.obj j ≅ G.obj j) j with
              | WalkingMulticospan.left i => left i
              | WalkingMulticospan.right i => right i :
              F.obj j ≅ G.obj j))
          (WalkingMulticospan.right b)) =
    Iso.hom
        ((fun (j : WalkingMulticospan J) ↦
            (match (motive := (j : WalkingMulticospan J) → F.obj j ≅ G.obj j) j with
              | WalkingMulticospan.left i => left i
              | WalkingMulticospan.right i => right i :
              F.obj j ≅ G.obj j))
          (WalkingMulticospan.left (J.snd b))) ≫
      G.map (Hom.snd b)

Tactic:
simp [wl, wr]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
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)
a : J.L
⊢ F.obj (WalkingMulticospan.left a) = G.obj (WalkingMulticospan.left a)

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
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)
a : J.R
⊢ F.obj (WalkingMulticospan.right a) = G.obj (WalkingMulticospan.right a)

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
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)
a : J.L
⊢ Eq.{v_1 + 1} (α := F.obj (WalkingMulticospan.left a) ⟶ G.obj (WalkingMulticospan.left a))
    (NatTrans.app (Iso.hom (functorExt (fun (x : J.L) ↦ eqToIso ⋯) (fun (x : J.R) ↦ eqToIso ⋯) wl wr))
      (WalkingMulticospan.left a))
    (eqToHom ⋯)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
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)
a : J.R
⊢ Eq.{v_1 + 1} (α := F.obj (WalkingMulticospan.right a) ⟶ G.obj (WalkingMulticospan.right a))
    (NatTrans.app (Iso.hom (functorExt (fun (x : J.L) ↦ eqToIso ⋯) (fun (x : J.R) ↦ eqToIso ⋯) wl wr))
      (WalkingMulticospan.right a))
    (eqToHom ⋯)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
inst : Small.{t, w} J.L
inst_1 : Small.{t, w'} J.R
a : J.L
⊢ ∃ (a_1 : Sum.{w, w'} J.L J.R), Sum.elim left right a_1 = left a

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
inst : Small.{t, w} J.L
inst_1 : Small.{t, w'} J.R
a : J.R
⊢ ∃ (a_1 : Sum.{w, w'} J.L J.R), Sum.elim left right a_1 = right a

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
a : J.L
⊢ (Hom.id (left a)).comp (Hom.id (left a)) = Hom.id (left a)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
a : J.L
⊢ (Hom.id (left a)).comp (Hom.fst a) = Hom.fst a

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
a : J.L
⊢ (Hom.id (left a)).comp (Hom.snd a) = Hom.snd a

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
a : J.R
⊢ (Hom.id (right a)).comp (Hom.id (right a)) = Hom.id (right a)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
a : J.L
⊢ (Hom.fst a).comp (Hom.id (right (J.fst a))) = Hom.fst a

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
a : J.L
⊢ (Hom.snd a).comp (Hom.id (right (J.snd a))) = Hom.snd a

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
a : J.L
⊢ ((Hom.id (left a)).comp (Hom.id (left a))).comp (Hom.id (left a)) =
    (Hom.id (left a)).comp ((Hom.id (left a)).comp (Hom.id (left a)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
a : J.L
⊢ ((Hom.id (left a)).comp (Hom.id (left a))).comp (Hom.fst a) =
    (Hom.id (left a)).comp ((Hom.id (left a)).comp (Hom.fst a))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
a : J.L
⊢ ((Hom.id (left a)).comp (Hom.id (left a))).comp (Hom.snd a) =
    (Hom.id (left a)).comp ((Hom.id (left a)).comp (Hom.snd a))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
a : J.L
⊢ ((Hom.id (left a)).comp (Hom.fst a)).comp (Hom.id (right (J.fst a))) =
    (Hom.id (left a)).comp ((Hom.fst a).comp (Hom.id (right (J.fst a))))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
a : J.L
⊢ ((Hom.id (left a)).comp (Hom.snd a)).comp (Hom.id (right (J.snd a))) =
    (Hom.id (left a)).comp ((Hom.snd a).comp (Hom.id (right (J.snd a))))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
a : J.L
⊢ ((Hom.fst a).comp (Hom.id (right (J.fst a)))).comp (Hom.id (right (J.fst a))) =
    (Hom.fst a).comp ((Hom.id (right (J.fst a))).comp (Hom.id (right (J.fst a))))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
a : J.L
⊢ ((Hom.snd a).comp (Hom.id (right (J.snd a)))).comp (Hom.id (right (J.snd a))) =
    (Hom.snd a).comp ((Hom.id (right (J.snd a))).comp (Hom.id (right (J.snd a))))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
a : J.R
⊢ ((Hom.id (right a)).comp (Hom.id (right a))).comp (Hom.id (right a)) =
    (Hom.id (right a)).comp ((Hom.id (right a)).comp (Hom.id (right a)))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
X : WalkingMultispan J
⊢ id X = 𝟙 X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
X Y Z : WalkingMultispan J
f : X ⟶ Y
g : Y ⟶ Z
⊢ comp f g = f ≫ g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
C : Type u_1
inst : Category.{v_1, u_1} C
F G : WalkingMultispan J ⥤ C
left : (i : J.L) → F.obj (WalkingMultispan.left i) ≅ G.obj (WalkingMultispan.left i)
right : (i : J.R) → F.obj (WalkingMultispan.right i) ≅ G.obj (WalkingMultispan.right i)
wl : ∀ (i : J.L), F.map (Hom.fst i) ≫ Iso.hom (right (J.fst i)) = (left i).hom ≫ G.map (Hom.fst i)
wr : ∀ (i : J.L), F.map (Hom.snd i) ≫ Iso.hom (right (J.snd i)) = (left i).hom ≫ G.map (Hom.snd i)
X : WalkingMultispan J
⊢ F.map (Hom.id X) ≫
      Iso.hom
        ((fun (j : WalkingMultispan J) ↦
            (match (motive := (j : WalkingMultispan J) → F.obj j ≅ G.obj j) j with
              | WalkingMultispan.left i => left i
              | WalkingMultispan.right i => right i :
              F.obj j ≅ G.obj j))
          X) =
    Iso.hom
        ((fun (j : WalkingMultispan J) ↦
            (match (motive := (j : WalkingMultispan J) → F.obj j ≅ G.obj j) j with
              | WalkingMultispan.left i => left i
              | WalkingMultispan.right i => right i :
              F.obj j ≅ G.obj j))
          X) ≫
      G.map (Hom.id X)

Tactic:
simp [wl, wr]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
C : Type u_1
inst : Category.{v_1, u_1} C
F G : WalkingMultispan J ⥤ C
left : (i : J.L) → F.obj (WalkingMultispan.left i) ≅ G.obj (WalkingMultispan.left i)
right : (i : J.R) → F.obj (WalkingMultispan.right i) ≅ G.obj (WalkingMultispan.right i)
wl : ∀ (i : J.L), F.map (Hom.fst i) ≫ Iso.hom (right (J.fst i)) = (left i).hom ≫ G.map (Hom.fst i)
wr : ∀ (i : J.L), F.map (Hom.snd i) ≫ Iso.hom (right (J.snd i)) = (left i).hom ≫ G.map (Hom.snd i)
a : J.L
⊢ F.map (Hom.fst a) ≫
      Iso.hom
        ((fun (j : WalkingMultispan J) ↦
            (match (motive := (j : WalkingMultispan J) → F.obj j ≅ G.obj j) j with
              | WalkingMultispan.left i => left i
              | WalkingMultispan.right i => right i :
              F.obj j ≅ G.obj j))
          (WalkingMultispan.right (J.fst a))) =
    Iso.hom
        ((fun (j : WalkingMultispan J) ↦
            (match (motive := (j : WalkingMultispan J) → F.obj j ≅ G.obj j) j with
              | WalkingMultispan.left i => left i
              | WalkingMultispan.right i => right i :
              F.obj j ≅ G.obj j))
          (WalkingMultispan.left a)) ≫
      G.map (Hom.fst a)

Tactic:
simp [wl, wr]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
C : Type u_1
inst : Category.{v_1, u_1} C
F G : WalkingMultispan J ⥤ C
left : (i : J.L) → F.obj (WalkingMultispan.left i) ≅ G.obj (WalkingMultispan.left i)
right : (i : J.R) → F.obj (WalkingMultispan.right i) ≅ G.obj (WalkingMultispan.right i)
wl : ∀ (i : J.L), F.map (Hom.fst i) ≫ Iso.hom (right (J.fst i)) = (left i).hom ≫ G.map (Hom.fst i)
wr : ∀ (i : J.L), F.map (Hom.snd i) ≫ Iso.hom (right (J.snd i)) = (left i).hom ≫ G.map (Hom.snd i)
a : J.L
⊢ F.map (Hom.snd a) ≫
      Iso.hom
        ((fun (j : WalkingMultispan J) ↦
            (match (motive := (j : WalkingMultispan J) → F.obj j ≅ G.obj j) j with
              | WalkingMultispan.left i => left i
              | WalkingMultispan.right i => right i :
              F.obj j ≅ G.obj j))
          (WalkingMultispan.right (J.snd a))) =
    Iso.hom
        ((fun (j : WalkingMultispan J) ↦
            (match (motive := (j : WalkingMultispan J) → F.obj j ≅ G.obj j) j with
              | WalkingMultispan.left i => left i
              | WalkingMultispan.right i => right i :
              F.obj j ≅ G.obj j))
          (WalkingMultispan.left a)) ≫
      G.map (Hom.snd a)

Tactic:
simp [wl, wr]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
a : WalkingMultispan J
⊢ Hom.id a = 𝟙 a

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
a b : J.L
pos : ∀ (h : a = b), Subsingleton (left a ⟶ left b)
neg : ∀ (h : ¬a = b), Subsingleton (left a ⟶ left b)
⊢ Subsingleton (left a ⟶ left b)

Tactic:
by_cases h : a = b
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
a b : J.L
h : a = b
pos : Subsingleton (left a ⟶ left a)
⊢ Subsingleton (left a ⟶ left b)

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
a : J.L
⊢ Subsingleton (left a ⟶ left a)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
a : J.L
h : ¬a = a
⊢ False

Tactic:
simp at h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
a b : J.L
h : ¬a = b
⊢ IsEmpty (left a ⟶ left b)

Tactic:
have : IsEmpty (left a ⟶ left b) := ⟨by rintro ⟨⟩; simp at h⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
a b : J.L
h : ¬a = b
this : IsEmpty (left a ⟶ left b)
⊢ Subsingleton (left a ⟶ left b)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
a b : J.R
pos : ∀ (h : a = b), Subsingleton (right a ⟶ right b)
neg : ∀ (h : ¬a = b), Subsingleton (right a ⟶ right b)
⊢ Subsingleton (right a ⟶ right b)

Tactic:
by_cases h : a = b
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
a b : J.R
h : a = b
pos : Subsingleton (right a ⟶ right a)
⊢ Subsingleton (right a ⟶ right b)

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
a : J.R
⊢ Subsingleton (right a ⟶ right a)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
a : J.R
h : ¬a = a
⊢ False

Tactic:
simp at h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
Goal:
J : MultispanShape
a b : J.R
h : ¬a = b
⊢ IsEmpty (right a ⟶ right b)

Tactic:
have : IsEmpty (right a ⟶ right b) := ⟨by rintro ⟨⟩; simp at h⟩