mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
G' : SimpleGraph W
⊢ G ≤ SimpleGraph.comap (⇑f) G' → SimpleGraph.map (⇑f) G ≤ G'

Tactic:
rintro h _ _ ⟨-, u, v, ha, rfl, rfl⟩

Goal state after:
V : Type u_1
W : Type u_2
f : V ↪ W
G : SimpleGraph V
G' : SimpleGraph W
h : G ≤ SimpleGraph.comap (⇑f) G'
u v : V
ha : G.Adj u v
⊢ G'.Adj (f u) (f v)
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
W : Type u_2
G' : SimpleGraph W
inst✝³ : Fintype V
inst✝² : DecidableRel G.Adj
inst✝¹ : Fintype W
inst✝ : DecidableRel G'.Adj
f : G ≃g G'
⊢ G.maxDegree = G'.maxDegree

Tactic:
classical
  have : (G'.degree ·) ∘ f = (G.degree ·) := funext (f.degree_eq ·)
  rw [maxDegree, maxDegree, ← this, ← image_image, Finset.image_univ_of_surjective f.surjective]

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

Goal state before:
pp: V : Type u_1
s : Set V
inst✝³ : DecidablePred fun x ↦ x ∈ s
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
⊢ map (Embedding.subtype fun x ↦ x ∈ s).sym2Map (induce s G).edgeFinset = G.edgeFinset ∩ s.toFinset.sym2

Tactic:
aesop (add simp [Finset.ext_iff, Sym2.exists, Sym2.forall, adj_comm])

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

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
a : α
P : Finpartition a
β : Type u_2
f : α → β
inst✝¹ : SemilatticeInf β
inst✝ : OrderBot β
hf : ∀ (x y : α), f (x ⊓ y) = f x ⊓ f y
hbot : f ⊥ = ⊥
x✝ : α
⊢ x✝ ∈ ↑P.parts → ∀ ⦃y : α⦄, y ∈ ↑P.parts → x✝ ≠ y → (Disjoint on f) x✝ y

Tactic:
hx

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
a : α
P : Finpartition a
β : Type u_2
f : α → β
inst✝¹ : SemilatticeInf β
inst✝ : OrderBot β
hf : ∀ (x y : α), f (x ⊓ y) = f x ⊓ f y
hbot : f ⊥ = ⊥
x✝ : α
hx : x✝ ∈ ↑P.parts
⊢ ∀ ⦃y : α⦄, y ∈ ↑P.parts → x✝ ≠ y → (Disjoint on f) x✝ y
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case pos
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
P✝ : Finpartition a
inst✝ : Decidable (a = ⊥)
P : Finpartition a
h : a = ⊥
x : α
⊢ x ∈ P.parts → ∃ c ∈ ((Finpartition.empty α).copy ⋯).parts, x ≤ c

Tactic:
hx

Goal state after:
case pos
α : Type u_1
inst✝² : Lattice α
inst✝¹ : OrderBot α
a : α
P✝ : Finpartition a
inst✝ : Decidable (a = ⊥)
P : Finpartition a
h : a = ⊥
x : α
hx : x ∈ P.parts
⊢ ∃ c ∈ ((Finpartition.empty α).copy ⋯).parts, x ≤ c
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a✝ b c : α
ι : Type u_2
I : Finset ι
a : ι → α
P : (i : ι) → Finpartition (a i)
ha : I.SupIndep a
⊢ I.SupIndep fun i ↦ (P i).parts.sup id

Tactic:
simpa only [sup_parts]

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
P : Finpartition univ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
⊢ stepBound #P.parts ≤ #P.parts * 16 ^ #P.parts

Tactic:
unfold stepBound; gcongr; simp

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
P : Finpartition s
a✝ : α
parts : Finset (Finset α)
h : ∀ p ∈ parts, p ⊆ s
h' : ∀ a ∈ s, ∃! t, t ∈ parts ∧ a ∈ t
h'' : ∅ ∉ parts
a : Finset α
ha : a ∈ ↑parts
b : Finset α
hb : b ∈ ↑parts
hab : a ≠ b
x : α
⊢ x ∈ id a → x ∉ id b

Tactic:
hx

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
P : Finpartition s
a✝ : α
parts : Finset (Finset α)
h : ∀ p ∈ parts, p ⊆ s
h' : ∀ a ∈ s, ∃! t, t ∈ parts ∧ a ∈ t
h'' : ∅ ∉ parts
a : Finset α
ha : a ∈ ↑parts
b : Finset α
hb : b ∈ ↑parts
hab : a ≠ b
x : α
hx : x ∈ id a
⊢ x ∉ id b
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n : ℤ
i : EInt
h : WithBotTop.coe n ≤ i
X : C
⊢ t.IsGE ((t.eTruncGE.obj i).obj X) n

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

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

Goal state before:
pp: case inl
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : ℕ
P : Finpartition s
hs : a * 0 + b * (0 + 1) = #s
⊢ ∀ x ∈ P.parts, #(x \ {y ∈ ⊥.parts | y ⊆ x}.biUnion id) ≤ 0

Tactic:
simp only [le_zero_iff, card_eq_zero, mem_biUnion, mem_filter, id,
      and_assoc, sdiff_eq_empty_iff_subset, subset_iff]

Goal state after:
case inl
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a b : ℕ
P : Finpartition s
hs : a * 0 + b * (0 + 1) = #s
⊢ ∀ x ∈ P.parts, ∀ ⦃x_1 : α⦄, x_1 ∈ x → ∃ a ∈ ⊥.parts, (∀ ⦃x_2 : α⦄, x_2 ∈ a → x_2 ∈ x) ∧ x_1 ∈ a
Module: Mathlib.Combinatorics.SimpleGraph.Density

Goal state before:
pp: α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
t : Finset β
⊢ interedges r ∅ t = ∅

Tactic:
by
  rw [interedges, Finset.empty_product, filter_empty]

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 s' : Finset α
hs : ∀ ⦃a : α⦄, a ∈ s → a ∉ s'
t : Finset β
a✝ : α × β
⊢ a✝ ∈ interedges r s t → a✝ ∉ interedges r s' t

Tactic:
hx

Goal state after:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s s' : Finset α
hs : ∀ ⦃a : α⦄, a ∈ s → a ∉ s'
t : Finset β
a✝ : α × β
hx : a✝ ∈ interedges r s t
⊢ a✝ ∉ interedges r s' t
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 t' : Finset β
ht : ∀ ⦃a : β⦄, a ∈ t → a ∉ t'
a✝ : α × β
⊢ a✝ ∈ interedges r s t → a✝ ∉ interedges r s t'

Tactic:
hx

Goal state after:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t t' : Finset β
ht : ∀ ⦃a : β⦄, a ∈ t → a ∉ t'
a✝ : α × β
hx : a✝ ∈ interedges r s t
⊢ a✝ ∉ interedges r s t'
Module: Mathlib.Combinatorics.SimpleGraph.Density

Goal state before:
pp: ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset ι
t : Finset κ
f : ι → Finset α
g : κ → Finset β
⊢ interedges r (s.biUnion f) (t.biUnion g) = (s ×ˢ t).biUnion fun ab ↦ interedges r (f ab.1) (g ab.2)

Tactic:
product_biUnion,

Goal state after:
ι : Type u_2
κ : Type u_3
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝² : (a : α) → DecidablePred (r a)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Finset ι
t : Finset κ
f : ι → Finset α
g : κ → Finset β
⊢ interedges r (s.biUnion f) (t.biUnion g) = s.biUnion fun a ↦ t.biUnion fun b ↦ interedges r (f a) (g b)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: case inl
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
a b : α
hε : 0 < ε
t' : Finset α
ht' : t' ⊆ {b}
ht : ε ≤ ↑(#t')
hs' : ∅ ⊆ {a}
hs : ε ≤ ↑(#∅)
⊢ |↑(G.edgeDensity ∅ t') - ↑(G.edgeDensity {a} {b})| < ε

pp: case inr
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
a b : α
hε : 0 < ε
t' : Finset α
ht' : t' ⊆ {b}
ht : ε ≤ ↑(#t')
hs' : {a} ⊆ {a}
hs : ε ≤ ↑(#{a})
⊢ |↑(G.edgeDensity {a} t') - ↑(G.edgeDensity {a} {b})| < ε

Tactic:
· replace hs : ε ≤ 0 := by simpa using hs
    exact (hε.not_ge hs).elim

Goal state after:
case inr
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
a b : α
hε : 0 < ε
t' : Finset α
ht' : t' ⊆ {b}
ht : ε ≤ ↑(#t')
hs' : {a} ⊆ {a}
hs : ε ≤ ↑(#{a})
⊢ |↑(G.edgeDensity {a} t') - ↑(G.edgeDensity {a} {b})| < ε
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: case inr
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
a b : α
hε : 0 < ε
t' : Finset α
ht' : t' ⊆ {b}
ht : ε ≤ ↑(#t')
hs' : {a} ⊆ {a}
hs : ε ≤ ↑(#{a})
⊢ |↑(G.edgeDensity {a} t') - ↑(G.edgeDensity {a} {b})| < ε

Tactic:
obtain rfl | rfl := Finset.subset_singleton_iff.1 ht'

Goal state after:
case inr.inl
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
a b : α
hε : 0 < ε
hs' : {a} ⊆ {a}
hs : ε ≤ ↑(#{a})
ht' : ∅ ⊆ {b}
ht : ε ≤ ↑(#∅)
⊢ |↑(G.edgeDensity {a} ∅) - ↑(G.edgeDensity {a} {b})| < ε

case inr.inr
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
a b : α
hε : 0 < ε
hs' : {a} ⊆ {a}
hs : ε ≤ ↑(#{a})
ht' : {b} ⊆ {b}
ht : ε ≤ ↑(#{b})
⊢ |↑(G.edgeDensity {a} {b}) - ↑(G.edgeDensity {a} {b})| < ε
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
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
⊢ ↑(#(P.parts.biUnion offDiag)) ≤ ε / 2 * ↑(#A) ^ 2

Tactic:
obtain rfl | hA : A = ⊥ ∨ _ := A.eq_empty_or_nonempty
  · simp [Subsingleton.elim P ⊥]
  apply hP.card_biUnion_offDiag_le'.trans
  rw [div_le_iff₀ (Nat.cast_pos.2 (P.parts_nonempty hA.ne_empty).card_pos)]
  have : (#A : 𝕜) + #P.parts ≤ 2 * #A := by
    rw [two_mul]; gcongr; exact P.card_parts_le_card
  refine (mul_le_mul_of_nonneg_left this <| by positivity).trans ?_
  suffices 1 ≤ ε / 4 * #P.parts by
    rw [mul_left_comm, ← sq]
    convert! mul_le_mul_of_nonneg_left this (mul_nonneg zero_le_two <| sq_nonneg (#A : 𝕜)) using 1
      <;> ring
  rwa [← div_le_iff₀', one_div_div]
  positivity

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

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

Tactic:
hx

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ Function.Injective fun G' ↦ (G'.verts, G'.spanningCoe)

Tactic:
intro G₁ G₂ h

Goal state after:
V : Type u
G : SimpleGraph V
G₁ G₂ : G.Subgraph
h : (fun G' ↦ (G'.verts, G'.spanningCoe)) G₁ = (fun G' ↦ (G'.verts, G'.spanningCoe)) G₂
⊢ G₁ = G₂
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: 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 : ⊤.Copy G
v w : α
h : G.Adj (f.toEmbedding v) (f.toEmbedding w)
⊢ ⊤.Adj v w

Tactic:
by simpa using h.ne

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
i : ℕ
⊢ p.getVert i ∈ p.support

Tactic:
induction p generalizing i <;> cases i <;> simp [*]

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
s✝ s' s : Set V
h : s ⊆ G'.verts
x✝ : ↑(G'.induce s).verts
v : V
hv : v ∈ (G'.induce s).verts
⊢ ⟨v, ⋯⟩ ∈ {v | ↑v ∈ s}

Tactic:
simp at hv

Goal state after:
ι : Sort u_1
V : Type u
W : Type v
G : SimpleGraph V
G' G'' : G.Subgraph
s✝ s' s : Set V
h : s ⊆ G'.verts
x✝ : ↑(G'.induce s).verts
v : V
hv✝ : v ∈ (G'.induce s).verts
hv : v ∈ s
⊢ ⟨v, ⋯⟩ ∈ {v | ↑v ∈ s}
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hnil : ¬p.Nil
⊢ 1 < p.support.length

Tactic:
grind [not_nil_iff_lt_length]

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
hm : m ≠ 0
⊢ #(chunk hP G ε hU).parts = 4 ^ #P.parts

Tactic:
by
  unfold chunk
  split_ifs
  · rw [card_parts_equitabilise _ _ hm, tsub_add_cancel_of_le]
    exact le_of_lt a_add_one_le_four_pow_parts_card
  · rw [card_parts_equitabilise _ _ hm, tsub_add_cancel_of_le a_add_one_le_four_pow_parts_card]

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

Goal state before:
pp: case nil.nil
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Function.Injective ⇑f
u v u✝ : V
h : Walk.map f nil = Walk.map f nil
⊢ nil = nil

Tactic:
simp at h ⊢

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

Goal state before:
pp: case nil.cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
hinj : Function.Injective ⇑f
u v u✝ v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ u✝
h : Walk.map f nil = Walk.map f (cons h✝ p✝)
⊢ nil = cons h✝ p✝

Tactic:
simp at h ⊢

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
q : G.Walk v w
i : ℕ
⊢ (p.append q).getVert i = if i < p.length then p.getVert i else q.getVert (i - p.length)

Tactic:
induction p generalizing i <;> cases i <;> simp [*]

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
q : G.Walk v w
i : ℕ
⊢ (p.append q).getVert i = if i ≤ p.length then p.getVert i else q.getVert (i - p.length)

Tactic:
induction p generalizing i <;> cases i <;> simp [*]

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

Goal state before:
pp: case cons.cons
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u✝ v✝¹ w✝ : V
h✝¹ : G.Adj u✝ v✝¹
p✝¹ : G.Walk v✝¹ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : G.Walk v✝¹ v'}, p✝¹.concat h = p'.concat h' → ∃ (hv : w✝ = v'), p✝¹.copy ⋯ hv = p'
h : G.Adj w✝ w
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ v'
he : cons h✝¹ (p✝¹.concat h) = cons h✝ (p✝.concat h')
⊢ ∃ (hv : w✝ = v'), (cons h✝¹ p✝¹).copy ⋯ hv = cons h✝ p✝

Tactic:
cons.injEq

Goal state after:
case cons.cons
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
u✝ v✝¹ w✝ : V
h✝¹ : G.Adj u✝ v✝¹
p✝¹ : G.Walk v✝¹ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : G.Walk v✝¹ v'}, p✝¹.concat h = p'.concat h' → ∃ (hv : w✝ = v'), p✝¹.copy ⋯ hv = p'
h : G.Adj w✝ w
v✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ v'
he : v✝¹ = v✝ ∧ p✝¹.concat h ≍ p✝.concat h'
⊢ ∃ (hv : w✝ = v'), (cons h✝¹ p✝¹).copy ⋯ hv = cons h✝ p✝
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
p : G.Walk u v
h : w ∈ p.support
⊢ (p.dropUntil w h).support = ((p.drop (List.idxOf w p.support)).copy ⋯ ⋯).support

Tactic:
induction p with
  | nil =>
    simp only [dropUntil, eq_mpr_eq_cast, support_nil, getVert_nil, drop, support_copy]
    grind [mem_support_nil_iff, support_nil]
  | @cons a _ _ _ p ih =>
    by_cases! h' : w = a
    · subst h'
      simp [dropUntil_first]
    · rw [drop_cons_eq _ _ _ (by grind), support_copy, dropUntil]
      grind

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

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p₁ : G.Walk u v
p₂ : G.Walk u' v'
hnil : ¬p₁.Nil
x✝ :
  ∃ k, p₁.darts.length + k ≤ p₂.darts.length ∧ ∀ (i : ℕ) (h : i < p₁.darts.length), p₂.darts[i + k]? = some p₁.darts[i]
k : ℕ
hk : p₁.darts.length + k ≤ p₂.darts.length
h : ∀ (i : ℕ) (h : i < p₁.darts.length), p₂.darts[i + k]? = some p₁.darts[i]
i : ℕ
hi : i < p₁.support.length
hi' : i = p₁.length
⊢ p₂.support[i + k] = p₁.support[i]

Tactic:
have := h <| i - 1
      grind [not_nil_iff_lt_length, snd_darts_getElem]

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
q : G.Walk v w
⊢ (p.append q).Nil ↔ p.Nil ∧ q.Nil

Tactic:
cases p <;> cases q <;> simp

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
hc : (G ⊔ edge v w).IsClique s
x✝ : α
⊢ x✝ ∈ s \ {v} → ∀ ⦃y : α⦄, y ∈ s \ {v} → x✝ ≠ y → G.Adj x✝ y

Tactic:
hx

Goal state after:
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
hc : (G ⊔ edge v w).IsClique s
x✝ : α
hx : x✝ ∈ s \ {v}
⊢ ∀ ⦃y : α⦄, y ∈ s \ {v} → x✝ ≠ y → G.Adj x✝ y
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
h : v ≠ w
hv : G.IsClique (s \ {v})
hw : G.IsClique (s \ {w})
x : α
⊢ x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → (G ⊔ edge v w).Adj x y

Tactic:
hx

Goal state after:
α : Type u_1
G : SimpleGraph α
v w : α
s : Set α
h : v ≠ w
hv : G.IsClique (s \ {v})
hw : G.IsClique (s \ {w})
x : α
hx : x ∈ s
⊢ ∀ ⦃y : α⦄, y ∈ s → x ≠ y → (G ⊔ edge v w).Adj x y
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case mp.inl.inl
α : Type u_1
G : SimpleGraph α
b d e : α
hde : G.Adj d e
hab : b ≠ b
hcd : G.Adj b d
hce : G.Adj b e
⊢ G.Adj b b ∧ ∃ c, G.Adj b c ∧ G.Adj b c ∧ {b, d, e} = {b, b, c}

Tactic:
simp only [*, adj_comm, true_and, Ne, not_true] at *

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

Goal state before:
pp: case mp.inl.inr.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
e : α
hce : G.Adj a e
hde : G.Adj b e
hcd : G.Adj a b
⊢ G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {a, b, e} = {a, b, c}

Tactic:
simp only [*, adj_comm, true_and, Ne, not_true] at *

Goal state after:
case mp.inl.inr.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
e : α
hce : G.Adj a e
hde : G.Adj b e
hcd : G.Adj a b
⊢ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {a, b, e} = {a, b, c}
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case mp.inl.inr.inr
α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
d : α
hcd : G.Adj a d
hde : G.Adj d b
hce : G.Adj a b
⊢ G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {a, d, b} = {a, b, c}

Tactic:
simp only [*, adj_comm, true_and, Ne, not_true] at *

Goal state after:
case mp.inl.inr.inr
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
d : α
hcd : G.Adj a d
hce : G.Adj a b
hde : G.Adj b d
⊢ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {a, d, b} = {a, b, c}
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case mp.inr.inl.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
e : α
hde : G.Adj a e
hce : G.Adj b e
hcd : G.Adj b a
⊢ G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {b, a, e} = {a, b, c}

Tactic:
simp only [*, adj_comm, true_and, Ne, not_true] at *

Goal state after:
case mp.inr.inl.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
e : α
hde : G.Adj a e
hce : G.Adj b e
hcd : G.Adj a b
⊢ G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {b, a, e} = {a, b, c}
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case mp.inr.inl.inr.inl
α : Type u_1
G : SimpleGraph α
b c e : α
hce : G.Adj c e
hab : b ≠ b
hcd : G.Adj c b
hde : G.Adj b e
⊢ G.Adj b b ∧ ∃ c_1, G.Adj b c_1 ∧ G.Adj b c_1 ∧ {c, b, e} = {b, b, c_1}

Tactic:
simp only [*, adj_comm, true_and, Ne, not_true] at *

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

Goal state before:
pp: case mp.inr.inl.inr.inr
α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
c : α
hcd : G.Adj c a
hce : G.Adj c b
hde : G.Adj a b
⊢ G.Adj a b ∧ ∃ c_1, G.Adj a c_1 ∧ G.Adj b c_1 ∧ {c, a, b} = {a, b, c_1}

Tactic:
simp only [*, adj_comm, true_and, Ne, not_true] at *

Goal state after:
case mp.inr.inl.inr.inr
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
c : α
hde : G.Adj a b
hcd : G.Adj a c
hce : G.Adj b c
⊢ ∃ c_1, G.Adj a c_1 ∧ G.Adj b c_1 ∧ {c, a, b} = {a, b, c_1}
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case mp.inr.inr.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
d : α
hde : G.Adj d a
hcd : G.Adj b d
hce : G.Adj b a
⊢ G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {b, d, a} = {a, b, c}

Tactic:
simp only [*, adj_comm, true_and, Ne, not_true] at *

Goal state after:
case mp.inr.inr.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
d : α
hcd : G.Adj b d
hde : G.Adj a d
hce : G.Adj a b
⊢ G.Adj a b ∧ ∃ c, G.Adj a c ∧ G.Adj b c ∧ {b, d, a} = {a, b, c}
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case mp.inr.inr.inr.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : a ≠ b
c : α
hce : G.Adj c a
hcd : G.Adj c b
hde : G.Adj b a
⊢ G.Adj a b ∧ ∃ c_1, G.Adj a c_1 ∧ G.Adj b c_1 ∧ {c, b, a} = {a, b, c_1}

Tactic:
simp only [*, adj_comm, true_and, Ne, not_true] at *

Goal state after:
case mp.inr.inr.inr.inl
α : Type u_1
G : SimpleGraph α
a b : α
hab : ¬a = b
c : α
hce : G.Adj a c
hcd : G.Adj b c
hde : G.Adj a b
⊢ G.Adj a b ∧ ∃ c_1, G.Adj a c_1 ∧ G.Adj b c_1 ∧ {c, b, a} = {a, b, c_1}
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case mp.inr.inr.inr.inr
α : Type u_1
G : SimpleGraph α
b c d : α
hcd : G.Adj c d
hab : b ≠ b
hce : G.Adj c b
hde : G.Adj d b
⊢ G.Adj b b ∧ ∃ c_1, G.Adj b c_1 ∧ G.Adj b c_1 ∧ {c, d, b} = {b, b, c_1}

Tactic:
simp only [*, adj_comm, true_and, Ne, not_true] at *

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 V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
x y : Finset α
⊢ x ∈ A →
    y ∈ B →
      ↑(#(interedges G.Adj x y)) / (↑(#x) * ↑(#y) * (↑(#A) * ↑(#B))) ≤
        ↑(#(interedges G.Adj x y)) * ((1 + ε ^ 5 / 49) / (↑(#(A.sup id)) * ↑(#(B.sup id))))

Tactic:
hx

Goal state after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  (1 + ε ^ 5 / 49) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) ≤
    ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) + ε ^ 5 / 49
x y : Finset α
hx : x ∈ A
⊢ y ∈ B →
    ↑(#(interedges G.Adj x y)) / (↑(#x) * ↑(#y) * (↑(#A) * ↑(#B))) ≤
      ↑(#(interedges G.Adj x y)) * ((1 + ε ^ 5 / 49) / (↑(#(A.sup id)) * ↑(#(B.sup id))))