mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
k : ℕ
ih : k ≤ 2 * m - 1 → ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
hk : k + 1 ≤ 2 * m - 1
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = k
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
this✝ : 2 * n - 1 ≤ #(s \ 𝒜.biUnion id)
t₀ : Finset ι
ht₀ : t₀ ⊆ s \ 𝒜.biUnion id
ht₀card : #t₀ = n
ht₀sum : ↑n ∣ ∑ i ∈ t₀, a i
this : t₀ ∉ 𝒜
⊢ #𝒜 + 1 = k + 1

Tactic:
h𝒜card

Goal state after:
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
k : ℕ
ih : k ≤ 2 * m - 1 → ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
hk : k + 1 ≤ 2 * m - 1
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = k
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
this✝ : 2 * n - 1 ≤ #(s \ 𝒜.biUnion id)
t₀ : Finset ι
ht₀ : t₀ ⊆ s \ 𝒜.biUnion id
ht₀card : #t₀ = n
ht₀sum : ↑n ∣ ∑ i ∈ t₀, a i
this : t₀ ∉ 𝒜
⊢ k + 1 = k + 1
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
hf : f ∈ derangements (Subtype p)
a : α
ha : p a
hfa : (Perm.ofSubtype f) a = a
⊢ ↑(f ⟨a, ha⟩) = ↑⟨a, ha⟩

Tactic:
Perm.ofSubtype_apply_of_mem _ ha

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
hf : f ∈ derangements (Subtype p)
a : α
ha : p a
hfa : ↑(f ⟨a, ha⟩) = a
⊢ ↑(f ⟨a, ha⟩) = ↑⟨a, ha⟩
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
⊢ Fintype.card P ≤ Fintype.card L

Tactic:
by_contra hc₂

Goal state after:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hc₂ : ¬Fintype.card P ≤ Fintype.card L
⊢ False
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
a b c d x✝ y✝ : G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
x : G
hx : x ∈ A
y : G
hy : y ∈ A
⊢ 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A))

Tactic:
convert! lt_card_smul_inter_smul (by simpa using Rat.cast_strictMono (K := ℝ) h) hx hy

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A✝ B S : Finset G
a b c d x✝ y✝ : G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
x : G
hx : x ∈ A
y : G
hy : y ∈ A
⊢ 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A)) ↔ (2 - 3 / 2) * ↑(#A) < ↑(#(x •> A ∩ y •> A))
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝³ : NonAssocSemiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableLE α
a b : α
⊢ (zeta 𝕜 * zeta 𝕜) a b = ↑(#(Icc a b))

Tactic:
by
  rw [mul_apply, card_eq_sum_ones, Nat.cast_sum, Nat.cast_one]
  refine sum_congr rfl fun x hx ↦ ?_
  rw [mem_Icc] at hx
  rw [zeta_of_le hx.1, zeta_of_le hx.2, one_mul]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: ⊢ Nat.bell 0 = 1

Tactic:
by
  simp [Nat.bell]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
hprod : ∀ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) ≠ 0
x : ℕ
hx : g x ≠ 0
⊢ x ∈ g.support

Tactic:
by simpa using hx

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Basic

Goal state before:
pp: k : ℤ
⊢ pentagonal (-k) = (k * (3 * k + 1) / 2).toNat

Tactic:
by
  grind [pentagonal_def]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: case refine_3
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : IsTopologicalRing R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
i : ↑(Function.mulSupport fun i ↦ 1 - (X ^ (i + 1)) ^ m)
⊢ (if m ∣ (↑i + 1) * m - 1 + 1 then 1 * (1 - X ^ ((↑i + 1) * m - 1 + 1)) else 1) = 1 - (X ^ (↑i + 1)) ^ m

Tactic:
have : (i + 1) * m - 1 + 1 = (i + 1) * m := by grind

Goal state after:
case refine_3
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : IsTopologicalRing R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
i : ↑(Function.mulSupport fun i ↦ 1 - (X ^ (i + 1)) ^ m)
this : (↑i + 1) * m - 1 + 1 = (↑i + 1) * m
⊢ (if m ∣ (↑i + 1) * m - 1 + 1 then 1 * (1 - X ^ ((↑i + 1) * m - 1 + 1)) else 1) = 1 - (X ^ (↑i + 1)) ^ m
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
this✝ : ↑(#(A ∩ B)) + ↑(#(A ∪ B)) = ↑(#A) + ↑(#B)
this : K * ↑(#(A ∩ B)) + K * ↑(#(A ∪ B)) = K * ↑(#A) + K * ↑(#B)
⊢ expansion K S (A ∩ B) + expansion K S (A ∪ B) ≤ expansion K S A + expansion K S B

Tactic:
have : (#(A * S ∩ (B * S)) + #(A * S ∪ B * S) : ℝ) = #(A * S) + #(B * S) :=
    mod_cast card_inter_add_card_union (A * S) (B * S)

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A B S : Finset G
this✝¹ : ↑(#(A ∩ B)) + ↑(#(A ∪ B)) = ↑(#A) + ↑(#B)
this✝ : K * ↑(#(A ∩ B)) + K * ↑(#(A ∪ B)) = K * ↑(#A) + K * ↑(#B)
this : ↑(#(A * S ∩ (B * S))) + ↑(#(A * S ∪ B * S)) = ↑(#(A * S)) + ↑(#(B * S))
⊢ expansion K S (A ∩ B) + expansion K S (A ∪ B) ≤ expansion K S A + expansion K S B
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))
k : ℕ
| x ^ 2 * x ^ k * ∏ x_1 ∈ Finset.range (k + 1), (1 - x ^ (x_1 + 1))

Tactic:
mul_assoc (x ^ 2)

Goal state after:
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))
k : ℕ
| x ^ 2 * (x ^ k * ∏ x_1 ∈ Finset.range (k + 1), (1 - x ^ (x_1 + 1)))
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
k : ℕ
⊢ Tendsto (fun i ↦ (-X ^ (i + k + 1)).order) atTop (𝓝 ⊤)

Tactic:
nontriviality R using Subsingleton.eq_zero (α := R⟦X⟧)
  simp_rw [order_neg, order_X_pow, add_assoc]
  exact ENat.tendsto_natCast_nhds_top.comp (tendsto_add_atTop_nat _)

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

Goal state before:
pp: case calc_2
n : ℕ
⊢ ↑(2 * (n / 6) + 1) * ↑(rothNumberNat (n / 6)) ≤ ↑(ruzsaSzemerediNumberNat (6 * (n / 6) + 3))

Tactic:
· norm_cast
      exact rothNumberNat_le_ruzsaSzemerediNumberNat _

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case inr.inr
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
e : η
hl : l.idxFun i = Sum.inr e
f : η
hm : m.idxFun i = Sum.inr f
a b : α
hab : a ≠ b
⊢ e = f

Tactic:
by_contra! hef

Goal state after:
case inr.inr
η : Type u_5
α : Type u_6
ι : Type u_7
inst✝ : Nontrivial α
l m : Subspace η α ι
i : ι
hlm : ∀ (x : η → α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
e : η
hl : l.idxFun i = Sum.inr e
f : η
hm : m.idxFun i = Sum.inr f
a b : α
hab : a ≠ b
hef : e ≠ f
⊢ False
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

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

Tactic:
delete_ground,

Goal state after:
α : Type u_1
M : Matroid α
D₁ D₂ : Set α
h : M.E \ (M.E \ (D₁ ∩ M.E)) = M.E \ (M.E \ (D₂ ∩ M.E))
⊢ D₁ ∩ M.E = D₂ ∩ M.E
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D X : Set α
⊢ ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ (M ＼ D).E ↔ (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D

Tactic:
delete_ground,

Goal state after:
α : Type u_1
M : Matroid α
D X : Set α
⊢ ¬(M.Indep X ∧ Disjoint X D) ∧ X ⊆ M.E \ D ↔ (¬M.Indep X ∧ X ⊆ M.E) ∧ Disjoint X D
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
I D X : Set α
⊢ M.IsBasis I (X ∩ (M ＼ D).E) ∧ Disjoint (X ∩ (M ＼ D).E) D ↔ M.IsBasis' I (X \ D)

Tactic:
delete_ground,

Goal state after:
α : Type u_1
M : Matroid α
I D X : Set α
⊢ M.IsBasis I (X ∩ (M.E \ D)) ∧ Disjoint (X ∩ (M.E \ D)) D ↔ M.IsBasis' I (X \ D)
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: X : Type u_1
inst✝¹ : Fintype X
f : Numbering X
s : Finset X
inst✝ : DecidableEq X
⊢ f ∈ prefixed s ↔ f.IsPrefix s

Tactic:
by simp [prefixed]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C D : Set α
hE : M.E ⊆ (M ／ C ＼ D).E
⊢ M = M ／ C ＼ D

Tactic:
delete_ground,

Goal state after:
α : Type u_1
M : Matroid α
C D : Set α
hE : M.E ⊆ (M ／ C).E \ D
⊢ M = M ／ C ＼ D
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 ((M✶ ＼ I).E \ B) ∧ B ⊆ (M✶ ＼ I).E ↔ M.IsBase (B ∪ I) ∧ Disjoint B I

Tactic:
delete_ground,

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
C : Set α
h : e ∈ M.E \ M.closure C
heC : e ∈ C
⊢ e ∈ M.closure C

Tactic:
rw [← closure_inter_ground]

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
h : ∀ (i : ι), (M i).Finitary
⊢ (Matroid.sigma M).Finitary

Tactic:
by
  refine ⟨fun I hI ↦ ?_⟩
  simp only [sigma_indep_iff] at hI ⊢
  intro i
  apply indep_of_forall_finite_subset_indep
  intro J hJI hJ
  convert! hI (Sigma.mk i '' J) (by simpa) (hJ.image _) i
  rw [sigma_mk_preimage_image_eq_self]

Goal state after:
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:
delete_ground,

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.E \ D)) = C ∩ (M.E \ D)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

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

Tactic:
delete_ground,

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

Goal state before:
pp: case nil
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
height_le : ∀ {a b : V} (a_1 : Path a b), height a ≤ height b
q : Path r r
⊢ Path.nil = q

Tactic:
rcases q with _ | ⟨q, f⟩

Goal state after:
case nil.nil
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
height_le : ∀ {a b : V} (a_1 : Path a b), height a ≤ height b
⊢ Path.nil = Path.nil

case nil.cons
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
height_le : ∀ {a b : V} (a_1 : Path a b), height a ≤ height b
b✝ : V
q : Path r b✝
f : b✝ ⟶ r
⊢ Path.nil = q.cons f
Module: Mathlib.Combinatorics.Quiver.Arborescence

Goal state before:
pp: case cons
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
height_le : ∀ {a b : V} (a_1 : Path a b), height a ≤ height b
b✝ c✝ : V
p : Path r b✝
e : b✝ ⟶ c✝
ih : ∀ (q : Path r b✝), p = q
q : Path r c✝
⊢ p.cons e = q

Tactic:
rcases q with _ | ⟨q, f⟩

Goal state after:
case cons.nil
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
height_le : ∀ {a b : V} (a_1 : Path a b), height a ≤ height b
b✝ : V
p : Path r b✝
ih : ∀ (q : Path r b✝), p = q
e : b✝ ⟶ r
⊢ p.cons e = Path.nil

case cons.cons
V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
height_le : ∀ {a b : V} (a_1 : Path a b), height a ≤ height b
b✝¹ c✝ : V
p : Path r b✝¹
e : b✝¹ ⟶ c✝
ih : ∀ (q : Path r b✝¹), p = q
b✝ : V
q : Path r b✝
f : b✝ ⟶ c✝
⊢ p.cons e = q.cons f
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case h.Hdeg
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 σ := ⋯
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
⊢ ∀ (i : σ), degreeOf i r < #(S i)

pp: case h.Heval
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 σ := ⋯
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
⊢ ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) r = 0

Tactic:
· intro i
    rw [degreeOf_eq_sup, Finset.sup_lt_iff (by simp [Sne i])]
    aesop (add simp [Alon.degree_P])

Goal state after:
case h.Heval
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 σ := ⋯
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
⊢ ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) r = 0
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: case cons.inl
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
v b✝ c✝ : V
pPrev : Path a b✝
e : b✝ ⟶ c✝
ih : v ∈ pPrev.vertices → ∃ p₁ p₂, pPrev = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
hv : v ∈ (pPrev.cons e).vertices
h_case₁ : v = (pPrev.cons e).end → ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
h_case₂ : v ∈ pPrev.vertices → v ≠ (pPrev.cons e).end → ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
h_in_prefix : v ∈ pPrev.vertices
⊢ ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail

Tactic:
| inl h_in_prefix =>

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: case cons
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
v b✝ c✝ : V
pPrev : Path a b✝
e : b✝ ⟶ c✝
ih : v ∈ pPrev.vertices → ∃ p₁ p₂, pPrev = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
hv : v ∈ (pPrev.cons e).vertices
⊢ ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail

Tactic:
| cons pPrev e ih =>

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
f : MvPolynomial σ R
t : σ →₀ ℕ
ht : coeff t f ≠ 0
ht' : f.totalDegree = Finsupp.degree t
S : σ → Finset R
htS : ∀ (i : σ), t i < #(S i)
x✝ : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
Heval : ∀ (s : σ → R), (∀ (i : σ), s i ∈ S i) → (eval s) f = 0
h : σ →₀ MvPolynomial σ R
hh : ∀ (i : σ), ((∏ s ∈ S i, (X i - C s)) * h i).totalDegree ≤ f.totalDegree
hf : f = (linearCombination (MvPolynomial σ R) fun i ↦ ∏ r ∈ S i, (X i - C r)) h
i : σ
a✝ : i ∈ h.support
g : MvPolynomial σ R := h i * Alon.P (S i) i
hg : g = h i * Alon.P (S i) i
hi : ¬h i = 0
⊢ (Alon.P (S i) i * h i).totalDegree ≤ f.totalDegree

Tactic:
exact hh i

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case mp.inl
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
hA : 0 ∈ A
h : {0}ᶜ ⊆ A
⊢ 0 ∈ A

Tactic:
exact hA

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ 𝒜 ∧ s.erase a ∉ 𝒜
⊢ s ∈ {s | a ∈ s}

Tactic:
exact not_imp_comm.1 erase_eq_of_notMem (ne_of_mem_of_not_mem hs.1 hs.2).symm

Goal state after:
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
h : u ⊆ s ∪ t
⊢ (s ∪ t) ∩ u = u

Tactic:
inter_eq_right

Goal state after:
case refine_1
α : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
h : u ⊆ s ∪ t
⊢ u ⊆ s ∪ t
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
h : u ⊆ s ∩ t
⊢ s ∩ t ∩ u = u

Tactic:
inter_eq_right

Goal state after:
case refine_1
α : Type u_2
inst✝ : DecidableEq α
s t u : Finset α
h : u ⊆ s ∩ t
⊢ u ⊆ s ∩ t
Module: Mathlib.Combinatorics.SetFamily.Shadow

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

Tactic:
by
  induction k generalizing t with
  | zero => simp
  | succ k ih =>
    simp only [mem_upShadow_iff_erase_mem, ih, Function.iterate_succ_apply', card_eq_succ,
      subset_erase, erase_sdiff_comm, ← sdiff_insert]
    constructor
    · rintro ⟨a, hat, u, rfl, ⟨hut, hau⟩, htu⟩
      exact ⟨_, ⟨_, _, hau, rfl, rfl⟩, insert_subset hat hut, htu⟩
    · rintro ⟨_, ⟨a, u, hau, rfl, rfl⟩, hut, htu⟩
      rw [insert_subset_iff] at hut
      exact ⟨a, hut.1, _, rfl, ⟨hut.2, hau⟩, htu⟩

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
⊢ supSum {s} = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹

Tactic:
have : ∀ t : Finset α,
    (card α - #(truncatedSup {s} t) : ℚ) / ((card α - #t) * (card α).choose #t) =
    if t ⊆ s then (card α - #s : ℚ) / ((card α - #t) * (card α).choose #t) else 0 := by
    rintro t
    simp_rw [truncatedSup_singleton]
    split_ifs <;> simp

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
this :
  ∀ (t : Finset α),
    (↑(card α) - ↑(#({s}.truncatedSup t))) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
      if t ⊆ s then (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) else 0
⊢ supSum {s} = ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: case succ.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
hcard : #t + (k + 1) = #s
u : Finset α
htu : t ⊆ u
hus : u ⊆ s
hu : #u = #t + 1
⊢ #t + 1 + k = #s

Tactic:
← hcard,

Goal state after:
case succ.mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ℕ
𝒜 : Finset (Finset α)
s t : Finset α
ht : t ∈ 𝒜
hts : t ⊆ s
hcard : #t + (k + 1) = #s
u : Finset α
htu : t ⊆ u
hus : u ⊆ s
hu : #u = #t + 1
⊢ #t + 1 + k = #t + (k + 1)
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
𝒜 : Finset (Finset α)
inst✝ : Nonempty α
h𝒜₁ : 𝒜.Nonempty
h𝒜₀ : ∅ ∉ 𝒜
⊢ infSum 𝒜 = 1

Tactic:
← compls_compls 𝒜,

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
𝒜 : Finset (Finset α)
inst✝ : Nonempty α
h𝒜₁ : 𝒜.Nonempty
h𝒜₀ : ∅ ∉ 𝒜
⊢ infSum 𝒜ᶜˢᶜˢ = 1
Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman

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

Tactic:
sdiff_inter_self_right,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsLowerSet ↑ℬ
this : 2 ^ Fintype.card α * #(ℬ \ 𝒜ᶜ) ≤ #𝒜 * #ℬ
⊢ 2 ^ Fintype.card α * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ
Module: Mathlib.Combinatorics.SetFamily.HarrisKleitman

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

pp: case h₁
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsUpperSet ↑ℬ
this : 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * #ℬ - #𝒜 * #ℬ
⊢ 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * #ℬ

pp: case h₂
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsUpperSet ↑ℬ
this : 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * #ℬ - #𝒜 * #ℬ
⊢ #𝒜 * #ℬ ≤ 2 ^ Fintype.card α * #ℬ

Tactic:
sdiff_inter_self_right,

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

case h₁
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsUpperSet ↑ℬ
this : 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * #ℬ - #𝒜 * #ℬ
⊢ 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * #ℬ

case h₂
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜ᶜ
hℬ : IsUpperSet ↑ℬ
this : 2 ^ Fintype.card α * #(𝒜ᶜ ∩ ℬ) ≤ 2 ^ Fintype.card α * #ℬ - #𝒜 * #ℬ
⊢ #𝒜 * #ℬ ≤ 2 ^ Fintype.card α * #ℬ