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₂
s : PushoutCocone f g
t : S
⊢ Eq.{u + 1} (α := s.pt)
    ((fun (x : X₁ ⊕ X₂) ↦
        (match (motive := X₁ ⊕ X₂ → s.pt) x with
          | Sum.inl x₁ =>
            (ConcreteCategory.hom (FC := TypeCat.Fun) s.inl :
                (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) s.pt)
              x₁
          | Sum.inr x₂ =>
            (ConcreteCategory.hom (FC := TypeCat.Fun) s.inr :
                (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) s.pt)
              x₂ :
          s.pt))
      (Sum.inl
        ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) t)))
    ((fun (x : X₁ ⊕ X₂) ↦
        (match (motive := X₁ ⊕ X₂ → s.pt) x with
          | Sum.inl x₁ =>
            (ConcreteCategory.hom (FC := TypeCat.Fun) s.inl :
                (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) s.pt)
              x₁
          | Sum.inr x₂ =>
            (ConcreteCategory.hom (FC := TypeCat.Fun) s.inr :
                (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) s.pt)
              x₂ :
          s.pt))
      (Sum.inr
        ((ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₂) t)))

Tactic:
exact ConcreteCategory.congr_hom s.condition t

Premises used: CategoryTheory.Limits.PushoutCocone.condition, CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s : PushoutCocone f g
m : Pushout f g ⟶ s.pt
h₁ : inl f g ≫ m = s.inl
h₂ : inr f g ≫ m = s.inr
h :
  ∀ (x : Pushout f g) (x₁ : X₁),
    (ConcreteCategory.hom (FC := TypeCat.Fun) m).toFun (Quot.mk (Rel f g) (Sum.inl x₁)) =
      TypeCat.Fun.toFun
        (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
          ((fun (s : PushoutCocone f g) ↦
              ↾Quot.lift (r := Rel f g)
                  (fun (x : X₁ ⊕ X₂) ↦
                    match (motive := X₁ ⊕ X₂ → s.pt) x with
                    | Sum.inl x₁ =>
                      (ConcreteCategory.hom (FC := TypeCat.Fun) s.inl :
                          (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) s.pt)
                        x₁
                    | Sum.inr x₂ =>
                      (ConcreteCategory.hom (FC := TypeCat.Fun) s.inr :
                          (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) s.pt)
                        x₂)
                  ⋯)
            s))
        (Quot.mk (Rel f g) (Sum.inl x₁))
h₃ :
  ∀ (x : Pushout f g) (x₂ : X₂),
    (ConcreteCategory.hom (FC := TypeCat.Fun) m).toFun (Quot.mk (Rel f g) (Sum.inr x₂)) =
      TypeCat.Fun.toFun
        (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
          ((fun (s : PushoutCocone f g) ↦
              ↾Quot.lift (r := Rel f g)
                  (fun (x : X₁ ⊕ X₂) ↦
                    match (motive := X₁ ⊕ X₂ → s.pt) x with
                    | Sum.inl x₁ =>
                      (ConcreteCategory.hom (FC := TypeCat.Fun) s.inl :
                          (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) s.pt)
                        x₁
                    | Sum.inr x₂ =>
                      (ConcreteCategory.hom (FC := TypeCat.Fun) s.inr :
                          (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) s.pt)
                        x₂)
                  ⋯)
            s))
        (Quot.mk (Rel f g) (Sum.inr x₂))
⊢ m =
    (fun (s : PushoutCocone f g) ↦
        ↾Quot.lift (r := Rel f g)
            (fun (x : X₁ ⊕ X₂) ↦
              match (motive := X₁ ⊕ X₂ → s.pt) x with
              | Sum.inl x₁ =>
                (ConcreteCategory.hom (FC := TypeCat.Fun) s.inl :
                    (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) s.pt)
                  x₁
              | Sum.inr x₂ =>
                (ConcreteCategory.hom (FC := TypeCat.Fun) s.inr :
                    (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) s.pt)
                  x₂)
            ⋯)
      s

Tactic:
ext ⟨x₁ | x₂⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s : PushoutCocone f g
m : Pushout f g ⟶ s.pt
h₁ : inl f g ≫ m = s.inl
h₂ : inr f g ≫ m = s.inr
x : Pushout f g
x₁ : X₁
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) m).toFun (Quot.mk (Rel f g) (Sum.inl x₁)) =
    TypeCat.Fun.toFun
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
        ((fun (s : PushoutCocone f g) ↦
            ↾Quot.lift (r := Rel f g)
                (fun (x : X₁ ⊕ X₂) ↦
                  match (motive := X₁ ⊕ X₂ → s.pt) x with
                  | Sum.inl x₁ =>
                    (ConcreteCategory.hom (FC := TypeCat.Fun) s.inl :
                        (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) s.pt)
                      x₁
                  | Sum.inr x₂ =>
                    (ConcreteCategory.hom (FC := TypeCat.Fun) s.inr :
                        (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) s.pt)
                      x₂)
                ⋯)
          s))
      (Quot.mk (Rel f g) (Sum.inl x₁))

Tactic:
ConcreteCategory.congr_hom h₁ x₁

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s : PushoutCocone f g
m : Pushout f g ⟶ s.pt
h₁ : inl f g ≫ m = s.inl
h₂ : inr f g ≫ m = s.inr
x : Pushout f g
x₁ : X₁
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) m).toFun (Quot.mk (Rel f g) (Sum.inl x₁)) =
    TypeCat.Fun.toFun
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
        ((fun (s : PushoutCocone f g) ↦
            ↾Quot.lift (r := Rel f g)
                (fun (x : X₁ ⊕ X₂) ↦
                  match (motive := X₁ ⊕ X₂ → s.pt) x with
                  | Sum.inl x₁ =>
                    (ConcreteCategory.hom (FC := TypeCat.Fun) s.inl :
                        (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) s.pt)
                      x₁
                  | Sum.inr x₂ =>
                    (ConcreteCategory.hom (FC := TypeCat.Fun) s.inr :
                        (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) s.pt)
                      x₂)
                ⋯)
          s))
      (Quot.mk (Rel f g) (Sum.inl x₁))

Tactic:
exact ConcreteCategory.congr_hom h₁ x₁

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s : PushoutCocone f g
m : Pushout f g ⟶ s.pt
h₁ : inl f g ≫ m = s.inl
h₂ : inr f g ≫ m = s.inr
x : Pushout f g
x₂ : X₂
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) m).toFun (Quot.mk (Rel f g) (Sum.inr x₂)) =
    TypeCat.Fun.toFun
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
        ((fun (s : PushoutCocone f g) ↦
            ↾Quot.lift (r := Rel f g)
                (fun (x : X₁ ⊕ X₂) ↦
                  match (motive := X₁ ⊕ X₂ → s.pt) x with
                  | Sum.inl x₁ =>
                    (ConcreteCategory.hom (FC := TypeCat.Fun) s.inl :
                        (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) s.pt)
                      x₁
                  | Sum.inr x₂ =>
                    (ConcreteCategory.hom (FC := TypeCat.Fun) s.inr :
                        (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) s.pt)
                      x₂)
                ⋯)
          s))
      (Quot.mk (Rel f g) (Sum.inr x₂))

Tactic:
ConcreteCategory.congr_hom h₂ x₂

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s : PushoutCocone f g
m : Pushout f g ⟶ s.pt
h₁ : inl f g ≫ m = s.inl
h₂ : inr f g ≫ m = s.inr
x : Pushout f g
x₂ : X₂
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) m).toFun (Quot.mk (Rel f g) (Sum.inr x₂)) =
    TypeCat.Fun.toFun
      (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
        ((fun (s : PushoutCocone f g) ↦
            ↾Quot.lift (r := Rel f g)
                (fun (x : X₁ ⊕ X₂) ↦
                  match (motive := X₁ ⊕ X₂ → s.pt) x with
                  | Sum.inl x₁ =>
                    (ConcreteCategory.hom (FC := TypeCat.Fun) s.inl :
                        (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) s.pt)
                      x₁
                  | Sum.inr x₂ =>
                    (ConcreteCategory.hom (FC := TypeCat.Fun) s.inr :
                        (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) s.pt)
                      x₂)
                ⋯)
          s))
      (Quot.mk (Rel f g) (Sum.inr x₂))

Tactic:
exact ConcreteCategory.congr_hom h₂ x₂

Premises used: CategoryTheory.ConcreteCategory.congr_hom
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₁ y₁ : X₁
mp :
  Rel' f g (Sum.inl x₁) (Sum.inl y₁) →
    x₁ = y₁ ∨
      ∃ (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₂)),
        x₁ =
            (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁)
              x₀ ∧
          y₁ =
            (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) y₀
mpr :
  (x₁ = y₁ ∨
      ∃ (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₂)),
        x₁ =
            (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁)
              x₀ ∧
          y₁ =
            (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁)
              y₀) →
    Rel' f g (Sum.inl x₁) (Sum.inl y₁)
⊢ Rel' f g (Sum.inl x₁) (Sum.inl y₁) ↔
    x₁ = y₁ ∨
      ∃ (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₂)),
        x₁ =
            (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁)
              x₀ ∧
          y₁ =
            (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) y₀

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₁ : X₁
⊢ x₁ = x₁ ∨
    ∃ (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₂)),
      x₁ =
          (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) x₀ ∧
        x₁ =
          (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) y₀

Tactic:
Or.inl rfl

Premises used: Or.inl, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₁ : X₁
⊢ x₁ = x₁ ∨
    ∃ (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₂)),
      x₁ =
          (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) x₀ ∧
        x₁ =
          (ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) y₀

Tactic:
exact Or.inl rfl

Premises used: Or.inl, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
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₂)
⊢ Eq (α := 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₁)
      ((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₁) ∨
    ∃ (x₀_1 : S) (y₀_1 : 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₀_1 :
          (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₀_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₁)
              x₀ :
            (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₀_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₁)
              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₀_1 :
            (fun (X : Type u) ↦ X) X₁)

Tactic:
Or.inr ⟨_, _, h, rfl, rfl⟩

Premises used: And.intro, Exists.intro, Or.inr, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
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₂)
⊢ Eq (α := 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₁)
      ((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₁) ∨
    ∃ (x₀_1 : S) (y₀_1 : 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₀_1 :
          (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₀_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₁)
              x₀ :
            (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₀_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₁)
              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₀_1 :
            (fun (X : Type u) ↦ X) X₁)

Tactic:
exact Or.inr ⟨_, _, h, rfl, rfl⟩

Premises used: Or.inr
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₁ : X₁
⊢ Rel' f g (Sum.inl x₁) (Sum.inl x₁)

Tactic:
apply Rel'.refl

Premises used: CategoryTheory.Limits.Types.Pushout.Rel'.refl
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
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₂)
⊢ Rel' f g
    (Sum.inl
      ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (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_1))

Tactic:
Rel'.inl_inl _ _ h

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₂
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₂)
⊢ Rel' f g
    (Sum.inl
      ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (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_1))

Tactic:
exact Rel'.inl_inl _ _ h

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₂
x₁ : X₁
x₂ : X₂
mp :
  Rel' f g (Sum.inl x₁) (Sum.inr x₂) →
    ∃ (s : S),
      x₁ = (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
mpr :
  (∃ (s : S),
      x₁ = (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) →
    Rel' f g (Sum.inl x₁) (Sum.inr x₂)
⊢ Rel' f g (Sum.inl x₁) (Sum.inr x₂) ↔
    ∃ (s : S),
      x₁ = (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

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s : S
⊢ ∃ (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₁) ∧
      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:
⟨_, rfl, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s : S
⊢ ∃ (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₁) ∧
      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:
exact ⟨_, rfl, rfl⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
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:
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₂
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:
exact 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₂
x₂ y₂ : X₂
mp : Rel' f g (Sum.inr x₂) (Sum.inr y₂) → x₂ = y₂
mpr : x₂ = y₂ → Rel' f g (Sum.inr x₂) (Sum.inr y₂)
⊢ Rel' f g (Sum.inr x₂) (Sum.inr y₂) ↔ x₂ = y₂

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₂ : X₂
⊢ x₂ = x₂

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₂ : X₂
⊢ Rel' f g (Sum.inr x₂) (Sum.inr x₂)

Tactic:
apply Rel'.refl

Premises used: CategoryTheory.Limits.Types.Pushout.Rel'.refl