awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
inst_2 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
ι' : Type u_2
inst_3 : Finite ι
inst_4 : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
e_3 :
  Eq.{u + 1} (α := C) (∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))
    (Cocone.pt (J := Discrete (ι × ι')) (F :=
      Discrete.functor fun (b : ι × ι') ↦ pullback (X := X b.1) (Y := Y b.2) (f b.1) (g b.2))
      (Cofan.mk (∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))
        (Sigma.ι fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))))
e_5 :
  sigmaObj.{u_2, v, u} Y =
    Cocone.pt.{u_2, v, u_2, u} (J := Discrete ι') (F := Discrete.functor Y)
      (Cofan.mk (sigmaObj.{u_2, v, u} Y) fun (i : ι') ↦ Sigma.ι Y i)
h :
  ∀ (x : C) (x_1 : (b : ι × ι') → pullback (X := X b.1) (Y := Y b.2) (f b.1) (g b.2) ⟶ x) (b : ι × ι'),
    CategoryStruct.comp (Y := ∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))
        (Sigma.ι (C := C) (fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)) b) (Sigma.desc x_1) =
      CategoryStruct.comp (Y := ∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))
        (Sigma.ι (C := C) (fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)) b)
        (Cofan.IsColimit.desc
          (coproductIsCoproduct fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)) x_1)
⊢ Eq (α :=
    {P : C} →
      (p : (b : ι × ι') → pullback (X := X b.1) (Y := Y b.2) (f b.1) (g b.2) ⟶ P) →
        (∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)) ⟶ P)
    (@Sigma.desc (ι × ι') C inst (fun (p : ι × ι') ↦ pullback (f p.1) (g p.2)) ⋯)
    (@Cofan.IsColimit.desc (ι × ι') C inst (fun (b : ι × ι') ↦ pullback (f b.1) (g b.2))
      (Cofan.mk (∐ fun (p : ι × ι') ↦ pullback (f p.1) (g p.2)) (Sigma.ι fun (p : ι × ι') ↦ pullback (f p.1) (g p.2)))
      (coproductIsCoproduct fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)))

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
inst_2 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
ι' : Type u_2
inst_3 : Finite ι
inst_4 : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
e_3 :
  Eq.{u + 1} (α := C) (∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))
    (Cocone.pt (J := Discrete (ι × ι')) (F :=
      Discrete.functor fun (b : ι × ι') ↦ pullback (X := X b.1) (Y := Y b.2) (f b.1) (g b.2))
      (Cofan.mk (∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))
        (Sigma.ι fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))))
e_5 :
  sigmaObj.{u_2, v, u} Y =
    Cocone.pt.{u_2, v, u_2, u} (J := Discrete ι') (F := Discrete.functor Y)
      (Cofan.mk (sigmaObj.{u_2, v, u} Y) fun (i : ι') ↦ Sigma.ι Y i)
x : C
x_1 : (b : ι × ι') → pullback (X := X b.1) (Y := Y b.2) (f b.1) (g b.2) ⟶ x
b : ι × ι'
⊢ CategoryStruct.comp (Y := ∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))
      (Sigma.ι (C := C) (fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)) b) (Sigma.desc x_1) =
    CategoryStruct.comp (Y := ∐ fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))
      (Sigma.ι (C := C) (fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2)) b)
      (Cofan.IsColimit.desc (coproductIsCoproduct fun (p : ι × ι') ↦ pullback (X := X p.1) (Y := Y p.2) (f p.1) (g p.2))
        x_1)

Tactic:
simp [Cofan.IsColimit.desc, Sigma.ι, coproductIsCoproduct]

Premises used: CategoryTheory.Limits.Cofan.IsColimit.desc, CategoryTheory.Limits.Sigma.ι, CategoryTheory.Limits.coproductIsCoproduct
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
inst_2 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
ι' : Type u_2
inst_3 : Finite ι
inst_4 : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
⊢ IsUniversalColimit.{u_1, u_1, v, u} (J := Discrete ι) (F := Discrete.functor X)
    (Cofan.mk (sigmaObj.{u_1, v, u} X) fun (i : ι) ↦ Sigma.ι X i)

Tactic:
FinitaryPreExtensive.isUniversal_finiteCoproducts (coproductIsCoproduct X)

Premises used: CategoryTheory.Limits.coproductIsCoproduct, CategoryTheory.FinitaryPreExtensive.isUniversal_finiteCoproducts
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
inst_2 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
ι' : Type u_2
inst_3 : Finite ι
inst_4 : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
⊢ IsUniversalColimit.{u_1, u_1, v, u} (J := Discrete ι) (F := Discrete.functor X)
    (Cofan.mk (sigmaObj.{u_1, v, u} X) fun (i : ι) ↦ Sigma.ι X i)

Tactic:
exact FinitaryPreExtensive.isUniversal_finiteCoproducts (coproductIsCoproduct X)

Premises used: CategoryTheory.Limits.coproductIsCoproduct, CategoryTheory.FinitaryPreExtensive.isUniversal_finiteCoproducts
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
inst_2 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
ι' : Type u_2
inst_3 : Finite ι
inst_4 : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
⊢ IsUniversalColimit.{u_2, u_2, v, u} (J := Discrete ι') (F := Discrete.functor Y)
    (Cofan.mk (sigmaObj.{u_2, v, u} Y) fun (i : ι') ↦ Sigma.ι Y i)

Tactic:
FinitaryPreExtensive.isUniversal_finiteCoproducts (coproductIsCoproduct Y)

Premises used: CategoryTheory.Limits.coproductIsCoproduct, CategoryTheory.FinitaryPreExtensive.isUniversal_finiteCoproducts
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPullbacks.{v, u} C
inst_2 : FinitaryPreExtensive.{v, u} C
ι : Type u_1
ι' : Type u_2
inst_3 : Finite ι
inst_4 : Finite ι'
S : C
X : ι → C
Y : ι' → C
f : (i : ι) → X i ⟶ S
g : (i : ι') → Y i ⟶ S
⊢ IsUniversalColimit.{u_2, u_2, v, u} (J := Discrete ι') (F := Discrete.functor Y)
    (Cofan.mk (sigmaObj.{u_2, v, u} Y) fun (i : ι') ↦ Sigma.ι Y i)

Tactic:
exact FinitaryPreExtensive.isUniversal_finiteCoproducts (coproductIsCoproduct Y)

Premises used: CategoryTheory.Limits.coproductIsCoproduct, CategoryTheory.FinitaryPreExtensive.isUniversal_finiteCoproducts
-- Module: Mathlib.CategoryTheory.ExtremalEpi
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : ExtremalEpi f
A : Subobject.{v, u} Y
hA : A.Factors f
rw : IsIso A.arrow
⊢ A = ⊤

Tactic:
rw [← Subobject.isIso_arrow_iff_eq_top]

Premises used: CategoryTheory.Subobject.isIso_arrow_iff_eq_top
-- Module: Mathlib.CategoryTheory.ExtremalEpi
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : ExtremalEpi f
A : Subobject.{v, u} Y
hA : A.Factors f
⊢ A.factorThru f hA ≫ A.arrow = f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ExtremalEpi
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : ExtremalEpi f
A : Subobject.{v, u} Y
hA : A.Factors f
⊢ IsIso A.arrow

Tactic:
exact isIso f (Subobject.factorThru A f hA) _ (by simp)

Premises used: CategoryTheory.Subobject.factorThru, CategoryTheory.ExtremalEpi.isIso
-- Module: Mathlib.CategoryTheory.ExtremalEpi
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasEqualizers.{v, u} C
hf : ∀ ⦃Z : C⦄ (p : X ⟶ Z) (i : Z ⟶ Y), p ≫ i = f → ∀ [Mono i], IsIso i
Z : C
p q : Y ⟶ Z
h : f ≫ p = f ≫ q
⊢ CategoryStruct.comp (Y := equalizer p q) (equalizer.lift f h) (equalizer.ι p q) = f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ExtremalEpi
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasEqualizers.{v, u} C
hf : ∀ ⦃Z : C⦄ (p : X ⟶ Z) (i : Z ⟶ Y), p ≫ i = f → ∀ [Mono i], IsIso i
Z : C
p q : Y ⟶ Z
h : f ≫ p = f ≫ q
⊢ IsIso (X := equalizer p q) (equalizer.ι p q)

Tactic:
have := hf (equalizer.lift f h) (equalizer.ι p q) (by simp)
-- Module: Mathlib.CategoryTheory.ExtremalEpi
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasEqualizers.{v, u} C
hf : ∀ ⦃Z : C⦄ (p : X ⟶ Z) (i : Z ⟶ Y), p ≫ i = f → ∀ [Mono i], IsIso i
Z : C
p q : Y ⟶ Z
h : f ≫ p = f ≫ q
this : IsIso (X := equalizer p q) (equalizer.ι p q)
rw : Eq (α := equalizer p q ⟶ Z) (equalizer.ι p q ≫ p) (equalizer.ι p q ≫ q)
rw₁ rw₂ : Eq (α := equalizer p q ⟶ Z) (equalizer.ι p q ≫ q) (equalizer.ι p q ≫ q)
⊢ p = q

Tactic:
rw [← cancel_epi (equalizer.ι p q), equalizer.condition]

Premises used: CategoryTheory.Limits.equalizer.condition, CategoryTheory.Limits.equalizer.ι, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.ExtremalEpi
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasEqualizers.{v, u} C
hf : ∀ ⦃Z : C⦄ (p : X ⟶ Z) (i : Z ⟶ Y), p ≫ i = f → ∀ [Mono i], IsIso i
⊢ ∀ {Z : C} (p : X ⟶ Z) (i : Z ⟶ Y) (fac : p ≫ i = f) [Mono i], IsIso i

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.ExtremalEpi
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : StrongEpi f
Z : C
p : X ⟶ Z
i : Z ⟶ Y
fac : p ≫ i = f
h : Mono i
⊢ CommSq p f i (𝟙 Y)

Tactic:
have sq : CommSq p f i (𝟙 Y) := { }
-- Module: Mathlib.CategoryTheory.ExtremalEpi
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : StrongEpi f
Z : C
p : X ⟶ Z
i : Z ⟶ Y
fac : p ≫ i = f
h : Mono i
sq : CommSq p f i (𝟙 Y)
⊢ i ≫ sq.lift = 𝟙 Z

Tactic:
simp [← cancel_mono i]

Premises used: CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.ExtremalEpi
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : StrongEpi f
Z : C
p : X ⟶ Z
i : Z ⟶ Y
fac : p ≫ i = f
h : Mono i
sq : CommSq p f i (𝟙 Y)
⊢ sq.lift ≫ i = 𝟙 Y

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ExtremalEpi
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : StrongEpi f
Z : C
p : X ⟶ Z
i : Z ⟶ Y
fac : p ≫ i = f
h : Mono i
sq : CommSq p f i (𝟙 Y)
⊢ IsIso i

Tactic:
exact ⟨sq.lift, by simp [← cancel_mono i], by simp⟩
-- Module: Mathlib.CategoryTheory.ExtremalEpi
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasPullbacks.{v, u} C
⊢ ExtremalEpi f ↔ StrongEpi f

Tactic:
⟨fun _ ↦ ⟨inferInstance, fun A B i _ ↦ ⟨fun {t b} sq ↦ ⟨⟨?_⟩⟩⟩⟩,
    fun _ ↦ inferInstance⟩

Premises used: CategoryTheory.StrongEpi.mk, inferInstance, Nonempty.intro, CategoryTheory.HasLiftingProperty.mk, CategoryTheory.CommSq.HasLift.mk, Iff.intro
-- Module: Mathlib.CategoryTheory.ExtremalEpi
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasPullbacks.{v, u} C
refine :
  ExtremalEpi f → (A B : C) → (i : A ⟶ B) → Mono i → {t : X ⟶ A} → {b : Y ⟶ B} → (sq : CommSq t f i b) → sq.LiftStruct
⊢ ExtremalEpi f ↔ StrongEpi f

Tactic:
refine ⟨fun _ ↦ ⟨inferInstance, fun A B i _ ↦ ⟨fun {t b} sq ↦ ⟨⟨?_⟩⟩⟩⟩,
    fun _ ↦ inferInstance⟩
-- Module: Mathlib.CategoryTheory.ExtremalEpi
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasPullbacks.{v, u} C
h : ExtremalEpi f
A B : C
i : A ⟶ B
h_1 : Mono i
t : X ⟶ A
b : Y ⟶ B
sq : CommSq t f i b
⊢ CategoryStruct.comp (Y := pullback i b) (pullback.lift t f ⋯) (pullback.snd i b) = f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.ExtremalEpi
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasPullbacks.{v, u} C
h : ExtremalEpi f
A B : C
i : A ⟶ B
h_1 : Mono i
t : X ⟶ A
b : Y ⟶ B
sq : CommSq t f i b
⊢ IsIso (X := pullback i b) (pullback.snd i b)

Tactic:
have := ExtremalEpi.isIso f (pullback.lift _ _ sq.w)
    (pullback.snd _ _) (by simp)
-- Module: Mathlib.CategoryTheory.ExtremalEpi
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasPullbacks.{v, u} C
h : ExtremalEpi f
A B : C
i : A ⟶ B
h_1 : Mono i
t : X ⟶ A
b : Y ⟶ B
sq : CommSq t f i b
this : IsIso (X := pullback i b) (pullback.snd i b)
rw : f ≫ CategoryStruct.comp (Y := pullback i b) (inv (pullback.snd i b)) (pullback.fst i b ≫ i) = f ≫ b
⊢ f ≫ CategoryStruct.comp (Y := pullback i b) (inv (pullback.snd i b)) (pullback.fst i b) = t

Tactic:
rw [← cancel_mono i, sq.w, Category.assoc, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.cancel_mono, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.ExtremalEpi
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasPullbacks.{v, u} C
h : ExtremalEpi f
A B : C
i : A ⟶ B
h_1 : Mono i
t : X ⟶ A
b : Y ⟶ B
sq : CommSq t f i b
this : IsIso (X := pullback i b) (pullback.snd i b)
e_a : CategoryStruct.comp (Y := pullback i b) (inv (pullback.snd i b)) (pullback.fst i b ≫ i) = b
⊢ f ≫ CategoryStruct.comp (Y := pullback i b) (inv (pullback.snd i b)) (pullback.fst i b ≫ i) = f ≫ b

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.ExtremalEpi
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasPullbacks.{v, u} C
h : ExtremalEpi f
A B : C
i : A ⟶ B
h_1 : Mono i
t : X ⟶ A
b : Y ⟶ B
sq : CommSq t f i b
this : IsIso (X := pullback i b) (pullback.snd i b)
e_a :
  Eq (α := pullback i b ⟶ B)
    (pullback.snd i b ≫ CategoryStruct.comp (Y := pullback i b) (inv (pullback.snd i b)) (pullback.fst i b ≫ i))
    (pullback.snd i b ≫ b)
e_a₁ : Eq (α := pullback i b ⟶ B) (pullback.fst i b ≫ i) (pullback.snd i b ≫ b)
e_a₂ e_a₃ : Eq (α := pullback i b ⟶ B) (pullback.snd i b ≫ b) (pullback.snd i b ≫ b)
⊢ CategoryStruct.comp (Y := pullback i b) (inv (pullback.snd i b)) (pullback.fst i b ≫ i) = b

Tactic:
rw [← cancel_epi (pullback.snd i b), IsIso.hom_inv_id_assoc,
          pullback.condition]

Premises used: CategoryTheory.Limits.pullback.snd, CategoryTheory.IsIso.hom_inv_id_assoc, CategoryTheory.Limits.pullback.condition, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.ExtremalEpi
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasPullbacks.{v, u} C
h : ExtremalEpi f
A B : C
i : A ⟶ B
h_1 : Mono i
t : X ⟶ A
b : Y ⟶ B
sq : CommSq t f i b
this : IsIso (X := pullback i b) (pullback.snd i b)
⊢ CategoryStruct.comp (Y := pullback i b) (inv (pullback.snd i b)) (pullback.fst i b) ≫ i = b

Tactic:
simp [pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.ExtremalEpi
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst_1 : HasPullbacks.{v, u} C
h : ExtremalEpi f
A B : C
i : A ⟶ B
h_1 : Mono i
t : X ⟶ A
b : Y ⟶ B
sq : CommSq t f i b
this : IsIso (X := pullback i b) (pullback.snd i b)
⊢ sq.LiftStruct

Tactic:
exact
    { l := inv (pullback.snd i b) ≫ pullback.fst _ _
      fac_left := by
        rw [← cancel_mono i, sq.w, Category.assoc, Category.assoc]
        congr 1
        rw [← cancel_epi (pullback.snd i b), IsIso.hom_inv_id_assoc,
          pullback.condition]
      fac_right := by simp [pullback.condition] }
-- Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
𝒵 : BasedCategory.{v₄, u₄, v₁, u₁} 𝒮
F : 𝒳 ⥤ᵇ 𝒴
G : 𝒴 ⥤ᵇ 𝒵
rw : F.toFunctor ⋙ G.toFunctor ⋙ 𝒵.p = 𝒳.p
rw₁ : F.toFunctor ⋙ 𝒴.p = 𝒳.p
rw₂ rw₃ : 𝒳.p = 𝒳.p
⊢ (F.toFunctor ⋙ G.toFunctor) ⋙ 𝒵.p = 𝒳.p

Tactic:
rw [Functor.assoc, G.w, F.w]

Premises used: CategoryTheory.Functor.assoc, CategoryTheory.BasedFunctor.w
-- Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
F : 𝒳 ⥤ᵇ 𝒴
⊢ F ⋙ 𝟭 𝒴 = F

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, rfl, CategoryTheory.BasedFunctor.comp
-- Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
F : 𝒳 ⥤ᵇ 𝒴
⊢ 𝟭 𝒳 ⋙ F = F

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, rfl, CategoryTheory.BasedFunctor.comp
-- Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
𝒵 : BasedCategory.{v₄, u₄, v₁, u₁} 𝒮
𝒜 : BasedCategory.{v₅, u₅, v₁, u₁} 𝒮
F : 𝒳 ⥤ᵇ 𝒴
G : 𝒴 ⥤ᵇ 𝒵
H : 𝒵 ⥤ᵇ 𝒜
⊢ (F ⋙ G) ⋙ H = F ⋙ G ⋙ H

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, rfl, CategoryTheory.BasedFunctor.comp
-- Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
F : 𝒳 ⥤ᵇ 𝒴
a : 𝒳.obj
rw : (F.toFunctor ⋙ 𝒴.p).obj a = 𝒳.p.obj a
rw₁ rw₂ : 𝒳.p.obj a = 𝒳.p.obj a
⊢ 𝒴.p.obj (F.obj a) = 𝒳.p.obj a

Tactic:
rw [← Functor.comp_obj, F.w]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.BasedFunctor.w
-- Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
F : 𝒳 ⥤ᵇ 𝒴
a : 𝒳.obj
⊢ 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (𝟙 (F.obj a))

Tactic:
IsHomLift.id (w_obj F a)

Premises used: CategoryTheory.IsHomLift.id, CategoryTheory.BasedFunctor.w_obj
-- Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
F : 𝒳 ⥤ᵇ 𝒴
R S : 𝒮
a b : 𝒳.obj
f : R ⟶ S
φ : a ⟶ b
inst_1 : 𝒳.p.IsHomLift f φ
apply : f = eqToHom ⋯ ≫ 𝒴.p.map (F.map φ) ≫ eqToHom ⋯
⊢ 𝒴.p.IsHomLift f (F.map φ)

Tactic:
apply of_fac 𝒴.p f (F.map φ) (Eq.trans (F.w_obj a) (domain_eq 𝒳.p f φ))
    (Eq.trans (F.w_obj b) (codomain_eq 𝒳.p f φ))

Premises used: CategoryTheory.IsHomLift.of_fac, CategoryTheory.BasedCategory.p, CategoryTheory.IsHomLift.codomain_eq, CategoryTheory.Functor.map, CategoryTheory.BasedFunctor.w_obj, CategoryTheory.BasedFunctor.toFunctor, CategoryTheory.IsHomLift.domain_eq, Eq.trans
-- Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
F : 𝒳 ⥤ᵇ 𝒴
R S : 𝒮
a b : 𝒳.obj
f : R ⟶ S
φ : a ⟶ b
inst_1 : 𝒳.p.IsHomLift f φ
rw : f = eqToHom ⋯ ≫ (eqToHom ⋯ ≫ 𝒳.p.map φ ≫ eqToHom ⋯) ≫ eqToHom ⋯
⊢ f = eqToHom ⋯ ≫ 𝒴.p.map (F.map φ) ≫ eqToHom ⋯

Tactic:
rw [← Functor.comp_map, congr_hom F.w]

Premises used: CategoryTheory.Functor.congr_hom, CategoryTheory.BasedFunctor.w, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
F : 𝒳 ⥤ᵇ 𝒴
R S : 𝒮
a b : 𝒳.obj
f : R ⟶ S
φ : a ⟶ b
inst_1 : 𝒳.p.IsHomLift f φ
⊢ f = eqToHom ⋯ ≫ (eqToHom ⋯ ≫ 𝒳.p.map φ ≫ eqToHom ⋯) ≫ eqToHom ⋯

Tactic:
simpa using (fac 𝒳.p f φ)

Premises used: CategoryTheory.BasedCategory.p, CategoryTheory.IsHomLift.fac
-- Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
F : 𝒳 ⥤ᵇ 𝒴
R S : 𝒮
a b : 𝒳.obj
f : R ⟶ S
φ : a ⟶ b
inst_1 : 𝒴.p.IsHomLift f (F.map φ)
apply : f = eqToHom ⋯ ≫ 𝒳.p.map φ ≫ eqToHom ⋯
⊢ 𝒳.p.IsHomLift f φ

Tactic:
apply of_fac 𝒳.p f φ (F.w_obj a ▸ domain_eq 𝒴.p f (F.map φ))
    (F.w_obj b ▸ codomain_eq 𝒴.p f (F.map φ))

Premises used: CategoryTheory.IsHomLift.of_fac, CategoryTheory.BasedCategory.p, CategoryTheory.IsHomLift.codomain_eq, Eq.rec, CategoryTheory.Functor.map, CategoryTheory.BasedFunctor.w_obj, CategoryTheory.BasedFunctor.toFunctor, CategoryTheory.IsHomLift.domain_eq
-- Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
F : 𝒳 ⥤ᵇ 𝒴
R S : 𝒮
a b : 𝒳.obj
f : R ⟶ S
φ : a ⟶ b
inst_1 : 𝒴.p.IsHomLift f (F.map φ)
⊢ f = eqToHom ⋯ ≫ 𝒳.p.map φ ≫ eqToHom ⋯

Tactic:
simp [congr_hom F.w.symm, fac 𝒴.p f (F.map φ)]

Premises used: CategoryTheory.BasedCategory.p, CategoryTheory.Functor.congr_hom, CategoryTheory.Functor.map, CategoryTheory.BasedFunctor.toFunctor, CategoryTheory.BasedFunctor.w, Eq.symm, CategoryTheory.IsHomLift.fac
-- Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
F : 𝒳 ⥤ᵇ 𝒴
R S : 𝒮
a b : 𝒳.obj
f : R ⟶ S
φ : a ⟶ b
⊢ 𝒴.p.IsHomLift f (F.map φ) ↔ 𝒳.p.IsHomLift f φ

Tactic:
⟨fun _ ↦ isHomLift_map F f φ, fun _ ↦ preserves_isHomLift F f φ⟩

Premises used: CategoryTheory.BasedFunctor.isHomLift_map, Iff.intro, CategoryTheory.BasedFunctor.preserves_isHomLift
-- Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
α β : BasedNatTrans F G
h : α.toNatTrans = β.toNatTrans
mk :
  ∀ (toNatTrans : NatTrans F.toFunctor G.toFunctor)
    (isHomLift' : ∀ (a : 𝒳.obj), 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (toNatTrans.app a))
    (h : { toNatTrans := toNatTrans, isHomLift' := isHomLift' : BasedNatTrans F G }.toNatTrans = β.toNatTrans),
    { toNatTrans := toNatTrans, isHomLift' := isHomLift' : BasedNatTrans F G } = β
⊢ α = β

Tactic:
cases α
-- Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
β : BasedNatTrans F G
toNatTrans : NatTrans F.toFunctor G.toFunctor
isHomLift' : ∀ (a : 𝒳.obj), 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (toNatTrans.app a)
h : { toNatTrans := toNatTrans, isHomLift' := isHomLift' : BasedNatTrans F G }.toNatTrans = β.toNatTrans
mk :
  ∀ (isHomLift' : ∀ (a : 𝒳.obj), 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (β.app a)),
    { toNatTrans := β.toNatTrans, isHomLift' := isHomLift' : BasedNatTrans F G } = β
⊢ { toNatTrans := toNatTrans, isHomLift' := isHomLift' : BasedNatTrans F G } = β

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
β : BasedNatTrans F G
isHomLift' : ∀ (a : 𝒳.obj), 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (β.app a)
⊢ { toNatTrans := β.toNatTrans, isHomLift' := isHomLift' : BasedNatTrans F G } = β

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
α : BasedNatTrans F G
a : 𝒳.obj
⊢ 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.app a)

Tactic:
α.isHomLift' a

Premises used: CategoryTheory.BasedNatTrans.isHomLift'
-- Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
α : BasedNatTrans F G
a : 𝒳.obj
S : 𝒮
ha : 𝒳.p.obj a = S
subst : 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.app a)
⊢ 𝒴.p.IsHomLift (𝟙 S) (α.app a)

Tactic:
subst ha
-- Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
F G : 𝒳 ⥤ᵇ 𝒴
α : BasedNatTrans F G
a : 𝒳.obj
⊢ 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.app a)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
F : 𝒳 ⥤ᵇ 𝒴
a : 𝒳.obj
⊢ 𝟙 (𝒳.p.obj a) = eqToHom ⋯ ≫ 𝒴.p.map ((NatTrans.id F.toFunctor).app a) ≫ eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
F G H : 𝒳 ⥤ᵇ 𝒴
α : BasedNatTrans F G
β : BasedNatTrans G H
a : 𝒳.obj
rw : 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.app a ≫ β.app a)
⊢ 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) ((α.vcomp β.toNatTrans).app a)

Tactic:
rw [CategoryTheory.NatTrans.vcomp_app]

Premises used: CategoryTheory.NatTrans.vcomp_app
-- Module: Mathlib.CategoryTheory.FiberedCategory.BasedCategory
Goal:
𝒮 : Type u₁
inst : Category.{v₁, u₁} 𝒮
𝒳 : BasedCategory.{v₂, u₂, v₁, u₁} 𝒮
𝒴 : BasedCategory.{v₃, u₃, v₁, u₁} 𝒮
F G H : 𝒳 ⥤ᵇ 𝒴
α : BasedNatTrans F G
β : BasedNatTrans G H
a : 𝒳.obj
⊢ 𝒴.p.IsHomLift (𝟙 (𝒳.p.obj a)) (α.app a ≫ β.app a)

Tactic:
infer_instance