awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian
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.IsStronglyCocartesian f φ
S' S'' : 𝒮
b' b'' : 𝒳
f' : R ⟶ S'
f'' : R ⟶ S''
g : S ⟶ S'
g' : S' ⟶ S''
H : f' = f ≫ g
H' : f'' = f' ≫ g'
φ' : a ⟶ b'
φ'' : a ⟶ b''
inst_3 : p.IsStronglyCocartesian f' φ'
inst_4 : p.IsHomLift f'' φ''
⊢ φ ≫ map p f φ H φ' ≫ map p f' φ' H' φ'' = φ''

Tactic:
simp only [fac_assoc, fac]

Premises used: CategoryTheory.Functor.IsStronglyCocartesian.fac_assoc, CategoryTheory.Functor.IsStronglyCocartesian.fac
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian
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.IsStronglyCocartesian f φ
inst_3 : p.IsStronglyCocartesian g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : a ⟶ c'
hτ : p.IsHomLift ((f ≫ g) ≫ h) τ
h₁ :
  (fun (χ : c ⟶ c') ↦ p.IsHomLift h χ ∧ (φ ≫ ψ) ≫ χ = τ) (map p g ψ (S' := p.obj c') (g := h) ⋯ (map p f φ ⋯ τ)) ∧
    ∀ (y : c ⟶ c'),
      (fun (χ : c ⟶ c') ↦ p.IsHomLift h χ ∧ (φ ≫ ψ) ≫ χ = τ) y →
        y = map p g ψ (S' := p.obj c') (g := h) ⋯ (map p f φ ⋯ τ)
⊢ ∃! χ : c ⟶ c', p.IsHomLift h χ ∧ (φ ≫ ψ) ≫ χ = τ

Tactic:
use map p g ψ (f' := g ≫ h) rfl <| map p f φ (assoc f g h) τ

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.IsStronglyCocartesian.map, rfl
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian
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.IsStronglyCocartesian f φ
inst_3 : p.IsStronglyCocartesian g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : a ⟶ c'
hτ : p.IsHomLift ((f ≫ g) ≫ h) τ
⊢ (fun (χ : c ⟶ c') ↦ p.IsHomLift h χ ∧ (φ ≫ ψ) ≫ χ = τ) (map p g ψ (S' := p.obj c') (g := h) ⋯ (map p f φ ⋯ τ)) ∧
    ∀ (y : c ⟶ c'),
      (fun (χ : c ⟶ c') ↦ p.IsHomLift h χ ∧ (φ ≫ ψ) ≫ χ = τ) y →
        y = map p g ψ (S' := p.obj c') (g := h) ⋯ (map p f φ ⋯ τ)

Tactic:
⟨⟨inferInstance, ?_⟩, ?_⟩

Premises used: inferInstance, And.intro
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian
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.IsStronglyCocartesian f φ
inst_3 : p.IsStronglyCocartesian g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : a ⟶ c'
hτ : p.IsHomLift ((f ≫ g) ≫ h) τ
h₁ : (φ ≫ ψ) ≫ map p g ψ (S' := p.obj c') (g := h) ⋯ (map p f φ ⋯ τ) = τ
h₂ :
  ∀ (y : c ⟶ c'),
    (fun (χ : c ⟶ c') ↦ p.IsHomLift h χ ∧ (φ ≫ ψ) ≫ χ = τ) y → y = map p g ψ (S' := p.obj c') (g := h) ⋯ (map p f φ ⋯ τ)
⊢ (fun (χ : c ⟶ c') ↦ p.IsHomLift h χ ∧ (φ ≫ ψ) ≫ χ = τ) (map p g ψ (S' := p.obj c') (g := h) ⋯ (map p f φ ⋯ τ)) ∧
    ∀ (y : c ⟶ c'),
      (fun (χ : c ⟶ c') ↦ p.IsHomLift h χ ∧ (φ ≫ ψ) ≫ χ = τ) y →
        y = map p g ψ (S' := p.obj c') (g := h) ⋯ (map p f φ ⋯ τ)

Tactic:
refine ⟨⟨inferInstance, ?_⟩, ?_⟩
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian
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.IsStronglyCocartesian f φ
inst_3 : p.IsStronglyCocartesian g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : a ⟶ c'
hτ : p.IsHomLift ((f ≫ g) ≫ h) τ
⊢ (φ ≫ ψ) ≫ map p g ψ (S' := p.obj c') (g := h) ⋯ (map p f φ ⋯ τ) = τ

Tactic:
simp only [assoc, fac]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.IsStronglyCocartesian.fac
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian
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.IsStronglyCocartesian f φ
inst_3 : p.IsStronglyCocartesian g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : a ⟶ c'
hτ : p.IsHomLift ((f ≫ g) ≫ h) τ
π' : c ⟶ c'
h₁ : ∀ (hπ'₁ : p.IsHomLift h π') (hπ'₂ : (φ ≫ ψ) ≫ π' = τ), π' = map p g ψ (S' := p.obj c') (g := h) ⋯ (map p f φ ⋯ τ)
⊢ (fun (χ : c ⟶ c') ↦ p.IsHomLift h χ ∧ (φ ≫ ψ) ≫ χ = τ) π' → π' = map p g ψ (S' := p.obj c') (g := h) ⋯ (map p f φ ⋯ τ)

Tactic:
⟨hπ'₁, hπ'₂⟩
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian
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.IsStronglyCocartesian f φ
inst_3 : p.IsStronglyCocartesian g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : a ⟶ c'
hτ : p.IsHomLift ((f ≫ g) ≫ h) τ
π' : c ⟶ c'
hπ'₁ : p.IsHomLift h π'
hπ'₂ : (φ ≫ ψ) ≫ π' = τ
h₁ : ψ ≫ π' = map p f φ ⋯ τ
⊢ π' = map p g ψ (S' := p.obj c') (g := h) ⋯ (map p f φ ⋯ τ)

Tactic:
apply map_uniq

Premises used: CategoryTheory.Functor.IsStronglyCocartesian.map_uniq
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian
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.IsStronglyCocartesian f φ
inst_3 : p.IsStronglyCocartesian g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : a ⟶ c'
hτ : p.IsHomLift ((f ≫ g) ≫ h) τ
π' : c ⟶ c'
hπ'₁ : p.IsHomLift h π'
hπ'₂ : (φ ≫ ψ) ≫ π' = τ
h₁ : φ ≫ ψ ≫ π' = τ
⊢ ψ ≫ π' = map p f φ ⋯ τ

Tactic:
apply map_uniq

Premises used: CategoryTheory.Functor.IsStronglyCocartesian.map_uniq
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian
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.IsStronglyCocartesian f φ
inst_3 : p.IsStronglyCocartesian g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : a ⟶ c'
hτ : p.IsHomLift ((f ≫ g) ≫ h) τ
π' : c ⟶ c'
hπ'₁ : p.IsHomLift h π'
hπ'₂ : (φ ≫ ψ) ≫ π' = τ
⊢ φ ≫ ψ ≫ π' = τ

Tactic:
simp only [← hπ'₂, assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian
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.IsStronglyCocartesian f φ
inst_3 : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst_4 : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
h₁ :
  (fun (χ : c ⟶ c') ↦ p.IsHomLift h χ ∧ ψ ≫ χ = τ) (map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ)) ∧
    ∀ (y : c ⟶ c'), (fun (χ : c ⟶ c') ↦ p.IsHomLift h χ ∧ ψ ≫ χ = τ) y → y = map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ)
⊢ ∃! χ : c ⟶ c', p.IsHomLift h χ ∧ ψ ≫ χ = τ

Tactic:
use map p (f ≫ g) (φ ≫ ψ) (f' := f ≫ g ≫ h) (assoc f g h).symm (φ ≫ τ)

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.IsStronglyCocartesian.map, CategoryTheory.CategoryStruct.comp, Eq.symm
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian
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.IsStronglyCocartesian f φ
inst_3 : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst_4 : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
⊢ (fun (χ : c ⟶ c') ↦ p.IsHomLift h χ ∧ ψ ≫ χ = τ) (map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ)) ∧
    ∀ (y : c ⟶ c'), (fun (χ : c ⟶ c') ↦ p.IsHomLift h χ ∧ ψ ≫ χ = τ) y → y = map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ)

Tactic:
⟨⟨inferInstance, ?_⟩, ?_⟩

Premises used: inferInstance, And.intro
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian
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.IsStronglyCocartesian f φ
inst_3 : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst_4 : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
h₁ : ψ ≫ map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ) = τ
h₂ : ∀ (y : c ⟶ c'), (fun (χ : c ⟶ c') ↦ p.IsHomLift h χ ∧ ψ ≫ χ = τ) y → y = map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ)
⊢ (fun (χ : c ⟶ c') ↦ p.IsHomLift h χ ∧ ψ ≫ χ = τ) (map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ)) ∧
    ∀ (y : c ⟶ c'), (fun (χ : c ⟶ c') ↦ p.IsHomLift h χ ∧ ψ ≫ χ = τ) y → y = map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ)

Tactic:
refine ⟨⟨inferInstance, ?_⟩, ?_⟩
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian
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.IsStronglyCocartesian f φ
inst_3 : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst_4 : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
⊢ φ ≫ ψ ≫ map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ) = φ ≫ τ

Tactic:
simp only [← assoc, fac]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.IsStronglyCocartesian.fac
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian
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.IsStronglyCocartesian f φ
inst_3 : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst_4 : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
⊢ ψ ≫ map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ) = τ

Tactic:
apply IsStronglyCocartesian.ext p f φ (g ≫ h) <| by simp only [← assoc, fac]

Premises used: CategoryTheory.Functor.IsStronglyCocartesian.ext, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian
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.IsStronglyCocartesian f φ
inst_3 : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst_4 : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
π' : c ⟶ c'
h₁ : ∀ (hπ'₁ : p.IsHomLift h π') (hπ'₂ : ψ ≫ π' = τ), π' = map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ)
⊢ (fun (χ : c ⟶ c') ↦ p.IsHomLift h χ ∧ ψ ≫ χ = τ) π' → π' = map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ)

Tactic:
⟨hπ'₁, hπ'₂⟩
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian
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.IsStronglyCocartesian f φ
inst_3 : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst_4 : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
π' : c ⟶ c'
hπ'₁ : p.IsHomLift h π'
hπ'₂ : ψ ≫ π' = τ
h₁ : (φ ≫ ψ) ≫ π' = φ ≫ τ
⊢ π' = map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ)

Tactic:
apply map_uniq

Premises used: CategoryTheory.Functor.IsStronglyCocartesian.map_uniq
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian
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.IsStronglyCocartesian f φ
inst_3 : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst_4 : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
π' : c ⟶ c'
hπ'₁ : p.IsHomLift h π'
hπ'₂ : ψ ≫ π' = τ
⊢ (φ ≫ ψ) ≫ π' = φ ≫ τ

Tactic:
simp [hπ'₂.symm]

Premises used: Eq.symm
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian
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 φ.hom
b' : 𝒳
g : S ⟶ p.obj b'
τ : a ⟶ b'
hτ : p.IsHomLift (f ≫ g) τ
h :
  (fun (χ : b ⟶ b') ↦ p.IsHomLift g χ ∧ φ.hom ≫ χ = τ) (φ.inv ≫ τ) ∧
    ∀ (y : b ⟶ b'), (fun (χ : b ⟶ b') ↦ p.IsHomLift g χ ∧ φ.hom ≫ χ = τ) y → y = φ.inv ≫ τ
⊢ ∃! χ : b ⟶ b', p.IsHomLift g χ ∧ φ.hom ≫ χ = τ

Tactic:
use φ.inv ≫ τ

Premises used: CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian
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 φ.hom
b' : 𝒳
g : S ⟶ p.obj b'
τ : a ⟶ b'
hτ : p.IsHomLift (f ≫ g) τ
h : (fun (χ : b ⟶ b') ↦ p.IsHomLift g χ ∧ φ.hom ≫ χ = τ) (φ.inv ≫ τ)
⊢ (fun (χ : b ⟶ b') ↦ p.IsHomLift g χ ∧ φ.hom ≫ χ = τ) (φ.inv ≫ τ) ∧
    ∀ (y : b ⟶ b'), (fun (χ : b ⟶ b') ↦ p.IsHomLift g χ ∧ φ.hom ≫ χ = τ) y → y = φ.inv ≫ τ

Tactic:
refine ⟨?_, by cat_disch⟩
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian
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 φ.hom
b' : 𝒳
g : S ⟶ p.obj b'
τ : a ⟶ b'
hτ : p.IsHomLift (f ≫ g) τ
⊢ (fun (χ : b ⟶ b') ↦ p.IsHomLift g χ ∧ φ.hom ≫ χ = τ) (φ.inv ≫ τ)

Tactic:
simpa [← assoc] using (IsHomLift.comp p (isoOfIsoLift p f φ).inv (f ≫ g) φ.inv τ)

Premises used: CategoryTheory.Category.assoc, CategoryTheory.IsHomLift.comp, CategoryTheory.CategoryStruct.comp, CategoryTheory.IsHomLift.isoOfIsoLift, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian
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 φ
inst_3 : IsIso φ
⊢ p.IsHomLift f (asIso φ).hom

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian
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.IsStronglyCocartesian f φ
inst_3 : IsIso f
subst_hom_lift : ∀ {R S : 𝒮} {a_1 b_1 : 𝒳} [p.IsStronglyCocartesian (p.map φ) φ] [IsIso (p.map φ)], IsIso φ
⊢ IsIso φ

Tactic:
subst_hom_lift p f φ
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
a b : 𝒳
φ : a ⟶ b
inst_2 : p.IsStronglyCocartesian (p.map φ) φ
inst_3 : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ (g := CategoryTheory.inv (p.map φ)) ⋯ (𝟙 a)
h : φ ≫ φ' = 𝟙 a ∧ φ' ≫ φ = 𝟙 b
⊢ IsIso φ

Tactic:
use φ'
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
a b : 𝒳
φ : a ⟶ b
inst_2 : p.IsStronglyCocartesian (p.map φ) φ
inst_3 : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ (g := CategoryTheory.inv (p.map φ)) ⋯ (𝟙 a)
⊢ φ ≫ φ' = 𝟙 a

Tactic:
have inv_hom : φ ≫ φ' = 𝟙 a := fac p (p.map φ) φ _ (𝟙 a)
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
a b : 𝒳
φ : a ⟶ b
inst_2 : p.IsStronglyCocartesian (p.map φ) φ
inst_3 : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ (g := CategoryTheory.inv (p.map φ)) ⋯ (𝟙 a)
inv_hom : φ ≫ φ' = 𝟙 a
⊢ φ ≫ φ' = 𝟙 a ∧ φ' ≫ φ = 𝟙 b

Tactic:
⟨inv_hom, ?_⟩

Premises used: And.intro
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
a b : 𝒳
φ : a ⟶ b
inst_2 : p.IsStronglyCocartesian (p.map φ) φ
inst_3 : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ (g := CategoryTheory.inv (p.map φ)) ⋯ (𝟙 a)
inv_hom : φ ≫ φ' = 𝟙 a
h : φ' ≫ φ = 𝟙 b
⊢ φ ≫ φ' = 𝟙 a ∧ φ' ≫ φ = 𝟙 b

Tactic:
refine ⟨inv_hom, ?_⟩
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
a b : 𝒳
φ : a ⟶ b
inst_2 : p.IsStronglyCocartesian (p.map φ) φ
inst_3 : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ (g := CategoryTheory.inv (p.map φ)) ⋯ (𝟙 a)
inv_hom : φ ≫ φ' = 𝟙 a
rw : p.IsHomLift (CategoryTheory.inv (p.map φ) ≫ p.map φ) (φ' ≫ φ)
⊢ p.IsHomLift (𝟙 (p.obj b)) (φ' ≫ φ)

Tactic:
rw [← IsIso.inv_hom_id (p.map φ)]

Premises used: CategoryTheory.IsIso.inv_hom_id, CategoryTheory.Functor.map
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
a b : 𝒳
φ : a ⟶ b
inst_2 : p.IsStronglyCocartesian (p.map φ) φ
inst_3 : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ (g := CategoryTheory.inv (p.map φ)) ⋯ (𝟙 a)
inv_hom : φ ≫ φ' = 𝟙 a
⊢ p.IsHomLift (CategoryTheory.inv (p.map φ) ≫ p.map φ) (φ' ≫ φ)

Tactic:
apply IsHomLift.comp

Premises used: CategoryTheory.IsHomLift.comp
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
a b : 𝒳
φ : a ⟶ b
inst_2 : p.IsStronglyCocartesian (p.map φ) φ
inst_3 : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ (g := CategoryTheory.inv (p.map φ)) ⋯ (𝟙 a)
inv_hom : φ ≫ φ' = 𝟙 a
⊢ p.IsHomLift (𝟙 (p.obj b)) (φ' ≫ φ)

Tactic:
have h₁ : IsHomLift p (𝟙 (p.obj b)) (φ' ≫ φ) := by
    rw [← IsIso.inv_hom_id (p.map φ)]
    apply IsHomLift.comp
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
a b : 𝒳
φ : a ⟶ b
inst_2 : p.IsStronglyCocartesian (p.map φ) φ
inst_3 : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ (g := CategoryTheory.inv (p.map φ)) ⋯ (𝟙 a)
inv_hom : φ ≫ φ' = 𝟙 a
h₁ : p.IsHomLift (𝟙 (p.obj b)) (φ' ≫ φ)
h : φ ≫ φ' ≫ φ = φ ≫ 𝟙 b
⊢ φ' ≫ φ = 𝟙 b

Tactic:
apply IsStronglyCocartesian.ext p (p.map φ) φ (𝟙 (p.obj b))

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.IsStronglyCocartesian.ext, CategoryTheory.Functor.map, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
a b : 𝒳
φ : a ⟶ b
inst_2 : p.IsStronglyCocartesian (p.map φ) φ
inst_3 : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ (g := CategoryTheory.inv (p.map φ)) ⋯ (𝟙 a)
inv_hom : φ ≫ φ' = 𝟙 a
h₁ : p.IsHomLift (𝟙 (p.obj b)) (φ' ≫ φ)
⊢ φ ≫ φ' ≫ φ = φ ≫ 𝟙 b

Tactic:
simp only [← assoc, inv_hom, comp_id, id_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
R S S' : 𝒮
a b b' : 𝒳
f : R ⟶ S
f' : R ⟶ S'
g : S ≅ S'
h : f' = f ≫ g.hom
φ : a ⟶ b
φ' : a ⟶ b'
inst_2 : p.IsStronglyCocartesian f φ
inst_3 : p.IsStronglyCocartesian f' φ'
simp : p.IsHomLift f φ
⊢ p.IsHomLift (R := R) (S := S) ((fun (x : R ⟶ S') ↦ x ≫ g.inv) (f ≫ g.hom)) φ

Tactic:
simp only [assoc, Iso.hom_inv_id, comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
R S S' : 𝒮
a b b' : 𝒳
f : R ⟶ S
f' : R ⟶ S'
g : S ≅ S'
h : f' = f ≫ g.hom
φ : a ⟶ b
φ' : a ⟶ b'
inst_2 : p.IsStronglyCocartesian f φ
inst_3 : p.IsStronglyCocartesian f' φ'
⊢ p.IsHomLift f φ

Tactic:
infer_instance
-- 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 : 𝒮
X Y Z : p.Fiber S
φ : { φ : (↑X : 𝒳) ⟶ (↑Y : 𝒳) // p.IsHomLift (𝟙 S) φ }
ψ : { φ : (↑Y : 𝒳) ⟶ (↑Z : 𝒳) // p.IsHomLift (𝟙 S) φ }
⊢ p.IsHomLift (𝟙 S) (↑φ : (↑X : 𝒳) ⟶ (↑Y : 𝒳))

Tactic:
have := φ.2
-- 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 : 𝒮
X Y Z : p.Fiber S
φ : { φ : (↑X : 𝒳) ⟶ (↑Y : 𝒳) // p.IsHomLift (𝟙 S) φ }
ψ : { φ : (↑Y : 𝒳) ⟶ (↑Z : 𝒳) // p.IsHomLift (𝟙 S) φ }
this : p.IsHomLift (𝟙 S) (↑φ : (↑X : 𝒳) ⟶ (↑Y : 𝒳))
⊢ p.IsHomLift (𝟙 S) (↑ψ : (↑Y : 𝒳) ⟶ (↑Z : 𝒳))

Tactic:
have := ψ.2
-- 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 : 𝒮
X Y Z : p.Fiber S
φ : { φ : (↑X : 𝒳) ⟶ (↑Y : 𝒳) // p.IsHomLift (𝟙 S) φ }
ψ : { φ : (↑Y : 𝒳) ⟶ (↑Z : 𝒳) // p.IsHomLift (𝟙 S) φ }
this_1 : p.IsHomLift (𝟙 S) (↑φ : (↑X : 𝒳) ⟶ (↑Y : 𝒳))
this : p.IsHomLift (𝟙 S) (↑ψ : (↑Y : 𝒳) ⟶ (↑Z : 𝒳))
⊢ p.IsHomLift (𝟙 S) ((↑φ : (↑X : 𝒳) ⟶ (↑Y : 𝒳)) ≫ (↑ψ : (↑Y : 𝒳) ⟶ (↑Z : 𝒳)))

Tactic:
infer_instance
-- 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 : p.Fiber S
φ : a ⟶ b
⊢ p.IsHomLift (a := obj fiberInclusion a) (𝟙 S) (map fiberInclusion φ)

Tactic:
φ.2

Premises used: Subtype.property
-- 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 : p.Fiber S
φ ψ : a ⟶ b
h : Eq (α := obj fiberInclusion a ⟶ obj fiberInclusion b) (map fiberInclusion φ) (map fiberInclusion ψ)
⊢ φ = ψ

Tactic:
Subtype.ext h

Premises used: Subtype.ext
-- 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 : 𝒮
⊢ Function.Injective.{u₂ + 1, u₂ + 1} (α := p.Fiber S) (obj fiberInclusion)

Tactic:
fun _ _ f ↦ Subtype.val_inj.1 f

Premises used: Subtype.val_inj, CategoryTheory.Functor.Fiber, Iff.mp, Function.Injective
-- 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 : 𝒮
X Y : p.Fiber S
φ : X ⟶ Y
⊢ Eq (α := obj (fiberInclusion ⋙ p) X ⟶ obj.{v₂, v₁, u₂, u₁} (obj (const (p.Fiber S)) S) Y)
    (map (fiberInclusion ⋙ p) φ ≫
      Iso.hom
        ((fun (X : p.Fiber S) ↦
            (eqToIso ⋯ : obj (fiberInclusion ⋙ p) X ≅ obj.{v₂, v₁, u₂, u₁} (obj (const (p.Fiber S)) S) X))
          Y))
    (Iso.hom
        ((fun (X : p.Fiber S) ↦
            (eqToIso ⋯ : obj (fiberInclusion ⋙ p) X ≅ obj.{v₂, v₁, u₂, u₁} (obj (const (p.Fiber S)) S) X))
          X) ≫
      map (obj (const (p.Fiber S)) S) φ)

Tactic:
simp [IsHomLift.fac' p (𝟙 S) (fiberInclusion.map φ)]

Premises used: CategoryTheory.Functor.Fiber.fiberInclusion, CategoryTheory.CategoryStruct.id, CategoryTheory.IsHomLift.fac', CategoryTheory.Functor.map
-- 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 : 𝒮
⊢ Eq (α := Functor.{v₂, v₁, u₂, u₁} (p.Fiber S) 𝒮) (fiberInclusion ⋙ p) (obj (const (p.Fiber S)) S)

Tactic:
Functor.ext_of_iso fiberInclusionCompIsoConst (fun x ↦ x.2)

Premises used: CategoryTheory.Functor.Fiber.fiberInclusionCompIsoConst, CategoryTheory.Functor.ext_of_iso, Subtype.property
-- 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 : 𝒳
ha : p.obj a = S
⊢ obj fiberInclusion (mk ha) = a

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 : 𝒮
a b : 𝒳
φ : a ⟶ b
inst_2 : p.IsHomLift (𝟙 S) φ
⊢ map fiberInclusion (homMk p S φ) = φ

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 : 𝒮
a : 𝒳
inst_2 : p.IsHomLift (𝟙 S) (𝟙 a)
⊢ Eq (α := mk ⋯ ⟶ mk ⋯) (homMk p S (𝟙 a) : mk ⋯ ⟶ mk ⋯) (𝟙 (mk ⋯) : mk ⋯ ⟶ mk ⋯)

Tactic:
rfl

Premises used: CategoryTheory.Functor.Fiber.homMk, rfl