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

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
hs : s.Intersecting
h : ∀ (t : Set α), t.Intersecting → s ⊆ t → s = t
⊢ IsUpperSet s

Tactic:
rintro a b hab ha

Goal state after:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Set α
hs : s.Intersecting
h : ∀ (t : Set α), t.Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ s
⊢ b ∈ s
Module: Mathlib.Combinatorics.SetFamily.Intersecting

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Finset α
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
⊢ IsUpperSet ↑s

Tactic:
rintro a b hab ha

Goal state after:
α : Type u_1
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
s : Finset α
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
a b : α
hab : a ≤ b
ha : a ∈ ↑s
⊢ b ∈ ↑s
Module: Mathlib.Combinatorics.SetFamily.Kleitman

Goal state before:
pp: case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ i ∈ s, (↑(f i)).Intersecting) →
      #s ≤ Fintype.card α → #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) := fun j ↦ if hj : j ∈ cons i s hi then ⋯.choose else ∅
hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * #(f' j) = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting
hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)
⊢ 2 ^ Fintype.card α * (2 * #(f' i)) + 2 ^ Fintype.card α * 2 * #(s.biUnion f' ∩ (f' i)ᶜ) ≤
    2 ^ Fintype.card α * 2 * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - #(cons i s hi)))

Tactic:
mul_comm _ 2,

Goal state after:
case inr.cons
ι : Type u_1
α : Type u_2
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
this : DecidableEq ι
i : ι
s : Finset ι
hi : i ∉ s
ih :
  ∀ (f : ι → Finset (Finset α)),
    (∀ i ∈ s, (↑(f i)).Intersecting) →
      #s ≤ Fintype.card α → #(s.biUnion f) ≤ 2 ^ Fintype.card α - 2 ^ (Fintype.card α - #s)
f : ι → Finset (Finset α)
hf : ∀ i_1 ∈ cons i s hi, (↑(f i_1)).Intersecting
hs : #(cons i s hi) ≤ Fintype.card α
f' : ι → Finset (Finset α) := fun j ↦ if hj : j ∈ cons i s hi then ⋯.choose else ∅
hf₁ : ∀ j ∈ cons i s hi, f j ⊆ f' j ∧ 2 * #(f' j) = 2 ^ Fintype.card α ∧ (↑(f' j)).Intersecting
hf₂ : ∀ j ∈ cons i s hi, IsUpperSet ↑(f' j)
⊢ 2 ^ Fintype.card α * (2 * #(f' i)) + 2 * 2 ^ Fintype.card α * #(s.biUnion f' ∩ (f' i)ᶜ) ≤
    2 * 2 ^ Fintype.card α * (2 ^ Fintype.card α - 2 ^ (Fintype.card α - #(cons i s hi)))
Module: Mathlib.Combinatorics.SetFamily.Intersecting

Goal state before:
pp: case neg
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : #s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    #t₂ ≤ Fintype.card α / 2 → s ⊂ t₂ → (↑t₂).Intersecting → ∃ t, t₂ ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t).Intersecting
_hcard : #s ≤ Fintype.card α / 2
hs : (↑s).Intersecting
t : Finset α
ht : (↑t).Intersecting
hst : s ⊆ t ∧ s ≠ t
⊢ #t ≤ Fintype.card α / 2

Tactic:
rw [Nat.le_div_iff_mul_le Nat.two_pos, Nat.mul_comm]

Goal state after:
case neg
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s✝ : Finset α
this : #s✝ ≤ Fintype.card α / 2
s : Finset α
ih :
  ∀ {t₂ : Finset α},
    #t₂ ≤ Fintype.card α / 2 → s ⊂ t₂ → (↑t₂).Intersecting → ∃ t, t₂ ⊆ t ∧ 2 * #t = Fintype.card α ∧ (↑t).Intersecting
_hcard : #s ≤ Fintype.card α / 2
hs : (↑s).Intersecting
t : Finset α
ht : (↑t).Intersecting
hst : s ⊆ t ∧ s ≠ t
⊢ 2 * #t ≤ Fintype.card α
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
⊢ 𝒜.shatterer = 𝒜 ↔ IsLowerSet ↑𝒜

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ Subset.antisymm (fun s hs ↦ ?_) <| subset_shatterer h⟩
  · rw [← h]
    exact isLowerSet_shatterer _
  · obtain ⟨t, ht, hst⟩ := (mem_shatterer.1 hs).exists_superset
    exact h hst ht

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

Goal state before:
pp: case refine_3
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
⊢ #𝒜 ≤ #𝒜.shatterer

Tactic:
set ℬ : Finset (Finset α) :=
    ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer).image (insert a)

Goal state after:
case refine_3
α : Type u_1
inst✝ : DecidableEq α
𝒜✝ : Finset (Finset α)
a : α
𝒜 : Finset (Finset α)
ih₀ : #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer
ih₁ : #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer
ℬ : Finset (Finset α) := image (insert a) ((memberSubfamily a 𝒜).shatterer ∩ (nonMemberSubfamily a 𝒜).shatterer)
⊢ #𝒜 ≤ #𝒜.shatterer
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ ∀ ⦃x : Finset α⦄, (𝓓 a 𝒜).Shatters x → 𝒜.Shatters x

Tactic:
exact fun s hs ↦ hs.of_compression

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

Goal state before:
pp: case inr.inr
V : Type u
G : SimpleGraph V
hG : G.Connected
x y : V
h : (G.deleteEdges {s(x, y)}).Reachable x y
hxy : G.Adj x y
w : V
P : G.Walk w x
hP : P.IsPath
heP : s(x, y) ∈ P.edges
hyP : y ∈ P.support
P₁ : G.Walk w y := P.takeUntil y hyP
hxP₁ : x ∉ (P.takeUntil y hyP).support
heP₁ : s(x, y) ∉ P₁.edges
⊢ (G.deleteEdges {s(x, y)}).Reachable x w

Tactic:
exact h.trans (.symm ⟨P₁.toDeleteEdges {s(x, y)} (by grind)⟩)

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
α : Type u_2
inst✝ : Fintype α
s : Finset V
h : G.IsClique ↑s
hc : card α ≤ s.card
C : G.Coloring α
⊢ Set.SurjOn (⇑C) (↑s) Set.univ

Tactic:
intro _ _

Goal state after:
V : Type u
G : SimpleGraph V
α : Type u_2
inst✝ : Fintype α
s : Finset V
h : G.IsClique ↑s
hc : card α ≤ s.card
C : G.Coloring α
a✝¹ : α
a✝ : a✝¹ ∈ Set.univ
⊢ a✝¹ ∈ ⇑C '' ↑s
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity

Goal state before:
pp: case neg.inl
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
hs₂ : {s(u, v)}.encard < ↑2
hs₁ : {s(u, v)}.encard = ↑1
⊢ (G.deleteEdges {s(u, v)}).Reachable u v

pp: case neg.inr
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
x : Sym2 V
hs₂ : {x}.encard < ↑2
hs₁ : {x}.encard = ↑1
hx : s(u, v) ≠ x
⊢ (G.deleteEdges {x}).Reachable u v

Tactic:
· exact hr

Goal state after:
case neg.inr
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
x : Sym2 V
hs₂ : {x}.encard < ↑2
hs₁ : {x}.encard = ↑1
hx : s(u, v) ≠ x
⊢ (G.deleteEdges {x}).Reachable u v
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

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

Tactic:
simpa using (hc ⟨w, hw⟩ ⟨v, hv⟩).map H.hom

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w : V ⊕ V
val✝¹ val✝ : V
hadj : G.bipartiteDoubleCover.Adj (Sum.inl val✝¹) (Sum.inl val✝)
⊢ (completeBipartiteGraph V V).Adj (Sum.inl val✝¹) (Sum.inl val✝)

Tactic:
simp at hadj

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v w : V ⊕ V
val✝¹ val✝ : V
hadj : G.bipartiteDoubleCover.Adj (Sum.inr val✝¹) (Sum.inr val✝)
⊢ (completeBipartiteGraph V V).Adj (Sum.inr val✝¹) (Sum.inr val✝)

Tactic:
simp at hadj

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

Goal state before:
pp: case neg.inl
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hu : ¬↑u = n + 2 - 1
h✝ : ¬↑v = n + 2 - 1
hu' : ↑u + ↑1 < n + 2
hv' : ↑v + ↑1 < n + 2
huv : u - v = 1
⊢ ¬↑u % 2 = ↑v % 2

Tactic:
rw [← add_eq_of_eq_sub' huv.symm]

Goal state after:
case neg.inl
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hu : ¬↑u = n + 2 - 1
h✝ : ¬↑v = n + 2 - 1
hu' : ↑u + ↑1 < n + 2
hv' : ↑v + ↑1 < n + 2
huv : u - v = 1
⊢ ¬↑(v + 1) % 2 = ↑v % 2
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: case neg.inr
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hu : ¬↑u = n + 2 - 1
h✝ : ¬↑v = n + 2 - 1
hu' : ↑u + ↑1 < n + 2
hv' : ↑v + ↑1 < n + 2
huv : v - u = 1
⊢ ¬↑u % 2 = ↑v % 2

Tactic:
rw [← add_eq_of_eq_sub' huv.symm]

Goal state after:
case neg.inr
n✝ n : ℕ
h : 2 ≤ n + 2
u v : Fin (n + 2)
hu : ¬↑u = n + 2 - 1
h✝ : ¬↑v = n + 2 - 1
hu' : ↑u + ↑1 < n + 2
hv' : ↑v + ↑1 < n + 2
huv : v - u = 1
⊢ ¬↑u % 2 = ↑(u + 1) % 2
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : Nontrivial V
inst✝¹ : Finite ↑G.edgeSet
inst✝ : G.LocallyFinite
h : G.IsTree
u v : V
p : G.Walk u v
hp : p.IsPath
hmax : ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length
u' v' : V
hne : u' ≠ v'
p' : G.Walk u' v'
hp' : p'.IsPath
⊢ ∃ u v, u ≠ v ∧ G.degree u = 1 ∧ G.degree v = 1

Tactic:
have hnil : ¬p.Nil := by grind

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝² : Nontrivial V
inst✝¹ : Finite ↑G.edgeSet
inst✝ : G.LocallyFinite
h : G.IsTree
u v : V
p : G.Walk u v
hp : p.IsPath
hmax : ∀ (u' v' : V) (p' : G.Walk u' v'), p'.IsPath → p'.length ≤ p.length
u' v' : V
hne : u' ≠ v'
p' : G.Walk u' v'
hp' : p'.IsPath
hnil : ¬p.Nil
⊢ ∃ u v, u ≠ v ∧ G.degree u = 1 ∧ G.degree v = 1
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 b : Fin 3},
    G.Adj
        ({
            toFun := fun x ↦
              match x with
              | 0 => w₁
              | 1 => v
              | 2 => w₂,
            inj' := ⋯ }
          a)
        ({
            toFun := fun x ↦
              match x with
              | 0 => w₁
              | 1 => v
              | 2 => w₂,
            inj' := ⋯ }
          b) ↔
      (pathGraph 3)ᶜ.Adj a b

Tactic:
intro _ _

Goal state after:
α : Type u
G : SimpleGraph α
s : Set α
v w₁ w₂ : α
h : G.IsPathGraph3Compl v w₁ w₂
a✝ b✝ : Fin 3
⊢ G.Adj
      ({
          toFun := fun x ↦
            match x with
            | 0 => w₁
            | 1 => v
            | 2 => w₂,
          inj' := ⋯ }
        a✝)
      ({
          toFun := fun x ↦
            match x with
            | 0 => w₁
            | 1 => v
            | 2 => w₂,
          inj' := ⋯ }
        b✝) ↔
    (pathGraph 3)ᶜ.Adj a✝ b✝
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

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

Tactic:
set fp := h.finpartition
  apply le_antisymm (le_min fp.card_parts_le_card h.card_parts_le)
  by_contra! l
  rw [lt_min_iff] at l
  obtain ⟨x, -, y, -, hn, he⟩ :=
    exists_ne_map_eq_of_card_lt_of_maps_to l.1 fun a _ ↦ fp.part_mem.2 (mem_univ a)
  apply absurd h
  rw [IsTuranMaximal, IsExtremal]; push Not; rintro -
  have cf : G.CliqueFree r := by
    simp_rw [← cliqueFinset_eq_empty_iff, cliqueFinset, filter_eq_empty_iff, mem_univ,
      forall_true_left, isNClique_iff, and_comm, not_and, isClique_iff, Set.Pairwise]
    intro z zc; push Not; simp_rw [h.not_adj_iff_part_eq]
    exact exists_ne_map_eq_of_card_lt_of_maps_to (zc.symm ▸ l.2) fun a _ ↦
      fp.part_mem.2 (mem_univ a)
  use G ⊔ edge x y, inferInstance, cf.sup_edge x y
  convert! Nat.lt_add_one #G.edgeFinset
  convert! G.card_edgeFinset_sup_edge _ hn
  rwa [h.not_adj_iff_part_eq]

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
C : Set G.ConnectedComponent
⊢ Set.MapsTo G.connectedComponentMk (Quot.out '' C) C

Tactic:
by rintro c ⟨x, ⟨hx, rfl⟩⟩; simp_all [connectedComponentMk]

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

Goal state before:
pp: α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
⊢ (completeEquipartiteGraph r t).Copy G

Tactic:
by
  by_cases ht : t = 0
  · rw [completeEquipartiteGraph_eq_bot_iff.mpr <| .inr ht]
    have : IsEmpty (Fin r × Fin t) := by simp [ht, Fin.isEmpty]
    exact Copy.bot .ofIsEmpty
  · have : Nonempty (Fin r ↪ K.parts) := by
      rw [Embedding.nonempty_iff_card_le,
        Fintype.card_fin, card_coe, K.card_parts.resolve_right ht]
    let fᵣ : Fin r ↪ K.parts := Classical.arbitrary (Fin r ↪ K.parts)
    have (p : K.parts) : Nonempty (Fin t ↪ p) := by
      rw [Embedding.nonempty_iff_card_le, Fintype.card_fin, card_coe, K.card_mem_parts p.prop]
    let fₜ (p : K.parts) : Fin t ↪ p :=
      Classical.arbitrary (Fin t ↪ p)
    let f : (Fin r) × (Fin t) ↪ V := by
      use fun (i, j) ↦ fₜ (fᵣ i) j
      intro (i₁, j₁) (i₂, j₂) heq
      rw [Prod.mk.injEq]
      contrapose! heq with hne
      rcases eq_or_ne i₁ i₂ with heq | hne
      · rw [heq, ← Subtype.ext_iff.ne]
        exact (fₜ _).injective.ne (hne heq)
      · refine (K.isCompleteBetween (fᵣ _).prop (fᵣ _).prop ?_ (fₜ _ _).prop (fₜ _ _).prop).ne
        exact Subtype.ext_iff.ne.mp <| fᵣ.injective.ne hne
    refine ⟨⟨f, fun hne ↦ ?_⟩, f.injective⟩
    refine K.isCompleteBetween (fᵣ _).prop (fᵣ _).prop ?_ (fₜ _ _).prop (fₜ _ _).prop
    exact Subtype.ext_iff.ne.mp <| fᵣ.injective.ne hne

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
K : Set V
⊢ Pairwise fun C D ↦ Disjoint ↑C ↑D

Tactic:
rintro C D ne

Goal state after:
V : Type u
G : SimpleGraph V
K : Set V
C D : G.ComponentCompl K
ne : C ≠ D
⊢ Disjoint ↑C ↑D
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
v v' : V
e : G.Adj v v'
⊢ F.Adj ((u (Opposite.op (singletonFinsubgraph v))).toFun ⟨v, ⋯⟩)
    ((u (Opposite.op (singletonFinsubgraph v'))).toFun ⟨v', ⋯⟩)

Tactic:
have hv : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v) :=
      Quiver.Hom.op (CategoryTheory.homOfLE singletonFinsubgraph_le_adj_left)

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' : V
e : G.Adj v v'
hv : Opposite.op (finsubgraphOfAdj e) ⟶ Opposite.op (singletonFinsubgraph v)
⊢ F.Adj ((u (Opposite.op (singletonFinsubgraph v))).toFun ⟨v, ⋯⟩)
    ((u (Opposite.op (singletonFinsubgraph v'))).toFun ⟨v', ⋯⟩)
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 : ℕ
⊢ zarankiewicz m n s t ≤ x ↔
    ∀ ⦃G : SimpleGraph (V ⊕ W)⦄ [inst : DecidableRel G.Adj],
      G ≤ completeBipartiteGraph V W → (completeBipartiteGraph α β).Free G → #G.edgeFinset ≤ x

Tactic:
simp_rw [zarankiewicz_of_fintypeCard_eq hm hn hs ht,
    Finset.sup_le_iff, mem_filter, mem_univ, true_and]
  exact ⟨fun h _ _ h_le h_free ↦ (h _ ⟨h_le, h_free⟩).trans_eq' <| by convert rfl,
    fun h _ ⟨h_le, h_free⟩ ↦ by convert h h_le h_free⟩

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✝ : Subsingleton α
⊢ p.IsHamiltonian

Tactic:
by
  intro v
  rw [nil_iff_support_eq.mp p.nil_of_subsingleton, Subsingleton.elim v a, List.count_singleton_self]

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

Goal state before:
pp: case h
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
u v : α
he : G.IsBridge s(u, v)
this : Nontrivial α
hG : G.IsHamiltonian
p : G.Walk u u
hp : p.IsHamiltonianCycle
⊢ False

Tactic:
refine hp.isHamiltonian_tail.isPath.isTrail.not_mem_support_of_not_reachable
    (fun huv ↦ he <| .trans ?_ huv) he (hp.isHamiltonian_tail.mem_support v)

Goal state after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
G : SimpleGraph α
inst✝ : Fintype α
u v : α
he : G.IsBridge s(u, v)
this : Nontrivial α
hG : G.IsHamiltonian
p : G.Walk u u
hp : p.IsHamiltonianCycle
huv : (G.deleteEdges {s(u, v)}).Reachable p.snd v
⊢ (G.deleteEdges {s(u, v)}).Reachable (u, v).1 p.snd
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
M : G.Subgraph
f : G →g G'
hf : Injective ⇑f
hM : M.IsMatching
⊢ (Subgraph.map f M).IsMatching

Tactic:
rintro _ ⟨v, hv, rfl⟩
  obtain ⟨v', hv'⟩ := hM hv
  use f v'
  refine ⟨⟨v, v', hv'.1, rfl, rfl⟩, ?_⟩
  rintro _ ⟨w, w', hw, hw', rfl⟩
  cases hf hw'.symm
  rw [hv'.2 w' hw]

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

Goal state before:
pp: V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
f : G ≃g G'
x✝ : ↑G.edgeSet
⊢ f.symm.toCopy.lineGraph (f.toCopy.lineGraph x✝) = x✝

Tactic:
by simp [Copy.lineGraph, Copy.toLineGraphEmbedding, Sym2.map_map]

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

Goal state before:
pp: V : Type u_1
V' : Type u_2
G : SimpleGraph V
G' : SimpleGraph V'
f : G ≃g G'
x✝ : ↑G'.edgeSet
⊢ f.toCopy.lineGraph (f.symm.toCopy.lineGraph x✝) = x✝

Tactic:
by simp [Copy.lineGraph, Copy.toLineGraphEmbedding, Sym2.map_map]

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

Goal state before:
pp: V : Type u_1
r : V
⊢ (starGraph r).IsUniversal r

Tactic:
intro _ _

Goal state after:
V : Type u_1
r w✝ : V
a✝ : r ≠ w✝
⊢ (starGraph r).Adj r w✝
Module: Mathlib.Combinatorics.SimpleGraph.StronglyRegular

Goal state before:
pp: V : Type u
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v w : V
h : G.Adj v w
⊢ ((G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ) \ ({w} ∪ {v}) = (G.neighborFinset v)ᶜ ∩ (G.neighborFinset w)ᶜ

Tactic:
simpa using ⟨h, adj_symm _ h⟩

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

Goal state before:
pp: n k ℓ μ : ℕ
V : Type u
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
h : G.IsSRGWith n k ℓ μ
hn : 0 < n
⊢ k * (k - ℓ - 1) = (n - k - 1) * μ

Tactic:
by
  let := Classical.decEq V
  rw [← h.card, Fintype.card_pos_iff] at hn
  obtain ⟨v⟩ := hn
  convert! card_mul_eq_card_mul G.Adj (s := G.neighborFinset v) (t := Gᶜ.neighborFinset v) _ _
  · simp [h.regular v]
  · simp [h.compl.regular v]
  · intro w hw
    rw [mem_neighborFinset] at hw
    simp_rw [bipartiteAbove, ← mem_neighborFinset, filter_mem_eq_inter]
    have s : {v} ⊆ G.neighborFinset w \ G.neighborFinset v := by
      rw [singleton_subset_iff, mem_sdiff, mem_neighborFinset]
      exact ⟨hw.symm, G.notMem_neighborFinset_self v⟩
    rw [inter_comm, neighborFinset_compl, ← inter_sdiff_assoc, ← sdiff_eq_inter_compl,
      card_sdiff_of_subset s, card_singleton, ← sdiff_inter_self_left,
      card_sdiff_of_subset inter_subset_left]
    congr
    · simp [h.regular w]
    · simp_rw [inter_comm, neighborFinset_def, ← Set.toFinset_inter, ← h.of_adj v w hw,
        ← Set.toFinset_card]
      congr!
  · intro w hw
    simp_rw [neighborFinset_compl, mem_sdiff, mem_compl, mem_singleton, mem_neighborFinset,
      ← Ne.eq_def] at hw
    simp_rw [bipartiteBelow, adj_comm, ← mem_neighborFinset, filter_mem_eq_inter,
      neighborFinset_def, ← Set.toFinset_inter, ← h.of_not_adj hw.2.symm hw.1,
      ← Set.toFinset_card]
    congr!

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

Goal state before:
pp: case inr
V : Type u_1
G : SimpleGraph V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
u v : V
p : G.Walk u v
ht : p.IsEulerian
hn : u ≠ v
⊢ {x | ¬u = v ∧ (¬x = u → x = v)} = ∅ ∨ {x | ¬u = v ∧ (¬x = u → x = v)}.card = 2

Tactic:
· right
    convert_to _ = ({u, v} : Finset V).card
    · simp [hn]
    · congr
      ext x
      simp [hn, imp_iff_not_or]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
hveven : Even (Nat.card V)
h : ¬G.IsTutteViolator G.universalVerts
h' : ∀ (K : G.deleteUniversalVerts.coe.ConnectedComponent), G.deleteUniversalVerts.coe.IsClique K.supp
val✝ : Fintype V
M : G.Subgraph
hM : M.IsMatching
hsub : M.vertsᶜ ⊆ G.universalVerts
⊢ Even M.vertsᶜ.ncard

Tactic:
by simpa [Set.even_ncard_compl_iff hveven, -Set.toFinset_card,
      ← Set.ncard_eq_toFinset_card'] using hM.even_card

Goal state after:
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: μ ν : YoungDiagram
⊢ IsLowerSet ↑(μ.cells ∪ ν.cells)

Tactic:
by
        rw [Finset.coe_union]
        exact μ.isLowerSet.union ν.isLowerSet

Goal state after:
Module: Mathlib.Combinatorics.Tiling.Tile

Goal state before:
pp: G : Type u_1
X : Type u_2
ιₚ : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G X
ps : Protoset G X ιₚ
ppt : PlacedTile ps → Prop
pt : PlacedTile ps
h : ∀ (i : ιₚ) (gx : G), ppt { index := i, groupElts := ↑gx }
⊢ ppt pt

Tactic:
rcases pt with ⟨i, gx⟩
  induction gx using Quotient.inductionOn
  apply h

Goal state after:
Module: Mathlib.Combinatorics.Young.YoungDiagram

Goal state before:
pp: w : List ℕ
hw : w.SortedGE
i2 j2 i1 j1 : ℕ
hi : i1 ≤ i2
hj : j1 ≤ j2
h1 : (i2, j2).1 < w.length
h2 : (i2, j2).2 < w[(i2, j2).1]
⊢ w[i2] ≤ w[i1]

Tactic:
obtain rfl | h := eq_or_lt_of_le hi

Goal state after:
case inl
w : List ℕ
hw : w.SortedGE
j2 i1 j1 : ℕ
hj : j1 ≤ j2
hi : i1 ≤ i1
h1 : (i1, j2).1 < w.length
h2 : (i1, j2).2 < w[(i1, j2).1]
⊢ w[i1] ≤ w[i1]

case inr
w : List ℕ
hw : w.SortedGE
i2 j2 i1 j1 : ℕ
hi : i1 ≤ i2
hj : j1 ≤ j2
h1 : (i2, j2).1 < w.length
h2 : (i2, j2).2 < w[(i2, j2).1]
h : i1 < i2
⊢ w[i2] ≤ w[i1]