case intro
α : Type u_1
β : Type ?u.43518
s t : Finset α
f : α → β
n : ℕ
A B : Finset α
i : ℕ
h₁ : i + card B ≤ card A
h₂ : B ⊆ A
k : ℕ
h : i + card B + k = card A
⊢ ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
α : Type u_1
β : Type ?u.43518
s t : Finset α
f : α → β
n : ℕ
A B : Finset α
i : ℕ
h₁ : i + card B ≤ card A
h₂ : B ⊆ A
⊢ ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
rcases Nat.le.dest h₁ with ⟨k, h⟩
case intro
α : Type u_1
β : Type ?u.43518
s t : Finset α
f : α → β
n : ℕ
A B : Finset α
i : ℕ
h₂ : B ⊆ A
k : ℕ
h : i + card B + k = card A
⊢ ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
case intro
α : Type u_1
β : Type ?u.43518
s t : Finset α
f : α → β
n : ℕ
A B : Finset α
i : ℕ
h₁ : i + card B ≤ card A
h₂ : B ⊆ A
k : ℕ
h : i + card B + k = card A
⊢ ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
clear h₁
case intro.zero
α : Type u_1
β : Type ?u.43518
s t : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k : ℕ
h✝ : i + card B + k = card A✝
A : Finset α
h₂ : B ⊆ A
h : i + card B + zero = card A
⊢ ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B

case intro.succ
α : Type u_1
β : Type ?u.43518
s t : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
⊢ ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
case intro
α : Type u_1
β : Type ?u.43518
s t : Finset α
f : α → β
n : ℕ
A B : Finset α
i : ℕ
h₂ : B ⊆ A
k : ℕ
h : i + card B + k = card A
⊢ ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
induction' k with k ih generalizing A
case intro.succ.intro
α : Type u_1
β : Type ?u.43518
s t : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
a : α
ha : a ∈ A \ B
⊢ ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
case intro.succ
α : Type u_1
β : Type ?u.43518
s t : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
⊢ ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
obtain ⟨a, ha⟩ : (A \ B).Nonempty := by
  rw [← card_pos, card_sdiff h₂, ← h, Nat.add_right_comm, add_tsub_cancel_right, Nat.add_succ]
  apply Nat.succ_pos
case intro.succ.intro
α : Type u_1
β : Type ?u.43518
s t : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
a : α
ha : a ∈ A \ B
z : i + card B + k = card (erase A a)
⊢ ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
case intro.succ.intro
α : Type u_1
β : Type ?u.43518
s t : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
a : α
ha : a ∈ A \ B
⊢ ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
have z : i + card B + k = card (erase A a) := by
  rw [card_erase_of_mem (mem_sdiff.1 ha).1, ← h,
    Nat.add_sub_assoc (Nat.one_le_iff_ne_zero.mpr k.succ_ne_zero), ←pred_eq_sub_one,
    k.pred_succ]
case intro.succ.intro
α : Type u_1
β : Type ?u.43518
s t : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
a : α
ha : a ∈ A \ B
z : i + card B + k = card (erase A a)
this : B ⊆ erase A a
⊢ ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
case intro.succ.intro
α : Type u_1
β : Type ?u.43518
s t : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
a : α
ha : a ∈ A \ B
z : i + card B + k = card (erase A a)
⊢ ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
have : B ⊆ A.erase a := by
  rintro t th
  apply mem_erase_of_ne_of_mem _ (h₂ th)
  rintro rfl
  exact not_mem_sdiff_of_mem_right th ha
case intro.succ.intro.intro.intro.intro
α : Type u_1
β : Type ?u.43518
s t : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
a : α
ha : a ∈ A \ B
z : i + card B + k = card (erase A a)
this : B ⊆ erase A a
B' : Finset α
hB' : B ⊆ B'
B'subA' : B' ⊆ erase A a
cards : card B' = i + card B
⊢ ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
case intro.succ.intro
α : Type u_1
β : Type ?u.43518
s t : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
a : α
ha : a ∈ A \ B
z : i + card B + k = card (erase A a)
this : B ⊆ erase A a
⊢ ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
rcases ih this z with ⟨B', hB', B'subA', cards⟩
no goals
case intro.succ.intro.intro.intro.intro
α : Type u_1
β : Type ?u.43518
s t : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
a : α
ha : a ∈ A \ B
z : i + card B + k = card (erase A a)
this : B ⊆ erase A a
B' : Finset α
hB' : B ⊆ B'
B'subA' : B' ⊆ erase A a
cards : card B' = i + card B
⊢ ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
exact ⟨B', hB', B'subA'.trans (erase_subset _ _), cards⟩
no goals
case intro.zero
α : Type u_1
β : Type ?u.43518
s t : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k : ℕ
h✝ : i + card B + k = card A✝
A : Finset α
h₂ : B ⊆ A
h : i + card B + zero = card A
⊢ ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
exact ⟨A, h₂, Subset.refl _, h.symm⟩
α : Type u_1
β : Type ?u.43518
s t : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
⊢ 0 < succ (i + k)
α : Type u_1
β : Type ?u.43518
s t : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
⊢ Finset.Nonempty (A \ B)
rw [← card_pos, card_sdiff h₂, ← h, Nat.add_right_comm, add_tsub_cancel_right, Nat.add_succ]
no goals
α : Type u_1
β : Type ?u.43518
s t : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
⊢ 0 < succ (i + k)
apply Nat.succ_pos
no goals
α : Type u_1
β : Type ?u.43518
s t : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
a : α
ha : a ∈ A \ B
⊢ i + card B + k = card (erase A a)
rw [card_erase_of_mem (mem_sdiff.1 ha).1, ← h,
  Nat.add_sub_assoc (Nat.one_le_iff_ne_zero.mpr k.succ_ne_zero), ←pred_eq_sub_one,
  k.pred_succ]
α : Type u_1
β : Type ?u.43518
s t✝ : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
a : α
ha : a ∈ A \ B
z : i + card B + k = card (erase A a)
t : α
th : t ∈ B
⊢ t ∈ erase A a
α : Type u_1
β : Type ?u.43518
s t : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
a : α
ha : a ∈ A \ B
z : i + card B + k = card (erase A a)
⊢ B ⊆ erase A a
rintro t th
α : Type u_1
β : Type ?u.43518
s t✝ : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
a : α
ha : a ∈ A \ B
z : i + card B + k = card (erase A a)
t : α
th : t ∈ B
⊢ t ≠ a
α : Type u_1
β : Type ?u.43518
s t✝ : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
a : α
ha : a ∈ A \ B
z : i + card B + k = card (erase A a)
t : α
th : t ∈ B
⊢ t ∈ erase A a
apply mem_erase_of_ne_of_mem _ (h₂ th)
α : Type u_1
β : Type ?u.43518
s t✝ : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
t : α
th : t ∈ B
ha : t ∈ A \ B
z : i + card B + k = card (erase A t)
⊢ False
α : Type u_1
β : Type ?u.43518
s t✝ : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
a : α
ha : a ∈ A \ B
z : i + card B + k = card (erase A a)
t : α
th : t ∈ B
⊢ t ≠ a
rintro rfl
no goals
α : Type u_1
β : Type ?u.43518
s t✝ : Finset α
f : α → β
n : ℕ
A✝ B : Finset α
i : ℕ
h₂✝ : B ⊆ A✝
k✝ : ℕ
h✝ : i + card B + k✝ = card A✝
k : ℕ
ih : ∀ {A : Finset α}, B ⊆ A → i + card B + k = card A → ∃ C, B ⊆ C ∧ C ⊆ A ∧ card C = i + card B
A : Finset α
h₂ : B ⊆ A
h : i + card B + succ k = card A
t : α
th : t ∈ B
ha : t ∈ A \ B
z : i + card B + k = card (erase A t)
⊢ False
exact not_mem_sdiff_of_mem_right th ha