awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
val : J
⊢ Membership.mem (γ := Finset (some val ⟶ some val))
    (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ Finset (x ⟶ some val)) (some val)
        (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ Finset (none ⟶ x)) (some val) {Hom.id none}
          fun (j' : J) ↦ {Hom.init j'})
        fun (j : J) ↦
        if h : some j = some val then Eq.mpr (β := Finset (some val ⟶ some val)) ⋯ {Hom.id (some val)} else ∅ :
      Finset (some val ⟶ some val))
    (Hom.id (some val))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
j : J
⊢ Membership.mem (γ := Finset (none ⟶ some j))
    (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ Finset (x ⟶ some j)) none
        (Option.casesOn (motive := fun (x : WidePushoutShape J) ↦ Finset (none ⟶ x)) (some j) {Hom.id none}
          fun (j' : J) ↦ {Hom.init j'})
        fun (j_1 : J) ↦
        if h : some j_1 = some j then Eq.mpr (β := Finset (some j ⟶ some j)) ⋯ {Hom.id (some j)} else ∅ :
      Finset (none ⟶ some j))
    (Hom.init j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type v
J : Type
inst_1 : Finite J
inst_2 : HasFiniteWidePullbacks.{v, u} C
⊢ ∀ [Finite J], HasLimitsOfShape.{0, 0, v, u} (WidePullbackShape J) C

Tactic:
haveI := @HasFiniteWidePullbacks.out C _ _ J
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type v
J : Type
inst_1 : Finite J
inst_2 : HasFiniteWidePullbacks.{v, u} C
this : ∀ [Finite J], HasLimitsOfShape.{0, 0, v, u} (WidePullbackShape J) C
⊢ HasLimitsOfShape.{0, 0, v, u} (WidePullbackShape J) C

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type v
J : Type
inst_1 : Finite J
inst_2 : HasFiniteWidePushouts.{v, u} C
⊢ ∀ [Finite J], HasColimitsOfShape.{0, 0, v, u} (WidePushoutShape J) C

Tactic:
haveI := @HasFiniteWidePushouts.out C _ _ J
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type v
J : Type
inst_1 : Finite J
inst_2 : HasFiniteWidePushouts.{v, u} C
this : ∀ [Finite J], HasColimitsOfShape.{0, 0, v, u} (WidePushoutShape J) C
⊢ HasColimitsOfShape.{0, 0, v, u} (WidePushoutShape J) C

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type v
inst_1 : HasFiniteLimits.{v, u} C
J : Type
h : Finite J
intro : ∀ (val : Fintype J), HasLimitsOfShape.{0, 0, v, u} (WidePullbackShape J) C
⊢ HasLimitsOfShape.{0, 0, v, u} (WidePullbackShape J) C

Tactic:
cases nonempty_fintype J

Premises used: nonempty_fintype
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type v
inst_1 : HasFiniteLimits.{v, u} C
J : Type
h : Finite J
val : Fintype J
⊢ HasLimitsOfShape.{0, 0, v, u} (WidePullbackShape J) C

Tactic:
HasFiniteLimits.out _

Premises used: CategoryTheory.Limits.HasFiniteLimits.out
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type v
inst_1 : HasFiniteLimits.{v, u} C
J : Type
h : Finite J
val : Fintype J
⊢ HasLimitsOfShape.{0, 0, v, u} (WidePullbackShape J) C

Tactic:
exact HasFiniteLimits.out _

Premises used: CategoryTheory.Limits.HasFiniteLimits.out
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type v
inst_1 : HasFiniteColimits.{v, u} C
J : Type
h : Finite J
intro : ∀ (val : Fintype J), HasColimitsOfShape.{0, 0, v, u} (WidePushoutShape J) C
⊢ HasColimitsOfShape.{0, 0, v, u} (WidePushoutShape J) C

Tactic:
cases nonempty_fintype J

Premises used: nonempty_fintype
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type v
inst_1 : HasFiniteColimits.{v, u} C
J : Type
h : Finite J
val : Fintype J
⊢ HasColimitsOfShape.{0, 0, v, u} (WidePushoutShape J) C

Tactic:
HasFiniteColimits.out _

Premises used: CategoryTheory.Limits.HasFiniteColimits.out
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
J_1 : Type v
inst_1 : HasFiniteColimits.{v, u} C
J : Type
h : Finite J
val : Fintype J
⊢ HasColimitsOfShape.{0, 0, v, u} (WidePushoutShape J) C

Tactic:
exact HasFiniteColimits.out _

Premises used: CategoryTheory.Limits.HasFiniteColimits.out
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
x : WalkingPair
left : Membership.mem (γ := Finset WalkingPair) {WalkingPair.left, WalkingPair.right} WalkingPair.left
right : Membership.mem (γ := Finset WalkingPair) {WalkingPair.left, WalkingPair.right} WalkingPair.right
⊢ Membership.mem (γ := Finset WalkingPair) {WalkingPair.left, WalkingPair.right} x

Tactic:
cases x
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
⊢ Membership.mem (γ := Finset WalkingPair) {WalkingPair.left, WalkingPair.right} WalkingPair.left

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
⊢ Membership.mem (γ := Finset WalkingPair) {WalkingPair.left, WalkingPair.right} WalkingPair.right

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
inst_1 : HasFiniteWidePullbacks.{v, u} C
⊢ HasPullbacks.{v, u} C

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
Goal:
C : Type u
inst : Category.{v, u} C
J : Type v
inst_1 : HasFiniteWidePushouts.{v, u} C
⊢ HasPushouts.{v, u} C

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MulticospanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
⊢ Membership.mem (γ := Finset (left a ⟶ left a)) (if e : a = a then {eqToHom ⋯} else ∅) (Hom.id (left a))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MulticospanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
b : J.R
pos :
  ∀ (h₁ : J.fst b = a) (h₂ : J.snd b = a),
    (HAdd.hAdd (α := Multiset (left a ⟶ right b)) {eqToHom ⋯ ≫ Hom.fst b} {eqToHom ⋯ ≫ Hom.snd b}).Nodup
neg :
  ∀ (h₁ : J.fst b = a) (h₂ : ¬J.snd b = a),
    (HAdd.hAdd (α := Multiset (left a ⟶ right b)) {eqToHom ⋯ ≫ Hom.fst b} 0).Nodup
pos₁ :
  ∀ (h₁ : ¬J.fst b = a) (h : J.snd b = a),
    (HAdd.hAdd (α := Multiset (left a ⟶ right b)) 0 {eqToHom ⋯ ≫ Hom.snd b}).Nodup
neg₁ : ∀ (h₁ : ¬J.fst b = a), ¬J.snd b = a → (HAdd.hAdd (α := Multiset (left a ⟶ right b)) 0 0).Nodup
⊢ (HAdd.hAdd (α := Multiset (left a ⟶ right b)) (if e : J.fst b = a then {eqToHom ⋯ ≫ Hom.fst b} else 0)
      (if e : J.snd b = a then {eqToHom ⋯ ≫ Hom.snd b} else 0)).Nodup

Tactic:
split_ifs with h₁ h₂
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MulticospanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst b = a
h₂ : J.snd b = a
pos : ¬Eq (α := left a ⟶ right b) (eqToHom ⋯ ≫ Hom.fst b) (eqToHom ⋯ ≫ Hom.snd b)
⊢ (HAdd.hAdd (α := Multiset (left a ⟶ right b)) {eqToHom ⋯ ≫ Hom.fst b} {eqToHom ⋯ ≫ Hom.snd b}).Nodup

Tactic:
simp only [Multiset.singleton_add, Multiset.nodup_cons, Multiset.mem_singleton,
            Multiset.nodup_singleton, and_true]

Premises used: Multiset.singleton_add, and_true, Multiset.nodup_cons, Multiset.mem_singleton, Multiset.nodup_singleton
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MulticospanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst b = a
h₂ : J.snd b = a
f : (left a ⟶ right b) → Prop :=
  fun (x : left a ⟶ right b) ↦
    match (motive := (b : J.R) → (a : J.L) → (left a ⟶ right b) → (h₁ : J.fst b = a) → (h₂ : J.snd b = a) → Prop) b, a,
      x, h₁, h₂ with
    | a, .(J.fst a), Hom.fst .(a), h₁, h₂ => True
    | a, .(J.snd a), Hom.snd .(a), h₁, h₂ => False
pos : f (eqToHom ⋯ ≫ Hom.fst b) ≠ f (eqToHom ⋯ ≫ Hom.snd b)
⊢ ¬Eq (α := left a ⟶ right b) (eqToHom ⋯ ≫ Hom.fst b) (eqToHom ⋯ ≫ Hom.snd b)

Tactic:
apply ne_of_apply_ne f

Premises used: ne_of_apply_ne
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MulticospanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst b = a
h₂ : J.snd b = a
f : (left a ⟶ right b) → Prop :=
  fun (x : left a ⟶ right b) ↦
    match (motive := (b : J.R) → (a : J.L) → (left a ⟶ right b) → (h₁ : J.fst b = a) → (h₂ : J.snd b = a) → Prop) b, a,
      x, h₁, h₂ with
    | a, .(J.fst a), Hom.fst .(a), h₁, h₂ => True
    | a, .(J.snd a), Hom.snd .(a), h₁, h₂ => False
subst :
  ∀ (h₂ : J.snd b = J.fst b),
    let f : (left (J.fst b) ⟶ right b) → Prop := fun (x : left (J.fst b) ⟶ right b) ↦
      match (motive := (b : J.R) → (a : J.L) → (left a ⟶ right b) → (h₁ : J.fst b = a) → (h₂ : J.snd b = a) → Prop) b,
        J.fst b, x, ⋯, h₂ with
      | a, .(J.fst a), Hom.fst .(a), h₁, h₂ => True
      | a, .(J.snd a), Hom.snd .(a), h₁, h₂ => False;
    f (eqToHom ⋯ ≫ Hom.fst b) = True
⊢ f (eqToHom ⋯ ≫ Hom.fst b) = True

Tactic:
subst h₁
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MulticospanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
b : J.R
h₂ : J.snd b = J.fst b
f : (left (J.fst b) ⟶ right b) → Prop :=
  fun (x : left (J.fst b) ⟶ right b) ↦
    match (motive := (b : J.R) → (a : J.L) → (left a ⟶ right b) → (h₁ : J.fst b = a) → (h₂ : J.snd b = a) → Prop) b,
      J.fst b, x, ⋯, h₂ with
    | a, .(J.fst a), Hom.fst .(a), h₁, h₂ => True
    | a, .(J.snd a), Hom.snd .(a), h₁, h₂ => False
simp : True = True
⊢ f (eqToHom ⋯ ≫ Hom.fst b) = True

Tactic:
simp only [eqToHom_refl, Category.id_comp, f]

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MulticospanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst b = a
h₂ : J.snd b = a
f : (left a ⟶ right b) → Prop :=
  fun (x : left a ⟶ right b) ↦
    match (motive := (b : J.R) → (a : J.L) → (left a ⟶ right b) → (h₁ : J.fst b = a) → (h₂ : J.snd b = a) → Prop) b, a,
      x, h₁, h₂ with
    | a, .(J.fst a), Hom.fst .(a), h₁, h₂ => True
    | a, .(J.snd a), Hom.snd .(a), h₁, h₂ => False
tactic : ∀ (h₂ : J.snd b = J.fst b), True
| f (eqToHom ⋯ ≫ Hom.fst b)

Tactic:
tactic => subst h₁; simp only [eqToHom_refl, Category.id_comp, f]

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MulticospanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst b = a
h₂ : J.snd b = a
f : (left a ⟶ right b) → Prop :=
  fun (x : left a ⟶ right b) ↦
    match (motive := (b : J.R) → (a : J.L) → (left a ⟶ right b) → (h₁ : J.fst b = a) → (h₂ : J.snd b = a) → Prop) b, a,
      x, h₁, h₂ with
    | a, .(J.fst a), Hom.fst .(a), h₁, h₂ => True
    | a, .(J.snd a), Hom.snd .(a), h₁, h₂ => False
pos : True ≠ f (eqToHom ⋯ ≫ Hom.snd b)
⊢ f (eqToHom ⋯ ≫ Hom.fst b) ≠ f (eqToHom ⋯ ≫ Hom.snd b)

Tactic:
conv_lhs => tactic => subst h₁; simp only [eqToHom_refl, Category.id_comp, f]

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MulticospanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst b = a
h₂ : J.snd b = a
f : (left a ⟶ right b) → Prop :=
  fun (x : left a ⟶ right b) ↦
    match (motive := (b : J.R) → (a : J.L) → (left a ⟶ right b) → (h₁ : J.fst b = a) → (h₂ : J.snd b = a) → Prop) b, a,
      x, h₁, h₂ with
    | a, .(J.fst a), Hom.fst .(a), h₁, h₂ => True
    | a, .(J.snd a), Hom.snd .(a), h₁, h₂ => False
subst :
  ∀ (h₁ : J.fst b = J.snd b),
    let f : (left (J.snd b) ⟶ right b) → Prop := fun (x : left (J.snd b) ⟶ right b) ↦
      match (motive := (b : J.R) → (a : J.L) → (left a ⟶ right b) → (h₁ : J.fst b = a) → (h₂ : J.snd b = a) → Prop) b,
        J.snd b, x, h₁, ⋯ with
      | a, .(J.fst a), Hom.fst .(a), h₁, h₂ => True
      | a, .(J.snd a), Hom.snd .(a), h₁, h₂ => False;
    f (eqToHom ⋯ ≫ Hom.snd b) = False
⊢ f (eqToHom ⋯ ≫ Hom.snd b) = False

Tactic:
subst h₂
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MulticospanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
b : J.R
h₁ : J.fst b = J.snd b
f : (left (J.snd b) ⟶ right b) → Prop :=
  fun (x : left (J.snd b) ⟶ right b) ↦
    match (motive := (b : J.R) → (a : J.L) → (left a ⟶ right b) → (h₁ : J.fst b = a) → (h₂ : J.snd b = a) → Prop) b,
      J.snd b, x, h₁, ⋯ with
    | a, .(J.fst a), Hom.fst .(a), h₁, h₂ => True
    | a, .(J.snd a), Hom.snd .(a), h₁, h₂ => False
simp : False = False
⊢ f (eqToHom ⋯ ≫ Hom.snd b) = False

Tactic:
simp only [eqToHom_refl, Category.id_comp, f]

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MulticospanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst b = a
h₂ : J.snd b = a
f : (left a ⟶ right b) → Prop :=
  fun (x : left a ⟶ right b) ↦
    match (motive := (b : J.R) → (a : J.L) → (left a ⟶ right b) → (h₁ : J.fst b = a) → (h₂ : J.snd b = a) → Prop) b, a,
      x, h₁, h₂ with
    | a, .(J.fst a), Hom.fst .(a), h₁, h₂ => True
    | a, .(J.snd a), Hom.snd .(a), h₁, h₂ => False
tactic : ∀ (h₁ : J.fst b = J.snd b), False
| f (eqToHom ⋯ ≫ Hom.snd b)

Tactic:
tactic => subst h₂; simp only [eqToHom_refl, Category.id_comp, f]

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MulticospanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst b = a
h₂ : J.snd b = a
f : (left a ⟶ right b) → Prop :=
  fun (x : left a ⟶ right b) ↦
    match (motive := (b : J.R) → (a : J.L) → (left a ⟶ right b) → (h₁ : J.fst b = a) → (h₂ : J.snd b = a) → Prop) b, a,
      x, h₁, h₂ with
    | a, .(J.fst a), Hom.fst .(a), h₁, h₂ => True
    | a, .(J.snd a), Hom.snd .(a), h₁, h₂ => False
pos : True ≠ False
⊢ True ≠ f (eqToHom ⋯ ≫ Hom.snd b)

Tactic:
conv_rhs => tactic => subst h₂; simp only [eqToHom_refl, Category.id_comp, f]

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MulticospanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst b = a
h₂ : J.snd b = a
f : (left a ⟶ right b) → Prop :=
  fun (x : left a ⟶ right b) ↦
    match (motive := (b : J.R) → (a : J.L) → (left a ⟶ right b) → (h₁ : J.fst b = a) → (h₂ : J.snd b = a) → Prop) b, a,
      x, h₁, h₂ with
    | a, .(J.fst a), Hom.fst .(a), h₁, h₂ => True
    | a, .(J.snd a), Hom.snd .(a), h₁, h₂ => False
⊢ True ≠ False

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MulticospanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst b = a
h₂ : ¬J.snd b = a
⊢ (HAdd.hAdd (α := Multiset (left a ⟶ right b)) {eqToHom ⋯ ≫ Hom.fst b} 0).Nodup

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MulticospanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
b : J.R
h₁ : ¬J.fst b = a
h : J.snd b = a
⊢ (HAdd.hAdd (α := Multiset (left a ⟶ right b)) 0 {eqToHom ⋯ ≫ Hom.snd b}).Nodup

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MulticospanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
b : J.R
h₁ : ¬J.fst b = a
h : ¬J.snd b = a
⊢ (HAdd.hAdd (α := Multiset (left a ⟶ right b)) 0 0).Nodup

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MulticospanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
b : J.R
⊢ Hom.fst b ∈
    {
      val :=
        HAdd.hAdd (α := Multiset (left (J.fst b) ⟶ right b))
          (if e : J.fst b = J.fst b then {eqToHom ⋯ ≫ Hom.fst b} else 0)
          (if e : J.snd b = J.fst b then {eqToHom ⋯ ≫ Hom.snd b} else 0),
      nodup := ⋯ : Finset (left (J.fst b) ⟶ right b) }

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MulticospanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
b : J.R
⊢ Hom.snd b ∈
    {
      val :=
        HAdd.hAdd (α := Multiset (left (J.snd b) ⟶ right b))
          (if e : J.fst b = J.snd b then {eqToHom ⋯ ≫ Hom.fst b} else 0)
          (if e : J.snd b = J.snd b then {eqToHom ⋯ ≫ Hom.snd b} else 0),
      nodup := ⋯ : Finset (left (J.snd b) ⟶ right b) }

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MulticospanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.R
⊢ Membership.mem (γ := Finset (right a ⟶ right a)) (if e : a = a then {eqToHom ⋯} else ∅) (Hom.id (right a))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MultispanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
⊢ Membership.mem (γ := Finset (left a ⟶ left a)) (if e : a = a then {eqToHom ⋯} else ∅) (Hom.id (left a))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MultispanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
b : J.R
pos :
  ∀ (h₁ : J.fst a = b) (h₂ : J.snd a = b),
    (HAdd.hAdd (α := Multiset (left a ⟶ right b)) {Hom.fst a ≫ eqToHom ⋯} {Hom.snd a ≫ eqToHom ⋯}).Nodup
neg :
  ∀ (h₁ : J.fst a = b) (h₂ : ¬J.snd a = b),
    (HAdd.hAdd (α := Multiset (left a ⟶ right b)) {Hom.fst a ≫ eqToHom ⋯} 0).Nodup
pos₁ :
  ∀ (h₁ : ¬J.fst a = b) (h : J.snd a = b),
    (HAdd.hAdd (α := Multiset (left a ⟶ right b)) 0 {Hom.snd a ≫ eqToHom ⋯}).Nodup
neg₁ : ∀ (h₁ : ¬J.fst a = b), ¬J.snd a = b → (HAdd.hAdd (α := Multiset (left a ⟶ right b)) 0 0).Nodup
⊢ (HAdd.hAdd (α := Multiset (left a ⟶ right b)) (if e : J.fst a = b then {Hom.fst a ≫ eqToHom ⋯} else 0)
      (if e : J.snd a = b then {Hom.snd a ≫ eqToHom ⋯} else 0)).Nodup

Tactic:
split_ifs with h₁ h₂
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MultispanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst a = b
h₂ : J.snd a = b
pos : ¬Eq (α := left a ⟶ right b) (Hom.fst a ≫ eqToHom ⋯) (Hom.snd a ≫ eqToHom ⋯)
⊢ (HAdd.hAdd (α := Multiset (left a ⟶ right b)) {Hom.fst a ≫ eqToHom ⋯} {Hom.snd a ≫ eqToHom ⋯}).Nodup

Tactic:
simp only [Multiset.singleton_add, Multiset.nodup_cons, Multiset.mem_singleton,
            Multiset.nodup_singleton, and_true]

Premises used: Multiset.singleton_add, and_true, Multiset.nodup_cons, Multiset.mem_singleton, Multiset.nodup_singleton
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MultispanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst a = b
h₂ : J.snd a = b
f : (left a ⟶ right b) → Prop :=
  fun (x : left a ⟶ right b) ↦
    match (motive := (b : J.R) → (a : J.L) → (left a ⟶ right b) → (h₁ : J.fst a = b) → (h₂ : J.snd a = b) → Prop) b, a,
      x, h₁, h₂ with
    | .(J.fst a), a, Hom.fst .(a), h₁, h₂ => True
    | .(J.snd a), a, Hom.snd .(a), h₁, h₂ => False
pos : f (Hom.fst a ≫ eqToHom ⋯) ≠ f (Hom.snd a ≫ eqToHom ⋯)
⊢ ¬Eq (α := left a ⟶ right b) (Hom.fst a ≫ eqToHom ⋯) (Hom.snd a ≫ eqToHom ⋯)

Tactic:
apply ne_of_apply_ne f

Premises used: ne_of_apply_ne
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MultispanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst a = b
h₂ : J.snd a = b
f : (left a ⟶ right b) → Prop :=
  fun (x : left a ⟶ right b) ↦
    match (motive := (b : J.R) → (a : J.L) → (left a ⟶ right b) → (h₁ : J.fst a = b) → (h₂ : J.snd a = b) → Prop) b, a,
      x, h₁, h₂ with
    | .(J.fst a), a, Hom.fst .(a), h₁, h₂ => True
    | .(J.snd a), a, Hom.snd .(a), h₁, h₂ => False
subst :
  ∀ (h₂ : J.snd a = J.fst a),
    let f : (left a ⟶ right (J.fst a)) → Prop := fun (x : left a ⟶ right (J.fst a)) ↦
      match (motive := (b : J.R) → (a : J.L) → (left a ⟶ right b) → (h₁ : J.fst a = b) → (h₂ : J.snd a = b) → Prop)
        J.fst a, a, x, ⋯, h₂ with
      | .(J.fst a), a, Hom.fst .(a), h₁, h₂ => True
      | .(J.snd a), a, Hom.snd .(a), h₁, h₂ => False;
    f (Hom.fst a ≫ eqToHom ⋯) = True
⊢ f (Hom.fst a ≫ eqToHom ⋯) = True

Tactic:
subst h₁
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MultispanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
h₂ : J.snd a = J.fst a
f : (left a ⟶ right (J.fst a)) → Prop :=
  fun (x : left a ⟶ right (J.fst a)) ↦
    match (motive := (b : J.R) → (a : J.L) → (left a ⟶ right b) → (h₁ : J.fst a = b) → (h₂ : J.snd a = b) → Prop)
      J.fst a, a, x, ⋯, h₂ with
    | .(J.fst a), a, Hom.fst .(a), h₁, h₂ => True
    | .(J.snd a), a, Hom.snd .(a), h₁, h₂ => False
simp :
  (match (motive := (b : J.R) → (a : J.L) → (left a ⟶ right b) → (h₁ : J.fst a = b) → (h₂ : J.snd a = b) → Prop)
      J.fst a, a, Hom.fst a ≫ 𝟙 (right (J.fst a)), ⋯, h₂ with
    | .(J.fst a), a, Hom.fst .(a), h₁, h₂ => True
    | .(J.snd a), a, Hom.snd .(a), h₁, h₂ => False) =
    True
⊢ f (Hom.fst a ≫ eqToHom ⋯) = True

Tactic:
simp only [eqToHom_refl, f]

Premises used: CategoryTheory.eqToHom_refl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MultispanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst a = b
h₂ : J.snd a = b
f : (left a ⟶ right b) → Prop :=
  fun (x : left a ⟶ right b) ↦
    match (motive := (b : J.R) → (a : J.L) → (left a ⟶ right b) → (h₁ : J.fst a = b) → (h₂ : J.snd a = b) → Prop) b, a,
      x, h₁, h₂ with
    | .(J.fst a), a, Hom.fst .(a), h₁, h₂ => True
    | .(J.snd a), a, Hom.snd .(a), h₁, h₂ => False
tactic :
  ∀ (h₂ : J.snd a = J.fst a),
    match (motive := (b : J.R) → (a : J.L) → (left a ⟶ right b) → (h₁ : J.fst a = b) → (h₂ : J.snd a = b) → Prop)
      J.fst a, a, Hom.fst a ≫ 𝟙 (right (J.fst a)), ⋯, h₂ with
    | .(J.fst a), a, Hom.fst .(a), h₁, h₂ => True
    | .(J.snd a), a, Hom.snd .(a), h₁, h₂ => False
| f (Hom.fst a ≫ eqToHom ⋯)

Tactic:
tactic => subst h₁; simp only [eqToHom_refl, f]

Premises used: CategoryTheory.eqToHom_refl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
Goal:
J : MultispanShape
inst : Fintype J.L
inst_1 : Fintype J.R
inst_2 : DecidableEq J.L
inst_3 : DecidableEq J.R
a : J.L
b : J.R
h₁ : J.fst a = b
h₂ : J.snd a = b
f : (left a ⟶ right b) → Prop :=
  fun (x : left a ⟶ right b) ↦
    match (motive := (b : J.R) → (a : J.L) → (left a ⟶ right b) → (h₁ : J.fst a = b) → (h₂ : J.snd a = b) → Prop) b, a,
      x, h₁, h₂ with
    | .(J.fst a), a, Hom.fst .(a), h₁, h₂ => True
    | .(J.snd a), a, Hom.snd .(a), h₁, h₂ => False
pos : True ≠ f (Hom.snd a ≫ eqToHom ⋯)
⊢ f (Hom.fst a ≫ eqToHom ⋯) ≠ f (Hom.snd a ≫ eqToHom ⋯)

Tactic:
conv_lhs => tactic => subst h₁; simp only [eqToHom_refl, f]

Premises used: CategoryTheory.eqToHom_refl