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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : SemilatticeSup α
inst✝⁴ : SemilatticeSup β
inst✝³ : BoundedOrder β
inst✝² : DecidableLE α
inst✝¹ : OrderTop α
inst✝ : DecidableLE β
e : α ≃o β
s : Finset α
a : α
⊢ e (s.truncatedSup a) = (map e.toEmbedding s).truncatedSup (e a)

Tactic:
have : e a ∈ lowerClosure (s.map e.toEquiv.toEmbedding : Set β) ↔ a ∈ lowerClosure s := by simp
  simp_rw [truncatedSup, apply_dite e, map_finset_sup', map_top, this]
  congr with h
  simp only [filter_map, Function.comp_def, Equiv.coe_toEmbedding, RelIso.coe_fn_toEquiv,
    OrderIso.le_iff_le, id, sup'_map]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
⊢ t ∈ ∂⁺ 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = 1

Tactic:
mem_upShadow_iff,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
⊢ (∃ s ∈ 𝒜, ∃ a ∉ s, insert a s = t) ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = 1
Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h : IsLowerSet ↑𝒜
s : Finset α
⊢ s ∈ Finset.memberSubfamily a 𝒜 → s ∈ Finset.nonMemberSubfamily a 𝒜

Tactic:
by
  rw [mem_memberSubfamily, mem_nonMemberSubfamily]
  exact And.imp_left (h <| subset_insert _ _)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsUpperSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
⊢ 2 ^ Fintype.card α * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ

Tactic:
rw [← isLowerSet_compl, ← coe_compl] at h𝒜
  have := h𝒜.le_card_inter_finset hℬ
  rwa [card_compl, Fintype.card_finset, tsub_mul, tsub_le_iff_tsub_le, ← mul_tsub, ←
    card_sdiff_of_subset inter_subset_right, sdiff_inter_self_right, sdiff_compl,
    _root_.inf_comm] at this

Goal state after:
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
a b : α
hab : a ≤ b
ha : a ∈ ↑s
⊢ (↑(insert b s)).Intersecting

Tactic:
rw [coe_insert]

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
⊢ (insert b ↑s).Intersecting
Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsUpperSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
⊢ #𝒜 * #ℬ ≤ 2 ^ Fintype.card α * #(𝒜 ∩ ℬ)

Tactic:
rw [← isLowerSet_compl, ← coe_compl] at h𝒜
  have := h𝒜.card_inter_le_finset hℬ
  rwa [card_compl, Fintype.card_finset, tsub_mul, le_tsub_iff_le_tsub, ← mul_tsub, ←
    card_sdiff_of_subset inter_subset_right, sdiff_inter_self_right, sdiff_compl,
    _root_.inf_comm] at this
  · grw [inter_subset_right]
  · grw [← Fintype.card_finset, card_le_univ]

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

Goal state before:
pp: α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
a : α
ha : a ∉ ↑s ∧ aᶜ ∉ ↑s
⊢ (↑(insert a s)).Intersecting

Tactic:
rw [coe_insert]

Goal state after:
α : Type u_1
inst✝² : BooleanAlgebra α
inst✝¹ : Nontrivial α
inst✝ : Fintype α
s : Finset α
hs : (↑s).Intersecting
h : ∀ (t : Finset α), (↑t).Intersecting → s ⊆ t → s = t
a : α
ha : a ∉ ↑s ∧ aᶜ ∉ ↑s
⊢ (insert a ↑s).Intersecting
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ 𝒜.shatterer ↔ 𝒜.Shatters s

Tactic:
refine mem_filter.trans <| and_iff_right_of_imp fun h ↦ ?_

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : 𝒜.Shatters s
⊢ s ∈ 𝒜.biUnion powerset
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
_x : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v
a✝² :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    InvImage (fun x1 x2 ↦ x1 < x2) (fun x ↦ PSigma.casesOn x fun v' hv' ↦ PSigma.casesOn hv' fun hv' p ↦ p.length) y
        _x →
      v ∈ H.verts
v' : V
hv'✝ : (_ : v' ∈ H.verts) ×' G.Walk v' v
a✝¹ :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    InvImage (fun x1 x2 ↦ x1 < x2) (fun x ↦ PSigma.casesOn x fun v' hv' ↦ PSigma.casesOn hv' fun hv' p ↦ p.length) y
        ⟨v', hv'✝⟩ →
      v ∈ H.verts
hv' : v' ∈ H.verts
p : G.Walk v' v
a✝ :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    InvImage (fun x1 x2 ↦ x1 < x2) (fun x ↦ PSigma.casesOn x fun v' hv' ↦ PSigma.casesOn hv' fun hv' p ↦ p.length) y
        ⟨v', ⟨hv', p⟩⟩ →
      v ∈ H.verts
hnp : ¬p.Nil
⊢ p.tail.length < p.length

Tactic:
← Walk.length_tail_add_one hnp

Goal state after:
V : Type u
G : SimpleGraph V
v : V
H : G.Subgraph
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
_x : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v
a✝² :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    InvImage (fun x1 x2 ↦ x1 < x2) (fun x ↦ PSigma.casesOn x fun v' hv' ↦ PSigma.casesOn hv' fun hv' p ↦ p.length) y
        _x →
      v ∈ H.verts
v' : V
hv'✝ : (_ : v' ∈ H.verts) ×' G.Walk v' v
a✝¹ :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    InvImage (fun x1 x2 ↦ x1 < x2) (fun x ↦ PSigma.casesOn x fun v' hv' ↦ PSigma.casesOn hv' fun hv' p ↦ p.length) y
        ⟨v', hv'✝⟩ →
      v ∈ H.verts
hv' : v' ∈ H.verts
p : G.Walk v' v
a✝ :
  ∀ (y : (v' : V) ×' (_ : v' ∈ H.verts) ×' G.Walk v' v),
    InvImage (fun x1 x2 ↦ x1 < x2) (fun x ↦ PSigma.casesOn x fun v' hv' ↦ PSigma.casesOn hv' fun hv' p ↦ p.length) y
        ⟨v', ⟨hv', p⟩⟩ →
      v ∈ H.verts
hnp : ¬p.Nil
⊢ p.tail.length < p.tail.length + 1
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Fintype V
h : G.chromaticNumber = ↑(card V)
hh : G ≠ ⊤
a b : V
hne : a ≠ b
right✝ : ¬G.Adj a b
x : V
h' : x ≠ b
⊢ x ∈ Finset.univ.erase b

Tactic:
by simp [h']

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Fintype V
⊢ G.chromaticNumber ≤ ↑(card V)

Tactic:
by
  rw [← chromaticNumber_top]
  exact chromaticNumber_mono_of_hom G.selfColoring

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

Goal state before:
pp: case calc_1
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
⊢ ∑ s ∈ u.powerset, collapse 𝒜 a f s =
    (∑ i ∈ u.powerset, if i ∈ 𝒜 then f i else 0) + ∑ i ∈ image (insert a) u.powerset, if i ∈ 𝒜 then f i else 0

Tactic:
sum_image,

Goal state after:
case calc_1
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
⊢ ∑ s ∈ u.powerset, collapse 𝒜 a f s =
    (∑ i ∈ u.powerset, if i ∈ 𝒜 then f i else 0) + ∑ x ∈ u.powerset, if insert a x ∈ 𝒜 then f (insert a x) else 0

case calc_1
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
u : Finset α
h𝒜 : 𝒜 ⊆ (insert a u).powerset
hu : a ∉ u
⊢ Set.InjOn (insert a) ↑u.powerset
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝ : G.LocallyFinite
h : G.IsBipartiteWith ↑s ↑t
| ∑ x ∈ s.attach, #(G.neighborFinset ↑x)

Tactic:
rhs; intro v
    rw [isBipartiteWith_bipartiteAbove h v.prop]

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : Finset V
inst✝ : G.LocallyFinite
h : G.IsBipartiteWith ↑s ↑t
v : ↥s
| #(bipartiteAbove G.Adj t ↑v)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
hnil : ¬w.Nil
G' : G.Subgraph
hw : w.edgeSet ⊆ G'.edgeSet
v' : V
hv' : v' ∈ w.support
⊢ v' ∈ G'.verts

Tactic:
mem_support_iff_exists_mem_edges_of_not_nil hnil

Goal state after:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
hnil : ¬w.Nil
G' : G.Subgraph
hw : w.edgeSet ⊆ G'.edgeSet
v' : V
hv' : ∃ e ∈ w.edges, v' ∈ e
⊢ v' ∈ G'.verts
Module: Mathlib.Combinatorics.SimpleGraph.Bipartite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ #G.bipartiteDoubleCover.edgeFinset = 2 * #G.edgeFinset

Tactic:
rw [two_mul_card_edgeFinset, eq_comm]
  apply card_bij (fun (v, w) _ ↦ s(.inl v, .inr w))
    (fun _ h ↦ by simpa using h) (by grind) (fun e he ↦ ?_)
  induction e with | _ v w
  rw [mem_edgeFinset, mem_edgeSet] at he
  match v, w with
  | .inl _, .inr _ => simpa using he
  | .inr _, .inl _ => simpa using he.symm
  | .inl _, .inl _ | .inr _, .inr _ => simp at he

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

Goal state before:
pp: case inr
V : Type u
G : SimpleGraph V
u v v' : V
p : G.Walk u v
hp : p.IsPath
hadj : p.toSubgraph.Adj u v'
i : ℕ
hi : (p.getVert i = u ∧ p.getVert (i + 1) = v' ∨ p.getVert i = v' ∧ p.getVert (i + 1) = u) ∧ i < p.length
hr1 : p.getVert i = v'
hr2 : p.getVert (i + 1) = u
⊢ p.snd = v'

Tactic:
have : i + 1 = 0 := by
      apply hp.getVert_injOn (by rw [Set.mem_ofPred]; lia) (by rw [Set.mem_ofPred]; lia)
      rw [p.getVert_zero, hr2]

Goal state after:
case inr
V : Type u
G : SimpleGraph V
u v v' : V
p : G.Walk u v
hp : p.IsPath
hadj : p.toSubgraph.Adj u v'
i : ℕ
hi : (p.getVert i = u ∧ p.getVert (i + 1) = v' ∨ p.getVert i = v' ∧ p.getVert (i + 1) = u) ∧ i < p.length
hr1 : p.getVert i = v'
hr2 : p.getVert (i + 1) = u
this : i + 1 = 0
⊢ p.snd = v'
Module: Mathlib.Combinatorics.SimpleGraph.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
x : α × β
inst✝² : Fintype ↑(G.neighborSet x.1)
inst✝¹ : Fintype ↑(H.neighborSet x.2)
inst✝ : Fintype ↑((G □ H).neighborSet x)
⊢ (G □ H).neighborFinset x = (G.neighborFinset x.1 ×ˢ {x.2}).disjUnion ({x.1} ×ˢ H.neighborFinset x.2) ⋯

Tactic:
let : Fintype ((G □ H).neighborSet x) := SimpleGraph.boxProdFintypeNeighborSet _
  convert_to (G □ H).neighborFinset x = _ using 2
  exact Eq.trans (Finset.map_map _ _ _) Finset.attach_map_val

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

Goal state before:
pp: V : Type u_1
inst✝ : Fintype V
p : SimpleGraph V → Prop
x✝ : ∃ G, p G
G : SimpleGraph V
hp : p G
⊢ ?m.66

Tactic:
apply exists_max_image { G | p G } (#·.edgeFinset)
    use G, by simpa using hp

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
k : K
x y : V
⊢ (C.labelGraph k).Adj x y ↔ ∃ (H : G.Adj x y), C ⟨s(x, y), H⟩ = k

Tactic:
rw [EdgeLabeling.labelGraph]

Goal state after:
V : Type u_1
G : SimpleGraph V
K : Type u_3
C : G.EdgeLabeling K
k : K
x y : V
⊢ (fromEdgeSet {e | ∃ (h : e ∈ G.edgeSet), C ⟨e, h⟩ = k}).Adj x y ↔ ∃ (H : G.Adj x y), C ⟨s(x, y), H⟩ = k
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
hconn : G.Connected
⊢ ∃ v, (induce {v}ᶜ G).Preconnected

Tactic:
by
  nontriviality V using hconn.nonempty
  obtain ⟨v, hv⟩ := hconn.exists_connected_induce_compl_singleton_of_finite_nontrivial
  exact ⟨v, hv.preconnected⟩

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

Goal state before:
pp: α : Type u
G : SimpleGraph α
e : (pathGraph 3)ᶜ ↪g G
h : G.IsCompleteMultipartite
h0 : ¬G.Adj (e 0) (e 1)
h1 : ¬G.Adj (e 1) (e 2)
h2 : G.Adj (e 0) (e 2)
⊢ False

Tactic:
exact h.trans _ _ _ h0 h1 h2

Goal state after:
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
fp : Finpartition univ := h.finpartition
l : #fp.parts < #univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
cf : G.CliqueFree r
⊢ ∃ G' inst, G'.CliqueFree (r + 1) ∧ #G.edgeFinset < #G'.edgeFinset

Tactic:
use G ⊔ edge x y, inferInstance, cf.sup_edge x y

Goal state after:
case right
V : Type u_1
inst✝² : Fintype V
G : SimpleGraph V
inst✝¹ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
fp : Finpartition univ := ⋯
l : #fp.parts < #univ ∧ #fp.parts < r
x y : V
hn : x ≠ y
he : fp.part x = fp.part y
cf : G.CliqueFree r
⊢ #G.edgeFinset < #(G ⊔ edge x y).edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: r t : ℕ
v : Fin r × Fin t
| (completeEquipartiteGraph r t).degree v

Tactic:
degree_completeEquipartiteGraph v

Goal state after:
r t : ℕ
v : Fin r × Fin t
| (r - 1) * t
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: α : Type u
G : SimpleGraph α
inst✝ : Fintype α
n : ℕ
C : G.Coloring (Fin n)
t : ℕ
h : ∀ (c : Fin n), Fintype.card ↑(C.colorClass c) ≤ t
⊢ G ⊑ completeEquipartiteGraph n t

Tactic:
have (c : Fin n) : Nonempty (C.colorClass c ↪ Fin t) := by
    rw [Embedding.nonempty_iff_card_le, Fintype.card_fin]
    exact h c
  have F (c : Fin n) := Classical.arbitrary (C.colorClass c ↪ Fin t)
  have hF {c₁ c₂ v₁ v₂} (hc : c₁ = c₂) (hv : F c₁ v₁ = F c₂ v₂) : v₁.val = v₂.val := by
    let v₁' : C.colorClass c₂ := ⟨v₁, by simp [← hc]⟩
    have hv' : F c₁ v₁ = F c₂ v₁' := by
      apply congr_heq
      · rw [hc]
      · rw [Subtype.heq_iff_coe_eq]
        simp [hc]
    rw [hv'] at hv
    simpa [Subtype.ext_iff] using (F c₂).injective hv
  use ⟨fun v ↦ (C v, F (C v) ⟨v, C.mem_colorClass v⟩), C.valid⟩
  intro v w h
  rw [Prod.mk.injEq] at h
  exact hF h.1 h.2

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

Goal state before:
pp: case inr.a
n r c : ℕ
hr : r > 0
⊢ #({i ∈ range r | c ≡ n + i [MOD r]}) ≤ 1

Tactic:
rw [card_le_one_iff]

Goal state after:
case inr.a
n r c : ℕ
hr : r > 0
⊢ ∀ {a b : ℕ}, a ∈ {i ∈ range r | c ≡ n + i [MOD r]} → b ∈ {i ∈ range r | c ≡ n + i [MOD r]} → a = b
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case refine_3
α : Type u_1
G : SimpleGraph α
x✝ : Nonempty α ∧ Subsingleton α
left✝ : Nonempty α
right✝ : Subsingleton α
⊢ G.radius = 0

Tactic:
· rw [radius, ENat.iInf_eq_zero]
    use Classical.ofNonempty
    simpa [eccent] using Subsingleton.elim _

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : Nonempty α
⊢ G.ediam = ⊤ ↔ G.radius = ⊤

Tactic:
refine ⟨?_, fun hr ↦ eq_top_iff.mpr (hr ▸ radius_le_ediam)⟩
  contrapose
  intro hr
  obtain ⟨w, hw⟩ := G.exists_eccent_eq_radius
  have hdiam : G.ediam ≤ 2 * G.eccent w := ediam_le_two_mul_eccent w
  exact ne_top_of_lt <| lt_of_le_of_lt hdiam <| WithTop.mul_lt_top (ENat.natCast_lt_top 2) <|
    lt_top_iff_ne_top.mpr (hw ▸ hr)

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

Goal state before:
pp: α : Type u_1
⊢ ⊥.center = Set.univ

Tactic:
cases subsingleton_or_nontrivial α
  · exact center_eq_univ_of_subsingleton
  · rw [Set.eq_univ_iff_forall]
    intro u
    rw [mem_center_iff, eccent_bot, radius_bot]

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

Goal state before:
pp: case neg.refine_5
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
x✝³ x✝² : Finset V
hne : x✝³ ≠ x✝²
x✝¹ x✝ : V
w✝¹ : Fin r
h₁ : map { toFun := fun j ↦ f (w✝¹, j), inj' := ⋯ } univ = x✝³
w✝ : Fin r
h₂ : map { toFun := fun j ↦ f (w✝, j), inj' := ⋯ } univ = x✝²
h₁' : ∃ y, f (w✝¹, y) = x✝¹
h₂' : ∃ y, f (w✝, y) = x✝
⊢ G.Adj x✝¹ x✝

Tactic:
replace ⟨_, h₁'⟩ := h₁'

Goal state after:
case neg.refine_5
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
f : (completeEquipartiteGraph r t).Copy G
ht : ¬t = 0
x✝³ x✝² : Finset V
hne : x✝³ ≠ x✝²
x✝¹ x✝ : V
w✝² : Fin r
h₁ : map { toFun := fun j ↦ f (w✝², j), inj' := ⋯ } univ = x✝³
w✝¹ : Fin r
h₂ : map { toFun := fun j ↦ f (w✝¹, j), inj' := ⋯ } univ = x✝²
h₂' : ∃ y, f (w✝¹, y) = x✝
w✝ : Fin t
h₁' : f (w✝², w✝) = x✝¹
⊢ G.Adj x✝¹ x✝
Module: Mathlib.Combinatorics.SimpleGraph.Finsubgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : Finite V
ι : Sort u_1
f : ι → G.Finsubgraph
⊢ ↑(⨅ i, f i) = ⨅ i, ↑(f i)

Tactic:
rw [iInf, coe_sInf, iInf_range]

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

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

Tactic:
simpa [edgeFinset_deleteIncidenceSet_eq_filter]
      using! card_edgeFinset_deleteIncidenceSet_le_extremalNumber h v

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
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
⊢ SimpleGraph.map (⇑e₁.toEmbedding) G ∈ {G | G ≤ completeBipartiteGraph V W ∧ K.Free G}

Tactic:
mem_filter_univ,

Goal state after:
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁✝ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K✝ : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂✝ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
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
⊢ SimpleGraph.map (⇑e₁.toEmbedding) G ≤ completeBipartiteGraph V W ∧ K.Free (SimpleGraph.map (⇑e₁.toEmbedding) G)
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

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

Tactic:
mem_filter_univ,

Goal state after:
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
G : SimpleGraph (V ⊕ W)
h_le : G ≤ completeBipartiteGraph V W
h_free : (completeBipartiteGraph α β).Free G
⊢ SimpleGraph.map (⇑e₁.toEmbedding) G ≤ completeBipartiteGraph (Fin m) (Fin n) ∧
    K.Free (SimpleGraph.map (⇑e₁.toEmbedding) G)
Module: Mathlib.Combinatorics.SimpleGraph.Girth

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
a : α
w : G.Walk a a
hwc : w.IsCircuit
⊢ G.egirth ≤ ↑w.length

Tactic:
by_contra! hlg
  let w' : G.Walk a a := w.cycleBypass
  have hwc' : w'.IsCycle := hwc.isCycle_cycleBypass
  have hwlg' : w'.length < G.egirth := by
    grw [w.length_cycleBypass_le_length]
    exact hlg
  exact not_le_of_gt hwlg' (SimpleGraph.egirth_le_length hwc')

Goal state after:
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : ∀ i ∈ t, (s i).Finite
h : t.PairwiseDisjoint s
⊢ ∑ᶠ (i : ι) (_ : i ∈ t) (j : α) (_ : j ∈ s i), 1 = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).ncard

Tactic:
finsum_mem_congr rfl fun i hi ↦ finsum_one

Goal state after:
α : Type u_1
ι : Type u_2
t : Set ι
ht : t.Finite
s : ι → Set α
hs : ∀ i ∈ t, (s i).Finite
h : t.PairwiseDisjoint s
⊢ ∑ᶠ (i : ι) (_ : i ∈ t), (s i).ncard = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).ncard
Module: Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Goal state before:
pp: α : Type u_1
s : Finset α
G : SimpleGraph α
r k : ℕ
inst✝ : DecidableEq α
v w₁ w₂ : α
t : Finset α
hw : G.IsFiveWheelLike r k v w₁ w₂ s t
C : G.Coloring (Fin (r + 1))
h : Set.SurjOn (⇑C) (insert w₁ ↑s) Set.univ
this : Set.SurjOn (⇑C) (insert w₂ ↑t) Set.univ
x : α
hcx : C x = C v
y : α
hy : y ∈ insert w₂ ↑t
hcy : C y = C v
hx : x ∈ ↑s
⊢ x ∈ ↑(insert v s)

Tactic:
simp [hx]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
β : Type u_2
H : SimpleGraph β
a b : α
p : G.Walk a b
f : G →g H
hp : p.IsHamiltonian
h : (Walk.map f p).IsPath
⊢ Injective ⇑f

Tactic:
← Set.injOn_univ,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
G : SimpleGraph α
β : Type u_2
H : SimpleGraph β
a b : α
p : G.Walk a b
f : G →g H
hp : p.IsHamiltonian
h : (Walk.map f p).IsPath
⊢ Set.InjOn (⇑f) Set.univ
Module: Mathlib.Combinatorics.SimpleGraph.IncMatrix

Goal state before:
pp: R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝² : MulZeroOneClass R
inst✝¹ : DecidableEq α
inst✝ : DecidableRel G.Adj
a : α
e : Sym2 α
h : e ∈ G.incidenceSet a
⊢ incMatrix R G a e = 1

Tactic:
rw [incMatrix_apply, Set.indicator_of_mem h, Pi.one_apply]

Goal state after: