awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Fibered (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsStronglyCartesian f φ
a b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst_2 : p.IsCartesian (p.map φ) φ
hφ' : p.IsHomLift (g ≫ p.map φ) φ'
a' : 𝒳
ψ : a' ⟶ b
hψ : p.IsStronglyCartesian (p.map φ) ψ
τ' : c ⟶ a' := IsStronglyCartesian.map p (p.map φ) ψ (R' := p.obj c) (g := g) ⋯ φ'
Φ : a' ≅ a := domainUniqueUpToIso p (p.map φ) φ ψ
π : c ⟶ a
hπ : p.IsHomLift g π
hπ_comp : π ≫ φ = φ'
⊢ π ≫ Φ.inv = τ'
have h₁ : (π ≫ Φ.inv) ≫ ψ = φ'
Tactic: apply IsStronglyCartesian.map_uniq p (p.map φ) ψ rfl φ'
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Fibered (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsStronglyCartesian f φ
a : 𝒳
R : 𝒮
f : R ⟶ p.obj a
⊢ ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsCartesian f φ
have obtain : ∀ (b : 𝒳) (φ : b ⟶ a) (hφ : p.IsStronglyCartesian f φ), ∃ (b : 𝒳), ∃ (φ : b ⟶ a), p.IsCartesian f φ
Tactic: obtain ⟨b, φ, hφ⟩ := h a R f
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Grothendieck (goal)
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
R S : 𝒮
a : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)
f : R ⟶ S
a' : ∫ᶜ F
g : (forget F).obj a' ⟶ R
φ' : a' ⟶ { base := S, fiber := a }
hφ' : (forget F).IsHomLift (g ≫ f) φ'
⊢ ∃! χ : a' ⟶ domainCartesianLift a f, (forget F).IsHomLift g χ ∧ χ ≫ cartesianLift a f = φ'
have refine_1 : homCartesianLift f g φ' ≫ cartesianLift a f = φ'
Tactic: refine ⟨homCartesianLift f g φ', ⟨inferInstance, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Grothendieck (goal)
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
R S : 𝒮
a : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)
f : R ⟶ S
a' : ∫ᶜ F
g : (forget F).obj a' ⟶ R
φ' : a' ⟶ { base := S, fiber := a }
hφ' : (forget F).IsHomLift (g ≫ f) φ'
refine_1 : homCartesianLift f g φ' ≫ cartesianLift a f = φ'
⊢ ∃! χ : a' ⟶ domainCartesianLift a f, (forget F).IsHomLift g χ ∧ χ ≫ cartesianLift a f = φ'
have refine_2 : ∀ (y : a' ⟶ domainCartesianLift a f),
  (fun (χ : a' ⟶ domainCartesianLift a f) ↦ (forget F).IsHomLift g χ ∧ χ ≫ cartesianLift a f = φ') y →
    y = homCartesianLift f g φ'
Tactic: refine ⟨homCartesianLift f g φ', ⟨inferInstance, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Grothendieck (goal)
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
R S : 𝒮
a : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)
f : R ⟶ S
a' : ∫ᶜ F
g : (forget F).obj a' ⟶ R
χ' : a' ⟶ domainCartesianLift a f
hχ'.symm : (forget F).IsHomLift g χ'
hφ' : (forget F).IsHomLift (g ≫ f) (χ' ≫ cartesianLift a f)
⊢ χ' = homCartesianLift f g (χ' ≫ cartesianLift a f)
have refine_2 : ∀ (hχ'.symm : (forget F).IsHomLift χ'.base χ') (hφ' : (forget F).IsHomLift (χ'.base ≫ f) (χ' ≫ cartesianLift a f)),
  χ' = homCartesianLift f χ'.base (χ' ≫ cartesianLift a f)
Tactic: obtain ⟨rfl⟩ : g = χ'.1 := by simpa using IsHomLift.fac (forget F) g χ'
Cleared hypotheses: g, hχ'.symm, hφ'
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Grothendieck (goal)
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
R S : 𝒮
a : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)
f : R ⟶ S
a' : ∫ᶜ F
χ' : a' ⟶ domainCartesianLift a f
hχ'.symm : (forget F).IsHomLift χ'.base χ'
hφ' : (forget F).IsHomLift (χ'.base ≫ f) (χ' ≫ cartesianLift a f)
⊢ χ' = homCartesianLift f χ'.base (χ' ≫ cartesianLift a f)
have refine_2 : χ'.base = (homCartesianLift f χ'.base (χ' ≫ cartesianLift a f)).base
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Grothendieck (goal)
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
R S : 𝒮
a : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)
f : R ⟶ S
a' : ∫ᶜ F
χ' : a' ⟶ domainCartesianLift a f
hχ'.symm : (forget F).IsHomLift χ'.base χ'
hφ' : (forget F).IsHomLift (χ'.base ≫ f) (χ' ≫ cartesianLift a f)
refine_2 : χ'.base = (homCartesianLift f χ'.base (χ' ≫ cartesianLift a f)).base
⊢ χ' = homCartesianLift f χ'.base (χ' ≫ cartesianLift a f)
have refine_2₁ : χ'.fiber = (homCartesianLift f χ'.base (χ' ≫ cartesianLift a f)).fiber ≫ eqToHom sorry
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Grothendieck (goal)
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
a b c : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_2)
φ : a ⟶ b
ψ : b ⟶ c
⊢ Eq (α := { base := S, fiber := a : ∫ᶜ F } ⟶ { base := S, fiber := c })
    { base := 𝟙 S,
      fiber := (φ ≫ ψ) ≫ NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ }))) c }
    (CategoryStruct.comp (Y := { base := S, fiber := b })
      { base := 𝟙 S,
        fiber := φ ≫ NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ }))) b }
      { base := 𝟙 S,
        fiber := ψ ≫ NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ }))) c })
have hfg₁ : Eq.{v_1 + 1} (α := { base := S, fiber := a : ∫ᶜ F }.base ⟶ { base := S, fiber := c : ∫ᶜ F }.base)
  (Hom.base
    { base := 𝟙 S,
      fiber :=
        (φ ≫ ψ) ≫ NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ }))) c })
  (Hom.base
    (CategoryStruct.comp (Y := { base := S, fiber := b })
      { base := 𝟙 S,
        fiber := φ ≫ NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ }))) b }
      { base := 𝟙 S,
        fiber := ψ ≫ NatTrans.app (Cat.Hom₂.toNatTrans (Iso.inv (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ }))) c }))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Grothendieck (hypothesis)
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
X Y : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)
f : (Fiber.inducedFunctor ⋯).obj X ⟶ (Fiber.inducedFunctor ⋯).obj Y
⊢ ∃ (a : X ⟶ Y), (Fiber.inducedFunctor ⋯).map a = f
have hf : Eq (α :=
  (obj fiberInclusion ((Fiber.inducedFunctor sorry).obj X)).base ⟶
    (obj fiberInclusion ((Fiber.inducedFunctor sorry).obj Y)).base)
  (Hom.base (Functor.map fiberInclusion f)) (𝟙 S)
Tactic: have hf : (fiberInclusion.map f).base = 𝟙 S := by
      simpa using (IsHomLift.fac (forget F) (𝟙 S) (fiberInclusion.map f)).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Grothendieck (goal)
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
X Y : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)
f : (Fiber.inducedFunctor ⋯).obj X ⟶ (Fiber.inducedFunctor ⋯).obj Y
hf :
  Eq (α :=
    (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj X)).base ⟶
      (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj Y)).base)
    (Hom.base (Functor.map fiberInclusion f)) (𝟙 S)
⊢ ∃ (a : X ⟶ Y), (Fiber.inducedFunctor ⋯).map a = f
have h : (Fiber.inducedFunctor sorry).map
    (CategoryStruct.comp (Y :=
      obj (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (Hom.base (Functor.map fiberInclusion f))))))
        (obj fiberInclusion ((Fiber.inducedFunctor sorry).obj Y)).fiber)
      (Hom.fiber (Functor.map fiberInclusion f))
      (eqToHom sorry ≫ NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ }))) Y)) =
  f
Tactic: use (fiberInclusion.map f).fiber ≫ eqToHom (by simp [hf]) ≫
      (F.mapId ⟨op S⟩).hom.toNatTrans.app Y
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Grothendieck (goal)
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
X Y : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)
f : (Fiber.inducedFunctor ⋯).obj X ⟶ (Fiber.inducedFunctor ⋯).obj Y
hf :
  Eq (α :=
    (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj X)).base ⟶
      (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj Y)).base)
    (Hom.base (Functor.map fiberInclusion f)) (𝟙 S)
⊢ (Fiber.inducedFunctor ⋯).map
      (CategoryStruct.comp (Y :=
        obj (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (Hom.base (Functor.map fiberInclusion f))))))
          (obj fiberInclusion ((Fiber.inducedFunctor ⋯).obj Y)).fiber)
        (Hom.fiber (Functor.map fiberInclusion f))
        (eqToHom ⋯ ≫ NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ }))) Y)) =
    f
have h : Eq (α :=
  (obj fiberInclusion ((Fiber.inducedFunctor sorry).obj X)).base ⟶
    (obj fiberInclusion ((Fiber.inducedFunctor sorry).obj Y)).base)
  (Hom.base
    (Functor.map fiberInclusion
      ((Fiber.inducedFunctor sorry).map
        (CategoryStruct.comp (Y :=
          obj (Cat.Hom.toFunctor (F.map (Quiver.Hom.toLoc (Quiver.Hom.op (Hom.base (Functor.map fiberInclusion f))))))
            (obj fiberInclusion ((Fiber.inducedFunctor sorry).obj Y)).fiber)
          (Hom.fiber (Functor.map fiberInclusion f))
          (eqToHom sorry ≫
            NatTrans.app (Cat.Hom₂.toNatTrans (Iso.hom (F.mapId { as := op S : LocallyDiscrete 𝒮ᵒᵖ }))) Y)))))
  (Hom.base (Functor.map fiberInclusion f))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Grothendieck (hypothesis)
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
a b : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)
f g : a ⟶ b
heq : (Fiber.inducedFunctor ⋯).map f = (Fiber.inducedFunctor ⋯).map g
⊢ f = g
have heq₁ : Eq (α := obj fiberInclusion ((Fiber.inducedFunctor sorry).obj a) ⟶ obj fiberInclusion ((Fiber.inducedFunctor sorry).obj b))
  (Functor.map fiberInclusion ((Fiber.inducedFunctor sorry).map f))
  (Functor.map fiberInclusion ((Fiber.inducedFunctor sorry).map g))
Tactic: replace heq := fiberInclusion.congr_map heq
Cleared hypotheses: heq
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Grothendieck (goal)
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
⊢ (Fiber.inducedFunctor ⋯).EssSurj
have h : Function.Surjective (Fiber.inducedFunctor sorry).obj
Tactic: apply essSurj_of_surj
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Grothendieck (hypothesis)
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
Y : (forget F).Fiber S
⊢ ∃ (a : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)), (Fiber.inducedFunctor ⋯).obj a = Y
have hYS : (obj fiberInclusion Y).base = S
Tactic: have hYS : (fiberInclusion.obj Y).base = S := by simpa using Y.2
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Grothendieck (goal)
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
Y : (forget F).Fiber S
hYS : (obj fiberInclusion Y).base = S
⊢ ∃ (a : (↑(F.obj { as := op S : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)), (Fiber.inducedFunctor ⋯).obj a = Y
have h : (Fiber.inducedFunctor sorry).obj
    (Eq.rec (motive := fun (x : 𝒮) (h : (obj fiberInclusion Y).base = x) ↦
      (↑(F.obj { as := op x : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)) (obj fiberInclusion Y).fiber hYS) =
  Y
Tactic: use hYS ▸ (fiberInclusion.obj Y).fiber
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Grothendieck (goal)
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
Y : (forget F).Fiber S
hYS : (obj fiberInclusion Y).base = S
⊢ (Fiber.inducedFunctor ⋯).obj
      (Eq.rec (motive := fun (x : 𝒮) (h : (obj fiberInclusion Y).base = x) ↦
        (↑(F.obj { as := op x : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)) (obj fiberInclusion Y).fiber hYS) =
    Y
have h : obj fiberInclusion
    ((Fiber.inducedFunctor sorry).obj
      (Eq.rec (motive := fun (x : 𝒮) (h : (obj fiberInclusion Y).base = x) ↦
        (↑(F.obj { as := op x : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)) (obj fiberInclusion Y).fiber hYS)) =
  obj fiberInclusion Y
Tactic: apply fiberInclusion_obj_inj
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Grothendieck (goal)
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
Y : (forget F).Fiber S
hYS : (obj fiberInclusion Y).base = S
⊢ obj fiberInclusion
      ((Fiber.inducedFunctor ⋯).obj
        (Eq.rec (motive := fun (x : 𝒮) (h : (obj fiberInclusion Y).base = x) ↦
          (↑(F.obj { as := op x : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)) (obj fiberInclusion Y).fiber hYS)) =
    obj fiberInclusion Y
have h : (obj fiberInclusion
      ((Fiber.inducedFunctor sorry).obj
        (Eq.rec (motive := fun (x : 𝒮) (h : (obj fiberInclusion Y).base = x) ↦
          (↑(F.obj { as := op x : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)) (obj fiberInclusion Y).fiber hYS))).base =
  (obj fiberInclusion Y).base
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.Grothendieck (goal)
Goal:
𝒮 : Type u_1
inst : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
Y : (forget F).Fiber S
hYS : (obj fiberInclusion Y).base = S
h :
  (obj fiberInclusion
        ((Fiber.inducedFunctor ⋯).obj
          (Eq.rec (motive := fun (x : 𝒮) (h : (obj fiberInclusion Y).base = x) ↦
            (↑(F.obj { as := op x : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)) (obj fiberInclusion Y).fiber hYS))).base =
    (obj fiberInclusion Y).base
⊢ obj fiberInclusion
      ((Fiber.inducedFunctor ⋯).obj
        (Eq.rec (motive := fun (x : 𝒮) (h : (obj fiberInclusion Y).base = x) ↦
          (↑(F.obj { as := op x : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)) (obj fiberInclusion Y).fiber hYS)) =
    obj fiberInclusion Y
have h₁ : (obj fiberInclusion
      ((Fiber.inducedFunctor sorry).obj
        (Eq.rec (motive := fun (x : 𝒮) (h : (obj fiberInclusion Y).base = x) ↦
          (↑(F.obj { as := op x : LocallyDiscrete 𝒮ᵒᵖ }) : Type u_3)) (obj fiberInclusion Y).fiber hYS))).fiber ≍
  (obj fiberInclusion Y).fiber
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.HasFibers (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : CategoryTheory.Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : HasFibers.{u_1, u_2, v₂, u₂, v₁, u₁} p
S : 𝒮
a b : Fib.{u_1, u_2, v₂, u₂, v₁, u₁} p S
φ : a ⟶ b
⊢ p.IsHomLift (a := obj (ι S) a) (𝟙 S) (CategoryTheory.Functor.map (ι S) φ)
have apply : 𝟙 S = eqToHom sorry ≫ p.map (CategoryTheory.Functor.map (ι S) φ) ≫ eqToHom sorry
Tactic: apply of_fac p _ _ (proj_eq a) (proj_eq b)
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.HasFibers (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : CategoryTheory.Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : HasFibers.{u_1, u_2, v₂, u₂, v₁, u₁} p
S : 𝒮
a b : Fib.{u_1, u_2, v₂, u₂, v₁, u₁} p S
φ : a ⟶ b
⊢ 𝟙 S = eqToHom ⋯ ≫ p.map (CategoryTheory.Functor.map (ι S) φ) ≫ eqToHom ⋯
have rw : 𝟙 S =
  eqToHom sorry ≫
    (eqToHom sorry ≫ CategoryTheory.Functor.map (obj (const (Fib.{u_1, u_2, v₂, u₂, v₁, u₁} p S)) S) φ ≫ eqToHom sorry) ≫
      eqToHom sorry
Tactic: rw [← Functor.comp_map, Functor.congr_hom (comp_const S)]
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.HasFibers (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : CategoryTheory.Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : HasFibers.{u_1, u_2, v₂, u₂, v₁, u₁} p
inst_3 : p.IsPreFibered
R S : 𝒮
a : 𝒳
f : R ⟶ S
ha : p.obj a = S
| f
have rw : 𝟙 R ≫ f
Tactic: rw [← id_comp f]
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.HasFibers (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : CategoryTheory.Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : HasFibers.{u_1, u_2, v₂, u₂, v₁, u₁} p
inst_3 : p.IsPreFibered
R S : 𝒮
a : 𝒳
f : R ⟶ S
ha : p.obj a = S
⊢ p.IsCartesian (a := obj.{u_1, v₂, u_2, u₂} (C := Fib.{u_1, u_2, v₂, u₂, v₁, u₁} p R) (ι R) (mkPullback f ha)) f
    (pullbackMap f ha)
have conv : p.IsCartesian (a := obj.{u_1, v₂, u_2, u₂} (C := Fib.{u_1, u_2, v₂, u₂, v₁, u₁} p R) (ι R) (mkPullback f ha)) (𝟙 R ≫ f)
  (pullbackMap f ha)
Tactic: conv in f => rw [← id_comp f]
-- Lean 4 proof step from Mathlib.CategoryTheory.FiberedCategory.HasFibers (goal)
Goal:
𝒮 : Type u₁
𝒳 : Type u₂
inst : Category.{v₁, u₁} 𝒮
inst_1 : Category.{v₂, u₂} 𝒳
p : CategoryTheory.Functor.{v₂, v₁, u₂, u₁} 𝒳 𝒮
inst_2 : HasFibers.{u_1, u_2, v₂, u₂, v₁, u₁} p
inst_3 : p.IsPreFibered
R S : 𝒮
a : 𝒳
f : R ⟶ S
ha : p.obj a = S
⊢ p.IsCartesian (a := obj.{u_1, v₂, u_2, u₂} (C := Fib.{u_1, u_2, v₂, u₂, v₁, u₁} p R) (ι R) (mkPullback f ha))
    (𝟙 R ≫ f) (pullbackMap f ha)
have simp : p.IsCartesian (a := obj.{u_1, v₂, u_2, u₂} (C := Fib.{u_1, u_2, v₂, u₂, v₁, u₁} p R) (ι R) (mkPullback f ha)) f
  (Iso.hom (Fib.mkIsoSelf sorry) ≫ IsPreFibered.pullbackMap ha f)
Tactic: simp only [id_comp, pullbackMap]
-- 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 : 𝒳
⊢ p.IsHomLift (𝟙 (p.obj a)) (𝟙 a)
have rw : p.IsHomLift (p.map (𝟙 a)) (𝟙 a)
Tactic: rw [← p.map_id]
-- 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 : 𝒮
a : 𝒳
ha : p.obj a = R
⊢ p.IsHomLift (𝟙 R) (𝟙 a)
have refl : p.IsHomLift (𝟙 (p.obj a)) (𝟙 a)
Tactic: cases ha
Cleared hypotheses: R, 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 : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
inst_2 : p.IsHomLift f φ
⊢ p.obj a = R
have subst_hom_lift : ∀ {R S : 𝒮} {a_1 b_1 : 𝒳} [p.IsHomLift (p.map φ) φ], p.obj a = p.obj a
Tactic: subst_hom_lift p f φ
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 φ
⊢ p.obj b = S
have subst_hom_lift : ∀ {R S : 𝒮} {a_1 b_1 : 𝒳} [p.IsHomLift (p.map φ) φ], p.obj b = p.obj b
Tactic: subst_hom_lift p f φ
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 φ
⊢ f = eqToHom ⋯ ≫ p.map φ ≫ eqToHom ⋯
have subst_hom_lift : ∀ {R S : 𝒮} {a_1 b_1 : 𝒳} [inst_3 : p.IsHomLift (p.map φ) φ], p.map φ = eqToHom sorry ≫ p.map φ ≫ eqToHom sorry
Tactic: subst_hom_lift p f φ
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 φ
⊢ p.map φ = eqToHom ⋯ ≫ f ≫ eqToHom ⋯
have subst_hom_lift : ∀ {R S : 𝒮} {a_1 b_1 : 𝒳} [inst_3 : p.IsHomLift (p.map φ) φ], p.map φ = eqToHom sorry ≫ p.map φ ≫ eqToHom sorry
Tactic: subst_hom_lift p f φ
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
ha : p.obj a = R
hb : p.obj b = S
h : f = eqToHom ⋯ ≫ p.map φ ≫ eqToHom hb
⊢ p.IsHomLift f φ
have subst : p.IsHomLift (eqToHom sorry ≫ p.map φ ≫ eqToHom sorry) φ
Tactic: subst ha hb h
Cleared hypotheses: R, S, f, ha, hb, 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
ha : p.obj a = R
hb : p.obj b = S
h : p.map φ = eqToHom ha ≫ f ≫ eqToHom ⋯
⊢ p.IsHomLift f φ
have subst : ∀ (f : p.obj a ⟶ p.obj b) (h : p.map φ = eqToHom sorry ≫ f ≫ eqToHom sorry), p.IsHomLift f φ
Tactic: subst ha hb
Cleared hypotheses: R, S, f, ha, hb, 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₁} 𝒳 𝒮
a b : 𝒳
φ : a ⟶ b
f : p.obj a ⟶ p.obj b
h : p.map φ = eqToHom ⋯ ≫ f ≫ eqToHom ⋯
⊢ p.IsHomLift f φ
have obtain : ∀ (h : p.map φ = eqToHom sorry ≫ p.map φ ≫ eqToHom sorry), p.IsHomLift (p.map φ) φ
Tactic: obtain rfl : f = p.map φ := by simpa using h.symm
Cleared hypotheses: f, 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
ha : p.obj a = R
hb : p.obj b = S
h : p.map φ ≫ eqToHom hb = eqToHom ha ≫ f
⊢ p.IsHomLift f φ
have subst : ∀ (f : p.obj a ⟶ p.obj b) (h : p.map φ ≫ eqToHom sorry = eqToHom sorry ≫ f), p.IsHomLift f φ
Tactic: subst ha hb
Cleared hypotheses: R, S, f, ha, hb, 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₁} 𝒳 𝒮
a b : 𝒳
φ : a ⟶ b
f : p.obj a ⟶ p.obj b
h : p.map φ ≫ eqToHom ⋯ = eqToHom ⋯ ≫ f
⊢ p.IsHomLift f φ
have obtain : ∀ (h : p.map φ ≫ eqToHom sorry = eqToHom sorry ≫ p.map φ), p.IsHomLift (p.map φ) φ
Tactic: obtain rfl : f = p.map φ := by simpa using h.symm
Cleared hypotheses: f, 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 T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst_2 : p.IsHomLift f φ
inst_3 : p.IsHomLift g ψ
⊢ p.IsHomLift (f ≫ g) (φ ≫ ψ)
have h : CommSq (p.map (φ ≫ ψ)) (eqToHom sorry) (eqToHom sorry) (f ≫ g)
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 T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst_2 : p.IsHomLift f φ
inst_3 : p.IsHomLift g ψ
h : CommSq (p.map (φ ≫ ψ)) (eqToHom ⋯) (eqToHom ⋯) (f ≫ g)
⊢ p.IsHomLift (f ≫ g) (φ ≫ ψ)
have ha : 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 T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst_2 : p.IsHomLift f φ
inst_3 : p.IsHomLift g ψ
h : CommSq (p.map (φ ≫ ψ)) (eqToHom ⋯) (eqToHom ⋯) (f ≫ g)
ha : p.obj a = R
⊢ p.IsHomLift (f ≫ g) (φ ≫ ψ)
have hb : p.obj c = T
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 T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst_2 : p.IsHomLift f φ
inst_3 : p.IsHomLift g ψ
⊢ CommSq (p.map (φ ≫ ψ)) (eqToHom ⋯) (eqToHom ⋯) (f ≫ g)
have h : CommSq (p.map φ ≫ p.map ψ) (eqToHom sorry) (eqToHom sorry) (f ≫ g)
Tactic: rw [p.map_comp]
-- 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 T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst_2 : p.IsHomLift f φ
inst_3 : p.IsHomLift g ψ
⊢ CommSq (p.map (φ ≫ ψ)) (eqToHom ⋯) (eqToHom ⋯) (f ≫ g)
have h : CommSq (p.map φ ≫ p.map ψ) (eqToHom sorry) (eqToHom sorry) (f ≫ g)
Tactic: on_goal 1 => rw [p.map_comp]