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

Goal state before:
pp: case insert
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
a : α
u : Finset α
a✝ : a ∉ u
ih : ∀ (𝒜 : Finset (Finset α)), (∀ s ∈ 𝒜, s ⊆ u) → p 𝒜
𝒜 : Finset (Finset α)
hu : ∀ s ∈ 𝒜, s ⊆ insert a u
⊢ p 𝒜

Tactic:
refine subfamily a (ih _ ?_) (ih _ ?_)

Goal state after:
case insert.refine_1
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
a : α
u : Finset α
a✝ : a ∉ u
ih : ∀ (𝒜 : Finset (Finset α)), (∀ s ∈ 𝒜, s ⊆ u) → p 𝒜
𝒜 : Finset (Finset α)
hu : ∀ s ∈ 𝒜, s ⊆ insert a u
⊢ ∀ s ∈ nonMemberSubfamily a 𝒜, s ⊆ u

case insert.refine_2
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
a : α
u : Finset α
a✝ : a ∉ u
ih : ∀ (𝒜 : Finset (Finset α)), (∀ s ∈ 𝒜, s ⊆ u) → p 𝒜
𝒜 : Finset (Finset α)
hu : ∀ s ∈ 𝒜, s ⊆ insert a u
⊢ ∀ s ∈ memberSubfamily a 𝒜, s ⊆ u
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case mp
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
x : ℕ
hx : x ∈ {0}ᶜ
hx' : x ∉ A
⊢ 1 - (↑x)⁻¹ < 1

Tactic:
simpa only [one_div, sub_lt_self_iff, inv_pos, Nat.cast_pos, pos_iff_ne_zero] using! hx

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Finset ℕ
⊢ schnirelmannDensity ↑A = 0

Tactic:
by
  refine le_antisymm ?_ schnirelmannDensity_nonneg
  simp only [schnirelmannDensity_le_iff_forall, zero_add]
  intro ε hε
  wlog hε₁ : ε ≤ 1 generalizing ε
  · obtain ⟨n, hn, hn'⟩ := this 1 zero_lt_one le_rfl
    exact ⟨n, hn, hn'.trans_le (le_of_not_ge hε₁)⟩
  let n : ℕ := ⌊#A / ε⌋₊ + 1
  have hn : 0 < n := Nat.succ_pos _
  use n, hn
  rw [div_lt_iff₀ (Nat.cast_pos.2 hn), ← div_lt_iff₀' hε, Nat.cast_add_one]
  exact (Nat.lt_floor_add_one _).trans_le' <| by gcongr; simp [subset_iff]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
k : ℕ
⊢ ∂^[k] ∅ = ∅

Tactic:
by
  induction k <;> simp [*, shadow_empty]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
⊢ #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)

Tactic:
by_cases h𝒜 : s ∈ upperClosure (𝒜 : Set <| Finset α)

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∈ upperClosure ↑𝒜
⊢ #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∉ upperClosure ↑𝒜
⊢ #((𝒜 ∪ ℬ).truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #(ℬ.truncatedInf s)
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ t ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ #t = #s + k

Tactic:
by
  refine mem_upShadow_iterate_iff_exists_sdiff.trans <| exists_congr fun t ↦ and_congr_right fun _ ↦
    and_congr_right fun hst ↦ ?_
  rw [card_sdiff_of_subset hst, tsub_eq_iff_eq_add_of_le, add_comm]
  exact card_mono hst

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:
unfold infSum supSum

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
𝒜 : Finset (Finset α)
⊢ ∑ s, ↑(#(𝒜ᶜˢ.truncatedInf s)) / (↑(#s) * ↑((card α).choose #s)) +
      ∑ s, ↑(#(𝒜.truncatedSup s)) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) =
    ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case pos
α : 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 ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ⊆ t.erase a
hav : a ∉ v
hvt : v ⊆ t
ht : t ∈ 𝒜
hau : a ∈ u
b : α
hbv : b ∈ v
Hcomp : IsCompressed (u.erase a) (v.erase b) 𝒜
⊢ (t.erase a ⊔ u) \ v ∈ ∂ 𝒜

Tactic:
refine mem_shadow_iff_insert_mem.2 ⟨b, notMem_sdiff_of_mem_right hbv, ?_⟩

Goal state after:
case pos
α : 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 ∉ ∂ 𝒜'
t : Finset α
Ht : t ∈ 𝒜'
a : α
hat : a ∈ t
hs : t.erase a ∈ ∂ 𝒜
huvs : Disjoint u (t.erase a) ∧ v ⊆ t.erase a
hav : a ∉ v
hvt : v ⊆ t
ht : t ∈ 𝒜
hau : a ∈ u
b : α
hbv : b ∈ v
Hcomp : IsCompressed (u.erase a) (v.erase b) 𝒜
⊢ insert b ((t.erase a ⊔ u) \ v) ∈ 𝒜
Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman

Goal state before:
pp: α : 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
𝒞 : Finset (Finset α)
h𝒞 : ∀ t ∈ 𝒞, t ⊆ insert a s
t : Finset α
ht : t ∈ Finset.nonMemberSubfamily a 𝒞
⊢ t ⊆ s

Tactic:
rw [mem_nonMemberSubfamily] at ht

Goal state after:
α : 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
𝒞 : Finset (Finset α)
h𝒞 : ∀ t ∈ 𝒞, t ⊆ insert a s
t : Finset α
ht : t ∈ 𝒞 ∧ a ∉ t
⊢ t ⊆ s
Module: Mathlib.Combinatorics.SetFamily.Intersecting

Goal state before:
pp: α : Type u_1
inst✝ : BooleanAlgebra α
s : Finset α
hs : (↑s).Intersecting
⊢ Disjoint s (map { toFun := compl, inj' := ⋯ } s)

Tactic:
by
  rw [Finset.disjoint_left]
  rintro x hx hxc
  obtain ⟨x, hx', rfl⟩ := mem_map.mp hxc
  exact hs.compl_notMem hx' hx

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

Goal state before:
pp: case mp
α : Type u_1
c : Set (Set α)
hc : IsPartition c
s : Set α
⊢ s ∈ (mkClasses c ⋯).classes → s ∈ c

pp: case mpr
α : Type u_1
c : Set (Set α)
hc : IsPartition c
s : Set α
⊢ s ∈ c → s ∈ (mkClasses c ⋯).classes

Tactic:
· rintro ⟨y, rfl⟩
    obtain ⟨b, ⟨hb, hy⟩, _⟩ := hc.2 y
    rwa [← eq_eqv_class_of_mem _ hb hy]

Goal state after:
case mpr
α : Type u_1
c : Set (Set α)
hc : IsPartition c
s : Set α
⊢ s ∈ c → s ∈ (mkClasses c ⋯).classes
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
h1r : r > 0
size : (n - 1).choose (r - 1) < #𝒜
A : Finset (Fin n)
hA : A ∈ 𝒜
C : Finset (Fin n)
hC : Cᶜ ∈ 𝒜
hAC : A ⊆ C
right✝ : #(C \ A) = n - 2 * r
⊢ False

Tactic:
exact h𝒜 hA hC (disjoint_of_subset_left hAC disjoint_compl_right)

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
v w : V
hadj : G.Adj v w
⊢ v ∈ t ∧ w ∈ s ∨ v ∈ s ∧ w ∈ t

Tactic:
@and_comm (v ∈ t) (w ∈ s),

Goal state after:
V : Type u_1
G : SimpleGraph V
s t : Set V
h : G.IsBipartiteWith s t
v w : V
hadj : G.Adj v w
⊢ w ∈ s ∧ v ∈ t ∨ v ∈ s ∧ w ∈ t
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.IsEdgeReachable 1 u v ↔ G.Reachable u v

Tactic:
by
  simp [IsEdgeReachable, Order.lt_one_iff]

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 v
⊢ u ∈ p.toSubgraph.verts

Tactic:
simp [mem_verts_toSubgraph]

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 v
⊢ v ∈ p.toSubgraph.verts

Tactic:
simp [mem_verts_toSubgraph]

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

Goal state before:
pp: case nil
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
f : G →g G'
u✝ : V
⊢ (Walk.map f nil).toSubgraph = Subgraph.map f nil.toSubgraph

Tactic:
simp [*, Subgraph.map_sup]

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

Goal state before:
pp: case cons
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u v : V
f : G →g G'
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : (Walk.map f p✝).toSubgraph = Subgraph.map f p✝.toSubgraph
⊢ (Walk.map f (cons h✝ p✝)).toSubgraph = Subgraph.map f (cons h✝ p✝).toSubgraph

Tactic:
simp [*, Subgraph.map_sup]

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

Goal state before:
pp: V : Type u_1
u v : V
inst✝ : DecidableEq V
⊢ ⊥.edist u v = if u = v then 0 else ⊤

Tactic:
by
  by_cases h : u = v <;> simp [h, edist_bot_of_ne]

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

Goal state before:
pp: case neg
V : Type u_1
G : SimpleGraph V
u v w : V
hadj : G.Adj v w
huw : G.Reachable u w
this : G.dist v w = 1
⊢ G.dist u w = G.dist u v ∨ G.dist u w = G.dist u v + 1 ∨ G.dist u w = G.dist u v - 1

Tactic:
have : G.dist w v = 1 := dist_eq_one_iff_adj.mpr hadj.symm

Goal state after:
case neg
V : Type u_1
G : SimpleGraph V
u v w : V
hadj : G.Adj v w
huw : G.Reachable u w
this✝ : G.dist v w = 1
this : G.dist w v = 1
⊢ G.dist u w = G.dist u v ∨ G.dist u w = G.dist u v + 1 ∨ G.dist u w = G.dist u v - 1
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.length = G.dist u v
⊢ p.IsPath

Tactic:
have : p.bypass = p := by
    apply bypass_eq_self_of_length_le_length_bypass
    calc p.length
      _ = G.dist u v := hp
      _ ≤ p.bypass.length := dist_le p.bypass

Goal state after:
V : Type u_1
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : p.length = G.dist u v
this : p.bypass = p
⊢ p.IsPath
Module: Mathlib.Combinatorics.SimpleGraph.CycleGraph

Goal state before:
pp: n : ℕ
v : Fin (n + 3)
⊢ ¬1 + 1 = 0

Tactic:
exact ne_of_beq_false rfl

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, C.labelGraph k = G

Tactic:
ext x y
  simp only [iSup_adj, EdgeLabeling.labelGraph_adj]
  grind

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

Goal state before:
pp: case w
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
⊢ 2 ≤ List.count u pwz.support + List.count u pzx.support.tail

Tactic:
have := List.one_le_count_iff.mpr (pzx.snd_mem_tail_support (not_nil_of_ne (by aesop)))

Goal state after:
case w
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
⊢ 2 ≤ List.count u pwz.support + List.count u pzx.support.tail
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 : ℕ
s : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
⊢ G.degree s = #{t | G.Adj s t}

Tactic:
simp [← card_neighborFinset_eq_degree, neighborFinset]

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

Goal state before:
pp: case inr
r t : ℕ
ht_pos : t > 0
⊢ (completeEquipartiteGraph r t).IsCompleteMultipartite

Tactic:
rw [isCompleteMultipartite_iff]
    use (Fin r), const (Fin r) (Fin t)
    simp_rw [const_apply, exists_prop]
    exact ⟨const (Fin r) (Fin.pos_iff_nonempty.mp ht_pos),
      ⟨completeEquipartiteGraph.completeMultipartiteGraph⟩⟩

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
⊢ K.verts = K.parts.biUnion id

Tactic:
rw [verts, disjiUnion_eq_biUnion]

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

Goal state before:
pp: case inj'.inl
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : ¬t = 0
this✝ : Nonempty (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
this : ∀ (p : ↥K.parts), Nonempty (Fin t ↪ ↥↑p)
fₜ : (p : ↥K.parts) → Fin t ↪ ↥↑p := fun p ↦ Classical.arbitrary (Fin t ↪ ↥↑p)
i₁ : Fin r
j₁ : Fin t
i₂ : Fin r
j₂ : Fin t
hne : i₁ = i₂ → j₁ ≠ j₂
heq : i₁ = i₂
⊢ (fₜ (fᵣ i₂)) j₁ ≠ (fₜ (fᵣ i₂)) j₂

Tactic:
exact (fₜ _).injective.ne (hne heq)

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

Goal state before:
pp: case inl
α : Type u_1
G : SimpleGraph α
h : ¬G.Connected
h✝ : IsEmpty α
⊢ G.diam = 0

Tactic:
rw [diam, ediam, ciSup_of_empty, bot_eq_zero']

Goal state after:
case inl
α : Type u_1
G : SimpleGraph α
h : ¬G.Connected
h✝ : IsEmpty α
⊢ ENat.toNat 0 = 0
Module: Mathlib.Combinatorics.SimpleGraph.Ends.Defs

Goal state before:
pp: V : Type u
G : SimpleGraph V
K : Set V
Gc : G.Preconnected
hK : K.Nonempty
⊢ ∀ (C : G.ComponentCompl K), ∃ ck, ck.1 ∈ C ∧ ck.2 ∈ K ∧ G.Adj ck.1 ck.2

Tactic:
refine ComponentCompl.ind fun v vnK => ?_
  let C : G.ComponentCompl K := G.componentComplMk vnK
  let dis := Set.disjoint_iff.mp C.disjoint_right
  by_contra! h
  suffices Set.univ = (C : Set V) by exact dis ⟨hK.choose_spec, this ▸ Set.mem_univ hK.some⟩
  symm
  rw [Set.eq_univ_iff_forall]
  rintro u
  by_contra unC
  obtain ⟨p⟩ := Gc v u
  obtain ⟨⟨⟨x, y⟩, xy⟩, -, xC, ynC⟩ :=
    p.exists_boundary_dart (C : Set V) (G.componentComplMk_mem vnK) unC
  exact ynC (mem_of_adj x y xC (fun yK : y ∈ K => h ⟨x, y⟩ xC yK xy) xy)

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

Goal state before:
pp: case e'_4
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
cf : G.CliqueFree (r + 1)
hr : r > 0
H : SimpleGraph V
w✝ : DecidableRel H.Adj
maxH : H.IsTuranMaximal r
⊢ (Fintype.card V ^ 2 - (Fintype.card V % r) ^ 2) * (r - 1) / (2 * r) + (Fintype.card V % r).choose 2 = #H.edgeFinset

Tactic:
((isTuranMaximal_iff_nonempty_iso_turanGraph hr).mp maxH).some.card_edgeFinset_eq,

Goal state after:
case e'_4
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
cf : G.CliqueFree (r + 1)
hr : r > 0
H : SimpleGraph V
w✝ : DecidableRel H.Adj
maxH : H.IsTuranMaximal r
⊢ (Fintype.card V ^ 2 - (Fintype.card V % r) ^ 2) * (r - 1) / (2 * r) + (Fintype.card V % r).choose 2 =
    #(turanGraph (Fintype.card V) r).edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

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

Tactic:
mem_edgeFinset

Goal state after:
case refine_1
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁✝ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K✝ : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂✝ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
e₁ : completeBipartiteGraph (Fin m) (Fin n) ≃g completeBipartiteGraph V W := e₁✝.symm
K : SimpleGraph (α ⊕ β) := completeBipartiteGraph α β
e₂ : completeBipartiteGraph (Fin s) (Fin t) ≃g completeBipartiteGraph α β := e₂✝.symm
G : SimpleGraph (Fin m ⊕ Fin n)
h_le : G ≤ completeBipartiteGraph (Fin m) (Fin n)
h_free : (completeBipartiteGraph (Fin s) (Fin t)).Free G
h' : SimpleGraph.map (⇑e₁.toEmbedding) G ∈ {G | G ≤ completeBipartiteGraph V W ∧ K.Free G}
h_le_sup :
  Fintype.card { x // x ∈ (SimpleGraph.map (⇑e₁.toEmbedding) G).edgeSet } ≤
    {G | G ≤ completeBipartiteGraph V W ∧ K.Free G}.sup fun x ↦ Fintype.card { x_1 // x_1 ∈ x.edgeSet }
⊢ Fintype.card { x // x ∈ (SimpleGraph.map (⇑e₁.toEquiv) G).edgeSet } ≤
    {G | G ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free G}.sup fun x ↦
      Fintype.card { x_1 // x_1 ∈ x.edgeSet }
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz

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

Tactic:
mem_edgeFinset

Goal state after:
case refine_2
m n s t : ℕ
V : Type u_1
W : Type u_2
α : Type u_3
β : Type u_4
inst✝³ : Fintype V
inst✝² : Fintype W
inst✝¹ : Fintype α
inst✝ : Fintype β
hm : Fintype.card V = m
hn : Fintype.card W = n
hs : Fintype.card α = s
ht : Fintype.card β = t
e₁ : completeBipartiteGraph V W ≃g completeBipartiteGraph (Fin m) (Fin n) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hm) (Fintype.equivFinOfCardEq hn)
K : SimpleGraph (Fin s ⊕ Fin t) := completeBipartiteGraph (Fin s) (Fin t)
e₂ : completeBipartiteGraph α β ≃g completeBipartiteGraph (Fin s) (Fin t) :=
  completeBipartiteGraphCongr (Fintype.equivFinOfCardEq hs) (Fintype.equivFinOfCardEq ht)
G : SimpleGraph (V ⊕ W)
h_le : G ≤ completeBipartiteGraph V W
h_free : (completeBipartiteGraph α β).Free G
h' : SimpleGraph.map (⇑e₁.toEmbedding) G ∈ {G | G ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ K.Free G}
h_le_sup :
  Fintype.card { x // x ∈ (SimpleGraph.map (⇑e₁.toEmbedding) G).edgeSet } ≤
    {G | G ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ K.Free G}.sup fun x ↦ Fintype.card { x_1 // x_1 ∈ x.edgeSet }
⊢ Fintype.card { x // x ∈ (SimpleGraph.map (⇑e₁.toEquiv) G).edgeSet } ≤
    {G | G ≤ completeBipartiteGraph (Fin m) (Fin n) ∧ (completeBipartiteGraph (Fin s) (Fin t)).Free G}.sup fun x ↦
      Fintype.card { x_1 // x_1 ∈ x.edgeSet }
Module: Mathlib.Data.Set.Card.Arithmetic

Goal state before:
pp: case mpr.inr
α : Type u_1
t u : Set α
hdtu : Disjoint t u
hctu : #↑t = #↑u
hnfin : (t ∪ u).Infinite
⊢ Even (t ∪ u).ncard

Tactic:
· simp [hnfin.ncard]

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 ∈ ⋃ i ∈ t, s i), 1 = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).ncard

Tactic:
finsum_mem_biUnion h ht hs,

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) (j : α) (_ : j ∈ s i), 1 = ∑ᶠ (i : ι) (_ : i ∈ t), (s i).ncard
Module: Mathlib.Combinatorics.SimpleGraph.Matching

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
M : G.Subgraph
v w : V
h : M.IsMatching
hvw : M.Adj v w
⊢ h.toEdge ⟨v, ⋯⟩ = ⟨s(v, w), hvw⟩

Tactic:
IsMatching.toEdge,

Goal state after:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
v w : V
h : M.IsMatching
hvw : M.Adj v w
⊢ ⟨s(↑⟨v, ⋯⟩, Exists.choose ⋯), ⋯⟩ = ⟨s(v, w), hvw⟩
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⟩

Goal state after:
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
v : V
hv : v ∈ M.verts
⊢ ∃! w, (Subgraph.map f M).Adj (f v) w