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

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
S : C
E : PreOneHypercover S
F : PreOneHypercover S
inst✝ : HasPullbacks C
f g : E.Hom F
i j : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)
⊢ Sieve.pullback
      (pullback.map ((cylinder f g).f i) ((cylinder f g).f j) (E.f i.fst) (E.f j.fst)
        (pullback.fst (pullback.lift (f.h₀ i.fst) (g.h₀ i.fst) ⋯) (F.toPullback i.snd))
        (pullback.fst (pullback.lift (f.h₀ j.fst) (g.h₀ j.fst) ⋯) (F.toPullback j.snd)) (𝟙 S) ⋯ ⋯)
      (E.sieve₁' i.fst j.fst) ≤
    (cylinder f g).sieve₁' i j

Tactic:
rw [sieve₁', Sieve.ofArrows, ← Sieve.pullbackArrows_comm, Sieve.generate_le_iff]
    rintro Z u ⟨W, v, ⟨k⟩⟩
    simp_rw [← pullbackSymmetry_inv_comp_fst]
    apply (((cylinder f g).sieve₁' i j)).downward_closed
    rw [sieve₁']
    convert! Sieve.ofArrows_mk _ _ (ULift.up k)
    simp [toPullback_cylinder f g ⟨k⟩]

Goal state after:
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₂
⊢ (pullFunctor F ⋯).map { hom := fun i ↦ full_pullFunctor.hom w hf' φ i, comm := ⋯ } = φ

Tactic:
ext i

Goal state after:
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 : ι'
⊢ ((pullFunctor F ⋯).map { hom := fun i ↦ full_pullFunctor.hom w hf' φ i, comm := ⋯ }).hom i = φ.hom i
Module: Mathlib.CategoryTheory.Sites.SheafHom

Goal state before:
pp: case mpr
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)
⊢ (∀ (Y : C) (g : Y ⟶ X) (hg : S.arrows g), y.app (op (Over.mk g)) = (x g hg).app (op (Over.mk (𝟙 Y)))) →
    x.IsAmalgamation y

Tactic:
· intro h Y g hg
    dsimp
    ext ⟨W : Over Y⟩
    refine (h W.left (W.hom ≫ g) (S.downward_closed hg _)).trans ?_
    have H := hx (𝟙 _) W.hom (S.downward_closed hg W.hom) hg (by simp)
    simp only [op_id, Functor.map_id, id_apply] at H
    rw [H, presheafHom_map_app _ _ W.hom (by simp)]
    rfl

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.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
X✝ Y✝ : ↑(F.obj { as := op S })
f : X✝ ⟶ Y✝
⊢ (F.toDescentData f✝ ⋙ pullFunctor F w).map f ≫
      (isoMk (fun i ↦ (Cat.Hom.toNatIso (F.isoMapOfCommSq ⋯)).symm.app Y✝) ⋯).hom =
    (isoMk (fun i ↦ (Cat.Hom.toNatIso (F.isoMapOfCommSq ⋯)).symm.app X✝) ⋯).hom ≫
      ((F.map p.op.toLoc).toFunctor ⋙ F.toDescentData f').map f

Tactic:
ext i

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
X✝ Y✝ : ↑(F.obj { as := op S })
f : X✝ ⟶ Y✝
i : ι'
⊢ ((F.toDescentData f✝ ⋙ pullFunctor F w).map f ≫
          (isoMk (fun i ↦ (Cat.Hom.toNatIso (F.isoMapOfCommSq ⋯)).symm.app Y✝) ⋯).hom).hom
      i =
    ((isoMk (fun i ↦ (Cat.Hom.toNatIso (F.isoMapOfCommSq ⋯)).symm.app X✝) ⋯).hom ≫
          ((F.map p.op.toLoc).toFunctor ⋙ F.toDescentData f').map f).hom
      i
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 : J.W f
hg : J.W g
⊢ J.W (f ⊗ₘ g)

Tactic:
by
    simp only [hP.W_iff (A := A)] at hf hg ⊢
    intro Φ
    rw [Functor.Monoidal.map_tensor]
    infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : LocallySmall.{w, v, u} C
X : C
S : Sieve X
hS :
  ∀ (Φ : (pointsBot C).FullSubcategory) (x : Φ.obj.fiber.obj X),
    ∃ Y g, ∃ (_ : S.arrows g), ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g)) y = x
⊢ S ∈ ⊥ X

Tactic:
obtain ⟨Y, a, ha, b, hb⟩ := hS ⟨_, ⟨X⟩⟩ (shrinkYonedaObjObjEquiv.symm (𝟙 X))
    obtain ⟨b, rfl⟩ := shrinkYonedaObjObjEquiv.symm.surjective b
    dsimp at b hb
    have : b ≫ a = 𝟙 _ :=
      shrinkYonedaObjObjEquiv.symm.injective (by
        rw [← hb, shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm])
    simpa only [bot_covering, ← Sieve.id_mem_iff_eq_top, this]
      using S.downward_closed ha b

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Precoverage.Subsheaf

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

Tactic:
choose i hi using this

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

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
K : Coverage C
⊢ K.Generates K.toGrothendieck

Tactic:
exact Coverage.generates_toGrothendieck _

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

Goal state before:
pp: S : Sheaf typesGrothendieckTopology (Type u)
⊢ { hom := (equivYoneda S.obj ⋯).inv } ≫ { hom := (equivYoneda S.obj ⋯).hom } =
    𝟙 (yoneda'.obj (S.obj.obj (op PUnit.{u + 1})))

Tactic:
by ext1; apply (equivYoneda S.1 S.2).inv_hom_id

Goal state after:
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'
p : M ⟶ M'
S : SubmonoidFunctor M
U✝ V✝ : C
i : U✝ ⟶ V✝
⊢ Submonoid.map (MonCat.Hom.hom (p.app U✝)) (S.obj U✝) ≤
    Submonoid.comap (MonCat.Hom.hom (M'.map i)) (Submonoid.map (MonCat.Hom.hom (p.app V✝)) (S.obj V✝))

Tactic:
← Submonoid.map_le_iff_le_comap,

Goal state after:
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'
p : M ⟶ M'
S : SubmonoidFunctor M
U✝ V✝ : C
i : U✝ ⟶ V✝
⊢ Submonoid.map (MonCat.Hom.hom (M'.map i)) (Submonoid.map (MonCat.Hom.hom (p.app U✝)) (S.obj U✝)) ≤
    Submonoid.map (MonCat.Hom.hom (p.app V✝)) (S.obj V✝)
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
M N : ↑(F.obj { as := op S })
φ : M ⟶ N
⊢ (subtypeCompatibleHomEquiv F f)
      (Presieve.Arrows.toCompatible (F.presheafHom M N) (fun i ↦ Over.homMk (f i) ⋯) (F.presheafHomObjHomEquiv φ)) =
    (F.toDescentData f).map φ

Tactic:
ext i

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
M N : ↑(F.obj { as := op S })
φ : M ⟶ N
i : ι
⊢ ((subtypeCompatibleHomEquiv F f)
          (Presieve.Arrows.toCompatible (F.presheafHom M N) (fun i ↦ Over.homMk (f i) ⋯)
            (F.presheafHomObjHomEquiv φ))).hom
      i =
    ((F.toDescentData f).map φ).hom i
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✝ })
⊢ Presieve.IsSheaf (J.over S✝) (F.presheafHom M N)

Tactic:
intro U

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✝ })
U : Over S✝
⊢ ∀ S ∈ (J.over S✝) U, Presieve.IsSheafFor (F.presheafHom M N) S.arrows
Module: Mathlib.Combinatorics.Pigeonhole

Goal state before:
pp: α : Type u
β : Type v
M : Type w
inst✝³ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : M
inst✝² : CommSemiring M
inst✝¹ : LinearOrder M
inst✝ : IsStrictOrderedRing M
ht : t.Nonempty
hb : ↑(#s) ≤ #t • b
⊢ ∃ y ∈ t, ↑(#({x ∈ s | f x = y})) ≤ b

Tactic:
by
  simp_rw [cast_card] at hb ⊢
  refine
    exists_sum_fiber_le_of_sum_fiber_nonneg_of_sum_le_nsmul
      (fun _ _ => sum_nonneg fun _ _ => zero_le_one) ht hb

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

Goal state before:
pp: case succ
n✝ d n : ℕ
ih :
  ∀ ⦃x₁ : Fin n → ℕ⦄,
    x₁ ∈ {x | ∀ (i : Fin n), x i < d} →
      ∀ ⦃x₂ : Fin n → ℕ⦄, x₂ ∈ {x | ∀ (i : Fin n), x i < d} → (map d) x₁ = (map d) x₂ → x₁ = x₂
x₁ : Fin (n + 1) → ℕ
hx₁ : x₁ ∈ {x | ∀ (i : Fin (n + 1)), x i < d}
x₂ : Fin (n + 1) → ℕ
hx₂ : x₂ ∈ {x | ∀ (i : Fin (n + 1)), x i < d}
h : (map d) x₁ = (map d) x₂
⊢ x₁ = x₂

Tactic:
ext i

Goal state after:
case succ
n✝ d n : ℕ
ih :
  ∀ ⦃x₁ : Fin n → ℕ⦄,
    x₁ ∈ {x | ∀ (i : Fin n), x i < d} →
      ∀ ⦃x₂ : Fin n → ℕ⦄, x₂ ∈ {x | ∀ (i : Fin n), x i < d} → (map d) x₁ = (map d) x₂ → x₁ = x₂
x₁ : Fin (n + 1) → ℕ
hx₁ : x₁ ∈ {x | ∀ (i : Fin (n + 1)), x i < d}
x₂ : Fin (n + 1) → ℕ
hx₂ : x₂ ∈ {x | ∀ (i : Fin (n + 1)), x i < d}
h : (map d) x₁ = (map d) x₂
i : Fin (n + 1)
⊢ x₁ i = x₂ i
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: n d k : ℕ
⊢ ↑(sphere n d k) + ↑(sphere n d k) ⊆ {x | ∀ (i : Fin n), x i < 2 * d - 1}

Tactic:
Set.add_subset_iff

Goal state after:
n d k : ℕ
⊢ ∀ x ∈ ↑(sphere n d k), ∀ y ∈ ↑(sphere n d k), x + y ∈ {x | ∀ (i : Fin n), x i < 2 * d - 1}
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

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

Tactic:
by
  simpa using ruzsa_triangle_inequality_div_div_div A B⁻¹ C

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

Goal state before:
pp: case bot
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
⊢ (t.eTruncLT.obj ⊥).Additive

Tactic:
dsimp; infer_instance

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

Goal state before:
pp: case coe
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
a✝ : ℤ
⊢ (t.eTruncLT.obj (WithBotTop.coe a✝)).Additive

Tactic:
dsimp; infer_instance

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

Goal state before:
pp: case 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
⊢ (t.eTruncLT.obj ⊤).Additive

Tactic:
dsimp; infer_instance

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

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hAB : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
n : ℕ
⊢ ↑(#(A * B ^ n)) ≤ (↑(#(A * B)) / ↑(#A)) ^ n * ↑(#A)

Tactic:
obtain rfl | hA := A.eq_empty_or_nonempty

Goal state after:
case inl
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
B : Finset G
n : ℕ
hAB : ∀ A' ⊆ ∅, #(∅ * B) * #A' ≤ #(A' * B) * #∅
⊢ ↑(#(∅ * B ^ n)) ≤ (↑(#(∅ * B)) / ↑(#∅)) ^ n * ↑(#∅)

case inr
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hAB : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
n : ℕ
hA : A.Nonempty
⊢ ↑(#(A * B ^ n)) ≤ (↑(#(A * B)) / ↑(#A)) ^ n * ↑(#A)
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hAB : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
hA : A.Nonempty
n : ℕ
ih : ↑(#(A * B ^ n)) ≤ (↑(#(A * B)) / ↑(#A)) ^ n * ↑(#A)
⊢ ↑(#(A * (B ^ n * B))) * ↑(#A) = ↑(#(B ^ n * A * B)) * ↑(#A)

Tactic:
mul_left_comm,

Goal state after:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B : Finset G
hAB : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
hA : A.Nonempty
n : ℕ
ih : ↑(#(A * B ^ n)) ≤ (↑(#(A * B)) / ↑(#A)) ^ n * ↑(#A)
⊢ ↑(#(B ^ n * (A * B))) * ↑(#A) = ↑(#(B ^ n * A * B)) * ↑(#A)
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A : Finset G
hA : A.Nonempty
B : Finset G
n : ℕ
⊢ ↑(#(B ^ n)) ≤ (↑(#(A / B)) / ↑(#A)) ^ n * ↑(#A)

Tactic:
simpa only [_root_.pow_zero, div_one] using! pluennecke_ruzsa_inequality_pow_div_pow_div hA _ _ 0

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

Goal state before:
pp: case succ.succ
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
⊢ ↑(#(List.map (fun i ↦ A ^ ε i) (finRange (m + 1 + 1))).prod) ≤ k ^ (m + 1 + 1 - 2) * ↑(#A)

Tactic:
obtain rfl | hA := A.eq_empty_or_nonempty

Goal state after:
case succ.succ.inl
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
k : ℝ
m✝ m : ℕ
hm : 3 ≤ m + 1
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin (m + 1 + 1)), ε i ≠ 0
h : ∀ (ε : Fin 3 → ℤ), (∀ (i : Fin 3), |ε i| = 1) → ↑(#(List.map (fun i ↦ ∅ ^ ε i) (finRange 3)).prod) ≤ k * ↑(#∅)
ih :
  ∀ (ε : Fin (m + 1) → ℤ),
    (∀ (i : Fin (m + 1)), |ε i| = 1) →
      ↑(#(List.map (fun i ↦ ∅ ^ ε i) (finRange (m + 1))).prod) ≤ k ^ (m + 1 - 2) * ↑(#∅)
⊢ ↑(#(List.map (fun i ↦ ∅ ^ ε i) (finRange (m + 1 + 1))).prod) ≤ k ^ (m + 1 + 1 - 2) * ↑(#∅)

case succ.succ.inr
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
⊢ ↑(#(List.map (fun i ↦ A ^ ε i) (finRange (m + 1 + 1))).prod) ≤ k ^ (m + 1 + 1 - 2) * ↑(#A)
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : DecidableRel G.Adj
v : V
⊢ insert v (G.neighborFinset v) = univ ↔ G.IsUniversal v

Tactic:
simp only [Finset.ext_iff, mem_insert, mem_neighborFinset, IsUniversal]
  grind

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ Q.parts
hbc : b ≤ c
d : α
hd : d ∈ P.parts
hcd : c ≤ d
⊢ c ≤ b

Tactic:
rwa [P.disjoint.eq_of_le hb hd (P.ne_bot hb) (hbc.trans hcd)]

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

Goal state before:
pp: case bot
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
⊢ (t.eTruncGE.obj ⊥).Additive

Tactic:
dsimp; infer_instance

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

Goal state before:
pp: case coe
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
a✝ : ℤ
⊢ (t.eTruncGE.obj (WithBotTop.coe a✝)).Additive

Tactic:
dsimp; infer_instance

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

Goal state before:
pp: case 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
⊢ (t.eTruncGE.obj ⊤).Additive

Tactic:
dsimp; infer_instance

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

Goal state before:
pp: case bot
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
X : C
⊢ (t.eTriangleLTGE.obj ⊥).obj X ∈ distinguishedTriangles

Tactic:
Triangle.distinguished_iff_of_isZero₁ _ (Functor.zero_obj X)

Goal state after:
case bot
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
X : C
⊢ IsIso ((t.eTriangleLTGE.obj ⊥).obj X).mor₂
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≠ ⊥
hab : Disjoint a b
hc : a ⊔ b = c
⊢ b ⊔ a = c

Tactic:
_root_.sup_comm

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≠ ⊥
hab : Disjoint a b
hc : a ⊔ b = c
⊢ a ⊔ b = c
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
⊢ 4 ^ #P.parts * (#P.parts * 4 ^ #P.parts) ≤ Fintype.card α

Tactic:
mul_left_comm,

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
⊢ #P.parts * (4 ^ #P.parts * 4 ^ #P.parts) ≤ Fintype.card α
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case coe
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
X : C
n : ℤ
inst✝ : t.IsLE X n
a✝ : ℤ
⊢ t.IsLE ((t.eTruncLT.obj (WithBotTop.coe a✝)).obj X) n

Tactic:
dsimp; infer_instance

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

Goal state before:
pp: case 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
X : C
n : ℤ
inst✝ : t.IsLE X n
⊢ t.IsLE ((t.eTruncLT.obj ⊤).obj X) n

Tactic:
dsimp; infer_instance

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

Goal state before:
pp: case bot
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
X : C
n : ℤ
inst✝ : t.IsGE X n
⊢ t.IsGE ((t.eTruncGE.obj ⊥).obj X) n

Tactic:
dsimp; infer_instance

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

Goal state before:
pp: case coe
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
X : C
n : ℤ
inst✝ : t.IsGE X n
a✝ : ℤ
⊢ t.IsGE ((t.eTruncGE.obj (WithBotTop.coe a✝)).obj X) n

Tactic:
dsimp; infer_instance

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 : α
parts : Finset (Finset α)
h : ∀ p ∈ parts, p ⊆ s
h' : ∀ a ∈ s, ∃! t, t ∈ parts ∧ a ∈ t
h'' : ∅ ∉ parts
⊢ parts.sup id = s

Tactic:
ext i

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
P : Finpartition s
a : α
parts : Finset (Finset α)
h : ∀ p ∈ parts, p ⊆ s
h' : ∀ a ∈ s, ∃! t, t ∈ parts ∧ a ∈ t
h'' : ∅ ∉ parts
i : α
⊢ i ∈ parts.sup id ↔ i ∈ s