mathlib-initiative/mathlib-tactics huggingface dataset:
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 : Type (max u v)
inst✝ : Unique X
X✝ Y✝ : Sheaf J (Type (max u v))
f : X✝ ⟶ Y✝
⊢ (Γ J (Type (max u v))).map f ≫ (ΓObjEquivHom J Y✝ X).toIso.hom =
    (ΓObjEquivHom J X✝ X).toIso.hom ≫ (coyoneda.obj (op ((constantSheaf J (Type (max u v))).obj X))).map f

Tactic:
by
    ext x
    exact ΓObjEquivHom_naturality J X f x

Goal state after:
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)
obj obj' : (i : ι) → ↑(F.obj { as := op (X i) })
hom :
  (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j)
Y Y' : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hq : g ≫ q = q'
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
p : Y ⟶ (sq i₁ i₂).pullback := ⋯.lift f₁ f₂ ⋯
⊢ (p ≫ (sq i₁ i₂).p₁).op.toLoc = f₁.op.toLoc

Tactic:
IsPullback.lift_fst

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)
obj obj' : (i : ι) → ↑(F.obj { as := op (X i) })
hom :
  (i j : ι) → (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j)
Y Y' : C
g : Y' ⟶ Y
q : Y ⟶ S
q' : Y' ⟶ S
i₁ i₂ : ι
f₁ : Y ⟶ X i₁
f₂ : Y ⟶ X i₂
gf₁ : Y' ⟶ X i₁
gf₂ : Y' ⟶ X i₂
hq : g ≫ q = q'
hf₁ : f₁ ≫ f i₁ = q
hf₂ : f₂ ≫ f i₂ = q
hgf₁ : g ≫ f₁ = gf₁
hgf₂ : g ≫ f₂ = gf₂
p : Y ⟶ (sq i₁ i₂).pullback := ⋯.lift f₁ f₂ ⋯
⊢ f₁.op.toLoc = f₁.op.toLoc
Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
S : C
E : J.OneHypercover S
F : J.OneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
i j : (PreOneHypercover.cylinder f g).I₀
⊢ (PreOneHypercover.cylinder f g).sieve₁' i j ∈
    J (Limits.pullback ((PreOneHypercover.cylinder f g).f i) ((PreOneHypercover.cylinder f g).f j))

Tactic:
rw [PreOneHypercover.sieve₁'_cylinder]
      exact J.pullback_stable _ (mem_sieve₁' E _ _)

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
φ : (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
H : (Sieve.overEquiv (Over.mk f₁)).symm (Sieve.pullback q (Sieve.ofArrows X' f')) ∈ (J.over (X i₁)) (Over.mk f₁)
Y : C
j : ι'
T : C
g : T ⟶ X' j
p : T ⟶ W
fac : g ≫ f' j = p ≫ q
⊢ (F.map (p ≫ f₁).op.toLoc).toFunctor.map (hom w hf' φ i₁) =
    (F.mapComp' f₁.op.toLoc p.op.toLoc (p ≫ f₁).op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
      (F.map p.op.toLoc).toFunctor.map (D₁.hom q f₁ f₂ ⋯ ⋯) ≫
        ((F.mapComp' f₂.op.toLoc p.op.toLoc (p ≫ f₂).op.toLoc ⋯).inv.toNatTrans.app (D₁.obj i₂) ≫
            (F.map (p ≫ f₂).op.toLoc).toFunctor.map (hom w hf' φ i₂) ≫
              (F.mapComp' f₂.op.toLoc p.op.toLoc (p ≫ f₂).op.toLoc ⋯).hom.toNatTrans.app (D₂.obj i₂)) ≫
          (F.map p.op.toLoc).toFunctor.map (D₂.hom q f₂ f₁ ⋯ ⋯) ≫
            (F.mapComp' f₁.op.toLoc p.op.toLoc (p ≫ f₁).op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i₁)

Tactic:
map_hom _ _ _ _ g (by grind),

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
H : (Sieve.overEquiv (Over.mk f₁)).symm (Sieve.pullback q (Sieve.ofArrows X' f')) ∈ (J.over (X i₁)) (Over.mk f₁)
Y : C
j : ι'
T : C
g : T ⟶ X' j
p : T ⟶ W
fac : g ≫ f' j = p ≫ q
⊢ mor w φ (p ≫ f₁) g ⋯ =
    (F.mapComp' f₁.op.toLoc p.op.toLoc (p ≫ f₁).op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
      (F.map p.op.toLoc).toFunctor.map (D₁.hom q f₁ f₂ ⋯ ⋯) ≫
        ((F.mapComp' f₂.op.toLoc p.op.toLoc (p ≫ f₂).op.toLoc ⋯).inv.toNatTrans.app (D₁.obj i₂) ≫
            (F.map (p ≫ f₂).op.toLoc).toFunctor.map (hom w hf' φ i₂) ≫
              (F.mapComp' f₂.op.toLoc p.op.toLoc (p ≫ f₂).op.toLoc ⋯).hom.toNatTrans.app (D₂.obj i₂)) ≫
          (F.map p.op.toLoc).toFunctor.map (D₂.hom q f₂ f₁ ⋯ ⋯) ≫
            (F.mapComp' f₁.op.toLoc p.op.toLoc (p ≫ f₁).op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i₁)
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
H : (Sieve.overEquiv (Over.mk f₁)).symm (Sieve.pullback q (Sieve.ofArrows X' f')) ∈ (J.over (X i₁)) (Over.mk f₁)
Y : C
j : ι'
T : C
g : T ⟶ X' j
p : T ⟶ W
fac : g ≫ f' j = p ≫ q
⊢ mor w φ (p ≫ f₁) g ⋯ =
    (F.mapComp' f₁.op.toLoc p.op.toLoc (p ≫ f₁).op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
      (F.map p.op.toLoc).toFunctor.map (D₁.hom q f₁ f₂ ⋯ ⋯) ≫
        ((F.mapComp' f₂.op.toLoc p.op.toLoc (p ≫ f₂).op.toLoc ⋯).inv.toNatTrans.app (D₁.obj i₂) ≫
            (F.map (p ≫ f₂).op.toLoc).toFunctor.map (hom w hf' φ i₂) ≫
              (F.mapComp' f₂.op.toLoc p.op.toLoc (p ≫ f₂).op.toLoc ⋯).hom.toNatTrans.app (D₂.obj i₂)) ≫
          (F.map p.op.toLoc).toFunctor.map (D₂.hom q f₂ f₁ ⋯ ⋯) ≫
            (F.mapComp' f₁.op.toLoc p.op.toLoc (p ≫ f₁).op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i₁)

Tactic:
map_hom _ _ _ _ g (by grind),

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
H : (Sieve.overEquiv (Over.mk f₁)).symm (Sieve.pullback q (Sieve.ofArrows X' f')) ∈ (J.over (X i₁)) (Over.mk f₁)
Y : C
j : ι'
T : C
g : T ⟶ X' j
p : T ⟶ W
fac : g ≫ f' j = p ≫ q
⊢ mor w φ (p ≫ f₁) g ⋯ =
    (F.mapComp' f₁.op.toLoc p.op.toLoc (p ≫ f₁).op.toLoc ⋯).hom.toNatTrans.app (D₁.obj i₁) ≫
      (F.map p.op.toLoc).toFunctor.map (D₁.hom q f₁ f₂ ⋯ ⋯) ≫
        ((F.mapComp' f₂.op.toLoc p.op.toLoc (p ≫ f₂).op.toLoc ⋯).inv.toNatTrans.app (D₁.obj i₂) ≫
            mor w φ (p ≫ f₂) g ⋯ ≫
              (F.mapComp' f₂.op.toLoc p.op.toLoc (p ≫ f₂).op.toLoc ⋯).hom.toNatTrans.app (D₂.obj i₂)) ≫
          (F.map p.op.toLoc).toFunctor.map (D₂.hom q f₂ f₁ ⋯ ⋯) ≫
            (F.mapComp' f₁.op.toLoc p.op.toLoc (p ≫ f₁).op.toLoc ⋯).inv.toNatTrans.app (D₂.obj i₁)
Module: Mathlib.CategoryTheory.Sites.MayerVietorisSquare

Goal state before:
pp: case left.left
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
W : C
a b : W ⟶ pairFunction sq.X₂ sq.X₃ WalkingPair.left
fac : a ≫ WalkingPair.casesOn WalkingPair.left sq.f₂₄ sq.f₃₄ = b ≫ WalkingPair.casesOn WalkingPair.left sq.f₂₄ sq.f₃₄
⊢ WalkingPair.casesOn WalkingPair.left s.fst s.snd ≫ F.obj.map a.op =
    WalkingPair.casesOn WalkingPair.left s.fst s.snd ≫ F.obj.map b.op

Tactic:
obtain rfl : a = b := by simpa only [← cancel_mono sq.f₂₄] using fac
            rfl

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

Goal state before:
pp: case hex
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
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
Y : C
g : Y ⟶ X
hg : S.arrows g
H : app hG x hx g = 𝟙 (F.obj (op Y)) ≫ (x (𝟙 Y ≫ g) ⋯).app (op (Over.mk (𝟙 Y)))
⊢ app hG x hx g = (x g hg).app (op (Over.mk (𝟙 Y)))

Tactic:
id_comp

Goal state after:
case hex
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
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
Y : C
g : Y ⟶ X
hg : S.arrows g
H : app hG x hx g = (x (𝟙 Y ≫ g) ⋯).app (op (Over.mk (𝟙 Y)))
⊢ app hG x hx g = (x g hg).app (op (Over.mk (𝟙 Y)))
Module: Mathlib.CategoryTheory.Sites.Point.Presheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X U : C
R : Sieve U
hR : R ∈ ⊥ U
x : (shrinkYoneda.{w, v, u}.flip.obj (op X)).obj U
⊢ R = ⊤

Tactic:
simpa using hR

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
J : GrothendieckTopology C
inst✝⁴ : HasPullbacks D
inst✝³ : HasPushouts D
inst✝² : IsRegularEpiCategory D
h : ∀ {F G : Sheaf J D} (f : F ⟶ G) [Epi f], ∃ I p i, Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst✝¹ : HasSheafify J D
inst✝ : Balanced (Sheaf J D)
F G : Sheaf J D
f : F ⟶ G
x✝ : Epi f
I : Cᵒᵖ ⥤ D
p : F.obj ⟶ I
i : I ⟶ G.obj
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  (presheafToSheaf J D).map f.hom =
    (sheafificationAdjunction J D).counit.app F ≫ f ≫ inv ((sheafificationAdjunction J D).counit.app G)
⊢ f =
    inv ((sheafificationAdjunction J D).counit.app F) ≫
      (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G

Tactic:
simp [h₁]

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
S : C
R R' : Presieve S
h : Sieve.generate R = Sieve.generate R'
⊢ F.IsStackFor R ↔ F.IsStackFor R'

Tactic:
by
  simp only [isStackFor_iff]
  obtain ⟨_, _, f, rfl⟩ := Presieve.exists_eq_ofArrows R
  obtain ⟨_, _, f', rfl⟩ := Presieve.exists_eq_ofArrows R'
  apply DescentData.isEquivalence_toDescentData_iff_of_sieve_eq
  simpa only [Sieve.ofArrows_category']

Goal state after:
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
⊢ IsPullback m ((Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F) (χ m) (truth C)

Tactic:
refine IsPullback.of_forall_isPullback_app fun X => ?_

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
X : Cᵒᵖ
⊢ IsPullback (m.app X) (((Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F).app X) ((χ m).app X)
    ((truth C).app X)
Module: Mathlib.CategoryTheory.Topos.Sheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Sheaf J (Type (max u v))
m : F ⟶ G
inst✝ : Mono m
⊢ Subfunctor.range (Presheaf.χ m.hom) ≤ closedSieves J

Tactic:
by
    intro X
    simp only [Subfunctor.range_obj, closedSieves_obj, Set.range_subset_iff]
    exact J.isClosed_χ_app_apply_of_isSheaf_of_isSeparated m.hom
      ((isSheaf_iff_isSheaf_of_type _ _).mp F.property)
      ((isSheaf_iff_isSheaf_of_type _ _).mp G.property).isSeparated _

Goal state after:
Module: Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
⊢ Precomp.map (mk₄ (S.fromBiprod F n₀) (S.δ F n₀ n₁ h) (S.toBiprod F n₁) (S.fromBiprod F n₁)) (S.toBiprod F n₀) 2 3 ⋯ =
    𝟙 (Precomp.obj (mk₄ (S.fromBiprod F n₀) (S.δ F n₀ n₁ h) (S.toBiprod F n₁) (S.fromBiprod F n₁)) (F.H' n₀ S.X₄) 2) ≫
      (Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).map (homOfLE ⋯)

Tactic:
id_comp

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
inst✝¹ : HasSheafify J AddCommGrpCat
inst✝ : HasExt (Sheaf J AddCommGrpCat)
S : J.MayerVietorisSquare
F : Sheaf J AddCommGrpCat
n₀ n₁ : ℕ
h : n₀ + 1 = n₁
⊢ Precomp.map (mk₄ (S.fromBiprod F n₀) (S.δ F n₀ n₁ h) (S.toBiprod F n₁) (S.fromBiprod F n₁)) (S.toBiprod F n₀) 2 3 ⋯ =
    (Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).map (homOfLE ⋯)
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

Goal state before:
pp: case e_a
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X)) =
    𝟙 ((shiftFunctor D n).obj ((shiftFunctor D (-n)).obj (F.obj (unop X)))) ≫
      (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X))

Tactic:
id_comp

Goal state after:
case e_a
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X)) =
    (shiftFunctorCompIsoId D (-n) n ⋯).hom.app (F.obj (unop X))
Module: Mathlib.CategoryTheory.Triangulated.Adjunction

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✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj (G.obj T.obj₁)
mem : Triangle.mk (G.map T.mor₁) f g ∈ distinguishedTriangles
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫ (Functor.commShiftIso F 1).hom.app (G.obj T.obj₁) ≫ (shiftFunctor D 1).map (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' : g ≫ (Functor.commShiftIso G 1).inv.app T.obj₁ = (adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃
P✝ : C
ψ : P✝ ⟶ G.obj T.obj₂
hφ : (ψ ≫ f) ≫ (adj.homEquiv Z T.obj₃) h = 0
⊢ (adj.homEquiv P✝ T.obj₃) ((adj.homEquiv P✝ T.obj₂).symm ψ ≫ T.mor₂) = (adj.homEquiv P✝ T.obj₃) 0

Tactic:
by simpa [homEquiv_counit, homEquiv_unit, ← h₁'] using hφ

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

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✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ F.map ((opShiftFunctorEquivalence C n).counitIso.inv.app X).unop =
    ((commShiftIso F.op n).inv.app (op ((shiftFunctor C n).obj (unop X)))).unop ≫
      ((shiftFunctor Dᵒᵖ n).map ((commShiftIso F n).hom.app (unop X)).op).unop ≫
        ((opShiftFunctorEquivalence D n).counitIso.inv.app (op (F.obj (unop X)))).unop

Tactic:
rw [← cancel_epi (F.map ((opShiftFunctorEquivalence C n).counitIso.hom.app X).unop),
    ← F.map_comp, ← unop_comp, Iso.inv_hom_id_app,
    map_opShiftFunctorEquivalence_counitIso_hom_app_unop]
  dsimp
  simp only [map_id, assoc, ← Functor.map_comp_assoc,
    ← unop_comp, Iso.inv_hom_id_app_assoc, ← op_comp,
    Iso.inv_hom_id_app]
  simp

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : DecidableEq β
A : Finset α
B : Finset β
f : α → β
hf : IsMulFreimanIso 2 (↑A) (↑B) f
s : Finset α
hsA : ↑s ⊆ ↑A
hcard : #s = mulRothNumber A
hs : ThreeGPFree ↑s
hfs : Set.InjOn f ↑s
this : ThreeGPFree ↑(image f s)
⊢ f '' ↑s ⊆ ↑B

Tactic:
exact (hf.bijOn.mapsTo.mono hsA Subset.rfl).image_subset

Goal state after:
Module: Mathlib.Combinatorics.Additive.FreimanHom

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
n : ℕ
hf : IsMulFreimanHom n A B f
s t : Finset α
hsA : ↑s ⊆ A
htA : ↑t ⊆ A
hs : s.card = n
ht : t.card = n
⊢ ∏ i ∈ s, i = ∏ i ∈ t, i → ∏ i ∈ s, f i = ∏ i ∈ t, f i

Tactic:
simpa using hf.map_prod_eq_map_prod hsA htA hs ht

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

Goal state before:
pp: case refine_2
n : ℕ
k : Fin (n + 1)
⊢ Set.SurjOn Nat.cast ↑(range ↑k) ↑(Iio k)

Tactic:
simp only [Set.SurjOn, coe_Iio, Set.subset_def, Set.mem_Iio, Set.mem_image, lt_def, coe_range]

Goal state after:
case refine_2
n : ℕ
k : Fin (n + 1)
⊢ ∀ (x : Fin n.succ), ↑x < ↑k → ∃ x_1 < ↑k, ↑x_1 = x
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: case hx
N : ℕ
hN : 4096 ≤ N
⊢ 0 < 2 / (1 - 2 / rexp 1)

Tactic:
field_simp
        simp (disch := positivity) [exp_one_gt_two]

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

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
⊢ (3 * log 2 * (69 / 50)) ^ 2 ≤ 12 * log 2

Tactic:
nlinarith [log_two_lt_d9, log_two_gt_d9]

Goal state after:
Module: Mathlib.Combinatorics.Additive.RuzsaCovering

Goal state before:
pp: case pos
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
hFA : F ⊆ A
hF : (↑F).PairwiseDisjoint fun x ↦ x • B
a : G
ha : a ∈ A
hau : a ∉ F
H : ∀ b ∈ F, Disjoint (a • B) (b • B)
⊢ insert a F ⊆ A ∧ (↑(insert a F)).PairwiseDisjoint fun x ↦ x • B

Tactic:
rw [insert_subset_iff, coe_insert]

Goal state after:
case pos
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
hFA : F ⊆ A
hF : (↑F).PairwiseDisjoint fun x ↦ x • B
a : G
ha : a ∈ A
hau : a ∉ F
H : ∀ b ∈ F, Disjoint (a • B) (b • B)
⊢ (a ∈ A ∧ F ⊆ A) ∧ (insert a ↑F).PairwiseDisjoint fun x ↦ x • B
Module: Mathlib.Combinatorics.Additive.RuzsaCovering

Goal state before:
pp: case neg
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
hFA : F ⊆ A
hF : (↑F).PairwiseDisjoint fun x ↦ x • B
a : G
ha : a ∈ A
hau : a ∉ F
H : ∃ b ∈ F, ∃ a_1 ∈ a • B, a_1 ∈ b • B
⊢ a ∈ F * (B / B)

Tactic:
← inv_smul_mem_iff

Goal state after:
case neg
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
hFA : F ⊆ A
hF : (↑F).PairwiseDisjoint fun x ↦ x • B
a : G
ha : a ∈ A
hau : a ∉ F
H : ∃ b ∈ F, ∃ a_1, a⁻¹ • a_1 ∈ B ∧ b⁻¹ • a_1 ∈ B
⊢ a ∈ F * (B / B)
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ 1 ∈ ↑A ^ 2

Tactic:
rw [sq, ← one_mul 1]

Goal state after:
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ 1 * 1 ∈ ↑A * ↑A
Module: Mathlib.Combinatorics.Additive.CauchyDavenport

Goal state before:
pp: α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : Mul α
inst✝² : IsCancelMul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this : s * {t.min' ht} ∩ ({s.max' hs} * t) = {s.max' hs * t.min' ht}
⊢ #s + #t - 1 ≤ #(s * t)

Tactic:
← card_singleton_mul (s.max' hs) t,

Goal state after:
α : Type u_2
inst✝⁴ : LinearOrder α
inst✝³ : Mul α
inst✝² : IsCancelMul α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this : s * {t.min' ht} ∩ ({s.max' hs} * t) = {s.max' hs * t.min' ht}
⊢ #s + #({s.max' hs} * t) - 1 ≤ #(s * t)
Module: Mathlib.Combinatorics.Additive.Convolution

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
x : G
⊢ 0 < A.convolution B x ↔ x ∈ A * B

Tactic:
aesop (add simp [convolution, Finset.Nonempty, mem_mul])

Goal state after:
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ ↑(#(A⁻¹ * A⁻¹ * A)) ≤ K ^ 2 * ↑(#A)

Tactic:
rw [← card_inv]

Goal state after:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ ↑(#(A⁻¹ * A⁻¹ * A)⁻¹) ≤ K ^ 2 * ↑(#A)
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ ↑(#(A * A * A⁻¹)) ≤ K ^ 2 * ↑(#A)

Tactic:
rw [← card_inv]

Goal state after:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ ↑(#(A * A * A⁻¹)⁻¹) ≤ K ^ 2 * ↑(#A)
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ ↑(#(A⁻¹ * A * A⁻¹)) ≤ K ^ 3 * ↑(#A)

Tactic:
rw [← card_inv]

Goal state after:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ ↑(#(A⁻¹ * A * A⁻¹)⁻¹) ≤ K ^ 3 * ↑(#A)