awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Category.FinBoolAlg (goal)
Goal:
α β : FinBoolAlg
e : (↑α.toBoolAlg : Type u) ≃o (↑β.toBoolAlg : Type u)
⊢ CategoryStruct.comp (Y := α)
      (InducedCategory.homMk
        (BoolAlg.ofHom
          (let __src : LatticeHom (↑β.1 : Type u) (↑α.1 : Type u) :=
            { toFun := (⇑e.symm : (a : (↑β.1 : Type u)) → (↑α.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯ };
          { toFun := (⇑e.symm : (a : (↑β.1 : Type u)) → (↑α.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯,
            map_bot' := ⋯ })))
      (InducedCategory.homMk
        (BoolAlg.ofHom
          (let __src : LatticeHom (↑α.1 : Type u) (↑β.1 : Type u) :=
            { toFun := (⇑e : (a : (↑α.1 : Type u)) → (↑β.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯ };
          { toFun := (⇑e : (a : (↑α.1 : Type u)) → (↑β.1 : Type u)), map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯,
            map_bot' := ⋯ }))) =
    𝟙 β
have h : ∀ (a : (↑β.toBoolAlg : Type u)),
  Eq (α := (↑β.toBoolAlg : Type u))
    ((@ConcreteCategory.hom FinBoolAlg largeCategory
            (fun (x1 x2 : FinBoolAlg.{u}) ↦ BoundedLatticeHom (↑x1.toBoolAlg : Type u) (↑x2.toBoolAlg : Type u))
            (fun (X : FinBoolAlg.{u}) ↦ (↑X.toBoolAlg : Type u)) _ _ β β
            (CategoryStruct.comp (Y := α)
              (InducedCategory.homMk
                (BoolAlg.ofHom
                  (let __src : LatticeHom (↑β.1 : Type u) (↑α.1 : Type u) :=
                    { toFun := (⇑e.symm : (a : (↑β.1 : Type u)) → (↑α.1 : Type u)), map_sup' := sorry, map_inf' := sorry };
                  { toFun := (⇑e.symm : (a : (↑β.1 : Type u)) → (↑α.1 : Type u)), map_sup' := sorry, map_inf' := sorry,
                    map_top' := sorry, map_bot' := sorry })))
              (InducedCategory.homMk
                (BoolAlg.ofHom
                  (let __src : LatticeHom (↑α.1 : Type u) (↑β.1 : Type u) :=
                    { toFun := (⇑e : (a : (↑α.1 : Type u)) → (↑β.1 : Type u)), map_sup' := sorry, map_inf' := sorry };
                  { toFun := (⇑e : (a : (↑α.1 : Type u)) → (↑β.1 : Type u)), map_sup' := sorry, map_inf' := sorry,
                    map_top' := sorry, map_bot' := sorry })))) :
          (a : (↑β.toBoolAlg : Type u)) → (↑β.toBoolAlg : Type u))
        a :
      (↑β.toBoolAlg : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : FinBoolAlg.{u}) ↦
            BoundedLatticeHom (↑x1.toBoolAlg : Type u) (↑x2.toBoolAlg : Type u)) (CC := fun (X : FinBoolAlg.{u}) ↦
            (↑X.toBoolAlg : Type u)) (𝟙 β) :
          (a : (↑β.toBoolAlg : Type u)) → (↑β.toBoolAlg : Type u))
        a :
      (↑β.toBoolAlg : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Category.HeytAlg (goal)
Goal:
α β : HeytAlg
e : (↑α : Type u) ≃o (↑β : Type u)
⊢ CategoryStruct.comp (Y := β)
      (ofHom
        { toFun := (⇑e : (a : (↑α : Type u)) → (↑β : Type u)), map_sup' := ⋯, map_inf' := ⋯, map_bot' := ⋯,
          map_himp' := ⋯ })
      (ofHom
        { toFun := (⇑e.symm : (a : (↑β : Type u)) → (↑α : Type u)), map_sup' := ⋯, map_inf' := ⋯, map_bot' := ⋯,
          map_himp' := ⋯ }) =
    𝟙 α
have hf : ∀ (a : (↑α : Type u)),
  Eq (α := (↑α : Type u))
    ((Hom.hom
            (CategoryStruct.comp (Y := β)
              (ofHom
                { toFun := (⇑e : (a : (↑α : Type u)) → (↑β : Type u)), map_sup' := sorry, map_inf' := sorry, map_bot' := sorry,
                  map_himp' := sorry })
              (ofHom
                { toFun := (⇑e.symm : (a : (↑β : Type u)) → (↑α : Type u)), map_sup' := sorry, map_inf' := sorry, map_bot' := sorry,
                  map_himp' := sorry })) :
          (a : (↑α : Type u)) → (↑α : Type u))
        a :
      (↑α : Type u))
    ((Hom.hom (𝟙 α) : (a : (↑α : Type u)) → (↑α : Type u)) a : (↑α : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Category.HeytAlg (goal)
Goal:
α β : HeytAlg
e : (↑α : Type u) ≃o (↑β : Type u)
⊢ CategoryStruct.comp (Y := α)
      (ofHom
        { toFun := (⇑e.symm : (a : (↑β : Type u)) → (↑α : Type u)), map_sup' := ⋯, map_inf' := ⋯, map_bot' := ⋯,
          map_himp' := ⋯ })
      (ofHom
        { toFun := (⇑e : (a : (↑α : Type u)) → (↑β : Type u)), map_sup' := ⋯, map_inf' := ⋯, map_bot' := ⋯,
          map_himp' := ⋯ }) =
    𝟙 β
have hf : ∀ (a : (↑β : Type u)),
  Eq (α := (↑β : Type u))
    ((Hom.hom
            (CategoryStruct.comp (Y := α)
              (ofHom
                { toFun := (⇑e.symm : (a : (↑β : Type u)) → (↑α : Type u)), map_sup' := sorry, map_inf' := sorry, map_bot' := sorry,
                  map_himp' := sorry })
              (ofHom
                { toFun := (⇑e : (a : (↑α : Type u)) → (↑β : Type u)), map_sup' := sorry, map_inf' := sorry, map_bot' := sorry,
                  map_himp' := sorry })) :
          (a : (↑β : Type u)) → (↑β : Type u))
        a :
      (↑β : Type u))
    ((Hom.hom (𝟙 β) : (a : (↑β : Type u)) → (↑β : Type u)) a : (↑β : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (goal)
Goal:
A B : NonemptyFinLinOrd
f : A ⟶ B
⊢ Mono f ↔
    Function.Injective (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) A) (β :=
      (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) B)
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
            (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
            (↑X.toLinOrd : Type u)) f) :
        (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) A) →
          (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) B)
have refine : Mono f →
  Function.Injective (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) A) (β :=
    (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) B)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
          (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
          (↑X.toLinOrd : Type u)) f) :
      (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) A) →
        (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) B)
Tactic: refine ⟨?_, ConcreteCategory.mono_of_injective f⟩
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (goal)
Goal:
A B : NonemptyFinLinOrd
f : A ⟶ B
h_1 : Mono f
a₁ a₂ : (↑A.toLinOrd : Type u)
h :
  Eq (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) B)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
            (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
            (↑X.toLinOrd : Type u)) f :
          (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) A) →
            (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) B)
        a₁ :
      (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) B)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
            (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
            (↑X.toLinOrd : Type u)) f :
          (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) A) →
            (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) B)
        a₂ :
      (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) B)
X : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 1))
g₁ : X ⟶ A := ofHom { toFun := fun (x : ULift.{u, 0} (Fin 1)) ↦ a₁, monotone' := ⋯ }
g₂ : X ⟶ A := ofHom { toFun := fun (x : ULift.{u, 0} (Fin 1)) ↦ a₂, monotone' := ⋯ }
⊢ a₁ = a₂
have change : Eq (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) A)
  ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
          (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
          (↑X.toLinOrd : Type u)) g₁ :
        (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
          (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) A)
      { down := 0 } :
    (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) A)
  ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
          (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
          (↑X.toLinOrd : Type u)) g₂ :
        (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
          (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) A)
      { down := 0 } :
    (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) A)
Tactic: change g₁ (ULift.up (0 : Fin 1)) = g₂ (ULift.up (0 : Fin 1))
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (goal)
Goal:
A B : NonemptyFinLinOrd
f : A ⟶ B
h_1 : Mono f
a₁ a₂ : (↑A.toLinOrd : Type u)
h :
  Eq (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) B)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
            (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
            (↑X.toLinOrd : Type u)) f :
          (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) A) →
            (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) B)
        a₁ :
      (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) B)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
            (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
            (↑X.toLinOrd : Type u)) f :
          (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) A) →
            (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) B)
        a₂ :
      (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) B)
X : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 1))
g₁ : X ⟶ A := ofHom { toFun := fun (x : ULift.{u, 0} (Fin 1)) ↦ a₁, monotone' := ⋯ }
g₂ : X ⟶ A := ofHom { toFun := fun (x : ULift.{u, 0} (Fin 1)) ↦ a₂, monotone' := ⋯ }
⊢ g₁ ≫ f = g₂ ≫ f
have hf : ∀ (x : (↑X.toLinOrd : Type u)),
  Eq (α := (↑B.toLinOrd : Type u))
    ((LinOrd.Hom.hom (g₁ ≫ f).hom : (a : (↑X.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) x : (↑B.toLinOrd : Type u))
    ((LinOrd.Hom.hom (g₂ ≫ f).hom : (a : (↑X.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) x : (↑B.toLinOrd : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (hypothesis)
Goal:
A B : NonemptyFinLinOrd
f : A ⟶ B
h_1 : Mono f
a₁ a₂ : (↑A.toLinOrd : Type u)
h :
  Eq (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) B)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
            (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
            (↑X.toLinOrd : Type u)) f :
          (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) A) →
            (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) B)
        a₁ :
      (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) B)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
            (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
            (↑X.toLinOrd : Type u)) f :
          (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) A) →
            (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) B)
        a₂ :
      (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) B)
X : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 1))
g₁ : X ⟶ A := ofHom { toFun := fun (x : ULift.{u, 0} (Fin 1)) ↦ a₁, monotone' := ⋯ }
g₂ : X ⟶ A := ofHom { toFun := fun (x : ULift.{u, 0} (Fin 1)) ↦ a₂, monotone' := ⋯ }
⊢ Eq (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) A)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
            (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
            (↑X.toLinOrd : Type u)) g₁ :
          (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
            (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) A)
        { down := 0 } :
      (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) A)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
            (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
            (↑X.toLinOrd : Type u)) g₂ :
          (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
            (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) A)
        { down := 0 } :
      (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) A)
have eq : g₁ ≫ f = g₂ ≫ f
Tactic: have eq : g₁ ≫ f = g₂ ≫ f := by
    ext
    exact h
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (hypothesis)
Goal:
A B : NonemptyFinLinOrd
f : A ⟶ B
h_1 : Mono f
a₁ a₂ : (↑A.toLinOrd : Type u)
h :
  Eq (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) B)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
            (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
            (↑X.toLinOrd : Type u)) f :
          (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) A) →
            (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) B)
        a₁ :
      (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) B)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
            (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
            (↑X.toLinOrd : Type u)) f :
          (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) A) →
            (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) B)
        a₂ :
      (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) B)
X : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 1))
g₁ : X ⟶ A := ofHom { toFun := fun (x : ULift.{u, 0} (Fin 1)) ↦ a₁, monotone' := ⋯ }
g₂ : X ⟶ A := ofHom { toFun := fun (x : ULift.{u, 0} (Fin 1)) ↦ a₂, monotone' := ⋯ }
eq : g₁ ≫ f = g₂ ≫ f
⊢ Eq (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) A)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
            (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
            (↑X.toLinOrd : Type u)) g₁ :
          (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
            (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) A)
        { down := 0 } :
      (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) A)
    ((ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
            (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
            (↑X.toLinOrd : Type u)) g₂ :
          (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) X) →
            (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) A)
        { down := 0 } :
      (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) A)
have eq₁ : g₁ = g₂
Tactic: rw [cancel_mono] at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (goal)
Goal:
A B : NonemptyFinLinOrd
f : A ⟶ B
⊢ Epi f ↔
    Function.Surjective (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) A) (β :=
      (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) B)
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
            (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
            (↑X.toLinOrd : Type u)) f) :
        (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) A) →
          (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) B)
have mp : Epi f →
  Function.Surjective (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) A) (β :=
    (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) B)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
          (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
          (↑X.toLinOrd : Type u)) f) :
      (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) A) →
        (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) B)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (goal)
Goal:
A B : NonemptyFinLinOrd
f : A ⟶ B
mp :
  Epi f →
    Function.Surjective (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) A) (β :=
      (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) B)
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
            (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
            (↑X.toLinOrd : Type u)) f) :
        (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) A) →
          (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) B)
⊢ Epi f ↔
    Function.Surjective (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) A) (β :=
      (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) B)
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
            (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
            (↑X.toLinOrd : Type u)) f) :
        (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) A) →
          (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) B)
have mpr : Function.Surjective (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) A) (β :=
    (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) B)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
          (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
          (↑X.toLinOrd : Type u)) f) :
      (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) A) →
        (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) B) →
  Epi f
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (goal)
Goal:
A B : NonemptyFinLinOrd
f : A ⟶ B
h : Epi f
⊢ ∀ (b : (↑B.toLinOrd : Type u)),
    ∃ (a : (↑A.toLinOrd : Type u)),
      (ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
              (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
              (↑X.toLinOrd : Type u)) f :
            (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u))
          a =
        b
have mp : ∀ (m : (↑B.toLinOrd : Type u))
  (hm :
    ∀ (a : (↑A.toLinOrd : Type u)),
      (ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
              (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
              (↑X.toLinOrd : Type u)) f :
            (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u))
          a ≠
        m),
  False
Tactic: by_contra! ⟨m, hm⟩
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (goal)
Goal:
A B : NonemptyFinLinOrd
f : A ⟶ B
h_1 : Epi f
m : (↑B.toLinOrd : Type u)
hm :
  ∀ (a : (↑A.toLinOrd : Type u)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
            (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
            (↑X.toLinOrd : Type u)) f :
          (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u))
        a ≠
      m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
x₁ x₂ : (↑B.1 : Type u)
h : x₁ ≤ x₂
⊢ LE.le.{u} (α := ULift.{u, 0} (Fin 2)) (if x₁ < m then { down := 0 } else { down := 1 })
    (if x₂ < m then { down := 0 } else { down := 1 })
have pos : ∀ (h₁ : x₁ < m) (h₂ : x₂ < m), LE.le.{u} (α := ULift.{u, 0} (Fin 2)) { down := 0 } { down := 0 }
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (goal)
Goal:
A B : NonemptyFinLinOrd
f : A ⟶ B
h_1 : Epi f
m : (↑B.toLinOrd : Type u)
hm :
  ∀ (a : (↑A.toLinOrd : Type u)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
            (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
            (↑X.toLinOrd : Type u)) f :
          (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u))
        a ≠
      m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
x₁ x₂ : (↑B.1 : Type u)
h : x₁ ≤ x₂
pos : ∀ (h₁ : x₁ < m) (h₂ : x₂ < m), LE.le.{u} (α := ULift.{u, 0} (Fin 2)) { down := 0 } { down := 0 }
⊢ LE.le.{u} (α := ULift.{u, 0} (Fin 2)) (if x₁ < m then { down := 0 } else { down := 1 })
    (if x₂ < m then { down := 0 } else { down := 1 })
have neg : ∀ (h₁ : x₁ < m) (h₂ : ¬x₂ < m), LE.le.{u} (α := ULift.{u, 0} (Fin 2)) { down := 0 } { down := 1 }
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (goal)
Goal:
A B : NonemptyFinLinOrd
f : A ⟶ B
h_1 : Epi f
m : (↑B.toLinOrd : Type u)
hm :
  ∀ (a : (↑A.toLinOrd : Type u)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
            (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
            (↑X.toLinOrd : Type u)) f :
          (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u))
        a ≠
      m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
x₁ x₂ : (↑B.1 : Type u)
h : x₁ ≤ x₂
pos : ∀ (h₁ : x₁ < m) (h₂ : x₂ < m), LE.le.{u} (α := ULift.{u, 0} (Fin 2)) { down := 0 } { down := 0 }
neg : ∀ (h₁ : x₁ < m) (h₂ : ¬x₂ < m), LE.le.{u} (α := ULift.{u, 0} (Fin 2)) { down := 0 } { down := 1 }
⊢ LE.le.{u} (α := ULift.{u, 0} (Fin 2)) (if x₁ < m then { down := 0 } else { down := 1 })
    (if x₂ < m then { down := 0 } else { down := 1 })
have pos₁ : ∀ (h₁ : ¬x₁ < m) (h₂ : x₂ < m), LE.le.{u} (α := ULift.{u, 0} (Fin 2)) { down := 1 } { down := 0 }
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (goal)
Goal:
A B : NonemptyFinLinOrd
f : A ⟶ B
h_1 : Epi f
m : (↑B.toLinOrd : Type u)
hm :
  ∀ (a : (↑A.toLinOrd : Type u)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
            (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
            (↑X.toLinOrd : Type u)) f :
          (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u))
        a ≠
      m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
x₁ x₂ : (↑B.1 : Type u)
h : x₁ ≤ x₂
pos : ∀ (h₁ : x₁ < m) (h₂ : x₂ < m), LE.le.{u} (α := ULift.{u, 0} (Fin 2)) { down := 0 } { down := 0 }
neg : ∀ (h₁ : x₁ < m) (h₂ : ¬x₂ < m), LE.le.{u} (α := ULift.{u, 0} (Fin 2)) { down := 0 } { down := 1 }
pos₁ : ∀ (h₁ : ¬x₁ < m) (h₂ : x₂ < m), LE.le.{u} (α := ULift.{u, 0} (Fin 2)) { down := 1 } { down := 0 }
⊢ LE.le.{u} (α := ULift.{u, 0} (Fin 2)) (if x₁ < m then { down := 0 } else { down := 1 })
    (if x₂ < m then { down := 0 } else { down := 1 })
have neg₁ : ∀ (h₁ : ¬x₁ < m) (h₂ : ¬x₂ < m), LE.le.{u} (α := ULift.{u, 0} (Fin 2)) { down := 1 } { down := 1 }
Tactic: split_ifs with h₁ h₂ h₂
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (goal)
Goal:
A B : NonemptyFinLinOrd
f : A ⟶ B
h_1 : Epi f
m : (↑B.toLinOrd : Type u)
hm :
  ∀ (a : (↑A.toLinOrd : Type u)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : NonemptyFinLinOrd.{u}) ↦
            (↑x1.toLinOrd : Type u) →o (↑x2.toLinOrd : Type u)) (CC := fun (X : NonemptyFinLinOrd.{u}) ↦
            (↑X.toLinOrd : Type u)) f :
          (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u))
        a ≠
      m
Y : NonemptyFinLinOrd := of (ULift.{u, 0} (Fin 2))
x₁ x₂ : (↑B.1 : Type u)
h : x₁ ≤ x₂
h₁ : ¬x₁ < m
h₂ : x₂ < m
⊢ LE.le.{u} (α := ULift.{u, 0} (Fin 2)) { down := 1 } { down := 0 }
have pos : False
Tactic: exfalso