case inl
α : Type u_1
β : Type ?u.130854
s t : Set α
a b x y : α
f : α → β
i : ℕ
h₁ : i + ncard s ≤ ncard t
h₂ : s ⊆ t
ht : Set.Finite t
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ ncard r = i + ncard s

case inr
α : Type u_1
β : Type ?u.130854
s t : Set α
a b x y : α
f : α → β
i : ℕ
h₁ : i + ncard s ≤ ncard t
h₂ : s ⊆ t
ht : Set.Infinite t
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ ncard r = i + ncard s
α : Type u_1
β : Type ?u.130854
s t : Set α
a b x y : α
f : α → β
i : ℕ
h₁ : i + ncard s ≤ ncard t
h₂ : s ⊆ t
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ ncard r = i + ncard s
cases' t.finite_or_infinite with ht ht
case inr
α : Type u_1
β : Type ?u.130854
s t : Set α
a b x y : α
f : α → β
i : ℕ
h₁ : i + ncard s ≤ 0
h₂ : s ⊆ t
ht : Set.Infinite t
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ ncard r = i + ncard s
case inr
α : Type u_1
β : Type ?u.130854
s t : Set α
a b x y : α
f : α → β
i : ℕ
h₁ : i + ncard s ≤ ncard t
h₂ : s ⊆ t
ht : Set.Infinite t
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ ncard r = i + ncard s
rw [ht.ncard] at h₁
case inr
α : Type u_1
β : Type ?u.130854
s t : Set α
a b x y : α
f : α → β
i : ℕ
h₁ : i + ncard s ≤ 0
h₂ : s ⊆ t
ht : Set.Infinite t
h₁' : i + ncard s = 0
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ ncard r = i + ncard s
case inr
α : Type u_1
β : Type ?u.130854
s t : Set α
a b x y : α
f : α → β
i : ℕ
h₁ : i + ncard s ≤ 0
h₂ : s ⊆ t
ht : Set.Infinite t
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ ncard r = i + ncard s
have h₁' := Nat.eq_zero_of_le_zero h₁
case inr
α : Type u_1
β : Type ?u.130854
s t : Set α
a b x y : α
f : α → β
i : ℕ
h₁ : i + ncard s ≤ 0
h₂ : s ⊆ t
ht : Set.Infinite t
h₁' : i = 0 ∧ ncard s = 0
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ ncard r = i + ncard s
case inr
α : Type u_1
β : Type ?u.130854
s t : Set α
a b x y : α
f : α → β
i : ℕ
h₁ : i + ncard s ≤ 0
h₂ : s ⊆ t
ht : Set.Infinite t
h₁' : i + ncard s = 0
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ ncard r = i + ncard s
rw [add_eq_zero_iff] at h₁'
case inr
α : Type u_1
β : Type ?u.130854
s t : Set α
a b x y : α
f : α → β
i : ℕ
h₁ : i + ncard s ≤ 0
h₂ : s ⊆ t
ht : Set.Infinite t
h₁' : i = 0 ∧ ncard s = 0
⊢ ncard t = i + ncard s
case inr
α : Type u_1
β : Type ?u.130854
s t : Set α
a b x y : α
f : α → β
i : ℕ
h₁ : i + ncard s ≤ 0
h₂ : s ⊆ t
ht : Set.Infinite t
h₁' : i = 0 ∧ ncard s = 0
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ ncard r = i + ncard s
refine' ⟨t, h₂, rfl.subset, _⟩
no goals
case inr
α : Type u_1
β : Type ?u.130854
s t : Set α
a b x y : α
f : α → β
i : ℕ
h₁ : i + ncard s ≤ 0
h₂ : s ⊆ t
ht : Set.Infinite t
h₁' : i = 0 ∧ ncard s = 0
⊢ ncard t = i + ncard s
rw [h₁'.2, h₁'.1, ht.ncard, add_zero]
case inl
α : Type u_1
β : Type ?u.130854
s t : Set α
a b x y : α
f : α → β
i : ℕ
h₂ : s ⊆ t
ht : Set.Finite t
h₁ : i + Finset.card (Finite.toFinset (_ : Set.Finite s)) ≤ ncard t
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ ncard r = i + Finset.card (Finite.toFinset (_ : Set.Finite s))
case inl
α : Type u_1
β : Type ?u.130854
s t : Set α
a b x y : α
f : α → β
i : ℕ
h₁ : i + ncard s ≤ ncard t
h₂ : s ⊆ t
ht : Set.Finite t
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ ncard r = i + ncard s
rw [ncard_eq_toFinset_card _ (ht.subset h₂)] at h₁ ⊢
case inl
α : Type u_1
β : Type ?u.130854
s t : Set α
a b x y : α
f : α → β
i : ℕ
h₂ : s ⊆ t
ht : Set.Finite t
h₁ : i + Finset.card (Finite.toFinset (_ : Set.Finite s)) ≤ Finset.card (Finite.toFinset ht)
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ ncard r = i + Finset.card (Finite.toFinset (_ : Set.Finite s))
case inl
α : Type u_1
β : Type ?u.130854
s t : Set α
a b x y : α
f : α → β
i : ℕ
h₂ : s ⊆ t
ht : Set.Finite t
h₁ : i + Finset.card (Finite.toFinset (_ : Set.Finite s)) ≤ ncard t
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ ncard r = i + Finset.card (Finite.toFinset (_ : Set.Finite s))
rw [ncard_eq_toFinset_card t ht] at h₁
case inl.intro.intro.intro
α : Type u_1
β : Type ?u.130854
s t : Set α
a b x y : α
f : α → β
i : ℕ
h₂ : s ⊆ t
ht : Set.Finite t
h₁ : i + Finset.card (Finite.toFinset (_ : Set.Finite s)) ≤ Finset.card (Finite.toFinset ht)
r' : Finset α
hsr' : Finite.toFinset (_ : Set.Finite s) ⊆ r'
hr't : r' ⊆ Finite.toFinset ht
hr' : Finset.card r' = i + Finset.card (Finite.toFinset (_ : Set.Finite s))
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ ncard r = i + Finset.card (Finite.toFinset (_ : Set.Finite s))
case inl
α : Type u_1
β : Type ?u.130854
s t : Set α
a b x y : α
f : α → β
i : ℕ
h₂ : s ⊆ t
ht : Set.Finite t
h₁ : i + Finset.card (Finite.toFinset (_ : Set.Finite s)) ≤ Finset.card (Finite.toFinset ht)
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ ncard r = i + Finset.card (Finite.toFinset (_ : Set.Finite s))
obtain ⟨r', hsr', hr't, hr'⟩ := Finset.exists_intermediate_set _ h₁ (by simpa)
no goals
case inl.intro.intro.intro
α : Type u_1
β : Type ?u.130854
s t : Set α
a b x y : α
f : α → β
i : ℕ
h₂ : s ⊆ t
ht : Set.Finite t
h₁ : i + Finset.card (Finite.toFinset (_ : Set.Finite s)) ≤ Finset.card (Finite.toFinset ht)
r' : Finset α
hsr' : Finite.toFinset (_ : Set.Finite s) ⊆ r'
hr't : r' ⊆ Finite.toFinset ht
hr' : Finset.card r' = i + Finset.card (Finite.toFinset (_ : Set.Finite s))
⊢ ∃ r, s ⊆ r ∧ r ⊆ t ∧ ncard r = i + Finset.card (Finite.toFinset (_ : Set.Finite s))
exact ⟨r', by simpa using hsr', by simpa using hr't, by rw [← hr', ncard_coe_Finset]⟩
no goals
α : Type u_1
β : Type ?u.130854
s t : Set α
a b x y : α
f : α → β
i : ℕ
h₂ : s ⊆ t
ht : Set.Finite t
h₁ : i + Finset.card (Finite.toFinset (_ : Set.Finite s)) ≤ Finset.card (Finite.toFinset ht)
⊢ Finite.toFinset (_ : Set.Finite s) ⊆ Finite.toFinset ht
simpa
no goals
α : Type u_1
β : Type ?u.130854
s t : Set α
a b x y : α
f : α → β
i : ℕ
h₂ : s ⊆ t
ht : Set.Finite t
h₁ : i + Finset.card (Finite.toFinset (_ : Set.Finite s)) ≤ Finset.card (Finite.toFinset ht)
r' : Finset α
hsr' : Finite.toFinset (_ : Set.Finite s) ⊆ r'
hr't : r' ⊆ Finite.toFinset ht
hr' : Finset.card r' = i + Finset.card (Finite.toFinset (_ : Set.Finite s))
⊢ s ⊆ ↑r'
simpa using hsr'
no goals
α : Type u_1
β : Type ?u.130854
s t : Set α
a b x y : α
f : α → β
i : ℕ
h₂ : s ⊆ t
ht : Set.Finite t
h₁ : i + Finset.card (Finite.toFinset (_ : Set.Finite s)) ≤ Finset.card (Finite.toFinset ht)
r' : Finset α
hsr' : Finite.toFinset (_ : Set.Finite s) ⊆ r'
hr't : r' ⊆ Finite.toFinset ht
hr' : Finset.card r' = i + Finset.card (Finite.toFinset (_ : Set.Finite s))
⊢ ↑r' ⊆ t
simpa using hr't
no goals
α : Type u_1
β : Type ?u.130854
s t : Set α
a b x y : α
f : α → β
i : ℕ
h₂ : s ⊆ t
ht : Set.Finite t
h₁ : i + Finset.card (Finite.toFinset (_ : Set.Finite s)) ≤ Finset.card (Finite.toFinset ht)
r' : Finset α
hsr' : Finite.toFinset (_ : Set.Finite s) ⊆ r'
hr't : r' ⊆ Finite.toFinset ht
hr' : Finset.card r' = i + Finset.card (Finite.toFinset (_ : Set.Finite s))
⊢ ncard ↑r' = i + Finset.card (Finite.toFinset (_ : Set.Finite s))
rw [← hr', ncard_coe_Finset]