mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Quiver.Schreier

Goal state before:
pp: V : Type u_1
M : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M V
S : Type u_3
ι : S → M
W : Type u_4
inst✝ : MulAction M W
φ : SchreierGraph V ι ⥤q SchreierGraph W ι
φm : φ ⋙q labelling W ι = labelling V ι
v : SchreierGraph V ι
s : S
e : v ⟶ ι s • v := ⟨s, ⋯⟩
h : ι ↑(φ.map e) • φ.obj v = φ.obj (ι s • v)
⊢ (φ ⋙q labelling W ι).map e = (labelling V ι).map e

Tactic:
by

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

Goal state before:
pp: 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
hv' : v ∈ pPrev.vertices ∨ v = (pPrev.cons e).end
h_case₁ : v = (pPrev.cons e).end → ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
hxPrev : v ∈ pPrev.vertices
hxe_ne : v ≠ (pPrev.cons e).end
q₁ : Path a v
q₂ : Path v b✝
h_prev : pPrev = q₁.comp q₂
h_not_tail : ¬v ∈ q₂.vertices.tail
q₂' : Path v (pPrev.cons e).end := q₂.cons e
h_no_tail : ¬v ∈ q₂'.vertices.tail
⊢ pPrev.cons e = q₁.comp q₂'

Tactic:
by

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

Goal state before:
pp: 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
hv' : v ∈ pPrev.vertices ∨ v = (pPrev.cons e).end
h_case₁ : v = (pPrev.cons e).end → ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
⊢ v ∈ pPrev.vertices → v ≠ (pPrev.cons e).end → ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail

Tactic:
by

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

Goal state before:
pp: V : Type u_1
M : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M V
S : Type u_3
ι : S → M
W : Type u_4
inst✝ : MulAction M W
φ : SchreierGraph V ι ⥤q SchreierGraph W ι
φm : φ ⋙q labelling W ι = labelling V ι
v : SchreierGraph V ι
s : S
e : v ⟶ ι s • v := ⟨s, ⋯⟩
h : ι ↑(φ.map e) • φ.obj v = φ.obj (ι s • v)
⊢ ↑(φ.map e) = s

Tactic:
by

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

Goal state before:
pp: V : Type u_1
M : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M V
S : Type u_3
ι : S → M
W : Type u_4
inst✝ : MulAction M W
φ : SchreierGraph V ι ⥤q SchreierGraph W ι
φm : φ ⋙q labelling W ι = labelling V ι
v : SchreierGraph V ι
s : S
⊢ φ.obj (ι s • v) = ι s • φ.obj v

Tactic:
by

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

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
v : V
hv : v ∈ p.vertices
⊢ ∃ p₁ p₂, p = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail

Tactic:
by

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
⊢ g.totalDegree ≤ f.totalDegree

Tactic:
by

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

Goal state before:
pp: U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨x₁, p₁⟩ = (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a₂ → ⟨x₁, p₁⟩ = a₂
y₂ x₂ : U
p₂ : Path u x₂
e₂ : x₂ ⟶ y₂
hφy : φ.obj y₁ = φ.obj y₂
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₂).cons (φ.map e₂)
hφx : φ.obj x₁ = φ.obj x₂
hφp : φ.mapPath p₁ ≍ φ.mapPath p₂
hφe : φ.map e₁ ≍ φ.map e₂
⊢ φ.pathStar u ⟨x₁, p₁⟩ = φ.pathStar u ⟨x₂, p₂⟩

Tactic:
by

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
this : Finsupp.degree (degLex.degree (h i * Alon.P (S i) i)) ≤ f.totalDegree
⊢ IsRegular (degLex.leadingCoeff (Alon.P (S i) i))

Tactic:
by

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

Goal state before:
pp: U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨x₁, p₁⟩ = (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a₂ → ⟨x₁, p₁⟩ = a₂
y₂ : U
hφy : φ.obj y₁ = φ.obj y₂
e₂ : x₁ ⟶ y₂
hφx : φ.obj x₁ = φ.obj x₁
hφe : φ.map e₁ ≍ φ.map e₂
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₁).cons (φ.map e₂)
hφp : φ.mapPath p₁ ≍ φ.mapPath p₁
h_path_star : φ.pathStar u ⟨x₁, p₁⟩ = φ.pathStar u ⟨x₁, p₁⟩
⊢ φ.star x₁ ⟨y₁, e₁⟩ = φ.star x₁ ⟨y₂, e₂⟩

Tactic:
by

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

Goal state before:
pp: U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u : U
⊢ Injective (φ.pathStar u)

Tactic:
by

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

Goal state before:
pp: 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
⊢ Surjective (φ.pathStar u)

Tactic:
by

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

Goal state before:
pp: U : Type ?u.2
inst✝⁴ : Quiver U
V : Type ?u.6
inst✝³ : Quiver V
φ : U ⥤q V
W : Type ?u.15
inst✝² : Quiver W
ψ : V ⥤q W
inst✝¹ : HasInvolutiveReverse U
inst✝ : HasInvolutiveReverse V
u : U
e : Star u
⊢ (fun e ↦ ⟨e.fst, reverse e.snd⟩) ((fun e ↦ ⟨e.fst, reverse e.snd⟩) e) = e

Tactic:
by

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

Goal state before:
pp: U : Type ?u.2
inst✝⁴ : Quiver U
V : Type ?u.6
inst✝³ : Quiver V
φ : U ⥤q V
W : Type ?u.15
inst✝² : Quiver W
ψ : V ⥤q W
inst✝¹ : HasInvolutiveReverse U
inst✝ : HasInvolutiveReverse V
u : U
e : Costar u
⊢ (fun e ↦ ⟨e.fst, reverse e.snd⟩) ((fun e ↦ ⟨e.fst, reverse e.snd⟩) e) = e

Tactic:
by

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

Goal state before:
pp: U : Type u_1
inst✝⁴ : Quiver U
V : Type u_2
inst✝³ : Quiver V
φ : U ⥤q V
inst✝² : HasInvolutiveReverse U
inst✝¹ : HasInvolutiveReverse V
inst✝ : φ.MapReverse
u : U
⊢ φ.costar u = ⇑(starEquivCostar (φ.obj u)) ∘ φ.star u ∘ ⇑(starEquivCostar u).symm

Tactic:
by

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

Goal state before:
pp: U : Type u_1
inst✝⁴ : Quiver U
V : Type u_2
inst✝³ : Quiver V
φ : U ⥤q V
inst✝² : HasInvolutiveReverse U
inst✝¹ : HasInvolutiveReverse V
inst✝ : φ.MapReverse
u : U
⊢ Bijective (φ.costar u) ↔ Bijective (φ.star u)

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : SemilatticeSup α
s t : Set α
c : α
⊢ c ∈ s ⊻ t ↔ ∃ a ∈ s, ∃ b ∈ t, a ⊔ b = c

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : SemilatticeSup α
s t : Set α
a : α
⊢ {b | b ∈ s ⊻ t ∧ b ≤ a} = {b | b ∈ s ∧ b ≤ a} ⊻ {b | b ∈ t ∧ b ≤ a}

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
c : α
⊢ c ∈ s ⊼ t ↔ ∃ a ∈ s, ∃ b ∈ t, a ⊓ b = c

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
a : α
⊢ {b | b ∈ s ⊼ t ∧ a ≤ b} = {b | b ∈ s ∧ a ≤ b} ⊼ {b | b ∈ t ∧ a ≤ b}

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : SemilatticeSup α
s t : Set α
⊢ upperClosure (s ⊻ t) = upperClosure s ⊔ upperClosure t

Tactic:
by

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

Goal state before:
pp: α : Type u_2
inst✝ : SemilatticeInf α
s t : Set α
⊢ lowerClosure (s ⊼ t) = lowerClosure s ⊓ lowerClosure t

Tactic:
by

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)
⊢ ∃ s, (∀ (i : σ), s i ∈ S i) ∧ (eval s) f ≠ 0

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ nonMemberSubfamily a 𝒜 ↔ s ∈ 𝒜 ∧ a ∉ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
h : insert a s ∈ 𝒜 ∧ a ∉ s
⊢ a ∈ insert a s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ memberSubfamily a 𝒜 ↔ insert a s ∈ 𝒜 ∧ a ∉ s

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ #(memberSubfamily a 𝒜) + #(nonMemberSubfamily a 𝒜) = #𝒜

Tactic:
by

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 ∈ 𝒜
ha : a ∈ s
⊢ insert a (s.erase a) ∈ 𝒜

Tactic:
by

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 ∈ 𝒜
ha : a ∉ s
⊢ s.erase a ∈ 𝒜

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ memberSubfamily a 𝒜 ∪ nonMemberSubfamily a 𝒜 = image (fun s ↦ s.erase a) 𝒜

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h𝒜 : ∀ s ∈ 𝒜, a ∉ s
⊢ memberSubfamily a (image (insert a) 𝒜) = 𝒜

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
⊢ nonMemberSubfamily a (image (insert a) 𝒜) = ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
⊢ memberSubfamily a (image (fun x ↦ x.erase a) 𝒜) = ∅

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
⊢ image (insert a) (memberSubfamily a 𝒜) = {s ∈ 𝒜 | a ∈ s}

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
x✝ : { n // 0 < n }
⊢ 0 ≤ ↑(#({a ∈ Ioc 0 ↑x✝ | a ∈ A})) / ↑↑x✝

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
n : ℕ
hn : n ≠ 0
x✝¹ : ℝ
x✝ : x✝¹ ∈ Set.range fun n ↦ ↑(#({a ∈ Ioc 0 ↑n | a ∈ A})) / ↑↑n
w✝ : { n // 0 < n }
hx : (fun n ↦ ↑(#({a ∈ Ioc 0 ↑n | a ∈ A})) / ↑↑n) w✝ = x✝¹
⊢ 0 ≤ (fun n ↦ ↑(#({a ∈ Ioc 0 ↑n | a ∈ A})) / ↑↑n) w✝

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
n : ℕ
hn : n ≠ 0
⊢ 0 < ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
n : ℕ
⊢ schnirelmannDensity A * ↑n ≤ ↑(#({a ∈ Ioc 0 n | a ∈ A}))

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
⊢ ↑(#({a ∈ Ioc 0 1 | a ∈ A})) / ↑1 ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
this : {a ∈ Ioc 0 k | a ∈ A} ⊆ Ioo 0 k
⊢ #(Ioo 0 k) = k - 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
𝒜 : Finset (Finset α)
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
⊢ p 𝒜

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
k : ℕ
hk : k ∉ A
⊢ schnirelmannDensity A ≤ 1 - (↑k)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
h : 1 ∉ A
⊢ 1 - (↑1)⁻¹ ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ B
h : A ⊆ B
x✝¹ : ℝ
x✝ : x✝¹ ∈ Set.range fun n ↦ ↑(#({a ∈ Ioc 0 ↑n | a ∈ A})) / ↑↑n
w✝ : { n // 0 < n }
hx : (fun n ↦ ↑(#({a ∈ Ioc 0 ↑n | a ∈ A})) / ↑↑n) w✝ = x✝¹
⊢ 0 ≤ (fun n ↦ ↑(#({a ∈ Ioc 0 ↑n | a ∈ A})) / ↑↑n) w✝

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ B
h : A ⊆ B
x✝ : { n // 0 < n }
⊢ ↑(#({a ∈ Ioc 0 ↑x✝ | a ∈ A})) / ↑↑x✝ ≤ ↑(#({a ∈ Ioc 0 ↑x✝ | a ∈ B})) / ↑↑x✝

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
𝒜✝ : Finset (Finset α)
empty : p ∅
singleton_empty : p {∅}
image_insert : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, (∀ s ∈ 𝒜, a ∉ s) → p 𝒜 → p (image (insert a) 𝒜)
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p ({s ∈ 𝒜 | a ∉ s}) → p ({s ∈ 𝒜 | a ∈ s}) → p 𝒜
a : α
𝒜 : Finset (Finset α)
h𝒜₀ : p (nonMemberSubfamily a 𝒜)
h𝒜₁ : p (memberSubfamily a 𝒜)
⊢ ∀ s ∈ memberSubfamily a 𝒜, a ∉ s

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
𝒜 : Finset (Finset α)
empty : p ∅
singleton_empty : p {∅}
image_insert : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, (∀ s ∈ 𝒜, a ∉ s) → p 𝒜 → p (image (insert a) 𝒜)
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p ({s ∈ 𝒜 | a ∉ s}) → p ({s ∈ 𝒜 | a ∈ s}) → p 𝒜
⊢ p 𝒜

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ 𝓓 a 𝒜 ↔ s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s ∉ 𝒜 ∧ insert a s ∈ 𝒜

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
⊢ schnirelmannDensity A = 1 ↔ {0}ᶜ ⊆ A

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : s ∈ 𝒜
⊢ s.erase a ∈ 𝓓 a 𝒜

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
hA : 0 ∈ A
⊢ schnirelmannDensity A = 1 ↔ A = Set.univ

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
x x✝¹ : ℝ
x✝ : x✝¹ ∈ Set.range fun n ↦ ↑(#({a ∈ Ioc 0 ↑n | a ∈ A})) / ↑↑n
w✝ : { n // 0 < n }
hx : (fun n ↦ ↑(#({a ∈ Ioc 0 ↑n | a ∈ A})) / ↑↑n) w✝ = x✝¹
⊢ 0 ≤ (fun n ↦ ↑(#({a ∈ Ioc 0 ↑n | a ∈ A})) / ↑↑n) w✝

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
x : ℝ
⊢ schnirelmannDensity A < x ↔ ∃ n, 0 < n ∧ ↑(#({a ∈ Ioc 0 n | a ∈ A})) / ↑n < x

Tactic:
by

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

Goal state before:
pp: m n : ℕ
h : n < m
f : ℕ → ℚ := fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹
hf : f = fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹
this : ∀ i ∈ range (n + 1), f i - f (i + 1) = ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i))
⊢ ∑ i ∈ range (n + 1), ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i)) = 1

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
x : ℝ
⊢ schnirelmannDensity A ≤ x ↔ ∀ (ε : ℝ), 0 < ε → ∃ n, 0 < n ∧ ↑(#({a ∈ Ioc 0 n | a ∈ A})) / ↑n < x + ε

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ 𝓓 a 𝒜 → s.erase a ∈ 𝓓 a 𝒜

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
⊢ schnirelmannDensity A = schnirelmannDensity B

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
inst✝ : DecidablePred fun x ↦ x ∈ insert 0 A
⊢ ∀ n > 0, n ∈ insert 0 A ↔ n ∈ A

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
inst✝ : DecidablePred fun x ↦ x ∈ A \ {0}
⊢ ∀ n > 0, n ∈ A \ {0} ↔ n ∈ A

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ B
h : A = B
⊢ ∀ n > 0, n ∈ A ↔ n ∈ B

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
h : insert a s ∈ 𝓓 a 𝒜
⊢ s ∈ 𝓓 a 𝒜

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
ε : ℝ
hε : 0 < ε
hA : schnirelmannDensity A = 0
⊢ ∃ n, 0 < n ∧ ↑(#({a ∈ Ioc 0 n | a ∈ A})) / ↑n < ε

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
ε : ℝ
hε : 0 < ε
hA : schnirelmannDensity A = 0
⊢ ∃ n, 0 < n ∧ ↑(#({a ∈ Ioc 0 n | a ∈ A})) / ↑n < ε

Tactic:
by
  by_contra! h
  rw [← le_schnirelmannDensity_iff] at h
  linarith

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: ⊢ 1 ∉ ∅

Tactic:
by

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:
by

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

Goal state before:
pp: m n : ℕ
h : n < m
⊢ ∑ i ∈ range (n + 1), ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i)) = 1

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

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

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

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

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
hA : A.Finite
⊢ schnirelmannDensity A = 0

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: ⊢ 0 ∈ Set.univ

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: ⊢ Set.univ = Set.univ

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: ⊢ 1 ∉ Set.ofPred Even

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: ⊢ 1 ∉ Set.ofPred Nat.Prime

Tactic:
simp [Nat.not_prime_one]

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: ⊢ 1 ∉ Set.ofPred Nat.Prime

Tactic:
by

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

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

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
⊢ image (fun x ↦ x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ {x ∈ Ioc 0 n | x % m = 1}

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: m : ℕ
hm : m ≠ 1
⊢ schnirelmannDensity {n | n % m = 1} = (↑m)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: m : ℕ
⊢ schnirelmannDensity {n | n ≡ 1 [MOD m]} = (↑m)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: h : Set.ofPred Odd = {n | n % 2 = 1}
⊢ 2 ≠ 1

Tactic:
by

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: ⊢ schnirelmannDensity (Set.ofPred Odd) = 2⁻¹

Tactic:
by

Goal state after: