[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β
⊢ InjOn f (f ⁻¹' ↑∅)
[PROOFSTEP]
simp [InjOn]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β
⊢ ↑(preimage ∅ f (_ : ∀ (a : α), a ∈ f ⁻¹' ↑∅ → ∀ (a_2 : α), a_2 ∈ f ⁻¹' ↑∅ → f a = f a_2 → a = a_2)) = ↑∅
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α → β
inst✝¹ : Fintype α
inst✝ : Fintype β
hf : InjOn f (f ⁻¹' ↑univ)
⊢ ↑(preimage univ f hf) = ↑univ
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s t : Finset β
hs : InjOn f (f ⁻¹' ↑s)
ht : InjOn f (f ⁻¹' ↑t)
⊢ ↑(preimage (s ∩ t) f
        (_ : ∀ (x₁ : α), x₁ ∈ f ⁻¹' ↑(s ∩ t) → ∀ (x₂ : α), x₂ ∈ f ⁻¹' ↑(s ∩ t) → f x₁ = f x₂ → x₁ = x₂)) =
    ↑(preimage s f hs ∩ preimage t f ht)
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
s t : Finset β
hst : InjOn f (f ⁻¹' ↑(s ∪ t))
⊢ ↑(preimage (s ∪ t) f hst) =
    ↑(preimage s f (_ : ∀ (x₁ : α), x₁ ∈ f ⁻¹' ↑s → ∀ (x₂ : α), x₂ ∈ f ⁻¹' ↑s → f x₁ = f x₂ → x₁ = x₂) ∪
        preimage t f (_ : ∀ (x₁ : α), x₁ ∈ f ⁻¹' ↑t → ∀ (x₂ : α), x₂ ∈ f ⁻¹' ↑t → f x₁ = f x₂ → x₁ = x₂))
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → β
s : Finset β
hf : Injective f
⊢ ↑(preimage sᶜ f (_ : InjOn f (f ⁻¹' ↑sᶜ))) = ↑(preimage s f (_ : InjOn f (f ⁻¹' ↑s)))ᶜ
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : DecidableEq β
f : α → β
s : Finset α
t : Finset β
hf : InjOn f (f ⁻¹' ↑t)
⊢ (∀ (x : α), x ∈ s → f x ∈ t) ↔ s ⊆ preimage t f hf
[PROOFSTEP]
simp only [subset_iff, mem_preimage]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α ↪ β
s : Finset α
t : Finset β
⊢ map f s ⊆ t ↔ s ⊆ preimage t ↑f (_ : InjOn (↑f) (↑f ⁻¹' ↑t))
[PROOFSTEP]
classical rw [map_eq_image, image_subset_iff_subset_preimage]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α ↪ β
s : Finset α
t : Finset β
⊢ map f s ⊆ t ↔ s ⊆ preimage t ↑f (_ : InjOn (↑f) (↑f ⁻¹' ↑t))
[PROOFSTEP]
rw [map_eq_image, image_subset_iff_subset_preimage]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : DecidableEq β
f : α → β
s : Finset β
inst✝ : (x : β) → Decidable (x ∈ Set.range f)
hf : InjOn f (f ⁻¹' ↑s)
⊢ ↑(image f (preimage s f hf)) = ↑(filter (fun x => x ∈ Set.range f) s)
[PROOFSTEP]
simp only [coe_image, coe_preimage, coe_filter, Set.image_preimage_eq_inter_range, ← Set.sep_mem_eq]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : DecidableEq β
f : α → β
s : Finset β
inst✝ : (x : β) → Decidable (x ∈ Set.range f)
hf : InjOn f (f ⁻¹' ↑s)
⊢ {x | x ∈ ↑s ∧ x ∈ Set.range f} = {x | x ∈ s ∧ x ∈ Set.range f}
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : DecidableEq β
f : α → β
s : Finset β
hf : BijOn f (f ⁻¹' ↑s) ↑s
⊢ ↑(image f (preimage s f (_ : InjOn f (f ⁻¹' ↑s)))) = ↑s
[PROOFSTEP]
simpa using hf.image_eq
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α ↪ β
s : Finset β
t : Finset α
⊢ s ⊆ map f t ↔ ∃ u x, s = map f u
[PROOFSTEP]
classical
refine' ⟨fun h => ⟨_, preimage_subset h, _⟩, _⟩
· rw [map_eq_image, image_preimage, filter_true_of_mem]
  exact fun x hx ↦ coe_map_subset_range _ _ (h hx)
· rintro ⟨u, hut, rfl⟩
  exact map_subset_map.2 hut
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
f : α ↪ β
s : Finset β
t : Finset α
⊢ s ⊆ map f t ↔ ∃ u x, s = map f u
[PROOFSTEP]
refine' ⟨fun h => ⟨_, preimage_subset h, _⟩, _⟩
[GOAL]
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)))
[PROOFSTEP]
rw [map_eq_image, image_preimage, filter_true_of_mem]
[GOAL]
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
[PROOFSTEP]
exact fun x hx ↦ coe_map_subset_range _ _ (h hx)
[GOAL]
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
[PROOFSTEP]
rintro ⟨u, hut, rfl⟩
[GOAL]
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
[PROOFSTEP]
exact map_subset_map.2 hut
[GOAL]
α : Type u
β✝ : Type v
ι : Sort w
γ : Type x
β : α → Type u_1
inst✝ : DecidableEq α
s : Finset ((a : α) × β a)
t : Finset α
⊢ (Finset.sigma t fun a => preimage s (Sigma.mk a) (_ : InjOn (Sigma.mk a) (Sigma.mk a ⁻¹' ↑s))) =
    filter (fun a => a.fst ∈ t) s
[PROOFSTEP]
ext x
[GOAL]
case a
α : Type u
β✝ : Type v
ι : Sort w
γ : Type x
β : α → Type u_1
inst✝ : DecidableEq α
s : Finset ((a : α) × β a)
t : Finset α
x : (i : α) × β i
⊢ (x ∈ Finset.sigma t fun a => preimage s (Sigma.mk a) (_ : InjOn (Sigma.mk a) (Sigma.mk a ⁻¹' ↑s))) ↔
    x ∈ filter (fun a => a.fst ∈ t) s
[PROOFSTEP]
simp [and_comm]
[GOAL]
α : Type u
β✝ : Type v
ι : Sort w
γ : Type x
β : α → Type u_1
inst✝ : DecidableEq α
s : Finset ((a : α) × β a)
t : Finset α
ht : image Sigma.fst s ⊆ t
⊢ (Finset.sigma t fun a => preimage s (Sigma.mk a) (_ : InjOn (Sigma.mk a) (Sigma.mk a ⁻¹' ↑s))) = s
[PROOFSTEP]
rw [sigma_preimage_mk, filter_true_of_mem <| image_subset_iff.1 ht]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : CommMonoid β
f : α → γ
inst✝ : DecidablePred fun x => x ∈ Set.range f
s : Finset γ
hf : InjOn f (f ⁻¹' ↑s)
g : γ → β
⊢ ∏ x in preimage s f hf, g (f x) = ∏ x in filter (fun x => x ∈ Set.range f) s, g x
[PROOFSTEP]
haveI := Classical.decEq γ
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : CommMonoid β
f : α → γ
inst✝ : DecidablePred fun x => x ∈ Set.range f
s : Finset γ
hf : InjOn f (f ⁻¹' ↑s)
g : γ → β
this : DecidableEq γ
⊢ ∏ x in preimage s f hf, g (f x) = ∏ x in filter (fun x => x ∈ Set.range f) s, g x
[PROOFSTEP]
calc
  (∏ x in preimage s f hf, g (f x)) = ∏ x in image f (preimage s f hf), g x :=
    Eq.symm <| prod_image <| by simpa only [mem_preimage, InjOn] using hf
  _ = ∏ x in s.filter fun x => x ∈ Set.range f, g x := by rw [image_preimage]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : CommMonoid β
f : α → γ
inst✝ : DecidablePred fun x => x ∈ Set.range f
s : Finset γ
hf : InjOn f (f ⁻¹' ↑s)
g : γ → β
this : DecidableEq γ
⊢ ∀ (x : α), x ∈ preimage s f hf → ∀ (y : α), y ∈ preimage s f hf → f x = f y → x = y
[PROOFSTEP]
simpa only [mem_preimage, InjOn] using hf
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝¹ : CommMonoid β
f : α → γ
inst✝ : DecidablePred fun x => x ∈ Set.range f
s : Finset γ
hf : InjOn f (f ⁻¹' ↑s)
g : γ → β
this : DecidableEq γ
⊢ ∏ x in image f (preimage s f hf), g x = ∏ x in filter (fun x => x ∈ Set.range f) s, g x
[PROOFSTEP]
rw [image_preimage]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : CommMonoid β
f : α → γ
s : Finset γ
hf : InjOn f (f ⁻¹' ↑s)
g : γ → β
hg : ∀ (x : γ), x ∈ s → ¬x ∈ Set.range f → g x = 1
⊢ ∏ x in preimage s f hf, g (f x) = ∏ x in s, g x
[PROOFSTEP]
classical
rw [prod_preimage', prod_filter_of_ne]
exact fun x hx => Not.imp_symm (hg x hx)
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : CommMonoid β
f : α → γ
s : Finset γ
hf : InjOn f (f ⁻¹' ↑s)
g : γ → β
hg : ∀ (x : γ), x ∈ s → ¬x ∈ Set.range f → g x = 1
⊢ ∏ x in preimage s f hf, g (f x) = ∏ x in s, g x
[PROOFSTEP]
rw [prod_preimage', prod_filter_of_ne]
[GOAL]
α : Type u
β : Type v
ι : Sort w
γ : Type x
inst✝ : CommMonoid β
f : α → γ
s : Finset γ
hf : InjOn f (f ⁻¹' ↑s)
g : γ → β
hg : ∀ (x : γ), x ∈ s → ¬x ∈ Set.range f → g x = 1
⊢ ∀ (x : γ), x ∈ s → g x ≠ 1 → x ∈ Set.range f
[PROOFSTEP]
exact fun x hx => Not.imp_symm (hg x hx)
