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

Goal state before:
pp: 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
data : FunctorialSurjectiveInjectiveFactorizationData A
inst✝ : HasWeakSheafify J A
x✝ : Arrow (Sheaf J A)
⊢ Presheaf.IsLocallySurjective J
    ((sheafToPresheaf J A).map ((inv (sheafificationAdjunction J A).counit).app x✝.left) ≫
      (sheafToPresheaf J A).map
        ((presheafToSheaf J A).map
          ((MorphismProperty.FunctorialFactorizationData.functorCategory data Cᵒᵖ).i.app (Arrow.mk x✝.hom.hom))))

Tactic:
Presheaf.comp_isLocallySurjective_iff,

Goal state after:
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
data : FunctorialSurjectiveInjectiveFactorizationData A
inst✝ : HasWeakSheafify J A
x✝ : Arrow (Sheaf J A)
⊢ Presheaf.IsLocallySurjective J
    ((sheafToPresheaf J A).map
      ((presheafToSheaf J A).map
        ((MorphismProperty.FunctorialFactorizationData.functorCategory data Cᵒᵖ).i.app (Arrow.mk x✝.hom.hom))))
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 : ι
⊢ (familyOfElements w φ i).Compatible

Tactic:
by
  intro Y₁ Y₂ Z g₁ g₂ f₁ f₂ h₁ h₂ fac
  obtain rfl : f₁ = Over.homMk Y₁.hom := by ext; simpa using Over.w f₁
  obtain rfl : f₂ = Over.homMk Y₂.hom := by ext; simpa using Over.w f₂
  obtain ⟨g₁, hg₁, rfl⟩ := Over.homMk_surjective g₁
  obtain ⟨g₂, hg₂, rfl⟩ := Over.homMk_surjective g₂
  obtain ⟨_, a₁, _, ⟨j₁⟩, fac₁⟩ := h₁
  obtain ⟨_, a₂, _, ⟨j₂⟩, fac₂⟩ := h₂
  dsimp at *
  rw [familyOfElements_eq _ _ _ _ fac₁, familyOfElements_eq _ _ _ _ fac₂,
    ← dsimp% mor_precomp w φ Y₁.hom a₁ fac₁ _ _ _ hg₁ rfl,
    ← dsimp% mor_precomp w φ Y₂.hom a₂ fac₂ _ _ _ hg₂ rfl]
  apply mor_unique

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical

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

Tactic:
← IsPullback.paste_vert_iff this.flip (by ext <;> simp [m, pullback.condition])

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
J : Precoverage C
inst✝² : J.toGrothendieck.Subcanonical
inst✝¹ : Limits.HasPullbacks C
inst✝ : J.IsStableUnderBaseChange
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
𝒰 : J.ZeroHypercover X
H : ∀ (i : 𝒰.I₀), IsPullback (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) (𝒰.f i ≫ f) g
h : fst ≫ f = snd ≫ g
i : (𝒰.pullbackCoverOfLeft f g).I₀
m : pullback (𝒰.f i ≫ f) g ⟶ pullback f g := pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯
this : IsPullback (pullback.fst (𝒰.f i ≫ f) g) m (𝒰.f i) (pullback.fst f g)
⊢ IsPullback (pullback.fst fst (𝒰.f i))
    (pullback.lift (pullback.snd fst (𝒰.f i)) (pullback.fst fst (𝒰.f i) ≫ snd) ⋯ ≫ pullback.fst (𝒰.f i ≫ f) g)
    (pullback.lift fst snd h ≫ pullback.fst f g) (𝒰.f i)
Module: Mathlib.CategoryTheory.Sites.LocalProperties

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
K : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf K A
f : F ⟶ G
h : ∀ (i : ι), IsIso ((K.overPullback A (X i)).map f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
harrow : ∀ (I : S.Arrow), IsIso (f.hom.app (op I.Y))
I₁ I₂ : S.Arrow
r : I₁.Relation I₂
hZ : IsIso (f.hom.app (op r.Z))
⊢ (G.obj.map I₁.f.op ≫ inv (f.hom.app (op I₁.Y))) ≫ F.obj.map r.g₁.op =
    (G.obj.map I₂.f.op ≫ inv (f.hom.app (op I₂.Y))) ≫ F.obj.map r.g₂.op

Tactic:
simp only [Category.assoc, f.hom.naturality_inv]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
K : GrothendieckTopology C
A : Type u_2
inst✝ : Category.{v_2, u_2} A
ι : Type u_3
X : ι → C
hX : K.CoversTop X
F G : Sheaf K A
f : F ⟶ G
h : ∀ (i : ι), IsIso ((K.overPullback A (X i)).map f)
hiso : ∀ (Z : C) (i : ι) (g : Z ⟶ X i), IsIso (f.hom.app (op Z))
W : Cᵒᵖ
S : K.Cover (unop W) := hX.cover (unop W)
harrow : ∀ (I : S.Arrow), IsIso (f.hom.app (op I.Y))
I₁ I₂ : S.Arrow
r : I₁.Relation I₂
hZ : IsIso (f.hom.app (op r.Z))
⊢ G.obj.map I₁.f.op ≫ G.obj.map r.g₁.op ≫ inv (f.hom.app (op r.Z)) =
    G.obj.map I₂.f.op ≫ G.obj.map r.g₂.op ≫ inv (f.hom.app (op r.Z))
Module: Mathlib.CategoryTheory.Sites.SheafHom

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
y : (presheafHom F G).obj (op X)
⊢ x.IsAmalgamation y →
    ∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))

Tactic:
intro h Y g hg
    rw [← h g hg]
    dsimp
    rw [presheafHom_map_app_op_mk_id]

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
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
D₁ D₂ : F.DescentData f
φ : D₁ ⟶ D₂
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
this :
  (F.map (f₁ ≫ p' j₁).op.toLoc).toFunctor.map (φ.hom (α j₁)) ≫ D₂.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ =
    D₁.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫ (F.map (f₂ ≫ p' j₂).op.toLoc).toFunctor.map (φ.hom (α j₂))
⊢ (F.map f₁.op.toLoc).toFunctor.map ((F.map (p' j₁).op.toLoc).toFunctor.map (φ.hom (α j₁))) ≫
      (pullFunctorObj w D₂).hom q f₁ f₂ ⋯ ⋯ =
    (pullFunctorObj w D₁).hom q f₁ f₂ ⋯ ⋯ ≫
      (F.map f₂.op.toLoc).toFunctor.map ((F.map (p' j₂).op.toLoc).toFunctor.map (φ.hom (α j₂)))

Tactic:
dsimp at this ⊢

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
S' : C
p : S' ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S'
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j ≫ p
D₁ D₂ : F.DescentData f
φ : D₁ ⟶ D₂
Y : C
q : Y ⟶ S'
j₁ j₂ : ι'
f₁ : Y ⟶ X' j₁
f₂ : Y ⟶ X' j₂
hf₁ : f₁ ≫ f' j₁ = q
hf₂ : f₂ ≫ f' j₂ = q
this :
  (F.map ((p' j₁).op.toLoc ≫ f₁.op.toLoc)).toFunctor.map (φ.hom (α j₁)) ≫ D₂.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ =
    D₁.hom (q ≫ p) (f₁ ≫ p' j₁) (f₂ ≫ p' j₂) ⋯ ⋯ ≫ (F.map ((p' j₂).op.toLoc ≫ f₂.op.toLoc)).toFunctor.map (φ.hom (α j₂))
⊢ (F.map f₁.op.toLoc).toFunctor.map ((F.map (p' j₁).op.toLoc).toFunctor.map (φ.hom (α j₁))) ≫
      pullFunctorObjHom w D₂ (f₁ ≫ f' j₁) f₁ f₂ ⋯ ⋯ =
    pullFunctorObjHom w D₁ (f₁ ≫ f' j₁) f₁ f₂ ⋯ ⋯ ≫
      (F.map f₂.op.toLoc).toFunctor.map ((F.map (p' j₂).op.toLoc).toFunctor.map (φ.hom (α j₂)))
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 (presheafHom (F ⊗ (Functor.const Cᵒᵖ).obj M) G)

Tactic:
← isSheaf_iff_isSheaf_of_type

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
F G : Cᵒᵖ ⥤ A
hG : IsSheaf J G
inst✝ : HasFunctorEnrichedHom A F G
M : A
⊢ IsSheaf J (presheafHom (F ⊗ (Functor.const Cᵒᵖ).obj M) G)
Module: Mathlib.CategoryTheory.Sites.SheafHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
hG : IsSheaf J G
⊢ IsSheaf J (presheafHom F G)

Tactic:
rw [isSheaf_iff_isSheaf_of_type]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
hG : IsSheaf J G
⊢ Presieve.IsSheaf J (presheafHom F G)
Module: Mathlib.CategoryTheory.Sites.Types

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

Tactic:
rw [isSheaf_iff_isSheaf_of_type]

Goal state after:
α : Type u
⊢ Presieve.IsSheaf typesGrothendieckTopology (yoneda.obj α)
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'
S : Set (SubmonoidFunctor M)
U✝ V✝ : C
f : U✝ ⟶ V✝
⊢ ⨅ F ∈ S, F.obj U✝ ≤ Submonoid.comap (MonCat.Hom.hom (M.map f)) (⨅ F ∈ S, F.obj V✝)

Tactic:
by
        rw [(Submonoid.gc_map_comap (M.map f).hom).u_iInf₂]
        exact iInf₂_mono fun F _ ↦ F.map f

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
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
h₁ : ∀ (i' : ι'), ∃ i g', g' ≫ f i = f' i'
h₂ : ∀ (i : ι), ∃ i' g, g ≫ f' i' = f i
⊢ ∃ e, Nonempty (F.toDescentData f ⋙ e.functor ≅ F.toDescentData f')

Tactic:
choose α p' w using h₁

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
ι' : Type t'
X' : ι' → C
f' : (i' : ι') → X' i' ⟶ S
h : Sieve.ofArrows X f = Sieve.ofArrows X' f'
h₂ : ∀ (i : ι), ∃ i' g, g ≫ f' i' = f i
α : ι' → ι
p' : (i' : ι') → X' i' ⟶ X (α i')
w : ∀ (i' : ι'), p' i' ≫ f (α i') = f' i'
⊢ ∃ e, Nonempty (F.toDescentData f ⋙ e.functor ≅ F.toDescentData f')
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
J : GrothendieckTopology C
hF : ∀ (S : C), ∀ R ∈ J S, F.IsPrestackFor R.arrows
S✝ : C
M N : ↑(F.obj { as := op S✝ })
⊢ Presheaf.IsSheaf (J.over S✝) (F.presheafHom M N)

Tactic:
rw [isSheaf_iff_isSheaf_of_type]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
J : GrothendieckTopology C
hF : ∀ (S : C), ∀ R ∈ J S, F.IsPrestackFor R.arrows
S✝ : C
M N : ↑(F.obj { as := op S✝ })
⊢ Presieve.IsSheaf (J.over S✝) (F.presheafHom M N)
Module: Mathlib.CategoryTheory.Triangulated.Opposite.OpOp

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : HasZeroObject C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
this :
  (𝟭 C).map T.mor₃ ≫ (shiftFunctorCompIsoId C (-1) 1 ⋯).inv.app ((shiftFunctor C 1).obj T.obj₁) =
    (shiftFunctorCompIsoId C (-1) 1 ⋯).inv.app T.obj₃ ≫ (shiftFunctor C (-1) ⋙ shiftFunctor C 1).map T.mor₃
⊢ (((opOp C).mapTriangle.obj T).mor₃ ≫
        (shiftFunctor Cᵒᵖᵒᵖ 1).map (Iso.refl ((opOp C).mapTriangle.obj T).obj₁).hom).unop =
    ((Iso.refl ((opOp C).mapTriangle.obj T).obj₃).hom ≫
        ((triangleOpEquivalence Cᵒᵖ).functor.obj (op ((triangleOpEquivalence C).functor.obj (op T)))).mor₃).unop

Tactic:
dsimp at this ⊢

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : HasZeroObject C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
this :
  T.mor₃ ≫ (shiftFunctorCompIsoId C (-1) 1 ⋯).inv.app ((shiftFunctor C 1).obj T.obj₁) =
    (shiftFunctorCompIsoId C (-1) 1 ⋯).inv.app T.obj₃ ≫ (shiftFunctor C 1).map ((shiftFunctor C (-1)).map T.mor₃)
⊢ ((shiftFunctor Cᵒᵖᵒᵖ 1).map (𝟙 (op (op T.obj₁)))).unop ≫
      ((Functor.commShiftIso (opOp C) 1).hom.app T.obj₁).unop ≫ T.mor₃.op =
    (((shiftFunctor Cᵒᵖᵒᵖ 1).map
            (((shiftFunctor Cᵒᵖ 1).map T.mor₃.op).op ≫
              ((opShiftFunctorEquivalence C 1).counitIso.inv.app (op T.obj₁)).op)).unop ≫
        ((opShiftFunctorEquivalence Cᵒᵖ 1).counitIso.inv.app (op (op T.obj₃))).unop) ≫
      𝟙 (op T.obj₃)
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
s A : Set α
t : Set β
f : α → β
hf : IsMulFreimanIso 2 s t f
hAs : A ⊆ s
⊢ ThreeGPFree (f '' A) ↔ ThreeGPFree A

Tactic:
rw [ThreeGPFree, ThreeGPFree]
  have := (hf.bijOn.injOn.mono hAs).bijOn_image (f := f)
  simp +contextual only
    [((hf.bijOn.injOn.mono hAs).bijOn_image (f := f)).forall,
    hf.mul_eq_mul (hAs _) (hAs _) (hAs _) (hAs _), this.injOn.eq_iff]

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

Goal state before:
pp: n d : ℕ
hd : d ≠ 0
hn : 2 ≤ n
⊢ ↑d ^ (n - 2) / ↑n ≤ ↑(rothNumberNat ((2 * d - 1) ^ n))

Tactic:
by
  convert! bound_aux' n d using 1
  rw [cast_mul, cast_pow, mul_comm, ← div_div, pow_sub₀ _ _ hn, ← div_eq_mul_inv, cast_pow]
  rwa [cast_ne_zero]

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 * rexp (-4 * √(log ↑N)) ≤ ↑N / (↑N ^ (2 / ↑n) * (rexp (↑n - 2) * ↑n))

Tactic:
div_eq_mul_inv

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

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
⊢ #(A * C⁻¹) * #B ≤ #(A * B) * #(B / C)

Tactic:
div_eq_mul_inv

Goal state after:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
⊢ #(A * C⁻¹) * #B ≤ #(A * B) * #(B * C⁻¹)
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
⊢ #(A / C) * #B ≤ #(A / B) * #(B / C⁻¹)

Tactic:
div_eq_mul_inv

Goal state after:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
⊢ #(A * C⁻¹) * #B ≤ #(A / B) * #(B / C⁻¹)
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
⊢ #A * #(A * A⁻¹ * A) ≤ #(A * (A * A⁻¹)) * #(A * A)

Tactic:
simpa using ruzsa_triangle_inequality_invMul_mul_mul (A * A⁻¹) A A

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} = G.degree v

Tactic:
by
  simpa only [dart_fst_fiber, Finset.card_univ, card_neighborSet_eq_degree] using
    card_image_of_injective univ (G.dartOfNeighborSet_injective v)

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
⊢ Fintype.card G.Dart = ∑ v, G.degree v

Tactic:
have := Classical.decEq V

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
this : DecidableEq V
⊢ Fintype.card G.Dart = ∑ v, G.degree v
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
⊢ ∃ w, w ≠ v ∧ Odd (G.degree w)

Tactic:
have := Classical.decEq V

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
this : DecidableEq V
⊢ ∃ w, w ≠ v ∧ Odd (G.degree w)
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G₁ G₂ : SimpleGraph V
inst✝¹ : Fintype ↑G₁.edgeSet
inst✝ : Fintype ↑G₂.edgeSet
⊢ G₁.edgeFinset ⊆ G₂.edgeFinset ↔ G₁ ≤ G₂

Tactic:
by
  simp [edgeFinset]

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

Goal state before:
pp: V : Type u_1
G₁ G₂ : SimpleGraph V
inst✝¹ : Fintype ↑G₁.edgeSet
inst✝ : Fintype ↑G₂.edgeSet
⊢ G₁.edgeFinset ⊂ G₂.edgeFinset ↔ G₁ < G₂

Tactic:
by
  simp [edgeFinset]

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

Goal state before:
pp: V : Type u_1
G₁ G₂ : SimpleGraph V
inst✝³ : Fintype ↑G₁.edgeSet
inst✝² : Fintype ↑G₂.edgeSet
inst✝¹ : Fintype ↑(G₁ ⊓ G₂).edgeSet
inst✝ : DecidableEq V
⊢ (G₁ ⊓ G₂).edgeFinset = G₁.edgeFinset ∩ G₂.edgeFinset

Tactic:
by
  simp [edgeFinset]

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

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
k : ℕ
h : G.IsRegularOfDegree k
⊢ Gᶜ.IsRegularOfDegree (Fintype.card V - 1 - k)

Tactic:
by
  intro v
  rw [degree_compl, h 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 w : V
⊢ Fintype.card ↑(G.commonNeighbors v w) ≤ G.degree v

Tactic:
by
  rw [← card_neighborSet_eq_degree]
  exact Set.card_le_card Set.inter_subset_left

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

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
⊢ IsIso (t.eTruncLTι ⊤)

Tactic:
dsimp [eTruncLTι]
  infer_instance

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

Goal state before:
pp: α : 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
⊢ ∑ p ∈ (ofPairwiseDisjoint parts hdisjoint).parts, f p = ∑ p ∈ parts, f p

Tactic:
by_cases hbot : ⊥ ∈ parts

Goal state after:
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

case neg
α : 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
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∈ s
⊢ P.part a ⊆ s

Tactic:
exact P.le <| P.part_mem.2 ha

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
⊢ (image (fun a ↦ {b ∈ x | s a b}) x).sup id = x

Tactic:
by
    ext a
    simp_rw [sup_image, id_comp, mem_sup, mem_filter]
    refine ⟨(·.choose_spec.2.1), fun _ ↦ by use a⟩

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

Goal state before:
pp: case coe.top
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✝ : EInt
X : C
b : ℤ
⊢ IsIso ((t.eTruncLTGELTSelfToLTGE ⊤ (WithBotTop.coe b)).app X)

Tactic:
simp only [eTruncLT_obj_coe, eTruncGE_obj_top, Functor.comp_obj, eTruncLTGELTSelfToLTGE_app,
        eTruncLT_map_eq_truncLTι, zero_map, Functor.map_zero, isIsoZero_iff_source_target_isZero]
      constructor
      all_goals exact Functor.map_isZero _ (Functor.zero_obj _)

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s t s' : Finset α
hs' : s' ⊆ s
t' : Finset α
⊢ t' ⊆ t → ↑(#s) * 1 ≤ ↑(#s') → ↑(#t) * 1 ≤ ↑(#t') → |↑(G.edgeDensity s' t') - ↑(G.edgeDensity s t)| < 1

Tactic:
ht'

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s t s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
⊢ ↑(#s) * 1 ≤ ↑(#s') → ↑(#t) * 1 ≤ ↑(#t') → |↑(G.edgeDensity s' t') - ↑(G.edgeDensity s t)| < 1
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
a b : α
hε : 0 < ε
s' : Finset α
hs' : s' ⊆ {a}
t' : Finset α
ht' : t' ⊆ {b}
hs : ↑(#{a}) * ε ≤ ↑(#s')
ht : ↑(#{b}) * ε ≤ ↑(#t')
⊢ |↑(G.edgeDensity s' t') - ↑(G.edgeDensity {a} {b})| < ε

Tactic:
rw [card_singleton, Nat.cast_one, one_mul] at hs ht

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
a b : α
hε : 0 < ε
s' : Finset α
hs' : s' ⊆ {a}
t' : Finset α
ht' : t' ⊆ {b}
hs : ε ≤ ↑(#s')
ht : ε ≤ ↑(#t')
⊢ |↑(G.edgeDensity s' t') - ↑(G.edgeDensity {a} {b})| < ε
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hH : H ≠ ⊥
⊢ (∀ (b : G.Subgraph), ∀ a ∈ G.edgeSet, ∀ (a_2 : H ≃g b.coe), a ∉ {⋯.some}) ↔ ∀ (x : G.Subgraph), IsEmpty (H ≃g x.coe)

Tactic:
exact forall_congr' fun G' ↦ ⟨fun h ↦ ⟨fun f ↦ h _
    (Subgraph.edgeSet_subset _ <| (aux hH ⟨f⟩).choose_spec) f rfl⟩, fun h _ _ ↦ h.elim⟩

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
hn : ¬G.Adj s t
e : Sym2 V
x✝ y✝ : V
h✝¹ : ¬x✝ = t
h✝ : y✝ = t
⊢ G.Adj x✝ s ↔ G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x ↦ s(x, t)) '' G.neighborSet s

Tactic:
rw [adj_comm]; aesop

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
ha : G.Adj s t
e : Sym2 V
x✝ y✝ : V
h✝¹ : ¬x✝ = t
h✝ : y✝ = t
⊢ G.Adj x✝ s ↔
    (G.Adj x✝ y✝ ∧ ¬(G.Adj x✝ y✝ ∧ (t = x✝ ∨ t = y✝)) ∨ s(x✝, y✝) ∈ (fun x ↦ s(x, t)) '' G.neighborSet s) ∧
      s(x✝, y✝) ∉ {s(t, t)}

Tactic:
rw [adj_comm]; aesop

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
hvw : G.Adj v w
⊢ (G.subgraphOfAdj hvw).neighborSet u = (if u = v then {w} else ∅) ∪ if u = w then {v} else ∅

Tactic:
split_ifs <;> subst_vars <;> simp [*]

Goal state after: