internlm/Lean-Github huggingface dataset:
Theorem: ProbabilityTheory.IsBernoulliSeq.inter
Proof state before:
case refine'_2.refine'_2
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
s : Finset α
i : α
hi : i ∈ s
⊢ MeasurableSet {ω | Y ω i}

case refine'_2
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
s : Finset α
⊢ ∀ i ∈ s, MeasurableSet {ω | Y ω i}

case refine'_2
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
s : Finset α
⊢ ∀ i ∈ s, MeasurableSet {ω | X ω i}

case refine'_2.hs
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
s : Finset α
⊢ MeasurableSet (⋂ i ∈ s, {ω | X ω i})

case refine'_2.ht
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
s : Finset α
⊢ MeasurableSet (⋂ i ∈ s, {ω | Y ω i})
Tactic:
sorry
Proof state after:
case refine'_2
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
s : Finset α
⊢ ∀ i ∈ s, MeasurableSet {ω | Y ω i}

case refine'_2
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
s : Finset α
⊢ ∀ i ∈ s, MeasurableSet {ω | X ω i}

case refine'_2.hs
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
s : Finset α
⊢ MeasurableSet (⋂ i ∈ s, {ω | X ω i})

case refine'_2.ht
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
s : Finset α
⊢ MeasurableSet (⋂ i ∈ s, {ω | Y ω i})
Theorem: ProbabilityTheory.IsBernoulliSeq.inter
Proof state before:
case refine'_2
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
s : Finset α
⊢ ∀ i ∈ s, MeasurableSet {ω | Y ω i}

case refine'_2
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
s : Finset α
⊢ ∀ i ∈ s, MeasurableSet {ω | X ω i}

case refine'_2.hs
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
s : Finset α
⊢ MeasurableSet (⋂ i ∈ s, {ω | X ω i})

case refine'_2.ht
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
s : Finset α
⊢ MeasurableSet (⋂ i ∈ s, {ω | Y ω i})
Tactic:
sorry
Proof state after:
case refine'_2
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
s : Finset α
⊢ ∀ i ∈ s, MeasurableSet {ω | X ω i}

case refine'_2.hs
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
s : Finset α
⊢ MeasurableSet (⋂ i ∈ s, {ω | X ω i})

case refine'_2.ht
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
s : Finset α
⊢ MeasurableSet (⋂ i ∈ s, {ω | Y ω i})
Theorem: ProbabilityTheory.IsBernoulliSeq.inter
Proof state before:
case refine'_2
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
s : Finset α
⊢ ∀ i ∈ s, MeasurableSet {ω | X ω i}

case refine'_2.hs
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
s : Finset α
⊢ MeasurableSet (⋂ i ∈ s, {ω | X ω i})

case refine'_2.ht
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
s : Finset α
⊢ MeasurableSet (⋂ i ∈ s, {ω | Y ω i})
Tactic:
sorry
Proof state after:
case refine'_2.hs
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
s : Finset α
⊢ MeasurableSet (⋂ i ∈ s, {ω | X ω i})

case refine'_2.ht
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
s : Finset α
⊢ MeasurableSet (⋂ i ∈ s, {ω | Y ω i})
Theorem: ProbabilityTheory.IsBernoulliSeq.inter
Proof state before:
case refine'_2.hs
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
s : Finset α
⊢ MeasurableSet (⋂ i ∈ s, {ω | X ω i})

case refine'_2.ht
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
s : Finset α
⊢ MeasurableSet (⋂ i ∈ s, {ω | Y ω i})
Tactic:
sorry
Proof state after:
case refine'_2.ht
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
s : Finset α
⊢ MeasurableSet (⋂ i ∈ s, {ω | Y ω i})
Theorem: ProbabilityTheory.IsBernoulliSeq.inter
Proof state before:
case refine'_2.ht
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
s : Finset α
⊢ MeasurableSet (⋂ i ∈ s, {ω | Y ω i})
Tactic:
sorry
Proof state after:
no goals
Theorem: ProbabilityTheory.IsBernoulliSeq.union
Proof state before:
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
⊢ IsBernoulliSeq (fun ω => X ω ∪ Y ω) (p + q - p * q) μ
Tactic:
convert (hX.compl.inter hY.compl _).compl using 1
Proof state after:
case h.e'_4
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
⊢ (fun ω => X ω ∪ Y ω) = fun ω => ((X ω)ᶜ ∩ (Y ω)ᶜ)ᶜ

case h.e'_5
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
⊢ p + q - p * q = 1 - (1 - p) * (1 - q)

α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
⊢ IndepFun (fun ω => (X ω)ᶜ) (fun ω => (Y ω)ᶜ) μ
Theorem: ProbabilityTheory.IsBernoulliSeq.union
Proof state before:
case h.e'_4
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
⊢ (fun ω => X ω ∪ Y ω) = fun ω => ((X ω)ᶜ ∩ (Y ω)ᶜ)ᶜ
Tactic:
simp [compl_inter]
Proof state after:
no goals
Theorem: ProbabilityTheory.IsBernoulliSeq.union
Proof state before:
case h.e'_5
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
⊢ p + q - p * q = 1 - (1 - p) * (1 - q)
Tactic:
rw [mul_tsub, mul_one, tsub_tsub, tsub_tsub_cancel_of_le, tsub_mul, one_mul,
  add_tsub_assoc_of_le (mul_le_of_le_one_left' $ hX.le_one)]
Proof state after:
case h.e'_5
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
⊢ p + (1 - p) * q ≤ 1
Theorem: ProbabilityTheory.IsBernoulliSeq.union
Proof state before:
case h.e'_5
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
⊢ p + (1 - p) * q ≤ 1
Tactic:
exact (add_le_add_left (mul_le_of_le_one_right' $ hY.le_one) _).trans_eq
  (add_tsub_cancel_of_le hX.le_one)
Proof state after:
no goals
Theorem: ProbabilityTheory.IsBernoulliSeq.union
Proof state before:
α : Type u_1
Ω : Type u_2
inst✝¹ : MeasurableSpace Ω
X Y : Ω → Set α
μ : Measure Ω
p q : ℝ≥0
hX : IsBernoulliSeq X p μ
hY : IsBernoulliSeq Y q μ
inst✝ : IsProbabilityMeasure μ
h : IndepFun X Y μ
⊢ IndepFun (fun ω => (X ω)ᶜ) (fun ω => (Y ω)ᶜ) μ
Tactic:
rwa [IndepFun_iff, MeasurableSpace.comap_compl measurable_compl,
  MeasurableSpace.comap_compl measurable_compl, ← IndepFun_iff]
Proof state after:
no goals
Theorem: one_le_schnirelmannDensity_iff
Proof state before:
A B : Set ℕ
n : ℕ
⊢ 1 ≤ schnirelmannDensity A ↔ {0}ᶜ ⊆ A
Tactic:
rw [schnirelmannDensity_le_one.ge_iff_eq, schnirelmannDensity_eq_one_iff]
Proof state after:
no goals
Theorem: one_le_schnirelmannDensity_iff_of_zero_mem
Proof state before:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
⊢ 1 ≤ schnirelmannDensity A ↔ A = Set.univ
Tactic:
rw [schnirelmannDensity_le_one.ge_iff_eq, schnirelmannDensity_eq_one_iff_of_zero_mem hA]
Proof state after:
no goals
Theorem: countelements_nonneg
Proof state before:
A✝ B : Set ℕ
n✝ : ℕ
A : Set ℕ
n : ℕ
⊢ 0 ≤ countelements A n
Tactic:
positivity
Proof state after:
no goals
Theorem: card_Icc_one_n_n
Proof state before:
A B : Set ℕ
n✝ n : ℕ
⊢ (Icc 1 n).card = n
Tactic:
rw [Nat.card_Icc 1 n, add_tsub_cancel_right]
Proof state after:
no goals
Theorem: countelements_le_n
Proof state before:
A✝ B : Set ℕ
n✝ : ℕ
A : Set ℕ
n : ℕ
⊢ countelements A n ≤ n
Tactic:
simpa [countelements] using card_filter_le (Icc 1 n) _
Proof state after:
no goals
Theorem: countelements_pred
Proof state before:
A B : Set ℕ
n : ℕ
hn : n ∉ A
⊢ countelements A (n - 1) = countelements A n
Tactic:
repeat rw [countelements]
Proof state after:
A B : Set ℕ
n : ℕ
hn : n ∉ A
⊢ (filter (fun x => x ∈ A) (Icc 1 (n - 1))).card = (filter (fun x => x ∈ A) (Icc 1 n)).card
Theorem: countelements_pred
Proof state before:
case refine_2
A B : Set ℕ
n : ℕ
hn : n ∉ A
⊢ (filter (fun x => x ∈ A) (Icc 1 n)).card ≤ (filter (fun x => x ∈ A) (Icc 1 (n - 1))).card
Tactic:
refine card_le_card fun x hx ↦ ?_
Proof state after:
case refine_2
A B : Set ℕ
n : ℕ
hn : n ∉ A
x : ℕ
hx : x ∈ filter (fun x => x ∈ A) (Icc 1 n)
⊢ x ∈ filter (fun x => x ∈ A) (Icc 1 (n - 1))
Theorem: countelements_pred
Proof state before:
case refine_2
A B : Set ℕ
n : ℕ
hn : n ∉ A
x : ℕ
hx : x ∈ filter (fun x => x ∈ A) (Icc 1 n)
⊢ x ∈ filter (fun x => x ∈ A) (Icc 1 (n - 1))
Tactic:
rw [mem_filter]
Proof state after:
case refine_2
A B : Set ℕ
n : ℕ
hn : n ∉ A
x : ℕ
hx : x ∈ filter (fun x => x ∈ A) (Icc 1 n)
⊢ x ∈ Icc 1 (n - 1) ∧ x ∈ A
Theorem: countelements_pred
Proof state before:
case refine_2
A B : Set ℕ
n : ℕ
hn : n ∉ A
x : ℕ
hx : x ∈ filter (fun x => x ∈ A) (Icc 1 n)
⊢ x ∈ Icc 1 (n - 1) ∧ x ∈ A
Tactic:
rw [mem_filter, mem_Icc] at hx
Proof state after:
case refine_2
A B : Set ℕ
n : ℕ
hn : n ∉ A
x : ℕ
hx : (1 ≤ x ∧ x ≤ n) ∧ x ∈ A
⊢ x ∈ Icc 1 (n - 1) ∧ x ∈ A
Theorem: countelements_pred
Proof state before:
case refine_2
A B : Set ℕ
n : ℕ
hn : n ∉ A
x : ℕ
hx : (1 ≤ x ∧ x ≤ n) ∧ x ∈ A
⊢ x ∈ Icc 1 (n - 1) ∧ x ∈ A
Tactic:
refine ⟨mem_Icc.2 ⟨hx.1.1, Nat.le_pred_of_lt $ hx.1.2.lt_of_ne ?_⟩, hx.2⟩
Proof state after:
case refine_2
A B : Set ℕ
n : ℕ
hn : n ∉ A
x : ℕ
hx : (1 ≤ x ∧ x ≤ n) ∧ x ∈ A
⊢ x ≠ n
Theorem: countelements_pred
Proof state before:
case refine_2
A B : Set ℕ
n : ℕ
hn : n ∉ A
x : ℕ
hx : (1 ≤ x ∧ x ≤ n) ∧ x ∈ A
⊢ x ≠ n
Tactic:
rintro rfl
Proof state after:
case refine_2
A B : Set ℕ
x : ℕ
hn : x ∉ A
hx : (1 ≤ x ∧ x ≤ x) ∧ x ∈ A
⊢ False
Theorem: countelements_pred
Proof state before:
case refine_2
A B : Set ℕ
x : ℕ
hn : x ∉ A
hx : (1 ≤ x ∧ x ≤ x) ∧ x ∈ A
⊢ False
Tactic:
exact hn hx.2
Proof state after:
no goals
Theorem: countelements_pred
Proof state before:
A B : Set ℕ
n : ℕ
hn : n ∉ A
⊢ (filter (fun x => x ∈ A) (Icc 1 (n - 1))).card = countelements A n
Tactic:
rw [countelements]
Proof state after:
A B : Set ℕ
n : ℕ
hn : n ∉ A
⊢ (filter (fun x => x ∈ A) (Icc 1 (n - 1))).card = (filter (fun x => x ∈ A) (Icc 1 n)).card
Theorem: countelements_pred
Proof state before:
case refine_1
A B : Set ℕ
n : ℕ
hn : n ∉ A
⊢ n - 1 ≤ n
Tactic:
simp only [tsub_le_iff_right, le_add_iff_nonneg_right, zero_le_one]
Proof state after:
no goals
Theorem: sumset_contains_n
Proof state before:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
⊢ n ∈ A + B
Tactic:
by_contra! h
Proof state after:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
h : n ∉ A + B
⊢ False
Theorem: sumset_contains_n
Proof state before:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
h : n ∉ A + B
⊢ False
Tactic:
have hnA : n ∉ A := Set.not_mem_subset (Set.subset_add_left _ hB) h
Proof state after:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
h : n ∉ A + B
hnA : n ∉ A
⊢ False
Theorem: sumset_contains_n
Proof state before:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
h : n ∉ A + B
hnA : n ∉ A
⊢ False
Tactic:
have hnB : n ∉ B := Set.not_mem_subset (Set.subset_add_right _ hA) h
Proof state after:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
h : n ∉ A + B
hnA : n ∉ A
hnB : n ∉ B
⊢ False
Theorem: sumset_contains_n
Proof state before:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
h : n ∉ A + B
hnA : n ∉ A
hnB : n ∉ B
⊢ False
Tactic:
have hca : countelements A (n - 1) = countelements A n := countelements_pred hnA
Proof state after:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
h : n ∉ A + B
hnA : n ∉ A
hnB : n ∉ B
hca : countelements A (n - 1) = countelements A n
⊢ False
Theorem: sumset_contains_n
Proof state before:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
h : n ∉ A + B
hnA : n ∉ A
hnB : n ∉ B
hca : countelements A (n - 1) = countelements A n
⊢ False
Tactic:
have hcb : countelements B (n - 1) = countelements B n := countelements_pred hnB
Proof state after:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
h : n ∉ A + B
hnA : n ∉ A
hnB : n ∉ B
hca : countelements A (n - 1) = countelements A n
hcb : countelements B (n - 1) = countelements B n
⊢ False
Theorem: sumset_contains_n
Proof state before:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
h : n ∉ A + B
hnA : n ∉ A
hnB : n ∉ B
hca : countelements A (n - 1) = countelements A n
hcb : countelements B (n - 1) = countelements B n
⊢ False
Tactic:
obtain rfl | hn1 := n.eq_zero_or_pos
Proof state after:
case inl
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : 0 ≤ countelements A 0 + countelements B 0
h : 0 ∉ A + B
hnA : 0 ∉ A
hnB : 0 ∉ B
hca : countelements A (0 - 1) = countelements A 0
hcb : countelements B (0 - 1) = countelements B 0
⊢ False

case inr
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
h : n ∉ A + B
hnA : n ∉ A
hnB : n ∉ B
hca : countelements A (n - 1) = countelements A n
hcb : countelements B (n - 1) = countelements B n
hn1 : n > 0
⊢ False
Theorem: sumset_contains_n
Proof state before:
case inr
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
h : n ∉ A + B
hnA : n ∉ A
hnB : n ∉ B
hca : countelements A (n - 1) = countelements A n
hcb : countelements B (n - 1) = countelements B n
hn1 : n > 0
⊢ False
Tactic:
apply h
Proof state after:
case inr
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
h : n ∉ A + B
hnA : n ∉ A
hnB : n ∉ B
hca : countelements A (n - 1) = countelements A n
hcb : countelements B (n - 1) = countelements B n
hn1 : n > 0
⊢ n ∈ A + B
Theorem: sumset_contains_n
Proof state before:
case inr
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
h : n ∉ A + B
hnA : n ∉ A
hnB : n ∉ B
hca : countelements A (n - 1) = countelements A n
hcb : countelements B (n - 1) = countelements B n
hn1 : n > 0
lem1 : (filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card = countelements B (n - 1)
lem3 : (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => x ∈ {n} - B) (Ioo 0 n)).Nonempty
⊢ n ∈ A + B
Tactic:
simp only [Nat.lt_one_iff, tsub_eq_zero_iff_le, mem_Ioo, and_imp, Set.singleton_sub,
  Set.mem_image, ne_eq] at lem3
Proof state after:
case inr
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
h : n ∉ A + B
hnA : n ∉ A
hnB : n ∉ B
hca : countelements A (n - 1) = countelements A n
hcb : countelements B (n - 1) = countelements B n
hn1 : n > 0
lem1 : (filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card = countelements B (n - 1)
lem3 : (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => ∃ x_1 ∈ B, n - x_1 = x) (Ioo 0 n)).Nonempty
⊢ n ∈ A + B
Theorem: sumset_contains_n
Proof state before:
case inr
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
h : n ∉ A + B
hnA : n ∉ A
hnB : n ∉ B
hca : countelements A (n - 1) = countelements A n
hcb : countelements B (n - 1) = countelements B n
hn1 : n > 0
lem1 : (filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card = countelements B (n - 1)
lem3 : (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => ∃ x_1 ∈ B, n - x_1 = x) (Ioo 0 n)).Nonempty
⊢ n ∈ A + B
Tactic:
have lem31 : (A ∩ ({n} - B) ∩ Set.Ioo 0 n).Nonempty := by
  rw [← filter_and, ← coe_nonempty, coe_filter, Set.setOf_and, Set.setOf_and, Set.setOf_mem_eq,
    Set.inter_comm] at lem3
  convert lem3 using 3 <;> ext <;> simp
Proof state after:
case inr
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
h : n ∉ A + B
hnA : n ∉ A
hnB : n ∉ B
hca : countelements A (n - 1) = countelements A n
hcb : countelements B (n - 1) = countelements B n
hn1 : n > 0
lem1 : (filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card = countelements B (n - 1)
lem3 : (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => ∃ x_1 ∈ B, n - x_1 = x) (Ioo 0 n)).Nonempty
lem31 : (A ∩ ({n} - B) ∩ Set.Ioo 0 n).Nonempty
⊢ n ∈ A + B
Theorem: sumset_contains_n
Proof state before:
case inr
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
h : n ∉ A + B
hnA : n ∉ A
hnB : n ∉ B
hca : countelements A (n - 1) = countelements A n
hcb : countelements B (n - 1) = countelements B n
hn1 : n > 0
lem1 : (filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card = countelements B (n - 1)
lem3 : (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => ∃ x_1 ∈ B, n - x_1 = x) (Ioo 0 n)).Nonempty
lem31 : (A ∩ ({n} - B) ∩ Set.Ioo 0 n).Nonempty
⊢ n ∈ A + B
Tactic:
obtain ⟨_, ⟨hxA, n, rfl, x, hxB, rfl⟩, hx⟩ := lem31
Proof state after:
case inr.intro.intro.intro.intro.intro.intro.intro
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
n : ℕ
hc : n ≤ countelements A n + countelements B n
h : n ∉ A + B
hnA : n ∉ A
hnB : n ∉ B
hca : countelements A (n - 1) = countelements A n
hcb : countelements B (n - 1) = countelements B n
hn1 : n > 0
lem1 : (filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card = countelements B (n - 1)
lem3 : (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => ∃ x_1 ∈ B, n - x_1 = x) (Ioo 0 n)).Nonempty
x : ℕ
hxB : x ∈ B
hxA : (fun x x_1 => x - x_1) n x ∈ A
hx : (fun x x_1 => x - x_1) n x ∈ Set.Ioo 0 n
⊢ n ∈ A + B
Theorem: sumset_contains_n
Proof state before:
case inr.intro.intro.intro.intro.intro.intro.intro
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
n : ℕ
hc : n ≤ countelements A n + countelements B n
h : n ∉ A + B
hnA : n ∉ A
hnB : n ∉ B
hca : countelements A (n - 1) = countelements A n
hcb : countelements B (n - 1) = countelements B n
hn1 : n > 0
lem1 : (filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card = countelements B (n - 1)
lem3 : (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => ∃ x_1 ∈ B, n - x_1 = x) (Ioo 0 n)).Nonempty
x : ℕ
hxB : x ∈ B
hxA : (fun x x_1 => x - x_1) n x ∈ A
hx : (fun x x_1 => x - x_1) n x ∈ Set.Ioo 0 n
⊢ n ∈ A + B
Tactic:
simp only [Set.mem_Ioo, Nat.succ_le_iff, tsub_pos_iff_lt, tsub_le_iff_right] at hx
Proof state after:
case inr.intro.intro.intro.intro.intro.intro.intro
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
n : ℕ
hc : n ≤ countelements A n + countelements B n
h : n ∉ A + B
hnA : n ∉ A
hnB : n ∉ B
hca : countelements A (n - 1) = countelements A n
hcb : countelements B (n - 1) = countelements B n
hn1 : n > 0
lem1 : (filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card = countelements B (n - 1)
lem3 : (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => ∃ x_1 ∈ B, n - x_1 = x) (Ioo 0 n)).Nonempty
x : ℕ
hxB : x ∈ B
hxA : (fun x x_1 => x - x_1) n x ∈ A
hx : x < n ∧ n - x < n
⊢ n ∈ A + B
Theorem: sumset_contains_n
Proof state before:
case inr.intro.intro.intro.intro.intro.intro.intro
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
n : ℕ
hc : n ≤ countelements A n + countelements B n
h : n ∉ A + B
hnA : n ∉ A
hnB : n ∉ B
hca : countelements A (n - 1) = countelements A n
hcb : countelements B (n - 1) = countelements B n
hn1 : n > 0
lem1 : (filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card = countelements B (n - 1)
lem3 : (filter (fun x => x ∈ A) (Ioo 0 n) ∩ filter (fun x => ∃ x_1 ∈ B, n - x_1 = x) (Ioo 0 n)).Nonempty
x : ℕ
hxB : x ∈ B
hxA : (fun x x_1 => x - x_1) n x ∈ A
hx : x < n ∧ n - x < n
⊢ n ∈ A + B
Tactic:
exact ⟨_, hxA, x, hxB, tsub_add_cancel_of_le hx.1.le⟩
Proof state after:
no goals
Theorem: sumset_contains_n
Proof state before:
case inl
A B : Set ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : 0 ≤ countelements A 0 + countelements B 0
h : 0 ∉ A + B
hnA : 0 ∉ A
hnB : 0 ∉ B
hca : countelements A (0 - 1) = countelements A 0
hcb : countelements B (0 - 1) = countelements B 0
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: sumset_contains_n
Proof state before:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
h : n ∉ A + B
hnA : n ∉ A
hnB : n ∉ B
hca : countelements A (n - 1) = countelements A n
hcb : countelements B (n - 1) = countelements B n
hn1 : n > 0
⊢ (filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card = countelements B (n - 1)
Tactic:
rw [countelements]
Proof state after:
A B : Set ℕ
n : ℕ
hA : 0 ∈ A
hB : 0 ∈ B
hc : n ≤ countelements A n + countelements B n
h : n ∉ A + B
hnA : n ∉ A
hnB : n ∉ B
hca : countelements A (n - 1) = countelements A n
hcb : countelements B (n - 1) = countelements B n
hn1 : n > 0
⊢ (filter (fun x => x ∈ {n} - B) (Ioo 0 n)).card = (filter (fun x => x ∈ B) (Icc 1 (n - 1))).card