mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Descent.IsPrestack

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
S : C
M N : ↑(F.obj { as := op S })
S' : C
q : S' ⟶ S
⊢ ∀ {X Y : (Over S')ᵒᵖ} (f : X ⟶ Y),
    ((Over.map q).op ⋙ F.presheafHom M N).map f ≫
        (((Cat.Hom.toNatIso
                        (F.mapComp' q.op.toLoc (unop Y).hom.op.toLoc ((Over.map q).obj (unop Y)).hom.op.toLoc ⋯)).app
                    M).homFromEquiv.trans
              ((Cat.Hom.toNatIso
                      (F.mapComp' q.op.toLoc (unop Y).hom.op.toLoc ((Over.map q).obj (unop Y)).hom.op.toLoc ⋯)).app
                  N).homToEquiv).toIso.hom =
      (((Cat.Hom.toNatIso (F.mapComp' q.op.toLoc (unop X).hom.op.toLoc ((Over.map q).obj (unop X)).hom.op.toLoc ⋯)).app
                    M).homFromEquiv.trans
              ((Cat.Hom.toNatIso
                      (F.mapComp' q.op.toLoc (unop X).hom.op.toLoc ((Over.map q).obj (unop X)).hom.op.toLoc ⋯)).app
                  N).homToEquiv).toIso.hom ≫
        (F.presheafHom ((F.map q.op.toLoc).toFunctor.obj M) ((F.map q.op.toLoc).toFunctor.obj N)).map f

Tactic:
rintro ⟨T₁⟩ ⟨T₂⟩ ⟨f⟩
      ext g
      dsimp [pullHom]
      simp only [Category.assoc,
        Functor.map_comp]
      rw [F.mapComp'₀₁₃_inv_comp_mapComp'₀₂₃_hom_app_assoc _ _ _ _ _ _ rfl _ rfl,
        F.mapComp'₀₂₃_inv_comp_mapComp'₀₁₃_hom_app _ _ _ _ _ _ _ _ (by
          simp only [← Quiver.Hom.comp_toLoc, ← op_comp, Over.w_assoc])]

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
hF : ∀ (S : C), ∀ R ∈ J S, F.IsStackFor R.arrows
S✝ : C
R : Sieve S✝
hR : R ∈ J S✝
⊢ (F.toDescentData fun f ↦ f.obj.hom).EssSurj

Tactic:
have := (isStackFor_iff _ _).1 (hF _ _ hR)

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
hF : ∀ (S : C), ∀ R ∈ J S, F.IsStackFor R.arrows
S✝ : C
R : Sieve S✝
hR : R ∈ J S✝
this : (F.toDescentData fun f ↦ f.obj.hom).IsEquivalence
⊢ (F.toDescentData fun f ↦ f.obj.hom).EssSurj
Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: case _i
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
this :
  ∀ (ψ : 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 ⋯ ⋯
⊢ (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g.op)) (F.presheafHomObjHomEquiv (φ.hom i)) =
    (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g.op)) (F.presheafHomObjHomEquiv (φ'.hom i))

Tactic:
replace hφ := congr_fun (congr_arg DescentData.Hom.hom hφ) j

Goal state after:
case _i
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₂
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
this :
  ∀ (ψ : 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 ⋯ ⋯
hφ : ((pullFunctor F ⋯).map φ).hom j = ((pullFunctor F ⋯).map φ').hom j
⊢ (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g.op)) (F.presheafHomObjHomEquiv (φ.hom i)) =
    (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g.op)) (F.presheafHomObjHomEquiv (φ'.hom 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
inst✝ : HasPullbacks C
f g : E.Hom F
i j : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)
Y✝ Y : C
k : E.I₁ i.fst j.fst
⊢ ((cylinder f g).sieve₁' i j).arrows
    (pullback.fst
      (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.toPullback k))

Tactic:
rw [sieve₁']

Goal state after:
case refine_2
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)
Y✝ Y : C
k : E.I₁ i.fst j.fst
⊢ (Sieve.ofArrows (cylinder f g).Y fun j_1 ↦ (cylinder f g).toPullback j_1).arrows
    (pullback.fst
      (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.toPullback k))
Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H : ∀ (i : 𝒰.I₀), IsPullback (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
⊢ ∀ (i : (𝒰.pullbackCoverOfLeft f g).I₀),
    IsIso (pullback.snd (pullback.lift fst snd h) ((𝒰.pullbackCoverOfLeft f g).f i))

Tactic:
intro i

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H : ∀ (i : 𝒰.I₀), IsPullback (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : (𝒰.pullbackCoverOfLeft f g).I₀
⊢ IsIso (pullback.snd (pullback.lift fst snd h) ((𝒰.pullbackCoverOfLeft f g).f i))
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)
⊢ IsRegularEpi f

Tactic:
have h₂ : f = inv ((sheafificationAdjunction J D).counit.app F) ≫
        (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G := by
      simp [h₁]

Goal state after:
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)
h₂ :
  f =
    inv ((sheafificationAdjunction J D).counit.app F) ≫
      (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G
⊢ IsRegularEpi f
Module: Mathlib.CategoryTheory.Sites.Types

Goal state before:
pp: α : Type u
⊢ IsSheaf typesGrothendieckTopology (yoneda.obj α)

Tactic:
rw [isSheaf_iff_isSheaf_of_type]
  exact Presieve.isSheaf_yoneda'

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Presheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Limits.HasPullbacks C
x✝ : Cᵒᵖ
⊢ ↾(pullback (𝟙 x✝).unop).obj = 𝟙 (Subobject (Opposite.unop x✝))

Tactic:
ext : 3

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Limits.HasPullbacks C
x✝¹ : Cᵒᵖ
x✝ : Subobject (Opposite.unop x✝¹)
⊢ (ConcreteCategory.hom (↾(pullback (𝟙 x✝¹).unop).obj)).toFun x✝ =
    (ConcreteCategory.hom (𝟙 (Subobject (Opposite.unop x✝¹)))).toFun x✝
Module: Mathlib.CategoryTheory.Subobject.Presheaf

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Limits.HasPullbacks C
X✝ Y✝ Z✝ : Cᵒᵖ
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ ↾(pullback (x✝¹ ≫ x✝).unop).obj = ↾(pullback x✝¹.unop).obj ≫ ↾(pullback x✝.unop).obj

Tactic:
ext : 3

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Limits.HasPullbacks C
X✝ Y✝ Z✝ : Cᵒᵖ
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : Subobject (Opposite.unop X✝)
⊢ (ConcreteCategory.hom (↾(pullback (x✝² ≫ x✝¹).unop).obj)).toFun x✝ =
    (ConcreteCategory.hom (↾(pullback x✝².unop).obj ≫ ↾(pullback x✝¹.unop).obj)).toFun x✝
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
𝒞 : Classifier C
Ω₀ Ω : C
eΩ : 𝒞.Ω ≅ Ω
eΩ₀ : 𝒞.Ω₀ ≅ Ω₀
from' : (C_1 : C) → C_1 ⟶ Ω₀
t : Ω₀ ⟶ Ω
ht : t = eΩ₀.inv ≫ 𝒞.truth ≫ eΩ.hom
F G : C
m : F ⟶ G
x✝ : Mono m
⊢ ∀ {χ₀' : F ⟶ Ω₀} {χ' : G ⟶ Ω}, IsPullback m χ₀' χ' t → χ' = 𝒞.χ m ≫ eΩ.hom

Tactic:
intro χ₀'

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
𝒞 : Classifier C
Ω₀ Ω : C
eΩ : 𝒞.Ω ≅ Ω
eΩ₀ : 𝒞.Ω₀ ≅ Ω₀
from' : (C_1 : C) → C_1 ⟶ Ω₀
t : Ω₀ ⟶ Ω
ht : t = eΩ₀.inv ≫ 𝒞.truth ≫ eΩ.hom
F G : C
m : F ⟶ G
x✝ : Mono m
χ₀' : F ⟶ Ω₀
⊢ ∀ {χ' : G ⟶ Ω}, IsPullback m χ₀' χ' t → χ' = 𝒞.χ m ≫ eΩ.hom
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
𝒞₁ : Classifier C
e : C ≌ D
F G : D
m : F ⟶ G
x✝ : Mono m
⊢ ∀ {χ₀' : F ⟶ e.functor.obj 𝒞₁.Ω₀} {χ' : G ⟶ e.functor.obj 𝒞₁.Ω},
    IsPullback m χ₀' χ' (e.functor.map 𝒞₁.truth) → χ' = e.counitInv.app G ≫ e.functor.map (𝒞₁.χ (e.inverse.map m))

Tactic:
intro χ₀'

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
𝒞₁ : Classifier C
e : C ≌ D
F G : D
m : F ⟶ G
x✝ : Mono m
χ₀' : F ⟶ e.functor.obj 𝒞₁.Ω₀
⊢ ∀ {χ' : G ⟶ e.functor.obj 𝒞₁.Ω},
    IsPullback m χ₀' χ' (e.functor.map 𝒞₁.truth) → χ' = e.counitInv.app G ≫ e.functor.map (𝒞₁.χ (e.inverse.map m))
Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory

Goal state before:
pp: C : Type u_1
A : Type u_2
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
W'✝ : A
x₁ : W'✝ ⟶ X₁
hx₁ : x₁ ≫ f₁ = 0
m : W'✝ ⟶ K
hm : m ≫ ιK f₃ α = x₁
⊢ m = ⋯.choose

Tactic:
have := mono_ιK hι hT hT'

Goal state after:
C : Type u_1
A : Type u_2
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
W'✝ : A
x₁ : W'✝ ⟶ X₁
hx₁ : x₁ ≫ f₁ = 0
m : W'✝ ⟶ K
hm : m ≫ ιK f₃ α = x₁
this : Mono (ιK f₃ α)
⊢ m = ⋯.choose
Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory

Goal state before:
pp: C : Type u_1
A : Type u_2
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
inst✝² : Preadditive A
inst✝¹ : ι.Full
inst✝ : ι.Faithful
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
hf₁ : admissibleMorphism ι f₁
⊢ HasCokernel f₁

Tactic:
obtain ⟨X₃, f₂, f₃, hT⟩ := distinguished_cocone_triangle (ι.map f₁)
  obtain ⟨K, Q, α, β, γ, hT'⟩ := hf₁ f₂ f₃ hT
  exact hasCokernel hι hT hT'

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.DoubleCounting

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsOrderedRing R
m n : R
inst✝ : (a : α) → (b : β) → Decidable (r a b)
hm : ∀ a ∈ s, m ≤ ↑(#(bipartiteAbove r t a))
hn : ∀ b ∈ t, ↑(#(bipartiteBelow r s b)) ≤ n
⊢ ∑ a ∈ s, ↑(#(bipartiteAbove r t a)) = ∑ b ∈ t, ↑(#(bipartiteBelow r s b))

Tactic:
norm_cast

Goal state after:
R : Type u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsOrderedRing R
m n : R
inst✝ : (a : α) → (b : β) → Decidable (r a b)
hm : ∀ a ∈ s, m ≤ ↑(#(bipartiteAbove r t a))
hn : ∀ b ∈ t, ↑(#(bipartiteBelow r s b)) ≤ n
⊢ ↑(∑ x ∈ s, #(bipartiteAbove r t x)) = ↑(∑ x ∈ t, #(bipartiteBelow r s x))
Module: Mathlib.Combinatorics.Enumerative.DoubleCounting

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsOrderedRing R
m n : R
inst✝ : (a : α) → (b : β) → Decidable (r a b)
hm : ∀ a ∈ s, m ≤ ↑(#(bipartiteAbove r t a))
hn : ∀ b ∈ t, ↑(#(bipartiteBelow r s b)) ≤ n
⊢ ∑ a ∈ s, ↑(#(bipartiteAbove r t a)) = ∑ b ∈ t, ↑(#(bipartiteBelow r s b))

Tactic:
norm_cast; rw [sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.DoubleCounting

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
r : α → β → Prop
s : Finset α
t : Finset β
m n : R
inst✝ : (a : α) → (b : β) → Decidable (r a b)
hs : s.Nonempty
hm : ∀ a ∈ s, m < ↑(#(bipartiteAbove r t a))
hn : ∀ b ∈ t, ↑(#(bipartiteBelow r s b)) ≤ n
⊢ ∑ a ∈ s, ↑(#(bipartiteAbove r t a)) = ∑ b ∈ t, ↑(#(bipartiteBelow r s b))

Tactic:
norm_cast

Goal state after:
R : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
r : α → β → Prop
s : Finset α
t : Finset β
m n : R
inst✝ : (a : α) → (b : β) → Decidable (r a b)
hs : s.Nonempty
hm : ∀ a ∈ s, m < ↑(#(bipartiteAbove r t a))
hn : ∀ b ∈ t, ↑(#(bipartiteBelow r s b)) ≤ n
⊢ ∑ x ∈ s, #(bipartiteAbove r t x) = ∑ x ∈ t, #(bipartiteBelow r s x)
Module: Mathlib.Combinatorics.Enumerative.DoubleCounting

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
r : α → β → Prop
s : Finset α
t : Finset β
m n : R
inst✝ : (a : α) → (b : β) → Decidable (r a b)
hs : s.Nonempty
hm : ∀ a ∈ s, m < ↑(#(bipartiteAbove r t a))
hn : ∀ b ∈ t, ↑(#(bipartiteBelow r s b)) ≤ n
⊢ ∑ a ∈ s, ↑(#(bipartiteAbove r t a)) = ∑ b ∈ t, ↑(#(bipartiteBelow r s b))

Tactic:
norm_cast; rw [sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.DoubleCounting

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
r : α → β → Prop
s : Finset α
t : Finset β
m n : R
inst✝ : (a : α) → (b : β) → Decidable (r a b)
ht : t.Nonempty
hm : ∀ a ∈ s, m ≤ ↑(#(bipartiteAbove r t a))
hn : ∀ b ∈ t, ↑(#(bipartiteBelow r s b)) < n
⊢ ∑ a ∈ s, ↑(#(bipartiteAbove r t a)) = ∑ b ∈ t, ↑(#(bipartiteBelow r s b))

Tactic:
norm_cast

Goal state after:
R : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
r : α → β → Prop
s : Finset α
t : Finset β
m n : R
inst✝ : (a : α) → (b : β) → Decidable (r a b)
ht : t.Nonempty
hm : ∀ a ∈ s, m ≤ ↑(#(bipartiteAbove r t a))
hn : ∀ b ∈ t, ↑(#(bipartiteBelow r s b)) < n
⊢ ∑ x ∈ s, #(bipartiteAbove r t x) = ∑ x ∈ t, #(bipartiteBelow r s x)
Module: Mathlib.Combinatorics.Enumerative.DoubleCounting

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
r : α → β → Prop
s : Finset α
t : Finset β
m n : R
inst✝ : (a : α) → (b : β) → Decidable (r a b)
ht : t.Nonempty
hm : ∀ a ∈ s, m ≤ ↑(#(bipartiteAbove r t a))
hn : ∀ b ∈ t, ↑(#(bipartiteBelow r s b)) < n
⊢ ∑ a ∈ s, ↑(#(bipartiteAbove r t a)) = ∑ b ∈ t, ↑(#(bipartiteBelow r s b))

Tactic:
norm_cast; rw [sum_card_bipartiteAbove_eq_sum_card_bipartiteBelow]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
⊢ ThreeGPFree ↑∅

Tactic:
norm_cast

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
⊢ ThreeGPFree ∅
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: case zero
n d : ℕ
x₁ : Fin 0 → ℕ
hx₁ : x₁ ∈ {x | ∀ (i : Fin 0), x i < d}
x₂ : Fin 0 → ℕ
hx₂ : x₂ ∈ {x | ∀ (i : Fin 0), x i < d}
h : (map d) x₁ = (map d) x₂
⊢ x₁ = x₂

Tactic:
simp [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
K : ℝ
A B : Finset G
hB₀ : (↑B).Nonempty
hK : ↑(Nat.card ↑(↑A * ↑B)) ≤ K * ↑(Nat.card ↑↑B)
F : Finset G
hFA : F ⊆ A
hF : ↑F.card ≤ K
hAF : A ⊆ F * (B / B)
⊢ ↑F ⊆ ↑A ∧ ↑(Nat.card ↑↑F) ≤ K ∧ ↑A ⊆ ↑F * (↑B / ↑B) ∧ (↑F).Finite

Tactic:
norm_cast

Goal state after:
G : Type u_1
inst✝ : Group G
K : ℝ
A B : Finset G
hB₀ : (↑B).Nonempty
hK : ↑(Nat.card ↑(↑A * ↑B)) ≤ K * ↑(Nat.card ↑↑B)
F : Finset G
hFA : F ⊆ A
hF : ↑F.card ≤ K
hAF : A ⊆ F * (B / B)
⊢ F ⊆ A ∧ ↑(Nat.card ↥F) ≤ K ∧ A ⊆ F * (B / B) ∧ (↑F).Finite
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ ↑N * rexp (-4 * √(log ↑N)) ≤ (↑N ^ (↑(nValue N))⁻¹ / rexp 1) ^ ↑(n - 2) / ↑n

Tactic:
div_rpow (rpow_nonneg hN₀.le _) (exp_pos _).le,

Goal state after:
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this : (2 * dValue N - 1) ^ n ≤ N
⊢ ↑N * rexp (-4 * √(log ↑N)) ≤ (↑N ^ (↑(nValue N))⁻¹) ^ ↑(n - 2) / rexp 1 ^ ↑(n - 2) / ↑n
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: ⊢ 4096 = 2 ^ 12

Tactic:
norm_cast

Goal state after:
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 ^ 4 * A)) ≤ K ^ 3 * ↑(#A)
hA₀ : A.Nonempty
F : Finset G
hF : ↑(#F) ≤ K ^ 3
hAF : A ^ 4 ⊆ F * (A / A)
⊢ (↑A ^ 2) ^ 2 ⊆ ↑F • ↑A ^ 2

Tactic:
norm_cast

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 ^ 4 * A)) ≤ K ^ 3 * ↑(#A)
hA₀ : A.Nonempty
F : Finset G
hF : ↑(#F) ≤ K ^ 3
hAF : A ^ 4 ⊆ F * (A / A)
⊢ (A ^ 2) ^ 2 ⊆ F • A ^ 2
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: case h₁.hst
G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
F₁ : Finset G
hF₁ : ↑(#F₁) ≤ K
hAF₁ : A ^ 2 ⊆ ↑F₁ • A
F₂ : Finset G
hF₂ : ↑(#F₂) ≤ L
hBF₂ : B ^ 2 ⊆ ↑F₂ • B
this : 1 ≤ K
f : G → G → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
⊢ A ^ 2 ⊆ ↑F₁ * A

Tactic:
norm_cast

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

Goal state before:
pp: case hn
G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
F₁ : Finset G
hF₁ : ↑(#F₁) ≤ K
hAF₁ : A ^ 2 ⊆ ↑F₁ • A
F₂ : Finset G
hF₂ : ↑(#F₂) ≤ L
hBF₂ : B ^ 2 ⊆ ↑F₂ • B
this : 1 ≤ K
f : G → G → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
⊢ m ≠ 0

Tactic:
norm_cast

Goal state after:
case hn
G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
F₁ : Finset G
hF₁ : ↑(#F₁) ≤ K
hAF₁ : A ^ 2 ⊆ ↑F₁ • A
F₂ : Finset G
hF₂ : ↑(#F₂) ≤ L
hBF₂ : B ^ 2 ⊆ ↑F₂ • B
this : 1 ≤ K
f : G → G → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
⊢ ¬m = 0
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: case h₂.hst
G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
F₁ : Finset G
hF₁ : ↑(#F₁) ≤ K
hAF₁ : A ^ 2 ⊆ ↑F₁ • A
F₂ : Finset G
hF₂ : ↑(#F₂) ≤ L
hBF₂ : B ^ 2 ⊆ ↑F₂ • B
this : 1 ≤ K
f : G → G → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
⊢ B ^ 2 ⊆ ↑F₂ * B

Tactic:
norm_cast

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

Goal state before:
pp: case hn
G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
F₁ : Finset G
hF₁ : ↑(#F₁) ≤ K
hAF₁ : A ^ 2 ⊆ ↑F₁ • A
F₂ : Finset G
hF₂ : ↑(#F₂) ≤ L
hBF₂ : B ^ 2 ⊆ ↑F₂ • B
this : 1 ≤ K
f : G → G → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
⊢ n ≠ 0

Tactic:
norm_cast

Goal state after:
case hn
G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
F₁ : Finset G
hF₁ : ↑(#F₁) ≤ K
hAF₁ : A ^ 2 ⊆ ↑F₁ • A
F₂ : Finset G
hF₂ : ↑(#F₂) ≤ L
hBF₂ : B ^ 2 ⊆ ↑F₂ • B
this : 1 ≤ K
f : G → G → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
⊢ ¬n = 0
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
F₁ : Finset G
hF₁ : ↑(#F₁) ≤ K
hAF₁ : A ^ 2 ⊆ ↑F₁ • A
F₂ : Finset G
hF₂ : ↑(#F₂) ≤ L
hBF₂ : B ^ 2 ⊆ ↑F₂ • B
this : 1 ≤ K
f : G → G → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
⊢ ⋃ i₁ ∈ ↑F₁ ^ (m - 1), ⋃ j₁ ∈ ↑F₂ ^ (n - 1), i₁ • A ∩ j₁ • B = ⋃ a ∈ F₁ ^ (m - 1), ⋃ b ∈ F₂ ^ (n - 1), a • A ∩ b • B

Tactic:
norm_cast

Goal state after: