awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst : Mono f
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₂)
hs :
  Eq (α := X₁)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) y₀ :
      (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₁) y₀ :
      (fun (X : Type u) ↦ X) X₁)
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₁) x₀))
    (Sum.inr
      ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) x₀))
⊢ 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₂) y₀))

Tactic:
rw [← h]
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst : Mono f
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₂)
hs :
  Eq (α := X₁)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) y₀ :
      (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₁) y₀ :
      (fun (X : Type u) ↦ X) X₁)
⊢ 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:
apply Rel'.inl_inr

Premises used: CategoryTheory.Limits.Types.Pushout.Rel'.inl_inr
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
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.inr
      ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) s))
    z
inl_inr :
  ∀ (z₁ : X₁)
    (hyz :
      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.inl
        ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) s))
      (Sum.inl z₁)
inl_inr₁ :
  ∀ (z₂ : X₂)
    (hyz :
      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₂)),
    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.inl
      ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) s))
    z

Tactic:
obtain z₁ | z₂ := z
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst : Mono f
s : S
z₁ : X₁
hyz :
  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.inl z₁)
    (Sum.inr
      ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) s))

Tactic:
replace hyz := hyz.symm
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
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 z₁)
    (Sum.inr
      ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) s))
⊢ ∃ (s_1 : S),
    z₁ = (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) s_1 ∧
      Eq (α := 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₂) s_1 :
          (fun (X : Type u) ↦ X) X₂)

Tactic:
rw [inl_rel'_inr_iff] at hyz

Premises used: CategoryTheory.Limits.Types.Pushout.inl_rel'_inr_iff
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst : Mono f
s : S
z₁ : X₁
hyz :
  ∃ (s_1 : S),
    z₁ = (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) s_1 ∧
      Eq (α := 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₂) s_1 :
          (fun (X : Type u) ↦ X) X₂)
inl_inr :
  ∀ (s' : S)
    (hs' :
      Eq (α := 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₂) s' :
          (fun (X : Type u) ↦ X) X₂)),
    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
        ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) s'))
⊢ 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₁)

Tactic:
obtain ⟨s', rfl, hs'⟩ := hyz

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst : Mono f
s s' : S
hs' :
  Eq (α := 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₂) s' :
      (fun (X : Type u) ↦ X) X₂)
⊢ 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
      ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) s'))

Tactic:
Rel'.inl_inl _ _ hs'

Premises used: CategoryTheory.Limits.Types.Pushout.Rel'.inl_inl
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst : Mono f
s s' : S
hs' :
  Eq (α := 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₂) s' :
      (fun (X : Type u) ↦ X) X₂)
⊢ 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
      ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) s'))

Tactic:
exact Rel'.inl_inl _ _ hs'

Premises used: CategoryTheory.Limits.Types.Pushout.Rel'.inl_inl
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst : Mono f
s : S
z₂ : X₂
hyz :
  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₂)
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) s = z₂

Tactic:
rw [inr_rel'_inr_iff] at hyz

Premises used: CategoryTheory.Limits.Types.Pushout.inr_rel'_inr_iff
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
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) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) s = z₂
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))
⊢ 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₂)

Tactic:
subst hyz
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst : Mono f
s : S
⊢ 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 Rel'.inl_inr

Premises used: CategoryTheory.Limits.Types.Pushout.Rel'.inl_inr
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
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₁)
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₂)
⊢ 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

Tactic:
obtain z₁ | z₂ := z
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
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₁)
⊢ (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

Premises used: CategoryTheory.Limits.Types.Pushout.inl_rel'_inl_iff
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
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))
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))
⊢ 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 rfl | ⟨_, _, h, h', rfl⟩ := hyz

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst : Mono f
s : 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
      ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) s))

Tactic:
apply Rel'.inr_inl

Premises used: CategoryTheory.Limits.Types.Pushout.Rel'.inr_inl
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
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₁)
⊢ 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'

Premises used: CategoryTheory.mono_iff_injective, inferInstance, Iff.mp, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
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₂)
⊢ 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'

Premises used: CategoryTheory.mono_iff_injective, inferInstance, Iff.mp, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
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₁)
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))
⊢ 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))

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
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₂) w))
    (Sum.inl
      ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) w))

Tactic:
apply Rel'.inr_inl

Premises used: CategoryTheory.Limits.Types.Pushout.Rel'.inr_inl
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
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₂)
⊢ ∃ (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

Premises used: CategoryTheory.Limits.Types.Pushout.inl_rel'_inr_iff
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
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
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))
⊢ 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 ⟨s, hs, rfl⟩ := hyz

Premises used: rfl