case h.mk
α : Type u_1
β : Type ?u.97081
γ : Type ?u.97084
ι : Sort ?u.97087
ι' : Sort ?u.97090
f : ι → α
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
⊢ { val := x, property := hx } ∈ range (inclusion h) ↔ { val := x, property := hx } ∈ {x | ↑x ∈ s}
α : Type u_1
β : Type ?u.97081
γ : Type ?u.97084
ι : Sort ?u.97087
ι' : Sort ?u.97090
f : ι → α
s t : Set α
h : s ⊆ t
⊢ range (inclusion h) = {x | ↑x ∈ s}
ext ⟨x, hx⟩
case h.mk.mp
α : Type u_1
β : Type ?u.97081
γ : Type ?u.97084
ι : Sort ?u.97087
ι' : Sort ?u.97090
f : ι → α
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
⊢ { val := x, property := hx } ∈ range (inclusion h) → { val := x, property := hx } ∈ {x | ↑x ∈ s}

case h.mk.mpr
α : Type u_1
β : Type ?u.97081
γ : Type ?u.97084
ι : Sort ?u.97087
ι' : Sort ?u.97090
f : ι → α
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
⊢ { val := x, property := hx } ∈ {x | ↑x ∈ s} → { val := x, property := hx } ∈ range (inclusion h)
case h.mk
α : Type u_1
β : Type ?u.97081
γ : Type ?u.97084
ι : Sort ?u.97087
ι' : Sort ?u.97090
f : ι → α
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
⊢ { val := x, property := hx } ∈ range (inclusion h) ↔ { val := x, property := hx } ∈ {x | ↑x ∈ s}
apply Iff.intro
case h.mk.mpr
α : Type u_1
β : Type ?u.97081
γ : Type ?u.97084
ι : Sort ?u.97087
ι' : Sort ?u.97090
f : ι → α
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
⊢ { val := x, property := hx } ∈ {x | ↑x ∈ s} → { val := x, property := hx } ∈ range (inclusion h)
case h.mk.mp
α : Type u_1
β : Type ?u.97081
γ : Type ?u.97084
ι : Sort ?u.97087
ι' : Sort ?u.97090
f : ι → α
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
⊢ { val := x, property := hx } ∈ range (inclusion h) → { val := x, property := hx } ∈ {x | ↑x ∈ s}

case h.mk.mpr
α : Type u_1
β : Type ?u.97081
γ : Type ?u.97084
ι : Sort ?u.97087
ι' : Sort ?u.97090
f : ι → α
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
⊢ { val := x, property := hx } ∈ {x | ↑x ∈ s} → { val := x, property := hx } ∈ range (inclusion h)
. rw [mem_range]
  rintro ⟨a, ha⟩
  rw [inclusion, Subtype.mk.injEq] at ha
  rw [mem_setOf, Subtype.coe_mk, ← ha]
  exact Subtype.coe_prop _
no goals
case h.mk.mpr
α : Type u_1
β : Type ?u.97081
γ : Type ?u.97084
ι : Sort ?u.97087
ι' : Sort ?u.97090
f : ι → α
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
⊢ { val := x, property := hx } ∈ {x | ↑x ∈ s} → { val := x, property := hx } ∈ range (inclusion h)
. rw [mem_setOf, Subtype.coe_mk, mem_range]
  intro hx'
  use ⟨x, hx'⟩
  trivial
case h.mk.mp
α : Type u_1
β : Type ?u.97081
γ : Type ?u.97084
ι : Sort ?u.97087
ι' : Sort ?u.97090
f : ι → α
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
⊢ (∃ y, inclusion h y = { val := x, property := hx }) → { val := x, property := hx } ∈ {x | ↑x ∈ s}
case h.mk.mp
α : Type u_1
β : Type ?u.97081
γ : Type ?u.97084
ι : Sort ?u.97087
ι' : Sort ?u.97090
f : ι → α
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
⊢ { val := x, property := hx } ∈ range (inclusion h) → { val := x, property := hx } ∈ {x | ↑x ∈ s}
rw [mem_range]
case h.mk.mp.intro
α : Type u_1
β : Type ?u.97081
γ : Type ?u.97084
ι : Sort ?u.97087
ι' : Sort ?u.97090
f : ι → α
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
a : ↑s
ha : inclusion h a = { val := x, property := hx }
⊢ { val := x, property := hx } ∈ {x | ↑x ∈ s}
case h.mk.mp
α : Type u_1
β : Type ?u.97081
γ : Type ?u.97084
ι : Sort ?u.97087
ι' : Sort ?u.97090
f : ι → α
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
⊢ (∃ y, inclusion h y = { val := x, property := hx }) → { val := x, property := hx } ∈ {x | ↑x ∈ s}
rintro ⟨a, ha⟩
case h.mk.mp.intro
α : Type u_1
β : Type ?u.97081
γ : Type ?u.97084
ι : Sort ?u.97087
ι' : Sort ?u.97090
f : ι → α
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
a : ↑s
ha : ↑a = x
⊢ { val := x, property := hx } ∈ {x | ↑x ∈ s}
case h.mk.mp.intro
α : Type u_1
β : Type ?u.97081
γ : Type ?u.97084
ι : Sort ?u.97087
ι' : Sort ?u.97090
f : ι → α
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
a : ↑s
ha : inclusion h a = { val := x, property := hx }
⊢ { val := x, property := hx } ∈ {x | ↑x ∈ s}
rw [inclusion, Subtype.mk.injEq] at ha
case h.mk.mp.intro
α : Type u_1
β : Type ?u.97081
γ : Type ?u.97084
ι : Sort ?u.97087
ι' : Sort ?u.97090
f : ι → α
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
a : ↑s
ha : ↑a = x
⊢ ↑a ∈ s
case h.mk.mp.intro
α : Type u_1
β : Type ?u.97081
γ : Type ?u.97084
ι : Sort ?u.97087
ι' : Sort ?u.97090
f : ι → α
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
a : ↑s
ha : ↑a = x
⊢ { val := x, property := hx } ∈ {x | ↑x ∈ s}
rw [mem_setOf, Subtype.coe_mk, ← ha]
no goals
case h.mk.mp.intro
α : Type u_1
β : Type ?u.97081
γ : Type ?u.97084
ι : Sort ?u.97087
ι' : Sort ?u.97090
f : ι → α
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
a : ↑s
ha : ↑a = x
⊢ ↑a ∈ s
exact Subtype.coe_prop _
case h.mk.mpr
α : Type u_1
β : Type ?u.97081
γ : Type ?u.97084
ι : Sort ?u.97087
ι' : Sort ?u.97090
f : ι → α
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
⊢ x ∈ s → ∃ y, inclusion h y = { val := x, property := hx }
case h.mk.mpr
α : Type u_1
β : Type ?u.97081
γ : Type ?u.97084
ι : Sort ?u.97087
ι' : Sort ?u.97090
f : ι → α
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
⊢ { val := x, property := hx } ∈ {x | ↑x ∈ s} → { val := x, property := hx } ∈ range (inclusion h)
rw [mem_setOf, Subtype.coe_mk, mem_range]
case h.mk.mpr
α : Type u_1
β : Type ?u.97081
γ : Type ?u.97084
ι : Sort ?u.97087
ι' : Sort ?u.97090
f : ι → α
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
hx' : x ∈ s
⊢ ∃ y, inclusion h y = { val := x, property := hx }
case h.mk.mpr
α : Type u_1
β : Type ?u.97081
γ : Type ?u.97084
ι : Sort ?u.97087
ι' : Sort ?u.97090
f : ι → α
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
⊢ x ∈ s → ∃ y, inclusion h y = { val := x, property := hx }
intro hx'
case h.mk.mpr
α : Type u_1
β : Type ?u.97081
γ : Type ?u.97084
ι : Sort ?u.97087
ι' : Sort ?u.97090
f : ι → α
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
hx' : x ∈ s
⊢ inclusion h { val := x, property := hx' } = { val := x, property := hx }
case h.mk.mpr
α : Type u_1
β : Type ?u.97081
γ : Type ?u.97084
ι : Sort ?u.97087
ι' : Sort ?u.97090
f : ι → α
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
hx' : x ∈ s
⊢ ∃ y, inclusion h y = { val := x, property := hx }
use ⟨x, hx'⟩
no goals
case h.mk.mpr
α : Type u_1
β : Type ?u.97081
γ : Type ?u.97084
ι : Sort ?u.97087
ι' : Sort ?u.97090
f : ι → α
s t : Set α
h : s ⊆ t
x : α
hx : x ∈ t
hx' : x ∈ s
⊢ inclusion h { val := x, property := hx' } = { val := x, property := hx }
trivial