awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.FiniteExhaustion (goal)
Goal:
α : Type u_1
s : Set α
K : s.FiniteExhaustion
β : Type u_2
t : Set β
K' : t.FiniteExhaustion
rw :
  SProd.sprod (α := Set α) (β := Set β) (⋃ (x : ℕ), (K : (a : ℕ) → Set α) x) (⋃ (x : ℕ), (K' : (a : ℕ) → Set β) x) =
    s ×ˢ t
rw₁ : SProd.sprod (β := Set β) s (⋃ (x : ℕ), (K' : (a : ℕ) → Set β) x) = s ×ˢ t
⊢ ⋃ (n : ℕ),
      SProd.sprod (α := Set α) (β := Set β) ((K : (a : ℕ) → Set α) n : Set α) ((K' : (a : ℕ) → Set β) n : Set β) =
    s ×ˢ t
have rw₂ : s ×ˢ t = s ×ˢ t
Tactic: rw [Set.iUnion_prod_of_monotone (OrderHomClass.mono K) (OrderHomClass.mono K'),
          K.iUnion_eq, K'.iUnion_eq]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
f : α → α
s : Set α
h : MapsTo f s s
n : ℕ
⊢ (restrict f s s h)^[n] = restrict f^[n] s s ⋯
have h₁ : ∀ (x : (↑s : Type u_1)), (↑((restrict f s s h)^[n] x) : α) = (↑(restrict f^[n] s s sorry x) : α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
⊢ InjOn f (s₁ ∪ s₂) ↔ InjOn f s₁ ∧ InjOn f s₂ ∧ ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y
have refine_1 : ∀ (H : InjOn f (s₁ ∪ s₂)) (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y
Tactic: refine ⟨fun H => ⟨H.mono subset_union_left, H.mono subset_union_right, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
refine_1 : ∀ (H : InjOn f (s₁ ∪ s₂)) (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y
⊢ InjOn f (s₁ ∪ s₂) ↔ InjOn f s₁ ∧ InjOn f s₂ ∧ ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y
have refine_2 : (InjOn f s₁ ∧ InjOn f s₂ ∧ ∀ (x : α), x ∈ s₁ → ∀ (y : α), y ∈ s₂ → f x ≠ f y) → InjOn f (s₁ ∪ s₂)
Tactic: refine ⟨fun H => ⟨H.mono subset_union_left, H.mono subset_union_right, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Function (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
H : InjOn f (s₁ ∪ s₂)
x : α
hx : x ∈ s₁
y : α
hy : y ∈ s₂
hxy : f x = f y
⊢ False
have hy₁ : x ∈ s₂
Tactic: obtain rfl : x = y := H (Or.inl hx) (Or.inr hy) hxy
Cleared hypotheses: y, hy, hxy
-- Lean 4 proof step from Mathlib.Data.Set.Function (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
f : α → β
h : Disjoint s₁ s₂
H : InjOn f (s₁ ∪ s₂)
x : α
hx : x ∈ s₁
y : α
hy : y ∈ s₂
hxy : f x = f y
hy₁ : x ∈ s₂
⊢ False
have hxy₁ : f x = f x
Tactic: obtain rfl : x = y := H (Or.inl hx) (Or.inr hy) hxy
Cleared hypotheses: y, hy, hxy
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
a : α
has : ¬a ∈ s
⊢ InjOn f (insert a s) ↔ InjOn f s ∧ ¬f a ∈ f '' s
have rw : (InjOn f s ∧ InjOn f {a} ∧ ∀ (x : α), x ∈ s → ∀ (y : α), Membership.mem (γ := Set α) {a} y → f x ≠ f y) ↔
  InjOn f s ∧ ¬f a ∈ f '' s
Tactic: rw [← union_singleton, injOn_union (disjoint_singleton_right.2 has)]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
inst : Nonempty β
h : ∃ (f : (↑s : Type u_1) → β), Injective f
f : (↑s : Type u_1) → β
hf : Injective f
⊢ ∃ (f : α → β), InjOn f s
have lift : ∀ (f : α → β) (hf : Injective.{u_1 + 1, u_2 + 1} (β := β) fun (i : (↑s : Type u_1)) ↦ f (↑i : α)),
  ∃ (f : α → β), InjOn f s
Tactic: lift f to α → β using trivial
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
⊢ f '' (s ∩ t) = f '' s ∩ f '' t
have apply : f '' s ∩ f '' t ⊆ f '' (s ∩ t)
Tactic: apply Subset.antisymm (image_inter_subset _ _ _)
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
⊢ x ∈ f '' s ∩ f '' t → x ∈ f '' (s ∩ t)
have this : ∀ (y : α) (ys : y ∈ s) (hy : f y = x) (z : α) (zt : z ∈ t) (hz : f z = x), x ∈ f '' (s ∩ t)
Tactic: ⟨⟨y, ys, hy⟩, ⟨z, zt, hz⟩⟩
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
hy : f y = x
z : α
zt : z ∈ t
hz : f z = x
⊢ y = z
have apply : f y = f z
Tactic: apply hf (hs ys) (ht zt)
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
hy : f y = x
z : α
zt : z ∈ t
hz : f z = x
⊢ f y = f z
have rwa : ∀ (hy : f y = f z) (zt : z ∈ t) (hz : f z = x), f y = f z
Tactic: rwa [← hz] at hy
Cleared hypotheses: hy, zt, hz
-- Lean 4 proof step from Mathlib.Data.Set.Function (hypothesis)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
hy : f y = x
z : α
zt : z ∈ t
hz : f z = x
⊢ x ∈ f '' (s ∩ t)
have this : y = z
Tactic: have : y = z := by
    apply hf (hs ys) (ht zt)
    rwa [← hz] at hy
-- Lean 4 proof step from Mathlib.Data.Set.Function (hypothesis)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
hy : f y = x
z : α
zt : z ∈ t
hz : f z = x
this : y = z
⊢ x ∈ f '' (s ∩ t)
have zt₁ : y ∈ t
Tactic: rw [← this] at zt
Cleared hypotheses: zt, hz, this
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : InjOn f s
s₁ : Set α
hs₁ : s₁ ∈ 𝒫 s
s₂ : Set α
hs₂ : s₂ ∈ 𝒫 s
h' : f '' s₁ = f '' s₂
⊢ s₁ = s₂
have rw : f ⁻¹' f '' s₁ ∩ s = s₂
Tactic: rw [← h.preimage_image_inter hs₁, h', h.preimage_image_inter hs₂]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : InjOn f s
s₁ : Set α
hs₁ : s₁ ∈ 𝒫 s
s₂ : Set α
hs₂ : s₂ ∈ 𝒫 s
h' : f '' s₁ = f '' s₂
rw : f ⁻¹' f '' s₁ ∩ s = s₂
⊢ s₁ = s₂
have rw₁ : f ⁻¹' f '' s₂ ∩ s = s₂
Tactic: rw [← h.preimage_image_inter hs₁, h', h.preimage_image_inter hs₂]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
h : InjOn f s
s₁ : Set α
hs₁ : s₁ ∈ 𝒫 s
s₂ : Set α
hs₂ : s₂ ∈ 𝒫 s
h' : f '' s₁ = f '' s₂
rw : f ⁻¹' f '' s₁ ∩ s = s₂
rw₁ : f ⁻¹' f '' s₂ ∩ s = s₂
⊢ s₁ = s₂
have rw₂ : s₂ = s₂
Tactic: rw [← h.preimage_image_inter hs₁, h', h.preimage_image_inter hs₂]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
f : α → β
h : InjOn f s
h₁ : s₁ ⊆ s
h₂ : s₂ ⊆ s
⊢ f '' s₁ ⊆ f '' s₂ ↔ s₁ ⊆ s₂
have refine : ∀ (h' : f '' s₁ ⊆ f '' s₂), s₁ ⊆ s₂
Tactic: refine ⟨fun h' ↦ ?_, image_mono⟩
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
f : α → β
h : InjOn f s
h₁ : s₁ ⊆ s
h₂ : s₂ ⊆ s
h' : f '' s₁ ⊆ f '' s₂
⊢ s₁ ⊆ s₂
have rw : f ⁻¹' f '' s₁ ∩ s ⊆ f ⁻¹' f '' s₂ ∩ s
Tactic: rw [← h.preimage_image_inter h₁, ← h.preimage_image_inter h₂]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
f : α → β
h : InjOn f s
h₁ : s₁ ⊆ s
h₂ : s₂ ⊆ s
⊢ f '' s₁ ⊂ f '' s₂ ↔ s₁ ⊂ s₂
have simp_rw : f '' s₁ ⊆ f '' s₂ ∧ ¬f '' s₂ ⊆ f '' s₁ ↔ s₁ ⊆ s₂ ∧ ¬s₂ ⊆ s₁
Tactic: simp_rw [ssubset_def, h.image_subset_image_iff h₁ h₂, h.image_subset_image_iff h₂ h₁]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
f : α → β
h : InjOn f s
h₁ : s₁ ⊆ s
h₂ : s₂ ⊆ s
simp_rw : f '' s₁ ⊆ f '' s₂ ∧ ¬f '' s₂ ⊆ f '' s₁ ↔ s₁ ⊆ s₂ ∧ ¬s₂ ⊆ s₁
⊢ f '' s₁ ⊂ f '' s₂ ↔ s₁ ⊂ s₂
have simp_rw₁ : s₁ ⊆ s₂ ∧ ¬f '' s₂ ⊆ f '' s₁ ↔ s₁ ⊆ s₂ ∧ ¬s₂ ⊆ s₁
Tactic: simp_rw [ssubset_def, h.image_subset_image_iff h₁ h₂, h.image_subset_image_iff h₂ h₁]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s t u : Set α
f : α → β
h : Disjoint s t
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
⊢ Disjoint (f '' s) (f '' t)
have rw : ∀ (h : s ∩ t = ∅) (hf : InjOn f u) (hs : s ⊆ u) (ht : t ⊆ u), f '' s ∩ f '' t = ∅
Tactic: rw [disjoint_iff_inter_eq_empty] at h ⊢
Cleared hypotheses: h, hf, hs, ht
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s t u : Set α
f : α → β
h : s ∩ t = ∅
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
⊢ f '' s ∩ f '' t = ∅
have rw : f '' (s ∩ t) = ∅
Tactic: rw [← hf.image_inter hs ht, h, image_empty]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s t u : Set α
f : α → β
h : s ∩ t = ∅
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
rw : f '' (s ∩ t) = ∅
⊢ f '' s ∩ f '' t = ∅
have rw₁ : f '' ∅ = ∅
Tactic: rw [← hf.image_inter hs ht, h, image_empty]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s t u : Set α
f : α → β
h : s ∩ t = ∅
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
rw : f '' (s ∩ t) = ∅
rw₁ : f '' ∅ = ∅
⊢ f '' s ∩ f '' t = ∅
have rw₂ : Eq.{u_2 + 1} (α := Set β) ∅ ∅
Tactic: rw [← hf.image_inter hs ht, h, image_empty]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
t : Set α
h : InjOn f s
⊢ f '' s ⊆ f '' (s ∩ t) ∪ f '' (s \ t)
have rw : f '' s ⊆ f '' (s ∩ t ∪ s \ t)
Tactic: rw [← image_union, inter_union_diff]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
t : Set α
h : InjOn f s
rw : f '' s ⊆ f '' (s ∩ t ∪ s \ t)
⊢ f '' s ⊆ f '' (s ∩ t) ∪ f '' (s \ t)
have rw₁ : f '' s ⊆ f '' s
Tactic: rw [← image_union, inter_union_diff]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
t : Set α
h : InjOn f s
⊢ f '' (s \ t) = f '' s \ f '' (s ∩ t)
have refine : Disjoint (f '' (s \ t)) (f '' (s ∩ t))
Tactic: refine subset_antisymm (subset_diff.2 ⟨image_mono diff_subset, ?_⟩)
    (diff_subset_iff.2 (by rw [← image_union, inter_union_diff]))
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
t : Set α
h : InjOn f s
hst : t ⊆ s
⊢ f '' (s \ t) = f '' s \ f '' t
have rw : f '' s \ f '' (s ∩ t) = f '' s \ f '' t
Tactic: rw [h.image_diff, inter_eq_self_of_subset_right hst]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
t : Set α
h : InjOn f s
hst : t ⊆ s
rw : f '' s \ f '' (s ∩ t) = f '' s \ f '' t
⊢ f '' (s \ t) = f '' s \ f '' t
have rw₁ : f '' s \ f '' t = f '' s \ f '' t
Tactic: rw [h.image_diff, inter_eq_self_of_subset_right hst]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set (α × β)
⊢ (∃ (f : α → β), s = graphOn f (Prod.fst '' s)) ↔ InjOn Prod.fst s
have refine_1 : (∃ (f : α → β), s = graphOn f (Prod.fst '' s)) → InjOn Prod.fst s
Tactic: refine ⟨?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set (α × β)
refine_1 : (∃ (f : α → β), s = graphOn f (Prod.fst '' s)) → InjOn Prod.fst s
⊢ (∃ (f : α → β), s = graphOn f (Prod.fst '' s)) ↔ InjOn Prod.fst s
have refine_2 : ∀ (h : InjOn Prod.fst s), ∃ (f : α → β), s = graphOn f (Prod.fst '' s)
Tactic: refine ⟨?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set (α × β)
f : α → β
hf : s = graphOn f (Prod.fst '' s)
⊢ InjOn Prod.fst s
have refine_1 : InjOn Prod.fst (graphOn f (Prod.fst '' s))
Tactic: rw [hf]
-- Lean 4 proof step from Mathlib.Data.Set.Function (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
⊢ ∃ (f : α → β), s = graphOn f (Prod.fst '' s)
have this : ∀ (x : α), x ∈ Prod.fst '' s → ∃ (y : β), (x, y) ∈ s
Tactic: have : ∀ x ∈ Prod.fst '' s, ∃ y, (x, y) ∈ s := forall_mem_image.2 fun (x, y) h ↦ ⟨y, h⟩
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
this : ∀ (x : α), x ∈ Prod.fst '' s → ∃ (y : β), (x, y) ∈ s
⊢ ∃ (f : α → β), s = graphOn f (Prod.fst '' s)
have refine_2 : ∀ (f : (x : α) → β) (hf : ∀ (x : α), x ∈ Prod.fst '' s → (x, f x) ∈ s), ∃ (f : α → β), s = graphOn f (Prod.fst '' s)
Tactic: choose! f hf using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Set.Function (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
f : (x : α) → β
hf : ∀ (x : α), x ∈ Prod.fst '' s → (x, f x) ∈ s
⊢ ∃ (f : α → β), s = graphOn f (Prod.fst '' s)
have hf₁ : ∀ ⦃x : α × β⦄, x ∈ s → (x.1, f x.1) ∈ s
Tactic: rw [forall_mem_image] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
f : (x : α) → β
hf : ∀ ⦃x : α × β⦄, x ∈ s → (x.1, f x.1) ∈ s
⊢ ∃ (f : α → β), s = graphOn f (Prod.fst '' s)
have h₁ : s = graphOn f (Prod.fst '' s)
Tactic: use f
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set (α × β)
h : InjOn Prod.fst s
f : (x : α) → β
hf : ∀ ⦃x : α × β⦄, x ∈ s → (x.1, f x.1) ∈ s
⊢ s = graphOn f (Prod.fst '' s)
have h₁ : EqOn (fun (x : α × β) ↦ (x.1, f x.1)) id s
Tactic: rw [graphOn, image_image, EqOn.image_eq_self]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set (α × β)
h : ∃ (f : α → β), ∃ (t : Set α), s = graphOn f t
f : α → β
t : Set α
hs : s = graphOn f t
⊢ s = graphOn f (Prod.fst '' s)
have rw : graphOn f t = graphOn f (Prod.fst '' graphOn f t)
Tactic: rw [hs, image_fst_graphOn]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
s : Set (α × β)
h : ∃ (f : α → β), ∃ (t : Set α), s = graphOn f t
f : α → β
t : Set α
hs : s = graphOn f t
rw : graphOn f t = graphOn f (Prod.fst '' graphOn f t)
⊢ s = graphOn f (Prod.fst '' s)
have rw₁ : graphOn f t = graphOn f t
Tactic: rw [hs, image_fst_graphOn]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h :
  ∃ (t' : Set β),
    ∃ (g : (↑s : Type u_1) → (↑t' : Type u_2)),
      t ⊆ t' ∧ Surjective g ∧ ∀ (x : (↑s : Type u_1)), f (↑x : α) = (↑(g x) : β)
y : β
hy : y ∈ t
t' : Set β
g : (↑s : Type u_1) → (↑t' : Type u_2)
htt' : t ⊆ t'
hg : Surjective g
hfg : ∀ (x : (↑s : Type u_1)), f (↑x : α) = (↑(g x) : β)
x : (↑s : Type u_1)
hx : g x = Subtype.mk (p := fun (x : β) ↦ x ∈ t') y ⋯
⊢ f (↑x : α) = y
have rw : (↑(g x) : β) = y
Tactic: rw [hfg, hx, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h :
  ∃ (t' : Set β),
    ∃ (g : (↑s : Type u_1) → (↑t' : Type u_2)),
      t ⊆ t' ∧ Surjective g ∧ ∀ (x : (↑s : Type u_1)), f (↑x : α) = (↑(g x) : β)
y : β
hy : y ∈ t
t' : Set β
g : (↑s : Type u_1) → (↑t' : Type u_2)
htt' : t ⊆ t'
hg : Surjective g
hfg : ∀ (x : (↑s : Type u_1)), f (↑x : α) = (↑(g x) : β)
x : (↑s : Type u_1)
hx : g x = Subtype.mk (p := fun (x : β) ↦ x ∈ t') y ⋯
rw : (↑(g x) : β) = y
⊢ f (↑x : α) = y
have rw₁ : (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ t') y sorry) : β) = y
Tactic: rw [hfg, hx, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h :
  ∃ (t' : Set β),
    ∃ (g : (↑s : Type u_1) → (↑t' : Type u_2)),
      t ⊆ t' ∧ Surjective g ∧ ∀ (x : (↑s : Type u_1)), f (↑x : α) = (↑(g x) : β)
y : β
hy : y ∈ t
t' : Set β
g : (↑s : Type u_1) → (↑t' : Type u_2)
htt' : t ⊆ t'
hg : Surjective g
hfg : ∀ (x : (↑s : Type u_1)), f (↑x : α) = (↑(g x) : β)
x : (↑s : Type u_1)
hx : g x = Subtype.mk (p := fun (x : β) ↦ x ∈ t') y ⋯
rw : (↑(g x) : β) = y
rw₁ : (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ t') y ⋯) : β) = y
⊢ f (↑x : α) = y
have rw₂ : y = y
Tactic: rw [hfg, hx, Subtype.coe_mk]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
inst : Subsingleton β
inst_1 : Nonempty β
⊢ SurjOn f s univ ↔ s.Nonempty
have intro : ∀ (val : Unique β), SurjOn f s univ ↔ s.Nonempty
Tactic: cases nonempty_unique β
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
h : SurjOn f s t
⊢ s.Nonempty ∨ t = ∅
have by_contra! : ∀ (this : s = ∅ ∧ t.Nonempty), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f₁ f₂ : α → β
h : SurjOn f₁ s t
H : EqOn f₁ f₂ s
⊢ SurjOn f₂ s t
have rwa : t ⊆ f₂ '' s
Tactic: rwa [SurjOn, ← H.image_eq]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f₁ f₂ : α → β
h : SurjOn f₁ s t
H : EqOn f₁ f₂ s
rwa : t ⊆ f₂ '' s
⊢ SurjOn f₂ s t
have rwa₁ : t ⊆ f₁ '' s
Tactic: rwa [SurjOn, ← H.image_eq]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : SurjOn f s₁ t₁
h₂ : SurjOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
y : β
hy : y ∈ t₁ ∩ t₂
⊢ y ∈ f '' (s₁ ∩ s₂)
have rcases : ∀ (x₁ : α) (hx₁ : x₁ ∈ s₁) (hy : f x₁ ∈ t₁ ∩ t₂), f x₁ ∈ f '' (s₁ ∩ s₂)
Tactic: rcases h₁ hy.1 with ⟨x₁, hx₁, rfl⟩
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : SurjOn f s₁ t₁
h₂ : SurjOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
x₁ : α
hx₁ : x₁ ∈ s₁
hy : f x₁ ∈ t₁ ∩ t₂
⊢ f x₁ ∈ f '' (s₁ ∩ s₂)
have rcases : ∀ (x₂ : α) (hx₂ : x₂ ∈ s₂) (heq : f x₂ = f x₁), f x₁ ∈ f '' (s₁ ∩ s₂)
Tactic: rcases h₂ hy.2 with ⟨x₂, hx₂, heq⟩
-- Lean 4 proof step from Mathlib.Data.Set.Function (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : SurjOn f s₁ t₁
h₂ : SurjOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
x₁ : α
hx₁ : x₁ ∈ s₁
hy : f x₁ ∈ t₁ ∩ t₂
x₂ : α
hx₂ : x₂ ∈ s₂
heq : f x₂ = f x₁
⊢ f x₁ ∈ f '' (s₁ ∩ s₂)
have hx₃ : x₁ ∈ s₂
Tactic: obtain rfl : x₁ = x₂ := h (Or.inl hx₁) (Or.inr hx₂) heq.symm
Cleared hypotheses: x₂, hx₂, heq
-- Lean 4 proof step from Mathlib.Data.Set.Function (hypothesis)
Goal:
α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t₁ t₂ : Set β
f : α → β
h₁ : SurjOn f s₁ t₁
h₂ : SurjOn f s₂ t₂
h : InjOn f (s₁ ∪ s₂)
x₁ : α
hx₁ : x₁ ∈ s₁
hy : f x₁ ∈ t₁ ∩ t₂
x₂ : α
hx₂ : x₂ ∈ s₂
heq : f x₂ = f x₁
hx₃ : x₁ ∈ s₂
⊢ f x₁ ∈ f '' (s₁ ∩ s₂)
have heq₁ : f x₁ = f x₁
Tactic: obtain rfl : x₁ = x₂ := h (Or.inl hx₁) (Or.inr hx₂) heq.symm
Cleared hypotheses: x₂, hx₂, heq
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
p : Set γ
f : α → β
g : β → γ
h : SurjOn (g ∘ f) s p
hr : MapsTo f s t
z : γ
hz : z ∈ p
⊢ z ∈ g '' t
have obtain : ∀ (x : α) (hx : x ∈ s) (hz : (g ∘ f) x ∈ p), (g ∘ f) x ∈ g '' t
Tactic: obtain ⟨x, hx, rfl⟩ := h hz
Cleared hypotheses: z, hz
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β
hf : SurjOn f s t
g : β → γ
⊢ SurjOn (g ∘ f) s (g '' t)
have rw : g '' t ⊆ g '' f '' s
Tactic: rw [SurjOn, image_comp g f]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
s : Set β
t : Set γ
hf : Surjective f
hg : SurjOn g s t
⊢ SurjOn (g ∘ f) (f ⁻¹' s) t
have rwa : t ⊆ g ∘ f '' f ⁻¹' s
Tactic: rwa [SurjOn, image_comp g f, image_preimage_eq _ hf]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
s : Set β
t : Set γ
hf : Surjective f
hg : SurjOn g s t
rwa : t ⊆ g ∘ f '' f ⁻¹' s
⊢ SurjOn (g ∘ f) (f ⁻¹' s) t
have rwa₁ : t ⊆ g '' f '' f ⁻¹' s
Tactic: rwa [SurjOn, image_comp g f, image_preimage_eq _ hf]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
s : Set β
t : Set γ
hf : Surjective f
hg : SurjOn g s t
rwa : t ⊆ g ∘ f '' f ⁻¹' s
rwa₁ : t ⊆ g '' f '' f ⁻¹' s
⊢ SurjOn (g ∘ f) (f ⁻¹' s) t
have rwa₂ : t ⊆ g '' s
Tactic: rwa [SurjOn, image_comp g f, image_preimage_eq _ hf]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ f '' s = t ↔ SurjOn f s t ∧ MapsTo f s t
have refine : f '' s = t → SurjOn f s t ∧ MapsTo f s t
Tactic: refine ⟨?_, fun h => h.1.image_eq_of_mapsTo h.2⟩
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
f : α → β
g₁ g₂ : β → γ
hf : EqOn (g₁ ∘ f) (g₂ ∘ f) s
hf' : SurjOn f s t
b : β
hb : b ∈ t
⊢ g₁ b = g₂ b
have obtain : ∀ (a : α) (ha : a ∈ s) (hb : f a ∈ t), g₁ (f a) = g₂ (f a)
Tactic: obtain ⟨a, ha, rfl⟩ := hf' 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 : α → β
h : SurjOn f s t
u : β
hu : u ∈ t
⊢ u ∈ f '' f ⁻¹' t
have rw : u ∈ t ∩ range f
Tactic: rw [image_preimage_eq_inter_range]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
h : ∀ (a : α), a ∈ s → p (f a)
b : β
hb : b ∈ t
⊢ p b
have obtain : ∀ (a : α) (ha : a ∈ s) (hb : f a ∈ t), p (f a)
Tactic: obtain ⟨a, ha, rfl⟩ := hf.surjOn 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 : α → β
p : β → Prop
hf : BijOn f s t
b : β
hb : b ∈ t
h : p b
⊢ ∃ (a : α), a ∈ s ∧ p (f a)
have obtain : ∀ (a : α) (ha : a ∈ s) (hb : f a ∈ t) (h : p (f a)), ∃ (a : α), a ∈ s ∧ p (f a)
Tactic: obtain ⟨a, ha, rfl⟩ := hf.surjOn hb
Cleared hypotheses: b, hb, h
-- Lean 4 proof step from Mathlib.Data.Set.Function (hypothesis)
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)
hbij : BijOn f s t
hinj : InjOn g (p₁ '' s)
⊢ BijOn g (p₁ '' s) (p₂ '' t)
have h1 : MapsTo f s t
Tactic: obtain ⟨h1, h2, h3⟩ := hbij
Cleared hypotheses: hbij
-- Lean 4 proof step from Mathlib.Data.Set.Function (hypothesis)
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)
hbij : BijOn f s t
hinj : InjOn g (p₁ '' s)
h1 : MapsTo f s t
⊢ BijOn g (p₁ '' s) (p₂ '' t)
have h2 : InjOn f s
Tactic: obtain ⟨h1, h2, h3⟩ := hbij
Cleared hypotheses: hbij
-- Lean 4 proof step from Mathlib.Data.Set.Function (hypothesis)
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)
hbij : BijOn f s t
hinj : InjOn g (p₁ '' s)
h1 : MapsTo f s t
h2 : InjOn f s
⊢ BijOn g (p₁ '' s) (p₂ '' t)
have h3 : SurjOn f s t
Tactic: obtain ⟨h1, h2, h3⟩ := hbij
Cleared hypotheses: hbij
-- 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
⊢ BijOn g (p₁ '' s) (p₂ '' t)
have refine_1 : MapsTo g (p₁ '' s) (p₂ '' t)
Tactic: refine ⟨?_, hinj, ?_⟩
-- 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
refine_1 : MapsTo g (p₁ '' s) (p₂ '' t)
⊢ BijOn g (p₁ '' s) (p₂ '' t)
have refine_2 : SurjOn g (p₁ '' s) (p₂ '' t)
Tactic: refine ⟨?_, hinj, ?_⟩
-- 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
a : α
ha : a ∈ s
⊢ p₂ (f a) = g (p₁ a)
have rw : g (p₁ a) = g (p₁ a)
Tactic: rw [comm a]