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₂
inst : Mono f
z : X₁ ⊕ X₂
s : S
hyz :
  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))
    z
⊢ 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))
    z
have inr_inl : ∀ (z₁ : X₁)
  (hyz :
    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.inl z₁)),
  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))
    (Sum.inl z₁)
Tactic: obtain z₁ | z₂ := z
Cleared hypotheses: z, hyz
-- 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
z : X₁ ⊕ X₂
s : S
hyz :
  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))
    z
inr_inl :
  ∀ (z₁ : X₁)
    (hyz :
      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.inl z₁)),
    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))
      (Sum.inl z₁)
⊢ 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))
    z
have inr_inl₁ : ∀ (z₂ : X₂)
  (hyz :
    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 z₂)),
  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))
    (Sum.inr z₂)
Tactic: obtain z₁ | z₂ := z
Cleared hypotheses: z, hyz
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (hypothesis)
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst : Mono f
s : S
z₁ : X₁
hyz :
  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.inl z₁)
⊢ 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))
    (Sum.inl z₁)
have hyz₁ : (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) s = z₁ ∨
  ∃ (x₀ : S) (y₀ : S) (_ :
    Eq (α := (fun (X : Type u) ↦ X) X₂)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) x₀ :
        (fun (X : Type u) ↦ X) X₂)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) y₀ :
        (fun (X : Type u) ↦ X) X₂)),
    Eq (α := X₁)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) 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₀ :
          (fun (X : Type u) ↦ X) X₁) ∧
      z₁ = (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) y₀
Tactic: rw [inl_rel'_inl_iff] at hyz
Cleared hypotheses: hyz
-- 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
s : S
z₁ : X₁
hyz :
  (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) s = z₁ ∨
    ∃ (x₀ : S) (y₀ : S) (_ :
      Eq (α := (fun (X : Type u) ↦ X) X₂)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) x₀ :
          (fun (X : Type u) ↦ X) X₂)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) y₀ :
          (fun (X : Type u) ↦ X) X₂)),
      Eq (α := X₁)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) 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₀ :
            (fun (X : Type u) ↦ X) X₁) ∧
        z₁ =
          (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) y₀
⊢ 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))
    (Sum.inl z₁)
have inr_inl : 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))
  (Sum.inl
    ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) s))
Tactic: obtain rfl | ⟨_, _, h, h', rfl⟩ := hyz
Cleared hypotheses: z₁, hyz
-- 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
s : S
z₁ : X₁
hyz :
  (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) s = z₁ ∨
    ∃ (x₀ : S) (y₀ : S) (_ :
      Eq (α := (fun (X : Type u) ↦ X) X₂)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) x₀ :
          (fun (X : Type u) ↦ X) X₂)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) y₀ :
          (fun (X : Type u) ↦ X) X₂)),
      Eq (α := X₁)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) 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₀ :
            (fun (X : Type u) ↦ X) X₁) ∧
        z₁ =
          (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) y₀
inr_inl :
  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))
    (Sum.inl
      ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) s))
⊢ 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))
    (Sum.inl z₁)
have inr_inl₁ : ∀ (w w_1 : S)
  (h :
    Eq (α := (fun (X : Type u) ↦ X) X₂)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) w :
        (fun (X : Type u) ↦ X) X₂)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) w_1 :
        (fun (X : Type u) ↦ X) X₂))
  (h' :
    Eq (α := X₁)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) 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₁) w :
        (fun (X : Type u) ↦ X) X₁)),
  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))
    (Sum.inl
      ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) w_1))
Tactic: obtain rfl | ⟨_, _, h, h', rfl⟩ := hyz
Cleared hypotheses: z₁, hyz
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (hypothesis)
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst : Mono f
s w w_1 : S
h :
  Eq (α := (fun (X : Type u) ↦ X) X₂)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) w :
      (fun (X : Type u) ↦ X) X₂)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) w_1 :
      (fun (X : Type u) ↦ X) X₂)
h' :
  Eq (α := X₁)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) 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₁) w :
      (fun (X : Type u) ↦ X) X₁)
⊢ 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))
    (Sum.inl
      ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) w_1))
have h₁ : Eq (α := (fun (X : Type u) ↦ X) X₂)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) s :
    (fun (X : Type u) ↦ X) X₂)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) w_1 :
    (fun (X : Type u) ↦ X) X₂)
Tactic: obtain rfl := (mono_iff_injective f).1 inferInstance h'
Cleared hypotheses: w, h, h'
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (hypothesis)
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst : Mono f
s w w_1 : S
h :
  Eq (α := (fun (X : Type u) ↦ X) X₂)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) w :
      (fun (X : Type u) ↦ X) X₂)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) w_1 :
      (fun (X : Type u) ↦ X) X₂)
h' :
  Eq (α := X₁)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) 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₁) w :
      (fun (X : Type u) ↦ X) X₁)
h₁ :
  Eq (α := (fun (X : Type u) ↦ X) X₂)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) s :
      (fun (X : Type u) ↦ X) X₂)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) w_1 :
      (fun (X : Type u) ↦ X) X₂)
⊢ 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))
    (Sum.inl
      ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) w_1))
have h'₁ : Eq (α := X₁)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) 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₁) s :
    (fun (X : Type u) ↦ X) X₁)
Tactic: obtain rfl := (mono_iff_injective f).1 inferInstance h'
Cleared hypotheses: w, h, h'
-- 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
s w : S
h :
  Eq (α := (fun (X : Type u) ↦ X) X₂)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) s :
      (fun (X : Type u) ↦ X) X₂)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) w :
      (fun (X : Type u) ↦ X) X₂)
h' :
  Eq (α := X₁)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) 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₁) s :
      (fun (X : Type u) ↦ X) X₁)
⊢ 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))
    (Sum.inl
      ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) w))
have inr_inl : Rel' f g
  (Sum.inr
    ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) w))
  (Sum.inl
    ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) w))
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (hypothesis)
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst : Mono f
s : S
z₂ : X₂
hyz :
  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 z₂)
⊢ 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))
    (Sum.inr z₂)
have hyz₁ : ∃ (s_1 : S),
  Eq (α := X₁)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) 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₁) s_1 :
        (fun (X : Type u) ↦ X) X₁) ∧
    z₂ = (ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) s_1
Tactic: rw [inl_rel'_inr_iff] at hyz
Cleared hypotheses: hyz
-- 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
s : S
z₂ : X₂
hyz :
  ∃ (s_1 : S),
    Eq (α := X₁)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) 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₁) s_1 :
          (fun (X : Type u) ↦ X) X₁) ∧
      z₂ = (ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) s_1
⊢ 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))
    (Sum.inr z₂)
have inr_inl : ∀ (s_1 : S)
  (hs :
    Eq (α := X₁)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) 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₁) s_1 :
        (fun (X : Type u) ↦ X) X₁)),
  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))
    (Sum.inr
      ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) s_1))
Tactic: obtain ⟨s, hs, rfl⟩ := hyz
Cleared hypotheses: z₂, hyz
-- 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
s_1 s : S
hs :
  Eq (α := X₁)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) s_1 :
      (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₁) s :
      (fun (X : Type u) ↦ X) X₁)
⊢ 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_1))
    (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 : ∀
  (hs :
    Eq (α := X₁)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) s_1 :
        (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₁) s_1 :
        (fun (X : Type u) ↦ X) X₁)),
  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_1))
    (Sum.inr
      ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) s_1))
Tactic: obtain rfl := (mono_iff_injective f).1 inferInstance hs
Cleared hypotheses: s, hs
-- 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 a : 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 (hypothesis)
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₀ y₀ : S
h :
  Eq (α := (fun (X : Type u) ↦ X) X₂)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) x₀ :
      (fun (X : Type u) ↦ X) X₂)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) y₀ :
      (fun (X : Type u) ↦ X) X₂)
⊢ 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₁)
          x₀)) =
    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₁) y₀))
have h₀ : Rel f g
  (Sum.inl
    ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) x₀))
  (Sum.inr
    ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) x₀))
Tactic: have h₀ : Rel f g _ _ := Rel.inl_inr x₀
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₀ y₀ : S
h :
  Eq (α := (fun (X : Type u) ↦ X) X₂)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) x₀ :
      (fun (X : Type u) ↦ X) X₂)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) y₀ :
      (fun (X : Type u) ↦ X) X₂)
h₀ :
  Rel f g
    (Sum.inl
      ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) x₀))
    (Sum.inr
      ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) x₀))
⊢ 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₁)
          x₀)) =
    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₁) y₀))
have inl_inl : 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₂) y₀)) =
  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₁) y₀))
Tactic: rw [Quot.sound h₀, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₀ y₀ : S
h :
  Eq (α := (fun (X : Type u) ↦ X) X₂)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) x₀ :
      (fun (X : Type u) ↦ X) X₂)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) y₀ :
      (fun (X : Type u) ↦ X) X₂)
h₀ :
  Rel f g
    (Sum.inl
      ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) x₀))
    (Sum.inr
      ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) x₀))
⊢ 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₂)
          y₀)) =
    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₁) y₀))
have inl_inl : 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₁) y₀)) =
  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₂) y₀))
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₀ y₀ : S
h :
  Eq (α := (fun (X : Type u) ↦ X) X₂)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) x₀ :
      (fun (X : Type u) ↦ X) X₂)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) y₀ :
      (fun (X : Type u) ↦ X) X₂)
h₀ :
  Rel f g
    (Sum.inl
      ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) x₀))
    (Sum.inr
      ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) x₀))
⊢ 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₁)
          y₀)) =
    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₂) y₀))
have inl_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₁) y₀))
  (Sum.inr
    ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) y₀))
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₂
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 inl_inr : 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₂
s : 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)) =
    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))
have inr_inl : 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))
Tactic: symm