-- Mathlib/CategoryTheory/Functor/Flat.lean
/-- Representably flat functors preserve finite limits. -/
lemma preservesFiniteLimits_of_flat (F : C ⥤ D) [RepresentablyFlat F] :
    PreservesFiniteLimits F

Proof state:
case h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type v₁
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
m : s.pt ⟶ (F.mapCone c).pt
h : ∀ (j : J), m ≫ (F.mapCone c).π.app j = s.π.app j
⊢ ∀ (j : J), m ≫ (F.mapCone c).π.app j = s.π.app j

Tactic:
exact h

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type v₁
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
m : s.pt ⟶ (F.mapCone c).pt
h : ∀ (j : J), m ≫ (F.mapCone c).π.app j = s.π.app j
⊢ m = PreservesFiniteLimitsOfFlat.lift F hc s

Tactic:
apply PreservesFiniteLimitsOfFlat.uniq F hc

Result:
case h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type v₁
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
m : s.pt ⟶ (F.mapCone c).pt
h : ∀ (j : J), m ≫ (F.mapCone c).π.app j = s.π.app j
⊢ ∀ (j : J), m ≫ (F.mapCone c).π.app j = s.π.app j

case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type v₁
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
m : s.pt ⟶ (F.mapCone c).pt
h : ∀ (j : J), m ≫ (F.mapCone c).π.app j = s.π.app j
⊢ ∀ (j : J), PreservesFiniteLimitsOfFlat.lift F hc s ≫ (F.mapCone c).π.app j = s.π.app j

Proof state:
case h.preservesLimit.preserves
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type ?u.182404
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : J ⥤ C
c : Cone K
hc : IsLimit c
⊢ Nonempty (IsLimit (F.mapCone c))

Tactic:
constructor

Result:
case h.preservesLimit.preserves.val
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type ?u.182404
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : J ⥤ C
c : Cone K
hc : IsLimit c
⊢ IsLimit (F.mapCone c)

Proof state:
case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type v₁
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : J ⥤ C
c : Cone K
hc : IsLimit c
s : Cone (K ⋙ F)
m : s.pt ⟶ (F.mapCone c).pt
h : ∀ (j : J), m ≫ (F.mapCone c).π.app j = s.π.app j
⊢ ∀ (j : J), PreservesFiniteLimitsOfFlat.lift F hc s ≫ (F.mapCone c).π.app j = s.π.app j

Tactic:
exact PreservesFiniteLimitsOfFlat.fac F hc s

Result:
no goals

Proof state:
case h.preservesLimit.preserves
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type ?u.182404
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : J ⥤ C
⊢ ∀ {c : Cone K}, IsLimit c → Nonempty (IsLimit (F.mapCone c))

Tactic:
intro c hc

Result:
case h.preservesLimit.preserves
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type ?u.182404
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : J ⥤ C
c : Cone K
hc : IsLimit c
⊢ Nonempty (IsLimit (F.mapCone c))

Proof state:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type ?u.182404
𝒥✝ : SmallCategory J
x✝ : FinCategory J
⊢ PreservesLimitsOfShape J F

Tactic:
constructor

Result:
case h.preservesLimit
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type ?u.182404
𝒥✝ : SmallCategory J
x✝ : FinCategory J
⊢ autoParam (∀ {K : J ⥤ C}, PreservesLimit K F) _auto✝

Proof state:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
⊢ ∀ (J : Type ?u.182404) {𝒥 : SmallCategory J}, FinCategory J → PreservesLimitsOfShape J F

Tactic:
intro J _ _

Result:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type ?u.182404
𝒥✝ : SmallCategory J
x✝ : FinCategory J
⊢ PreservesLimitsOfShape J F

Proof state:
case h.preservesLimit
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type ?u.182404
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : J ⥤ C
⊢ PreservesLimit K F

Tactic:
constructor

Result:
case h.preservesLimit.preserves
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type ?u.182404
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : J ⥤ C
⊢ ∀ {c : Cone K}, IsLimit c → Nonempty (IsLimit (F.mapCone c))

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
⊢ PreservesFiniteLimits F

Tactic:
apply preservesFiniteLimits_of_preservesFiniteLimitsOfSize

Result:
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
⊢ ∀ (J : Type ?u.182404) {𝒥 : SmallCategory J}, FinCategory J → PreservesLimitsOfShape J F

Proof state:
case h.preservesLimit
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type ?u.182404
𝒥✝ : SmallCategory J
x✝ : FinCategory J
⊢ autoParam (∀ {K : J ⥤ C}, PreservesLimit K F) _auto✝

Tactic:
intro K

Result:
case h.preservesLimit
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : RepresentablyFlat F
J : Type ?u.182404
𝒥✝ : SmallCategory J
x✝ : FinCategory J
K : J ⥤ C
⊢ PreservesLimit K F