awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
Goal:
X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
e : Functor.{w, u, w, u + 1} (WalkingMultispan (MultispanShape.prod ι)) (Type u) :=
  (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan
x_1 :
  Functor.CoconeTypes.pt.{u, u, w, w} (J := WalkingMultispan (MultispanShape.prod ι)) (F :=
    (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan)
    (((c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan.coconeTypesEquiv.symm :
        (a : Cocone (c.multispanIndex.map Set.functorToTypes).multispan) →
          (c.multispanIndex.map Set.functorToTypes).multispan.CoconeTypes)
      (c.multicofork (x := A) (u := U) (v := V).map Set.functorToTypes))
x : X
hx : x ∈ c.multicofork (x := A) (u := U) (v := V).pt
i : ι
hi : x ∈ U i
⊢ ∃ (i : (MultispanShape.prod ι).R) (a : (c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).right i),
    Functor.CoconeTypes.ι
        (((c.multispanIndex (x := A) (u := U) (v := V).map Set.functorToTypes).multispan.coconeTypesEquiv.symm :
            (a : Cocone (c.multispanIndex.map Set.functorToTypes).multispan) →
              (c.multispanIndex.map Set.functorToTypes).multispan.CoconeTypes)
          (c.multicofork (x := A) (u := U) (v := V).map Set.functorToTypes))
        (WalkingMultispan.right i) a =
      Subtype.mk (p := fun (x : X) ↦ x ∈ c.multicofork (x := A) (u := U) (v := V).pt) x hx

Tactic:
exact ⟨i, ⟨x, hi⟩, rfl⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
Goal:
X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
inst : LinearOrder ι
c : MulticoequalizerDiagram A U V
i j : ι
dsimp : V i j = V j i
⊢ c.multispanIndex (x := A) (u := U) (v := V).left (i, j) = c.multispanIndex (x := A) (u := U) (v := V).left (j, i)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
Goal:
X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
inst : LinearOrder ι
c : MulticoequalizerDiagram A U V
i j : ι
rw : U i ⊓ U j = V j i
rw₁ : U i ⊓ U j = U j ⊓ U i
rw₂ rw₃ : U j ⊓ U i = U j ⊓ U i
⊢ V i j = V j i

Tactic:
rw [c.eq_inf, c.eq_inf, inf_comm]

Premises used: CompleteLattice.MulticoequalizerDiagram.eq_inf, inf_comm
-- Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
Goal:
X : Type u
S₁ S₂ S₃ S₄ : Set X
h : Lattice.BicartSq S₁ S₂ S₃ S₄
h₁ :
  Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R)
      {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} false ↔
    Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ false
h₂ :
  Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R)
      {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} true ↔
    Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ true
⊢ Eq (α := Set (MultispanShape.ofLinearOrder Bool).R)
    {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} Set.univ

Tactic:
ext (_ | _)
-- Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
Goal:
X : Type u
S₁ S₂ S₃ S₄ : Set X
h : Lattice.BicartSq S₁ S₂ S₃ S₄
h₁ :
  Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R)
      {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} false →
    Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ false
h₂ :
  Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ false →
    Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R)
      {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} false
h₃ h₄ h₅ :
  Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R)
      {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} false →
    Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ false
h₆ h₇ :
  Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ false →
    Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R)
      {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} false
h₈ :
  Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ false →
    ¬false = (MultispanShape.ofLinearOrder Bool).fst default →
      Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) {(MultispanShape.ofLinearOrder Bool).snd default}
        false
h₉ h₁₀ h₁₁ :
  Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R)
      {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} false →
    Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ false
h₁₂ :
  Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ false →
    ¬false = (MultispanShape.ofLinearOrder Bool).fst default →
      Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) {(MultispanShape.ofLinearOrder Bool).snd default}
        false
h₁₃ h₁₄ h₁₅ h₁₆ h₁₇ :
  Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R)
      {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} false →
    Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ false
⊢ Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R)
      {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} false ↔
    Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ false

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
Goal:
X : Type u
S₁ S₂ S₃ S₄ : Set X
h : Lattice.BicartSq S₁ S₂ S₃ S₄
h₁ :
  Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R)
      {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} true →
    Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ true
h₂ :
  Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ true →
    Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R)
      {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} true
h₃ h₄ h₅ :
  Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R)
      {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} true →
    Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ true
h₆ h₇ :
  Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ true →
    Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R)
      {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} true
h₈ :
  Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ true →
    ¬true = (MultispanShape.ofLinearOrder Bool).fst default →
      Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) {(MultispanShape.ofLinearOrder Bool).snd default}
        true
h₉ h₁₀ h₁₁ :
  Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R)
      {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} true →
    Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ true
h₁₂ h₁₃ h₁₄ :
  Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ true →
    ¬true = (MultispanShape.ofLinearOrder Bool).fst default →
      Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) {(MultispanShape.ofLinearOrder Bool).snd default}
        true
h₁₅ h₁₆ :
  Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R)
      {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} true →
    Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ true
h₁₇ :
  Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ true →
    ¬true = (MultispanShape.ofLinearOrder Bool).fst default →
      Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) {(MultispanShape.ofLinearOrder Bool).snd default}
        true
⊢ Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R)
      {(MultispanShape.ofLinearOrder Bool).fst default, (MultispanShape.ofLinearOrder Bool).snd default} true ↔
    Membership.mem (γ := Set (MultispanShape.ofLinearOrder Bool).R) Set.univ true

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer
Goal:
X : Type u
S₁ S₂ S₃ S₄ : Set X
h : Lattice.BicartSq S₁ S₂ S₃ S₄
tauto :
  Eq (α := (MultispanShape.ofLinearOrder Bool).R) ((MultispanShape.ofLinearOrder Bool).fst default)
      ((MultispanShape.ofLinearOrder Bool).snd default) →
    False
⊢ Ne (α := (MultispanShape.ofLinearOrder Bool).R) ((MultispanShape.ofLinearOrder Bool).fst default)
    ((MultispanShape.ofLinearOrder Bool).snd default)

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Limits.Types.Multiequalizer
Goal:
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : I.sections
j : WalkingMulticospan J
⊢ Eq (α := (fun (X : Type u) ↦ X) (I.multicospan.obj j))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (I.multicospan.map (WalkingMulticospan.Hom.id j)) :
          (a : (fun (X : Type u) ↦ X) (I.multicospan.obj j)) → (fun (X : Type u) ↦ X) (I.multicospan.obj j))
        ((fun (i : WalkingMulticospan J) ↦
            (match (motive := (i : WalkingMulticospan J) → I.multicospan.obj i) i with
              | WalkingMulticospan.left i => s.val i
              | WalkingMulticospan.right j =>
                (ConcreteCategory.hom (FC := TypeCat.Fun) (I.fst j) :
                    (a : (fun (X : Type u) ↦ X) (I.left (J.fst j))) → (fun (X : Type u) ↦ X) (I.right j))
                  (s.val (J.fst j)) :
              I.multicospan.obj i))
          j) :
      (fun (X : Type u) ↦ X) (I.multicospan.obj j))
    ((fun (i : WalkingMulticospan J) ↦
          (match (motive := (i : WalkingMulticospan J) → I.multicospan.obj i) i with
            | WalkingMulticospan.left i => s.val i
            | WalkingMulticospan.right j =>
              (ConcreteCategory.hom (FC := TypeCat.Fun) (I.fst j) :
                  (a : (fun (X : Type u) ↦ X) (I.left (J.fst j))) → (fun (X : Type u) ↦ X) (I.right j))
                (s.val (J.fst j)) :
            I.multicospan.obj i))
        j :
      I.multicospan.obj j)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Multiequalizer
Goal:
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : I.sections
b : J.R
⊢ Eq (α := (fun (X : Type u) ↦ X) (I.multicospan.obj (WalkingMulticospan.right b)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (I.multicospan.map (WalkingMulticospan.Hom.fst b)) :
          (a : (fun (X : Type u) ↦ X) (I.multicospan.obj (WalkingMulticospan.left (J.fst b)))) →
            (fun (X : Type u) ↦ X) (I.multicospan.obj (WalkingMulticospan.right b)))
        ((fun (i : WalkingMulticospan J) ↦
            (match (motive := (i : WalkingMulticospan J) → I.multicospan.obj i) i with
              | WalkingMulticospan.left i => s.val i
              | WalkingMulticospan.right j =>
                (ConcreteCategory.hom (FC := TypeCat.Fun) (I.fst j) :
                    (a : (fun (X : Type u) ↦ X) (I.left (J.fst j))) → (fun (X : Type u) ↦ X) (I.right j))
                  (s.val (J.fst j)) :
              I.multicospan.obj i))
          (WalkingMulticospan.left (J.fst b))) :
      (fun (X : Type u) ↦ X) (I.multicospan.obj (WalkingMulticospan.right b)))
    ((fun (i : WalkingMulticospan J) ↦
          (match (motive := (i : WalkingMulticospan J) → I.multicospan.obj i) i with
            | WalkingMulticospan.left i => s.val i
            | WalkingMulticospan.right j =>
              (ConcreteCategory.hom (FC := TypeCat.Fun) (I.fst j) :
                  (a : (fun (X : Type u) ↦ X) (I.left (J.fst j))) → (fun (X : Type u) ↦ X) (I.right j))
                (s.val (J.fst j)) :
            I.multicospan.obj i))
        (WalkingMulticospan.right b) :
      I.multicospan.obj (WalkingMulticospan.right b))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Multiequalizer
Goal:
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : I.sections
r : J.R
⊢ Eq (α := (fun (X : Type u) ↦ X) (I.multicospan.obj (WalkingMulticospan.right r)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (I.multicospan.map (WalkingMulticospan.Hom.snd r)) :
          (a : (fun (X : Type u) ↦ X) (I.multicospan.obj (WalkingMulticospan.left (J.snd r)))) →
            (fun (X : Type u) ↦ X) (I.multicospan.obj (WalkingMulticospan.right r)))
        ((fun (i : WalkingMulticospan J) ↦
            (match (motive := (i : WalkingMulticospan J) → I.multicospan.obj i) i with
              | WalkingMulticospan.left i => s.val i
              | WalkingMulticospan.right j =>
                (ConcreteCategory.hom (FC := TypeCat.Fun) (I.fst j) :
                    (a : (fun (X : Type u) ↦ X) (I.left (J.fst j))) → (fun (X : Type u) ↦ X) (I.right j))
                  (s.val (J.fst j)) :
              I.multicospan.obj i))
          (WalkingMulticospan.left (J.snd r))) :
      (fun (X : Type u) ↦ X) (I.multicospan.obj (WalkingMulticospan.right r)))
    ((fun (i : WalkingMulticospan J) ↦
          (match (motive := (i : WalkingMulticospan J) → I.multicospan.obj i) i with
            | WalkingMulticospan.left i => s.val i
            | WalkingMulticospan.right j =>
              (ConcreteCategory.hom (FC := TypeCat.Fun) (I.fst j) :
                  (a : (fun (X : Type u) ↦ X) (I.left (J.fst j))) → (fun (X : Type u) ↦ X) (I.right j))
                (s.val (J.fst j)) :
            I.multicospan.obj i))
        (WalkingMulticospan.right r) :
      I.multicospan.obj (WalkingMulticospan.right r))

Tactic:
(s.property r).symm

Premises used: CategoryTheory.Limits.MulticospanIndex.sections.property, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Types.Multiequalizer
Goal:
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : I.sections
r : J.R
⊢ Eq (α := (fun (X : Type u) ↦ X) (I.multicospan.obj (WalkingMulticospan.right r)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (I.multicospan.map (WalkingMulticospan.Hom.snd r)) :
          (a : (fun (X : Type u) ↦ X) (I.multicospan.obj (WalkingMulticospan.left (J.snd r)))) →
            (fun (X : Type u) ↦ X) (I.multicospan.obj (WalkingMulticospan.right r)))
        ((fun (i : WalkingMulticospan J) ↦
            (match (motive := (i : WalkingMulticospan J) → I.multicospan.obj i) i with
              | WalkingMulticospan.left i => s.val i
              | WalkingMulticospan.right j =>
                (ConcreteCategory.hom (FC := TypeCat.Fun) (I.fst j) :
                    (a : (fun (X : Type u) ↦ X) (I.left (J.fst j))) → (fun (X : Type u) ↦ X) (I.right j))
                  (s.val (J.fst j)) :
              I.multicospan.obj i))
          (WalkingMulticospan.left (J.snd r))) :
      (fun (X : Type u) ↦ X) (I.multicospan.obj (WalkingMulticospan.right r)))
    ((fun (i : WalkingMulticospan J) ↦
          (match (motive := (i : WalkingMulticospan J) → I.multicospan.obj i) i with
            | WalkingMulticospan.left i => s.val i
            | WalkingMulticospan.right j =>
              (ConcreteCategory.hom (FC := TypeCat.Fun) (I.fst j) :
                  (a : (fun (X : Type u) ↦ X) (I.left (J.fst j))) → (fun (X : Type u) ↦ X) (I.right j))
                (s.val (J.fst j)) :
            I.multicospan.obj i))
        (WalkingMulticospan.right r) :
      I.multicospan.obj (WalkingMulticospan.right r))

Tactic:
exact (s.property r).symm

Premises used: CategoryTheory.Limits.MulticospanIndex.sections.property, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Types.Multiequalizer
Goal:
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : (↑I.multicospan.sections : Type (max (max u u_2) u_1))
a : J.L
⊢ (↑((fun (s : I.sections) ↦
              Subtype.mk (p := fun (x : (j : WalkingMulticospan J) → I.multicospan.obj j) ↦ x ∈ I.multicospan.sections)
                (fun (i : WalkingMulticospan J) ↦
                  match (motive := (i : WalkingMulticospan J) → I.multicospan.obj i) i with
                  | WalkingMulticospan.left i => s.val i
                  | WalkingMulticospan.right j =>
                    (ConcreteCategory.hom (FC := TypeCat.Fun) (I.fst j) :
                        (a : (fun (X : Type u) ↦ X) (I.left (J.fst j))) → (fun (X : Type u) ↦ X) (I.right j))
                      (s.val (J.fst j)))
                ⋯)
            ((fun (s : (↑I.multicospan.sections : Type (max (max u u_2) u_1))) ↦
                ({
                    val := fun (i : J.L) ↦
                      (↑s : (j : WalkingMulticospan J) → I.multicospan.obj j) (WalkingMulticospan.left i),
                    property := ⋯ } :
                  I.sections))
              s)) :
        (j : WalkingMulticospan J) → I.multicospan.obj j)
      (WalkingMulticospan.left a) =
    (↑s : (j : WalkingMulticospan J) → I.multicospan.obj j) (WalkingMulticospan.left a)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Multiequalizer
Goal:
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : (↑I.multicospan.sections : Type (max (max u u_2) u_1))
r : J.R
⊢ (↑((fun (s : I.sections) ↦
              Subtype.mk (p := fun (x : (j : WalkingMulticospan J) → I.multicospan.obj j) ↦ x ∈ I.multicospan.sections)
                (fun (i : WalkingMulticospan J) ↦
                  match (motive := (i : WalkingMulticospan J) → I.multicospan.obj i) i with
                  | WalkingMulticospan.left i => s.val i
                  | WalkingMulticospan.right j =>
                    (ConcreteCategory.hom (FC := TypeCat.Fun) (I.fst j) :
                        (a : (fun (X : Type u) ↦ X) (I.left (J.fst j))) → (fun (X : Type u) ↦ X) (I.right j))
                      (s.val (J.fst j)))
                ⋯)
            ((fun (s : (↑I.multicospan.sections : Type (max (max u u_2) u_1))) ↦
                ({
                    val := fun (i : J.L) ↦
                      (↑s : (j : WalkingMulticospan J) → I.multicospan.obj j) (WalkingMulticospan.left i),
                    property := ⋯ } :
                  I.sections))
              s)) :
        (j : WalkingMulticospan J) → I.multicospan.obj j)
      (WalkingMulticospan.right r) =
    (↑s : (j : WalkingMulticospan J) → I.multicospan.obj j) (WalkingMulticospan.right r)

Tactic:
s.property (.fst r)

Premises used: Subtype.property, CategoryTheory.Limits.WalkingMulticospan.Hom.fst
-- Module: Mathlib.CategoryTheory.Limits.Types.Multiequalizer
Goal:
J : MulticospanShape
I : MulticospanIndex J (Type u)
s : (↑I.multicospan.sections : Type (max (max u u_2) u_1))
r : J.R
⊢ (↑((fun (s : I.sections) ↦
              Subtype.mk (p := fun (x : (j : WalkingMulticospan J) → I.multicospan.obj j) ↦ x ∈ I.multicospan.sections)
                (fun (i : WalkingMulticospan J) ↦
                  match (motive := (i : WalkingMulticospan J) → I.multicospan.obj i) i with
                  | WalkingMulticospan.left i => s.val i
                  | WalkingMulticospan.right j =>
                    (ConcreteCategory.hom (FC := TypeCat.Fun) (I.fst j) :
                        (a : (fun (X : Type u) ↦ X) (I.left (J.fst j))) → (fun (X : Type u) ↦ X) (I.right j))
                      (s.val (J.fst j)))
                ⋯)
            ((fun (s : (↑I.multicospan.sections : Type (max (max u u_2) u_1))) ↦
                ({
                    val := fun (i : J.L) ↦
                      (↑s : (j : WalkingMulticospan J) → I.multicospan.obj j) (WalkingMulticospan.left i),
                    property := ⋯ } :
                  I.sections))
              s)) :
        (j : WalkingMulticospan J) → I.multicospan.obj j)
      (WalkingMulticospan.right r) =
    (↑s : (j : WalkingMulticospan J) → I.multicospan.obj j) (WalkingMulticospan.right r)

Tactic:
exact s.property (.fst r)

Premises used: Subtype.property, CategoryTheory.Limits.WalkingMulticospan.Hom.fst
-- Module: Mathlib.CategoryTheory.Limits.Types.Multiequalizer
Goal:
J : MulticospanShape
I : MulticospanIndex J (Type u)
c : Multifork I
⊢ (⇑I.sectionsEquiv.symm : (a : (↑I.multicospan.sections : Type (max (max u u_2) u_1))) → I.sections) ∘
      Types.sectionOfCone c =
    c.toSections

Tactic:
rfl

Premises used: CategoryTheory.Limits.Multifork.toSections, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Multiequalizer
Goal:
J : MulticospanShape
I : MulticospanIndex J (Type u)
c : Multifork I
rw : Function.Bijective (Types.sectionOfCone c) ↔ Function.Bijective c.toSections
rw₁ :
  Function.Bijective (Types.sectionOfCone c) ↔
    Function.Bijective (β := I.sections)
      ((⇑I.sectionsEquiv.symm : (a : (↑I.multicospan.sections : Type (max (max u u_1) u_2))) → I.sections) ∘
        Types.sectionOfCone c)
rw₂ rw₃ : Function.Bijective (Types.sectionOfCone c) ↔ Function.Bijective (Types.sectionOfCone c)
⊢ Nonempty (IsLimit c) ↔ Function.Bijective c.toSections

Tactic:
rw [Types.isLimit_iff_bijective_sectionOfCone, ← toSections_fac, EquivLike.comp_bijective]

Premises used: EquivLike.comp_bijective, CategoryTheory.Limits.Types.isLimit_iff_bijective_sectionOfCone, CategoryTheory.Limits.Multifork.toSections_fac
-- Module: Mathlib.CategoryTheory.Limits.Types.Multiequalizer
Goal:
J : MulticospanShape
I : MulticospanIndex J (Type u)
c : Multifork I
hc : IsLimit c
x : c.pt
i : J.L
⊢ Eq.{u + 1} (α := I.left i) (MulticospanIndex.sections.val (((sectionsEquiv hc).symm : (a : c.pt) → I.sections) x) i)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι i) :
        (a : (fun (X : Type u) ↦ X) c.pt) → (fun (X : Type u) ↦ X) (I.left i))
      x)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Multiequalizer
Goal:
J : MulticospanShape
I : MulticospanIndex J (Type u)
c : Multifork I
hc : IsLimit c
s : I.sections
i : J.L
obtain :
  ∀ (x : c.pt),
    Eq (α := (fun (X : Type u) ↦ X) (I.left i))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι i) :
            (a : (fun (X : Type u) ↦ X) c.pt) → (fun (X : Type u) ↦ X) (I.left i))
          ((sectionsEquiv hc : (a : I.sections) → c.pt) (((sectionsEquiv hc).symm : (a : c.pt) → I.sections) x) :
            c.pt) :
        (fun (X : Type u) ↦ X) (I.left i))
      (MulticospanIndex.sections.val (((sectionsEquiv hc).symm : (a : c.pt) → I.sections) x) i : I.left i)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι i) :
        (a : (fun (X : Type u) ↦ X) c.pt) → (fun (X : Type u) ↦ X) (I.left i))
      ((sectionsEquiv hc : (a : I.sections) → c.pt) s : c.pt) =
    s.val i

Tactic:
obtain ⟨x, rfl⟩ := (sectionsEquiv hc).symm.surjective s

Premises used: CategoryTheory.Limits.Multifork.IsLimit.sectionsEquiv, Equiv.surjective, Equiv.symm, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Multiequalizer
Goal:
J : MulticospanShape
I : MulticospanIndex J (Type u)
c : Multifork I
hc : IsLimit c
i : J.L
x : c.pt
⊢ Eq (α := (fun (X : Type u) ↦ X) (I.left i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι i) :
          (a : (fun (X : Type u) ↦ X) c.pt) → (fun (X : Type u) ↦ X) (I.left i))
        ((sectionsEquiv hc : (a : I.sections) → c.pt) (((sectionsEquiv hc).symm : (a : c.pt) → I.sections) x) : c.pt) :
      (fun (X : Type u) ↦ X) (I.left i))
    (MulticospanIndex.sections.val (((sectionsEquiv hc).symm : (a : c.pt) → I.sections) x) i : I.left i)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
⊢ HasProducts (Type v)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Limits.Types.Products
Goal:
inst : UnivLE.{v, u}
⊢ HasProducts (Type u)

Tactic:
inferInstance

Premises used: inferInstance