awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type v₁
inst_2 : SmallCategory J
inst_3 : FinCategory J
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : RepresentablyFlat F
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j
h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j
α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow :=
  { app := fun (X : J) ↦ eqToHom ⋯, naturality := ⋯ }
α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow :=
  { app := fun (X : J) ↦ eqToHom ⋯, naturality := ⋯ }
c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₁ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₁)
c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₂ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := c₀.π.app Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := c₀.π.app Bicone.right
j : J
left_eq_1 :
  CommaMorphism.left (Functor.map (Functor.obj (Functor.const (Bicone J)) c₀.pt) (BiconeHom.left j)) ≫
      CommaMorphism.left (c₀.π.app (Bicone.diagram j)) =
    CommaMorphism.left (c₀.π.app Bicone.left) ≫ ((biconeMk J c₁ c₂).map (BiconeHom.left j)).left
e₁ :
  CommaMorphism.right (Functor.map (Functor.obj (Functor.const (Bicone J)) c₀.pt) (BiconeHom.left j)) ≫
      CommaMorphism.right (c₀.π.app (Bicone.diagram j)) =
    CommaMorphism.right (c₀.π.app Bicone.left) ≫ ((biconeMk J c₁ c₂).map (BiconeHom.left j)).right
left_eq :
  CommaMorphism.left (Functor.map (Functor.obj (Functor.const (Bicone J)) c₀.pt) (BiconeHom.right j)) ≫
      CommaMorphism.left (c₀.π.app (Bicone.diagram j)) =
    CommaMorphism.left (c₀.π.app Bicone.right) ≫ ((biconeMk J c₁ c₂).map (BiconeHom.right j)).left
⊢ Hom.right g₁ ≫ c.π.app j = Hom.right g₂ ≫ c.π.app j
have e₂ : CommaMorphism.right (Functor.map (Functor.obj (Functor.const (Bicone J)) c₀.pt) (BiconeHom.right j)) ≫
    CommaMorphism.right (c₀.π.app (Bicone.diagram j)) =
  CommaMorphism.right (c₀.π.app Bicone.right) ≫ ((biconeMk J c₁ c₂).map (BiconeHom.right j)).right
Tactic: injection c₀.π.naturality (BiconeHom.right j) with _ e₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type v₁
inst_2 : SmallCategory J
inst_3 : FinCategory J
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : RepresentablyFlat F
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j
h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j
α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow :=
  { app := fun (X : J) ↦ eqToHom ⋯, naturality := ⋯ }
α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow :=
  { app := fun (X : J) ↦ eqToHom ⋯, naturality := ⋯ }
c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₁ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₁)
c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₂ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := c₀.π.app Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := c₀.π.app Bicone.right
j : J
left_eq :
  CommaMorphism.left (Functor.map (Functor.obj (Functor.const (Bicone J)) c₀.pt) (BiconeHom.left j)) ≫
      CommaMorphism.left (c₀.π.app (Bicone.diagram j)) =
    CommaMorphism.left (c₀.π.app Bicone.left) ≫ ((biconeMk J c₁ c₂).map (BiconeHom.left j)).left
e₁ :
  CommaMorphism.right (Functor.map (Functor.obj (Functor.const (Bicone J)) c₀.pt) (BiconeHom.left j)) ≫
      CommaMorphism.right (c₀.π.app (Bicone.diagram j)) =
    CommaMorphism.right (c₀.π.app Bicone.left) ≫ ((biconeMk J c₁ c₂).map (BiconeHom.left j)).right
left_eq_1 :
  CommaMorphism.left (Functor.map (Functor.obj (Functor.const (Bicone J)) c₀.pt) (BiconeHom.right j)) ≫
      CommaMorphism.left (c₀.π.app (Bicone.diagram j)) =
    CommaMorphism.left (c₀.π.app Bicone.right) ≫ ((biconeMk J c₁ c₂).map (BiconeHom.right j)).left
e₂ :
  CommaMorphism.right (Functor.map (Functor.obj (Functor.const (Bicone J)) c₀.pt) (BiconeHom.right j)) ≫
      CommaMorphism.right (c₀.π.app (Bicone.diagram j)) =
    CommaMorphism.right (c₀.π.app Bicone.right) ≫ ((biconeMk J c₁ c₂).map (BiconeHom.right j)).right
⊢ Hom.right g₁ ≫ c.π.app j = Hom.right g₂ ≫ c.π.app j
have h : (c₀.pt.right ⟶ K.obj j) =
    ((Functor.obj (C := Bicone J) (Functor.obj (Functor.const (Bicone J)) c₀.pt) Bicone.left).right ⟶
      ((biconeMk J c₁ c₂).obj (Bicone.diagram j)).right) →
  c₁.pt.right = ((biconeMk J c₁ c₂).obj Bicone.left).right →
    K.obj j = ((biconeMk J c₁ c₂).obj (Bicone.diagram j)).right →
      c.π.app j = ((biconeMk J c₁ c₂).map (BiconeHom.left j)).right
Tactic: convert! e₁.symm.trans e₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type v₁
inst_2 : SmallCategory J
inst_3 : FinCategory J
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : RepresentablyFlat F
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j
h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j
α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow :=
  { app := fun (X : J) ↦ eqToHom ⋯, naturality := ⋯ }
α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow :=
  { app := fun (X : J) ↦ eqToHom ⋯, naturality := ⋯ }
c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₁ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₁)
c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₂ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := c₀.π.app Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := c₀.π.app Bicone.right
j : J
left_eq :
  CommaMorphism.left (Functor.map (Functor.obj (Functor.const (Bicone J)) c₀.pt) (BiconeHom.left j)) ≫
      CommaMorphism.left (c₀.π.app (Bicone.diagram j)) =
    CommaMorphism.left (c₀.π.app Bicone.left) ≫ ((biconeMk J c₁ c₂).map (BiconeHom.left j)).left
e₁ :
  CommaMorphism.right (Functor.map (Functor.obj (Functor.const (Bicone J)) c₀.pt) (BiconeHom.left j)) ≫
      CommaMorphism.right (c₀.π.app (Bicone.diagram j)) =
    CommaMorphism.right (c₀.π.app Bicone.left) ≫ ((biconeMk J c₁ c₂).map (BiconeHom.left j)).right
left_eq_1 :
  CommaMorphism.left (Functor.map (Functor.obj (Functor.const (Bicone J)) c₀.pt) (BiconeHom.right j)) ≫
      CommaMorphism.left (c₀.π.app (Bicone.diagram j)) =
    CommaMorphism.left (c₀.π.app Bicone.right) ≫ ((biconeMk J c₁ c₂).map (BiconeHom.right j)).left
e₂ :
  CommaMorphism.right (Functor.map (Functor.obj (Functor.const (Bicone J)) c₀.pt) (BiconeHom.right j)) ≫
      CommaMorphism.right (c₀.π.app (Bicone.diagram j)) =
    CommaMorphism.right (c₀.π.app Bicone.right) ≫ ((biconeMk J c₁ c₂).map (BiconeHom.right j)).right
h :
  (c₀.pt.right ⟶ K.obj j) =
      ((Functor.obj (C := Bicone J) (Functor.obj (Functor.const (Bicone J)) c₀.pt) Bicone.left).right ⟶
        ((biconeMk J c₁ c₂).obj (Bicone.diagram j)).right) →
    c₁.pt.right = ((biconeMk J c₁ c₂).obj Bicone.left).right →
      K.obj j = ((biconeMk J c₁ c₂).obj (Bicone.diagram j)).right →
        c.π.app j = ((biconeMk J c₁ c₂).map (BiconeHom.left j)).right
⊢ Hom.right g₁ ≫ c.π.app j = Hom.right g₂ ≫ c.π.app j
have h₃ : (c₀.pt.right ⟶ K.obj j) =
    ((Functor.obj (C := Bicone J) (Functor.obj (Functor.const (Bicone J)) c₀.pt) Bicone.left).right ⟶
      ((biconeMk J c₁ c₂).obj (Bicone.diagram j)).right) →
  c₂.pt.right = ((biconeMk J c₁ c₂).obj Bicone.right).right →
    K.obj j = ((biconeMk J c₁ c₂).obj (Bicone.diagram j)).right →
      c.π.app j = ((biconeMk J c₁ c₂).map (BiconeHom.right j)).right
Tactic: convert! e₁.symm.trans e₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type v₁
inst_2 : SmallCategory J
inst_3 : FinCategory J
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : RepresentablyFlat F
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j
h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j
α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow :=
  { app := fun (X : J) ↦ eqToHom ⋯, naturality := ⋯ }
α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow :=
  { app := fun (X : J) ↦ eqToHom ⋯, naturality := ⋯ }
c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₁ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₁)
c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₂ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := c₀.π.app Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := c₀.π.app Bicone.right
⊢ f₁ = f₂
have this : ∀ (j : J), Hom.right g₁ ≫ c.π.app j = Hom.right g₂ ≫ c.π.app j
Tactic: have : ∀ j : J, g₁.right ≫ c.π.app j = g₂.right ≫ c.π.app j := by
    intro j
    injection c₀.π.naturality (BiconeHom.left j) with _ e₁
    injection c₀.π.naturality (BiconeHom.right j) with _ e₂
    convert! e₁.symm.trans e₂ <;> simp [c₁, c₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type v₁
inst_2 : SmallCategory J
inst_3 : FinCategory J
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : RepresentablyFlat F
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j
h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j
α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow :=
  { app := fun (X : J) ↦ eqToHom ⋯, naturality := ⋯ }
α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow :=
  { app := fun (X : J) ↦ eqToHom ⋯, naturality := ⋯ }
c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₁ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₁)
c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₂ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := c₀.π.app Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := c₀.π.app Bicone.right
this : ∀ (j : J), Hom.right g₁ ≫ c.π.app j = Hom.right g₂ ≫ c.π.app j
⊢ { pt := c₀.pt.right, π := Functor.map (Functor.const J) (Hom.right g₁) ≫ c.π : Cone K } =
    { pt := c₀.pt.right, π := Functor.map (Functor.const J) (Hom.right g₂) ≫ c.π }
have e_π : Functor.map (Functor.const J) (Hom.right g₁) ≫ c.π = Functor.map (Functor.const J) (Hom.right g₂) ≫ c.π
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type v₁
inst_2 : SmallCategory J
inst_3 : FinCategory J
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : RepresentablyFlat F
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j
h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j
α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow :=
  { app := fun (X : J) ↦ eqToHom ⋯, naturality := ⋯ }
α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow :=
  { app := fun (X : J) ↦ eqToHom ⋯, naturality := ⋯ }
c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₁ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₁)
c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₂ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := c₀.π.app Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := c₀.π.app Bicone.right
this : ∀ (j : J), Hom.right g₁ ≫ c.π.app j = Hom.right g₂ ≫ c.π.app j
⊢ Functor.map (Functor.const J) (Hom.right g₁) ≫ c.π = Functor.map (Functor.const J) (Hom.right g₂) ≫ c.π
have e_π : ∀ (x : J),
  (Functor.map (Functor.const J) (Hom.right g₁) ≫ c.π).app x =
    (Functor.map (Functor.const J) (Hom.right g₂) ≫ c.π).app x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type v₁
inst_2 : SmallCategory J
inst_3 : FinCategory J
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : RepresentablyFlat F
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j
h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j
α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow :=
  { app := fun (X : J) ↦ eqToHom ⋯, naturality := ⋯ }
α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow :=
  { app := fun (X : J) ↦ eqToHom ⋯, naturality := ⋯ }
c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₁ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₁)
c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₂ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := c₀.π.app Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := c₀.π.app Bicone.right
this : ∀ (j : J), Hom.right g₁ ≫ c.π.app j = Hom.right g₂ ≫ c.π.app j
⊢ f₁ = f₂
have this₁ : c.extend (Hom.right g₁) = c.extend (Hom.right g₂)
Tactic: have : c.extend g₁.right = c.extend g₂.right := by
    unfold Cone.extend
    congr 1
    ext x
    apply this
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type v₁
inst_2 : SmallCategory J
inst_3 : FinCategory J
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : RepresentablyFlat F
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j
h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j
α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow :=
  { app := fun (X : J) ↦ eqToHom ⋯, naturality := ⋯ }
α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow :=
  { app := fun (X : J) ↦ eqToHom ⋯, naturality := ⋯ }
c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₁ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₁)
c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₂ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := c₀.π.app Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := c₀.π.app Bicone.right
this_1 : ∀ (j : J), Hom.right g₁ ≫ c.π.app j = Hom.right g₂ ≫ c.π.app j
this : c.extend (Hom.right g₁) = c.extend (Hom.right g₂)
⊢ Hom.right g₁ = hc.lift (c.extend (Hom.right g₁))
have x : ∀ (j : J), Hom.right g₁ ≫ c.π.app j = (c.extend (Hom.right g₁)).π.app j
Tactic: apply hc.uniq (c.extend _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type v₁
inst_2 : SmallCategory J
inst_3 : FinCategory J
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : RepresentablyFlat F
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j
h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j
α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow :=
  { app := fun (X : J) ↦ eqToHom ⋯, naturality := ⋯ }
α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow :=
  { app := fun (X : J) ↦ eqToHom ⋯, naturality := ⋯ }
c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₁ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₁)
c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₂ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := c₀.π.app Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := c₀.π.app Bicone.right
this_1 : ∀ (j : J), Hom.right g₁ ≫ c.π.app j = Hom.right g₂ ≫ c.π.app j
this : c.extend (Hom.right g₁) = c.extend (Hom.right g₂)
⊢ hc.lift (c.extend (Hom.right g₂)) = Hom.right g₂
have symm : Hom.right g₂ = hc.lift (c.extend (Hom.right g₂))
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type v₁
inst_2 : SmallCategory J
inst_3 : FinCategory J
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : RepresentablyFlat F
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j
h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j
α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow :=
  { app := fun (X : J) ↦ eqToHom ⋯, naturality := ⋯ }
α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow :=
  { app := fun (X : J) ↦ eqToHom ⋯, naturality := ⋯ }
c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₁ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₁)
c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₂ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := c₀.π.app Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := c₀.π.app Bicone.right
this_1 : ∀ (j : J), Hom.right g₁ ≫ c.π.app j = Hom.right g₂ ≫ c.π.app j
this : c.extend (Hom.right g₁) = c.extend (Hom.right g₂)
⊢ Hom.right g₂ = hc.lift (c.extend (Hom.right g₂))
have x : ∀ (j : J), Hom.right g₂ ≫ c.π.app j = (c.extend (Hom.right g₂)).π.app j
Tactic: apply hc.uniq (c.extend _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type v₁
inst_2 : SmallCategory J
inst_3 : FinCategory J
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : RepresentablyFlat F
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j
h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j
α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow :=
  { app := fun (X : J) ↦ eqToHom ⋯, naturality := ⋯ }
α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow :=
  { app := fun (X : J) ↦ eqToHom ⋯, naturality := ⋯ }
c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₁ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₁)
c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₂ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := c₀.π.app Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := c₀.π.app Bicone.right
this_1 : ∀ (j : J), Hom.right g₁ ≫ c.π.app j = Hom.right g₂ ≫ c.π.app j
this : c.extend (Hom.right g₁) = c.extend (Hom.right g₂)
⊢ f₁ = f₂
have this₁ : Hom.right g₁ = Hom.right g₂
Tactic: have : g₁.right = g₂.right := calc
    g₁.right = hc.lift (c.extend g₁.right) := by
      apply hc.uniq (c.extend _)
      simp
    _ = hc.lift (c.extend g₂.right) := by
      congr
    _ = g₂.right := by
      symm
      apply hc.uniq (c.extend _)
      simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type v₁
inst_2 : SmallCategory J
inst_3 : FinCategory J
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : RepresentablyFlat F
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j
h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j
α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow :=
  { app := fun (X : J) ↦ eqToHom ⋯, naturality := ⋯ }
α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow :=
  { app := fun (X : J) ↦ eqToHom ⋯, naturality := ⋯ }
c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₁ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₁)
c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₂ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := c₀.π.app Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := c₀.π.app Bicone.right
this_1 : ∀ (j : J), Hom.right g₁ ≫ c.π.app j = Hom.right g₂ ≫ c.π.app j
this_2 : c.extend (Hom.right g₁) = c.extend (Hom.right g₂)
this : Hom.right g₁ = Hom.right g₂
⊢ c₀.pt.hom ≫ F.map (Hom.right g₁) = c₀.pt.hom ≫ F.map (Hom.right g₂)
have rw : c₀.pt.hom ≫ F.map (Hom.right g₂) = c₀.pt.hom ≫ F.map (Hom.right g₂)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J : Type v₁
inst_2 : SmallCategory J
inst_3 : FinCategory J
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : RepresentablyFlat F
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
f₁ f₂ : s.pt ⟶ F.obj c.pt
h₁ : ∀ (j : J), f₁ ≫ (F.mapCone c).π.app j = s.π.app j
h₂ : ∀ (j : J), f₂ ≫ (F.mapCone c).π.app j = s.π.app j
α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow :=
  { app := fun (X : J) ↦ eqToHom ⋯, naturality := ⋯ }
α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow :=
  { app := fun (X : J) ↦ eqToHom ⋯, naturality := ⋯ }
c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₁ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₁)
c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
  (Cone.postcompose (Functor.whiskerRight α₂ (pre s.pt K F))).obj (c.toStructuredArrowCone F f₂)
c₀ : Cone (biconeMk J c₁ c₂) := IsCofiltered.cone (biconeMk J c₁ c₂)
g₁ : c₀.pt ⟶ c₁.pt := c₀.π.app Bicone.left
g₂ : c₀.pt ⟶ c₂.pt := c₀.π.app Bicone.right
this_1 : ∀ (j : J), Hom.right g₁ ≫ c.π.app j = Hom.right g₂ ≫ c.π.app j
this_2 : c.extend (Hom.right g₁) = c.extend (Hom.right g₂)
this : Hom.right g₁ = Hom.right g₂
⊢ f₁ = f₂
have f₃ : c₀.pt.hom ≫ F.map (Hom.right g₁) = c₀.pt.hom ≫ F.map (Hom.right g₂)
Tactic: calc
    f₁ = c₀.pt.hom ≫ F.map g₁.right := g₁.w.symm
    _ = c₀.pt.hom ≫ F.map g₂.right := by rw [this]
    _ = f₂ := g₂.w
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : RepresentablyFlat F
⊢ PreservesFiniteLimits F
have h : ∀ (J : Type v₁) {𝒥 : SmallCategory J} (x : FinCategory J), PreservesLimitsOfShape J F
Tactic: apply preservesFiniteLimits_of_preservesFiniteLimitsOfSize
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : RepresentablyFlat F
J : Type v₁
𝒥 : SmallCategory J
x : FinCategory J
⊢ PreservesLimitsOfShape J F
have h : autoParam (∀ {K : J ⥤ C}, PreservesLimit K F) PreservesLimitsOfShape.preservesLimit._autoParam
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Flat (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : RepresentablyFlat F
J : Type v₁
𝒥 : SmallCategory J
x : FinCategory J
K : J ⥤ C
⊢ PreservesLimit K F
have h : ∀ {c : Cone K} (hc : IsLimit c), Nonempty (IsLimit (F.mapCone c))
Tactic: constructor