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

Goal state before:
pp: case refine_1
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
K : Type u
α : K → Subtype J.PropSet
hK : HasCardinalLT K κ
t : (k : K) → ↑↑(α k) := fun k ↦ ⊤_ ↑↑(α k)
m : ↑J.obj := IsCardinalFiltered.max (fun k ↦ ↑(t k)) hK
S : Set ↑J.obj := (⋃ k, ↑(α k)) ∪ {m}
this : OrderTop ↑S := { top := ⟨m, ⋯⟩, le_top := ⋯ }
⊢ HasCardinalLT (↑S) κ

pp: case refine_2
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
K : Type u
α : K → Subtype J.PropSet
hK : HasCardinalLT K κ
t : (k : K) → ↑↑(α k) := fun k ↦ ⊤_ ↑↑(α k)
m : ↑J.obj := IsCardinalFiltered.max (fun k ↦ ↑(t k)) hK
S : Set ↑J.obj := (⋃ k, ↑(α k)) ∪ {m}
this : OrderTop ↑S := { top := ⟨m, ⋯⟩, le_top := ⋯ }
k : K
⊢ α k ≤ ⟨S, ⋯⟩

Tactic:
· have hκ : Cardinal.aleph0 ≤ κ :=  Cardinal.IsRegular.aleph0_le Fact.out
      exact hasCardinalLT_union hκ (hasCardinalLT_iUnion _ hK (fun k ↦ (α k).2.1))
        (hasCardinalLT_of_finite _ _ hκ)

Goal state after:
case refine_2
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
K : Type u
α : K → Subtype J.PropSet
hK : HasCardinalLT K κ
t : (k : K) → ↑↑(α k) := fun k ↦ ⊤_ ↑↑(α k)
m : ↑J.obj := IsCardinalFiltered.max (fun k ↦ ↑(t k)) hK
S : Set ↑J.obj := (⋃ k, ↑(α k)) ∪ {m}
this : OrderTop ↑S := { top := ⟨m, ⋯⟩, le_top := ⋯ }
k : K
⊢ α k ≤ ⟨S, ⋯⟩
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
⊢ IsIso (toSucc W Z)

Tactic:
obtain ⟨f, hf⟩ := (isLocal_isLocal_toSucc W Z _ hZ).2 (𝟙 _)

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 : (fun g ↦ toSucc W Z ≫ g) f = 𝟙 Z
⊢ IsIso (toSucc W Z)
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology

Goal state before:
pp: case mp.of
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : S = Presieve.ofArrows Y π
h' : IsIso (Sigma.desc π)
⊢ ∃ α, ∃ (_ : Finite α), ∃ Y π, Nonempty (IsColimit (Cofan.mk X π)) ∧ ∀ (a : α), (Sieve.generate S).arrows (π a)

Tactic:
refine ⟨α, inferInstance, Y, π, ?_, fun a ↦ ?_⟩

Goal state after:
case mp.of.refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : S = Presieve.ofArrows Y π
h' : IsIso (Sigma.desc π)
⊢ Nonempty (IsColimit (Cofan.mk X π))

case mp.of.refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : FinitaryPreExtensive C
X✝ : C
S✝ : Sieve X✝
X : C
S : Presieve X
α : Type
w✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : S = Presieve.ofArrows Y π
h' : IsIso (Sigma.desc π)
a : α
⊢ (Sieve.generate S).arrows (π a)
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
x✝ : Arrow (Sheaf J A)
⊢ Presheaf.IsLocallySurjective J
    ((MorphismProperty.FunctorialFactorizationData.functorCategory data Cᵒᵖ).i.app (Arrow.mk x✝.hom.hom))

Tactic:
apply Presheaf.isLocallySurjective_of_surjective

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
x✝ : Arrow (Sheaf J A)
⊢ ∀ (U : Cᵒᵖ),
    Function.Surjective
      ⇑(ConcreteCategory.hom
          (((MorphismProperty.FunctorialFactorizationData.functorCategory data Cᵒᵖ).i.app (Arrow.mk x✝.hom.hom)).app U))
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
this : HasPullback π π
hP :
  ∀
    (b :
      (fun X ↦ X)
        ↑{x |
            (ConcreteCategory.hom (P.map (pullback.fst π π).op)) x =
              (ConcreteCategory.hom (P.map (pullback.snd π π).op)) x}),
    ∃! a, (ConcreteCategory.hom (mapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯)) a = b
b : P.obj (op X)
hb : (ConcreteCategory.hom (P.map c.fst.op)) b = (ConcreteCategory.hom (P.map c.snd.op)) b
h₁ : ((pullbackIsPullback π π).conePointUniqueUpToIso hc).hom ≫ c.fst = pullback.fst π π
⊢ (ConcreteCategory.hom (P.map (((pullbackIsPullback π π).conePointUniqueUpToIso hc).hom ≫ c.fst).op)) b =
    (ConcreteCategory.hom (P.map (pullback.snd π π).op)) b

Tactic:
op_comp,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
X B : C
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
this : HasPullback π π
hP :
  ∀
    (b :
      (fun X ↦ X)
        ↑{x |
            (ConcreteCategory.hom (P.map (pullback.fst π π).op)) x =
              (ConcreteCategory.hom (P.map (pullback.snd π π).op)) x}),
    ∃! a, (ConcreteCategory.hom (mapToEqualizer P π (pullback.fst π π) (pullback.snd π π) ⋯)) a = b
b : P.obj (op X)
hb : (ConcreteCategory.hom (P.map c.fst.op)) b = (ConcreteCategory.hom (P.map c.snd.op)) b
h₁ : ((pullbackIsPullback π π).conePointUniqueUpToIso hc).hom ≫ c.fst = pullback.fst π π
⊢ (ConcreteCategory.hom (P.map (c.fst.op ≫ ((pullbackIsPullback π π).conePointUniqueUpToIso hc).hom.op))) b =
    (ConcreteCategory.hom (P.map (pullback.snd π π).op)) b
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
X : C
S : Sieve X
this : Precoherent C
⊢ S ∈ (coherentTopology C) X ↔ S ∈ (F.inducedTopology (coherentTopology D)) X

Tactic:
← exists_effectiveEpiFamily_iff_mem_induced F X

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
X : C
S : Sieve X
this : Precoherent C
⊢ S ∈ (coherentTopology C) X ↔ ∃ α, ∃ (_ : Finite α), ∃ Y π, EffectiveEpiFamily Y π ∧ ∀ (a : α), S.arrows (π a)
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: case mpr
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
P : Cᵒᵖ ⥤ D
X B : C
π : X ⟶ B
inst✝ : HasPullback π π
⊢ Nonempty (IsLimit (P.mapCone (Sieve.ofArrows (fun x ↦ X) fun x ↦ π).arrows.cocone.op)) → SingleEqualizerCondition P π

Tactic:
· intro ⟨h⟩
    exact fun c hc ↦ ⟨(isLimit_forkOfι_equiv _ _ _ hc).symm h⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.IsStack

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsStack J
S : C
R : Sieve S
hR : R ∈ J S
hF : (F.toDescentData fun f ↦ f.obj.hom).FullyFaithful
this✝¹ : (F.toDescentData fun f ↦ f.obj.hom).Full
this✝ : (F.toDescentData fun f ↦ f.obj.hom).Faithful
this : (F.toDescentData fun f ↦ f.obj.hom).EssSurj
⊢ (F.toDescentData fun f ↦ f.obj.hom).IsEquivalence

Tactic:
(Tactic.exact
 "exact"
 (choice («term{}» "{" "}") (Term.structInst "{" [] (Term.structInstFields []) (Term.optEllipsis []) [] "}")))

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : 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
hf' : Sieve.ofArrows X' f' ∈ J S
D₁ D₂ : F.DescentData f
φ φ' : D₁ ⟶ D₂
hφ : (pullFunctor F ⋯).map φ = (pullFunctor F ⋯).map φ'
i : ι
this✝ :
  (Sieve.overEquiv (Over.mk (𝟙 (X i)))).symm (Sieve.pullback (f i) (Sieve.ofArrows X' f')) ∈
    (J.over (X i)) (Over.mk (𝟙 (X i)))
Z : Over (X i)
g : Z ⟶ Over.mk (𝟙 (X i))
Y : C
j : ι'
p : Z.left ⟶ X' j
hp : p ≫ f' j = Over.Hom.left g ≫ f i
this : Over.Hom.left g = Z.hom
ψ : D₁ ⟶ D₂
⊢ (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g.op)) (F.presheafHomObjHomEquiv (ψ.hom i)) =
    D₁.hom (Z.hom ≫ f i) Z.hom (p ≫ p' j) ⋯ ⋯ ≫
      pullHom ((F.map (p' j).op.toLoc).toFunctor.map (ψ.hom (α j))) p (p ≫ p' j) (p ≫ p' j) ⋯ ⋯ ≫
        D₂.hom (Z.hom ≫ f i) (p ≫ p' j) Z.hom ⋯ ⋯

Tactic:
obtain rfl : g = Over.homMk Z.hom := by cat_disch

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : 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
hf' : Sieve.ofArrows X' f' ∈ J S
D₁ D₂ : F.DescentData f
φ φ' : D₁ ⟶ D₂
hφ : (pullFunctor F ⋯).map φ = (pullFunctor F ⋯).map φ'
i : ι
this✝ :
  (Sieve.overEquiv (Over.mk (𝟙 (X i)))).symm (Sieve.pullback (f i) (Sieve.ofArrows X' f')) ∈
    (J.over (X i)) (Over.mk (𝟙 (X i)))
Z : Over (X i)
Y : C
j : ι'
p : Z.left ⟶ X' j
ψ : D₁ ⟶ D₂
hp : p ≫ f' j = Over.Hom.left (Over.homMk Z.hom ⋯) ≫ f i
this : Over.Hom.left (Over.homMk Z.hom ⋯) = Z.hom
⊢ (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map (Over.homMk Z.hom ⋯).op))
      (F.presheafHomObjHomEquiv (ψ.hom i)) =
    D₁.hom (Z.hom ≫ f i) Z.hom (p ≫ p' j) ⋯ ⋯ ≫
      pullHom ((F.map (p' j).op.toLoc).toFunctor.map (ψ.hom (α j))) p (p ≫ p' j) (p ≫ p' j) ⋯ ⋯ ≫
        D₂.hom (Z.hom ≫ f i) (p ≫ p' j) Z.hom ⋯ ⋯
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
inst✝ : HasGlobalSectionsFunctor J A
F : Sheaf J A
c : Cone F.obj
f : c.pt ⟶ F.coneΓ.pt
hf : ∀ (j : Cᵒᵖ), f ≫ F.coneΓ.π.app j = c.π.app j
⊢ (Functor.const Cᵒᵖ).map f ≫ F.coneΓ.π = c.π

Tactic:
ext j

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
inst✝¹ : HasWeakSheafify J A
inst✝ : HasGlobalSectionsFunctor J A
F : Sheaf J A
c : Cone F.obj
f : c.pt ⟶ F.coneΓ.pt
hf : ∀ (j : Cᵒᵖ), f ≫ F.coneΓ.π.app j = c.π.app j
j : Cᵒᵖ
⊢ ((Functor.const Cᵒᵖ).map f ≫ F.coneΓ.π).app j = c.π.app j
Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : 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
hf' : Sieve.ofArrows X' f' ∈ J S
D₁ D₂ : F.DescentData f
φ φ' : D₁ ⟶ D₂
hφ : (pullFunctor F ⋯).map φ = (pullFunctor F ⋯).map φ'
⊢ φ = φ'

Tactic:
ext i
    refine F.presheafHomObjHomEquiv.injective ?_i
    have : (Sieve.overEquiv (Over.mk (𝟙 (X i)))).symm
      (Sieve.pullback (f i) (Sieve.ofArrows X' f')) ∈ J.over (X i) _ := by
      simpa only [J.mem_over_iff, OrderIso.apply_symm_apply] using! J.pullback_stable (f i) hf'
    refine (((isSheaf_iff_isSheaf_of_type _ _).1
      (IsPrestack.isSheaf _ _ _)).isSeparated _ this).ext ?_
    rintro Z g ⟨Y, p, c, ⟨j⟩, hp⟩
    dsimp at p hp
    have : g.left = Z.hom := by simpa using! Over.w g
    have (ψ : D₁ ⟶ D₂) :
      (F.presheafHom _ _).map g.op (F.presheafHomObjHomEquiv (ψ.hom i)) =
        D₁.hom (Z.hom ≫ f i) Z.hom (p ≫ p' j) ≫
          pullHom ((F.map (p' j).op.toLoc).toFunctor.map (ψ.hom (α j))) p _ _ ≫
          D₂.hom (Z.hom ≫ f i) (p ≫ p' j) Z.hom := by
      obtain rfl : g = Over.homMk Z.hom := by cat_disch
      have := ψ.comm _ Z.hom (p ≫ p' j) rfl (by grind)
      dsimp [presheafHomObjHomEquiv, pullHom] at this ⊢
      simp [mapComp'_inv_naturality, Cat.Hom.comp_toFunctor,
        Functor.comp_obj, Cat.Hom.hom_inv_id_toNatTrans_app_assoc, ← reassoc_of% this,
        D₂.hom_self _ _ rfl, F.mapComp'_id_comp_inv_app, ← Functor.map_comp,
        F.mapComp'_id_comp_hom_app_assoc]
    replace hφ := congr_fun (congr_arg DescentData.Hom.hom hφ) j
    dsimp at hφ
    simp only [this, hφ]

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

Goal state before:
pp: case refine_2
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)
i : F.multicospanShape.L
h1 : hgf.a i ≫ F.p₁ (hgf.H i) = g.h₀ i ≫ f.h₀ (g.s₀ i)
h2 : t.ι (f.s₀ (g.s₀ i)) ≫ G.map (F.p₁ (hgf.H i)).op = t.ι i ≫ G.map (F.p₂ (hgf.H i)).op
⊢ Multifork.IsLimit.lift hE (fun a ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ⋯ ≫ G.map (g.h₀ i ≫ E.f (g.s₀ i)).op = t.ι i

Tactic:
op_comp,

Goal state after:
case refine_2
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)
i : F.multicospanShape.L
h1 : hgf.a i ≫ F.p₁ (hgf.H i) = g.h₀ i ≫ f.h₀ (g.s₀ i)
h2 : t.ι (f.s₀ (g.s₀ i)) ≫ G.map (F.p₁ (hgf.H i)).op = t.ι i ≫ G.map (F.p₂ (hgf.H i)).op
⊢ Multifork.IsLimit.lift hE (fun a ↦ t.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ⋯ ≫ G.map ((E.f (g.s₀ i)).op ≫ (g.h₀ i).op) =
    t.ι i
Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

Goal state before:
pp: case refine_2
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)
i : F.multicospanShape.L
h1 : hgf.a i ≫ F.p₁ (hgf.H i) = g.h₀ i ≫ f.h₀ (g.s₀ i)
h2 : t.ι (f.s₀ (g.s₀ i)) ≫ G.map (F.p₁ (hgf.H i)).op = t.ι i ≫ G.map (F.p₂ (hgf.H i)).op
⊢ t.ι (f.s₀ (g.s₀ i)) ≫ G.map (hgf.a i ≫ F.p₁ (hgf.H i)).op = t.ι i

Tactic:
op_comp,

Goal state after:
case refine_2
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)
i : F.multicospanShape.L
h1 : hgf.a i ≫ F.p₁ (hgf.H i) = g.h₀ i ≫ f.h₀ (g.s₀ i)
h2 : t.ι (f.s₀ (g.s₀ i)) ≫ G.map (F.p₁ (hgf.H i)).op = t.ι i ≫ G.map (F.p₂ (hgf.H i)).op
⊢ t.ι (f.s₀ (g.s₀ i)) ≫ G.map ((F.p₁ (hgf.H i)).op ≫ (hgf.a i).op) = t.ι i
Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

Goal state before:
pp: case refine_3
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)
m : t.pt ⟶ (F.multifork G).pt
hm : ∀ (i : F.multicospanShape.L), m ≫ (F.multifork G).ι i = t.ι i
i : E.multicospanShape.L
⊢ m ≫ G.map (f.h₀ i ≫ F.f (f.s₀ i)).op = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).op

Tactic:
op_comp,

Goal state after:
case refine_3
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)
m : t.pt ⟶ (F.multifork G).pt
hm : ∀ (i : F.multicospanShape.L), m ≫ (F.multifork G).ι i = t.ι i
i : E.multicospanShape.L
⊢ m ≫ G.map ((F.f (f.s₀ i)).op ≫ (f.h₀ i).op) = t.ι (f.s₀ i) ≫ G.map (f.h₀ i).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 : ι
Y₁ Y₂ Z : Over (X i)
g₁ : Z.left ⟶ Y₁.left
hg₁ : g₁ ≫ Y₁.hom = Z.hom
g₂ : Z.left ⟶ Y₂.left
hg₂ : g₂ ≫ Y₂.hom = Z.hom
fac : Over.homMk g₁ ⋯ ≫ Over.homMk Y₁.hom ⋯ = Over.homMk g₂ ⋯ ≫ Over.homMk Y₂.hom ⋯
Y✝ : C
j₁ : ι'
a₁ : (Over.forget (X i)).obj Y₁ ⟶ X' j₁
fac₁ : a₁ ≫ f' j₁ = (Over.forget (X i)).map (Over.homMk Y₁.hom ⋯) ≫ f i
Y : C
j₂ : ι'
a₂ : (Over.forget (X i)).obj Y₂ ⟶ X' j₂
fac₂ : a₂ ≫ f' j₂ = (Over.forget (X i)).map (Over.homMk Y₂.hom ⋯) ≫ f i
⊢ mor w φ Z.hom (g₁ ≫ a₁) ⋯ = mor w φ Z.hom (g₂ ≫ a₂) ⋯

Tactic:
apply mor_unique

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
F : Sheaf J (Type v)
sq : Square C
⊢ (sq.op.map ((yoneda ⋙ presheafToSheaf J (Type v)).op ⋙ yoneda.obj F)).IsPullback ↔ (sq.op.map F.obj).IsPullback

Tactic:
refine Square.IsPullback.iff_of_equiv _ _
    (((sheafificationAdjunction J (Type v)).homEquiv _ _).trans yonedaEquiv)
    (((sheafificationAdjunction J (Type v)).homEquiv _ _).trans yonedaEquiv)
    (((sheafificationAdjunction J (Type v)).homEquiv _ _).trans yonedaEquiv)
    (((sheafificationAdjunction J (Type v)).homEquiv _ _).trans yonedaEquiv) ?_ ?_ ?_ ?_
  all_goals
    ext x
    simp [Adjunction.homEquiv, yonedaEquiv_naturality]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
inst✝¹ : HasWeakSheafify J (Type v)
sq : Square C
inst✝ : Mono sq.f₁₃
H : ∀ (F : Sheaf J (Type v)), (sq.op.map F.obj).IsPullback
⊢ (sq.map (yoneda ⋙ presheafToSheaf J (Type v))).IsPushout

Tactic:
rw [Square.isPushout_iff_op_map_yoneda_isPullback]
    intro F
    exact (F.isPullback_square_op_map_yoneda_presheafToSheaf_yoneda_iff sq).2 (H F)

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝¹ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
h₁ : Sieve.ofArrows X' f' ∈ J S
h₂ : Sieve.ofArrows X' f' ≤ Sieve.ofArrows X f
inst✝ : (F.toDescentData f').IsEquivalence
α : ι' → ι
p : (i' : ι') → X' i' ⟶ X (α i')
hp : ∀ (i' : ι'), p i' ≫ f (α i') = f' i'
H : F.DescentData f ⥤ F.DescentData f'
h : H.FullyFaithful
e : F.toDescentData f ⋙ H ≅ F.toDescentData f'
this✝¹ : (F.toDescentData f).Faithful
this✝ : (F.toDescentData f).Full
this : (F.toDescentData f).EssSurj
⊢ (F.toDescentData f).IsEquivalence

Tactic:
(Tactic.exact
 "exact"
 (choice («term{}» "{" "}") (Term.structInst "{" [] (Term.structInstFields []) (Term.optEllipsis []) [] "}")))

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
M : A
F G : Cᵒᵖ ⥤ A
inst✝ : HasFunctorEnrichedHom A F G
X : C
f : (functorEnrichedHom A F G ⋙ coyoneda.obj (op M)).obj (op X)
⊢ end_.lift
      (fun j ↦
        curry (uncurry (f ≫ enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk j.hom))))
      ⋯ =
    f

Tactic:
ext j

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
M : A
F G : Cᵒᵖ ⥤ A
inst✝ : HasFunctorEnrichedHom A F G
X : C
f : (functorEnrichedHom A F G ⋙ coyoneda.obj (op M)).obj (op X)
j : Under (op X)
⊢ end_.lift
        (fun j ↦
          curry (uncurry (f ≫ enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk j.hom))))
        ⋯ ≫
      end_.π (diagram A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G)) j =
    f ≫ end_.π (diagram A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G)) j
Module: Mathlib.CategoryTheory.Sites.Monoidal

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
M : A
F G : Cᵒᵖ ⥤ A
inst✝ : HasFunctorEnrichedHom A F G
X : C
g : (presheafHom (F ⊗ (Functor.const Cᵒᵖ).obj M) G).obj (op X)
⊢ {
      app := fun j ↦
        uncurry
          (end_.lift (fun j ↦ curry (g.app (op (Over.mk j.hom.unop)))) ⋯ ≫
            enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j).hom.op)),
      naturality := ⋯ } =
    g

Tactic:
ext j

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
M : A
F G : Cᵒᵖ ⥤ A
inst✝ : HasFunctorEnrichedHom A F G
X : C
g : (presheafHom (F ⊗ (Functor.const Cᵒᵖ).obj M) G).obj (op X)
j : (Over X)ᵒᵖ
⊢ {
          app := fun j ↦
            uncurry
              (end_.lift (fun j ↦ curry (g.app (op (Over.mk j.hom.unop)))) ⋯ ≫
                enrichedHomπ A (Under.forget (op X) ⋙ F) (Under.forget (op X) ⋙ G) (Under.mk (unop j).hom.op)),
          naturality := ⋯ }.app
      j =
    g.app j
Module: Mathlib.CategoryTheory.Sites.Point.Over

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : LocallySmall.{w, v, u} C
Φ : J.Point
X : C
x : Φ.fiber.obj X
U : Over X
u : (Over.forget X ⋙ Φ.fiber).obj U
hu : u ∈ (FunctorToTypes.fromOverSubfunctor Φ.fiber x).obj U
R : Sieve U.left
hR : (Sieve.overEquiv U).symm R ∈ (J.over X) U
⊢ ∃ Y f,
    ∃ (_ : ((Sieve.overEquiv U).symm R).arrows f),
      ∃ y, (ConcreteCategory.hom ((FunctorToTypes.fromOverFunctor Φ.fiber x).map f)) y = ⟨u, hu⟩

Tactic:
simp only [mem_over_iff, OrderIso.apply_symm_apply] at hR

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : LocallySmall.{w, v, u} C
Φ : J.Point
X : C
x : Φ.fiber.obj X
U : Over X
u : (Over.forget X ⋙ Φ.fiber).obj U
hu : u ∈ (FunctorToTypes.fromOverSubfunctor Φ.fiber x).obj U
R : Sieve U.left
hR : R ∈ J U.left
⊢ ∃ Y f,
    ∃ (_ : ((Sieve.overEquiv U).symm R).arrows f),
      ∃ y, (ConcreteCategory.hom ((FunctorToTypes.fromOverFunctor Φ.fiber x).map f)) y = ⟨u, hu⟩