mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: α : Type u_1
s : Set α
f : α → ℕ
x✝ : ∃ b, ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
x y : α
hx : x ∈ s
hy : y ∈ s
b : ℕ
hb : ∀ a ∈ s, b ≤ f a ∧ f a ≤ b + 1
⊢ f x ≤ f y + 1

Tactic:
grw [(hb x hx).2, (hb y hy).1]

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
a b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
ha : a ∈ ↑(g c)
d : ι'
hd : d ∈ s
hb : b ∈ ↑(g d)
⊢ Function.onFun Disjoint f a b

Tactic:
obtain hcd | hcd := eq_or_ne (g c) (g d)

Goal state after:
case inl
α : 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 b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
ha : a ∈ ↑(g c)
d : ι'
hd : d ∈ s
hb : b ∈ ↑(g d)
hcd : g c = g d
⊢ Function.onFun Disjoint f a b

case inr
α : 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 b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
ha : a ∈ ↑(g c)
d : ι'
hd : d ∈ s
hb : b ∈ ↑(g d)
hcd : g c ≠ g d
⊢ Function.onFun Disjoint f a b
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G₁ G₂ : SimpleGraph V
inst✝¹ : Fintype ↑G₁.edgeSet
inst✝ : Fintype ↑G₂.edgeSet
⊢ Disjoint ↑G₁.edgeFinset ↑G₂.edgeFinset ↔ Disjoint G₁ G₂

Tactic:
coe_edgeFinset,

Goal state after:
V : Type u_1
G₁ G₂ : SimpleGraph V
inst✝¹ : Fintype ↑G₁.edgeSet
inst✝ : Fintype ↑G₂.edgeSet
⊢ Disjoint G₁.edgeSet G₂.edgeSet ↔ Disjoint G₁ G₂
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
v : V
h : G.IsUniversal v
⊢ G.degree v = Fintype.card V - 1

Tactic:
· simp [← card_neighborFinset_eq_degree, (G.neighborFinset_eq_erase_univ v).mpr h]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
⊢ a + 1 ≤ 4 ^ #P.parts

Tactic:
by
  have h : 1 ≤ 4 ^ #P.parts := one_le_pow₀ (by simp)
  rw [stepBound, ← Nat.div_div_eq_div_mul]
  conv_rhs => rw [← Nat.sub_add_cancel h]
  rw [add_le_add_iff_right, tsub_le_iff_left, ← Nat.add_sub_assoc h]
  exact Nat.le_sub_one_of_lt (Nat.lt_div_mul_add h)

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 β
x : α × β
⊢ (x.1 ∈ s ∧ x.2 ∈ t) ∧ r x.1 x.2 ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ r x.1 x.2

Tactic:
and_assoc

Goal state after:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
x : α × β
⊢ x.1 ∈ s ∧ x.2 ∈ t ∧ r x.1 x.2 ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ r x.1 x.2
Module: Mathlib.Combinatorics.SimpleGraph.Density

Goal state before:
pp: α : 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
⊢ edgeDensity r s₂ t₂ - edgeDensity r s₁ t₁ ≤ 1 - ↑(#s₂) / ↑(#s₁) * (↑(#t₂) / ↑(#t₁))

Tactic:
by
  refine (sub_le_sub_left (mul_edgeDensity_le_edgeDensity r hs ht hs₂ ht₂) _).trans ?_
  refine le_trans ?_ (mul_le_of_le_one_right ?_ (edgeDensity_le_one r s₂ t₂))
  · rw [sub_mul, one_mul]
  refine sub_nonneg_of_le (mul_le_one₀ ?_ ?_ ?_)
  · exact div_le_one_of_le₀ ((@Nat.cast_le ℚ).2 (card_le_card hs)) (Nat.cast_nonneg _)
  · apply div_nonneg <;> exact mod_cast Nat.zero_le _
  · exact div_le_one_of_le₀ ((@Nat.cast_le ℚ).2 (card_le_card ht)) (Nat.cast_nonneg _)

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

Goal state before:
pp: case neg
α : 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
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
⊢ ∃ 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:
obtain ⟨hn₀, hn₁, hn₂, hn₃⟩ : 0 < n ∧ n ≤ m + 1 ∧ n ≤ a * m + b * (m + 1) ∧
      ite (0 < a) (a - 1) a * m + ite (0 < a) b (b - 1) * (m + 1) = #s - n := by
    rw [hn, ← hs]
    split_ifs with h <;> rw [tsub_mul, one_mul]
    · refine ⟨m_pos, le_succ _, le_add_right (Nat.le_mul_of_pos_left _ ‹0 < a›), ?_⟩
      rw [tsub_add_eq_add_tsub (Nat.le_mul_of_pos_left _ h)]
    · refine ⟨succ_pos', le_rfl,
        le_add_left (Nat.le_mul_of_pos_left _ <| hab.resolve_left ‹¬0 < a›), ?_⟩
      rw [← add_tsub_assoc_of_le (Nat.le_mul_of_pos_left _ <| hab.resolve_left ‹¬0 < a›)]

Goal state after:
case neg
α : 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
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #s - n
⊢ ∃ 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: α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
u v : Finset α
ε : 𝕜
⊢ ((u, v).1 ∈ P.parts ∧
      ((u, v).2 ∈ P.parts ∧ (u, v).1 ≠ (u, v).2) ∧
        match (u, v) with
        | (u, v) => ↑(G.edgeDensity u v) < ε) ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ↑(G.edgeDensity u v) < ε

Tactic:
and_assoc

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
u v : Finset α
ε : 𝕜
⊢ ((u, v).1 ∈ P.parts ∧
      (u, v).2 ∈ P.parts ∧
        (u, v).1 ≠ (u, v).2 ∧
          match (u, v) with
          | (u, v) => ↑(G.edgeDensity u v) < ε) ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ↑(G.edgeDensity u v) < ε
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
u v : Finset α
⊢ ((u, v).1 ∈ P.parts ∧
      ((u, v).2 ∈ P.parts ∧ (u, v).1 ≠ (u, v).2) ∧
        match (u, v) with
        | (u, v) => ¬G.IsUniform ε u v) ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v

Tactic:
and_assoc

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
u v : Finset α
⊢ ((u, v).1 ∈ P.parts ∧
      (u, v).2 ∈ P.parts ∧
        (u, v).1 ≠ (u, v).2 ∧
          match (u, v) with
          | (u, v) => ¬G.IsUniform ε u v) ↔
    u ∈ P.parts ∧ v ∈ P.parts ∧ u ≠ v ∧ ¬G.IsUniform ε u v
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: case neg
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
x y : α
hx✝ : x ∈ A
hy✝ : y ∈ A
h : G.Adj x y
h' :
  ∀ x_1 ∈ P.parts,
    ∀ x_2 ∈ P.parts, x ∈ x_1 → y ∈ x_2 → x_1 ≠ x_2 → G.IsUniform (ε / 8) x_1 x_2 → ↑(G.edgeDensity x_1 x_2) < ε / 4
U : Finset α
hU : U ∈ P.parts
hx : x ∈ U
V : Finset α
hV : V ∈ P.parts
hy : y ∈ V
hUV : U ≠ V
h₂ : ¬G.IsUniform (ε / 8) U V
⊢ (∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ¬G.IsUniform (ε / 8) a b ∧ x ∈ a ∧ y ∈ b) ∨
    (∃ a ∈ P.parts, x ∈ a ∧ y ∈ a ∧ x ≠ y) ∨
      ∃ a b, a ∈ P.parts ∧ b ∈ P.parts ∧ a ≠ b ∧ ↑(G.edgeDensity a b) < ε / 4 ∧ x ∈ a ∧ y ∈ b ∧ G.Adj x y

Tactic:
exact Or.inl ⟨U, V, hU, hV, hUV, h₂, hx, hy⟩

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

Goal state before:
pp: case refine_1
α : 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
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      P.IsEquipartition ∧ t ≤ #P.parts ∧ #P.parts ≤ stepBound^[i] t ∧ (P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G))
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[⌊4 / ε ^ 5⌋₊ + 1] t
hP₄ : P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑(⌊4 / ε ^ 5⌋₊ + 1) ≤ ↑(P.energy G)
⊢ stepBound^[⌊4 / ε ^ 5⌋₊ + 1] t ≤ bound ε l

Tactic:
iterate_succ_apply',

Goal state after:
case refine_1
α : 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
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      P.IsEquipartition ∧ t ≤ #P.parts ∧ #P.parts ≤ stepBound^[i] t ∧ (P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G))
P : Finpartition univ
hP₁ : P.IsEquipartition
hP₂ : t ≤ #P.parts
hP₃ : #P.parts ≤ stepBound^[⌊4 / ε ^ 5⌋₊ + 1] t
hP₄ : P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑(⌊4 / ε ^ 5⌋₊ + 1) ≤ ↑(P.energy G)
⊢ stepBound (stepBound^[⌊4 / ε ^ 5⌋₊] t) ≤ bound ε l
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Equitabilise

Goal state before:
pp: case neg.refine_1
α : 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
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ #u
t : Finset α
htu : t ⊆ u
htn : #t = n
ht : t.Nonempty
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #(s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ x ∈ R.parts, #x = m ∨ #x = m + 1
hR₂ : ∀ x ∈ (P.avoid t).parts, #(x \ {y ∈ R.parts | y ⊆ x}.biUnion id) ≤ m
hR₃ : #({i ∈ R.parts | #i = m + 1}) = if 0 < a then b else b - 1
⊢ ∀ x ∈ (R.extend ⋯ ⋯ ⋯).parts, #x = m ∨ #x = m + 1

Tactic:
simp only [mem_insert, forall_eq_or_imp, extend_parts, and_iff_left hR₁, htn, hn]

Goal state after:
case neg.refine_1
α : 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
hs : a * m + b * (m + 1) = #s
hab : 0 < a ∨ 0 < b
n : ℕ := if 0 < a then m else m + 1
hn : n = if 0 < a then m else m + 1
hn₀ : 0 < n
hn₁ : n ≤ m + 1
hn₂ : n ≤ a * m + b * (m + 1)
hn₃ : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #s - n
u : Finset α
hu₁ : u ∈ P.parts
hu₂ : m + 1 ≤ #u
t : Finset α
htu : t ⊆ u
htn : #t = n
ht : t.Nonempty
hcard : (if 0 < a then a - 1 else a) * m + (if 0 < a then b else b - 1) * (m + 1) = #(s \ t)
R : Finpartition (s \ t)
hR₁ : ∀ x ∈ R.parts, #x = m ∨ #x = m + 1
hR₂ : ∀ x ∈ (P.avoid t).parts, #(x \ {y ∈ R.parts | y ⊆ x}.biUnion id) ≤ m
hR₃ : #({i ∈ R.parts | #i = m + 1}) = if 0 < a then b else b - 1
⊢ (if 0 < a then m else m + 1) = m ∨ (if 0 < a then m else m + 1) = m + 1
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma

Goal state before:
pp: case inr.inr.zero
α : 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
this : Nonempty α
⊢ ε ^ 5 / 4 * ↑0 ≤ ↑(dum.energy G)

Tactic:
rw [Nat.cast_zero, mul_zero]

Goal state after:
case inr.inr.zero
α : 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
this : Nonempty α
⊢ 0 ≤ ↑(dum.energy G)
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
⊢ Disjoint H.verts H'.verts → Disjoint H H'

pp: case mpr
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
⊢ Disjoint H H' → Disjoint H.verts H'.verts

Tactic:
· rintro hdisj M' ⟨hsub₀, _⟩ ⟨hsub₁, _⟩
    rw [le_bot_iff]
    ext
    · grind [verts_bot]
    · exact ⟨(hdisj hsub₀ hsub₁ <| M'.edge_vert · :), False.elim⟩

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
H H' : G.Subgraph
⊢ Disjoint H H' → Disjoint H.verts H'.verts
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
v w : V
⊢ (if v = t then if w = t then False else G.Adj s w else if w = t then G.Adj v s else G.Adj v w) →
    if w = t then if v = t then False else G.Adj s v else if v = t then G.Adj w s else G.Adj w v

Tactic:
split_ifs <;> simp [adj_comm]

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
⊢ 2 ^ #P.parts * ε ^ 2 / 10 = 2 ^ #P.parts * (ε * (ε / 10))

Tactic:
mul_div_assoc,

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
⊢ 2 ^ #P.parts * (ε ^ 2 / 10) = 2 ^ #P.parts * (ε * (ε / 10))
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case h₁
α : 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
𝒜 : Finset (Finset α)
s : Finset α
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ ↑(#𝒜) * ↑m ≤ ↑(#(𝒜.sup id))

Tactic:
rw [← (ofSubset _ h𝒜 rfl).sum_card_parts, ofSubset_parts, ← cast_mul, cast_le]

Goal state after:
case h₁
α : 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
𝒜 : Finset (Finset α)
s : Finset α
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ #𝒜 * m ≤ ∑ i ∈ 𝒜, #i
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h : G.Adj u' v'
⊢ { fst := u', snd := v', adj := h } ∈ p.darts ↔ [u', v'] <:+: p.support

Tactic:
refine .trans ⟨fun h ↦ ?_, fun ⟨i, hi, h⟩ ↦ ?_⟩ List.infix_iff_getElem?.symm
  · have ⟨i, hi, h⟩ := List.getElem_of_mem h
    exact ⟨i, by grind, fun j hj ↦ by grind [fst_darts_getElem, snd_darts_getElem]⟩
  · have := h 0
    have := h 1
    convert! p.darts.getElem_mem (n := i) (by grind)
      <;> grind [fst_darts_getElem, snd_darts_getElem]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v u' v' w : V
p : G.Walk u v
q : G.Walk u' v'
hpq : p.IsSubwalk q
h : G.Adj w u'
⊢ p.IsSubwalk (cons h q)

Tactic:
obtain ⟨r1, r2, rfl⟩ := hpq
  use r1.cons h, r2
  simp

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v : V
i : ℕ
u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : p.reverse.getVert i = p.getVert (p.length - i)
⊢ (cons h p).reverse.getVert i = (cons h p).getVert ((cons h p).length - i)

Tactic:
simp only [reverse_cons, getVert_append, length_reverse, ih, length_cons]
    split_ifs
    next hi => simp [Nat.succ_sub hi.le]
    next hi =>
      obtain rfl | hi' := eq_or_gt_of_not_lt hi
      · simp
      · rw [Nat.eq_add_of_sub_eq (Nat.sub_pos_of_lt hi') rfl, Nat.sub_eq_zero_of_le hi']
        simp

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

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
u v w : V
q : G.Walk u w
r : G.Walk w v
⊢ w ∈ (q.append r).support

Tactic:
simp only [mem_support_append_iff, end_mem_support, start_mem_support, or_self_iff]

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
⊢ (SimpleGraph.map (⇑f) G).IsClique ↑t ↔ ∃ s, G.IsClique ↑s ∧ map f s = t

Tactic:
constructor
  · rw [isClique_map_iff_of_nontrivial (by simpa)]
    rintro ⟨s, hs, hst⟩
    obtain ⟨s, rfl⟩ := Set.Finite.exists_finset_coe <|
      (show s.Finite from Set.Finite.of_finite_image (by simp [hst]) f.injective.injOn)
    exact ⟨s,hs, Finset.coe_inj.1 (by simpa)⟩
  rintro ⟨s, hs, rfl⟩
  simpa using hs.map (f := f)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : ⊤.Copy G
⊢ G.IsClique (Set.range ⇑f)

Tactic:
intro _ ⟨_, h⟩ _ ⟨_, h'⟩ nh

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : ⊤.Copy G
x✝ : α
w✝¹ : β
h : f w✝¹ = x✝
y✝ : α
w✝ : β
h' : f w✝ = y✝
nh : x✝ ≠ y✝
⊢ G.Adj x✝ y✝
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case pos
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ : ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b
x : Fin n
hx : φ x = t
y : Fin n
hy : φ y = s
e : (G.replaceVertex s t).Adj (φ x) (φ y) ↔ (completeGraph (Fin n)).Adj x y
⊢ completeGraph (Fin n) ⊑ G

Tactic:
hx,

Goal state after:
case pos
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
s t : α
h : ¬(G.replaceVertex s t).CliqueFree n
φ : Fin n ↪ α
hφ : ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b
x : Fin n
hx : φ x = t
y : Fin n
hy : φ y = s
e : (G.replaceVertex s t).Adj t (φ y) ↔ (completeGraph (Fin n)).Adj x y
⊢ completeGraph (Fin n) ⊑ G
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case right
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
h : Maximal (fun H ↦ H.CliqueFree (n + 1)) G
x y : α
hne : x ≠ y
hn : ¬G.Adj x y
t : Finset α
hc : (G ⊔ edge x y).IsNClique (n + 1) t
⊢ G.IsNClique n (insert x ((t.erase x).erase y)) ∧ G.IsNClique n (insert y ((t.erase x).erase y))

Tactic:
have h1 := h.1.mem_of_sup_edge_isNClique hc

Goal state after:
case right
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
h : Maximal (fun H ↦ H.CliqueFree (n + 1)) G
x y : α
hne : x ≠ y
hn : ¬G.Adj x y
t : Finset α
hc : (G ⊔ edge x y).IsNClique (n + 1) t
h1 : x ∈ t
⊢ G.IsNClique n (insert x ((t.erase x).erase y)) ∧ G.IsNClique n (insert y ((t.erase x).erase y))
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
⊢ G.cliqueSet n = ∅ ↔ G.CliqueFree n

Tactic:
simp_rw [CliqueFree, Set.eq_empty_iff_forall_notMem, mem_cliqueSet_iff]

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

Goal state before:
pp: α : Type u_1
R : Type u_2
s t : Finset α
inst✝¹ : DecidableEq α
inst✝ : AddGroupWithOne R
⊢ ↑(#(s ∩ t)) + ↑(#(s ∪ t)) = ↑(#s) + ↑(#t)

Tactic:
← cast_add,

Goal state after:
α : Type u_1
R : Type u_2
s t : Finset α
inst✝¹ : DecidableEq α
inst✝ : AddGroupWithOne R
⊢ ↑(#(s ∩ t) + #(s ∪ t)) = ↑(#s) + ↑(#t)
Module: Mathlib.Data.Finset.CastCard

Goal state before:
pp: α : Type u_1
R : Type u_2
s t : Finset α
inst✝¹ : DecidableEq α
inst✝ : AddGroupWithOne R
⊢ ↑(#(s ∪ t)) + ↑(#(s ∩ t)) = ↑(#s) + ↑(#t)

Tactic:
← cast_add,

Goal state after:
α : Type u_1
R : Type u_2
s t : Finset α
inst✝¹ : DecidableEq α
inst✝ : AddGroupWithOne R
⊢ ↑(#(s ∪ t) + #(s ∩ t)) = ↑(#s) + ↑(#t)
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: α : Type u_1
𝕜 : Type u_3
inst✝⁶ : Field 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
ε : 𝕜
inst✝³ : Fintype α
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq α
tris : Finset (Finset α)
htris : tris ⊆ G.cliqueFinset 3
pd : (↑tris).Pairwise fun x y ↦ (↑x ∩ ↑y).Subsingleton
tris_big : ε * ↑(Fintype.card α ^ 2) ≤ ↑(#tris)
H : SimpleGraph α
inst✝ : DecidableRel H.Adj
hG : H ≤ G
hH : H.CliqueFree 3
⊢ ε * ↑(Fintype.card α ^ 2) ≤ ↑(#G.edgeFinset - #H.edgeFinset)

Tactic:
exact tris_big.trans
    (Nat.cast_le.2 <| farFromTriangleFree_of_disjoint_triangles_aux htris pd hG hH)

Goal state after:
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝³ : Fintype K
inst✝² : Field K
inst✝¹ : Fintype σ
inst✝ : DecidableEq σ
f : MvPolynomial σ K
h : f.totalDegree < (q - 1) * Fintype.card σ
this✝ : DecidableEq K
d : σ →₀ ℕ
hd : d ∈ f.support
i : σ
hi : d i < q - 1
x₀ : { j // j ≠ i } → K
e : K ≃ { x // x ∘ Subtype.val = x₀ } := (Equiv.subtypeEquivCodomain x₀).symm
a : K
e' : { j // j = i } ⊕ { j // j ≠ i } ≃ σ := Equiv.sumCompl fun j ↦ j = i
this : Unique { j // j = i } := { default := ⟨i, ⋯⟩, uniq := ⋯ }
⊢ ∏ j, ↑(e a) j ^ d j = ↑(e a) i ^ d i * ∏ j, ↑(e a) ↑j ^ d ↑j

Tactic:
rw [← e'.prod_comp, Fintype.prod_sum_type, univ_unique, prod_singleton]; rfl

Goal state after: