mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝³ : HasCoproduct D₁.obj₁
inst✝² : HasCoproduct D₁.obj₂
inst✝¹ : HasPushouts C
inst✝ : HasMulticoequalizer (D₂.multispanIndex W Z)
T : C
hT : W.isLocal T
φ₁ φ₂ : succ W Z ⟶ T
h : toStep W Z ≫ fromStep W Z ≫ φ₁ = toStep W Z ≫ fromStep W Z ≫ φ₂
⊢ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₁ =
    Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₂

Tactic:
dsimp

Goal state after:
case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝³ : HasCoproduct D₁.obj₁
inst✝² : HasCoproduct D₁.obj₂
inst✝¹ : HasPushouts C
inst✝ : HasMulticoequalizer (D₂.multispanIndex W Z)
T : C
hT : W.isLocal T
φ₁ φ₂ : succ W Z ⟶ T
h : toStep W Z ≫ fromStep W Z ≫ φ₁ = toStep W Z ≫ fromStep W Z ≫ φ₂
⊢ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₁ =
    Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ φ₂
Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝³ : HasCoproduct D₁.obj₁
inst✝² : HasCoproduct D₁.obj₂
inst✝¹ : HasPushouts C
inst✝ : HasMulticoequalizer (D₂.multispanIndex W Z)
hZ : W.isLocal Z
f : succ W Z ⟶ Z
hf : toSucc W Z ≫ f = 𝟙 Z
⊢ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ f ≫ toSucc W Z =
    Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ 𝟙 (succ W Z)

Tactic:
dsimp

Goal state after:
case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
Z : C
inst✝³ : HasCoproduct D₁.obj₁
inst✝² : HasCoproduct D₁.obj₂
inst✝¹ : HasPushouts C
inst✝ : HasMulticoequalizer (D₂.multispanIndex W Z)
hZ : W.isLocal Z
f : succ W Z ⟶ Z
hf : toSucc W Z ≫ f = 𝟙 Z
⊢ Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ f ≫ toSucc W Z =
    Multicoequalizer.π (D₂.multispanIndex W Z) PUnit.unit ≫ 𝟙 (succ W Z)
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Goal state before:
pp: κ₁ κ₂ : Cardinal.{w}
inst✝ : Fact κ₁.IsRegular
X : Type w
Y : (B : Set X) → HasCardinalLT (↑B) κ₂ → Set (SetCardinalLT κ₁ ↑B)
m : (B : Set X) → (hB : HasCardinalLT (↑B) κ₂) → (C : SetCardinalLT κ₁ ↑B) → C ∈ Y B hB → X
A : Set X
this✝ : Nonempty κ₁.ord.ToType
this : OrderBot κ₁.ord.ToType := WellFoundedLT.toOrderBot κ₁.ord.ToType
⊢ A ⊆ ⋃ j, transfiniteIterate (φ Y m) j A

Tactic:
exact subset_trans (by simp) (Set.subset_iUnion _ ⊥)

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Type

Goal state before:
pp: case refine_1
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst✝ : Fact κ.IsRegular
J : Type u
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
f : X ⟶ c.pt
j : X → J
g : (x : X) → (fun X ↦ X) (F.obj (j x))
hg : ∀ (x : X), (hom (c.ι.app (j x))) (g x) = (hom f) x
⊢ f =
    (hom (((coyoneda.obj (op X)).mapCocone c).ι.app (IsCardinalFiltered.max j hX)))
      (↾fun x ↦ (hom (F.map (IsCardinalFiltered.toMax j hX x))) (g x))

Tactic:
dsimp

Goal state after:
case refine_1
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst✝ : Fact κ.IsRegular
J : Type u
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
f : X ⟶ c.pt
j : X → J
g : (x : X) → (fun X ↦ X) (F.obj (j x))
hg : ∀ (x : X), (hom (c.ι.app (j x))) (g x) = (hom f) x
⊢ f = (↾fun x ↦ (hom (F.map (IsCardinalFiltered.toMax j hX x))) (g x)) ≫ c.ι.app (IsCardinalFiltered.max j hX)
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: case refine_1
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → ↑x.snd ⟶ m := fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst
hD : ∀ {i : ι}, ¬(D i).P m
H : ∀ {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m}, (D₂ D hι u).W f → f = φ ⟨i, ⟨j, hj⟩⟩
⊢ (D₂ D hι u).W (𝟙 m)

Tactic:
exact Or.inl (Or.inr ⟨⟨⟩⟩)

Goal state after:
Module: Mathlib.CategoryTheory.RegularCategory.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Regular C
X Y : C
f : X ⟶ Y
m : coequalizer (pullback.fst f f) (pullback.snd f f) ⟶ Y := coequalizer.desc f ⋯
e : X ⟶ coequalizer (pullback.fst f f) (pullback.snd f f) := coequalizer.π (pullback.fst f f) (pullback.snd f f)
k₁ : pullback m m ⟶ coequalizer (pullback.fst f f) (pullback.snd f f) := pullback.fst m m
k₂ : pullback m m ⟶ coequalizer (pullback.fst f f) (pullback.snd f f) := pullback.snd m m
⊢ (pullback.fst f f ≫ e) ≫ m = (pullback.snd f f ≫ e) ≫ m

Tactic:
by simp [m, e, pullback.condition]

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
D : DiagramWithUniqueTerminal J κ
m₁ : J
φ : (x : Subtype D.P) → ↑x ⟶ m₁
⊢ ∀ {i j : J} {f : i ⟶ j}, ((D₃ D m₁).W ⊔ MorphismProperty.ofHoms φ) f → (D₃ D m₁).P i

Tactic:
rintro i j f (hf | ⟨⟨j, hj⟩⟩)
    · exact (D₃ D m₁).src hf
    · exact Or.inl hj

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N : Bimod Y Z
⊢ coequalizer.π ((M.tensorBimod (regular Y)).actRight ▷ N.X)
        ((α_ (M.tensorBimod (regular Y)).X Y.X N.X).hom ≫ (M.tensorBimod (regular Y)).X ◁ N.actLeft) ≫
      ((isoOfIso
              { hom := AssociatorBimod.hom M (regular Y) N, inv := AssociatorBimod.inv M (regular Y) N, hom_inv_id := ⋯,
                inv_hom_id := ⋯ }
              ⋯ ⋯).hom ≫
          M.whiskerLeft
            (isoOfIso { hom := LeftUnitorBimod.hom N, inv := LeftUnitorBimod.inv N, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
                ⋯).hom).hom =
    coequalizer.π ((M.tensorBimod (regular Y)).actRight ▷ N.X)
        ((α_ (M.tensorBimod (regular Y)).X Y.X N.X).hom ≫ (M.tensorBimod (regular Y)).X ◁ N.actLeft) ≫
      (whiskerRight
          (isoOfIso { hom := RightUnitorBimod.hom M, inv := RightUnitorBimod.inv M, hom_inv_id := ⋯, inv_hom_id := ⋯ } ⋯
              ⋯).hom
          N).hom

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
X Y Z : Mon C
M : Bimod X Y
N : Bimod Y Z
⊢ coequalizer.π (TensorBimod.actRight M (regular Y) ▷ N.X)
        ((α_ (TensorBimod.X M (regular Y)) Y.X N.X).hom ≫ TensorBimod.X M (regular Y) ◁ N.actLeft) ≫
      AssociatorBimod.hom M (regular Y) N ≫
        colimMap
          (parallelPairHom (M.actRight ▷ TensorBimod.X (regular Y) N)
            ((α_ M.X Y.X (TensorBimod.X (regular Y) N)).hom ≫ M.X ◁ TensorBimod.actLeft (regular Y) N)
            (M.actRight ▷ N.X) ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft) ((M.X ⊗ Y.X) ◁ LeftUnitorBimod.hom N)
            (M.X ◁ LeftUnitorBimod.hom N) ⋯ ⋯) =
    coequalizer.π (TensorBimod.actRight M (regular Y) ▷ N.X)
        ((α_ (TensorBimod.X M (regular Y)) Y.X N.X).hom ≫ TensorBimod.X M (regular Y) ◁ N.actLeft) ≫
      colimMap
        (parallelPairHom (TensorBimod.actRight M (regular Y) ▷ N.X)
          ((α_ (TensorBimod.X M (regular Y)) Y.X N.X).hom ≫ TensorBimod.X M (regular Y) ◁ N.actLeft) (M.actRight ▷ N.X)
          ((α_ M.X Y.X N.X).hom ≫ M.X ◁ N.actLeft) (RightUnitorBimod.hom M ▷ Y.X ▷ N.X) (RightUnitorBimod.hom M ▷ N.X) ⋯
          ⋯)
Module: Mathlib.CategoryTheory.Sites.Adjunction

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{v_1, u_1} E
F : D ⥤ E
G : E ⥤ D
inst✝¹ : HasWeakSheafify J D
inst✝ : J.HasSheafCompose F
adj : G ⊣ F
X : Sheaf J E
⊢ ((adjunction J adj).unit.app X).hom =
    (Adjunction.whiskerRight Cᵒᵖ adj).unit.app X.obj ≫ whiskerRight (toSheafify J (X.obj ⋙ G)) F

Tactic:
by
  change (sheafToPresheaf _ _).map ((adjunction J adj).unit.app X) = _
  simp only [Functor.id_obj, Functor.comp_obj, whiskeringRight_obj_obj, adjunction,
    Adjunction.map_restrictFullyFaithful_unit_app, Adjunction.comp_unit_app,
    sheafificationAdjunction_unit_app, whiskeringRight_obj_map, Iso.refl_hom, NatTrans.id_app,
    Functor.comp_map, Functor.map_id, whiskerRight_id', Category.comp_id]
  rfl

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Adjunction

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u_1
inst✝ : Category.{v_1, u_1} E
F : D ⥤ E
G : E ⥤ D
adj : G ⊣ F
P Q : Cᵒᵖ ⥤ E
f : P ⟶ Q
hf : J.W f
this : F.IsRightAdjoint
⊢ J.W (((whiskeringRight Cᵒᵖ E D).obj G).map f)

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u_1
inst✝ : Category.{v_1, u_1} E
F : D ⥤ E
G : E ⥤ D
adj : G ⊣ F
P Q : Cᵒᵖ ⥤ E
f : P ⟶ Q
hf : J.W f
this : F.IsRightAdjoint
⊢ J.W (whiskerRight f G)
Module: Mathlib.CategoryTheory.Sites.Adjunction

Goal state before:
pp: case e'_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u_1
inst✝ : Category.{v_1, u_1} E
F : D ⥤ E
G : E ⥤ D
adj : G ⊣ F
P Q : Cᵒᵖ ⥤ E
f : P ⟶ Q
hf : J.W f
this : F.IsRightAdjoint
R : Cᵒᵖ ⥤ D
hR : Presheaf.IsSheaf J R
e_1✝ : (Q ⋙ G ⟶ R) = (((whiskeringRight Cᵒᵖ E D).obj G).obj Q ⟶ R)
e_2✝ : (P ⟶ ((whiskeringRight Cᵒᵖ D E).obj F).obj R) = (P ⟶ R ⋙ F)
g : Q ⋙ G ⟶ R
X : Cᵒᵖ
⊢ ((⇑((Adjunction.whiskerRight Cᵒᵖ adj).homEquiv P R) ∘ fun g ↦ whiskerRight f G ≫ g) g).app X =
    ((((Adjunction.whiskerRight Cᵒᵖ adj).homEquiv Q R).trans (ObjectProperty.isLocal.homEquiv hf (R ⋙ F) ⋯)) g).app X

Tactic:
dsimp

Goal state after:
case e'_3
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u_1
inst✝ : Category.{v_1, u_1} E
F : D ⥤ E
G : E ⥤ D
adj : G ⊣ F
P Q : Cᵒᵖ ⥤ E
f : P ⟶ Q
hf : J.W f
this : F.IsRightAdjoint
R : Cᵒᵖ ⥤ D
hR : Presheaf.IsSheaf J R
e_1✝ : (Q ⋙ G ⟶ R) = (((whiskeringRight Cᵒᵖ E D).obj G).obj Q ⟶ R)
e_2✝ : (P ⟶ ((whiskeringRight Cᵒᵖ D E).obj F).obj R) = (P ⟶ R ⋙ F)
g : Q ⋙ G ⟶ R
X : Cᵒᵖ
⊢ (((Adjunction.whiskerRight Cᵒᵖ adj).homEquiv P R) (whiskerRight f G ≫ g)).app X =
    f.app X ≫ (((Adjunction.whiskerRight Cᵒᵖ adj).homEquiv Q R) g).app X
Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison

Goal state before:
pp: case refine_2.of.a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y : C
I : Type
w✝ : Finite I
X : I → C
f : (a : I) → X a ⟶ Y
hT : EffectiveEpiFamily X f
⊢ (extensiveCoverage C ⊔ regularCoverage C).Saturate Y
    (generate (Presieve.ofArrows (fun x ↦ ∐ fun i ↦ X i) fun x ↦ Sigma.desc f))

pp: case refine_2.of.a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y : C
I : Type
w✝ : Finite I
X : I → C
f : (a : I) → X a ⟶ Y
hT : EffectiveEpiFamily X f
⊢ ∀ ⦃Y_1 : C⦄ ⦃f_1 : Y_1 ⟶ Y⦄,
    (generate (Presieve.ofArrows (fun x ↦ ∐ fun i ↦ X i) fun x ↦ Sigma.desc f)).arrows f_1 →
      (extensiveCoverage C ⊔ regularCoverage C).Saturate Y_1 (Sieve.pullback f_1 (generate (Presieve.ofArrows X f)))

Tactic:
· apply Coverage.Saturate.of
        simp only [Coverage.sup_covering, extensiveCoverage, regularCoverage, Set.mem_union,
          Set.mem_ofPred_eq]
        exact Or.inr ⟨_, Sigma.desc f, ⟨rfl, inferInstance⟩⟩

Goal state after:
case refine_2.of.a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y : C
I : Type
w✝ : Finite I
X : I → C
f : (a : I) → X a ⟶ Y
hT : EffectiveEpiFamily X f
⊢ ∀ ⦃Y_1 : C⦄ ⦃f_1 : Y_1 ⟶ Y⦄,
    (generate (Presieve.ofArrows (fun x ↦ ∐ fun i ↦ X i) fun x ↦ Sigma.desc f)).arrows f_1 →
      (extensiveCoverage C ⊔ regularCoverage C).Saturate Y_1 (Sieve.pullback f_1 (generate (Presieve.ofArrows X f)))
Module: Mathlib.CategoryTheory.Sites.EpiMono

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁵ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝⁴ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝³ : ConcreteCategory A FA
inst✝² : HasFunctorialSurjectiveInjectiveFactorization A
inst✝¹ : J.WEqualsLocallyBijective A
data : FunctorialSurjectiveInjectiveFactorizationData A
inst✝ : HasWeakSheafify J A
f : Arrow (Sheaf J A)
⊢ ((Arrow.leftFunc.whiskerLeft (inv (sheafificationAdjunction J A).counit) ≫
            (sheafToPresheaf J A).mapArrow.whiskerLeft
              (whiskerRight (MorphismProperty.FunctorialFactorizationData.functorCategory data Cᵒᵖ).i
                (presheafToSheaf J A))) ≫
          (sheafToPresheaf J A).mapArrow.whiskerLeft
              (whiskerRight (MorphismProperty.FunctorialFactorizationData.functorCategory data Cᵒᵖ).p
                (presheafToSheaf J A)) ≫
            Arrow.rightFunc.whiskerLeft (sheafificationAdjunction J A).counit).app
      f =
    Arrow.leftToRight.app f

Tactic:
dsimp

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁵ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝⁴ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝³ : ConcreteCategory A FA
inst✝² : HasFunctorialSurjectiveInjectiveFactorization A
inst✝¹ : J.WEqualsLocallyBijective A
data : FunctorialSurjectiveInjectiveFactorizationData A
inst✝ : HasWeakSheafify J A
f : Arrow (Sheaf J A)
⊢ ((inv (sheafificationAdjunction J A).counit).app f.left ≫
        (presheafToSheaf J A).map
          ((MorphismProperty.FunctorialFactorizationData.functorCategory data Cᵒᵖ).i.app (Arrow.mk f.hom.hom))) ≫
      (presheafToSheaf J A).map
          ((MorphismProperty.FunctorialFactorizationData.functorCategory data Cᵒᵖ).p.app (Arrow.mk f.hom.hom)) ≫
        (sheafificationAdjunction J A).counit.app f.right =
    f.hom
Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
X : C
x : G.obj (op X)
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), (Presheaf.imageSieve f x).arrows (π a)
y : (a : α) → F.obj (op (Y a)) := fun a ↦ Exists.choose ⋯
ht : IsLimit (Types.productLimitCone fun a ↦ F.obj (op (Y a))).cone :=
  (Types.productLimitCone fun a ↦ F.obj (op (Y a))).isLimit
ht' : IsLimit (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))) :=
  (Functor.Initial.isLimitWhiskerEquiv (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))).symm h.some.op
i : ((a : α) → F.obj (op (Y a))) ≅ F.obj (op X) :=
  ht.conePointsIsoOfNatIso (isLimitOfPreserves F ht') (Discrete.natIso fun x ↦ Iso.refl (F.obj (op (Y x.as))))
a : α
⊢ (ConcreteCategory.hom
        ((IsLimit.map (Types.productLimitCone fun a ↦ F.obj (op (Y a))).cone (isLimitOfPreserves F ht')
              (Discrete.natIso fun x ↦ Iso.refl (F.obj (op (Y x.as)))).hom ≫
            F.map (π a).op) ≫
          f.app (op (Y a))))
      y =
    (ConcreteCategory.hom (f.app (op (Y a)))) (Exists.choose ⋯)

Tactic:
IsLimit.map_π

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ Type w
f : F ⟶ G
inst✝¹ : PreservesFiniteProducts F
inst✝ : PreservesFiniteProducts G
X : C
x : G.obj (op X)
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : Nonempty (IsColimit (Cofan.mk X π))
h' : ∀ (a : α), (Presheaf.imageSieve f x).arrows (π a)
y : (a : α) → F.obj (op (Y a)) := fun a ↦ Exists.choose ⋯
ht : IsLimit (Types.productLimitCone fun a ↦ F.obj (op (Y a))).cone :=
  (Types.productLimitCone fun a ↦ F.obj (op (Y a))).isLimit
ht' : IsLimit (Cone.whisker (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))) :=
  (Functor.Initial.isLimitWhiskerEquiv (Discrete.opposite α).inverse (Cocone.op (Cofan.mk X π))).symm h.some.op
i : ((a : α) → F.obj (op (Y a))) ≅ F.obj (op X) :=
  ht.conePointsIsoOfNatIso (isLimitOfPreserves F ht') (Discrete.natIso fun x ↦ Iso.refl (F.obj (op (Y x.as))))
a : α
⊢ (ConcreteCategory.hom
        (((Types.productLimitCone fun a ↦ F.obj (op (Y a))).cone.π.app { as := a } ≫
            (Discrete.natIso fun x ↦ Iso.refl (F.obj (op (Y x.as)))).hom.app { as := a }) ≫
          f.app (op (Y a))))
      y =
    (ConcreteCategory.hom (f.app (op (Y a)))) (Exists.choose ⋯)
Module: Mathlib.CategoryTheory.Sites.GlobalSections

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u₂
inst✝¹ : Category.{v₂, u₂} A
inst✝ : HasWeakSheafify J A
X✝ Y✝ : Sheaf J (Type (max u v))
f : X✝ ⟶ Y✝
x : (Γ J (Type (max u v))).obj X✝
⊢ (ConcreteCategory.hom ((Γ J (Type (max u v))).map f ≫ (ΓObjEquivSections J Y✝).toIso.hom)).toFun x =
    (ConcreteCategory.hom
          ((ΓObjEquivSections J X✝).toIso.hom ≫
            (sheafToPresheaf J (Type (max u v)) ⋙ Functor.sectionsFunctor Cᵒᵖ).map f)).toFun
      x

Tactic:
exact ΓObjEquivSections_naturality J f x

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
A : Type u_1
inst✝ : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Cᵒᵖ ⥤ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
b : E.multicospanShape.R
⊢ (t.ι (f.s₀ (E.multicospanShape.fst b)) ≫ G.map (f.h₀ (E.multicospanShape.fst b)).op) ≫ (E.multicospanIndex G).fst b =
    (t.ι (f.s₀ (E.multicospanShape.snd b)) ≫ G.map (f.h₀ (E.multicospanShape.snd b)).op) ≫ (E.multicospanIndex G).snd b

Tactic:
dsimp

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
A : Type u_1
inst✝ : Category.{v_1, u_1} A
f : E.Hom F
g : F.Hom E
hgf : Homotopy (g.comp f) (Hom.id F)
G : Cᵒᵖ ⥤ A
hE : IsLimit (E.multifork G)
t : Multifork (F.multicospanIndex G)
b : E.multicospanShape.R
⊢ (t.ι (f.s₀ b.fst.1) ≫ G.map (f.h₀ b.fst.1).op) ≫ G.map (E.p₁ b.snd).op =
    (t.ι (f.s₀ b.fst.2) ≫ G.map (f.h₀ b.fst.2).op) ≫ G.map (E.p₂ b.snd).op
Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Z : C
q : Z ⟶ X i
j : ι'
a : Z ⟶ X' j
fac : a ≫ f' j = q ≫ f i
Z' : C
r : Z' ⟶ Z
r' : Z' ⟶ X i
a' : Z' ⟶ X' j
hr' : r ≫ q = r'
ha' : r ≫ a = a'
⊢ mor w φ r' a' ⋯ =
    (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map (Over.homMk r ⋯).op)) (mor w φ q a fac)

Tactic:
dsimp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Z : C
q : Z ⟶ X i
j : ι'
a : Z ⟶ X' j
fac : a ≫ f' j = q ≫ f i
Z' : C
r : Z' ⟶ Z
r' : Z' ⟶ X i
a' : Z' ⟶ X' j
hr' : r ≫ q = r'
ha' : r ≫ a = a'
⊢ mor w φ r' a' ⋯ = pullHom (mor w φ q a fac) r r' r' ⋯ ⋯
Module: Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D₁ D₂ : F.DescentData' sq sq₃
φ : D₁ ⟶ D₂
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
p : Y ⟶ (sq i₁ i₂).pullback
left✝ : p ≫ (sq i₁ i₂).p₁ = f₁
right✝ : p ≫ (sq i₁ i₂).p₂ = f₂
⊢ (F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
      (F.map (sq i₁ i₂).p₁.op.toLoc ≫ F.map p.op.toLoc).toFunctor.map (φ.hom i₁) ≫
        (F.map p.op.toLoc).toFunctor.map (D₂.hom i₁ i₂) ≫
          (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i₂) =
    ((F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
        (F.map p.op.toLoc).toFunctor.map (D₁.hom i₁ i₂) ≫
          (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₁.obj i₂)) ≫
      (F.map f₂.op.toLoc).toFunctor.map (φ.hom i₂)

Tactic:
dsimp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D₁ D₂ : F.DescentData' sq sq₃
φ : D₁ ⟶ D₂
Y : C
q : Y ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
p : Y ⟶ (sq i₁ i₂).pullback
left✝ : p ≫ (sq i₁ i₂).p₁ = f₁
right✝ : p ≫ (sq i₁ i₂).p₂ = f₂
⊢ (F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
      (F.map p.op.toLoc).toFunctor.map ((F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.map (φ.hom i₁)) ≫
        (F.map p.op.toLoc).toFunctor.map (D₂.hom i₁ i₂) ≫
          (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i₂) =
    ((F.mapComp' (sq i₁ i₂).p₁.op.toLoc p.op.toLoc f₁.op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
        (F.map p.op.toLoc).toFunctor.map (D₁.hom i₁ i₂) ≫
          (F.mapComp' (sq i₁ i₂).p₂.op.toLoc p.op.toLoc f₂.op.toLoc ⋯).inv.toNatTrans.app (D₁.obj i₂)) ≫
      (F.map f₂.op.toLoc).toFunctor.map (φ.hom i₂)