mathlib-initiative/mathlib-tactics huggingface dataset:
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₃
⊢ Triangle.mk (G.map T.mor₁) (G.map T.mor₂) (G.map T.mor₃ ≫ (Functor.commShiftIso G 1).hom.app T.obj₁) ∈
    distinguishedTriangles

Tactic:
assoc

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₃
⊢ Triangle.mk (G.map T.mor₁) (G.map T.mor₂) (G.map T.mor₃ ≫ (Functor.commShiftIso G 1).hom.app T.obj₁) ∈
    distinguishedTriangles
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 m : ℤ
h : n + m = 0
⊢ 𝟙 ((shiftFunctor Cᵒᵖ n ⋙ F.op).obj X) =
    (F.map ((shiftFunctorOpIso C n m h).hom.app X).unop).op ≫
      (((commShiftIso F m).inv.app (unop X)).op ≫ (shiftFunctorOpIso D n m h).inv.app (op (F.obj (unop X)))) ≫
        (shiftFunctorOpIso D n m h).hom.app (op (F.obj (unop X))) ≫
          ((commShiftIso F m).hom.app (unop X)).op ≫ (F.map ((shiftFunctorOpIso C n m h).inv.app X).unop).op

Tactic:
assoc

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 m : ℤ
h : n + m = 0
⊢ 𝟙 ((shiftFunctor Cᵒᵖ n ⋙ F.op).obj X) =
    (F.map ((shiftFunctorOpIso C n m h).hom.app X).unop).op ≫
      ((commShiftIso F m).inv.app (unop X)).op ≫
        (shiftFunctorOpIso D n m h).inv.app (op (F.obj (unop X))) ≫
          (shiftFunctorOpIso D n m h).hom.app (op (F.obj (unop X))) ≫
            ((commShiftIso F m).hom.app (unop X)).op ≫ (F.map ((shiftFunctorOpIso C n m h).inv.app X).unop).op
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Set α
a : α
hs : ThreeGPFree (a • s)
b : α
hb : b ∈ s
c : α
hc : c ∈ s
d : α
hd : d ∈ s
h : b * d = c * c
⊢ a • b * a • d = a * c * (a * c)

Tactic:
by
        rw [mul_mul_mul_comm, smul_eq_mul, smul_eq_mul, mul_mul_mul_comm, h]

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

Tactic:
simp_rw [cast_card] at ht ⊢

Goal state after:
α : 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 • b < ∑ x ∈ s, 1
⊢ ∃ y ∈ t, b < ∑ x ∈ s with f x = y, 1
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 ⊢

Goal state after:
α : 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 : ∑ x ∈ s, 1 < #t • b
⊢ ∃ y ∈ t, ∑ x ∈ s with f x = y, 1 < b
Module: Mathlib.Combinatorics.Additive.FreimanHom

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
f : α → β
n : ℕ
s t : Multiset α
hs : ∀ ⦃x : α⦄, x ∈ s → x ∈ ∅
ht : ∀ ⦃x : α⦄, x ∈ t → x ∈ ∅
⊢ s.card = n → t.card = n → ((map f s).prod = (map f t).prod ↔ s.prod = t.prod)

Tactic:
simp [eq_zero_of_forall_notMem hs, eq_zero_of_forall_notMem ht]

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

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

pp: ⊢ 0 < 1 - 2 / rexp 1

Tactic:
mul_sub,

Goal state after:
⊢ 2 ≤ 8 * 1 - 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
⊢ 0 < ↑N ^ (↑(nValue N))⁻¹ / 2

Tactic:
exact div_pos (rpow_pos_of_pos hN₀ _) zero_lt_two

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

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / rexp 1)) ≤ log ↑N / ↑⌈√(log ↑N)⌉₊

Tactic:
ceil_lt_mul

Goal state after:
N : ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / rexp 1)) ≤ log ↑N / (1.38 * √(log ↑N))

case hd
N : ℕ
hN : 4096 ≤ N
⊢ 0 < ↑⌈√(log ↑N)⌉₊

case hx
N : ℕ
hN : 4096 ≤ N
⊢ 50 / 19 ≤ √(log ↑N)
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

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

Tactic:
div_eq_mul_inv,

Goal state after:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
⊢ #(A * C) * #B ≤ #(A * B⁻¹) * #(B / C)
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

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

Tactic:
div_eq_mul_inv,

Goal state after:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : CommGroup G
A B C : Finset G
⊢ #(A * C⁻¹) * #B ≤ #(A * B) * #(B / C)
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
⊢ ↑(#(List.map (fun i ↦ A ^ ε i) (finRange (m + 1 + 1))).prod) ≤ k ^ (m + 1 + 1 - 2) * ↑(#A)

Tactic:
have hε₀ i : ε i ≠ 0 := fun h ↦ by simpa [h] using hε i

Goal state after:
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)
Module: Mathlib.Combinatorics.Additive.Convolution

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
x : G
⊢ A.convolution B x ≤ #A

Tactic:
rw [← inv_inv B, ← card_inter_smul]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
x : G
⊢ #(A ∩ x •> B⁻¹) ≤ #A
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
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
⊢ IsCorner (Prod.map f f '' A) (f x₁) (f y₁) (f x₂) (f y₂) ↔ IsCorner A x₁ y₁ x₂ y₂

Tactic:
have hf' := hf.bijOn.injOn.prodMap hf.bijOn.injOn

Goal state after:
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)
⊢ IsCorner (Prod.map f f '' A) (f x₁) (f y₁) (f x₂) (f y₂) ↔ IsCorner A x₁ y₁ x₂ y₂
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
⊢ ↑(#(List.map (fun i ↦ A ^ ε i) (finRange m)).prod) ≤ K ^ (3 * (m - 2)) * ↑(#A)

Tactic:
have hε₀ i : ε i ≠ 0 := fun h ↦ by simpa [h] using hε i

Goal state after:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
⊢ ↑(#(List.map (fun i ↦ A ^ ε i) (finRange m)).prod) ≤ K ^ (3 * (m - 2)) * ↑(#A)
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
f : V ↪ W
v : V
⊢ (SimpleGraph.map (⇑f) G).neighborSet (f v) = ⇑f '' G.neighborSet v

Tactic:
refine Set.ext fun u ↦ ⟨?_, ?_⟩
  · exact fun ⟨hne, v', u', hadj, hv, hu⟩ ↦ ⟨u', f.injective hv ▸ hadj, hu⟩
  · exact fun ⟨u', hadj, hu⟩ ↦ ⟨hu ▸ f.injective.ne hadj.ne, v, u', hadj, rfl, hu⟩

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
⊢ ∑ v ∈ G.support.toFinset, G.degree v = 2 * #G.edgeFinset

Tactic:
simp_rw [← sum_degrees_eq_twice_card_edges,
    ← sum_add_sum_compl G.support.toFinset, left_eq_add]
  apply Finset.sum_eq_zero
  intro v hv
  rw [degree_eq_zero_iff_notMem_support]
  rwa [mem_compl, Set.mem_toFinset] at hv

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsCompleteBetween s t
u : Set V
⊢ (SimpleGraph.induce u G).IsCompleteBetween (u ↓∩ s) (u ↓∩ t)

Tactic:
intro _ hs _ ht
  rw [comap_adj, Embedding.coe_subtype]
  exact h hs ht

Goal state after:
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:
by
  simp only [Finset.ext_iff, mem_insert, mem_neighborFinset, IsUniversal]
  grind

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

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
β : Type u_2
inst✝¹ : Lattice β
inst✝ : OrderBot β
a : α
e : α ≃o β
P : Finpartition a
u : Finset β
hu : u ⊆ Finset.map (↑e).toEmbedding P.parts
x✝¹ : β
hb : x✝¹ ∈ Finset.map (↑e).toEmbedding P.parts
hbu : x✝¹ ∉ u
x✝ : β
hx : x✝ ≤ id x✝¹
hxu : x✝ ≤ u.sup id
⊢ x✝ ≤ ⊥

Tactic:
by
    rw [← map_symm_subset] at hu
    simp only [mem_map_equiv] at hb
    have := P.supIndep hu hb (by simp [hbu]) (map_rel e.symm hx) ?_
    · rw [← e.symm.map_bot] at this
      exact e.symm.map_rel_iff.mp this
    · convert! e.symm.map_rel_iff.mpr hxu
      rw [map_finset_sup, sup_map]
      rfl

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

Goal state before:
pp: α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
⊢ ((P.parts ×ˢ Q.parts).sup fun bc ↦ bc.1 ⊓ bc.2) = a

Tactic:
sup_product_left

Goal state after:
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P Q : Finpartition a
⊢ (P.parts.sup fun i ↦ Q.parts.sup fun i' ↦ (i, i').1 ⊓ (i, i').2) = a
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
n : ℤ
i : EInt
h : WithBotTop.coe n ≤ i
X : C
⊢ t.IsGE ((t.eTruncGE.obj i).obj X) n

Tactic:
induction i using WithBotTop.rec with
  | bot => simp at h
  | coe i =>
    dsimp
    exact t.isGE_of_ge _ _ _ (by simpa using h)
  | top => exact t.isGE_of_isZero (Functor.zero_obj _) _

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

Goal state before:
pp: case inr
ι : Type u_2
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 < ↑(#s)
htcard : 0 < ↑(#t)
h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)) ^ 2
⊢ d + ↑(#s) / ↑(#t) * x ^ 2 ≤ (∑ i ∈ t, f i ^ 2) / ↑(#t)

Tactic:
have h₂ : x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / #t)) / #s) ^ 2 := by
    apply h₁.trans
    rw [sum_sub_distrib, sum_const, nsmul_eq_mul, sub_div, mul_div_cancel_left₀ _ hscard.ne']

Goal state after:
case inr
ι : Type u_2
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 < ↑(#s)
htcard : 0 < ↑(#t)
h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)) ^ 2
h₂ : x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / ↑(#t))) / ↑(#s)) ^ 2
⊢ d + ↑(#s) / ↑(#t) * x ^ 2 ≤ (∑ i ∈ t, f i ^ 2) / ↑(#t)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ ∑ UV ∈ P.sparsePairs G ε, ε * (↑(#UV.1) * ↑(#UV.2)) ≤ ∑ UV ∈ P.parts.offDiag, ε * (↑(#UV.1) * ↑(#UV.2))

Tactic:
gcongr; apply filter_subset

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
⊢ #({x ∈ P.parts.attach | #↑x = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)}) * ?m.162 +
      #({x ∈ P.parts.attach | ¬#↑x = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)}) * ?m.168 =
    stepBound #P.parts

Tactic:
exact fun x hx => card_parts_equitabilise _ _ (Nat.div_pos hPα' hPpos).ne'

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
⊢ #({x ∈ P.parts.attach | #↑x = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)}) * ?m.162 +
      #({x ∈ P.parts.attach | ¬#↑x = m * 4 ^ #P.parts + (Fintype.card α / #P.parts - m * 4 ^ #P.parts)}) * ?m.168 =
    stepBound #P.parts
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
⊢ ∀ x ∈ univ, #(equitabilise ⋯).parts = ?m.168

Tactic:
exact fun x hx => card_parts_equitabilise _ _ (Nat.div_pos hPα' hPpos).ne'

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
⊢ ∀ x ∈ univ, #(equitabilise ⋯).parts = ?m.162

Tactic:
exact fun x hx => card_parts_equitabilise _ _ (Nat.div_pos hPα' hPpos).ne'

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

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

Tactic:
← sum_biUnion pairwiseDisjoint_distinctPairs

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

Goal state before:
pp: ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
ι✝ : Type u
κ✝ : ι✝ → Type u
f : (a : ι✝) → κ✝ a → G.Subgraph
⊢ (⨅ a, ⨆ b, f a b).verts = (⨆ g, ⨅ a, f a (g a)).verts

Tactic:
by simpa using! iInf_iSup_eq

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

Goal state before:
pp: case left
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H₁ H₂ : G.Subgraph
hH : H₁ ≤ H₂
v : V
hv : v ∈ H₁.verts
⊢ ∃ x ∈ H₂.verts, f x = f v

Tactic:
exact ⟨_, hH.1 hv, rfl⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    {B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion fun B ↦
      B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
B : Finset α
⊢ B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts → #(B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id) ≤ m

Tactic:
hB

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
h₂ : ¬G.IsUniform ε U V
hX : G.nonuniformWitness ε U V ∈ P.nonuniformWitnesses G ε U
q :
  G.nonuniformWitness ε U V \ (star hP G ε hU V).biUnion id ⊆
    {B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts | B ⊆ G.nonuniformWitness ε U V ∧ B.Nonempty}.biUnion fun B ↦
      B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id
B : Finset α
hB : B ∈ (atomise U (P.nonuniformWitnesses G ε U)).parts
⊢ #(B \ {A ∈ (chunk hP G ε hU).parts | A ⊆ B}.biUnion id) ≤ m
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
inst✝ : Fintype V
G : SimpleGraph V
⊢ G.copyCount ⊥ = 1

Tactic:
by
  classical
  rw [copyCount]
  convert!
    card_singleton (α := G.Subgraph)
      { verts := .univ
        Adj := ⊥
        adj_sub := False.elim
        edge_vert := False.elim }
  simp only [eq_singleton_iff_unique_mem, mem_filter_univ, Nonempty.forall]
  refine ⟨⟨⟨(Equiv.Set.univ _).symm, by simp⟩⟩, fun H' e ↦
    Subgraph.ext ((set_fintype_card_eq_univ_iff _).1 <| Fintype.card_congr e.toEquiv.symm) ?_⟩
  ext a b
  simp only [Prop.bot_eq_false, Pi.bot_apply, iff_false]
  exact fun hab ↦ e.symm.map_rel_iff.2 hab.coe

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

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
⊢ G.killCopies H ≤ G

Tactic:
rw [killCopies]

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
⊢ (if hH : H = ⊥ then G else G.deleteEdges (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})) ≤ G
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
⊢ G.killCopies ⊥ = G

Tactic:
rw [killCopies]

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
⊢ (if hH : ⊥ = ⊥ then G else G.deleteEdges (⋃ G', ⋃ (hG' : Nonempty (⊥ ≃g G'.coe)), {⋯.some})) = G
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
W : Type u_2
H : SimpleGraph W
hH : H ≠ ⊥
G : SimpleGraph V
⊢ G.killCopies H = G.deleteEdges (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})

Tactic:
rw [killCopies]

Goal state after:
V : Type u_1
W : Type u_2
H : SimpleGraph W
hH : H ≠ ⊥
G : SimpleGraph V
⊢ (if hH : H = ⊥ then G else G.deleteEdges (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})) =
    G.deleteEdges (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 V)
⊢ (G'.deleteEdges s).coe ≤ G'.coe

Tactic:
intro v w
  simp +contextual

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this : 2 ^ #P.parts * ↑m / (↑(#U) * ε) ≤ ε / 10
⊢ ↑(#(G.nonuniformWitness ε U V)) - 2 ^ #P.parts * ↑m / (↑(#U) * ε) * ↑(#(G.nonuniformWitness ε U V)) ≤
    ↑(#(G.nonuniformWitness ε U V)) - 2 ^ (#P.parts - 1) * ↑m

Tactic:
refine sub_le_sub_left ?_ _
      have : (2 : ℝ) ^ #P.parts = ↑2 ^ (#P.parts - 1) * 2 := by
        rw [← _root_.pow_succ, tsub_add_cancel_of_le (succ_le_iff.2 hP₁)]
      rw [← mul_div_right_comm, this, mul_right_comm _ (2 : ℝ), mul_assoc, le_div_iff₀]
      · gcongr _ * ?_
        exact (G.le_card_nonuniformWitness hunif).trans
          (le_mul_of_one_le_left (cast_nonneg _) one_le_two)
      have := Finset.card_pos.mpr (P.nonempty_of_mem_parts hU)
      sz_positivity

Goal state after: