case mp
α : Type u_1
β : Type u_2
γ : Type ?u.77161
ι : Sort ?u.77164
ι' : Sort ?u.77167
f✝ : ι → α
s✝ t✝ s t : Set α
f : β → α
hs : s ⊆ range f
⊢ f ⁻¹' s ⊆ f ⁻¹' t → s ⊆ t

case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.77161
ι : Sort ?u.77164
ι' : Sort ?u.77167
f✝ : ι → α
s✝ t✝ s t : Set α
f : β → α
hs : s ⊆ range f
⊢ s ⊆ t → f ⁻¹' s ⊆ f ⁻¹' t
α : Type u_1
β : Type u_2
γ : Type ?u.77161
ι : Sort ?u.77164
ι' : Sort ?u.77167
f✝ : ι → α
s✝ t✝ s t : Set α
f : β → α
hs : s ⊆ range f
⊢ f ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t
constructor
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.77161
ι : Sort ?u.77164
ι' : Sort ?u.77167
f✝ : ι → α
s✝ t✝ s t : Set α
f : β → α
hs : s ⊆ range f
h : s ⊆ t
x : β
⊢ x ∈ f ⁻¹' s → x ∈ f ⁻¹' t
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.77161
ι : Sort ?u.77164
ι' : Sort ?u.77167
f✝ : ι → α
s✝ t✝ s t : Set α
f : β → α
hs : s ⊆ range f
⊢ s ⊆ t → f ⁻¹' s ⊆ f ⁻¹' t
intro h x
no goals
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.77161
ι : Sort ?u.77164
ι' : Sort ?u.77167
f✝ : ι → α
s✝ t✝ s t : Set α
f : β → α
hs : s ⊆ range f
h : s ⊆ t
x : β
⊢ x ∈ f ⁻¹' s → x ∈ f ⁻¹' t
apply h
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.77161
ι : Sort ?u.77164
ι' : Sort ?u.77167
f✝ : ι → α
s✝ t✝ s t : Set α
f : β → α
hs : s ⊆ range f
h : f ⁻¹' s ⊆ f ⁻¹' t
x : α
hx : x ∈ s
⊢ x ∈ t
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.77161
ι : Sort ?u.77164
ι' : Sort ?u.77167
f✝ : ι → α
s✝ t✝ s t : Set α
f : β → α
hs : s ⊆ range f
⊢ f ⁻¹' s ⊆ f ⁻¹' t → s ⊆ t
intro h x hx
case mp.intro
α : Type u_1
β : Type u_2
γ : Type ?u.77161
ι : Sort ?u.77164
ι' : Sort ?u.77167
f✝ : ι → α
s✝ t✝ s t : Set α
f : β → α
hs : s ⊆ range f
h : f ⁻¹' s ⊆ f ⁻¹' t
y : β
hx : f y ∈ s
⊢ f y ∈ t
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.77161
ι : Sort ?u.77164
ι' : Sort ?u.77167
f✝ : ι → α
s✝ t✝ s t : Set α
f : β → α
hs : s ⊆ range f
h : f ⁻¹' s ⊆ f ⁻¹' t
x : α
hx : x ∈ s
⊢ x ∈ t
rcases hs hx with ⟨y, rfl⟩
no goals
case mp.intro
α : Type u_1
β : Type u_2
γ : Type ?u.77161
ι : Sort ?u.77164
ι' : Sort ?u.77167
f✝ : ι → α
s✝ t✝ s t : Set α
f : β → α
hs : s ⊆ range f
h : f ⁻¹' s ⊆ f ⁻¹' t
y : β
hx : f y ∈ s
⊢ f y ∈ t
exact h hx