awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A B : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun (x : ℕ ⊕ ℕ) ↦
    match (motive := ℕ ⊕ ℕ → ℕ) x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
a : ℕ
ha : Sum.inl a ∈ sA.disjSum sB
b : ℕ
hb : Sum.inr b ∈ sA.disjSum sB
left : Sum.inl a ≠ Sum.inr b
hxy : f (Sum.inl a) = f (Sum.inr b)
⊢ (0 < a ∧ a ≤ n) ∧ a ∈ A

Tactic:
simp only [sA, sB, inl_mem_disjSum, mem_filter, mem_Ioc, inr_mem_disjSum] at ha hb

Premises used: Finset.inr_mem_disjSum, Finset.inl_mem_disjSum, Finset.mem_filter, Finset.mem_Ioc
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A B : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun (x : ℕ ⊕ ℕ) ↦
    match (motive := ℕ ⊕ ℕ → ℕ) x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
a : ℕ
ha : Sum.inl a ∈ sA.disjSum sB
b : ℕ
hb : Sum.inr b ∈ sA.disjSum sB
left : Sum.inl a ≠ Sum.inr b
hxy : f (Sum.inl a) = f (Sum.inr b)
ha₁ : (0 < a ∧ a ≤ n) ∧ a ∈ A
⊢ (0 < b ∧ b ≤ n) ∧ b ∈ B

Tactic:
simp only [sA, sB, inl_mem_disjSum, mem_filter, mem_Ioc, inr_mem_disjSum] at ha hb

Premises used: Finset.inr_mem_disjSum, Finset.inl_mem_disjSum, Finset.mem_filter, Finset.mem_Ioc
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A B : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun (x : ℕ ⊕ ℕ) ↦
    match (motive := ℕ ⊕ ℕ → ℕ) x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
b : ℕ
ha : Sum.inr b ∈ sA.disjSum sB
a : ℕ
hb : Sum.inl a ∈ sA.disjSum sB
left : Sum.inr b ≠ Sum.inl a
hxy : f (Sum.inr b) = f (Sum.inl a)
⊢ (0 < b ∧ b ≤ n) ∧ b ∈ B

Tactic:
simp only [sA, sB, inl_mem_disjSum, mem_filter, mem_Ioc, inr_mem_disjSum] at ha hb

Premises used: Finset.inr_mem_disjSum, Finset.inl_mem_disjSum, Finset.mem_filter, Finset.mem_Ioc
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A B : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun (x : ℕ ⊕ ℕ) ↦
    match (motive := ℕ ⊕ ℕ → ℕ) x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
b : ℕ
ha : Sum.inr b ∈ sA.disjSum sB
a : ℕ
hb : Sum.inl a ∈ sA.disjSum sB
left : Sum.inr b ≠ Sum.inl a
hxy : f (Sum.inr b) = f (Sum.inl a)
ha₁ : (0 < b ∧ b ≤ n) ∧ b ∈ B
⊢ (0 < a ∧ a ≤ n) ∧ a ∈ A

Tactic:
simp only [sA, sB, inl_mem_disjSum, mem_filter, mem_Ioc, inr_mem_disjSum] at ha hb

Premises used: Finset.inr_mem_disjSum, Finset.inl_mem_disjSum, Finset.mem_filter, Finset.mem_Ioc
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A B : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun (x : ℕ ⊕ ℕ) ↦
    match (motive := ℕ ⊕ ℕ → ℕ) x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
b_1 : ℕ
ha : Sum.inr b_1 ∈ sA.disjSum sB
b : ℕ
hb : Sum.inr b ∈ sA.disjSum sB
left : Ne (α := ℕ ⊕ ℕ) (Sum.inr b_1) (Sum.inr b)
hxy : f (Sum.inr b_1) = f (Sum.inr b)
⊢ (0 < b_1 ∧ b_1 ≤ n) ∧ b_1 ∈ B

Tactic:
simp only [sA, sB, inl_mem_disjSum, mem_filter, mem_Ioc, inr_mem_disjSum] at ha hb

Premises used: Finset.inr_mem_disjSum, Finset.inl_mem_disjSum, Finset.mem_filter, Finset.mem_Ioc
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A B : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun (x : ℕ ⊕ ℕ) ↦
    match (motive := ℕ ⊕ ℕ → ℕ) x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
b_1 : ℕ
ha : Sum.inr b_1 ∈ sA.disjSum sB
b : ℕ
hb : Sum.inr b ∈ sA.disjSum sB
left : Ne (α := ℕ ⊕ ℕ) (Sum.inr b_1) (Sum.inr b)
hxy : f (Sum.inr b_1) = f (Sum.inr b)
ha₁ : (0 < b_1 ∧ b_1 ≤ n) ∧ b_1 ∈ B
⊢ (0 < b ∧ b ≤ n) ∧ b ∈ B

Tactic:
simp only [sA, sB, inl_mem_disjSum, mem_filter, mem_Ioc, inr_mem_disjSum] at ha hb

Premises used: Finset.inr_mem_disjSum, Finset.inl_mem_disjSum, Finset.mem_filter, Finset.mem_Ioc
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A B : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun (x : ℕ ⊕ ℕ) ↦
    match (motive := ℕ ⊕ ℕ → ℕ) x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
a_1 a : ℕ
left : Ne (α := ℕ ⊕ ℕ) (Sum.inl a_1) (Sum.inl a)
hxy : f (Sum.inl a_1) = f (Sum.inl a)
ha : (0 < a_1 ∧ a_1 ≤ n) ∧ a_1 ∈ A
hb : (0 < a ∧ a ≤ n) ∧ a ∈ A
⊢ n ∈ A + B

Tactic:
grind [inr_mem_disjSum]

Premises used: Finset.inr_mem_disjSum
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A B : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun (x : ℕ ⊕ ℕ) ↦
    match (motive := ℕ ⊕ ℕ → ℕ) x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
a_1 a : ℕ
left : Ne (α := ℕ ⊕ ℕ) (Sum.inl a_1) (Sum.inl a)
hxy : f (Sum.inl a_1) = f (Sum.inl a)
ha : (0 < a_1 ∧ a_1 ≤ n) ∧ a_1 ∈ A
hb : (0 < a ∧ a ≤ n) ∧ a ∈ A
⊢ n ∈ A + B

Tactic:
first | grind [inr_mem_disjSum] | exact ⟨a, by simp [*], b, by simp [*], by grind⟩

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

Tactic:
grind [inr_mem_disjSum]

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

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A B : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun (x : ℕ ⊕ ℕ) ↦
    match (motive := ℕ ⊕ ℕ → ℕ) x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
a b : ℕ
left : Sum.inl a ≠ Sum.inr b
hxy : f (Sum.inl a) = f (Sum.inr b)
ha : (0 < a ∧ a ≤ n) ∧ a ∈ A
hb : (0 < b ∧ b ≤ n) ∧ b ∈ B
⊢ b ∈ B

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A B : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun (x : ℕ ⊕ ℕ) ↦
    match (motive := ℕ ⊕ ℕ → ℕ) x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
a b : ℕ
left : Sum.inl a ≠ Sum.inr b
hxy : f (Sum.inl a) = f (Sum.inr b)
ha : (0 < a ∧ a ≤ n) ∧ a ∈ A
hb : (0 < b ∧ b ≤ n) ∧ b ∈ B
⊢ (fun (x1 x2 : ℕ) ↦ x1 + x2) a b = n

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

Tactic:
exact ⟨a, by simp [*], b, by simp [*], by grind⟩
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A B : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun (x : ℕ ⊕ ℕ) ↦
    match (motive := ℕ ⊕ ℕ → ℕ) x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
a b : ℕ
left : Sum.inl a ≠ Sum.inr b
hxy : f (Sum.inl a) = f (Sum.inr b)
ha : (0 < a ∧ a ≤ n) ∧ a ∈ A
hb : (0 < b ∧ b ≤ n) ∧ b ∈ B
⊢ n ∈ A + B

Tactic:
first | grind [inr_mem_disjSum] | exact ⟨a, by simp [*], b, by simp [*], by grind⟩

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

Tactic:
grind [inr_mem_disjSum]

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

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A B : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun (x : ℕ ⊕ ℕ) ↦
    match (motive := ℕ ⊕ ℕ → ℕ) x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
b a : ℕ
left : Sum.inr b ≠ Sum.inl a
hxy : f (Sum.inr b) = f (Sum.inl a)
ha : (0 < b ∧ b ≤ n) ∧ b ∈ B
hb : (0 < a ∧ a ≤ n) ∧ a ∈ A
⊢ b ∈ B

Tactic:
simp [*]
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A B : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun (x : ℕ ⊕ ℕ) ↦
    match (motive := ℕ ⊕ ℕ → ℕ) x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
b a : ℕ
left : Sum.inr b ≠ Sum.inl a
hxy : f (Sum.inr b) = f (Sum.inl a)
ha : (0 < b ∧ b ≤ n) ∧ b ∈ B
hb : (0 < a ∧ a ≤ n) ∧ a ∈ A
⊢ (fun (x1 x2 : ℕ) ↦ x1 + x2) a b = n

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

Tactic:
exact ⟨a, by simp [*], b, by simp [*], by grind⟩
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A B : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun (x : ℕ ⊕ ℕ) ↦
    match (motive := ℕ ⊕ ℕ → ℕ) x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
b a : ℕ
left : Sum.inr b ≠ Sum.inl a
hxy : f (Sum.inr b) = f (Sum.inl a)
ha : (0 < b ∧ b ≤ n) ∧ b ∈ B
hb : (0 < a ∧ a ≤ n) ∧ a ∈ A
⊢ n ∈ A + B

Tactic:
first | grind [inr_mem_disjSum] | exact ⟨a, by simp [*], b, by simp [*], by grind⟩

Premises used: Finset.inr_mem_disjSum
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A B : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun (x : ℕ ⊕ ℕ) ↦
    match (motive := ℕ ⊕ ℕ → ℕ) x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
b_1 b : ℕ
left : Ne (α := ℕ ⊕ ℕ) (Sum.inr b_1) (Sum.inr b)
hxy : f (Sum.inr b_1) = f (Sum.inr b)
ha : (0 < b_1 ∧ b_1 ≤ n) ∧ b_1 ∈ B
hb : (0 < b ∧ b ≤ n) ∧ b ∈ B
⊢ n ∈ A + B

Tactic:
grind [inr_mem_disjSum]

Premises used: Finset.inr_mem_disjSum
-- Module: Mathlib.Combinatorics.Schnirelmann
Goal:
A B : Set ℕ
inst : DecidablePred fun (x : ℕ) ↦ x ∈ A
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun (x : ℕ ⊕ ℕ) ↦
    match (motive := ℕ ⊕ ℕ → ℕ) x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
b_1 b : ℕ
left : Ne (α := ℕ ⊕ ℕ) (Sum.inr b_1) (Sum.inr b)
hxy : f (Sum.inr b_1) = f (Sum.inr b)
ha : (0 < b_1 ∧ b_1 ≤ n) ∧ b_1 ∈ B
hb : (0 < b ∧ b ≤ n) ∧ b ∈ B
⊢ n ∈ A + B

Tactic:
first | grind [inr_mem_disjSum] | exact ⟨a, by simp [*], b, by simp [*], by grind⟩

Premises used: Finset.inr_mem_disjSum
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
m n : ℕ
h : n < m
⊢ let f : ℕ → ℚ := fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹;
  f = fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹

Tactic:
set f : ℕ → ℚ := fun i ↦ n.choose i * (m.choose i : ℚ)⁻¹ with hf

Premises used: Nat.choose, HMul.hMul, Nat.cast, Inv.inv
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
m n : ℕ
h : n < m
f : ℕ → ℚ := fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹
hf : f = fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹
this :
  ∀ i ∈ range (n + 1),
    f i - f (i + 1) =
      (↑(n.choose i) : ℚ) * HSub.hSub (α := ℚ) (↑m : ℚ) (↑n : ℚ) /
        (HSub.hSub (α := ℚ) (↑m : ℚ) (↑i : ℚ) * (↑(m.choose i) : ℚ))
rw :
  HSub.hSub (α := ℚ) ((fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹) 0)
      ((fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹) (n + 1)) =
    1
⊢ Eq (α := ℚ)
    (∑ i ∈ range (n + 1),
      (↑(n.choose i) : ℚ) * HSub.hSub (α := ℚ) (↑m : ℚ) (↑n : ℚ) /
        (HSub.hSub (α := ℚ) (↑m : ℚ) (↑i : ℚ) * (↑(m.choose i) : ℚ)))
    1

Tactic:
rw [← sum_congr rfl this, sum_range_sub', hf]

Premises used: Finset.sum_congr, rfl, Finset.sum_range_sub'
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
m n : ℕ
h : n < m
f : ℕ → ℚ := fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹
hf : f = fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹
this :
  ∀ i ∈ range (n + 1),
    f i - f (i + 1) =
      (↑(n.choose i) : ℚ) * HSub.hSub (α := ℚ) (↑m : ℚ) (↑n : ℚ) /
        (HSub.hSub (α := ℚ) (↑m : ℚ) (↑i : ℚ) * (↑(m.choose i) : ℚ))
⊢ HSub.hSub (α := ℚ) ((fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹) 0)
      ((fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹) (n + 1)) =
    1

Tactic:
simp [choose_zero_right]

Premises used: Nat.choose_zero_right
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
m n : ℕ
h : n < m
f : ℕ → ℚ := fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹
hf : f = fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹
suffices :
  ∀ i ∈ range (n + 1),
    f i - f (i + 1) =
      (↑(n.choose i) : ℚ) * HSub.hSub (α := ℚ) (↑m : ℚ) (↑n : ℚ) /
        (HSub.hSub (α := ℚ) (↑m : ℚ) (↑i : ℚ) * (↑(m.choose i) : ℚ))
⊢ Eq (α := ℚ)
    (∑ i ∈ range (n + 1),
      (↑(n.choose i) : ℚ) * HSub.hSub (α := ℚ) (↑m : ℚ) (↑n : ℚ) /
        (HSub.hSub (α := ℚ) (↑m : ℚ) (↑i : ℚ) * (↑(m.choose i) : ℚ)))
    1

Tactic:
suffices ∀ i ∈ range (n + 1), f i - f (i + 1) = n.choose i * (m - n) / ((m - i) * m.choose i) by
    rw [← sum_congr rfl this, sum_range_sub', hf]
    simp [choose_zero_right]
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
m n : ℕ
h : n < m
f : ℕ → ℚ := fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹
hf : f = fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹
i : ℕ
h₁ : i ∈ range (n + 1)
⊢ i < n + 1

Tactic:
rw [mem_range] at h₁

Premises used: Finset.mem_range
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
m n : ℕ
h : n < m
f : ℕ → ℚ := fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹
hf : f = fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹
i : ℕ
h₁ : i < n + 1
⊢ i ≤ n

Tactic:
have h₁ := le_of_lt_succ h₁
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
m n : ℕ
h : n < m
f : ℕ → ℚ := fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹
hf : f = fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹
i : ℕ
h₁_1 : i < n + 1
h₁ : i ≤ n
⊢ i < m

Tactic:
have h₂ := h₁.trans_lt h
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
m n : ℕ
h : n < m
f : ℕ → ℚ := fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹
hf : f = fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹
i : ℕ
h₁_1 : i < n + 1
h₁ : i ≤ n
h₂ : i < m
⊢ i ≤ m

Tactic:
have h₃ := h₂.le
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
m n : ℕ
h : n < m
f : ℕ → ℚ := fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹
hf : f = fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹
i : ℕ
h₁_1 : i < n + 1
h₁ : i ≤ n
h₂ : i < m
h₃ : i ≤ m
⊢ HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 ≠ 0

Tactic:
have hi₄ : (i + 1 : ℚ) ≠ 0 := i.cast_add_one_ne_zero
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
m n : ℕ
h : n < m
f : ℕ → ℚ := fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹
hf : f = fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹
i : ℕ
h₁_1 : i < n + 1
h₁ : i ≤ n
h₂ : i < m
h₃ : i ≤ m
hi₄ : HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 ≠ 0
⊢ Eq (α := ℚ) (↑(m.choose (i + 1) * (i + 1)) : ℚ) (↑(m.choose i * (m - i)) : ℚ)

Tactic:
have := congr_arg ((↑) : ℕ → ℚ) (choose_succ_right_eq m i)
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
m n : ℕ
h : n < m
f : ℕ → ℚ := fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹
hf : f = fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹
i : ℕ
h₁_1 : i < n + 1
h₁ : i ≤ n
h₂ : i < m
h₃ : i ≤ m
hi₄ : HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 ≠ 0
this : Eq (α := ℚ) (↑(m.choose (i + 1) * (i + 1)) : ℚ) (↑(m.choose i * (m - i)) : ℚ)
⊢ (↑(m.choose (i + 1)) : ℚ) * HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 = HMul.hMul (α := ℚ) (↑(m.choose i) : ℚ) (↑(m - i) : ℚ)

Tactic:
push_cast at this
-- Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Goal:
m n : ℕ
h : n < m
f : ℕ → ℚ := fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹
hf : f = fun (i : ℕ) ↦ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹
i : ℕ
h₁_1 : i < n + 1
h₁ : i ≤ n
h₂ : i < m
h₃ : i ≤ m
hi₄ : HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 ≠ 0
this : (↑(m.choose (i + 1)) : ℚ) * HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 = HMul.hMul (α := ℚ) (↑(m.choose i) : ℚ) (↑(m - i) : ℚ)
dsimp :
  HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹ -
      HMul.hMul (α := ℚ) (↑(n.choose (i + 1)) : ℚ) (↑(m.choose (i + 1)) : ℚ)⁻¹ =
    (↑(n.choose i) : ℚ) * HSub.hSub (α := ℚ) (↑m : ℚ) (↑n : ℚ) /
      (HSub.hSub (α := ℚ) (↑m : ℚ) (↑i : ℚ) * (↑(m.choose i) : ℚ))
⊢ f i - f (i + 1) =
    (↑(n.choose i) : ℚ) * HSub.hSub (α := ℚ) (↑m : ℚ) (↑n : ℚ) /
      (HSub.hSub (α := ℚ) (↑m : ℚ) (↑i : ℚ) * (↑(m.choose i) : ℚ))

Tactic:
dsimp [f, hf]