α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
⊢ Nonempty (↑s ↪ ↑(f ⁻¹' s))
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
⊢ lift (#↑s) ≤ lift (#↑(f ⁻¹' s))
rw [lift_mk_le.{v, u, 0}]
case refine'_1
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
⊢ ↑s → ↑(f ⁻¹' s)

case refine'_2
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
⊢ Injective ?refine'_1
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
⊢ Nonempty (↑s ↪ ↑(f ⁻¹' s))
refine' ⟨⟨_, _⟩⟩
case refine'_2.mk.mk
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
y : β
hy : y ∈ s
y' : β
hy' : y' ∈ s
⊢ (fun a =>
          Subtype.casesOn a fun y hy =>
            Subtype.casesOn (subtype_of_exists (_ : y ∈ range f)) fun x property =>
              Eq.ndrec (motive := fun y => y ∈ s → ↑(f ⁻¹' s)) (fun hy => { val := x, property := hy }) property hy)
        { val := y, property := hy } =
      (fun a =>
          Subtype.casesOn a fun y hy =>
            Subtype.casesOn (subtype_of_exists (_ : y ∈ range f)) fun x property =>
              Eq.ndrec (motive := fun y => y ∈ s → ↑(f ⁻¹' s)) (fun hy => { val := x, property := hy }) property hy)
        { val := y', property := hy' } →
    { val := y, property := hy } = { val := y', property := hy' }
case refine'_2
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
⊢ Injective fun a =>
    Subtype.casesOn a fun y hy =>
      Subtype.casesOn (subtype_of_exists (_ : y ∈ range f)) fun x property =>
        Eq.ndrec (motive := fun y => y ∈ s → ↑(f ⁻¹' s)) (fun hy => { val := x, property := hy }) property hy
rintro ⟨y, hy⟩ ⟨y', hy'⟩
case refine'_2.mk.mk
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
y : β
hy : y ∈ s
y' : β
hy' : y' ∈ s
⊢ Eq.rec (motive := fun x x_1 => x ∈ s → ↑(f ⁻¹' s))
        (fun hy_1 => { val := ↑(subtype_of_exists (_ : y ∈ range f)), property := hy_1 })
        (_ : f ↑(subtype_of_exists (_ : y ∈ range f)) = y) hy =
      Eq.rec (motive := fun x x_1 => x ∈ s → ↑(f ⁻¹' s))
        (fun hy => { val := ↑(subtype_of_exists (_ : y' ∈ range f)), property := hy })
        (_ : f ↑(subtype_of_exists (_ : y' ∈ range f)) = y') hy' →
    { val := y, property := hy } = { val := y', property := hy' }
case refine'_2.mk.mk
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
y : β
hy : y ∈ s
y' : β
hy' : y' ∈ s
⊢ (fun a =>
          Subtype.casesOn a fun y hy =>
            Subtype.casesOn (subtype_of_exists (_ : y ∈ range f)) fun x property =>
              Eq.ndrec (motive := fun y => y ∈ s → ↑(f ⁻¹' s)) (fun hy => { val := x, property := hy }) property hy)
        { val := y, property := hy } =
      (fun a =>
          Subtype.casesOn a fun y hy =>
            Subtype.casesOn (subtype_of_exists (_ : y ∈ range f)) fun x property =>
              Eq.ndrec (motive := fun y => y ∈ s → ↑(f ⁻¹' s)) (fun hy => { val := x, property := hy }) property hy)
        { val := y', property := hy' } →
    { val := y, property := hy } = { val := y', property := hy' }
dsimp
case refine'_2.mk.mk.mk
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
y' : β
hy' : y' ∈ s
x : α
hy : f x ∈ s
⊢ Eq.rec (motive := fun x_1 x => x_1 ∈ s → ↑(f ⁻¹' s))
        (fun hy => { val := ↑{ val := x, property := (_ : f x = f x) }, property := hy })
        (_ : f ↑{ val := x, property := (_ : f x = f x) } = f x) hy =
      Eq.rec (motive := fun x x_1 => x ∈ s → ↑(f ⁻¹' s))
        (fun hy => { val := ↑(subtype_of_exists (_ : y' ∈ range f)), property := hy })
        (_ : f ↑(subtype_of_exists (_ : y' ∈ range f)) = y') hy' →
    { val := f x, property := hy } = { val := y', property := hy' }
case refine'_2.mk.mk
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
y : β
hy : y ∈ s
y' : β
hy' : y' ∈ s
⊢ Eq.rec (motive := fun x x_1 => x ∈ s → ↑(f ⁻¹' s))
        (fun hy_1 => { val := ↑(subtype_of_exists (_ : y ∈ range f)), property := hy_1 })
        (_ : f ↑(subtype_of_exists (_ : y ∈ range f)) = y) hy =
      Eq.rec (motive := fun x x_1 => x ∈ s → ↑(f ⁻¹' s))
        (fun hy => { val := ↑(subtype_of_exists (_ : y' ∈ range f)), property := hy })
        (_ : f ↑(subtype_of_exists (_ : y' ∈ range f)) = y') hy' →
    { val := y, property := hy } = { val := y', property := hy' }
rcases Classical.subtype_of_exists (h hy) with ⟨x, rfl⟩
case refine'_2.mk.mk.mk.mk
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
x : α
hy : f x ∈ s
x' : α
hy' : f x' ∈ s
⊢ Eq.rec (motive := fun x_1 x => x_1 ∈ s → ↑(f ⁻¹' s))
        (fun hy => { val := ↑{ val := x, property := (_ : f x = f x) }, property := hy })
        (_ : f ↑{ val := x, property := (_ : f x = f x) } = f x) hy =
      Eq.rec (motive := fun x x_1 => x ∈ s → ↑(f ⁻¹' s))
        (fun hy => { val := ↑{ val := x', property := (_ : f x' = f x') }, property := hy })
        (_ : f ↑{ val := x', property := (_ : f x' = f x') } = f x') hy' →
    { val := f x, property := hy } = { val := f x', property := hy' }
case refine'_2.mk.mk.mk
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
y' : β
hy' : y' ∈ s
x : α
hy : f x ∈ s
⊢ Eq.rec (motive := fun x_1 x => x_1 ∈ s → ↑(f ⁻¹' s))
        (fun hy => { val := ↑{ val := x, property := (_ : f x = f x) }, property := hy })
        (_ : f ↑{ val := x, property := (_ : f x = f x) } = f x) hy =
      Eq.rec (motive := fun x x_1 => x ∈ s → ↑(f ⁻¹' s))
        (fun hy => { val := ↑(subtype_of_exists (_ : y' ∈ range f)), property := hy })
        (_ : f ↑(subtype_of_exists (_ : y' ∈ range f)) = y') hy' →
    { val := f x, property := hy } = { val := y', property := hy' }
rcases Classical.subtype_of_exists (h hy') with ⟨x', rfl⟩
case refine'_2.mk.mk.mk.mk
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
x : α
hy : f x ∈ s
x' : α
hy' : f x' ∈ s
⊢ x = x' → f x = f x'
case refine'_2.mk.mk.mk.mk
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
x : α
hy : f x ∈ s
x' : α
hy' : f x' ∈ s
⊢ Eq.rec (motive := fun x_1 x => x_1 ∈ s → ↑(f ⁻¹' s))
        (fun hy => { val := ↑{ val := x, property := (_ : f x = f x) }, property := hy })
        (_ : f ↑{ val := x, property := (_ : f x = f x) } = f x) hy =
      Eq.rec (motive := fun x x_1 => x ∈ s → ↑(f ⁻¹' s))
        (fun hy => { val := ↑{ val := x', property := (_ : f x' = f x') }, property := hy })
        (_ : f ↑{ val := x', property := (_ : f x' = f x') } = f x') hy' →
    { val := f x, property := hy } = { val := f x', property := hy' }
simp
case refine'_2.mk.mk.mk.mk
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
x : α
hy : f x ∈ s
x' : α
hy' : f x' ∈ s
hxx' : x = x'
⊢ f x = f x'
case refine'_2.mk.mk.mk.mk
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
x : α
hy : f x ∈ s
x' : α
hy' : f x' ∈ s
⊢ x = x' → f x = f x'
intro hxx'
no goals
case refine'_2.mk.mk.mk.mk
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
x : α
hy : f x ∈ s
x' : α
hy' : f x' ∈ s
hxx' : x = x'
⊢ f x = f x'
rw [hxx']
case refine'_1.mk
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
y : β
hy : y ∈ s
⊢ ↑(f ⁻¹' s)
case refine'_1
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
⊢ ↑s → ↑(f ⁻¹' s)
rintro ⟨y, hy⟩
case refine'_1.mk.mk
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
x : α
hy : f x ∈ s
⊢ ↑(f ⁻¹' s)
case refine'_1.mk
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
y : β
hy : y ∈ s
⊢ ↑(f ⁻¹' s)
rcases Classical.subtype_of_exists (h hy) with ⟨x, rfl⟩
no goals
case refine'_1.mk.mk
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
x : α
hy : f x ∈ s
⊢ ↑(f ⁻¹' s)
exact ⟨x, hy⟩