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

Goal state before:
pp: A : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
⊢ schnirelmannDensity A = schnirelmannDensity B

Tactic:
schnirelmannDensity,

Goal state after:
A : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
⊢ ⨅ n, ↑(#({a ∈ Ioc 0 ↑n | a ∈ A})) / ↑↑n = schnirelmannDensity B
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ 𝓓 a 𝒜 → s.erase a ∈ 𝓓 a 𝒜

Tactic:
by
  simp_rw [mem_compression, erase_idem]
  refine Or.imp (fun h => ⟨h.2, h.2⟩) fun h => ?_
  rwa [erase_eq_of_notMem (insert_ne_self.1 <| ne_of_mem_of_not_mem h.2 h.1)]

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝³ : DistribLattice α
inst✝² : DecidableEq α
s t : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
ha : a ∉ lowerClosure ↑s ⊓ lowerClosure ↑t
⊢ a ∉ lowerClosure ↑(s ⊼ t)

Tactic:
rwa [coe_infs, lowerClosure_infs]

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: case refine_1
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 ↦ x1 ⊆ x2 := fun x x_1 ↦ Classical.dec ((fun x1 x2 ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ 𝒜
⊢ #s ≤ #(bipartiteBelow (fun x1 x2 ↦ x1 ⊆ x2) (∂ 𝒜) s)

Tactic:
← card_image_of_injOn s.erase_injOn

Goal state after:
case refine_1
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
r : ℕ
h𝒜 : Set.Sized r ↑𝒜
i : DecidableRel fun x1 x2 ↦ x1 ⊆ x2 := fun x x_1 ↦ Classical.dec ((fun x1 x2 ↦ x1 ⊆ x2) x x_1)
s : Finset α
hs : s ∈ 𝒜
⊢ #(image s.erase s) ≤ #(bipartiteBelow (fun x1 x2 ↦ x1 ⊆ x2) (∂ 𝒜) s)
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: 𝕜 : Type u_1
α : Type u_2
inst✝³ : Semifield 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
⊢ #(falling (Fintype.card α - Fintype.card α) 𝒜) ≤ 1 * (Fintype.card α).choose (Fintype.card α - Fintype.card α)

pp: 𝕜 : Type u_1
α : Type u_2
inst✝³ : Semifield 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
⊢ 0 < (Fintype.card α).choose (Fintype.card α - Fintype.card α)

Tactic:
· simpa only [Nat.sub_self, one_mul, Nat.choose_zero_right, falling] using
        Set.Sized.card_le (sized_falling 0 𝒜)

Goal state after:
𝕜 : Type u_1
α : Type u_2
inst✝³ : Semifield 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
⊢ 0 < (Fintype.card α).choose (Fintype.card α - Fintype.card α)
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : 𝓒 U V 𝒜 ≠ 𝒜
⊢ familyMeasure (𝓒 U V 𝒜) < familyMeasure 𝒜

Tactic:
rw [compression] at a ⊢

Goal state after:
n : ℕ
U V : Finset (Fin n)
hU : U.Nonempty
hV : V.Nonempty
h : U.max' hU < V.max' hV
𝒜 : Finset (Finset (Fin n))
a : {a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜} ≠ 𝒜
⊢ familyMeasure ({a ∈ 𝒜 | compress U V a ∈ 𝒜} ∪ {a ∈ image (compress U V) 𝒜 | a ∉ 𝒜}) < familyMeasure 𝒜
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: α : Type u_1
c : Set (Set α)
H : ∀ (a : α), ∃! b, b ∈ c ∧ a ∈ b
x _y : α
h : ∀ s ∈ c, x ∈ s → _y ∈ s
s : Set α
hs : s ∈ c
hy : _y ∈ s
⊢ x ∈ s

Tactic:
by
    obtain ⟨t, ⟨ht, hx⟩, _⟩ := H x
    rwa [eq_of_mem_eqv_class H hs hy ht (h t ht hx)]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
W : G.Walk u v
⊢ ∃ p, p.IsPath

Tactic:
exact ⟨_, Path.isPath W.toPath⟩

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
H : G.Subgraph
hr : G.Reachable u v
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
hu : u ∈ H.verts
⊢ v ∈ H.verts

Tactic:
by
  let rec aux {v' : V} (hv' : v' ∈ H.verts) (p : G.Walk v' v) : v ∈ H.verts := by
    by_cases hnp : p.Nil
    · exact hnp.eq ▸ hv'
    exact aux (H.edge_vert (h _ hv' _ (Walk.adj_snd hnp)).symm) p.tail
  termination_by p.length
  decreasing_by {
    rw [← Walk.length_tail_add_one hnp]
    lia
  }
  exact aux hu hr.some

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
inst✝ : Fintype ↑(G.neighborSet v)
huv : u ≠ v
hu : G.degree v = 0
⊢ ¬G.Reachable u v

Tactic:
rw [reachable_comm]
  exact not_reachable_of_left_degree_zero huv.symm hu

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case refine_2
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
A B : Finset (Fin n)
hA : A ⊆ range'k ∧ #A = r
HB₁ : toColex B < toColex A
HB₂ : #B = r
t : Fin n
ht : t ∈ B
⊢ t ∈ range'k

Tactic:
rw [mem_attachFin, mem_range]

Goal state after:
case refine_2
n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
A B : Finset (Fin n)
hA : A ⊆ range'k ∧ #A = r
HB₁ : toColex B < toColex A
HB₂ : #B = r
t : Fin n
ht : t ∈ B
⊢ ↑t < k
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
ι : Type u_1
α✝ : Type u_2
β✝ : Type u_3
C✝ : G.Coloring α✝
α : Type u_4
β : Type u_5
f : α ≃ β
C : G.Coloring β
⊢ (G.recolorOfEmbedding f.toEmbedding) ((G.recolorOfEmbedding f.symm.toEmbedding) C) = C

Tactic:
ext v
    apply Equiv.apply_symm_apply

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
hne : u ≠ v
h : G.IsEdgeReachable 2 u v
⊢ ∃ w, G.Adj u w ∧ G.IsEdgeReachable 2 u w

Tactic:
by
  obtain ⟨w, hw⟩ := h.reachable (by simp) |>.exists_isPath
  have : G.Adj u w.snd := Walk.adj_snd (by grind [Walk.not_nil_of_ne])
  refine ⟨w.snd, this, fun s hs ↦ ?_⟩
  by_cases! h' : s = {s(u, w.snd)}
  · subst h'
    refine Reachable.trans (h hs) <| w.tail.toDeleteEdge _ (fun hh ↦ ?_) |>.reachable.symm
    have := hw.tail.eq_snd_of_mem_edges (Sym2.eq_swap ▸ hh)
    simp only [Walk.getVert_tail, Nat.reduceAdd] at this
    simpa using hw.getVert_eq_start_iff_of_not_nil (Walk.not_nil_of_ne hne) |>.mp this.symm
  · refine Walk.reachable <| Walk.cons (deleteEdges_adj.mpr ⟨this, ?_⟩) Walk.nil
    contrapose h'
    refine (Set.subsingleton_iff_singleton h').mp ?_
    exact Set.encard_le_one_iff_subsingleton.mp (Order.le_of_lt_succ hs)

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
inst✝ : Nontrivial ↑H.verts
h : H.Preconnected
v : ↑H.verts
⊢ ∃ u, H.Adj (↑v) u

Tactic:
by
  have := h.coe.exists_adj_of_nontrivial v
  tauto

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

Goal state before:
pp: case cons.e_a
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : p✝.reverse.toSubgraph = p✝.toSubgraph
⊢ G.subgraphOfAdj h✝ ⊔ G.singletonSubgraph u✝ = G.subgraphOfAdj h✝

Tactic:
ext <;> simp [-Set.bot_eq_empty]

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

Goal state before:
pp: W₁ : Type u_2
W₂ : Type u_3
⊢ (completeBipartiteGraph W₁ W₂).edgeSet.encard = ENat.card W₁ * ENat.card W₂

Tactic:
rw [edgeSet_completeBipartiteGraph, ← ENat.card_prod, ← Set.encard_univ, ← Set.image_univ]
  exact Function.Injective.encard_image (by grind [Function.Injective]) Set.univ

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.IsPath
hnp : ¬p.Nil
⊢ 0 < p.length

Tactic:
exact
        Walk.not_nil_iff_lt_length.mp hnp

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

Goal state before:
pp: case inl.inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v v' : V
w w' : W
f : G →g G'
g : H →g H'
val✝¹ val✝ : V
⊢ (G ⊕g H).Adj (Sum.inl val✝¹) (Sum.inl val✝) →
    (G' ⊕g H').Adj (Sum.map (⇑f) (⇑g) (Sum.inl val✝¹)) (Sum.map (⇑f) (⇑g) (Sum.inl val✝))

Tactic:
simp_all [f.map_rel, g.map_rel]

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

Goal state before:
pp: case inl.inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v v' : V
w w' : W
f : G →g G'
g : H →g H'
val✝¹ : V
val✝ : W
⊢ (G ⊕g H).Adj (Sum.inl val✝¹) (Sum.inr val✝) →
    (G' ⊕g H').Adj (Sum.map (⇑f) (⇑g) (Sum.inl val✝¹)) (Sum.map (⇑f) (⇑g) (Sum.inr val✝))

Tactic:
simp_all [f.map_rel, g.map_rel]

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

Goal state before:
pp: case inr.inl
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v v' : V
w w' : W
f : G →g G'
g : H →g H'
val✝¹ : W
val✝ : V
⊢ (G ⊕g H).Adj (Sum.inr val✝¹) (Sum.inl val✝) →
    (G' ⊕g H').Adj (Sum.map (⇑f) (⇑g) (Sum.inr val✝¹)) (Sum.map (⇑f) (⇑g) (Sum.inl val✝))

Tactic:
simp_all [f.map_rel, g.map_rel]

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

Goal state before:
pp: case inr.inr
U : Type u_1
U' : Type u_2
V : Type u_3
V' : Type u_4
W : Type u_5
W' : Type u_6
γ : Type u_7
G : SimpleGraph V
H : SimpleGraph W
I : SimpleGraph U
G' : SimpleGraph V'
H' : SimpleGraph W'
I' : SimpleGraph U'
v v' : V
w w' : W
f : G →g G'
g : H →g H'
val✝¹ val✝ : W
⊢ (G ⊕g H).Adj (Sum.inr val✝¹) (Sum.inr val✝) →
    (G' ⊕g H').Adj (Sum.map (⇑f) (⇑g) (Sum.inr val✝¹)) (Sum.map (⇑f) (⇑g) (Sum.inr val✝))

Tactic:
simp_all [f.map_rel, g.map_rel]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
s : Set V
⊢ (⊤.induce s).coe.Connected ↔ (⊤.induce s).Connected

Tactic:
← Subgraph.connected_iff'

Goal state after:
V : Type u
G : SimpleGraph V
s : Set V
⊢ (⊤.induce s).Connected ↔ (⊤.induce s).Connected
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : H.Free G
⊢ #G.edgeFinset ≤ {G | H.Free G}.sup fun x ↦ #x.edgeFinset

Tactic:
convert! @le_sup _ _ _ _ {G | H.Free G} (#·.edgeFinset) G (by simpa using h)

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

Goal state before:
pp: case refine_1
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h✝ : n₁ = n₂
e : H₁ ≃g H₂
G : SimpleGraph (Fin n₂)
inst✝ : DecidableRel G.Adj
h : H₁.Free G
⊢ #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n₂)) H₂

Tactic:
apply card_edgeFinset_le_extremalNumber

Goal state after:
case refine_1
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h✝ : n₁ = n₂
e : H₁ ≃g H₂
G : SimpleGraph (Fin n₂)
inst✝ : DecidableRel G.Adj
h : H₁.Free G
⊢ H₂.Free G
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: case refine_2
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h✝ : n₁ = n₂
e : H₂ ≃g H₁
G : SimpleGraph (Fin n₂)
inst✝ : DecidableRel G.Adj
h : H₂.Free G
⊢ #G.edgeFinset ≤ extremalNumber (Fintype.card (Fin n₂)) H₁

Tactic:
apply card_edgeFinset_le_extremalNumber

Goal state after:
case refine_2
n₁ n₂ : ℕ
W₁ : Type u_4
W₂ : Type u_5
H₁ : SimpleGraph W₁
H₂ : SimpleGraph W₂
h✝ : n₁ = n₂
e : H₂ ≃g H₁
G : SimpleGraph (Fin n₂)
inst✝ : DecidableRel G.Adj
h : H₂.Free G
⊢ H₁.Free G
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: case inl
α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h✝ : A.IsAdjMatrix
v w : V
h : A v w = 0
⊢ ⋯.toGraph.Adj v w ↔ h✝.toGraphᶜ.Adj v w

Tactic:
by_cases hvw : v = w

Goal state after:
case pos
α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h✝ : A.IsAdjMatrix
v w : V
h : A v w = 0
hvw : v = w
⊢ ⋯.toGraph.Adj v w ↔ h✝.toGraphᶜ.Adj v w

case neg
α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h✝ : A.IsAdjMatrix
v w : V
h : A v w = 0
hvw : ¬v = w
⊢ ⋯.toGraph.Adj v w ↔ h✝.toGraphᶜ.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.AdjMatrix

Goal state before:
pp: case inr
α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h✝ : A.IsAdjMatrix
v w : V
h : A v w = 1
⊢ ⋯.toGraph.Adj v w ↔ h✝.toGraphᶜ.Adj v w

Tactic:
by_cases hvw : v = w

Goal state after:
case pos
α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h✝ : A.IsAdjMatrix
v w : V
h : A v w = 1
hvw : v = w
⊢ ⋯.toGraph.Adj v w ↔ h✝.toGraphᶜ.Adj v w

case neg
α : Type u_1
V : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq V
A : Matrix V V α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
h✝ : A.IsAdjMatrix
v w : V
h : A v w = 1
hvw : ¬v = w
⊢ ⋯.toGraph.Adj v w ↔ h✝.toGraphᶜ.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
h : H.Free G
v : V
⊢ #(induce {v}ᶜ G).edgeFinset ≤ extremalNumber (Fintype.card ↑{v}ᶜ) H

Tactic:
apply card_edgeFinset_le_extremalNumber

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
h : H.Free G
v : V
⊢ H.Free (induce {v}ᶜ G)
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: case w
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
v : V
inst✝ : Fintype ↑(G.neighborSet v)
hdeg : G.degree v = 1
u : V
adj_vu : G.Adj v u
hu : ∀ (y : V), (fun w ↦ G.Adj v w) y → y = u
w x : ↑{v}ᶜ
pwu : G.Walk (↑w) u
hpwu : pwu.IsPath
pux : G.Walk u ↑x
hpux : pux.IsPath
z : V
hz : z ∈ (↑(pwu.append pux).toPath).support
⊢ z ∈ {v}ᶜ

Tactic:
rw [Set.mem_compl_iff, Set.mem_singleton_iff]

Goal state after:
case w
V : Type u_1
G : SimpleGraph V
hconn : G.Connected
v : V
inst✝ : Fintype ↑(G.neighborSet v)
hdeg : G.degree v = 1
u : V
adj_vu : G.Adj v u
hu : ∀ (y : V), (fun w ↦ G.Adj v w) y → y = u
w x : ↑{v}ᶜ
pwu : G.Walk (↑w) u
hpwu : pwu.IsPath
pux : G.Walk u ↑x
hpux : pux.IsPath
z : V
hz : z ∈ (↑(pwu.append pux).toPath).support
⊢ ¬z = v
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
⊢ h.finpartition.IsEquipartition

Tactic:
set fp := h.finpartition

Goal state after:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
⊢ fp.IsEquipartition
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
⊢ #h.finpartition.parts = min (Fintype.card V) r

Tactic:
set fp := h.finpartition

Goal state after:
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := h.finpartition
⊢ #fp.parts = min (Fintype.card V) r
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case inr
α : Type u_1
G : SimpleGraph α
h : ¬G.Preconnected
h✝ : Nonempty α
⊢ G.ediam = ⊤

Tactic:
apply ediam_eq_top_of_not_connected

Goal state after:
case inr
α : Type u_1
G : SimpleGraph α
h : ¬G.Preconnected
h✝ : Nonempty α
⊢ ¬G.Connected
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝¹ : Nonempty α
inst✝ : Finite α
h : G.Connected
u v : α
huv : G.edist u v = G.radius
⊢ G.Reachable u v

Tactic:
exact h u v

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

Goal state before:
pp: case inr
α : Type u_1
h✝ : Nontrivial α
u : α
⊢ ⊤.eccent u = ⊤.radius

Tactic:
eccent_top,

Goal state after:
case inr
α : Type u_1
h✝ : Nontrivial α
u : α
⊢ 1 = ⊤.radius
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: V : Type u
G : SimpleGraph V
K : Set V
C : G.ComponentCompl K
c d : V
x✝ : c ∈ C
dnK : d ∉ K
cd : G.Adj c d
cnK : c ∉ K
h : G.componentComplMk cnK = C
⊢ G.componentComplMk dnK = C

Tactic:
rw [← h, ConnectedComponent.eq]
    exact Adj.reachable cd.symm

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: V : Type u
G : SimpleGraph V
K L M : Set V
C : G.ComponentCompl L
h : K ⊆ L
h' : M ⊆ K
⊢ ConnectedComponent.map (induceHom Hom.id ⋯) C =
    ConnectedComponent.map (induceHom Hom.id ⋯) (ConnectedComponent.map (induceHom Hom.id ⋯) C)

Tactic:
ConnectedComponent.map_comp,

Goal state after:
V : Type u
G : SimpleGraph V
K L M : Set V
C : G.ComponentCompl L
h : K ⊆ L
h' : M ⊆ K
⊢ ConnectedComponent.map (induceHom Hom.id ⋯) C =
    ConnectedComponent.map ((induceHom Hom.id ⋯).comp (induceHom Hom.id ⋯)) C
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: case inr
V : Type u
G : SimpleGraph V
K✝ L M : Set V
inst✝ : G.LocallyFinite
Gpc : Fact G.Preconnected
K : Finset V
h : K.Nonempty
touch : G.ComponentCompl ↑K → ↑{v | ∃ k ∈ K, G.Adj k v} :=
  fun C ↦
    let p := ⋯;
    ⟨p.choose.1, ⋯⟩
touch_inj : Function.Injective touch
⊢ Finite (G.ComponentCompl ↑K)

Tactic:
have : Finite (Set.range touch) := by
      refine @Subtype.finite _ (Set.Finite.to_subtype ?_) _
      apply Set.Finite.ofFinset (K.biUnion (fun v => G.neighborFinset v))
      simp only [Finset.mem_biUnion, mem_neighborFinset, Set.mem_ofPred_eq, implies_true]

Goal state after:
case inr
V : Type u
G : SimpleGraph V
K✝ L M : Set V
inst✝ : G.LocallyFinite
Gpc : Fact G.Preconnected
K : Finset V
h : K.Nonempty
touch : G.ComponentCompl ↑K → ↑{v | ∃ k ∈ K, G.Adj k v} :=
  fun C ↦
    let p := ⋯;
    ⟨p.choose.1, ⋯⟩
touch_inj : Function.Injective touch
this : Finite ↑(Set.range touch)
⊢ Finite (G.ComponentCompl ↑K)
Module: Mathlib.Combinatorics.SimpleGraph.Girth

Goal state before:
pp: α : Type u_1
h : 3 ≤ ENat.card α
⊢ ⊤.girth = 3

Tactic:
by
  simp [girth, egirth_top h]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

Tactic:
by_cases hvw : v = w

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : v = w
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v

case neg
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
v w : V
hcyc : G.IsCycles
p : G.Walk v w
hp : p.IsPath
hvw : ¬v = w
⊢ (G \ p.toSubgraph.spanningCoe).Reachable w v
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
inst✝² : Primcodable α
inst✝¹ : Primcodable β
hf : PrimrecRel R
inst✝ : DecidableRel R
⊢ Primrec₂ fun L b ↦ filter (fun a ↦ decide (R a b)) L

Tactic:
by
  simp only [← List.filterMap_eq_filter]
  refine listFilterMap fst (Primrec.ite ?_ ?_ (Primrec.const Option.none))
  · exact Primrec.eq.comp (hf.decide.comp snd (snd.comp fst)) (.const true)
  · exact option_some.comp snd

Goal state after:
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
n : ℕ
f : Fin n → α → σ
hf : ∀ (i : Fin n), Primrec (f i)
⊢ Primrec fun a ↦ (List.Vector.ofFn fun i ↦ f i a).toList

Tactic:
simp [list_ofFn hf]

Goal state after:
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_5
σ : Type u_6
f : α →. σ ⊕ α
a : α
b : σ
F : α → ℕ →. σ ⊕ α :=
  fun a n ↦ Nat.rec (Part.some (Sum.inr a)) (fun x IH ↦ IH.bind fun s ↦ Sum.casesOn s (fun x ↦ Part.some s) f) n
h : b ∈ f.fix a
this :
  ∀ (a' : α),
    b ∈ f.fix a' → ∀ (k : ℕ), Sum.inr a' ∈ F a k → ∃ n, Sum.inl b ∈ F a n ∧ ∀ m < n, k ≤ m → ∃ a₂, Sum.inr a₂ ∈ F a m
⊢ Sum.inr a ∈ F a 0

Tactic:
simp [F]

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: f : ℕ →. ℕ
hf : Nat.Partrec f
⊢ Nat.Partrec (unpaired fun a b ↦ Nat.rfind fun n ↦ (fun m ↦ decide (m = 0)) <$> f (Nat.pair a (n + b)))

Tactic:
have : Nat.Partrec (fun a => Nat.rfind (fun n => (fun m => decide (m = 0)) <$>
      Nat.unpaired (fun a b => f (Nat.pair (Nat.unpair a).1 (b + (Nat.unpair a).2)))
        (Nat.pair a n))) :=
      rfind
        (Partrec₂.unpaired'.2
          ((Partrec.nat_iff.2 hf).comp
              (Primrec₂.pair.comp (Primrec.fst.comp <| Primrec.unpair.comp Primrec.fst)
                  (Primrec.nat_add.comp Primrec.snd
                    (Primrec.snd.comp <| Primrec.unpair.comp Primrec.fst))).to_comp))

Goal state after:
f : ℕ →. ℕ
hf : Nat.Partrec f
this :
  Nat.Partrec fun a ↦
    Nat.rfind fun n ↦
      (fun m ↦ decide (m = 0)) <$> unpaired (fun a b ↦ f (Nat.pair (unpair a).1 (b + (unpair a).2))) (Nat.pair a n)
⊢ Nat.Partrec (unpaired fun a b ↦ Nat.rfind fun n ↦ (fun m ↦ decide (m = 0)) <$> f (Nat.pair a (n + b)))
Module: Mathlib.Computability.Ackermann

Goal state before:
pp: case succ
k : ℕ
a✝ : k ^ 2 ≤ 2 ^ (k + 1) - 3
⊢ (k + 1) ^ 2 ≤ 2 ^ (k + 1 + 1) - 3

Tactic:
cases k <;> lia

Goal state after:
Module: Mathlib.Computability.PartrecCode

Goal state before:
pp: cf cg : Code
this : Nat.pair cf.encodeCode cg.encodeCode ≤ 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode)
⊢ cf.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4 ∧
    cg.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4

Tactic:
have := lt_of_le_of_lt this (lt_add_of_pos_right _ (by decide : 0 < 4))

Goal state after:
cf cg : Code
this✝ : Nat.pair cf.encodeCode cg.encodeCode ≤ 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode)
this : Nat.pair cf.encodeCode cg.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4
⊢ cf.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4 ∧
    cg.encodeCode < 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 4