awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
κ : Cardinal.{w}
C : Type u
inst : Category.{v, u} C
hC : HasCardinalLT (Arrow.{v, u} C) κ
Ω : Type w := κ.ord.ToType
ι : Arrow.{v, u} C ↪ Ω
rw : Nonempty (C ↪ Ω)
⊢ Cardinal.lift.{w, u} (Cardinal.mk C) ≤ Cardinal.lift.{u, w} (Cardinal.mk Ω)

Tactic:
rw [Cardinal.lift_mk_le']

Premises used: Cardinal.lift_mk_le'
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
κ : Cardinal.{w}
C : Type u
inst : Category.{v, u} C
hC : HasCardinalLT (Arrow.{v, u} C) κ
Ω : Type w := κ.ord.ToType
ι : Arrow.{v, u} C ↪ Ω
⊢ Nonempty (C ↪ Ω)

Tactic:
⟨Function.Embedding.trans { toFun X := Arrow.mk (𝟙 X), inj' := ?_ } ι⟩

Premises used: Function.Embedding.mk, CategoryTheory.CategoryStruct.id, Nonempty.intro, Function.Embedding.trans, CategoryTheory.Arrow.mk
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
κ : Cardinal.{w}
C : Type u
inst : Category.{v, u} C
hC : HasCardinalLT (Arrow.{v, u} C) κ
Ω : Type w := κ.ord.ToType
ι : Arrow.{v, u} C ↪ Ω
refine : Function.Injective (β := Arrow.{v, u} C) fun (X : C) ↦ Arrow.mk (𝟙 X)
⊢ Nonempty (C ↪ Ω)

Tactic:
refine ⟨Function.Embedding.trans { toFun X := Arrow.mk (𝟙 X), inj' := ?_ } ι⟩
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
κ : Cardinal.{w}
C : Type u
inst : Category.{v, u} C
hC : HasCardinalLT (Arrow.{v, u} C) κ
Ω : Type w := κ.ord.ToType
ι : Arrow.{v, u} C ↪ Ω
X Y : C
h :
  Eq (α := Arrow.{v, u} C) ((fun (X : C) ↦ (Arrow.mk (𝟙 X) : Arrow.{v, u} C)) X)
    ((fun (X : C) ↦ (Arrow.mk (𝟙 X) : Arrow.{v, u} C)) Y)
⊢ X = Y

Tactic:
congr_arg Arrow.leftFunc.obj h

Premises used: CategoryTheory.Arrow.leftFunc, congr_arg, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
κ : Cardinal.{w}
C : Type u
inst : Category.{v, u} C
hC : HasCardinalLT (Arrow.{v, u} C) κ
Ω : Type w := κ.ord.ToType
ι : Arrow.{v, u} C ↪ Ω
X Y : C
h :
  Eq (α := Arrow.{v, u} C) ((fun (X : C) ↦ (Arrow.mk (𝟙 X) : Arrow.{v, u} C)) X)
    ((fun (X : C) ↦ (Arrow.mk (𝟙 X) : Arrow.{v, u} C)) Y)
⊢ X = Y

Tactic:
exact congr_arg Arrow.leftFunc.obj h

Premises used: CategoryTheory.Arrow.leftFunc, congr_arg, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
κ : Cardinal.{w}
C : Type u
inst : Category.{v, u} C
hC : HasCardinalLT (Arrow.{v, u} C) κ
Ω : Type w := κ.ord.ToType
ι : Arrow.{v, u} C ↪ Ω
⊢ Cardinal.lift.{w, u} (Cardinal.mk C) ≤ Cardinal.lift.{u, w} (Cardinal.mk Ω)

Tactic:
have h₁ : Cardinal.lift.{w} (Cardinal.mk C) ≤
      Cardinal.lift.{u} (Cardinal.mk Ω) := by
    rw [Cardinal.lift_mk_le']
    refine ⟨Function.Embedding.trans { toFun X := Arrow.mk (𝟙 X), inj' := ?_ } ι⟩
    intro X Y h
    exact congr_arg Arrow.leftFunc.obj h
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
κ : Cardinal.{w}
C : Type u
inst : Category.{v, u} C
hC : HasCardinalLT (Arrow.{v, u} C) κ
Ω : Type w := κ.ord.ToType
ι : Arrow.{v, u} C ↪ Ω
h₁ : Cardinal.lift.{w, u} (Cardinal.mk C) ≤ Cardinal.lift.{u, w} (Cardinal.mk Ω)
X Y : C
rw : Nonempty (Function.Embedding.{v + 1, w + 1} (X ⟶ Y) Ω)
⊢ Cardinal.lift.{w, v} (Cardinal.mk (X ⟶ Y)) ≤ Cardinal.lift.{v, w} (Cardinal.mk Ω)

Tactic:
rw [Cardinal.lift_mk_le']

Premises used: Cardinal.lift_mk_le'
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
κ : Cardinal.{w}
C : Type u
inst : Category.{v, u} C
hC : HasCardinalLT (Arrow.{v, u} C) κ
Ω : Type w := κ.ord.ToType
ι : Arrow.{v, u} C ↪ Ω
h₁ : Cardinal.lift.{w, u} (Cardinal.mk C) ≤ Cardinal.lift.{u, w} (Cardinal.mk Ω)
X Y : C
⊢ Nonempty (Function.Embedding.{v + 1, w + 1} (X ⟶ Y) Ω)

Tactic:
⟨Function.Embedding.trans { toFun f := Arrow.mk f, inj' := ?_ } ι⟩

Premises used: Function.Embedding.mk, Nonempty.intro, Function.Embedding.trans, CategoryTheory.Arrow.mk
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
κ : Cardinal.{w}
C : Type u
inst : Category.{v, u} C
hC : HasCardinalLT (Arrow.{v, u} C) κ
Ω : Type w := κ.ord.ToType
ι : Arrow.{v, u} C ↪ Ω
h₁ : Cardinal.lift.{w, u} (Cardinal.mk C) ≤ Cardinal.lift.{u, w} (Cardinal.mk Ω)
X Y : C
refine : Function.Injective (β := Arrow.{v, u} C) fun (f : X ⟶ Y) ↦ Arrow.mk f
⊢ Nonempty (Function.Embedding.{v + 1, w + 1} (X ⟶ Y) Ω)

Tactic:
refine ⟨Function.Embedding.trans { toFun f := Arrow.mk f, inj' := ?_ } ι⟩
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
κ : Cardinal.{w}
C : Type u
inst : Category.{v, u} C
hC : HasCardinalLT (Arrow.{v, u} C) κ
Ω : Type w := κ.ord.ToType
ι : Arrow.{v, u} C ↪ Ω
h₁ : Cardinal.lift.{w, u} (Cardinal.mk C) ≤ Cardinal.lift.{u, w} (Cardinal.mk Ω)
X Y : C
f g : X ⟶ Y
h : Eq (α := Arrow.{v, u} C) ((fun (f : X ⟶ Y) ↦ Arrow.mk f) f) ((fun (f : X ⟶ Y) ↦ Arrow.mk f) g)
⊢ f = g

Tactic:
simpa [Arrow.mk_eq_mk_iff] using h

Premises used: CategoryTheory.Arrow.mk_eq_mk_iff
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
κ : Cardinal.{w}
C : Type u
inst : Category.{v, u} C
hC : HasCardinalLT (Arrow.{v, u} C) κ
Ω : Type w := κ.ord.ToType
ι : Arrow.{v, u} C ↪ Ω
h₁ : Cardinal.lift.{w, u} (Cardinal.mk C) ≤ Cardinal.lift.{u, w} (Cardinal.mk Ω)
⊢ ∀ (X Y : C), Cardinal.lift.{w, v} (Cardinal.mk (X ⟶ Y)) ≤ Cardinal.lift.{v, w} (Cardinal.mk Ω)

Tactic:
have h₂ (X Y : C) : Cardinal.lift.{w} (Cardinal.mk (X ⟶ Y)) ≤
      Cardinal.lift.{v} (Cardinal.mk Ω) := by
    rw [Cardinal.lift_mk_le']
    refine ⟨Function.Embedding.trans { toFun f := Arrow.mk f, inj' := ?_ } ι⟩
    intro f g h
    simpa [Arrow.mk_eq_mk_iff] using h
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
κ : Cardinal.{w}
C : Type u
inst : Category.{v, u} C
hC : HasCardinalLT (Arrow.{v, u} C) κ
Ω : Type w := κ.ord.ToType
ι : Arrow.{v, u} C ↪ Ω
h₁ : Cardinal.lift.{w, u} (Cardinal.mk C) ≤ Cardinal.lift.{u, w} (Cardinal.mk Ω)
h₂ : ∀ (X Y : C), Cardinal.lift.{w, v} (Cardinal.mk (X ⟶ Y)) ≤ Cardinal.lift.{v, w} (Cardinal.mk Ω)
f₁ : C ↪ Ω := ⋯.some
f₂ : (X Y : C) → Function.Embedding.{v + 1, w + 1} (X ⟶ Y) Ω := fun (X Y : C) ↦ ⋯.some
e : Equiv.{u + 1, w + 1} C (↑(Set.range.{w, u + 1} (ι := C) (⇑f₁ : (a : C) → Ω)) : Type w) :=
  Equiv.ofInjective (⇑f₁ : (a : C) → Ω) ⋯
x x_1 : (↑(Set.range.{w, u + 1} (ι := C) (⇑f₁ : (a : C) → Ω)) : Type w)
⊢ Equiv.{w + 1, v + 1}
    (↑(Set.range.{w, v + 1} (ι :=
          Quiver.Hom.{v, u} (V := C) ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x : C)
            ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x_1 : C))
          (⇑(f₂ ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x)
                ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x_1)) :
            (a :
                (e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x ⟶
                  (e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x_1) →
              Ω)) :
      Type w)
    (Quiver.Hom.{v, u} (V := C) ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x : C)
      ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x_1 : C))

Tactic:
simpa using (Equiv.ofInjective _ ((f₂ _ _).injective)).symm

Premises used: Equiv.ofInjective, Function.Embedding.injective, Equiv.symm
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
κ : Cardinal.{w}
C : Type u
inst : Category.{v, u} C
hC : HasCardinalLT (Arrow.{v, u} C) κ
Ω : Type w := κ.ord.ToType
ι : Arrow.{v, u} C ↪ Ω
h₁ : Cardinal.lift.{w, u} (Cardinal.mk C) ≤ Cardinal.lift.{u, w} (Cardinal.mk Ω)
h₂ : ∀ (X Y : C), Cardinal.lift.{w, v} (Cardinal.mk (X ⟶ Y)) ≤ Cardinal.lift.{v, w} (Cardinal.mk Ω)
f₁ : C ↪ Ω := ⋯.some
f₂ : (X Y : C) → Function.Embedding.{v + 1, w + 1} (X ⟶ Y) Ω := fun (X Y : C) ↦ ⋯.some
e : Equiv.{u + 1, w + 1} C (↑(Set.range.{w, u + 1} (ι := C) (⇑f₁ : (a : C) → Ω)) : Type w) :=
  Equiv.ofInjective (⇑f₁ : (a : C) → Ω) ⋯
h : CoreSmallCategoryOfSet.{w, v, u} Ω C :=
  { obj := Set.range.{w, u + 1} (ι := C) (⇑f₁ : (a : C) → Ω),
    hom := fun (X Y : (↑(Set.range.{w, u + 1} (ι := C) (⇑f₁ : (a : C) → Ω)) : Type w)) ↦
      Set.range.{w, v + 1} (ι :=
        Quiver.Hom.{v, u} (V := C) ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) X : C)
          ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) Y : C))
        (⇑(f₂ ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) X)
              ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) Y)) :
          (a :
              (e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) X ⟶
                (e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) Y) →
            Ω),
    objEquiv := e.symm,
    homEquiv := fun {x x_1 : (↑(Set.range.{w, u + 1} (ι := C) (⇑f₁ : (a : C) → Ω)) : Type w)} ↦
      Equiv.symm
        (Equiv.ofInjective
          (⇑(f₂ ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x)
                ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x_1)) :
            (a :
                (e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x ⟶
                  (e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x_1) →
              Ω)
          ⋯) }
⊢ ∃ (S : SmallCategoryCardinalLT κ), Nonempty (Equivalence.{w, v, w, u} (categoryFamily κ S) C)

Tactic:
⟨⟨h.smallCategoryOfSet, ?_⟩, ⟨h.equivalence⟩⟩

Premises used: CategoryTheory.CoreSmallCategoryOfSet.smallCategoryOfSet, Nonempty.intro, Subtype.mk, Exists.intro, CategoryTheory.CoreSmallCategoryOfSet.equivalence
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
κ : Cardinal.{w}
C : Type u
inst : Category.{v, u} C
hC : HasCardinalLT (Arrow.{v, u} C) κ
Ω : Type w := κ.ord.ToType
ι : Arrow.{v, u} C ↪ Ω
h₁ : Cardinal.lift.{w, u} (Cardinal.mk C) ≤ Cardinal.lift.{u, w} (Cardinal.mk Ω)
h₂ : ∀ (X Y : C), Cardinal.lift.{w, v} (Cardinal.mk (X ⟶ Y)) ≤ Cardinal.lift.{v, w} (Cardinal.mk Ω)
f₁ : C ↪ Ω := ⋯.some
f₂ : (X Y : C) → Function.Embedding.{v + 1, w + 1} (X ⟶ Y) Ω := fun (X Y : C) ↦ ⋯.some
e : Equiv.{u + 1, w + 1} C (↑(Set.range.{w, u + 1} (ι := C) (⇑f₁ : (a : C) → Ω)) : Type w) :=
  Equiv.ofInjective (⇑f₁ : (a : C) → Ω) ⋯
h : CoreSmallCategoryOfSet.{w, v, u} Ω C :=
  { obj := Set.range.{w, u + 1} (ι := C) (⇑f₁ : (a : C) → Ω),
    hom := fun (X Y : (↑(Set.range.{w, u + 1} (ι := C) (⇑f₁ : (a : C) → Ω)) : Type w)) ↦
      Set.range.{w, v + 1} (ι :=
        Quiver.Hom.{v, u} (V := C) ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) X : C)
          ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) Y : C))
        (⇑(f₂ ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) X)
              ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) Y)) :
          (a :
              (e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) X ⟶
                (e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) Y) →
            Ω),
    objEquiv := e.symm,
    homEquiv := fun {x x_1 : (↑(Set.range.{w, u + 1} (ι := C) (⇑f₁ : (a : C) → Ω)) : Type w)} ↦
      Equiv.symm
        (Equiv.ofInjective
          (⇑(f₂ ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x)
                ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x_1)) :
            (a :
                (e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x ⟶
                  (e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x_1) →
              Ω)
          ⋯) }
refine : HasCardinalLT (Arrow (↑h.smallCategoryOfSet.obj : Type w)) κ
⊢ ∃ (S : SmallCategoryCardinalLT κ), Nonempty (Equivalence.{w, v, w, u} (categoryFamily κ S) C)

Tactic:
refine ⟨⟨h.smallCategoryOfSet, ?_⟩, ⟨h.equivalence⟩⟩
-- Module: Mathlib.CategoryTheory.SmallRepresentatives
Goal:
κ : Cardinal.{w}
C : Type u
inst : Category.{v, u} C
hC : HasCardinalLT (Arrow.{v, u} C) κ
Ω : Type w := κ.ord.ToType
ι : Arrow.{v, u} C ↪ Ω
h₁ : Cardinal.lift.{w, u} (Cardinal.mk C) ≤ Cardinal.lift.{u, w} (Cardinal.mk Ω)
h₂ : ∀ (X Y : C), Cardinal.lift.{w, v} (Cardinal.mk (X ⟶ Y)) ≤ Cardinal.lift.{v, w} (Cardinal.mk Ω)
f₁ : C ↪ Ω := ⋯.some
f₂ : (X Y : C) → Function.Embedding.{v + 1, w + 1} (X ⟶ Y) Ω := fun (X Y : C) ↦ ⋯.some
e : Equiv.{u + 1, w + 1} C (↑(Set.range.{w, u + 1} (ι := C) (⇑f₁ : (a : C) → Ω)) : Type w) :=
  Equiv.ofInjective (⇑f₁ : (a : C) → Ω) ⋯
h : CoreSmallCategoryOfSet.{w, v, u} Ω C :=
  { obj := Set.range.{w, u + 1} (ι := C) (⇑f₁ : (a : C) → Ω),
    hom := fun (X Y : (↑(Set.range.{w, u + 1} (ι := C) (⇑f₁ : (a : C) → Ω)) : Type w)) ↦
      Set.range.{w, v + 1} (ι :=
        Quiver.Hom.{v, u} (V := C) ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) X : C)
          ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) Y : C))
        (⇑(f₂ ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) X)
              ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) Y)) :
          (a :
              (e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) X ⟶
                (e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) Y) →
            Ω),
    objEquiv := e.symm,
    homEquiv := fun {x x_1 : (↑(Set.range.{w, u + 1} (ι := C) (⇑f₁ : (a : C) → Ω)) : Type w)} ↦
      Equiv.symm
        (Equiv.ofInjective
          (⇑(f₂ ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x)
                ((e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x_1)) :
            (a :
                (e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x ⟶
                  (e.symm : (a : (↑(Set.range (⇑f₁ : (a : C) → Ω)) : Type w)) → C) x_1) →
              Ω)
          ⋯) }
rwa rwa₁ rwa₂ rwa₃ : HasCardinalLT (Arrow.{v, u} C) κ
⊢ HasCardinalLT (Arrow (↑h.smallCategoryOfSet.obj : Type w)) κ

Tactic:
rwa [hasCardinalLT_iff_of_equiv h.arrowEquiv]

Premises used: hasCardinalLT_iff_of_equiv, CategoryTheory.CoreSmallCategoryOfSet.arrowEquiv
-- Module: Mathlib.CategoryTheory.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq₁ sq₂ : Square.{v, u} C
f g : sq₁ ⟶ sq₂
h₁ : f.τ₁ = g.τ₁
h₂ : f.τ₂ = g.τ₂
h₃ : f.τ₃ = g.τ₃
h₄ : f.τ₄ = g.τ₄
⊢ f = g

Tactic:
Hom.ext h₁ h₂ h₃ h₄

Premises used: CategoryTheory.Square.Hom.ext
-- Module: Mathlib.CategoryTheory.Square
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
sq₁ sq₂ : Square.{v, u} C
e₁ : sq₁.X₁ ≅ sq₂.X₁
e₂ : sq₁.X₂ ≅ sq₂.X₂
e₃ : sq₁.X₃ ≅ sq₂.X₃
e₄ : sq₁.X₄ ≅ sq₂.X₄
comm₁₂ : sq₁.f₁₂ ≫ e₂.hom = e₁.hom ≫ sq₂.f₁₂
comm₁₃ : sq₁.f₁₃ ≫ e₃.hom = e₁.hom ≫ sq₂.f₁₃
comm₂₄ : sq₁.f₂₄ ≫ e₄.hom = e₂.hom ≫ sq₂.f₂₄
comm₃₄ : sq₁.f₃₄ ≫ e₄.hom = e₃.hom ≫ sq₂.f₃₄
⊢ sq₂.f₁₂ ≫ e₂.inv = e₁.inv ≫ sq₁.f₁₂

Tactic:
simp only [← cancel_mono e₂.hom, assoc, Iso.inv_hom_id,
                      comp_id, comm₁₂, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Square
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
sq₁ sq₂ : Square.{v, u} C
e₁ : sq₁.X₁ ≅ sq₂.X₁
e₂ : sq₁.X₂ ≅ sq₂.X₂
e₃ : sq₁.X₃ ≅ sq₂.X₃
e₄ : sq₁.X₄ ≅ sq₂.X₄
comm₁₂ : sq₁.f₁₂ ≫ e₂.hom = e₁.hom ≫ sq₂.f₁₂
comm₁₃ : sq₁.f₁₃ ≫ e₃.hom = e₁.hom ≫ sq₂.f₁₃
comm₂₄ : sq₁.f₂₄ ≫ e₄.hom = e₂.hom ≫ sq₂.f₂₄
comm₃₄ : sq₁.f₃₄ ≫ e₄.hom = e₃.hom ≫ sq₂.f₃₄
⊢ sq₂.f₁₃ ≫ e₃.inv = e₁.inv ≫ sq₁.f₁₃

Tactic:
simp only [← cancel_mono e₃.hom, assoc, Iso.inv_hom_id,
                      comp_id, comm₁₃, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Square
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
sq₁ sq₂ : Square.{v, u} C
e₁ : sq₁.X₁ ≅ sq₂.X₁
e₂ : sq₁.X₂ ≅ sq₂.X₂
e₃ : sq₁.X₃ ≅ sq₂.X₃
e₄ : sq₁.X₄ ≅ sq₂.X₄
comm₁₂ : sq₁.f₁₂ ≫ e₂.hom = e₁.hom ≫ sq₂.f₁₂
comm₁₃ : sq₁.f₁₃ ≫ e₃.hom = e₁.hom ≫ sq₂.f₁₃
comm₂₄ : sq₁.f₂₄ ≫ e₄.hom = e₂.hom ≫ sq₂.f₂₄
comm₃₄ : sq₁.f₃₄ ≫ e₄.hom = e₃.hom ≫ sq₂.f₃₄
⊢ sq₂.f₂₄ ≫ e₄.inv = e₂.inv ≫ sq₁.f₂₄

Tactic:
simp only [← cancel_mono e₄.hom, assoc, Iso.inv_hom_id,
                      comp_id, comm₂₄, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Square
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
sq₁ sq₂ : Square.{v, u} C
e₁ : sq₁.X₁ ≅ sq₂.X₁
e₂ : sq₁.X₂ ≅ sq₂.X₂
e₃ : sq₁.X₃ ≅ sq₂.X₃
e₄ : sq₁.X₄ ≅ sq₂.X₄
comm₁₂ : sq₁.f₁₂ ≫ e₂.hom = e₁.hom ≫ sq₂.f₁₂
comm₁₃ : sq₁.f₁₃ ≫ e₃.hom = e₁.hom ≫ sq₂.f₁₃
comm₂₄ : sq₁.f₂₄ ≫ e₄.hom = e₂.hom ≫ sq₂.f₂₄
comm₃₄ : sq₁.f₃₄ ≫ e₄.hom = e₃.hom ≫ sq₂.f₃₄
⊢ sq₂.f₃₄ ≫ e₄.inv = e₃.inv ≫ sq₁.f₃₄

Tactic:
simp only [← cancel_mono e₄.hom, assoc, Iso.inv_hom_id,
                      comp_id, comm₃₄, Iso.inv_hom_id_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.inv_hom_id, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Iso.inv_hom_id_assoc, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Square
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y : (Square.{v, u} C)ᵒᵖ
φ : X ⟶ Y
⊢ ((Opposite.unop X).op.f₁₂ ≫ φ.unop.τ₂.op).unop = Quiver.Hom.unop (φ.unop.τ₄.op ≫ (Opposite.unop Y).op.f₁₂)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Square
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y : (Square.{v, u} C)ᵒᵖ
φ : X ⟶ Y
⊢ ((Opposite.unop X).op.f₁₃ ≫ φ.unop.τ₃.op).unop = Quiver.Hom.unop (φ.unop.τ₄.op ≫ (Opposite.unop Y).op.f₁₃)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Square
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y : (Square.{v, u} C)ᵒᵖ
φ : X ⟶ Y
⊢ ((Opposite.unop X).op.f₂₄ ≫ φ.unop.τ₁.op).unop = Quiver.Hom.unop (φ.unop.τ₂.op ≫ (Opposite.unop Y).op.f₂₄)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Square
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y : (Square.{v, u} C)ᵒᵖ
φ : X ⟶ Y
⊢ ((Opposite.unop X).op.f₃₄ ≫ φ.unop.τ₁.op).unop = Quiver.Hom.unop (φ.unop.τ₃.op ≫ (Opposite.unop Y).op.f₃₄)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Square
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y : (Square.{v, u} Cᵒᵖ)ᵒᵖ
φ : X ⟶ Y
⊢ ((Opposite.unop X).unop.f₁₂ ≫ φ.unop.τ₂.unop).op = (φ.unop.τ₄.unop ≫ (Opposite.unop Y).unop.f₁₂).op

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Square
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y : (Square.{v, u} Cᵒᵖ)ᵒᵖ
φ : X ⟶ Y
⊢ ((Opposite.unop X).unop.f₁₃ ≫ φ.unop.τ₃.unop).op = (φ.unop.τ₄.unop ≫ (Opposite.unop Y).unop.f₁₃).op

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Square
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y : (Square.{v, u} Cᵒᵖ)ᵒᵖ
φ : X ⟶ Y
⊢ ((Opposite.unop X).unop.f₂₄ ≫ φ.unop.τ₁.unop).op = (φ.unop.τ₂.unop ≫ (Opposite.unop Y).unop.f₂₄).op

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Square
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
X Y : (Square.{v, u} Cᵒᵖ)ᵒᵖ
φ : X ⟶ Y
⊢ ((Opposite.unop X).unop.f₃₄ ≫ φ.unop.τ₁.unop).op = (φ.unop.τ₃.unop ≫ (Opposite.unop Y).unop.f₃₄).op

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Square
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
sq : Square.{v, u} C
F : Functor.{v, v', u, u'} C D
⊢ F.map sq.f₁₂ ≫ F.map sq.f₂₄ = F.map sq.f₁₃ ≫ F.map sq.f₃₄

Tactic:
simpa using F.congr_map sq.fac

Premises used: CategoryTheory.Square.fac, CategoryTheory.Functor.congr_map
-- Module: Mathlib.CategoryTheory.Square
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
X Y : Square.{v, u} C
φ : X ⟶ Y
⊢ (X.map F).f₁₂ ≫ F.map φ.τ₂ = F.map φ.τ₁ ≫ (Y.map F).f₁₂

Tactic:
simpa only [Functor.map_comp] using F.congr_map φ.comm₁₂

Premises used: CategoryTheory.Square.Hom.comm₁₂, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.congr_map
-- Module: Mathlib.CategoryTheory.Square
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
X Y : Square.{v, u} C
φ : X ⟶ Y
⊢ (X.map F).f₁₃ ≫ F.map φ.τ₃ = F.map φ.τ₁ ≫ (Y.map F).f₁₃

Tactic:
simpa only [Functor.map_comp] using F.congr_map φ.comm₁₃

Premises used: CategoryTheory.Square.Hom.comm₁₃, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.congr_map
-- Module: Mathlib.CategoryTheory.Square
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
X Y : Square.{v, u} C
φ : X ⟶ Y
⊢ (X.map F).f₂₄ ≫ F.map φ.τ₄ = F.map φ.τ₂ ≫ (Y.map F).f₂₄

Tactic:
simpa only [Functor.map_comp] using F.congr_map φ.comm₂₄

Premises used: CategoryTheory.Square.Hom.comm₂₄, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.congr_map
-- Module: Mathlib.CategoryTheory.Square
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
X Y : Square.{v, u} C
φ : X ⟶ Y
⊢ (X.map F).f₃₄ ≫ F.map φ.τ₄ = F.map φ.τ₃ ≫ (Y.map F).f₃₄

Tactic:
simpa only [Functor.map_comp] using F.congr_map φ.comm₃₄

Premises used: CategoryTheory.Square.Hom.comm₃₄, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.congr_map
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F_1 F' F'' : Functor.{v, w, u, w + 1} C (Type w)
G_1 G' F G : Subfunctor F_1
U V : C
x : U ⟶ V
x_1 : F_1.obj U
h : x_1 ∈ F.obj U
⊢ Membership.mem (γ := Set (F_1.obj U))
    ((⇑(hom (FC := TypeCat.Fun) (F_1.map x)) :
        (a : (fun (X : Type w) ↦ X) (F_1.obj U)) → (fun (X : Type w) ↦ X) (F_1.obj V)) ⁻¹'
      (F.obj V ⊔ G.obj V))
    x_1

Tactic:
Or.inl (F.map _ h)

Premises used: Set.union, Set.Mem, setOf, CategoryTheory.Subfunctor.map, Set.preimage, Or.inl
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F_1 F' F'' : Functor.{v, w, u, w + 1} C (Type w)
G_1 G' F G : Subfunctor F_1
U V : C
x : U ⟶ V
x_1 : F_1.obj U
h : x_1 ∈ F.obj U
⊢ Membership.mem (γ := Set (F_1.obj U))
    ((⇑(hom (FC := TypeCat.Fun) (F_1.map x)) :
        (a : (fun (X : Type w) ↦ X) (F_1.obj U)) → (fun (X : Type w) ↦ X) (F_1.obj V)) ⁻¹'
      (F.obj V ⊔ G.obj V))
    x_1

Tactic:
exact Or.inl (F.map _ h)

Premises used: CategoryTheory.Subfunctor.map, Or.inl
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F_1 F' F'' : Functor.{v, w, u, w + 1} C (Type w)
G_1 G' F G : Subfunctor F_1
U V : C
x : U ⟶ V
x_1 : F_1.obj U
h : x_1 ∈ G.obj U
⊢ Membership.mem (γ := Set (F_1.obj U))
    ((⇑(hom (FC := TypeCat.Fun) (F_1.map x)) :
        (a : (fun (X : Type w) ↦ X) (F_1.obj U)) → (fun (X : Type w) ↦ X) (F_1.obj V)) ⁻¹'
      (F.obj V ⊔ G.obj V))
    x_1

Tactic:
Or.inr (G.map _ h)

Premises used: Set.union, Set.Mem, setOf, CategoryTheory.Subfunctor.map, Set.preimage, Or.inr
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F_1 F' F'' : Functor.{v, w, u, w + 1} C (Type w)
G_1 G' F G : Subfunctor F_1
U V : C
x : U ⟶ V
x_1 : F_1.obj U
h : x_1 ∈ G.obj U
⊢ Membership.mem (γ := Set (F_1.obj U))
    ((⇑(hom (FC := TypeCat.Fun) (F_1.map x)) :
        (a : (fun (X : Type w) ↦ X) (F_1.obj U)) → (fun (X : Type w) ↦ X) (F_1.obj V)) ⁻¹'
      (F.obj V ⊔ G.obj V))
    x_1

Tactic:
exact Or.inr (G.map _ h)

Premises used: CategoryTheory.Subfunctor.map, Or.inr
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F F' F'' : Functor.{v, w, u, w + 1} C (Type w)
G G' x x_1 : Subfunctor F
x_2 : C
⊢ x.obj x_2 ≤ Subfunctor.obj { obj := fun (U : C) ↦ x.obj U ⊔ x_1.obj U, map := ⋯ } x_2

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Subfunctor.Basic
Goal:
C : Type u
inst : Category.{v, u} C
F F' F'' : Functor.{v, w, u, w + 1} C (Type w)
G G' x x_1 : Subfunctor F
x_2 : C
⊢ x_1.obj x_2 ≤ Subfunctor.obj { obj := fun (U : C) ↦ x.obj U ⊔ x_1.obj U, map := ⋯ } x_2

Tactic:
simp