awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.FiberedCategory.HasFibers
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : CategoryTheory.Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : HasFibers.{u_1, u_2, v₂, u₂, v₁, u₁} p
S : 𝒮
⊢ Faithful.{u_1, v₂, u_2, u₂} (C := Fib.{u_1, u_2, v₂, u₂, v₁, u₁} p S) (ι S)

Tactic:
Functor.Faithful.of_iso (inducedFunctor.natIso p S).symm

Premises used: CategoryTheory.Iso.symm, CategoryTheory.Functor.Faithful.of_iso, HasFibers.inducedFunctor.natIso
-- Module: Mathlib.CategoryTheory.FiberedCategory.HasFibers
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : CategoryTheory.Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : HasFibers.{u_1, u_2, v₂, u₂, v₁, u₁} p
S : 𝒮
a : Fib.{u_1, u_2, v₂, u₂, v₁, u₁} p S
⊢ p.obj (obj (ι S) a) = S

Tactic:
simp only [← comp_obj, comp_const, const_obj_obj]

Premises used: CategoryTheory.Functor.comp_obj, HasFibers.comp_const, CategoryTheory.Functor.const_obj_obj
-- Module: Mathlib.CategoryTheory.FiberedCategory.HasFibers
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : CategoryTheory.Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : HasFibers.{u_1, u_2, v₂, u₂, v₁, u₁} p
S : 𝒮
a b : Fib.{u_1, u_2, v₂, u₂, v₁, u₁} p S
φ : a ⟶ b
apply : 𝟙 S = eqToHom ⋯ ≫ p.map (CategoryTheory.Functor.map (ι S) φ) ≫ eqToHom ⋯
⊢ p.IsHomLift (a := obj (ι S) a) (𝟙 S) (CategoryTheory.Functor.map (ι S) φ)

Tactic:
apply of_fac p _ _ (proj_eq a) (proj_eq b)

Premises used: CategoryTheory.IsHomLift.of_fac, HasFibers.proj_eq
-- Module: Mathlib.CategoryTheory.FiberedCategory.HasFibers
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : CategoryTheory.Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : HasFibers.{u_1, u_2, v₂, u₂, v₁, u₁} p
S : 𝒮
a b : Fib.{u_1, u_2, v₂, u₂, v₁, u₁} p S
φ : a ⟶ b
rw :
  𝟙 S =
    eqToHom ⋯ ≫
      (eqToHom ⋯ ≫ CategoryTheory.Functor.map (obj (const (Fib.{u_1, u_2, v₂, u₂, v₁, u₁} p S)) S) φ ≫ eqToHom ⋯) ≫
        eqToHom ⋯
⊢ 𝟙 S = eqToHom ⋯ ≫ p.map (CategoryTheory.Functor.map (ι S) φ) ≫ eqToHom ⋯

Tactic:
rw [← Functor.comp_map, Functor.congr_hom (comp_const S)]

Premises used: HasFibers.comp_const, CategoryTheory.Functor.congr_hom, CategoryTheory.Functor.comp_map
-- Module: Mathlib.CategoryTheory.FiberedCategory.HasFibers
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : CategoryTheory.Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : HasFibers.{u_1, u_2, v₂, u₂, v₁, u₁} p
S : 𝒮
a b : Fib.{u_1, u_2, v₂, u₂, v₁, u₁} p S
φ : a ⟶ b
⊢ 𝟙 S =
    eqToHom ⋯ ≫
      (eqToHom ⋯ ≫ CategoryTheory.Functor.map (obj (const (Fib.{u_1, u_2, v₂, u₂, v₁, u₁} p S)) S) φ ≫ eqToHom ⋯) ≫
        eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.FiberedCategory.HasFibers
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : CategoryTheory.Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : HasFibers.{u_1, u_2, v₂, u₂, v₁, u₁} p
S : 𝒮
a b : Fib.{u_1, u_2, v₂, u₂, v₁, u₁} p S
φ : obj (ι S) a ⟶ obj (ι S) b
inst_3 : p.IsHomLift (𝟙 S) φ
⊢ CategoryTheory.Functor.map (ι S) (homMk φ) = φ

Tactic:
simp [Fib.homMk, congr_hom (inducedFunctor_comp p S)]

Premises used: HasFibers.Fib.homMk, CategoryTheory.Functor.congr_hom, HasFibers.inducedFunctor_comp
-- Module: Mathlib.CategoryTheory.FiberedCategory.HasFibers
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : CategoryTheory.Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : HasFibers.{u_1, u_2, v₂, u₂, v₁, u₁} p
S : 𝒮
a b : Fib.{u_1, u_2, v₂, u₂, v₁, u₁} p S
f g : a ⟶ b
h : Eq (α := obj (ι S) a ⟶ obj (ι S) b) (CategoryTheory.Functor.map (ι S) f) (CategoryTheory.Functor.map (ι S) g)
⊢ f = g

Tactic:
(ι S).map_injective h

Premises used: HasFibers.ι, CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.FiberedCategory.HasFibers
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : CategoryTheory.Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : HasFibers.{u_1, u_2, v₂, u₂, v₁, u₁} p
S : 𝒮
a : 𝒳
ha : p.obj a = S
⊢ p.IsHomLift (a := obj.{u_1, v₂, u_2, u₂} (C := Fib.{u_1, u_2, v₂, u₂, v₁, u₁} p S) (ι S) (mk ha)) (𝟙 S)
    (Iso.hom (mkIsoSelf ha))

Tactic:
(Functor.objObjPreimageIso (inducedFunctor p S) (Fiber.mk ha)).hom.2

Premises used: HasFibers.Fib.mk, CategoryTheory.Functor.objObjPreimageIso, CategoryTheory.Functor.Fiber.mk, HasFibers.inducedFunctor, CategoryTheory.Iso.hom, Subtype.property
-- Module: Mathlib.CategoryTheory.FiberedCategory.HasFibers
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : CategoryTheory.Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : HasFibers.{u_1, u_2, v₂, u₂, v₁, u₁} p
inst_3 : p.IsPreFibered
R S : 𝒮
a : 𝒳
f : R ⟶ S
ha : p.obj a = S
rw : 𝟙 R ≫ f
| f

Tactic:
rw [← id_comp f]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.FiberedCategory.HasFibers
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : CategoryTheory.Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : HasFibers.{u_1, u_2, v₂, u₂, v₁, u₁} p
inst_3 : p.IsPreFibered
R S : 𝒮
a : 𝒳
f : R ⟶ S
ha : p.obj a = S
conv :
  p.IsCartesian (a := obj.{u_1, v₂, u_2, u₂} (C := Fib.{u_1, u_2, v₂, u₂, v₁, u₁} p R) (ι R) (mkPullback f ha))
    (𝟙 R ≫ f) (pullbackMap f ha)
⊢ p.IsCartesian (a := obj.{u_1, v₂, u_2, u₂} (C := Fib.{u_1, u_2, v₂, u₂, v₁, u₁} p R) (ι R) (mkPullback f ha)) f
    (pullbackMap f ha)

Tactic:
conv in f => rw [← id_comp f]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.FiberedCategory.HasFibers
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : CategoryTheory.Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : HasFibers.{u_1, u_2, v₂, u₂, v₁, u₁} p
inst_3 : p.IsPreFibered
R S : 𝒮
a : 𝒳
f : R ⟶ S
ha : p.obj a = S
simp :
  p.IsCartesian (a := obj.{u_1, v₂, u_2, u₂} (C := Fib.{u_1, u_2, v₂, u₂, v₁, u₁} p R) (ι R) (mkPullback f ha)) f
    (Iso.hom (Fib.mkIsoSelf ⋯) ≫ IsPreFibered.pullbackMap ha f)
⊢ p.IsCartesian (a := obj.{u_1, v₂, u_2, u₂} (C := Fib.{u_1, u_2, v₂, u₂, v₁, u₁} p R) (ι R) (mkPullback f ha))
    (𝟙 R ≫ f) (pullbackMap f ha)

Tactic:
simp only [id_comp, pullbackMap]

Premises used: HasFibers.pullbackMap, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.FiberedCategory.HasFibers
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : CategoryTheory.Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : HasFibers.{u_1, u_2, v₂, u₂, v₁, u₁} p
inst_3 : p.IsPreFibered
R S : 𝒮
a : 𝒳
f : R ⟶ S
ha : p.obj a = S
⊢ p.IsCartesian (a := obj.{u_1, v₂, u_2, u₂} (C := Fib.{u_1, u_2, v₂, u₂, v₁, u₁} p R) (ι R) (mkPullback f ha)) f
    (Iso.hom (Fib.mkIsoSelf ⋯) ≫ IsPreFibered.pullbackMap ha f)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.FiberedCategory.HasFibers
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : CategoryTheory.Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : HasFibers.{u_1, u_2, v₂, u₂, v₁, u₁} p
R S : 𝒮
a : 𝒳
b b' : Fib.{u_1, u_2, v₂, u₂, v₁, u₁} p R
f : R ⟶ S
ψ : obj (ι R) b' ⟶ a
inst_3 : p.IsCartesian f ψ
φ : obj (ι R) b ⟶ a
inst_4 : p.IsHomLift f φ
⊢ CategoryTheory.Functor.map (ι R) (inducedMap f ψ φ) ≫ ψ = φ

Tactic:
simp only [inducedMap, Fib.map_homMk, IsCartesian.fac]

Premises used: HasFibers.Fib.map_homMk, HasFibers.inducedMap, CategoryTheory.Functor.IsCartesian.fac
-- Module: Mathlib.CategoryTheory.FiberedCategory.HasFibers
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : CategoryTheory.Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : HasFibers.{u_1, u_2, v₂, u₂, v₁, u₁} p
inst_3 : p.IsFibered
R S : 𝒮
a : 𝒳
ha : p.obj a = S
b : Fib.{u_1, u_2, v₂, u₂, v₁, u₁} p R
f : R ⟶ S
φ : obj (ι R) b ⟶ a
inst_4 : p.IsHomLift f φ
⊢ ∃ (b' : Fib.{u_1, u_2, v₂, u₂, v₁, u₁} p R),
    ∃ (τ : b ⟶ b'), ∃ (ψ : obj (ι R) b' ⟶ a), p.IsStronglyCartesian f ψ ∧ CategoryTheory.Functor.map (ι R) τ ≫ ψ = φ

Tactic:
let ψ := pullbackMap f ha
  ⟨mkPullback f ha, inducedMap f ψ φ, ψ, inferInstance, inducedMap_comp f ψ φ⟩

Premises used: HasFibers.inducedMap_comp, inferInstance, HasFibers.mkPullback, HasFibers.pullbackMap, HasFibers.inducedMap, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
a b : 𝒳
φ : a ⟶ b
⊢ p.IsHomLift (p.map φ) φ

Tactic:
.map φ

Premises used: CategoryTheory.Functor.IsHomLift.map
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
a : 𝒳
rw : p.IsHomLift (p.map (𝟙 a)) (𝟙 a)
⊢ p.IsHomLift (𝟙 (p.obj a)) (𝟙 a)

Tactic:
rw [← p.map_id]

Premises used: CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
a : 𝒳
⊢ p.IsHomLift (p.map (𝟙 a)) (𝟙 a)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
R : 𝒮
a : 𝒳
ha : p.obj a = R
refl : p.IsHomLift (𝟙 (p.obj a)) (𝟙 a)
⊢ p.IsHomLift (𝟙 R) (𝟙 a)

Tactic:
cases ha
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
a : 𝒳
⊢ p.IsHomLift (𝟙 (p.obj a)) (𝟙 a)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsHomLift f φ
subst_hom_lift : ∀ {R S : 𝒮} {a_1 b_1 : 𝒳} [p.IsHomLift (p.map φ) φ], p.obj a = p.obj a
⊢ p.obj a = R

Tactic:
subst_hom_lift p f φ
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
a_1 b_1 : 𝒳
φ : a_1 ⟶ b_1
R S : 𝒮
a b : 𝒳
inst_2 : p.IsHomLift (p.map φ) φ
⊢ p.obj a_1 = p.obj a_1

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsHomLift f φ
subst_hom_lift : ∀ {R S : 𝒮} {a_1 b_1 : 𝒳} [p.IsHomLift (p.map φ) φ], p.obj b = p.obj b
⊢ p.obj b = S

Tactic:
subst_hom_lift p f φ
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
a_1 b_1 : 𝒳
φ : a_1 ⟶ b_1
R S : 𝒮
a b : 𝒳
inst_2 : p.IsHomLift (p.map φ) φ
⊢ p.obj b_1 = p.obj b_1

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsHomLift f φ
subst_hom_lift : ∀ {R S : 𝒮} {a_1 b_1 : 𝒳} [inst_3 : p.IsHomLift (p.map φ) φ], p.map φ = eqToHom ⋯ ≫ p.map φ ≫ eqToHom ⋯
⊢ f = eqToHom ⋯ ≫ p.map φ ≫ eqToHom ⋯

Tactic:
subst_hom_lift p f φ
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
a_1 b_1 : 𝒳
φ : a_1 ⟶ b_1
R S : 𝒮
a b : 𝒳
inst_2 : p.IsHomLift (p.map φ) φ
⊢ p.map φ = eqToHom ⋯ ≫ p.map φ ≫ eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsHomLift f φ
subst_hom_lift : ∀ {R S : 𝒮} {a_1 b_1 : 𝒳} [inst_3 : p.IsHomLift (p.map φ) φ], p.map φ = eqToHom ⋯ ≫ p.map φ ≫ eqToHom ⋯
⊢ p.map φ = eqToHom ⋯ ≫ f ≫ eqToHom ⋯

Tactic:
subst_hom_lift p f φ
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsHomLift f φ
⊢ p.map φ ≫ eqToHom ⋯ = eqToHom ⋯ ≫ f

Tactic:
simp only [fac p f φ, eqToHom_trans_assoc, eqToHom_refl, id_comp]

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.eqToHom_trans_assoc, CategoryTheory.Category.id_comp, CategoryTheory.IsHomLift.fac
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
a b : 𝒳
f : p.obj a ⟶ p.obj b
φ : a ⟶ b
inst_2 : p.IsHomLift f φ
⊢ f = p.map φ

Tactic:
simp only [fac p f φ, eqToHom_refl, comp_id, id_comp]

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp, CategoryTheory.IsHomLift.fac
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
ha : p.obj a = R
hb : p.obj b = S
h : f = eqToHom ⋯ ≫ p.map φ ≫ eqToHom hb
subst : p.IsHomLift (eqToHom ⋯ ≫ p.map φ ≫ eqToHom ⋯) φ
⊢ p.IsHomLift f φ

Tactic:
subst ha hb h
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
a b : 𝒳
φ : a ⟶ b
⊢ p.IsHomLift (eqToHom ⋯ ≫ p.map φ ≫ eqToHom ⋯) φ

Tactic:
simp
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
ha : p.obj a = R
hb : p.obj b = S
h : p.map φ = eqToHom ha ≫ f ≫ eqToHom ⋯
subst : ∀ (f : p.obj a ⟶ p.obj b) (h : p.map φ = eqToHom ⋯ ≫ f ≫ eqToHom ⋯), p.IsHomLift f φ
⊢ p.IsHomLift f φ

Tactic:
subst ha hb
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
a b : 𝒳
φ : a ⟶ b
f : p.obj a ⟶ p.obj b
h : p.map φ = eqToHom ⋯ ≫ f ≫ eqToHom ⋯
⊢ f = p.map φ

Tactic:
simpa using h.symm

Premises used: Eq.symm
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
a b : 𝒳
φ : a ⟶ b
f : p.obj a ⟶ p.obj b
h : p.map φ = eqToHom ⋯ ≫ f ≫ eqToHom ⋯
obtain : ∀ (h : p.map φ = eqToHom ⋯ ≫ p.map φ ≫ eqToHom ⋯), p.IsHomLift (p.map φ) φ
⊢ p.IsHomLift f φ

Tactic:
obtain rfl : f = p.map φ := by simpa using h.symm

Premises used: CategoryTheory.Functor.map, rfl
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
a b : 𝒳
φ : a ⟶ b
h : p.map φ = eqToHom ⋯ ≫ p.map φ ≫ eqToHom ⋯
⊢ p.IsHomLift (p.map φ) φ

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
ha : p.obj a = R
hb : p.obj b = S
h : p.map φ ≫ eqToHom hb = eqToHom ha ≫ f
subst : ∀ (f : p.obj a ⟶ p.obj b) (h : p.map φ ≫ eqToHom ⋯ = eqToHom ⋯ ≫ f), p.IsHomLift f φ
⊢ p.IsHomLift f φ

Tactic:
subst ha hb
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
a b : 𝒳
φ : a ⟶ b
f : p.obj a ⟶ p.obj b
h : p.map φ ≫ eqToHom ⋯ = eqToHom ⋯ ≫ f
⊢ f = p.map φ

Tactic:
simpa using h.symm

Premises used: Eq.symm
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
a b : 𝒳
φ : a ⟶ b
f : p.obj a ⟶ p.obj b
h : p.map φ ≫ eqToHom ⋯ = eqToHom ⋯ ≫ f
obtain : ∀ (h : p.map φ ≫ eqToHom ⋯ = eqToHom ⋯ ≫ p.map φ), p.IsHomLift (p.map φ) φ
⊢ p.IsHomLift f φ

Tactic:
obtain rfl : f = p.map φ := by simpa using h.symm

Premises used: CategoryTheory.Functor.map, rfl
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
a b : 𝒳
φ : a ⟶ b
h : p.map φ ≫ eqToHom ⋯ = eqToHom ⋯ ≫ p.map φ
⊢ p.IsHomLift (p.map φ) φ

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
ha : p.obj a = R
hb : p.obj b = S
h : CommSq (p.map φ) (eqToHom ha) (eqToHom hb) f
⊢ p.IsHomLift f φ

Tactic:
of_commsq p f φ ha hb h.1

Premises used: CategoryTheory.IsHomLift.of_commsq, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst_2 : p.IsHomLift f φ
inst_3 : p.IsHomLift g ψ
h : CommSq (p.map (φ ≫ ψ)) (eqToHom ⋯) (eqToHom ⋯) (f ≫ g)
ha : p.obj a = R
hb : p.obj c = T
⊢ p.IsHomLift (f ≫ g) (φ ≫ ψ)

Tactic:
apply of_commSq

Premises used: CategoryTheory.IsHomLift.of_commSq
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst_2 : p.IsHomLift f φ
inst_3 : p.IsHomLift g ψ
h : CommSq (p.map φ ≫ p.map ψ) (eqToHom ⋯) (eqToHom ⋯) (f ≫ g)
⊢ CommSq (p.map (φ ≫ ψ)) (eqToHom ⋯) (eqToHom ⋯) (f ≫ g)

Tactic:
rw [p.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst_2 : p.IsHomLift f φ
inst_3 : p.IsHomLift g ψ
h : CommSq (p.map φ ≫ p.map ψ) (eqToHom ⋯) (eqToHom ⋯) (f ≫ g)
⊢ CommSq (p.map (φ ≫ ψ)) (eqToHom ⋯) (eqToHom ⋯) (f ≫ g)

Tactic:
on_goal 1 => rw [p.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
R : 𝒮
a b c : 𝒳
φ : a ⟶ b
ψ : b ⟶ c
inst_2 : p.IsHomLift (𝟙 R) φ
inst_3 : p.IsHomLift (𝟙 R) ψ
⊢ p.IsHomLift (𝟙 R) (φ ≫ ψ)

Tactic:
comp_id (𝟙 R) ▸ comp p (𝟙 R) (𝟙 R) φ ψ

Premises used: CategoryTheory.CategoryStruct.id, Eq.rec, CategoryTheory.IsHomLift.comp, CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
a b c : 𝒳
S T : 𝒮
f : S ⟶ T
φ : a ⟶ b
inst_2 : p.IsHomLift f φ
ψ : b ⟶ c
inst_3 : p.IsHomLift (𝟙 T) ψ
⊢ p.IsHomLift f (φ ≫ ψ)

Tactic:
simpa using (inferInstance : p.IsHomLift (f ≫ 𝟙 T) (φ ≫ ψ))

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
R S : 𝒮
a b c : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsHomLift f φ
T : 𝒮
ψ : b ⟶ c
inst_3 : p.IsHomLift (𝟙 T) ψ
rw : p.obj b = T
rw₁ rw₂ : T = T
⊢ S = T

Tactic:
rw [← codomain_eq p f φ, domain_eq p (𝟙 T) ψ]

Premises used: CategoryTheory.IsHomLift.codomain_eq, CategoryTheory.CategoryStruct.id, CategoryTheory.IsHomLift.domain_eq
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
R S : 𝒮
a b c : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsHomLift f φ
T : 𝒮
ψ : b ⟶ c
inst_3 : p.IsHomLift (𝟙 T) ψ
⊢ p.IsHomLift (𝟙 S) ψ

Tactic:
obtain rfl : S = T := by rw [← codomain_eq p f φ, domain_eq p (𝟙 T) ψ]

Premises used: rfl
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
R S : 𝒮
a b c : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsHomLift f φ
ψ : b ⟶ c
inst_3 : p.IsHomLift (𝟙 S) ψ
⊢ p.IsHomLift f (φ ≫ ψ)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
a b c : 𝒳
S T : 𝒮
f : S ⟶ T
ψ : b ⟶ c
inst_2 : p.IsHomLift f ψ
φ : a ⟶ b
inst_3 : p.IsHomLift (𝟙 S) φ
⊢ p.IsHomLift f (φ ≫ ψ)

Tactic:
simpa using (inferInstance : p.IsHomLift (𝟙 S ≫ f) (φ ≫ ψ))

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
a b c : 𝒳
R : 𝒮
φ : a ⟶ b
inst_2 : p.IsHomLift (𝟙 R) φ
S T : 𝒮
f : S ⟶ T
ψ : b ⟶ c
inst_3 : p.IsHomLift f ψ
rw : p.obj b = S
rw₁ rw₂ : S = S
⊢ R = S

Tactic:
rw [← codomain_eq p (𝟙 R) φ, domain_eq p f ψ]

Premises used: CategoryTheory.IsHomLift.codomain_eq, CategoryTheory.CategoryStruct.id, CategoryTheory.IsHomLift.domain_eq
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
a b c : 𝒳
R : 𝒮
φ : a ⟶ b
inst_2 : p.IsHomLift (𝟙 R) φ
S T : 𝒮
f : S ⟶ T
ψ : b ⟶ c
inst_3 : p.IsHomLift f ψ
obtain : ∀ (f : R ⟶ T) [p.IsHomLift f ψ], p.IsHomLift f (φ ≫ ψ)
⊢ p.IsHomLift f (φ ≫ ψ)

Tactic:
obtain rfl : R = S := by rw [← codomain_eq p (𝟙 R) φ, domain_eq p f ψ]

Premises used: rfl
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
a b c : 𝒳
R : 𝒮
φ : a ⟶ b
inst_2 : p.IsHomLift (𝟙 R) φ
T : 𝒮
ψ : b ⟶ c
f : R ⟶ T
inst_3 : p.IsHomLift f ψ
⊢ p.IsHomLift f (φ ≫ ψ)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
a b : 𝒳
hab : a = b
R : 𝒮
hR : p.obj a = R
subst : p.IsHomLift (𝟙 (p.obj a)) (eqToHom ⋯)
⊢ p.IsHomLift (𝟙 R) (eqToHom hab)

Tactic:
subst hR hab
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
a : 𝒳
⊢ p.IsHomLift (𝟙 (p.obj a)) (eqToHom ⋯)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
a b : 𝒳
hab : a = b
S : 𝒮
hS : p.obj b = S
subst : p.IsHomLift (𝟙 (p.obj a)) (eqToHom ⋯)
⊢ p.IsHomLift (𝟙 S) (eqToHom hab)

Tactic:
subst hS hab
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
R S : 𝒮
hRS : R = S
a : 𝒳
ha : p.obj a = R
subst : p.IsHomLift (eqToHom ⋯) (𝟙 a)
⊢ p.IsHomLift (eqToHom hRS) (𝟙 a)

Tactic:
subst hRS ha
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
a : 𝒳
⊢ p.IsHomLift (eqToHom ⋯) (𝟙 a)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
R S : 𝒮
hRS : R = S
b : 𝒳
hb : p.obj b = S
subst : p.IsHomLift (eqToHom ⋯) (𝟙 b)
⊢ p.IsHomLift (eqToHom hRS) (𝟙 b)

Tactic:
subst hRS hb
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
b : 𝒳
⊢ p.IsHomLift (eqToHom ⋯) (𝟙 b)

Tactic:
simp