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

Goal state before:
pp: C : Type u
D : Type u'
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
P : ObjectProperty C
hP : P.IsCardinalFilteredGenerator κ
inst✝² : G.IsCardinalAccessible κ
inst✝¹ : G.Full
inst✝ : G.Faithful
Y : D
X : C
hX : P X
e : F.obj X ≅ Y
hX' : isCardinalPresentable C κ X
⊢ isCardinalPresentable D κ Y

Tactic:
isCardinalPresentable_iff

Goal state after:
C : Type u
D : Type u'
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
P : ObjectProperty C
hP : P.IsCardinalFilteredGenerator κ
inst✝² : G.IsCardinalAccessible κ
inst✝¹ : G.Full
inst✝ : G.Faithful
Y : D
X : C
hX : P X
e : F.obj X ≅ Y
hX' : IsCardinalPresentable X κ
⊢ IsCardinalPresentable Y κ
Module: Mathlib.CategoryTheory.Preadditive.Schur

Goal state before:
pp: case mpr
C : Type u_1
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Preadditive C
𝕜 : Type u_2
inst✝⁷ : Field 𝕜
inst✝⁶ : IsAlgClosed 𝕜
inst✝⁵ : Linear 𝕜 C
inst✝⁴ : HasKernels C
X Y : C
inst✝³ : FiniteDimensional 𝕜 (X ⟶ X)
inst✝² : FiniteDimensional 𝕜 (X ⟶ Y)
inst✝¹ : Simple X
inst✝ : Simple Y
⊢ Nonempty (X ≅ Y) → finrank 𝕜 (X ⟶ Y) = 1

Tactic:
rintro ⟨f⟩
    have le_one := finrank_hom_simple_simple_le_one 𝕜 X Y
    have zero_lt : 0 < finrank 𝕜 (X ⟶ Y) :=
      finrank_pos_iff_exists_ne_zero.mpr ⟨f.hom, (isIso_iff_nonzero f.hom).mp inferInstance⟩
    lia

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

Goal state before:
pp: J : Type w
inst✝ : SmallCategory J
κ : Cardinal.{w}
D : Diagram J κ
e : J
h₁ h₂ : D.IsTerminal e
this : @lift J inst✝ κ D e h₁ = @lift J inst✝ κ D e h₂
⊢ h₁ = h₂

Tactic:
cases h₁

Goal state after:
case mk
J : Type w
inst✝ : SmallCategory J
κ : Cardinal.{w}
D : Diagram J κ
e : J
h₂ : D.IsTerminal e
prop_id✝ : D.W (𝟙 e)
lift✝ : {j : J} → D.P j → (j ⟶ e)
hlift✝ : ∀ {j : J} (hj : D.P j), D.W (lift✝ hj)
uniq✝ : ∀ {j : J} (hj : D.P j) {φ : j ⟶ e}, D.W φ → lift✝ hj = φ
comm✝ : ∀ {i j : J} (f : i ⟶ j) (hf : D.W f), f ≫ lift✝ ⋯ = lift✝ ⋯
this :
  @lift J inst✝ κ D e { prop_id := prop_id✝, lift := lift✝, hlift := hlift✝, uniq := uniq✝, comm := comm✝ } =
    @lift J inst✝ κ D e h₂
⊢ { prop_id := prop_id✝, lift := lift✝, hlift := hlift✝, uniq := uniq✝, comm := comm✝ } = h₂
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: J : Type w
inst✝ : SmallCategory J
κ : Cardinal.{w}
x✝¹ x✝ : DiagramWithUniqueTerminal J κ
h₁ : x✝¹.W ≤ x✝.W ∧ x✝¹.P ≤ x✝.P
h₂ : x✝.W ≤ x✝¹.W ∧ x✝.P ≤ x✝¹.P
⊢ x✝¹ = x✝

Tactic:
by
    ext : 1
    · exact le_antisymm h₁.1 h₂.1
    · exact le_antisymm h₁.2 h₂.2

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

Goal state before:
pp: κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
left✝ : HasCardinalLT (↑J.obj) κ
right✝ : HasTerminal ↑J.obj
⊢ isCardinalPresentable (CardinalDirectedPoset κ) κ J

Tactic:
isCardinalPresentable_iff,

Goal state after:
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
left✝ : HasCardinalLT (↑J.obj) κ
right✝ : HasTerminal ↑J.obj
⊢ IsCardinalPresentable J κ
Module: Mathlib.CategoryTheory.Presentable.SharplyLT.Basic

Goal state before:
pp: κ₁ κ₂ : Cardinal.{w}
inst✝³ : Fact κ₁.IsRegular
inst✝² : Fact κ₂.IsRegular
h₀ : κ₁ < κ₂
h : ∀ (X : Type w), HasCardinalLT X κ₂ → ∃ Y, HasCardinalLT (↑Y) κ₂ ∧ IsCofinal Y
X : Type w
inst✝¹ : PartialOrder X
inst✝ : IsCardinalFiltered X κ₁
A : Set X
hA : HasCardinalLT (↑A) κ₂
⊢ ∃ B, A ⊆ B ∧ IsCardinalFiltered (↑B) κ₁ ∧ HasCardinalLT (↑B) κ₂

Tactic:
by
  choose Y hY hY' using fun (B : Set X) hB ↦ h B hB
  have hY'' (B : Set X) (hB : HasCardinalLT B κ₂)
      (C : SetCardinalLT κ₁ B) (hC : C ∈ Y B hB) :
    ∃ (m : X), ∀ (b : B), b ∈ C.val → b ≤ m :=
      ⟨IsCardinalFiltered.max (fun (c : C.val) ↦ c.val.val) C.prop,
        fun b hb ↦ leOfHom (IsCardinalFiltered.toMax
          (fun (c : C.val) ↦ c.val.val) C.prop ⟨_, hb⟩)⟩
  choose m hm using hY''
  -- The expected subset `B` is obtained as the union over
  -- all `j : κ₁.ord.ToType` of the transfinite iterations
  -- of the map `φ`
  exact ⟨⋃ j, transfiniteIterate (φ Y m) j A, subset_iUnion Y m A,
    isCardinalFiltered_iUnion h₀ Y hY hY' m hm A hA,
    hasCardinalLT_iUnion _ (by simpa [hasCardinalLT_iff_cardinal_mk_lt])
      (hasCardinalLT_transfiniteIterate_φ h₀ Y hY m A hA)⟩

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

Goal state before:
pp: case refine_2
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
j : J
f g : (fun X ↦ X) ((F ⋙ coyoneda.obj (op X)).obj j)
h : (hom (((coyoneda.obj (op X)).mapCocone c).ι.app j)) f = (hom (((coyoneda.obj (op X)).mapCocone c).ι.app j)) g
⊢ ∃ k f_1, (hom ((F ⋙ coyoneda.obj (op X)).map f_1)) f = (hom ((F ⋙ coyoneda.obj (op X)).map f_1)) g

Tactic:
choose k a hk using fun x ↦
          (Types.FilteredColimit.isColimit_eq_iff' hc _ _).1 (congr_hom h x)
        dsimp at f g h k a hk ⊢
        replace hk : ∀ x, F.map (a x) (f x) = F.map (a x) (g x) := by assumption
        obtain ⟨l, b, c, hl⟩ : ∃ (l : J) (c : j ⟶ l) (b : ∀ x, k x ⟶ l),
            ∀ x, a x ≫ b x = c := by
          let φ (x : X) : j ⟶ IsCardinalFiltered.max k hX :=
            a x ≫ IsCardinalFiltered.toMax k hX x
          exact ⟨IsCardinalFiltered.coeq φ hX,
            IsCardinalFiltered.toCoeq φ hX,
            fun x ↦ IsCardinalFiltered.toMax k hX x ≫ IsCardinalFiltered.coeqHom φ hX,
            fun x ↦ by simpa [φ] using IsCardinalFiltered.coeq_condition φ hX x⟩
        refine ⟨l, b, by ext x; simp [← hl x, hk]⟩

Goal state after:
Module: Mathlib.CategoryTheory.RepresentedBy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : C
x : F.obj (op X)
Y : C
⊢ (Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f.op)) x) ↔
    Function.Bijective (⇑(ConcreteCategory.hom ((uliftYonedaEquiv.symm { down := x }).app (op Y))) ∘ ⇑Equiv.ulift.symm)

Tactic:
← Function.Bijective.of_comp_iff' Equiv.ulift.{v}.bijective

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : C
x : F.obj (op X)
Y : C
⊢ (Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f.op)) x) ↔
    Function.Bijective
      (⇑Equiv.ulift ∘ ⇑(ConcreteCategory.hom ((uliftYonedaEquiv.symm { down := x }).app (op Y))) ∘ ⇑Equiv.ulift.symm)
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Precoherent C
W X : C
α : Type
inst✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone
x : Presieve.FamilyOfElements (yoneda.obj W) (Presieve.ofArrows Y π)
hx : x.Compatible
x_ext : Presieve.FamilyOfElements (yoneda.obj W) (Sieve.generate (Presieve.ofArrows Y π)).arrows := x.sieveExtend
hx_ext : x.sieveExtend.Compatible
S : Sieve X := Sieve.generate (Presieve.ofArrows Y π)
⊢ ∃! t, x.IsAmalgamation t

Tactic:
obtain ⟨t, t_amalg, t_uniq⟩ : ∃! t, x_ext.IsAmalgamation t :=
    (Sieve.forallYonedaIsSheaf_iff_colimit S).mpr ⟨h_colim⟩ W x_ext hx_ext

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Precoherent C
W X : C
α : Type
inst✝ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
H : EffectiveEpiFamily Y π
h_colim : Limits.IsColimit (Sieve.generate (Presieve.ofArrows Y π)).arrows.cocone
x : Presieve.FamilyOfElements (yoneda.obj W) (Presieve.ofArrows Y π)
hx : x.Compatible
x_ext : Presieve.FamilyOfElements (yoneda.obj W) (Sieve.generate (Presieve.ofArrows Y π)).arrows := x.sieveExtend
hx_ext : x.sieveExtend.Compatible
S : Sieve X := Sieve.generate (Presieve.ofArrows Y π)
t : (yoneda.obj W).obj (Opposite.op X)
t_amalg : x_ext.IsAmalgamation t
t_uniq : ∀ (y : (yoneda.obj W).obj (Opposite.op X)), (fun t ↦ x_ext.IsAmalgamation t) y → y = t
⊢ ∃! t, x.IsAmalgamation t
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves

Goal state before:
pp: case refine_1
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : IsSheaf (extensiveTopology C) F
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
⊢ PreservesLimit K F

Tactic:
rw [extensiveTopology, isSheaf_coverage] at hF

Goal state after:
case refine_1
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : ∀ {X : C}, ∀ R ∈ (extensiveCoverage C).coverings X, IsSheafFor F R
n : ℕ
K : Discrete (Fin n) ⥤ Cᵒᵖ
⊢ PreservesLimit K F
Module: Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves

Goal state before:
pp: case refine_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : PreservesFiniteProducts F
⊢ IsSheaf (extensiveCoverage C).toGrothendieck F

Tactic:
Presieve.isSheaf_coverage

Goal state after:
case refine_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : FinitaryPreExtensive C
inst✝ : FinitaryExtensive C
F : Cᵒᵖ ⥤ Type w
hF : PreservesFiniteProducts F
⊢ ∀ {X : C}, ∀ R ∈ (extensiveCoverage C).coverings X, IsSheafFor F R
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
⊢ coherentTopology C = F.inducedTopology (coherentTopology D)

Tactic:
ext X S
  have := F.reflects_precoherent
  rw [← exists_effectiveEpiFamily_iff_mem_induced F X]
  rw [← coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily S]

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
inst✝³ : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ Presheaf.IsLocallySurjective (extensiveTopology C) f →
    ∀ (X : C), Function.Surjective ⇑(ConcreteCategory.hom (f.app (op X)))

Tactic:
rw [Presheaf.isLocallySurjective_iff_whisker_forget (J := extensiveTopology C)]

Goal state after:
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
inst✝³ : FinitaryPreExtensive C
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
inst✝² : PreservesFiniteProducts F
inst✝¹ : PreservesFiniteProducts G
inst✝ : PreservesFiniteProducts (forget D)
⊢ Presheaf.IsLocallySurjective (extensiveTopology C) (Functor.whiskerRight f (forget D)) →
    ∀ (X : C), Function.Surjective ⇑(ConcreteCategory.hom (f.app (op X)))
Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
i j : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)
⊢ (cylinder f g).sieve₁' i j =
    Sieve.pullback
      (pullback.map ((cylinder f g).f i) ((cylinder f g).f j) (E.f i.fst) (E.f j.fst)
        (pullback.fst (pullback.lift (f.h₀ i.fst) (g.h₀ i.fst) ⋯) (F.toPullback i.snd))
        (pullback.fst (pullback.lift (f.h₀ j.fst) (g.h₀ j.fst) ⋯) (F.toPullback j.snd)) (𝟙 S) ⋯ ⋯)
      (E.sieve₁' i.fst j.fst)

Tactic:
refine le_antisymm ?_ ?_
  · rw [sieve₁', Sieve.ofArrows, Sieve.generate_le_iff]
    rintro - - ⟨k⟩
    refine ⟨E.Y k.down, pullback.snd _ _, E.toPullback k.down, Presieve.ofArrows.mk k.down, ?_⟩
    simp only [cylinder_Y, cylinder_f, toPullback_cylinder, pullback.condition]
  · rw [sieve₁', Sieve.ofArrows, ← Sieve.pullbackArrows_comm, Sieve.generate_le_iff]
    rintro Z u ⟨W, v, ⟨k⟩⟩
    simp_rw [← pullbackSymmetry_inv_comp_fst]
    apply (((cylinder f g).sieve₁' i j)).downward_closed
    rw [sieve₁']
    convert! Sieve.ofArrows_mk _ _ (ULift.up k)
    simp [toPullback_cylinder f g ⟨k⟩]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
K : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf K A
f : F ⟶ G
h : ∀ (i : ι), IsIso ((K.overPullback A (X i)).map f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
harrow : ∀ (I : S.Arrow), IsIso (f.hom.app (op I.Y))
I₁ I₂ : S.Arrow
r : I₁.Relation I₂
hZ : IsIso (f.hom.app (op r.Z))
⊢ (G.obj.map I₁.f.op ≫ G.obj.map r.g₁.op) ≫ inv (f.hom.app (op r.Z)) =
    (G.obj.map I₂.f.op ≫ G.obj.map r.g₂.op) ≫ inv (f.hom.app (op r.Z))

Tactic:
← G.obj.map_comp,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
K : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf K A
f : F ⟶ G
h : ∀ (i : ι), IsIso ((K.overPullback A (X i)).map f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
harrow : ∀ (I : S.Arrow), IsIso (f.hom.app (op I.Y))
I₁ I₂ : S.Arrow
r : I₁.Relation I₂
hZ : IsIso (f.hom.app (op r.Z))
⊢ G.obj.map (I₁.f.op ≫ r.g₁.op) ≫ inv (f.hom.app (op r.Z)) =
    (G.obj.map I₂.f.op ≫ G.obj.map r.g₂.op) ≫ inv (f.hom.app (op r.Z))
Module: Mathlib.CategoryTheory.Sites.LocalProperties

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
K : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf K A
f : F ⟶ G
h : ∀ (i : ι), IsIso ((K.overPullback A (X i)).map f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
harrow : ∀ (I : S.Arrow), IsIso (f.hom.app (op I.Y))
I₁ I₂ : S.Arrow
r : I₁.Relation I₂
hZ : IsIso (f.hom.app (op r.Z))
⊢ G.obj.map (I₁.f.op ≫ r.g₁.op) ≫ inv (f.hom.app (op r.Z)) =
    (G.obj.map I₂.f.op ≫ G.obj.map r.g₂.op) ≫ inv (f.hom.app (op r.Z))

Tactic:
← G.obj.map_comp,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
K : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf K A
f : F ⟶ G
h : ∀ (i : ι), IsIso ((K.overPullback A (X i)).map f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
harrow : ∀ (I : S.Arrow), IsIso (f.hom.app (op I.Y))
I₁ I₂ : S.Arrow
r : I₁.Relation I₂
hZ : IsIso (f.hom.app (op r.Z))
⊢ G.obj.map (I₁.f.op ≫ r.g₁.op) ≫ inv (f.hom.app (op r.Z)) = G.obj.map (I₂.f.op ≫ r.g₂.op) ≫ inv (f.hom.app (op r.Z))
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

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
D D₁ D₂ : F.DescentData f
e : (i : ι) → D₁.obj i ≅ D₂.obj i
comm :
  ∀ ⦃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),
    (F.map f₁.op.toLoc).toFunctor.map (e i₁).hom ≫ D₂.hom q f₁ f₂ ⋯ ⋯ =
      D₁.hom q f₁ f₂ ⋯ ⋯ ≫ (F.map f₂.op.toLoc).toFunctor.map (e i₂).hom
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
⊢ D₁.hom q f₁ f₂ ⋯ ⋯ ≫ (F.map f₂.op.toLoc).toFunctor.map (e i₂).hom =
    (F.map f₁.op.toLoc).toFunctor.map (e i₁).hom ≫ D₂.hom q f₁ f₂ ⋯ ⋯

Tactic:
comm q f₁ f₂ hf₁ hf₂

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
D D₁ D₂ : F.DescentData f
e : (i : ι) → D₁.obj i ≅ D₂.obj i
comm :
  ∀ ⦃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),
    (F.map f₁.op.toLoc).toFunctor.map (e i₁).hom ≫ D₂.hom q f₁ f₂ ⋯ ⋯ =
      D₁.hom q f₁ f₂ ⋯ ⋯ ≫ (F.map f₂.op.toLoc).toFunctor.map (e i₂).hom
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
⊢ D₁.hom q f₁ f₂ ⋯ ⋯ ≫ (F.map f₂.op.toLoc).toFunctor.map (e i₂).hom =
    D₁.hom q f₁ f₂ ⋯ ⋯ ≫ (F.map f₂.op.toLoc).toFunctor.map (e i₂).hom
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
s : ↑(presheafHom F G).sections
X : C
Y : Over X
H : (ConcreteCategory.hom ((presheafHom F G).map Y.hom.op)) (↑s (op X)) = ↑s (op Y.left)
⊢ ((ConcreteCategory.hom ((presheafHom F G).map Y.hom.op)) (↑s (op X))).app (op (Over.mk (𝟙 Y.left))) =
    (↑s (op X)).app (op Y)

Tactic:
apply presheafHom_map_app_op_mk_id

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)
S : J.MayerVietorisSquare
P : Cᵒᵖ ⥤ Type v'
h : S.SheafCondition P
x y : P.obj (op S.X₄)
h₁ : (ConcreteCategory.hom (P.map S.f₂₄.op)) x = (ConcreteCategory.hom (P.map S.f₂₄.op)) y
h₂ : (ConcreteCategory.hom (P.map S.f₃₄.op)) x = (ConcreteCategory.hom (P.map S.f₃₄.op)) y
⊢ S.toPullbackObj P x = S.toPullbackObj P y

Tactic:
by ext <;> assumption

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

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
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
D₁ D₂ : F.DescentData f
φ : D₁ ⟶ D₂
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
this :
  (F.map ((p' j₁).op.toLoc ≫ f₁.op.toLoc)).toFunctor.map (φ.hom (α j₁)) ≫ D₂.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ =
    D₁.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫ (F.map ((p' j₂).op.toLoc ≫ f₂.op.toLoc)).toFunctor.map (φ.hom (α j₂))
⊢ (F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc ((p' j₁).op.toLoc ≫ f₁.op.toLoc) ⋯).inv.toNatTrans.app (D₁.obj (α j₁)) ≫
      (F.map ((p' j₁).op.toLoc ≫ f₁.op.toLoc)).toFunctor.map (φ.hom (α j₁)) ≫
        D₂.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫
          (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc ((p' j₂).op.toLoc ≫ f₂.op.toLoc) ⋯).hom.toNatTrans.app
            (D₂.obj (α j₂)) =
    (F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc ((p' j₁).op.toLoc ≫ f₁.op.toLoc) ⋯).inv.toNatTrans.app (D₁.obj (α j₁)) ≫
      D₁.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫
        (F.map ((p' j₂).op.toLoc ≫ f₂.op.toLoc)).toFunctor.map (φ.hom (α j₂)) ≫
          (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc ((p' j₂).op.toLoc ≫ f₂.op.toLoc) ⋯).hom.toNatTrans.app
            (D₂.obj (α j₂))

Tactic:
reassoc_of% this

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
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
D₁ D₂ : F.DescentData f
φ : D₁ ⟶ D₂
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
this :
  (F.map ((p' j₁).op.toLoc ≫ f₁.op.toLoc)).toFunctor.map (φ.hom (α j₁)) ≫ D₂.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ =
    D₁.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫ (F.map ((p' j₂).op.toLoc ≫ f₂.op.toLoc)).toFunctor.map (φ.hom (α j₂))
⊢ (F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc ((p' j₁).op.toLoc ≫ f₁.op.toLoc) ⋯).inv.toNatTrans.app (D₁.obj (α j₁)) ≫
      D₁.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫
        (F.map ((p' j₂).op.toLoc ≫ f₂.op.toLoc)).toFunctor.map (φ.hom (α j₂)) ≫
          (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc ((p' j₂).op.toLoc ≫ f₂.op.toLoc) ⋯).hom.toNatTrans.app
            (D₂.obj (α j₂)) =
    (F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc ((p' j₁).op.toLoc ≫ f₁.op.toLoc) ⋯).inv.toNatTrans.app (D₁.obj (α j₁)) ≫
      D₁.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫
        (F.map ((p' j₂).op.toLoc ≫ f₂.op.toLoc)).toFunctor.map (φ.hom (α j₂)) ≫
          (F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc ((p' j₂).op.toLoc ≫ f₂.op.toLoc) ⋯).hom.toNatTrans.app
            (D₂.obj (α j₂))
Module: Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
F : Cᵒᵖ ⥤ Type w
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))
X : C
R : Presieve X
h : R ∈ K.coverings X
h' : Presieve.IsSheafFor F R
G : Subfunctor F := K.subsheafify 𝒮
x : Presieve.FamilyOfElements (K.subsheafify 𝒮).toFunctor R
hx : x.Compatible
t : F.obj (Opposite.op X)
ht : (x.map G.ι).IsAmalgamation t
uniq : ∀ (y : F.obj (Opposite.op X)), (fun t ↦ (x.map G.ι).IsAmalgamation t) y → y = t
⊢ ∃ t, x.IsAmalgamation t

Tactic:
exact ⟨⟨t, .amalgamate h (hx.map G.ι) (fun _ _ hr ↦ (x _ hr).property) ht⟩, .of_mono _ ht⟩

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : Coverage C
F : Cᵒᵖ ⥤ Type (max u v)
h : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
⊢ Presieve.IsSheaf K.toGrothendieck F

Tactic:
Presieve.isSheaf_coverage

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
K : Coverage C
F : Cᵒᵖ ⥤ Type (max u v)
h : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
⊢ ∀ {X : C}, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
Module: Mathlib.CategoryTheory.Sites.Types

Goal state before:
pp: S : Type uᵒᵖ ⥤ Type u
hs : IsSheaf typesGrothendieckTopology S
α : Type u
s : S.obj (op α)
⊢ typesGlue S hs α ⇑(ConcreteCategory.hom (eval S α s)) = s

Tactic:
apply (hs.isSheafFor _ (generate_discretePresieve_mem α)).isSeparatedFor.ext
  intro β f hf
  apply (IsSheafFor.valid_glue _ _ _ hf).trans
  simp only [eval, ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk, ← comp_apply,
    ← Functor.map_comp, ← op_comp]
  congr
  ext x
  exact congr_arg f (Classical.choose_spec hf x).symm

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: n d : ℕ
x : Fin n → ℕ
⊢ x ∈ box n d ↔ ∀ (i : Fin n), x i < d

Tactic:
by simp only [box, Fintype.mem_piFinset, mem_range]

Goal state after:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: n d : ℕ
a : Fin n.succ → ℕ
⊢ (a 0 + (∑ x, a x.succ * d ^ ↑x) * d) % d = a 0 % d

Tactic:
Nat.add_mul_mod_self_right

Goal state after:
n d : ℕ
a : Fin n.succ → ℕ
⊢ a 0 % d = a 0 % d
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: case hb
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
hn : n > 0
hd : d > 0
⊢ 1 ≤ 2 * ↑d - 1

Tactic:
rw [_root_.le_sub_iff_add_le]

Goal state after:
case hb
n d k : ℕ
hk : ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))
hn : n > 0
hd : d > 0
⊢ 1 + 1 ≤ 2 * ↑d
Module: Mathlib.Combinatorics.Additive.RuzsaCovering

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : ↑(#(A * B)) ≤ K * ↑(#B)
this : (F : Set G) → Decidable (F.PairwiseDisjoint fun x ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F).PairwiseDisjoint fun x ↦ x • B}
F : Finset G
hFmax : Maximal (fun x ↦ x ∈ C) F
⊢ ∃ F ⊆ A, ↑(#F) ≤ K ∧ A ⊆ F * (B / B)

Tactic:
simp only [C, mem_filter, mem_powerset] at hFmax

Goal state after:
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : ↑(#(A * B)) ≤ K * ↑(#B)
this : (F : Set G) → Decidable (F.PairwiseDisjoint fun x ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F).PairwiseDisjoint fun x ↦ x • B}
F : Finset G
hFmax : Maximal (fun x ↦ x ⊆ A ∧ (↑x).PairwiseDisjoint fun x ↦ x • B) F
⊢ ∃ F ⊆ A, ↑(#F) ≤ K ∧ A ⊆ F * (B / B)
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 64 ≤ N
⊢ 2 < √(log ↑N)

Tactic:
apply lt_sqrt_of_sq_lt

Goal state after:
N : ℕ
hN : 64 ≤ N
⊢ 2 ^ 2 < log ↑N