awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Sums.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
C : Type u₃
inst_2 : Category.{v₃, u₃} C
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F G : Functor.{v₁, v₂, u₁, u₂} A B
H I : Functor.{v₃, v₄, u₃, u₄} C D
α : F ⟶ G
β : H ⟶ I
x y : C
f : x ⟶ y
⊢ Eq (α := (F.sum H).obj (obj (Sum.inr_ A C) x) ⟶ (G.sum I).obj (obj (Sum.inr_ A C) y))
    ((F.sum H).map (map (Sum.inr_ A C) f) ≫
      match (motive := (X : A ⊕ C) → (F.sum H).obj X ⟶ (G.sum I).obj X) obj (Sum.inr_ A C) y with
      | inl X => map (Sum.inl_ B D) (α.app X)
      | inr X => map (Sum.inr_ B D) (β.app X))
    ((match (motive := (X : A ⊕ C) → (F.sum H).obj X ⟶ (G.sum I).obj X) obj (Sum.inr_ A C) x with
      | inl X => map (Sum.inl_ B D) (α.app X)
      | inr X => map (Sum.inr_ B D) (β.app X)) ≫
      (G.sum I).map (map (Sum.inr_ A C) f))

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Sums.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
C : Type u₃
inst_2 : Category.{v₃, u₃} C
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F G : Functor.{v₁, v₂, u₁, u₂} A B
H I : Functor.{v₃, v₄, u₃, u₄} C D
α : F ⟶ G
β : H ⟶ I
a : A
⊢ Eq (α := (F.sum H).obj (inl a) ⟶ (G.sum I).obj (inl a)) ((sum α β).app (inl a)) (map (Sum.inl_ B D) (α.app a))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sums.Basic
Goal:
A : Type u₁
inst : Category.{v₁, u₁} A
B : Type u₂
inst_1 : Category.{v₂, u₂} B
C : Type u₃
inst_2 : Category.{v₃, u₃} C
D : Type u₄
inst_3 : Category.{v₄, u₄} D
F G : Functor.{v₁, v₂, u₁, u₂} A B
H I : Functor.{v₃, v₄, u₃, u₄} C D
α : F ⟶ G
β : H ⟶ I
c : C
⊢ Eq (α := (F.sum H).obj (inr c) ⟶ (G.sum I).obj (inr c)) ((sum α β).app (inr c)) (map (Sum.inr_ B D) (β.app c))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sums.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : C
⊢ obj (swap C D) (inl X) = inr X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sums.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X : D
⊢ obj (swap C D) (inr X) = inl X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sums.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
f : Quiver.Hom (V := C ⊕ D) (inl X) (inl Y)
⊢ map (swap C D) f = f

Tactic:
rfl

Premises used: CategoryTheory.Sum.homInduction, rfl
-- Module: Mathlib.CategoryTheory.Sums.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : D
f : Quiver.Hom (V := C ⊕ D) (inr X) (inr Y)
⊢ map (swap C D) f = f

Tactic:
rfl

Premises used: CategoryTheory.Sum.homInduction, rfl
-- Module: Mathlib.CategoryTheory.Sums.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
⊢ IsEquivalence (Equivalence.functor (equivalence C D))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Sums.Products
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
A' : Type u_2
inst_1 : Category.{v_2, u_2} A'
B : Type u
inst_2 : Category.{v, u} B
X : A ⊕ A' ⥤ B
a : A
⊢ Eq (α :=
    (obj (𝟭 (A ⊕ A' ⥤ B)) X).obj (Sum.inl a) ⟶
      (obj (Equivalence.functor (functorEquiv A A' B) ⋙ Equivalence.inverse (functorEquiv A A' B)) X).obj (Sum.inl a))
    (NatTrans.app (NatTrans.app (Equivalence.unit (functorEquiv A A' B)) X) (Sum.inl a)) (𝟙 (X.obj (Sum.inl a)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sums.Products
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
A' : Type u_2
inst_1 : Category.{v_2, u_2} A'
B : Type u
inst_2 : Category.{v, u} B
X : A ⊕ A' ⥤ B
a' : A'
⊢ Eq (α :=
    (obj (𝟭 (A ⊕ A' ⥤ B)) X).obj (Sum.inr a') ⟶
      (obj (Equivalence.functor (functorEquiv A A' B) ⋙ Equivalence.inverse (functorEquiv A A' B)) X).obj (Sum.inr a'))
    (NatTrans.app (NatTrans.app (Equivalence.unit (functorEquiv A A' B)) X) (Sum.inr a')) (𝟙 (X.obj (Sum.inr a')))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sums.Products
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
A' : Type u_2
inst_1 : Category.{v_2, u_2} A'
B : Type u
inst_2 : Category.{v, u} B
X : A ⊕ A' ⥤ B
a : A
⊢ Eq (α :=
    (obj (Equivalence.functor (functorEquiv A A' B) ⋙ Equivalence.inverse (functorEquiv A A' B)) X).obj (Sum.inl a) ⟶
      (obj (𝟭 (A ⊕ A' ⥤ B)) X).obj (Sum.inl a))
    (NatTrans.app (NatTrans.app (Iso.inv (Equivalence.unitIso (functorEquiv A A' B))) X) (Sum.inl a))
    (𝟙 (X.obj (Sum.inl a)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sums.Products
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
A' : Type u_2
inst_1 : Category.{v_2, u_2} A'
B : Type u
inst_2 : Category.{v, u} B
X : A ⊕ A' ⥤ B
a' : A'
⊢ Eq (α :=
    (obj (Equivalence.functor (functorEquiv A A' B) ⋙ Equivalence.inverse (functorEquiv A A' B)) X).obj (Sum.inr a') ⟶
      (obj (𝟭 (A ⊕ A' ⥤ B)) X).obj (Sum.inr a'))
    (NatTrans.app (NatTrans.app (Iso.inv (Equivalence.unitIso (functorEquiv A A' B))) X) (Sum.inr a'))
    (𝟙 (X.obj (Sum.inr a')))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Sums.Products
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
A' : Type u_2
inst_1 : Category.{v_2, u_2} A'
B : Type u
inst_2 : Category.{v, u} B
T : Type u_3
inst_3 : Category.{v_3, u_3} T
X Y : (A ⊕ A') ⊕ T ⥤ B
f : X ⟶ Y
x : A
⊢ f.app (Sum.inl (Sum.inl x)) ≫
      𝟙 (Y.obj (Sum.inl (Sum.inl x))) ≫
        Y.map (NatTrans.app (Iso.hom (sum.inlCompInverseAssociator A A' T)) x) ≫ 𝟙 (Y.obj (Sum.inl (Sum.inl x))) =
    (𝟙 (X.obj (Sum.inl (Sum.inl x))) ≫
        X.map (NatTrans.app (Iso.hom (sum.inlCompInverseAssociator A A' T)) x) ≫ 𝟙 (X.obj (Sum.inl (Sum.inl x)))) ≫
      f.app (Sum.inl (Sum.inl x))

Tactic:
simp only [Category.comp_id, Category.id_comp, NatTrans.naturality]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.NatTrans.naturality, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Sums.Products
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
A' : Type u_2
inst_1 : Category.{v_2, u_2} A'
B : Type u
inst_2 : Category.{v, u} B
T : Type u_3
inst_3 : Category.{v_3, u_3} T
X Y : (A ⊕ A') ⊕ T ⥤ B
f : X ⟶ Y
x : A'
⊢ f.app (Sum.inl (Sum.inr x)) ≫
      𝟙 (Y.obj (Sum.inl (Sum.inr x))) ≫
        𝟙 (Y.obj (Sum.inl (Sum.inr x))) ≫
          Y.map (NatTrans.app (Iso.hom (sum.inlCompInrCompInverseAssociator A A' T)) x) ≫
            𝟙 (Y.obj (Sum.inl (Sum.inr x))) =
    (𝟙 (X.obj (Sum.inl (Sum.inr x))) ≫
        𝟙 (X.obj (Sum.inl (Sum.inr x))) ≫
          X.map (NatTrans.app (Iso.hom (sum.inlCompInrCompInverseAssociator A A' T)) x) ≫
            𝟙 (X.obj (Sum.inl (Sum.inr x)))) ≫
      f.app (Sum.inl (Sum.inr x))

Tactic:
simp only [Category.comp_id, Category.id_comp, NatTrans.naturality]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.NatTrans.naturality, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Sums.Products
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
A' : Type u_2
inst_1 : Category.{v_2, u_2} A'
B : Type u
inst_2 : Category.{v, u} B
T : Type u_3
inst_3 : Category.{v_3, u_3} T
X Y : (A ⊕ A') ⊕ T ⥤ B
f : X ⟶ Y
x : T
⊢ f.app (Sum.inr x) ≫
      𝟙 (Y.obj (Sum.inr x)) ≫
        𝟙 (Y.obj (Sum.inr x)) ≫ Y.map (NatTrans.app (Iso.hom (sum.inrCompInrCompInverseAssociator A A' T)) x) =
    (𝟙 (X.obj (Sum.inr x)) ≫
        𝟙 (X.obj (Sum.inr x)) ≫ X.map (NatTrans.app (Iso.hom (sum.inrCompInrCompInverseAssociator A A' T)) x)) ≫
      f.app (Sum.inr x)

Tactic:
simp only [Category.comp_id, Category.id_comp, NatTrans.naturality]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.NatTrans.naturality, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Thin
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Quiver.IsThin.{u₁, v₁} C
x x_1 : Functor.{v₂, v₁, u₂, u₁} D C
α β : x ⟶ x_1
⊢ α.app = β.app

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Thin
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Quiver.IsThin.{u₁, v₁} C
X Y : C
i₁ i₂ : X ≅ Y
w : i₁.hom = i₂.hom
⊢ i₁ = i₂

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Thin
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : Quiver.IsThin.{u₁, v₁} C
X Y : C
i₁ i₂ : X ≅ Y
⊢ i₁.hom = i₂.hom

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
X : Cᵒᵖ
x : G.obj X
Y Z : C
f : Y ⟶ Opposite.unop X
a : (fun (X : Type (max u v)) ↦ X) (F.obj (Opposite.op Y))
ha :
  Eq (α := (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f.op) :
          (a : (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op (Opposite.unop X)))) →
            (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y)))
        x :
      (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Y)) :
          (a : (fun (X : Type (max u v)) ↦ X) (F.obj (Opposite.op Y))) →
            (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y)))
        a :
      (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y)))
g : Z ⟶ Y
h :
  Eq (α := (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map (g ≫ f).op) :
          (a : (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op (Opposite.unop X)))) →
            (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
        x :
      (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Z)) :
          (a : (fun (X : Type (max u v)) ↦ X) (F.obj (Opposite.op Z))) →
            (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g.op) :
            (a : (fun (X : Type (max u v)) ↦ X) (F.obj (Opposite.op Y))) →
              (fun (X : Type (max u v)) ↦ X) (F.obj (Opposite.op Z)))
          a) :
      (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
⊢ ∃ (a : (fun (X : Type (max u v)) ↦ X) (F.obj (Opposite.op Z))),
    Eq (α := (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map (g ≫ f).op) :
            (a : (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op (Opposite.unop X)))) →
              (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
          x :
        (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Z)) :
            (a : (fun (X : Type (max u v)) ↦ X) (F.obj (Opposite.op Z))) →
              (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
          a :
        (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))

Tactic:
use F.map g.op a

Premises used: CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.Functor.map, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
X : Cᵒᵖ
x : G.obj X
Y Z : C
f : Y ⟶ Opposite.unop X
a : (fun (X : Type (max u v)) ↦ X) (F.obj (Opposite.op Y))
ha :
  Eq (α := (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f.op) :
          (a : (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op (Opposite.unop X)))) →
            (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y)))
        x :
      (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Y)) :
          (a : (fun (X : Type (max u v)) ↦ X) (F.obj (Opposite.op Y))) →
            (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y)))
        a :
      (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Y)))
g : Z ⟶ Y
⊢ Eq (α := (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map (g ≫ f).op) :
          (a : (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op (Opposite.unop X)))) →
            (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
        x :
      (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Z)) :
          (a : (fun (X : Type (max u v)) ↦ X) (F.obj (Opposite.op Z))) →
            (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g.op) :
            (a : (fun (X : Type (max u v)) ↦ X) (F.obj (Opposite.op Y))) →
              (fun (X : Type (max u v)) ↦ X) (F.obj (Opposite.op Z)))
          a) :
      (fun (X : Type (max u v)) ↦ X) (G.obj (Opposite.op Z)))

Tactic:
simp [ha, NatTrans.naturality_apply]

Premises used: CategoryTheory.NatTrans.naturality_apply
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
w :
  ∀ (x : Cᵒᵖ) (x_1 : F.obj x),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((m ≫ χ m).app x)).toFun x_1 =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            ((IsTerminal.from (Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit) F ≫ truth C).app x)).toFun
        x_1
⊢ m ≫ χ m = IsTerminal.from (Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit) F ≫ truth C

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
x : Cᵒᵖ
x_1 : F.obj x
w :
  ∀ ⦃Y : C⦄ (f : Y ⟶ Opposite.unop x),
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((m ≫ χ m).app x)).toFun x_1).arrows f ↔
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
                ((IsTerminal.from (Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit) F ≫ truth C).app x)).toFun
            x_1).arrows
        f
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) ((m ≫ χ m).app x)).toFun x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((IsTerminal.from (Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit) F ≫ truth C).app x)).toFun
      x_1

Tactic:
apply Sieve.ext

Premises used: CategoryTheory.Sieve.ext
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
x : Cᵒᵖ
x_1 : F.obj x
⊢ ∀ ⦃Y : C⦄ (f : Y ⟶ Opposite.unop x),
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((m ≫ χ m).app x)).toFun x_1).arrows f ↔
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
                ((IsTerminal.from (Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit) F ≫ truth C).app x)).toFun
            x_1).arrows
        f

Tactic:
simp [← NatTrans.naturality_apply]

Premises used: CategoryTheory.NatTrans.naturality_apply
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst_1 : Mono m
⊢ IsPullback m (IsTerminal.from (Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit) F) (χ m) (truth C)

Tactic:
IsPullback.of_forall_isPullback_app fun X => ?_

Premises used: CategoryTheory.IsPullback.of_forall_isPullback_app
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst_1 : Mono m
refine :
  ∀ (X : Cᵒᵖ),
    IsPullback (m.app X) ((IsTerminal.from (Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit) F).app X) ((χ m).app X)
      (NatTrans.app (truth C) X)
⊢ IsPullback m (IsTerminal.from (Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit) F) (χ m) (truth C)

Tactic:
refine IsPullback.of_forall_isPullback_app fun X => ?_

Premises used: CategoryTheory.IsPullback.of_forall_isPullback_app
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst_1 : Mono m
X : Cᵒᵖ
⊢ ∀ (x₁ y₁ : (fun (X : Type (max u v)) ↦ X) (F.obj X)),
    Eq (α := (fun (X : Type (max u v)) ↦ X) (G.obj X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app X) :
                (a : (fun (X : Type (max u v)) ↦ X) (F.obj X)) → (fun (X : Type (max u v)) ↦ X) (G.obj X))
              x₁ :
            (fun (X : Type (max u v)) ↦ X) (G.obj X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app X) :
                (a : (fun (X : Type (max u v)) ↦ X) (F.obj X)) → (fun (X : Type (max u v)) ↦ X) (G.obj X))
              y₁ :
            (fun (X : Type (max u v)) ↦ X) (G.obj X)) ∧
        Eq (α := (fun (X : Type (max u v)) ↦ X) (Functor.obj (Functor.obj (Functor.const Cᵒᵖ) PUnit.{(max u v) + 1}) X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  ((IsTerminal.from (Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit) F).app X) :
                (a : (fun (X : Type (max u v)) ↦ X) (F.obj X)) →
                  (fun (X : Type (max u v)) ↦ X) (((Functor.const Cᵒᵖ).obj PUnit.{(max u v) + 1}).obj X))
              x₁ :
            (fun (X : Type (max u v)) ↦ X) (Functor.obj (Functor.obj (Functor.const Cᵒᵖ) PUnit.{(max u v) + 1}) X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun)
                  ((IsTerminal.from (Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit) F).app X) :
                (a : (fun (X : Type (max u v)) ↦ X) (F.obj X)) →
                  (fun (X : Type (max u v)) ↦ X) (((Functor.const Cᵒᵖ).obj PUnit.{(max u v) + 1}).obj X))
              y₁ :
            (fun (X : Type (max u v)) ↦ X) (Functor.obj (Functor.obj (Functor.const Cᵒᵖ) PUnit.{(max u v) + 1}) X)) →
      x₁ = y₁

Tactic:
simpa using (mono_iff_injective (m.app X)).mp (inferInstance)

Premises used: CategoryTheory.mono_iff_injective, inferInstance, Iff.mp, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst_1 : Mono m
X : Cᵒᵖ
refine_2 :
  ∀ (x₂ : G.obj X),
    {
          arrows := fun (Y : C) (f : Y ⟶ Opposite.unop X) ↦
            ∃ (a : F.obj (Opposite.op Y)),
              Eq (α := G.obj (Opposite.op Y))
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f.op) : (a : G.obj X) → G.obj (Opposite.op Y)) x₂ :
                  G.obj (Opposite.op Y))
                ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Y)) :
                      (a : F.obj (Opposite.op Y)) → G.obj (Opposite.op Y))
                    a :
                  G.obj (Opposite.op Y)),
          downward_closed := ⋯ : Sieve.{v, u} (Opposite.unop X) } =
        ⊤ →
      ∃ (x₁ : F.obj X), (ConcreteCategory.hom (FC := TypeCat.Fun) (m.app X) : (a : F.obj X) → G.obj X) x₁ = x₂
⊢ ∀ (x₂ : (fun (X : Type (max u v)) ↦ X) (G.obj X))
    (x₃ : (fun (X : Type (max u v)) ↦ X) (Functor.obj (Functor.obj (Functor.const Cᵒᵖ) PUnit.{(max u v) + 1}) X)),
    Eq (α := (fun (X : Type (max u v)) ↦ X) (Functor.obj (Functor.sieves C) X))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((χ m).app X) :
              (a : (fun (X : Type (max u v)) ↦ X) (G.obj X)) →
                (fun (X : Type (max u v)) ↦ X) ((Functor.sieves C).obj X))
            x₂ :
          (fun (X : Type (max u v)) ↦ X) (Functor.obj (Functor.sieves C) X))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (truth C) X) :
              (a : (fun (X : Type (max u v)) ↦ X) (((Functor.const Cᵒᵖ).obj PUnit.{(max u v) + 1}).obj X)) →
                (fun (X : Type (max u v)) ↦ X) ((Functor.sieves C).obj X))
            x₃ :
          (fun (X : Type (max u v)) ↦ X) (Functor.obj (Functor.sieves C) X)) →
      ∃ (x₁ : (fun (X : Type (max u v)) ↦ X) (F.obj X)),
        (ConcreteCategory.hom (FC := TypeCat.Fun) (m.app X) :
                (a : (fun (X : Type (max u v)) ↦ X) (F.obj X)) → (fun (X : Type (max u v)) ↦ X) (G.obj X))
              x₁ =
            x₂ ∧
          (ConcreteCategory.hom (FC := TypeCat.Fun)
                  ((IsTerminal.from (Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit) F).app X) :
                (a : (fun (X : Type (max u v)) ↦ X) (F.obj X)) →
                  (fun (X : Type (max u v)) ↦ X) (((Functor.const Cᵒᵖ).obj PUnit.{(max u v) + 1}).obj X))
              x₁ =
            x₃

Tactic:
simp only [Functor.const_obj_obj, Functor.sieves_obj, χ_app, Opposite.op_unop,
      TypeCat.hom_ofHom, TypeCat.Fun.coe_mk, truth_app, Functor.isTerminalConst_from_app,
      Types.isTerminalPUnit_from_apply, and_true, forall_const]

Premises used: and_true, CategoryTheory.Presheaf.truth_app, CategoryTheory.Presheaf.χ_app, Opposite.op_unop, TypeCat.Fun.coe_mk, TypeCat.hom_ofHom, CategoryTheory.Limits.Types.isTerminalPUnit_from_apply, CategoryTheory.Functor.sieves_obj, forall_const, CategoryTheory.Functor.const_obj_obj, CategoryTheory.Functor.isTerminalConst_from_app
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst_1 : Mono m
X : Cᵒᵖ
p : G.obj X
hp :
  {
      arrows := fun (Y : C) (f : Y ⟶ Opposite.unop X) ↦
        ∃ (a : F.obj (Opposite.op Y)),
          Eq (α := G.obj (Opposite.op Y))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map f.op) : (a : G.obj X) → G.obj (Opposite.op Y)) p :
              G.obj (Opposite.op Y))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app (Opposite.op Y)) :
                  (a : F.obj (Opposite.op Y)) → G.obj (Opposite.op Y))
                a :
              G.obj (Opposite.op Y)),
      downward_closed := ⋯ : Sieve.{v, u} (Opposite.unop X) } =
    ⊤
⊢ ∃ (x₁ : F.obj X), (ConcreteCategory.hom (FC := TypeCat.Fun) (m.app X) : (a : F.obj X) → G.obj X) x₁ = p

Tactic:
simpa [eq_comm] using congr($(hp).arrows (𝟙 _))

Premises used: eq_comm
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
χ' : G ⟶ Functor.sieves C
hχ' : IsPullback m (IsTerminal.from (Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit) F) χ' (truth C)
w :
  ∀ (X : Cᵒᵖ) (x : G.obj X),
    (ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app X)).toFun x =
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((χ m).app X)).toFun x
⊢ χ' = χ m

Tactic:
ext X x
-- Module: Mathlib.CategoryTheory.Topos.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
χ' : G ⟶ Functor.sieves C
hχ' : IsPullback m (IsTerminal.from (Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit) F) χ' (truth C)
X : Cᵒᵖ
x : G.obj X
⊢ (∀ (x : Cᵒᵖ), m.app x ≫ χ'.app x = Types.isTerminalPUnit.from (F.obj x) ≫ ↾fun (x_1 : PUnit.{(max u v) + 1}) ↦ ⊤) ∧
    (∀ (x : Cᵒᵖ) (x₁ y₁ : F.obj x),
        Eq (α := G.obj x) ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) x₁ : G.obj x)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) y₁ : G.obj x) →
          x₁ = y₁) ∧
      ∀ (x : Cᵒᵖ) (x₂ : G.obj x),
        Eq (α := Sieve.{v, u} (Opposite.unop x))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (χ'.app x) : (a : G.obj x) → Sieve (Opposite.unop x)) x₂ :
              Sieve.{v, u} (Opposite.unop x))
            (⊤ : Sieve.{v, u} (Opposite.unop x)) →
          ∃ (x₁ : F.obj x), (ConcreteCategory.hom (FC := TypeCat.Fun) (m.app x) : (a : F.obj x) → G.obj x) x₁ = x₂

Tactic:
simp only [IsPullback.iff_app, Functor.const_obj_obj, Functor.sieves_obj,
    Functor.isTerminalConst_from_app, truth_app, Types.isPullback_iff,
    Types.isTerminalPUnit_from_apply, and_true, TypeCat.hom_ofHom, TypeCat.Fun.coe_mk,
    forall_const, forall_and] at hχ'

Premises used: and_true, CategoryTheory.Presheaf.truth_app, TypeCat.Fun.coe_mk, TypeCat.hom_ofHom, CategoryTheory.Limits.Types.isTerminalPUnit_from_apply, CategoryTheory.Limits.Types.isPullback_iff, CategoryTheory.Functor.sieves_obj, forall_const, CategoryTheory.Functor.const_obj_obj, CategoryTheory.IsPullback.iff_app, CategoryTheory.Functor.isTerminalConst_from_app, forall_and