awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
Goal:
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPushout t l r b
x₄ : X₄
inl :
  ∀
    (h₁ :
      ∃ (x₂ : (fun (X : Type u) ↦ X) X₂),
        (ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) x₂ =
          x₄),
    (∃ (x₂ : (fun (X : Type u) ↦ X) X₂),
        (ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) x₂ =
          x₄) ∨
      ∃ (x₃ : (fun (X : Type u) ↦ X) X₃),
        (ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) x₃ =
            x₄ ∧
          x₃ ∉
            Set.range (ι := (fun (X : Type u) ↦ X) X₁)
              (⇑(ConcreteCategory.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₂),
      (ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) x₂ =
        x₄) ∨
    ∃ (x₃ : (fun (X : Type u) ↦ X) X₃),
      (ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) x₃ =
          x₄ ∧
        x₃ ∉
          Set.range (ι := (fun (X : Type u) ↦ X) X₁)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
              (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃)
have inr : ∀ (x₃ : X₃)
  (hx₃ :
    (ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) x₃ = x₄),
  (∃ (x₂ : (fun (X : Type u) ↦ X) X₂),
      (ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) x₂ =
        x₄) ∨
    ∃ (x₃ : (fun (X : Type u) ↦ X) X₃),
      (ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) x₃ =
          x₄ ∧
        x₃ ∉
          Set.range (ι := (fun (X : Type u) ↦ X) X₁)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
              (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃)
Tactic: obtain h₁ | ⟨x₃, hx₃⟩ := eq_or_eq_of_isPushout h x₄
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
Goal:
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPushout t l r b
x₄ : X₄
x₃ : X₃
hx₃ : (ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) x₃ = x₄
⊢ (∃ (x₂ : (fun (X : Type u) ↦ X) X₂),
      (ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) x₂ =
        x₄) ∨
    ∃ (x₃ : (fun (X : Type u) ↦ X) X₃),
      (ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) x₃ =
          x₄ ∧
        x₃ ∉
          Set.range (ι := (fun (X : Type u) ↦ X) X₁)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
              (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃)
have pos : ∀
  (h₂ :
    Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X₃))
      (Set.range (ι := (fun (X : Type u) ↦ X) X₁)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃))
      x₃),
  (∃ (x₂ : (fun (X : Type u) ↦ X) X₂),
      (ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) x₂ =
        x₄) ∨
    ∃ (x₃ : (fun (X : Type u) ↦ X) X₃),
      (ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) x₃ =
          x₄ ∧
        x₃ ∉
          Set.range (ι := (fun (X : Type u) ↦ X) X₁)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
              (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃)
Tactic: by_cases h₂ : x₃ ∈ Set.range l
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
Goal:
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPushout t l r b
x₄ : X₄
x₃ : X₃
hx₃ : (ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) x₃ = x₄
pos :
  ∀
    (h₂ :
      Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X₃))
        (Set.range (ι := (fun (X : Type u) ↦ X) X₁)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃))
        x₃),
    (∃ (x₂ : (fun (X : Type u) ↦ X) X₂),
        (ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) x₂ =
          x₄) ∨
      ∃ (x₃ : (fun (X : Type u) ↦ X) X₃),
        (ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) x₃ =
            x₄ ∧
          x₃ ∉
            Set.range (ι := (fun (X : Type u) ↦ X) X₁)
              (⇑(ConcreteCategory.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₂),
      (ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) x₂ =
        x₄) ∨
    ∃ (x₃ : (fun (X : Type u) ↦ X) X₃),
      (ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) x₃ =
          x₄ ∧
        x₃ ∉
          Set.range (ι := (fun (X : Type u) ↦ X) X₁)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
              (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃)
have neg : ∀
  (h₂ :
    x₃ ∉
      Set.range (ι := (fun (X : Type u) ↦ X) X₁)
        (⇑(ConcreteCategory.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₂),
      (ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) x₂ =
        x₄) ∨
    ∃ (x₃ : (fun (X : Type u) ↦ X) X₃),
      (ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) x₃ =
          x₄ ∧
        x₃ ∉
          Set.range (ι := (fun (X : Type u) ↦ X) X₁)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
              (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃)
Tactic: by_cases h₂ : x₃ ∈ Set.range l
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
Goal:
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPushout t l r b
x₄ : X₄
x₃ : X₃
hx₃ : (ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) x₃ = x₄
h₂ :
  Membership.mem (γ := Set ((fun (X : Type u) ↦ X) X₃))
    (Set.range (ι := (fun (X : Type u) ↦ X) X₁)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃))
    x₃
⊢ (∃ (x₂ : (fun (X : Type u) ↦ X) X₂),
      (ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) x₂ =
        x₄) ∨
    ∃ (x₃ : (fun (X : Type u) ↦ X) X₃),
      (ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) x₃ =
          x₄ ∧
        x₃ ∉
          Set.range (ι := (fun (X : Type u) ↦ X) X₁)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
              (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃)
have pos : ∀ (x₁ : X₁)
  (hx₃ :
    (ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄)
        ((ConcreteCategory.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₃) =
      x₄),
  (∃ (x₂ : (fun (X : Type u) ↦ X) X₂),
      (ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) x₂ =
        x₄) ∨
    ∃ (x₃ : (fun (X : Type u) ↦ X) X₃),
      (ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) x₃ =
          x₄ ∧
        x₃ ∉
          Set.range (ι := (fun (X : Type u) ↦ X) X₁)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
              (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃)
Tactic: obtain ⟨x₁, rfl⟩ := h₂
Cleared hypotheses: x₃, hx₃, h₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
Goal:
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPushout t l r b
ht :
  Function.Injective (α := (fun (X : Type u) ↦ X) X₁) (β := (fun (X : Type u) ↦ X) X₂)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) t) : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂)
⊢ IsPullback t l r b
have rw : t ≫ r = l ≫ b ∧
  (∀ (x₁ y₁ : (fun (X : Type u) ↦ X) X₁),
      Eq (α := (fun (X : Type u) ↦ X) X₂)
            ((ConcreteCategory.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₂)
            ((ConcreteCategory.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₃)
            ((ConcreteCategory.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₃)
            ((ConcreteCategory.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₁) ∧
    ∀ (x₂ : (fun (X : Type u) ↦ X) X₂) (x₃ : (fun (X : Type u) ↦ X) X₃),
      Eq (α := (fun (X : Type u) ↦ X) X₄)
          ((ConcreteCategory.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₄)
          ((ConcreteCategory.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₁),
          (ConcreteCategory.hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂)
                x₁ =
              x₂ ∧
            (ConcreteCategory.hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃)
                x₁ =
              x₃
Tactic: rw [isPullback_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
Goal:
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPushout t l r b
ht :
  Function.Injective (α := (fun (X : Type u) ↦ X) X₁) (β := (fun (X : Type u) ↦ X) X₂)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) t) : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂)
⊢ t ≫ r = l ≫ b ∧
    (∀ (x₁ y₁ : (fun (X : Type u) ↦ X) X₁),
        Eq (α := (fun (X : Type u) ↦ X) X₂)
              ((ConcreteCategory.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₂)
              ((ConcreteCategory.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₃)
              ((ConcreteCategory.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₃)
              ((ConcreteCategory.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₁) ∧
      ∀ (x₂ : (fun (X : Type u) ↦ X) X₂) (x₃ : (fun (X : Type u) ↦ X) X₃),
        Eq (α := (fun (X : Type u) ↦ X) X₄)
            ((ConcreteCategory.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₄)
            ((ConcreteCategory.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₁),
            (ConcreteCategory.hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂)
                  x₁ =
                x₂ ∧
              (ConcreteCategory.hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃)
                  x₁ =
                x₃
have refine : ∀ (x₂ : (fun (X : Type u) ↦ X) X₂) (x₃ : (fun (X : Type u) ↦ X) X₃)
  (hx :
    Eq (α := (fun (X : Type u) ↦ X) X₄)
      ((ConcreteCategory.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₄)
      ((ConcreteCategory.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₁),
    (ConcreteCategory.hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) x₁ = x₂ ∧
      (ConcreteCategory.hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) x₁ = x₃
Tactic: refine ⟨h.w, fun x₁ y₁ ⟨h₂, _⟩ ↦ ht h₂, fun x₂ x₃ hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (hypothesis)
Goal:
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
hr' : Mono r'
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉
        Set.range (ι := (fun (X : Type u) ↦ X) X₁)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
            (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
      y₃ ∉
          Set.range (ι := (fun (X : Type u) ↦ X) X₁)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
              (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
        Eq (α := (fun (X : Type u) ↦ X) X₅)
            ((ConcreteCategory.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₅)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) b' : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₅)
                y₃ :
              (fun (X : Type u) ↦ X) X₅) →
          x₃ = y₃
⊢ Mono k
have hr'₁ : Mono (r ≫ k)
Tactic: subst facr facb
Cleared hypotheses: r', b', h₂, facr, facb, hr', H
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (hypothesis)
Goal:
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
hr' : Mono r'
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉
        Set.range (ι := (fun (X : Type u) ↦ X) X₁)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
            (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
      y₃ ∉
          Set.range (ι := (fun (X : Type u) ↦ X) X₁)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
              (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
        Eq (α := (fun (X : Type u) ↦ X) X₅)
            ((ConcreteCategory.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₅)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) b' : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₅)
                y₃ :
              (fun (X : Type u) ↦ X) X₅) →
          x₃ = y₃
hr'₁ : Mono (r ≫ k)
⊢ Mono k
have H₁ : ∀ (x₃ y₃ : X₃),
  x₃ ∉
      Set.range (ι := (fun (X : Type u) ↦ X) X₁)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
    y₃ ∉
        Set.range (ι := (fun (X : Type u) ↦ X) X₁)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
            (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
      Eq (α := (fun (X : Type u) ↦ X) X₅)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (b ≫ k) :
                (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₅)
              x₃ :
            (fun (X : Type u) ↦ X) X₅)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (b ≫ k) :
                (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₅)
              y₃ :
            (fun (X : Type u) ↦ X) X₅) →
        x₃ = y₃
Tactic: subst facr facb
Cleared hypotheses: r', b', h₂, facr, facb, hr', H
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (hypothesis)
Goal:
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
r' : X₂ ⟶ X₅
b' : X₃ ⟶ X₅
h₂ : IsPullback t l r' b'
facr : r ≫ k = r'
facb : b ≫ k = b'
hr' : Mono r'
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉
        Set.range (ι := (fun (X : Type u) ↦ X) X₁)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
            (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
      y₃ ∉
          Set.range (ι := (fun (X : Type u) ↦ X) X₁)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
              (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
        Eq (α := (fun (X : Type u) ↦ X) X₅)
            ((ConcreteCategory.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₅)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) b' : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₅)
                y₃ :
              (fun (X : Type u) ↦ X) X₅) →
          x₃ = y₃
hr'₁ : Mono (r ≫ k)
H₁ :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉
        Set.range (ι := (fun (X : Type u) ↦ X) X₁)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
            (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
      y₃ ∉
          Set.range (ι := (fun (X : Type u) ↦ X) X₁)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
              (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
        Eq (α := (fun (X : Type u) ↦ X) X₅)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (b ≫ k) :
                  (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₅)
                x₃ :
              (fun (X : Type u) ↦ X) X₅)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (b ≫ k) :
                  (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₅)
                y₃ :
              (fun (X : Type u) ↦ X) X₅) →
          x₃ = y₃
⊢ Mono k
have h₃ : IsPullback t l (r ≫ k) (b ≫ k)
Tactic: subst facr facb
Cleared hypotheses: r', b', h₂, facr, facb, hr', H
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (hypothesis)
Goal:
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Mono (r ≫ k)
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉
        Set.range (ι := (fun (X : Type u) ↦ X) X₁)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
            (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
      y₃ ∉
          Set.range (ι := (fun (X : Type u) ↦ X) X₁)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
              (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
        Eq (α := (fun (X : Type u) ↦ X) X₅)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (b ≫ k) :
                  (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₅)
                x₃ :
              (fun (X : Type u) ↦ X) X₅)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (b ≫ k) :
                  (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₅)
                y₃ :
              (fun (X : Type u) ↦ X) X₅) →
          x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
⊢ Mono k
have this : Function.Injective (α := (fun (X : Type u) ↦ X) X₁) (β := (fun (X : Type u) ↦ X) X₃)
  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃)
Tactic: have : Function.Injective l :=
    fun x₁ y₁ h ↦ ext_of_isPullback h₂ ((mono_iff_injective _).1 hr'
      ((ConcreteCategory.congr_hom h₂.w x₁).trans (Eq.trans (by simp [h])
      (ConcreteCategory.congr_hom h₂.w.symm y₁)))) h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
Goal:
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Mono (r ≫ k)
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉
        Set.range (ι := (fun (X : Type u) ↦ X) X₁)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
            (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
      y₃ ∉
          Set.range (ι := (fun (X : Type u) ↦ X) X₁)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
              (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
        Eq (α := (fun (X : Type u) ↦ X) X₅)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (b ≫ k) :
                  (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₅)
                x₃ :
              (fun (X : Type u) ↦ X) X₅)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (b ≫ k) :
                  (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₅)
                y₃ :
              (fun (X : Type u) ↦ X) X₅) →
          x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this :
  Function.Injective (α := (fun (X : Type u) ↦ X) X₁) (β := (fun (X : Type u) ↦ X) X₃)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃)
⊢ Mono k
have rw : ∀
  (hr' :
    Function.Injective (α := (fun (X : Type u) ↦ X) X₂) (β := (fun (X : Type u) ↦ X) X₅)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (r ≫ k)) :
        (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₅))
  (H :
    ∀ (x₃ y₃ : X₃),
      x₃ ∉
          Set.range (ι := (fun (X : Type u) ↦ X) X₁)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
              (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
        y₃ ∉
            Set.range (ι := (fun (X : Type u) ↦ X) X₁)
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
                (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
          Eq (α := (fun (X : Type u) ↦ X) X₅)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (b ≫ k) :
                    (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₅)
                  x₃ :
                (fun (X : Type u) ↦ X) X₅)
              ((ConcreteCategory.hom (FC := TypeCat.Fun) (b ≫ k) :
                    (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₅)
                  y₃ :
                (fun (X : Type u) ↦ X) X₅) →
            x₃ = y₃)
  (h₂ : IsPullback t l (r ≫ k) (b ≫ k))
  (this :
    Function.Injective (α := (fun (X : Type u) ↦ X) X₁) (β := (fun (X : Type u) ↦ X) X₃)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃)),
  Function.Injective (α := (fun (X : Type u) ↦ X) X₄) (β := (fun (X : Type u) ↦ X) X₅)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) k) : (a : (fun (X : Type u) ↦ X) X₄) → (fun (X : Type u) ↦ X) X₅)
Tactic: rw [mono_iff_injective] at hr' ⊢
Cleared hypotheses: hr', H, h₂, this