case refine'_1
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α ↪ β
s : Finset β
t : Finset α
h : s ⊆ map f t
⊢ s = map f (preimage s ↑f (_ : InjOn (↑f) (↑f ⁻¹' ↑s)))

case refine'_2
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α ↪ β
s : Finset β
t : Finset α
⊢ (∃ u x, s = map f u) → s ⊆ map f t
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α ↪ β
s : Finset β
t : Finset α
⊢ s ⊆ map f t ↔ ∃ u x, s = map f u
refine' ⟨fun h => ⟨_, preimage_subset h, _⟩, _⟩
case refine'_1
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α ↪ β
s : Finset β
t : Finset α
h : s ⊆ map f t
⊢ ∀ (x : β), x ∈ s → x ∈ Set.range ↑f
case refine'_1
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α ↪ β
s : Finset β
t : Finset α
h : s ⊆ map f t
⊢ s = map f (preimage s ↑f (_ : InjOn (↑f) (↑f ⁻¹' ↑s)))
rw [map_eq_image, image_preimage, filter_true_of_mem]
no goals
case refine'_1
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α ↪ β
s : Finset β
t : Finset α
h : s ⊆ map f t
⊢ ∀ (x : β), x ∈ s → x ∈ Set.range ↑f
exact fun x hx ↦ coe_map_subset_range _ _ (h hx)
case refine'_2.intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α ↪ β
t u : Finset α
hut : u ⊆ t
⊢ map f u ⊆ map f t
case refine'_2
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α ↪ β
s : Finset β
t : Finset α
⊢ (∃ u x, s = map f u) → s ⊆ map f t
rintro ⟨u, hut, rfl⟩
no goals
case refine'_2.intro.intro
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α ↪ β
t u : Finset α
hut : u ⊆ t
⊢ map f u ⊆ map f t
exact map_subset_map.2 hut