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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nonempty α
n : ℕ
s : Finset α
hs : s ∈ powersetCard n univ
⊢ ↑(card α) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) = ↑(card α) / ((↑(card α) - ↑n) * ↑((card α).choose n))

Tactic:
rw [mem_powersetCard_univ.1 hs]

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case right
A : Finset ℕ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
n : ℕ := ⌊↑(#A) / ε⌋₊ + 1
hn : 0 < n
⊢ ↑(#({a ∈ Ioc 0 n | a ∈ ↑A})) / ε < ↑⌊↑(#A) / ε⌋₊ + 1

Tactic:
exact (Nat.lt_floor_add_one _).trans_le' <| by gcongr; simp [subset_iff]

Goal state after:
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
s : Finset α
p : α → Prop
⊢ (∃ a ∈ sᶜˢ, p a) ↔ ∃ a ∈ s, p aᶜ

Tactic:
aesop

Goal state after:
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝¹ : BooleanAlgebra α
inst✝ : DecidableEq α
s t : Finset α
a✝ : α
⊢ (∃ a ∈ s, ∃ b, bᶜ ∈ t ∧ a ⊓ b = a✝) ↔ ∃ a ∈ s, ∃ b ∈ t, a ⊓ bᶜ = a✝

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t : Finset α
⊢ (∃ s ∈ 𝒜, ∃ a ∉ t, insert a t = s) ↔ ∃ a ∉ t, insert a t ∈ 𝒜

Tactic:
aesop

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

Goal state before:
pp: case succ
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
k : ℕ
ih : ∀ {t : Finset α}, t ∈ ∂^[k] 𝒜 ↔ ∃ u, #u = k ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜
t : Finset α
⊢ (∃ a ∉ t, ∃ u, #u = k ∧ Disjoint (insert a t) u ∧ insert a t ∪ u ∈ 𝒜) ↔
    ∃ u, (∃ a t, a ∉ t ∧ insert a t = u ∧ #t = k) ∧ Disjoint t u ∧ t ∪ u ∈ 𝒜

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
⊢ (∃ s ∈ 𝒜, ∃ a ∈ t, t.erase a = s) ↔ ∃ a ∈ t, t.erase a ∈ 𝒜

Tactic:
aesop

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case inr
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
r : ℕ
huv : #u = #v
h𝒜 : Set.Sized r ↑𝒜
t : Finset α
ht : t ∈ 𝒜
huvt : compress u v t ∉ 𝒜
⊢ #(compress u v t) = r

Tactic:
· rw [card_compress huv, h𝒜 ht]

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

Goal state before:
pp: case insert
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
hs : a ∉ s
ih :
  ∀ {𝒜 ℬ : Finset (Finset α)},
    IsLowerSet ↑𝒜 → IsLowerSet ↑ℬ → (∀ t ∈ 𝒜, t ⊆ s) → (∀ t ∈ ℬ, t ⊆ s) → #𝒜 * #ℬ ≤ 2 ^ #s * #(𝒜 ∩ ℬ)
𝒜 ℬ : Finset (Finset α)
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ t ∈ 𝒜, t ⊆ insert a s
hℬs : ∀ t ∈ ℬ, t ⊆ insert a s
⊢ #𝒜 * #ℬ ≤ 2 ^ #(insert a s) * #(𝒜 ∩ ℬ)

Tactic:
| insert a s hs ih =>

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
h✝¹ : s ∈ 𝒜
h✝ : insert a s ∈ 𝒜
⊢ t = s ∨ t = insert a s → t ∈ 𝒜

Tactic:
aesop

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
h✝¹ : s ∈ 𝒜
h✝ : insert a s ∉ 𝒜
⊢ t ∈ 𝒜 ∧ (t = s ∨ t = insert a s) ↔ t = s

Tactic:
aesop

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
h✝¹ : s ∉ 𝒜
h✝ : insert a s ∈ 𝒜
⊢ t ∈ 𝒜 ∧ (t = s ∨ t = insert a s) ↔ t = insert a s

Tactic:
aesop

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ∉ s
𝒜 : Finset (Finset α)
t : Finset α
h✝¹ : s ∉ 𝒜
h✝ : insert a s ∉ 𝒜
⊢ t ∈ 𝒜 → ¬t = s ∧ ¬t = insert a s

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝² : s ⊆ insert a u
this✝¹ : t ⊆ insert a u
this✝ : insert a s ⊆ insert a u
this : insert a t ⊆ insert a u
⊢ collapse 𝒜 a f₁ s * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
have has := notMem_mono hsu hu

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝² : s ⊆ insert a u
this✝¹ : t ⊆ insert a u
this✝ : insert a s ⊆ insert a u
this : insert a t ⊆ insert a u
has : a ∉ s
⊢ collapse 𝒜 a f₁ s * collapse ℬ a f₂ t ≤ collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : 𝒜.Shatters s
t : Finset α
⊢ (∃ a ∈ 𝒜, s ∩ a = t) ↔ t ∈ s.powerset

Tactic:
mem_powerset,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : 𝒜.Shatters s
t : Finset α
⊢ (∃ a ∈ 𝒜, s ∩ a = t) ↔ t ⊆ s
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: case mp.inl
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
h : s ∈ 𝒜 ∧ #s = k
⊢ (∃ t ∈ 𝒜, s ⊆ t) ∧ #s = k

pp: case mp.inr
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k + 1
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
⊢ (∃ t ∈ 𝒜, s.erase a ⊆ t) ∧ #(s.erase a) = k

Tactic:
· exact ⟨⟨s, h.1, Subset.refl _⟩, h.2⟩

Goal state after:
case mp.inr
α : Type u_2
inst✝ : DecidableEq α
k : ℕ
𝒜 : Finset (Finset α)
s : Finset α
hs : #s = k + 1
t : Finset α
ht : t ∈ 𝒜
hst : s ⊆ t
a : α
ha : a ∈ s
⊢ (∃ t ∈ 𝒜, s.erase a ⊆ t) ∧ #(s.erase a) = k
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∈ s
v : Finset α
hv : v ∈ 𝓓 a 𝒜
hsv : s ∩ v = insert a (s ∩ u)
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u

Tactic:
rw [Down.mem_compression] at hv

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : (𝓓 a 𝒜).Shatters s
u : Finset α
ht : s ∩ u ⊆ s
hu : u ∉ 𝒜 ∧ insert a u ∈ 𝒜
ha : a ∈ s
v : Finset α
hv : v ∈ 𝒜 ∧ v.erase a ∈ 𝒜 ∨ v ∉ 𝒜 ∧ insert a v ∈ 𝒜
hsv : s ∩ v = insert a (s ∩ u)
⊢ ∃ u_1 ∈ 𝒜, s ∩ u_1 = s ∩ u
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]

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
inst✝ : Fintype ↑(G.neighborSet v)
huv : u ≠ v
hu : G.degree v = 0
⊢ ¬G.Reachable v u
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
⊢ ⊥.Connected ↔ Subsingleton V ∧ Nonempty V

Tactic:
simp [preconnected_bot_iff_subsingleton, connected_iff]

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

Goal state before:
pp: case h
V : Type u
G : SimpleGraph V
v w : V
H : G.Subgraph
c : H.coe.ConnectedComponent
hw : w ∈ H.verts
hadj : H.Adj v w
w✝ : ↑H.verts
h : w✝ ∈ ↑c ∧ ↑w✝ = v
⊢ ⟨w, hw⟩ ∈ ↑(H.coe.connectedComponentMk w✝) ∧ ↑⟨w, hw⟩ = w

Tactic:
exact ⟨connectedComponentMk_eq_of_adj <| Subgraph.Adj.coe <| h.2 ▸ hadj.symm, rfl⟩

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

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
v w : V
C : G.ConnectedComponent
⊢ v ∈ C.supp ∧ G.Adj v w → C.toSimpleGraph.spanningCoe.Adj v w

Tactic:
simp only [toSimpleGraph, map_adj, comap_adj, Embedding.subtype_apply, Subtype.exists,
      exists_and_left, and_imp]
    intro h hadj
    exact ⟨v, h, w, hadj, rfl, (C.mem_supp_congr_adj hadj).mp h, rfl⟩

Goal state after:
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: case left
ι : Type u_1
α : Type u_2
s : ι → Set α
hs✝ : IndexedPartition s
β : Type u_3
f : ι → α → β
hs : IndexedPartition s
κ : Type u_4
g : ι → κ
hg : Surjective g
k : κ
⊢ g ⋯.some = k

pp: case right
ι : Type u_1
α : Type u_2
s : ι → Set α
hs✝ : IndexedPartition s
β : Type u_3
f : ι → α → β
hs : IndexedPartition s
κ : Type u_4
g : ι → κ
hg : Surjective g
k : κ
⊢ hs.some ⋯.some ∈ s ⋯.some

Tactic:
· simpa using ((singleton_nonempty k).preimage hg).some_mem

Goal state after:
case right
ι : Type u_1
α : Type u_2
s : ι → Set α
hs✝ : IndexedPartition s
β : Type u_3
f : ι → α → β
hs : IndexedPartition s
κ : Type u_4
g : ι → κ
hg : Surjective g
k : κ
⊢ hs.some ⋯.some ∈ s ⋯.some
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝⁴ : DecidableEq α
inst✝³ : CommSemiring β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
a : α
f₁ f₂ f₃ f₄ : Finset α → β
u : Finset α
inst✝ : ExistsAddOfLE β
hu : a ∉ u
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)
𝒜 ℬ : Finset (Finset α)
s : Finset α
hsu : s ⊆ u
t : Finset α
htu : t ⊆ u
this✝⁴ : s ⊆ insert a u
this✝³ : t ⊆ insert a u
this✝² : insert a s ⊆ insert a u
this✝¹ : insert a t ⊆ insert a u
has : a ∉ s
hat : a ∉ t
this✝ : a ∉ s ∩ t
this : a ∉ s ∪ t
h✝³ : s ∉ 𝒜
h✝² : insert a s ∈ 𝒜
h✝¹ : t ∈ ℬ
h✝ : insert a t ∈ ℬ
⊢ f₁ (insert a s) * f₂ t + f₁ (insert a s) * f₂ (insert a t) ≤
    collapse (𝒜 ⊼ ℬ) a f₃ (s ∩ t) * collapse (𝒜 ⊻ ℬ) a f₄ (s ∪ t)

Tactic:
refine (add_le_add (h ‹_› ‹_›) <| h ‹_› ‹_›).trans ?_
      rw [collapse_of_mem ‹_› (inter_mem_infs ‹_› ‹_›) (inter_mem_infs ‹_› ‹_›)
        (insert_inter_of_notMem ‹_›) (insert_inter_distrib _ _ _).symm,
        insert_inter_of_notMem ‹_›, ← insert_inter_distrib, insert_union, insert_union_distrib,
        ← add_mul]
      gcongr
      · exact add_nonneg (h₃ _) (h₃ _)
      · exact le_collapse_of_insert_mem ‹_› h₄
          (insert_union_distrib _ _ _).symm <| union_mem_sups ‹_› ‹_›

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.chromaticNumber ≤ ↑n ↔ G.Colorable n

Tactic:
by
  refine ⟨fun h ↦ ?_, Colorable.chromaticNumber_le⟩
  have : G.chromaticNumber ≠ ⊤ := (trans h (ENat.natCast_lt_top n)).ne
  rw [chromaticNumber_ne_top_iff_exists] at this
  obtain ⟨m, hm⟩ := this
  rw [hm.chromaticNumber_eq_sInf, Nat.cast_le] at h
  have := Nat.sInf_mem (⟨m, hm⟩ : {n' | G.Colorable n'}.Nonempty)
  rw [Set.mem_ofPred_eq] at this
  exact this.mono h

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
e : Sym2 V
⊢ (G.deleteEdges {e}).IsBridge e ↔ G.IsBridge e

Tactic:
induction e with | h u v =>  _ 

Goal state after:
case h
V : Type u
G : SimpleGraph V
u v : V
⊢ (G.deleteEdges {s(u, v)}).IsBridge s(u, v) ↔ G.IsBridge s(u, v)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
u v : V
huv : G.Adj u v
hc : ¬G.IsEdgeReachable 2 u v
hr : (G.deleteEdges {s(u, v)}).Reachable (u, v).1 (u, v).2
s : Set (Sym2 V)
hs₂ : s.encard < ↑2
hs₁ : s.encard ≠ ↑1
⊢ (G.deleteEdges s).Reachable u v

pp: case neg
V : Type u_1
G : SimpleGraph V
u v : V
huv : G.Adj u v
hc : ¬G.IsEdgeReachable 2 u v
hr : (G.deleteEdges {s(u, v)}).Reachable (u, v).1 (u, v).2
s : Set (Sym2 V)
hs₂ : s.encard < ↑2
hs₁ : s.encard = ↑1
⊢ (G.deleteEdges s).Reachable u v

Tactic:
· apply G.isEdgeReachable_one.mpr huv.reachable
    exact lt_of_le_of_ne (ENat.lt_natCast_add_one_iff.mp hs₂) hs₁

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
u v : V
huv : G.Adj u v
hc : ¬G.IsEdgeReachable 2 u v
hr : (G.deleteEdges {s(u, v)}).Reachable (u, v).1 (u, v).2
s : Set (Sym2 V)
hs₂ : s.encard < ↑2
hs₁ : s.encard = ↑1
⊢ (G.deleteEdges s).Reachable u v
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
h : H.Preconnected ∧ H.verts.Nonempty
⊢ H.Preconnected

Tactic:
exact h.1

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
⊢ v = p.getVert (i - 1) ∨ v = p.getVert (i + 1) →
    ∃ i_1,
      (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = v ∨ p.getVert i_1 = v ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
        i_1 < p.length

Tactic:
aesop

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.edist u v = G.edist v u

Tactic:
by
  rw [edist_eq_sInf, ← Set.image_univ, ← Set.image_univ_of_surjective Walk.reverse_surjective,
    ← Set.image_comp, Set.image_univ, Function.comp_def]
  simp_rw [Walk.length_reverse, ← edist_eq_sInf]

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

Goal state before:
pp: case refine_2
V : Type u_1
G : SimpleGraph V
u v : V
h : u ≠ v ∧ ¬G.Adj u v ∧ G.commonNeighbors u v = ∅
⊢ 2 ≤ G.edist u v

Tactic:
rw [← one_add_one_eq_two]
    refine Order.add_one_le_of_lt <| lt_of_le_of_ne ?_ ?_
    <;> grind [Order.one_le_iff_pos, pos_iff_ne_zero, edist_eq_zero_iff, edist_eq_one_iff_adj]

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

Goal state before:
pp: case inl
V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝¹ : i' < p.length
right✝ : p.getVert (i' + 1) = v
hl : i' = i
⊢ v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)

Tactic:
aesop

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

Goal state before:
pp: case inr
V : Type u
G : SimpleGraph V
v✝ u : V
i : ℕ
p : G.Walk u v✝
hp : p.IsPath
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝ : i' < p.length
left✝ : p.getVert i' = v
hl : i' + 1 = i
⊢ v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)

Tactic:
aesop

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
hr : G.Reachable u v
⊢ ∃ p, p.IsPath ∧ p.length = G.dist u v

Tactic:
by
  obtain ⟨p, h⟩ := hr.exists_walk_length_eq_dist
  exact ⟨p, p.isPath_of_length_eq_dist h, h⟩

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
⊢ v = p.getVert (i - 1) ∨ v = p.getVert (i + 1) →
    ∃ i_1,
      (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = v ∨ p.getVert i_1 = v ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
        i_1 < p.length

Tactic:
aesop

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

Goal state before:
pp: case inr
V : Type u
G : SimpleGraph V
u : V
i : ℕ
p : G.Walk u u
hpc : p.IsCycle
v : V
h : ¬i = 0
h' : i < p.length
hadj1 :
  ∃ i_1,
    (p.getVert i_1 = p.getVert i ∧ p.getVert (i_1 + 1) = p.getVert (i - 1) ∨
        p.getVert i_1 = p.getVert (i - 1) ∧ p.getVert (i_1 + 1) = p.getVert i) ∧
      i_1 < p.length
i' : ℕ
right✝ : i' < p.length
hr1 : p.getVert i' = v
hr2 : i' + 1 = i
⊢ v = p.getVert (i - 1) ∨ v = p.getVert (i + 1)

Tactic:
aesop

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 u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i = 0 ∨ i = p.length
⊢ u = v

Tactic:
aesop

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
⊢ (G □ H).edist x y = G.edist x.1 y.1 + H.edist x.2 y.2

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x y : α × β
top_case : (G □ H).edist x y = ⊤ ↔ G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤
h : ¬(G.edist x.1 y.1 = ⊤ ∨ H.edist x.2 y.2 = ⊤)
⊢ G.edist x.1 y.1 ≠ ⊤ ∧ H.edist x.2 y.2 ≠ ⊤

Tactic:
aesop

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
u v : V
n : ℕ
p : G.Walk u v
⊢ p ∈ G.finsetWalkLength n u v ↔ p ∈ {p | p.length = n}

Tactic:
← Finset.mem_coe,

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
u v : V
n : ℕ
p : G.Walk u v
⊢ p ∈ ↑(G.finsetWalkLength n u v) ↔ p ∈ {p | p.length = n}
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
u v : V
n : ℕ
p : G.Walk u v
⊢ p ∈ G.finsetWalkLengthLT n u v ↔ p ∈ {p | p.length < n}

Tactic:
← Finset.mem_coe,

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
u v : V
n : ℕ
p : G.Walk u v
⊢ p ∈ ↑(G.finsetWalkLengthLT n u v) ↔ p ∈ {p | p.length < n}
Module: Mathlib.Combinatorics.SimpleGraph.Cayley

Goal state before:
pp: M : Type u_1
s : Set M
inst✝ : Mul M
G : SimpleGraph M
⊢ mulCayley s ≤ G ↔ ∀ g ∈ s, ∀ (a : M), a * g ≠ a → G.Adj (a * g) a

Tactic:
SimpleGraph.le_iff_adj

Goal state after:
M : Type u_1
s : Set M
inst✝ : Mul M
G : SimpleGraph M
⊢ (∀ (v w : M), (mulCayley s).Adj v w → G.Adj v w) ↔ ∀ g ∈ s, ∀ (a : M), a * g ≠ a → G.Adj (a * g) a
Module: Mathlib.Combinatorics.SimpleGraph.Circulant

Goal state before:
pp: case succ
n✝ : ℕ
⊢ cycleGraph (n✝ + 1 + 1) = circulantGraph {1}

Tactic:
aesop

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

Goal state before:
pp: α : Type u_1
V : Type u_2
inst✝ : MulZeroOneClass α
A : Matrix V V α
hA : A.IsAdjMatrix
i j : V
this : A i j = 0 ∨ A i j = 1
⊢ (A ⊙ A) i j = A i j

Tactic:
aesop

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

Goal state before:
pp: case succ
α : Type u_1
V : Type u_2
G : SimpleGraph V
inst✝³ : DecidableRel G.Adj
inst✝² : Fintype V
inst✝¹ : DecidableEq V
inst✝ : Semiring α
n : ℕ
ih : ∀ (u v : V), (adjMatrix α G ^ n) u v = ↑(#(G.finsetWalkLength n u v))
u v : V
⊢ (↑univ).PairwiseDisjoint fun w ↦
    Finset.map { toFun := fun p ↦ Walk.cons ⋯ p, inj' := ⋯ } (G.finsetWalkLength n (↑w) v)

Tactic:
rintro ⟨x, hx⟩ - ⟨y, hy⟩ - hxy
      rw [Function.onFun, disjoint_iff_inf_le]
      intro p hp
      simp only [inf_eq_inter, mem_inter, mem_map] at hp
      obtain ⟨⟨px, _, rfl⟩, ⟨py, hpy, hp⟩⟩ := hp
      cases hp
      simp at hxy

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

Goal state before:
pp: V : Type u_1
G F : SimpleGraph V
h : Maximal (fun H ↦ H ≤ G ∧ H.IsAcyclic) F
u v : V
x✝ : G.Reachable u v
p : G.Walk u v
this✝¹ : ¬F.Reachable u v
s : F.ConnectedComponent := Quot.mk F.Reachable u
this✝ : v ∉ s
u' v' : V
huv : G.Adj (u', v').1 (u', v').2
left✝ : { fst := u', snd := v', adj := huv } ∈ p.darts
hu : { fst := u', snd := v', adj := huv }.toProd.1 ∈ s
hv : { fst := u', snd := v', adj := huv }.toProd.2 ∉ s
this : ¬F.Reachable v' u'
⊢ F ⊔ edge v' u' ≤ F

Tactic:
refine h.le_of_ge ⟨?_, h.prop.right.sup_edge_of_not_reachable this⟩ le_sup_left

Goal state after:
V : Type u_1
G F : SimpleGraph V
h : Maximal (fun H ↦ H ≤ G ∧ H.IsAcyclic) F
u v : V
x✝ : G.Reachable u v
p : G.Walk u v
this✝¹ : ¬F.Reachable u v
s : F.ConnectedComponent := Quot.mk F.Reachable u
this✝ : v ∉ s
u' v' : V
huv : G.Adj (u', v').1 (u', v').2
left✝ : { fst := u', snd := v', adj := huv } ∈ p.darts
hu : { fst := u', snd := v', adj := huv }.toProd.1 ∈ s
hv : { fst := u', snd := v', adj := huv }.toProd.2 ∉ s
this : ¬F.Reachable v' u'
⊢ F ⊔ edge v' u' ≤ G
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: 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
⊢ u ∈ {v}ᶜ

Tactic:
aesop

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

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

Tactic:
aesop

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

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

Tactic:
aesop

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

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

Tactic:
aesop

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

Goal state before:
pp: α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a₁✝ a₂✝ : Fin 3
a✝ :
  (fun x ↦
        match x with
        | 0 => w₁
        | 1 => v
        | 2 => w₂)
      a₁✝ =
    (fun x ↦
        match x with
        | 0 => w₁
        | 1 => v
        | 2 => w₂)
      a₂✝
this✝¹ : v ≠ w₁
this✝ : v ≠ w₂
this : w₁ ≠ w₂
⊢ a₁✝ = a₂✝

Tactic:
aesop

Goal state after: