awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
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)
neg :
  ∀ (a : ℕ) (ha : Sum.inl a ∈ sA.disjSum sB) (a_1 : ℕ) (hb : Sum.inl a_1 ∈ sA.disjSum sB),
    Ne (α := ℕ ⊕ ℕ) (Sum.inl a) (Sum.inl a_1) → ∀ (hxy : f (Sum.inl a) = f (Sum.inl a_1)), n ∈ A + B
⊢ n ∈ A + B
have neg₁ : ∀ (a : ℕ) (ha : Sum.inl a ∈ sA.disjSum sB) (b : ℕ) (hb : Sum.inr b ∈ sA.disjSum sB),
  Sum.inl a ≠ Sum.inr b → ∀ (hxy : f (Sum.inl a) = f (Sum.inr b)), n ∈ A + B
Tactic: obtain ⟨a | b, ha, a | b, hb, _, hxy⟩ := exists_ne_map_eq_of_card_image_lt hc
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
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)
neg :
  ∀ (a : ℕ) (ha : Sum.inl a ∈ sA.disjSum sB) (a_1 : ℕ) (hb : Sum.inl a_1 ∈ sA.disjSum sB),
    Ne (α := ℕ ⊕ ℕ) (Sum.inl a) (Sum.inl a_1) → ∀ (hxy : f (Sum.inl a) = f (Sum.inl a_1)), n ∈ A + B
neg₁ :
  ∀ (a : ℕ) (ha : Sum.inl a ∈ sA.disjSum sB) (b : ℕ) (hb : Sum.inr b ∈ sA.disjSum sB),
    Sum.inl a ≠ Sum.inr b → ∀ (hxy : f (Sum.inl a) = f (Sum.inr b)), n ∈ A + B
⊢ n ∈ A + B
have neg₂ : ∀ (b : ℕ) (ha : Sum.inr b ∈ sA.disjSum sB) (a : ℕ) (hb : Sum.inl a ∈ sA.disjSum sB),
  Sum.inr b ≠ Sum.inl a → ∀ (hxy : f (Sum.inr b) = f (Sum.inl a)), n ∈ A + B
Tactic: obtain ⟨a | b, ha, a | b, hb, _, hxy⟩ := exists_ne_map_eq_of_card_image_lt hc
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (goal)
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)
neg :
  ∀ (a : ℕ) (ha : Sum.inl a ∈ sA.disjSum sB) (a_1 : ℕ) (hb : Sum.inl a_1 ∈ sA.disjSum sB),
    Ne (α := ℕ ⊕ ℕ) (Sum.inl a) (Sum.inl a_1) → ∀ (hxy : f (Sum.inl a) = f (Sum.inl a_1)), n ∈ A + B
neg₁ :
  ∀ (a : ℕ) (ha : Sum.inl a ∈ sA.disjSum sB) (b : ℕ) (hb : Sum.inr b ∈ sA.disjSum sB),
    Sum.inl a ≠ Sum.inr b → ∀ (hxy : f (Sum.inl a) = f (Sum.inr b)), n ∈ A + B
neg₂ :
  ∀ (b : ℕ) (ha : Sum.inr b ∈ sA.disjSum sB) (a : ℕ) (hb : Sum.inl a ∈ sA.disjSum sB),
    Sum.inr b ≠ Sum.inl a → ∀ (hxy : f (Sum.inr b) = f (Sum.inl a)), n ∈ A + B
⊢ n ∈ A + B
have neg₃ : ∀ (b : ℕ) (ha : Sum.inr b ∈ sA.disjSum sB) (b_1 : ℕ) (hb : Sum.inr b_1 ∈ sA.disjSum sB),
  Ne (α := ℕ ⊕ ℕ) (Sum.inr b) (Sum.inr b_1) → ∀ (hxy : f (Sum.inr b) = f (Sum.inr b_1)), n ∈ A + B
Tactic: obtain ⟨a | b, ha, a | b, hb, _, hxy⟩ := exists_ne_map_eq_of_card_image_lt hc
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (hypothesis)
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 : ℕ
ha : Sum.inl a_1 ∈ sA.disjSum sB
a : ℕ
hb : Sum.inl a ∈ sA.disjSum sB
left : Ne (α := ℕ ⊕ ℕ) (Sum.inl a_1) (Sum.inl a)
hxy : f (Sum.inl a_1) = f (Sum.inl a)
⊢ n ∈ A + B
have ha₁ : (0 < a_1 ∧ a_1 ≤ n) ∧ a_1 ∈ A
Tactic: simp only [sA, sB, inl_mem_disjSum, mem_filter, mem_Ioc, inr_mem_disjSum] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (hypothesis)
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 : ℕ
ha : Sum.inl a_1 ∈ sA.disjSum sB
a : ℕ
hb : Sum.inl a ∈ sA.disjSum sB
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
⊢ n ∈ A + B
have hb₁ : (0 < a ∧ a ≤ n) ∧ a ∈ A
Tactic: simp only [sA, sB, inl_mem_disjSum, mem_filter, mem_Ioc, inr_mem_disjSum] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (hypothesis)
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)
⊢ n ∈ A + B
have ha₁ : (0 < a ∧ a ≤ n) ∧ a ∈ A
Tactic: simp only [sA, sB, inl_mem_disjSum, mem_filter, mem_Ioc, inr_mem_disjSum] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (hypothesis)
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
⊢ n ∈ A + B
have hb₁ : (0 < b ∧ b ≤ n) ∧ b ∈ B
Tactic: simp only [sA, sB, inl_mem_disjSum, mem_filter, mem_Ioc, inr_mem_disjSum] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (hypothesis)
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)
⊢ n ∈ A + B
have ha₁ : (0 < b ∧ b ≤ n) ∧ b ∈ B
Tactic: simp only [sA, sB, inl_mem_disjSum, mem_filter, mem_Ioc, inr_mem_disjSum] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (hypothesis)
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
⊢ n ∈ A + B
have hb₁ : (0 < a ∧ a ≤ n) ∧ a ∈ A
Tactic: simp only [sA, sB, inl_mem_disjSum, mem_filter, mem_Ioc, inr_mem_disjSum] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (hypothesis)
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)
⊢ n ∈ A + B
have ha₁ : (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
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Combinatorics.Schnirelmann (hypothesis)
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
⊢ n ∈ A + B
have hb₁ : (0 < b ∧ b ≤ n) ∧ b ∈ B
Tactic: simp only [sA, sB, inl_mem_disjSum, mem_filter, mem_Ioc, inr_mem_disjSum] at ha hb
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (hypothesis)
Goal:
m n : ℕ
h : n < m
⊢ Eq (α := ℚ)
    (∑ i ∈ range (n + 1),
      (↑(n.choose i) : ℚ) * HSub.hSub (α := ℚ) (↑m : ℚ) (↑n : ℚ) /
        (HSub.hSub (α := ℚ) (↑m : ℚ) (↑i : ℚ) * (↑(m.choose i) : ℚ)))
    1
have hf : 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
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
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) : ℚ))
⊢ Eq (α := ℚ)
    (∑ i ∈ range (n + 1),
      (↑(n.choose i) : ℚ) * HSub.hSub (α := ℚ) (↑m : ℚ) (↑n : ℚ) /
        (HSub.hSub (α := ℚ) (↑m : ℚ) (↑i : ℚ) * (↑(m.choose i) : ℚ)))
    1
have 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
Tactic: rw [← sum_congr rfl this, sum_range_sub', hf]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
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) : ℚ)⁻¹
⊢ Eq (α := ℚ)
    (∑ i ∈ range (n + 1),
      (↑(n.choose i) : ℚ) * HSub.hSub (α := ℚ) (↑m : ℚ) (↑n : ℚ) /
        (HSub.hSub (α := ℚ) (↑m : ℚ) (↑i : ℚ) * (↑(m.choose i) : ℚ)))
    1
have suffices : ∀ i ∈ range (n + 1),
  f i - f (i + 1) =
    (↑(n.choose i) : ℚ) * HSub.hSub (α := ℚ) (↑m : ℚ) (↑n : ℚ) /
      (HSub.hSub (α := ℚ) (↑m : ℚ) (↑i : ℚ) * (↑(m.choose i) : ℚ))
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]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (hypothesis)
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)
⊢ f i - f (i + 1) =
    (↑(n.choose i) : ℚ) * HSub.hSub (α := ℚ) (↑m : ℚ) (↑n : ℚ) /
      (HSub.hSub (α := ℚ) (↑m : ℚ) (↑i : ℚ) * (↑(m.choose i) : ℚ))
have h₂ : i < n + 1
Tactic: rw [mem_range] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (hypothesis)
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
⊢ f i - f (i + 1) =
    (↑(n.choose i) : ℚ) * HSub.hSub (α := ℚ) (↑m : ℚ) (↑n : ℚ) /
      (HSub.hSub (α := ℚ) (↑m : ℚ) (↑i : ℚ) * (↑(m.choose i) : ℚ))
have h₂ : i ≤ n
Tactic: have h₁ := le_of_lt_succ h₁
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (hypothesis)
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
⊢ f i - f (i + 1) =
    (↑(n.choose i) : ℚ) * HSub.hSub (α := ℚ) (↑m : ℚ) (↑n : ℚ) /
      (HSub.hSub (α := ℚ) (↑m : ℚ) (↑i : ℚ) * (↑(m.choose i) : ℚ))
have h₂ : i < m
Tactic: have h₂ := h₁.trans_lt h
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (hypothesis)
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
⊢ f i - f (i + 1) =
    (↑(n.choose i) : ℚ) * HSub.hSub (α := ℚ) (↑m : ℚ) (↑n : ℚ) /
      (HSub.hSub (α := ℚ) (↑m : ℚ) (↑i : ℚ) * (↑(m.choose i) : ℚ))
have h₃ : i ≤ m
Tactic: have h₃ := h₂.le
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (hypothesis)
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
⊢ f i - f (i + 1) =
    (↑(n.choose i) : ℚ) * HSub.hSub (α := ℚ) (↑m : ℚ) (↑n : ℚ) /
      (HSub.hSub (α := ℚ) (↑m : ℚ) (↑i : ℚ) * (↑(m.choose i) : ℚ))
have hi₄ : HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 ≠ 0
Tactic: have hi₄ : (i + 1 : ℚ) ≠ 0 := i.cast_add_one_ne_zero
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (hypothesis)
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
⊢ f i - f (i + 1) =
    (↑(n.choose i) : ℚ) * HSub.hSub (α := ℚ) (↑m : ℚ) (↑n : ℚ) /
      (HSub.hSub (α := ℚ) (↑m : ℚ) (↑i : ℚ) * (↑(m.choose i) : ℚ))
have this : Eq (α := ℚ) (↑(m.choose (i + 1) * (i + 1)) : ℚ) (↑(m.choose i * (m - i)) : ℚ)
Tactic: have := congr_arg ((↑) : ℕ → ℚ) (choose_succ_right_eq m i)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (hypothesis)
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)) : ℚ)
⊢ f i - f (i + 1) =
    (↑(n.choose i) : ℚ) * HSub.hSub (α := ℚ) (↑m : ℚ) (↑n : ℚ) /
      (HSub.hSub (α := ℚ) (↑m : ℚ) (↑i : ℚ) * (↑(m.choose i) : ℚ))
have this₁ : (↑(m.choose (i + 1)) : ℚ) * HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 = HMul.hMul (α := ℚ) (↑(m.choose i) : ℚ) (↑(m - i) : ℚ)
Tactic: push_cast at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
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) : ℚ)
⊢ 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) : ℚ))
have rw : HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹ -
    (↑(n.choose (i + 1)) : ℚ) *
      (HMul.hMul (α := ℚ) (↑(m.choose i) : ℚ) (↑(m - i) : ℚ) * (HAdd.hAdd (α := ℚ) (↑i : ℚ) 1)⁻¹)⁻¹ =
  (↑(n.choose i) : ℚ) * HSub.hSub (α := ℚ) (↑m : ℚ) (↑n : ℚ) /
    (HSub.hSub (α := ℚ) (↑m : ℚ) (↑i : ℚ) * (↑(m.choose i) : ℚ))
Tactic: rw [(eq_mul_inv_iff_mul_eq₀ hi₄).mpr this]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (hypothesis)
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) : ℚ)
⊢ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹ -
      (↑(n.choose (i + 1)) : ℚ) *
        (HMul.hMul (α := ℚ) (↑(m.choose i) : ℚ) (↑(m - i) : ℚ) * (HAdd.hAdd (α := ℚ) (↑i : ℚ) 1)⁻¹)⁻¹ =
    (↑(n.choose i) : ℚ) * HSub.hSub (α := ℚ) (↑m : ℚ) (↑n : ℚ) /
      (HSub.hSub (α := ℚ) (↑m : ℚ) (↑i : ℚ) * (↑(m.choose i) : ℚ))
have this₁ : Eq (α := ℚ) (↑(n.choose (i + 1) * (i + 1)) : ℚ) (↑(n.choose i * (n - i)) : ℚ)
Tactic: have := congr_arg ((↑) : ℕ → ℚ) (choose_succ_right_eq n i)
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (hypothesis)
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_1 :
  (↑(m.choose (i + 1)) : ℚ) * HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 = HMul.hMul (α := ℚ) (↑(m.choose i) : ℚ) (↑(m - i) : ℚ)
this : Eq (α := ℚ) (↑(n.choose (i + 1) * (i + 1)) : ℚ) (↑(n.choose i * (n - i)) : ℚ)
⊢ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹ -
      (↑(n.choose (i + 1)) : ℚ) *
        (HMul.hMul (α := ℚ) (↑(m.choose i) : ℚ) (↑(m - i) : ℚ) * (HAdd.hAdd (α := ℚ) (↑i : ℚ) 1)⁻¹)⁻¹ =
    (↑(n.choose i) : ℚ) * HSub.hSub (α := ℚ) (↑m : ℚ) (↑n : ℚ) /
      (HSub.hSub (α := ℚ) (↑m : ℚ) (↑i : ℚ) * (↑(m.choose i) : ℚ))
have this₁ : (↑(n.choose (i + 1)) : ℚ) * HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 = HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(n - i) : ℚ)
Tactic: push_cast at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (goal)
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_1 :
  (↑(m.choose (i + 1)) : ℚ) * HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 = HMul.hMul (α := ℚ) (↑(m.choose i) : ℚ) (↑(m - i) : ℚ)
this : (↑(n.choose (i + 1)) : ℚ) * HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 = HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(n - i) : ℚ)
⊢ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹ -
      (↑(n.choose (i + 1)) : ℚ) *
        (HMul.hMul (α := ℚ) (↑(m.choose i) : ℚ) (↑(m - i) : ℚ) * (HAdd.hAdd (α := ℚ) (↑i : ℚ) 1)⁻¹)⁻¹ =
    (↑(n.choose i) : ℚ) * HSub.hSub (α := ℚ) (↑m : ℚ) (↑n : ℚ) /
      (HSub.hSub (α := ℚ) (↑m : ℚ) (↑i : ℚ) * (↑(m.choose i) : ℚ))
have rw : HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹ -
    HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(n - i) : ℚ) * (HAdd.hAdd (α := ℚ) (↑i : ℚ) 1)⁻¹ *
      (HMul.hMul (α := ℚ) (↑(m.choose i) : ℚ) (↑(m - i) : ℚ) * (HAdd.hAdd (α := ℚ) (↑i : ℚ) 1)⁻¹)⁻¹ =
  (↑(n.choose i) : ℚ) * HSub.hSub (α := ℚ) (↑m : ℚ) (↑n : ℚ) /
    (HSub.hSub (α := ℚ) (↑m : ℚ) (↑i : ℚ) * (↑(m.choose i) : ℚ))
Tactic: rw [(eq_mul_inv_iff_mul_eq₀ hi₄).mpr this]
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (hypothesis)
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_1 :
  (↑(m.choose (i + 1)) : ℚ) * HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 = HMul.hMul (α := ℚ) (↑(m.choose i) : ℚ) (↑(m - i) : ℚ)
this : (↑(n.choose (i + 1)) : ℚ) * HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 = HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(n - i) : ℚ)
⊢ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹ -
      HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(n - i) : ℚ) * (HAdd.hAdd (α := ℚ) (↑i : ℚ) 1)⁻¹ *
        (HMul.hMul (α := ℚ) (↑(m.choose i) : ℚ) (↑(m - i) : ℚ) * (HAdd.hAdd (α := ℚ) (↑i : ℚ) 1)⁻¹)⁻¹ =
    (↑(n.choose i) : ℚ) * HSub.hSub (α := ℚ) (↑m : ℚ) (↑n : ℚ) /
      (HSub.hSub (α := ℚ) (↑m : ℚ) (↑i : ℚ) * (↑(m.choose i) : ℚ))
have this₁ : HSub.hSub (α := ℚ) (↑m : ℚ) (↑i : ℚ) ≠ 0
Tactic: have : (m - i : ℚ) ≠ 0 := sub_ne_zero_of_ne (cast_lt.mpr h₂).ne'
-- Lean 4 proof step from Mathlib.Combinatorics.SetFamily.AhlswedeZhang (hypothesis)
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_1 :
  (↑(m.choose (i + 1)) : ℚ) * HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 = HMul.hMul (α := ℚ) (↑(m.choose i) : ℚ) (↑(m - i) : ℚ)
this_2 :
  (↑(n.choose (i + 1)) : ℚ) * HAdd.hAdd (α := ℚ) (↑i : ℚ) 1 = HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(n - i) : ℚ)
this : HSub.hSub (α := ℚ) (↑m : ℚ) (↑i : ℚ) ≠ 0
⊢ HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(m.choose i) : ℚ)⁻¹ -
      HMul.hMul (α := ℚ) (↑(n.choose i) : ℚ) (↑(n - i) : ℚ) * (HAdd.hAdd (α := ℚ) (↑i : ℚ) 1)⁻¹ *
        (HMul.hMul (α := ℚ) (↑(m.choose i) : ℚ) (↑(m - i) : ℚ) * (HAdd.hAdd (α := ℚ) (↑i : ℚ) 1)⁻¹)⁻¹ =
    (↑(n.choose i) : ℚ) * HSub.hSub (α := ℚ) (↑m : ℚ) (↑n : ℚ) /
      (HSub.hSub (α := ℚ) (↑m : ℚ) (↑i : ℚ) * (↑(m.choose i) : ℚ))
have this₁ : Ne (α := ℚ) (↑(m.choose i) : ℚ) 0
Tactic: have : (m.choose i : ℚ) ≠ 0 := cast_ne_zero.2 (choose_pos h₂.le).ne'