mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
i✝ j✝ : (cylinder f g).I₀
k : (cylinder f g).I₁ i✝ j✝
this : E.p₁ k.down = pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯ ≫ pullback.fst (E.f i✝.fst) (E.f j✝.fst)
⊢ pullback.snd
        (pullback.map (cylinderf f g i✝.snd) (cylinderf f g j✝.snd) (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) ⋯ ⋯)
        (pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯) ≫
      pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯ ≫ pullback.fst (E.f i✝.fst) (E.f j✝.fst) =
    (cylinder f g).p₁ k ≫ pullback.fst (pullback.lift (f.h₀ i✝.fst) (g.h₀ i✝.fst) ⋯) (F.toPullback i✝.snd)

Tactic:
← pullback.condition_assoc

Goal state after:
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✝ : (cylinder f g).I₀
k : (cylinder f g).I₁ i✝ j✝
this : E.p₁ k.down = pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯ ≫ pullback.fst (E.f i✝.fst) (E.f j✝.fst)
⊢ pullback.fst
        (pullback.map (cylinderf f g i✝.snd) (cylinderf f g j✝.snd) (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) ⋯ ⋯)
        (pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯) ≫
      pullback.map (cylinderf f g i✝.snd) (cylinderf f g j✝.snd) (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) ⋯ ⋯ ≫
        pullback.fst (E.f i✝.fst) (E.f j✝.fst) =
    (cylinder f g).p₁ k ≫ pullback.fst (pullback.lift (f.h₀ i✝.fst) (g.h₀ i✝.fst) ⋯) (F.toPullback i✝.snd)
Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
p q : (cylinder f g).I₀
k : (cylinder f g).I₁ p q
this : E.p₂ k.down = pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯ ≫ pullback.snd (E.f p.fst) (E.f q.fst)
⊢ pullback.snd
        (pullback.map (cylinderf f g p.snd) (cylinderf f g q.snd) (E.f p.fst) (E.f q.fst)
          (pullback.fst (pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd))
          (pullback.fst (pullback.lift (f.h₀ q.fst) (g.h₀ q.fst) ⋯) (F.toPullback q.snd)) (𝟙 S) ⋯ ⋯)
        (pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯) ≫
      pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯ ≫ pullback.snd (E.f p.fst) (E.f q.fst) =
    (cylinder f g).p₂ k ≫ pullback.fst (pullback.lift (f.h₀ q.fst) (g.h₀ q.fst) ⋯) (F.toPullback q.snd)

Tactic:
← pullback.condition_assoc

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
p q : (cylinder f g).I₀
k : (cylinder f g).I₁ p q
this : E.p₂ k.down = pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯ ≫ pullback.snd (E.f p.fst) (E.f q.fst)
⊢ pullback.fst
        (pullback.map (cylinderf f g p.snd) (cylinderf f g q.snd) (E.f p.fst) (E.f q.fst)
          (pullback.fst (pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd))
          (pullback.fst (pullback.lift (f.h₀ q.fst) (g.h₀ q.fst) ⋯) (F.toPullback q.snd)) (𝟙 S) ⋯ ⋯)
        (pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯) ≫
      pullback.map (cylinderf f g p.snd) (cylinderf f g q.snd) (E.f p.fst) (E.f q.fst)
          (pullback.fst (pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd))
          (pullback.fst (pullback.lift (f.h₀ q.fst) (g.h₀ q.fst) ⋯) (F.toPullback q.snd)) (𝟙 S) ⋯ ⋯ ≫
        pullback.snd (E.f p.fst) (E.f q.fst) =
    (cylinder f g).p₂ k ≫ pullback.fst (pullback.lift (f.h₀ q.fst) (g.h₀ q.fst) ⋯) (F.toPullback q.snd)
Module: Mathlib.CategoryTheory.Sites.Hypercover.Homotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
p : (cylinder f g).I₀
this : F.p₁ p.snd = pullback.lift (F.p₁ p.snd) (F.p₂ p.snd) ⋯ ≫ pullback.fst (F.f (f.s₀ p.fst)) (F.f (g.s₀ p.fst))
⊢ pullback.snd (pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd) ≫
      pullback.lift (F.p₁ p.snd) (F.p₂ p.snd) ⋯ ≫ pullback.fst (F.f (f.s₀ p.fst)) (F.f (g.s₀ p.fst)) =
    ((cylinderHom f g).comp f).h₀ p

Tactic:
← pullback.condition_assoc

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
p : (cylinder f g).I₀
this : F.p₁ p.snd = pullback.lift (F.p₁ p.snd) (F.p₂ p.snd) ⋯ ≫ pullback.fst (F.f (f.s₀ p.fst)) (F.f (g.s₀ p.fst))
⊢ pullback.fst (pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯) (F.toPullback p.snd) ≫
      pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯ ≫ pullback.fst (F.f (f.s₀ p.fst)) (F.f (g.s₀ p.fst)) =
    ((cylinderHom f g).comp f).h₀ p
Module: Mathlib.CategoryTheory.Sites.Hypercover.Saturate

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
S : C
E : PreZeroHypercover S
F : Cᵒᵖ ⥤ Type u_3
⊢ Nonempty (IsLimit (E.saturate.multifork F)) ↔ Presieve.IsSheafFor F E.presieve₀

Tactic:
rw [Multifork.isLimit_types_iff, Presieve.isSheafFor_ofArrows_iff_bijective_toCompabible,
    ← Function.Bijective.of_comp_iff' (E.sectionsSaturateEquiv F).symm.bijective]
  rfl

Goal state after:
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
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
K : GrothendieckTopology D
G : D ⥤ C
inst✝⁴ : G.IsCoverDense J
inst✝³ : G.Full
inst✝² : G.IsContinuous K J
inst✝¹ : (G.sheafPushforwardContinuous A K J).EssSurj
inst✝ : K.W.IsMonoidal
⊢ J.W.IsMonoidal

Tactic:
rw [← J.W_inverseImage_whiskeringLeft K G]
  infer_instance

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

Goal state before:
pp: case e'_3
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
inst✝¹ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasFunctorEnrichedHom A F₁ F₂
inst✝ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasEnrichedHom A F₁ F₂
G₁ G₂ : Cᵒᵖ ⥤ A
g : G₁ ⟶ G₂
hg : J.W g
F H : Cᵒᵖ ⥤ A
h : Presheaf.IsSheaf J H
this : Function.Bijective ((fun g_1 ↦ g ≫ g_1) ∘ curry)
e_2✝ : (G₁ ⟶ F ⟹ H) = (G₁ ⟶ functorEnrichedHom A F H)
α : F ⊗ G₂ ⟶ H
⊢ curry (F ◁ g ≫ α) = g ≫ curry α

Tactic:
curry_natural_left

Goal state after:
case e'_3
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
inst✝¹ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasFunctorEnrichedHom A F₁ F₂
inst✝ : ∀ (F₁ F₂ : Cᵒᵖ ⥤ A), HasEnrichedHom A F₁ F₂
G₁ G₂ : Cᵒᵖ ⥤ A
g : G₁ ⟶ G₂
hg : J.W g
F H : Cᵒᵖ ⥤ A
h : Presheaf.IsSheaf J H
this : Function.Bijective ((fun g_1 ↦ g ≫ g_1) ∘ curry)
e_2✝ : (G₁ ⟶ F ⟹ H) = (G₁ ⟶ functorEnrichedHom A F H)
α : F ⊗ G₂ ⟶ H
⊢ g ≫ curry α = g ≫ curry α
Module: Mathlib.CategoryTheory.Sites.Precoverage.Generates

Goal state before:
pp: 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
inst✝ : ∀ (Z : C), _root_.Small.{max u v, w} (F.obj (Opposite.op Z))
X✝ : C
S : Sieve X✝
hS : S ∈ J X✝
F' : Cᵒᵖ ⥤ Type (max u v) := FunctorToTypes.shrink.{max u v, w, v, u} F
e : (X : C) → F.obj (Opposite.op X) ≃ F'.obj (Opposite.op X) := fun X ↦ equivShrink (F.obj (Opposite.op X))
he :
  ∀ (X Y : C) (f : X ⟶ Y) (x : F.obj (Opposite.op Y)),
    (e X) ((ConcreteCategory.hom (F.map f.op)) x) = (ConcreteCategory.hom (F'.map f.op)) ((e Y) x)
X : C
R : Presieve X
hR : R ∈ K.coverings X
⊢ Presieve.IsSheafFor F' R

Tactic:
← Presieve.isSheafFor_iff_of_nat_equiv e he

Goal state after:
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
inst✝ : ∀ (Z : C), _root_.Small.{max u v, w} (F.obj (Opposite.op Z))
X✝ : C
S : Sieve X✝
hS : S ∈ J X✝
F' : Cᵒᵖ ⥤ Type (max u v) := FunctorToTypes.shrink.{max u v, w, v, u} F
e : (X : C) → F.obj (Opposite.op X) ≃ F'.obj (Opposite.op X) := fun X ↦ equivShrink (F.obj (Opposite.op X))
he :
  ∀ (X Y : C) (f : X ⟶ Y) (x : F.obj (Opposite.op Y)),
    (e X) ((ConcreteCategory.hom (F.map f.op)) x) = (ConcreteCategory.hom (F'.map f.op)) ((e Y) x)
X : C
R : Presieve X
hR : R ∈ K.coverings X
⊢ Presieve.IsSheafFor F R
Module: Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
F : Cᵒᵖ ⥤ Type w
hF : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))
h : ∀ (Z : C), Small.{max u v, w} ↑(𝒮 Z)
X : C
ι : C → Type (max u v) := fun X ↦ Shrink.{max u v, w} ↑(𝒮 X)
t : (X : C) → ι X → F.obj (Opposite.op X) := fun X i ↦ ↑((equivShrink ↑(𝒮 X)).symm i)
i : (x : F.obj (Opposite.op X)) → K.SubsheafClosure 𝒮 X x → Witness K ι X
hi : ∀ (x : F.obj (Opposite.op X)) (hx : K.SubsheafClosure 𝒮 X x), Witness.eval hF ι t (i x hx) = some x
⊢ Function.Injective fun x ↦ i ↑x ⋯

Tactic:
intro x y hxy

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
F : Cᵒᵖ ⥤ Type w
hF : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
𝒮 : (Z : C) → Set (F.obj (Opposite.op Z))
h : ∀ (Z : C), Small.{max u v, w} ↑(𝒮 Z)
X : C
ι : C → Type (max u v) := fun X ↦ Shrink.{max u v, w} ↑(𝒮 X)
t : (X : C) → ι X → F.obj (Opposite.op X) := fun X i ↦ ↑((equivShrink ↑(𝒮 X)).symm i)
i : (x : F.obj (Opposite.op X)) → K.SubsheafClosure 𝒮 X x → Witness K ι X
hi : ∀ (x : F.obj (Opposite.op X)) (hx : K.SubsheafClosure 𝒮 X x), Witness.eval hF ι t (i x hx) = some x
x y : { x // K.SubsheafClosure 𝒮 X x }
hxy : (fun x ↦ i ↑x ⋯) x = (fun x ↦ i ↑x ⋯) y
⊢ x = y
Module: Mathlib.CategoryTheory.Subfunctor.Subobject

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
A B : Subfunctor F
⊢ A ≤ B →
    { toFun := fun A ↦ Subobject.mk A.ι, invFun := fun X ↦ range X.arrow, left_inv := ⋯, right_inv := ⋯ } A ≤
      { toFun := fun A ↦ Subobject.mk A.ι, invFun := fun X ↦ range X.arrow, left_inv := ⋯, right_inv := ⋯ } B

Tactic:
intro h
      exact leOfHom (((equivalenceMonoOver F).trans
        (ThinSkeleton.equivalence _).symm).functor.map (homOfLE 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 : Sieve S
⊢ F.IsPrestackFor R.arrows ↔
    ∀ (M N : ↑(F.obj { as := op S })),
      Presieve.IsSheafFor (F.presheafHom M N) ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R).arrows

Tactic:
by
  rw [isPrestackFor_iff, Functor.FullyFaithful.nonempty_iff_map_bijective]
  refine forall_congr' (fun M ↦ forall_congr' (fun N ↦ ?_))
  rw [bijective_toDescentData_map_iff]
  convert! Iff.rfl
  refine le_antisymm ?_ ?_
  · rintro X f (hf : R.arrows f.left)
    obtain ⟨X, g, rfl⟩ := Over.mk_surjective X
    obtain rfl : f = Over.homMk g := by ext; simpa using Over.w f
    exact Presieve.ofArrows.mk (ι := R.arrows.category) ⟨Over.mk g, hf⟩
  · rintro _ _ ⟨_, h⟩
    exact h

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
U X : C
m : U ⟶ X
inst✝ : Mono m
χ' : X ⟶ Ω
π : U ⟶ underlying.obj h.Ω₀
sq : IsPullback m π χ' h.Ω₀.arrow
⊢ χ' = h.χ m

Tactic:
by
  apply h.homEquiv.injective
  simp only [χ, Equiv.apply_symm_apply, homEquiv_eq]
  simpa using! Subobject.pullback_obj_mk sq.flip

Goal state after:
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₂
⊢ (adj.homEquiv Z ((shiftFunctor D 1).obj T.obj₁)).symm (g ≫ (Functor.commShiftIso G 1).inv.app T.obj₁) =
    (adj.homEquiv Z ((shiftFunctor D 1).obj T.obj₁)).symm ((adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃)

Tactic:
simp only [Functor.comp_obj, homEquiv_counit, Functor.id_obj, Functor.map_comp, assoc,
        homEquiv_unit, counit_naturality, counit_naturality_assoc, left_triangle_components_assoc,
        ← h₂, adj.shift_counit_app, Iso.hom_inv_id_app_assoc]

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

Goal state before:
pp: case refine_1
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
⊢ 𝟙 ((shiftFunctor C 1).obj (ι.obj 0)) = 0

Tactic:
← Functor.map_id,

Goal state after:
case refine_1
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
⊢ (shiftFunctor C 1).map (𝟙 (ι.obj 0)) = 0
Module: Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory

Goal state before:
pp: case refine_1
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
⊢ (shiftFunctor C 1).map (𝟙 (ι.obj 0)) = 0

Tactic:
← Functor.map_id,

Goal state after:
case refine_1
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
⊢ (shiftFunctor C 1).map (ι.map (𝟙 0)) = 0
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
⊢ 𝟙 ((shiftFunctor C (-1)).obj 0) = 0

Tactic:
← Functor.map_id,

Goal state after:
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
⊢ (shiftFunctor C (-1)).map (𝟙 0) = 0
Module: Mathlib.Combinatorics.Enumerative.DoubleCounting

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
s : Finset α
t : Finset β
hs : ∀ a ∈ s, ∃ b ∈ t, r a b
ht : ∀ b ∈ t, {a | a ∈ s ∧ r a b}.Subsingleton
b : β
h : b ∈ t
⊢ ∀ a ∈ bipartiteBelow r s b, ∀ b_1 ∈ bipartiteBelow r s b, a = b_1

Tactic:
simp_rw [mem_bipartiteBelow]
        exact ht _ h

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

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

Tactic:
simpa [*] using hf.map_prod_eq_map_prod (s := a ::ₘ s) (t := a ::ₘ t)
            (by simpa [hsA ha]) (by simpa [hsA ha])

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

Goal state before:
pp: x : ℝ
hx : 50 / 19 ≤ x
⊢ ↑⌈x⌉₊ < 1.38 * x

Tactic:
refine (ceil_lt_add_one <| hx.trans' <| by norm_num).trans_le ?_

Goal state after:
x : ℝ
hx : 50 / 19 ≤ x
⊢ x + 1 ≤ 1.38 * x
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: case refine_2
G : Type u_1
inst✝³ : Group G
A : Set G
K : ℝ
F✝ : Type u_2
H : Type u_3
inst✝² : Group H
inst✝¹ : FunLike F✝ G H
inst✝ : MonoidHomClass F✝ G H
f : F✝
hA : IsApproximateSubgroup K A
F : Finset G
hF : ↑(#F) ≤ K
hAF : A ^ 2 ⊆ ↑F • A
⊢ (⇑f '' A) ^ 2 ⊆ ↑(Finset.image (⇑f) F) • ⇑f '' A

Tactic:
simp only [← Set.image_pow, Finset.coe_image, ← Set.image_mul, smul_eq_mul] at hAF ⊢
      gcongr

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

Goal state before:
pp: case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
hB : B.Nonempty
hB' : B ∈ B.powerset.erase ∅
U : Finset G
hU : U.Nonempty ∧ U ⊆ B
hUA : ∀ x' ∈ B.powerset.erase ∅, ↑(#(U * A)) / ↑(#U) ≤ ↑(#(x' * A)) / ↑(#x')
⊢ ↑(#(U * A * C)) ≤ ↑(#(U * A)) * ↑(#(U * C)) / ↑(#U)

Tactic:
le_div_iff₀ (cast_pos.2 hU.1.card_pos),

Goal state after:
case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
hB : B.Nonempty
hB' : B ∈ B.powerset.erase ∅
U : Finset G
hU : U.Nonempty ∧ U ⊆ B
hUA : ∀ x' ∈ B.powerset.erase ∅, ↑(#(U * A)) / ↑(#U) ≤ ↑(#(x' * A)) / ↑(#x')
⊢ ↑(#(U * A * C)) * ↑(#U) ≤ ↑(#(U * A)) * ↑(#(U * C))
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ∑ x with ↑(G.degree x) ≠ 0, ↑(G.degree x) = 0
v : V
⊢ v ∈ {x | ↑(G.degree x) ≠ 0} → ↑(G.degree v) = 1

Tactic:
rw [mem_filter_univ, Ne, ZMod.natCast_eq_zero_iff_even, ZMod.natCast_eq_one_iff_odd,
      ← Nat.not_even_iff_odd]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ∑ x with ↑(G.degree x) ≠ 0, ↑(G.degree x) = 0
v : V
⊢ ¬Even (G.degree v) → ¬Even (G.degree v)
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)
k : ℕ
hg : #{v | Odd (G.degree v)} = k + k
⊢ Odd #{w | w ≠ v ∧ Odd (G.degree w)}

Tactic:
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

Goal state after:
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
k : ℕ
hg : #{v | Odd (G.degree v)} = k + k
hk : 0 < k
⊢ Odd #{w | w ≠ v ∧ Odd (G.degree w)}
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: α : Type u_1
s : Set α
f : α → ℕ
⊢ s.EquitableOn f → ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1

Tactic:
obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty

Goal state after:
case inl
α : Type u_1
f : α → ℕ
⊢ ∅.EquitableOn f → ∃ b, ∀ a ∈ ∅, b ≤ f a ∧ f a ≤ b + 1

case inr
α : Type u_1
s : Set α
f : α → ℕ
x : α
hx : x ∈ s
⊢ s.EquitableOn f → ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
Module: Mathlib.Data.Finset.Pairwise

Goal state before:
pp: α : Type u_1
⊢ (Set.range singleton).PairwiseDisjoint id

Tactic:
rintro _ ⟨a, rfl⟩ _ ⟨b, rfl⟩ h

Goal state after:
α : Type u_1
a b : α
h : {a} ≠ {b}
⊢ Function.onFun Disjoint id {a} {b}
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
v : V
hv : G.maxDegree = G.degree v
⊢ G.degree v < Fintype.card V

Tactic:
apply G.degree_lt_card_verts v

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
⊢ G.degree v = Fintype.card V - 1 ↔ G.IsUniversal v

Tactic:
classical
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · rw [← G.insert_neighborFinset_eq_univ v, ← Finset.card_eq_iff_eq_univ]
    simp [h, Nat.sub_add_cancel <| Fintype.card_pos_iff.mpr ⟨v⟩]
  · simp [← card_neighborFinset_eq_degree, (G.neighborFinset_eq_erase_univ v).mpr h]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
⊢ (↑(Finset.map { toFun := singleton, inj' := ⋯ } s)).PairwiseDisjoint id

Tactic:
Finset.coe_map

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
⊢ (⇑{ toFun := singleton, inj' := ⋯ } '' ↑s).PairwiseDisjoint id
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

Goal state before:
pp: ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 100 < 4 ^ ↑(initialBound ε l) * ε ^ 5

Tactic:
← div_lt_iff₀ (pow_pos hε 5),

Goal state after:
ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 100 / ε ^ 5 < 4 ^ ↑(initialBound ε l)