-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : Type u₁
inst_1 : Nonempty X
X_1 Y : Type u₁
g : X_1 ⟶ X
f : X_1 ⟶ Y
mono : Mono f
y : X_1
h :
  (if h :
        Membership.mem (α := (fun (X : Type u₁) ↦ X) Y) (γ := Set ((fun (X : Type u₁) ↦ X) Y))
          (Set.range (ι := (fun (X : Type u₁) ↦ X) X_1)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
              (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y)
              y :
            (fun (X : Type u₁) ↦ X) Y) then
      (ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) X)
        (Classical.choose (p := fun (x : X_1) ↦
          Eq (α := (fun (X : Type u₁) ↦ X) Y)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                  (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y)
                x :
              (fun (X : Type u₁) ↦ X) Y)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                  (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y)
                y :
              (fun (X : Type u₁) ↦ X) Y))
          h)
    else Nonempty.some ⋯) =
    (ConcreteCategory.hom (FC := TypeCat.Fun) g).toFun y
pos :
  ∀
    (h :
      Membership.mem (α := (fun (X : Type u₁) ↦ X) Y) (γ := Set ((fun (X : Type u₁) ↦ X) Y))
        (Set.range (ι := (fun (X : Type u₁) ↦ X) X_1)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
            (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y)
            y :
          (fun (X : Type u₁) ↦ X) Y)),
    (ConcreteCategory.hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) X)
        (Classical.choose (p := fun (x : X_1) ↦
          Eq (α := (fun (X : Type u₁) ↦ X) Y)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                  (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y)
                x :
              (fun (X : Type u₁) ↦ X) Y)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
                  (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y)
                y :
              (fun (X : Type u₁) ↦ X) Y))
          h) =
      (ConcreteCategory.hom (FC := TypeCat.Fun) g).toFun y
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (f ≫
          ↾fun (z : Y) ↦
            if h :
                Membership.mem (γ := Set ((fun (X : Type u₁) ↦ X) Y))
                  (Set.range (ι := (fun (X : Type u₁) ↦ X) X_1)
                    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                      (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y))
                  z then
              (ConcreteCategory.hom (FC := TypeCat.Fun) g :
                  (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) X)
                (Classical.choose (p := fun (x : X_1) ↦
                  (ConcreteCategory.hom (FC := TypeCat.Fun) f :
                        (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y)
                      x =
                    z)
                  h)
            else Nonempty.some ⋯))
      y =
    (ConcreteCategory.hom (FC := TypeCat.Fun) g).toFun y
have neg : ∀
  (h :
    ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y) y :
        (fun (X : Type u₁) ↦ X) Y) ∉
      Set.range (ι := (fun (X : Type u₁) ↦ X) X_1)
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
          (a : (fun (X : Type u₁) ↦ X) X_1) → (fun (X : Type u₁) ↦ X) Y)),
  Nonempty.some sorry = (ConcreteCategory.hom (FC := TypeCat.Fun) g).toFun y
Tactic: classical
      change dite (f y ∈ Set.range f) (fun h => g (Classical.choose h)) _ = _
      split_ifs <;> rename_i h
      · rw [mono_iff_injective] at mono
        simp [mono (Classical.choose_spec h)]
      · exact False.elim (h ⟨y, rfl⟩)