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

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

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

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

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

Tactic:
apply map_uniq

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

Tactic:
simp only [id_comp]

Premises used: CategoryTheory.Category.id_comp
-- 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 S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsStronglyCartesian f φ
R' R'' : 𝒮
a' a'' : 𝒳
f' : R' ⟶ S
f'' : R'' ⟶ S
g : R' ⟶ R
g' : R'' ⟶ R'
H : f' = g ≫ f
H' : f'' = g' ≫ f'
φ' : a' ⟶ b
φ'' : a'' ⟶ b
inst_3 : p.IsStronglyCartesian f' φ'
inst_4 : p.IsHomLift f'' φ''
rwa : f'' = g' ≫ g ≫ f
rwa₁ rwa₂ rwa₃ rwa₄ : f'' = g' ≫ f'
⊢ f'' = (g' ≫ g) ≫ f

Tactic:
rwa [assoc, ← H]

Premises used: CategoryTheory.Category.assoc
-- 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 S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsStronglyCartesian f φ
R' R'' : 𝒮
a' a'' : 𝒳
f' : R' ⟶ S
f'' : R'' ⟶ S
g : R' ⟶ R
g' : R'' ⟶ R'
H : f' = g ≫ f
H' : f'' = g' ≫ f'
φ' : a' ⟶ b
φ'' : a'' ⟶ b
inst_3 : p.IsStronglyCartesian 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 φ (R' := R'') (g := g' ≫ g) (f' := f'') ⋯ φ''

Tactic:
apply map_uniq p f φ

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

Tactic:
simp only [assoc, fac]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.IsStronglyCartesian.fac
-- 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 S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst_2 : p.IsStronglyCartesian f φ
inst_3 : p.IsStronglyCartesian g ψ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ c
hτ : p.IsHomLift (h ≫ f ≫ g) τ
h₁ :
  (fun (χ : a' ⟶ a) ↦ p.IsHomLift h χ ∧ χ ≫ φ ≫ ψ = τ) (map p f φ (R' := p.obj a') (g := h) ⋯ (map p g ψ ⋯ τ)) ∧
    ∀ (y : a' ⟶ a),
      (fun (χ : a' ⟶ a) ↦ p.IsHomLift h χ ∧ χ ≫ φ ≫ ψ = τ) y → y = map p f φ (R' := p.obj a') (g := h) ⋯ (map p g ψ ⋯ τ)
⊢ ∃! χ : a' ⟶ a, p.IsHomLift h χ ∧ χ ≫ φ ≫ ψ = τ

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

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

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

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

Tactic:
refine ⟨⟨inferInstance, ?_⟩, ?_⟩
-- 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 S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst_2 : p.IsStronglyCartesian f φ
inst_3 : p.IsStronglyCartesian g ψ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ c
hτ : p.IsHomLift (h ≫ f ≫ g) τ
h₁ : (map p f φ (R' := p.obj a') (g := h) ⋯ (map p g ψ ⋯ τ) ≫ φ) ≫ ψ = τ
h₂ : map p g ψ ⋯ τ ≫ ψ = τ
h₃ h₄ : τ = τ
⊢ map p f φ (R' := p.obj a') (g := h) ⋯ (map p g ψ ⋯ τ) ≫ φ ≫ ψ = τ

Tactic:
rw [← assoc, fac, fac]

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

Tactic:
⟨hπ'₁, hπ'₂⟩
-- 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 S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst_2 : p.IsStronglyCartesian f φ
inst_3 : p.IsStronglyCartesian g ψ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ c
hτ : p.IsHomLift (h ≫ f ≫ g) τ
π' : a' ⟶ a
hπ'₁ : p.IsHomLift h π'
hπ'₂ : π' ≫ φ ≫ ψ = τ
h₁ : π' ≫ φ = map p g ψ ⋯ τ
⊢ π' = map p f φ (R' := p.obj a') (g := h) ⋯ (map p g ψ ⋯ τ)

Tactic:
apply map_uniq

Premises used: CategoryTheory.Functor.IsStronglyCartesian.map_uniq
-- 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 S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst_2 : p.IsStronglyCartesian f φ
inst_3 : p.IsStronglyCartesian g ψ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ c
hτ : p.IsHomLift (h ≫ f ≫ g) τ
π' : a' ⟶ a
hπ'₁ : p.IsHomLift h π'
hπ'₂ : π' ≫ φ ≫ ψ = τ
h₁ : (π' ≫ φ) ≫ ψ = τ
⊢ π' ≫ φ = map p g ψ ⋯ τ

Tactic:
apply map_uniq

Premises used: CategoryTheory.Functor.IsStronglyCartesian.map_uniq
-- 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 S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst_2 : p.IsStronglyCartesian f φ
inst_3 : p.IsStronglyCartesian g ψ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ c
hτ : p.IsHomLift (h ≫ f ≫ g) τ
π' : a' ⟶ a
hπ'₁ : p.IsHomLift h π'
hπ'₂ : π' ≫ φ ≫ ψ = τ
⊢ (π' ≫ φ) ≫ ψ = τ

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

Premises used: CategoryTheory.Category.assoc
-- 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 S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst_2 : p.IsStronglyCartesian g ψ
inst_3 : p.IsStronglyCartesian (f ≫ g) (φ ≫ ψ)
inst_4 : p.IsHomLift f φ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ b
hτ : p.IsHomLift (h ≫ f) τ
⊢ p.IsHomLift (h ≫ f ≫ g) (τ ≫ ψ)

Tactic:
simpa using IsHomLift.comp p (h ≫ f) _ τ ψ

Premises used: CategoryTheory.IsHomLift.comp, CategoryTheory.CategoryStruct.comp
-- 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 S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst_2 : p.IsStronglyCartesian g ψ
inst_3 : p.IsStronglyCartesian (f ≫ g) (φ ≫ ψ)
inst_4 : p.IsHomLift f φ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ b
hτ : p.IsHomLift (h ≫ f) τ
⊢ p.IsHomLift (h ≫ f ≫ g) (τ ≫ ψ)

Tactic:
have h₁ : IsHomLift p (h ≫ f ≫ g) (τ ≫ ψ) := by simpa using IsHomLift.comp p (h ≫ f) _ τ ψ
-- 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 S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst_2 : p.IsStronglyCartesian g ψ
inst_3 : p.IsStronglyCartesian (f ≫ g) (φ ≫ ψ)
inst_4 : p.IsHomLift f φ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ b
hτ : p.IsHomLift (h ≫ f) τ
h₁ : p.IsHomLift (h ≫ f ≫ g) (τ ≫ ψ)
h₂ :
  (fun (χ : a' ⟶ a) ↦ p.IsHomLift h χ ∧ χ ≫ φ = τ) (map p (f ≫ g) (φ ≫ ψ) (R' := p.obj a') (g := h) ⋯ (τ ≫ ψ)) ∧
    ∀ (y : a' ⟶ a),
      (fun (χ : a' ⟶ a) ↦ p.IsHomLift h χ ∧ χ ≫ φ = τ) y → y = map p (f ≫ g) (φ ≫ ψ) (R' := p.obj a') (g := h) ⋯ (τ ≫ ψ)
⊢ ∃! χ : a' ⟶ a, p.IsHomLift h χ ∧ χ ≫ φ = τ

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

Premises used: CategoryTheory.Functor.IsStronglyCartesian.map, CategoryTheory.CategoryStruct.comp, rfl
-- 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 S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst_2 : p.IsStronglyCartesian g ψ
inst_3 : p.IsStronglyCartesian (f ≫ g) (φ ≫ ψ)
inst_4 : p.IsHomLift f φ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ b
hτ : p.IsHomLift (h ≫ f) τ
h₁ : p.IsHomLift (h ≫ f ≫ g) (τ ≫ ψ)
⊢ (fun (χ : a' ⟶ a) ↦ p.IsHomLift h χ ∧ χ ≫ φ = τ) (map p (f ≫ g) (φ ≫ ψ) (R' := p.obj a') (g := h) ⋯ (τ ≫ ψ)) ∧
    ∀ (y : a' ⟶ a),
      (fun (χ : a' ⟶ a) ↦ p.IsHomLift h χ ∧ χ ≫ φ = τ) y → y = map p (f ≫ g) (φ ≫ ψ) (R' := p.obj a') (g := h) ⋯ (τ ≫ ψ)

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

Premises used: inferInstance, And.intro
-- 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 S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst_2 : p.IsStronglyCartesian g ψ
inst_3 : p.IsStronglyCartesian (f ≫ g) (φ ≫ ψ)
inst_4 : p.IsHomLift f φ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ b
hτ : p.IsHomLift (h ≫ f) τ
h₁ : p.IsHomLift (h ≫ f ≫ g) (τ ≫ ψ)
h₂ : map p (f ≫ g) (φ ≫ ψ) (R' := p.obj a') (g := h) ⋯ (τ ≫ ψ) ≫ φ = τ
h₃ :
  ∀ (y : a' ⟶ a),
    (fun (χ : a' ⟶ a) ↦ p.IsHomLift h χ ∧ χ ≫ φ = τ) y → y = map p (f ≫ g) (φ ≫ ψ) (R' := p.obj a') (g := h) ⋯ (τ ≫ ψ)
⊢ (fun (χ : a' ⟶ a) ↦ p.IsHomLift h χ ∧ χ ≫ φ = τ) (map p (f ≫ g) (φ ≫ ψ) (R' := p.obj a') (g := h) ⋯ (τ ≫ ψ)) ∧
    ∀ (y : a' ⟶ a),
      (fun (χ : a' ⟶ a) ↦ p.IsHomLift h χ ∧ χ ≫ φ = τ) y → y = map p (f ≫ g) (φ ≫ ψ) (R' := p.obj a') (g := h) ⋯ (τ ≫ ψ)

Tactic:
refine ⟨⟨inferInstance, ?_⟩, ?_⟩
-- 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 S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst_2 : p.IsStronglyCartesian g ψ
inst_3 : p.IsStronglyCartesian (f ≫ g) (φ ≫ ψ)
inst_4 : p.IsHomLift f φ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ b
hτ : p.IsHomLift (h ≫ f) τ
h₁ : p.IsHomLift (h ≫ f ≫ g) (τ ≫ ψ)
⊢ (map p (f ≫ g) (φ ≫ ψ) (R' := p.obj a') (g := h) ⋯ (τ ≫ ψ) ≫ φ) ≫ ψ = τ ≫ ψ

Tactic:
simp
-- 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 S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst_2 : p.IsStronglyCartesian g ψ
inst_3 : p.IsStronglyCartesian (f ≫ g) (φ ≫ ψ)
inst_4 : p.IsHomLift f φ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ b
hτ : p.IsHomLift (h ≫ f) τ
h₁ : p.IsHomLift (h ≫ f ≫ g) (τ ≫ ψ)
⊢ map p (f ≫ g) (φ ≫ ψ) (R' := p.obj a') (g := h) ⋯ (τ ≫ ψ) ≫ φ = τ

Tactic:
apply IsStronglyCartesian.ext p g ψ (h ≫ f) (by simp)

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

Tactic:
⟨hπ'₁, hπ'₂⟩
-- 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 S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst_2 : p.IsStronglyCartesian g ψ
inst_3 : p.IsStronglyCartesian (f ≫ g) (φ ≫ ψ)
inst_4 : p.IsHomLift f φ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ b
hτ : p.IsHomLift (h ≫ f) τ
h₁ : p.IsHomLift (h ≫ f ≫ g) (τ ≫ ψ)
π' : a' ⟶ a
hπ'₁ : p.IsHomLift h π'
hπ'₂ : π' ≫ φ = τ
h₂ : π' ≫ φ ≫ ψ = τ ≫ ψ
⊢ π' = map p (f ≫ g) (φ ≫ ψ) (R' := p.obj a') (g := h) ⋯ (τ ≫ ψ)

Tactic:
apply map_uniq

Premises used: CategoryTheory.Functor.IsStronglyCartesian.map_uniq
-- 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 S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst_2 : p.IsStronglyCartesian g ψ
inst_3 : p.IsStronglyCartesian (f ≫ g) (φ ≫ ψ)
inst_4 : p.IsHomLift f φ
a' : 𝒳
h : p.obj a' ⟶ R
τ : a' ⟶ b
hτ : p.IsHomLift (h ≫ f) τ
h₁ : p.IsHomLift (h ≫ f ≫ g) (τ ≫ ψ)
π' : a' ⟶ a
hπ'₁ : p.IsHomLift h π'
hπ'₂ : π' ≫ φ = τ
⊢ π' ≫ φ ≫ ψ = τ ≫ ψ

Tactic:
simp [hπ'₂.symm]

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

Tactic:
use τ ≫ φ.inv

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

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

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

Premises used: CategoryTheory.IsHomLift.comp, CategoryTheory.CategoryStruct.comp, CategoryTheory.IsHomLift.isoOfIsoLift, CategoryTheory.Iso.inv
-- 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 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.Cartesian
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.IsStronglyCartesian f φ
inst_3 : IsIso f
subst_hom_lift : ∀ {R S : 𝒮} {a_1 b_1 : 𝒳} [p.IsStronglyCartesian (p.map φ) φ] [IsIso (p.map φ)], IsIso φ
⊢ IsIso φ

Tactic:
subst_hom_lift p f φ
-- 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₁} 𝒳 𝒮
a b : 𝒳
φ : a ⟶ b
inst_2 : p.IsStronglyCartesian (p.map φ) φ
inst_3 : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ (g := CategoryTheory.inv (p.map φ)) ⋯ (𝟙 b)
h : φ ≫ φ' = 𝟙 a ∧ φ' ≫ φ = 𝟙 b
⊢ IsIso φ

Tactic:
use φ'
-- 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₁} 𝒳 𝒮
a b : 𝒳
φ : a ⟶ b
inst_2 : p.IsStronglyCartesian (p.map φ) φ
inst_3 : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ (g := CategoryTheory.inv (p.map φ)) ⋯ (𝟙 b)
⊢ φ' ≫ φ = 𝟙 b

Tactic:
have inv_hom : φ' ≫ φ = 𝟙 b := fac p (p.map φ) φ _ (𝟙 b)
-- 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₁} 𝒳 𝒮
a b : 𝒳
φ : a ⟶ b
inst_2 : p.IsStronglyCartesian (p.map φ) φ
inst_3 : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ (g := CategoryTheory.inv (p.map φ)) ⋯ (𝟙 b)
inv_hom : φ' ≫ φ = 𝟙 b
⊢ φ ≫ φ' = 𝟙 a ∧ φ' ≫ φ = 𝟙 b

Tactic:
⟨?_, inv_hom⟩

Premises used: And.intro
-- 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₁} 𝒳 𝒮
a b : 𝒳
φ : a ⟶ b
inst_2 : p.IsStronglyCartesian (p.map φ) φ
inst_3 : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ (g := CategoryTheory.inv (p.map φ)) ⋯ (𝟙 b)
inv_hom : φ' ≫ φ = 𝟙 b
h : φ ≫ φ' = 𝟙 a
⊢ φ ≫ φ' = 𝟙 a ∧ φ' ≫ φ = 𝟙 b

Tactic:
refine ⟨?_, inv_hom⟩
-- 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₁} 𝒳 𝒮
a b : 𝒳
φ : a ⟶ b
inst_2 : p.IsStronglyCartesian (p.map φ) φ
inst_3 : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ (g := CategoryTheory.inv (p.map φ)) ⋯ (𝟙 b)
inv_hom : φ' ≫ φ = 𝟙 b
rw : p.IsHomLift (p.map φ ≫ CategoryTheory.inv (p.map φ)) (φ ≫ φ')
⊢ p.IsHomLift (𝟙 (p.obj a)) (φ ≫ φ')

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

Premises used: CategoryTheory.Functor.map, CategoryTheory.IsIso.hom_inv_id
-- 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₁} 𝒳 𝒮
a b : 𝒳
φ : a ⟶ b
inst_2 : p.IsStronglyCartesian (p.map φ) φ
inst_3 : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ (g := CategoryTheory.inv (p.map φ)) ⋯ (𝟙 b)
inv_hom : φ' ≫ φ = 𝟙 b
⊢ p.IsHomLift (p.map φ ≫ CategoryTheory.inv (p.map φ)) (φ ≫ φ')

Tactic:
apply IsHomLift.comp

Premises used: CategoryTheory.IsHomLift.comp
-- 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₁} 𝒳 𝒮
a b : 𝒳
φ : a ⟶ b
inst_2 : p.IsStronglyCartesian (p.map φ) φ
inst_3 : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ (g := CategoryTheory.inv (p.map φ)) ⋯ (𝟙 b)
inv_hom : φ' ≫ φ = 𝟙 b
⊢ p.IsHomLift (𝟙 (p.obj a)) (φ ≫ φ')

Tactic:
have h₁ : IsHomLift p (𝟙 (p.obj a)) (φ ≫ φ') := by
    rw [← IsIso.hom_inv_id (p.map φ)]
    apply IsHomLift.comp
-- 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₁} 𝒳 𝒮
a b : 𝒳
φ : a ⟶ b
inst_2 : p.IsStronglyCartesian (p.map φ) φ
inst_3 : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ (g := CategoryTheory.inv (p.map φ)) ⋯ (𝟙 b)
inv_hom : φ' ≫ φ = 𝟙 b
h₁ : p.IsHomLift (𝟙 (p.obj a)) (φ ≫ φ')
h : (φ ≫ φ') ≫ φ = 𝟙 a ≫ φ
⊢ φ ≫ φ' = 𝟙 a

Tactic:
apply IsStronglyCartesian.ext p (p.map φ) φ (𝟙 (p.obj a))

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.map, CategoryTheory.Functor.IsStronglyCartesian.ext, CategoryTheory.Functor.obj
-- 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₁} 𝒳 𝒮
a b : 𝒳
φ : a ⟶ b
inst_2 : p.IsStronglyCartesian (p.map φ) φ
inst_3 : IsIso (p.map φ)
φ' : b ⟶ a := map p (p.map φ) φ (g := CategoryTheory.inv (p.map φ)) ⋯ (𝟙 b)
inv_hom : φ' ≫ φ = 𝟙 b
h₁ : p.IsHomLift (𝟙 (p.obj a)) (φ ≫ φ')
⊢ (φ ≫ φ') ≫ φ = 𝟙 a ≫ φ

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp