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

Goal state before:
pp: case _i
C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ J S
D₁ D₂ : F.DescentData f
φ φ' : D₁ ⟶ D₂
hφ : (pullFunctor F ⋯).map φ = (pullFunctor F ⋯).map φ'
i : ι
this :
  (Sieve.overEquiv (Over.mk (𝟙 (X i)))).symm (Sieve.pullback (f i) (Sieve.ofArrows X' f')) ∈
    (J.over (X i)) (Over.mk (𝟙 (X i)))
⊢ F.presheafHomObjHomEquiv (φ.hom i) = F.presheafHomObjHomEquiv (φ'.hom i)

Tactic:
refine (((isSheaf_iff_isSheaf_of_type _ _).1
      (IsPrestack.isSheaf _ _ _)).isSeparated _ this).ext ?_

Goal state after:
case _i
C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ J S
D₁ D₂ : F.DescentData f
φ φ' : D₁ ⟶ D₂
hφ : (pullFunctor F ⋯).map φ = (pullFunctor F ⋯).map φ'
i : ι
this :
  (Sieve.overEquiv (Over.mk (𝟙 (X i)))).symm (Sieve.pullback (f i) (Sieve.ofArrows X' f')) ∈
    (J.over (X i)) (Over.mk (𝟙 (X i)))
⊢ ∀ ⦃Y : Over (X i)⦄ ⦃f_1 : Y ⟶ Over.mk (𝟙 (X i))⦄,
    ((Sieve.overEquiv (Over.mk (𝟙 (X i)))).symm (Sieve.pullback (f i) (Sieve.ofArrows X' f'))).arrows f_1 →
      (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map f_1.op)) (F.presheafHomObjHomEquiv (φ.hom i)) =
        (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map f_1.op)) (F.presheafHomObjHomEquiv (φ'.hom i))
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 : ι
Y₁ Y₂ Z : Over (X i)
h₁ : (sieve f f' i).arrows (Over.homMk Y₁.hom ⋯)
h₂ : (sieve f f' i).arrows (Over.homMk Y₂.hom ⋯)
g₁ : Z.left ⟶ Y₁.left
hg₁ : g₁ ≫ Y₁.hom = Z.hom
g₂ : Z.left ⟶ Y₂.left
hg₂ : g₂ ≫ Y₂.hom = Z.hom
fac : Over.homMk g₁ ⋯ ≫ Over.homMk Y₁.hom ⋯ = Over.homMk g₂ ⋯ ≫ Over.homMk Y₂.hom ⋯
⊢ (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map (Over.homMk g₁ ⋯).op))
      (familyOfElements w φ i (Over.homMk Y₁.hom ⋯) h₁) =
    (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map (Over.homMk g₂ ⋯).op))
      (familyOfElements w φ i (Over.homMk Y₂.hom ⋯) h₂)

Tactic:
obtain ⟨_, a₁, _, ⟨j₁⟩, fac₁⟩ := h₁

Goal state after:
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 : ι
Y₁ Y₂ Z : Over (X i)
h₂ : (sieve f f' i).arrows (Over.homMk Y₂.hom ⋯)
g₁ : Z.left ⟶ Y₁.left
hg₁ : g₁ ≫ Y₁.hom = Z.hom
g₂ : Z.left ⟶ Y₂.left
hg₂ : g₂ ≫ Y₂.hom = Z.hom
fac : Over.homMk g₁ ⋯ ≫ Over.homMk Y₁.hom ⋯ = Over.homMk g₂ ⋯ ≫ Over.homMk Y₂.hom ⋯
Y : C
j₁ : ι'
a₁ : (Over.forget (X i)).obj Y₁ ⟶ X' j₁
fac₁ : a₁ ≫ f' j₁ = (Over.forget (X i)).map (Over.homMk Y₁.hom ⋯) ≫ f i
⊢ (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map (Over.homMk g₁ ⋯).op))
      (familyOfElements w φ i (Over.homMk Y₁.hom ⋯) ⋯) =
    (ConcreteCategory.hom ((F.presheafHom (D₁.obj i) (D₂.obj i)).map (Over.homMk g₂ ⋯).op))
      (familyOfElements w φ i (Over.homMk Y₂.hom ⋯) h₂)
Module: Mathlib.CategoryTheory.Sites.Descent.Precoverage

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F : LocallyDiscrete Cᵒᵖ ⥤ᵖ Cat
J : GrothendieckTopology C
inst✝ : F.IsPrestack J
ι : Type t
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
ι' : Type t'
X' : ι' → C
f' : (j : ι') → X' j ⟶ S
α : ι' → ι
p' : (j : ι') → X' j ⟶ X (α j)
w : ∀ (j : ι'), p' j ≫ f (α j) = f' j
hf' : Sieve.ofArrows X' f' ∈ J S
D₁ D₂ : F.DescentData f
φ : (pullFunctor F ⋯).obj D₁ ⟶ (pullFunctor F ⋯).obj D₂
i : ι'
⊢ (F.map (p' i).op.toLoc).toFunctor.map (full_pullFunctor.hom w hf' φ (α i)) = φ.hom i

Tactic:
rw [map_hom _ _ _ _ (𝟙 _) (by cat_disch),
        mor_eq _ _ _ _ _ (f' i) (p' i), pullHom_id,
        D₁.hom_self _ _ (by cat_disch), D₂.hom_self _ _ (by cat_disch),
        Category.id_comp, Category.comp_id]

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

Goal state before:
pp: C : Type u
inst✝¹³ : Category.{v, u} C
inst✝¹² : LocallySmall.{w, v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
hP : P.IsConservativeFamilyOfPoints
A : Type u'
inst✝¹¹ : Category.{v', u'} A
inst✝¹⁰ : MonoidalCategory A
inst✝⁹ : HasColimitsOfSize.{w, w, v', u'} A
inst✝⁸ : HasProducts A
FC : A → A → Type u_1
CC : A → Type w
inst✝⁷ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁶ : ConcreteCategory A FC
inst✝⁵ : HasWeakSheafify J A
inst✝⁴ : (forget A).ReflectsIsomorphisms
inst✝³ : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A)
inst✝² : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorLeft X)
inst✝¹ : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorRight X)
inst✝ : J.HasSheafCompose (forget A)
X₁✝ X₂✝ Y₁✝ Y₂✝ : Cᵒᵖ ⥤ A
f : X₁✝ ⟶ X₂✝
g : Y₁✝ ⟶ Y₂✝
hf : ∀ (Φ : P.FullSubcategory), IsIso (Φ.obj.presheafFiber.map f)
hg : ∀ (Φ : P.FullSubcategory), IsIso (Φ.obj.presheafFiber.map g)
Φ : P.FullSubcategory
⊢ IsIso (Φ.obj.presheafFiber.map (f ⊗ₘ g))

Tactic:
rw [Functor.Monoidal.map_tensor]

Goal state after:
C : Type u
inst✝¹³ : Category.{v, u} C
inst✝¹² : LocallySmall.{w, v, u} C
J : GrothendieckTopology C
P : ObjectProperty J.Point
hP : P.IsConservativeFamilyOfPoints
A : Type u'
inst✝¹¹ : Category.{v', u'} A
inst✝¹⁰ : MonoidalCategory A
inst✝⁹ : HasColimitsOfSize.{w, w, v', u'} A
inst✝⁸ : HasProducts A
FC : A → A → Type u_1
CC : A → Type w
inst✝⁷ : (X Y : A) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁶ : ConcreteCategory A FC
inst✝⁵ : HasWeakSheafify J A
inst✝⁴ : (forget A).ReflectsIsomorphisms
inst✝³ : PreservesFilteredColimitsOfSize.{w, w, v', w, u', w + 1} (forget A)
inst✝² : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorLeft X)
inst✝¹ : ∀ (X : A), PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'} (tensorRight X)
inst✝ : J.HasSheafCompose (forget A)
X₁✝ X₂✝ Y₁✝ Y₂✝ : Cᵒᵖ ⥤ A
f : X₁✝ ⟶ X₂✝
g : Y₁✝ ⟶ Y₂✝
hf : ∀ (Φ : P.FullSubcategory), IsIso (Φ.obj.presheafFiber.map f)
hg : ∀ (Φ : P.FullSubcategory), IsIso (Φ.obj.presheafFiber.map g)
Φ : P.FullSubcategory
⊢ IsIso
    (Functor.OplaxMonoidal.δ Φ.obj.presheafFiber X₁✝ Y₁✝ ≫
      (Φ.obj.presheafFiber.map f ⊗ₘ Φ.obj.presheafFiber.map g) ≫ Functor.LaxMonoidal.μ Φ.obj.presheafFiber X₂✝ Y₂✝)
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
β : ι' → ι
p'' : (j : ι') → X' j ⟶ X (β j)
w' : ∀ (j : ι'), p'' j ≫ f (β j) = f' j ≫ p
D : F.DescentData f
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
⊢ f₂ ≫ p' j₂ ≫ f (α j₂) = q ≫ p

Tactic:
rw [w, reassoc_of% hf₂]

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 : F.DescentData f
⊢ ∀ ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂) (hf₁ : f₁ ≫ f i₁ = q) (hf₂ : f₂ ≫ f i₂ = q),
    (F.map f₁.op.toLoc).toFunctor.map
          ((Cat.Hom.toNatIso (F.mapId { as := op (X ((fun x ↦ x) i₁)) })).app (D.obj ((fun x ↦ x) i₁))).hom ≫
        ((𝟭 (F.DescentData f)).obj D).hom q f₁ f₂ ⋯ ⋯ =
      ((pullFunctor F ⋯).obj D).hom q f₁ f₂ ⋯ ⋯ ≫
        (F.map f₂.op.toLoc).toFunctor.map
          ((Cat.Hom.toNatIso (F.mapId { as := op (X ((fun x ↦ x) i₂)) })).app (D.obj ((fun x ↦ x) i₂))).hom

Tactic:
by
    intro Y q i₁ i₂ f₁ f₂ hf₁ hf₂
    dsimp
    rw [pullFunctorObjHom_eq_assoc _ _ _ _ _ q f₁ f₂ rfl]
    simp [mapComp'_id_comp_inv_app_assoc, mapComp'_id_comp_hom_app, ← Functor.map_comp]

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
⊢ m ≫ χ m = (Functor.isTerminalConst Cᵒᵖ Types.isTerminalPUnit).from F ≫ truth C

Tactic:
by
  ext
  apply Sieve.ext
  simp [← NatTrans.naturality_apply]

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J✝ : GrothendieckTopology C
F G : Sheaf J✝ (Type (max u v))
J : GrothendieckTopology C
⊢ Presheaf.IsSheaf J (closedSieves J).toFunctor

Tactic:
rw [CategoryTheory.isSheaf_iff_isSheaf_of_type]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
J✝ : GrothendieckTopology C
F G : Sheaf J✝ (Type (max u v))
J : GrothendieckTopology C
⊢ Presieve.IsSheaf J (closedSieves J).toFunctor
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Functor

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✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X Y : Cᵒᵖ
f : X ⟶ Y
n : ℤ
⊢ F.map ((shiftFunctor Cᵒᵖ n).map f).unop =
    ((commShiftIso F.op n).inv.app Y).unop ≫
      ((shiftFunctor Dᵒᵖ n).map (F.map f.unop).op).unop ≫ ((commShiftIso F.op n).hom.app X).unop

Tactic:
simp [shift_map_op]

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

Goal state before:
pp: α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Set α
a : α
hs : ∀ i ∈ s, i < a
⊢ ThreeGPFree (insert a s) ↔ ThreeGPFree s ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b

Tactic:
refine threeGPFree_insert.trans ?_

Goal state after:
α : Type u_2
inst✝² : CommMonoid α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedCancelMonoid α
s : Set α
a : α
hs : ∀ i ∈ s, i < a
⊢ (ThreeGPFree s ∧
      (∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b) ∧
        ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → b * c = a * a → b = a) ↔
    ThreeGPFree s ∧ ∀ ⦃b : α⦄, b ∈ s → ∀ ⦃c : α⦄, c ∈ s → a * c = b * b → a = b
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s t : Finset α
⊢ Monotone fun s ↦ Nat.findGreatest (fun m ↦ ∃ t ⊆ s, #t = m ∧ ThreeGPFree ↑t) #s

Tactic:
by
    rintro t u htu
    refine Nat.findGreatest_mono (fun m => ?_) (card_le_card htu)
    rintro ⟨v, hvt, hv⟩
    exact ⟨v, hvt.trans htu, hv⟩

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

Goal state before:
pp: M : Type u_1
N : Type u_2
X : Type u_3
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : MulAction M X
inst✝² : MulAction N X
K L : ℝ
A B C : Set X
inst✝¹ : SMul M N
inst✝ : IsScalarTower M N X
hAB : CovBySMul M K A B
hBC : CovBySMul N L B C
⊢ CovBySMul N (K * L) A C

Tactic:
classical
  have := hAB.nonneg
  obtain ⟨F₁, hF₁, hFAB⟩ := hAB
  obtain ⟨F₂, hF₂, hFBC⟩ := hBC
  refine ⟨F₁ • F₂, ?_, ?_⟩
  · calc
      (#(F₁ • F₂) : ℝ) ≤ #F₁ * #F₂ := mod_cast Finset.card_smul_le
      _ ≤ K * L := by gcongr
  · calc
      A ⊆ (F₁ : Set M) • B := hFAB
      _ ⊆ (F₁ : Set M) • (F₂ : Set N) • C := by gcongr
      _ = (↑(F₁ • F₂) : Set N) • C := by simp

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

Goal state before:
pp: n d : ℕ
x : Fin n → ℕ
hx : x ∈ box n d
⊢ ∑ i, x i ^ 2 ≤ n * (d - 1) ^ 2

Tactic:
rw [mem_box] at hx
  have : ∀ i, x i ^ 2 ≤ (d - 1) ^ 2 := fun i =>
    Nat.pow_le_pow_left (Nat.le_sub_one_of_lt (hx i)) _
  exact (sum_le_card_nsmul univ _ _ fun i _ => this i).trans (by rw [Finset.card_fin, smul_eq_mul])

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

Goal state before:
pp: x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
h₂ : 1 - x ≤ 2 - ↑⌈x⌉₊
⊢ rexp (-2 * x) * (x + 1) ≤ rexp (1 - x)

Tactic:
← le_div_iff₀' (exp_pos _),

Goal state after:
x : ℝ
hx : 0 < x
h₁ : ↑⌈x⌉₊ < x + 1
h₂ : 1 - x ≤ 2 - ↑⌈x⌉₊
⊢ x + 1 ≤ rexp (1 - x) / rexp (-2 * x)
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: x : ℝ
hx : 2 / (1 - 2 / rexp 1) ≤ x
⊢ x / rexp 1 < ↑⌊x / 2⌋₊

Tactic:
apply lt_of_le_of_lt _ (sub_one_lt_floor _)
  have : 0 < 1 - 2 / exp 1 := by
    rw [sub_pos, div_lt_one (exp_pos _)]
    exact exp_one_gt_two
  rwa [le_sub_comm, div_eq_mul_one_div x, div_eq_mul_one_div x, ← mul_sub, div_sub', ←
    div_eq_mul_one_div, mul_div_assoc', one_le_div, ← div_le_iff₀ this]
  · exact zero_lt_two
  · exact two_ne_zero

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ (↑A ^ 2)⁻¹ = ↑A ^ 2

Tactic:
simp [← inv_pow, hAsymm, ← coe_inv]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : ↑(#(A ^ 4 * A)) ≤ K ^ 3 * ↑(#A)
hA₀ : A.Nonempty
⊢ CovBySMul G (K ^ 3) ((↑A ^ 2) ^ 2) (↑A ^ 2)

Tactic:
obtain ⟨F, -, hF, hAF⟩ := ruzsa_covering_mul hA₀ hA

Goal state after:
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA₁ : 1 ∈ A
hAsymm : A⁻¹ = A
hA : ↑(#(A ^ 4 * A)) ≤ K ^ 3 * ↑(#A)
hA₀ : A.Nonempty
F : Finset G
hF : ↑(#F) ≤ K ^ 3
hAF : A ^ 4 ⊆ F * (A / A)
⊢ CovBySMul G (K ^ 3) ((↑A ^ 2) ^ 2) (↑A ^ 2)
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
⊢ A ^ 2 ∩ B ^ 2 ⊆ A ^ m ∩ B ^ n

Tactic:
by gcongr; exacts [hA.one_mem, hB.one_mem]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
k : ℝ
m✝ : ℕ
h : ∀ (ε : Fin 3 → ℤ), (∀ (i : Fin 3), |ε i| = 1) → ↑(#(List.map (fun i ↦ A ^ ε i) (finRange 3)).prod) ≤ k * ↑(#A)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ),
    (∀ (i : Fin (m + 1)), |ε i| = 1) →
      ↑(#(List.map (fun i ↦ A ^ ε i) (finRange (m + 1))).prod) ≤ k ^ (m + 1 - 2) * ↑(#A)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin (m + 1 + 1)), ε i ≠ 0
hA : A.Nonempty
hk : 0 ≤ k
π : {n : ℕ} → (Fin n → ℤ) → Finset G := fun {n} δ ↦ (List.map (fun i ↦ A ^ δ i) (finRange n)).prod
V : Finset G := π ![-ε 1, -ε 0]
W : Finset G := π (tail (tail ε))
i : Fin 3
⊢ |![1, -ε 1, -ε 0] i| = 1

Tactic:
by fin_cases i <;> simp [hε]

Goal state after:
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: case neg
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ ↑s, b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
⊢ (∑ i ∈ s, f i) / #s = b

Tactic:
refine
    Nat.div_eq_of_lt_le (le_trans (by simp [mul_comm]) (sum_le_sum fun a ha => (hb a ha).1))
      ((sum_lt_sum (fun a ha => (hb a ha).2) ⟨_, hx₁, (hb _ hx₁).2.lt_of_ne hx₂⟩).trans_le ?_)

Goal state after:
case neg
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ ↑s, b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
⊢ ∑ i ∈ s, (b + 1) ≤ (b + 1) * #s
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
⊢ Disjoint G₁.edgeFinset G₂.edgeFinset ↔ Disjoint G₁ G₂

Tactic:
← Finset.disjoint_coe,

Goal state after:
V : Type u_1
G₁ G₂ : SimpleGraph V
inst✝¹ : Fintype ↑G₁.edgeSet
inst✝ : Fintype ↑G₂.edgeSet
⊢ Disjoint ↑G₁.edgeFinset ↑G₂.edgeFinset ↔ Disjoint G₁ G₂
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
W : Type u_2
G' : SimpleGraph W
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype W
inst✝ : DecidableRel G'.Adj
f : G ≃g G'
this : (fun x ↦ G'.degree x) ∘ ⇑f = fun x ↦ G.degree x
⊢ G.minDegree = G'.minDegree

Tactic:
minDegree,

Goal state after:
V : Type u_1
G : SimpleGraph V
W : Type u_2
G' : SimpleGraph W
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype W
inst✝ : DecidableRel G'.Adj
f : G ≃g G'
this : (fun x ↦ G'.degree x) ∘ ⇑f = fun x ↦ G.degree x
⊢ WithTop.untopD 0 (image (fun v ↦ G.degree v) univ).min = G'.minDegree
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
W : Type u_2
G' : SimpleGraph W
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype W
inst✝ : DecidableRel G'.Adj
f : G ≃g G'
this : (fun x ↦ G'.degree x) ∘ ⇑f = fun x ↦ G.degree x
⊢ WithTop.untopD 0 (image (fun v ↦ G.degree v) univ).min = G'.minDegree

Tactic:
minDegree,

Goal state after:
V : Type u_1
G : SimpleGraph V
W : Type u_2
G' : SimpleGraph W
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype W
inst✝ : DecidableRel G'.Adj
f : G ≃g G'
this : (fun x ↦ G'.degree x) ∘ ⇑f = fun x ↦ G.degree x
⊢ WithTop.untopD 0 (image (fun v ↦ G.degree v) univ).min = WithTop.untopD 0 (image (fun v ↦ G'.degree v) univ).min
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.support ⊆ s
⊢ G.edgeFinset ⊆ s.toFinset.sym2

Tactic:
rw [← coe_subset, coe_sym2, edgeFinset, Set.coe_toFinset, Set.coe_toFinset]

Goal state after:
V : Type u_1
s : Set V
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.support ⊆ s
⊢ G.edgeSet ⊆ s.sym2
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 | #x = #s / #P.parts + 1}) * (#s / #P.parts + 1) +
      #({p ∈ P.parts | #p = #s / #P.parts}) * (#s / #P.parts) =
    #s
⊢ #({p ∈ P.parts | #p = #s / #P.parts + 1}) = #s % #P.parts

Tactic:
← hP.filter_ne_average_add_one_eq_average,

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) +
      #({p ∈ P.parts | ¬#p = #s / #P.parts + 1}) * (#s / #P.parts) =
    #s
⊢ #({p ∈ P.parts | #p = #s / #P.parts + 1}) = #s % #P.parts
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b✝ c : α
P Q : Finpartition a
b : α
hb : b ∈ (P ⊓ Q).parts
⊢ ∃ c ∈ P.parts, b ≤ c

Tactic:
obtain ⟨c, hc, rfl⟩ := mem_image.1 (mem_of_mem_erase hb)

Goal state after:
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c✝ : α
P Q : Finpartition a
c : α × α
hc : c ∈ P.parts ×ˢ Q.parts
hb : c.1 ⊓ c.2 ∈ (P ⊓ Q).parts
⊢ ∃ c_1 ∈ P.parts, c.1 ⊓ c.2 ≤ c_1
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b✝ c : α
P Q : Finpartition a
b : α
hb : b ∈ (P ⊓ Q).parts
⊢ ∃ c ∈ Q.parts, b ≤ c

Tactic:
obtain ⟨c, hc, rfl⟩ := mem_image.1 (mem_of_mem_erase hb)

Goal state after:
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c✝ : α
P Q : Finpartition a
c : α × α
hc : c ∈ P.parts ×ˢ Q.parts
hb : c.1 ⊓ c.2 ∈ (P ⊓ Q).parts
⊢ ∃ c_1 ∈ Q.parts, c.1 ⊓ c.2 ≤ c_1
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

Tactic:
suffices ∀ x₁ ∈ x, ∃ x₂ ∈ x, s x₁ x₂ by simpa [filter_eq_empty_iff]
    intro x _
    use x

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ u : Finset α
P : Finpartition s✝
a✝ : α
s : Finset α
F : Finset (Finset α)
a : α
ha : a ∈ s
t : Finset α
ht : t ∈ F
⊢ t ∈ {u ∈ F | a ∈ u} ↔ a ∈ t

Tactic:
rw [mem_filter]

Goal state after:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
s✝ t✝ u : Finset α
P : Finpartition s✝
a✝ : α
s : Finset α
F : Finset (Finset α)
a : α
ha : a ∈ s
t : Finset α
ht : t ∈ F
⊢ t ∈ F ∧ a ∈ t ↔ a ∈ t
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
⊢ ↑(#s) * ε ≤ ↑(#(G.nonuniformWitness ε s t))

Tactic:
by
  unfold nonuniformWitness
  split_ifs
  · exact G.left_nonuniformWitnesses_card h
  · exact G.right_nonuniformWitnesses_card fun i => h i.symm

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

Goal state before:
pp: case pos
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
x : ↥P.parts.offDiag
hε₁ : ε ≤ 1
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
h : G.IsUniform ε (↑x).1 (↑x).2
⊢ ↑(G.edgeDensity (↑x).1 (↑x).2) ^ 2 - ε ^ 5 / 25 + 0 ≤
    (∑ i ∈ (chunk hP G ε ⋯).parts ×ˢ (chunk hP G ε ⋯).parts, ↑(G.edgeDensity i.1 i.2) ^ 2) / 16 ^ #P.parts

Tactic:
rw [add_zero]

Goal state after:
case pos
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
x : ↥P.parts.offDiag
hε₁ : ε ≤ 1
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
h : G.IsUniform ε (↑x).1 (↑x).2
⊢ ↑(G.edgeDensity (↑x).1 (↑x).2) ^ 2 - ε ^ 5 / 25 ≤
    (∑ i ∈ (chunk hP G ε ⋯).parts ×ˢ (chunk hP G ε ⋯).parts, ↑(G.edgeDensity i.1 i.2) ^ 2) / 16 ^ #P.parts
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ (∑ x ∈ P.parts.offDiag.attach, ∑ i ∈ distinctPairs hP G ε x, ↑(G.edgeDensity i.1 i.2) ^ 2) /
      ↑(#(increment hP G ε).parts) ^ 2 ≤
    ↑((increment hP G ε).energy G)

Tactic:
rw [coe_energy]
        gcongr
        rw [← sum_biUnion pairwiseDisjoint_distinctPairs]
        exact sum_le_sum_of_subset_of_nonneg distinctPairs_increment fun i _ _ ↦ sq_nonneg _

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
x : V
⊢ (G \ fromEdgeSet (G.incidenceSet x)).edgeSet = G.edgeSet \ G.incidenceSet x

Tactic:
edgeSet_sdiff,

Goal state after:
V : Type u_1
G : SimpleGraph V
x : V
⊢ G.edgeSet \ (fromEdgeSet (G.incidenceSet x)).edgeSet = G.edgeSet \ G.incidenceSet x
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s : Set V
x : V
h : x ∉ s
⊢ induce s (G.deleteIncidenceSet x) = induce s G

Tactic:
ext v₁ v₂

Goal state after:
V : Type u_1
G : SimpleGraph V
s : Set V
x : V
h : x ∉ s
v₁ v₂ : ↑s
⊢ (induce s (G.deleteIncidenceSet x)).Adj v₁ v₂ ↔ (induce s G).Adj v₁ v₂