-- Mathlib/CategoryTheory/Sites/CoverPreserving.lean
theorem compatiblePreservingOfFlat {C : Type u₁} [Category.{v₁} C] {D : Type u₁} [Category.{v₁} D]
    (K : GrothendieckTopology D) (G : C ⥤ D) [RepresentablyFlat G] : CompatiblePreserving K G

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
⊢ f₁ = (c'.pt.hom ≫ G.map (c'.π.app left).right) ≫ eqToHom ⋯

Tactic:
erw [← (c'.π.app left).w]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
⊢ f₁ =
    ((Functor.fromPUnit c.pt).map (c'.π.app left).left ≫
        ((c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G).obj left).hom) ≫
      eqToHom ⋯

Proof state:
case compatible
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
eq₁ : f₁ = (c'.pt.hom ≫ G.map (c'.π.app left).right) ≫ eqToHom ⋯
eq₂ : f₂ = (c'.pt.hom ≫ G.map (c'.π.app right).right) ≫ eqToHom ⋯
⊢ ℱ.val.map f₁.op (x g₁ hg₁) = ℱ.val.map f₂.op (x g₂ hg₂)

Tactic:
conv_lhs => rw [eq₁]

Result:
case compatible
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
eq₁ : f₁ = (c'.pt.hom ≫ G.map (c'.π.app left).right) ≫ eqToHom ⋯
eq₂ : f₂ = (c'.pt.hom ≫ G.map (c'.π.app right).right) ≫ eqToHom ⋯
⊢ ℱ.val.map ((c'.pt.hom ≫ G.map (c'.π.app left).right) ≫ eqToHom ⋯).op (x g₁ hg₁) = ℱ.val.map f₂.op (x g₂ hg₂)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
⊢ G.obj ((c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G).obj left).right = G.obj Y₁

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
⊢ f₁ =
    ((Functor.fromPUnit c.pt).map (c'.π.app left).left ≫
        ((c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G).obj left).hom) ≫
      eqToHom ⋯

Tactic:
dsimp [c]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
⊢ f₁ = (𝟙 X ≫ f₁ ≫ 𝟙 (G.obj Y₁)) ≫ 𝟙 (G.obj Y₁)

Proof state:
case compatible
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
⊢ ℱ.val.map f₁.op (x g₁ hg₁) = ℱ.val.map f₂.op (x g₂ hg₂)

Tactic:
let c' := IsCofiltered.cone (c.toStructuredArrow ⋙ StructuredArrow.pre _ _ _)

Result:
case compatible
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
K : GrothendieckTopology D
G : C ⥤ D
inst✝ : RepresentablyFlat G
ℱ : Sheaf K (Type u_1)
Z : C
T : Presieve Z
x : FamilyOfElements (G.op ⋙ ℱ.val) T
hx : x.Compatible
Y₁ Y₂ : C
X : D
f₁ : X ⟶ G.obj Y₁
f₂ : X ⟶ G.obj Y₂
g₁ : Y₁ ⟶ Z
g₂ : Y₂ ⟶ Z
hg₁ : T g₁
hg₂ : T g₂
e : f₁ ≫ G.map g₁ = f₂ ≫ G.map g₂
c : Cone (cospan g₁ g₂ ⋙ G) :=
  (Cones.postcompose (diagramIsoCospan (cospan g₁ g₂ ⋙ G)).inv).obj (PullbackCone.mk f₁ f₂ e)
c' : Cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G) :=
  IsCofiltered.cone (c.toStructuredArrow ⋙ StructuredArrow.pre c.pt (cospan g₁ g₂) G)
⊢ ℱ.val.map f₁.op (x g₁ hg₁) = ℱ.val.map f₂.op (x g₂ hg₂)