case h
α : Type u_1
β : Type u_2
γ : Type ?u.51072
δ : Type ?u.51075
ε : Type ?u.51078
ι : Type ?u.51081
f✝ f : α →. β
s : Set β
x : ↑(Dom f)
⊢ x ∈ asSubtype f ⁻¹' s ↔ x ∈ Subtype.val ⁻¹' preimage f s
α : Type u_1
β : Type u_2
γ : Type ?u.51072
δ : Type ?u.51075
ε : Type ?u.51078
ι : Type ?u.51081
f✝ f : α →. β
s : Set β
⊢ asSubtype f ⁻¹' s = Subtype.val ⁻¹' preimage f s
ext x
case h
α : Type u_1
β : Type u_2
γ : Type ?u.51072
δ : Type ?u.51075
ε : Type ?u.51078
ι : Type ?u.51081
f✝ f : α →. β
s : Set β
x : ↑(Dom f)
⊢ fn f ↑x (_ : ↑x ∈ Dom f) ∈ s ↔ ∃ y, y ∈ s ∧ y ∈ f ↑x
case h
α : Type u_1
β : Type u_2
γ : Type ?u.51072
δ : Type ?u.51075
ε : Type ?u.51078
ι : Type ?u.51081
f✝ f : α →. β
s : Set β
x : ↑(Dom f)
⊢ x ∈ asSubtype f ⁻¹' s ↔ x ∈ Subtype.val ⁻¹' preimage f s
simp only [Set.mem_preimage, Set.mem_setOf_eq, PFun.asSubtype, PFun.mem_preimage]
case h
α : Type u_1
β : Type u_2
γ : Type ?u.51072
δ : Type ?u.51075
ε : Type ?u.51078
ι : Type ?u.51081
f✝ f : α →. β
s : Set β
x : ↑(Dom f)
⊢ fn f ↑x (_ : ↑x ∈ Dom f) ∈ s ↔ ∃ y, y ∈ s ∧ y ∈ f ↑x
case h
α : Type u_1
β : Type u_2
γ : Type ?u.51072
δ : Type ?u.51075
ε : Type ?u.51078
ι : Type ?u.51081
f✝ f : α →. β
s : Set β
x : ↑(Dom f)
⊢ fn f ↑x (_ : ↑x ∈ Dom f) ∈ s ↔ ∃ y, y ∈ s ∧ y ∈ f ↑x
show f.fn x.val _ ∈ s ↔ ∃ y ∈ s, y ∈ f x.val
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.51072
δ : Type ?u.51075
ε : Type ?u.51078
ι : Type ?u.51081
f✝ f : α →. β
s : Set β
x : ↑(Dom f)
⊢ fn f ↑x (_ : ↑x ∈ Dom f) ∈ s ↔ ∃ y, y ∈ s ∧ y ∈ f ↑x
exact
  Iff.intro (fun h => ⟨_, h, Part.get_mem _⟩) fun ⟨y, ys, fxy⟩ =>
    have : f.fn x.val x.property ∈ f x.val := Part.get_mem _
    Part.mem_unique fxy this ▸ ys