awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
s : Set α
t : Set β
f : α → β
p₁ : α → γ
p₂ : β → δ
g : γ → δ
comm : ∀ (a : α), p₂ (f a) = g (p₁ a)
hinj : InjOn g (p₁ '' s)
h1 : MapsTo f s t
h2 : InjOn f s
h3 : SurjOn f s t
b : β
hb : b ∈ t
⊢ p₂ b ∈ g '' p₁ '' s
have refine_2 : ∀ (a : α) (ha : a ∈ s) (hb : f a ∈ t), p₂ (f a) ∈ g '' p₁ '' s
Tactic: obtain ⟨a, ha, rfl⟩ := h3 hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
r : Set β
hf : BijOn f s t
hrt : r ⊆ t
⊢ BijOn f (s ∩ f ⁻¹' r) r
have refine : ∀ (x : β) (hx : x ∈ r), x ∈ f '' (s ∩ f ⁻¹' r)
Tactic: refine ⟨inter_subset_right, hf.injOn.mono inter_subset_left, fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
r : Set β
hf : BijOn f s t
hrt : r ⊆ t
x : β
hx : x ∈ r
⊢ x ∈ f '' (s ∩ f ⁻¹' r)
have obtain : ∀ (y : α) (hy : y ∈ s) (hx : f y ∈ r), f y ∈ f '' (s ∩ f ⁻¹' r)
Tactic: obtain ⟨y, hy, rfl⟩ := hf.surjOn (hrt hx)
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.Set.Function (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
⊢ BijOn f s t
have this : Eq.{u_2 + 1} (α := Set β) ((fun (x : Set β) ↦ x \ {f a}) (insert (f a) (f '' s)))
  ((fun (x : Set β) ↦ x \ {f a}) (insert (f a) t))
Tactic: have := congrArg (· \ {f a}) (image_insert_eq ▸ h.image_eq)
-- Lean 4 proof step from Mathlib.Data.Set.Function (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
this :
  Eq.{u_2 + 1} (α := Set β) ((fun (x : Set β) ↦ x \ {f a}) (insert (f a) (f '' s)))
    ((fun (x : Set β) ↦ x \ {f a}) (insert (f a) t))
⊢ BijOn f s t
have this₁ : f '' s \ {f a} = t \ {f a}
Tactic: simp only [mem_singleton_iff, insert_diff_of_mem] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s \ {f a} = t \ {f a}
⊢ BijOn f s t
have rw : ∀ (this : f '' s = t), BijOn f s t
Tactic: rw [diff_singleton_eq_self hfa, diff_singleton_eq_self] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s \ {f a} = t \ {f a}
rw : ∀ (this : f '' s = t), BijOn f s t
⊢ BijOn f s t
have rw₁ : ∀ (this : f '' s \ {f a} = t), ¬f a ∈ f '' s
Tactic: rw [diff_singleton_eq_self hfa, diff_singleton_eq_self] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s \ {f a} = t
⊢ ¬f a ∈ f '' s
have simp : ∀ (x : α), x ∈ s → ¬f x = f a
Tactic: simp only [mem_image, not_exists, not_and]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f (insert a s) (insert (f a) t)
this : f '' s \ {f a} = t
x : α
hx : x ∈ s
⊢ ¬f x = f a
have rw : ¬x = a
Tactic: rw [h.injOn.eq_iff (by simp [hx]) (by simp)]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f s t
⊢ BijOn f ({a} ∪ s) ({f a} ∪ t)
have refine : InjOn f ({a} ∪ s)
Tactic: refine (bijOn_singleton.mpr rfl).union h ?_
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
ha : ¬a ∈ s
hfa : ¬f a ∈ t
h : BijOn f s t
⊢ InjOn f ({a} ∪ s)
have simp : ∀ (x : α), x ∈ s → ¬f x = f a
Tactic: simp only [singleton_union, injOn_insert fun x ↦ (hfa (h.mapsTo x)), h.injOn, mem_image,
      not_exists, not_and, true_and]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
a : α
h₁ : BijOn f s t
h₂ : a ∈ s
⊢ BijOn f (s \ {a}) (t \ {f a})
have h : t \ {f a} = f '' (s \ {a})
Tactic: convert! h₁.subset_left diff_subset
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
f' : β → α
h : LeftInvOn f' f s
hf : SurjOn f s t
y : β
hy : y ∈ t
⊢ f' y ∈ s
have let : ∀ (x : α) (hs : x ∈ s) (hx : f x = y), f' y ∈ s
Tactic: let ⟨x, hs, hx⟩ := hf hy
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
f' : β → α
h : LeftInvOn f' f s
hf : SurjOn f s t
y : β
hy : y ∈ t
x : α
hs : x ∈ s
hx : f x = y
⊢ f' y ∈ s
have rwa : f' (f x) ∈ s
Tactic: rwa [← hx, h hs]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
⊢ f '' (s₁ ∩ s) = f' ⁻¹' s₁ ∩ f '' s
have h₁ : f '' (s₁ ∩ s) ⊆ f' ⁻¹' s₁ ∩ f '' s
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
h₁ : f '' (s₁ ∩ s) ⊆ f' ⁻¹' s₁ ∩ f '' s
⊢ f '' (s₁ ∩ s) = f' ⁻¹' s₁ ∩ f '' s
have h₂ : f' ⁻¹' s₁ ∩ f '' s ⊆ f '' (s₁ ∩ s)
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
x : α
h₁ : x ∈ s₁
h : x ∈ s
⊢ f x ∈ f' ⁻¹' s₁
have rwa : f' (f x) ∈ s₁
Tactic: rwa [mem_preimage, hf h]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
x : α
h : x ∈ s
h₁ : f x ∈ f' ⁻¹' s₁
⊢ x ∈ s₁
have rwa : f' (f x) ∈ s₁
Tactic: rwa [← hf h]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
⊢ f '' (s₁ ∩ s) = f' ⁻¹' (s₁ ∩ s) ∩ f '' s
have rw : f' ⁻¹' s₁ ∩ f '' s = f' ⁻¹' (s₁ ∩ s) ∩ f '' s
Tactic: rw [hf.image_inter']
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
⊢ f' ⁻¹' s₁ ∩ f '' s = f' ⁻¹' (s₁ ∩ s) ∩ f '' s
have refine : f' ⁻¹' s₁ ∩ f '' s ⊆ f' ⁻¹' (s₁ ∩ s) ∩ f '' s
Tactic: refine Subset.antisymm ?_ (inter_subset_inter_left _ (preimage_mono inter_subset_left))
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
⊢ f' '' f '' s = s
have rw : (fun (x : α) ↦ f' (f x)) '' s = s
Tactic: rw [Set.image_image, image_congr hf, image_id']
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
rw : (fun (x : α) ↦ f' (f x)) '' s = s
⊢ f' '' f '' s = s
have rw₁ : (fun (a : α) ↦ a) '' s = s
Tactic: rw [Set.image_image, image_congr hf, image_id']
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
rw : (fun (x : α) ↦ f' (f x)) '' s = s
rw₁ : (fun (a : α) ↦ a) '' s = s
⊢ f' '' f '' s = s
have rw₂ : s = s
Tactic: rw [Set.image_image, image_congr hf, image_id']
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
f' : β → α
hf : SurjOn f s t
hf' : RightInvOn f f' s
y : β
hy : y ∈ t
⊢ f (f' y) = y
have let : ∀ (x : α) (hx : x ∈ s) (heq : f x = y), f (f' y) = y
Tactic: let ⟨x, hx, heq⟩ := hf hy
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
f' : β → α
hf : SurjOn f s t
hf' : RightInvOn f f' s
y : β
hy : y ∈ t
x : α
hx : x ∈ s
heq : f x = y
⊢ f (f' y) = y
have rw : f (f' (f x)) = f x
Tactic: rw [← heq, hf' hx]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
f' : β → α
hf : SurjOn f s t
hf' : RightInvOn f f' s
y : β
hy : y ∈ t
x : α
hx : x ∈ s
heq : f x = y
rw : f (f' (f x)) = f x
⊢ f (f' y) = y
have rw₁ : f x = f x
Tactic: rw [← heq, hf' hx]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
⊢ f '' s = g ⁻¹' s
have h : ∀ (x : β), x ∈ f '' s ↔ x ∈ g ⁻¹' s
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
x : β
⊢ x ∈ f '' s ↔ x ∈ g ⁻¹' s
have h : x ∈ f '' s → x ∈ g ⁻¹' s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
x : β
h : x ∈ f '' s → x ∈ g ⁻¹' s
⊢ x ∈ f '' s ↔ x ∈ g ⁻¹' s
have h₁ : x ∈ g ⁻¹' s → x ∈ f '' s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
hgf : LeftInvOn g f s
ginj : InjOn g (g ⁻¹' s)
x : β
hx : x ∈ g ⁻¹' s
⊢ x ∈ f '' s
have h : MapsTo f s (g ⁻¹' s)
Tactic: refine ⟨g x, hx, Set.InjOn.rightInvOn_of_leftInvOn ginj hgf (Set.mapsTo_preimage g s) ?_ hx⟩
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
b : β
inst : Nonempty α
h : ∃ (a : α), a ∈ s ∧ f a = b
⊢ invFunOn f s b ∈ s ∧ f (invFunOn f s b) = b
have rw : Classical.choose (p := fun (x : α) ↦ x ∈ s ∧ f x = b) h ∈ s ∧
  f (Classical.choose (p := fun (x : α) ↦ x ∈ s ∧ f x = b) h) = b
Tactic: rw [invFunOn, dif_pos h]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
b : β
inst : Nonempty α
h : ¬∃ (a : α), a ∈ s ∧ f a = b
⊢ invFunOn f s b = Classical.choice inst
have rw : (if h : ∃ (a : α), a ∈ s ∧ f a = b then Classical.choose (p := fun (x : α) ↦ x ∈ s ∧ f x = b) h
  else Classical.choice inst) =
  Classical.choice inst
Tactic: rw [invFunOn, dif_neg h]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
b : β
inst : Nonempty α
h : ¬∃ (a : α), a ∈ s ∧ f a = b
rw :
  (if h : ∃ (a : α), a ∈ s ∧ f a = b then Classical.choose (p := fun (x : α) ↦ x ∈ s ∧ f x = b) h
    else Classical.choice inst) =
    Classical.choice inst
⊢ invFunOn f s b = Classical.choice inst
have rw₁ : Classical.choice inst = Classical.choice inst
Tactic: rw [invFunOn, dif_neg h]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
inst : Nonempty α
h : s ⊆ invFunOn f s '' f '' s
x : α
hx : x ∈ s
⊢ invFunOn f s (f x) = x
have obtain : ∀ (x : α) (hx' : x ∈ s) (hx : invFunOn f s (f x) ∈ s), invFunOn f s (f (invFunOn f s (f x))) = invFunOn f s (f x)
Tactic: obtain ⟨-, ⟨x, hx', rfl⟩, rfl⟩ := h hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
inst : Nonempty α
h : s ⊆ invFunOn f s '' f '' s
x : α
hx' : x ∈ s
hx : invFunOn f s (f x) ∈ s
⊢ invFunOn f s (f (invFunOn f s (f x))) = invFunOn f s (f x)
have rw : invFunOn f s (f x) = invFunOn f s (f x)
Tactic: rw [invFunOn_apply_eq (f := f) hx']
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty α
f : α → β
s : Set α
x : α
hx : x ∈ s
x' : α
hx' : x' ∈ s
he : invFunOn f s (f x) = invFunOn f s (f x')
⊢ f x = f x'
have rw : f (invFunOn f s (f x)) = f x'
Tactic: rw [← invFunOn_apply_eq (f := f) hx, he, invFunOn_apply_eq (f := f) hx']
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty α
f : α → β
s : Set α
x : α
hx : x ∈ s
x' : α
hx' : x' ∈ s
he : invFunOn f s (f x) = invFunOn f s (f x')
rw : f (invFunOn f s (f x)) = f x'
⊢ f x = f x'
have rw₁ : f (invFunOn f s (f x')) = f x'
Tactic: rw [← invFunOn_apply_eq (f := f) hx, he, invFunOn_apply_eq (f := f) hx']
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty α
f : α → β
s : Set α
x : α
hx : x ∈ s
x' : α
hx' : x' ∈ s
he : invFunOn f s (f x) = invFunOn f s (f x')
rw : f (invFunOn f s (f x)) = f x'
rw₁ : f (invFunOn f s (f x')) = f x'
⊢ f x = f x'
have rw₂ : f x' = f x'
Tactic: rw [← invFunOn_apply_eq (f := f) hx, he, invFunOn_apply_eq (f := f) hx']
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst : Nonempty α
h : SurjOn f s t
⊢ InvOn (invFunOn f s) f (invFunOn f s '' t) t
have refine : LeftInvOn (invFunOn f s) f (invFunOn f s '' t)
Tactic: refine ⟨?_, h.rightInvOn_invFunOn⟩
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst : Nonempty α
h : SurjOn f s t
y : β
hy : y ∈ t
⊢ invFunOn f s (f (invFunOn f s y)) = invFunOn f s y
have rw : invFunOn f s y = invFunOn f s y
Tactic: rw [h.rightInvOn_invFunOn hy]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
inst : Nonempty α
h : SurjOn f s t
⊢ BijOn f (invFunOn f s '' t) t
have refine : MapsTo f (invFunOn f s '' t) t
Tactic: refine h.invOn_invFunOn.bijOn ?_ (mapsTo_image _ _)
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ SurjOn f s t ↔ ∃ (s' : Set α), s' ⊆ s ∧ BijOn f s' t
have mp : SurjOn f s t → ∃ (s' : Set α), s' ⊆ s ∧ BijOn f s' t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
mp : SurjOn f s t → ∃ (s' : Set α), s' ⊆ s ∧ BijOn f s' t
⊢ SurjOn f s t ↔ ∃ (s' : Set α), s' ⊆ s ∧ BijOn f s' t
have mpr : (∃ (s' : Set α), s' ⊆ s ∧ BijOn f s' t) → SurjOn f s t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ SurjOn f s t → ∃ (s' : Set α), s' ⊆ s ∧ BijOn f s' t
have mp : SurjOn f s ∅ → ∃ (s' : Set α), s' ⊆ s ∧ BijOn f s' ∅
Tactic: rcases eq_empty_or_nonempty t with (rfl | ht)
Cleared hypotheses: t
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
mp : SurjOn f s ∅ → ∃ (s' : Set α), s' ⊆ s ∧ BijOn f s' ∅
⊢ SurjOn f s t → ∃ (s' : Set α), s' ⊆ s ∧ BijOn f s' t
have mp₁ : ∀ (ht : t.Nonempty), SurjOn f s t → ∃ (s' : Set α), s' ⊆ s ∧ BijOn f s' t
Tactic: rcases eq_empty_or_nonempty t with (rfl | ht)
-- Lean 4 proof step from Mathlib.Data.Set.Function (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
ht : t.Nonempty
h : SurjOn f s t
⊢ ∃ (s' : Set α), s' ⊆ s ∧ BijOn f s' t
have this : Nonempty α
Tactic: haveI : Nonempty α := ⟨Classical.choose (h.comap_nonempty ht)⟩
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
⊢ ∃ (s' : Set α), s ⊆ s' ∧ s' ⊆ s₁ ∧ BijOn f s' t'
have obtain : ∀ (r : Set α) (hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t) (hbij : BijOn f r (f '' ((s₁ ∩ f ⁻¹' t') \ f ⁻¹' t))),
  ∃ (s' : Set α), s ⊆ s' ∧ s' ⊆ s₁ ∧ BijOn f s' t'
Tactic: obtain ⟨r, hrss, hbij⟩ := exists_subset_bijOn ((s₁ ∩ f ⁻¹' t') \ f ⁻¹' t) f
-- Lean 4 proof step from Mathlib.Data.Set.Function (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r (f '' ((s₁ ∩ f ⁻¹' t') \ f ⁻¹' t))
⊢ ∃ (s' : Set α), s ⊆ s' ∧ s' ⊆ s₁ ∧ BijOn f s' t'
have hbij₁ : BijOn f r ((f '' s₁ ∩ t') \ t)
Tactic: rw [image_diff_preimage, image_inter_preimage] at hbij
Cleared hypotheses: hbij
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ ∃ (s' : Set α), s ⊆ s' ∧ s' ⊆ s₁ ∧ BijOn f s' t'
have refine_1 : s ∪ r ⊆ s₁
Tactic: refine ⟨s ∪ r, subset_union_left, ?_, ?_, ?_, fun y hyt' ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
refine_1 : s ∪ r ⊆ s₁
⊢ ∃ (s' : Set α), s ⊆ s' ∧ s' ⊆ s₁ ∧ BijOn f s' t'
have refine_2 : MapsTo f (s ∪ r) t'
Tactic: refine ⟨s ∪ r, subset_union_left, ?_, ?_, ?_, fun y hyt' ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
refine_1 : s ∪ r ⊆ s₁
refine_2 : MapsTo f (s ∪ r) t'
⊢ ∃ (s' : Set α), s ⊆ s' ∧ s' ⊆ s₁ ∧ BijOn f s' t'
have refine_3 : InjOn f (s ∪ r)
Tactic: refine ⟨s ∪ r, subset_union_left, ?_, ?_, ?_, fun y hyt' ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
refine_1 : s ∪ r ⊆ s₁
refine_2 : MapsTo f (s ∪ r) t'
refine_3 : InjOn f (s ∪ r)
⊢ ∃ (s' : Set α), s ⊆ s' ∧ s' ⊆ s₁ ∧ BijOn f s' t'
have refine_4 : ∀ (y : β) (hyt' : y ∈ t'), y ∈ f '' (s ∪ r)
Tactic: refine ⟨s ∪ r, subset_union_left, ?_, ?_, ?_, fun y hyt' ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ MapsTo f (s ∪ r) t'
have refine_2 : t ⊆ t' ∧ (f '' s₁ ∩ t') \ t ⊆ t'
Tactic: rw [mapsTo_iff_image_subset, image_union, hbij.image_eq, h.image_eq, union_subset_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ InjOn f (s ∪ r)
have refine_3 : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ r → f x ≠ f y
Tactic: rw [injOn_union, and_iff_right h.injOn, and_iff_right hbij.injOn]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
refine_3 : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ r → f x ≠ f y
⊢ InjOn f (s ∪ r)
have refine_3₁ : Disjoint s r
Tactic: rw [injOn_union, and_iff_right h.injOn, and_iff_right hbij.injOn]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
⊢ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ r → f x ≠ f y
have refine_3 : ∀ (x : α) (hxs : x ∈ s) (y : α) (hyr : y ∈ r) (hxy : f x = f y), y ∈ f ⁻¹' t
Tactic: refine fun x hxs y hyr hxy ↦ (hrss hyr).2 ?_
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
x : α
hxs : x ∈ s
y : α
hyr : y ∈ r
hxy : f x = f y
⊢ y ∈ f ⁻¹' t
have refine_3 : y ∈ f ⁻¹' f '' s
Tactic: rw [← h.image_eq]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ : Set α
t : Set β
f : α → β
t' : Set β
h : BijOn f s t
hss₁ : s ⊆ s₁
htt' : t ⊆ t'
ht' : SurjOn f s₁ t'
r : Set α
hrss : r ⊆ (s₁ ∩ f ⁻¹' t') \ f ⁻¹' t
hbij : BijOn f r ((f '' s₁ ∩ t') \ t)
y : β
hyt' : y ∈ t'
⊢ y ∈ f '' (s ∪ r)
have refine_4 : y ∈ t ∪ f '' s₁ ∩ t'
Tactic: rw [image_union, h.image_eq, hbij.image_eq, union_diff_self]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
r : Set α
hinj : InjOn f r
hrs : r ⊆ s
⊢ ∃ (u : Set α), r ⊆ u ∧ u ⊆ s ∧ f '' u = f '' s ∧ InjOn f u
have obtain : ∀ (u : Set α) (hru : r ⊆ u) (hus : u ⊆ s) (h : BijOn f u (f '' s)),
  ∃ (u : Set α), r ⊆ u ∧ u ⊆ s ∧ f '' u = f '' s ∧ InjOn f u
Tactic: obtain ⟨u, hru, hus, h⟩ := hinj.bijOn_image.exists_extend_of_subset hrs
    (image_mono hrs) Subset.rfl
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : Classical.choice n ∈ s
⊢ invFun f ⁻¹' s = f '' s ∪ (range f)ᶜ
have h₁ : ∀ (x : β), x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s ∪ (range f)ᶜ
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : Classical.choice n ∈ s
x : β
⊢ x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s ∪ (range f)ᶜ
have h₁ : ∀ (a : α), f a ∈ invFun f ⁻¹' s ↔ f a ∈ f '' s ∪ (range f)ᶜ
Tactic: rcases em (x ∈ range f) with (⟨a, rfl⟩ | hx)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : Classical.choice n ∈ s
x : β
h₁ : ∀ (a : α), f a ∈ invFun f ⁻¹' s ↔ f a ∈ f '' s ∪ (range f)ᶜ
⊢ x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s ∪ (range f)ᶜ
have h₂ : ∀ (hx : ¬x ∈ range f), x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s ∪ (range f)ᶜ
Tactic: rcases em (x ∈ range f) with (⟨a, rfl⟩ | hx)
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
⊢ invFun f ⁻¹' s = f '' s
have h₁ : ∀ (x : β), x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
x : β
⊢ x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s
have h₁ : ∀ (a : α), f a ∈ invFun f ⁻¹' s ↔ f a ∈ f '' s
Tactic: rcases em (x ∈ range f) with (⟨a, rfl⟩ | hx)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
x : β
h₁ : ∀ (a : α), f a ∈ invFun f ⁻¹' s ↔ f a ∈ f '' s
⊢ x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s
have h₂ : ∀ (hx : ¬x ∈ range f), x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s
Tactic: rcases em (x ∈ range f) with (⟨a, rfl⟩ | hx)
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
a : α
⊢ f a ∈ invFun f ⁻¹' s ↔ f a ∈ f '' s
have h₁ : invFun f (f a) ∈ s ↔ f a ∈ f '' s
Tactic: rw [mem_preimage, leftInverse_invFun hf, hf.mem_set_image]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
a : α
h₁ : invFun f (f a) ∈ s ↔ f a ∈ f '' s
⊢ f a ∈ invFun f ⁻¹' s ↔ f a ∈ f '' s
have h₂ : a ∈ s ↔ f a ∈ f '' s
Tactic: rw [mem_preimage, leftInverse_invFun hf, hf.mem_set_image]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
a : α
h₁ : invFun f (f a) ∈ s ↔ f a ∈ f '' s
h₂ : a ∈ s ↔ f a ∈ f '' s
⊢ f a ∈ invFun f ⁻¹' s ↔ f a ∈ f '' s
have h₃ : a ∈ s ↔ a ∈ s
Tactic: rw [mem_preimage, leftInverse_invFun hf, hf.mem_set_image]