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

Goal state before:
pp: case refine_2
α : 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 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left✝ : x ∉ s
right✝ : insert x s ∈ 𝒜'
hus✝ : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝¹ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this✝ : v \ u = v
this : x ∉ u
hus : u ⊆ s
⊢ insert x (s ∪ v) \ u ∈ 𝒜

Tactic:
← insert_union

Goal state after:
case refine_2
α : 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 𝒜
s : Finset α
hs𝒜' : s ∈ ∂ 𝒜'
hs𝒜 : s ∉ ∂ 𝒜
m : ∀ y ∉ s, insert y s ∉ 𝒜
x : α
left✝ : x ∉ s
right✝ : insert x s ∈ 𝒜'
hus✝ : u ⊆ insert x s
hvs : Disjoint v (insert x s)
this✝¹ : (insert x s ∪ v) \ u ∈ 𝒜
hsv : Disjoint s v
hvu : Disjoint v u
hxv : x ∉ v
this✝ : v \ u = v
this : x ∉ u
hus : u ⊆ s
⊢ (insert x s ∪ v) \ u ∈ 𝒜
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case intro.inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Finite α
val✝ : Fintype α
s : Finset α
hr : #s > 0
h𝒜 : (initSeg s).Nonempty
h₁ : IsInitSeg (initSeg s) #s
⊢ IsInitSeg (initSeg (s.erase (s.min' ⋯))) (#s - 1)

Tactic:
← card_erase_of_mem (min'_mem _ _)

Goal state after:
case intro.inr.inr
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Finite α
val✝ : Fintype α
s : Finset α
hr : #s > 0
h𝒜 : (initSeg s).Nonempty
h₁ : IsInitSeg (initSeg s) #s
⊢ IsInitSeg (initSeg (s.erase (s.min' ⋯))) #(s.erase (s.min' ?m.172))

α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : Finite α
val✝ : Fintype α
s : Finset α
hr : #s > 0
h𝒜 : (initSeg s).Nonempty
h₁ : IsInitSeg (initSeg s) #s
⊢ s.Nonempty
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
⊢ #{∅} ≤ #{∅}.shatterer

pp: case refine_3
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
⊢ ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄,
    #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer →
      #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer → #𝒜 ≤ #𝒜.shatterer

Tactic:
· rfl

Goal state after:
case refine_3
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
⊢ ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄,
    #(nonMemberSubfamily a 𝒜) ≤ #(nonMemberSubfamily a 𝒜).shatterer →
      #(memberSubfamily a 𝒜) ≤ #(memberSubfamily a 𝒜).shatterer → #𝒜 ≤ #𝒜.shatterer
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

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

Tactic:
rw [add_zero, collapse_eq hat, mul_add]

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

Goal state before:
pp: case left.a.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
a b : α
h_eq : {x | r x a} = {x | r x b}
⊢ ⟦a⟧ = ⟦b⟧

Tactic:
apply Quotient.sound

Goal state after:
case left.a.a
α : Type u_1
r : Setoid α
f : α → ↑r.classes := ⋯
f_respects_relation : ∀ (a b : α), r a b → f a = f b
a b : α
h_eq : {x | r x a} = {x | r x b}
⊢ a ≈ b
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
u v w : V
huv : ¬G.Reachable u v
huw : G.Reachable u w
huv' : Gᶜ.Adj u v
⊢ Gᶜ.Reachable u w

Tactic:
have hvw' := G.reachable_or_compl_adj .. |>.resolve_left fun hvw ↦ huv <| huw.trans hvw.symm

Goal state after:
case pos
V : Type u
G : SimpleGraph V
u v w : V
huv : ¬G.Reachable u v
huw : G.Reachable u w
huv' : Gᶜ.Adj u v
hvw' : Gᶜ.Adj v w
⊢ Gᶜ.Reachable u w
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
⊢ Pairwise fun c c' ↦ Disjoint c.supp c'.supp

Tactic:
simp_rw [Set.disjoint_left]
  intro _ _ h a hsx hsy
  rw [ConnectedComponent.mem_supp_iff] at hsx hsy
  rw [hsx] at hsy
  exact h hsy

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

Goal state before:
pp: n r k i : ℕ
𝒜 : Finset (Finset (Fin n))
hir : i ≤ r
hrk : r ≤ k
hkn : k ≤ n
h₁ : Set.Sized r ↑𝒜
h₂ : k.choose r ≤ #𝒜
⊢ k.choose (r - i) ≤ #(∂^[i] 𝒜)

Tactic:
set range'k : Finset (Fin n) :=
    attachFin (range k) fun m ↦ by rw [mem_range]; apply forall_lt_iff_le.2 hkn
  set 𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
  have : (𝒞 : Set (Finset (Fin n))).Sized r := Set.sized_powersetCard _ _
  calc
    k.choose (r - i)
    _ = #(powersetCard (r - i) range'k) := by rw [card_powersetCard, card_attachFin, card_range]
    _ = #(∂^[i] 𝒞) := by
      congr!
      ext B
      rw [mem_powersetCard, mem_shadow_iterate_iff_exists_sdiff]
      constructor
      · rintro ⟨hBk, hB⟩
        have := exists_subsuperset_card_eq hBk (Nat.le_add_left _ i) <| by
          rwa [hB, card_attachFin, card_range, ← Nat.add_sub_assoc hir, Nat.add_sub_cancel_left]
        obtain ⟨C, BsubC, hCrange, hcard⟩ := this
        rw [hB, ← Nat.add_sub_assoc hir, Nat.add_sub_cancel_left] at hcard
        refine ⟨C, mem_powersetCard.2 ⟨hCrange, hcard⟩, BsubC, ?_⟩
        rw [card_sdiff_of_subset BsubC, hcard, hB, Nat.sub_sub_self hir]
      · rintro ⟨A, Ah, hBA, card_sdiff_i⟩
        rw [mem_powersetCard] at Ah
        refine ⟨hBA.trans Ah.1, eq_tsub_of_add_eq ?_⟩
        rw [← Ah.2, ← card_sdiff_i, add_comm, card_sdiff_add_card_eq_card hBA]
    _ ≤ #(∂^[i] 𝒜) := by
      refine iterated_kk h₁ ?_ ⟨‹_›, ?_⟩
      · rwa [card_powersetCard, card_attachFin, card_range]
      simp_rw [𝒞, mem_powersetCard]
      rintro A B hA ⟨HB₁, HB₂⟩
      refine ⟨fun t ht ↦ ?_, ‹_›⟩
      rw [mem_attachFin, mem_range]
      have : toColex (image Fin.val B) < toColex (image Fin.val A) := by
        rwa [toColex_image_lt_toColex_image Fin.val_strictMono]
      apply Colex.forall_lt_mono this.le _ t (mem_image.2 ⟨t, ht, rfl⟩)
      simp_rw [mem_image]
      rintro _ ⟨a, ha, hab⟩
      simpa [range'k, hab] using hA.1 ha

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

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

Tactic:
rw [hc.chromaticNumber_eq_sInf]

Goal state after:
V : Type u
G : SimpleGraph V
n : ℕ
hc : G.Colorable n
⊢ ↑(sInf {n' | G.Colorable n'}) ≤ ↑n
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
α : Type u_2
inst✝ : Fintype α
hG : G.Colorable (card α)
⊢ ↑(card α) ≤ G.chromaticNumber ↔ ∀ (C : G.Coloring α), Surjective ⇑C

Tactic:
card_le_chromaticNumber_iff_forall_surjective

Goal state after:
V : Type u
G : SimpleGraph V
α : Type u_2
inst✝ : Fintype α
hG : G.Colorable (card α)
⊢ (∀ (C : G.Coloring α), Surjective ⇑C) ↔ ∀ (C : G.Coloring α), Surjective ⇑C
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 = ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ image (insert a) u.powerset ∩ 𝒜, f s

Tactic:
rw [← Finset.sum_ite_mem, ← Finset.sum_ite_mem, sum_image, ← sum_add_distrib]

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 =
    ∑ x ∈ u.powerset, ((if x ∈ 𝒜 then f x else 0) + 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
v w : V
G : SimpleGraph V
s t : Set V
α : Type u_2
β : Type u_3
inst✝¹ : Fintype α
inst✝ : Fintype β
left right : Finset V
card_left : #left = Fintype.card α
card_right : #right = Fintype.card β
h : G.IsCompleteBetween ↑left ↑right
this✝ : Nonempty (α ↪ ↥left)
fα : α ↪ ↥left := Classical.arbitrary (α ↪ ↥left)
this : Nonempty (β ↪ ↥right)
fβ : β ↪ ↥right := Classical.arbitrary (β ↪ ↥right)
s₁ s₂ : α ⊕ β
p₁ : β
p₂ : α
⊢ Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ) (Sum.inr p₁) =
      Sum.elim (Subtype.val ∘ ⇑fα) (Subtype.val ∘ ⇑fβ) (Sum.inl p₂) →
    Sum.inr p₁ = Sum.inl p₂

Tactic:
simpa using (h (fα p₂).prop (fβ p₁).prop).ne'

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
inst✝ : DecidableEq V
⊢ p.bypass.toSubgraph ≤ p.toSubgraph

Tactic:
constructor
  · simpa using! p.support_bypass_subset_support
  · simpa [adj_toSubgraph_iff_mem_edges] using! fun _ _ h ↦ p.edges_toPath_subset_edges h

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

Goal state before:
pp: case refine_1.inl
α : 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 α
L : Sublattice α := { carrier := latticeClosure (↑s ∪ ↑t✝), supClosed' := ⋯, infClosed' := ⋯ }
this : Finite ↥L
s' t' : Finset ↥L
hs' : map { toFun := ⇑L.subtype, inj' := ⋯ } s' = s
ht' : map { toFun := ⇑L.subtype, inj' := ⋯ } t' = t✝
β : Type u_1
w✝¹ : DecidableEq β
w✝ : Fintype β
g : LatticeHom (↥L) (Finset β)
hg : Injective ⇑g
t : Finset β
a : ↥L
⊢ extend (⇑g) (f₁ ∘ Subtype.val) 0 (g a) * extend (⇑g) (f₂ ∘ Subtype.val) 0 t ≤
    extend (⇑g) (f₃ ∘ Subtype.val) 0 (g a ∩ t) * extend (⇑g) (f₄ ∘ Subtype.val) 0 (g a ∪ t)

Tactic:
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 _)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : GeneralizedBooleanAlgebra α
s t : Finset α
⊢ #s * #t ≤ #(s \\ t) * #(t \\ s)

Tactic:
have : ∀ s t : Finset α, (s \\ t).map ⟨_, liftLatticeHom_injective⟩ =
      s.map ⟨_, liftLatticeHom_injective⟩ \\ t.map ⟨_, liftLatticeHom_injective⟩ := by
    rintro s t
    simp_rw [map_eq_image]
    exact image_image₂_distrib fun a b ↦ rfl
  simpa [← card_compls (_ ⊻ _), ← map_sup, ← map_inf, ← this] using
    (s.map ⟨_, liftLatticeHom_injective⟩).le_card_infs_mul_card_sups
      (t.map ⟨_, liftLatticeHom_injective⟩)ᶜˢ

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
hG : G.IsAcyclic
v w : V
p : G.Walk v w
⊢ p.IsPath ↔ List.IsChain (fun x1 x2 ↦ x1 ≠ x2) p.edges

Tactic:
refine ⟨fun h ↦ (edges_nodup_of_support_nodup <| p.isPath_def.mp h).isChain, fun h ↦ ?_⟩
  induction p with
  | nil => simp
  | @cons u' v' _ head tail ih =>
    have hcc := List.isChain_cons.mp (edges_cons _ _ ▸ h)
    refine cons_isPath_iff head tail |>.mpr ⟨ih hcc.2, ?_⟩
    rcases tail.length.eq_zero_or_pos with h' | h'
    · simp [nil_iff_support_eq.mp (length_eq_zero_iff.mp h'), head.ne]
    · by_contra hh
      apply hG <| cons head (tail.takeUntil u' hh)
      simp only [isCycle_def, isTrail_def, edges_cons, List.nodup_cons, ne_eq, reduceCtorEq,
        not_false_eq_true, support_cons, List.tail_cons, true_and]
      have : cons head (tail.takeUntil u' hh) |>.support.tail.Nodup :=
        tail.isPath_def.mp (ih hcc.2) |>.sublist <| List.IsInfix.sublist
          ⟨[], (tail.dropUntil u' hh).support.tail, by simp [← support_append]⟩
      refine ⟨⟨?_, edges_nodup_of_support_nodup this⟩, this⟩
      by_contra hhh
      refine hcc.1 s(u', v') ?_ rfl
      rw [← tail.cons_tail_eq (by simp [not_nil_iff_lt_length, h'])]
      have := IsPath.mk' this |>.eq_snd_of_mem_edges (Sym2.eq_swap ▸ hhh)
      simp [this, snd_takeUntil head.ne]

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

Goal state before:
pp: α : Type u_1
V : Type u_2
W : Type u_3
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
f : W → V
hf : Function.Surjective f
h : (A.submatrix f f).IsAdjMatrix
⊢ A.IsAdjMatrix

Tactic:
rw [← A.submatrix_id_id, ← f.comp_surjInv hf]

Goal state after:
α : Type u_1
V : Type u_2
W : Type u_3
A : Matrix V V α
inst✝¹ : Zero α
inst✝ : One α
f : W → V
hf : Function.Surjective f
h : (A.submatrix f f).IsAdjMatrix
⊢ (A.submatrix (f ∘ Function.surjInv hf) (f ∘ Function.surjInv hf)).IsAdjMatrix
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Constructions

Goal state before:
pp: case a
n : ℕ
h : 2 ≤ n
hEven : Even n
hc : (cycleGraph n).Colorable (Fintype.card Bool)
⊢ 2 ≤ (cycleGraph n).chromaticNumber

Tactic:
· have hadj : (cycleGraph n).Adj ⟨0, Nat.zero_lt_of_lt h⟩ ⟨1, h⟩ := by
      simp [cycleGraph_adj', Fin.sub_val_of_le]
    exact two_le_chromaticNumber_of_adj hadj

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 : ℕ
s : V
h : G.IsTuranMaximal r
inst✝ : DecidableEq V
⊢ Fintype.card V - #{t | ¬G.Adj s t} = Fintype.card V - #(h.finpartition.part s)

Tactic:
congr; ext; rw [mem_filter]
      convert! Finpartition.mem_part_ofSetoid_iff_rel.symm
      simp +instances [setoid]

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
l : r < #h.finpartition.parts
z : Finset V
hz : Set.BijOn h.finpartition.part ↑z ↑h.finpartition.parts
ncf : ¬G.CliqueFree #h.finpartition.parts
⊢ False

Tactic:
exact absurd (h.1.mono (Nat.succ_le_of_lt l)) ncf

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

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

Tactic:
by
  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.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
ht : ¬t = 0
⊢ r ≤ Fintype.card ↥K.parts

Tactic:
card_coe,

Goal state after:
α : Type u
G✝ : SimpleGraph α
s : Set α
V : Type u_1
G : SimpleGraph V
r t : ℕ
K : G.CompleteEquipartiteSubgraph r t
ht : ¬t = 0
⊢ r ≤ #K.parts
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
ht : ¬t = 0
this : Nonempty (Fin r ↪ ↥K.parts)
fᵣ : Fin r ↪ ↥K.parts := Classical.arbitrary (Fin r ↪ ↥K.parts)
p : ↥K.parts
⊢ t ≤ Fintype.card ↥↑p

Tactic:
card_coe,

Goal state after:
α : 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)
p : ↥K.parts
⊢ t ≤ #↑p
Module: Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Goal state before:
pp: n r : ℕ
⊢ (∑ x, ∑ i, if ↑x % r ≠ ↑i % r then 1 else 0) =
    (∑ x, ∑ i, if ↑x % r ≠ ↑i % r then 1 else 0) + 2 * (n * (r - 1)) + 2 * r.choose 2

Tactic:
conv_lhs =>
    enter [2, v]
    rw [Fin.sum_univ_eq_sum_range fun w ↦ if v % r ≠ w % r then 1 else 0, sum_range_add]

Goal state after:
n r : ℕ
⊢ ∑ v, ((∑ x ∈ range n, if ↑v % r ≠ x % r then 1 else 0) + ∑ x ∈ range r, if ↑v % r ≠ (n + x) % r then 1 else 0) =
    (∑ x, ∑ i, if ↑x % r ≠ ↑i % r then 1 else 0) + 2 * (n * (r - 1)) + 2 * r.choose 2
Module: Mathlib.Combinatorics.SimpleGraph.Diam

Goal state before:
pp: case inr
α : Type u_1
G : SimpleGraph α
h : ¬G.Preconnected
h✝ : Nonempty α
⊢ G.ediam = ⊤

Tactic:
apply ediam_eq_top_of_not_connected
    rw [connected_iff]
    tauto

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

Goal state before:
pp: case inr.inr.e_a.e_a
n r : ℕ
hr : r > 0
ring₁ : ∀ (n : ℕ), (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) = n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
rd : 2 ∣ r * (r - 1)
ring₂ :
  n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * (n' / r + 1) ^ 2 =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 + r.choose 2 * 2 * (n' / r) + r.choose 2 * (n' / r) ^ 2
⊢ n' % r * (n' / r) * (r - 1) + n' * (r - 1) + r.choose 2 =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 + r.choose 2 * 2 * (n' / r)

Tactic:
← add_rotate _ _ (r.choose 2)

Goal state after:
case inr.inr.e_a.e_a
n r : ℕ
hr : r > 0
ring₁ : ∀ (n : ℕ), (n ^ 2 - (n % r) ^ 2) * (r - 1) / (2 * r) = n % r * (n / r) * (r - 1) + r * (r - 1) * (n / r) ^ 2 / 2
h : r ≤ n
n' : ℕ := n - r
n'r : n = n' + r
rd : 2 ∣ r * (r - 1)
ring₂ :
  n' % r * (n' / r + 1) * (r - 1) + r.choose 2 * (n' / r + 1) ^ 2 =
    n' % r * (n' / r + 1) * (r - 1) + r.choose 2 + r.choose 2 * 2 * (n' / r) + r.choose 2 * (n' / r) ^ 2
⊢ n' % r * (n' / r) * (r - 1) + n' * (r - 1) + r.choose 2 =
    r.choose 2 * 2 * (n' / r) + n' % r * (n' / r + 1) * (r - 1) + r.choose 2
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)
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
⊢ (completeBipartiteGraph (Fin s) (Fin t)).Free G

Tactic:
exact h_free

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

Goal state before:
pp: W : Type u_1
H : SimpleGraph W
ε : ℝ
hε_pos : 0 < ε
hπ : sInf {x | ∃ n ∈ Set.Ici 2, ↑(extremalNumber n H) / ↑(n.choose 2) = x} ≤ H.turanDensity
⊢ ∃ a,
    ∀ (b : ℕ),
      a ≤ b →
        ∀ {G : SimpleGraph (Fin b)} [inst : DecidableRel G.Adj],
          ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(b.choose 2) → H ⊑ G

Tactic:
contrapose! hπ with h

Goal state after:
W : Type u_1
H : SimpleGraph W
ε : ℝ
hε_pos : 0 < ε
h : ∀ (a : ℕ), ∃ b, a ≤ b ∧ ∃ G inst, ↑(#G.edgeFinset) ≥ (H.turanDensity + ε) * ↑(b.choose 2) ∧ IsEmpty (H.Copy G)
⊢ H.turanDensity < sInf {x | ∃ n ∈ Set.Ici 2, ↑(extremalNumber n H) / ↑(n.choose 2) = x}
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
⊢ (completeBipartiteGraph α β).Free G

Tactic:
exact h_free

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
x : ℕ
⊢ (∀ (b : SimpleGraph (V ⊕ W)),
      b ≤ completeBipartiteGraph V W ∧ (completeBipartiteGraph α β).Free b → #b.edgeFinset ≤ x) ↔
    ∀ ⦃G : SimpleGraph (V ⊕ W)⦄ [inst : DecidableRel G.Adj],
      G ≤ completeBipartiteGraph V W → (completeBipartiteGraph α β).Free G → #G.edgeFinset ≤ x

Tactic:
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.Girth

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
G : SimpleGraph α
G' : SimpleGraph β
h : G ⊑ G'
hacyc : G.IsAcyclic
⊢ G'.egirth ≤ G.egirth

Tactic:
simp [hacyc.egirth_eq_top]

Goal state after:
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:
rw [IsMatching.toEdge, Subtype.mk_eq_mk, ← h hvw.fst_mem |>.choose_spec.right w hvw]

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

Goal state before:
pp: α : Type u_1
a b c : α
s : Finset α
G : SimpleGraph α
r : ℕ
inst✝ : DecidableEq α
hs : G.IsNClique r (insert a s)
hc : c ∈ s
ha : a ∉ s
hd : ∀ w ∈ insert a s, w ≠ c → G.Adj w b
⊢ G.IsNClique r (insert a (insert b (s.erase c)))

Tactic:
insert_comm,

Goal state after:
α : Type u_1
a b c : α
s : Finset α
G : SimpleGraph α
r : ℕ
inst✝ : DecidableEq α
hs : G.IsNClique r (insert a s)
hc : c ∈ s
ha : a ∉ s
hd : ∀ w ∈ insert a s, w ≠ c → G.Adj w b
⊢ G.IsNClique r (insert b (insert a (s.erase c)))