case h
α : Type u_1
β : Type u_2
γ : Type ?u.92494
ι : Sort ?u.92497
ι' : Sort ?u.92500
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set α
x✝ : β
⊢ x✝ ∈ f '' s ↔ x✝ ∈ range fun x => f ↑x
α : Type u_1
β : Type u_2
γ : Type ?u.92494
ι : Sort ?u.92497
ι' : Sort ?u.92500
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set α
⊢ f '' s = range fun x => f ↑x
ext
case h.mp
α : Type u_1
β : Type u_2
γ : Type ?u.92494
ι : Sort ?u.92497
ι' : Sort ?u.92500
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set α
x✝ : β
⊢ x✝ ∈ f '' s → x✝ ∈ range fun x => f ↑x

case h.mpr
α : Type u_1
β : Type u_2
γ : Type ?u.92494
ι : Sort ?u.92497
ι' : Sort ?u.92500
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set α
x✝ : β
⊢ (x✝ ∈ range fun x => f ↑x) → x✝ ∈ f '' s
case h
α : Type u_1
β : Type u_2
γ : Type ?u.92494
ι : Sort ?u.92497
ι' : Sort ?u.92500
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set α
x✝ : β
⊢ x✝ ∈ f '' s ↔ x✝ ∈ range fun x => f ↑x
constructor
case h.mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.92494
ι : Sort ?u.92497
ι' : Sort ?u.92500
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set α
x✝ : β
x : α
h1 : x ∈ s
h2 : f x = x✝
⊢ x✝ ∈ range fun x => f ↑x

case h.mpr
α : Type u_1
β : Type u_2
γ : Type ?u.92494
ι : Sort ?u.92497
ι' : Sort ?u.92500
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set α
x✝ : β
⊢ (x✝ ∈ range fun x => f ↑x) → x✝ ∈ f '' s
case h.mp
α : Type u_1
β : Type u_2
γ : Type ?u.92494
ι : Sort ?u.92497
ι' : Sort ?u.92500
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set α
x✝ : β
⊢ x✝ ∈ f '' s → x✝ ∈ range fun x => f ↑x

case h.mpr
α : Type u_1
β : Type u_2
γ : Type ?u.92494
ι : Sort ?u.92497
ι' : Sort ?u.92500
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set α
x✝ : β
⊢ (x✝ ∈ range fun x => f ↑x) → x✝ ∈ f '' s
rintro ⟨x, h1, h2⟩
case h.mpr
α : Type u_1
β : Type u_2
γ : Type ?u.92494
ι : Sort ?u.92497
ι' : Sort ?u.92500
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set α
x✝ : β
⊢ (x✝ ∈ range fun x => f ↑x) → x✝ ∈ f '' s
case h.mp.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.92494
ι : Sort ?u.92497
ι' : Sort ?u.92500
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set α
x✝ : β
x : α
h1 : x ∈ s
h2 : f x = x✝
⊢ x✝ ∈ range fun x => f ↑x

case h.mpr
α : Type u_1
β : Type u_2
γ : Type ?u.92494
ι : Sort ?u.92497
ι' : Sort ?u.92500
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set α
x✝ : β
⊢ (x✝ ∈ range fun x => f ↑x) → x✝ ∈ f '' s
exact ⟨⟨x, h1⟩, h2⟩
case h.mpr.intro.mk
α : Type u_1
β : Type u_2
γ : Type ?u.92494
ι : Sort ?u.92497
ι' : Sort ?u.92500
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set α
x✝ : β
x : α
h1 : x ∈ s
h2 : (fun x => f ↑x) { val := x, property := h1 } = x✝
⊢ x✝ ∈ f '' s
case h.mpr
α : Type u_1
β : Type u_2
γ : Type ?u.92494
ι : Sort ?u.92497
ι' : Sort ?u.92500
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set α
x✝ : β
⊢ (x✝ ∈ range fun x => f ↑x) → x✝ ∈ f '' s
rintro ⟨⟨x, h1⟩, h2⟩
no goals
case h.mpr.intro.mk
α : Type u_1
β : Type u_2
γ : Type ?u.92494
ι : Sort ?u.92497
ι' : Sort ?u.92500
f✝ : ι → α
s✝ t : Set α
f : α → β
s : Set α
x✝ : β
x : α
h1 : x ∈ s
h2 : (fun x => f ↑x) { val := x, property := h1 } = x✝
⊢ x✝ ∈ f '' s
exact ⟨x, h1, h2⟩