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

Goal state before:
pp: case refine_1
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)
e₁ : completeBipartiteGraph (Fin m) (Fin n) ≃g completeBipartiteGraph V W := e₁✝.symm
K : SimpleGraph (α ⊕ β) := completeBipartiteGraph α β
e₂ : completeBipartiteGraph (Fin s) (Fin t) ≃g completeBipartiteGraph α β := e₂✝.symm
G : SimpleGraph (Fin m ⊕ Fin n)
h_le : G ≤ completeBipartiteGraph (Fin m) (Fin n)
h_free : (completeBipartiteGraph (Fin s) (Fin t)).Free G
h' : SimpleGraph.map (⇑e₁.toEmbedding) G ∈ {G | G ≤ completeBipartiteGraph V W ∧ K.Free G}
h_le_sup :
  #(SimpleGraph.map (⇑e₁.toEmbedding) G).edgeFinset ≤
    {G | G ≤ completeBipartiteGraph V W ∧ K.Free G}.sup fun x ↦ #x.edgeFinset
⊢ #(SimpleGraph.map (⇑e₁.toEquiv) G).edgeFinset ≤
    {G | G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G}.sup fun x ↦ #x.edgeFinset

Tactic:
simp_rw [← card_coe, mem_edgeFinset] at h_le_sup ⊢

Goal state after:
case refine_1
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)
e₁ : completeBipartiteGraph (Fin m) (Fin n) ≃g completeBipartiteGraph V W := e₁✝.symm
K : SimpleGraph (α ⊕ β) := completeBipartiteGraph α β
e₂ : completeBipartiteGraph (Fin s) (Fin t) ≃g completeBipartiteGraph α β := e₂✝.symm
G : SimpleGraph (Fin m ⊕ Fin n)
h_le : G ≤ completeBipartiteGraph (Fin m) (Fin n)
h_free : (completeBipartiteGraph (Fin s) (Fin t)).Free G
h' : SimpleGraph.map (⇑e₁.toEmbedding) G ∈ {G | G ≤ completeBipartiteGraph V W ∧ K.Free G}
h_le_sup :
  Fintype.card { x // x ∈ (SimpleGraph.map (⇑e₁.toEmbedding) G).edgeSet } ≤
    {G | G ≤ completeBipartiteGraph V W ∧ K.Free G}.sup fun x ↦ Fintype.card { x_1 // x_1 ∈ x.edgeSet }
⊢ Fintype.card { x // x ∈ (SimpleGraph.map (⇑e₁.toEquiv) G).edgeSet } ≤
    {G | G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G}.sup fun x ↦
      Fintype.card { x_1 // x_1 ∈ x.edgeSet }
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

Goal state before:
pp: case refine_2
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 : SimpleGraph (V ⊕ W)
h_le : G ≤ completeBipartiteGraph V W
h_free : (completeBipartiteGraph α β).Free G
h' : SimpleGraph.map (⇑e₁.toEmbedding) G ∈ {G | G ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ K.Free G}
h_le_sup :
  #(SimpleGraph.map (⇑e₁.toEmbedding) G).edgeFinset ≤
    {G | G ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ K.Free G}.sup fun x ↦ #x.edgeFinset
⊢ #(SimpleGraph.map (⇑e₁.toEquiv) G).edgeFinset ≤
    {G | G ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free G}.sup fun x ↦
      #x.edgeFinset

Tactic:
simp_rw [← card_coe, mem_edgeFinset] at h_le_sup ⊢

Goal state after:
case refine_2
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 : SimpleGraph (V ⊕ W)
h_le : G ≤ completeBipartiteGraph V W
h_free : (completeBipartiteGraph α β).Free G
h' : SimpleGraph.map (⇑e₁.toEmbedding) G ∈ {G | G ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ K.Free G}
h_le_sup :
  Fintype.card { x // x ∈ (SimpleGraph.map (⇑e₁.toEmbedding) G).edgeSet } ≤
    {G | G ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ K.Free G}.sup fun x ↦ Fintype.card { x_1 // x_1 ∈ x.edgeSet }
⊢ Fintype.card { x // x ∈ (SimpleGraph.map (⇑e₁.toEquiv) G).edgeSet } ≤
    {G | G ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free G}.sup fun x ↦
      Fintype.card { x_1 // x_1 ∈ x.edgeSet }
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
x : ℕ
h :
  ∀ (b : SimpleGraph (V ⊕ W)), b ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free b → #b.edgeFinset ≤ x
x✝¹ : SimpleGraph (V ⊕ W)
x✝ : DecidableRel x✝¹.Adj
h_le : x✝¹ ≤ completeBipartiteGraph V W
h_free : (completeBipartiteGraph α β).Free x✝¹
⊢ #x✝¹.edgeFinset = #x✝¹.edgeFinset

Tactic:
by convert rfl

Goal state after:
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
x : ℕ
x✝ : ∃ G x_1, G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G ∧ x < #G.edgeFinset
w✝¹ : SimpleGraph (V ⊕ W)
w✝ : DecidableRel w✝¹.Adj
h_le : w✝¹ ≤ completeBipartiteGraph V W
h_free : (completeBipartiteGraph α β).Free w✝¹
h_lt : x < #w✝¹.edgeFinset
⊢ #w✝¹.edgeFinset = #w✝¹.edgeFinset

Tactic:
by convert rfl

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

Goal state before:
pp: case inr
α : Type u_1
a b✝ : α
s : Finset α
G : SimpleGraph α
r : ℕ
inst✝ : DecidableEq α
h1 : G.IsNClique r (insert a s)
h2 : G.IsNClique r (insert b✝ s)
h3 : b✝ ∉ s
ha : G.Adj a b✝
b : α
hb : b ∈ insert a s
h : b ∈ s
⊢ G.Adj b✝ b

Tactic:
· exact h2.1 (mem_insert_self _ s) (mem_insert_of_mem h) <| fun h' ↦ (h3 (h' ▸ h)).elim

Goal state after:
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 hv
  obtain ⟨i, hi⟩ := Set.mem_iUnion.mp (verts_iSup ▸ hv)
  obtain ⟨w, hw⟩ := hM i hi
  use w
  refine ⟨iSup_adj.mpr ⟨i, hw.1⟩, ?_⟩
  intro y hy
  obtain ⟨i', hi'⟩ := iSup_adj.mp hy
  by_cases heq : i = i'
  · exact hw.2 y (heq.symm ▸ hi')
  · have := hd heq
    simp only [Set.disjoint_left] at this
    simpa [(mem_support _).mpr ⟨w, hw.1⟩, (mem_support _).mpr ⟨y, hi'⟩] using @this v

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst✝ : Fintype α
hp : p.IsHamiltonian
⊢ ∑ x ∈ p.support.toFinset, 1 = Fintype.card α

Tactic:
← card_eq_sum_ones,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
a b : α
p : G.Walk a b
inst✝ : Fintype α
hp : p.IsHamiltonian
⊢ #p.support.toFinset = Fintype.card α
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 : V
⊢ ∀ {w : V}, ((∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v) → G.Adj v w

Tactic:
w

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 w : V
⊢ ((∃ (h : v ∈ s), ↑(f ⟨v, h⟩) = w) ∨ ∃ (h : w ∈ s), ↑(f ⟨w, h⟩) = v) → G.Adj v w
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)
v : α
⊢ ∀ (y : α), s(v, y) ∈ G.edgeSet → ↑(#{x | s(v, y) ∈ G.incidenceSet x}) = 2

Tactic:
w

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 w : α
⊢ s(v, w) ∈ G.edgeSet → ↑(#{x | s(v, w) ∈ 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)
v : α
⊢ ∀ (y : α), s(v, y) ∉ G.edgeSet → ↑(#{x | s(v, y) ∈ G.incidenceSet x}) = 0

Tactic:
w

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 w : α
⊢ s(v, w) ∉ G.edgeSet → ↑(#{x | s(v, w) ∈ G.incidenceSet x}) = 0
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
hvw : ¬v = w
hpn : ¬p.Nil
w' : V
hwu : ∀ (y : V), (fun w' ↦ p.snd ≠ w' ∧ G.Adj v w') y → y = w'
hw'1 : p.snd ≠ w'
hw'2 : G.Adj v w'
hnpvw' : ¬p.toSubgraph.Adj v w'
hww' : ¬w = w'
⊢ G \ (Walk.cons ⋯ p).toSubgraph.spanningCoe ≤ G \ p.toSubgraph.spanningCoe

Tactic:
apply sdiff_le_sdiff (by rfl) ?hcd

Goal state after:
case hcd
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
hpn : ¬p.Nil
w' : V
hwu : ∀ (y : V), (fun w' ↦ p.snd ≠ w' ∧ G.Adj v w') y → y = w'
hw'1 : p.snd ≠ w'
hw'2 : G.Adj v w'
hnpvw' : ¬p.toSubgraph.Adj v w'
hww' : ¬w = w'
⊢ p.toSubgraph.spanningCoe ≤ (Walk.cons ⋯ p).toSubgraph.spanningCoe
Module: Mathlib.Combinatorics.SimpleGraph.Partition

Goal state before:
pp: V : Type u
G : SimpleGraph V
P : G.Partition
v : V
⊢ v ∈ P.partOfVertex v

Tactic:
by
  obtain ⟨⟨_, h⟩, _⟩ := (P.isPartition.2 v).choose_spec
  exact h

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w : V
inst✝ : Finite V
hadj : G.Adj v w
hcyc : G.IsCycles
this : fromEdgeSet {s(v, w)} = hadj.toWalk.toSubgraph.spanningCoe
⊢ (G.deleteEdges {s(v, w)}).Reachable v w

Tactic:
show G.deleteEdges {s(v, w)} = G \ fromEdgeSet {s(v, w)} by rfl

Goal state after:
V : Type u_1
G : SimpleGraph V
v w : V
inst✝ : Finite V
hadj : G.Adj v w
hcyc : G.IsCycles
this : fromEdgeSet {s(v, w)} = hadj.toWalk.toSubgraph.spanningCoe
⊢ (G \ fromEdgeSet {s(v, w)}).Reachable v w
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 : V
hv : v ∈ p.toSubgraph.verts
⊢ ∀ (w : V), G.Adj v w → p.toSubgraph.Adj v w

Tactic:
w

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
hv : 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
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')

Tactic:
w

Goal state after:
V : Type u_1
G G' : SimpleGraph V
halt : G.IsAlternating G'
H : G.Subgraph
v w : V
⊢ ∀ ⦃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
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')

Tactic:
w

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 w : V
⊢ ∀ ⦃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.Matching

Goal state before:
pp: case neg.inr.inl
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 w w' : V
hww' : w ≠ w'
hr : (v = u ∧ w = x ∨ v = x ∧ w = u) ∧ v ≠ w
h1 : G.Adj v w'
⊢ G'.Adj v w ↔ ¬G'.Adj v w'

Tactic:
G'.adj_congr_of_sym2 (by grind : s(v, w) = s(u, x))

Goal state after:
case neg.inr.inl
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 w w' : V
hww' : w ≠ w'
hr : (v = u ∧ w = x ∨ v = x ∧ w = u) ∧ v ≠ w
h1 : G.Adj v w'
⊢ G'.Adj u x ↔ ¬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 ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
⊢ #((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) - (#{v} + 1) = n - (2 * k - μ) - 2

pp: V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
⊢ w ∉ {v}

pp: V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
⊢ {w} ∪ {v} ⊆ (G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ

Tactic:
card_singleton,

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 ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
⊢ #((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) - (1 + 1) = n - (2 * k - μ) - 2

V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
⊢ w ∉ {v}

V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
n k ℓ μ : ℕ
inst✝ : DecidableEq V
h : G.IsSRGWith n k ℓ μ
v w : V
ha : v ≠ w ∧ ¬G.Adj v w
hne : v ≠ w
⊢ {w} ∪ {v} ⊆ (G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: case convert_3
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
s : {v} ⊆ G.neighborFinset w \ G.neighborFinset v
⊢ #(G.neighborFinset w \ G.neighborFinset v) - #{v} = k - ℓ - 1

Tactic:
card_singleton,

Goal state after:
case convert_3
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
s : {v} ⊆ G.neighborFinset w \ G.neighborFinset v
⊢ #(G.neighborFinset w \ G.neighborFinset v) - 1 = k - ℓ - 1
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
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')

Tactic:
w

Goal state after:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
M' : G'.Subgraph
hM : M.IsPerfectMatching
hM' : M'.IsPerfectMatching
v w : V
⊢ ∀ ⦃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: case h
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x b
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x b
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V), x' ≠ c → ¬M2.Adj x' a
p : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp : p.IsCycle ∧ p.toSubgraph.verts = (cycles.connectedComponentMk c).supp
p' : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp' : p'.IsCycle ∧ p'.snd = c ∧ p'.toSubgraph.verts = p.toSubgraph.verts
⊢ x ∈ p.toSubgraph.verts

Tactic:
hp.2

Goal state after:
case h
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x b
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x b
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V), x' ≠ c → ¬M2.Adj x' a
p : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp : p.IsCycle ∧ p.toSubgraph.verts = (cycles.connectedComponentMk c).supp
p' : (M1.spanningCoe ∆ M2.spanningCoe).Walk a a
hp' : p'.IsCycle ∧ p'.snd = c ∧ p'.toSubgraph.verts = p.toSubgraph.verts
⊢ x ∈ (cycles.connectedComponentMk c).supp
Module: Mathlib.Computability.Primrec.List

Goal state before:
pp: case nil
β : Type u_2
inst✝ : Primcodable β
H : Nat.Primrec fun n ↦ encode (decode n)
this : Primcodable (List β) := prim H
⊢ ∀ (r : List β), List.foldl (fun s b ↦ b :: s) r [] = [].reverseAux r

Tactic:
simp [*, List.reverseAux]

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

Goal state before:
pp: case cons
β : Type u_2
inst✝ : Primcodable β
H : Nat.Primrec fun n ↦ encode (decode n)
this : Primcodable (List β) := prim H
head✝ : β
tail✝ : List β
tail_ih✝ : ∀ (r : List β), List.foldl (fun s b ↦ b :: s) r tail✝ = tail✝.reverseAux r
⊢ ∀ (r : List β), List.foldl (fun s b ↦ b :: s) r (head✝ :: tail✝) = (head✝ :: tail✝).reverseAux r

Tactic:
simp [*, List.reverseAux]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x b
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x b
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V), x' ≠ c → ¬M2.Adj x' a
x' : V
hx' : x' ∈ {x, b}
p : cycles.Walk a x'
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
v : V
⊢ ∀ ⦃w : V⦄, p.toSubgraph.spanningCoe.Adj v w → (G ⊔ edge a c ⊔ edge x b).Adj v w

Tactic:
w

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
x a b c : V
M1 : (G ⊔ edge x b).Subgraph
M2 : (G ⊔ edge a c).Subgraph
hxa : G.Adj x a
hab : G.Adj a b
hnGxb : ¬G.Adj x b
hnGac : ¬G.Adj a c
hnxb : x ≠ b
hnxc : x ≠ c
hnac : a ≠ c
hnbc : b ≠ c
hM1 : M1.IsPerfectMatching
hM2 : M2.IsPerfectMatching
hM1xb : M1.Adj x b
hM2ac : M2.Adj a c
hM1nac : ¬M1.Adj a c
hsupG : G ⊔ edge x b ⊔ (G ⊔ edge a c) = G ⊔ edge a c ⊔ edge x b
cycles : SimpleGraph V := M1.spanningCoe ∆ M2.spanningCoe
hcalt : cycles.IsAlternating M2.spanningCoe
hcycles : (M1.spanningCoe ∆ M2.spanningCoe).IsCycles
hcac : cycles.Adj a c
hM1sub : M1.spanningCoe ≤ G ⊔ edge x b
hM2sub : M2.spanningCoe ≤ G ⊔ edge a c
induce_le : (cycles.connectedComponentMk c).toSimpleGraph.spanningCoe ≤ G ⊔ edge a c ⊔ edge x b
hxc : x ∈ (cycles.connectedComponentMk c).supp
hacc : a ∈ (cycles.connectedComponentMk c).supp
this : (G : SimpleGraph V) → G.LocallyFinite
hnM2 : ∀ (x' : V), x' ≠ c → ¬M2.Adj x' a
x' : V
hx' : x' ∈ {x, b}
p : cycles.Walk a x'
hp : p.IsPath
hpac : p.toSubgraph.Adj a c
hnpxb : ¬p.toSubgraph.Adj x b
v w : V
⊢ p.toSubgraph.spanningCoe.Adj v w → (G ⊔ edge a c ⊔ edge x b).Adj v w
Module: Mathlib.Computability.Partrec

Goal state before:
pp: α : Type u_1
σ : Type u_2
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → ℕ
g : α → σ
h : α → ℕ →. σ
hf : Computable f
hg : Computable g
hh : Partrec₂ h
a : α
n : ℕ
b : σ
H : b ∈ Nat.rec (Part.some (g a)) (fun n n_ih ↦ h a n) (n + 1)
m : ℕ
⊢ (Nat.rec (Part.some (g a)) (fun y IH ↦ IH.bind fun x ↦ h a n) m).Dom

Tactic:
induction m <;> simp [*, H.fst]

Goal state after: