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

Goal state before:
pp: α : Type u_1
inst✝³ : SemilatticeInf α
s t : Finset α
a : α
inst✝² : DecidableLE α
inst✝¹ : BoundedOrder α
inst✝ : DecidableEq α
hs : a ∈ upperClosure ↑s
ht : ∀ x ∈ t, ¬x ≤ a
⊢ (s ∪ t).truncatedInf a = s.truncatedInf a

Tactic:
simp only [truncatedInf_of_mem, hs, filter_union, filter_false_of_mem ht, union_empty,
    upper_aux.2 (Or.inl hs)]

Goal state after:
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a : α
s t : UpperSet α
hst : s ⊓ t = Ici a
⊢ s = Ici a ∨ t = Ici a

Tactic:
have := mem_Ici_iff.2 (le_refl a)

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a : α
s t : UpperSet α
hst : s ⊓ t = Ici a
this : a ∈ Ici a
⊢ s = Ici a ∨ t = Ici a
Module: Mathlib.Order.Booleanisation

Goal state before:
pp: α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a✝ b✝ a b c : α
⊢ (a ⊔ c) \ (b \ a) ≤ a ⊔ c \ b

Tactic:
by
      simp [sup_left_comm (a := b \ a), sup_comm (a := b \ a)]

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
𝒜 : Finset (Finset α)
⊢ infSum 𝒜ᶜˢ + supSum 𝒜 = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1

Tactic:
by
  unfold infSum supSum
  rw [← @map_univ_of_surjective (Finset α) _ _ _ ⟨compl, compl_injective⟩ compl_surjective, sum_map]
  simp only [Function.Embedding.coeFn_mk, univ_map_embedding, ← compl_truncatedSup,
    ← sum_add_distrib, card_compl, cast_sub (card_le_univ _), choose_symm (card_le_univ _),
    ← add_div, sub_add_cancel, Fintype.sum_div_mul_card_choose_card]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
H : ∀ s ∈ ∂ 𝒜', s ∉ ∂ 𝒜 → u ⊆ s ∧ Disjoint v s ∧ (s ∪ v) \ u ∈ ∂ 𝒜 ∧ (s ∪ v) \ u ∉ ∂ 𝒜'
⊢ ∂ 𝒜' ⊆ 𝓒 u v (∂ 𝒜)

Tactic:
rintro s hs'
    rw [mem_compression]
    by_cases hs : s ∈ 𝒜.shadow
    swap
    · obtain ⟨hus, hvs, h, _⟩ := H _ hs' hs
      exact Or.inr ⟨hs, _, h, compress_of_disjoint_of_le' hvs hus⟩
    refine Or.inl ⟨hs, ?_⟩
    rw [compress]
    split_ifs with huvs
    swap
    · exact hs
    rw [mem_shadow_iff] at hs'
    obtain ⟨t, Ht, a, hat, rfl⟩ := hs'
    have hav : a ∉ v := notMem_mono huvs.2 (notMem_erase a t)
    have hvt : v ≤ t := huvs.2.trans (erase_subset _ t)
    have ht : t ∈ 𝒜 := mem_of_mem_compression Ht hvt (aux huv)
    by_cases hau : a ∈ u
    · obtain ⟨b, hbv, Hcomp⟩ := huv a hau
      refine mem_shadow_iff_insert_mem.2 ⟨b, notMem_sdiff_of_mem_right hbv, ?_⟩
      rw [← Hcomp.eq] at ht
      have hsb :=
        sup_sdiff_mem_of_mem_compression ht ((erase_subset _ _).trans hvt)
          (disjoint_erase_comm.2 huvs.1)
      rwa [sup_eq_union, sdiff_erase (mem_union_left _ <| hvt hbv), union_erase_of_mem hat, ←
        erase_union_of_mem hau] at hsb
    · refine mem_shadow_iff.2
        ⟨(t ⊔ u) \ v,
          sup_sdiff_mem_of_mem_compression Ht hvt <| disjoint_of_erase_right hau huvs.1, a, ?_, ?_⟩
      · rw [sup_eq_union, mem_sdiff, mem_union]
        exact ⟨Or.inl hat, hav⟩
      · simp [← erase_sdiff_comm, erase_union_distrib, erase_eq_of_notMem hau]

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

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
r : ℕ
i : DecidableRel fun x1 x2 ↦ x1 ⊆ x2 := fun x x_1 ↦ Classical.dec ((fun x1 x2 ↦ x1 ⊆ x2) x x_1)
s t : Finset α
h𝒜 : Set.Sized r ↑{∅}
hs : s ∈ ∂ {∅}
ht : t ∈ {∅} ∧ s ⊆ t
⊢ False

Tactic:
shadow_singleton_empty

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
r : ℕ
i : DecidableRel fun x1 x2 ↦ x1 ⊆ x2 := fun x x_1 ↦ Classical.dec ((fun x1 x2 ↦ x1 ⊆ x2) x x_1)
s t : Finset α
h𝒜 : Set.Sized r ↑{∅}
hs : s ∈ ∅
ht : t ∈ {∅} ∧ s ⊆ t
⊢ False
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
r : ℕ
i : DecidableRel fun x1 x2 ↦ x1 ⊆ x2 := fun x x_1 ↦ Classical.dec ((fun x1 x2 ↦ x1 ⊆ x2) x x_1)
s t : Finset α
h𝒜 : Set.Sized r ↑{∅}
hs : s ∈ ∂ {∅}
ht : t ∈ {∅} ∧ s ⊆ t
⊢ False

Tactic:
rw [shadow_singleton_empty] at hs

Goal state after:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
r : ℕ
i : DecidableRel fun x1 x2 ↦ x1 ⊆ x2 := fun x x_1 ↦ Classical.dec ((fun x1 x2 ↦ x1 ⊆ x2) x x_1)
s t : Finset α
h𝒜 : Set.Sized r ↑{∅}
hs : s ∈ ∅
ht : t ∈ {∅} ∧ s ⊆ t
⊢ False
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: case pos.inl
α : 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 α
hsv : s ∩ v = insert a (s ∩ u)
hv : v ∈ 𝒜 ∧ v.erase a ∈ 𝒜
⊢ (insert a (s ∩ u)).erase a = s ∩ u

Tactic:
erase_insert

Goal state after:
case pos.inl
α : 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 α
hsv : s ∩ v = insert a (s ∩ u)
hv : v ∈ 𝒜 ∧ v.erase a ∈ 𝒜
⊢ s ∩ u = s ∩ u

case pos.inl
α : 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 α
hsv : s ∩ v = insert a (s ∩ u)
hv : v ∈ 𝒜 ∧ v.erase a ∈ 𝒜
⊢ a ∉ s ∩ u
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case inl
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r ↑𝒜
usable : Finset (Finset (Fin n) × Finset (Fin n)) := {t | UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜}
husable : usable = ∅
⊢ ∃ ℬ, #(∂ ℬ) ≤ #(∂ 𝒜) ∧ #𝒜 = #ℬ ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ

pp: case inr
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r ↑𝒜
usable : Finset (Finset (Fin n) × Finset (Fin n)) := {t | UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜}
husable : usable.Nonempty
⊢ ∃ ℬ, #(∂ ℬ) ≤ #(∂ 𝒜) ∧ #𝒜 = #ℬ ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ

Tactic:
· refine ⟨𝒜, le_rfl, rfl, h, fun U V hUV ↦ ?_⟩
    rw [eq_empty_iff_forall_notMem] at husable
    by_contra h
    exact husable ⟨U, V⟩ <| mem_filter.2 ⟨mem_univ _, hUV, h⟩

Goal state after:
case inr
n r : ℕ
𝒜 : Finset (Finset (Fin n))
h : Set.Sized r ↑𝒜
usable : Finset (Finset (Fin n) × Finset (Fin n)) := {t | UsefulCompression t.1 t.2 ∧ ¬IsCompressed t.1 t.2 𝒜}
husable : usable.Nonempty
⊢ ∃ ℬ, #(∂ ℬ) ≤ #(∂ 𝒜) ∧ #𝒜 = #ℬ ∧ Set.Sized r ↑ℬ ∧ ∀ (U V : Finset (Fin n)), UsefulCompression U V → IsCompressed U V ℬ
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: case left
α : Type u_1
r : Setoid α
f : α → ↑r.classes := fun a ↦ ⟨{x | r x a}, ⋯⟩
f_respects_relation : ∀ (a b : α), r a b → f a = f b
q_a q_b : Quotient r
h_eq : Quot.lift f f_respects_relation q_a = Quot.lift f f_respects_relation q_b
⊢ q_a = q_b

Tactic:
induction q_a using Quotient.ind with | _ a
     =>  _ 

Goal state after:
case left.a
α : Type u_1
r : Setoid α
f : α → ↑r.classes := fun a ↦ ⟨{x | r x a}, ⋯⟩
f_respects_relation : ∀ (a b : α), r a b → f a = f b
q_b : Quotient r
a : α
h_eq : Quot.lift f f_respects_relation ⟦a⟧ = Quot.lift f f_respects_relation q_b
⊢ ⟦a⟧ = q_b
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mp.nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ Relation.ReflTransGen G.Adj u✝ u✝

Tactic:
| nil =>

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

Goal state before:
pp: case left
α : Type u_1
r : Setoid α
f : α → ↑r.classes := ⋯
f_respects_relation : ∀ (a b : α), r a b → f a = f b
⊢ Function.Injective (Quot.lift f f_respects_relation)

pp: case right
α : Type u_1
r : Setoid α
f : α → ↑r.classes := ⋯
f_respects_relation : ∀ (a b : α), r a b → f a = f b
⊢ Function.Surjective (Quot.lift f f_respects_relation)

Tactic:
· intro (q_a : Quotient r) (q_b : Quotient r) h_eq
    induction q_a using Quotient.ind with | _ a
    induction q_b using Quotient.ind with | _ b
    simp only [f, Quotient.lift_mk, Subtype.ext_iff] at h_eq
    apply Quotient.sound
    change a ∈ { x | r x b }
    rw [← h_eq]
    exact Setoid.refl a

Goal state after:
case right
α : Type u_1
r : Setoid α
f : α → ↑r.classes := ⋯
f_respects_relation : ∀ (a b : α), r a b → f a = f b
⊢ Function.Surjective (Quot.lift f f_respects_relation)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case nil
V : Type u
inst✝ : Nontrivial V
G : SimpleGraph V
h : G.Preconnected
v : V
hw : v ≠ v
⊢ v ∈ G.support

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
C : G.ConnectedComponent
u : V
hu hv : u ∈ C
⊢ C.toSimpleGraph.Walk ⟨u, hu⟩ ⟨u, hv⟩

Tactic:
| nil =>

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:
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 H' : G.Subgraph
hle : ∀ (v w : V), H.Adj v w → H'.Adj v w
hv : H.verts = H'.verts
h : H.Connected
⊢ H'.Connected

Tactic:
by
  exact h.mono ⟨hv.le, hle⟩ hv

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
⊢ w ∈ nil.toSubgraph.verts ↔ w ∈ nil.support

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ nil.reverse.toSubgraph = nil.toSubgraph

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v w u✝ : V
⊢ (nil.toSubgraph.neighborSet w).Finite

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
i : ℕ
hi : i < nil.length
⊢ nil.toSubgraph.Adj (nil.getVert i) (nil.getVert (i + 1))

Tactic:
| nil =>

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : DistribLattice α
inst✝⁴ : CommSemiring β
inst✝³ : LinearOrder β
inst✝² : IsStrictOrderedRing β
inst✝¹ : ExistsAddOfLE β
f₁ f₂ f₃ f₄ : α → β
inst✝ : DecidableEq α
h₁ : 0 ≤ f₁
h₂ : 0 ≤ f₂
h₃ : 0 ≤ f₃
h₄ : 0 ≤ f₄
h : ∀ (a b : α), f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b)
s t : Finset α
⊢ (∑ a ∈ s, f₁ a) * ∑ a ∈ t, f₂ a ≤ (∑ a ∈ s ⊼ t, f₃ a) * ∑ a ∈ s ⊻ t, f₄ a

Tactic:
set L : Sublattice α := ⟨latticeClosure (s ∪ t), isSublattice_latticeClosure.1,
    isSublattice_latticeClosure.2⟩
  have : Finite L := (s.finite_toSet.union t.finite_toSet).latticeClosure.to_subtype
  set s' : Finset L := s.preimage (↑) Subtype.coe_injective.injOn
  set t' : Finset L := t.preimage (↑) Subtype.coe_injective.injOn
  have hs' : s'.map ⟨L.subtype, Subtype.coe_injective⟩ = s := by
    simpa [s', map_eq_image, image_preimage, filter_eq_self] using!
      fun a ha ↦ subset_latticeClosure <| Set.subset_union_left ha
  have ht' : t'.map ⟨L.subtype, Subtype.coe_injective⟩ = t := by
    simpa [t', map_eq_image, image_preimage, filter_eq_self] using!
      fun a ha ↦ subset_latticeClosure <| Set.subset_union_right ha
  clear_value s' t'
  obtain ⟨β, _, _, g, hg⟩ := exists_birkhoff_representation L
  have := four_functions_theorem_aux (extend g (f₁ ∘ (↑)) 0) (extend g (f₂ ∘ (↑)) 0)
    (extend g (f₃ ∘ (↑)) 0) (extend g (f₄ ∘ (↑)) 0) (extend_nonneg (fun _ ↦ h₁ _) le_rfl)
    (extend_nonneg (fun _ ↦ h₂ _) le_rfl) (extend_nonneg (fun _ ↦ h₃ _) le_rfl)
    (extend_nonneg (fun _ ↦ h₄ _) le_rfl) ?_ (s'.map ⟨g, hg⟩) (t'.map ⟨g, hg⟩)
  · simpa only [← hs', ← ht', ← map_sups, ← map_infs, sum_map, Embedding.coeFn_mk, hg.extend_apply]
      using! this
  rintro s t
  obtain ⟨a, rfl⟩ | hs := em (∃ a, g a = s)
  · obtain ⟨b, rfl⟩ | ht := em (∃ b, g b = t)
    · simp_rw [← sup_eq_union, ← inf_eq_inter, ← map_sup, ← map_inf, hg.extend_apply]
      exact h _ _
    · simpa [extend_apply' _ _ _ ht] using! mul_nonneg
        (extend_nonneg (fun a : L ↦ h₃ a) le_rfl _) (extend_nonneg (fun a : L ↦ h₄ a) le_rfl _)
  · simpa [extend_apply' _ _ _ hs] using! mul_nonneg
      (extend_nonneg (fun a : L ↦ h₃ a) le_rfl _) (extend_nonneg (fun a : L ↦ h₄ a) le_rfl _)

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

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u v u✝ : V
⊢ Walk.nil.toSubgraph.Connected

Tactic:
| nil =>

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

Goal state before:
pp: case refine_1
V : Type u_1
G : SimpleGraph V
n : ℕ
hn : 2 < n
x✝ : cycleGraph n ⊑ G
h : (cycleGraph n).Copy G
⊢ ∃ v p, p.IsCycle ∧ p.length = n

pp: case refine_2
V : Type u_1
G : SimpleGraph V
n : ℕ
hn : 2 < n
h' : ∃ v p, p.IsCycle ∧ p.length = n
⊢ cycleGraph n ⊑ G

Tactic:
· have : n = n - 3 + 3 := by lia
    rw [this] at h
    refine ⟨h.toHom ⟨0, by lia⟩, Walk.map h.toHom <| cycleGraph.cycle (n - 3), ?_, ?_⟩
    · exact (isCycle_map_iff_of_injective h.injective).mpr cycleGraph.isCycle_cycle
    · simp [cycleGraph.length_cycle, ← this]

Goal state after:
case refine_2
V : Type u_1
G : SimpleGraph V
n : ℕ
hn : 2 < n
h' : ∃ v p, p.IsCycle ∧ p.length = n
⊢ cycleGraph n ⊑ G
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
f : G'.coe →g G
hpreconn : G''.Preconnected
u' : V
u : ↑G'.verts
hu : u ∈ G''.verts
hfu : f u = u'
v' : V
v : ↑G'.verts
hv : v ∈ G''.verts
hfv : f v = v'
⊢ (Subgraph.map f G'').coe.Reachable ⟨u', ⋯⟩ ⟨v', ⋯⟩

Tactic:
simp_rw [← hfu, ← hfv]

Goal state after:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
G'' : G'.coe.Subgraph
f : G'.coe →g G
hpreconn : G''.Preconnected
u' : V
u : ↑G'.verts
hu : u ∈ G''.verts
hfu : f u = u'
v' : V
v : ↑G'.verts
hv : v ∈ G''.verts
hfv : f v = v'
⊢ (Subgraph.map f G'').coe.Reachable ⟨f u, ⋯⟩ ⟨f v, ⋯⟩
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Counting

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
u : V
n : ℕ
⊢ nil ∈ {p | p.length = n + 1} ↔ nil ∈ ⋃ w, ⋃ (h : G.Adj u w), cons h '' {p' | p'.length = n}

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u_1
Hs : Set (SimpleGraph V)
hHs : Hs.Nonempty
h_dir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) Hs
u v u✝ : V
⊢ ∃ H ∈ Hs, ∀ e ∈ nil.edges, e ∈ H.edgeSet

Tactic:
| nil =>

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

Goal state before:
pp: case nil
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
v w u✝ : V
h : List.IsChain (fun x1 x2 ↦ x1 ≠ x2) nil.edges
⊢ nil.IsPath

Tactic:
| nil =>

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

Goal state before:
pp: case cons
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
v w u' v' w✝ : V
head : G.Adj u' v'
tail : G.Walk v' w✝
ih : List.IsChain (fun x1 x2 ↦ x1 ≠ x2) tail.edges → tail.IsPath
h : List.IsChain (fun x1 x2 ↦ x1 ≠ x2) (cons head tail).edges
hcc : (∀ y ∈ tail.edges.head?, s(u', v') ≠ y) ∧ List.IsChain (fun x1 x2 ↦ x1 ≠ x2) tail.edges
⊢ (cons head tail).IsPath

Tactic:
refine cons_isPath_iff head tail |>.mpr ⟨ih hcc.2, ?_⟩

Goal state after:
case cons
V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
v w u' v' w✝ : V
head : G.Adj u' v'
tail : G.Walk v' w✝
ih : List.IsChain (fun x1 x2 ↦ x1 ≠ x2) tail.edges → tail.IsPath
h : List.IsChain (fun x1 x2 ↦ x1 ≠ x2) (cons head tail).edges
hcc : (∀ y ∈ tail.edges.head?, s(u', v') ≠ y) ∧ List.IsChain (fun x1 x2 ↦ x1 ≠ x2) tail.edges
⊢ u' ∉ tail.support
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
⊢ G.edgeFinset.card + 1 = {default}ᶜ.card + 1

Tactic:
add_left_inj

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : Fintype ↑G.edgeSet
hG : G.IsTree
this✝ : Nonempty V
inhabited_h : Inhabited V
this : {default}ᶜ.card + 1 = Fintype.card V
⊢ G.edgeFinset.card = {default}ᶜ.card
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: case nil
α : Type u_1
G : SimpleGraph α
c : G.Coloring Bool
u v u✝ : α
⊢ Even Walk.nil.length ↔ (c u✝ = true ↔ c u✝ = true)

Tactic:
| nil =>

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

Goal state before:
pp: case mpr
α : Type u
G : SimpleGraph α
w✝² : Type u
w✝¹ : w✝² → Type u
w✝ : ∀ (i : w✝²), Nonempty (w✝¹ i)
e : G ≃g completeMultipartiteGraph w✝¹
⊢ G.IsCompleteMultipartite

Tactic:
refine ⟨fun _ _ _ h1 h2 ↦ ?_⟩

Goal state after:
case mpr
α : Type u
G : SimpleGraph α
w✝² : Type u
w✝¹ : w✝² → Type u
w✝ : ∀ (i : w✝²), Nonempty (w✝¹ i)
e : G ≃g completeMultipartiteGraph w✝¹
x✝² x✝¹ x✝ : α
h1 : ¬G.Adj x✝² x✝¹
h2 : ¬G.Adj x✝¹ x✝
⊢ ¬G.Adj x✝² x✝
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: r t : ℕ
⊢ completeEquipartiteGraph r t = ⊥ ↔ r ≤ 1 ∨ t = 0

Tactic:
contrapose!
  rw [← edgeSet_nonempty, ← Nat.succ_le_iff, ← Fin.nontrivial_iff_two_le, ← Nat.pos_iff_ne_zero,
    Fin.pos_iff_nonempty]
  refine ⟨fun ⟨e, he⟩ ↦ ?_, fun ⟨⟨i₁, i₂, hv⟩, ⟨x⟩⟩ ↦ ?_⟩
  · induction e with | _ v₁ v₂
    rw [mem_edgeSet, completeEquipartiteGraph_adj] at he
    exact ⟨⟨v₁.1, v₂.1, he⟩, ⟨v₁.2⟩⟩
  · use s((i₁, x), (i₂, x))
    rw [mem_edgeSet, completeEquipartiteGraph_adj]
    exact hv

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

Goal state before:
pp: n : ℕ
α : Type u_2
inst✝¹ : Fintype α
inst✝ : Nontrivial α
| extremalNumber n ⊤ = #(turanGraph n (Fintype.card α - 1)).edgeFinset

Tactic:
enter [1, 1]
    rw [← Fintype.card_fin n]

Goal state after:
n : ℕ
α : Type u_2
inst✝¹ : Fintype α
inst✝ : Nontrivial α
| Fintype.card (Fin n)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n : ℕ
α : Type u_2
inst✝¹ : Fintype α
inst✝ : Nontrivial α
⊢ extremalNumber (Fintype.card (Fin n)) ⊤ = #(turanGraph n (Fintype.card α - 1)).edgeFinset

Tactic:
exact (card_edgeFinset_of_isExtremal_free isExtremal_top_free_turanGraph).symm

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
⊢ ∃ x, s ∩ c.supp = {x}

Tactic:
by
  obtain ⟨a, ha⟩ := existsUnique_rep hrep h
  aesop

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
a : V
ha : s ∩ c.supp = {a}
⊢ c.supp.ncard - {a}.ncard = c.supp.ncard - 1

pp: V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
a : V
ha : s ∩ c.supp = {a}
⊢ {a} ⊆ c.supp

Tactic:
Set.ncard_singleton

Goal state after:
V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
a : V
ha : s ∩ c.supp = {a}
⊢ c.supp.ncard - 1 = c.supp.ncard - 1

V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
s : Set V
c : G.ConnectedComponent
hrep : Represents s C
h : c ∈ C
a : V
ha : s ∩ c.supp = {a}
⊢ {a} ⊆ c.supp
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case pos
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : t = 0
this : ∀ (r' : ℕ), IsEmpty (Fin r' × Fin t)
h_bot : ∀ (r' : ℕ), completeEquipartiteGraph r' t = ⊥
⊢ ⊥ ⊑ G ↔ ∃ K, True

Tactic:
exists_true_iff_nonempty

Goal state after:
case pos
V : Type u_1
G : SimpleGraph V
r t : ℕ
ht : t = 0
this : ∀ (r' : ℕ), IsEmpty (Fin r' × Fin t)
h_bot : ∀ (r' : ℕ), completeEquipartiteGraph r' t = ⊥
⊢ ⊥ ⊑ G ↔ Nonempty (G.CompleteEquipartiteSubgraph r t)
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: case nil
V : Type u
G : SimpleGraph V
K L M : Set V
β : Sort u_1
f : ⦃v : V⦄ → v ∉ K → β
h : ∀ ⦃v w : V⦄ (hv : v ∉ K) (hw : w ∉ K), G.Adj v w → f hv = f hw
v w u✝ : ↑Kᶜ
⊢ Walk.nil.IsPath → f ⋯ = f ⋯

Tactic:
| nil =>

Goal state after:
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
⊢ (induce Kᶜ G).Reachable ⟨d, dnK⟩ ⟨c, cnK⟩

Tactic:
exact Adj.reachable cd.symm

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.FiveWheelLike

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
r k : ℕ
x v w₁ w₂ : α
s t : Finset α
inst✝ : DecidableEq α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
hcf : G.CliqueFree (r + 2)
hW : ∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y
a : α
ha : a ∈ insert w₁ s
haj : ¬G.Adj x a
b : α
hb : b ∈ insert w₂ t
hbj : ¬G.Adj x b
c : α
hc : c ∈ insert v s
hcj : ¬G.Adj x c
d : α
hd : d ∈ insert v t
hdj : ¬G.Adj x d
⊢ ∃ a b c d,
    a ∈ insert w₁ s ∧
      ¬G.Adj x a ∧
        b ∈ insert w₂ t ∧
          ¬G.Adj x b ∧ c ∈ insert v s ∧ ¬G.Adj x c ∧ d ∈ insert v t ∧ ¬G.Adj x d ∧ a ≠ b ∧ a ≠ d ∧ b ≠ c ∧ a ∉ t ∧ b ∉ s

Tactic:
exact ⟨_, _, _, _, ha, haj, hb, hbj, hc, hcj, hd, hdj, by grind⟩

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v : V
hv : v ∈ M.verts
⊢ v ∈ M.support

Tactic:
obtain ⟨w, hvw, -⟩ := h hv

Goal state after:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v : V
hv : v ∈ M.verts
w : V
hvw : M.Adj v w
⊢ v ∈ M.support
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
c : G.ConnectedComponent
v✝ : V
hv : v✝ ∈ (M.induce (M.verts ∩ c.supp)).verts
⊢ ∃! w, (M.induce (M.verts ∩ c.supp)).Adj v✝ w

Tactic:
obtain ⟨hv, rfl⟩ := hv

Goal state after:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
v✝ : V
hv : v✝ ∈ M.verts
⊢ ∃! w, (M.induce (M.verts ∩ (G.connectedComponentMk v✝).supp)).Adj v✝ w
Module: Mathlib.Combinatorics.SimpleGraph.LapMatrix

Goal state before:
pp: case nil
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
x : V → ℝ
h : ∀ (i j : V), G.Adj i j → x i = x j
i j u✝ : V
⊢ x u✝ = x u✝

Tactic:
| nil =>

Goal state after: