mathlib-initiative/mathlib-tactics huggingface dataset:
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
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
B : A
k : B ⟶ K
hk : (ι ⋙ shiftFunctor C 1).map (k ≫ ιK f₃ α) = (ι ⋙ shiftFunctor C 1).map 0
⊢ (ι ⋙ shiftFunctor C 1).map k = (ι ⋙ shiftFunctor C 1).map 0

Tactic:
simp only [Functor.comp_map, Functor.map_comp,
    shift_ι_map_ιK, Functor.map_zero, ← assoc] at hk ⊢

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
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
B : A
k : B ⟶ K
hk : ((shiftFunctor C 1).map (ι.map k) ≫ α) ≫ f₃ = 0
⊢ (shiftFunctor C 1).map (ι.map k) = 0
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
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
B : A
k : B ⟶ K
hk : ((shiftFunctor C 1).map (ι.map k) ≫ α) ≫ f₃ = 0
l : (shiftFunctor C 1).obj (ι.obj B) ⟶ (Triangle.mk (ι.map f₁) f₂ f₃).obj₂
hl : (shiftFunctor C 1).map (ι.map k) ≫ α = 0
m : (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj B)) ⟶ (Triangle.mk α β γ).obj₃
hm : (shiftFunctor C 1).map ((shiftFunctor C 1).map (ι.map k)) = m ≫ (Triangle.mk α β γ).mor₃
⊢ m = 0

Tactic:
rw [← cancel_epi ((shiftFunctorAdd' C (1 : ℤ) 1 2 (by lia)).hom.app _), comp_zero]
    exact eq_zero_of_hom_shift_pos hι _ (by lia)

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
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
B : A
k : Q ⟶ B
hk : f₂ ≫ β ≫ ι.map k = 0
l : (shiftFunctor C 1).obj (Triangle.mk (ι.map f₁) f₂ f₃).obj₁ ⟶ ι.obj B
hl : β ≫ ι.map k = 0
m : (shiftFunctor C 1).obj (Triangle.mk α β γ).obj₁ ⟶ ι.obj B
hm : ι.map k = (Triangle.mk α β γ).mor₃ ≫ m
⊢ m = 0

Tactic:
rw [← cancel_epi ((shiftFunctorAdd' C (1 : ℤ) 1 2 (by lia)).hom.app _), comp_zero]
    exact eq_zero_of_hom_shift_pos hι _ (by lia)

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
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
B : A
k : Q ⟶ B
hk : f₂ ≫ β ≫ ι.map k = 0
l : (shiftFunctor C 1).obj (Triangle.mk (ι.map f₁) f₂ f₃).obj₁ ⟶ ι.obj B
hl : β ≫ ι.map k = 0
hm : ι.map k = (Triangle.mk α β γ).mor₃ ≫ 0
⊢ k = 0

Tactic:
exact ι.map_injective (by rw [hm, comp_zero, ι.map_zero])

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
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
B : A
x₂ : X₂ ⟶ B
hx₂ : f₁ ≫ x₂ = 0
x₁ : (Triangle.mk (ι.map f₁) f₂ f₃).obj₃ ⟶ ι.obj B
hx₁ : ι.map x₂ = (Triangle.mk (ι.map f₁) f₂ f₃).mor₂ ≫ x₁
⊢ ∃ k, πQ f₂ β ≫ k = x₂

Tactic:
obtain ⟨k, hk⟩ := Triangle.yoneda_exact₂ _ hT' x₁
    (eq_zero_of_hom_shift_pos hι _ (by lia))

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
X₁ X₂ : A
f₁ : X₁ ⟶ X₂
X₃ : C
f₂ : ι.obj X₂ ⟶ X₃
f₃ : X₃ ⟶ (shiftFunctor C 1).obj (ι.obj X₁)
hT : Triangle.mk (ι.map f₁) f₂ f₃ ∈ distinguishedTriangles
K Q : A
α : (shiftFunctor C 1).obj (ι.obj K) ⟶ X₃
β : X₃ ⟶ ι.obj Q
γ : ι.obj Q ⟶ (shiftFunctor C 1).obj ((shiftFunctor C 1).obj (ι.obj K))
hT' : Triangle.mk α β γ ∈ distinguishedTriangles
inst✝² : ι.Full
inst✝¹ : Preadditive A
inst✝ : ι.Faithful
B : A
x₂ : X₂ ⟶ B
hx₂ : f₁ ≫ x₂ = 0
x₁ : (Triangle.mk (ι.map f₁) f₂ f₃).obj₃ ⟶ ι.obj B
hx₁ : ι.map x₂ = (Triangle.mk (ι.map f₁) f₂ f₃).mor₂ ≫ x₁
k : (Triangle.mk α β γ).obj₃ ⟶ ι.obj B
hk : x₁ = (Triangle.mk α β γ).mor₂ ≫ k
⊢ ∃ k, πQ f₂ β ≫ k = x₂
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:
sum_const

Goal state after:
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 = #s • m
Module: Mathlib.Combinatorics.Additive.AP.Three.Defs

Goal state before:
pp: case inl
a b : ℕ
h : b ≤ a
⊢ addRothNumber (Ico a b) = rothNumberNat (b - a)

pp: case inr
a b : ℕ
h : a ≤ b
⊢ addRothNumber (Ico a b) = rothNumberNat (b - a)

Tactic:
· rw [Nat.sub_eq_zero_of_le h, Ico_eq_empty_of_le h, rothNumberNat_zero, addRothNumber_empty]

Goal state after:
case inr
a b : ℕ
h : a ≤ b
⊢ addRothNumber (Ico a b) = rothNumberNat (b - a)
Module: Mathlib.Combinatorics.Additive.FreimanHom

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
h : BijOn f A B
⊢ ∀ ⦃s t : Multiset α⦄,
    (∀ ⦃x : α⦄, x ∈ s → x ∈ A) →
      (∀ ⦃x : α⦄, x ∈ t → x ∈ A) → s.card = 1 → t.card = 1 → ((map f s).prod = (map f t).prod ↔ s.prod = t.prod)

Tactic:
by aesop (add simp [card_eq_one, BijOn])

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

Goal state before:
pp: N : ℕ
hN : 4096 ≤ N
⊢ log (2 / (1 - 2 / rexp 1)) * (69 / 50) ≤ √(log ↑N)

Tactic:
calc
    _ ≤ log (2 ^ 3) * (69 / 50) := by
      gcongr
      · field_simp
        simp (disch := positivity) [exp_one_gt_two]
      · norm_num1
        exact two_div_one_sub_two_div_e_le_eight
    _ ≤ √(log (2 ^ 12)) := by
      simp only [Real.log_pow, Nat.cast_ofNat]
      apply le_sqrt_of_sq_le
      nlinarith [log_two_lt_d9, log_two_gt_d9]
    _ ≤ √(log ↑N) := by
      gcongr
      exact mod_cast hN

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 / ↑(nValue N)

pp: case hx
N : ℕ
hN : 4096 ≤ N
⊢ 0 < ↑N

pp: case h
N : ℕ
hN : 4096 ≤ N
⊢ 0 < 2 / (1 - 2 / rexp 1)

pp: case h₁
N : ℕ
hN : 4096 ≤ N
⊢ 0 < ↑N ^ (↑(nValue N))⁻¹

Tactic:
nValue

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

case hx
N : ℕ
hN : 4096 ≤ N
⊢ 0 < ↑N

case h
N : ℕ
hN : 4096 ≤ N
⊢ 0 < 2 / (1 - 2 / rexp 1)

case h₁
N : ℕ
hN : 4096 ≤ N
⊢ 0 < ↑N ^ (↑(nValue N))⁻¹
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:
by
  dsimp
  rw [smul_finset_inter, smul_inv_smul, inter_comm]
  exact inter_subset_union

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 : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
⊢ ↑(#(A * A⁻¹ * A)) ≤ K ^ 3 * ↑(#A)

Tactic:
by
  obtain rfl | hA₀ := A.eq_empty_or_nonempty
  · simp
  refine le_of_mul_le_mul_left ?_ (by positivity : (0 : ℝ) < #A)
  calc
    (#A * #(A * A⁻¹ * A) : ℝ) ≤ #(A * (A * A⁻¹)) * #(A * A) := by
      norm_cast; simpa using ruzsa_triangle_inequality_invMul_mul_mul (A * A⁻¹) A A
    _ = #(A * A * A⁻¹) * #(A ^ 2) := by simp [pow_succ, mul_assoc]
    _ ≤ (K ^ 2 * #A) * (K * #A) := by
      gcongr
      · exact small_pos_pos_neg_mul hA
      calc
        (#(A ^ 2) : ℝ) ≤ #(A ^ 3) := mod_cast hA₀.card_pow_mono (by simp)
        _ ≤ K * #A := hA
    _ = #A * (K ^ 3 * #A) := by ring

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
inst✝ : DecidableEq V
v : V
d : G.Dart
⊢ d ∈ {d | d.toProd.1 = v} ↔ d ∈ image (G.dartOfNeighborSet v) univ

Tactic:
simp only [mem_image, true_and, mem_filter, SetCoe.exists, mem_univ]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v : V
d : G.Dart
⊢ d.toProd.1 = v ↔ ∃ x, ∃ (h : x ∈ G.neighborSet v), G.dartOfNeighborSet v ⟨x, h⟩ = d
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
s : Set V
h : (induce s G).spanningCoe = G
v : V
hv : v ∈ Subtype.val '' (induce s G).support
u : ↑s
left✝ : u ∈ (induce s G).support
hvu : ↑u = v
⊢ v ∈ s

Tactic:
exact hvu ▸ u.prop

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

Goal state before:
pp: V : Type u_1
inst✝¹ : Fintype V
inst✝ : DecidableEq V
⊢ ⊤.edgeFinset = Sym2.diagSetᶜ.toFinset

Tactic:
simp [← coe_inj]

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

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
s : Finset V
h : #(induce (↑s) G).edgeFinset = #(G.edgeFinset ∩ (↑s).toFinset.sym2)
⊢ #({e ∈ G.edgeFinset | e.toFinset ⊆ s}) = #(induce (↑s) G).edgeFinset

Tactic:
toFinset_coe

Goal state after:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
s : Finset V
h : #(induce (↑s) G).edgeFinset = #(G.edgeFinset ∩ s.sym2)
⊢ #({e ∈ G.edgeFinset | e.toFinset ⊆ s}) = #(induce (↑s) G).edgeFinset
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
hP : P.IsEquipartition
f : ↥s ≃ (t : ↥P.parts) × Fin #↑t
hf : ∀ (a b : ↥s), P.part ↑a = P.part ↑b ↔ (f a).fst = (f b).fst
g : ↥P.parts ≃ Fin #P.parts
hg : ∀ (t : ↥P.parts), #↑t = #s / #P.parts + 1 ↔ ↑(g t) < #s % #P.parts
z : ↥s → ℕ := fun a ↦ #P.parts * ↑(f a).snd + ↑(g (f a).fst)
gl : ∀ (a : ↥s), ↑(g (f a).fst) < #P.parts
less : ∀ (a : ↥s), z a < #s
z' : ↥s → Fin #s := fun a ↦ ⟨z a, ⋯⟩
a b : ↥s
this : NeZero #P.parts
e : (f a).snd.1 = (f b).snd.1 ∧ (f a).fst = (f b).fst
⊢ f a = f b

Tactic:
exact Sigma.ext e.2 <| (Fin.heq_ext_iff (by rw [e.2])).mpr e.1

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 β
⊢ 0 ≤ edgeDensity r s t

Tactic:
apply div_nonneg <;> exact mod_cast Nat.zero_le _

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

Goal state before:
pp: case a
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
hst : ↑(#s₂) * ↑(#t₂) ≠ 0
⊢ interedges r s₂ t₂ ⊆ interedges r s₁ t₁

Tactic:
exact interedges_mono hs ht

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

Goal state before:
pp: case refine_2.refine_2
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hs₂ : s₂.Nonempty
ht₂ : t₂.Nonempty
⊢ 0 ≤ ↑(#t₂) / ↑(#t₁)

Tactic:
apply div_nonneg <;> exact mod_cast Nat.zero_le _

Goal state after:
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
hP : P.IsEquipartition
h : P.parts.Nonempty
U : Finset α
hU : U ∈ P.parts
this : #U * #U - #U ≤ #A / #P.parts * (#A / #P.parts + 1)
⊢ #U.offDiag ≤ #A / #P.parts * (#A / #P.parts + 1)

Tactic:
← offDiag_card

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts.Nonempty
U : Finset α
hU : U ∈ P.parts
this : #U.offDiag ≤ #A / #P.parts * (#A / #P.parts + 1)
⊢ #U.offDiag ≤ #A / #P.parts * (#A / #P.parts + 1)
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 ε
⊢ #(increment hP G ε).parts = stepBound #P.parts

Tactic:
have hPα' : stepBound #P.parts ≤ card α := by grw [← hPα, stepBound]; gcongr; simp
  have hPpos : 0 < stepBound #P.parts := stepBound_pos (nonempty_of_not_uniform hPG).card_pos
  rw [increment, card_bind]
  simp_rw [chunk, apply_dite Finpartition.parts, apply_dite card, sum_dite]
  rw [sum_const_nat, sum_const_nat, univ_eq_attach, univ_eq_attach, card_attach, card_attach]
  any_goals exact fun x hx => card_parts_equitabilise _ _ (Nat.div_pos hPα' hPpos).ne'
  rw [Nat.sub_add_cancel a_add_one_le_four_pow_parts_card,
    Nat.sub_add_cancel ((Nat.le_succ _).trans a_add_one_le_four_pow_parts_card), ← add_mul]
  congr
  rw [card_filter_add_card_filter_not, card_attach]

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.parts * #P.parts - #P.parts) * ε < ↑(#(P.nonUniforms G ε))
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ ∑ x ∈ P.parts.offDiag, ↑(G.edgeDensity x.1 x.2) ^ 2 + ↑(#P.parts) ^ 2 * (ε ^ 5 / 4) ≤
    ∑ x ∈ P.parts.offDiag.attach, (∑ i ∈ distinctPairs hP G ε x, ↑(G.edgeDensity i.1 i.2) ^ 2) / 16 ^ #P.parts

Tactic:
← offDiag_card

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.parts.offDiag) * ε < ↑(#(P.nonUniforms G ε))
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ ∑ x ∈ P.parts.offDiag, ↑(G.edgeDensity x.1 x.2) ^ 2 + ↑(#P.parts) ^ 2 * (ε ^ 5 / 4) ≤
    ∑ x ∈ P.parts.offDiag.attach, (∑ i ∈ distinctPairs hP G ε x, ↑(G.edgeDensity i.1 i.2) ^ 2) / 16 ^ #P.parts
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
x : V
⊢ ∀ x_1 ∈ G.edgeFinset, x_1 ∉ G.incidenceFinset x ↔ x ∉ x_1

Tactic:
intro _ h

Goal state after:
V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
x : V
x✝ : Sym2 V
h : x✝ ∈ G.edgeFinset
⊢ x✝ ∉ G.incidenceFinset x ↔ x ∉ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
m a b : ℕ
P : Finpartition s
h : a * m + b * (m + 1) = #s
hm : m ≠ 0
⊢ #(equitabilise h).parts = a + b

Tactic:
by
  rw [← filter_true_of_mem fun x => card_eq_of_mem_parts_equitabilise, filter_or,
    card_union_of_disjoint, P.card_filter_equitabilise_small _ hm, P.card_filter_equitabilise_big]
  aesop (add norm disjoint_filter)

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
p' : G.Walk v w
⊢ ↑(p.append p').support = {u} + ↑p.support.tail + ↑p'.support.tail

Tactic:
rw [support_append, ← Multiset.coe_add, coe_support]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks

Goal state before:
pp: case succ.cons.zero
V : Type u_1
G : SimpleGraph V
u v : V
n k : ℕ
v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
h : n ≤ 0
ih : ((cons h✝ p✝).take n).IsSubwalk ((cons h✝ p✝).take 0)
⊢ ((cons h✝ p✝).take 0).IsSubwalk ((cons h✝ p✝).take (0 + 1))

Tactic:
exact isSubwalk_of_append_left rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : t.Nontrivial
s : Set α
hs : G.IsClique s
hst : ⇑f '' s = ↑t
⊢ (⇑f '' s).Finite

Tactic:
simp [hst]

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
⊢ (∃ s, G.IsNClique 3 s) ↔ ∃ u w, w.IsCycle ∧ w.length = 3

Tactic:
simp_rw [is3Clique_iff, isCycle_def]

Goal state after:
α : Type u_1
G : SimpleGraph α
⊢ (∃ s a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ↔
    ∃ u w, (w.IsTrail ∧ w ≠ nil ∧ w.support.tail.Nodup) ∧ w.length = 3
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
hp : p.IsPath
hq : q.IsPath
h : p.support.tail.Disjoint q.support.tail
hn : 1 < p.length ∨ 1 < q.length
⊢ (p.append q).IsCycle

Tactic:
by
  rw [isCycle_def, isTrail_append]
  refine ⟨⟨hp.isTrail, hq.isTrail, ?_⟩, ?_, ?_⟩
  · grind [IsPath.disjoint_edges_of_disjoint_support, List.Disjoint.symm]
  · grind [nil_append_iff]
  · rw [tail_support_append, List.nodup_append']
    exact ⟨hp.support_nodup.tail, hq.support_nodup.tail, h⟩

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

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
s : Finset α
⊢ Gᶜ.IsMaximumClique s ↔ G.IsMaximumIndepSet s

Tactic:
simp [isMaximumIndepSet_iff, isMaximumClique_iff]

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

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
s : Finset α
⊢ Gᶜ.IsMaximumIndepSet s ↔ G.IsMaximumClique s

Tactic:
simp [isMaximumIndepSet_iff, isMaximumClique_iff]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: n k : ℕ
hk : 0 < k
hn : k ≤ n
⊢ n + n % k < k * (n / k) + n % k + k * (n / k)

Tactic:
add_assoc,

Goal state after:
n k : ℕ
hk : 0 < k
hn : k ≤ n
⊢ n + n % k < k * (n / k) + (n % k + k * (n / k))
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : NoAccidental t
s : Finset (α ⊕ β ⊕ γ)
⊢ (∃ x ∈ t, toTriangle x = s) → (graph t).IsNClique 3 s

Tactic:
rintro ⟨x, hx, rfl⟩

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : NoAccidental t
x : α × β × γ
hx : x ∈ t
⊢ (graph t).IsNClique 3 (toTriangle x)
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : ↑(#(G.cliqueFinset 3)) < triangleRemovalBound ε * ↑(Fintype.card α) ^ 3
h :
  ∀ G' ≤ G,
    ∀ (x : DecidableRel G'.Adj), ↑(#G.edgeFinset) - ↑(#G'.edgeFinset) < ε * ↑(Fintype.card α ^ 2) → ¬G'.CliqueFree 3
⊢ ∀ ⦃H : SimpleGraph α⦄ [inst : DecidableRel H.Adj],
    H ≤ G → H.CliqueFree 3 → ε * ↑(Fintype.card α ^ 2) ≤ ↑(#G.edgeFinset) - ↑(#H.edgeFinset)

Tactic:
intro G' _ hG hG'

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : Fintype α
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
hG✝ : ↑(#(G.cliqueFinset 3)) < triangleRemovalBound ε * ↑(Fintype.card α) ^ 3
h :
  ∀ G' ≤ G,
    ∀ (x : DecidableRel G'.Adj), ↑(#G.edgeFinset) - ↑(#G'.edgeFinset) < ε * ↑(Fintype.card α ^ 2) → ¬G'.CliqueFree 3
G' : SimpleGraph α
inst✝ : DecidableRel G'.Adj
hG : G' ≤ G
hG' : G'.CliqueFree 3
⊢ ε * ↑(Fintype.card α ^ 2) ≤ ↑(#G.edgeFinset) - ↑(#G'.edgeFinset)
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝¹ : ExplicitDisjoint t
inst✝ : NoAccidental t
⊢ (graph t).EdgeDisjointTriangles

Tactic:
unfold EdgeDisjointTriangles
    convert! map_toTriangle_disjoint t
    rw [cliqueSet_eq_image, coe_map]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
⊢ σₘ[A, B⁻¹] = δₘ[A, B]

Tactic:
rw [mulConst, divConst, ← div_eq_mul_inv]

Goal state after: