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
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₁)
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))
⊢ 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))

Tactic:
obtain rfl := (mono_iff_injective f).1 inferInstance hs

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 : 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 :
      (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))

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₂
s : S
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))
⊢ 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:
apply Quot.sound

Premises used: Quot.sound
-- 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:
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₂
a : X₁ ⊕ X₂
⊢ Quot.mk (Rel f g) a = Quot.mk (Rel f g) a

Tactic:
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₂)
⊢ 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₀
-- 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₂)
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₀))
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₀))
⊢ 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₀))

Tactic:
rw [Quot.sound h₀, h]

Premises used: Quot.sound
-- 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₂)
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₀))
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₀))
⊢ 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:
symm
-- 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₂)
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₀))
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₀))
⊢ 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:
apply Quot.sound

Premises used: Quot.sound
-- 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₂)
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₀))
⊢ 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 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
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))
⊢ 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:
apply Quot.sound

Premises used: Quot.sound
-- 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:
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₂
s : S
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))
⊢ 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))

Tactic:
symm
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s : S
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))
⊢ 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:
apply Quot.sound

Premises used: Quot.sound
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x_1 : Pushout f g
x : X₁ ⊕ X₂
⊢ Quot.lift (r := Rel' f g) (Quot.mk (Rel f g)) ⋯
      (Quot.lift (r := Rel f g) (Quot.mk (Rel' f g)) ⋯ (Quot.mk (Rel f g) x)) =
    Quot.mk (Rel f g) x

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x_1 : Pushout' f g
x : X₁ ⊕ X₂
⊢ Quot.lift (r := Rel f g) (Quot.mk (Rel' f g)) ⋯
      (Quot.lift (r := Rel' f g) (Quot.mk (Rel f g)) ⋯ (Quot.mk (Rel' f g) x)) =
    Quot.mk (Rel' f g) x

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst : Mono f
a b : X₁ ⊕ X₂
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
⊢ Quot.mk (Rel f g) a = Quot.mk (Rel f g) b ↔ Rel' f g a b

Tactic:
rw [← (equivalence_rel' f g).quot_mk_eq_iff]

Premises used: CategoryTheory.Limits.Types.Pushout.equivalence_rel', Equivalence.quot_mk_eq_iff
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
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 ↔ Quot.mk (Rel' f g) a = Quot.mk (Rel' f g) b

Tactic:
⟨fun h => (equivPushout' f g).symm.injective h,
    fun h => (equivPushout' f g).injective h⟩

Premises used: CategoryTheory.Limits.Types.Pushout.equivPushout', Iff.intro, Equiv.injective, Equiv.symm
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
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 ↔ Quot.mk (Rel' f g) a = Quot.mk (Rel' f g) b

Tactic:
exact ⟨fun h => (equivPushout' f g).symm.injective h,
    fun h => (equivPushout' f g).injective h⟩
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
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₂

Tactic:
(Pushout.quot_mk_eq_iff f g (Sum.inl x₁) (Sum.inr x₂)).trans ?_

Premises used: Sum.inl, CategoryTheory.Limits.Types.Pushout.quot_mk_eq_iff, Sum.inr, Iff.trans, CategoryTheory.Limits.Types.Pushout
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst : Mono f
x₁ : X₁
x₂ : X₂
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₂
⊢ 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₂

Tactic:
refine (Pushout.quot_mk_eq_iff f g (Sum.inl x₁) (Sum.inr x₂)).trans ?_

Premises used: Sum.inl, CategoryTheory.Limits.Types.Pushout.quot_mk_eq_iff, Sum.inr, Iff.trans
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
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₂
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₂)
⊢ 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
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst : Mono f
s : S
⊢ ∃ (s_1 : S),
    Eq (α := (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₁)
        ((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₁) ∧
      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_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₂) s :
          (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₂
inst : Mono f
s : S
⊢ ∃ (s_1 : S),
    Eq (α := (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₁)
        ((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₁) ∧
      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_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₂) s :
          (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₂
inst : Mono f
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))
⊢ Mono (inr f g)

Tactic:
rw [mono_iff_injective]

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

Tactic:
simpa using (Pushout.quot_mk_eq_iff f g (Sum.inr x₂) (Sum.inr y₂)).1 h

Premises used: CategoryTheory.Limits.Types.Pushout.quot_mk_eq_iff, Sum.inr, Iff.mp
-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
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) 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)
    ((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:
congr_arg e.hom.hom h

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.CoconeMorphism.hom, congr_arg, CategoryTheory.Iso.hom, DFunLike.coe