awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s : S
⊢ Quot.mk (Rel f g)
      (Sum.inl
        ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) s)) =
    Quot.mk (Rel f g)
      (Sum.inr
        ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) s))
have inr_inl : Rel f g
  (Sum.inl
    ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) s))
  (Sum.inr
    ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) s))
Tactic: apply Quot.sound
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst : Mono f
a b : X₁ ⊕ X₂
⊢ Quot.mk (Rel f g) a = Quot.mk (Rel f g) b ↔ Rel' f g a b
have rw : Quot.mk (Rel f g) a = Quot.mk (Rel f g) b ↔ Quot.mk (Rel' f g) a = Quot.mk (Rel' f g) b
Tactic: rw [← (equivalence_rel' f g).quot_mk_eq_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst : Mono f
x₁ : X₁
x₂ : X₂
⊢ Eq (α := (fun (X : Type u) ↦ X) (Pushout f g))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (inl f g) :
            (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) (Pushout f g))
          x₁ :
        (fun (X : Type u) ↦ X) (Pushout f g))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (inr f g) :
            (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) (Pushout f g))
          x₂ :
        (fun (X : Type u) ↦ X) (Pushout f g)) ↔
    ∃ (s : S),
      (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) s = x₁ ∧
        (ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) s = x₂
have refine : Rel' f g (Sum.inl x₁) (Sum.inr x₂) ↔
  ∃ (s : S),
    (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) s = x₁ ∧
      (ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) s = x₂
Tactic: refine (Pushout.quot_mk_eq_iff f g (Sum.inl x₁) (Sum.inr x₂)).trans ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst : Mono f
x₁ : X₁
x₂ : X₂
⊢ Rel' f g (Sum.inl x₁) (Sum.inr x₂) ↔
    ∃ (s : S),
      (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) s = x₁ ∧
        (ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) s = x₂
have mp : Rel' f g (Sum.inl x₁) (Sum.inr x₂) →
  ∃ (s : S),
    (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) s = x₁ ∧
      (ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) s = x₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst : Mono f
x₁ : X₁
x₂ : X₂
mp :
  Rel' f g (Sum.inl x₁) (Sum.inr x₂) →
    ∃ (s : S),
      (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) s = x₁ ∧
        (ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) s = x₂
⊢ Rel' f g (Sum.inl x₁) (Sum.inr x₂) ↔
    ∃ (s : S),
      (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) s = x₁ ∧
        (ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) s = x₂
have mpr : (∃ (s : S),
    (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) s = x₁ ∧
      (ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) s =
        x₂) →
  Rel' f g (Sum.inl x₁) (Sum.inr x₂)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst : Mono f
⊢ Mono (inr f g)
have rw : Function.Injective (α := (fun (X : Type u) ↦ X) X₂) (β := (fun (X : Type u) ↦ X) (Pushout f g))
  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (inr f g)) :
    (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) (Pushout f g))
Tactic: rw [mono_iff_injective]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c c' : PushoutCocone f g
e : c ≅ c'
x₁ : X₁
x₂ : X₂
h :
  Eq (α := (fun (X : Type u) ↦ X) c.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inl : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c.pt)
        x₁ :
      (fun (X : Type u) ↦ X) c.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inr : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c.pt)
        x₂ :
      (fun (X : Type u) ↦ X) c.pt)
⊢ Eq (α := (fun (X : Type u) ↦ X) c'.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) c'.inl : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c'.pt)
        x₁ :
      (fun (X : Type u) ↦ X) c'.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) c'.inr : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c'.pt)
        x₂ :
      (fun (X : Type u) ↦ X) c'.pt)
have h₁ : Eq (α := (fun (X : Type u) ↦ X) c'.pt)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) c'.inl : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c'.pt)
      x₁ :
    (fun (X : Type u) ↦ X) c'.pt)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) e.hom.hom :
        (a : (fun (X : Type u) ↦ X) c.pt) → (fun (X : Type u) ↦ X) c'.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inl : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c.pt)
          x₁ :
        (fun (X : Type u) ↦ X) c.pt) :
    (fun (X : Type u) ↦ X) c'.pt)
Tactic: convert! congr_arg e.hom.hom h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c c' : PushoutCocone f g
e : c ≅ c'
x₁ : X₁
x₂ : X₂
h :
  Eq (α := (fun (X : Type u) ↦ X) c.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inl : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c.pt)
        x₁ :
      (fun (X : Type u) ↦ X) c.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inr : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c.pt)
        x₂ :
      (fun (X : Type u) ↦ X) c.pt)
h₁ :
  Eq (α := (fun (X : Type u) ↦ X) c'.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) c'.inl : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c'.pt)
        x₁ :
      (fun (X : Type u) ↦ X) c'.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) e.hom.hom :
          (a : (fun (X : Type u) ↦ X) c.pt) → (fun (X : Type u) ↦ X) c'.pt)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inl :
              (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c.pt)
            x₁ :
          (fun (X : Type u) ↦ X) c.pt) :
      (fun (X : Type u) ↦ X) c'.pt)
⊢ Eq (α := (fun (X : Type u) ↦ X) c'.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) c'.inl : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c'.pt)
        x₁ :
      (fun (X : Type u) ↦ X) c'.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) c'.inr : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c'.pt)
        x₂ :
      (fun (X : Type u) ↦ X) c'.pt)
have h₂ : Eq (α := (fun (X : Type u) ↦ X) c'.pt)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) c'.inr : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c'.pt)
      x₂ :
    (fun (X : Type u) ↦ X) c'.pt)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) e.hom.hom :
        (a : (fun (X : Type u) ↦ X) c.pt) → (fun (X : Type u) ↦ X) c'.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inr : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c.pt)
          x₂ :
        (fun (X : Type u) ↦ X) c.pt) :
    (fun (X : Type u) ↦ X) c'.pt)
Tactic: convert! congr_arg e.hom.hom h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c c' : PushoutCocone f g
e : c ≅ c'
x₁ : X₁
x₂ : X₂
⊢ Eq (α := (fun (X : Type u) ↦ X) c.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inl : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c.pt)
          x₁ :
        (fun (X : Type u) ↦ X) c.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inr : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c.pt)
          x₂ :
        (fun (X : Type u) ↦ X) c.pt) ↔
    Eq (α := (fun (X : Type u) ↦ X) c'.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c'.inl :
            (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c'.pt)
          x₁ :
        (fun (X : Type u) ↦ X) c'.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c'.inr :
            (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c'.pt)
          x₂ :
        (fun (X : Type u) ↦ X) c'.pt)
have mp : Eq (α := (fun (X : Type u) ↦ X) c.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inl : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c.pt)
        x₁ :
      (fun (X : Type u) ↦ X) c.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inr : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c.pt)
        x₂ :
      (fun (X : Type u) ↦ X) c.pt) →
  Eq (α := (fun (X : Type u) ↦ X) c'.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) c'.inl : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c'.pt)
        x₁ :
      (fun (X : Type u) ↦ X) c'.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) c'.inr : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c'.pt)
        x₂ :
      (fun (X : Type u) ↦ X) c'.pt)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c c' : PushoutCocone f g
e : c ≅ c'
x₁ : X₁
x₂ : X₂
mp :
  Eq (α := (fun (X : Type u) ↦ X) c.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inl : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c.pt)
          x₁ :
        (fun (X : Type u) ↦ X) c.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inr : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c.pt)
          x₂ :
        (fun (X : Type u) ↦ X) c.pt) →
    Eq (α := (fun (X : Type u) ↦ X) c'.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c'.inl :
            (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c'.pt)
          x₁ :
        (fun (X : Type u) ↦ X) c'.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c'.inr :
            (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c'.pt)
          x₂ :
        (fun (X : Type u) ↦ X) c'.pt)
⊢ Eq (α := (fun (X : Type u) ↦ X) c.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inl : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c.pt)
          x₁ :
        (fun (X : Type u) ↦ X) c.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inr : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c.pt)
          x₂ :
        (fun (X : Type u) ↦ X) c.pt) ↔
    Eq (α := (fun (X : Type u) ↦ X) c'.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c'.inl :
            (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c'.pt)
          x₁ :
        (fun (X : Type u) ↦ X) c'.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c'.inr :
            (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c'.pt)
          x₂ :
        (fun (X : Type u) ↦ X) c'.pt)
have mpr : Eq (α := (fun (X : Type u) ↦ X) c'.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) c'.inl : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c'.pt)
        x₁ :
      (fun (X : Type u) ↦ X) c'.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) c'.inr : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c'.pt)
        x₂ :
      (fun (X : Type u) ↦ X) c'.pt) →
  Eq (α := (fun (X : Type u) ↦ X) c.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inl : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c.pt)
        x₁ :
      (fun (X : Type u) ↦ X) c.pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inr : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c.pt)
        x₂ :
      (fun (X : Type u) ↦ X) c.pt)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c : PushoutCocone f g
hc : IsColimit c
h₁ :
  Function.Injective (α := (fun (X : Type u) ↦ X) S) (β := (fun (X : Type u) ↦ X) X₁)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁)
x₁ : X₁
x₂ : X₂
⊢ Eq (α := (fun (X : Type u) ↦ X) c.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inl : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) c.pt)
          x₁ :
        (fun (X : Type u) ↦ X) c.pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) c.inr : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c.pt)
          x₂ :
        (fun (X : Type u) ↦ X) c.pt) ↔
    ∃ (s : S),
      (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) s = x₁ ∧
        (ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) s = x₂
have rw : Eq (α := (fun (X : Type u) ↦ X) (Pushout.cocone f g).pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Pushout.cocone f g).inl :
          (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) (Pushout.cocone f g).pt)
        x₁ :
      (fun (X : Type u) ↦ X) (Pushout.cocone f g).pt)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Pushout.cocone f g).inr :
          (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) (Pushout.cocone f g).pt)
        x₂ :
      (fun (X : Type u) ↦ X) (Pushout.cocone f g).pt) ↔
  ∃ (s : S),
    (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) s = x₁ ∧
      (ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) s = x₂
Tactic: rw [pushoutCocone_inl_eq_inr_iff_of_iso
    (Cocone.ext (IsColimit.coconePointUniqueUpToIso hc (Pushout.isColimitCocone f g))
    (by simp))]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (hypothesis)
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c : PushoutCocone f g
hc : IsColimit c
h₁ :
  Function.Injective (α := (fun (X : Type u) ↦ X) S) (β := (fun (X : Type u) ↦ X) X₁)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁)
x₁ : X₁
x₂ : X₂
⊢ Eq (α := (fun (X : Type u) ↦ X) (Pushout.cocone f g).pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Pushout.cocone f g).inl :
            (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) (Pushout.cocone f g).pt)
          x₁ :
        (fun (X : Type u) ↦ X) (Pushout.cocone f g).pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (Pushout.cocone f g).inr :
            (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) (Pushout.cocone f g).pt)
          x₂ :
        (fun (X : Type u) ↦ X) (Pushout.cocone f g).pt) ↔
    ∃ (s : S),
      (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) s = x₁ ∧
        (ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) s = x₂
have this : Mono f
Tactic: have := (mono_iff_injective f).2 h₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c : PushoutCocone f g
hc : IsColimit c
inst : Mono f
⊢ Mono c.inr
have change : Mono
  (Pushout.inr f g ≫
    ((Cocone.forget (span f g)).mapIso (Cocone.ext (hc.coconePointUniqueUpToIso (Pushout.isColimitCocone f g)) sorry)).inv)
Tactic: change Mono ((Pushout.inr f g) ≫
    ((Cocone.forget _).mapIso
      (Cocone.ext (IsColimit.coconePointUniqueUpToIso hc
        (Pushout.isColimitCocone f g)) (by simp))).inv)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c : PushoutCocone f g
hc : IsColimit c
h₁ :
  Function.Injective (α := (fun (X : Type u) ↦ X) S) (β := (fun (X : Type u) ↦ X) X₁)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁)
⊢ Function.Injective (α := (fun (X : Type u) ↦ X) X₂) (β := (fun (X : Type u) ↦ X) c.pt)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) c.inr) : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) c.pt)
have rw : ∀ (h₁ : Mono f), Mono c.inr
Tactic: rw [← mono_iff_injective] at h₁ ⊢
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
Goal:
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPushout t l r b
x₄ : X₄
⊢ (∃ (x₂ : (fun (X : Type u) ↦ X) X₂),
      (ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) x₂ =
        x₄) ∨
    ∃ (x₃ : (fun (X : Type u) ↦ X) X₃),
      (ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) x₃ = x₄
have obtain : ∀ (j : WalkingSpan) (x : (span t l).obj j),
  (∃ (x₂ : (fun (X : Type u) ↦ X) X₂),
      Eq (α := (fun (X : Type u) ↦ X) X₄)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) x₂ :
          (fun (X : Type u) ↦ X) X₄)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (h.cocone.ι.app j) :
              (a : (fun (X : Type u) ↦ X) ((span t l).obj j)) →
                (fun (X : Type u) ↦ X) (((Functor.const WalkingSpan).obj h.cocone.pt).obj j))
            x :
          (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const WalkingSpan) h.cocone.pt) j))) ∨
    ∃ (x₃ : (fun (X : Type u) ↦ X) X₃),
      Eq (α := (fun (X : Type u) ↦ X) X₄)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) x₃ :
          (fun (X : Type u) ↦ X) X₄)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (h.cocone.ι.app j) :
              (a : (fun (X : Type u) ↦ X) ((span t l).obj j)) →
                (fun (X : Type u) ↦ X) (((Functor.const WalkingSpan).obj h.cocone.pt).obj j))
            x :
          (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const WalkingSpan) h.cocone.pt) j))
Tactic: obtain ⟨j, x, rfl⟩ := jointly_surjective_of_isColimit h.isColimit x₄
Cleared hypotheses: x₄
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
Goal:
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPushout t l r b
j : WalkingSpan
x : (span t l).obj j
⊢ (∃ (x₂ : (fun (X : Type u) ↦ X) X₂),
      Eq (α := (fun (X : Type u) ↦ X) X₄)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) x₂ :
          (fun (X : Type u) ↦ X) X₄)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (h.cocone.ι.app j) :
              (a : (fun (X : Type u) ↦ X) ((span t l).obj j)) →
                (fun (X : Type u) ↦ X) (((Functor.const WalkingSpan).obj h.cocone.pt).obj j))
            x :
          (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const WalkingSpan) h.cocone.pt) j))) ∨
    ∃ (x₃ : (fun (X : Type u) ↦ X) X₃),
      Eq (α := (fun (X : Type u) ↦ X) X₄)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) x₃ :
          (fun (X : Type u) ↦ X) X₄)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (h.cocone.ι.app j) :
              (a : (fun (X : Type u) ↦ X) ((span t l).obj j)) →
                (fun (X : Type u) ↦ X) (((Functor.const WalkingSpan).obj h.cocone.pt).obj j))
            x :
          (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const WalkingSpan) h.cocone.pt) j))
have none : ∀ (x : (span t l).obj none),
  (∃ (x₂ : (fun (X : Type u) ↦ X) X₂),
      Eq (α := (fun (X : Type u) ↦ X) X₄)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) x₂ :
          (fun (X : Type u) ↦ X) X₄)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (h.cocone.ι.app none) :
              (a : (fun (X : Type u) ↦ X) ((span t l).obj none)) →
                (fun (X : Type u) ↦ X) (((Functor.const WalkingSpan).obj h.cocone.pt).obj none))
            x :
          (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const WalkingSpan) h.cocone.pt) none))) ∨
    ∃ (x₃ : (fun (X : Type u) ↦ X) X₃),
      Eq (α := (fun (X : Type u) ↦ X) X₄)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) x₃ :
          (fun (X : Type u) ↦ X) X₄)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (h.cocone.ι.app none) :
              (a : (fun (X : Type u) ↦ X) ((span t l).obj none)) →
                (fun (X : Type u) ↦ X) (((Functor.const WalkingSpan).obj h.cocone.pt).obj none))
            x :
          (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const WalkingSpan) h.cocone.pt) none))
Tactic: obtain (_ | _ | _) := j
Cleared hypotheses: j, x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
Goal:
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPushout t l r b
x : (span t l).obj none
⊢ Eq (α := (fun (X : Type u) ↦ X) X₄)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) x :
          (fun (X : Type u) ↦ X) X₂) :
      (fun (X : Type u) ↦ X) X₄)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (h.cocone.ι.app none) :
          (a : (fun (X : Type u) ↦ X) ((span t l).obj none)) →
            (fun (X : Type u) ↦ X) (((Functor.const WalkingSpan).obj h.cocone.pt).obj none))
        x :
      (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const WalkingSpan) h.cocone.pt) none))
have simp : Eq (α := X₄)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : X₂) → X₄)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) t : (a : X₁) → X₂) x : X₂) :
    X₄)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (t ≫ r) : (a : X₁) → h.cocone.pt) x : h.cocone.pt)
Tactic: simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
Goal:
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPushout t l r b
x₄ : X₄
⊢ (∃ (x₂ : (fun (X : Type u) ↦ X) X₂),
      (ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) x₂ =
        x₄) ∨
    ∃ (x₃ : (fun (X : Type u) ↦ X) X₃),
      (ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) x₃ =
          x₄ ∧
        x₃ ∉
          Set.range (ι := (fun (X : Type u) ↦ X) X₁)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
              (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃)
have inl : ∀
  (h₁ :
    ∃ (x₂ : (fun (X : Type u) ↦ X) X₂),
      (ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) x₂ =
        x₄),
  (∃ (x₂ : (fun (X : Type u) ↦ X) X₂),
      (ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) x₂ =
        x₄) ∨
    ∃ (x₃ : (fun (X : Type u) ↦ X) X₃),
      (ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) x₃ =
          x₄ ∧
        x₃ ∉
          Set.range (ι := (fun (X : Type u) ↦ X) X₁)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
              (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃)
Tactic: obtain h₁ | ⟨x₃, hx₃⟩ := eq_or_eq_of_isPushout h x₄