mathlib-initiative/mathlib-tactics huggingface dataset:
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
P : ObjectProperty J.Point
inst✝³ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
inst✝² : J.WEqualsLocallyBijective (Type w)
inst✝¹ : HasSheafify J (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
inst✝ : HasSheafify (J.over X) (Type w)
Y : C
f : Y ⟶ X
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ (Over.mk f).left
hS :
  ∀ (Φ : (ofObj fun ψ ↦ ψ.fst.obj.over ψ.snd).FullSubcategory) (x : Φ.obj.fiber.obj (Over.mk f)),
    ∃ Y_1 g_1,
      ∃ (_ : ((Sieve.overEquiv (Over.mk f)).symm (Sieve.ofArrows Z g)).arrows g_1),
        ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g_1)) y = x
⊢ Sieve.ofArrows Z g ∈ J (Over.mk f).left

Tactic:
rw [hP.jointly_reflect_ofArrows_mem_of_small]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
J : GrothendieckTopology C
inst✝⁴ : LocallySmall.{w, v, u} C
P : ObjectProperty J.Point
inst✝³ : ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)} P
inst✝² : J.WEqualsLocallyBijective (Type w)
inst✝¹ : HasSheafify J (Type w)
hP : P.IsConservativeFamilyOfPoints
X : C
inst✝ : HasSheafify (J.over X) (Type w)
Y : C
f : Y ⟶ X
ι : Type (max u v)
Z : ι → C
g : (i : ι) → Z i ⟶ (Over.mk f).left
hS :
  ∀ (Φ : (ofObj fun ψ ↦ ψ.fst.obj.over ψ.snd).FullSubcategory) (x : Φ.obj.fiber.obj (Over.mk f)),
    ∃ Y_1 g_1,
      ∃ (_ : ((Sieve.overEquiv (Over.mk f)).symm (Sieve.ofArrows Z g)).arrows g_1),
        ∃ y, (ConcreteCategory.hom (Φ.obj.fiber.map g_1)) y = x
⊢ ∀ (Φ : P.FullSubcategory) (x : Φ.obj.fiber.obj (Over.mk f).left),
    ∃ i y, (ConcreteCategory.hom (Φ.obj.fiber.map (g i))) y = x
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'
S : Set (SubmonoidFunctor M)
U✝ V✝ : C
f : U✝ ⟶ V✝
⊢ ⨅ F ∈ S, F.obj U✝ ≤ Submonoid.comap (MonCat.Hom.hom (M.map f)) (⨅ F ∈ S, F.obj V✝)

Tactic:
rw [(Submonoid.gc_map_comap (M.map f).hom).u_iInf₂]
        exact iInf₂_mono fun F _ ↦ F.map f

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasPullbacks C
Ω : C
h : SubobjectRepresentableBy Ω
X : C
f : X ⟶ Ω
⊢ h.homEquiv f = (Subobject.pullback f).obj h.Ω₀

Tactic:
by
  simpa using! h.homEquiv_comp f (𝟙 _)

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Classifier.Defs

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasPullbacks C
h : HasSubobjectClassifier C
⊢ (Subobject.presheaf C).IsRepresentable

pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasPullbacks C
h : (Subobject.presheaf C).IsRepresentable
⊢ HasSubobjectClassifier C

Tactic:
· obtain ⟨⟨𝒞⟩⟩ := h
    apply RepresentableBy.isRepresentable
    exact 𝒞.representableBy

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasPullbacks C
h : (Subobject.presheaf C).IsRepresentable
⊢ HasSubobjectClassifier C
Module: Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject

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
inst✝ : IsTriangulated C
X : C
D D' : ComposableArrows EInt 2
φ : D ⟶ D'
⊢ (functorArrows EInt 1 2 2 SpectralObject._proof_2 SpectralObject._proof_4 ⋙ t.ω₁ ⋙ (evaluation C C).obj X).map φ ≫
      (t.ω₁δ (D'.obj 0) (D'.obj 1) (D'.obj 2) ⋯ ⋯).app X =
    (t.ω₁δ (D.obj 0) (D.obj 1) (D.obj 2) ⋯ ⋯).app X ≫
      (functorArrows EInt 0 1 2 SpectralObject._proof_6 SpectralObject._proof_2 ⋙
            (t.ω₁ ⋙ (evaluation C C).obj X) ⋙ shiftFunctor C 1).map
        φ

Tactic:
obtain ⟨a, b, c, f, g, rfl⟩ := mk₂_surjective D

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
inst✝ : IsTriangulated C
X : C
D' : ComposableArrows EInt 2
a b c : EInt
f : a ⟶ b
g : b ⟶ c
φ : mk₂ f g ⟶ D'
⊢ (functorArrows EInt 1 2 2 SpectralObject._proof_2 SpectralObject._proof_4 ⋙ t.ω₁ ⋙ (evaluation C C).obj X).map φ ≫
      (t.ω₁δ (D'.obj 0) (D'.obj 1) (D'.obj 2) ⋯ ⋯).app X =
    (t.ω₁δ ((mk₂ f g).obj 0) ((mk₂ f g).obj 1) ((mk₂ f g).obj 2) ⋯ ⋯).app X ≫
      (functorArrows EInt 0 1 2 SpectralObject._proof_6 SpectralObject._proof_2 ⋙
            (t.ω₁ ⋙ (evaluation C C).obj X) ⋙ shiftFunctor C 1).map
        φ
Module: Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject

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
inst✝ : IsTriangulated C
X : C
D : ComposableArrows EInt 2
⊢ Triangle.mk
      ((t.ω₁ ⋙ (evaluation C C).obj X).map
        ((mapFunctorArrows EInt 0 1 0 2 2 SpectralObject._proof_6 SpectralObject._proof_8 SpectralObject._proof_10
              SpectralObject._proof_2 SpectralObject._proof_4).app
          D))
      ((t.ω₁ ⋙ (evaluation C C).obj X).map
        ((mapFunctorArrows EInt 0 2 1 2 2 SpectralObject._proof_8 SpectralObject._proof_2 SpectralObject._proof_6
              SpectralObject._proof_4 SpectralObject._proof_4).app
          D))
      ({ app := fun D ↦ (t.ω₁δ (D.obj 0) (D.obj 1) (D.obj 2) ⋯ ⋯).app X, naturality := ⋯ }.app D) ∈
    distinguishedTriangles

Tactic:
obtain ⟨a, b, c, f, g, rfl⟩ := mk₂_surjective D

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
inst✝ : IsTriangulated C
X : C
a b c : EInt
f : a ⟶ b
g : b ⟶ c
⊢ Triangle.mk
      ((t.ω₁ ⋙ (evaluation C C).obj X).map
        ((mapFunctorArrows EInt 0 1 0 2 2 SpectralObject._proof_6 SpectralObject._proof_8 SpectralObject._proof_10
              SpectralObject._proof_2 SpectralObject._proof_4).app
          (mk₂ f g)))
      ((t.ω₁ ⋙ (evaluation C C).obj X).map
        ((mapFunctorArrows EInt 0 2 1 2 2 SpectralObject._proof_8 SpectralObject._proof_2 SpectralObject._proof_6
              SpectralObject._proof_4 SpectralObject._proof_4).app
          (mk₂ f g)))
      ({ app := fun D ↦ (t.ω₁δ (D.obj 0) (D.obj 1) (D.obj 2) ⋯ ⋯).app X, naturality := ⋯ }.app (mk₂ f g)) ∈
    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
⊢ (fun s ↦ Nat.findGreatest (fun m ↦ ∃ t ⊆ s, #t = m ∧ ThreeGPFree ↑t) #s) t ≤
    (fun s ↦ Nat.findGreatest (fun m ↦ ∃ t ⊆ s, #t = m ∧ ThreeGPFree ↑t) #s) u

Tactic:
refine Nat.findGreatest_mono (fun m => ?_) (card_le_card htu)

Goal state after:
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 : ℕ
⊢ (∃ t_1 ⊆ t, #t_1 = m ∧ ThreeGPFree ↑t_1) → ∃ t ⊆ u, #t = m ∧ ThreeGPFree ↑t
Module: Mathlib.Combinatorics.Additive.FreimanHom

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
hf : IsMulFreimanHom 2 A B f
a b c d : α
ha : a ∈ A
hb : b ∈ A
hc : c ∈ A
hd : d ∈ A
h : a * b = c * d
⊢ f a * f b = f c * f d

Tactic:
simp_rw [← prod_pair] at h ⊢
  refine hf.map_prod_eq_map_prod ?_ ?_ (card_pair _ _) (card_pair _ _) h <;> simp [ha, hb, hc, hd]

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

Goal state before:
pp: n d k : ℕ
⊢ ThreeAPFree ↑(image (⇑(map (2 * d - 1))) (sphere n d k))

Tactic:
rw [coe_image]
  apply ThreeAPFree.image' (α := Fin n → ℕ) (β := ℕ) (s := sphere n d k) (map (2 * d - 1))
    (map_injOn.mono _) threeAPFree_sphere
  rw [Set.add_subset_iff]
  rintro a ha b hb i
  have hai := mem_box.1 (sphere_subset_box ha) i
  have hbi := mem_box.1 (sphere_subset_box hb) i
  rw [lt_tsub_iff_right, ← succ_le_iff, two_mul]
  exact (add_add_add_comm _ _ 1 1).trans_le (_root_.add_le_add hai hbi)

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

Goal state before:
pp: k n✝¹ n✝ : ℕ
⊢ ∀ x ∈ image (⇑(map (2 * (n✝ + 1) - 1))) (sphere (n✝¹ + 1) (n✝ + 1) k), x < (2 * (n✝ + 1) - 1) ^ (n✝¹ + 1)

Tactic:
simp only [mem_image, and_imp, forall_exists_index,
      sphere, mem_filter]

Goal state after:
k n✝¹ n✝ : ℕ
⊢ ∀ (x : ℕ),
    ∀ x_1 ∈ box (n✝¹ + 1) (n✝ + 1),
      ∑ i, x_1 i ^ 2 = k → (map (2 * (n✝ + 1) - 1)) x_1 = x → x < (2 * (n✝ + 1) - 1) ^ (n✝¹ + 1)
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 _)]

Goal state after:
⊢ 8 * 2 ≤ (8 - 2) * rexp 1

⊢ 0 < 1 - 2 / rexp 1
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ √(log ↑N) + 1 ≤ √(log ↑N) + √(log ↑N)

Tactic:
add_le_add_iff_left

Goal state after:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ 1 ≤ √(log ↑N)
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

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

Tactic:
simpa [div_eq_mul_inv] using ruzsa_triangle_inequality_mul_div_mul A B C

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

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

Tactic:
union_mul,

Goal state after:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
⊢ (C * A ∪ {x} * A) * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
Module: Mathlib.Combinatorics.Additive.ApproximateSubgroup

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
K : ℝ
inst✝ : DecidableEq G
A : Finset G
hA : IsApproximateSubgroup K ↑A
n : ℕ
F : Finset G
hF : ↑(#F) ≤ K
hSF : ↑A ^ 2 ⊆ ↑F • ↑A
⊢ ↑(#(A ^ (n + 2))) ≤ K ^ (n + 2 - 1) * ↑(#A)

Tactic:
calc
      (#(A ^ (n + 2)) : ℝ) ≤ #(F ^ (n + 1) * A) := by
        gcongr; exact mod_cast Set.pow_subset_pow_mul_of_sq_subset_mul hSF (by lia)
      _ ≤ #(F ^ (n + 1)) * #A := mod_cast Finset.card_mul_le
      _ ≤ #F ^ (n + 1) * #A := by gcongr; exact mod_cast Finset.card_pow_le
      _ ≤ K ^ (n + 1) * #A := by gcongr

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

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
A : Set G
K : ℝ
F : Type u_2
H : Type u_3
inst✝² : Group H
inst✝¹ : FunLike F G H
inst✝ : MonoidHomClass F G H
f : F
hA : IsApproximateSubgroup K A
⊢ CovBySMul H K ((⇑f '' A) ^ 2) (⇑f '' A)

Tactic:
classical
    obtain ⟨F, hF, hAF⟩ := hA.sq_covBySMul
    refine ⟨F.image f, ?_, ?_⟩
    · calc
        (#(F.image f) : ℝ) ≤ #F := mod_cast F.card_image_le
        _ ≤ K := hF
    · simp only [← Set.image_pow, Finset.coe_image, ← Set.image_mul, smul_eq_mul] at hAF ⊢
      gcongr

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

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

Tactic:
union_mul,

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ #(mulETransformLeft e x).1 + #(mulETransformRight e x).1 +
      (#(mulETransformLeft e x).2 + #(mulETransformRight e x).2) =
    #x.1 + #x.2 + (#x.1 + #x.2)

Tactic:
mulETransformLeft.card,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ 2 * #x.1 + (#(mulETransformLeft e x).2 + #(mulETransformRight e x).2) = #x.1 + #x.2 + (#x.1 + #x.2)
Module: Mathlib.Combinatorics.SimpleGraph.Dart

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ ∀ {d : G.Dart} {u v : V}, d.edge = s(u, v) ↔ d.toProd = (u, v) ∨ d.toProd = (v, u)

Tactic:
by
  rintro ⟨p, h⟩ _ _
  simp

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Defs

Goal state before:
pp: case e'_1
G : Type u_1
H : Type u_2
inst✝¹ : AddCommMonoid G
inst✝ : AddCommMonoid H
A : Set (G × G)
s : Set G
t : Set H
f : G → H
x₁ y₁ x₂ y₂ : G
hf : IsAddFreimanIso 2 s t f
hAs : A ⊆ s ×ˢ s
hx₁ : x₁ ∈ s
hy₁ : y₁ ∈ s
hx₂ : x₂ ∈ s
hy₂ : y₂ ∈ s
hf' : InjOn (fun x ↦ (f x.1, f x.2)) (s ×ˢ s)
⊢ (f x₁, f y₁) ∈ Prod.map f f '' A ↔ (x₁, y₁) ∈ A

Tactic:
exact hf'.mem_image_iff hAs (mk_mem_prod hx₁ hy₁)

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Defs

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : AddCommMonoid G
inst✝ : AddCommMonoid H
A : Set (G × G)
s : Set G
t : Set H
f : G → H
hf : IsAddFreimanIso 2 s t f
hAs : A ⊆ s ×ˢ s
this : Prod.map f f '' A ⊆ t ×ˢ t
⊢ (∀ ⦃x₁ : H⦄,
      x₁ ∈ t →
        ∀ ⦃y₁ : H⦄,
          y₁ ∈ t → ∀ ⦃x₂ : H⦄, x₂ ∈ t → ∀ ⦃y₂ : H⦄, y₂ ∈ t → IsCorner (Prod.map f f '' A) x₁ y₁ x₂ y₂ → x₁ = x₂) ↔
    ∀ ⦃x₁ : G⦄, x₁ ∈ s → ∀ ⦃y₁ : G⦄, y₁ ∈ s → ∀ ⦃x₂ : G⦄, x₂ ∈ s → ∀ ⦃y₂ : G⦄, y₂ ∈ s → IsCorner A x₁ y₁ x₂ y₂ → x₁ = x₂

Tactic:
simp +contextual only [hf.bijOn.forall, isCorner_image hf hAs, hf.bijOn.injOn.eq_iff]

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 : ↑(#{x | ¬↑(G.degree x) = 0}) = 0
⊢ Even #{v | Odd (G.degree v)}

Tactic:
← ZMod.natCast_eq_zero_iff_even

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ↑(#{x | ¬↑(G.degree x) = 0}) = 0
⊢ ↑(#{v | Odd (G.degree v)}) = 0
Module: Mathlib.Data.Finset.Pairwise

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
l : List α
inst✝ : Std.Symm r
hn : l.Nodup
⊢ {a | a ∈ l}.Pairwise r ↔ Pairwise r l

Tactic:
hn.pairwise_coe

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
r : α → α → Prop
l : List α
inst✝ : Std.Symm r
hn : l.Nodup
⊢ Pairwise r l ↔ Pairwise r l
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
| #P.parts - #s % #P.parts

Tactic:
arg 1
    rw [← card_filter_add_card_filter_not (p := fun p ↦ #p = #s / #P.parts + 1)]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
| #({p ∈ P.parts | #p = #s / #P.parts + 1}) + #({a ∈ P.parts | ¬#a = #s / #P.parts + 1})
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ : Finpartition a
s : α
P : Finpartition s
Pr : α → Prop
Prsup : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊔ t)
Prinf : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊓ t)
Prbot : Pr ⊥
hs : Pr s
hP : ∀ p ∈ P.parts, Pr p
this✝ : Lattice (Subtype Pr) := Subtype.lattice Prsup Prinf
this : OrderBot (Subtype Pr) := Subtype.orderBot Prbot
t : Finset (Subtype Pr)
ht : t ⊆ P.parts.preimage Subtype.val ⋯
i : Subtype Pr
hi : i ∈ P.parts.preimage Subtype.val ⋯
hi' : i ∉ t
⊢ Disjoint (id i) (t.sup id)

Tactic:
by
      classical
      have : (fun (i : Subtype Pr) => (id i).val) = id ∘ Subtype.val := rfl
      rw [disjoint_subtype_iff Prinf Prbot, sup_coe, this, ← sup_image t Subtype.val id]
      · apply P.supIndep
        · simpa [image_subset_iff_subset_preimage] using ht
        · simpa using hi
        · simpa [i.property] using hi'
      exact Prsup

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
j : ℤ
hj : WithBotTop.coe j ≤ WithBotTop.coe n
⊢ IsZero ((t.eTruncLT.obj (WithBotTop.coe j)).obj X)

Tactic:
| coe j =>

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.IsLE X n
j : ℤ
hj : WithBotTop.coe n < WithBotTop.coe j
⊢ IsZero ((t.eTruncGE.obj (WithBotTop.coe j)).obj X)

Tactic:
| coe j =>

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

Goal state before:
pp: ε : ℝ
hε : 0 < ε
l : ℕ
⊢ log (100 / ε ^ 5) / log 4 < max (↑7) (max ↑l ↑(⌊log (100 / ε ^ 5) / log 4⌋₊ + 1))

Tactic:
push_cast
    exact lt_max_of_lt_right (lt_max_of_lt_right <| Nat.lt_floor_add_one _)

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
⊢ ∀ ⦃x : Finset α⦄,
    x ∈ (atomise s F).parts → x ⊆ t → x.Nonempty → ∃ a ⊆ F.erase t, {i ∈ s | ∀ x ∈ F, x ∈ insert t a ↔ i ∈ x} = x

Tactic:
Finset.Nonempty,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
⊢ ∀ ⦃x : Finset α⦄,
    x ∈ (atomise s F).parts → x ⊆ t → (∃ x_1, x_1 ∈ x) → ∃ a ⊆ F.erase t, {i ∈ s | ∀ x ∈ F, x ∈ insert t a ↔ i ∈ x} = x
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
⊢ ∀ ⦃x : Finset α⦄,
    x.Nonempty →
      (∃ Q ⊆ F, {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u} = x) →
        x ⊆ t → ∀ x_1 ∈ x, ∃ a ⊆ F.erase t, {i ∈ s | ∀ x ∈ F, x ∈ insert t a ↔ i ∈ x} = x

Tactic:
Finset.Nonempty,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
F : Finset (Finset α)
ht : t ∈ F
⊢ ∀ ⦃x : Finset α⦄,
    (∃ x_1, x_1 ∈ x) →
      (∃ Q ⊆ F, {i ∈ s | ∀ u ∈ F, u ∈ Q ↔ i ∈ u} = x) →
        x ⊆ t → ∀ x_1 ∈ x, ∃ a ⊆ F.erase t, {i ∈ s | ∀ x ∈ F, x ∈ insert t a ↔ i ∈ x} = x
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Goal state before:
pp: case inl
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : ℕ
P : Finpartition s
hs : a * 0 + b * (0 + 1) = #s
⊢ ∃ Q,
    (∀ x ∈ Q.parts, #x = 0 ∨ #x = 0 + 1) ∧
      (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ 0) ∧ #({i ∈ Q.parts | #i = 0 + 1}) = b

pp: case inr
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
m_pos : m > 0
⊢ ∃ Q,
    (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
      (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b

Tactic:
· refine ⟨⊥, by simp, ?_, by simpa [Finset.filter_true_of_mem] using hs.symm⟩
    simp only [le_zero_iff, card_eq_zero, mem_biUnion, mem_filter, id,
      and_assoc, sdiff_eq_empty_iff_subset, subset_iff]
    exact fun x hx a ha =>
      ⟨{a}, mem_map_of_mem _ (P.le hx ha), singleton_subset_iff.2 ha, mem_singleton_self _⟩

Goal state after:
case inr
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
hs : a * m + b * (m + 1) = #s
m_pos : m > 0
⊢ ∃ Q,
    (∀ x ∈ Q.parts, #x = m ∨ #x = m + 1) ∧
      (∀ x ∈ P.parts, #(x \ {y ∈ Q.parts | y ⊆ x}.biUnion id) ≤ m) ∧ #({i ∈ Q.parts | #i = m + 1}) = b
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 β
⊢ edgeDensity r s t ≤ 1

Tactic:
apply div_le_one_of_le₀
  · exact mod_cast card_interedges_le_mul r s t
  · exact mod_cast Nat.zero_le _

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

Goal state before:
pp: case inr.inr
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h₁ : s ≠ t
h₂ : ¬G.IsUniform ε s t
gt : WellOrderingRel t s
⊢ ε ≤ ↑|G.edgeDensity (G.nonuniformWitnesses ε t s).1 (G.nonuniformWitnesses ε t s).2 - G.edgeDensity t s|

Tactic:
apply G.nonuniformWitnesses_spec fun i => h₂ i.symm

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hPα' : stepBound #P.parts ≤ Fintype.card α
hPpos : 0 < stepBound #P.parts
⊢ #(P.bind fun x ↦ chunk hP G ε).parts = stepBound #P.parts

Tactic:
card_bind

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ¬P.IsUniform G ε
hPα' : stepBound #P.parts ≤ Fintype.card α
hPpos : 0 < stepBound #P.parts
⊢ ∑ A ∈ P.parts.attach, #(chunk hP G ε ⋯).parts = stepBound #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
⊢ ↑(P.energy G) + ε ^ 5 / 4 =
    (∑ x ∈ P.parts.offDiag, ↑(G.edgeDensity x.1 x.2) ^ 2 + ↑(#P.parts) ^ 2 * (ε ^ 5 / 4)) / ↑(#P.parts) ^ 2

Tactic:
coe_energy,

Goal state after:
α : 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
⊢ (∑ uv ∈ P.parts.offDiag, ↑(G.edgeDensity uv.1 uv.2) ^ 2) / ↑(#P.parts) ^ 2 + ε ^ 5 / 4 =
    (∑ x ∈ P.parts.offDiag, ↑(G.edgeDensity x.1 x.2) ^ 2 + ↑(#P.parts) ^ 2 * (ε ^ 5 / 4)) / ↑(#P.parts) ^ 2