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

Goal state before:
pp: m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
⊢ zarankiewicz m n s t =
    {G | G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G}.sup fun x ↦ #x.edgeFinset

Tactic:
zarankiewicz,

Goal state after:
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
⊢ ({G | G ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free G}.sup fun x ↦
      #x.edgeFinset) =
    {G | G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G}.sup fun x ↦ #x.edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Finite V
ι : Sort u_1
f : ι → G.Finsubgraph
⊢ ⨆ G_1 ∈ range fun i ↦ f i, ↑G_1 = ⨆ i, ↑(f i)

Tactic:
iSup_range

Goal state after:
V : Type u
G : SimpleGraph V
inst✝ : Finite V
ι : Sort u_1
f : ι → G.Finsubgraph
⊢ ⨆ i, ↑(f i) = ⨆ i, ↑(f i)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity

Goal state before:
pp: case hm
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst✝ : DecidableRel G.Adj
h : H.Free G
⊢ ∀ a ∈ univ, ↑(#(bipartiteAbove (fun v e ↦ v ∉ e) G.edgeFinset a)) ≤ extremalNumber n H

Tactic:
intro v

Goal state after:
case hm
W : Type u_1
H : SimpleGraph W
n : ℕ
hn : n ≥ 2
G : SimpleGraph (Fin (n + 1))
inst✝ : DecidableRel G.Adj
h : H.Free G
v : Fin (n + 1)
⊢ v ∈ univ → ↑(#(bipartiteAbove (fun v e ↦ v ∉ e) G.edgeFinset v)) ≤ extremalNumber n H
Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph

Goal state before:
pp: case intro.refine_2
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
val✝ : Fintype W
this✝ : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')
this : (G' : G.Finsubgraphᵒᵖ) → Fintype ((G.finsubgraphHomFunctor F).obj G')
u : (j : G.Finsubgraphᵒᵖ) → (G.finsubgraphHomFunctor F).obj j
hu : u ∈ (G.finsubgraphHomFunctor F).sections
⊢ ∀ {a b : V},
    G.Adj a b →
      F.Adj ((u (Opposite.op (singletonFinsubgraph a))).toFun ⟨a, ⋯⟩)
        ((u (Opposite.op (singletonFinsubgraph b))).toFun ⟨b, ⋯⟩)

Tactic:
intro v

Goal state after:
case intro.refine_2
V : Type u
W : Type v
G : SimpleGraph V
F : SimpleGraph W
inst✝ : Finite W
h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F
val✝ : Fintype W
this✝ : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')
this : (G' : G.Finsubgraphᵒᵖ) → Fintype ((G.finsubgraphHomFunctor F).obj G')
u : (j : G.Finsubgraphᵒᵖ) → (G.finsubgraphHomFunctor F).obj j
hu : u ∈ (G.finsubgraphHomFunctor F).sections
v : V
⊢ ∀ {b : V},
    G.Adj v b →
      F.Adj ((u (Opposite.op (singletonFinsubgraph v))).toFun ⟨v, ⋯⟩)
        ((u (Opposite.op (singletonFinsubgraph b))).toFun ⟨b, ⋯⟩)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
⊢ ↑(#(between (↑K.verts) (↑K.verts)ᶜ G).edgeFinset) = ∑ x ∈ K.vertsᶜ, ↑((between (↑K.verts) (↑K.verts)ᶜ G).degree x)

Tactic:
eq_comm

Goal state after:
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
⊢ ∑ x ∈ K.vertsᶜ, ↑((between (↑K.verts) (↑K.verts)ᶜ G).degree x) = ↑(#(between (↑K.verts) (↑K.verts)ᶜ G).edgeFinset)
Module: Mathlib.Combinatorics.SimpleGraph.Girth

Goal state before:
pp: case refine_2
α : Type u_1
G : SimpleGraph α
h : Nonempty ((i : α) × Subtype Walk.IsCycle)
⊢ ∃ x, ⨅ x, ↑(↑x.snd).length = ↑(↑x.snd).length

Tactic:
eq_comm

Goal state after:
case refine_2
α : Type u_1
G : SimpleGraph α
h : Nonempty ((i : α) × Subtype Walk.IsCycle)
⊢ ∃ x, ↑(↑x.snd).length = ⨅ x, ↑(↑x.snd).length
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.ErdosStoneSimonovits

Goal state before:
pp: n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
⊢ (↑n - ↑(#K.verts)) * (↑(#K.verts) - (↑t' - ↑t)) + ↑(#(filter K t)) * (↑t' - ↑t) - ↑(#(filter K t)) * ↑(#K.verts) +
      ↑(#(filter K t)) * ↑(#K.verts) =
    (↑n - ↑(#K.verts)) * (↑(#K.verts) - (↑t' - ↑t)) + ↑(#(filter K t)) * (↑t' - ↑t)

Tactic:
sub_add_cancel

Goal state after:
n : ℕ
G : SimpleGraph (Fin n)
inst✝ : DecidableRel G.Adj
r t t' : ℕ
K : G.CompleteEquipartiteSubgraph r t'
hr_pos : 0 < r
ht'_pos : 0 < t'
⊢ (↑n - ↑(#K.verts)) * (↑(#K.verts) - (↑t' - ↑t)) + ↑(#(filter K t)) * (↑t' - ↑t) =
    (↑n - ↑(#K.verts)) * (↑(#K.verts) - (↑t' - ↑t)) + ↑(#(filter K t)) * (↑t' - ↑t)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: m n s t : ℕ
α : Type u_3
β : Type u_4
inst✝¹ : Fintype α
inst✝ : Fintype β
hs : Fintype.card α = s
ht : Fintype.card β = t
⊢ zarankiewicz m n s t ≤ extremalNumber (Fintype.card (Fin (m + n))) (completeBipartiteGraph α β)

Tactic:
zarankiewicz,

Goal state after:
m n s t : ℕ
α : Type u_3
β : Type u_4
inst✝¹ : Fintype α
inst✝ : Fintype β
hs : Fintype.card α = s
ht : Fintype.card β = t
⊢ ({G | G ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free G}.sup fun x ↦
      #x.edgeFinset) ≤
    extremalNumber (Fintype.card (Fin (m + n))) (completeBipartiteGraph α β)
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
⊢ (⋃ i ∈ t, s i).encard ≤ ∑ᶠ (i : ι) (_ : i ∈ t), (s i).encard

Tactic:
by
  simpa [← finsum_mem_eq_finite_toFinset_sum] using ht.toFinset.set_encard_biUnion_le s

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd : Disjoint M.support M'.support
⊢ (M ⊔ M').IsMatching

Tactic:
intro v

Goal state after:
V : Type u_1
G : SimpleGraph V
M M' : G.Subgraph
hM : M.IsMatching
hM' : M'.IsMatching
hd : Disjoint M.support M'.support
v : V
⊢ v ∈ (M ⊔ M').verts → ∃! w, (M ⊔ M').Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
ι : Type u_3
f : ι → G.Subgraph
hM : ∀ (i : ι), (f i).IsMatching
hd : Pairwise fun i j ↦ Disjoint (f i).support (f j).support
⊢ (⨆ i, f i).IsMatching

Tactic:
intro v

Goal state after:
V : Type u_1
G : SimpleGraph V
ι : Type u_3
f : ι → G.Subgraph
hM : ∀ (i : ι), (f i).IsMatching
hd : Pairwise fun i j ↦ Disjoint (f i).support (f j).support
v : V
⊢ v ∈ (⨆ i, f i).verts → ∃! w, (⨆ i, f i).Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst✝ : Subsingleton α
⊢ p.IsHamiltonian

Tactic:
intro v

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst✝ : Subsingleton α
v : α
⊢ List.count v p.support = 1
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
⊢ ∀ {v w : V}, ((∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v) → G.Adj v w

Tactic:
intro v

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
⊢ ∀ {w : V}, ((∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v) → G.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Set V
h✝ : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v w : V
h : (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v
⊢ G.Adj v w

Tactic:
obtain (⟨hv, rfl⟩ | ⟨hw, rfl⟩) := h

Goal state after:
case inl
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
hv : v ∈ s
⊢ G.Adj v ↑(f ⟨v, hv⟩)

case inr
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
w : V
hw : w ∈ s
⊢ G.Adj (↑(f ⟨w, hw⟩)) w
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case h
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
⊢ ∀ ⦃v : V⦄, v ∈ s ∨ v ∈ t → ∃! w, (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v

Tactic:
intro v

Goal state after:
case h
V : Type u_1
G : SimpleGraph V
s t : Set V
h : Disjoint s t
f : ↑s ≃ ↑t
hadj : ∀ (v : ↑s), G.Adj ↑v ↑(f v)
v : V
⊢ v ∈ s ∨ v ∈ t → ∃! w, (∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v
Module: Mathlib.Combinatorics.SimpleGraph.Hamiltonian

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
h : Fintype.card α = 2
hG : G.IsHamiltonian
⊢ False

Tactic:
have ⟨v, p, hp⟩ := hG <| by lia

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
h : Fintype.card α = 2
hG : G.IsHamiltonian
v : α
p : G.Walk v v
hp : p.IsHamiltonianCycle
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix

Goal state before:
pp: case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : NonAssocSemiring R
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
⊢ ∀ (x y : α), s(x, y) ∈ G.edgeSet → ↑(#{x_1 | s(x, y) ∈ G.incidenceSet x_1}) = 2

Tactic:
intro v

Goal state after:
case pos
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : NonAssocSemiring R
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
v : α
⊢ ∀ (y : α), s(v, y) ∈ G.edgeSet → ↑(#{x | s(v, y) ∈ G.incidenceSet x}) = 2
Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix

Goal state before:
pp: case neg
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : NonAssocSemiring R
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
⊢ ∀ (x y : α), s(x, y) ∉ G.edgeSet → ↑(#{x_1 | s(x, y) ∈ G.incidenceSet x_1}) = 0

Tactic:
intro v

Goal state after:
case neg
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝⁴ : NonAssocSemiring R
inst✝³ : DecidableEq α
inst✝² : DecidableRel G.Adj
e : Sym2 α
inst✝¹ : Fintype α
inst✝ : Decidable (e ∈ G.edgeSet)
v : α
⊢ ∀ (y : α), s(v, y) ∉ G.edgeSet → ↑(#{x | s(v, y) ∈ G.incidenceSet x}) = 0
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Finite V
u : Set V
hM : M.IsPerfectMatching
c : ↑(⊤.deleteVerts u).coe.oddComponents
h : ∀ w ∈ u, ∀ (v : ↑(⊤.deleteVerts u).verts), M.Adj (↑v) w → v ∉ (↑c).supp
⊢ (M.induce (Subtype.val '' (↑c).supp)).IsMatching

Tactic:
intro v

Goal state after:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : Finite V
u : Set V
hM : M.IsPerfectMatching
c : ↑(⊤.deleteVerts u).coe.oddComponents
h : ∀ w ∈ u, ∀ (v : ↑(⊤.deleteVerts u).verts), M.Adj (↑v) w → v ∉ (↑c).supp
v : V
⊢ v ∈ (M.induce (Subtype.val '' (↑c).supp)).verts → ∃! w, (M.induce (Subtype.val '' (↑c).supp)).Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
h : G ≤ G'
hmf : G'.IsMatchingFree
x : G.Subgraph
hc : x.IsPerfectMatching
⊢ (Subgraph.map (Hom.ofLE h) x).IsSpanning

Tactic:
intro v

Goal state after:
V : Type u_1
G G' : SimpleGraph V
h : G ≤ G'
hmf : G'.IsMatchingFree
x : G.Subgraph
hc : x.IsPerfectMatching
v : V
⊢ v ∈ (Subgraph.map (Hom.ofLE h) x).verts
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
c : G.ConnectedComponent
h : G.IsCycles
⊢ c.toSimpleGraph.spanningCoe.IsCycles

Tactic:
intro v

Goal state after:
V : Type u_1
G : SimpleGraph V
c : G.ConnectedComponent
h : G.IsCycles
v : V
⊢ (c.toSimpleGraph.spanningCoe.neighborSet v).Nonempty → (c.toSimpleGraph.spanningCoe.neighborSet v).ncard = 2
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
⊢ p.toSubgraph.spanningCoe.IsCycles

Tactic:
intro v

Goal state after:
V : Type u_1
G : SimpleGraph V
u : V
p : G.Walk u u
hpc : p.IsCycle
v : V
⊢ (p.toSubgraph.spanningCoe.neighborSet v).Nonempty → (p.toSubgraph.spanningCoe.neighborSet v).ncard = 2
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
⊢ (M.spanningCoe ∆ M'.spanningCoe).IsCycles

Tactic:
intro v

Goal state after:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v : V
⊢ ((M.spanningCoe ∆ M'.spanningCoe).neighborSet v).Nonempty → ((M.spanningCoe ∆ M'.spanningCoe).neighborSet v).ncard = 2
Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix

Goal state before:
pp: V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
⊢ ⊤ ≤ Submodule.span ℝ (Set.range G.lapMatrix_ker_basis_aux)

Tactic:
intro x _

Goal state after:
V : Type u_1
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : DecidableEq G.ConnectedComponent
x : ↥(toLin' (lapMatrix ℝ G)).ker
a✝ : x ∈ ⊤
⊢ x ∈ Submodule.span ℝ (Set.range G.lapMatrix_ker_basis_aux)
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝ : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv : v ∈ c.supp
w : V
hw : w ∈ G.neighborSet v
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v, w) ∈ p.edges
hvp : v ∈ p.support
⊢ ∀ v ∈ p.toSubgraph.verts, ∀ (w : V), G.Adj v w → p.toSubgraph.Adj v w

Tactic:
intro v

Goal state after:
V : Type u_1
G : SimpleGraph V
v✝ : V
inst✝ : Finite V
c : G.ConnectedComponent
h : G.IsCycles
hv : v✝ ∈ c.supp
w : V
hw : w ∈ G.neighborSet v✝
u : V
p : G.Walk u u
hp : p.IsCycle ∧ s(v✝, w) ∈ p.edges
hvp : v✝ ∈ p.support
v : V
⊢ v ∈ p.toSubgraph.verts → ∀ (w : V), G.Adj v w → p.toSubgraph.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
halt : G.IsAlternating G'
H : G.Subgraph
⊢ H.spanningCoe.IsAlternating G'

Tactic:
intro v

Goal state after:
V : Type u_1
G G' : SimpleGraph V
halt : G.IsAlternating G'
H : G.Subgraph
v : V
⊢ ∀ ⦃w w' : V⦄, w ≠ w' → H.spanningCoe.Adj v w → H.spanningCoe.Adj v w' → (G'.Adj v w ↔ ¬G'.Adj v w')
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: case neg
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
⊢ (G ⊔ edge u x).IsAlternating G'

Tactic:
intro v

Goal state after:
case neg
V : Type u_1
G G' : SimpleGraph V
u x : V
halt : G.IsAlternating G'
hnadj : ¬G'.Adj u x
hu' : ∀ (u' : V), u' ≠ u → G.Adj x u' → G'.Adj x u'
hx' : ∀ (x' : V), x' ≠ x → G.Adj x' u → G'.Adj x' u
hadj : ¬G.Adj u x
v : V
⊢ ∀ ⦃w w' : V⦄, w ≠ w' → (G ⊔ edge u x).Adj v w → (G ⊔ edge u x).Adj v w' → (G'.Adj v w ↔ ¬G'.Adj v w')
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
⊢ Gᶜ.IsRegularOfDegree (Fintype.card V - (k + 1))

Tactic:
add_comm,

Goal state after:
V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
⊢ Gᶜ.IsRegularOfDegree (Fintype.card V - (1 + k))
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
⊢ ∀ (v : V), ∃! w, ⊤.Adj v w

Tactic:
intro v

Goal state after:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
hM : M.IsPerfectMatching
hG' : G'.IsAlternating M.spanningCoe
hG'cyc : G'.IsCycles
v : V
⊢ ∃! w, ⊤.Adj v w
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: case convert_4
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : w ∉ G.neighborFinset v ∧ ¬w = v
⊢ #(bipartiteBelow G.Adj (G.neighborFinset v) w) = μ

Tactic:
mem_neighborFinset,

Goal state after:
case convert_4
n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
this : DecidableEq V := Classical.decEq V
v w : V
hw : ¬G.Adj v w ∧ ¬w = v
⊢ #(bipartiteBelow G.Adj (G.neighborFinset v) w) = μ
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
⊢ (M.spanningCoe ∆ M'.spanningCoe).IsAlternating M.spanningCoe

Tactic:
intro v

Goal state after:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v : V
⊢ ∀ ⦃w w' : V⦄,
    w ≠ w' →
      (M.spanningCoe ∆ M'.spanningCoe).Adj v w →
        (M.spanningCoe ∆ M'.spanningCoe).Adj v w' → (M.spanningCoe.Adj v w ↔ ¬M.spanningCoe.Adj v w')
Module: Mathlib.Combinatorics.SimpleGraph.Tutte

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents (Quot.out '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
t : Set V
ht : t ⊆ G.universalVerts
M1 : G.Subgraph
hM1 : M1.verts = Subtype.val '' Quot.out '' G.deleteUniversalVerts.coe.oddComponents ∪ t ∧ M1.IsMatching
complMatch : G.deleteUniversalVerts.coe.ConnectedComponent → G.Subgraph
hcomplMatch_compl :
  ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).verts = Subtype.val '' K.supp \ M1.verts
hcomplMatch_match : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).IsMatching
M2 : G.Subgraph := ⨆ K, complMatch K
hM2 : M2.IsMatching
disjointM12 : Disjoint M1.support M2.support
⊢ Set.univ \ G.universalVerts ⊆ M1.verts ∪ M2.verts

Tactic:
intro v

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
hrep :
  ConnectedComponent.Represents (Quot.out '' G.deleteUniversalVerts.coe.oddComponents)
    G.deleteUniversalVerts.coe.oddComponents
t : Set V
ht : t ⊆ G.universalVerts
M1 : G.Subgraph
hM1 : M1.verts = Subtype.val '' Quot.out '' G.deleteUniversalVerts.coe.oddComponents ∪ t ∧ M1.IsMatching
complMatch : G.deleteUniversalVerts.coe.ConnectedComponent → G.Subgraph
hcomplMatch_compl :
  ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).verts = Subtype.val '' K.supp \ M1.verts
hcomplMatch_match : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), (complMatch K).IsMatching
M2 : G.Subgraph := ⨆ K, complMatch K
hM2 : M2.IsMatching
disjointM12 : Disjoint M1.support M2.support
v : V
⊢ v ∈ Set.univ \ G.universalVerts → v ∈ M1.verts ∪ M2.verts
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case hi.some.none.some
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n ↦ encode (decode n) := prim (List ℕ)
this✝ : Primrec₂ fun a o ↦ Option.map (List.cons (encode a)) o
this :
  Primrec fun n ↦
    List.foldl (fun o m ↦ (decode m).bind fun a ↦ Option.map (List.cons (encode a)) o) (some [])
      (ofNat (List ℕ) n).reverse
n✝ n : ℕ
IH✝ :
  ∀ m ≤ n,
    encode
        (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
          (ofNat (List ℕ) m)) =
      encode (decode m)
a : α
val✝ : List α
IH : encode none = encode (some val✝)
⊢ encode (Option.map (List.cons (encode a)) none) = encode (Option.map (List.cons a) (some val✝))

Tactic:
injection IH

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

Goal state before:
pp: case hi.some.some.none
α : Type u_1
β : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable β
H : Nat.Primrec fun n ↦ encode (decode n) := prim (List ℕ)
this✝ : Primrec₂ fun a o ↦ Option.map (List.cons (encode a)) o
this :
  Primrec fun n ↦
    List.foldl (fun o m ↦ (decode m).bind fun a ↦ Option.map (List.cons (encode a)) o) (some [])
      (ofNat (List ℕ) n).reverse
n✝ n : ℕ
IH✝ :
  ∀ m ≤ n,
    encode
        (List.foldr (fun x y ↦ (decode x).bind fun a ↦ Option.map (List.cons (encode a)) y) (some [])
          (ofNat (List ℕ) m)) =
      encode (decode m)
a : α
val✝ : List ℕ
IH : encode (some val✝) = encode none
⊢ encode (Option.map (List.cons (encode a)) (some val✝)) = encode (Option.map (List.cons a) none)

Tactic:
injection IH

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

Goal state before:
pp: α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ → σ
g : α → List σ → Option σ
hg : Primrec₂ g
H : ∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = some (f a n)
a : α
n : ℕ
⊢ Nat.rec (some [])
      (fun n IH ↦
        (a, n, IH).2.2.bind fun b ↦
          Option.map (fun b_1 ↦ (((a, n, IH), b), b_1).1.2 ++ [(((a, n, IH), b), b_1).2])
            (g ((a, n, IH), b).1.1 ((a, n, IH), b).2))
      n =
    some (List.map (f a) (List.range n))

Tactic:
by
      induction n with
      | zero => rfl
      | succ n IH => simp [IH, H, List.range_succ]

Goal state after: