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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
hs1 : s ∈ 𝒜
hs2 : a ∈ s
⊢ s ∈ 𝒜 ∧ a ∉ s.erase a

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
hs1 : s ∈ 𝒜
hs2 : a ∈ s
⊢ s ∈ 𝒜 ∧ a ∉ s.erase a
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 ℬ : Finset (Finset α)
⊢ image (fun s ↦ s.erase a) ({s ∈ 𝒜 | a ∈ s}) ∩ image (fun s ↦ s.erase a) ({s ∈ ℬ | a ∈ s}) =
    image (fun s ↦ s.erase a) ({s ∈ 𝒜 | a ∈ s}) ∩ image (fun s ↦ s.erase a) ({s ∈ ℬ | a ∈ s})

pp: α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 ℬ : Finset (Finset α)
⊢ ↑({s ∈ 𝒜 | a ∈ s}) ∪ ↑({s ∈ ℬ | a ∈ s}) ⊆ {s | a ∈ s}

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 ℬ : Finset (Finset α)
⊢ ↑({s ∈ 𝒜 | a ∈ s}) ∪ ↑({s ∈ ℬ | a ∈ s}) ⊆ {s | a ∈ s}
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ #({s ∈ 𝒜 | a ∈ s}) + #({s ∈ 𝒜 | a ∉ s}) = #𝒜

pp: α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ Set.InjOn (fun s ↦ s.erase a) ↑({s ∈ 𝒜 | a ∈ s})

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ #({s ∈ 𝒜 | a ∈ s}) + #({s ∈ 𝒜 | a ∉ s}) = #𝒜

α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ Set.InjOn (fun s ↦ s.erase a) ↑({s ∈ 𝒜 | a ∈ s})
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 ∈ 𝒜

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ 𝒜
ha : a ∈ s
⊢ s ∈ 𝒜
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 ∈ 𝒜

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ 𝒜
ha : a ∉ s
⊢ s ∈ 𝒜
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

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

Tactic:
rintro ⟨⟨t, ht, hts⟩, hs⟩

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h𝒜 : ∀ s ∈ 𝒜, a ∉ s
s : Finset α
hs : a ∉ s
t : Finset α
ht : t ∈ 𝒜
hts : insert a t = insert a s
⊢ s ∈ 𝒜
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

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

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
h𝒜 : ∀ s ∈ 𝒜, a ∉ s
s : Finset α
hs : a ∉ s
t : Finset α
ht : t ∈ 𝒜
hts : insert a t = insert a s
⊢ t ∈ 𝒜
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
x✝ : s ∈ 𝒜 ∧ a ∈ s
hs : s ∈ 𝒜
ha : a ∈ s
⊢ s ∈ 𝒜

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
x✝ : s ∈ 𝒜 ∧ a ∈ s
hs : s ∈ 𝒜
ha : a ∈ s
⊢ s ∈ 𝒜
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

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

Tactic:
]

Goal state after:
case empty
α : Type u_1
inst✝ : DecidableEq α
p : Finset (Finset α) → Prop
empty : p ∅
singleton_empty : p {∅}
subfamily : ∀ (a : α) ⦃𝒜 : Finset (Finset α)⦄, p (nonMemberSubfamily a 𝒜) → p (memberSubfamily a 𝒜) → p 𝒜
𝒜 : Finset (Finset α)
hu : 𝒜 = ∅ ∨ 𝒜 = {∅}
⊢ p 𝒜
Module: Mathlib.Combinatorics.Schnirelmann

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

Tactic:
]

Goal state after:
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
⊢ #({a ∈ Ioc 0 1 | a ∈ A}) ≤ 1
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case inr
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ ↑(#({a ∈ Ioc 0 k | a ∈ A})) / ↑k ≤ (↑k - 1) / ↑k

Tactic:
]

Goal state after:
case inr
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ ↑(#({a ∈ Ioc 0 k | a ∈ A})) / ↑k ≤ (↑k - 1) / ↑k
Module: Mathlib.Combinatorics.Schnirelmann

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

Tactic:
]

Goal state after:
case hab
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ #({a ∈ Ioc 0 k | a ∈ A}) ≤ k - 1
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case hab
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ {a ∈ Ioo 0 k | a ∈ A} ⊆ Ioo 0 k

Tactic:
]

Goal state after:
case hab
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ {a ∈ Ioo 0 k | a ∈ A} ⊆ Ioo 0 k
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 𝒜)
⊢ p (image (insert a) (memberSubfamily a 𝒜))

Tactic:
]

Goal state after:
α : 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 𝒜)
⊢ p (image (insert a) (memberSubfamily a 𝒜))
Module: Mathlib.Combinatorics.Schnirelmann

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

Tactic:
]

Goal state after:
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
⊢ 1 ≤ schnirelmannDensity A ↔ {0}ᶜ ⊆ A
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case mp
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
⊢ ¬{0}ᶜ ⊆ A → schnirelmannDensity A < 1

Tactic:
]

Goal state after:
case mp
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
⊢ ¬{0}ᶜ ⊆ A → schnirelmannDensity A < 1
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

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

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
t : Finset α
ht : t ∈ 𝒜
hs : t.erase a ∉ 𝒜
⊢ t ∈ 𝒜
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case mpr
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
h : {0}ᶜ ⊆ A
x✝ : { n // 0 < n }
n : ℕ
hn : 0 < n
⊢ n ≤ ↑⟨n, hn⟩

pp: case mpr
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
h : {0}ᶜ ⊆ A
x✝ : { n // 0 < n }
n : ℕ
hn : 0 < n
⊢ ∀ x ∈ Ioc 0 ↑⟨n, hn⟩, x ∈ A

Tactic:
]

Goal state after:
case mpr
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
h : {0}ᶜ ⊆ A
x✝ : { n // 0 < n }
n : ℕ
hn : 0 < n
⊢ ∀ x ∈ Ioc 0 ↑⟨n, hn⟩, x ∈ A
Module: Mathlib.Combinatorics.Schnirelmann

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

Tactic:
]

Goal state after:
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
hA : 0 ∈ A
⊢ {0}ᶜ ⊆ A ↔ A = Set.univ
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

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

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : s ∈ 𝒜
h : s.erase a ∉ 𝒜
⊢ s ∈ 𝒜
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))
⊢ (fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹) 0 - (fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹) (n + 1) = 1

Tactic:
]

Goal state after:
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))
⊢ (fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹) 0 - (fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹) (n + 1) = 1
Module: Mathlib.Combinatorics.Schnirelmann

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

Tactic:
]

Goal state after:
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
x : ℝ
⊢ (¬∀ (n : ℕ), 0 < n → x ≤ ↑(#({a ∈ Ioc 0 n | a ∈ A})) / ↑n) ↔ ∃ n, 0 < n ∧ ↑(#({a ∈ Ioc 0 n | a ∈ A})) / ↑n < x
Module: Mathlib.Combinatorics.Schnirelmann

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

Tactic:
]

Goal state after:
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
x : ℝ
⊢ (∀ (ε : ℝ), 0 < ε → schnirelmannDensity A < x + ε) ↔
    ∀ (ε : ℝ), 0 < ε → ∃ n, 0 < n ∧ ↑(#({a ∈ Ioc 0 n | a ∈ A})) / ↑n < x + ε
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

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

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
h : s ∉ 𝒜 ∧ insert a s ∈ 𝒜
⊢ s ∉ 𝒜 ∧ insert a s ∈ 𝒜
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
⊢ ⨅ n, ↑(#({a ∈ Ioc 0 ↑n | a ∈ A})) / ↑↑n = ⨅ n, ↑(#({a ∈ Ioc 0 ↑n | a ∈ B})) / ↑↑n

Tactic:
]

Goal state after:
A : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
⊢ ⨅ n, ↑(#({a ∈ Ioc 0 ↑n | a ∈ A})) / ↑↑n = ⨅ n, ↑(#({a ∈ Ioc 0 ↑n | a ∈ B})) / ↑↑n
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

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

Tactic:
]

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
h : s ∈ 𝓓 a 𝒜
ha : a ∈ s
⊢ s ∈ 𝓓 a 𝒜
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))⁻¹
i : ℕ
h₁ : i < n + 1
⊢ f i - f (i + 1) = ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i))

Tactic:
]

Goal state after:
m n : ℕ
h : n < m
f : ℕ → ℚ := fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹
hf : f = fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹
i : ℕ
h₁ : i < n + 1
⊢ f i - f (i + 1) = ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i))
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
h : insert a s ∈ 𝓓 a 𝒜
ha : a ∉ s
⊢ (insert a s).erase a ∈ 𝓓 a 𝒜

Tactic:
]

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
h : insert a s ∈ 𝓓 a 𝒜
ha : a ∉ s
⊢ (insert a s).erase a ∈ 𝓓 a 𝒜
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
ε : ℝ
hε : 0 < ε
hA : schnirelmannDensity A = 0
h : ε ≤ schnirelmannDensity A
⊢ False

Tactic:
]

Goal state after:
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
ε : ℝ
hε : 0 < ε
hA : schnirelmannDensity A = 0
h : ε ≤ schnirelmannDensity A
⊢ False
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))⁻¹
i : ℕ
h₁✝ : i < n + 1
h₁ : i ≤ n
h₂ : i < m
h₃ : i ≤ m
hi₄ : ↑i + 1 ≠ 0
this : ↑(m.choose (i + 1)) * (↑i + 1) = ↑(m.choose i) * ↑(m - i)
⊢ ↑(n.choose i) * (↑(m.choose i))⁻¹ - ↑(n.choose (i + 1)) * (↑(m.choose i) * ↑(m - i) * (↑i + 1)⁻¹)⁻¹ =
    ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i))

Tactic:
]

Goal state after:
m n : ℕ
h : n < m
f : ℕ → ℚ := fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹
hf : f = fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹
i : ℕ
h₁✝ : i < n + 1
h₁ : i ≤ n
h₂ : i < m
h₃ : i ≤ m
hi₄ : ↑i + 1 ≠ 0
this : ↑(m.choose (i + 1)) * (↑i + 1) = ↑(m.choose i) * ↑(m - i)
⊢ ↑(n.choose i) * (↑(m.choose i))⁻¹ - ↑(n.choose (i + 1)) * (↑(m.choose i) * ↑(m - i) * (↑i + 1)⁻¹)⁻¹ =
    ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i))
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))⁻¹
i : ℕ
h₁✝ : i < n + 1
h₁ : i ≤ n
h₂ : i < m
h₃ : i ≤ m
hi₄ : ↑i + 1 ≠ 0
this✝ : ↑(m.choose (i + 1)) * (↑i + 1) = ↑(m.choose i) * ↑(m - i)
this : ↑(n.choose (i + 1)) * (↑i + 1) = ↑(n.choose i) * ↑(n - i)
⊢ ↑(n.choose i) * (↑(m.choose i))⁻¹ -
      ↑(n.choose i) * ↑(n - i) * (↑i + 1)⁻¹ * (↑(m.choose i) * ↑(m - i) * (↑i + 1)⁻¹)⁻¹ =
    ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i))

Tactic:
]

Goal state after:
m n : ℕ
h : n < m
f : ℕ → ℚ := fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹
hf : f = fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹
i : ℕ
h₁✝ : i < n + 1
h₁ : i ≤ n
h₂ : i < m
h₃ : i ≤ m
hi₄ : ↑i + 1 ≠ 0
this✝ : ↑(m.choose (i + 1)) * (↑i + 1) = ↑(m.choose i) * ↑(m - i)
this : ↑(n.choose (i + 1)) * (↑i + 1) = ↑(n.choose i) * ↑(n - i)
⊢ ↑(n.choose i) * (↑(m.choose i))⁻¹ -
      ↑(n.choose i) * ↑(n - i) * (↑i + 1)⁻¹ * (↑(m.choose i) * ↑(m - i) * (↑i + 1)⁻¹)⁻¹ =
    ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i))
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})) / ε < ↑⌊↑(#A) / ε⌋₊ + 1

Tactic:
]

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.Compression.Down

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

pp: α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ Disjoint ({s ∈ 𝒜 | s.erase a ∈ 𝒜}) ({a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜})

pp: α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ ∀ s ∈ ↑({a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜}), s ∈ {s | a ∈ s}

Tactic:
]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ #({s ∈ 𝒜 | s.erase a ∈ 𝒜} ∪ {a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜}) = #𝒜

α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ Disjoint ({s ∈ 𝒜 | s.erase a ∈ 𝒜}) ({a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜})

α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ ∀ s ∈ ↑({a_1 ∈ 𝒜 | a_1.erase a ∉ 𝒜}), s ∈ {s | a ∈ s}
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

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

Tactic:
]

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nonempty α
⊢ ∑ i ∈ range (#univ + 1), ∑ x ∈ powersetCard i univ, ↑(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✝¹ : Fintype α
inst✝ : Nonempty α
n : ℕ
s : Finset α
hs : s ∈ powersetCard n univ
⊢ ↑(card α) / ((↑(card α) - ↑n) * ↑((card α).choose n)) = ↑(card α) / ((↑(card α) - ↑n) * ↑((card α).choose n))

Tactic:
]

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

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
s : Finset α
hs : s ∈ 𝒜 ∧ s.erase a ∉ 𝒜
⊢ s ∈ {s | a ∈ s}
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ ↑(#({a ∈ Ioc 0 m | a ∈ {n | n % m = 1}})) / ↑m ≤ ↑1 / ↑m

Tactic:
]

Goal state after:
m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ ↑(#({a ∈ Ioc 0 m | a ∈ {n | n % m = 1}})) / ↑m ≤ ↑1 / ↑m
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case h.inr
m : ℕ
hm : m ≠ 1
hm' : m > 0
x : ℕ
a✝ : 0 < x
hxm : x ≤ m
h : x = 1
hxm' : x < m
⊢ x = 1

Tactic:
]

Goal state after:
case h.inr
m : ℕ
hm : m ≠ 1
hm' : m > 0
x : ℕ
a✝ : 0 < x
hxm : x ≤ m
h : x = 1
hxm' : x < m
⊢ x = 1
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ ∀ (n : ℕ), 0 < n → (↑m)⁻¹ ≤ ↑(#({a ∈ Ioc 0 n | a ∈ {n | n % m = 1}})) / ↑n

Tactic:
]

Goal state after:
m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ ∀ (n : ℕ), 0 < n → (↑m)⁻¹ ≤ ↑(#({a ∈ Ioc 0 n | a ∈ {n | n % m = 1}})) / ↑n
Module: Mathlib.Combinatorics.Schnirelmann

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

Tactic:
]

Goal state after:
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this : image (fun x ↦ x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ {x ∈ Ioc 0 n | x % m = 1}
⊢ ↑n / ↑m ≤ ↑(#({x ∈ Ioc 0 n | x % m = 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))
⊢ ↑(card α) * ∑ i ∈ range (card α + 1), ↑((card α).choose i) / ((↑(card α) - ↑i) * ↑((card α).choose i)) =
    ↑(card α) * ∑ x ∈ range (card α + 1), (↑x)⁻¹

Tactic:
]

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))
⊢ ↑(card α) * ∑ i ∈ range (card α + 1), ↑((card α).choose i) / ((↑(card α) - ↑i) * ↑((card α).choose i)) =
    ↑(card α) * ∑ x ∈ range (card α + 1), (↑x)⁻¹
Module: Mathlib.Combinatorics.Schnirelmann

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

pp: case H
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this : image (fun x ↦ x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ {x ∈ Ioc 0 n | x % m = 1}
⊢ Function.Injective fun x ↦ x * m + 1

Tactic:
]

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

case H
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this : image (fun x ↦ x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ {x ∈ Ioc 0 n | x % m = 1}
⊢ Function.Injective fun x ↦ x * m + 1
Module: Mathlib.Combinatorics.Schnirelmann

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

Tactic:
]

Goal state after:
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this✝ : image (fun x ↦ x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ {x ∈ Ioc 0 n | x % m = 1}
this : n ≤ n.pred / m * m + m
⊢ n ≤ (n - 1) / m * m + m
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))
n : ℕ
hn : n ∈ range (card α + 1)
⊢ (↑(card α) - ↑n)⁻¹ = (↑(card α) - ↑n)⁻¹

pp: case hb
α : 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))
n : ℕ
hn : n ∈ range (card α + 1)
⊢ ↑((card α).choose n) ≠ 0

Tactic:
]

Goal state after:
case hb
α : 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))
n : ℕ
hn : n ∈ range (card α + 1)
⊢ ↑((card α).choose n) ≠ 0
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case inr
m : ℕ
hm : m ≠ 1
⊢ schnirelmannDensity {n | n ≡ 1 [MOD m]} = schnirelmannDensity {n | n % m = 1}

Tactic:
]

Goal state after:
case inr
m : ℕ
hm : m ≠ 1
⊢ schnirelmannDensity {n | n ≡ 1 [MOD m]} = schnirelmannDensity {n | n % m = 1}
Module: Mathlib.Combinatorics.Schnirelmann

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

Tactic:
]

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
⊢ ∀ (x : ℕ), x ∈ A + B

Tactic:
]

Goal state after:
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
⊢ ∀ (x : ℕ), x ∈ A + B
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: case e'_1.e'_2.a
α : 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))
this : ∀ n ∈ range (card α + 1), ↑((card α).choose n) / ((↑(card α) - ↑n) * ↑((card α).choose n)) = (↑(card α) - ↑n)⁻¹
a : ℕ
ha : a ∈ range (card α + 1)
⊢ (↑(card α) - ↑a)⁻¹ = (↑(card α - a))⁻¹

Tactic:
cast_sub (mem_range_succ_iff.mp ha)

Goal state after:
case e'_1.e'_2.a
α : 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))
this : ∀ n ∈ range (card α + 1), ↑((card α).choose n) / ((↑(card α) - ↑n) * ↑((card α).choose n)) = (↑(card α) - ↑n)⁻¹
a : ℕ
ha : a ∈ range (card α + 1)
⊢ (↑(card α) - ↑a)⁻¹ = (↑(card α) - ↑a)⁻¹
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: case e'_1.e'_2.a
α : 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))
this : ∀ n ∈ range (card α + 1), ↑((card α).choose n) / ((↑(card α) - ↑n) * ↑((card α).choose n)) = (↑(card α) - ↑n)⁻¹
a : ℕ
ha : a ∈ range (card α + 1)
⊢ (↑(card α) - ↑a)⁻¹ = (↑(card α) - ↑a)⁻¹

Tactic:
]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : SemilatticeSup α
s t : Finset α
a : α
inst✝ : DecidableEq α
⊢ a ∈ lowerClosure ↑s ∨ a ∈ lowerClosure ↑t ↔ a ∈ lowerClosure ↑s ∨ a ∈ lowerClosure ↑t

Tactic:
]

Goal state after: