awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pullbacks (goal)
Goal:
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
w : t ≫ r = l ≫ b
h₁ :
  ∀ (x₁ y₁ : (fun (X : Type u) ↦ X) X₁),
    Eq (α := (fun (X : Type u) ↦ X) X₂)
          ((hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) x₁ :
            (fun (X : Type u) ↦ X) X₂)
          ((hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) y₁ :
            (fun (X : Type u) ↦ X) X₂) ∧
        Eq (α := (fun (X : Type u) ↦ X) X₃)
          ((hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) x₁ :
            (fun (X : Type u) ↦ X) X₃)
          ((hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) y₁ :
            (fun (X : Type u) ↦ X) X₃) →
      x₁ = y₁
h₂ :
  ∀ (x₂ : (fun (X : Type u) ↦ X) X₂) (x₃ : (fun (X : Type u) ↦ X) X₃),
    Eq (α := (fun (X : Type u) ↦ X) X₄)
        ((hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) x₂ :
          (fun (X : Type u) ↦ X) X₄)
        ((hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) x₃ :
          (fun (X : Type u) ↦ X) X₄) →
      ∃ (x₁ : (fun (X : Type u) ↦ X) X₁),
        (hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) x₁ = x₂ ∧
          (hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) x₁ = x₃
φ : X₁ ⟶ PullbackObj r b :=
  ↾fun (x₁ : X₁) ↦
    Subtype.mk (p := fun (p : X₂ × X₃) ↦
      Eq (α := (fun (X : Type u) ↦ X) X₄)
        ((hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) p.1 :
          (fun (X : Type u) ↦ X) X₄)
        ((hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) p.2 :
          (fun (X : Type u) ↦ X) X₄))
      ((hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) x₁,
        (hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) x₁)
      ⋯
x : PullbackObj r b
⊢ ∃ (a : (fun (X : Type u) ↦ X) X₁),
    (hom (FC := TypeCat.Fun) φ : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) (PullbackObj r b)) a = x
have right : ∀ (a : X₁)
  (ha :
    (hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) a = (↑x : X₂ × X₃).1 ∧
      (hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) a = (↑x : X₂ × X₃).2),
  ∃ (a : (fun (X : Type u) ↦ X) X₁),
    (hom (FC := TypeCat.Fun) φ : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) (PullbackObj r b)) a = x
Tactic: obtain ⟨a, ha⟩ := h₂ x.1.1 x.1.2 (by grind)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pullbacks (hypothesis)
Goal:
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
w : t ≫ r = l ≫ b
h₁ :
  ∀ (x₁ y₁ : (fun (X : Type u) ↦ X) X₁),
    Eq (α := (fun (X : Type u) ↦ X) X₂)
          ((hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) x₁ :
            (fun (X : Type u) ↦ X) X₂)
          ((hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) y₁ :
            (fun (X : Type u) ↦ X) X₂) ∧
        Eq (α := (fun (X : Type u) ↦ X) X₃)
          ((hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) x₁ :
            (fun (X : Type u) ↦ X) X₃)
          ((hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) y₁ :
            (fun (X : Type u) ↦ X) X₃) →
      x₁ = y₁
h₂ :
  ∀ (x₂ : (fun (X : Type u) ↦ X) X₂) (x₃ : (fun (X : Type u) ↦ X) X₃),
    Eq (α := (fun (X : Type u) ↦ X) X₄)
        ((hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) x₂ :
          (fun (X : Type u) ↦ X) X₄)
        ((hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) x₃ :
          (fun (X : Type u) ↦ X) X₄) →
      ∃ (x₁ : (fun (X : Type u) ↦ X) X₁),
        (hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) x₁ = x₂ ∧
          (hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) x₁ = x₃
φ : X₁ ⟶ PullbackObj r b :=
  ↾fun (x₁ : X₁) ↦
    Subtype.mk (p := fun (p : X₂ × X₃) ↦
      Eq (α := (fun (X : Type u) ↦ X) X₄)
        ((hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) p.1 :
          (fun (X : Type u) ↦ X) X₄)
        ((hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) p.2 :
          (fun (X : Type u) ↦ X) X₄))
      ((hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) x₁,
        (hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) x₁)
      ⋯
⊢ IsPullback t l r b
have hφ : IsIso φ
Tactic: have hφ : IsIso φ := by
      rw [isIso_iff_bijective]
      constructor
      · intro _ _ h
        simp [φ] at h
        grind
      · intro x
        obtain ⟨a, ha⟩ := h₂ x.1.1 x.1.2 (by grind)
        cat_disch
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
⊢ f ≫ inl f g = g ≫ inr f g
have h : ∀ (x : S),
  (ConcreteCategory.hom (FC := TypeCat.Fun) (f ≫ inl f g)).toFun x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (g ≫ inr f g)).toFun x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
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
⊢ 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
have 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₂)
                sorry)
          s))
      (Quot.mk (Rel f g) (Sum.inl x₁))
Tactic: ext ⟨x₁ | x₂⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
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₁))
⊢ 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
have 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₂)
                sorry)
          s))
      (Quot.mk (Rel f g) (Sum.inr x₂))
Tactic: ext ⟨x₁ | 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₁ : X₁
⊢ 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₀
have 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₀
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
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₀
⊢ 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₀
have 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₁)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₁ : X₁
x₂ : 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
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
⊢ 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
have 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₂)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₂ y₂ : X₂
⊢ Rel' f g (Sum.inr x₂) (Sum.inr y₂) ↔ x₂ = y₂
have mp : Rel' f g (Sum.inr x₂) (Sum.inr y₂) → x₂ = y₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₂ y₂ : X₂
mp : Rel' f g (Sum.inr x₂) (Sum.inr y₂) → x₂ = y₂
⊢ Rel' f g (Sum.inr x₂) (Sum.inr y₂) ↔ x₂ = y₂
have mpr : x₂ = y₂ → Rel' f g (Sum.inr x₂) (Sum.inr y₂)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
Goal:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x y : X₁ ⊕ X₂
h : Rel' f g x y
⊢ Rel' f g y x
have refl : Rel' f g x x
Tactic: obtain _ | ⟨_, _, h⟩ | _ | _ := h
Cleared hypotheses: y, 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 : X₁ ⊕ X₂
h : Rel' f g x y
refl : Rel' f g x x
⊢ Rel' f g y x
have inl_inl : ∀ (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₁) y₀))
    (Sum.inl
      ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) x₀))
Tactic: obtain _ | ⟨_, _, h⟩ | _ | _ := h
Cleared hypotheses: x, y, 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 : X₁ ⊕ X₂
h : Rel' f g x y
refl : Rel' f g x x
inl_inl :
  ∀ (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₁) y₀))
      (Sum.inl
        ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) x₀))
⊢ Rel' f g y x
have inl_inr : ∀ (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: obtain _ | ⟨_, _, h⟩ | _ | _ := h
Cleared hypotheses: x, y, 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 : X₁ ⊕ X₂
h : Rel' f g x y
refl : Rel' f g x x
inl_inl :
  ∀ (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₁) y₀))
      (Sum.inl
        ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) S) → (fun (X : Type u) ↦ X) X₁) x₀))
inl_inr :
  ∀ (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))
⊢ Rel' f g y x
have inr_inl : ∀ (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: obtain _ | ⟨_, _, h⟩ | _ | _ := h
Cleared hypotheses: x, y, 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
z : X₁ ⊕ 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₂)
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₁) y₀))
    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₁) x₀))
    z
have inl_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₁) y₀))
      (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₁) x₀))
    (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₂
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₂)
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₁) y₀))
    z
inl_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₁)
            y₀))
        (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₁) x₀))
      (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₁) x₀))
    z
have inl_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₁) y₀))
      (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₁) x₀))
    (Sum.inr z₂)
Tactic: obtain z₁ | z₂ := z
Cleared hypotheses: z, hyz