mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Mod

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
M : C
inst✝¹ : MonObj M
X : C
inst✝ : ModObj M X
H : ∀ (Z : C) (x : Z ⟶ X) (m : Z ⟶ M), lift m x ≫ leftSMul M X = lift (m • x) x
h : ∀ (Z : C) (f g : Z ⟶ X) (m : Z ⟶ M) (x : Z ⟶ X), lift m x ≫ leftSMul M X = lift f g ↔ x = g ∧ m • x = f
Z : C
⊢ (Function.Bijective fun x ↦ x ≫ leftSMul M X) ↔ ∀ (x y : Z ⟶ X), ∃! m, m • x = y

Tactic:
← Function.Bijective.of_comp_iff _ liftEquiv.bijective,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CartesianMonoidalCategory C
M : C
inst✝¹ : MonObj M
X : C
inst✝ : ModObj M X
H : ∀ (Z : C) (x : Z ⟶ X) (m : Z ⟶ M), lift m x ≫ leftSMul M X = lift (m • x) x
h : ∀ (Z : C) (f g : Z ⟶ X) (m : Z ⟶ M) (x : Z ⟶ X), lift m x ≫ leftSMul M X = lift f g ↔ x = g ∧ m • x = f
Z : C
⊢ Function.Bijective ((fun x ↦ x ≫ leftSMul M X) ∘ ⇑liftEquiv) ↔ ∀ (x y : Z ⟶ X), ∃! m, m • x = y
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

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
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
tfae_1_to_3 :
  (∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))
c : C
d : D
| IsIso ((pre (adj.unit.app d)).app (R.obj c))

Tactic:
rw [isIso_iff_isIso_yoneda_map]

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
inst✝⁴ : MonoidalCategory D
inst✝³ : SymmetricCategory D
inst✝² : MonoidalClosed D
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
L : D ⥤ C
adj : L ⊣ R
tfae_3_to_4 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
tfae_4_to_1 :
  (∀ (d d' : D), IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))) →
    ∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))
tfae_1_to_3 :
  (∀ (c : C) (d : D), IsIso (adj.unit.app ((ihom d).obj (R.obj c)))) → ∀ (d d' : D), IsIso (L.map (adj.unit.app d ▷ d'))
c : C
d : D
| ∀ (c_1 : D), IsIso ((yoneda.map ((pre (adj.unit.app d)).app (R.obj c))).app (Opposite.op c_1))
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon C
P : Bimod R S
⊢ hom P ≫ inv P = 𝟙 (TensorBimod.X (regular R) P)

Tactic:
by
  dsimp only [hom, inv, TensorBimod.X]
  ext; dsimp
  slice_lhs 1 2 => rw [coequalizer.π_desc]
  slice_lhs 1 2 => rw [leftUnitor_inv_naturality]
  slice_lhs 2 3 => rw [whisker_exchange]
  slice_lhs 3 3 => rw [← Iso.inv_hom_id_assoc (α_ R.X R.X P.X) (R.X ◁ P.actLeft)]
  slice_lhs 4 6 => rw [← Category.assoc, ← coequalizer.condition]
  slice_lhs 2 3 => rw [associator_inv_naturality_left]
  slice_lhs 3 4 => rw [← comp_whiskerRight, MonObj.one_mul]
  slice_rhs 1 2 => rw [Category.comp_id]
  monoidal

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁵ : Category.{v₂, u₂} V
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory V
U : C ⥤ V
inst✝² : DayConvolutionUnit U
F : C ⥤ V
inst✝¹ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝ : DayConvolution U F
y : C
⊢ can ▷ F.obj y ≫ (DayConvolution.unit U F).app (𝟙_ C, y) ≫ (leftUnitor U F).hom.app (𝟙_ C ⊗ y) =
    (λ_ (F.obj y)).hom ≫ F.map (λ_ y).inv

Tactic:
have := congrArg (fun t ↦ t.app (.mk PUnit.unit, y)) <|
      (corepresentableByLeft U F).homEquiv.rightInverse_symm <|
        ((leftUnitorCorepresentingIso F).symm.hom.app F) (𝟙 _)

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁵ : Category.{v₂, u₂} V
inst✝⁴ : MonoidalCategory C
inst✝³ : MonoidalCategory V
U : C ⥤ V
inst✝² : DayConvolutionUnit U
F : C ⥤ V
inst✝¹ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝ : DayConvolution U F
y : C
this :
  ((corepresentableByLeft U F).homEquiv
          ((corepresentableByLeft U F).homEquiv.symm
            ((ConcreteCategory.hom ((leftUnitorCorepresentingIso F).symm.hom.app F))
              (𝟙 (Opposite.unop (Opposite.op F)))))).app
      ({ as := PUnit.unit }, y) =
    ((ConcreteCategory.hom ((leftUnitorCorepresentingIso F).symm.hom.app F)) (𝟙 (Opposite.unop (Opposite.op F)))).app
      ({ as := PUnit.unit }, y)
⊢ can ▷ F.obj y ≫ (DayConvolution.unit U F).app (𝟙_ C, y) ≫ (leftUnitor U F).hom.app (𝟙_ C ⊗ y) =
    (λ_ (F.obj y)).hom ≫ F.map (λ_ y).inv
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C✝ : Type u₁
inst✝¹⁶ : Category.{v₁, u₁} C✝
V✝ : Type u₂
inst✝¹⁵ : Category.{v₂, u₂} V✝
inst✝¹⁴ : MonoidalCategory C✝
inst✝¹³ : MonoidalCategory V✝
C : Type u₁
inst✝¹² : Category.{v₁, u₁} C
V : Type u₂
inst✝¹¹ : Category.{v₂, u₂} V
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalCategory V
D : Type u₃
inst✝⁸ : Category.{v₃, u₃} D
inst✝⁷ : MonoidalCategoryStruct D
inst✝⁶ : LawfulDayConvolutionMonoidalCategoryStruct C V D
inst✝⁵ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝⁴ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
inst✝³ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
inst✝² :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝¹ :
  ∀ (v : V) (d : C × C),
    Limits.PreservesColimitsOfShape (CostructuredArrow ((𝟭 C).prod (Functor.fromPUnit (𝟙_ C))) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (𝟭 C)) d) (tensorRight v)
X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : D
f₁ : X₁✝ ⟶ Y₁✝
f₂ : X₂✝ ⟶ Y₂✝
f₃ : X₃✝ ⟶ Y₃✝
⊢ map (map ((ι C V D).map f₁) ((ι C V D).map f₂)) ((ι C V D).map f₃) ≫
      (DayConvolution.associator ((ι C V D).obj Y₁✝) ((ι C V D).obj Y₂✝) ((ι C V D).obj Y₃✝)).hom =
    (DayConvolution.associator ((ι C V D).obj X₁✝) ((ι C V D).obj X₂✝) ((ι C V D).obj X₃✝)).hom ≫
      map ((ι C V D).map f₁) (map ((ι C V D).map f₂) ((ι C V D).map f₃))

Tactic:
exact DayConvolution.associator_naturality
        ((ι C V D).map f₁) ((ι C V D).map f₂) ((ι C V D).map f₃)

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Goal state before:
pp: case comp
C : Type u
inst✝³ : Category.{v, u} C
K : Precoverage C
P Q : MorphismProperty C
X✝¹ Y✝¹ : C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderBaseChange
inst✝ : HasPullbacks C
Y X Z : C
f : X ⟶ Z
X✝ Y✝ : C
f' : X✝ ⟶ Y✝
hf' : sourceLocalClosure K P f'
R : Presieve X✝
hR : R ∈ K.coverings X✝
U✝ : C
g' : U✝ ⟶ X✝
hg' : R g'
ih : ∀ (W : C) (g : Y ⟶ Y✝) (fst : W ⟶ X✝) (snd : W ⟶ Y), IsPullback fst snd f' g → sourceLocalClosure K P snd
W : C
g : Y ⟶ Y✝
fst : W ⟶ U✝
snd : W ⟶ Y
h : IsPullback fst snd (g' ≫ f') g
⊢ sourceLocalClosure K P snd

Tactic:
| comp f' hf' R hR g' hg' ih =>

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Ind

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
H : P ≤ isFinitelyPresentable C
X Y : C
f : X ⟶ Y
inst✝ : IsFinitelyAccessibleCategory (Under X)
⊢ (∀ {Z : Under X} (g : Z ⟶ CategoryTheory.Under.mk f) [IsFinitelyPresentable Z], ∃ W u v, u ≫ v = g ∧ P.underObj W) ↔
    ∀ {Z : C} (p : X ⟶ Z) (g : Z ⟶ Y), isFinitelyPresentable C p → p ≫ g = f → ∃ W u v, u ≫ v = g ∧ P (p ≫ u)

Tactic:
refine ⟨fun H Z p g hp hpg ↦ ?_, fun H Z g hZ ↦ ?_⟩

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
H✝ : P ≤ isFinitelyPresentable C
X Y : C
f : X ⟶ Y
inst✝ : IsFinitelyAccessibleCategory (Under X)
H : ∀ {Z : Under X} (g : Z ⟶ CategoryTheory.Under.mk f) [IsFinitelyPresentable Z], ∃ W u v, u ≫ v = g ∧ P.underObj W
Z : C
p : X ⟶ Z
g : Z ⟶ Y
hp : isFinitelyPresentable C p
hpg : p ≫ g = f
⊢ ∃ W u v, u ≫ v = g ∧ P (p ≫ u)

case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
H✝ : P ≤ isFinitelyPresentable C
X Y : C
f : X ⟶ Y
inst✝ : IsFinitelyAccessibleCategory (Under X)
H : ∀ {Z : C} (p : X ⟶ Z) (g : Z ⟶ Y), isFinitelyPresentable C p → p ≫ g = f → ∃ W u v, u ≫ v = g ∧ P (p ≫ u)
Z : Under X
g : Z ⟶ CategoryTheory.Under.mk f
hZ : IsFinitelyPresentable Z
⊢ ∃ W u v, u ≫ v = g ∧ P.underObj W
Module: Mathlib.CategoryTheory.Preadditive.Comma

Goal state before:
pp: case h₁
A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ x✝ : u ⟶ v
⊢ (x✝¹ + x✝).left = (x✝ + x✝¹).left

Tactic:
simp [add_comm]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Comma

Goal state before:
pp: case h₂
A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ x✝ : u ⟶ v
⊢ (x✝¹ + x✝).right = (x✝ + x✝¹).right

Tactic:
simp [add_comm]

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

Goal state before:
pp: κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
h : κ ≤ κ'
x✝ : IsCardinalPresentable J κ'
X : Subtype (J.PropSetWithTop κ')
f : J ⟶ (functorOfPredicateSet (J.PropSetWithTop κ')).obj X
hf : Subtype.val ∘ ⇑(ConcreteCategory.hom f) = WithTop.some
⊢ Function.Injective WithTop.some

Tactic:
exact WithTop.coe_injective

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 j

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

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves

Goal state before:
pp: case mp
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
h : ∀ (E : D), Presieve.IsSheaf (extensiveTopology C) (F ⋙ coyoneda.obj (op E))
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
c : Cone K
hc : IsLimit c
⊢ (X : Dᵒᵖ) → IsLimit ((coyoneda.obj X).mapCone (F.mapCone c))

Tactic:
intro ⟨E⟩

Goal state after:
case mp
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ D
h : ∀ (E : D), Presieve.IsSheaf (extensiveTopology C) (F ⋙ coyoneda.obj (op E))
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
c : Cone K
hc : IsLimit c
E : D
⊢ IsLimit ((coyoneda.obj (op E)).mapCone (F.mapCone c))
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✝ : HasPullback π π
⊢ P.map π.op ≫ P.map (pullback.fst π π).op = P.map π.op ≫ P.map (pullback.snd π π).op

Tactic:
by
  simp only [← Functor.map_comp, ← op_comp, pullback.condition]

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: case mpr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : Cᵒᵖ ⥤ Type u_4
⊢ (∀ (X B : C) (π : X ⟶ B) [EffectiveEpi π] [inst : HasPullback π π], IsIso (equalizer.lift (P.map π.op) ⋯)) →
    EqualizerCondition P

Tactic:
intro hP
    apply EqualizerCondition.mk
    intro X B π _ _
    rw [mapToEqualizer_eq_comp, ← isIso_iff_bijective]
    infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective

Goal state before:
pp: case mp
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝⁶ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁵ : ConcreteCategory D FD
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝⁴ : Preregular C
inst✝³ : FinitaryPreExtensive C
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ Presheaf.IsLocallySurjective (coherentTopology C) f → Presheaf.IsLocallySurjective (regularTopology C) f

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
FD : D → D → Type u_3
CD : D → Type w
inst✝⁶ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁵ : ConcreteCategory D FD
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝⁴ : Preregular C
inst✝³ : FinitaryPreExtensive C
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ Presheaf.IsLocallySurjective (regularTopology C) f → Presheaf.IsLocallySurjective (coherentTopology C) f

Tactic:
· rw [Presheaf.isLocallySurjective_iff_whisker_forget,
      Presheaf.isLocallySurjective_iff_whisker_forget (J := regularTopology C)]
    exact regularTopology.isLocallySurjective_sheaf_of_types _

Goal state after:
case mpr
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
FD : D → D → Type u_3
CD : D → Type w
inst✝⁶ : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)
inst✝⁵ : ConcreteCategory D FD
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝⁴ : Preregular C
inst✝³ : FinitaryPreExtensive C
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ Presheaf.IsLocallySurjective (regularTopology C) f → Presheaf.IsLocallySurjective (coherentTopology C) f
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)
⊢ ∀ (E_1 : Multifork (F.multicospanIndex G)) (i : F.multicospanShape.L),
    Multifork.IsLimit.lift hE (fun a ↦ E_1.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ⋯ ≫ (F.multifork G).ι i = E_1.ι i

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)
⊢ ∀ (E_1 : Multifork (F.multicospanIndex G)) (m : E_1.pt ⟶ (F.multifork G).pt),
    (∀ (i : F.multicospanShape.L), m ≫ (F.multifork G).ι i = E_1.ι i) →
      m = Multifork.IsLimit.lift hE (fun a ↦ E_1.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ⋯

Tactic:
· intro t i
    simp only [multicospanIndex_left, multicospanShape_L, multifork_ι]
    have h1 := hgf.wl i
    have h2 := t.condition ⟨⟨_, _⟩, hgf.H i⟩
    dsimp at h1 h2
    rw [← g.w₀, op_comp, Functor.map_comp, ← E.multifork_ι, Multifork.IsLimit.fac_assoc,
      Category.assoc, ← Functor.map_comp, ← op_comp, ← h1, op_comp, Functor.map_comp,
      reassoc_of% h2, ← Functor.map_comp, ← op_comp, hgf.wr i]
    simp

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)
⊢ ∀ (E_1 : Multifork (F.multicospanIndex G)) (m : E_1.pt ⟶ (F.multifork G).pt),
    (∀ (i : F.multicospanShape.L), m ≫ (F.multifork G).ι i = E_1.ι i) →
      m = Multifork.IsLimit.lift hE (fun a ↦ E_1.ι (f.s₀ a) ≫ G.map (f.h₀ a).op) ⋯
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 : F.DescentData f
i₁ i₂ i₃ : ι
⊢ pullHom (D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p₁₂ (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯
        ⋯ ≫
      pullHom (D.hom (sq i₂ i₃).p (sq i₂ i₃).p₁ (sq i₂ i₃).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p₂₃ (sq₃ i₁ i₂ i₃).p₂
        (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯ =
    pullHom (D.hom (sq i₁ i₃).p (sq i₁ i₃).p₁ (sq i₁ i₃).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p₁₃ (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃
      ⋯ ⋯

Tactic:
D.pullHom_hom _ _ (sq₃ i₁ i₂ i₃).p,

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 : F.DescentData f
i₁ i₂ i₃ : ι
⊢ D.hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯ ≫
      pullHom (D.hom (sq i₂ i₃).p (sq i₂ i₃).p₁ (sq i₂ i₃).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p₂₃ (sq₃ i₁ i₂ i₃).p₂
        (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯ =
    pullHom (D.hom (sq i₁ i₃).p (sq i₁ i₃).p₁ (sq i₁ i₃).p₂ ⋯ ⋯) (sq₃ i₁ i₂ i₃).p₁₃ (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃
      ⋯ ⋯

case hq
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 : F.DescentData f
i₁ i₂ i₃ : ι
⊢ (sq₃ i₁ i₂ i₃).p₁₂ ≫ (sq i₁ i₂).p = (sq₃ i₁ i₂ i₃).p

case hf₁
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 : F.DescentData f
i₁ i₂ i₃ : ι
⊢ (sq i₁ i₂).p₁ ≫ f i₁ = (sq i₁ i₂).p

case hf₂
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 : F.DescentData f
i₁ i₂ i₃ : ι
⊢ (sq i₁ i₂).p₂ ≫ f i₂ = (sq i₁ i₂).p

case hgf₁
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 : F.DescentData f
i₁ i₂ i₃ : ι
⊢ (sq₃ i₁ i₂ i₃).p₁₂ ≫ (sq i₁ i₂).p₁ = (sq₃ i₁ i₂ i₃).p₁

case hgf₂
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 : F.DescentData f
i₁ i₂ i₃ : ι
⊢ (sq₃ i₁ i₂ i₃).p₁₂ ≫ (sq i₁ i₂).p₂ = (sq₃ i₁ i₂ i₃).p₂
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
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
W : C
q : W ⟶ S
i₁ i₂ : ι
f₁ : W ⟶ X i₁
f₂ : W ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
⊢ (Sieve.overEquiv (Over.mk f₁)) ((Sieve.overEquiv (Over.mk f₁)).symm (Sieve.pullback q (Sieve.ofArrows X' f'))) ∈
    J (Over.mk f₁).left

Tactic:
OrderIso.apply_symm_apply

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
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
W : C
q : W ⟶ S
i₁ i₂ : ι
f₁ : W ⟶ X i₁
f₂ : W ⟶ X i₂
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
⊢ Sieve.pullback q (Sieve.ofArrows X' f') ∈ J (Over.mk f₁).left
Module: Mathlib.CategoryTheory.Sites.SheafHom

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
y : (presheafHom F G).obj (op X)
h : ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))
Y : C
g : Y ⟶ X
hg : S.arrows g
W : Over Y
⊢ ((ConcreteCategory.hom ((presheafHom F G).map g.op)) y).app (op W) = (x g hg).app (op W)

Tactic:
refine (h W.left (W.hom ≫ g) (S.downward_closed hg _)).trans ?_

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
y : (presheafHom F G).obj (op X)
h : ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))
Y : C
g : Y ⟶ X
hg : S.arrows g
W : Over Y
⊢ (x (W.hom ≫ g) ⋯).app (op (Over.mk (𝟙 W.left))) = (x g hg).app (op W)
Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
γ₁ γ₂ : OneCochain G U
α : ZeroCochain G U
h : OneCohomologyRelation γ₁ γ₂ α
i j : I
T : C
a : T ⟶ U i
b : T ⟶ U j
⊢ ((ConcreteCategory.hom (G.map a.op)) (α i))⁻¹ * ((ConcreteCategory.hom (G.map a.op)) (α i) * γ₁.ev i j a b) =
    γ₁.ev i j a b * ((ConcreteCategory.hom (G.map b.op)) (α⁻¹ j) * (ConcreteCategory.hom (G.map b.op)) (α j))

Tactic:
inv_mul_cancel_left,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
γ₁ γ₂ : OneCochain G U
α : ZeroCochain G U
h : OneCohomologyRelation γ₁ γ₂ α
i j : I
T : C
a : T ⟶ U i
b : T ⟶ U j
⊢ γ₁.ev i j a b =
    γ₁.ev i j a b * ((ConcreteCategory.hom (G.map b.op)) (α⁻¹ j) * (ConcreteCategory.hom (G.map b.op)) (α j))
Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
γ₁ γ₂ γ₃ : OneCochain G U
α β : ZeroCochain G U
h₁₂ : OneCohomologyRelation γ₁ γ₂ α
h₂₃ : OneCohomologyRelation γ₂ γ₃ β
i j : I
T : C
a : T ⟶ U i
b : T ⟶ U j
⊢ (ConcreteCategory.hom (G.map a.op)) ((β * α) i) * γ₁.ev i j a b =
    γ₃.ev i j a b * (ConcreteCategory.hom (G.map b.op)) ((β * α) j)

Tactic:
dsimp
  rw [map_mul, map_mul, mul_assoc, h₁₂ i j a b, ← mul_assoc,
    h₂₃ i j a b, mul_assoc]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
hG : IsSheaf J G
⊢ IsSheaf J (presheafHom F G)

Tactic:
by
  rw [isSheaf_iff_isSheaf_of_type]
  intro X S hS
  exact presheafHom_isSheafFor F G S
    (fun _ _ => ((Presheaf.isSheaf_iff_isLimit J G).1 hG _ (J.pullback_stable _ hS)).some)

Goal state after: