case h.mk
α : Type u_2
β : Type u_1
γ : Type ?u.88408
ι : Sort ?u.88411
ι' : Sort ?u.88414
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
⊢ { val := x, property := hx } ∈ range (Subtype.map f h) ↔
    { val := x, property := hx } ∈ Subtype.val ⁻¹' (f '' {x | p x})
α : Type u_2
β : Type u_1
γ : Type ?u.88408
ι : Sort ?u.88411
ι' : Sort ?u.88414
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
⊢ range (Subtype.map f h) = Subtype.val ⁻¹' (f '' {x | p x})
ext ⟨x, hx⟩
case h.mk
α : Type u_2
β : Type u_1
γ : Type ?u.88408
ι : Sort ?u.88411
ι' : Sort ?u.88414
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
⊢ (∃ a b, Subtype.map f h { val := a, property := b } = { val := x, property := hx }) ↔
    ∃ x_1, x_1 ∈ {x | p x} ∧ f x_1 = x
case h.mk
α : Type u_2
β : Type u_1
γ : Type ?u.88408
ι : Sort ?u.88411
ι' : Sort ?u.88414
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
⊢ { val := x, property := hx } ∈ range (Subtype.map f h) ↔
    { val := x, property := hx } ∈ Subtype.val ⁻¹' (f '' {x | p x})
rw [mem_preimage, mem_range, mem_image, Subtype.exists, Subtype.coe_mk]
case h.mk.mp
α : Type u_2
β : Type u_1
γ : Type ?u.88408
ι : Sort ?u.88411
ι' : Sort ?u.88414
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
⊢ (∃ a b, Subtype.map f h { val := a, property := b } = { val := x, property := hx }) →
    ∃ x_1, x_1 ∈ {x | p x} ∧ f x_1 = x

case h.mk.mpr
α : Type u_2
β : Type u_1
γ : Type ?u.88408
ι : Sort ?u.88411
ι' : Sort ?u.88414
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
⊢ (∃ x_1, x_1 ∈ {x | p x} ∧ f x_1 = x) →
    ∃ a b, Subtype.map f h { val := a, property := b } = { val := x, property := hx }
case h.mk
α : Type u_2
β : Type u_1
γ : Type ?u.88408
ι : Sort ?u.88411
ι' : Sort ?u.88414
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
⊢ (∃ a b, Subtype.map f h { val := a, property := b } = { val := x, property := hx }) ↔
    ∃ x_1, x_1 ∈ {x | p x} ∧ f x_1 = x
apply Iff.intro
case h.mk.mpr
α : Type u_2
β : Type u_1
γ : Type ?u.88408
ι : Sort ?u.88411
ι' : Sort ?u.88414
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
⊢ (∃ x_1, x_1 ∈ {x | p x} ∧ f x_1 = x) →
    ∃ a b, Subtype.map f h { val := a, property := b } = { val := x, property := hx }
case h.mk.mp
α : Type u_2
β : Type u_1
γ : Type ?u.88408
ι : Sort ?u.88411
ι' : Sort ?u.88414
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
⊢ (∃ a b, Subtype.map f h { val := a, property := b } = { val := x, property := hx }) →
    ∃ x_1, x_1 ∈ {x | p x} ∧ f x_1 = x

case h.mk.mpr
α : Type u_2
β : Type u_1
γ : Type ?u.88408
ι : Sort ?u.88411
ι' : Sort ?u.88414
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
⊢ (∃ x_1, x_1 ∈ {x | p x} ∧ f x_1 = x) →
    ∃ a b, Subtype.map f h { val := a, property := b } = { val := x, property := hx }
. rintro ⟨a, b, hab⟩
  rw [Subtype.map, Subtype.mk.injEq] at hab
  use a
  trivial
no goals
case h.mk.mpr
α : Type u_2
β : Type u_1
γ : Type ?u.88408
ι : Sort ?u.88411
ι' : Sort ?u.88414
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
⊢ (∃ x_1, x_1 ∈ {x | p x} ∧ f x_1 = x) →
    ∃ a b, Subtype.map f h { val := a, property := b } = { val := x, property := hx }
. rintro ⟨a, b, hab⟩
  use a
  use b
  rw [Subtype.map, Subtype.mk.injEq]
  exact hab
case h.mk.mp.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.88408
ι : Sort ?u.88411
ι' : Sort ?u.88414
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
a : α
b : p a
hab : Subtype.map f h { val := a, property := b } = { val := x, property := hx }
⊢ ∃ x_1, x_1 ∈ {x | p x} ∧ f x_1 = x
case h.mk.mp
α : Type u_2
β : Type u_1
γ : Type ?u.88408
ι : Sort ?u.88411
ι' : Sort ?u.88414
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
⊢ (∃ a b, Subtype.map f h { val := a, property := b } = { val := x, property := hx }) →
    ∃ x_1, x_1 ∈ {x | p x} ∧ f x_1 = x
rintro ⟨a, b, hab⟩
case h.mk.mp.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.88408
ι : Sort ?u.88411
ι' : Sort ?u.88414
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
a : α
b : p a
hab : f ↑{ val := a, property := b } = x
⊢ ∃ x_1, x_1 ∈ {x | p x} ∧ f x_1 = x
case h.mk.mp.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.88408
ι : Sort ?u.88411
ι' : Sort ?u.88414
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
a : α
b : p a
hab : Subtype.map f h { val := a, property := b } = { val := x, property := hx }
⊢ ∃ x_1, x_1 ∈ {x | p x} ∧ f x_1 = x
rw [Subtype.map, Subtype.mk.injEq] at hab
case h.mk.mp.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.88408
ι : Sort ?u.88411
ι' : Sort ?u.88414
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
a : α
b : p a
hab : f ↑{ val := a, property := b } = x
⊢ a ∈ {x | p x} ∧ f a = x
case h.mk.mp.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.88408
ι : Sort ?u.88411
ι' : Sort ?u.88414
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
a : α
b : p a
hab : f ↑{ val := a, property := b } = x
⊢ ∃ x_1, x_1 ∈ {x | p x} ∧ f x_1 = x
use a
no goals
case h.mk.mp.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.88408
ι : Sort ?u.88411
ι' : Sort ?u.88414
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
a : α
b : p a
hab : f ↑{ val := a, property := b } = x
⊢ a ∈ {x | p x} ∧ f a = x
trivial
case h.mk.mpr.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.88408
ι : Sort ?u.88411
ι' : Sort ?u.88414
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
a : α
b : a ∈ {x | p x}
hab : f a = x
⊢ ∃ a b, Subtype.map f h { val := a, property := b } = { val := x, property := hx }
case h.mk.mpr
α : Type u_2
β : Type u_1
γ : Type ?u.88408
ι : Sort ?u.88411
ι' : Sort ?u.88414
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
⊢ (∃ x_1, x_1 ∈ {x | p x} ∧ f x_1 = x) →
    ∃ a b, Subtype.map f h { val := a, property := b } = { val := x, property := hx }
rintro ⟨a, b, hab⟩
case h.mk.mpr.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.88408
ι : Sort ?u.88411
ι' : Sort ?u.88414
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
a : α
b : a ∈ {x | p x}
hab : f a = x
⊢ ∃ b, Subtype.map f h { val := a, property := b } = { val := x, property := hx }
case h.mk.mpr.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.88408
ι : Sort ?u.88411
ι' : Sort ?u.88414
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
a : α
b : a ∈ {x | p x}
hab : f a = x
⊢ ∃ a b, Subtype.map f h { val := a, property := b } = { val := x, property := hx }
use a
case h.mk.mpr.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.88408
ι : Sort ?u.88411
ι' : Sort ?u.88414
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
a : α
b : a ∈ {x | p x}
hab : f a = x
⊢ Subtype.map f h { val := a, property := b } = { val := x, property := hx }
case h.mk.mpr.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.88408
ι : Sort ?u.88411
ι' : Sort ?u.88414
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
a : α
b : a ∈ {x | p x}
hab : f a = x
⊢ ∃ b, Subtype.map f h { val := a, property := b } = { val := x, property := hx }
use b
case h.mk.mpr.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.88408
ι : Sort ?u.88411
ι' : Sort ?u.88414
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
a : α
b : a ∈ {x | p x}
hab : f a = x
⊢ f ↑{ val := a, property := b } = x
case h.mk.mpr.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.88408
ι : Sort ?u.88411
ι' : Sort ?u.88414
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
a : α
b : a ∈ {x | p x}
hab : f a = x
⊢ Subtype.map f h { val := a, property := b } = { val := x, property := hx }
rw [Subtype.map, Subtype.mk.injEq]
no goals
case h.mk.mpr.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.88408
ι : Sort ?u.88411
ι' : Sort ?u.88414
f✝ : ι → α
s t : Set α
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
a : α
b : a ∈ {x | p x}
hab : f a = x
⊢ f ↑{ val := a, property := b } = x
exact hab