mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Additive.PluenneckeRuzsa

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

Tactic:
card_singleton_mul

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
n : ℕ∞
⊢ (∀ ⦃a : G⦄, a ≠ 1 → IsOfFinOrder a → n ≤ ↑(orderOf a)) ↔ ∀ ⦃s : Subgroup G⦄, s ≠ ⊥ → (↑s).Finite → n ≤ ↑(Nat.card ↥s)

Tactic:
refine ⟨fun h s hs hs' ↦ ?_, fun h a ha ha' ↦ ?_⟩

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
n : ℕ∞
h : ∀ ⦃a : G⦄, a ≠ 1 → IsOfFinOrder a → n ≤ ↑(orderOf a)
s : Subgroup G
hs : s ≠ ⊥
hs' : (↑s).Finite
⊢ n ≤ ↑(Nat.card ↥s)

case refine_2
G : Type u_1
inst✝ : Group G
n : ℕ∞
h : ∀ ⦃s : Subgroup G⦄, s ≠ ⊥ → (↑s).Finite → n ≤ ↑(Nat.card ↥s)
a : G
ha : a ≠ 1
ha' : IsOfFinOrder a
⊢ n ≤ ↑(orderOf 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⁻¹ = B⁻¹.convolution A⁻¹ x

Tactic:
← inv_inv B

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
x : G
⊢ A.convolution B⁻¹⁻¹ x⁻¹ = B⁻¹.convolution A⁻¹ x
Module: Mathlib.Combinatorics.Additive.Convolution

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
s x : G
⊢ A.convolution (B <• s) x = A.convolution B (x * s⁻¹)

Tactic:
← inv_inv B

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
s x : G
⊢ A.convolution (B <• s) x = A.convolution B⁻¹⁻¹ (x * s⁻¹)
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
v : V
h : Odd (G.degree v)
⊢ ∃ w, w ≠ v ∧ Odd (G.degree w)

Tactic:
by
  have := Classical.decEq V
  rcases G.odd_card_odd_degree_vertices_ne v h with ⟨k, hg⟩
  have hg' : 0 < #{w | w ≠ v ∧ Odd (G.degree w)} := by
    rw [hg]
    apply Nat.succ_pos
  rcases card_pos.mp hg' with ⟨w, hw⟩
  rw [mem_filter_univ] at hw
  exact ⟨w, hw⟩

Goal state after:
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℕ
b : ℕ
hb : ∀ a ∈ ↑s, b ≤ f a ∧ f a ≤ b + 1
x : α
hx₁ : x ∈ s
hx₂ : f x ≠ b + 1
h : b = (∑ i ∈ s, f i) / #s
⊢ ∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1

Tactic:
simp_rw [← h]
    apply hb

Goal state after:
Module: Mathlib.Data.Set.Equitable

Goal state before:
pp: α : Type u_1
s : Finset α
f : α → ℕ
⊢ (↑s).EquitableOn f ↔ ∀ a ∈ s, (∑ i ∈ s, f i) / #s ≤ f a ∧ f a ≤ (∑ i ∈ s, f i) / #s + 1

Tactic:
by
  rw [Set.equitableOn_iff_exists_le_le_add_one]
  refine ⟨?_, fun h => ⟨_, h⟩⟩
  rintro ⟨b, hb⟩
  by_cases! h : ∀ a ∈ s, f a = b + 1
  · intro a ha
    rw [h _ ha, sum_const_nat h, Nat.mul_div_cancel_left _ (card_pos.2 ⟨a, ha⟩)]
    exact ⟨le_rfl, Nat.le_succ _⟩
  obtain ⟨x, hx₁, hx₂⟩ := h
  suffices h : b = (∑ i ∈ s, f i) / s.card by
    simp_rw [← h]
    apply hb
  symm
  refine
    Nat.div_eq_of_lt_le (le_trans (by simp [mul_comm]) (sum_le_sum fun a ha => (hb a ha).1))
      ((sum_lt_sum (fun a ha => (hb a ha).2) ⟨_, hx₁, (hb _ hx₁).2.lt_of_ne hx₂⟩).trans_le ?_)
  rw [mul_comm, sum_const_nat]
  exact fun _ _ => rfl

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

Goal state before:
pp: case refine_2
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
v w : V
h : G.Adj v w
⊢ insert w (G.commonNeighbors v w).toFinset ⊆ G.neighborFinset v

Tactic:
· simpa [Finset.insert_subset_iff, G.commonNeighbors_subset_neighborSet_left v w]

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:
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 β
hs : s.Nonempty
ht : t.Nonempty
⊢ (↑(#(interedges r s t)) + ↑(#(interedges (fun x y ↦ ¬r x y) s t))) / (↑(#s) * ↑(#t)) = 1

Tactic:
div_eq_one_iff_eq

Goal state after:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
hs : s.Nonempty
ht : t.Nonempty
⊢ ↑(#(interedges r s t)) + ↑(#(interedges (fun x y ↦ ¬r x y) s t)) = ↑(#s) * ↑(#t)

α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
hs : s.Nonempty
ht : t.Nonempty
⊢ ↑(#s) * ↑(#t) ≠ 0
Module: Mathlib.Combinatorics.SimpleGraph.Density

Goal state before:
pp: α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝¹ : (a : α) → DecidablePred (r a)
t : Finset β
inst✝ : DecidableEq β
s : Finset α
P : Finpartition t
⊢ #(interedges r s t) = ∑ b ∈ P.parts, #(interedges r s b)

Tactic:
simp_rw [← P.biUnion_parts, interedges_biUnion_right, id]
  rw [card_biUnion]
  exact fun x hx y hy h ↦ interedges_disjoint_right r _ (P.disjoint hx hy h)

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

Goal state before:
pp: α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
hs : s.Nonempty
ht : t.Nonempty
h : Disjoint s t
⊢ (↑(#(G.interedges s t)) + ↑(#(Gᶜ.interedges s t))) / (↑(#s) * ↑(#t)) = 1

Tactic:
div_eq_one_iff_eq

Goal state after:
α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
hs : s.Nonempty
ht : t.Nonempty
h : Disjoint s t
⊢ ↑(#(G.interedges s t)) + ↑(#(Gᶜ.interedges s t)) = ↑(#s) * ↑(#t)

α : Type u_4
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
s t : Finset α
inst✝ : DecidableEq α
hs : s.Nonempty
ht : t.Nonempty
h : Disjoint s t
⊢ ↑(#s) * ↑(#t) ≠ 0
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma

Goal state before:

Tactic:
(1 : ℝ) = ε ^ 5 / ↑4 * (↑4 / ε ^ 5) := by
        rw [mul_comm, div_mul_div_cancel₀ (pow_pos hε 5).ne']; simp
      _ < ε ^ 5 / 4 * (⌊4 / ε ^ 5⌋₊ + 1) := by gcongr; exact Nat.lt_floor_add_one _
      _ ≤ (P.energy G : ℝ) := by rwa [← Nat.cast_add_one]
      _ ≤ 1 := mod_cast P.energy_le_one G

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
ε : ℝ
inst✝ : Nonempty α
x : ↥P.parts.offDiag
hε₁ : ε ≤ 1
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
⊢ ↑(G.edgeDensity (↑x).1 (↑x).2) ^ 2 + ((if G.IsUniform ε (↑x).1 (↑x).2 then 0 else ε ^ 4 / 3) - ε ^ 5 / 25) ≤
    (∑ i ∈ distinctPairs hP G ε x, ↑(G.edgeDensity i.1 i.2) ^ 2) / 16 ^ #P.parts

Tactic:
rw [distinctPairs, ← add_sub_assoc, add_sub_right_comm]
  split_ifs with h
  · rw [add_zero]
    exact edgeDensity_chunk_uniform hPα hPε _ _
  · exact edgeDensity_chunk_not_uniform hPα hPε hε₁ (mem_offDiag.1 x.2).2.2 h

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
hH : H ≠ ⊥
G' : G.Subgraph
e : Sym2 W
he : e ∈ H.edgeSet
⊢ Nonempty (H ≃g G'.coe) → G'.edgeSet.Nonempty

Tactic:
rw [← Subgraph.image_coe_edgeSet_coe]

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hH : H ≠ ⊥
G' : G.Subgraph
e : Sym2 W
he : e ∈ H.edgeSet
⊢ Nonempty (H ≃g G'.coe) → (Sym2.map Subtype.val '' G'.coe.edgeSet).Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case Adj
V : Type u
G : SimpleGraph V
H : G.Subgraph
v : V
h : H.verts = {v}
x✝¹ x✝ : V
⊢ H.Adj x✝¹ x✝ ↔ (G.singletonSubgraph v).Adj x✝¹ x✝

Tactic:
simp only [Prop.bot_eq_false, singletonSubgraph_adj, Pi.bot_apply, iff_false]
    intro ha
    have ha1 := ha.fst_mem
    have ha2 := ha.snd_mem
    rw [h, Set.mem_singleton_iff] at ha1 ha2
    subst_vars
    exact ha.ne rfl

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
v w : V
⊢ (Subgraph.coeSubgraph G'').Adj v w ↔ ∃ (hv : v ∈ G'.verts) (hw : w ∈ G'.verts), G''.Adj ⟨v, hv⟩ ⟨w, hw⟩

Tactic:
by
  simp [Relation.Map]

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

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v w u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
p : G.Walk v✝ w✝
ih : ¬p.Nil → (w ∈ p.support ↔ ∃ e ∈ p.edges, w ∈ e)
hnil : ¬(cons h p).Nil
⊢ w ∈ (cons h p).support ↔ ∃ e ∈ (cons h p).edges, w ∈ e

Tactic:
| cons h p ih =>

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

Goal state before:
pp: 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)
hi : ¬i < p.length
⊢ (cons ⋯ nil).getVert (i - p.length) = (cons h p).getVert (p.length + 1 - i)

Tactic:
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.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:
| cons h p ih =>

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
c : G.Walk v v
u : V
h : u ∈ c.support
⊢ (c.rotate u h).support.tail ~r c.support.tail

Tactic:
by
  simp only [rotate, tail_support_append]
  apply List.IsRotated.trans List.isRotated_append
  rw [← tail_support_append, take_spec]

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

Goal state before:
pp: case nil.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ (nil.drop 0).length = nil.length - 0

Tactic:
simp [*, drop]

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

Goal state before:
pp: case nil.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ (nil.drop (n✝ + 1)).length = nil.length - (n✝ + 1)

Tactic:
simp [*, drop]

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

Goal state before:
pp: case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).length = p✝.length - n
⊢ ((cons h✝ p✝).drop 0).length = (cons h✝ p✝).length - 0

Tactic:
simp [*, drop]

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

Goal state before:
pp: case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).length = p✝.length - n
n✝ : ℕ
⊢ ((cons h✝ p✝).drop (n✝ + 1)).length = (cons h✝ p✝).length - (n✝ + 1)

Tactic:
simp [*, drop]

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

Goal state before:
pp: case nil.zero
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ : V
⊢ nil.drop (m + 0) ≍ (nil.drop 0).drop m

Tactic:
simp [*, drop]

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

Goal state before:
pp: case nil.succ
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ : V
n✝ : ℕ
⊢ nil.drop (m + (n✝ + 1)) ≍ (nil.drop (n✝ + 1)).drop m

Tactic:
simp [*, drop]

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

Goal state before:
pp: case cons.zero
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), p✝.drop (m + n) ≍ (p✝.drop n).drop m
⊢ (cons h✝ p✝).drop (m + 0) ≍ ((cons h✝ p✝).drop 0).drop m

Tactic:
simp [*, drop]

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

Goal state before:
pp: case cons.succ
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), p✝.drop (m + n) ≍ (p✝.drop n).drop m
n✝ : ℕ
⊢ (cons h✝ p✝).drop (m + (n✝ + 1)) ≍ ((cons h✝ p✝).drop (n✝ + 1)).drop m

Tactic:
simp [*, drop]

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

Goal state before:
pp: case nil.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ (nil.drop 0).Nil ↔ nil.length ≤ 0

Tactic:
simp [*, drop]

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

Goal state before:
pp: case nil.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ (nil.drop (n✝ + 1)).Nil ↔ nil.length ≤ n✝ + 1

Tactic:
simp [*, drop]

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

Goal state before:
pp: case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).Nil ↔ p✝.length ≤ n
⊢ ((cons h✝ p✝).drop 0).Nil ↔ (cons h✝ p✝).length ≤ 0

Tactic:
simp [*, drop]

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

Goal state before:
pp: case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).Nil ↔ p✝.length ≤ n
n✝ : ℕ
⊢ ((cons h✝ p✝).drop (n✝ + 1)).Nil ↔ (cons h✝ p✝).length ≤ n✝ + 1

Tactic:
simp [*, drop]

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

Goal state before:
pp: case nil.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ (nil.drop 0).darts = List.drop 0 nil.darts

Tactic:
simp [*, drop]

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

Goal state before:
pp: case nil.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ (nil.drop (n✝ + 1)).darts = List.drop (n✝ + 1) nil.darts

Tactic:
simp [*, drop]

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

Goal state before:
pp: case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).darts = List.drop n p✝.darts
⊢ ((cons h✝ p✝).drop 0).darts = List.drop 0 (cons h✝ p✝).darts

Tactic:
simp [*, drop]

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

Goal state before:
pp: case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).darts = List.drop n p✝.darts
n✝ : ℕ
⊢ ((cons h✝ p✝).drop (n✝ + 1)).darts = List.drop (n✝ + 1) (cons h✝ p✝).darts

Tactic:
simp [*, drop]

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

Goal state before:
pp: case nil.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ (nil.drop 0).edges = List.drop 0 nil.edges

Tactic:
simp [*, drop]

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

Goal state before:
pp: case nil.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ (nil.drop (n✝ + 1)).edges = List.drop (n✝ + 1) nil.edges

Tactic:
simp [*, drop]

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

Goal state before:
pp: case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).edges = List.drop n p✝.edges
⊢ ((cons h✝ p✝).drop 0).edges = List.drop 0 (cons h✝ p✝).edges

Tactic:
simp [*, drop]

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

Goal state before:
pp: case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).edges = List.drop n p✝.edges
n✝ : ℕ
⊢ ((cons h✝ p✝).drop (n✝ + 1)).edges = List.drop (n✝ + 1) (cons h✝ p✝).edges

Tactic:
simp [*, drop]

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

Goal state before:
pp: case nil.zero
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ (nil.drop 0).support = List.drop (min 0 nil.length) nil.support

Tactic:
simp [*, drop]

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

Goal state before:
pp: case nil.succ
V : Type u
G : SimpleGraph V
u v u✝ : V
n✝ : ℕ
⊢ (nil.drop (n✝ + 1)).support = List.drop (min (n✝ + 1) nil.length) nil.support

Tactic:
simp [*, drop]

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

Goal state before:
pp: case cons.zero
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).support = List.drop (min n p✝.length) p✝.support
⊢ ((cons h✝ p✝).drop 0).support = List.drop (min 0 (cons h✝ p✝).length) (cons h✝ p✝).support

Tactic:
simp [*, drop]

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

Goal state before:
pp: case cons.succ
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), (p✝.drop n).support = List.drop (min n p✝.length) p✝.support
n✝ : ℕ
⊢ ((cons h✝ p✝).drop (n✝ + 1)).support = List.drop (min (n✝ + 1) (cons h✝ p✝).length) (cons h✝ p✝).support

Tactic:
simp [*, drop]

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
G : SimpleGraph α
s : Set α
f : α ↪ β
hs : s.Subsingleton
⊢ (s.Subsingleton ∨ ∃ s_1, G.IsClique s_1 ∧ ⇑f '' s_1 = ⇑f '' s) ↔ G.IsClique s

pp: case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
s : Set α
f : α ↪ β
hs : s.Nontrivial
⊢ (s.Subsingleton ∨ ∃ s_1, G.IsClique s_1 ∧ ⇑f '' s_1 = ⇑f '' s) ↔ G.IsClique s

Tactic:
· simp [hs, IsClique.of_subsingleton]

Goal state after:
case inr
α : Type u_1
β : Type u_2
G : SimpleGraph α
s : Set α
f : α ↪ β
hs : s.Nontrivial
⊢ (s.Subsingleton ∨ ∃ s_1, G.IsClique s_1 ∧ ⇑f '' s_1 = ⇑f '' s) ↔ G.IsClique s
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
t : Finset β
ht : #t ≤ 1
⊢ (SimpleGraph.map (⇑f) G).IsClique ↑t

Tactic:
exact IsClique.of_subsingleton <| card_le_one.1 ht

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.LocallyLinear
⊢ ∀ ⦃x y : β⦄, (SimpleGraph.map (⇑f) G).Adj x y → ∃ s, (SimpleGraph.map (⇑f) G).IsNClique 3 s ∧ x ∈ s ∧ y ∈ s

Tactic:
rintro _ _ ⟨-, a, b, h, rfl, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
G : SimpleGraph α
f : α ↪ β
hG : G.LocallyLinear
a b : α
h : G.Adj a b
⊢ ∃ s, (SimpleGraph.map (⇑f) G).IsNClique 3 s ∧ f a ∈ s ∧ f b ∈ s
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h : G.Adj u✝ v✝
q : G.Walk v✝ w✝
ih : Set.InjOn q.getVert {i | i ≤ q.length} → q.IsPath
⊢ Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length} → (cons h q).IsPath

Tactic:
intro hinj
    rw [cons_isPath_iff]
    refine ⟨ih (by
      intro n hn m hm hnm
      simp only [Set.mem_ofPred_eq] at hn hm
      have := hinj
        (by rw [length_cons]; lia : n + 1 ≤ (q.cons h).length)
        (by rw [length_cons]; lia : m + 1 ≤ (q.cons h).length)
        (by simpa [getVert_cons] using hnm)
      lia), fun h' => ?_⟩
    obtain ⟨n, ⟨hn, hnl⟩⟩ := mem_support_iff_exists_getVert.mp h'
    have := hinj
      (by rw [length_cons]; lia : (n + 1) ≤ (q.cons h).length)
      (by lia : 0 ≤ (q.cons h).length)
      (by rwa [getVert_cons _ _ n.add_one_ne_zero, getVert_zero])
    lia

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

Goal state before:
pp: case refine_1
V : Type u
G : SimpleGraph V
u v✝¹ : V
p✝ : G.Walk u v✝¹
v v✝ : V
hadj : G.Adj u v✝
p : G.Walk v✝ v
ht : (cons hadj p).IsTrail
h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk (cons hadj p) → ¬w.IsCycle
hp : p.IsPath
hup : u ∈ p.support
⊢ (cons hadj (p.takeUntil u hup)).IsSubwalk (cons hadj p)

Tactic:
rw [isSubwalk_iff_support_isInfix, support_cons, support_cons]

Goal state after:
case refine_1
V : Type u
G : SimpleGraph V
u v✝¹ : V
p✝ : G.Walk u v✝¹
v v✝ : V
hadj : G.Adj u v✝
p : G.Walk v✝ v
ht : (cons hadj p).IsTrail
h : ∀ (v_1 : V) (w : G.Walk v_1 v_1), w.IsSubwalk (cons hadj p) → ¬w.IsCycle
hp : p.IsPath
hup : u ∈ p.support
⊢ u :: (p.takeUntil u hup).support <:+: u :: p.support
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
β : Type u_3
inst✝ : Fintype β
⊢ ¬G.CliqueFree (Fintype.card β) ↔ ¬⊤.Free G

Tactic:
not_free,

Goal state after:
α : Type u_1
G : SimpleGraph α
β : Type u_3
inst✝ : Fintype β
⊢ ¬G.CliqueFree (Fintype.card β) ↔ ⊤ ⊑ G
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : 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
mt : ∀ (x : Fin n), φ x ≠ t
| ∀ {a b : Fin n}, (G.replaceVertex s t).Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b

Tactic:
conv =>

Goal state after:
α : 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
mt : ∀ (x : Fin n), φ x ≠ t
a b : Fin n
| G.Adj (φ a) (φ b) ↔ (completeGraph (Fin n)).Adj a b
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case refine_2
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ ∀ b ∈ G.cliqueFinset 3, #(bipartiteBelow (fun e s ↦ e ∈ s.sym2) G.edgeFinset b) ≤ 3

Tactic:
simp only [mem_cliqueFinset_iff, is3Clique_iff, forall_exists_index, and_imp]

Goal state after:
case refine_2
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ ∀ (b : Finset α) (x x_1 x_2 : α),
    G.Adj x x_1 →
      G.Adj x x_2 → G.Adj x_1 x_2 → b = {x, x_1, x_2} → #(bipartiteBelow (fun e s ↦ e ∈ s.sym2) G.edgeFinset b) ≤ 3
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
p : G.Walk u u
hinj : Injective ⇑f
⊢ (Walk.map f p).IsCircuit ↔ p.IsCircuit

Tactic:
by
  rw [isCircuit_def, isCircuit_def, isTrail_map_iff_of_injective hinj, ne_eq, ne_eq, eq_nil_iff_nil,
    eq_nil_iff_nil, nil_map_iff]

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

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
p : G.Walk u u
hp : (Walk.map f p).IsCycle
⊢ p.IsCycle

Tactic:
rw [isCycle_def, ne_eq, eq_nil_iff_nil]

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u : V
p : G.Walk u u
hp : (Walk.map f p).IsCycle
⊢ p.IsTrail ∧ ¬p.Nil ∧ p.support.tail.Nodup