mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Graph.Delete

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

Tactic:
inter_comm

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

Goal state before:
pp: α α' : Type u
e : α ≃ α'
κ : Type (max v u)
x✝¹ : Finite κ
ι : Type
x✝ : Fintype ι
h : ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
C : (ι → α') → κ
l : Line α ι
c : κ
lc : ∀ (x : α), (fun v ↦ C (⇑e ∘ v)) (↑l x) = c
x : α
⊢ C (↑(map (⇑e) l) (e x)) = c

Tactic:
rw [← lc x, Line.map_apply]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I D X : Set α
h : M.IsBasis I X
hX : Disjoint X D
⊢ (M ＼ D).IsBasis I X

Tactic:
rw [delete_isBasis_iff]

Goal state after:
α : Type u_1
M : Matroid α
I D X : Set α
h : M.IsBasis I X
hX : Disjoint X D
⊢ M.IsBasis I X ∧ Disjoint X D
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case H.inr
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih :
  ∀ s_1 ∈ s, ∀ (hs : (s.erase s_1).Nonempty), ∏ i ∈ s.erase s_1, a.get i ∈ FP (Stream'.drop ((s.erase s_1).min' hs) a)
hs : s.Nonempty
h : (s.erase (s.min' hs)).Nonempty
this : s.min' hs + 1 ≤ (s.erase (s.min' hs)).min' h
d : ℕ
hd : (s.erase (s.min' hs)).min' h = s.min' hs + 1 + d
⊢ FP (Stream'.drop ((s.erase (s.min' hs)).min' h) a) ⊆ FP (Stream'.drop (1 + s.min' hs) a)

Tactic:
rw [hd, ← Stream'.drop_drop, add_comm]

Goal state after:
case H.inr
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih :
  ∀ s_1 ∈ s, ∀ (hs : (s.erase s_1).Nonempty), ∏ i ∈ s.erase s_1, a.get i ∈ FP (Stream'.drop ((s.erase s_1).min' hs) a)
hs : s.Nonempty
h : (s.erase (s.min' hs)).Nonempty
this : s.min' hs + 1 ≤ (s.erase (s.min' hs)).min' h
d : ℕ
hd : (s.erase (s.min' hs)).min' h = s.min' hs + 1 + d
⊢ FP (Stream'.drop d (Stream'.drop (1 + s.min' hs) a)) ⊆ FP (Stream'.drop (1 + s.min' hs) a)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
X : Set α
⊢ (M ／ X)✶ = M✶ ＼ X

Tactic:
← dual_delete_dual,

Goal state after:
α : Type u_1
M : Matroid α
X : Set α
⊢ (M✶ ＼ X)✶✶ = M✶ ＼ X
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
⊢ M ／ C = M ↔ Disjoint C M.E

Tactic:
← dual_delete_dual,

Goal state after:
α : Type u_1
M : Matroid α
C : Set α
⊢ (M✶ ＼ C)✶ = M ↔ Disjoint C M.E
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
he : e ∉ M.E
⊢ M ／ {e} = M

Tactic:
← dual_delete_dual,

Goal state after:
α : Type u_1
M : Matroid α
e : α
he : e ∉ M.E
⊢ (M✶ ＼ {e})✶ = M
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M ／ ∅ = M

Tactic:
← dual_delete_dual,

Goal state after:
α : Type u_1
M : Matroid α
⊢ (M✶ ＼ ∅)✶ = M
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
C₁ C₂ : Set α
⊢ M ／ C₁ = M ／ C₂ ↔ C₁ ∩ M.E = C₂ ∩ M.E

Tactic:
← dual_delete_dual,

Goal state after:
α : Type u_1
M : Matroid α
C₁ C₂ : Set α
⊢ (M✶ ＼ C₁)✶ = M ／ C₂ ↔ C₁ ∩ M.E = C₂ ∩ M.E
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
C₁ C₂ : Set α
⊢ (M✶ ＼ C₁)✶ = M ／ C₂ ↔ C₁ ∩ M.E = C₂ ∩ M.E

Tactic:
← dual_delete_dual,

Goal state after:
α : Type u_1
M : Matroid α
C₁ C₂ : Set α
⊢ (M✶ ＼ C₁)✶ = (M✶ ＼ C₂)✶ ↔ C₁ ∩ M.E = C₂ ∩ M.E
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

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

Tactic:
← dual_delete_dual,

Goal state after:
α : Type u_1
M : Matroid α
C : Set α
⊢ (M✶ ＼ (C ∩ M.E))✶ = M ／ C
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
⊢ (M ／ I).IsBase B ↔ M.IsBase (B ∪ I) ∧ Disjoint B I

Tactic:
← dual_delete_dual,

Goal state after:
α : Type u_1
M : Matroid α
I B : Set α
hI : M.Indep I
⊢ (M✶ ＼ I)✶.IsBase B ↔ M.IsBase (B ∪ I) ∧ Disjoint B I
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

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

Tactic:
nth_rw 1 [← sdiff_union_of_subset hI.subset, ← dual_inj, dual_contract_delete, dual_contract,
    union_comm, ← delete_delete, ext_iff_indep]
  refine ⟨rfl, fun J hJ ↦ ?_⟩
  have hss : X \ I ⊆ (M✶ ＼ I).coloops := fun e he ↦ by
    rw [← dual_contract, dual_coloops, ← IsLoop, ← singleton_dep, hI.indep.contract_dep_iff,
      singleton_union, and_iff_right (by simpa using he.2), hI.indep.insert_dep_iff,
      hI.closure_eq_closure]
    exact sdiff_subset_sdiff_left (M.subset_closure X) he
  rw [((coloops_indep _).subset hss).contract_indep_iff, delete_indep_iff,
    union_indep_iff_indep_of_subset_coloops hss, and_comm]

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case refine_3.e_a
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
x : M
xs : x ∈ S
i : ι
hi : i ∈ {i | l.idxFun i = none}ᶜ
⊢ (Option.map (fun m ↦ ↑m) (l.idxFun i)).getD 0 = ↑(↑l ⟨x, xs⟩ i)

Tactic:
Finset.compl_filter,

Goal state after:
case refine_3.e_a
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
x : M
xs : x ∈ S
i : ι
hi : i ∈ {x | ¬l.idxFun x = none}
⊢ (Option.map (fun m ↦ ↑m) (l.idxFun i)).getD 0 = ↑(↑l ⟨x, xs⟩ i)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
C I : Set α
hI : M.IsBasis' I C
⊢ (M ／ C).IsLoop e ↔ e ∈ M.closure C ∧ e ∉ C

Tactic:
rw [hI.contract_eq_contract_delete, delete_isLoop_iff, ← singleton_dep,
    hI.indep.contract_dep_iff, singleton_union, hI.indep.insert_dep_iff, hI.closure_eq_closure]

Goal state after:
α : Type u_1
M : Matroid α
e : α
C I : Set α
hI : M.IsBasis' I C
⊢ (Disjoint {e} I ∧ e ∈ M.closure C \ I) ∧ e ∉ C \ I ↔ e ∈ M.closure C ∧ e ∉ C
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
C : Set α
⊢ (M ／ C).coloops = M.coloops \ C

Tactic:
← dual_delete_dual,

Goal state after:
α : Type u_1
M : Matroid α
C : Set α
⊢ (M✶ ＼ C)✶.coloops = M.coloops \ C
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
C : Set α
⊢ e ∈ (M.E \ C) \ (M ／ C).loops ↔ e ∈ M.E \ M.closure C

Tactic:
contract_loops_eq

Goal state after:
α : Type u_1
M : Matroid α
e : α
C : Set α
⊢ e ∈ (M.E \ C) \ (M.closure C \ C) ↔ e ∈ M.E \ M.closure C
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: case refine_1.inl
ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
hI : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)
x✝ :
  I ⊆ X ∧
    (∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t) ∧
      X ⊆ univ.sigma fun i ↦ (M i).E
hIX : I ⊆ X
h' : X ⊆ univ.sigma fun i ↦ (M i).E
i : ι
I₀ : Set (α i)
hI₀ : (M i).Indep I₀
hI₀X : I₀ ⊆ Sigma.mk i ⁻¹' X
hII₀ : Sigma.mk i ⁻¹' I ⊆ I₀
h : (∀ (i_1 : ι), (M i_1).Indep (Sigma.mk i_1 ⁻¹' I ∪ Sigma.mk i_1 ⁻¹' Sigma.mk i '' I₀)) → I = I ∪ Sigma.mk i '' I₀
⊢ (M i).Indep (Sigma.mk i ⁻¹' I ∪ Sigma.mk i ⁻¹' Sigma.mk i '' I₀)

Tactic:
rwa [sigma_mk_preimage_image_eq_self, union_eq_self_of_subset_left hII₀]

Goal state after:
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) f = 0
this✝ : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf : f = (linearCombination (MvPolynomial σ R) fun i ↦ Alon.P (S i) i) h + r
hh : ∀ (i : σ), degLex.toSyn (degLex.degree (Alon.P (S i) i * h i)) ≤ degLex.toSyn (degLex.degree f)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬degLex.degree (Alon.P (S i) i) ≤ c
this : r = 0
⊢ (∀ (i : σ), ((∏ s ∈ S i, (X i - C s)) * h i).totalDegree ≤ f.totalDegree) ∧
    f = (linearCombination (MvPolynomial σ R) fun i ↦ ∏ r ∈ S i, (X i - C r)) h

Tactic:
rw [this, add_zero] at hf

Goal state after:
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) f = 0
this✝ : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf : f = (linearCombination (MvPolynomial σ R) fun i ↦ Alon.P (S i) i) h
hh : ∀ (i : σ), degLex.toSyn (degLex.degree (Alon.P (S i) i * h i)) ≤ degLex.toSyn (degLex.degree f)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬degLex.degree (Alon.P (S i) i) ≤ c
this : r = 0
⊢ (∀ (i : σ), ((∏ s ∈ S i, (X i - C s)) * h i).totalDegree ≤ f.totalDegree) ∧
    f = (linearCombination (MvPolynomial σ R) fun i ↦ ∏ r ∈ S i, (X i - C r)) h
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
f : MvPolynomial σ R
t : σ →₀ ℕ
ht : coeff t f ≠ 0
ht' : f.totalDegree = Finsupp.degree t
S : σ → Finset R
htS : ∀ (i : σ), t i < #(S i)
⊢ ∃ s, (∀ (i : σ), s i ∈ S i) ∧ (eval s) f ≠ 0

Tactic:
let _ : LinearOrder σ := WellOrderingRel.isWellOrder.linearOrder
  by_contra! Heval
  apply ht
  obtain ⟨h, hh, hf⟩ := combinatorial_nullstellensatz_exists_linearCombination S
    (fun i ↦ by rw [← Finset.card_pos]; exact Nat.zero_lt_of_lt (htS i)) f Heval
  rw [hf]
  rw [linearCombination_apply, Finsupp.sum, coeff_sum]
  apply Finset.sum_eq_zero
  intro i _
  set g := h i * Alon.P (S i) i with hg
  by_cases hi : h i = 0
  · simp [hi]
  have : g.totalDegree ≤ f.totalDegree := by
    rw [hg, mul_comm]
    exact hh i
  -- one could simplify this by proving `totalDegree_mul_eq` (at least in a domain)
  rw [hg, ← degree_degLexDegree,
    degree_mul_of_isRegular_right hi (by simp only [(Alon.monic_P ..).leadingCoeff_eq_one,
      isRegular_one]),
    Alon.degree_P, map_add, degree_degLexDegree, degree_single, ht'] at this
  rw [smul_eq_mul, coeff_mul, Finset.sum_eq_zero]
  rintro ⟨p, q⟩ hpq
  simp only [Finset.mem_antidiagonal] at hpq
  simp only [mul_eq_zero, Classical.or_iff_not_imp_right]
  rw [← ne_eq, ← mem_support_iff]
  intro hq
  obtain ⟨e, hq', hq⟩ := Alon.of_mem_P_support _ _ _ hq
  apply coeff_eq_zero_of_totalDegree_lt
  rw [← Finsupp.degree_apply]
  apply lt_of_add_lt_add_right (lt_of_le_of_lt this _)
  rw [← hpq, map_add, add_lt_add_iff_left, hq, degree_single]
  apply lt_of_le_of_lt _ (htS i)
  simp [← hpq, hq]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ 𝓓 a (𝓓 a 𝒜) = 𝓓 a 𝒜

Tactic:
ext s
  refine mem_compression.trans ⟨?_, fun h => Or.inl ⟨h, erase_mem_compression_of_mem_compression h⟩⟩
  rintro (h | h)
  · exact h.1
  · cases h.1 (mem_compression_of_insert_mem_compression h.2)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nonempty α
⊢ ∑ s ∈ univ.powerset, ↑(card α) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) =
    ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1

Tactic:
powerset_card_disjiUnion,

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nonempty α
⊢ ∑ s ∈ (range (#univ + 1)).disjiUnion (fun i ↦ powersetCard i univ) ⋯,
      ↑(card α) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) =
    ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 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 (card α + 1), (card α).choose x • (↑(card α) / ((↑(card α) - ↑x) * ↑((card α).choose x))) =
    ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1

Tactic:
nsmul_eq_mul,

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.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeSup α
s : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : OrderTop α
⊢ a ≤ s.truncatedSup a

Tactic:
by
  rw [truncatedSup]
  split_ifs with h
  · obtain ⟨ℬ, hb, h⟩ := h
    exact h.trans <| le_sup' id <| mem_filter.2 ⟨hb, h⟩
  · exact le_top

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A B : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
inst✝ : DecidablePred fun x ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun x ↦
    match x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
a b : ℕ
left✝ : Sum.inl a ≠ Sum.inr b
hxy : f (Sum.inl a) = f (Sum.inr b)
ha : (0 < a ∧ a ≤ n) ∧ a ∈ A
hb : (0 < b ∧ b ≤ n) ∧ b ∈ B
⊢ a ∈ A

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A B : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
inst✝ : DecidablePred fun x ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun x ↦
    match x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
a b : ℕ
left✝ : Sum.inl a ≠ Sum.inr b
hxy : f (Sum.inl a) = f (Sum.inr b)
ha : (0 < a ∧ a ≤ n) ∧ a ∈ A
hb : (0 < b ∧ b ≤ n) ∧ b ∈ B
⊢ b ∈ B

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A B : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
inst✝ : DecidablePred fun x ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun x ↦
    match x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
b a : ℕ
left✝ : Sum.inr b ≠ Sum.inl a
hxy : f (Sum.inr b) = f (Sum.inl a)
ha : (0 < b ∧ b ≤ n) ∧ b ∈ B
hb : (0 < a ∧ a ≤ n) ∧ a ∈ A
⊢ a ∈ A

Tactic:
simp [*]

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A B : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
inst✝ : DecidablePred fun x ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun x ↦
    match x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
b a : ℕ
left✝ : Sum.inr b ≠ Sum.inl a
hxy : f (Sum.inr b) = f (Sum.inl a)
ha : (0 < b ∧ b ≤ n) ∧ b ∈ B
hb : (0 < a ∧ a ≤ n) ∧ a ∈ A
⊢ b ∈ B

Tactic:
simp [*]

Goal state after:
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:
by
  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.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : CommSemiring β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t : Finset α
ha : a ∉ s
hf : 0 ≤ f
hts : t = insert a s
ht : t ∈ 𝒜
⊢ f t ≤ collapse 𝒜 a f s

Tactic:
rw [collapse_eq ha, ← hts, if_pos ht]

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : CommSemiring β
inst✝¹ : LinearOrder β
inst✝ : IsStrictOrderedRing β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
s t : Finset α
ha : a ∉ s
hf : 0 ≤ f
hts : t = insert a s
ht : t ∈ 𝒜
⊢ f t ≤ (if s ∈ 𝒜 then f s else 0) + f 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 ∈ {x | r x a}

Tactic:
exact Setoid.refl a

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

Goal state before:
pp: V : Type u
inst✝ : Nontrivial V
G : SimpleGraph V
h : G.Preconnected
⊢ G.support = Set.univ

Tactic:
simp only [Set.eq_univ_iff_forall]

Goal state after:
V : Type u
inst✝ : Nontrivial V
G : SimpleGraph V
h : G.Preconnected
⊢ ∀ (x : V), x ∈ G.support
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mp
V : Type u
G : SimpleGraph V
hp : G.Preconnected
v : V
⊢ ∃ v, ∀ (w : V), G.Reachable v w

Tactic:
exact ⟨v, fun w => hp v w⟩

Goal state after:
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
⊢ Gᶜ.Reachable u w

Tactic:
have huv' := G.reachable_or_compl_adj .. |>.resolve_left huv

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
⊢ Gᶜ.Reachable u w
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 ≤ #𝒜
range'k : Finset (Fin n) := (range k).attachFin ⋯
𝒞 : Finset (Finset (Fin n)) := powersetCard r range'k
this : Set.Sized r ↑𝒞
⊢ k.choose (r - i) = (#(range k)).choose (r - i)

Tactic:
card_range

Goal state after:
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 ↑𝒞
⊢ k.choose (r - i) = k.choose (r - i)
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G G' : SimpleGraph V
v : V
h : G ≤ G'
c' : G'.ConnectedComponent
hc' : v ∈ c'.supp
⊢ (G.connectedComponentMk v).supp ⊆ c'.supp

Tactic:
intro v' hv'
  simp only [mem_supp_iff, ConnectedComponent.eq] at hv' ⊢
  rw [ConnectedComponent.sound (hv'.mono h)]
  exact hc'

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

Goal state before:
pp: V : Type u
G G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
v : V
⊢ v ∈ ⋃ c, ⋃ (_ : c.supp ⊆ c'.supp), c.supp ↔ v ∈ c'.supp

Tactic:
simp_rw [Set.mem_iUnion]

Goal state after:
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
v : V
⊢ (∃ i, ∃ (_ : i.supp ⊆ c'.supp), v ∈ i.supp) ↔ v ∈ c'.supp
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
v : V
hv : v ∈ c'.supp
⊢ ∃ i, ∃ (_ : i.supp ⊆ c'.supp), v ∈ i.supp

Tactic:
use G.connectedComponentMk v

Goal state after:
case h
V : Type u
G G' : SimpleGraph V
h : G ≤ G'
c' : G'.ConnectedComponent
v : V
hv : v ∈ c'.supp
⊢ ∃ (_ : (G.connectedComponentMk v).supp ⊆ c'.supp), v ∈ (G.connectedComponentMk v).supp
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: case refine_2
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : Set β
x : α
x✝ : x ∈ ⋃ i, s i ∩ f i ⁻¹' t
a : Set α
i : ι
hi : (fun i ↦ s i ∩ f i ⁻¹' t) i = a
ha : x ∈ a
⊢ x ∈ hs.piecewise f ⁻¹' t

Tactic:
rw [← hi, ← (mem_iff_index_eq hs).mp ha.1] at ha

Goal state after:
case refine_2
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
t : Set β
x : α
x✝ : x ∈ ⋃ i, s i ∩ f i ⁻¹' t
a : Set α
i : ι
hi : (fun i ↦ s i ∩ f i ⁻¹' t) i = a
ha : x ∈ (fun i ↦ s i ∩ f i ⁻¹' t) (hs.index x)
⊢ x ∈ hs.piecewise f ⁻¹' t
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: case refine_1
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 ↑𝒞
⊢ (#(range k)).choose r ≤ #𝒜

Tactic:
card_range

Goal state after:
case refine_1
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 ↑𝒞
⊢ k.choose r ≤ #𝒜
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
h : G.Colorable n
⊢ G.chromaticNumber = ↑(sInf {n' | G.Colorable n'})

Tactic:
by
  rw [ENat.natCast_sInf, chromaticNumber]
  exact ⟨_, h⟩

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

Goal state before:
pp: case mp.refine_1
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
p : G.Walk v w
hp : s(v, w) ∉ p.edges
⊢ (Walk.cons ⋯ ↑p.toPath).IsCycle

Tactic:
apply Path.cons_isCycle

Goal state after:
case mp.refine_1
V : Type u
G : SimpleGraph V
v w : V
h : G.Adj v w
p : G.Walk v w
hp : s(v, w) ∉ p.edges
⊢ s(w, v) ∉ (↑p.toPath).edges
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
e : Sym2 V
⊢ (G.deleteEdges {e}).IsBridge e ↔ G.IsBridge e

Tactic:
by
  induction e with | h u v; simp [isBridge_iff]

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

Goal state before:
pp: case pos
V : Type u
G : SimpleGraph V
h : G = ⊥
h' : IsEmpty V
⊢ G.chromaticNumber < 2

Tactic:
simp [chromaticNumber_eq_zero_of_isEmpty]

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

Goal state before:
pp: V✝ : Type u
G : SimpleGraph V✝
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
v w : V ⊕ W
⊢ (completeBipartiteGraph V W).Adj v w → v.isRight ≠ w.isRight

Tactic:
cases v <;> cases w

Goal state after:
case inl.inl
V✝ : Type u
G : SimpleGraph V✝
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
val✝¹ val✝ : V
⊢ (completeBipartiteGraph V W).Adj (Sum.inl val✝¹) (Sum.inl val✝) → (Sum.inl val✝¹).isRight ≠ (Sum.inl val✝).isRight

case inl.inr
V✝ : Type u
G : SimpleGraph V✝
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
val✝¹ : V
val✝ : W
⊢ (completeBipartiteGraph V W).Adj (Sum.inl val✝¹) (Sum.inr val✝) → (Sum.inl val✝¹).isRight ≠ (Sum.inr val✝).isRight

case inr.inl
V✝ : Type u
G : SimpleGraph V✝
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
val✝¹ : W
val✝ : V
⊢ (completeBipartiteGraph V W).Adj (Sum.inr val✝¹) (Sum.inl val✝) → (Sum.inr val✝¹).isRight ≠ (Sum.inl val✝).isRight

case inr.inr
V✝ : Type u
G : SimpleGraph V✝
n : ℕ
ι : Type u_1
α : Type u_2
β : Type u_3
C : G.Coloring α
V : Type u_4
W : Type u_5
val✝¹ val✝ : W
⊢ (completeBipartiteGraph V W).Adj (Sum.inr val✝¹) (Sum.inr val✝) → (Sum.inr val✝¹).isRight ≠ (Sum.inr val✝).isRight