awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.FiberedCategory.Fiber
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
S : 𝒮
a b c : 𝒳
φ : a ⟶ b
ψ : b ⟶ c
inst_2 : p.IsHomLift (𝟙 S) φ
inst_3 : p.IsHomLift (𝟙 S) ψ
⊢ Eq (α := mk ⋯ ⟶ mk ⋯)
    (CategoryStruct.comp (Y := mk ⋯) (homMk p S φ : mk ⋯ ⟶ mk ⋯) (homMk p S ψ : mk ⋯ ⟶ mk ⋯) : mk ⋯ ⟶ mk ⋯)
    (homMk p S (φ ≫ ψ) : mk ⋯ ⟶ mk ⋯)

Tactic:
rfl

Premises used: CategoryTheory.Functor.Fiber.homMk, rfl
-- Module: Mathlib.CategoryTheory.FiberedCategory.Fiber
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p_1 : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
S_1 : 𝒮
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
S : 𝒮
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₃, v₂, u₃, u₂} C 𝒳
hF : F ⋙ p = obj (const C) S
x : C
⊢ p.obj (F.obj x) = S

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

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.const_obj_obj
-- Module: Mathlib.CategoryTheory.FiberedCategory.Fiber
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p_1 : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
S_1 : 𝒮
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
S : 𝒮
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₃, v₂, u₃, u₂} C 𝒳
hF : F ⋙ p = obj (const C) S
X Y : C
φ : X ⟶ Y
⊢ p.map (F.map φ) ≫ eqToHom ⋯ = eqToHom ⋯ ≫ 𝟙 S

Tactic:
simpa using (eqToIso hF).hom.naturality φ

Premises used: CategoryTheory.eqToIso, CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.FiberedCategory.Fiber
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
S : 𝒮
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₃, v₂, u₃, u₂} C 𝒳
hF : F ⋙ p = obj (const C) S
⊢ inducedFunctor hF ⋙ fiberInclusion = F

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, rfl
-- Module: Mathlib.CategoryTheory.FiberedCategory.Fiber
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
S : 𝒮
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₃, v₂, u₃, u₂} C 𝒳
hF : F ⋙ p = obj (const C) S
X : C
⊢ obj fiberInclusion ((inducedFunctor hF).obj X) = F.obj X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.FiberedCategory.Fiber
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
S : 𝒮
C : Type u₃
inst_2 : Category.{v₃, u₃} C
F : Functor.{v₃, v₂, u₃, u₂} C 𝒳
hF : F ⋙ p = obj (const C) S
X Y : C
f : X ⟶ Y
⊢ map fiberInclusion ((inducedFunctor hF).map f) = F.map f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.FiberedCategory.Fibered
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : p.IsPreFibered
a : 𝒳
R S : 𝒮
ha : p.obj a = S
f : R ⟶ S
subst : ∀ (f : R ⟶ p.obj a), ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsCartesian f φ
⊢ ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsCartesian f φ

Tactic:
subst ha
-- Module: Mathlib.CategoryTheory.FiberedCategory.Fibered
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : p.IsPreFibered
a : 𝒳
R : 𝒮
f : R ⟶ p.obj a
⊢ ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsCartesian f φ

Tactic:
IsPreFibered.exists_isCartesian' f

Premises used: CategoryTheory.Functor.IsPreFibered.exists_isCartesian'
-- Module: Mathlib.CategoryTheory.FiberedCategory.Fibered
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : p.IsPreFibered
a : 𝒳
R : 𝒮
f : R ⟶ p.obj a
⊢ ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsCartesian f φ

Tactic:
exact IsPreFibered.exists_isCartesian' f

Premises used: CategoryTheory.Functor.IsPreFibered.exists_isCartesian'
-- Module: Mathlib.CategoryTheory.FiberedCategory.Fibered
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : p.IsFibered
R S T : 𝒮
f : R ⟶ S
g : S ⟶ T
a b c : 𝒳
φ : a ⟶ b
ψ : b ⟶ c
inst_3 : p.IsCartesian f φ
inst_4 : p.IsCartesian g ψ
⊢ p.IsCartesian (f ≫ g) (φ ≫ ψ)

Tactic:
IsFibered.comp f g φ ψ

Premises used: CategoryTheory.Functor.IsFibered.comp
-- Module: Mathlib.CategoryTheory.FiberedCategory.Fibered
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : p.IsPreFibered
R S : 𝒮
a : 𝒳
ha : p.obj a = S
f : R ⟶ S
⊢ p.IsCartesian (a := pullbackObj ha f) f (pullbackMap ha f)

Tactic:
Classical.choose_spec (Classical.choose_spec (IsPreFibered.exists_isCartesian p ha f))

Premises used: Classical.choose_spec, CategoryTheory.Functor.IsPreFibered.pullbackObj, CategoryTheory.Functor.IsPreFibered.pullbackMap, CategoryTheory.IsPreFibered.exists_isCartesian
-- Module: Mathlib.CategoryTheory.FiberedCategory.Fibered
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : p.IsPreFibered
R S : 𝒮
a : 𝒳
ha : p.obj a = S
f : R ⟶ S
⊢ p.obj (pullbackObj ha f) = R

Tactic:
domain_eq p f (pullbackMap ha f)

Premises used: CategoryTheory.IsHomLift.domain_eq, CategoryTheory.Functor.IsPreFibered.pullbackMap
-- Module: Mathlib.CategoryTheory.FiberedCategory.Fibered
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : p.IsFibered
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst_3 : p.IsCartesian f φ
a' : 𝒳
g : p.obj a' ⟶ R
φ' : a' ⟶ b
hφ' : p.IsHomLift (g ≫ f) φ'
ψ : pullbackObj ⋯ g ⟶ a := pullbackMap ⋯ g
τ : a' ⟶ pullbackObj ⋯ g := IsCartesian.map p (g ≫ f) (ψ ≫ φ) φ'
h :
  (fun (χ : a' ⟶ a) ↦ p.IsHomLift g χ ∧ χ ≫ φ = φ') (τ ≫ ψ) ∧
    ∀ (y : a' ⟶ a), (fun (χ : a' ⟶ a) ↦ p.IsHomLift g χ ∧ χ ≫ φ = φ') y → y = τ ≫ ψ
⊢ ∃! χ : a' ⟶ a, p.IsHomLift g χ ∧ χ ≫ φ = φ'

Tactic:
use τ ≫ ψ
-- Module: Mathlib.CategoryTheory.FiberedCategory.Fibered
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : p.IsFibered
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst_3 : p.IsCartesian f φ
a' : 𝒳
g : p.obj a' ⟶ R
φ' : a' ⟶ b
hφ' : p.IsHomLift (g ≫ f) φ'
ψ : pullbackObj ⋯ g ⟶ a := pullbackMap ⋯ g
τ : a' ⟶ pullbackObj ⋯ g := IsCartesian.map p (g ≫ f) (ψ ≫ φ) φ'
⊢ (τ ≫ ψ) ≫ φ = φ'

Tactic:
simp only [assoc, IsCartesian.fac, τ]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.IsCartesian.fac
-- Module: Mathlib.CategoryTheory.FiberedCategory.Fibered
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : p.IsFibered
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst_3 : p.IsCartesian f φ
a' : 𝒳
g : p.obj a' ⟶ R
φ' : a' ⟶ b
hφ' : p.IsHomLift (g ≫ f) φ'
ψ : pullbackObj ⋯ g ⟶ a := pullbackMap ⋯ g
τ : a' ⟶ pullbackObj ⋯ g := IsCartesian.map p (g ≫ f) (ψ ≫ φ) φ'
h : ∀ (y : a' ⟶ a), (fun (χ : a' ⟶ a) ↦ p.IsHomLift g χ ∧ χ ≫ φ = φ') y → y = τ ≫ ψ
⊢ (fun (χ : a' ⟶ a) ↦ p.IsHomLift g χ ∧ χ ≫ φ = φ') (τ ≫ ψ) ∧
    ∀ (y : a' ⟶ a), (fun (χ : a' ⟶ a) ↦ p.IsHomLift g χ ∧ χ ≫ φ = φ') y → y = τ ≫ ψ

Tactic:
refine ⟨⟨inferInstance, by simp only [assoc, IsCartesian.fac, τ]⟩, ?_⟩
-- Module: Mathlib.CategoryTheory.FiberedCategory.Fibered
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : p.IsFibered
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst_3 : p.IsCartesian f φ
a' : 𝒳
g : p.obj a' ⟶ R
φ' : a' ⟶ b
hφ' : p.IsHomLift (g ≫ f) φ'
ψ : pullbackObj ⋯ g ⟶ a := pullbackMap ⋯ g
τ : a' ⟶ pullbackObj ⋯ g := IsCartesian.map p (g ≫ f) (ψ ≫ φ) φ'
π : a' ⟶ a
h : ∀ (hπ : p.IsHomLift g π) (hπ_comp : π ≫ φ = φ'), π = τ ≫ ψ
⊢ (fun (χ : a' ⟶ a) ↦ p.IsHomLift g χ ∧ χ ≫ φ = φ') π → π = τ ≫ ψ

Tactic:
⟨hπ, hπ_comp⟩
-- Module: Mathlib.CategoryTheory.FiberedCategory.Fibered
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : p.IsFibered
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst_3 : p.IsCartesian f φ
a' : 𝒳
g : p.obj a' ⟶ R
φ' : a' ⟶ b
hφ' : p.IsHomLift (g ≫ f) φ'
ψ : pullbackObj ⋯ g ⟶ a := pullbackMap ⋯ g
τ : a' ⟶ pullbackObj ⋯ g := IsCartesian.map p (g ≫ f) (ψ ≫ φ) φ'
π : a' ⟶ a
hπ : p.IsHomLift g π
hπ_comp : π ≫ φ = φ'
h : IsCartesian.map p g ψ π ≫ ψ = τ ≫ ψ
⊢ π = τ ≫ ψ

Tactic:
rw [← fac p g ψ π]

Premises used: CategoryTheory.Functor.IsCartesian.fac
-- Module: Mathlib.CategoryTheory.FiberedCategory.Fibered
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : p.IsFibered
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst_3 : p.IsCartesian f φ
a' : 𝒳
g : p.obj a' ⟶ R
φ' : a' ⟶ b
hφ' : p.IsHomLift (g ≫ f) φ'
ψ : pullbackObj ⋯ g ⟶ a := pullbackMap ⋯ g
τ : a' ⟶ pullbackObj ⋯ g := IsCartesian.map p (g ≫ f) (ψ ≫ φ) φ'
π : a' ⟶ a
hπ : p.IsHomLift g π
hπ_comp : π ≫ φ = φ'
h : IsCartesian.map p g ψ π = τ
⊢ IsCartesian.map p g ψ π ≫ ψ = τ ≫ ψ

Tactic:
congr 1
-- Module: Mathlib.CategoryTheory.FiberedCategory.Fibered
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : p.IsFibered
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst_3 : p.IsCartesian f φ
a' : 𝒳
g : p.obj a' ⟶ R
φ' : a' ⟶ b
hφ' : p.IsHomLift (g ≫ f) φ'
ψ : pullbackObj ⋯ g ⟶ a := pullbackMap ⋯ g
τ : a' ⟶ pullbackObj ⋯ g := IsCartesian.map p (g ≫ f) (ψ ≫ φ) φ'
π : a' ⟶ a
hπ : p.IsHomLift g π
hπ_comp : π ≫ φ = φ'
h : IsCartesian.map p g ψ π ≫ ψ ≫ φ = φ'
⊢ IsCartesian.map p g ψ π = τ

Tactic:
apply map_uniq

Premises used: CategoryTheory.Functor.IsCartesian.map_uniq
-- Module: Mathlib.CategoryTheory.FiberedCategory.Fibered
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : p.IsFibered
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst_3 : p.IsCartesian f φ
a' : 𝒳
g : p.obj a' ⟶ R
φ' : a' ⟶ b
hφ' : p.IsHomLift (g ≫ f) φ'
ψ : pullbackObj ⋯ g ⟶ a := pullbackMap ⋯ g
τ : a' ⟶ pullbackObj ⋯ g := IsCartesian.map p (g ≫ f) (ψ ≫ φ) φ'
π : a' ⟶ a
hπ : p.IsHomLift g π
hπ_comp : π ≫ φ = φ'
h : (IsCartesian.map p g ψ π ≫ ψ) ≫ φ = φ'
h₁ h₂ h₃ h₄ : π ≫ φ = φ'
⊢ IsCartesian.map p g ψ π ≫ ψ ≫ φ = φ'

Tactic:
rwa [← assoc, IsCartesian.fac]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.IsCartesian.fac
-- Module: Mathlib.CategoryTheory.FiberedCategory.Fibered
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsStronglyCartesian f φ
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst_2 : p.IsCartesian f φ
universal_property' :
  ∀ {a' : 𝒳} (g : p.obj a' ⟶ R) (φ' : a' ⟶ b) [p.IsHomLift (g ≫ f) φ'], ∃! χ : a' ⟶ a, p.IsHomLift g χ ∧ χ ≫ φ = φ'
⊢ p.IsStronglyCartesian f φ

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.FiberedCategory.Fibered
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsStronglyCartesian f φ
R S : 𝒮
f : R ⟶ S
a b : 𝒳
φ : a ⟶ b
inst_2 : p.IsCartesian f φ
c : 𝒳
g : p.obj c ⟶ R
φ' : c ⟶ b
hφ' : p.IsHomLift (g ≫ f) φ'
universal_property' :
  ∀ {R S : 𝒮} {a_1 b_1 : 𝒳} (g : p.obj c ⟶ p.obj a) [p.IsCartesian (p.map φ) φ] [hφ' : p.IsHomLift (g ≫ p.map φ) φ'],
    ∃! χ : c ⟶ a, p.IsHomLift g χ ∧ χ ≫ φ = φ'
⊢ ∃! χ : c ⟶ a, p.IsHomLift g χ ∧ χ ≫ φ = φ'

Tactic:
subst_hom_lift p f φ
-- Module: Mathlib.CategoryTheory.FiberedCategory.Fibered
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsStronglyCartesian f φ
a b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst_2 : p.IsCartesian (p.map φ) φ
hφ' : p.IsHomLift (g ≫ p.map φ) φ'
universal_property' :
  ∀ (a' : 𝒳) (ψ : a' ⟶ b) (hψ : p.IsStronglyCartesian (p.map φ) ψ), ∃! χ : c ⟶ a, p.IsHomLift g χ ∧ χ ≫ φ = φ'
⊢ ∃! χ : c ⟶ a, p.IsHomLift g χ ∧ χ ≫ φ = φ'

Tactic:
obtain ⟨a', ψ, hψ⟩ := h _ _ (p.map φ)

Premises used: CategoryTheory.Functor.map
-- Module: Mathlib.CategoryTheory.FiberedCategory.Fibered
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsStronglyCartesian f φ
a b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst_2 : p.IsCartesian (p.map φ) φ
hφ' : p.IsHomLift (g ≫ p.map φ) φ'
a' : 𝒳
ψ : a' ⟶ b
hψ : p.IsStronglyCartesian (p.map φ) ψ
τ' : c ⟶ a' := IsStronglyCartesian.map p (p.map φ) ψ (R' := p.obj c) (g := g) ⋯ φ'
Φ : a' ≅ a := domainUniqueUpToIso p (p.map φ) φ ψ
h₁ :
  (fun (χ : c ⟶ a) ↦ p.IsHomLift g χ ∧ χ ≫ φ = φ') (τ' ≫ Φ.hom) ∧
    ∀ (y : c ⟶ a), (fun (χ : c ⟶ a) ↦ p.IsHomLift g χ ∧ χ ≫ φ = φ') y → y = τ' ≫ Φ.hom
⊢ ∃! χ : c ⟶ a, p.IsHomLift g χ ∧ χ ≫ φ = φ'

Tactic:
use τ' ≫ Φ.hom

Premises used: CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.FiberedCategory.Fibered
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsStronglyCartesian f φ
a b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst_2 : p.IsCartesian (p.map φ) φ
hφ' : p.IsHomLift (g ≫ p.map φ) φ'
a' : 𝒳
ψ : a' ⟶ b
hψ : p.IsStronglyCartesian (p.map φ) ψ
τ' : c ⟶ a' := IsStronglyCartesian.map p (p.map φ) ψ (R' := p.obj c) (g := g) ⋯ φ'
Φ : a' ≅ a := domainUniqueUpToIso p (p.map φ) φ ψ
simp : p.IsHomLift g (τ' ≫ (domainUniqueUpToIso p (p.map φ) φ ψ).hom)
⊢ p.IsHomLift g (τ' ≫ Φ.hom)

Tactic:
simp only [Φ]
-- Module: Mathlib.CategoryTheory.FiberedCategory.Fibered
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsStronglyCartesian f φ
a b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst_2 : p.IsCartesian (p.map φ) φ
hφ' : p.IsHomLift (g ≫ p.map φ) φ'
a' : 𝒳
ψ : a' ⟶ b
hψ : p.IsStronglyCartesian (p.map φ) ψ
τ' : c ⟶ a' := IsStronglyCartesian.map p (p.map φ) ψ (R' := p.obj c) (g := g) ⋯ φ'
Φ : a' ≅ a := domainUniqueUpToIso p (p.map φ) φ ψ
⊢ p.IsHomLift g (τ' ≫ (domainUniqueUpToIso p (p.map φ) φ ψ).hom)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.FiberedCategory.Fibered
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsStronglyCartesian f φ
a b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst_2 : p.IsCartesian (p.map φ) φ
hφ' : p.IsHomLift (g ≫ p.map φ) φ'
a' : 𝒳
ψ : a' ⟶ b
hψ : p.IsStronglyCartesian (p.map φ) ψ
τ' : c ⟶ a' := IsStronglyCartesian.map p (p.map φ) ψ (R' := p.obj c) (g := g) ⋯ φ'
Φ : a' ≅ a := domainUniqueUpToIso p (p.map φ) φ ψ
h₁ : (τ' ≫ Φ.hom) ≫ φ = φ'
h₂ : ∀ (y : c ⟶ a), (fun (χ : c ⟶ a) ↦ p.IsHomLift g χ ∧ χ ≫ φ = φ') y → y = τ' ≫ Φ.hom
⊢ (fun (χ : c ⟶ a) ↦ p.IsHomLift g χ ∧ χ ≫ φ = φ') (τ' ≫ Φ.hom) ∧
    ∀ (y : c ⟶ a), (fun (χ : c ⟶ a) ↦ p.IsHomLift g χ ∧ χ ≫ φ = φ') y → y = τ' ≫ Φ.hom

Tactic:
refine ⟨⟨by simp only [Φ]; infer_instance, ?_⟩, ?_⟩
-- Module: Mathlib.CategoryTheory.FiberedCategory.Fibered
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsStronglyCartesian f φ
a b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst_2 : p.IsCartesian (p.map φ) φ
hφ' : p.IsHomLift (g ≫ p.map φ) φ'
a' : 𝒳
ψ : a' ⟶ b
hψ : p.IsStronglyCartesian (p.map φ) ψ
τ' : c ⟶ a' := IsStronglyCartesian.map p (p.map φ) ψ (R' := p.obj c) (g := g) ⋯ φ'
Φ : a' ≅ a := domainUniqueUpToIso p (p.map φ) φ ψ
⊢ (τ' ≫ Φ.hom) ≫ φ = φ'

Tactic:
simp [τ', Φ]
-- Module: Mathlib.CategoryTheory.FiberedCategory.Fibered
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsStronglyCartesian f φ
a b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst_2 : p.IsCartesian (p.map φ) φ
hφ' : p.IsHomLift (g ≫ p.map φ) φ'
a' : 𝒳
ψ : a' ⟶ b
hψ : p.IsStronglyCartesian (p.map φ) ψ
τ' : c ⟶ a' := IsStronglyCartesian.map p (p.map φ) ψ (R' := p.obj c) (g := g) ⋯ φ'
Φ : a' ≅ a := domainUniqueUpToIso p (p.map φ) φ ψ
π : c ⟶ a
h₁ : ∀ (hπ : p.IsHomLift g π) (hπ_comp : π ≫ φ = φ'), π = τ' ≫ Φ.hom
⊢ (fun (χ : c ⟶ a) ↦ p.IsHomLift g χ ∧ χ ≫ φ = φ') π → π = τ' ≫ Φ.hom

Tactic:
⟨hπ, hπ_comp⟩
-- Module: Mathlib.CategoryTheory.FiberedCategory.Fibered
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsStronglyCartesian f φ
a b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst_2 : p.IsCartesian (p.map φ) φ
hφ' : p.IsHomLift (g ≫ p.map φ) φ'
a' : 𝒳
ψ : a' ⟶ b
hψ : p.IsStronglyCartesian (p.map φ) ψ
τ' : c ⟶ a' := IsStronglyCartesian.map p (p.map φ) ψ (R' := p.obj c) (g := g) ⋯ φ'
Φ : a' ≅ a := domainUniqueUpToIso p (p.map φ) φ ψ
π : c ⟶ a
hπ : p.IsHomLift g π
hπ_comp : π ≫ φ = φ'
h₁ : π ≫ Φ.inv = τ'
⊢ π = τ' ≫ Φ.hom

Tactic:
rw [← Iso.comp_inv_eq]

Premises used: CategoryTheory.Iso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.FiberedCategory.Fibered
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsStronglyCartesian f φ
a b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst_2 : p.IsCartesian (p.map φ) φ
hφ' : p.IsHomLift (g ≫ p.map φ) φ'
a' : 𝒳
ψ : a' ⟶ b
hψ : p.IsStronglyCartesian (p.map φ) ψ
τ' : c ⟶ a' := IsStronglyCartesian.map p (p.map φ) ψ (R' := p.obj c) (g := g) ⋯ φ'
Φ : a' ≅ a := domainUniqueUpToIso p (p.map φ) φ ψ
π : c ⟶ a
hπ : p.IsHomLift g π
hπ_comp : π ≫ φ = φ'
h₁ : (π ≫ Φ.inv) ≫ ψ = φ'
⊢ π ≫ Φ.inv = τ'

Tactic:
apply IsStronglyCartesian.map_uniq p (p.map φ) ψ rfl φ'

Premises used: CategoryTheory.Functor.map, CategoryTheory.Functor.IsStronglyCartesian.map_uniq, rfl
-- Module: Mathlib.CategoryTheory.FiberedCategory.Fibered
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsStronglyCartesian f φ
a b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst_2 : p.IsCartesian (p.map φ) φ
hφ' : p.IsHomLift (g ≫ p.map φ) φ'
a' : 𝒳
ψ : a' ⟶ b
hψ : p.IsStronglyCartesian (p.map φ) ψ
τ' : c ⟶ a' := IsStronglyCartesian.map p (p.map φ) ψ (R' := p.obj c) (g := g) ⋯ φ'
Φ : a' ≅ a := domainUniqueUpToIso p (p.map φ) φ ψ
π : c ⟶ a
hπ : p.IsHomLift g π
hπ_comp : π ≫ φ = φ'
⊢ (π ≫ Φ.inv) ≫ ψ = φ'

Tactic:
simp [hπ_comp, Φ]
-- Module: Mathlib.CategoryTheory.FiberedCategory.Fibered
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsStronglyCartesian f φ
a : 𝒳
R : 𝒮
f : R ⟶ p.obj a
obtain : ∀ (b : 𝒳) (φ : b ⟶ a) (hφ : p.IsStronglyCartesian f φ), ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsCartesian f φ
⊢ ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsCartesian f φ

Tactic:
obtain ⟨b, φ, hφ⟩ := h a R f
-- Module: Mathlib.CategoryTheory.FiberedCategory.Fibered
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsStronglyCartesian f φ
a : 𝒳
R : 𝒮
f : R ⟶ p.obj a
b : 𝒳
φ : b ⟶ a
hφ : p.IsStronglyCartesian f φ
⊢ ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsCartesian f φ

Tactic:
⟨b, φ, inferInstance⟩

Premises used: inferInstance, Exists.intro
-- Module: Mathlib.CategoryTheory.FiberedCategory.Fibered
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsStronglyCartesian f φ
a : 𝒳
R : 𝒮
f : R ⟶ p.obj a
b : 𝒳
φ : b ⟶ a
hφ : p.IsStronglyCartesian f φ
⊢ ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsCartesian f φ

Tactic:
refine ⟨b, φ, inferInstance⟩
-- Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
R S : 𝒮
a : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)
f : R ⟶ S
⊢ (forget F).IsHomLift f (cartesianLift a f)

Tactic:
IsHomLift.map (forget F) (cartesianLift a f)

Premises used: CategoryTheory.IsHomLift.map, CategoryTheory.Pseudofunctor.CoGrothendieck.cartesianLift, CategoryTheory.Pseudofunctor.CoGrothendieck.forget
-- Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
R S : 𝒮
a : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_2)
f : R ⟶ S
a' : ∫ᶜ F
g : a'.base ⟶ R
φ' : a' ⟶ { base := S, fiber := a }
inst_1 : (forget F).IsHomLift (g ≫ f) φ'
⊢ φ'.base = g ≫ f

Tactic:
simpa using IsHomLift.fac' (forget F) (g ≫ f) φ'

Premises used: CategoryTheory.IsHomLift.fac', CategoryTheory.CategoryStruct.comp, CategoryTheory.Pseudofunctor.CoGrothendieck.forget
-- Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
R S : 𝒮
a : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_2)
f : R ⟶ S
a' : ∫ᶜ F
g : a'.base ⟶ R
φ' : a' ⟶ { base := S, fiber := a }
inst_1 : (forget F).IsHomLift (g ≫ f) φ'
this : φ'.base = g ≫ f
⊢ Eq (α := (↑(F.obj { as := op a'.base : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_2))
    (obj (Cat.Hom.toFunctor (F.map φ'.base.op.toLoc)) { base := S, fiber := a : ∫ᶜ F }.fiber)
    (obj
      (Cat.Hom.toFunctor
        (F.map (CategoryStruct.comp (Y := { as := op R : LocallyDiscrete 𝒮ᵒᵖ }) f.op.toLoc g.op.toLoc)))
      a)

Tactic:
simp [this]
-- Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
R S : 𝒮
a : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)
f : R ⟶ S
a' : ∫ᶜ F
φ' : a' ⟶ { base := S, fiber := a }
g : a'.base ⟶ R
inst_1 : (forget F).IsHomLift (g ≫ f) φ'
⊢ (forget F).IsHomLift g (homCartesianLift f g φ')

Tactic:
IsHomLift.map (forget F) (homCartesianLift f g φ')

Premises used: CategoryTheory.IsHomLift.map, CategoryTheory.Pseudofunctor.CoGrothendieck.homCartesianLift, CategoryTheory.Pseudofunctor.CoGrothendieck.forget
-- Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
R S : 𝒮
a : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)
f : R ⟶ S
a' : ∫ᶜ F
g : (forget F).obj a' ⟶ R
φ' : a' ⟶ { base := S, fiber := a }
hφ' : (forget F).IsHomLift (g ≫ f) φ'
⊢ ∃! χ : a' ⟶ domainCartesianLift a f, (forget F).IsHomLift g χ ∧ χ ≫ cartesianLift a f = φ'

Tactic:
⟨homCartesianLift f g φ', ⟨inferInstance, ?_⟩, ?_⟩

Premises used: inferInstance, ExistsUnique, And.intro, Exists.intro, CategoryTheory.Pseudofunctor.CoGrothendieck.homCartesianLift
-- Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
R S : 𝒮
a : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)
f : R ⟶ S
a' : ∫ᶜ F
g : (forget F).obj a' ⟶ R
φ' : a' ⟶ { base := S, fiber := a }
hφ' : (forget F).IsHomLift (g ≫ f) φ'
refine_1 : homCartesianLift f g φ' ≫ cartesianLift a f = φ'
refine_2 :
  ∀ (y : a' ⟶ domainCartesianLift a f),
    (fun (χ : a' ⟶ domainCartesianLift a f) ↦ (forget F).IsHomLift g χ ∧ χ ≫ cartesianLift a f = φ') y →
      y = homCartesianLift f g φ'
⊢ ∃! χ : a' ⟶ domainCartesianLift a f, (forget F).IsHomLift g χ ∧ χ ≫ cartesianLift a f = φ'

Tactic:
refine ⟨homCartesianLift f g φ', ⟨inferInstance, ?_⟩, ?_⟩