mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Presentable.Type

Goal state before:
pp: X : Type u
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
⊢ IsCardinalPresentable X κ ↔ HasCardinalLT X κ

Tactic:
refine ⟨fun _ ↦ ?_, fun hX ↦ hX.isCardinalPresentable⟩
  have := preservesColimitsOfShape_of_isCardinalPresentable X κ
  obtain ⟨⟨A, hA⟩, f, hf⟩ := Types.jointly_surjective_of_isColimit
    (isColimitOfPreserves (coyoneda.obj (op X))
      (HasCardinalLT.Set.isColimitCocone X κ
        (Cardinal.IsRegular.aleph0_le Fact.out))) (𝟙 X)
  obtain rfl : A = .univ := by
    ext x
    have := congr_hom hf x
    dsimp at this
    rw [← this]
    simp
  exact (hasCardinalLT_iff_of_equiv (Equiv.Set.univ X) _).1 hA

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

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
sq : (i j : ι) → ChosenPullback (f i) (f j)
sq₃ : (i₁ i₂ i₃ : ι) → ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)
D₁ D₂ : F.DescentData' sq sq₃
e : (i : ι) → D₁.obj i ≅ D₂.obj i
comm :
  ∀ (i₁ i₂ : ι),
    (F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.map (e i₁).hom ≫ D₂.hom i₁ i₂ =
      D₁.hom i₁ i₂ ≫ (F.map (sq i₁ i₂).p₂.op.toLoc).toFunctor.map (e i₂).hom
i₁ i₂ : ι
⊢ (F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.map (e i₁).inv ≫ D₁.hom i₁ i₂ =
    D₂.hom i₁ i₂ ≫ (F.map (sq i₁ i₂).p₂.op.toLoc).toFunctor.map (e i₂).inv

Tactic:
rw [← cancel_mono ((F.map _).toFunctor.map (e i₂).hom), Category.assoc,
      Category.assoc, Iso.map_inv_hom_id, Category.comp_id,
      ← cancel_epi ((F.map _).toFunctor.map (e i₁).hom),
      Iso.map_hom_inv_id_assoc, comm i₁ i₂]

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

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

Tactic:
rw [← h g hg]

Goal state after:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
A : Type u'
inst✝ : Category.{v', u'} A
F G : Cᵒᵖ ⥤ A
X : C
S : Sieve X
x : Presieve.FamilyOfElements (presheafHom F G) S.arrows
hx : x.Compatible
y : (presheafHom F G).obj (op X)
h : x.IsAmalgamation y
Y : C
g : Y ⟶ X
hg : S.arrows g
⊢ y.app (op (Over.mk g)) = ((ConcreteCategory.hom ((presheafHom F G).map g.op)) y).app (op (Over.mk (𝟙 Y)))
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
γ₁ γ₂ : OneCochain G U
α : ZeroCochain G U
h : OneCohomologyRelation γ₁ γ₂ α
i j : I
T : C
a : T ⟶ U i
b : T ⟶ U j
⊢ (ConcreteCategory.hom (G.map a.op)) (α⁻¹ i) * (γ₂.ev i j a b * (ConcreteCategory.hom (G.map b.op)) (α j)) =
    γ₁.ev i j a b * (ConcreteCategory.hom (G.map b.op)) (α⁻¹ j) * (ConcreteCategory.hom (G.map b.op)) (α j)

Tactic:
← h i j a b,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
G : Cᵒᵖ ⥤ GrpCat
I : Type w'
U : I → C
γ₁ γ₂ : OneCochain G U
α : ZeroCochain G U
h : OneCohomologyRelation γ₁ γ₂ α
i j : I
T : C
a : T ⟶ U i
b : T ⟶ U j
⊢ (ConcreteCategory.hom (G.map a.op)) (α⁻¹ i) * ((ConcreteCategory.hom (G.map a.op)) (α i) * γ₁.ev i j a b) =
    γ₁.ev i j a b * (ConcreteCategory.hom (G.map b.op)) (α⁻¹ j) * (ConcreteCategory.hom (G.map b.op)) (α j)
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)
inst✝ : J.HasEnoughPoints
⊢ J.W.IsMonoidal

Tactic:
obtain ⟨P, _, hP⟩ := HasEnoughPoints.exists_objectProperty J

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)
inst✝ : J.HasEnoughPoints
P : ObjectProperty J.Point
left✝ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
hP : P.IsConservativeFamilyOfPoints
⊢ J.W.IsMonoidal
Module: Mathlib.CategoryTheory.Sites.Point.Over

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
inst✝⁴ : LocallySmall.{w, v, u} C
Φ : J.Point
X✝ : C
x : Φ.fiber.obj X✝
inst✝³ : J.HasEnoughPoints
inst✝² : J.WEqualsLocallyBijective (Type w)
inst✝¹ : HasSheafify J (Type w)
X : C
inst✝ : HasSheafify (J.over X) (Type w)
⊢ (J.over X).HasEnoughPoints

Tactic:
obtain ⟨P, _, hP⟩ := HasEnoughPoints.exists_objectProperty J

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
inst✝⁴ : LocallySmall.{w, v, u} C
Φ : J.Point
X✝ : C
x : Φ.fiber.obj X✝
inst✝³ : J.HasEnoughPoints
inst✝² : J.WEqualsLocallyBijective (Type w)
inst✝¹ : HasSheafify J (Type w)
X : C
inst✝ : HasSheafify (J.over X) (Type w)
P : ObjectProperty J.Point
left✝ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
hP : P.IsConservativeFamilyOfPoints
⊢ (J.over X).HasEnoughPoints
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 : Cᵒᵖ
n : ℤ
⊢ (F.map ((shiftFunctorOpIso C n (-n) ⋯).hom.app (op ((shiftFunctor C n).obj (unop X)))).unop).op ≫
      ((commShiftIso F (-n)).inv.app ((shiftFunctor C n).obj (unop X))).op ≫
        ((shiftFunctor D (-n)).map ((commShiftIso F n).inv.app (unop X))).op ≫
          ((shiftFunctorCompIsoId D n (-n) ⋯).inv.app (F.obj (unop X))).op =
    (F.map ((shiftFunctorOpIso C n (-n) ⋯).hom.app (op ((shiftFunctor C n).obj (unop X)))).unop).op ≫
      ((commShiftIso F (-n)).inv.app (unop (op ((shiftFunctor C n).obj (unop X))))).op ≫
        (shiftFunctorOpIso D n (-n) ⋯).inv.app (op (F.obj (unop (op ((shiftFunctor C n).obj (unop X)))))) ≫
          (shiftFunctorOpIso D n (-n) ⋯).hom.app (op (F.obj ((shiftFunctor C n).obj (unop X)))) ≫
            (shiftFunctor D (-n)).op.map ((commShiftIso F n).inv.app (unop X)).op ≫
              ((shiftFunctorCompIsoId D n (-n) ⋯).inv.app (F.obj (unop X))).op

Tactic:
op_map,

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✝² : HasShift C ℤ
inst✝¹ : HasShift D ℤ
F : C ⥤ D
inst✝ : F.CommShift ℤ
X : Cᵒᵖ
n : ℤ
⊢ (F.map ((shiftFunctorOpIso C n (-n) ⋯).hom.app (op ((shiftFunctor C n).obj (unop X)))).unop).op ≫
      ((commShiftIso F (-n)).inv.app ((shiftFunctor C n).obj (unop X))).op ≫
        ((shiftFunctor D (-n)).map ((commShiftIso F n).inv.app (unop X))).op ≫
          ((shiftFunctorCompIsoId D n (-n) ⋯).inv.app (F.obj (unop X))).op =
    (F.map ((shiftFunctorOpIso C n (-n) ⋯).hom.app (op ((shiftFunctor C n).obj (unop X)))).unop).op ≫
      ((commShiftIso F (-n)).inv.app (unop (op ((shiftFunctor C n).obj (unop X))))).op ≫
        (shiftFunctorOpIso D n (-n) ⋯).inv.app (op (F.obj (unop (op ((shiftFunctor C n).obj (unop X)))))) ≫
          (shiftFunctorOpIso D n (-n) ⋯).hom.app (op (F.obj ((shiftFunctor C n).obj (unop X)))) ≫
            ((shiftFunctor D (-n)).map ((commShiftIso F n).inv.app (unop X)).op.unop).op ≫
              ((shiftFunctorCompIsoId D n (-n) ⋯).inv.app (F.obj (unop X))).op
Module: Mathlib.CategoryTheory.UnivLE

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

Tactic:
exact ⟨a', ⟨(Iso.toEquiv m').symm.trans Equiv.ulift⟩⟩

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₁ i δ, Triangle.mk (ι.map i) (ι.map π) δ ∈ distinguishedTriangles

Tactic:
obtain ⟨X₁, f₂, f₃, hT⟩ := distinguished_cocone_triangle (ι.map π)

Goal state after:
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
⊢ ∃ X₁ i δ, Triangle.mk (ι.map i) (ι.map π) δ ∈ distinguishedTriangles
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✝ t u : Finset α
htu : t ⊆ u
m : ℕ
v : Finset α
hvt : v ⊆ t
hv : #v = m ∧ ThreeGPFree ↑v
⊢ ∃ t ⊆ u, #t = m ∧ ThreeGPFree ↑t

Tactic:
exact ⟨v, hvt.trans htu, hv⟩

Goal state after:
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 : ↑(#s) < #t • b
⊢ ∃ y ∈ t, ↑(#({x ∈ s | f x = y})) < b

Tactic:
simp_rw [cast_card] at ht ⊢
  exact
    exists_sum_fiber_lt_of_sum_fiber_nonneg_of_sum_lt_nsmul
      (fun _ _ => sum_nonneg fun _ _ => zero_le_one) ht

Goal state after:
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
hf : ∀ a ∈ s, f a ∈ t
ht : t.Nonempty
hb : #t • b ≤ ↑(#s)
⊢ ∃ y ∈ t, b ≤ ↑(#({x ∈ s | f x = y}))

Tactic:
by
  simp_rw [cast_card] at hb ⊢
  exact exists_le_sum_fiber_of_maps_to_of_nsmul_le_sum hf ht hb

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

Goal state before:
pp: n d : ℕ
x₁ x₂ : Fin n.succ → ℕ
hx₁ : ∀ (i : Fin n.succ), x₁ i < d
hx₂ : ∀ (i : Fin n.succ), x₂ i < d
h : (map d) x₁ = (map d) x₂
⊢ x₁ 0 % d = x₂ 0

Tactic:
← map_mod,

Goal state after:
n d : ℕ
x₁ x₂ : Fin n.succ → ℕ
hx₁ : ∀ (i : Fin n.succ), x₁ i < d
hx₂ : ∀ (i : Fin n.succ), x₂ i < d
h : (map d) x₁ = (map d) x₂
⊢ (map d) x₁ % d = x₂ 0
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: n d : ℕ
x₁ x₂ : Fin n.succ → ℕ
hx₁ : ∀ (i : Fin n.succ), x₁ i < d
hx₂ : ∀ (i : Fin n.succ), x₂ i < d
h : (map d) x₁ = (map d) x₂
⊢ (map d) x₁ % d = x₂ 0 % d

Tactic:
← map_mod,

Goal state after:
n d : ℕ
x₁ x₂ : Fin n.succ → ℕ
hx₁ : ∀ (i : Fin n.succ), x₁ i < d
hx₂ : ∀ (i : Fin n.succ), x₂ i < d
h : (map d) x₁ = (map d) x₂
⊢ (map d) x₁ % d = (map d) x₂ % d
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: n d k : ℕ
f : (Fin n → ℕ) →+ EuclideanSpace ℝ (Fin n) := { toFun := fun f ↦ toLp 2 (Nat.cast ∘ f), map_zero' := ⋯, map_add' := ⋯ }
x : Fin n → ℕ
⊢ x ∈ ↑(sphere n d k) → x ∈ ⇑f ⁻¹' Metric.sphere 0 √↑k

Tactic:
rw [Set.mem_preimage, mem_sphere_zero_iff_norm]

Goal state after:
n d k : ℕ
f : (Fin n → ℕ) →+ EuclideanSpace ℝ (Fin n) := { toFun := fun f ↦ toLp 2 (Nat.cast ∘ f), map_zero' := ⋯, map_add' := ⋯ }
x : Fin n → ℕ
⊢ x ∈ ↑(sphere n d k) → ‖f x‖ = √↑k
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: ⊢ 2 / (1 - 2 / rexp 1) ≤ 8

Tactic:
rw [div_le_iff₀, mul_sub, mul_one, mul_div_assoc', le_sub_comm, div_le_iff₀ (exp_pos _)]
  · linarith [exp_one_gt_d9]
  rw [sub_pos, div_lt_one] <;> exact exp_one_gt_d9.trans' (by norm_num)

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

Goal state before:
pp: case pos
G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A B : Finset G
hB : B.Nonempty
hK : ↑(#(A * B)) ≤ K * ↑(#B)
this : (F : Set G) → Decidable (F.PairwiseDisjoint fun x ↦ x • B)
C : Finset (Finset G) := {F ∈ A.powerset | (↑F).PairwiseDisjoint fun x ↦ x • B}
F : Finset G
hFmax : Maximal (fun x ↦ x ⊆ A ∧ (↑x).PairwiseDisjoint fun x ↦ x • B) F
hFA : F ⊆ A
hF : (↑F).PairwiseDisjoint fun x ↦ x • B
a : G
ha : a ∈ A
hau : a ∉ F
H : ∀ b ∈ F, Disjoint (a • B) (b • B)
⊢ a ∈ F * (B / B)

Tactic:
refine (hFmax.not_gt ?_ <| ssubset_insert hau).elim
    rw [insert_subset_iff, coe_insert]
    exact ⟨⟨ha, hFA⟩, hF.insert fun _ hb _ ↦ H _ hb⟩

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

Goal state before:
pp: case hd
N : ℕ
hN : 4096 ≤ N
⊢ 1 < N

Tactic:
exact hN.trans_lt' (by norm_num1)

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

Goal state before:
pp: case hx
N : ℕ
hN : 4096 ≤ N
⊢ 0 < N

Tactic:
exact hN.trans_lt' (by norm_num1)

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

Goal state before:
pp: case h₁
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ 1 < N

Tactic:
exact hN.trans_lt' (by norm_num1)

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

Goal state before:
pp: case h₂
N : ℕ
hN : 4096 ≤ N
n : ℕ := nValue N
hn : 0 < ↑n
hd : 0 < dValue N
hN₀ : 0 < ↑N
hn₂ : 2 < n
this✝ : (2 * dValue N - 1) ^ n ≤ N
this : rexp (-4 * √(log ↑N)) = rexp (-2 * √(log ↑N)) * rexp (-2 * √(log ↑N))
⊢ 1 < N

Tactic:
exact hN.trans_lt' (by norm_num1)

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
hA : A.Nonempty
n : ℕ
ih : ↑(#(A * B ^ n)) ≤ (↑(#(A * B)) / ↑(#A)) ^ n * ↑(#A)
⊢ ↑(#(A * B ^ (n + 1))) * ↑(#A) = ↑(#(B ^ n * A * B)) * ↑(#A)

Tactic:
pow_succ,

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)
⊢ ↑(#(A * (B ^ n * B))) * ↑(#A) = ↑(#(B ^ n * A * B)) * ↑(#A)
Module: Mathlib.Combinatorics.Additive.ETransform

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ e • (mulDysonETransform e x).2 ⊆ (mulDysonETransform e x).1

Tactic:
dsimp
  rw [smul_finset_inter, smul_inv_smul, inter_comm]
  exact inter_subset_union

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

Goal state before:
pp: V : Type u_1
W : Type u_2
X : Type u_3
Y : Type u_4
G✝ : SimpleGraph V
G' : SimpleGraph W
u v : V
f : V → W
G : SimpleGraph V
a b : W
⊢ (Ne ⊓ Relation.Map G.Adj f f) a b → (Ne ⊓ Relation.Map G.Adj f f) b a

Tactic:
by aesop (add norm unfold Relation.Map) (add forward safe Adj.symm)

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
h : ∑ _v with ↑(G.degree _v) ≠ 0, 1 = 0
⊢ Even #{v | Odd (G.degree v)}

pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ∑ x with ↑(G.degree x) ≠ 0, ↑(G.degree x) = 0
⊢ ∀ x ∈ {x | ↑(G.degree x) ≠ 0}, ↑(G.degree x) = 1

Tactic:
· simp only [mul_one, nsmul_eq_mul, sum_const, Ne] at h
    rw [← ZMod.natCast_eq_zero_iff_even]
    convert! h
    exact ZMod.natCast_ne_zero_iff_odd.symm

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ∑ x with ↑(G.degree x) ≠ 0, ↑(G.degree x) = 0
⊢ ∀ x ∈ {x | ↑(G.degree x) ≠ 0}, ↑(G.degree x) = 1
Module: Mathlib.Data.Finset.Pairwise

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
r : α → α → Prop
l : List α
hl : (↑l.toFinset).Pairwise r
hn : l.Nodup
⊢ Pairwise r l

Tactic:
coe_toFinset

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
r : α → α → Prop
l : List α
hl : {a | a ∈ l}.Pairwise r
hn : l.Nodup
⊢ Pairwise r l
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: case pos
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ ↑s, b ≤ f a ∧ f a ≤ b + 1
h : ∀ a ∈ s, f a = b + 1
a : α
ha : a ∈ s
⊢ (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1

Tactic:
rw [h _ ha, sum_const_nat h, Nat.mul_div_cancel_left _ (card_pos.2 ⟨a, ha⟩)]

Goal state after:
case pos
α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ ↑s, b ≤ f a ∧ f a ≤ b + 1
h : ∀ a ∈ s, f a = b + 1
a : α
ha : a ∈ s
⊢ b + 1 ≤ b + 1 ∧ b + 1 ≤ b + 1 + 1
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
P✝ : Finpartition a
inst✝ : Decidable (a = ⊥)
P : Finpartition a
⊢ P ≤ if ha : a = ⊥ then (Finpartition.empty α).copy ⋯ else indiscrete ha

Tactic:
by
    split_ifs with h
    · intro x hx
      simpa [h, P.ne_bot hx] using P.le hx
    · exact fun b hb ↦ ⟨a, mem_singleton_self _, P.le hb⟩

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
es : ↥({p ∈ P.parts | #p = #s / #P.parts}) ≃ Fin #({p ∈ P.parts | #p = #s / #P.parts}) :=
  {p ∈ P.parts | #p = #s / #P.parts}.equivFin
el : { x // x ∈ P.parts ∧ #x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
⊢ ∃ f, ∀ (t : ↥P.parts), #↑t = #s / #P.parts + 1 ↔ ↑(f t) < #s % #P.parts

Tactic:
simp_rw [mem_filter, hP.card_small_parts_eq_mod] at es

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
el : { x // x ∈ P.parts ∧ #x = #s / #P.parts + 1 } ≃ Fin (#s % #P.parts)
es : { x // x ∈ P.parts ∧ #x = #s / #P.parts } ≃ Fin (#P.parts - #s % #P.parts)
⊢ ∃ f, ∀ (t : ↥P.parts), #↑t = #s / #P.parts + 1 ↔ ↑(f t) < #s % #P.parts
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
a b : EInt
hab : a ⟶ b
⊢ t.eTruncGE.map hab ≫ WithBotTop.rec 0 t.truncGEδLT 0 b =
    WithBotTop.rec 0 t.truncGEδLT 0 a ≫ (t.eTruncLT ⋙ (Functor.whiskeringRight C C C).obj (shiftFunctor C 1)).map hab

Tactic:
replace hab := leOfHom hab
    induction a using WithBotTop.rec; rotate_right
    · apply (isZero_zero _).eq_of_src
    all_goals
      induction b using WithBotTop.rec <;> simp at hab <;>
        dsimp [eTruncGE, eTruncLT] <;>
        simp [t.truncGEδLT_comp_whiskerRight_natTransTruncLTOfLE]

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
i j : EInt
f : i ⟶ j
X : C
⊢ (t.eTruncLT.obj i).map ((t.eTruncLT.map (homOfLE ⋯)).app X) ≫ (t.eTruncLT.map f).app X =
    (t.eTruncLT.map (homOfLE ⋯)).app ((t.eTruncLT.obj j).obj X)

Tactic:
show homOfLE le_top = f ≫ homOfLE le_top by rfl

Goal state after:
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
i j : EInt
f : i ⟶ j
X : C
⊢ (t.eTruncLT.obj i).map ((t.eTruncLT.map (homOfLE ⋯)).app X) ≫ (t.eTruncLT.map f).app X =
    (t.eTruncLT.map (f ≫ homOfLE ⋯)).app ((t.eTruncLT.obj j).obj X)
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case mpr
α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a b : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
⊢ (∃ A, ∃ (hA : A ∈ P.parts), b ∈ (Q A hA).parts) → ∃ a_2 ∈ P.parts.attach, b ∈ (Q ↑a_2 ⋯).parts

Tactic:
rintro ⟨A, hA, h⟩
    exact ⟨⟨A, hA⟩, mem_attach _ ⟨A, hA⟩, h⟩

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a : α
h : a ∉ s
⊢ P.part a = ∅

Tactic:
simp [part, h]

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a b : α
⊢ (∃ p ∈ P.parts, a ∈ p ∧ b ∈ p) → a ∈ P.part b

Tactic:
rintro ⟨p, hp, hap, hbp⟩

Goal state after:
case mpr
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a b : α
p : Finset α
hp : p ∈ P.parts
hap : a ∈ p
hbp : b ∈ p
⊢ a ∈ P.part b
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 α
a b : α
s t : Finset α
h : G.IsUniform ε s t
t' : Finset α
ht' : t' ⊆ t
s' : Finset α
hs' : s' ⊆ s
ht : ↑(#t) * ε ≤ ↑(#t')
hs : ↑(#s) * ε ≤ ↑(#s')
⊢ |↑(G.edgeDensity s' t') - ↑(G.edgeDensity t s)| < ε

Tactic:
edgeDensity_comm _ t

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s✝ t✝ : Finset α
a b : α
s t : Finset α
h : G.IsUniform ε s t
t' : Finset α
ht' : t' ⊆ t
s' : Finset α
hs' : s' ⊆ s
ht : ↑(#t) * ε ≤ ↑(#t')
hs : ↑(#s) * ε ≤ ↑(#s')
⊢ |↑(G.edgeDensity s' t') - ↑(G.edgeDensity s 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 s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : ↑(#s) * 1 ≤ ↑(#s')
ht : ↑(#t) * 1 ≤ ↑(#t')
⊢ |↑(G.edgeDensity s' t') - ↑(G.edgeDensity s t)| < 1

Tactic:
rw [mul_one] at hs ht

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