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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Category.{v_3, u_3} E
P : Cᵒᵖ ⥤ D
F : E ⥤ C
inst✝² : ∀ {X B : E} (π : X ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) F
inst✝¹ : F.PreservesEffectiveEpis
hP : EqualizerCondition P
X B : E
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
⊢ Nonempty (IsLimit (Fork.ofι ((F.op ⋙ P).map π.op) ⋯))

Tactic:
have h : P.map (F.map π).op = (F.op ⋙ P).map π.op := by simp

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Category.{v_3, u_3} E
P : Cᵒᵖ ⥤ D
F : E ⥤ C
inst✝² : ∀ {X B : E} (π : X ⟶ B) [EffectiveEpi π], PreservesLimit (cospan π π) F
inst✝¹ : F.PreservesEffectiveEpis
hP : EqualizerCondition P
X B : E
π : X ⟶ B
inst✝ : EffectiveEpi π
c : PullbackCone π π
hc : IsLimit c
h : P.map (F.map π).op = (F.op ⋙ P).map π.op
⊢ Nonempty (IsLimit (Fork.ofι ((F.op ⋙ P).map π.op) ⋯))
Module: Mathlib.CategoryTheory.Sites.Coherent.Comparison

Goal state before:
pp: case refine_1.transitive.a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y : C
T S✝ : Sieve Y
a✝¹ : (extensiveCoverage C ⊔ regularCoverage C).Saturate Y T
a✝ :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, T.arrows f → (extensiveCoverage C ⊔ regularCoverage C).Saturate Y_1 (Sieve.pullback f S✝)
a_ih✝¹ : T ∈ (coherentTopology C) Y
a_ih✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, T.arrows f → Sieve.pullback f S✝ ∈ (coherentTopology C) Y_1
⊢ (coherentCoverage C).Saturate Y T

Tactic:
assumption

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

Goal state before:
pp: case refine_1.transitive.a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y : C
T S✝ : Sieve Y
a✝¹ : (extensiveCoverage C ⊔ regularCoverage C).Saturate Y T
a✝ :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, T.arrows f → (extensiveCoverage C ⊔ regularCoverage C).Saturate Y_1 (Sieve.pullback f S✝)
a_ih✝¹ : T ∈ (coherentTopology C) Y
a_ih✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, T.arrows f → Sieve.pullback f S✝ ∈ (coherentTopology C) Y_1
⊢ ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, T.arrows f → (coherentCoverage C).Saturate Y_1 (Sieve.pullback f S✝)

Tactic:
assumption

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

Goal state before:
pp: case refine_2.transitive.a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y : C
T S✝ : Sieve Y
a✝¹ : (coherentCoverage C).Saturate Y T
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, T.arrows f → (coherentCoverage C).Saturate Y_1 (Sieve.pullback f S✝)
a_ih✝¹ : T ∈ (extensiveCoverage C ⊔ regularCoverage C).toGrothendieck Y
a_ih✝ :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f → Sieve.pullback f S✝ ∈ (extensiveCoverage C ⊔ regularCoverage C).toGrothendieck Y_1
⊢ (extensiveCoverage C ⊔ regularCoverage C).Saturate Y T

Tactic:
assumption

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

Goal state before:
pp: case refine_2.transitive.a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preregular C
inst✝ : FinitaryPreExtensive C
B : C
S : Sieve B
Y : C
T S✝ : Sieve Y
a✝¹ : (coherentCoverage C).Saturate Y T
a✝ : ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, T.arrows f → (coherentCoverage C).Saturate Y_1 (Sieve.pullback f S✝)
a_ih✝¹ : T ∈ (extensiveCoverage C ⊔ regularCoverage C).toGrothendieck Y
a_ih✝ :
  ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄,
    T.arrows f → Sieve.pullback f S✝ ∈ (extensiveCoverage C ⊔ regularCoverage C).toGrothendieck Y_1
⊢ ∀ ⦃Y_1 : C⦄ ⦃f : Y_1 ⟶ Y⦄, T.arrows f → (extensiveCoverage C ⊔ regularCoverage C).Saturate Y_1 (Sieve.pullback f S✝)

Tactic:
assumption

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

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
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
X : C
S : Sieve X
hS : Sieve.functorPushforward F S ∈ (coherentTopology D) (F.obj X)
α : Type
w✝ : Finite α
Y : α → D
π : (a : α) → Y a ⟶ F.obj X
H₁ : EffectiveEpiFamily Y π
H₂ : ∀ (a : α), (Sieve.functorPushforward F S).arrows (π a)
Z : α → C := fun a ↦ ⋯.some.p
g₀ : (a : α) → F.obj (Z a) ⟶ Y a := fun a ↦ F.effectiveEpiOver (Y a)
this : EffectiveEpiFamily (fun a ↦ F.obj (Z a)) fun a ↦ g₀ a ≫ π a
a : α
W : C
g₁ : W ⟶ X
g₂ : Y a ⟶ F.obj W
h₁ : S.arrows g₁
h₂ : π a = g₂ ≫ F.map g₁
⊢ F.preimage (g₀ a ≫ g₂ ≫ F.map g₁) = F.preimage (g₀ a ≫ g₂) ≫ g₁

Tactic:
exact F.map_injective (by simp)

Goal state after:
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✝ : Preregular C
F G : Cᵒᵖ ⥤ D
f : F ⟶ G
⊢ Presheaf.IsLocallySurjective (regularTopology C) f ↔
    ∀ (X : C) (y : ToType (G.obj (op X))),
      ∃ X' φ,
        ∃ (_ : EffectiveEpi φ), ∃ x, (ConcreteCategory.hom (f.app (op X'))) x = (ConcreteCategory.hom (G.map (op φ))) y

Tactic:
constructor
  · intro ⟨h⟩ X y
    specialize h y
    rw [regularTopology.mem_sieves_iff_hasEffectiveEpi] at h
    obtain ⟨X', π, h, h'⟩ := h
    exact ⟨X', π, h, h'⟩
  · intro h
    refine ⟨fun y ↦ ?_⟩
    obtain ⟨X', π, h, h'⟩ := h _ y
    rw [regularTopology.mem_sieves_iff_hasEffectiveEpi]
    exact ⟨X', π, h, h'⟩

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

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
F : C ⥤ D
inst✝⁵ : F.PreservesEffectiveEpis
inst✝⁴ : F.ReflectsEffectiveEpis
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Preregular D
X : C
S : Sieve X
hS : Sieve.functorPushforward F S ∈ (regularTopology D) (F.obj X)
Y : D
π : Y ⟶ F.obj X
H₁ : EffectiveEpi π
g₀ : F.effectiveEpiOverObj Y ⟶ Y := F.effectiveEpiOver Y
W : C
g₁ : W ⟶ X
g₂ : Y ⟶ F.obj W
h₁ : S.arrows g₁
h₂ : π = g₂ ≫ F.map g₁
⊢ F.preimage (g₀ ≫ g₂ ≫ F.map g₁) = F.preimage (g₀ ≫ g₂) ≫ g₁

Tactic:
exact F.map_injective (by simp)

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u₂
inst✝² : Category.{v₂, u₂} A
inst✝¹ : HasWeakSheafify J A
X : Type (max u v)
inst✝ : Unique X
X✝ Y✝ : Sheaf J (Type (max u v))
f : X✝ ⟶ Y✝
x : (Γ J (Type (max u v))).obj X✝
⊢ (ConcreteCategory.hom ((Γ J (Type (max u v))).map f ≫ (ΓObjEquivHom J Y✝ X).toIso.hom)).toFun x =
    (ConcreteCategory.hom
          ((ΓObjEquivHom J X✝ X).toIso.hom ≫
            (coyoneda.obj (op ((constantSheaf J (Type (max u v))).obj X))).map f)).toFun
      x

Tactic:
exact ΓObjEquivHom_naturality J X f x

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

Goal state before:
pp: case refine_3
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : HasWeakSheafify J (Type v)
sq : Square C
inst✝¹ : Mono sq.f₂₄
inst✝ : Mono sq.f₃₄
h₁ : sq.IsPullback
h₂ : Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄
this : Mono sq.f₁₃
F : Sheaf J (Type v)
s : PullbackCone (sq.op.map F.obj).f₂₄ (sq.op.map F.obj).f₃₄
m : s.pt ⟶ (sq.op.map F.obj).X₁
hm₁ : m ≫ (sq.op.map F.obj).f₁₂ = s.fst
hm₂ : m ≫ (sq.op.map F.obj).f₁₃ = s.snd
⊢ m =
    ⋯.amalgamateOfArrows (fun k ↦ WalkingPair.casesOn k sq.f₂₄ sq.f₃₄) h₂ (fun j ↦ WalkingPair.casesOn j s.fst s.snd) ⋯

Tactic:
apply F.2.hom_ext_ofArrows _ h₂
      rintro (_ | _)
      · rw [F.2.amalgamateOfArrows_map _ _ _ _ WalkingPair.left]
        exact hm₁
      · rw [F.2.amalgamateOfArrows_map _ _ _ _ WalkingPair.right]
        exact hm₂

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

Goal state before:
pp: case fst
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
S : J.MayerVietorisSquare
P : Cᵒᵖ ⥤ Type v'
h : S.SheafCondition P
x y : P.obj (op S.X₄)
h₁ : (ConcreteCategory.hom (P.map S.f₂₄.op)) x = (ConcreteCategory.hom (P.map S.f₂₄.op)) y
h₂ : (ConcreteCategory.hom (P.map S.f₃₄.op)) x = (ConcreteCategory.hom (P.map S.f₃₄.op)) y
⊢ (↑(S.toPullbackObj P x)).1 = (↑(S.toPullbackObj P y)).1

Tactic:
assumption

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

Goal state before:
pp: case snd
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
S : J.MayerVietorisSquare
P : Cᵒᵖ ⥤ Type v'
h : S.SheafCondition P
x y : P.obj (op S.X₄)
h₁ : (ConcreteCategory.hom (P.map S.f₂₄.op)) x = (ConcreteCategory.hom (P.map S.f₂₄.op)) y
h₂ : (ConcreteCategory.hom (P.map S.f₃₄.op)) x = (ConcreteCategory.hom (P.map S.f₃₄.op)) y
⊢ (↑(S.toPullbackObj P x)).2 = (↑(S.toPullbackObj P y)).2

Tactic:
assumption

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
inst✝¹ : MonoidalClosed A
F G : Cᵒᵖ ⥤ A
hG : IsSheaf J G
inst✝ : HasFunctorEnrichedHom A F G
M : A
⊢ Presieve.IsSheaf J (functorEnrichedHom A F G ⋙ coyoneda.obj (op M))

Tactic:
rw [Presieve.isSheaf_iff_of_nat_equiv
    (functorEnrichedHomCoyonedaObjEquiv M F G)
    (fun _ _ _ _ ↦ functorEnrichedHomCoyonedaObjEquiv_naturality _ _)]
  rw [← isSheaf_iff_isSheaf_of_type]
  exact Presheaf.IsSheaf.hom (F ⊗ (Functor.const _).obj M) G hG

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
Φ : J.Point
A : Type u'
inst✝² : Category.{v', u'} A
inst✝¹ : MonoidalCategory A
inst✝ : HasColimitsOfSize.{w, w, v', u'} A
P₁ P₂ P₃ : Cᵒᵖ ⥤ A
X : C
x : Φ.fiber.obj X
⊢ (α_ (P₁.obj (Opposite.op X)) (P₂.obj (Opposite.op X)) (P₃.obj (Opposite.op X))).hom ≫
      (Φ.toPresheafFiber X x P₁ ⊗ₘ Φ.toPresheafFiber X x P₂ ⊗ₘ Φ.toPresheafFiber X x P₃) =
    Φ.toPresheafFiber X x ((P₁ ⊗ P₂) ⊗ P₃) ≫
      Φ.presheafFiber.map (α_ P₁ P₂ P₃).hom ≫
        Φ.presheafFiberDesc (fun X x ↦ Φ.toPresheafFiber X x P₁ ⊗ₘ Φ.toPresheafFiber X x (P₂ ⊗ P₃)) ⋯ ≫
          Φ.presheafFiber.obj P₁ ◁
            Φ.presheafFiberDesc (fun X x ↦ Φ.toPresheafFiber X x P₂ ⊗ₘ Φ.toPresheafFiber X x P₃) ⋯

Tactic:
conv_rhs =>
      simp only [toPresheafFiber_naturality_assoc, toPresheafFiber_presheafFiberDesc_assoc,
        tensorHom_def_assoc, ← MonoidalCategory.whiskerLeft_comp,
        toPresheafFiber_presheafFiberDesc]
      rw [← tensorHom_def]
      dsimp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
X : Cᵒᵖ
x : G.obj X
⊢ ∀ {Y Z : C} {f : Y ⟶ Opposite.unop X},
    (∃ a, (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a) →
      ∀ (g : Z ⟶ Y), ∃ a, (ConcreteCategory.hom (G.map (g ≫ f).op)) x = (ConcreteCategory.hom (m.app (Opposite.op Z))) a

Tactic:
by
    intro Y Z f ⟨a, ha⟩ g
    use F.map g.op a
    simp [ha, NatTrans.naturality_apply]

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

Goal state before:
pp: case left
C : Type u_1
D : Type u_2
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this✝ : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj (G.obj T.obj₁)
mem : Triangle.mk (G.map T.mor₁) f g ∈ distinguishedTriangles
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫ (Functor.commShiftIso F 1).hom.app (G.obj T.obj₁) ≫ (shiftFunctor D 1).map (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' : g ≫ (Functor.commShiftIso G 1).inv.app T.obj₁ = (adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃
this : Mono ((adj.homEquiv Z T.obj₃) h)
Y : C
⊢ Function.Injective fun x ↦ x ≫ (adj.homEquiv Z T.obj₃) h

Tactic:
intro φ₁ φ₂ hφ
        rw [← cancel_mono (adj.homEquiv _ _ h)]
        exact 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
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
Q : A
β : X₃ ⟶ ι.obj Q
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
⊢ ι.map (f₁ ≫ πQ f₂ β) = ι.map 0

Tactic:
by
    have := comp_distTriang_mor_zero₁₂ _ hT
    dsimp at this
    simp [reassoc_of% this]

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

Goal state before:
pp: d : ℕ
a : Fin 0 → ℕ
⊢ (map d) a = 0

Tactic:
simp [map]

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

Goal state before:
pp: case zero
d k : ℕ
⊢ #(sphere 0 d k) ≤ rothNumberNat 1

Tactic:
refine (card_le_univ _).trans_eq ?_

Goal state after:
case zero
d k : ℕ
⊢ Fintype.card (Fin 0 → ℕ) = rothNumberNat 1
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B C : Finset G
x : G × G
x✝ : x ∈ (A / B) ×ˢ (C / B)
a✝ b✝ : G
hu :
  a✝ ∈
    bipartiteBelow
      (fun b x ↦
        match x with
        | (a, c) => a / c = b)
      (A / C) x
hv :
  b✝ ∈
    bipartiteBelow
      (fun b x ↦
        match x with
        | (a, c) => a / c = b)
      (A / C) x
⊢ x.1 / x.2 = b✝

Tactic:
· exact ((mem_bipartiteBelow _).1 hv).2

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

Goal state before:
pp: 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 '' A)⁻¹ = ⇑f '' A

Tactic:
by simp [← Set.image_inv, hA.inv_eq_self]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hx : A * A ⊆ x • A
hx' : x⁻¹ • (A * A) ⊆ A
hx_inv : x⁻¹ ∈ A
hx_sq : x * x ∈ A
⊢ A * A ⊆ x • A

Tactic:
assumption

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A : Set G
⊢ (∃ H, ↑H = A) → IsApproximateSubgroup 1 A

Tactic:
rintro ⟨H, rfl⟩

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ IsApproximateSubgroup 1 ↑H
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: case inr.inr.inr.inl
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
hK₁ : 1 ≤ K
δ : Fin 3 → ℤ
this : K ^ 2 ≤ K ^ 3
hδ₀ : δ 0 = -1
hδ₁ : δ 1 = -1
hδ₂ : δ 2 = 1
⊢ ↑(#(A⁻¹ * A⁻¹ * A)) ≤ K ^ 3 * ↑(#A)

Tactic:
nlinarith [small_neg_neg_pos_mul hA]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
⊢ G.edgeFinset = ⊥.edgeFinset ↔ G = ⊥

Tactic:
edgeFinset_inj

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Fintype ↑G.edgeSet
⊢ G = ⊥ ↔ G = ⊥
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: case refine_2.convert_2
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : G = ⊥
⊢ Fintype V

Tactic:
assumption

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
z : ∑ x ∈ P.parts with #x = #s / #P.parts + 1, #x + ∑ x ∈ P.parts with #x = #s / #P.parts, #x = #s
⊢ #({p ∈ P.parts | #p = #s / #P.parts + 1}) = #s % #P.parts

Tactic:
sum_const_nat (m := #s / #P.parts + 1) (by simp),

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
z : #({x ∈ P.parts | #x = #s / #P.parts + 1}) * (#s / #P.parts + 1) + ∑ x ∈ P.parts with #x = #s / #P.parts, #x = #s
⊢ #({p ∈ P.parts | #p = #s / #P.parts + 1}) = #s % #P.parts
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : OrderBot α
inst✝¹ : DecidableEq α
parts : Finset α
hdisjoint : (↑parts).PairwiseDisjoint id
X : Type u_2
inst✝ : AddCommMonoid X
f : α → X
hf : f ⊥ = 0
hbot : ⊥ ∈ parts
⊢ ∑ p ∈ (ofPairwiseDisjoint parts hdisjoint).parts, f p = ∑ p ∈ parts, f p

Tactic:
simp only [Finpartition.ofPairwiseDisjoint]
    rw [← erase_union_eq ⊥ parts hbot, union_comm, sum_union_eq_right]
    · simp
    grind

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 : Setoid α
x : Finset α
inst✝ : DecidableRel ⇑s
this : ∀ (a b c d : α), s a d → s b d → (s a c ↔ s b c)
⊢ (image (fun a ↦ {b ∈ x | s a b}) x).SupIndep id

Tactic:
simp only [supIndep_iff_pairwiseDisjoint, Set.PairwiseDisjoint, Set.Pairwise, coe_image,
        Set.mem_image, mem_coe, ne_eq, onFun, id_eq, disjoint_iff_ne, forall_mem_not_eq,
        forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_filter, not_and, filter_inj',
        not_forall, @not_imp_comm (_ ↔ _), Decidable.not_not]
      intro _ _ _ _ _ _ _ _ ha _ hb
      exact ⟨(s.trans' hb <| s.trans' (s.symm' ha) ·), (s.trans' ha <| s.trans' (s.symm' hb) ·)⟩

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

Goal state before:
pp: α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
hs : s.Nonempty
ht : t.Nonempty
⊢ ↑(#s) * ↑(#t) ≠ 0

Tactic:
exact mod_cast (mul_pos hs.card_pos ht.card_pos).ne'

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ Q,
          (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
            (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #s - n
h : ∀ u ∈ P.parts, #u < m + 1
t : Finset α
hts : t ⊆ s
htn : #t = n
ht : t.Nonempty
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #(s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ x ∈ R.parts, #x = m ∨ #x = m + 1
left✝ : ∀ x ∈ (P.avoid t).parts, #(x \ {y ∈ R.parts | y ⊆ x}.biUnion id) ≤ m
hR₃ : #({i ∈ R.parts | #i = m + 1}) = if 0 < a then b else b - 1
ha : ¬0 < a
H : t ∈ {i ∈ R.parts | #i = m + 1}
⊢ False

Tactic:
exact ht.ne_empty (le_sdiff_right.1 <| R.le <| filter_subset _ _ H)

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
x : V
⊢ G.incidenceSet x ⊆ Sym2.diagSetᶜ

Tactic:
exact (incidenceSet_subset G x).trans G.edgeSet_subset_compl_diagSet

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

Goal state before:
pp: case mpr
α : Type u_4
β : Type u_5
A : SimpleGraph α
B : SimpleGraph β
H' : B.Subgraph
⊢ H' ∈ {B' | Nonempty (A ≃g B'.coe)} → H' ∈ Set.range toSubgraph

Tactic:
· rintro ⟨e⟩
    refine ⟨⟨H'.hom.comp e.toHom, Subgraph.hom_injective.comp e.injective⟩, ?_⟩
    simp [toSubgraph, Subgraph.map_comp]

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

Goal state before:
pp: case refine_2
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H : G.Subgraph
H' : G'.Subgraph
h : Subgraph.map f H ≤ H'
v w : V
hvw : H.Adj v w
⊢ (Subgraph.comap f H').Adj v w

pp: case refine_3
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H : G.Subgraph
H' : G'.Subgraph
h : H ≤ Subgraph.comap f H'
v : W
⊢ v ∈ (Subgraph.map f H).verts → v ∈ H'.verts

pp: case refine_4
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H : G.Subgraph
H' : G'.Subgraph
h : H ≤ Subgraph.comap f H'
v w : W
⊢ (Subgraph.map f H).Adj v w → H'.Adj v w

Tactic:
· simp only [H.adj_sub hvw, comap_adj, true_and]
    exact h.2 ⟨v, w, hvw, rfl, rfl⟩

Goal state after:
case refine_3
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H : G.Subgraph
H' : G'.Subgraph
h : H ≤ Subgraph.comap f H'
v : W
⊢ v ∈ (Subgraph.map f H).verts → v ∈ H'.verts

case refine_4
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H : G.Subgraph
H' : G'.Subgraph
h : H ≤ Subgraph.comap f H'
v w : W
⊢ (Subgraph.map f H).Adj v w → H'.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ Q,
          (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
            (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ #u
t : Finset α
htu : t ⊆ u
htn : #t = n
ht : t.Nonempty
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #(s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ x ∈ R.parts, #x = m ∨ #x = m + 1
hR₂ : ∀ x ∈ (P.avoid t).parts, #(x \ {y ∈ R.parts | y ⊆ x}.biUnion id) ≤ m
hR₃ : #({i ∈ R.parts | #i = m + 1}) = if 0 < a then b else b - 1
h : ¬0 < a
H : t ∈ {i ∈ R.parts | #i = m + 1}
⊢ False

Tactic:
exact ht.ne_empty (le_sdiff_right.1 <| R.le <| filter_subset _ _ H)

Goal state after: