case mp
α : Type u_1
β : Type u_2
γ : Type ?u.77374
ι : Sort ?u.77377
ι' : Sort ?u.77380
f✝ : ι → α
s✝ t✝ s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
⊢ f ⁻¹' s = f ⁻¹' t → s = t

case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.77374
ι : Sort ?u.77377
ι' : Sort ?u.77380
f✝ : ι → α
s✝ t✝ s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
⊢ s = t → f ⁻¹' s = f ⁻¹' t
α : Type u_1
β : Type u_2
γ : Type ?u.77374
ι : Sort ?u.77377
ι' : Sort ?u.77380
f✝ : ι → α
s✝ t✝ s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
⊢ f ⁻¹' s = f ⁻¹' t ↔ s = t
constructor
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.77374
ι : Sort ?u.77377
ι' : Sort ?u.77380
f✝ : ι → α
s✝ t s : Set α
f : β → α
hs ht : s ⊆ range f
⊢ f ⁻¹' s = f ⁻¹' s
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.77374
ι : Sort ?u.77377
ι' : Sort ?u.77380
f✝ : ι → α
s✝ t✝ s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
⊢ s = t → f ⁻¹' s = f ⁻¹' t
rintro rfl
no goals
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.77374
ι : Sort ?u.77377
ι' : Sort ?u.77380
f✝ : ι → α
s✝ t s : Set α
f : β → α
hs ht : s ⊆ range f
⊢ f ⁻¹' s = f ⁻¹' s
rfl
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.77374
ι : Sort ?u.77377
ι' : Sort ?u.77380
f✝ : ι → α
s✝ t✝ s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
h : f ⁻¹' s = f ⁻¹' t
⊢ s = t
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.77374
ι : Sort ?u.77377
ι' : Sort ?u.77380
f✝ : ι → α
s✝ t✝ s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
⊢ f ⁻¹' s = f ⁻¹' t → s = t
intro h
case mp.h₁
α : Type u_1
β : Type u_2
γ : Type ?u.77374
ι : Sort ?u.77377
ι' : Sort ?u.77380
f✝ : ι → α
s✝ t✝ s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
h : f ⁻¹' s = f ⁻¹' t
⊢ s ⊆ t

case mp.h₂
α : Type u_1
β : Type u_2
γ : Type ?u.77374
ι : Sort ?u.77377
ι' : Sort ?u.77380
f✝ : ι → α
s✝ t✝ s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
h : f ⁻¹' s = f ⁻¹' t
⊢ t ⊆ s
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.77374
ι : Sort ?u.77377
ι' : Sort ?u.77380
f✝ : ι → α
s✝ t✝ s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
h : f ⁻¹' s = f ⁻¹' t
⊢ s = t
apply Subset.antisymm
no goals
case mp.h₁
α : Type u_1
β : Type u_2
γ : Type ?u.77374
ι : Sort ?u.77377
ι' : Sort ?u.77380
f✝ : ι → α
s✝ t✝ s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
h : f ⁻¹' s = f ⁻¹' t
⊢ s ⊆ t
rw [← preimage_subset_preimage_iff hs, h]
no goals
case mp.h₂
α : Type u_1
β : Type u_2
γ : Type ?u.77374
ι : Sort ?u.77377
ι' : Sort ?u.77380
f✝ : ι → α
s✝ t✝ s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
h : f ⁻¹' s = f ⁻¹' t
⊢ t ⊆ s
rw [← preimage_subset_preimage_iff ht, h]