awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.HomLift (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
R S : 𝒮
a b c : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsHomLift f φ
T : 𝒮
ψ : b ⟶ c
inst_3 : p.IsHomLift (𝟙 T) ψ
⊢ S = T
have rw : p.obj b = T
Tactic: rw [← codomain_eq p f φ, domain_eq p (𝟙 T) ψ]
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.HomLift (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
R S : 𝒮
a b c : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsHomLift f φ
T : 𝒮
ψ : b ⟶ c
inst_3 : p.IsHomLift (𝟙 T) ψ
rw : p.obj b = T
⊢ S = T
have rw₁ : T = T
Tactic: rw [← codomain_eq p f φ, domain_eq p (𝟙 T) ψ]
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.HomLift (hypothesis)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
R S : 𝒮
a b c : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsHomLift f φ
T : 𝒮
ψ : b ⟶ c
inst_3 : p.IsHomLift (𝟙 T) ψ
⊢ p.IsHomLift f (φ ≫ ψ)
have inst : p.IsHomLift (𝟙 S) ψ
Tactic: obtain rfl : S = T := by rw [← codomain_eq p f φ, domain_eq p (𝟙 T) ψ]
Cleared hypotheses: T, inst_3
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.HomLift (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
a b c : 𝒳
R : 𝒮
φ : a ⟶ b
inst_2 : p.IsHomLift (𝟙 R) φ
S T : 𝒮
f : S ⟶ T
ψ : b ⟶ c
inst_3 : p.IsHomLift f ψ
⊢ R = S
have rw : p.obj b = S
Tactic: rw [← codomain_eq p (𝟙 R) φ, domain_eq p f ψ]
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.HomLift (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
a b c : 𝒳
R : 𝒮
φ : a ⟶ b
inst_2 : p.IsHomLift (𝟙 R) φ
S T : 𝒮
f : S ⟶ T
ψ : b ⟶ c
inst_3 : p.IsHomLift f ψ
rw : p.obj b = S
⊢ R = S
have rw₁ : S = S
Tactic: rw [← codomain_eq p (𝟙 R) φ, domain_eq p f ψ]
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.HomLift (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
a b c : 𝒳
R : 𝒮
φ : a ⟶ b
inst_2 : p.IsHomLift (𝟙 R) φ
S T : 𝒮
f : S ⟶ T
ψ : b ⟶ c
inst_3 : p.IsHomLift f ψ
⊢ p.IsHomLift f (φ ≫ ψ)
have obtain : ∀ (f : R ⟶ T) [p.IsHomLift f ψ], p.IsHomLift f (φ ≫ ψ)
Tactic: obtain rfl : R = S := by rw [← codomain_eq p (𝟙 R) φ, domain_eq p f ψ]
Cleared hypotheses: S, f, inst_3
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.HomLift (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
a b : 𝒳
hab : a = b
R : 𝒮
hR : p.obj a = R
⊢ p.IsHomLift (𝟙 R) (eqToHom hab)
have subst : p.IsHomLift (𝟙 (p.obj a)) (eqToHom sorry)
Tactic: subst hR hab
Cleared hypotheses: b, hab, R, hR
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.HomLift (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
a b : 𝒳
hab : a = b
S : 𝒮
hS : p.obj b = S
⊢ p.IsHomLift (𝟙 S) (eqToHom hab)
have subst : p.IsHomLift (𝟙 (p.obj a)) (eqToHom sorry)
Tactic: subst hS hab
Cleared hypotheses: b, hab, S, hS
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.HomLift (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
R S : 𝒮
hRS : R = S
a : 𝒳
ha : p.obj a = R
⊢ p.IsHomLift (eqToHom hRS) (𝟙 a)
have subst : p.IsHomLift (eqToHom sorry) (𝟙 a)
Tactic: subst hRS ha
Cleared hypotheses: R, S, hRS, ha
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.HomLift (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₂} 𝒳
inst_1 : Category.{v₂, u₁} 𝒮
p : Functor.{v₁, v₂, u₂, u₁} 𝒳 𝒮
R S : 𝒮
hRS : R = S
b : 𝒳
hb : p.obj b = S
⊢ p.IsHomLift (eqToHom hRS) (𝟙 b)
have subst : p.IsHomLift (eqToHom sorry) (𝟙 b)
Tactic: subst hRS hb
Cleared hypotheses: R, S, hRS, hb
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.HomLift (goal)
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
⊢ p.IsHomLift f (eqToHom h ≫ φ)
have subst : ∀ (φ : a' ⟶ b) [p.IsHomLift f φ], p.IsHomLift f (eqToHom sorry ≫ φ)
Tactic: subst h
Cleared hypotheses: a, φ, inst_2, h
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.HomLift (goal)
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'
⊢ p.IsHomLift f (φ ≫ eqToHom h)
have subst : p.IsHomLift f (φ ≫ eqToHom sorry)
Tactic: subst h
Cleared hypotheses: b', h
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.HomLift (goal)
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
⊢ p.IsHomLift (eqToHom h ≫ f) φ
have subst : ∀ (f : R' ⟶ S) [p.IsHomLift f φ], p.IsHomLift (eqToHom sorry ≫ f) φ
Tactic: subst h
Cleared hypotheses: R, f, inst_2, h
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.HomLift (goal)
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'
⊢ p.IsHomLift (f ≫ eqToHom h) φ
have subst : p.IsHomLift (f ≫ eqToHom sorry) φ
Tactic: subst h
Cleared hypotheses: S', h
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.HomLift (goal)
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 ≫ φ)
⊢ p.IsHomLift f φ
have subst : ∀ (φ : a' ⟶ b) (hφ' : p.IsHomLift f (eqToHom sorry ≫ φ)), p.IsHomLift f φ
Tactic: subst h
Cleared hypotheses: a, φ, h, hφ'
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.HomLift (hypothesis)
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 φ
have hφ'₁ : p.IsHomLift f (φ ≫ eqToHom sorry)
Tactic: subst h
Cleared hypotheses: b', h, hφ'
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.HomLift (goal)
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) φ
⊢ p.IsHomLift f φ
have subst : ∀ (f : R' ⟶ S) (hφ' : p.IsHomLift (eqToHom sorry ≫ f) φ), p.IsHomLift f φ
Tactic: subst h
Cleared hypotheses: R, f, h, hφ'
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.HomLift (hypothesis)
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 φ
have hφ'₁ : p.IsHomLift (f ≫ eqToHom sorry) φ
Tactic: subst h
Cleared hypotheses: S', h, hφ'
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.HomLift (goal)
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 ≫ eqToHom ⋯ ≫ (p.mapIso φ).inv ≫ eqToHom ⋯ = 𝟙 R
have subst_hom_lift : ∀ {R S : 𝒮} {a_1 b_1 : 𝒳} [inst_3 : p.IsHomLift (p.map φ.hom) φ.hom],
  p.map φ.hom ≫ eqToHom sorry ≫ (p.mapIso φ).inv ≫ eqToHom sorry = 𝟙 (p.obj a)
Tactic: subst_hom_lift p f φ.hom
Cleared hypotheses: R, S, f, inst_2
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.HomLift (goal)
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
⊢ (eqToHom ⋯ ≫ (p.mapIso φ).inv ≫ eqToHom ⋯) ≫ f = 𝟙 S
have subst_hom_lift : ∀ {R S : 𝒮} {a_1 b_1 : 𝒳} [inst_3 : p.IsHomLift (p.map φ.hom) φ.hom],
  (eqToHom sorry ≫ (p.mapIso φ).inv ≫ eqToHom sorry) ≫ p.map φ.hom = 𝟙 (p.obj b)
Tactic: subst_hom_lift p f φ.hom
Cleared hypotheses: R, S, f, inst_2
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.HomLift (goal)
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
⊢ p.IsHomLift f.inv φ.inv
have h : CommSq (p.map φ.inv) (eqToHom sorry) (eqToHom sorry) f.inv
Tactic: apply of_commSq
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.HomLift (goal)
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
⊢ p.IsHomLift f.inv φ.inv
have ha : p.obj b = S
Tactic: apply of_commSq
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.HomLift (goal)
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
⊢ p.IsHomLift f.inv φ.inv
have hb : p.obj a = R
Tactic: apply of_commSq
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.HomLift (goal)
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
⊢ p.IsHomLift (isoOfIsoLift p f φ).inv φ.inv
have h : CommSq (p.map φ.inv) (eqToHom sorry) (eqToHom sorry) (isoOfIsoLift p f φ).inv
Tactic: apply of_commSq
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.HomLift (goal)
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
⊢ p.IsHomLift (isoOfIsoLift p f φ).inv φ.inv
have ha : p.obj b = S
Tactic: apply of_commSq
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.HomLift (goal)
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
⊢ p.IsHomLift (isoOfIsoLift p f φ).inv φ.inv
have hb : p.obj a = R
Tactic: apply of_commSq
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
L : Functor.{v₁, v, u₁, u} D C
R : Functor.{v, v₁, u, u₁} C D
h : L ⊣ R
X Y : D
f g : X ⟶ Y
⊢ Eq (α := X ⟶ R.obj (coeq (L.map f) (L.map g)))
    (f ≫
      ((h.homEquiv Y (coeq (L.map f) (L.map g)) :
            Equiv.{v + 1, v₁ + 1} (L.obj Y ⟶ coeq (L.map f) (L.map g)) (Y ⟶ R.obj (coeq (L.map f) (L.map g)))) :
          (a : L.obj Y ⟶ coeq (L.map f) (L.map g)) → Y ⟶ R.obj (coeq (L.map f) (L.map g)))
        (coeqHom (L.map f) (L.map g)))
    (g ≫
      ((h.homEquiv Y (coeq (L.map f) (L.map g)) :
            Equiv.{v + 1, v₁ + 1} (L.obj Y ⟶ coeq (L.map f) (L.map g)) (Y ⟶ R.obj (coeq (L.map f) (L.map g)))) :
          (a : L.obj Y ⟶ coeq (L.map f) (L.map g)) → Y ⟶ R.obj (coeq (L.map f) (L.map g)))
        (coeqHom (L.map f) (L.map g)))
have rw : Eq.{v₁ + 1} (α := X ⟶ R.obj (coeq (L.map f) (L.map g)))
  (((h.homEquiv X (coeq (L.map f) (L.map g)) :
          Equiv.{v + 1, v₁ + 1} (L.obj X ⟶ coeq (L.map f) (L.map g)) (X ⟶ R.obj (coeq (L.map f) (L.map g)))) :
        (a : L.obj X ⟶ coeq (L.map f) (L.map g)) → X ⟶ R.obj (coeq (L.map f) (L.map g)))
      (L.map f ≫ coeqHom (L.map f) (L.map g)) :
    X ⟶ R.obj (coeq (L.map f) (L.map g)))
  (g ≫
      ((h.homEquiv Y (coeq (L.map f) (L.map g)) :
            Equiv.{v + 1, v₁ + 1} (L.obj Y ⟶ coeq (L.map f) (L.map g)) (Y ⟶ R.obj (coeq (L.map f) (L.map g)))) :
          (a : L.obj Y ⟶ coeq (L.map f) (L.map g)) → Y ⟶ R.obj (coeq (L.map f) (L.map g)))
        (coeqHom (L.map f) (L.map g)) :
    X ⟶ R.obj (coeq (L.map f) (L.map g)))
Tactic: rw [← h.homEquiv_naturality_left, ← h.homEquiv_naturality_left, coeq_condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFilteredOrEmpty.{v, u} C
D : Type u₁
inst_2 : Category.{v₁, u₁} D
L : Functor.{v₁, v, u₁, u} D C
R : Functor.{v, v₁, u, u₁} C D
h : L ⊣ R
X Y : D
f g : X ⟶ Y
rw :
  Eq.{v₁ + 1} (α := X ⟶ R.obj (coeq (L.map f) (L.map g)))
    (((h.homEquiv X (coeq (L.map f) (L.map g)) :
            Equiv.{v + 1, v₁ + 1} (L.obj X ⟶ coeq (L.map f) (L.map g)) (X ⟶ R.obj (coeq (L.map f) (L.map g)))) :
          (a : L.obj X ⟶ coeq (L.map f) (L.map g)) → X ⟶ R.obj (coeq (L.map f) (L.map g)))
        (L.map f ≫ coeqHom (L.map f) (L.map g)) :
      X ⟶ R.obj (coeq (L.map f) (L.map g)))
    (g ≫
        ((h.homEquiv Y (coeq (L.map f) (L.map g)) :
              Equiv.{v + 1, v₁ + 1} (L.obj Y ⟶ coeq (L.map f) (L.map g)) (Y ⟶ R.obj (coeq (L.map f) (L.map g)))) :
            (a : L.obj Y ⟶ coeq (L.map f) (L.map g)) → Y ⟶ R.obj (coeq (L.map f) (L.map g)))
          (coeqHom (L.map f) (L.map g)) :
      X ⟶ R.obj (coeq (L.map f) (L.map g)))
⊢ Eq (α := X ⟶ R.obj (coeq (L.map f) (L.map g)))
    (f ≫
      ((h.homEquiv Y (coeq (L.map f) (L.map g)) :
            Equiv.{v + 1, v₁ + 1} (L.obj Y ⟶ coeq (L.map f) (L.map g)) (Y ⟶ R.obj (coeq (L.map f) (L.map g)))) :
          (a : L.obj Y ⟶ coeq (L.map f) (L.map g)) → Y ⟶ R.obj (coeq (L.map f) (L.map g)))
        (coeqHom (L.map f) (L.map g)))
    (g ≫
      ((h.homEquiv Y (coeq (L.map f) (L.map g)) :
            Equiv.{v + 1, v₁ + 1} (L.obj Y ⟶ coeq (L.map f) (L.map g)) (Y ⟶ R.obj (coeq (L.map f) (L.map g)))) :
          (a : L.obj Y ⟶ coeq (L.map f) (L.map g)) → Y ⟶ R.obj (coeq (L.map f) (L.map g)))
        (coeqHom (L.map f) (L.map g)))
have rw₁ : Eq.{v₁ + 1} (α := X ⟶ R.obj (coeq (L.map f) (L.map g)))
  (((h.homEquiv X (coeq (L.map f) (L.map g)) :
          Equiv.{v + 1, v₁ + 1} (L.obj X ⟶ coeq (L.map f) (L.map g)) (X ⟶ R.obj (coeq (L.map f) (L.map g)))) :
        (a : L.obj X ⟶ coeq (L.map f) (L.map g)) → X ⟶ R.obj (coeq (L.map f) (L.map g)))
      (L.map f ≫ coeqHom (L.map f) (L.map g)) :
    X ⟶ R.obj (coeq (L.map f) (L.map g)))
  (((h.homEquiv X (coeq (L.map f) (L.map g)) :
          Equiv.{v + 1, v₁ + 1} (L.obj X ⟶ coeq (L.map f) (L.map g)) (X ⟶ R.obj (coeq (L.map f) (L.map g)))) :
        (a : L.obj X ⟶ coeq (L.map f) (L.map g)) → X ⟶ R.obj (coeq (L.map f) (L.map g)))
      (L.map g ≫ coeqHom (L.map f) (L.map g)) :
    X ⟶ R.obj (coeq (L.map f) (L.map g)))
Tactic: rw [← h.homEquiv_naturality_left, ← h.homEquiv_naturality_left, coeq_condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
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)
⊢ ∃ (S : C), ∀ {X_1 : C}, X_1 ∈ insert X O' → Nonempty.{v + 1} (X_1 ⟶ S)
have insert : ∀ (S' : C) (w' : ∀ {X : C}, X ∈ O' → Nonempty.{v + 1} (X ⟶ S')),
  ∃ (S : C), ∀ {X_1 : C}, X_1 ∈ insert X O' → Nonempty.{v + 1} (X_1 ⟶ S)
Tactic: obtain ⟨S', w'⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
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')
⊢ ∃ (S : C), ∀ {X_1 : C}, X_1 ∈ insert X O' → Nonempty.{v + 1} (X_1 ⟶ S)
have h : ∀ {X_1 : C}, X_1 ∈ insert X O' → Nonempty.{v + 1} (X_1 ⟶ max.{v, u} X S')
Tactic: use max X S'
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
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'
⊢ Nonempty.{v + 1} (Y ⟶ max.{v, u} X S')
have h : ∀ (nm : Y ∉ O') (mY : Y ∈ insert Y O'), Nonempty.{v + 1} (Y ⟶ max.{v, u} Y S')
Tactic: obtain rfl | h := eq_or_ne Y X
Cleared hypotheses: X, nm, mY
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
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')
⊢ Nonempty.{v + 1} (Y ⟶ max.{v, u} X S')
have h₁ : ∀ (h : Y ≠ X), Nonempty.{v + 1} (Y ⟶ max.{v, u} X S')
Tactic: obtain rfl | h := eq_or_ne Y X
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
O : Finset C
⊢ ∃ (S : C), ∀ {X : C}, X ∈ O → Nonempty.{v + 1} (X ⟶ S)
have empty : ∃ (S : C), ∀ {X : C}, Membership.mem (γ := Finset C) ∅ X → 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 _ _⟩
Cleared hypotheses: O
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
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)
⊢ ∃ (S : C), ∀ {X : C}, X ∈ O → Nonempty.{v + 1} (X ⟶ S)
have 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 X O' → Nonempty.{v + 1} (X_1 ⟶ 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 _ _⟩
Cleared hypotheses: O
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : IsFiltered.{v, u} C
O : Finset C
⊢ ∃ (S : C), ∀ {X : C}, X ∈ O → Nonempty.{v + 1} (X ⟶ S)
have empty : ∃ (S : C), ∀ {X : C}, Membership.mem (γ := Finset C) ∅ X → 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 _ _⟩
Cleared hypotheses: O
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
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)
⊢ ∃ (S : C), ∀ {X : C}, X ∈ O → Nonempty.{v + 1} (X ⟶ S)
have 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 X O' → Nonempty.{v + 1} (X_1 ⟶ 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 _ _⟩
Cleared hypotheses: O
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
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) (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
have 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
Tactic: obtain ⟨S, f⟩ := sup_objs_exists O
-- Lean 4 proof step from Mathlib.CategoryTheory.Filtered.Basic (goal)
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))
h' : (X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)
H' : Finset ((X : C) ×' (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y))
nmf : h' ∉ H'
h'' :
  ∃ (S : C) (T : {X : C} → X ∈ O → (X ⟶ S)),
    ∀ {X Y : C} (mX : X ∈ O) (mY : Y ∈ O) {f : 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))) ∈
          H' →
        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},
      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))) ∈
          insert h' H' →
        f ≫ T mY = T mX
have insert : ∀ (X Y : C) (mX : X ∈ O) (mY : Y ∈ O) (f : X ⟶ Y)
  (nmf :
    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))) ∉
      H'),
  ∃ (S : C) (T : {X : C} → X ∈ O → (X ⟶ S)),
    ∀ {X_1 Y_1 : C} (mX_1 : X_1 ∈ O) (mY_1 : Y_1 ∈ O) {f_1 : X_1 ⟶ Y_1},
      PSigma.mk (β := fun (X : C) ↦ (Y : C) ×' (_ : X ∈ O) ×' (_ : Y ∈ O) ×' (X ⟶ Y)) X_1
            (PSigma.mk (β := fun (Y : C) ↦ (_ : X_1 ∈ O) ×' (_ : Y ∈ O) ×' (X_1 ⟶ Y)) Y_1
              (PSigma.mk (β := fun (x : X_1 ∈ O) ↦ (_ : Y_1 ∈ O) ×' (X_1 ⟶ Y_1)) mX_1
                (PSigma.mk (β := fun (x : Y_1 ∈ O) ↦ X_1 ⟶ Y_1) mY_1 f_1))) ∈
          insert
            (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))))
            H' →
        f_1 ≫ T mY_1 = T mX_1
Tactic: obtain ⟨X, Y, mX, mY, f⟩ := h'
Cleared hypotheses: h', nmf