awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsHomLift f φ
⊢ p.IsHomLift f (𝟙 a ≫ φ)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Tactic:
subst_hom_lift p f φ.hom

Premises used: CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
a_1 b_1 : 𝒳
φ : a_1 ≅ b_1
R S : 𝒮
a b : 𝒳
inst_2 : p.IsHomLift (p.map φ.hom) φ.hom
⊢ p.map φ.hom ≫ eqToHom ⋯ ≫ (p.mapIso φ).inv ≫ eqToHom ⋯ = 𝟙 (p.obj a_1)

Tactic:
simp [← p.map_comp]

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

Tactic:
subst_hom_lift p f φ.hom

Premises used: CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
a_1 b_1 : 𝒳
φ : a_1 ≅ b_1
R S : 𝒮
a b : 𝒳
inst_2 : p.IsHomLift (p.map φ.hom) φ.hom
⊢ (eqToHom ⋯ ≫ (p.mapIso φ).inv ≫ eqToHom ⋯) ≫ p.map φ.hom = 𝟙 (p.obj b_1)

Tactic:
simp [← p.map_comp]

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

Tactic:
(isoOfIsoLift p f φ).inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.IsHomLift.isoOfIsoLift
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ≅ b
inst_2 : p.IsHomLift f φ.hom
⊢ f ≫ (isoOfIsoLift p f φ).inv = 𝟙 R

Tactic:
(isoOfIsoLift p f φ).hom_inv_id

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.IsHomLift.isoOfIsoLift
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsHomLift f φ
inst_3 : IsIso φ
⊢ IsIso f

Tactic:
(fac p f φ) ▸ inferInstance

Premises used: Eq.rec, inferInstance, Eq.symm, CategoryTheory.IsHomLift.fac
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
R S : 𝒮
a b : 𝒳
f : R ≅ S
φ : a ≅ b
inst_2 : p.IsHomLift f.hom φ.hom
h : CommSq (p.map φ.inv) (eqToHom ⋯) (eqToHom ⋯) f.inv
ha : p.obj b = S
hb : p.obj a = R
⊢ p.IsHomLift f.inv φ.inv

Tactic:
apply of_commSq

Premises used: CategoryTheory.IsHomLift.of_commSq
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ≅ b
inst_2 : p.IsHomLift f φ.hom
h : CommSq (p.map φ.inv) (eqToHom ⋯) (eqToHom ⋯) (isoOfIsoLift p f φ).inv
ha : p.obj b = S
hb : p.obj a = R
⊢ p.IsHomLift (isoOfIsoLift p f φ).inv φ.inv

Tactic:
apply of_commSq

Premises used: CategoryTheory.IsHomLift.of_commSq
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ≅ b
inst_2 : p.IsHomLift f φ.hom
⊢ CommSq (p.mapIso φ).hom (eqToHom ⋯) (eqToHom ⋯) (isoOfIsoLift p f φ).hom

Tactic:
apply commSq p f φ.hom

Premises used: CategoryTheory.IsHomLift.commSq, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : IsIso f
inst_3 : IsIso φ
inst_4 : p.IsHomLift f φ
⊢ p.IsHomLift (asIso f).hom (asIso φ).hom

Tactic:
simp_all
-- Module: Mathlib.CategoryTheory.FiberedCategory.HomLift
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
S : 𝒮
a b : 𝒳
φ : a ≅ b
inst_2 : p.IsHomLift (𝟙 S) φ.hom
⊢ p.IsHomLift (Iso.hom (asIso (𝟙 S))) φ.hom

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

Tactic:
(IsIso.inv_id (X := S)) ▸ (IsHomLift.inv p _ φ)

Premises used: CategoryTheory.IsIso.inv_id, Eq.rec, CategoryTheory.IsHomLift.inv
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
α : Type u
inst_1 : SemilatticeSup α
X Y : α
f g : X ⟶ Y
⊢ f ≫ 𝟙 Y = g ≫ 𝟙 Y

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
α : Type u
inst_1 : Preorder α
inst_2 : IsDirectedOrder α
X Y : α
f g : X ⟶ Y
⊢ f ≫ 𝟙 Y = g ≫ 𝟙 Y

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
α : Type u
inst_1 : SemilatticeSup α
inst_2 : OrderBot α
⊢ IsFiltered α

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
α : Type u
inst_1 : SemilatticeSup α
inst_2 : OrderTop α
⊢ IsFiltered α

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : Discrete PUnit.{u_1 + 1}
⊢ X.as = { as := PUnit.unit }.as

Tactic:
trivial
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : Discrete PUnit.{u_1 + 1}
⊢ Y.as = { as := PUnit.unit }.as

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : Discrete PUnit.{u_1 + 1}
f g : X ⟶ Y
⊢ Y.as = { as := PUnit.unit }.as

Tactic:
trivial
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
X Y : Discrete PUnit.{u_1 + 1}
f g : X ⟶ Y
⊢ f ≫
      { down := { down := ⋯ : PLift (Y.as = { as := PUnit.unit : Discrete PUnit.{u_1 + 1} }.as) } :
        ULift.{u_1, 0} (PLift (Y.as = { as := PUnit.unit : Discrete PUnit.{u_1 + 1} }.as)) } =
    g ≫ { down := { down := ⋯ } }

Tactic:
subsingleton
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
j j' : C
f f' : j ⟶ j'
⊢ Eq (α := j ⟶ coeq f f') (f ≫ coeqHom f f') (f' ≫ coeqHom f f')

Tactic:
(IsFilteredOrEmpty.cocone_maps f f').choose_spec.choose_spec

Premises used: Exists.choose_spec, CategoryTheory.IsFiltered.coeqHom, CategoryTheory.IsFiltered.coeq, CategoryTheory.IsFilteredOrEmpty.cocone_maps
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
R : Functor.{v, v₁, u, u₁} C D
inst_3 : R.IsRightAdjoint
⊢ IsFilteredOrEmpty.{v₁, u₁} D

Tactic:
of_right_adjoint (Adjunction.ofIsRightAdjoint R)

Premises used: CategoryTheory.IsFilteredOrEmpty.of_right_adjoint, CategoryTheory.Adjunction.ofIsRightAdjoint
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
h : Equivalence.{v, v₁, u, u₁} C D
⊢ IsFilteredOrEmpty.{v₁, u₁} D

Tactic:
of_right_adjoint h.symm.toAdjunction

Premises used: CategoryTheory.IsFilteredOrEmpty.of_right_adjoint, CategoryTheory.Equivalence.toAdjunction, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
⊢ ∀ {X : C}, Membership.mem (γ := Finset C) ∅ X → Nonempty.{v + 1} (X ⟶ Classical.choice ⋯)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
⊢ ∃ (S : C), ∀ {X : C}, Membership.mem (γ := Finset C) ∅ X → Nonempty.{v + 1} (X ⟶ S)

Tactic:
exact ⟨Classical.choice IsFiltered.nonempty, by simp⟩
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
X : C
O' : Finset C
nm : X ∉ O'
h : ∃ (S : C), ∀ {X : C}, X ∈ O' → Nonempty.{v + 1} (X ⟶ S)
insert :
  ∀ (S' : C) (w' : ∀ {X : C}, X ∈ O' → Nonempty.{v + 1} (X ⟶ S')),
    ∃ (S : C), ∀ {X_1 : C}, X_1 ∈ Insert.insert X O' → Nonempty.{v + 1} (X_1 ⟶ S)
⊢ ∃ (S : C), ∀ {X_1 : C}, X_1 ∈ Insert.insert X O' → Nonempty.{v + 1} (X_1 ⟶ S)

Tactic:
obtain ⟨S', w'⟩ := h
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
X : C
O' : Finset C
nm : X ∉ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → Nonempty.{v + 1} (X ⟶ S')
h : ∀ {X_1 : C}, X_1 ∈ insert X O' → Nonempty.{v + 1} (X_1 ⟶ max.{v, u} X S')
⊢ ∃ (S : C), ∀ {X_1 : C}, X_1 ∈ insert X O' → Nonempty.{v + 1} (X_1 ⟶ S)

Tactic:
use max X S'

Premises used: CategoryTheory.IsFiltered.max
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
X : C
O' : Finset C
nm : X ∉ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → Nonempty.{v + 1} (X ⟶ S')
Y : C
mY : Y ∈ insert X O'
h : ∀ (nm : Y ∉ O') (mY : Y ∈ insert Y O'), Nonempty.{v + 1} (Y ⟶ max.{v, u} Y S')
h₁ : ∀ (h : Y ≠ X), Nonempty.{v + 1} (Y ⟶ max.{v, u} X S')
⊢ Nonempty.{v + 1} (Y ⟶ max.{v, u} X S')

Tactic:
obtain rfl | h := eq_or_ne Y X

Premises used: eq_or_ne, rfl
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
O' : Finset C
S' : C
w' : ∀ {X : C}, X ∈ O' → Nonempty.{v + 1} (X ⟶ S')
Y : C
nm : Y ∉ O'
mY : Y ∈ insert Y O'
⊢ Nonempty.{v + 1} (Y ⟶ max.{v, u} Y S')

Tactic:
⟨leftToMax _ _⟩

Premises used: Nonempty.intro, CategoryTheory.IsFiltered.leftToMax
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
O' : Finset C
S' : C
w' : ∀ {X : C}, X ∈ O' → Nonempty.{v + 1} (X ⟶ S')
Y : C
nm : Y ∉ O'
mY : Y ∈ insert Y O'
⊢ Nonempty.{v + 1} (Y ⟶ max.{v, u} Y S')

Tactic:
exact ⟨leftToMax _ _⟩
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
X : C
O' : Finset C
nm : X ∉ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → Nonempty.{v + 1} (X ⟶ S')
Y : C
mY : Y ∈ insert X O'
h : Y ≠ X
⊢ Nonempty.{v + 1} (Y ⟶ max.{v, u} X S')

Tactic:
⟨(w' (Finset.mem_of_mem_insert_of_ne mY h)).some ≫ rightToMax _ _⟩

Premises used: CategoryTheory.IsFiltered.rightToMax, Nonempty.some, Nonempty.intro, CategoryTheory.CategoryStruct.comp, Finset.mem_of_mem_insert_of_ne
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
X : C
O' : Finset C
nm : X ∉ O'
S' : C
w' : ∀ {X : C}, X ∈ O' → Nonempty.{v + 1} (X ⟶ S')
Y : C
mY : Y ∈ insert X O'
h : Y ≠ X
⊢ Nonempty.{v + 1} (Y ⟶ max.{v, u} X S')

Tactic:
exact ⟨(w' (Finset.mem_of_mem_insert_of_ne mY h)).some ≫ rightToMax _ _⟩
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
O : Finset C
empty : ∃ (S : C), ∀ {X : C}, Membership.mem (γ := Finset C) ∅ X → Nonempty.{v + 1} (X ⟶ S)
insert :
  ∀ (X : C) (O' : Finset C) (nm : X ∉ O') (h : ∃ (S : C), ∀ {X : C}, X ∈ O' → Nonempty.{v + 1} (X ⟶ S)),
    ∃ (S : C), ∀ {X_1 : C}, X_1 ∈ Insert.insert X O' → Nonempty.{v + 1} (X_1 ⟶ S)
⊢ ∃ (S : C), ∀ {X : C}, X ∈ O → Nonempty.{v + 1} (X ⟶ S)

Tactic:
induction O using Finset.induction with
  | empty => exact ⟨Classical.choice IsFiltered.nonempty, by simp⟩
  | insert X O' nm h =>
    obtain ⟨S', w'⟩ := h
    use max X S'
    rintro Y mY
    obtain rfl | h := eq_or_ne Y X
    · exact ⟨leftToMax _ _⟩
    · exact ⟨(w' (Finset.mem_of_mem_insert_of_ne mY h)).some ≫ rightToMax _ _⟩

Premises used: Insert.insert, rfl
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
O : Finset C
empty : ∃ (S : C), ∀ {X : C}, Membership.mem (γ := Finset C) ∅ X → Nonempty.{v + 1} (X ⟶ S)
insert :
  ∀ (X : C) (O' : Finset C) (nm : X ∉ O') (h : ∃ (S : C), ∀ {X : C}, X ∈ O' → Nonempty.{v + 1} (X ⟶ S)),
    ∃ (S : C), ∀ {X_1 : C}, X_1 ∈ Insert.insert X O' → Nonempty.{v + 1} (X_1 ⟶ S)
⊢ ∃ (S : C), ∀ {X : C}, X ∈ O → Nonempty.{v + 1} (X ⟶ S)

Tactic:
classical
  induction O using Finset.induction with
  | empty => exact ⟨Classical.choice IsFiltered.nonempty, by simp⟩
  | insert X O' nm h =>
    obtain ⟨S', w'⟩ := h
    use max X S'
    rintro Y mY
    obtain rfl | h := eq_or_ne Y X
    · exact ⟨leftToMax _ _⟩
    · exact ⟨(w' (Finset.mem_of_mem_insert_of_ne mY h)).some ≫ rightToMax _ _⟩

Premises used: Insert.insert, rfl
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
O : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
empty :
  ∀ (S : C) (f : ∀ {X : C}, X ∈ O → Nonempty.{v + 1} (X ⟶ S)),
    ∃ (S : C) (T : {X : C} → X ∈ O → (X ⟶ S)),
      ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
        Membership.mem (γ := Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))) ∅
            (PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
              (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
                (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
                  (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f)))) →
          f ≫ T mY = T mX
⊢ ∃ (S : C) (T : {X : C} → X ∈ O → (X ⟶ S)),
    ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
      Membership.mem (γ := Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))) ∅
          (PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
            (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
              (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
                (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f)))) →
        f ≫ T mY = T mX

Tactic:
obtain ⟨S, f⟩ := sup_objs_exists O

Premises used: CategoryTheory.IsFiltered.sup_objs_exists
-- Module: Mathlib.CategoryTheory.Filtered.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
O : Finset C
H : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
S : C
f : ∀ {X : C}, X ∈ O → Nonempty.{v + 1} (X ⟶ S)
⊢ ∃ (S : C) (T : {X : C} → X ∈ O → (X ⟶ S)),
    ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : X ⟶ Y},
      Membership.mem (γ := Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))) ∅
          (PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X
            (PSigma.mk (β := fun (Y : C) ↦ (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) Y
              (PSigma.mk (β := fun (x : X ∈ O) ↦ (_ : Y ∈ O) ×' (X ⟶ Y)) mX
                (PSigma.mk (β := fun (x : Y ∈ O) ↦ X ⟶ Y) mY f)))) →
        f ≫ T mY = T mX

Tactic:
exact ⟨S, fun mX => (f mX).some, by rintro - - - - - ⟨⟩⟩