awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
inst_3 : ∀ (i : ι), InvariantBasisNumber.{v} (End (s i))
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_4 : Finite α
inst_5 : Finite β
f : α → ι
g : β → ι
i : Iso.{v, u} (C := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
refine refine₁ : (c : ι) → (↑(f ⁻¹' {c}) : Type) ≃ (↑(g ⁻¹' {c}) : Type)
h : ∀ (c : ι), Nonempty ((↑(f ⁻¹' {c}) : Type) ≃ (↑(g ⁻¹' {c}) : Type))
h₁ : ∀ (c : ι), Cardinal.mk (↑(f ⁻¹' {c}) : Type) = Cardinal.mk (↑(g ⁻¹' {c}) : Type)
h₂ h₃ : ∀ (c : ι) (val : Fintype α), Cardinal.mk (↑(f ⁻¹' {c}) : Type) = Cardinal.mk (↑(g ⁻¹' {c}) : Type)
⊢ ∃ (e : α ≃ β), ∀ (a : α), g ((e : (a : α) → β) a) = f a
have h₄ : ∀ (c : ι) (val : Fintype α) (val : Fintype β), Cardinal.mk (↑(f ⁻¹' {c}) : Type) = Cardinal.mk (↑(g ⁻¹' {c}) : Type)
Tactic: classical
  refine ⟨Equiv.ofPreimageEquiv ?_, fun a => Equiv.ofPreimageEquiv_map _ _⟩
  intro c
  apply Nonempty.some
  apply Cardinal.eq.1
  cases nonempty_fintype α; cases nonempty_fintype β
  simp only [Cardinal.mk_fintype, Nat.cast_inj]
  exact
    Matrix.square_of_invertible (o.matrixDecomposition i.inv c) (o.matrixDecomposition i.hom c)
      (by
        rw [← o.matrixDecomposition_comp]
        simp)
      (by
        rw [← o.matrixDecomposition_comp]
        simp)
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
inst_3 : ∀ (i : ι), InvariantBasisNumber.{v} (End (s i))
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_4 : Finite α
inst_5 : Finite β
f : α → ι
g : β → ι
i : Iso.{v, u} (C := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
refine refine₁ : (c : ι) → (↑(f ⁻¹' {c}) : Type) ≃ (↑(g ⁻¹' {c}) : Type)
h : ∀ (c : ι), Nonempty ((↑(f ⁻¹' {c}) : Type) ≃ (↑(g ⁻¹' {c}) : Type))
h₁ : ∀ (c : ι), Cardinal.mk (↑(f ⁻¹' {c}) : Type) = Cardinal.mk (↑(g ⁻¹' {c}) : Type)
h₂ h₃ : ∀ (c : ι) (val : Fintype α), Cardinal.mk (↑(f ⁻¹' {c}) : Type) = Cardinal.mk (↑(g ⁻¹' {c}) : Type)
h₄ :
  ∀ (c : ι) (val : Fintype α) (val : Fintype β), Cardinal.mk (↑(f ⁻¹' {c}) : Type) = Cardinal.mk (↑(g ⁻¹' {c}) : Type)
⊢ ∃ (e : α ≃ β), ∀ (a : α), g ((e : (a : α) → β) a) = f a
have h₅ : ∀ (c : ι) (val : Fintype α) (val_1 : Fintype β), Fintype.card (↑(f ⁻¹' {c}) : Type) = Fintype.card (↑(g ⁻¹' {c}) : Type)
Tactic: classical
  refine ⟨Equiv.ofPreimageEquiv ?_, fun a => Equiv.ofPreimageEquiv_map _ _⟩
  intro c
  apply Nonempty.some
  apply Cardinal.eq.1
  cases nonempty_fintype α; cases nonempty_fintype β
  simp only [Cardinal.mk_fintype, Nat.cast_inj]
  exact
    Matrix.square_of_invertible (o.matrixDecomposition i.inv c) (o.matrixDecomposition i.hom c)
      (by
        rw [← o.matrixDecomposition_comp]
        simp)
      (by
        rw [← o.matrixDecomposition_comp]
        simp)
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : C
i : P ≅ Q
hP : Injective.{v₁, u₁} P
X Y : C
g : X ⟶ Q
f : X ⟶ Y
mono : Mono f
⊢ ∃ (h : Y ⟶ Q), f ≫ h = g
have obtain : ∀ (h : Y ⟶ P) (h_eq : f ≫ h = g ≫ i.inv), ∃ (h : Y ⟶ Q), f ≫ h = g
Tactic: obtain ⟨h, h_eq⟩ := @Injective.factors C _ P _ _ _ (g ≫ i.inv) f mono
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : C
i : P ≅ Q
hP : Injective.{v₁, u₁} P
X Y : C
g : X ⟶ Q
f : X ⟶ Y
mono : Mono f
h : Y ⟶ P
h_eq : f ≫ h = g ≫ i.inv
⊢ ∃ (h : Y ⟶ Q), f ≫ h = g
have refine : f ≫ h ≫ i.hom = g
Tactic: refine ⟨h ≫ i.hom, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : C
i : P ≅ Q
hP : Injective.{v₁, u₁} P
X Y : C
g : X ⟶ Q
f : X ⟶ Y
mono : Mono f
h : Y ⟶ P
h_eq : f ≫ h = g ≫ i.inv
⊢ f ≫ h ≫ i.hom = g
have rw : (f ≫ h) ≫ i.hom = g
Tactic: rw [← Category.assoc, h_eq, Category.assoc, Iso.inv_hom_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : C
i : P ≅ Q
hP : Injective.{v₁, u₁} P
X Y : C
g : X ⟶ Q
f : X ⟶ Y
mono : Mono f
h : Y ⟶ P
h_eq : f ≫ h = g ≫ i.inv
rw : (f ≫ h) ≫ i.hom = g
⊢ f ≫ h ≫ i.hom = g
have rw₁ : (g ≫ i.inv) ≫ i.hom = g
Tactic: rw [← Category.assoc, h_eq, Category.assoc, Iso.inv_hom_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : C
i : P ≅ Q
hP : Injective.{v₁, u₁} P
X Y : C
g : X ⟶ Q
f : X ⟶ Y
mono : Mono f
h : Y ⟶ P
h_eq : f ≫ h = g ≫ i.inv
rw : (f ≫ h) ≫ i.hom = g
rw₁ : (g ≫ i.inv) ≫ i.hom = g
⊢ f ≫ h ≫ i.hom = g
have rw₂ : g ≫ i.inv ≫ i.hom = g
Tactic: rw [← Category.assoc, h_eq, Category.assoc, Iso.inv_hom_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : C
i : P ≅ Q
hP : Injective.{v₁, u₁} P
X Y : C
g : X ⟶ Q
f : X ⟶ Y
mono : Mono f
h : Y ⟶ P
h_eq : f ≫ h = g ≫ i.inv
rw : (f ≫ h) ≫ i.hom = g
rw₁ : (g ≫ i.inv) ≫ i.hom = g
rw₂ : g ≫ i.inv ≫ i.hom = g
⊢ f ≫ h ≫ i.hom = g
have rw₃ : g ≫ 𝟙 Q = g
Tactic: rw [← Category.assoc, h_eq, Category.assoc, Iso.inv_hom_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : C
i : P ≅ Q
hP : Injective.{v₁, u₁} P
X Y : C
g : X ⟶ Q
f : X ⟶ Y
mono : Mono f
h : Y ⟶ P
h_eq : f ≫ h = g ≫ i.inv
rw : (f ≫ h) ≫ i.hom = g
rw₁ : (g ≫ i.inv) ≫ i.hom = g
rw₂ : g ≫ i.inv ≫ i.hom = g
rw₃ : g ≫ 𝟙 Q = g
⊢ f ≫ h ≫ i.hom = g
have rw₄ : g = g
Tactic: rw [← Category.assoc, h_eq, Category.assoc, Iso.inv_hom_id, Category.comp_id]
-- 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
⊢ (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 ⋯) =
    g
have h : ∀ (y : X_1),
  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 sorry))
      y =
    (ConcreteCategory.hom (FC := TypeCat.Fun) g).toFun y
Tactic: ext y
-- 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
⊢ 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 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 sorry) =
  (ConcreteCategory.hom (FC := TypeCat.Fun) g).toFun y
Tactic: change dite (f y ∈ Set.range f) (fun h => g (Classical.choose h)) _ = _
-- 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
⊢ (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
have 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
Tactic: split_ifs
-- 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
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
⊢ (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
have neg : ((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: split_ifs
-- 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 :
  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
have pos : ∀
  (mono :
    Function.Injective (α := (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 : X_1)
  (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
Tactic: rw [mono_iff_injective] at mono
Cleared hypotheses: mono, y, h
-- 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
⊢ 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 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 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⟩)
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : Type u₁
⊢ Mono.{u₁, u₁ + 1} (X := X) (↾WithBot.some)
have rw : Function.Injective (α := (fun (X : Type u₁) ↦ X) X) (β := (fun (X : Type u₁) ↦ X) (WithBot X))
  (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (↾WithBot.some)) :
    (a : (fun (X : Type u₁) ↦ X) X) → (fun (X : Type u₁) ↦ X) (WithBot X))
Tactic: rw [mono_iff_injective]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : C
inst_1 : HasBinaryProduct.{v₁, u₁} P Q
inst_2 : Injective.{v₁, u₁} P
inst_3 : Injective.{v₁, u₁} Q
X Y : C
g : X ⟶ Limits.prod.{v₁, u₁} P Q
f : X ⟶ Y
mono : Mono f
⊢ ∃ (h : Y ⟶ Limits.prod.{v₁, u₁} P Q), f ≫ h = g
have h : f ≫ prod.lift (factorThru (g ≫ prod.fst) f) (factorThru (g ≫ prod.snd) f) = g
Tactic: use Limits.prod.lift (factorThru (g ≫ Limits.prod.fst) f) (factorThru (g ≫ Limits.prod.snd) f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : C
inst_1 : HasBinaryProduct.{v₁, u₁} P Q
inst_2 : Injective.{v₁, u₁} P
inst_3 : Injective.{v₁, u₁} Q
X Y : C
g : X ⟶ Limits.prod.{v₁, u₁} P Q
f : X ⟶ Y
mono : Mono f
⊢ f ≫ prod.lift (factorThru (g ≫ prod.fst) f) (factorThru (g ≫ prod.snd) f) = g
have h : prod.lift (g ≫ prod.fst) (g ≫ prod.snd) = g
Tactic: simp only [prod.comp_lift, comp_factorThru]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : C
inst_1 : HasBinaryProduct.{v₁, u₁} P Q
inst_2 : Injective.{v₁, u₁} P
inst_3 : Injective.{v₁, u₁} Q
X Y : C
g : X ⟶ Limits.prod.{v₁, u₁} P Q
f : X ⟶ Y
mono : Mono f
⊢ prod.lift (g ≫ prod.fst) (g ≫ prod.snd) = g
have h : CategoryStruct.comp (Y := Limits.prod.{v₁, u₁} P Q) (prod.lift (g ≫ prod.fst) (g ≫ prod.snd)) prod.fst = g ≫ prod.fst
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P Q : C
inst_1 : HasBinaryProduct.{v₁, u₁} P Q
inst_2 : Injective.{v₁, u₁} P
inst_3 : Injective.{v₁, u₁} Q
X Y : C
g : X ⟶ Limits.prod.{v₁, u₁} P Q
f : X ⟶ Y
mono : Mono f
h :
  CategoryStruct.comp (Y := Limits.prod.{v₁, u₁} P Q) (prod.lift (g ≫ prod.fst) (g ≫ prod.snd)) prod.fst = g ≫ prod.fst
⊢ prod.lift (g ≫ prod.fst) (g ≫ prod.snd) = g
have h₁ : CategoryStruct.comp (Y := Limits.prod.{v₁, u₁} P Q) (prod.lift (g ≫ prod.fst) (g ≫ prod.snd)) prod.snd = g ≫ prod.snd
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Injective.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
β : Type v
c : β → C
inst_1 : HasProduct.{v, v₁, u₁} c
inst_2 : ∀ (b : β), Injective.{v₁, u₁} (c b)
X Y : C
g : X ⟶ piObj.{v, v₁, u₁} c
f : X ⟶ Y
mono : Mono f
⊢ ∃ (h : Y ⟶ piObj.{v, v₁, u₁} c), f ≫ h = g
have refine : (f ≫ Pi.lift fun (b : β) ↦ factorThru (g ≫ Pi.π c b) f) = g
Tactic: refine ⟨Pi.lift fun b => factorThru (g ≫ Pi.π c _) f, ?_⟩