mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology

Goal state before:
pp: case a
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h✝ : EffectiveEpiFamily Y π
β : α → Type
inst✝ : ∀ (a : α), Finite (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
V : C
f : V ⟶ X
Y₁ : C
h : V ⟶ Y₁
g : Y₁ ⟶ X
hY : Presieve.ofArrows Y π g
hf : h ≫ g = f
⊢ (coherentCoverage C).Saturate V
    (Sieve.pullback f
      (Sieve.generate
        (Presieve.ofArrows
          (fun x ↦
            match x with
            | ⟨a, b⟩ => Y_n a b)
          fun x ↦
          match x with
          | ⟨a, b⟩ => π_n a b ≫ π a)))

Tactic:
← hf,

Goal state after:
case a
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h✝ : EffectiveEpiFamily Y π
β : α → Type
inst✝ : ∀ (a : α), Finite (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
V : C
f : V ⟶ X
Y₁ : C
h : V ⟶ Y₁
g : Y₁ ⟶ X
hY : Presieve.ofArrows Y π g
hf : h ≫ g = f
⊢ (coherentCoverage C).Saturate V
    (Sieve.pullback (h ≫ g)
      (Sieve.generate
        (Presieve.ofArrows
          (fun x ↦
            match x with
            | ⟨a, b⟩ => Y_n a b)
          fun x ↦
          match x with
          | ⟨a, b⟩ => π_n a b ≫ π a)))
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularTopology

Goal state before:
pp: case a
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preregular C
X Y Y' : C
π : Y ⟶ X
inst✝¹ : EffectiveEpi π
π' : Y' ⟶ Y
inst✝ : EffectiveEpi π'
V : C
f : V ⟶ X
Y₁ : C
h : V ⟶ Y₁
g : Y₁ ⟶ X
hY : Presieve.ofArrows (fun x ↦ Y) (fun x ↦ π) g
hf : h ≫ g = f
⊢ (regularCoverage C).Saturate V (Sieve.pullback f (Sieve.generate (Presieve.ofArrows (fun x ↦ Y') fun x ↦ π' ≫ π)))

Tactic:
← hf,

Goal state after:
case a
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preregular C
X Y Y' : C
π : Y ⟶ X
inst✝¹ : EffectiveEpi π
π' : Y' ⟶ Y
inst✝ : EffectiveEpi π'
V : C
f : V ⟶ X
Y₁ : C
h : V ⟶ Y₁
g : Y₁ ⟶ X
hY : Presieve.ofArrows (fun x ↦ Y) (fun x ↦ π) g
hf : h ≫ g = f
⊢ (regularCoverage C).Saturate V
    (Sieve.pullback (h ≫ g) (Sieve.generate (Presieve.ofArrows (fun x ↦ Y') fun x ↦ π' ≫ π)))
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
A : Type u₃
inst✝² : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
⊢ IsSheaf (coherentTopology C) F ↔ IsSheaf (extensiveTopology C) F ∧ IsSheaf (regularTopology C) F

Tactic:
← extensive_regular_generate_coherent

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
A : Type u₃
inst✝² : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
⊢ IsSheaf (extensiveCoverage C ⊔ regularCoverage C).toGrothendieck F ↔
    IsSheaf (extensiveTopology C) F ∧ IsSheaf (regularTopology C) F
Module: Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective

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
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:
by
  constructor
  · rw [Presheaf.isLocallySurjective_iff_whisker_forget (J := extensiveTopology C)]
    exact fun h _ ↦
      surjective_of_isLocallySurjective_sheaf_of_types (Functor.whiskerRight f (forget D)) h
  · exact fun a ↦
      Presheaf.isLocallySurjective_of_surjective _ _ (fun _ ↦ a _)

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

Goal state before:
pp: case mpr
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
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)
⊢ regularTopology C ≤ coherentTopology C

Tactic:
← extensive_regular_generate_coherent

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)
⊢ regularTopology C ≤ (extensiveCoverage C ⊔ regularCoverage C).toGrothendieck
Module: Mathlib.CategoryTheory.Sites.GlobalSections

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
inst✝¹ : HasWeakSheafify J A
inst✝ : HasGlobalSectionsFunctor J A
F : Sheaf J A
c : Cone F.obj
j : Cᵒᵖ
⊢ ΓHomEquiv c.π ≫ F.coneΓ.π.app j = c.π.app j

Tactic:
suffices h : ((Functor.const Cᵒᵖ).map (ΓHomEquiv c.π)) ≫ F.coneΓ.π = c.π from congr_app h j
    simp [coneΓ, ← ΓHomEquiv_naturality_left_symm]

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)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D : F.DescentData' sq sq₃
i₁ i₂ : ι
⊢ IsIso (D.hom i₁ i₂)

Tactic:
by
  simpa using (inferInstance : IsIso (pullHom' D.hom (sq i₁ i₂).p (sq i₁ i₂).p₁ (sq i₁ i₂).p₂))

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
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Y₁ Y₂ Z : Over (X i)
⊢ ∀ (g₁ : Z ⟶ Y₁) (g₂ : Z ⟶ Y₂) ⦃f₁ : Y₁ ⟶ Over.mk (𝟙 (X i))⦄ ⦃f₂ : Y₂ ⟶ Over.mk (𝟙 (X i))⦄
    (h₁ : (sieve f f' i).arrows f₁) (h₂ : (sieve f f' i).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g₁.op)) (familyOfElements w φ i f₁ h₁) =
        (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g₂.op)) (familyOfElements w φ i f₂ h₂)

Tactic:
g₁

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι
Y₁ Y₂ Z : Over (X i)
g₁ : Z ⟶ Y₁
⊢ ∀ (g₂ : Z ⟶ Y₂) ⦃f₁ : Y₁ ⟶ Over.mk (𝟙 (X i))⦄ ⦃f₂ : Y₂ ⟶ Over.mk (𝟙 (X i))⦄ (h₁ : (sieve f f' i).arrows f₁)
    (h₂ : (sieve f f' i).arrows f₂),
    g₁ ≫ f₁ = g₂ ≫ f₂ →
      (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g₁.op)) (familyOfElements w φ i f₁ h₁) =
        (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map g₂.op)) (familyOfElements w φ i f₂ h₂)
Module: Mathlib.CategoryTheory.Sites.Monoidal

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
M : A
F G : Cᵒᵖ ⥤ A
inst✝ : HasFunctorEnrichedHom A F G
X : C
g : (presheafHom (F ⊗ (Functor.const Cᵒᵖ).obj M) G).obj (op X)
j j' : Under (op X)
φ : j ⟶ j'
⊢ curry (g.app (op (Over.mk j.hom.unop)) ≫ G.map (Under.Hom.right φ)) =
    curry (F.map (Under.Hom.right φ) ▷ M ≫ g.app (op (Over.mk j'.hom.unop)))

Tactic:
congr 1

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
A : Type u₃
inst✝³ : Category.{v₃, u₃} A
inst✝² : MonoidalCategory A
inst✝¹ : MonoidalClosed A
M : A
F G : Cᵒᵖ ⥤ A
inst✝ : HasFunctorEnrichedHom A F G
X : C
g : (presheafHom (F ⊗ (Functor.const Cᵒᵖ).obj M) G).obj (op X)
j j' : Under (op X)
φ : j ⟶ j'
⊢ g.app (op (Over.mk j.hom.unop)) ≫ G.map (Under.Hom.right φ) =
    F.map (Under.Hom.right φ) ▷ M ≫ g.app (op (Over.mk j'.hom.unop))
Module: Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
M✝ : C ⥤ MonCat
S✝ : SubmonoidFunctor M✝
M M' M'' : C ⥤ MonCat
S : SubmonoidFunctor M
S' : SubmonoidFunctor M'
F G : SubmonoidFunctor M
U✝ V✝ : C
i : U✝ ⟶ V✝
⊢ F.obj U✝ ⊔ G.obj U✝ ≤ Submonoid.comap (MonCat.Hom.hom (M.map i)) (F.obj V✝ ⊔ G.obj V✝)

Tactic:
grw [F.map i, G.map i, (Submonoid.monotone_comap).le_map_sup]

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)
h₂ :
  f =
    inv ((sheafificationAdjunction J D).counit.app F) ≫
      (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G
this✝¹ : Epi ((presheafToSheaf J D).map f.hom)
this✝ : Epi ((presheafToSheaf J D).map i)
this : IsIso ((presheafToSheaf J D).map i)
⊢ (presheafToSheaf J D).map ((pullback.fst f f).hom ≫ p) = (presheafToSheaf J D).map ((pullback.snd f f).hom ≫ p)

Tactic:
congr 1

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
this✝¹ : Epi ((presheafToSheaf J D).map f.hom)
this✝ : Epi ((presheafToSheaf J D).map i)
this : IsIso ((presheafToSheaf J D).map i)
⊢ (pullback.fst f f).hom ≫ p = (pullback.snd f f).hom ≫ p
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
S : Over S₀
R : Sieve S
hF : F.IsPrestackFor ((Sieve.overEquiv S) R).arrows
M N : ↑(F.obj { as := op S₀ })
⊢ Presieve.IsSheafFor (F.presheafHom M N) R.arrows

Tactic:
by
  rw [isPrestackFor_iff_isSheafFor'] at hF
  obtain ⟨S, a, rfl⟩ := S.mk_surjective
  simpa using hF M N a

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
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
hf : Sieve.ofArrows X f ∈ J S
⊢ Nonempty (F.toDescentData f).FullyFaithful

Tactic:
← isPrestackFor_ofArrows_iff,

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
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
hf : Sieve.ofArrows X f ∈ J S
⊢ F.IsPrestackFor (Presieve.ofArrows X f)
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₁
⊢ (S.sequence F n₀ n₁ h).map' 0 1 homMk₁._proof_4 _proof_450✝ ≫
      ((F.H' n₀ S.X₂).biprodIsoProd (F.H' n₀ S.X₃) ≪≫ Ext.biprodAddEquiv.symm.toAddCommGrpIso).hom =
    (Iso.refl ((S.sequence F n₀ n₁ h).obj' 0 _proof_449✝)).hom ≫
      (Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).map' 0 1 homMk₁._proof_4 _proof_450✝

Tactic:
ext; apply biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply

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₁
⊢ (S.sequence F n₀ n₁ h).map' 3 4 _proof_364✝ _proof_453✝ ≫
      ((F.H' n₁ S.X₂).biprodIsoProd (F.H' n₁ S.X₃) ≪≫ Ext.biprodAddEquiv.symm.toAddCommGrpIso).hom =
    (Iso.refl ((S.sequence F n₀ n₁ h).obj' 3 _proof_452✝)).hom ≫
      (Ext.contravariantSequence ⋯ F n₀ n₁ ⋯).map' 3 4 _proof_364✝ _proof_453✝

Tactic:
ext; apply biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Generators

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : IsTriangulated C
n m m' : ℕ
h : m = m' + 1
⊢ P.triangEnvelopeIter (n + m) = ((P.triangEnvelopeIter n).extensionProduct (P.triangEnvelopeIter m')).retractClosure

Tactic:
simp only [triangEnvelopeIter, retractClosure_extensionProduct_retractClosure_retractClosure,
    extensionProductIter_add' _ h]

Goal state after:
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
B : A
x₁ : B ⟶ X₁
hx₁ : x₁ ≫ f₁ = 0
⊢ (shiftFunctor C 1).map (ι.map x₁) ≫ (shiftFunctor C 1).map (Triangle.mk (ι.map f₁) f₂ f₃).mor₁ = 0

Tactic:
by simp [← Functor.map_comp, hx₁]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory

Goal state before:
pp: case refine_2
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
inst✝¹ : HasFiniteProducts A
inst✝ : ι.Additive
X₁ X₂ X₃ : A
f₁ : X₁ ⟶ X₂
f₂ : X₂ ⟶ X₃
f₃ : ι.obj X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) (ι.map f₂) f₃ ∈ distinguishedTriangles
⊢ IsZero ((shiftFunctor C (-1)).obj 0)

Tactic:
rw [IsZero.iff_id_eq_zero, ← Functor.map_id, id_zero, Functor.map_zero]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s : Finset α
t : Finset β
⊢ mulRothNumber s * mulRothNumber t ≤ mulRothNumber (s ×ˢ t)

Tactic:
obtain ⟨u, hus, hucard, hu⟩ := mulRothNumber_spec s
  obtain ⟨v, hvt, hvcard, hv⟩ := mulRothNumber_spec t
  rw [← hucard, ← hvcard, ← card_product]
  refine ThreeGPFree.le_mulRothNumber ?_ (product_subset_product hus hvt)
  rw [coe_product]
  exact hu.prod hv

Goal state after:
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 ^ (↑(nValue N))⁻¹ / rexp 1) ^ (n - 2) / ↑n < ↑(dValue N) ^ (n - 2) / ↑n

Tactic:
by gcongr; exacts [(tsub_pos_of_lt hn₂).ne', bound hN]

Goal state after:
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
⊢ rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))

Tactic:
rw [← exp_add, ← add_mul]

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
⊢ rexp (-4 * √(log ↑N)) = rexp ((-2 + -2) * √(log ↑N))
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
⊢ ∀ a ∈ s, ∀ x ∈ t, s.max' hs * x = a * t.min' ht → a = s.max' hs

Tactic:
exact fun a' ha' b' hb' h ↦ (le_max' _ _ ha').eq_of_not_lt fun ha ↦
    (lt_of_eq_of_lt h (mul_lt_mul_left ha _)).not_ge <| mul_le_mul_right (min'_le _ _ hb') _

Goal state after:
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
⊢ A.convolution B⁻¹⁻¹ x ≤ #B⁻¹⁻¹

Tactic:
← inv_inv x,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
x : G
⊢ A.convolution B⁻¹⁻¹ x⁻¹⁻¹ ≤ #B⁻¹⁻¹
Module: Mathlib.Combinatorics.Additive.Convolution

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
s x : G
⊢ (s •> A).convolution B x = A.convolution B (s⁻¹ * x)

Tactic:
← inv_inv x,

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
s x : G
⊢ (s •> A).convolution B x⁻¹⁻¹ = A.convolution B (s⁻¹ * x)
Module: Mathlib.Combinatorics.Additive.Corner.Defs

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : AddCommMonoid G
inst✝ : AddCommMonoid H
A : Set (G × G)
s : Set G
t : Set H
f : G → H
x₁ y₁ x₂ y₂ : G
hf : IsAddFreimanHom 2 s t f
hAs : A ⊆ s ×ˢ s
hA : IsCorner A x₁ y₁ x₂ y₂
⊢ IsCorner (Prod.map f f '' A) (f x₁) (f y₁) (f x₂) (f y₂)

Tactic:
obtain ⟨hx₁y₁, hx₁y₂, hx₂y₁, hxy⟩ := hA
  exact ⟨mem_image_of_mem _ hx₁y₁, mem_image_of_mem _ hx₁y₂, mem_image_of_mem _ hx₂y₁,
    hf.add_eq_add (hAs hx₁y₁).1 (hAs hx₁y₂).2 (hAs hx₂y₁).1 (hAs hx₁y₁).2 hxy⟩

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v : V
⊢ {d | d.toProd.1 = v} = image (G.dartOfNeighborSet v) univ

Tactic:
ext d
  simp only [mem_image, true_and, mem_filter, SetCoe.exists, mem_univ]
  constructor
  · rintro rfl
    exact ⟨_, d.adj, by ext <;> rfl⟩
  · rintro ⟨e, he, rfl⟩
    rfl

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ∑ b ∈ G.edgeFinset, #{a | a.edge = b} = #G.edgeFinset * 2

Tactic:
sum_const_nat

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ #G.edgeFinset * ?m.53 = #G.edgeFinset * 2

V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ∀ x ∈ G.edgeFinset, #{a | a.edge = x} = ?m.53

V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ℕ
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
⊢ Odd #{w | w ≠ v ∧ Odd (G.degree w)}

Tactic:
rcases G.even_card_odd_degree_vertices with ⟨k, hg⟩
  have hk : 0 < k := by
    have hh : Finset.Nonempty {v : V | Odd (G.degree v)} := by
      use v
      rw [mem_filter_univ]
      exact h
    rwa [← card_pos, hg, ← two_mul, mul_pos_iff_of_pos_left] at hh
    exact zero_lt_two
  have hc : (fun w : V => w ≠ v ∧ Odd (G.degree w)) = fun w : V => Odd (G.degree w) ∧ w ≠ v := by
    ext w
    rw [and_comm]
  simp only [hc]
  rw [← filter_filter, filter_ne', card_erase_of_mem]
  · refine ⟨k - 1, tsub_eq_of_eq_add <| hg.trans ?_⟩
    lia
  · rwa [mem_filter_univ]

Goal state after:
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: case neg
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ ↑s, b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
⊢ ∑ i ∈ s, (b + 1) ≤ #s * (b + 1)

Tactic:
sum_const_nat

Goal state after:
case neg
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ ↑s, b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
⊢ #s * ?m.204 ≤ #s * (b + 1)

case neg
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ ↑s, b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
⊢ ∀ x ∈ s, b + 1 = ?m.204

α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ ↑s, b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
⊢ ℕ
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
inst✝³ : Fintype V
W : Type u_2
inst✝² : Fintype W
inst✝¹ : DecidableEq W
f : V ↪ W
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
⊢ #(SimpleGraph.map (⇑f) G).edgeFinset = #G.edgeFinset

Tactic:
by
  rw [edgeFinset_map]
  exact G.edgeFinset.card_map f.sym2Map

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a b : α
P : Finpartition a
hab : a ≤ b
hr : ¬b \ a = ⊥
⊢ P.parts ⊆ (P.extend hr ⋯ ⋯).parts

Tactic:
exact Finset.subset_insert _ _

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case coe
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
b : EInt
X : C
a : ℤ
h : WithBotTop.coe a ≤ b
⊢ IsIso ((t.eTruncLT.obj (WithBotTop.coe a)).map ((t.eTruncLTι b).app X))

Tactic:
induction b using WithBotTop.rec with
    | bot => simp at h
    | coe b =>
      exact t.isIso_truncLT_map_truncLTι_app a b (by simpa using h) X
    | top => dsimp; infer_instance

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Density

Goal state before:
pp: case hb
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
⊢ 0 ≤ ↑(#s) * ↑(#t)

Tactic:
· exact mod_cast Nat.zero_le _

Goal state after: