mathlib-initiative/mathlib-tactics huggingface dataset:
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)
hA₀ : A.Nonempty
⊢ K ^ 2 * ↑(#A) * (K * ↑(#A)) = ↑(#A) * (K ^ 3 * ↑(#A))

Tactic:
ring

Goal state after:
Module: Mathlib.Data.Finset.Pairwise

Goal state before:
pp: α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : s.PairwiseDisjoint fun i' ↦ (g i').sup f
hg : ∀ i ∈ s, (↑(g i)).PairwiseDisjoint f
⊢ (⋃ i ∈ s, ↑(g i)).PairwiseDisjoint f

Tactic:
rintro a ha b hb hab

Goal state after:
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝¹ : Lattice α
inst✝ : OrderBot α
s : Set ι'
g : ι' → Finset ι
f : ι → α
hs : s.PairwiseDisjoint fun i' ↦ (g i').sup f
hg : ∀ i ∈ s, (↑(g i)).PairwiseDisjoint f
a : ι
ha : a ∈ ⋃ i ∈ s, ↑(g i)
b : ι
hb : b ∈ ⋃ i ∈ s, ↑(g i)
hab : a ≠ b
⊢ Function.onFun Disjoint f a b
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : G = ⊥
⊢ G.maxDegree = 0

Tactic:
convert maxDegree_bot_eq_zero
    assumption

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v w : V
⊢ Fintype.card ↑(G.commonNeighbors v w) ≤ G.degree v

Tactic:
rw [← card_neighborSet_eq_degree]
  exact Set.card_le_card Set.inter_subset_left

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

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : G.degree v = Fintype.card V - 1
⊢ G.IsUniversal v

Tactic:
rw [← G.insert_neighborFinset_eq_univ v, ← Finset.card_eq_iff_eq_univ]
    simp [h, Nat.sub_add_cancel <| Fintype.card_pos_iff.mpr ⟨v⟩]

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
⊢ #({p ∈ P.parts | #p = #s / #P.parts}) =
    #({p ∈ P.parts | #p = #s / #P.parts + 1}) + #({a ∈ P.parts | ¬#a = #s / #P.parts + 1}) - #s % #P.parts

Tactic:
rw [hP.card_large_parts_eq_mod, add_tsub_cancel_left, hP.filter_ne_average_add_one_eq_average]

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

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

Tactic:
induction b using WithBotTop.rec <;> simp at hab

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

case bot.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
a✝ : ℤ
hab✝ : ⊥ ⟶ WithBotTop.coe a✝
hab : True
⊢ t.eTruncGE.map hab✝ ≫ WithBotTop.rec 0 t.truncGEδLT 0 (WithBotTop.coe a✝) =
    WithBotTop.rec 0 t.truncGEδLT 0 ⊥ ≫ (t.eTruncLT ⋙ (Functor.whiskeringRight C C C).obj (shiftFunctor C 1)).map hab✝

case bot.top
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
hab✝ : ⊥ ⟶ ⊤
hab : True
⊢ t.eTruncGE.map hab✝ ≫ WithBotTop.rec 0 t.truncGEδLT 0 ⊤ =
    WithBotTop.rec 0 t.truncGEδLT 0 ⊥ ≫ (t.eTruncLT ⋙ (Functor.whiskeringRight C C C).obj (shiftFunctor C 1)).map hab✝
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
b : EInt
a✝ : ℤ
hab✝ : WithBotTop.coe a✝ ⟶ b
hab : WithBotTop.coe a✝ ≤ b
⊢ t.eTruncGE.map hab✝ ≫ WithBotTop.rec 0 t.truncGEδLT 0 b =
    WithBotTop.rec 0 t.truncGEδLT 0 (WithBotTop.coe a✝) ≫
      (t.eTruncLT ⋙ (Functor.whiskeringRight C C C).obj (shiftFunctor C 1)).map hab✝

Tactic:
induction b using WithBotTop.rec <;> simp at hab

Goal state after:
case coe.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
a✝¹ a✝ : ℤ
hab✝ : WithBotTop.coe a✝¹ ⟶ WithBotTop.coe a✝
hab : a✝¹ ≤ a✝
⊢ t.eTruncGE.map hab✝ ≫ WithBotTop.rec 0 t.truncGEδLT 0 (WithBotTop.coe a✝) =
    WithBotTop.rec 0 t.truncGEδLT 0 (WithBotTop.coe a✝¹) ≫
      (t.eTruncLT ⋙ (Functor.whiskeringRight C C C).obj (shiftFunctor C 1)).map hab✝

case coe.top
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
a✝ : ℤ
hab✝ : WithBotTop.coe a✝ ⟶ ⊤
hab : True
⊢ t.eTruncGE.map hab✝ ≫ WithBotTop.rec 0 t.truncGEδLT 0 ⊤ =
    WithBotTop.rec 0 t.truncGEδLT 0 (WithBotTop.coe a✝) ≫
      (t.eTruncLT ⋙ (Functor.whiskeringRight C C C).obj (shiftFunctor C 1)).map hab✝
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a b : α
P : Finpartition a
hab : a ≤ b
hr : b \ a = ⊥
⊢ P.parts ⊆ (⋯ ▸ P).parts

Tactic:
cases le_antisymm (sdiff_eq_bot_iff.mp hr) hab; rfl

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

Goal state before:
pp: case inl
α : 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
a : ↥s
c : #↑(f a).fst = #s / #P.parts
⊢ z a < #s

pp: case inr
α : 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
a : ↥s
c : #↑(f a).fst = #s / #P.parts + 1
⊢ z a < #s

Tactic:
· calc
        _ < #P.parts * ((f a).2 + 1) := by simp only [z, mul_add_one]; gcongr; exact gl a
        _ ≤ #P.parts * (#s / #P.parts) := by gcongr; exact c ▸ (f a).2.2
        _ ≤ #P.parts * (#s / #P.parts) + #s % #P.parts := Nat.le_add_right ..
        _ = _ := Nat.div_add_mod ..

Goal state after:
case inr
α : 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
a : ↥s
c : #↑(f a).fst = #s / #P.parts + 1
⊢ z a < #s
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

Goal state before:
pp: ε : ℝ
hε : 0 < ε
l : ℕ
⊢ 100 < 4 ^ initialBound ε l * ε ^ 5

Tactic:
rw [← rpow_natCast 4, ← div_lt_iff₀ (pow_pos hε 5), lt_rpow_iff_log_lt _ zero_lt_four, ←
    div_lt_iff₀, initialBound, Nat.cast_max, Nat.cast_max]
  · push_cast
    exact lt_max_of_lt_right (lt_max_of_lt_right <| Nat.lt_floor_add_one _)
  · exact log_pos (by simp)
  · exact div_pos (by simp) (pow_pos hε 5)

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a✝ : α
s : Finset α
F : Finset (Finset α)
a : α
ha : a ∈ s
⊢ a ∈ (image (fun Q ↦ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}) F.powerset).sup id

Tactic:
rw [mem_sup]

Goal state after:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a✝ : α
s : Finset α
F : Finset (Finset α)
a : α
ha : a ∈ s
⊢ ∃ i ∈ image (fun Q ↦ {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t}) F.powerset, a ∈ id i
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
s : Finset α
ih :
  ∀ t ⊂ s,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ 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
a b : ℕ
P : Finpartition s
hab : a = 0 ∧ b = 0
hs : s = ⊥
⊢ ∃ 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:
subst hs

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
m : ℕ
m_pos : m > 0
a b : ℕ
hab : a = 0 ∧ b = 0
ih :
  ∀ t ⊂ ⊥,
    ∀ {a b : ℕ} {P : Finpartition t},
      a * m + b * (m + 1) = #t →
        ∃ 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
P : Finpartition ⊥
⊢ ∃ 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.Regularity.Uniform

Goal state before:
pp: case neg
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h : ¬G.IsUniform ε s t
h✝ : ¬WellOrderingRel s t
⊢ (G.nonuniformWitnesses ε t s).2 ⊆ s

Tactic:
exact G.right_nonuniformWitnesses_subset fun i => h i.symm

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

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(#s₁) ≤ ↑(#s₂)
ht₂ : (1 - δ) * ↑(#t₁) ≤ ↑(#t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : s₂.Nonempty
ht₂' : t₂.Nonempty
⊢ 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)

Tactic:
ring

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

Goal state before:
pp: case a.calc_1
α : 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 ≤ ε
⊢ ∀ x ∈ P.parts.offDiag, #x.1 * #x.2 ≤ (#A / #P.parts + 1) ^ 2

Tactic:
simp only [Prod.forall, and_imp, mem_offDiag, sq]
    rintro U V hU hV -
    exact_mod_cast Nat.mul_le_mul (hP.card_part_le_average_add_one hU)
      (hP.card_part_le_average_add_one hV)

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
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ ε * (↑(#A) + ↑(#A)) ^ 2 = 4 * ε * ↑(#A) ^ 2

Tactic:
ring

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

Goal state before:
pp: case e'_3
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
this✝ : ↑(#A) + ↑(#P.parts) ≤ 2 * ↑(#A)
this : 1 ≤ ε / 4 * ↑(#P.parts)
⊢ 2 * ↑(#A) ^ 2 = 2 * ↑(#A) ^ 2 * 1

Tactic:
ring

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

Goal state before:
pp: case e'_4
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
this✝ : ↑(#A) + ↑(#P.parts) ≤ 2 * ↑(#A)
this : 1 ≤ ε / 4 * ↑(#P.parts)
⊢ ε / 2 * ↑(#A) ^ 2 * ↑(#P.parts) = 2 * ↑(#A) ^ 2 * (ε / 4 * ↑(#P.parts))

Tactic:
ring

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
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ ε * (↑(#A) + ↑(#A)) ^ 2 = 4 * ε * ↑(#A) ^ 2

Tactic:
ring

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

Goal state before:
pp: case inr.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : 1 ≤ ε
⊢ ∃ P, P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε

pp: case inr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
⊢ ∃ P, P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε

Tactic:
· exact ⟨dum, hdum₁, (le_initialBound ε l).trans hdum₂.ge,
      hdum₂.le.trans (initialBound_le_bound ε l), (dum.isUniform_one G).mono hε₁⟩

Goal state after:
case inr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
⊢ ∃ P, P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε
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.parts.offDiag) * ε < ↑(#(P.nonUniforms G ε))
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ ↑(#P.parts) ^ 2 * (ε ^ 5 / 4) = 6 / 7 * ↑(#P.parts) ^ 2 * ε ^ 5 * (7 / 24)

Tactic:
ring

Goal state after:
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
s : Set G.Subgraph
a b : V
G' : G.Subgraph
hG' : G' ∈ s
hab : G'.Adj a b
⊢ a ∈ ⋃ G' ∈ s, G'.verts

Tactic:
exact Set.mem_iUnion₂_of_mem hG' (G'.edge_vert hab)

Goal state after:
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.parts.offDiag) * ε < ↑(#(P.nonUniforms G ε))
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ ↑(#P.parts.offDiag) * ε ^ 5 * (22 / 75) = ↑(#P.parts.offDiag) * ε * (ε ^ 4 / 3) - ↑(#P.parts.offDiag) * (ε ^ 5 / 25)

Tactic:
ring

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

Goal state before:
pp: case map_rel_iff'
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G G₁ G₂ G₃ : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
f : A.Copy B
A' : A.Subgraph
⊢ ∀ {a b : ↑A'.verts}, (∃ a_1 b_1, A'.Adj a_1 b_1 ∧ a_1 = ↑a ∧ b_1 = ↑b) ↔ A'.Adj ↑a ↑b

Tactic:
exists_eq_right_right,

Goal state after:
case map_rel_iff'
V : Type u_1
W : Type u_2
X : Type u_3
α : Type u_4
β : Type u_5
γ : Type u_6
G G₁ G₂ G₃ : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph X
A : SimpleGraph α
B : SimpleGraph β
C : SimpleGraph γ
f : A.Copy B
A' : A.Subgraph
⊢ ∀ {a b : ↑A'.verts}, (∃ a_1, A'.Adj a_1 ↑b ∧ a_1 = ↑a) ↔ A'.Adj ↑a ↑b
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
G' : SimpleGraph W
f✝ f : G →g G'
H : G.Subgraph
⊢ ∀ {v w : W}, Relation.Map H.Adj (⇑f) (⇑f) v w → G'.Adj v w

Tactic:
by
    rintro _ _ ⟨u, v, h, rfl, rfl⟩
    exact f.map_rel (H.adj_sub h)

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

Goal state before:
pp: case refine_2
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G₁ G₂ : G.Subgraph
a b : V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
H : G.Subgraph
⊢ ∃ a, (fun H ↦ { verts := ↑(↑H).1, Adj := fun a b ↦ (↑H).2 a b = true, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }) a = H

Tactic:
classical
    exact ⟨⟨(H.verts.toFinset, fun a b ↦ H.Adj a b), fun a b ↦ by simpa using H.adj_sub,
      fun a b ↦ by simpa using H.edge_vert, by simp [H.adj_comm]⟩, by simp⟩

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
⊢ 2 ^ #P.parts = 2 ^ (#P.parts - 1 + 1)

Tactic:
tsub_add_cancel_of_le (succ_le_iff.2 hP₁)

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
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
this : 2 ^ #P.parts * ↑m / (↑(#U) * ε) ≤ ε / 10
⊢ 2 ^ #P.parts = 2 ^ #P.parts
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ sSup {x | ∃ u v, ∃ (_ : G.Adj u v), fromEdgeSet {s(u, v)} = x} = sSup {x | ∃ y, fromEdgeSet {↑y} = x}

Tactic:
Subtype.exists,

Goal state after:
V : Type u_1
G : SimpleGraph V
⊢ sSup {x | ∃ u v, ∃ (_ : G.Adj u v), fromEdgeSet {s(u, v)} = x} =
    sSup {x | ∃ a, ∃ (_ : a ∈ G.edgeSet), fromEdgeSet {a} = x}
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v : V
S : Set V
u✝ x w✝ : V
a : G.Adj u✝ x
p' : G.Walk x w✝
ih : x ∈ S → w✝ ∉ S → ∃ d ∈ p'.darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
uS : u✝ ∈ S
vS : w✝ ∉ S
⊢ ∃ d ∈ (cons a p').darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S

Tactic:
by_cases h : x ∈ S

Goal state after:
case pos
V : Type u
G : SimpleGraph V
u v : V
S : Set V
u✝ x w✝ : V
a : G.Adj u✝ x
p' : G.Walk x w✝
ih : x ∈ S → w✝ ∉ S → ∃ d ∈ p'.darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
uS : u✝ ∈ S
vS : w✝ ∉ S
h : x ∈ S
⊢ ∃ d ∈ (cons a p').darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S

case neg
V : Type u
G : SimpleGraph V
u v : V
S : Set V
u✝ x w✝ : V
a : G.Adj u✝ x
p' : G.Walk x w✝
ih : x ∈ S → w✝ ∉ S → ∃ d ∈ p'.darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
uS : u✝ ∈ S
vS : w✝ ∉ S
h : x ∉ S
⊢ ∃ d ∈ (cons a p').darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
s : Set (Sym2 V)
p : G.Walk v w
hp : ∀ e ∈ p.edges, e ∉ s
⊢ (toDeleteEdges s p hp).transfer G ?hp = p

pp: case hp
V : Type u
G : SimpleGraph V
v w : V
s : Set (Sym2 V)
p : G.Walk v w
hp : ∀ e ∈ p.edges, e ∉ s
⊢ ∀ e ∈ (toDeleteEdges s p hp).edges, e ∈ G.edgeSet

Tactic:
transfer_transfer,

Goal state after:
V : Type u
G : SimpleGraph V
v w : V
s : Set (Sym2 V)
p : G.Walk v w
hp : ∀ e ∈ p.edges, e ∉ s
⊢ p.transfer G ⋯ = p

case hp
V : Type u
G : SimpleGraph V
v w : V
s : Set (Sym2 V)
p : G.Walk v w
hp : ∀ e ∈ p.edges, e ∉ s
⊢ ∀ e ∈ (toDeleteEdges s p hp).edges, e ∈ G.edgeSet
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
this : 0 ≤ ε
⊢ (1 + ε ^ 5 / 100) ^ 2 = 1 + ε ^ 5 * (50⁻¹ + ε ^ 5 / 10000)

Tactic:
ring

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
t u v w : V
p : G.Walk u v
p' : G.Walk v w
⊢ t ∈ (p.append p').support ↔ t ∈ p.support ∨ t ∈ p'.support

Tactic:
by
  grind [mem_support_iff, mem_tail_support_append_iff, end_mem_tail_support_of_ne]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
⊢ (∃ s, G.IsClique s ∧ ⇑f '' s = t) → (SimpleGraph.map (⇑f) G).IsClique t

Tactic:
rintro ⟨x, hs, rfl⟩; exact hs.map

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : (SimpleGraph.map (⇑f) G).IsClique t
x : β
hxt : x ∈ t
y : β
hyt : y ∈ t
hyne : y ≠ x
⊢ x ∈ Set.range ⇑f

Tactic:
obtain ⟨-, u, v, -, rfl, rfl⟩ := h hyt hxt hyne

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Set β
ht : t.Nontrivial
h : (SimpleGraph.map (⇑f) G).IsClique t
u v : α
hyt : f u ∈ t
hxt : f v ∈ t
hyne : f u ≠ f v
⊢ f v ∈ Set.range ⇑f
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
n : ℕ
hn : n ≤ p.length - 1
m : ℕ
hm : m ≤ p.length - 1
hnm : p.getVert n = p.getVert m
this : 3 ≤ p.length
⊢ p.reverse.length - n ∈ {i | 1 ≤ i ∧ i ≤ p.reverse.length}

Tactic:
simp only [Walk.length_reverse, Set.mem_ofPred_eq]

Goal state after:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
n : ℕ
hn : n ≤ p.length - 1
m : ℕ
hm : m ≤ p.length - 1
hnm : p.getVert n = p.getVert m
this : 3 ≤ p.length
⊢ 1 ≤ p.length - n ∧ p.length - n ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
n : ℕ
hn : n ≤ p.length - 1
m : ℕ
hm : m ≤ p.length - 1
hnm : p.getVert n = p.getVert m
this : 3 ≤ p.length
⊢ p.reverse.length - m ∈ {i | 1 ≤ i ∧ i ≤ p.reverse.length}

Tactic:
simp only [Walk.length_reverse, Set.mem_ofPred_eq]

Goal state after:
V : Type u
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
n : ℕ
hn : n ≤ p.length - 1
m : ℕ
hm : m ≤ p.length - 1
hnm : p.getVert n = p.getVert m
this : 3 ≤ p.length
⊢ 1 ≤ p.length - m ∧ p.length - m ≤ p.length
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
s : Finset α
⊢ G.IsNClique 0 s ↔ s = ∅

Tactic:
simp only [isNClique_iff, Finset.card_eq_zero, and_iff_right_iff_imp]

Goal state after:
α : Type u_1
G : SimpleGraph α
s : Finset α
⊢ s = ∅ → G.IsClique ↑s