Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case neg.inl.inl
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
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun x ↦
    match 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✝ a : ℕ
left✝ : Sum.inl a✝ ≠ Sum.inl a
hxy : f (Sum.inl a✝) = f (Sum.inl a)
ha : (0 < a✝ ∧ a✝ ≤ n) ∧ a✝ ∈ A
hb : (0 < a ∧ a ≤ n) ∧ a ∈ A
⊢ n ∈ A + B

pp: case neg.inl.inr
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
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun x ↦
    match 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

pp: case neg.inr.inl
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
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun x ↦
    match 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

pp: case neg.inr.inr
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
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun x ↦
    match 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✝ b : ℕ
left✝ : Sum.inr b✝ ≠ Sum.inr b
hxy : f (Sum.inr b✝) = f (Sum.inr b)
ha : (0 < b✝ ∧ b✝ ≤ n) ∧ b✝ ∈ B
hb : (0 < b ∧ b ≤ n) ∧ b ∈ B
⊢ n ∈ A + B

Tactic:
<;>

Goal state after:
case neg.inl.inl
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
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun x ↦
    match 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✝ a : ℕ
left✝ : Sum.inl a✝ ≠ Sum.inl a
hxy : f (Sum.inl a✝) = f (Sum.inl a)
ha : (0 < a✝ ∧ a✝ ≤ n) ∧ a✝ ∈ A
hb : (0 < a ∧ a ≤ n) ∧ a ∈ A
⊢ n ∈ A + B

case neg.inl.inr
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
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun x ↦
    match 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

case neg.inr.inl
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
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun x ↦
    match 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

case neg.inr.inr
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
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun x ↦
    match 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✝ b : ℕ
left✝ : Sum.inr b✝ ≠ Sum.inr b
hxy : f (Sum.inr b✝) = f (Sum.inr b)
ha : (0 < b✝ ∧ b✝ ≤ n) ∧ b✝ ∈ B
hb : (0 < b ∧ b ≤ n) ∧ b ∈ B
⊢ n ∈ A + B