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

Goal state before:
pp: 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
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
Y : C
hx : x.Compatible
g : Y ⟶ X
Z₁ : Over Y
hZ₁ : (Sieve.pullback g S).arrows Z₁.hom
Z₂ : Over Y
hZ₂ : (Sieve.pullback g S).arrows Z₂.hom
f : Z₂ ⟶ Z₁
H : (ConcreteCategory.hom ((presheafHom F G).map (Over.Hom.left f).op)) (x (Z₁.hom ≫ g) hZ₁) = x (Z₂.hom ≫ g) hZ₂
φ : Over.mk (Over.Hom.left f) ⟶ Over.mk (𝟙 Z₁.left) := Over.homMk (Over.Hom.left f) ⋯
H' :
  F.map (Over.Hom.left φ).op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f))) =
    (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left))) ≫ G.map (Over.Hom.left φ).op
⊢ F.map Z₂.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f))) =
    F.map Z₁.hom.op ≫ F.map (Over.Hom.left φ).op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f)))

Tactic:
← F.map_comp_assoc,

Goal state after:
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
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
Y : C
hx : x.Compatible
g : Y ⟶ X
Z₁ : Over Y
hZ₁ : (Sieve.pullback g S).arrows Z₁.hom
Z₂ : Over Y
hZ₂ : (Sieve.pullback g S).arrows Z₂.hom
f : Z₂ ⟶ Z₁
H : (ConcreteCategory.hom ((presheafHom F G).map (Over.Hom.left f).op)) (x (Z₁.hom ≫ g) hZ₁) = x (Z₂.hom ≫ g) hZ₂
φ : Over.mk (Over.Hom.left f) ⟶ Over.mk (𝟙 Z₁.left) := Over.homMk (Over.Hom.left f) ⋯
H' :
  F.map (Over.Hom.left φ).op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f))) =
    (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (𝟙 Z₁.left))) ≫ G.map (Over.Hom.left φ).op
⊢ F.map Z₂.hom.op ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f))) =
    F.map (Z₁.hom.op ≫ (Over.Hom.left φ).op) ≫ (x (Z₁.hom ≫ g) hZ₁).app (op (Over.mk (Over.Hom.left f)))
Module: Mathlib.CategoryTheory.Sites.SheafHom

Goal state before:
pp: 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
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
Y₁ Y₂ : Over X
φ : Y₂ ⟶ Y₁
Z : Over Y₂.left
hZ : (Sieve.pullback Y₂.hom S).arrows Z.hom
⊢ F.map (Over.Hom.left φ).op ≫ F.map Z.hom.op ≫ (x (Z.hom ≫ Y₂.hom) hZ).app (op (Over.mk (𝟙 Z.left))) =
    F.map (Z.hom ≫ Over.Hom.left φ).op ≫ (x ((Z.hom ≫ Over.Hom.left φ) ≫ Y₁.hom) ⋯).app (op (Over.mk (𝟙 Z.left)))

Tactic:
← F.map_comp_assoc,

Goal state after:
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
hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
Y₁ Y₂ : Over X
φ : Y₂ ⟶ Y₁
Z : Over Y₂.left
hZ : (Sieve.pullback Y₂.hom S).arrows Z.hom
⊢ F.map ((Over.Hom.left φ).op ≫ Z.hom.op) ≫ (x (Z.hom ≫ Y₂.hom) hZ).app (op (Over.mk (𝟙 Z.left))) =
    F.map (Z.hom ≫ Over.Hom.left φ).op ≫ (x ((Z.hom ≫ Over.Hom.left φ) ≫ Y₁.hom) ⋯).app (op (Over.mk (𝟙 Z.left)))
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 y : OneCocycle G U}, x.IsCohomologous y → y.IsCohomologous x

Tactic:
rintro γ₁ γ₂ ⟨α, h⟩
    exact ⟨_, h.symm⟩

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

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
h : K.Generates J
F : Cᵒᵖ ⥤ Type w
H : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
X : C
S : Sieve X
hS : S ∈ J X
x : Presieve.FamilyOfElements F S.arrows
t₁ : F.obj (Opposite.op X)
⊢ ∀ (t₂ : F.obj (Opposite.op X)), x.IsAmalgamation t₁ → x.IsAmalgamation t₂ → t₁ = t₂

Tactic:
t₂

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
K : Precoverage C
J : GrothendieckTopology C
h : K.Generates J
F : Cᵒᵖ ⥤ Type w
H : ∀ ⦃X : C⦄, ∀ R ∈ K.coverings X, Presieve.IsSheafFor F R
X : C
S : Sieve X
hS : S ∈ J X
x : Presieve.FamilyOfElements F S.arrows
t₁ t₂ : F.obj (Opposite.op X)
⊢ x.IsAmalgamation t₁ → x.IsAmalgamation t₂ → t₁ = t₂
Module: Mathlib.CategoryTheory.Sites.Types

Goal state before:
pp: S : Type uᵒᵖ ⥤ Type u
hs : Presheaf.IsSheaf typesGrothendieckTopology S
α : Type u
x✝ : α ⟶ S.obj (op PUnit.{u + 1})
⊢ eval S α ((fun f ↦ typesGlue S ⋯ α ⇑(ConcreteCategory.hom f)) x✝) = x✝

Tactic:
by ext; simp [eval_typesGlue]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_3, u_1} C
inst✝⁵ : Category.{u_4, u_2} D
J : GrothendieckTopology C
inst✝⁴ : HasPullbacks D
inst✝³ : HasPushouts D
inst✝² : IsRegularEpiCategory D
h : ∀ {F G : Sheaf J D} (f : F ⟶ G) [Epi f], ∃ I p i, Epi p ∧ Mono i ∧ p ≫ i = f.hom
inst✝¹ : HasSheafify J D
inst✝ : Balanced (Sheaf J D)
F G : Sheaf J D
f : F ⟶ G
x✝ : Epi f
I : Cᵒᵖ ⥤ D
p : F.obj ⟶ I
i : I ⟶ G.obj
hp : Epi p
hi : Mono i
hpi : p ≫ i = f.hom
h₁ :
  (presheafToSheaf J D).map f.hom =
    (sheafificationAdjunction J D).counit.app F ≫ f ≫ inv ((sheafificationAdjunction J D).counit.app G)
h₂ :
  f =
    inv ((sheafificationAdjunction J D).counit.app F) ≫
      (presheafToSheaf J D).map f.hom ≫ (sheafificationAdjunction J D).counit.app G
this✝² : Epi ((presheafToSheaf J D).map f.hom)
this✝¹ : Epi ((presheafToSheaf J D).map i)
this✝ : IsIso ((presheafToSheaf J D).map i)
this : IsRegularEpi p
⊢ IsColimit (Cofork.ofπ ((presheafToSheaf J D).map p) ⋯)

Tactic:
exact isColimitCoforkMapOfIsColimit (presheafToSheaf J D) _
          (isColimitCoforkOfEffectiveEpi p _
            (PullbackCone.isLimitOfFactors f.hom f.hom i _ _ hpi hpi _
              ((isLimitPullbackConeMapOfIsLimit (sheafToPresheaf _ _) _
                (pullbackIsPullback f f)))))

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

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
F G : Cᵒᵖ ⥤ Type (max u v)
m : F ⟶ G
inst✝ : Mono m
hF : Presieve.IsSheaf J F
hG : Presieve.IsSeparated J G
X : Cᵒᵖ
x : G.obj X
Y : C
f : Y ⟶ Opposite.unop X
hf :
  J.Covers
    ((ConcreteCategory.hom
        (↾fun x ↦
          {
            arrows := fun Y f ↦
              ∃ a, (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a,
            downward_closed := ⋯ }))
      x)
    f
a :
  (Z : C) →
    (g : Z ⟶ Y) →
      (Sieve.pullback f ((ConcreteCategory.hom ((χ m).app X)) x)).arrows g → (fun X ↦ X) (F.obj (Opposite.op Z))
ha :
  ∀ (Z : C) (g : Z ⟶ Y) (hg : (Sieve.pullback f ((ConcreteCategory.hom ((χ m).app X)) x)).arrows g),
    (ConcreteCategory.hom (G.map (g ≫ f).op)) x = (ConcreteCategory.hom (m.app (Opposite.op Z))) (a Z g hg)
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ Y
f₂ : Y₂ ⟶ Y
h₁ :
  (Sieve.pullback f
        ((ConcreteCategory.hom
            (↾fun x ↦
              {
                arrows := fun Y f ↦
                  ∃ a, (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a,
                downward_closed := ⋯ }))
          x)).arrows
    f₁
h₂ :
  (Sieve.pullback f
        ((ConcreteCategory.hom
            (↾fun x ↦
              {
                arrows := fun Y f ↦
                  ∃ a, (ConcreteCategory.hom (G.map f.op)) x = (ConcreteCategory.hom (m.app (Opposite.op Y))) a,
                downward_closed := ⋯ }))
          x)).arrows
    f₂
h : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (G.map (g₁ ≫ f₁ ≫ f).op)) x = (ConcreteCategory.hom (G.map (g₂ ≫ f₂ ≫ f).op)) x

Tactic:
reassoc_of% h

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

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

Tactic:
intro φ₁ φ₂ hφ

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

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✝¹³ : HasZeroObject C
inst✝¹² : HasZeroObject D
inst✝¹¹ : Preadditive C
inst✝¹⁰ : Preadditive D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : HasShift D ℤ
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝³ : F.CommShift ℤ
inst✝² : G.CommShift ℤ
inst✝¹ : adj.CommShift ℤ
inst✝ : F.IsTriangulated
T : Triangle D
hT : T ∈ distinguishedTriangles
this✝ : G.Additive
Z : C
f : G.obj T.obj₂ ⟶ Z
g : Z ⟶ (shiftFunctor C 1).obj (G.obj T.obj₁)
mem : Triangle.mk (G.map T.mor₁) f g ∈ distinguishedTriangles
h : F.obj Z ⟶ T.obj₃
h₁ : F.map f ≫ h = adj.counit.app T.obj₂ ≫ T.mor₂
h₂ :
  F.map g ≫ (Functor.commShiftIso F 1).hom.app (G.obj T.obj₁) ≫ (shiftFunctor D 1).map (adj.counit.app T.obj₁) =
    h ≫ T.mor₃
h₁' : f ≫ adj.unit.app Z ≫ G.map h = G.map T.mor₂
h₂' : g ≫ (Functor.commShiftIso G 1).inv.app T.obj₁ = (adj.homEquiv Z T.obj₃) h ≫ G.map T.mor₃
this : Mono ((adj.homEquiv Z T.obj₃) h)
Y : C
φ : Y ⟶ G.obj T.obj₃
⊢ φ ≫ G.map T.mor₃ ≫ (Functor.commShiftIso G 1).hom.app T.obj₁ ≫ (shiftFunctor C 1).map (G.map T.mor₁) = 0

Tactic:
← G.commShiftIso_hom_naturality,

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

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : IsStrictOrderedRing R
r : α → β → Prop
s : Finset α
t : Finset β
m n : R
inst✝ : (a : α) → (b : β) → Decidable (r a b)
hs : s.Nonempty
hm : ∀ a ∈ s, m < ↑(#(bipartiteAbove r t a))
hn : ∀ b ∈ t, ↑(#(bipartiteBelow r s b)) ≤ n
⊢ #s • m = ∑ _a ∈ s, m

Tactic:
by rw [sum_const]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Monoid α
s : Finset α
⊢ ThreeGPFree ↑∅

Tactic:
norm_cast; exact threeGPFree_empty

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

Goal state before:
pp: n d k : ℕ
a : Fin n → ℕ
ha : a ∈ ↑(sphere n d k)
b : Fin n → ℕ
hb : b ∈ ↑(sphere n d k)
i : Fin n
hai : a i < d
⊢ (a + b) i < 2 * d - 1

Tactic:
have hbi := mem_box.1 (sphere_subset_box hb) i

Goal state after:
n d k : ℕ
a : Fin n → ℕ
ha : a ∈ ↑(sphere n d k)
b : Fin n → ℕ
hb : b ∈ ↑(sphere n d k)
i : Fin n
hai : a i < d
hbi : b i < d
⊢ (a + b) i < 2 * d - 1
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: k n✝¹ n✝ : ℕ
x : Fin (n✝¹ + 1) → ℕ
⊢ (∀ (i : Fin (n✝¹ + 1)), x i < n✝ + 1) →
    ∑ i, x i ^ 2 = k → x ∈ {x | ∀ (i : Fin (n✝¹ + 1)), x i < n✝ + 1 + (n✝ + 1) - 1}

Tactic:
exact fun h _ i => (h i).trans_le le_self_add

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

Goal state before:
pp: k m n : ℕ
hm : m ≠ 0
hkmn : m * k ≤ n
s t : Multiset (Fin (n + 1))
hsA : ∀ ⦃x : Fin (n + 1)⦄, x ∈ s → x ∈ Iic ↑k
htA : ∀ ⦃x : Fin (n + 1)⦄, x ∈ t → x ∈ Iic ↑k
hs : s.card = m
ht : t.card = m
⊢ (map val s).sum = (map val t).sum ↔ s.sum = t.sum

Tactic:
have (u : Multiset (Fin (n + 1))) : Nat.castRingHom _ (u.map val).sum = u.sum := by simp
    rw [← this, ← this]
    have {u : Multiset (Fin (n + 1))} (huk : ∀ x ∈ u, x ≤ k) (hu : card u = m) :
        (u.map val).sum < (n + 1) := Nat.lt_succ_iff.2 <| hkmn.trans' <| by
      rw [← hu, ← card_map]
      refine sum_le_card_nsmul (u.map val) k ?_
      simpa [le_iff_val_le_val, -val_fin_le, Nat.mod_eq_of_lt, aux hm hkmn] using huk
    exact ⟨congr_arg _, CharP.natCast_injOn_Iio _ (n + 1) (this hsA hs) (this htA ht)⟩

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

Goal state before:
pp: case succ.zero
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)
hm : 3 ≤ 0
ih :
  ∀ (ε : Fin 0 → ℤ),
    (∀ (i : Fin 0), |ε i| = 1) → ↑(#(List.map (fun i ↦ A ^ ε i) (finRange 0)).prod) ≤ k ^ (0 - 2) * ↑(#A)
ε : Fin (0 + 1) → ℤ
hε : ∀ (i : Fin (0 + 1)), |ε i| = 1
⊢ ↑(#(List.map (fun i ↦ A ^ ε i) (finRange (0 + 1))).prod) ≤ k ^ (0 + 1 - 2) * ↑(#A)

Tactic:
simp at hm

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
⊢ m ≠ 0

Tactic:
simp at hm

Goal state after:
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 : ℕ
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 : 2 ≤ m
⊢ m ≠ 0
Module: Mathlib.Combinatorics.Additive.CauchyDavenport

Goal state before:
pp: case inr.inr.inr.inr.inl
α : 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 : #(s ∩ op g • s) < #s
aux1 : #((mulETransformLeft g (s, t)).1 * (mulETransformLeft g (s, t)).2) ≤ #((s, t).1 * (s, t).2)
aux2 : #((mulETransformRight g (s, t)).1 * (mulETransformRight g (s, t)).2) ≤ #((s, t).1 * (s, t).2)
hgt : (t ∩ g⁻¹ • t).Nonempty
hstg : #(s, t).1 + #(s, t).2 ≤ #(mulETransformLeft g (s, t)).1 + #(mulETransformLeft g (s, t)).2
⊢ minOrder α ≤ ↑(#(s * t)) ∨ #s + #t ≤ #(s * t) + 1

pp: case inr.inr.inr.inr.inr
α : 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 : #(s ∩ op g • s) < #s
aux1 : #((mulETransformLeft g (s, t)).1 * (mulETransformLeft g (s, t)).2) ≤ #((s, t).1 * (s, t).2)
aux2 : #((mulETransformRight g (s, t)).1 * (mulETransformRight g (s, t)).2) ≤ #((s, t).1 * (s, t).2)
hgt : (t ∩ g⁻¹ • t).Nonempty
hstg : #(s, t).1 + #(s, t).2 < #(mulETransformRight g (s, t)).1 + #(mulETransformRight g (s, t)).2
⊢ minOrder α ≤ ↑(#(s * t)) ∨ #s + #t ≤ #(s * t) + 1

Tactic:
· exact (ih _ _ hgs (hgt.mono inter_subset_union) <| devosMulRel_of_le_of_le aux1 hstg hsg).imp
      (WithTop.coe_le_coe.2 aux1).trans' fun h ↦ hstg.trans <| h.trans <| add_le_add_left aux1 _

Goal state after:
case inr.inr.inr.inr.inr
α : 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 : #(s ∩ op g • s) < #s
aux1 : #((mulETransformLeft g (s, t)).1 * (mulETransformLeft g (s, t)).2) ≤ #((s, t).1 * (s, t).2)
aux2 : #((mulETransformRight g (s, t)).1 * (mulETransformRight g (s, t)).2) ≤ #((s, t).1 * (s, t).2)
hgt : (t ∩ g⁻¹ • t).Nonempty
hstg : #(s, t).1 + #(s, t).2 < #(mulETransformRight g (s, t)).1 + #(mulETransformRight g (s, t)).2
⊢ minOrder α ≤ ↑(#(s * t)) ∨ #s + #t ≤ #(s * t) + 1
Module: Mathlib.Combinatorics.Additive.SmallTripling

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

Tactic:
nlinarith

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

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

Tactic:
nlinarith

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : Lattice α
inst✝³ : OrderBot α
inst✝² : IsModularLattice α
inst✝¹ : DecidableEq α
ι : Type u_2
I : Finset ι
s : ι → α
P : (i : ι) → Finpartition (s i)
ha : I.SupIndep s
M : Type u_3
inst✝ : AddCommMonoid M
f : α → M
⊢ ∑ p ∈ (combine P ha).parts, f p = ∑ i ∈ I, ∑ p ∈ (P i).parts, f p

Tactic:
simp_rw [combine]

Goal state after:
α : Type u_1
inst✝⁴ : Lattice α
inst✝³ : OrderBot α
inst✝² : IsModularLattice α
inst✝¹ : DecidableEq α
ι : Type u_2
I : Finset ι
s : ι → α
P : (i : ι) → Finpartition (s i)
ha : I.SupIndep s
M : Type u_3
inst✝ : AddCommMonoid M
f : α → M
⊢ ∑ p ∈ I.biUnion fun i ↦ (P i).parts, f p = ∑ i ∈ I, ∑ p ∈ (P i).parts, f p
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝⁴ : Lattice α
inst✝³ : OrderBot α
inst✝² : IsModularLattice α
inst✝¹ : DecidableEq α
ι : Type u_2
I : Finset ι
s : ι → α
P : (i : ι) → Finpartition (s i)
ha : I.SupIndep s
M : Type u_3
inst✝ : AddCommMonoid M
f : α → M
⊢ ∑ p ∈ (combine P ha).parts, f p = ∑ i ∈ I, ∑ p ∈ (P i).parts, f p

Tactic:
by
  simp_rw [combine]
  refine Finset.sum_biUnion fun i hi j hj hij => ?_
  rw [Function.onFun, Finset.disjoint_left]
  intro p hpi hpj
  have hp_disj : Disjoint p p := (ha.pairwiseDisjoint hi hj hij).mono ((P i).le hpi) ((P j).le hpj)
  exact (P i).ne_bot hpi (disjoint_self.mp hp_disj)

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.IsLE X n
⊢ t.IsLE ((t.eTruncLT.obj ⊥).obj X) n

Tactic:
exact isLE_of_isZero _ (by simp) _

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

Goal state before:
pp: case mpr
α : 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 ∈ s → ∃ i_1 ∈ parts, i ∈ i_1

Tactic:
rintro hi
      exact (h' i hi).exists

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
inst✝¹ : IsTriangulated C
X : C
n : ℤ
inst✝ : t.IsLE X n
⊢ t.IsLE ((t.eTruncGE.obj ⊤).obj X) n

Tactic:
exact isLE_of_isZero _ (by simp) _

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

Goal state before:
pp: α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : Finpartition s
Q : Finpartition t
⊢ ∑ a ∈ P.parts, #(interedges r a t) = ∑ ab ∈ P.parts ×ˢ Q.parts, #(interedges r ab.1 ab.2)

Tactic:
sum_product

Goal state after:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
P : Finpartition s
Q : Finpartition t
⊢ ∑ a ∈ P.parts, #(interedges r a t) = ∑ x ∈ P.parts, ∑ y ∈ Q.parts, #(interedges r (x, y).1 (x, y).2)
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) * ε ≤ ↑(#(⋯.choose, ⋯.choose).2)

Tactic:
exact (not_isUniform_iff.1 h).choose_spec.2.choose_spec.2.2.1

Goal state after: