awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
p₁ : B ⟶ Y :=
  ofHom { toFun := fun (b : (↑B.1 : Type u)) ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
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))
p₁ : B ⟶ Y :=
  ofHom { toFun := fun (b : (↑B.1 : Type u)) ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
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))
p₁ : B ⟶ Y :=
  ofHom { toFun := fun (b : (↑B.1 : Type u)) ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
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))
p₁ : B ⟶ Y :=
  ofHom { toFun := fun (b : (↑B.1 : Type u)) ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
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))
p₁ : B ⟶ Y :=
  ofHom { toFun := fun (b : (↑B.1 : Type u)) ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
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
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (goal)
Goal:
A B : NonemptyFinLinOrd
f : A ⟶ B
h : 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))
p₁ : B ⟶ Y :=
  ofHom { toFun := fun (b : (↑B.1 : Type u)) ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
p₂ : B ⟶ Y :=
  ofHom { toFun := fun (b : (↑B.1 : Type u)) ↦ if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
⊢ Eq (α := (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) Y)
    ((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)) p₁ :
          (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) B) →
            (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
        m :
      (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) Y)
    ((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)) p₂ :
          (a : (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) B) →
            (fun (X : NonemptyFinLinOrd) ↦ (↑X.toLinOrd : Type u)) Y)
        m :
      (fun (X : NonemptyFinLinOrd.{u}) ↦ (↑X.toLinOrd : Type u)) Y)
have e_a : p₁ = p₂
Tactic: congr
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (goal)
Goal:
A B : NonemptyFinLinOrd
f : A ⟶ B
h : 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))
p₁ : B ⟶ Y :=
  ofHom { toFun := fun (b : (↑B.1 : Type u)) ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
p₂ : B ⟶ Y :=
  ofHom { toFun := fun (b : (↑B.1 : Type u)) ↦ if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
⊢ p₁ = p₂
have e_a : f ≫ p₁ = f ≫ p₂
Tactic: rw [← cancel_epi f]
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (goal)
Goal:
A B : NonemptyFinLinOrd
f : A ⟶ B
h : 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))
p₁ : B ⟶ Y :=
  ofHom { toFun := fun (b : (↑B.1 : Type u)) ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
p₂ : B ⟶ Y :=
  ofHom { toFun := fun (b : (↑B.1 : Type u)) ↦ if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
⊢ f ≫ p₁ = f ≫ p₂
have e_a : ∀ (a : (↑A.toLinOrd : Type u)),
  Eq (α := (↑Y.toLinOrd : Type u))
    ((LinOrd.Hom.hom (f ≫ p₁).hom : (a : (↑A.toLinOrd : Type u)) → (↑Y.toLinOrd : Type u)) a : (↑Y.toLinOrd : Type u))
    ((LinOrd.Hom.hom (f ≫ p₂).hom : (a : (↑A.toLinOrd : Type u)) → (↑Y.toLinOrd : Type u)) a : (↑Y.toLinOrd : Type u))
Tactic: ext a : 3
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (goal)
Goal:
A B : NonemptyFinLinOrd
f : A ⟶ B
h : 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))
p₁ : B ⟶ Y :=
  ofHom { toFun := fun (b : (↑B.1 : Type u)) ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
p₂ : B ⟶ Y :=
  ofHom { toFun := fun (b : (↑B.1 : Type u)) ↦ if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
a : (↑A.toLinOrd : Type u)
⊢ Eq (α := (↑Y.toLinOrd : Type u))
    ((LinOrd.Hom.hom (f ≫ p₁).hom : (a : (↑A.toLinOrd : Type u)) → (↑Y.toLinOrd : Type u)) a : (↑Y.toLinOrd : Type u))
    ((LinOrd.Hom.hom (f ≫ p₂).hom : (a : (↑A.toLinOrd : Type u)) → (↑Y.toLinOrd : Type u)) a : (↑Y.toLinOrd : Type u))
have e_a : Eq (α := (↑Y.toLinOrd : Type u))
  ((LinOrd.Hom.hom
          (InducedCategory.Hom.hom
            (ofHom
              { toFun := fun (b : (↑B.1 : Type u)) ↦ if b < m then { down := 0 } else { down := 1 },
                monotone' := sorry })) :
        (a : (↑B.toLinOrd : Type u)) → (↑Y.toLinOrd : Type u))
      ((LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a : (↑B.toLinOrd : Type u)) :
    (↑Y.toLinOrd : Type u))
  ((LinOrd.Hom.hom
          (InducedCategory.Hom.hom
            (ofHom
              { toFun := fun (b : (↑B.1 : Type u)) ↦ if b ≤ m then { down := 0 } else { down := 1 },
                monotone' := sorry })) :
        (a : (↑B.toLinOrd : Type u)) → (↑Y.toLinOrd : Type u))
      ((LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a : (↑B.toLinOrd : Type u)) :
    (↑Y.toLinOrd : Type u))
Tactic: simp only [p₁, p₂, hom_hom_comp, OrderHom.comp_coe, Function.comp_apply]
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (goal)
Goal:
A B : NonemptyFinLinOrd
f : A ⟶ B
h : 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))
p₁ : B ⟶ Y :=
  ofHom { toFun := fun (b : (↑B.1 : Type u)) ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
p₂ : B ⟶ Y :=
  ofHom { toFun := fun (b : (↑B.1 : Type u)) ↦ if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
a : (↑A.toLinOrd : Type u)
⊢ Eq (α := (↑Y.toLinOrd : Type u))
    ((LinOrd.Hom.hom
            (InducedCategory.Hom.hom
              (ofHom
                { toFun := fun (b : (↑B.1 : Type u)) ↦ if b < m then { down := 0 } else { down := 1 },
                  monotone' := ⋯ })) :
          (a : (↑B.toLinOrd : Type u)) → (↑Y.toLinOrd : Type u))
        ((LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a : (↑B.toLinOrd : Type u)) :
      (↑Y.toLinOrd : Type u))
    ((LinOrd.Hom.hom
            (InducedCategory.Hom.hom
              (ofHom
                { toFun := fun (b : (↑B.1 : Type u)) ↦ if b ≤ m then { down := 0 } else { down := 1 },
                  monotone' := ⋯ })) :
          (a : (↑B.toLinOrd : Type u)) → (↑Y.toLinOrd : Type u))
        ((LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a : (↑B.toLinOrd : Type u)) :
      (↑Y.toLinOrd : Type u))
have e_a : Eq.{u + 1} (α := (↑Y.toLinOrd : Type u))
  (if (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a < m then { down := 0 }
  else { down := 1 })
  (if (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a ≤ m then { down := 0 }
  else { down := 1 })
Tactic: change ite _ _ _ = ite _ _ _
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (goal)
Goal:
A B : NonemptyFinLinOrd
f : A ⟶ B
h : 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))
p₁ : B ⟶ Y :=
  ofHom { toFun := fun (b : (↑B.1 : Type u)) ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
p₂ : B ⟶ Y :=
  ofHom { toFun := fun (b : (↑B.1 : Type u)) ↦ if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
a : (↑A.toLinOrd : Type u)
⊢ Eq.{u + 1} (α := (↑Y.toLinOrd : Type u))
    (if (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a < m then { down := 0 }
    else { down := 1 })
    (if (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a ≤ m then { down := 0 }
    else { down := 1 })
have pos : ∀ (h₁ : (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a < m)
  (h₂ : (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a ≤ m),
  Eq.{u + 1} (α := (↑Y.toLinOrd : Type u)) { 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 : 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))
p₁ : B ⟶ Y :=
  ofHom { toFun := fun (b : (↑B.1 : Type u)) ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
p₂ : B ⟶ Y :=
  ofHom { toFun := fun (b : (↑B.1 : Type u)) ↦ if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
a : (↑A.toLinOrd : Type u)
pos :
  ∀ (h₁ : (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a < m)
    (h₂ : (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a ≤ m),
    Eq.{u + 1} (α := (↑Y.toLinOrd : Type u)) { down := 0 } { down := 0 }
⊢ Eq.{u + 1} (α := (↑Y.toLinOrd : Type u))
    (if (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a < m then { down := 0 }
    else { down := 1 })
    (if (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a ≤ m then { down := 0 }
    else { down := 1 })
have neg : ∀ (h₁ : (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a < m)
  (h₂ : ¬(LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a ≤ m),
  Eq.{u + 1} (α := (↑Y.toLinOrd : Type u)) { 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 : 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))
p₁ : B ⟶ Y :=
  ofHom { toFun := fun (b : (↑B.1 : Type u)) ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
p₂ : B ⟶ Y :=
  ofHom { toFun := fun (b : (↑B.1 : Type u)) ↦ if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
a : (↑A.toLinOrd : Type u)
pos :
  ∀ (h₁ : (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a < m)
    (h₂ : (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a ≤ m),
    Eq.{u + 1} (α := (↑Y.toLinOrd : Type u)) { down := 0 } { down := 0 }
neg :
  ∀ (h₁ : (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a < m)
    (h₂ : ¬(LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a ≤ m),
    Eq.{u + 1} (α := (↑Y.toLinOrd : Type u)) { down := 0 } { down := 1 }
⊢ Eq.{u + 1} (α := (↑Y.toLinOrd : Type u))
    (if (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a < m then { down := 0 }
    else { down := 1 })
    (if (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a ≤ m then { down := 0 }
    else { down := 1 })
have pos₁ : ∀ (h₁ : ¬(LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a < m)
  (h₂ : (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a ≤ m),
  Eq.{u + 1} (α := (↑Y.toLinOrd : Type u)) { 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 : 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))
p₁ : B ⟶ Y :=
  ofHom { toFun := fun (b : (↑B.1 : Type u)) ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
p₂ : B ⟶ Y :=
  ofHom { toFun := fun (b : (↑B.1 : Type u)) ↦ if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
a : (↑A.toLinOrd : Type u)
pos :
  ∀ (h₁ : (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a < m)
    (h₂ : (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a ≤ m),
    Eq.{u + 1} (α := (↑Y.toLinOrd : Type u)) { down := 0 } { down := 0 }
neg :
  ∀ (h₁ : (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a < m)
    (h₂ : ¬(LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a ≤ m),
    Eq.{u + 1} (α := (↑Y.toLinOrd : Type u)) { down := 0 } { down := 1 }
pos₁ :
  ∀ (h₁ : ¬(LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a < m)
    (h₂ : (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a ≤ m),
    Eq.{u + 1} (α := (↑Y.toLinOrd : Type u)) { down := 1 } { down := 0 }
⊢ Eq.{u + 1} (α := (↑Y.toLinOrd : Type u))
    (if (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a < m then { down := 0 }
    else { down := 1 })
    (if (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a ≤ m then { down := 0 }
    else { down := 1 })
have neg₁ : ∀ (h₁ : ¬(LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a < m)
  (h₂ : ¬(LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a ≤ m),
  Eq.{u + 1} (α := (↑Y.toLinOrd : Type u)) { 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 : 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))
p₁ : B ⟶ Y :=
  ofHom { toFun := fun (b : (↑B.1 : Type u)) ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
p₂ : B ⟶ Y :=
  ofHom { toFun := fun (b : (↑B.1 : Type u)) ↦ if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
a : (↑A.toLinOrd : Type u)
h₁ : (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a < m
h₂ : ¬(LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a ≤ m
⊢ Eq.{u + 1} (α := (↑Y.toLinOrd : Type u)) { down := 0 } { down := 1 }
have neg : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Order.Category.NonemptyFinLinOrd (goal)
Goal:
A B : NonemptyFinLinOrd
f : A ⟶ B
h : 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))
p₁ : B ⟶ Y :=
  ofHom { toFun := fun (b : (↑B.1 : Type u)) ↦ if b < m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
p₂ : B ⟶ Y :=
  ofHom { toFun := fun (b : (↑B.1 : Type u)) ↦ if b ≤ m then { down := 0 } else { down := 1 }, monotone' := ⋯ }
a : (↑A.toLinOrd : Type u)
h₁ : ¬(LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a < m
h₂ : (LinOrd.Hom.hom f.hom : (a : (↑A.toLinOrd : Type u)) → (↑B.toLinOrd : Type u)) a ≤ m
⊢ Eq.{u + 1} (α := (↑Y.toLinOrd : Type u)) { down := 1 } { down := 0 }
have pos : False
Tactic: exfalso