awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
f g : α → β
s : Set α
inst : (x : α) → Decidable (x ∈ s)
⊢ sᶜ.restrict (π := fun (i : α) ↦ β) (s.piecewise (β := fun (i : α) ↦ β) f g) = sᶜ.restrict (π := fun (a : α) ↦ β) g

Tactic:
restrict_ite_compl _ _ _

Premises used: Set.restrict_ite_compl, Set.piecewise
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
⊢ (range f).restrict (π := fun (a : β) ↦ γ) (extend f g g') = fun (x : (↑(range f) : Type u_2)) ↦
    g (Exists.choose (p := fun (y : α) ↦ f y = (↑x : β)) ⋯)

Tactic:
restrict_dite _ _

Premises used: Set.restrict_dite, Set.Mem, setOf, Function.extend, Set.range
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
⊢ (range f).restrict (π := fun (a : β) ↦ γ) (extend f g g') = fun (x : (↑(range f) : Type u_2)) ↦
    g (Exists.choose (p := fun (y : α) ↦ f y = (↑x : β)) ⋯)

Tactic:
exact restrict_dite _ _

Premises used: Set.restrict_dite
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
⊢ (range f).restrict (π := fun (a : β) ↦ γ) (extend f g g') = fun (x : (↑(range f) : Type u_2)) ↦
    g (Exists.choose (p := fun (y : α) ↦ f y = (↑x : β)) ⋯)

Tactic:
classical
  exact restrict_dite _ _

Premises used: Set.restrict_dite
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
⊢ (range f)ᶜ.restrict (π := fun (a : β) ↦ γ) (extend f g g') = g' ∘ Subtype.val (p := fun (x : β) ↦ x ∈ (range f)ᶜ)

Tactic:
restrict_dite_compl _ _

Premises used: Set.Mem, setOf, Set.restrict_dite_compl, Function.extend, Set.range
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
⊢ (range f)ᶜ.restrict (π := fun (a : β) ↦ γ) (extend f g g') = g' ∘ Subtype.val (p := fun (x : β) ↦ x ∈ (range f)ᶜ)

Tactic:
exact restrict_dite_compl _ _

Premises used: Set.restrict_dite_compl
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
⊢ (range f)ᶜ.restrict (π := fun (a : β) ↦ γ) (extend f g g') = g' ∘ Subtype.val (p := fun (x : β) ↦ x ∈ (range f)ᶜ)

Tactic:
classical
  exact restrict_dite_compl _ _

Premises used: Set.restrict_dite_compl
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
π : α → Type u_6
s t : Set α
hst : s ⊆ t
⊢ Eq (α := (f : (a : (↑t : Type u_1)) → π (↑a : α)) → (a : (↑s : Type u_1)) → π (↑a : α))
    (restrict₂ (π := π) (s := s) (t := t) hst) fun (f : (a : (↑t : Type u_1)) → π (↑a : α)) (x : (↑s : Type u_1)) ↦
    f (Subtype.mk (p := fun (x : α) ↦ x ∈ t) (↑x : α) ⋯)

Tactic:
rfl

Premises used: Set.restrict₂, rfl
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
π : α → Type u_6
s t : Set α
hst : s ⊆ t
⊢ Eq (α := ((a : α) → π a) → (a : (↑s : Type u_1)) → π (↑a : α))
    (restrict₂ (π := π) (s := s) (t := t) hst ∘ t.restrict (π := π)) (s.restrict (π := π))

Tactic:
rfl

Premises used: Set.restrict₂, Set.restrict, rfl
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
π : α → Type u_6
s t u : Set α
hst : s ⊆ t
htu : t ⊆ u
⊢ Eq (α := ((a : (↑u : Type u_1)) → π (↑a : α)) → (a : (↑s : Type u_1)) → π (↑a : α))
    (restrict₂ (π := π) (s := s) (t := t) hst ∘ restrict₂ (π := π) (s := t) (t := u) htu)
    (restrict₂ (π := π) (s := s) (t := u) ⋯)

Tactic:
rfl

Premises used: Set.restrict₂, rfl
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
y : β
pos : ∀ (h : ∃ (a : α), f a = y), g (Classical.choose (p := fun (x : α) ↦ f x = y) h) ∈ range g ∪ g' '' (range f)ᶜ
neg : ∀ (h : ¬∃ (a : α), f a = y), g' y ∈ range g ∪ g' '' (range f)ᶜ
⊢ (if h : ∃ (a : α), f a = y then g (Classical.choose (p := fun (x : α) ↦ f x = y) h) else g' y) ∈
    range g ∪ g' '' (range f)ᶜ

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
y : β
h : ∃ (a : α), f a = y
⊢ g (Classical.choose (p := fun (x : α) ↦ f x = y) h) ∈ range g ∪ g' '' (range f)ᶜ

Tactic:
Or.inl (mem_range_self _)

Premises used: Set.mem_range_self, Set.union, Set.Mem, setOf, Or.inl
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
y : β
h : ¬∃ (a : α), f a = y
⊢ g' y ∈ range g ∪ g' '' (range f)ᶜ

Tactic:
Or.inr (mem_image_of_mem _ h)

Premises used: Set.union, Set.Mem, setOf, Set.mem_image_of_mem, Or.inr
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
y : β
h : ∃ (a : α), f a = y
⊢ g (Classical.choose (p := fun (x : α) ↦ f x = y) h) ∈ range g ∪ g' '' (range f)ᶜ

Tactic:
exacts [Or.inl (mem_range_self _), Or.inr (mem_image_of_mem _ h)]

Premises used: Set.mem_range_self, Set.mem_image_of_mem, Or.inl, Or.inr
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : α → γ
g' : β → γ
rintro : ∀ (y : β), extend f g g' y ∈ range g ∪ g' '' (range f)ᶜ
rintro₁ :
  ∀ (y : β),
    (if h : ∃ (a : α), f a = y then g (Classical.choose (p := fun (x : α) ↦ f x = y) h) else g' y) ∈
      range g ∪ g' '' (range f)ᶜ
pos :
  ∀ (y : β) (h : ∃ (a : α), f a = y), g (Classical.choose (p := fun (x : α) ↦ f x = y) h) ∈ range g ∪ g' '' (range f)ᶜ
neg : ∀ (y : β) (h : ¬∃ (a : α), f a = y), g' y ∈ range g ∪ g' '' (range f)ᶜ
⊢ range (extend f g g') ⊆ range g ∪ g' '' (range f)ᶜ

Tactic:
classical
  rintro _ ⟨y, rfl⟩
  rw [extend_def]
  split_ifs with h
  exacts [Or.inl (mem_range_self _), Or.inr (mem_image_of_mem _ h)]

Premises used: Set.mem_range_self, Function.extend_def, Or.inl, rfl
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Injective f
g : α → γ
g' : β → γ
⊢ range (extend f g g') = range g ∪ g' '' (range f)ᶜ

Tactic:
(range_extend_subset _ _ _).antisymm ?_

Premises used: Set.range_extend_subset, HasSubset.Subset.antisymm
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Injective f
g : α → γ
g' : β → γ
refine : range g ∪ g' '' (range f)ᶜ ⊆ range (extend f g g')
⊢ range (extend f g g') = range g ∪ g' '' (range f)ᶜ

Tactic:
refine (range_extend_subset _ _ _).antisymm ?_

Premises used: Set.range_extend_subset, HasSubset.Subset.antisymm
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Injective f
g : α → γ
g' : β → γ
x : α
⊢ g x ∈ range (extend f g g')

Tactic:
⟨f x, hf.extend_apply _ _ _⟩

Premises used: Set.Mem, setOf, Function.Injective.extend_apply, Exists.intro, Set.range
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Injective f
g : α → γ
g' : β → γ
y : β
hy : y ∈ (range f)ᶜ
⊢ g' y ∈ range (extend f g g')

Tactic:
⟨y, extend_apply' _ _ _ hy⟩

Premises used: Set.Mem, setOf, Exists.intro, Function.extend_apply', Set.range
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
hf : Injective f
g : α → γ
g' : β → γ
x : α
⊢ g x ∈ range (extend f g g')

Tactic:
exacts [⟨f x, hf.extend_apply _ _ _⟩, ⟨y, extend_apply' _ _ _ hy⟩]
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
ι : Sort u_5
f : ι → α
s : Set α
h : ∀ (x : ι), f x ∈ s
x : ι
⊢ (↑(codRestrict f s h x) : α) = f x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : ι → α
g : α → β
b : Set α
h : ∀ (x : ι), f x ∈ b
⊢ b.restrict (π := fun (a : α) ↦ β) g ∘ codRestrict f b h = g ∘ f

Tactic:
rfl

Premises used: Set.restrict, rfl
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
ι : Sort u_5
f : ι → α
s : Set α
h : ∀ (x : ι), f x ∈ s
⊢ Injective (codRestrict f s h) ↔ Injective f

Tactic:
simp only [Injective, Subtype.ext_iff, val_codRestrict_apply]

Premises used: Subtype.ext_iff, Function.Injective, Set.val_codRestrict_apply
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
ι : Sort u_5
f : ι → α
s : Set α
h : ∀ (x : ι), f x ∈ s
h₁ :
  ∀ (x : (↑s : Type u_1)),
    x ∈ range (codRestrict f s h) ↔
      Membership.mem (γ := Set (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' range f) x
⊢ range (codRestrict f s h) = Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' range f

Tactic:
ext
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
ι : Sort u_5
f : ι → α
s : Set α
h : ∀ (x : ι), f x ∈ s
x : (↑s : Type u_1)
⊢ x ∈ range (codRestrict f s h) ↔
    Membership.mem (γ := Set (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' range f) x

Tactic:
simp [Subtype.ext_iff]

Premises used: Subtype.ext_iff
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
ι : Sort u_5
f : ι → α
s : Set α
h : ∀ (x : ι), f x ∈ s
⊢ Surjective (codRestrict f s h) ↔ range f = s

Tactic:
simp [← range_eq_univ, Subset.antisymm_iff (a := range f), range_subset_iff, h]

Premises used: Set.range_eq_univ, Set.Subset.antisymm_iff, Set.range_subset_iff
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
ι : Sort u_5
f : ι → α
a : ι
⊢ ∃ (a_1 : ι), codRestrict f (range f) ⋯ a_1 = Subtype.mk (p := fun (x : α) ↦ x ∈ range f) (f a) ⋯

Tactic:
⟨a, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
ι : Sort u_5
f : ι → α
a : ι
⊢ ∃ (a_1 : ι), codRestrict f (range f) ⋯ a_1 = Subtype.mk (p := fun (x : α) ↦ x ∈ range f) (f a) ⋯

Tactic:
exact ⟨a, rfl⟩
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
⊢ s.restrict (π := fun (a : α) ↦ β) f₁ = s.restrict (π := fun (a : α) ↦ β) f₂ ↔ EqOn f₁ f₂ s

Tactic:
restrict_eq_iff

Premises used: Set.EqOn, Set.restrict_eq_iff, Set.restrict
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
h : MapsTo f s t
⊢ Subtype.val (p := fun (x : β) ↦ x ∈ t) ∘ restrict f s t h = f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ s)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
x : (↑s : Type u_1)
⊢ (↑(restrict f s t h x) : β) = f (↑x : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
s : Set α
f : α → α
h : MapsTo f s s
x : (↑s : Type u_1)
⊢ (↑((restrict f s s h)^[0] x) : α) = f^[0] (↑x : α)

Tactic:
simp
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
s : Set α
f : α → α
h : MapsTo f s s
x : (↑s : Type u_1)
k : ℕ
ih : (↑((restrict f s s h)^[k] x) : α) = f^[k] (↑x : α)
⊢ (↑((restrict f s s h)^[k + 1] x) : α) = f^[k + 1] (↑x : α)

Tactic:
simp only [iterate_succ', comp_apply, val_restrict_apply, ih]

Premises used: Set.MapsTo.val_restrict_apply, Function.iterate_succ', Function.comp_apply
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
s : Set α
f : α → α
h : MapsTo f s s
x : (↑s : Type u_1)
k : ℕ
zero : (↑((restrict f s s h)^[0] x) : α) = f^[0] (↑x : α)
succ :
  ∀ (k : ℕ) (ih : (↑((restrict f s s h)^[k] x) : α) = f^[k] (↑x : α)),
    (↑((restrict f s s h)^[k + 1] x) : α) = f^[k + 1] (↑x : α)
⊢ (↑((restrict f s s h)^[k] x) : α) = f^[k] (↑x : α)

Tactic:
induction k with
  | zero => simp
  | succ k ih => simp only [iterate_succ', comp_apply, val_restrict_apply, ih]

Premises used: Set.MapsTo.val_restrict_apply, Function.iterate_succ', Function.comp_apply
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : ∀ (x : (↑s : Type u_1)), f (↑x : α) ∈ t
⊢ codRestrict (s.restrict (π := fun (a : α) ↦ β) f) t h = MapsTo.restrict f s t ⋯

Tactic:
rfl

Premises used: Subtype.map, Set.codRestrict, Set.restrict, Set.MapsTo.restrict, rfl
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
⊢ restrict f s t h = codRestrict (s.restrict (π := fun (a : α) ↦ β) f) t ⋯

Tactic:
rfl

Premises used: Subtype.map, Set.codRestrict, Set.restrict, Set.MapsTo.restrict, rfl
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
⊢ Subtype.val (p := fun (x : β) ↦ x ∈ t) ∘ restrict f s t h = s.restrict (π := fun (a : α) ↦ β) f

Tactic:
rfl

Premises used: Set.restrict, rfl
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
h : MapsTo f s t
⊢ range (restrict f s t h) = Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s

Tactic:
Set.range_subtype_map f h

Premises used: Set.Mem, setOf, Set.range_subtype_map, Set.MapsTo.restrict
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : ∃ (g : (↑s : Type u_1) → (↑t : Type u_2)), ∀ (x : (↑s : Type u_1)), f (↑x : α) = (↑(g x) : β)
x : α
hx : x ∈ s
g : (↑s : Type u_1) → (↑t : Type u_2)
hg : ∀ (x : (↑s : Type u_1)), f (↑x : α) = (↑(g x) : β)
rw : (↑(g (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)) : β) ∈ t
⊢ f x ∈ t

Tactic:
rw [hg ⟨x, hx⟩]

Premises used: Subtype.mk
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : ∃ (g : (↑s : Type u_1) → (↑t : Type u_2)), ∀ (x : (↑s : Type u_1)), f (↑x : α) = (↑(g x) : β)
x : α
hx : x ∈ s
g : (↑s : Type u_1) → (↑t : Type u_2)
hg : ∀ (x : (↑s : Type u_1)), f (↑x : α) = (↑(g x) : β)
⊢ (↑(g (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x hx)) : β) ∈ t

Tactic:
apply Subtype.coe_prop

Premises used: Subtype.coe_prop
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ Surjective (MapsTo.restrict f s (f '' s) ⋯)

Tactic:
fun ⟨_, x, hs, hxy⟩ =>
  ⟨⟨x, hs⟩, Subtype.ext hxy⟩

Premises used: _private.0.Set.surjective_mapsTo_image_restrict.match_1, Exists, Set.mapsTo_image, Subtype.mk, Exists.intro, Set.image, Set.MapsTo.restrict, Eq, Function.Surjective, Subtype.ext
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
rw :
  Eq (α := Set β)
    ((fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) ''
      MapsTo.restrict f (f ⁻¹' t) t ⋯ '' Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' s)
    ((fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) '' Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s)
rw₁ :
  Eq (α := Set β)
    ((fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) ∘ MapsTo.restrict f (f ⁻¹' t) t ⋯ ''
      Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' s)
    ((fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) '' Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s)
rw₂ :
  image (α := (↑(f ⁻¹' t) : Type u_1)) (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t))
      (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' s) =
    (fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) '' Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s
rw₃ :
  f ''
      image (α := (↑(f ⁻¹' t) : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t))
        (Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' s) =
    (fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) '' Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s
rw₄ :
  f '' (f ⁻¹' t ∩ s) = (fun (a : { x : β // x ∈ t }) ↦ (↑a : β)) '' Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s
rw₅ : f '' (f ⁻¹' t ∩ s) = t ∩ f '' s
rw₆ rw₇ : t ∩ f '' s = t ∩ f '' s
⊢ MapsTo.restrict f (f ⁻¹' t) t ⋯ '' Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' s =
    Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' f '' s

Tactic:
rw [← (Subtype.coe_injective).image_injective.eq_iff, ← image_comp, MapsTo.restrict_commutes,
    image_comp, Subtype.image_preimage_coe, Subtype.image_preimage_coe, image_preimage_inter]

Premises used: Subtype.image_preimage_coe, Function.Injective.eq_iff, Set.image_preimage_inter, Subtype.coe_injective, Set.image_comp, Set.MapsTo.restrict_commutes, Function.Injective.image_injective
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
⊢ range (t.restrictPreimage f) = Subtype.val (p := fun (x : β) ↦ x ∈ t) ⁻¹' range f

Tactic:
simp only [← image_univ, ← image_restrictPreimage, preimage_univ]

Premises used: Set.image_univ, Set.image_restrictPreimage, Set.preimage_univ
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
a : α
h : a ∈ f ⁻¹' t
⊢ t.restrictPreimage f (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' t) a h) = Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f a) h

Tactic:
rfl

Premises used: Set.restrictPreimage, Subtype.map, Set.MapsTo.restrict, rfl
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
u : Set (↑t : Type u_2)
h :
  ∀ (x : α),
    x ∈ Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) '' t.restrictPreimage f ⁻¹' u ↔
      x ∈ f ⁻¹' Subtype.val (p := fun (x : β) ↦ x ∈ t) '' u
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) '' t.restrictPreimage f ⁻¹' u =
    f ⁻¹' Subtype.val (p := fun (x : β) ↦ x ∈ t) '' u

Tactic:
ext
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
u : Set (↑t : Type u_2)
x : α
⊢ x ∈ Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) '' t.restrictPreimage f ⁻¹' u ↔
    x ∈ f ⁻¹' Subtype.val (p := fun (x : β) ↦ x ∈ t) '' u

Tactic:
simp
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
u : Set (↑t : Type u_2)
rw :
  t.restrictPreimage f ⁻¹' u =
    Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹' f ⁻¹' Subtype.val (p := fun (x : β) ↦ x ∈ t) '' u
rw₁ :
  t.restrictPreimage f ⁻¹' u =
    Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) ⁻¹'
      Subtype.val (p := fun (x : α) ↦ x ∈ f ⁻¹' t) '' t.restrictPreimage f ⁻¹' u
rw₂ rw₃ : t.restrictPreimage f ⁻¹' u = t.restrictPreimage f ⁻¹' u
⊢ t.restrictPreimage f ⁻¹' u =
    (fun (a : (↑(f ⁻¹' t) : Type u_1)) ↦ f (↑a : α)) ⁻¹' Subtype.val (p := fun (x : β) ↦ x ∈ t) '' u

Tactic:
rw [← preimage_preimage (g := f) (f := Subtype.val), ← image_val_preimage_restrictPreimage,
    preimage_image_eq _ Subtype.val_injective]

Premises used: Set.preimage_preimage, Subtype.val_injective, Set.preimage_image_eq, Set.image_val_preimage_restrictPreimage
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
hf : Injective f
⊢ Injective (t.restrictPreimage f)

Tactic:
fun _ _ e => Subtype.coe_injective <| hf <| Subtype.mk.inj e

Premises used: Subtype.coe_injective, Subtype.mk.inj, Function.Injective
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
hf : Surjective f
⊢ Surjective (t.restrictPreimage f)

Tactic:
fun x => ⟨⟨_, ((hf x).choose_spec.symm ▸ x.2 : _ ∈ t)⟩, Subtype.ext (hf x).choose_spec⟩

Premises used: Exists.choose_spec, Classical.indefiniteDescription, Subtype.mk, Exists.intro, Subtype.val, Eq, Function.Surjective, Subtype.ext
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
t : Set β
f : α → β
hf : Bijective f
⊢ Bijective (t.restrictPreimage f)

Tactic:
⟨t.restrictPreimage_injective hf.1, t.restrictPreimage_surjective hf.2⟩

Premises used: Set.restrictPreimage_surjective, And.right, And.left, And.intro, Function.Bijective, Set.restrictPreimage_injective
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ InjOn f s ↔ Injective (s.restrict (π := fun (a : α) ↦ β) f)

Tactic:
⟨fun H a b h => Subtype.ext <| H a.2 b.2 h, fun H a as b bs h =>
    congr_arg Subtype.val <| @H ⟨a, as⟩ ⟨b, bs⟩ h⟩

Premises used: congr_arg, Iff.intro, Subtype.val, Subtype.property, Subtype.ext
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
rw : Injective (codRestrict (s.restrict (π := fun (a : α) ↦ β) f) t ⋯) ↔ InjOn f s
rw₁ : Injective (s.restrict (π := fun (a : α) ↦ β) f) ↔ InjOn f s
rw₂ rw₃ : Injective (s.restrict (π := fun (a : α) ↦ β) f) ↔ Injective (s.restrict (π := fun (a : α) ↦ β) f)
⊢ Injective (restrict f s t h) ↔ InjOn f s

Tactic:
rw [h.restrict_eq_codRestrict, injective_codRestrict, injOn_iff_injective]

Premises used: Set.injective_codRestrict, Set.injOn_iff_injective, Set.MapsTo.restrict_eq_codRestrict
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ SurjOn f s univ ↔ Surjective (s.restrict (π := fun (a : α) ↦ β) f)

Tactic:
⟨fun H b =>
    let ⟨a, as, e⟩ := @H b trivial
    ⟨⟨a, as⟩, e⟩,
    fun H b _ =>
    let ⟨⟨a, as⟩, e⟩ := H b
    ⟨a, as, e⟩⟩

Premises used: trivial, _private.0.Set.surjOn_iff_surjective.match_2, Membership.mem, Exists, _private.0.Set.surjOn_iff_surjective.match_1, Subtype.mk, And.intro, Iff.intro, Exists.intro, Set.image, Set.restrict, Eq
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
⊢ Surjective (restrict f s t h) ↔ SurjOn f s t

Tactic:
⟨fun h' b hb ↦ ?_, fun h' ⟨b, hb⟩ ↦ ?_⟩

Premises used: Exists, _private.0.Set.MapsTo.restrict_surjective_iff.match_1, Iff.intro, Set.MapsTo.restrict, Eq
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
refine_1 : ∀ (h' : Surjective (restrict f s t h)) (b : β) (hb : b ∈ t), b ∈ f '' s
refine_2 :
  ∀ (h' : SurjOn f s t) (x : (↑t : Type u_2)) (b : β) (hb : b ∈ t),
    ∃ (a : (↑s : Type u_1)), restrict f s t h a = Subtype.mk (p := fun (x : β) ↦ x ∈ t) b hb
⊢ Surjective (restrict f s t h) ↔ SurjOn f s t

Tactic:
refine ⟨fun h' b hb ↦ ?_, fun h' ⟨b, hb⟩ ↦ ?_⟩
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : Surjective (restrict f s t h)
b : β
hb : b ∈ t
refine_1 :
  ∀ (a : α) (ha : a ∈ s)
    (ha' : restrict f s t h (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha) = Subtype.mk (p := fun (x : β) ↦ x ∈ t) b hb),
    b ∈ f '' s
⊢ b ∈ f '' s

Tactic:
obtain ⟨⟨a, ha⟩, ha'⟩ := h' ⟨b, hb⟩

Premises used: Subtype.mk
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : Surjective (restrict f s t h)
b : β
hb : b ∈ t
a : α
ha : a ∈ s
ha' : restrict f s t h (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha) = Subtype.mk (p := fun (x : β) ↦ x ∈ t) b hb
⊢ f a = b

Tactic:
simpa [Subtype.ext_iff] using ha'

Premises used: Subtype.ext_iff
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : Surjective (restrict f s t h)
b : β
hb : b ∈ t
a : α
ha : a ∈ s
ha' : restrict f s t h (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha) = Subtype.mk (p := fun (x : β) ↦ x ∈ t) b hb
⊢ f a = b

Tactic:
replace ha' : f a = b := by simpa [Subtype.ext_iff] using ha'
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : Surjective (restrict f s t h)
b : β
hb : b ∈ t
a : α
ha : a ∈ s
ha' : f a = b
refine_1 : f a ∈ f '' s
⊢ b ∈ f '' s

Tactic:
rw [← ha']
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : Surjective (restrict f s t h)
b : β
hb : b ∈ t
a : α
ha : a ∈ s
ha' : f a = b
⊢ f a ∈ f '' s

Tactic:
mem_image_of_mem f ha

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : Surjective (restrict f s t h)
b : β
hb : b ∈ t
a : α
ha : a ∈ s
ha' : f a = b
⊢ f a ∈ f '' s

Tactic:
exact mem_image_of_mem f ha

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : SurjOn f s t
x : (↑t : Type u_2)
b : β
hb : b ∈ t
refine_2 :
  ∀ (a : α) (ha : a ∈ s) (hb : f a ∈ t),
    ∃ (a_1 : (↑s : Type u_1)), restrict f s t h a_1 = Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f a) hb
⊢ ∃ (a : (↑s : Type u_1)), restrict f s t h a = Subtype.mk (p := fun (x : β) ↦ x ∈ t) b hb

Tactic:
obtain ⟨a, ha, rfl⟩ := h' hb

Premises used: rfl
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : SurjOn f s t
x : (↑t : Type u_2)
a : α
ha : a ∈ s
hb : f a ∈ t
⊢ ∃ (a_1 : (↑s : Type u_1)), restrict f s t h a_1 = Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f a) hb

Tactic:
⟨⟨a, ha⟩, rfl⟩

Premises used: Subtype.mk, Exists.intro, rfl
-- Module: Mathlib.Data.Set.Restrict
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : MapsTo f s t
h' : SurjOn f s t
x : (↑t : Type u_2)
a : α
ha : a ∈ s
hb : f a ∈ t
⊢ ∃ (a_1 : (↑s : Type u_1)), restrict f s t h a_1 = Subtype.mk (p := fun (x : β) ↦ x ∈ t) (f a) hb

Tactic:
exact ⟨⟨a, ha⟩, rfl⟩