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

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

Tactic:
refine ⟨fun hF ↦ ⟨fun n ↦ ⟨fun {K} ↦ ?_⟩⟩, fun hF ↦ ?_⟩
  · rw [extensiveTopology, isSheaf_coverage] at hF
    let Z : Fin n → C := fun i ↦ unop (K.obj ⟨i⟩)
    have : (ofArrows Z (Cofan.mk (∐ Z) (Sigma.ι Z)).inj).HasPairwisePullbacks :=
      inferInstanceAs (ofArrows Z (Sigma.ι Z)).HasPairwisePullbacks
    have : ∀ (i : Fin n), Mono (Cofan.inj (Cofan.mk (∐ Z) (Sigma.ι Z)) i) :=
      inferInstanceAs <| ∀ (i : Fin n), Mono (Sigma.ι Z i)
    let i : K ≅ Discrete.functor (fun i ↦ op (Z i)) := Discrete.natIsoFunctor
    let _ : PreservesLimit (Discrete.functor (fun i ↦ op (Z i))) F :=
        Presieve.preservesProduct_of_isSheafFor F ?_ initialIsInitial _ (coproductIsCoproduct Z)
        (FinitaryExtensive.isPullback_initial_to_sigma_ι Z)
        (hF (Presieve.ofArrows Z (fun i ↦ Sigma.ι Z i)) ?_)
    · exact preservesLimit_of_iso_diagram F i.symm
    · apply hF
      refine ⟨Empty, inferInstance, Empty.elim, IsEmpty.elim inferInstance, rfl, ⟨default,?_, ?_⟩⟩
      · ext b
        cases b
      · simp only [eq_iff_true_of_subsingleton]
    · exact ⟨Fin n, inferInstance, Z, (fun i ↦ Sigma.ι Z i), rfl, instIsIsoDescι⟩
  · rw [extensiveTopology, Presieve.isSheaf_coverage]
    intro X R ⟨Y, α, Z, π, hR, hi⟩
    have : IsIso (Sigma.desc (Cofan.inj (Cofan.mk X π))) := hi
    have : R.Extensive := ⟨Y, α, Z, π, hR, ⟨Cofan.isColimitOfIsIsoSigmaDesc (Cofan.mk X π)⟩⟩
    exact isSheafFor_extensive_of_preservesFiniteProducts R F

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

Goal state before:
pp: A : Type u_1
C : Type u_2
J : Type u_3
inst✝⁵ : Category.{v_1, u_1} A
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} J
inst✝² : FinitaryExtensive C
inst✝¹ : HasColimitsOfShape J A
inst✝ : PreservesFiniteProducts colim
G : J ⥤ Sheaf (extensiveTopology C) A
⊢ Presheaf.IsSheaf (extensiveTopology C) (pointwiseCocone (G ⋙ sheafToPresheaf (extensiveTopology C) A)).pt

Tactic:
by
  rw [Presheaf.isSheaf_iff_preservesFiniteProducts]
  dsimp only [pointwiseCocone_pt]
  apply +allowSynthFailures comp_preservesFiniteProducts
  have : ∀ (i : J), PreservesFiniteProducts ((G ⋙ sheafToPresheaf _ A).obj i) := fun i ↦ by
    rw [← Presheaf.isSheaf_iff_preservesFiniteProducts]
    exact (G.obj i).property
  exact ⟨fun _ ↦ preservesLimitsOfShape_of_evaluation _ _ fun d ↦
    inferInstanceAs (PreservesLimitsOfShape _ ((G ⋙ sheafToPresheaf _ _).obj d))⟩

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

Goal state before:
pp: case mpr
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁷ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasFunctorialSurjectiveInjectiveFactorization A
inst✝³ : J.WEqualsLocallyBijective A
inst✝² : HasSheafify J A
inst✝¹ : J.HasSheafCompose (forget A)
inst✝ : Balanced (Sheaf J A)
F G : Sheaf J A
φ : F ⟶ G
a✝ : Epi φ
data : (locallySurjective J A).MapFactorizationData (locallyInjective J A) φ :=
  (locallySurjective J A).factorizationData (locallyInjective J A) φ
this : IsLocallySurjective data.i
⊢ IsLocallySurjective φ

Tactic:
have : IsLocallyInjective data.p := data.hp

Goal state after:
case mpr
C : Type u
inst✝⁸ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝⁷ : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w
inst✝⁶ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝⁵ : ConcreteCategory A FA
inst✝⁴ : HasFunctorialSurjectiveInjectiveFactorization A
inst✝³ : J.WEqualsLocallyBijective A
inst✝² : HasSheafify J A
inst✝¹ : J.HasSheafCompose (forget A)
inst✝ : Balanced (Sheaf J A)
F G : Sheaf J A
φ : F ⟶ G
a✝ : Epi φ
data : (locallySurjective J A).MapFactorizationData (locallyInjective J A) φ :=
  (locallySurjective J A).factorizationData (locallyInjective J A) φ
this✝ : IsLocallySurjective data.i
this : IsLocallyInjective data.p
⊢ IsLocallySurjective φ
Module: Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
W X w✝ Y : C
f : Y ⟶ X
hf : EffectiveEpi f
hS : ∃ f_1, ((ofArrows (fun x ↦ Y) fun x ↦ f) = ofArrows (fun x ↦ w✝) fun x ↦ f_1) ∧ EffectiveEpi f_1
this : (ofArrows (fun x ↦ Y) fun x ↦ f).regular
h_colim : IsColimit (Sieve.generateSingleton f).arrows.cocone
⊢ IsSheafFor (yoneda.obj W) (ofArrows (fun x ↦ Y) fun x ↦ f)

Tactic:
← Sieve.generateSingleton_eq,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preregular C
W X w✝ Y : C
f : Y ⟶ X
hf : EffectiveEpi f
hS : ∃ f_1, ((ofArrows (fun x ↦ Y) fun x ↦ f) = ofArrows (fun x ↦ w✝) fun x ↦ f_1) ∧ EffectiveEpi f_1
this : (ofArrows (fun x ↦ Y) fun x ↦ f).regular
h_colim : IsColimit (Sieve.generate (Presieve.singleton f)).arrows.cocone
⊢ IsSheafFor (yoneda.obj W) (ofArrows (fun x ↦ Y) fun x ↦ f)
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
X Y : C
𝒰 : J.ZeroHypercover X
f g : X ⟶ Y
h : ∀ (i : 𝒰.I₀), 𝒰.f i ≫ f = 𝒰.f i ≫ g
hs : Presieve.IsSheafFor (yoneda.obj Y) 𝒰.presieve₀
⊢ f = g

Tactic:
exact 𝒰.ext_of_isSeparatedFor hs.isSeparatedFor fun i ↦ by simp [h i]

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
⊢ (F.map f₁.op.toLoc).toFunctor.map (hom w hf' φ i₁) ≫ D₂.hom q f₁ f₂ ⋯ ⋯ ≫ D₂.hom q f₂ f₁ ⋯ ⋯ =
    D₁.hom q f₁ f₂ ⋯ ⋯ ≫ (F.map f₂.op.toLoc).toFunctor.map (hom w hf' φ i₂) ≫ D₂.hom q f₂ f₁ ⋯ ⋯

Tactic:
DescentData.hom_comp,

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
⊢ (F.map f₁.op.toLoc).toFunctor.map (hom w hf' φ i₁) ≫ D₂.hom q f₁ f₁ ⋯ ⋯ =
    D₁.hom q f₁ f₂ ⋯ ⋯ ≫ (F.map f₂.op.toLoc).toFunctor.map (hom w hf' φ i₂) ≫ D₂.hom q f₂ f₁ ⋯ ⋯
Module: Mathlib.CategoryTheory.Sites.Point.Over

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
inst✝⁴ : LocallySmall.{w, v, u} C
P : ObjectProperty J.Point
inst✝³ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
inst✝² : J.WEqualsLocallyBijective (Type w)
inst✝¹ : HasSheafify J (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
inst✝ : HasSheafify (J.over X) (Type w)
Y : C
f : Y ⟶ X
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ (Over.mk f).left
hS :
  ∀ (Φ : (ofObj fun ψ ↦ ψ.fst.obj.over ψ.snd).FullSubcategory) (x : Φ.obj.fiber.obj (Over.mk f)),
    ∃ Y_1 g_1,
      ∃ (_ : ((Sieve.overEquiv (Over.mk f)).symm (Sieve.ofArrows Z g)).arrows g_1),
        ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g_1)) y = x
Φ : P.FullSubcategory
y : Φ.obj.fiber.obj (Over.mk f).left
⊢ y ∈
    (FunctorToTypes.fromOverSubfunctor ⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.fst.obj.fiber
          ⟨Φ, (ConcreteCategory.hom (Φ.obj.fiber.map f)) y⟩.snd).obj
      (Over.mk f)

Tactic:
rw [FunctorToTypes.mem_fromOverSubfunctor_iff]; rfl

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

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
h : K.Generates J
F : Cᵒᵖ ⥤ Type w
H : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
X : C
S : Sieve X
hS : S ∈ J X
x : Presieve.FamilyOfElements F S.arrows
t₁ t₂ : F.obj (Opposite.op X)
ht₁ : x.IsAmalgamation t₁
ht₂ : x.IsAmalgamation t₂
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z)) :=
  fun Z ↦
    ((Set.range fun g ↦ x ↑g ⋯) ∪ Set.range fun g ↦ (ConcreteCategory.hom (F.map g.op)) t₁) ∪
      Set.range fun g ↦ (ConcreteCategory.hom (F.map g.op)) t₂
Q : Subfunctor F := K.subsheafify 𝒮
this✝ : ∀ (Z : C), _root_.Small.{max u v, w} (Q.toFunctor.obj (Opposite.op Z))
hQ : Presieve.IsSheaf J Q.toFunctor
x' : Presieve.FamilyOfElements Q.toFunctor S.arrows := fun Z g hg ↦ ⟨x g hg, ⋯⟩
ht₁' : t₁ ∈ Q.obj (Opposite.op X)
ht₂' : t₂ ∈ Q.obj (Opposite.op X)
this : ⟨t₁, ht₁'⟩ = ⟨t₂, ht₂'⟩
⊢ t₁ = t₂

Tactic:
simp_all

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
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
e : S' ≅ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ e.hom
β : ι → ι'
q' : (i : ι) → X i ⟶ X' (β i)
w' : ∀ (i : ι), q' i ≫ f' (β i) = f i ≫ e.inv
D : F.DescentData f
j : ι'
⊢ 𝟙 (X' j) ≫ f' j = p' j ≫ q' (α j) ≫ f' (β (α j))

Tactic:
by simp [w', reassoc_of% w]

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)
⊢ IsRegularEpi f

Tactic:
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
this✝¹ : Epi ((presheafToSheaf J D).map f.hom)
this✝ : Epi ((presheafToSheaf J D).map i)
this : IsIso ((presheafToSheaf J D).map i)
⊢ IsRegularEpi
    (inv ((sheafificationAdjunction J D).counit.app F) ≫
      (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G)
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasPullbacks C
h : (Subobject.presheaf C).IsRepresentable
⊢ HasSubobjectClassifier C

Tactic:
obtain ⟨Ω, ⟨h⟩⟩ := h

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasPullbacks C
Ω : C
h : (Subobject.presheaf C).RepresentableBy Ω
⊢ HasSubobjectClassifier C
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 ⟶ Ω
hχ' : IsPullback m χ₀' χ' t
this : χ' ≫ eΩ.inv = 𝒞.χ m
⊢ χ' = 𝒞.χ m ≫ eΩ.hom

Tactic:
simpa using this =≫ eΩ.hom

Goal state after:
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
⊢ 𝟙 G.obj ≫ Presheaf.χ m.hom = Subfunctor.lift (Presheaf.χ m.hom) ⋯ ≫ (closedSieves J).ι

Tactic:
simp_all

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
a : ℤ
X : C
hX : ∃ n, P.triangEnvelopeIter n X
⊢ P.triangEnvelope.shift a X

Tactic:
obtain ⟨n, hn⟩ := hX

Goal state after:
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
a : ℤ
X : C
n : ℕ
hn : P.triangEnvelopeIter n X
⊢ P.triangEnvelope.shift a X
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
k : B ⟶ K
hk : ((shiftFunctor C 1).map (ι.map k) ≫ α) ≫ f₃ = 0
l : (shiftFunctor C 1).obj (ι.obj B) ⟶ (Triangle.mk (ι.map f₁) f₂ f₃).obj₂
hl : (shiftFunctor C 1).map (ι.map k) ≫ α = l ≫ (Triangle.mk (ι.map f₁) f₂ f₃).mor₂
⊢ (shiftFunctor C 1).map (ι.map k) = 0

Tactic:
eq_zero_of_hom_shift_pos hι l (by lia),

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
B : A
k : B ⟶ K
hk : ((shiftFunctor C 1).map (ι.map k) ≫ α) ≫ f₃ = 0
l : (shiftFunctor C 1).obj (ι.obj B) ⟶ (Triangle.mk (ι.map f₁) f₂ f₃).obj₂
hl : (shiftFunctor C 1).map (ι.map k) ≫ α = 0 ≫ (Triangle.mk (ι.map f₁) f₂ f₃).mor₂
⊢ (shiftFunctor C 1).map (ι.map k) = 0
Module: Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject

Goal state before:
pp: 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
a b c : EInt
hab : a ≤ b
hbc : b ≤ c
a' b' c' : EInt
hab' : a' ≤ b'
hbc' : b' ≤ c'
φ : mk₂ (homOfLE hab) (homOfLE hbc) ⟶ mk₂ (homOfLE hab') (homOfLE hbc')
x✝ : C
⊢ ((t.eTruncGE.map (φ.app 1)).app ((t.eTruncLT.obj c).obj x✝) ≫
        (t.eTruncGE.obj b').map ((t.eTruncLT.map (φ.app 2)).app x✝)) ≫
      (t.ω₁δ a' b' c' hab' hbc').app x✝ =
    (t.ω₁δ a b c hab hbc).app x✝ ≫
      (shiftFunctor C 1).map
        ((t.eTruncGE.map (φ.app 0)).app ((t.eTruncLT.obj b).obj x✝) ≫
          (t.eTruncGE.obj a').map ((t.eTruncLT.map (φ.app 1)).app x✝))

Tactic:
simp only [ω₁δ_app, ← Functor.map_comp, NatTrans.naturality_assoc, Functor.comp_map,
    Category.assoc, ← Functor.map_comp_assoc, NatTrans.naturality_app_assoc,
    Functor.whiskeringRight_obj_map, Functor.whiskerRight_app, NatTrans.naturality]

Goal state after:
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
a b c : EInt
hab : a ≤ b
hbc : b ≤ c
a' b' c' : EInt
hab' : a' ≤ b'
hbc' : b' ≤ c'
φ : mk₂ (homOfLE hab) (homOfLE hbc) ⟶ mk₂ (homOfLE hab') (homOfLE hbc')
x✝ : C
⊢ (t.eTruncGEδLT.app b).app ((t.eTruncLT.obj c).obj x✝) ≫
      (shiftFunctor C 1).map
        ((t.eTruncLT.map (φ.app 1)).app ((t.eTruncLT.obj c).obj x✝) ≫
          (t.eTruncLT.obj b').map
              ((t.eTruncLT.map (φ.app 2)).app x✝ ≫ (t.eTruncGEπ a').app ((t.eTruncLT.obj c').obj x✝)) ≫
            (t.eTruncLTGEIsoGELT a' b').hom.app ((t.eTruncLT.obj c').obj x✝) ≫
              (t.eTruncGE.obj a').map ((t.eTruncLT.obj b').map ((t.eTruncLTι c').app x✝))) =
    (t.eTruncGEδLT.app b).app ((t.eTruncLT.obj c).obj x✝) ≫
      (shiftFunctor C 1).map
        ((t.eTruncLT.obj b).map ((t.eTruncGEπ a).app ((t.eTruncLT.obj c).obj x✝)) ≫
          (t.eTruncLTGEIsoGELT a b).hom.app ((t.eTruncLT.obj c).obj x✝) ≫
            (t.eTruncGE.map (φ.app 0)).app ((t.eTruncLT.obj b).obj ((t.eTruncLT.obj c).obj x✝)) ≫
              (t.eTruncGE.obj a').map
                ((t.eTruncLT.map (φ.app 1)).app ((t.eTruncLT.obj c).obj x✝) ≫
                  (t.eTruncLT.obj b').map ((t.eTruncLTι c).app x✝)))
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
k : Q ⟶ B
hk : πQ f₂ β ≫ k = 0
⊢ k = 0

Tactic:
replace hk := ι.congr_map hk

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
B : A
k : Q ⟶ B
hk : ι.map (πQ f₂ β ≫ k) = ι.map 0
⊢ k = 0
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
k : Q ⟶ B
hk : f₂ ≫ β ≫ ι.map k = 0
l : (shiftFunctor C 1).obj (Triangle.mk (ι.map f₁) f₂ f₃).obj₁ ⟶ ι.obj B
hl : β ≫ ι.map k = (Triangle.mk (ι.map f₁) f₂ f₃).mor₃ ≫ l
⊢ k = 0

Tactic:
eq_zero_of_hom_shift_pos hι l (by lia),

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
B : A
k : Q ⟶ B
hk : f₂ ≫ β ≫ ι.map k = 0
l : (shiftFunctor C 1).obj (Triangle.mk (ι.map f₁) f₂ f₃).obj₁ ⟶ ι.obj B
hl : β ≫ ι.map k = (Triangle.mk (ι.map f₁) f₂ f₃).mor₃ ≫ 0
⊢ k = 0
Module: Mathlib.Combinatorics.Additive.FreimanHom

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f₁ f₂ : α → β
n : ℕ
hf₁ : IsMulFreimanHom n A B f₁
h : EqOn f₁ f₂ A
s t : Multiset α
hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
h' : s.prod = t.prod
⊢ (map f₂ s).prod = (map f₂ t).prod

Tactic:
by
    rw [map_congr rfl fun x hx => (h (hsA hx)).symm, map_congr rfl fun x hx => (h (htA hx)).symm,
      hf₁.map_prod_eq_map_prod hsA htA hs ht h']

Goal state after:
Module: Mathlib.Combinatorics.Pigeonhole

Goal state before:
pp: α : Type u
β : Type v
inst✝² : DecidableEq β
s : Finset α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : α → Finset β
h₁ : s.Nonempty
h₂ : ∀ j ∈ s, 0 < #(f j)
k : ℕ := s.inf' h₁ fun j ↦ #(f j)
hk : k = s.inf' h₁ fun j ↦ #(f j)
h₃ : ∀ a ∈ s, ∀ x ∈ f a, #{j | j ∈ s ∧ x ∈ f j} ≤ k
this : #s • k ≤ #(s.biUnion f) • k
⊢ #s ≤ #(s.biUnion f)

Tactic:
simp_all

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 : α → β
h : MapsTo f A B
⊢ ∀ ⦃s t : Multiset α⦄,
    (∀ ⦃x : α⦄, x ∈ s → x ∈ A) →
      (∀ ⦃x : α⦄, x ∈ t → x ∈ A) → s.card = 0 → t.card = 0 → s.prod = t.prod → (map f s).prod = (map f t).prod

Tactic:
simp_all

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 : α → β
h : BijOn f A B
⊢ ∀ ⦃s t : Multiset α⦄,
    (∀ ⦃x : α⦄, x ∈ s → x ∈ A) →
      (∀ ⦃x : α⦄, x ∈ t → x ∈ A) → s.card = 0 → t.card = 0 → ((map f s).prod = (map f t).prod ↔ s.prod = t.prod)

Tactic:
simp_all

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

Goal state before:
pp: n d : ℕ
⊢ ∃ k ∈ range (n * (d - 1) ^ 2 + 1), ↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1) ≤ ↑(#(sphere n d k))

Tactic:
refine exists_le_card_fiber_of_nsmul_le_card_of_maps_to (fun x hx => ?_) nonempty_range_add_one ?_

Goal state after:
case refine_1
n d : ℕ
x : Fin n → ℕ
hx : x ∈ box n d
⊢ ∑ i, x i ^ 2 ∈ range (n * (d - 1) ^ 2 + 1)

case refine_2
n d : ℕ
⊢ #(range (n * (d - 1) ^ 2 + 1)) • (↑(d ^ n) / (↑(n * (d - 1) ^ 2) + 1)) ≤ ↑(#(box n d))