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

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

Tactic:
by
  constructor
  · rintro hdisj M' ⟨hsub₀, _⟩ ⟨hsub₁, _⟩
    rw [le_bot_iff]
    ext
    · grind [verts_bot]
    · exact ⟨(hdisj hsub₀ hsub₁ <| M'.edge_vert · :), False.elim⟩
  · intro hdisj S h₀ h₁ v hvS
    let M' : Subgraph G := { verts := {v}, Adj := ⊥, adj_sub := by simp, edge_vert := by simp }
    have hle {M : Subgraph G} (h : v ∈ M.verts) : M' ≤ M := by constructor <;> simp [h, M']
    exact hdisj (hle <| h₀ hvS) (hle <| h₁ hvS) |>.left <| Set.mem_singleton v

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

Goal state before:
pp: case mpr
α : Type u_4
β : Type u_5
A : SimpleGraph α
B : SimpleGraph β
H' : B.Subgraph
⊢ H' ∈ {B' | Nonempty (A ≃g B'.coe)} → H' ∈ Set.range toSubgraph

Tactic:
rintro ⟨e⟩

Goal state after:
case mpr
α : Type u_4
β : Type u_5
A : SimpleGraph α
B : SimpleGraph β
H' : B.Subgraph
e : A ≃g H'.coe
⊢ H' ∈ Set.range toSubgraph
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 \ fromEdgeSet (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})).Subgraph
hHG' : Nonempty (H ≃g G'.coe)
hG' : (Subgraph.map (Hom.ofLE ⋯) G').edgeSet.Nonempty
e : Sym2 ↑(Subgraph.map (Hom.ofLE ⋯) G').verts
he₀ : e ∈ (Subgraph.map (Hom.ofLE ⋯) G').coe.edgeSet
he₁ : Sym2.map Subtype.val e = hG'.some
e' : Sym2 ↑G'.verts :=
  Sym2.map
    (⇑((Copy.ofLE (G \ fromEdgeSet (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})) G ⋯).isoSubgraphMap G').symm) e
he' : e' ∈ Sym2.map Subtype.val ⁻¹' G'.edgeSet
this : Sym2.map Subtype.val e' ∈ (G \ fromEdgeSet (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})).edgeSet
⊢ False

Tactic:
simp only [edgeSet_sdiff, edgeSet_fromEdgeSet, edgeSet_sdiff_sdiff_isDiag, Set.mem_sdiff,
    Set.mem_iUnion, not_exists] at this

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
hH : H ≠ ⊥
G' : (G \ fromEdgeSet (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})).Subgraph
hHG' : Nonempty (H ≃g G'.coe)
hG' : (Subgraph.map (Hom.ofLE ⋯) G').edgeSet.Nonempty
e : Sym2 ↑(Subgraph.map (Hom.ofLE ⋯) G').verts
he₀ : e ∈ (Subgraph.map (Hom.ofLE ⋯) G').coe.edgeSet
he₁ : Sym2.map Subtype.val e = hG'.some
e' : Sym2 ↑G'.verts :=
  Sym2.map
    (⇑((Copy.ofLE (G \ fromEdgeSet (⋃ G', ⋃ (hG' : Nonempty (H ≃g G'.coe)), {⋯.some})) G ⋯).isoSubgraphMap G').symm) e
he' : e' ∈ Sym2.map Subtype.val ⁻¹' G'.edgeSet
this :
  Sym2.map Subtype.val e' ∈ G.edgeSet ∧
    ∀ (x : G.Subgraph) (x_1 : Nonempty (H ≃g x.coe)), Sym2.map Subtype.val e' ∉ {⋯.some}
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Operations

Goal state before:
pp: case inl
V : Type u_1
G : SimpleGraph V
v w : V
h : v = w
⊢ edge v w ≤ G ↔ v = w ∨ G.Adj v w

pp: case inr
V : Type u_1
G : SimpleGraph V
v w : V
h : v ≠ w
⊢ edge v w ≤ G ↔ v = w ∨ G.Adj v w

Tactic:
· simp [h]

Goal state after:
case inr
V : Type u_1
G : SimpleGraph V
v w : V
h : v ≠ w
⊢ edge v w ≤ G ↔ v = w ∨ G.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: case verts
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set (Sym2 V)
x✝ : V
⊢ x✝ ∈ ((G'.deleteEdges s).deleteEdges s').verts ↔ x✝ ∈ (G'.deleteEdges (s ∪ s')).verts

Tactic:
simp [and_assoc, not_or]

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

Goal state before:
pp: case Adj
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set (Sym2 V)
x✝¹ x✝ : V
⊢ ((G'.deleteEdges s).deleteEdges s').Adj x✝¹ x✝ ↔ (G'.deleteEdges (s ∪ s')).Adj x✝¹ x✝

Tactic:
simp [and_assoc, not_or]

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

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
hs : s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s
v' : V
hv' : v' ∈ G'.verts
w' : V
hw' : w' ∈ G'.verts
⊢ Sym2.Rel V (v', w') (v, w) → s(⟨v', hv'⟩, ⟨w', hw'⟩) ∉ s

Tactic:
rintro (_ | _)

Goal state after:
case mp.refl
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
hs : s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s
hv' : v ∈ G'.verts
hw' : w ∈ G'.verts
⊢ s(⟨v, hv'⟩, ⟨w, hw'⟩) ∉ s

case mp.swap
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s : Set (Sym2 ↑G'.verts)
v : V
hv : v ∈ G'.verts
w : V
hw : w ∈ G'.verts
a✝ : G'.Adj v w
hs : s(⟨v, hv⟩, ⟨w, hw⟩) ∉ s
hw' : v ∈ G'.verts
hv' : w ∈ G'.verts
⊢ s(⟨w, hv'⟩, ⟨v, hw'⟩) ∉ s
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Basic

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.support.Nodup
⊢ p.darts.Nodup

Tactic:
induction p with

Goal state after:
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 ∈ 𝒜
⊢ ↑(#s) ≤ ↑m + 1

Tactic:
exact mod_cast card_le_m_add_one_of_mem_chunk_parts (h𝒜 hs)

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.edges = List.zipWith (fun x1 x2 ↦ s(x1, x2)) p.support p.support.tail

Tactic:
induction p with

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

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

Tactic:
induction p with

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
hnil : ¬p.Nil
⊢ w ∈ p.support ↔ ∃ e ∈ p.edges, w ∈ e

Tactic:
induction p with

Goal state after:
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✝ v✝ w✝ : V
a : G.Adj u✝ v✝
p' : G.Walk v✝ w✝
ih : v✝ ∈ 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:
| cons a p' ih =>

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
S : Set V
uS : u ∈ S
vS : v ∉ S
⊢ ∃ d ∈ p.darts, d.toProd.1 ∈ S ∧ d.toProd.2 ∉ S

Tactic:
induction p with

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w x : V
p : G.Walk u v
q : G.Walk v w
r : G.Walk u x
⊢ (p.append q).reverseAux r = q.reverseAux (p.reverseAux r)

Tactic:
induction p with

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w x : V
p : G.Walk u v
q : G.Walk u w
r : G.Walk w x
⊢ (p.reverseAux q).append r = p.reverseAux (q.append r)

Tactic:
induction p with

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.reverse.reverse = p

Tactic:
induction p with

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 u w
⊢ (p.reverseAux q).length = p.length + q.length

Tactic:
induction p with

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
i : ℕ
⊢ p.reverse.getVert i = p.getVert (p.length - i)

Tactic:
induction p with

Goal state after:
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.takeUntil w h).support = ((p.take (List.idxOf w p.support)).copy ⋯ ⋯).support

Tactic:
induction p with

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
motive : (u v : V) → G.Walk u v → Sort u_1
Hnil : {u : V} → motive u u nil
Hconcat : {u v w : V} → (p : G.Walk u v) → (h : G.Adj v w) → motive u v p → motive u w (p.concat h)
u v w : V
p : G.Walk u v
h : G.Adj v w
⊢ concatRec Hnil Hconcat (p.concat h) = Hconcat p h (concatRec Hnil Hconcat p)

Tactic:
by
  simp only [concatRec]
  apply eq_of_heq (rec_heq_of_heq _ _)
  trans concatRecAux @Hnil @Hconcat (cons h.symm p.reverse)
  · congr
    simp
  · rw [concatRecAux, eqRec_heq_iff]
    congr <;> simp

Goal state after:
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

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v v' w : V
p : G.Walk u v
h : G.Adj v w
p' : G.Walk u v'
h' : G.Adj v' w
he : p.concat h = p'.concat h'
⊢ ∃ (hv : v = v'), p.copy ⋯ hv = p'

Tactic:
induction p with

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.reverse.support = p.support.reverse

Tactic:
by
  induction p <;> simp [support_append, *]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
x : V
⊢ List.count s(u, x) (p.takeUntil u h).edges ≤ 1

Tactic:
induction p with

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h✝¹ : G.Adj u' v'
h✝ : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h : (d.toProd.1, d.toProd.2) = (u', v') ∨ (d.toProd.1, d.toProd.2) = (u', v').swap
⊢ { fst := u', snd := v', adj := h✝¹ } ∈ p.darts ∨ { fst := v', snd := u', adj := ⋯ } ∈ p.darts

Tactic:
refine h.imp (fun h ↦ ?_) (fun h ↦ ?_)
    <;> convert! hd using 2

Goal state after:
case e'_3
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h✝² : G.Adj u' v'
h✝¹ : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h✝ : (d.toProd.1, d.toProd.2) = (u', v') ∨ (d.toProd.1, d.toProd.2) = (u', v').swap
h : (d.toProd.1, d.toProd.2) = (u', v')
⊢ (u', v') = d.toProd

case e'_3
V : Type u_1
G : SimpleGraph V
u v u' v' : V
p : G.Walk u v
h✝² : G.Adj u' v'
h✝¹ : ∃ a ∈ p.darts, a.edge = s(u', v')
d : G.Dart
hd : d ∈ p.darts
h✝ : (d.toProd.1, d.toProd.2) = (u', v') ∨ (d.toProd.1, d.toProd.2) = (u', v').swap
h : (d.toProd.1, d.toProd.2) = (u', v').swap
⊢ (v', u') = d.toProd
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w u : V
inst✝ : DecidableEq V
x : V
p : G.Walk u v
q : G.Walk v w
hx : x ∈ p.support
⊢ (p.append q).takeUntil x ⋯ = p.takeUntil x hx

Tactic:
induction p with

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.support.Nodup
⊢ p.edges.Nodup

Tactic:
induction p with

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
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 :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ ↑(#(interedges G.Adj x y)) *
      ((1 - ε ^ 5 / 50) / (↑(#(A.sup id)) * ↑(#(B.sup id))) * (↑(#A) * ↑(#x) * (↑(#B) * ↑(#y)))) ≤
    ↑(#(G.interedges x y))

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
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 :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ 0 < ↑(#A) * ↑(#x) * (↑(#B) * ↑(#y))

Tactic:
· refine mul_le_of_le_one_right (cast_nonneg _) ?_
    rw [div_mul_eq_mul_div, ← mul_assoc, mul_assoc]
    refine div_le_one_of_le₀ ?_ (by positivity)
    refine (mul_le_mul_of_nonneg_right (one_sub_le_m_div_m_add_one_sq hPα hPε) ?_).trans ?_
    · exact_mod_cast _root_.zero_le
    rw [sq, mul_mul_mul_comm, mul_comm ((m : ℝ) / _), mul_comm ((m : ℝ) / _)]
    gcongr
    · apply le_sum_card_subset_chunk_parts hA hx
    · apply le_sum_card_subset_chunk_parts hB hy

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
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 :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ 0 < ↑(#A) * ↑(#x) * (↑(#B) * ↑(#y))
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : G.Adj p.penultimate v
⊢ p.dropLast.concat hp = p

Tactic:
induction p with

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

Goal state before:
pp: 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
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
n : ℕ
hn : n ≤ q.length
m : ℕ
hm : m ≤ q.length
hnm : q.getVert n = q.getVert m
⊢ n + 1 ≤ (cons h q).length

Tactic:
rw [length_cons]

Goal state after:
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
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
n : ℕ
hn : n ≤ q.length
m : ℕ
hm : m ≤ q.length
hnm : q.getVert n = q.getVert m
⊢ n + 1 ≤ q.length + 1
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: 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
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
n : ℕ
hn : n ≤ q.length
m : ℕ
hm : m ≤ q.length
hnm : q.getVert n = q.getVert m
⊢ m + 1 ≤ (cons h q).length

Tactic:
rw [length_cons]

Goal state after:
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
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
n : ℕ
hn : n ≤ q.length
m : ℕ
hm : m ≤ q.length
hnm : q.getVert n = q.getVert m
⊢ m + 1 ≤ q.length + 1
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: 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
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
h' : u✝ ∈ q.support
n : ℕ
hn : q.getVert n = u✝
hnl : n ≤ q.length
⊢ n + 1 ≤ (cons h q).length

Tactic:
rw [length_cons]

Goal state after:
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
hinj : Set.InjOn (cons h q).getVert {i | i ≤ (cons h q).length}
h' : u✝ ∈ q.support
n : ℕ
hn : q.getVert n = u✝
hnl : n ≤ q.length
⊢ n + 1 ≤ q.length + 1
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ Set.InjOn p.getVert {i | i ≤ p.length} → p.IsPath

Tactic:
induction p with

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

Goal state before:
pp: α : Type u_1
s : Finset α
⊢ (↑s).Subsingleton ↔ #s ≤ 1

Tactic:
exact card_le_one.symm

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
h : s(u, v) ∈ p.edges
⊢ p = ⋯.toWalk

Tactic:
apply p.ext_getVert_le_length <| by simp [hp.length_eq_one_of_mem_edges h]

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
h : s(u, v) ∈ p.edges
⊢ ∀ k ≤ p.length, p.getVert k = ⋯.toWalk.getVert k
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
p : G.Walk u v
⊢ p.bypass.IsPath

Tactic:
induction p with

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
p : G.Walk u v
⊢ p.bypass.support <+ p.support

Tactic:
induction p with

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
inst✝ : DecidableEq V
p : G.Walk u v
⊢ p.bypass.darts <+ p.darts

Tactic:
induction p with

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).IsTrail ∧ ¬(Walk.map f p).Nil
⊢ p.IsTrail ∧ ¬p.Nil

Tactic:
nil_map_iff

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).IsTrail ∧ ¬p.Nil
⊢ p.IsTrail ∧ ¬p.Nil
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
⊢ p.IsTrail ∧ ¬(Walk.map f p).Nil ↔ p.IsTrail ∧ ¬p.Nil

Tactic:
nil_map_iff

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
hinj : Injective ⇑f
⊢ p.IsTrail ∧ ¬p.Nil ↔ p.IsTrail ∧ ¬p.Nil
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
H : SimpleGraph V
p : G.Walk u v
hp : ∀ e ∈ p.edges, e ∈ H.edgeSet
pp : p.IsPath
⊢ (p.transfer H hp).IsPath

Tactic:
induction p with

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
hst : G.IsUniform ε s t
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
h₁ : ↑(#(G.badVertices ε s t)) ≤ ↑(#s) * ε
h₂ : ↑(#(G.badVertices ε s u)) ≤ ↑(#s) * ε
X' : Finset α := s \ (G.badVertices ε s t ∪ G.badVertices ε s u)
this :
  (X'.biUnion fun x ↦ image (fun x_1 ↦ (x, x_1)) (G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) ⊆
    {x ∈ s ×ˢ t ×ˢ u |
      match x with
      | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}
⊢ (1 - 2 * ε) * ε ^ 3 * ↑(#s) * ↑(#t) * ↑(#u) ≤ ↑(#X') * (ε ^ 3 * ↑(#t) * ↑(#u))

Tactic:
have := hst.pos.le

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
hst : G.IsUniform ε s t
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
usu : G.IsUniform ε s u
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
h₁ : ↑(#(G.badVertices ε s t)) ≤ ↑(#s) * ε
h₂ : ↑(#(G.badVertices ε s u)) ≤ ↑(#s) * ε
X' : Finset α := s \ (G.badVertices ε s t ∪ G.badVertices ε s u)
this✝ :
  (X'.biUnion fun x ↦ image (fun x_1 ↦ (x, x_1)) (G.interedges ({y ∈ t | G.Adj x y}) ({y ∈ u | G.Adj x y}))) ⊆
    {x ∈ s ×ˢ t ×ˢ u |
      match x with
      | (a, b, c) => G.Adj a b ∧ G.Adj a c ∧ G.Adj b c}
this : 0 ≤ ε
⊢ (1 - 2 * ε) * ε ^ 3 * ↑(#s) * ↑(#t) * ↑(#u) ≤ ↑(#X') * (ε ^ 3 * ↑(#t) * ↑(#u))
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
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm : 0 ≤ 1 - (↑m)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
⊢ (1 - ε / 10) * ↑(#(G.nonuniformWitness ε U V)) * ((1 - (↑m)⁻¹) / ↑(#U)) ≤
    ↑(#((star hP G ε hU V).biUnion id)) * ((1 - (↑m)⁻¹) / ↑(#U))

Tactic:
gcongr
      exact one_sub_eps_mul_card_nonuniformWitness_le_card_star hV hUV hunif hPε hε₁

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : ExplicitDisjoint t
x✝ : Finset (α ⊕ β ⊕ γ)
⊢ x✝ ∈ ↑(map toTriangle t) →
    ∀ ⦃y : Finset (α ⊕ β ⊕ γ)⦄, y ∈ ↑(map toTriangle t) → x✝ ≠ y → (fun x y ↦ (↑x ∩ ↑y).Subsingleton) x✝ y

Tactic:
simp only [Finset.coe_map, Set.mem_image, Finset.mem_coe, Prod.exists, Ne,
    forall_exists_index, and_imp]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : ExplicitDisjoint t
x✝ : Finset (α ⊕ β ⊕ γ)
⊢ ∀ (x : α) (x_1 : β) (x_2 : γ),
    (x, x_1, x_2) ∈ t →
      toTriangle (x, x_1, x_2) = x✝ →
        ∀ ⦃y : Finset (α ⊕ β ⊕ γ)⦄ (x : α) (x_3 : β) (x_4 : γ),
          (x, x_3, x_4) ∈ t → toTriangle (x, x_3, x_4) = y → ¬x✝ = y → (↑x✝ ∩ ↑y).Subsingleton
Module: Mathlib.Combinatorics.Additive.Dissociation

Goal state before:
pp: α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
a : α
ha : a ∈ s
b : α
⊢ Pi.single a 1 b = -1 ∨ Pi.single a 1 b = 0 ∨ Pi.single a 1 b = 1

Tactic:
obtain rfl | hab := eq_or_ne a b

Goal state after:
case inl
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
a : α
ha : a ∈ s
⊢ Pi.single a 1 a = -1 ∨ Pi.single a 1 a = 0 ∨ Pi.single a 1 a = 1

case inr
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
a : α
ha : a ∈ s
b : α
hab : a ≠ b
⊢ Pi.single a 1 b = -1 ∨ Pi.single a 1 b = 0 ∨ Pi.single a 1 b = 1
Module: Mathlib.Combinatorics.Additive.DoublingConst

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

Tactic:
by
  rw [mulConst, divConst, div_inv_eq_mul]

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
⊢ #({x ∈ univ ×ˢ t ×ˢ t | x.1.1 * x.2.1 = x.1.2 * x.2.2}) = #(univ ×ˢ t ×ˢ t)

Tactic:
let f : α × α × α → (α × α) × α × α := fun x => ((x.1 * x.2.2, x.1 * x.2.1), x.2)

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
t : Finset α
f : α × α × α → (α × α) × α × α := fun x ↦ ((x.1 * x.2.2, x.1 * x.2.1), x.2)
⊢ #({x ∈ univ ×ˢ t ×ˢ t | x.1.1 * x.2.1 = x.1.2 * x.2.2}) = #(univ ×ˢ t ×ˢ t)