awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer (goal)
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
⊢ f (eqToHom ⋯ ≫ Hom.fst b) = True
have 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, sorry, h₂ with
    | a, .(J.fst a), Hom.fst .(a), h₁, h₂ => True
    | a, .(J.snd a), Hom.snd .(a), h₁, h₂ => False;
  f (eqToHom sorry ≫ Hom.fst b) = True
Tactic: subst h₁
Cleared hypotheses: a, h₁, h₂, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer (goal)
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
⊢ f (eqToHom ⋯ ≫ Hom.fst b) = True
have simp : True = True
Tactic: simp only [eqToHom_refl, Category.id_comp, f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer (goal)
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
| f (eqToHom ⋯ ≫ Hom.fst b)
have tactic : ∀ (h₂ : J.snd b = J.fst b), True
Tactic: tactic => subst h₁; simp only [eqToHom_refl, Category.id_comp, f]
Cleared hypotheses: a, h₁, h₂, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer (goal)
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
⊢ f (eqToHom ⋯ ≫ Hom.fst b) ≠ f (eqToHom ⋯ ≫ Hom.snd b)
have pos : True ≠ f (eqToHom sorry ≫ Hom.snd b)
Tactic: conv_lhs => tactic => subst h₁; simp only [eqToHom_refl, Category.id_comp, f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer (goal)
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
⊢ f (eqToHom ⋯ ≫ Hom.snd b) = False
have 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₁, sorry with
    | a, .(J.fst a), Hom.fst .(a), h₁, h₂ => True
    | a, .(J.snd a), Hom.snd .(a), h₁, h₂ => False;
  f (eqToHom sorry ≫ Hom.snd b) = False
Tactic: subst h₂
Cleared hypotheses: a, h₁, h₂, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer (goal)
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
⊢ f (eqToHom ⋯ ≫ Hom.snd b) = False
have simp : False = False
Tactic: simp only [eqToHom_refl, Category.id_comp, f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer (goal)
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
| f (eqToHom ⋯ ≫ Hom.snd b)
have tactic : ∀ (h₁ : J.fst b = J.snd b), False
Tactic: tactic => subst h₂; simp only [eqToHom_refl, Category.id_comp, f]
Cleared hypotheses: a, h₁, h₂, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer (goal)
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 ≠ f (eqToHom ⋯ ≫ Hom.snd b)
have pos : True ≠ False
Tactic: conv_rhs => tactic => subst h₂; simp only [eqToHom_refl, Category.id_comp, f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer (goal)
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
⊢ (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
have pos : ∀ (h₁ : J.fst a = b) (h₂ : J.snd a = b),
  (HAdd.hAdd (α := Multiset (left a ⟶ right b)) {Hom.fst a ≫ eqToHom sorry} {Hom.snd a ≫ eqToHom sorry}).Nodup
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer (goal)
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
⊢ (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
have neg : ∀ (h₁ : J.fst a = b) (h₂ : ¬J.snd a = b), (HAdd.hAdd (α := Multiset (left a ⟶ right b)) {Hom.fst a ≫ eqToHom sorry} 0).Nodup
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer (goal)
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
⊢ (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
have pos₁ : ∀ (h₁ : ¬J.fst a = b) (h : J.snd a = b), (HAdd.hAdd (α := Multiset (left a ⟶ right b)) 0 {Hom.snd a ≫ eqToHom sorry}).Nodup
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer (goal)
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
⊢ (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
have neg₁ : ∀ (h₁ : ¬J.fst a = b), ¬J.snd a = b → (HAdd.hAdd (α := Multiset (left a ⟶ right b)) 0 0).Nodup
Tactic: split_ifs with h₁ h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer (goal)
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
⊢ (HAdd.hAdd (α := Multiset (left a ⟶ right b)) {Hom.fst a ≫ eqToHom ⋯} {Hom.snd a ≫ eqToHom ⋯}).Nodup
have pos : ¬Eq (α := left a ⟶ right b) (Hom.fst a ≫ eqToHom sorry) (Hom.snd a ≫ eqToHom sorry)
Tactic: simp only [Multiset.singleton_add, Multiset.nodup_cons, Multiset.mem_singleton,
            Multiset.nodup_singleton, and_true]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer (goal)
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
⊢ ¬Eq (α := left a ⟶ right b) (Hom.fst a ≫ eqToHom ⋯) (Hom.snd a ≫ eqToHom ⋯)
have pos : f (Hom.fst a ≫ eqToHom sorry) ≠ f (Hom.snd a ≫ eqToHom sorry)
Tactic: apply ne_of_apply_ne f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer (goal)
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
⊢ f (Hom.fst a ≫ eqToHom ⋯) = True
have 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, sorry, 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 sorry) = True
Tactic: subst h₁
Cleared hypotheses: b, h₁, h₂, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer (goal)
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
⊢ f (Hom.fst a ≫ eqToHom ⋯) = True
have 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)), sorry, h₂ with
  | .(J.fst a), a, Hom.fst .(a), h₁, h₂ => True
  | .(J.snd a), a, Hom.snd .(a), h₁, h₂ => False) =
  True
Tactic: simp only [eqToHom_refl, f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer (goal)
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
| f (Hom.fst a ≫ eqToHom ⋯)
have 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)), sorry, h₂ with
  | .(J.fst a), a, Hom.fst .(a), h₁, h₂ => True
  | .(J.snd a), a, Hom.snd .(a), h₁, h₂ => False
Tactic: tactic => subst h₁; simp only [eqToHom_refl, f]
Cleared hypotheses: b, h₁, h₂, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer (goal)
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
⊢ f (Hom.fst a ≫ eqToHom ⋯) ≠ f (Hom.snd a ≫ eqToHom ⋯)
have pos : True ≠ f (Hom.snd a ≫ eqToHom sorry)
Tactic: conv_lhs => tactic => subst h₁; simp only [eqToHom_refl, f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer (goal)
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
⊢ f (Hom.snd a ≫ eqToHom ⋯) = False
have subst : ∀ (h₁ : J.fst a = J.snd a),
  let f : (left a ⟶ right (J.snd a)) → Prop := fun (x : left a ⟶ right (J.snd 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.snd a, a, x, h₁, sorry with
    | .(J.fst a), a, Hom.fst .(a), h₁, h₂ => True
    | .(J.snd a), a, Hom.snd .(a), h₁, h₂ => False;
  f (Hom.snd a ≫ eqToHom sorry) = False
Tactic: subst h₂
Cleared hypotheses: b, h₁, h₂, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer (goal)
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.fst a = J.snd a
f : (left a ⟶ right (J.snd a)) → Prop :=
  fun (x : left a ⟶ right (J.snd 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.snd 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.snd a ≫ eqToHom ⋯) = False
have 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.snd a,
    a, Hom.snd a ≫ 𝟙 (right (J.snd a)), h₁, sorry with
  | .(J.fst a), a, Hom.fst .(a), h₁, h₂ => True
  | .(J.snd a), a, Hom.snd .(a), h₁, h₂ => False) =
  False
Tactic: simp only [eqToHom_refl, f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer (goal)
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
| f (Hom.snd a ≫ eqToHom ⋯)
have tactic : ∀ (h₁ : J.fst a = J.snd 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.snd a,
    a, Hom.snd a ≫ 𝟙 (right (J.snd a)), h₁, sorry with
  | .(J.fst a), a, Hom.fst .(a), h₁, h₂ => True
  | .(J.snd a), a, Hom.snd .(a), h₁, h₂ => False
Tactic: tactic => subst h₂; simp only [eqToHom_refl, f]
Cleared hypotheses: b, h₁, h₂, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer (goal)
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
⊢ True ≠ f (Hom.snd a ≫ eqToHom ⋯)
have pos : True ≠ False
Tactic: conv_rhs => tactic => subst h₂; simp only [eqToHom_refl, f]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
ι : Type w
inst_2 : Finite ι
⊢ HasLimitsOfShape.{w, w, v, u} (Discrete ι) C
have rcases : ∀ (n : ℕ) (e : ι ≃ Fin n), HasLimitsOfShape.{w, w, v, u} (Discrete ι) C
Tactic: rcases Finite.exists_equiv_fin ι with ⟨n, ⟨e⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
ι : Type w
inst_2 : Finite ι
n : ℕ
e : ι ≃ Fin n
⊢ HasLimitsOfShape.{w, w, v, u} (Discrete ι) C
have this : HasLimitsOfShape.{0, 0, v, u} (Discrete (Fin n)) C
Tactic: haveI : HasLimitsOfShape (Discrete (Fin n)) C := HasFiniteProducts.out n
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteCoproducts.{v, u} C
ι : Type w
inst_2 : Finite ι
⊢ HasColimitsOfShape.{w, w, v, u} (Discrete ι) C
have rcases : ∀ (n : ℕ) (e : ι ≃ Fin n), HasColimitsOfShape.{w, w, v, u} (Discrete ι) C
Tactic: rcases Finite.exists_equiv_fin ι with ⟨n, ⟨e⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteCoproducts.{v, u} C
ι : Type w
inst_2 : Finite ι
n : ℕ
e : ι ≃ Fin n
⊢ HasColimitsOfShape.{w, w, v, u} (Discrete ι) C
have this : HasColimitsOfShape.{0, 0, v, u} (Discrete (Fin n)) C
Tactic: haveI : HasColimitsOfShape (Discrete (Fin n)) C := HasFiniteCoproducts.out n
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
x : Cone (pair F G)
x_1 : x.pt ⟶ (binaryProductCone F G).pt
h : ∀ (j : Discrete WalkingPair), x_1 ≫ (binaryProductCone F G).π.app j = x.π.app j
⊢ x_1 = prod.lift (BinaryFan.fst x) (BinaryFan.snd x)
have simp : x_1 =
  prod.lift (x_1 ≫ (binaryProductCone F G).π.app { as := WalkingPair.left })
    (x_1 ≫ (binaryProductCone F G).π.app { as := WalkingPair.right })
Tactic: simp only [← h ⟨WalkingPair.right⟩, ← h ⟨WalkingPair.left⟩]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
a : C
z w : (F ⨯ G).obj a
h1 :
  Eq (α := (fun (X : Type w) ↦ X) (F.obj a))
    ((hom (FC := TypeCat.Fun) (NatTrans.app Limits.prod.fst a) :
          (a_1 : (fun (X : Type w) ↦ X) ((F ⨯ G).obj a)) → (fun (X : Type w) ↦ X) (F.obj a))
        z :
      (fun (X : Type w) ↦ X) (F.obj a))
    ((hom (FC := TypeCat.Fun) (NatTrans.app Limits.prod.fst a) :
          (a_1 : (fun (X : Type w) ↦ X) ((F ⨯ G).obj a)) → (fun (X : Type w) ↦ X) (F.obj a))
        w :
      (fun (X : Type w) ↦ X) (F.obj a))
h2 :
  Eq (α := (fun (X : Type w) ↦ X) (G.obj a))
    ((hom (FC := TypeCat.Fun) (NatTrans.app Limits.prod.snd a) :
          (a_1 : (fun (X : Type w) ↦ X) ((F ⨯ G).obj a)) → (fun (X : Type w) ↦ X) (G.obj a))
        z :
      (fun (X : Type w) ↦ X) (G.obj a))
    ((hom (FC := TypeCat.Fun) (NatTrans.app Limits.prod.snd a) :
          (a_1 : (fun (X : Type w) ↦ X) ((F ⨯ G).obj a)) → (fun (X : Type w) ↦ X) (G.obj a))
        w :
      (fun (X : Type w) ↦ X) (G.obj a))
⊢ z = w
have a₁ : Eq (α := F.obj a × G.obj a)
  ((binaryProductEquiv F G a : (a_1 : (F ⨯ G).obj a) → F.obj a × G.obj a) z : F.obj a × G.obj a)
  ((binaryProductEquiv F G a : (a_1 : (F ⨯ G).obj a) → F.obj a × G.obj a) w : F.obj a × G.obj a)
Tactic: apply Equiv.injective (binaryProductEquiv F G a)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{v, w, u, w + 1} C (Type w)
x : C
⊢ ↾Sum.map
        (⇑(hom (FC := TypeCat.Fun) (F.map (𝟙 x))) :
          (a : (fun (X : Type w) ↦ X) (F.obj x)) → (fun (X : Type w) ↦ X) (F.obj x))
        (⇑(hom (FC := TypeCat.Fun) (G.map (𝟙 x))) :
          (a : (fun (X : Type w) ↦ X) (G.obj x)) → (fun (X : Type w) ↦ X) (G.obj x)) =
    𝟙 (F.obj x ⊕ G.obj x)
have h : ∀ (val : F.obj x),
  TypeCat.Fun.toFun (X := F.obj x ⊕ G.obj x)
      (hom (FC := TypeCat.Fun)
        (↾Sum.map
            (⇑(hom (FC := TypeCat.Fun) (F.map (𝟙 x))) :
              (a : (fun (X : Type w) ↦ X) (F.obj x)) → (fun (X : Type w) ↦ X) (F.obj x))
            (⇑(hom (FC := TypeCat.Fun) (G.map (𝟙 x))) :
              (a : (fun (X : Type w) ↦ X) (G.obj x)) → (fun (X : Type w) ↦ X) (G.obj x))))
      (Sum.inl val) =
    (hom (FC := TypeCat.Fun) (𝟙 (F.obj x ⊕ G.obj x))).toFun (Sum.inl val)
Tactic: ext ⟨⟩