mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: case mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
D : Type u_1
inst✝¹ : Category.{v₁, u_1} D
inst✝ : Preadditive D
N : Mat_ C
j✝ : ((𝟭 (Mat_ C)).obj N).ι
ι✝ : Type
fintype✝ : Fintype ι✝
X✝ : ι✝ → C
f : { ι := ι✝, fintype := fintype✝, X := X✝ } ⟶ N
i✝ : ((𝟭 C).mapMat_.obj { ι := ι✝, fintype := fintype✝, X := X✝ }).ι
⊢ ((𝟭 C).mapMat_.map f ≫ (eqToIso ⋯).hom) i✝ j✝ = ((eqToIso ⋯).hom ≫ (𝟭 (Mat_ C)).map f) i✝ j✝

Tactic:
cases N

Goal state after:
case mk.mk
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
D : Type u_1
inst✝¹ : Category.{v₁, u_1} D
inst✝ : Preadditive D
ι✝¹ : Type
fintype✝¹ : Fintype ι✝¹
X✝¹ : ι✝¹ → C
i✝ : ((𝟭 C).mapMat_.obj { ι := ι✝¹, fintype := fintype✝¹, X := X✝¹ }).ι
ι✝ : Type
fintype✝ : Fintype ι✝
X✝ : ι✝ → C
j✝ : ((𝟭 (Mat_ C)).obj { ι := ι✝, fintype := fintype✝, X := X✝ }).ι
f : { ι := ι✝¹, fintype := fintype✝¹, X := X✝¹ } ⟶ { ι := ι✝, fintype := fintype✝, X := X✝ }
⊢ ((𝟭 C).mapMat_.map f ≫ (eqToIso ⋯).hom) i✝ j✝ = ((eqToIso ⋯).hom ≫ (𝟭 (Mat_ C)).map f) i✝ j✝
Module: Mathlib.CategoryTheory.Preadditive.Mat

Goal state before:
pp: case mk
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Preadditive C
D : Type u_1
inst✝⁵ : Category.{v₁, u_1} D
inst✝⁴ : Preadditive D
E : Type u_2
inst✝³ : Category.{v₁, u_2} E
inst✝² : Preadditive E
F : C ⥤ D
inst✝¹ : F.Additive
G : D ⥤ E
inst✝ : G.Additive
N : Mat_ C
j✝ : ((F.mapMat_ ⋙ G.mapMat_).obj N).ι
ι✝ : Type
fintype✝ : Fintype ι✝
X✝ : ι✝ → C
f : { ι := ι✝, fintype := fintype✝, X := X✝ } ⟶ N
i✝ : ((F ⋙ G).mapMat_.obj { ι := ι✝, fintype := fintype✝, X := X✝ }).ι
⊢ ((F ⋙ G).mapMat_.map f ≫ (eqToIso ⋯).hom) i✝ j✝ = ((eqToIso ⋯).hom ≫ (F.mapMat_ ⋙ G.mapMat_).map f) i✝ j✝

Tactic:
cases N

Goal state after:
case mk.mk
C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
inst✝⁶ : Preadditive C
D : Type u_1
inst✝⁵ : Category.{v₁, u_1} D
inst✝⁴ : Preadditive D
E : Type u_2
inst✝³ : Category.{v₁, u_2} E
inst✝² : Preadditive E
F : C ⥤ D
inst✝¹ : F.Additive
G : D ⥤ E
inst✝ : G.Additive
ι✝¹ : Type
fintype✝¹ : Fintype ι✝¹
X✝¹ : ι✝¹ → C
i✝ : ((F ⋙ G).mapMat_.obj { ι := ι✝¹, fintype := fintype✝¹, X := X✝¹ }).ι
ι✝ : Type
fintype✝ : Fintype ι✝
X✝ : ι✝ → C
j✝ : ((F.mapMat_ ⋙ G.mapMat_).obj { ι := ι✝, fintype := fintype✝, X := X✝ }).ι
f : { ι := ι✝¹, fintype := fintype✝¹, X := X✝¹ } ⟶ { ι := ι✝, fintype := fintype✝, X := X✝ }
⊢ ((F ⋙ G).mapMat_.map f ≫ (eqToIso ⋯).hom) i✝ j✝ = ((eqToIso ⋯).hom ≫ (F.mapMat_ ⋙ G.mapMat_).map f) i✝ j✝
Module: Mathlib.CategoryTheory.Presentable.Type

Goal state before:
pp: case refine_1
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst✝ : Fact κ.IsRegular
J : Type u
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
f : ((coyoneda.obj (op X)).mapCocone c).pt
⊢ ∃ i xi, f = (hom (((coyoneda.obj (op X)).mapCocone c).ι.app i)) xi

pp: case refine_2
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst✝ : Fact κ.IsRegular
J : Type u
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
j : J
f g : (fun X ↦ X) ((F ⋙ coyoneda.obj (op X)).obj j)
h : (hom (((coyoneda.obj (op X)).mapCocone c).ι.app j)) f = (hom (((coyoneda.obj (op X)).mapCocone c).ι.app j)) g
⊢ ∃ k f_1, (hom ((F ⋙ coyoneda.obj (op X)).map f_1)) f = (hom ((F ⋙ coyoneda.obj (op X)).map f_1)) g

Tactic:
· dsimp at f
        choose j g hg using fun x ↦ Types.jointly_surjective_of_isColimit hc (f x)
        refine ⟨IsCardinalFiltered.max j hX,
          ↾fun x ↦ F.map (IsCardinalFiltered.toMax j hX x) (g x), ?_⟩
        dsimp
        ext x
        dsimp at j g hg x ⊢
        rw [← hg]
        exact congr_hom (c.w (IsCardinalFiltered.toMax j hX x)).symm (g x)

Goal state after:
case refine_2
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst✝ : Fact κ.IsRegular
J : Type u
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
j : J
f g : (fun X ↦ X) ((F ⋙ coyoneda.obj (op X)).obj j)
h : (hom (((coyoneda.obj (op X)).mapCocone c).ι.app j)) f = (hom (((coyoneda.obj (op X)).mapCocone c).ι.app j)) g
⊢ ∃ k f_1, (hom ((F ⋙ coyoneda.obj (op X)).map f_1)) f = (hom ((F ⋙ coyoneda.obj (op X)).map f_1)) g
Module: Mathlib.CategoryTheory.RepresentedBy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : C
x : F.obj (op X)
⊢ (∀ {Y : C}, Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f.op)) x) ↔
    IsIso (uliftYonedaEquiv.symm { down := x })

Tactic:
NatTrans.isIso_iff_isIso_app,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : C
x : F.obj (op X)
⊢ (∀ {Y : C}, Function.Bijective fun f ↦ (ConcreteCategory.hom (F.map f.op)) x) ↔
    ∀ (X_1 : Cᵒᵖ), IsIso ((uliftYonedaEquiv.symm { down := x }).app X_1)
Module: Mathlib.CategoryTheory.Sites.Coherent.Equivalence

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preregular C
A : Type u_3
inst✝ : Category.{v_3, u_3} A
e : C ≌ D
F : Cᵒᵖ ⥤ A
⊢ IsSheaf (regularTopology C) F ↔ IsSheaf (regularTopology D) (e.inverse.op ⋙ F)

Tactic:
refine ⟨fun hF ↦ ((e.sheafCongrPreregular A).functor.obj ⟨F, hF⟩).property, fun hF ↦ ?_⟩

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preregular C
A : Type u_3
inst✝ : Category.{v_3, u_3} A
e : C ≌ D
F : Cᵒᵖ ⥤ A
hF : IsSheaf (regularTopology D) (e.inverse.op ⋙ F)
⊢ IsSheaf (regularTopology C) F
Module: Mathlib.CategoryTheory.Sites.Coherent.SheafComparison

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A : Type u₃
inst✝⁵ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
B : Type u₄
inst✝⁴ : Category.{v₄, u₄} B
s : A ⥤ B
inst✝³ : Preregular C
inst✝² : FinitaryExtensive C
inst✝¹ : ∀ (X : C), Projective X
inst✝ : ReflectsFiniteProducts s
hF : PreservesFiniteProducts (F ⋙ s)
⊢ PreservesFiniteProducts F

Tactic:
exact ⟨fun n ↦ ⟨fun {K} ↦ ⟨fun {c} hc ↦ ⟨isLimitOfReflects s (isLimitOfPreserves (F ⋙ s) hc)⟩⟩⟩⟩

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
inst✝ : HasLimitsOfShape ℕᵒᵖ C
X : C
y : (F.obj (op 0)).obj.obj (op X)
n : ℕ
⊢ ((Functor.const ℕᵒᵖ).obj ((coherentTopology C).yoneda.obj (limit (preimageDiagram hF X y)))).map (homOfLE ⋯).op ≫
      (coherentTopology C).yoneda.map (limit.π (preimageDiagram hF X y) (op n)) ≫
        (coherentTopology C).yonedaEquiv.symm ((preimageStruct hF X y).x n) =
    ((coherentTopology C).yoneda.map (limit.π (preimageDiagram hF X y) (op (n + 1))) ≫
        (coherentTopology C).yonedaEquiv.symm ((preimageStruct hF X y).x (n + 1))) ≫
      F.map (homOfLE ⋯).op

Tactic:
simp only [Functor.const_obj_obj, homOfLE_leOfHom, Functor.const_obj_map, Category.id_comp,
      Category.assoc, ← limit.w (preimageDiagram hF X y) (homOfLE (n.le_add_right 1)).op,
      homOfLE_leOfHom, Functor.map_comp]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preregular C
inst✝¹ : FinitaryExtensive C
F : ℕᵒᵖ ⥤ Sheaf (coherentTopology C) (Type v)
c : Cone F
hc : IsLimit c
hF : ∀ (n : ℕ), Sheaf.IsLocallySurjective (F.map (homOfLE ⋯).op)
inst✝ : HasLimitsOfShape ℕᵒᵖ C
X : C
y : (F.obj (op 0)).obj.obj (op X)
n : ℕ
⊢ (coherentTopology C).yoneda.map (limit.π (preimageDiagram hF X y) (op (n + 1))) ≫
      (coherentTopology C).yoneda.map ((preimageDiagram hF X y).map (homOfLE ⋯).op) ≫
        (coherentTopology C).yonedaEquiv.symm ((preimageStruct hF X y).x n) =
    (coherentTopology C).yoneda.map (limit.π (preimageDiagram hF X y) (op (n + 1))) ≫
      (coherentTopology C).yonedaEquiv.symm ((preimageStruct hF X y).x (n + 1)) ≫ F.map (homOfLE ⋯).op
Module: Mathlib.CategoryTheory.Sites.Finite

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
X : C
s : Presieve X
t : ⦃Y : C⦄ → (f : Y ⟶ X) → s f → Presieve Y
hs : s ∈ (Precoverage.finite C).coverings X
ht : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : s f), t f H ∈ (Precoverage.finite C).coverings Y
⊢ s.bind t ∈ (Precoverage.finite C).coverings X

Tactic:
by simpa using hs.biUnion' fun _ _ ↦ (ht _ _).image _

Goal state after:
Module: Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
x✝ : OneCochain G U
⊢ 1 * x✝ = x✝

Tactic:
by ext; apply one_mul

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
inst✝² : J.Subcanonical
K : Type u_1
inst✝¹ : Category.{v_1, u_1} K
F : K ⥤ C
inst✝ : ∀ (X : Sheaf J (Type (max v v'))), PreservesLimit F.op X.obj
c : Cocone F
hc : IsColimit c
⊢ IsColimit ((GrothendieckTopology.uliftYoneda.{v', v, u} J).mapCocone c)

Tactic:
suffices IsLimit (coyoneda.mapCone (J.uliftYoneda.mapCocone c).op) from
      isColimitOfOp (isLimitOfReflects _ this)
    apply evaluationJointlyReflectsLimits
    intro X
    suffices IsLimit ((X.obj ⋙ uliftFunctor).mapCone c.op) from IsLimit.mapConeEquiv
      (isoWhiskerRight (J.uliftYonedaOpCompCoyoneda) ((evaluation _ _ ).obj X)).symm this
    exact isLimitOfPreserves _ hc.op

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Descent.DescentData

Goal state before:
pp: case e'_2.refine_2
C : Type u
inst✝ : Category.{v, u} C
F : Pseudofunctor (LocallyDiscrete Cᵒᵖ) Cat
S : C
R : Sieve S
M N : ↑(F.obj { as := op S })
⊢ (Presieve.ofArrows (fun i ↦ Over.mk i.obj.hom) fun i ↦ Over.homMk i.obj.hom ⋯) ≤
    ((Sieve.overEquiv (Over.mk (𝟙 S))).symm R).arrows

Tactic:
rintro _ _ ⟨_, h⟩
    exact h

Goal state after:
Module: Mathlib.CategoryTheory.UnivLE

Goal state before:
pp: w : uliftFunctor.{u, v}.EssSurj
α : Type (max u v)
a' : Type v
m : Nonempty (uliftFunctor.{u, v}.obj a' ≅ α)
⊢ Small.{v, max u v} α

Tactic:
obtain ⟨m'⟩ := m

Goal state after:
w : uliftFunctor.{u, v}.EssSurj
α : Type (max u v)
a' : Type v
m' : uliftFunctor.{u, v}.obj a' ≅ α
⊢ Small.{v, max u v} α
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
inst✝⁴ : Preadditive A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : ι.Additive
hA : admissibleMorphism ι = ⊤
X₂ X₃ : A
π : X₂ ⟶ X₃
inst✝ : Epi π
X₁ : C
f₂ : ι.obj X₃ ⟶ X₁
f₃ : X₁ ⟶ (shiftFunctor C 1).obj (ι.obj X₂)
hT : Triangle.mk (ι.map π) f₂ f₃ ∈ distinguishedTriangles
this : admissibleMorphism ι π
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
hQ : 𝟙 Q = 0
⊢ IsZero (Triangle.mk α β γ).obj₃

Tactic:
dsimp
    rw [IsZero.iff_id_eq_zero, ← ι.map_id, hQ, ι.map_zero]

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

Goal state before:
pp: C : Type u_1
A : Type u_2
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : Preadditive C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : Pretriangulated C
inst✝⁵ : Category.{v_2, u_2} A
ι : A ⥤ C
hι : ∀ ⦃X Y : A⦄ ⦃n : ℤ⦄ (f : ι.obj X ⟶ (shiftFunctor C n).obj (ι.obj Y)), n < 0 → f = 0
inst✝⁴ : Preadditive A
inst✝³ : ι.Full
inst✝² : ι.Faithful
inst✝¹ : ι.Additive
hA : admissibleMorphism ι = ⊤
X₂ X₃ : A
π : X₂ ⟶ X₃
inst✝ : Epi π
X₁ : C
f₂ : ι.obj X₃ ⟶ X₁
f₃ : X₁ ⟶ (shiftFunctor C 1).obj (ι.obj X₂)
hT : Triangle.mk (ι.map π) f₂ f₃ ∈ distinguishedTriangles
this✝ : admissibleMorphism ι π
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
hQ : 𝟙 Q = 0
this : IsIso α
⊢ (Triangle.mk (ι.map (-ιK f₃ α)) (ι.map π) (f₂ ≫ inv α)).rotate ≅ Triangle.mk (ι.map π) f₂ f₃

Tactic:
exact Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (asIso α)

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : CommMonoid α
inst✝² : CommMonoid β
s : Set α
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
f : F
hf : InjOn (⇑f) (s * s)
h : ThreeGPFree s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
habc : f a * f c = f b * f b
⊢ f (a * c) = f (b * b)

Tactic:
by rwa [map_mul, map_mul]

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

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : Module 𝕜 E
s : Set E
hs₀ : IsClosed s
hs₁ : StrictConvex 𝕜 s
⊢ ThreeAPFree (frontier s)

Tactic:
intro a ha b hb c hc habc
  obtain rfl : (1 / 2 : 𝕜) • a + (1 / 2 : 𝕜) • c = b := by
    rwa [← smul_add, one_div, inv_smul_eq_iff₀ (show (2 : 𝕜) ≠ 0 by simp), two_smul]
  have :=
    hs₁.eq (hs₀.frontier_subset ha) (hs₀.frontier_subset hc) one_half_pos one_half_pos
      (add_halves _) hb.2
  simp [this, ← add_smul]
  ring_nf
  simp

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

Goal state before:
pp: N : ℕ
hN : 64 ≤ N
⊢ 2 ^ ↑6 ≤ ↑N

Tactic:
rpow_natCast

Goal state after:
N : ℕ
hN : 64 ≤ N
⊢ 2 ^ 6 ≤ ↑N
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
⊢ log (2 ^ ↑12) ≤ log ↑N

Tactic:
rpow_natCast

Goal state after:
N : ℕ
hN : 4096 ≤ N
⊢ log (2 ^ 12) ≤ log ↑N
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
h₂ : {x} * A' * B ⊆ {x} * A * B
⊢ #(C' * A * B) * #A ≤ (#(C * A * B) + #(A * B) - #(A' * B)) * #A

Tactic:
gcongr
        rw [h₁]
        refine (card_union_le _ _).trans_eq ?_
        rw [card_sdiff_of_subset h₂, ← add_tsub_assoc_of_le (card_le_card h₂), mul_assoc {_},
          mul_assoc {_}, card_singleton_mul, card_singleton_mul]

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

Goal state before:
pp: ⊢ 64 = 2 ^ ↑6

Tactic:
rpow_natCast

Goal state after:
⊢ 64 = 2 ^ 6
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')
⊢ ↑(#(A * C)) * ↑(#B) ≤ ↑(#(A * B)) * ↑(#(B * C))

Tactic:
← le_div_iff₀ (cast_pos.2 hB.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')
⊢ ↑(#(A * C)) ≤ ↑(#(A * B)) * ↑(#(B * C)) / ↑(#B)
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
F₁ : Finset G
hF₁ : ↑(#F₁) ≤ K
hAF₁ : A ^ 2 ⊆ ↑F₁ • A
F₂ : Finset G
hF₂ : ↑(#F₂) ≤ L
hBF₂ : B ^ 2 ⊆ ↑F₂ • B
this : 1 ≤ K
f : G → G → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
⊢ ↑F₁ ^ (m - 1) * A ∩ (↑F₂ ^ (n - 1) * B) = ⋃ a ∈ F₁ ^ (m - 1), ⋃ b ∈ F₂ ^ (n - 1), a • A ∩ b • B

Tactic:
simp_rw [← smul_eq_mul, ← iUnion_smul_set, iUnion₂_inter_iUnion₂]

Goal state after:
G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
F₁ : Finset G
hF₁ : ↑(#F₁) ≤ K
hAF₁ : A ^ 2 ⊆ ↑F₁ • A
F₂ : Finset G
hF₂ : ↑(#F₂) ≤ L
hBF₂ : B ^ 2 ⊆ ↑F₂ • B
this : 1 ≤ K
f : G → G → G
hf : ∀ (a b : G), a • A ∩ b • B ⊆ f a b • (A⁻¹ * A ∩ (B⁻¹ * B))
⊢ ⋃ i₁ ∈ ↑F₁ ^ (m - 1), ⋃ j₁ ∈ ↑F₂ ^ (n - 1), i₁ • A ∩ j₁ • B = ⋃ a ∈ F₁ ^ (m - 1), ⋃ b ∈ F₂ ^ (n - 1), a • A ∩ b • B
Module: Mathlib.Combinatorics.Additive.ETransform

Goal state before:
pp: case fst
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.1 ∪ e • x.2 ∪ e • (x.2 ∩ e⁻¹ • x.1) = x.1 ∪ e • x.2

Tactic:
rw [smul_finset_inter, smul_inv_smul, inter_comm, union_eq_left]

Goal state after:
case fst
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.1 ∩ e • x.2 ⊆ x.1 ∪ e • x.2
Module: Mathlib.GroupTheory.Order.Min

Goal state before:
pp: n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this : Fact (1 < n)
⊢ ¬ringChar (ZMod n) ∣ n / n.minFac

Tactic:
ringChar.eq (ZMod n) n

Goal state after:
n : ℕ
hn : n ≠ 0
hn₁ : n ≠ 1
this : Fact (1 < n)
⊢ ¬n ∣ n / n.minFac
Module: Mathlib.Combinatorics.Additive.CauchyDavenport

Goal state before:
pp: case refine_2
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(#(a * b)) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : op g • s = s
c : α
hc : c ∈ a⁻¹ • ↑s
⊢ c ∈ a⁻¹ • op g • ↑s

Tactic:
← coe_smul_finset,

Goal state after:
case refine_2
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
ih :
  ∀ (a b : Finset α),
    a.Nonempty → b.Nonempty → DevosMulRel (a, b) (s, t) → minOrder α ≤ ↑(#(a * b)) ∨ #a + #b ≤ #(a * b) + 1
hst : #s ≤ #t
a : α
ha : a ∈ ↑s
b : α
hb : b ∈ ↑s
hab : a ≠ b
g : α
hg : g ≠ 1
hgs : (s ∩ op g • s).Nonempty
hsg : op g • s = s
c : α
hc : c ∈ a⁻¹ • ↑s
⊢ c ∈ a⁻¹ • ↑(op g • s)
Module: Mathlib.Combinatorics.Additive.Convolution

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

Tactic:
by
  simpa using card_smul_inter_smul _ _ x 1

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
d : G.Dart
_h : d ∈ ↑univ
⊢ d.edge ∈ G.edgeFinset

Tactic:
mem_edgeFinset

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
d : G.Dart
_h : d ∈ ↑univ
⊢ d.edge ∈ G.edgeSet
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, G.maxDegree = G.degree v

Tactic:
grind [maxDegree, WithBot.unbotD_coe, max_mem_image_coe <| univ_nonempty.image (G.degree ·)]

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

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
h : a = ⊥
⊢ Nonempty (Finpartition ⊥)

Tactic:
exact ⟨Finpartition.empty α⟩

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
| #P.parts - #s % #P.parts

Tactic:
arg 1

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
| #P.parts
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a : α
⊢ (P.part a).Nonempty ↔ a ∈ s

Tactic:
contrapose!; exact part_eq_empty P

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
⊢ t ∈ (atomise s F).parts ↔ t.Nonempty ∧ ∃ Q ⊆ F, {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u} = t

Tactic:
simp only [atomise, ofErase, bot_eq_empty, mem_erase, mem_image, nonempty_iff_ne_empty,
    mem_powerset]

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 α
inst✝ : DecidableEq α
P : Finpartition s
t : Finset β
⊢ (↑P.parts).PairwiseDisjoint fun a ↦ interedges r a t

Tactic:
exact fun x hx y hy h ↦ interedges_disjoint_left r (P.disjoint hx hy h) _

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 : Finset α
h : ¬G.IsUniform ε s t
⊢ ↑(#t) * ε ≤ ↑(#(G.nonuniformWitnesses ε s t).2)

Tactic:
by
  rw [nonuniformWitnesses, dif_pos h]
  exact (not_isUniform_iff.1 h).choose_spec.2.choose_spec.2.2.1

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

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
x : V
x✝ : Sym2 V
h : x✝ ∈ G.edgeFinset
⊢ x✝ ∈ G.edgeSet

Tactic:
mem_edgeFinset

Goal state after:
V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
x : V
x✝ : Sym2 V
h : x✝ ∈ G.edgeSet
⊢ x✝ ∈ G.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ G.subgraphOfAdj hvw = ⊤.induce {v, w}

Tactic:
by
  ext
  · simp
  · constructor
    · intro h
      simp only [subgraphOfAdj_adj, Sym2.eq, Sym2.rel_iff] at h
      obtain ⟨rfl, rfl⟩ | ⟨rfl, rfl⟩ := h <;> simp [hvw, hvw.symm]
    · intro h
      simp only [induce_adj, Set.mem_insert_iff, Set.mem_singleton_iff, top_adj] at h
      obtain ⟨rfl | rfl, rfl | rfl, ha⟩ := h <;> first | exact (ha.ne rfl).elim | simp

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
this : ↑m / (↑m + 1) = 1 - 1 / (↑m + 1)
⊢ 50 * 2 / ε ^ 5 ≤ ↑m + 1

Tactic:
refine le_trans ?_ (le_add_of_nonneg_right zero_le_one)

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
this : ↑m / (↑m + 1) = 1 - 1 / (↑m + 1)
⊢ 50 * 2 / ε ^ 5 ≤ ↑m
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u₁ v₁ u₂ v₂ : V
q : G.Walk u₁ v₁
p : G.Walk u₂ v₂
h : p.IsSubwalk q
⊢ p.length ≤ q.length

Tactic:
by
  grind [IsSubwalk, length_append]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: case pos.inr
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w x w✝ : V
h' : ¬(u, x).2 = u
p' : G.Walk (u, x).1 w✝
ih : ∀ (h : u ∈ p'.support), List.count s(u, x) (p'.takeUntil u h).edges ≤ 1
a✝ : List.Mem u p'.support
ha : G.Adj (u, x).2 (u, x).1
⊢ List.count s(u, x) (p'.takeUntil u ⋯).edges + 1 ≤ 1

Tactic:
cases p' <;> simp!

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hp : p.IsPath
hnil : ¬p.Nil
hmem : ((u, w) = (u, p.snd) ∨ (u, w) = (u, p.snd).swap) ∨ s(u, w) ∈ p.tail.edges
this : u ∉ p.tail.support
⊢ w = p.snd

Tactic:
grind [fst_mem_support_of_mem_edges]

Goal state after: