awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
R R' S : 𝒮
a a' b : 𝒳
f : R ⟶ S
f' : R' ⟶ S
g : R' ≅ R
h : f' = g.hom ≫ f
φ : a ⟶ b
φ' : a' ⟶ b
inst_2 : p.IsStronglyCartesian f φ
inst_3 : p.IsStronglyCartesian f' φ'
⊢ p.IsHomLift (R := R) (S := S) ((fun (x : R' ⟶ S) ↦ g.inv ≫ x) (g.hom ≫ f)) φ

Tactic:
simpa using IsCartesian.toIsHomLift

Premises used: CategoryTheory.Functor.IsCartesian.toIsHomLift
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
R R' S : 𝒮
a a' b : 𝒳
f : R ⟶ S
f' : R' ⟶ S
g : R' ≅ R
h : f' = g.hom ≫ f
φ : a ⟶ b
φ' : a' ⟶ b
inst_2 : p.IsStronglyCartesian f φ
inst_3 : p.IsStronglyCartesian f' φ'
⊢ p.IsHomLift g.hom (domainIsoOfBaseIso p h φ φ').hom

Tactic:
domainIsoOfBaseIso_hom p h φ φ' ▸ IsStronglyCartesian.map_isHomLift p f φ h φ'

Premises used: CategoryTheory.Functor.IsStronglyCartesian.domainIsoOfBaseIso_hom, Eq.rec, Eq.symm, CategoryTheory.Functor.IsStronglyCartesian.map_isHomLift
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
R R' S : 𝒮
a a' b : 𝒳
f : R ⟶ S
f' : R' ⟶ S
g : R' ≅ R
h : f' = g.hom ≫ f
φ : a ⟶ b
φ' : a' ⟶ b
inst_2 : p.IsStronglyCartesian f φ
inst_3 : p.IsStronglyCartesian f' φ'
⊢ p.IsHomLift (R := R) (S := S) ((fun (x : R' ⟶ S) ↦ g.inv ≫ x) (g.hom ≫ f)) φ

Tactic:
haveI : p.IsHomLift ((fun x ↦ g.inv ≫ x) (g.hom ≫ f)) φ := by
    simpa using IsCartesian.toIsHomLift
-- Module: Mathlib.CategoryTheory.FiberedCategory.Cartesian
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
R R' S : 𝒮
a a' b : 𝒳
f : R ⟶ S
f' : R' ⟶ S
g : R' ≅ R
h : f' = g.hom ≫ f
φ : a ⟶ b
φ' : a' ⟶ b
inst_2 : p.IsStronglyCartesian f φ
inst_3 : p.IsStronglyCartesian f' φ'
this : p.IsHomLift (R := R) (S := S) ((fun (x : R' ⟶ S) ↦ g.inv ≫ x) (g.hom ≫ f)) φ
⊢ p.IsHomLift g.inv (domainIsoOfBaseIso p h φ φ').inv

Tactic:
simpa using IsStronglyCartesian.map_isHomLift p f' φ' (congrArg (g.inv ≫ ·) h.symm) φ

Premises used: congrArg, CategoryTheory.CategoryStruct.comp, Eq.symm, CategoryTheory.Iso.inv, CategoryTheory.Functor.IsStronglyCartesian.map_isHomLift
-- 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.IsCocartesian f φ
b' : 𝒳
φ' : a ⟶ b'
inst_3 : p.IsHomLift f φ'
⊢ p.IsHomLift (𝟙 S) (IsCocartesian.map p f φ φ')

Tactic:
(Classical.choose_spec <| IsCocartesian.universal_property (p := p) (f := f) (φ := φ) φ').1.1

Premises used: Classical.choose_spec, CategoryTheory.Functor.IsCocartesian.universal_property, And.left, CategoryTheory.Functor.IsCocartesian.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₁} 𝒳 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsCocartesian f φ
b' : 𝒳
φ' : a ⟶ b'
inst_3 : p.IsHomLift f φ'
⊢ φ ≫ IsCocartesian.map p f φ φ' = φ'

Tactic:
(Classical.choose_spec <| IsCocartesian.universal_property (p := p) (f := f) (φ := φ) φ').1.2

Premises used: Classical.choose_spec, CategoryTheory.Functor.IsCocartesian.universal_property, And.right, And.left, CategoryTheory.Functor.IsCocartesian.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₁} 𝒳 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsCocartesian f φ
b' : 𝒳
φ' : a ⟶ b'
inst_3 : p.IsHomLift f φ'
ψ : b ⟶ b'
inst_4 : p.IsHomLift (𝟙 S) ψ
hψ : φ ≫ ψ = φ'
⊢ ψ = IsCocartesian.map p f φ φ'

Tactic:
(Classical.choose_spec <| IsCocartesian.universal_property (p := p) (f := f) (φ := φ) φ').2
    ψ ⟨inferInstance, hψ⟩

Premises used: inferInstance, Classical.choose_spec, CategoryTheory.Functor.IsCocartesian.universal_property, And.right, And.intro, CategoryTheory.Functor.IsCocartesian.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₁} 𝒳 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsCocartesian f φ
b' : 𝒳
ψ ψ' : b ⟶ b'
inst_3 : p.IsHomLift (𝟙 S) ψ
inst_4 : p.IsHomLift (𝟙 S) ψ'
h : φ ≫ ψ = φ ≫ ψ'
rw : IsCocartesian.map p f φ (φ ≫ ψ) = ψ'
rw₁ rw₂ : IsCocartesian.map p f φ (φ ≫ ψ) = IsCocartesian.map p f φ (φ ≫ ψ)
⊢ ψ = ψ'

Tactic:
rw [map_uniq p f φ (φ ≫ ψ) ψ rfl, map_uniq p f φ (φ ≫ ψ) ψ' h.symm]

Premises used: CategoryTheory.CategoryStruct.comp, Eq.symm, CategoryTheory.Functor.IsCocartesian.map_uniq, 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 : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsCocartesian f φ
subst_hom_lift :
  ∀ {R S : 𝒮} {a_1 b_1 : 𝒳} [inst_3 : p.IsCocartesian (p.map φ) φ], IsCocartesian.map p (p.map φ) φ φ = 𝟙 b
⊢ IsCocartesian.map p f φ φ = 𝟙 b

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_1 b_1 : 𝒳
φ : a_1 ⟶ b_1
R S : 𝒮
a b : 𝒳
inst_2 : p.IsCocartesian (p.map φ) φ
symm : 𝟙 b_1 = IsCocartesian.map p (p.map φ) φ φ
⊢ IsCocartesian.map p (p.map φ) φ φ = 𝟙 b_1

Tactic:
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₁} 𝒳 𝒮
a_1 b_1 : 𝒳
φ : a_1 ⟶ b_1
R S : 𝒮
a b : 𝒳
inst_2 : p.IsCocartesian (p.map φ) φ
hψ : φ ≫ 𝟙 b_1 = φ
⊢ 𝟙 b_1 = IsCocartesian.map p (p.map φ) φ φ

Tactic:
apply map_uniq

Premises used: CategoryTheory.Functor.IsCocartesian.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₁} 𝒳 𝒮
a_1 b_1 : 𝒳
φ : a_1 ⟶ b_1
R S : 𝒮
a b : 𝒳
inst_2 : p.IsCocartesian (p.map φ) φ
⊢ φ ≫ 𝟙 b_1 = φ

Tactic:
simp only [comp_id]

Premises used: 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 : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsCocartesian f φ
b' : 𝒳
φ' : a ⟶ b'
inst_3 : p.IsCocartesian f φ'
subst_hom_lift :
  ∀ {R S : 𝒮} {a_1 b_1 : 𝒳} [inst_4 : p.IsCocartesian (p.map φ) φ] [inst_5 : p.IsCocartesian (p.map φ) φ'],
    IsCocartesian.map p (p.map φ) φ φ' ≫ IsCocartesian.map p (p.map φ) φ' φ = 𝟙 b
⊢ IsCocartesian.map p f φ φ' ≫ IsCocartesian.map p f φ' φ = 𝟙 b

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_1 b_1 : 𝒳
φ : a_1 ⟶ b_1
b' : 𝒳
φ' : a_1 ⟶ b'
R S : 𝒮
a b : 𝒳
inst_2 : p.IsCocartesian (p.map φ) φ
inst_3 : p.IsCocartesian (p.map φ) φ'
h : φ ≫ IsCocartesian.map p (p.map φ) φ φ' ≫ IsCocartesian.map p (p.map φ) φ' φ = φ ≫ 𝟙 b_1
⊢ IsCocartesian.map p (p.map φ) φ φ' ≫ IsCocartesian.map p (p.map φ) φ' φ = 𝟙 b_1

Tactic:
apply IsCocartesian.ext p (p.map φ) φ

Premises used: CategoryTheory.Functor.IsCocartesian.ext, 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_1 b_1 : 𝒳
φ : a_1 ⟶ b_1
b' : 𝒳
φ' : a_1 ⟶ b'
R S : 𝒮
a b : 𝒳
inst_2 : p.IsCocartesian (p.map φ) φ
inst_3 : p.IsCocartesian (p.map φ) φ'
⊢ φ ≫ IsCocartesian.map p (p.map φ) φ φ' ≫ IsCocartesian.map p (p.map φ) φ' φ = φ ≫ 𝟙 b_1

Tactic:
simp only [fac_assoc, fac, comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.IsCocartesian.fac_assoc, CategoryTheory.Functor.IsCocartesian.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 : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsCocartesian f φ
b' : 𝒳
φ' : a ⟶ b'
inst_3 : p.IsCocartesian f φ'
subst_hom_lift :
  ∀ {R S : 𝒮} {a_1 b_1 : 𝒳} [inst_4 : p.IsCocartesian (p.map φ') φ] [inst_5 : p.IsCocartesian (p.map φ') φ'],
    IsCocartesian.map p (p.map φ') φ' φ ≫ IsCocartesian.map p (p.map φ') φ φ' = 𝟙 b'
⊢ IsCocartesian.map p f φ' φ ≫ IsCocartesian.map p f φ φ' = 𝟙 b'

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_1 b_1 : 𝒳
φ : a_1 ⟶ b_1
b' : 𝒳
φ' : a_1 ⟶ b'
R S : 𝒮
a b : 𝒳
inst_2 : p.IsCocartesian (p.map φ') φ
inst_3 : p.IsCocartesian (p.map φ') φ'
h : φ' ≫ IsCocartesian.map p (p.map φ') φ' φ ≫ IsCocartesian.map p (p.map φ') φ φ' = φ' ≫ 𝟙 b'
⊢ IsCocartesian.map p (p.map φ') φ' φ ≫ IsCocartesian.map p (p.map φ') φ φ' = 𝟙 b'

Tactic:
apply IsCocartesian.ext p (p.map φ') φ'

Premises used: CategoryTheory.Functor.IsCocartesian.ext, 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_1 b_1 : 𝒳
φ : a_1 ⟶ b_1
b' : 𝒳
φ' : a_1 ⟶ b'
R S : 𝒮
a b : 𝒳
inst_2 : p.IsCocartesian (p.map φ') φ
inst_3 : p.IsCocartesian (p.map φ') φ'
⊢ φ' ≫ IsCocartesian.map p (p.map φ') φ' φ ≫ IsCocartesian.map p (p.map φ') φ φ' = φ' ≫ 𝟙 b'

Tactic:
simp only [fac_assoc, fac, comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.IsCocartesian.fac_assoc, CategoryTheory.Functor.IsCocartesian.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 : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsCocartesian f φ
b' : 𝒳
φ' : b ≅ b'
inst_3 : p.IsHomLift (𝟙 S) φ'.hom
c : 𝒳
ψ : a ⟶ c
hψ : p.IsHomLift f ψ
h :
  (fun (χ : b' ⟶ c) ↦ p.IsHomLift (𝟙 S) χ ∧ (φ ≫ φ'.hom) ≫ χ = ψ) (φ'.inv ≫ IsCocartesian.map p f φ ψ) ∧
    ∀ (y : b' ⟶ c),
      (fun (χ : b' ⟶ c) ↦ p.IsHomLift (𝟙 S) χ ∧ (φ ≫ φ'.hom) ≫ χ = ψ) y → y = φ'.inv ≫ IsCocartesian.map p f φ ψ
⊢ ∃! χ : b' ⟶ c, p.IsHomLift (𝟙 S) χ ∧ (φ ≫ φ'.hom) ≫ χ = ψ

Tactic:
use φ'.inv ≫ IsCocartesian.map p f φ ψ

Premises used: CategoryTheory.Functor.IsCocartesian.map, 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.IsCocartesian f φ
b' : 𝒳
φ' : b ≅ b'
inst_3 : p.IsHomLift (𝟙 S) φ'.hom
c : 𝒳
ψ : a ⟶ c
hψ : p.IsHomLift f ψ
⊢ (φ ≫ φ'.hom) ≫ φ'.inv ≫ IsCocartesian.map p f φ ψ = ψ

Tactic:
simp
-- 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.IsCocartesian f φ
b' : 𝒳
φ' : b ≅ b'
inst_3 : p.IsHomLift (𝟙 S) φ'.hom
c : 𝒳
ψ : a ⟶ c
hψ : p.IsHomLift f ψ
h :
  ∀ (y : b' ⟶ c),
    (fun (χ : b' ⟶ c) ↦ p.IsHomLift (𝟙 S) χ ∧ (φ ≫ φ'.hom) ≫ χ = ψ) y → y = φ'.inv ≫ IsCocartesian.map p f φ ψ
⊢ (fun (χ : b' ⟶ c) ↦ p.IsHomLift (𝟙 S) χ ∧ (φ ≫ φ'.hom) ≫ χ = ψ) (φ'.inv ≫ IsCocartesian.map p f φ ψ) ∧
    ∀ (y : b' ⟶ c),
      (fun (χ : b' ⟶ c) ↦ p.IsHomLift (𝟙 S) χ ∧ (φ ≫ φ'.hom) ≫ χ = ψ) y → y = φ'.inv ≫ IsCocartesian.map p f φ ψ

Tactic:
refine ⟨⟨inferInstance, by simp⟩, ?_⟩
-- 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.IsCocartesian f φ
b' : 𝒳
φ' : b ≅ b'
inst_3 : p.IsHomLift (𝟙 S) φ'.hom
c : 𝒳
ψ : a ⟶ c
hψ : p.IsHomLift f ψ
τ : b' ⟶ c
hτ₁ : p.IsHomLift (𝟙 S) τ
hτ₂ : (φ ≫ φ'.hom) ≫ τ = ψ
h : φ'.hom ≫ τ = IsCocartesian.map p f φ ψ
⊢ τ = φ'.inv ≫ IsCocartesian.map p f φ ψ

Tactic:
rw [Iso.eq_inv_comp]

Premises used: CategoryTheory.Iso.eq_inv_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 : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsCocartesian f φ
b' : 𝒳
φ' : b ≅ b'
inst_3 : p.IsHomLift (𝟙 S) φ'.hom
c : 𝒳
ψ : a ⟶ c
hψ : p.IsHomLift f ψ
τ : b' ⟶ c
hτ₁ : p.IsHomLift (𝟙 S) τ
hτ₂ : (φ ≫ φ'.hom) ≫ τ = ψ
h : φ ≫ φ'.hom ≫ τ = ψ
⊢ φ'.hom ≫ τ = IsCocartesian.map p f φ ψ

Tactic:
apply map_uniq

Premises used: CategoryTheory.Functor.IsCocartesian.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 : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsCocartesian f φ
b' : 𝒳
φ' : b ≅ b'
inst_3 : p.IsHomLift (𝟙 S) φ'.hom
c : 𝒳
ψ : a ⟶ c
hψ : p.IsHomLift f ψ
τ : b' ⟶ c
hτ₁ : p.IsHomLift (𝟙 S) τ
hτ₂ : (φ ≫ φ'.hom) ≫ τ = ψ
⊢ φ ≫ φ'.hom ≫ τ = ψ

Tactic:
((assoc φ _ _) ▸ hτ₂)

Premises used: CategoryTheory.Category.assoc, Eq.rec
-- 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.IsCocartesian f φ
b' : 𝒳
φ' : b ≅ b'
inst_3 : p.IsHomLift (𝟙 S) φ'.hom
c : 𝒳
ψ : a ⟶ c
hψ : p.IsHomLift f ψ
τ : b' ⟶ c
hτ₁ : p.IsHomLift (𝟙 S) τ
hτ₂ : (φ ≫ φ'.hom) ≫ τ = ψ
⊢ φ ≫ φ'.hom ≫ τ = ψ

Tactic:
exact ((assoc φ _ _) ▸ 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 : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsCocartesian f φ
a' : 𝒳
φ' : a' ≅ a
inst_3 : p.IsHomLift (𝟙 R) φ'.hom
c : 𝒳
ψ : a' ⟶ c
hψ : p.IsHomLift f ψ
h :
  (fun (χ : b ⟶ c) ↦ p.IsHomLift (𝟙 S) χ ∧ (φ'.hom ≫ φ) ≫ χ = ψ) (IsCocartesian.map p f φ (φ'.inv ≫ ψ)) ∧
    ∀ (y : b ⟶ c),
      (fun (χ : b ⟶ c) ↦ p.IsHomLift (𝟙 S) χ ∧ (φ'.hom ≫ φ) ≫ χ = ψ) y → y = IsCocartesian.map p f φ (φ'.inv ≫ ψ)
⊢ ∃! χ : b ⟶ c, p.IsHomLift (𝟙 S) χ ∧ (φ'.hom ≫ φ) ≫ χ = ψ

Tactic:
use IsCocartesian.map p f φ (φ'.inv ≫ ψ)

Premises used: CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.IsCocartesian.map, 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.IsCocartesian f φ
a' : 𝒳
φ' : a' ≅ a
inst_3 : p.IsHomLift (𝟙 R) φ'.hom
c : 𝒳
ψ : a' ⟶ c
hψ : p.IsHomLift f ψ
⊢ (φ'.hom ≫ φ) ≫ IsCocartesian.map p f φ (φ'.inv ≫ ψ) = ψ

Tactic:
simp
-- 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.IsCocartesian f φ
a' : 𝒳
φ' : a' ≅ a
inst_3 : p.IsHomLift (𝟙 R) φ'.hom
c : 𝒳
ψ : a' ⟶ c
hψ : p.IsHomLift f ψ
h :
  ∀ (y : b ⟶ c),
    (fun (χ : b ⟶ c) ↦ p.IsHomLift (𝟙 S) χ ∧ (φ'.hom ≫ φ) ≫ χ = ψ) y → y = IsCocartesian.map p f φ (φ'.inv ≫ ψ)
⊢ (fun (χ : b ⟶ c) ↦ p.IsHomLift (𝟙 S) χ ∧ (φ'.hom ≫ φ) ≫ χ = ψ) (IsCocartesian.map p f φ (φ'.inv ≫ ψ)) ∧
    ∀ (y : b ⟶ c),
      (fun (χ : b ⟶ c) ↦ p.IsHomLift (𝟙 S) χ ∧ (φ'.hom ≫ φ) ≫ χ = ψ) y → y = IsCocartesian.map p f φ (φ'.inv ≫ ψ)

Tactic:
refine ⟨⟨inferInstance, by simp⟩, ?_⟩
-- 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.IsCocartesian f φ
a' : 𝒳
φ' : a' ≅ a
inst_3 : p.IsHomLift (𝟙 R) φ'.hom
c : 𝒳
ψ : a' ⟶ c
hψ : p.IsHomLift f ψ
τ : b ⟶ c
hτ₁ : p.IsHomLift (𝟙 S) τ
hτ₂ : (φ'.hom ≫ φ) ≫ τ = ψ
h : φ ≫ τ = φ'.inv ≫ ψ
⊢ τ = IsCocartesian.map p f φ (φ'.inv ≫ ψ)

Tactic:
apply map_uniq

Premises used: CategoryTheory.Functor.IsCocartesian.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 : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsCocartesian f φ
a' : 𝒳
φ' : a' ≅ a
inst_3 : p.IsHomLift (𝟙 R) φ'.hom
c : 𝒳
ψ : a' ⟶ c
hψ : p.IsHomLift f ψ
τ : b ⟶ c
hτ₁ : p.IsHomLift (𝟙 S) τ
hτ₂ : (φ'.hom ≫ φ) ≫ τ = ψ
⊢ φ ≫ τ = φ'.inv ≫ ψ

Tactic:
simp only [Iso.eq_inv_comp, ← assoc, hτ₂]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.eq_inv_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 : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsStronglyCocartesian f φ
S' : 𝒮
b' : 𝒳
g : S ⟶ S'
f' : R ⟶ S'
hf' : f' = f ≫ g
φ' : a ⟶ b'
inst_3 : p.IsHomLift f' φ'
subst_hom_lift :
  ∀ {R S_1 : 𝒮} {a_1 b_1 : 𝒳} (f : p.obj a ⟶ S) [p.IsStronglyCocartesian f φ] (g : S ⟶ p.obj b')
    (hf' : p.map φ' = f ≫ g) [p.IsHomLift (p.map φ') φ'], ∃! χ : b ⟶ b', p.IsHomLift g χ ∧ φ ≫ χ = φ'
⊢ ∃! χ : b ⟶ b', p.IsHomLift g χ ∧ φ ≫ χ = φ'

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₁} 𝒳 𝒮
S : 𝒮
a b : 𝒳
φ : a ⟶ b
b' : 𝒳
φ' : a ⟶ b'
f : p.obj a ⟶ S
inst_2 : p.IsStronglyCocartesian f φ
g : S ⟶ p.obj b'
hf' : p.map φ' = f ≫ g
inst_3 : p.IsHomLift (p.map φ') φ'
⊢ p.IsHomLift (f ≫ g) φ'

Tactic:
have : p.IsHomLift (f ≫ g) φ' := (hf' ▸ 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₁} 𝒳 𝒮
S : 𝒮
a b : 𝒳
φ : a ⟶ b
b' : 𝒳
φ' : a ⟶ b'
f : p.obj a ⟶ S
inst_2 : p.IsStronglyCocartesian f φ
g : S ⟶ p.obj b'
hf' : p.map φ' = f ≫ g
inst_3 : p.IsHomLift (p.map φ') φ'
this : p.IsHomLift (f ≫ g) φ'
⊢ ∃! χ : b ⟶ b', p.IsHomLift g χ ∧ φ ≫ χ = φ'

Tactic:
apply IsStronglyCocartesian.universal_property' f

Premises used: CategoryTheory.Functor.IsStronglyCocartesian.universal_property'
-- 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' : 𝒮
b' : 𝒳
g : S ⟶ S'
f' : R ⟶ S'
hf' : f' = f ≫ g
φ' : a ⟶ b'
inst_3 : p.IsHomLift f' φ'
⊢ p.IsHomLift g (map p f φ hf' φ')

Tactic:
(Classical.choose_spec <| universal_property p f φ _ _ hf' φ').1.1

Premises used: CategoryTheory.Functor.IsStronglyCocartesian.map, Classical.choose_spec, And.left, CategoryTheory.Functor.IsStronglyCocartesian.universal_property
-- 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' : 𝒮
b' : 𝒳
g : S ⟶ S'
f' : R ⟶ S'
hf' : f' = f ≫ g
φ' : a ⟶ b'
inst_3 : p.IsHomLift f' φ'
⊢ φ ≫ map p f φ hf' φ' = φ'

Tactic:
(Classical.choose_spec <| universal_property p f φ _ _ hf' φ').1.2

Premises used: CategoryTheory.Functor.IsStronglyCocartesian.map, Classical.choose_spec, And.right, And.left, CategoryTheory.Functor.IsStronglyCocartesian.universal_property
-- 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' : 𝒮
b' : 𝒳
g : S ⟶ S'
f' : R ⟶ S'
hf' : f' = f ≫ g
φ' : a ⟶ b'
inst_3 : p.IsHomLift f' φ'
ψ : b ⟶ b'
inst_4 : p.IsHomLift g ψ
hψ : φ ≫ ψ = φ'
⊢ ψ = map p f φ hf' φ'

Tactic:
(Classical.choose_spec <| universal_property p f φ _ _ hf' φ').2 ψ ⟨inferInstance, hψ⟩

Premises used: inferInstance, CategoryTheory.Functor.IsStronglyCocartesian.map, Classical.choose_spec, And.right, And.intro, CategoryTheory.Functor.IsStronglyCocartesian.universal_property
-- 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' : 𝒮
b' : 𝒳
g : S ⟶ S'
ψ ψ' : b ⟶ b'
inst_3 : p.IsHomLift g ψ
inst_4 : p.IsHomLift g ψ'
h : φ ≫ ψ = φ ≫ ψ'
rw : map p f φ (S' := S') (g := g) ⋯ (φ ≫ ψ) = ψ'
rw₁ rw₂ : map p f φ (S' := S') (g := g) ⋯ (φ ≫ ψ) = map p f φ (S' := S') (g := g) ⋯ (φ ≫ ψ)
⊢ ψ = ψ'

Tactic:
rw [map_uniq p f φ (g := g) rfl (φ ≫ ψ) ψ rfl, map_uniq p f φ (g := g) rfl (φ ≫ ψ) ψ' h.symm]

Premises used: CategoryTheory.CategoryStruct.comp, Eq.symm, rfl, 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 : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsStronglyCocartesian f φ
subst_hom_lift : ∀ {R S : 𝒮} {a_1 b_1 : 𝒳} [inst_3 : p.IsStronglyCocartesian (p.map φ) φ], map p (p.map φ) φ ⋯ φ = 𝟙 b
⊢ map p f φ ⋯ φ = 𝟙 b

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_1 b_1 : 𝒳
φ : a_1 ⟶ b_1
R S : 𝒮
a b : 𝒳
inst_2 : p.IsStronglyCocartesian (p.map φ) φ
symm : 𝟙 b_1 = map p (p.map φ) φ ⋯ φ
⊢ map p (p.map φ) φ ⋯ φ = 𝟙 b_1

Tactic:
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₁} 𝒳 𝒮
a_1 b_1 : 𝒳
φ : a_1 ⟶ b_1
R S : 𝒮
a b : 𝒳
inst_2 : p.IsStronglyCocartesian (p.map φ) φ
hψ : φ ≫ 𝟙 b_1 = φ
⊢ 𝟙 b_1 = map p (p.map φ) φ ⋯ φ

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₁} 𝒳 𝒮
a_1 b_1 : 𝒳
φ : a_1 ⟶ b_1
R S : 𝒮
a b : 𝒳
inst_2 : p.IsStronglyCocartesian (p.map φ) φ
⊢ φ ≫ 𝟙 b_1 = φ

Tactic:
simp only [comp_id]

Premises used: 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 : 𝒮
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'' φ''
rwa : f'' = (f ≫ g) ≫ g'
rwa₁ rwa₂ rwa₃ rwa₄ : f'' = f' ≫ g'
⊢ f'' = f ≫ g ≫ g'

Tactic:
rwa [← assoc, ← H]

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 : 𝒮
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'' φ''
hψ : φ ≫ map p f φ H φ' ≫ map p f' φ' H' φ'' = φ''
⊢ map p f φ H φ' ≫ map p f' φ' H' φ'' = map p f φ (S' := S'') (g := g ≫ g') (f' := f'') ⋯ φ''

Tactic:
apply map_uniq p f φ

Premises used: CategoryTheory.Functor.IsStronglyCocartesian.map_uniq