mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Ring

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hsum✝ : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
hsum : Summable fun x_1 ↦ x ^ x_1 * ∏ x_2 ∈ Finset.range (x_1 + 1), (1 - x ^ (x_2 + 1))
hsum' : Summable fun i ↦ x ^ (i + 1) * ∏ n ∈ Finset.range i, (1 - x ^ (n + 1))
⊢ Summable fun i ↦ x ^ (i + 1) * ∏ j < i, (1 - x ^ (j + 1))

Tactic:
by simpa [Nat.Iio_eq_range] using hsum'

Goal state after:
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A B S : Finset G
hK : K ≤ 1
hS : S.Nonempty
hA : IsFragment K S A
hB : IsFragment K S B
hAB : (A ∩ B).Nonempty
⊢ IsFragment K S (A ∩ B)

Tactic:
unfold IsFragment at *

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A B S : Finset G
hK : K ≤ 1
hS : S.Nonempty
hA : expansion K S A = connectivity K S
hB : expansion K S B = connectivity K S
hAB : (A ∩ B).Nonempty
⊢ expansion K S (A ∩ B) = connectivity K S
Module: Mathlib.Combinatorics.Enumerative.Schroder

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ 2 * (n + 1).smallSchroder = n.largeSchroder

Tactic:
by
  rw [smallSchroder_succ_eq_largeSchroder_div_two hn,
    Nat.mul_div_cancel_left' (even_largeSchroder hn).two_dvd]

Goal state after:
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: case inl
n : ℕ
hn : ↑n / 3 - 2 ≤ 0
⊢ (↑n / 3 - 2) * (↑((n - 3) / 6) * rexp (-4 * √(Real.log ↑((n - 3) / 6)))) ≤ ↑(ruzsaSzemerediNumberNat n)

Tactic:
exact (mul_nonpos_of_nonpos_of_nonneg hn <| by positivity).trans (Nat.cast_nonneg _)

Goal state after:
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
⊢ G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ) ∩ F₁ᶜ) = G.restrict (F₂ᶜ ∩ F₁ᶜ)

Tactic:
inter_assoc,

Goal state after:
α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
⊢ G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ ∩ F₁ᶜ)) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
⊢ G.restrict (F₂ᶜ ∩ (E(G) ∩ F₁ᶜ ∩ F₁ᶜ)) = G.restrict (F₂ᶜ ∩ F₁ᶜ)

Tactic:
inter_assoc,

Goal state after:
α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
⊢ G.restrict (F₂ᶜ ∩ (E(G) ∩ (F₁ᶜ ∩ F₁ᶜ))) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
⊢ G.restrict (E(G) ∩ F₁ᶜ ∩ F₂ᶜ) = G.restrict (F₂ᶜ ∩ F₁ᶜ)

Tactic:
inter_assoc,

Goal state after:
α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
⊢ G.restrict (E(G) ∩ (F₁ᶜ ∩ F₂ᶜ)) = G.restrict (F₂ᶜ ∩ F₁ᶜ)
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
⊢ (G.deleteEdges F₁).deleteEdges F₂ = G.deleteEdges (F₁ ∪ F₂)

Tactic:
by
  simp only [← restrict_edgeSet_sdiff_eq_deleteEdges, sdiff_eq_compl_inter, restrict_inter_edgeSet,
    edgeSet_restrict, restrict_restrict, compl_union]
  rw [← inter_comm, inter_comm F₁ᶜ, inter_assoc, inter_assoc, inter_self, inter_comm,
    inter_assoc, inter_comm, restrict_inter_edgeSet, inter_comm]

Goal state after:
Module: Mathlib.Combinatorics.Graph.Maps

Goal state before:
pp: α : Type u_1
α' : Type u_2
α'' : Type u_3
β : Type u_4
G✝ H : Graph α β
f✝ g : α → α'
u v : α
e : β
x y : α'
f : α → α'
G : Graph α β
⊢ ∀ ⦃e : β⦄ ⦃x y : α'⦄, Relation.Map (G.IsLink e) f f x y → x ∈ f '' V(G)

Tactic:
rintro e - - ⟨x, y, h, rfl, rfl⟩
    exact Set.mem_image_of_mem _ h.left_mem

Goal state after:
Module: Mathlib.Combinatorics.Graph.Simple

Goal state before:
pp: α : Type u_1
β : Type u_2
G H : Graph α β
h : G ≤s H
u v : ↑V(G)
hadj : G.toSimpleGraph.Adj u v
⊢ (⋯ ▸ H.toSimpleGraph).Adj u v

Tactic:
match G, H with
  | ⟨GV, GL, GE, _, _, _, _⟩, ⟨HV, HL, HE, _, _, _, _⟩ =>
    obtain ⟨hne, hadj⟩ := toSimpleGraph_adj .. ▸ hadj
    obtain ⟨hle, h⟩ := h
    simp only at h
    subst GV
    simp [toSimpleGraph_adj, hne, hadj.mono hle]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
X D : Set α
hD : D ⊆ M.E
h : M ＼ D ≤r M
hX : Disjoint X (M ＼ D).E
⊢ M ＼ D = M ＼ D ＼ X

Tactic:
eq_comm,

Goal state after:
α : Type u_1
M : Matroid α
X D : Set α
hD : D ⊆ M.E
h : M ＼ D ≤r M
hX : Disjoint X (M ＼ D).E
⊢ M ＼ D ＼ X = M ＼ D
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M ＼ M.loops = M.removeLoops

Tactic:
removeLoops,

Goal state after:
α : Type u_1
M : Matroid α
⊢ M ＼ M.loops = M ↾ {e | M.IsNonloop e}
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
d : ℕ
hd : j = i.succ + d
this : (Stream'.drop i a).get (1 + d) ∈ FP (Stream'.drop 1 (Stream'.drop i a))
⊢ FP (Stream'.drop i a).tail (a.get j)

Tactic:
Stream'.get_drop

Goal state after:
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
d : ℕ
hd : j = i.succ + d
this : a.get (i + (1 + d)) ∈ FP (Stream'.drop 1 (Stream'.drop i a))
⊢ FP (Stream'.drop i a).tail (a.get j)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis' I X
⊢ M ／ I ＼ ((X ∩ M.E) \ I) = M ／ I ＼ (X \ I)

Tactic:
eq_comm,

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis' I X
⊢ M ／ I ＼ (X \ I) = M ／ I ＼ ((X ∩ M.E) \ I)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: case inr
α : Type u_1
D C : Set α
M : Matroid α
hCD : Disjoint C D
aux : ∀ {C : Set α}, Disjoint C D → C ⊆ M.E → M ／ C ＼ D = M ＼ D ／ C
hCE : ¬C ⊆ M.E
⊢ C ∩ M.E ∩ (M ＼ D).E = C ∩ (M ＼ D).E

Tactic:
inter_assoc,

Goal state after:
case inr
α : Type u_1
D C : Set α
M : Matroid α
hCD : Disjoint C D
aux : ∀ {C : Set α}, Disjoint C D → C ⊆ M.E → M ／ C ＼ D = M ＼ D ／ C
hCE : ¬C ⊆ M.E
⊢ C ∩ (M.E ∩ (M ＼ D).E) = C ∩ (M ＼ D).E
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
D C : Set α
⊢ C ∩ (M.E \ D) = C \ D ∩ (M.E \ D)

Tactic:
← sdiff_inter_distrib_right,

Goal state after:
α : Type u_1
M : Matroid α
D C : Set α
⊢ C ∩ (M.E \ D) = (C ∩ M.E) \ D
Module: Mathlib.Combinatorics.Optimization.ValuedCSP

Goal state before:
pp: D : Type u_1
C : Type u_3
inst✝² : AddCommMonoid C
inst✝¹ : PartialOrder C
inst✝ : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
mcf : HasMaxCutProperty f
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
⊢ ¬AdmitsFractional f ω

Tactic:
intro contr
  obtain ⟨a, b, hab, mcfab⟩ := mcf
  specialize contr ![![a, b], ![b, a]]
  rw [Fin.sum_univ_two', ← mcfab.left, ← two_nsmul] at contr
  have sharp :
    2 • ((ω.tt ![![a, b], ![b, a]]).map (fun _ => f ![a, b])).sum <
    2 • ((ω.tt ![![a, b], ![b, a]]).map f).sum := by
    have half_sharp :
      ((ω.tt ![![a, b], ![b, a]]).map (fun _ => f ![a, b])).sum <
      ((ω.tt ![![a, b], ![b, a]]).map f).sum := by
      apply Multiset.sum_lt_sum
      · intro r rin
        exact le_of_lt (mcfab.rows_lt_aux hab symmega rin)
      · obtain ⟨g, _⟩ := valid.contains
        have : (fun i => g ((Function.swap ![![a, b], ![b, a]]) i)) ∈ ω.tt ![![a, b], ![b, a]] := by
          simp only [FractionalOperation.tt, Multiset.mem_map]
          use g
        exact ⟨_, this, mcfab.rows_lt_aux hab symmega this⟩
    rw [two_nsmul, two_nsmul]
    exact add_lt_add half_sharp half_sharp
  have impos : 2 • (ω.map (fun _ => f ![a, b])).sum < ω.size • 2 • f ![a, b] := by
    convert! lt_of_lt_of_le sharp contr
    simp [FractionalOperation.tt, Multiset.map_map]
  have rhs_swap : ω.size • 2 • f ![a, b] = 2 • ω.size • f ![a, b] := nsmul_left_comm ..
  have distrib : (ω.map (fun _ => f ![a, b])).sum = ω.size • f ![a, b] := by simp
  rw [rhs_swap, distrib] at impos
  exact ne_of_lt impos rfl

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: case cons
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Surjective (φ.star u)
u : U
v b✝ c✝ : V
p' : Path (φ.obj u) b✝
ev : b✝ ⟶ c✝
ih : ∃ a, (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a = ⟨b✝, p'⟩
⊢ ∃ a, (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a = ⟨c✝, p'.cons ev⟩

Tactic:
obtain ⟨⟨u', q'⟩, h⟩ := ih
    simp only at h
    obtain ⟨rfl, rfl⟩ := h
    obtain ⟨⟨u'', eu⟩, k⟩ := hφ u' ⟨_, ev⟩
    simp only [star_apply, Sigma.mk.inj_iff] at k
    -- Porting note: was `obtain ⟨rfl, rfl⟩ := k`
    obtain ⟨rfl, k⟩ := k
    simp only [heq_eq_eq] at k
    subst k
    use ⟨_, q'.cons eu⟩
    simp only [Prefunctor.mapPath_cons]

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case right
A : Finset ℕ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
n : ℕ := ⌊↑(#A) / ε⌋₊ + 1
hn : 0 < n
⊢ ↑(#({a ∈ Ioc 0 n | a ∈ ↑A})) / ε < ↑n

Tactic:
Nat.cast_add_one

Goal state after:
case right
A : Finset ℕ
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
n : ℕ := ⌊↑(#A) / ε⌋₊ + 1
hn : 0 < n
⊢ ↑(#({a ∈ Ioc 0 n | a ∈ ↑A})) / ε < ↑⌊↑(#A) / ε⌋₊ + 1
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nonempty α
this :
  ∀ {x : ℕ},
    ∀ s ∈ powersetCard x univ,
      ↑(card α) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) = ↑(card α) / ((↑(card α) - ↑x) * ↑((card α).choose x))
⊢ ∑ x ∈ range (#univ + 1), (#univ).choose x • (↑(card α) / ((↑(card α) - ↑x) * ↑((card α).choose x))) =
    ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1

Tactic:
card_univ,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nonempty α
this :
  ∀ {x : ℕ},
    ∀ s ∈ powersetCard x univ,
      ↑(card α) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) = ↑(card α) / ((↑(card α) - ↑x) * ↑((card α).choose x))
⊢ ∑ x ∈ range (card α + 1), (card α).choose x • (↑(card α) / ((↑(card α) - ↑x) * ↑((card α).choose x))) =
    ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝³ : DecidableEq α
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
⊢ ∀ (s t u : Finset α), s ○ t ○ u = s ○ (t ○ u)

Tactic:
refine (associative_of_commutative_of_le inferInstance ?_).assoc
  simp only [disjSups_subset_iff, mem_disjSups]
  rintro s t u _ ⟨a, ha, b, hb, hab, rfl⟩ c hc habc
  rw [disjoint_sup_left] at habc
  exact ⟨a, ha, _, ⟨b, hb, c, hc, habc.2, rfl⟩, hab.sup_right habc.1, (sup_assoc ..).symm⟩

Goal state after:
Module: Mathlib.Order.Irreducible

Goal state before:
pp: α : Type u_2
inst✝ : SemilatticeSup α
a : α
⊢ ¬SupPrime a ↔ IsMin a ∨ ∃ b c, a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c

Tactic:
rw [SupPrime, not_and_or]

Goal state after:
α : Type u_2
inst✝ : SemilatticeSup α
a : α
⊢ (¬¬IsMin a ∨ ¬∀ ⦃b c : α⦄, a ≤ b ⊔ c → a ≤ b ∨ a ≤ c) ↔ IsMin a ∨ ∃ b c, a ≤ b ⊔ c ∧ ¬a ≤ b ∧ ¬a ≤ c
Module: Mathlib.Order.Birkhoff

Goal state before:
pp: case refine_2
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : Fintype α
inst✝¹ : DecidablePred SupIrred
inst✝ : OrderBot α
s : LowerSet { a // SupIrred a }
a : { a // SupIrred a }
ha : a ∈ ↑s
⊢ a ∈ ↑{ carrier := {b | ↑b ≤ (↑s).toFinset.sup Subtype.val}, lower' := ⋯ }

Tactic:
· exact le_sup (Set.mem_toFinset.2 ha)

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

Goal state before:
pp: case inr
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
r : ℕ
huv : #u = #v
h𝒜 : Set.Sized r ↑𝒜
t : Finset α
ht : t ∈ 𝒜
huvt : compress u v t ∉ 𝒜
⊢ #(compress u v t) = r

Tactic:
rw [card_compress huv, h𝒜 ht]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := ⋯
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
hxu : x ∈ u
y : α
hyv : y ∈ v
hxy : IsCompressed (u.erase x) (v.erase y) 𝒜
⊢ insert y s ∈ 𝒜

Tactic:
have : ((insert x s ∪ v) \ u ∪ erase u x) \ erase v y ∈ 𝒜 := by
      refine
        sup_sdiff_mem_of_mem_compression (by rwa [hxy.eq]) ?_
          (disjoint_of_subset_left (erase_subset _ _) disjoint_sdiff)
      rw [union_sdiff_distrib, ‹v \ u = v›]
      exact (erase_subset _ _).trans subset_union_right

Goal state after:
α : 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
hxu : x ∈ u
y : α
hyv : y ∈ v
hxy : IsCompressed (u.erase x) (v.erase y) 𝒜
this : ((insert x s ∪ v) \ u ∪ u.erase x) \ v.erase y ∈ 𝒜
⊢ insert y s ∈ 𝒜
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
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
⊢ u ⊆ s ∧
    Disjoint v s ∧ (∃ a ∉ (s ∪ v) \ u, insert a ((s ∪ v) \ u) ∈ 𝒜) ∧ ¬∃ a ∉ (s ∪ v) \ u, insert a ((s ∪ v) \ u) ∈ 𝒜'

Tactic:
refine ⟨hus, hsv.symm, ⟨x, ?_, ?_⟩, ?_⟩

Goal state after:
case refine_1
α : 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
⊢ x ∉ (s ∪ v) \ u

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) ∈ 𝒜

case refine_3
α : 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
⊢ ¬∃ a ∉ (s ∪ v) \ u, insert a ((s ∪ v) \ u) ∈ 𝒜'
Module: Mathlib.Combinatorics.SetFamily.Shatter

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
x✝ : 𝒜.Nonempty
t : Finset α
ht : t ⊆ ∅
s : Finset α
hs : s ∈ 𝒜
⊢ ∅ = t

Tactic:
eq_comm,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
x✝ : 𝒜.Nonempty
t : Finset α
ht : t ⊆ ∅
s : Finset α
hs : s ∈ 𝒜
⊢ t = ∅
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case inr.refine_1
α : Type u_1
inst✝ : LinearOrder α
U V : Finset α
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : #U = #V
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 < #U
⊢ #U - 1 = #V - 1

Tactic:
same_size

Goal state after:
case inr.refine_1
α : Type u_1
inst✝ : LinearOrder α
U V : Finset α
𝒜 : Finset (Finset α)
h₂ : ∀ ⦃U₁ V₁ : Finset α⦄, UsefulCompression U₁ V₁ → #U₁ < #U → IsCompressed U₁ V₁ 𝒜
UVd : Disjoint U V
same_size : #U = #V
hU : U.Nonempty
hV : V.Nonempty
max_lt : U.max' hU < V.max' hV
x : α
Hx : x ∈ U
hU' : succ 0 < #U
⊢ #V - 1 = #V - 1
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case mp
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 ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : #B = r - i
C : Finset (Fin n)
BsubC : B ⊆ C
hCrange : C ⊆ range'k
hcard : #C = r
⊢ #C - #B = i

Tactic:
hcard,

Goal state after:
case mp
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 ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
B : Finset (Fin n)
hBk : B ⊆ range'k
hB : #B = r - i
C : Finset (Fin n)
BsubC : B ⊆ C
hCrange : C ⊆ range'k
hcard : #C = r
⊢ r - #B = i
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

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

Tactic:
by
  cases p with
  | nil => exact Walk.nil
  | @cons v w u h p =>
    have hw : w ∈ C := C.mem_supp_of_adj_mem_supp hu h
    have h' : C.toSimpleGraph.Adj ⟨u, hu⟩ ⟨w, hw⟩ := h
    exact Walk.cons h' (C.walk_toSimpleGraph hw hv p)

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

Goal state before:
pp: case e'_3
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
b : r = 0
⊢ ∀ (x : Finset (Fin n)), x ∉ 𝒜

Tactic:
refine fun A HA ↦ h𝒜 HA HA ?_

Goal state after:
case e'_3
n : ℕ
𝒜 : Finset (Finset (Fin n))
r : ℕ
h𝒜 : (↑𝒜).Intersecting
h₂ : Set.Sized r ↑𝒜
h₃ : r ≤ n / 2
b : r = 0
A : Finset (Fin n)
HA : A ∈ 𝒜
⊢ Disjoint A A
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
m : ℕ
hc : G.Colorable m
⊢ {n' | G.Colorable n'}.Nonempty

Tactic:
exact colorable_set_nonempty_of_colorable hc

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

Goal state before:
pp: α : 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 ∈ 𝒜, f s

Tactic:
calc
    _ = ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ u.powerset.image (insert a) ∩ 𝒜, f s := ?_
    _ = ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ ((insert a u).powerset \ u.powerset) ∩ 𝒜, f s := ?_
    _ = ∑ s ∈ 𝒜, f s := ?_

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 = ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ image (insert a) u.powerset ∩ 𝒜, f s

case calc_2
α : 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 ∩ 𝒜, f s + ∑ s ∈ image (insert a) u.powerset ∩ 𝒜, f s =
    ∑ s ∈ u.powerset ∩ 𝒜, f s + ∑ s ∈ (insert a u).powerset \ u.powerset ∩ 𝒜, f s

case calc_3
α : 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 ∩ 𝒜, f s + ∑ s ∈ (insert a u).powerset \ u.powerset ∩ 𝒜, f s = ∑ s ∈ 𝒜, f s
Module: Mathlib.Combinatorics.SimpleGraph.Metric

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.edist u v = 1 ↔ G.Adj u v

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · obtain ⟨w, hw⟩ := exists_walk_of_edist_ne_top <| by rw [h]; simp
    exact w.adj_of_length_eq_one <| Nat.cast_eq_one.mp <| h ▸ hw
  · exact le_antisymm (edist_le h.toWalk) (Order.one_le_iff_pos.mpr <| edist_pos_of_ne h.ne)

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

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i ≠ 0 ∧ i ≠ p.length
⊢ (p.toSubgraph.neighborSet (p.getVert i)).ncard = 2

Tactic:
hpc.neighborSet_toSubgraph_internal he.1 (by lia)

Goal state after:
case neg
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u u
hpc : p.IsCycle
i : ℕ
hi : p.getVert i = v ∧ i ≤ p.length
he : i ≠ 0 ∧ i ≠ p.length
⊢ {p.getVert (i - 1), p.getVert (i + 1)}.ncard = 2
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
H K : G.Subgraph
Hconn : H.Preconnected
Kconn : K.Preconnected
u v : V
uH : u ∈ H.verts
vK : v ∈ K.verts
huv : G.Adj u v
⊢ u ∈ (⊤.induce {u, v} ⊓ H).verts

Tactic:
by simp [uH]

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

Goal state before:
pp: case refine_2.patches
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
⊢ ∀ {v : V},
    v ∈ ↑(t.biUnion fun v ↦ (Nonempty.some ⋯).support.toFinset) →
      ∃ s' ⊆ ↑(t.biUnion fun v ↦ (Nonempty.some ⋯).support.toFinset),
        ∃ (hu' : u ∈ s') (hv' : v ∈ s'), (induce s' G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩

Tactic:
intro v hv

Goal state after:
case refine_2.patches
V : Type u
G : SimpleGraph V
Gpc : G.Preconnected
t : Finset V
u : V
ut : u ∈ t
v : V
hv : v ∈ ↑(t.biUnion fun v ↦ (Nonempty.some ⋯).support.toFinset)
⊢ ∃ s' ⊆ ↑(t.biUnion fun v ↦ (Nonempty.some ⋯).support.toFinset),
    ∃ (hu' : u ∈ s') (hv' : v ∈ s'), (induce s' G).Reachable ⟨u, hu'⟩ ⟨v, hv'⟩
Module: Mathlib.Combinatorics.SimpleGraph.Acyclic

Goal state before:
pp: V : Type u_1
G H : SimpleGraph V
h : G.Connected
hH_le : H ≤ G
hH_isAcyclic : H.IsAcyclic
⊢ ∃ F, H ≤ F ∧ F ≤ G ∧ F.IsTree

Tactic:
by
  obtain ⟨F, hF⟩ := G.exists_isAcyclic_reachable_eq_le_of_le_of_isAcyclic hH_le hH_isAcyclic
  grind [IsTree, Connected, preconnected_iff_reachable_eq_top]

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

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
this : Fintype V
x✝ : G.Connected ∧ Nat.card ↑G.edgeSet + 1 = Nat.card V
h₁ : G.Connected
h₂ : Nat.card ↑G.edgeSet + 1 = Nat.card V
x y : V
h : G.Adj x y
hbr : ¬G.IsBridge s(x, y)
⊢ Nat.card ↑(G.deleteEdges {s(x, y)}).edgeSet + 1 < Nat.card V

Tactic:
rw [Nat.card_eq_fintype_card, ← edgeFinset_card, ← h₂, Nat.card_eq_fintype_card,
    ← edgeFinset_card, add_lt_add_iff_right]

Goal state after:
V : Type u_1
G : SimpleGraph V
inst✝ : Finite V
this : Fintype V
x✝ : G.Connected ∧ Nat.card ↑G.edgeSet + 1 = Nat.card V
h₁ : G.Connected
h₂ : Nat.card ↑G.edgeSet + 1 = Nat.card V
x y : V
h : G.Adj x y
hbr : ¬G.IsBridge s(x, y)
⊢ (G.deleteEdges {s(x, y)}).edgeFinset.card < G.edgeFinset.card
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case refine_1.h
r t : ℕ
x✝ : (completeEquipartiteGraph r t).edgeSet.Nonempty
v₁ v₂ : Fin r × Fin t
he : (completeEquipartiteGraph r t).Adj v₁ v₂
⊢ Nontrivial (Fin r) ∧ Nonempty (Fin t)

Tactic:
completeEquipartiteGraph_adj

Goal state after:
case refine_1.h
r t : ℕ
x✝ : (completeEquipartiteGraph r t).edgeSet.Nonempty
v₁ v₂ : Fin r × Fin t
he : v₁.1 ≠ v₂.1
⊢ Nontrivial (Fin r) ∧ Nonempty (Fin t)
Module: Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite

Goal state before:
pp: case h
r t : ℕ
x✝ : Nontrivial (Fin r) ∧ Nonempty (Fin t)
i₁ i₂ : Fin r
hv : i₁ ≠ i₂
x : Fin t
⊢ (completeEquipartiteGraph r t).Adj (i₁, x) (i₂, x)

Tactic:
completeEquipartiteGraph_adj

Goal state after:
case h
r t : ℕ
x✝ : Nontrivial (Fin r) ∧ Nonempty (Fin t)
i₁ i₂ : Fin r
hv : i₁ ≠ i₂
x : Fin t
⊢ (i₁, x).1 ≠ (i₂, x).1