awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_5
β : Type u_6
f : α → β
s : Set α
rw : f '' s = ∅ ↔ s = ∅
⊢ ∅ = f '' s ↔ s = ∅
have rw₁ : s = ∅ ↔ s = ∅
Tactic: rw [eq_comm, image_eq_empty]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := (s : Set α) → Set α) (image id) id
have h : ∀ (x : Set α) (x_1 : α), x_1 ∈ id '' x ↔ x_1 ∈ id x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
s : Set α
⊢ (fun (x : α) ↦ x) '' s = s
have h : ∀ (x : α), Membership.mem (γ := Set α) ((fun (x : α) ↦ x) '' s) x ↔ x ∈ s
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
f : α → α
n : ℕ
ih : image f^[n] = (image f)^[n]
⊢ image f^[n + 1] = (image f)^[n + 1]
have succ : image (f ∘ f^[n]) = (image f)^[n + 1]
Tactic: rw [iterate_succ', iterate_succ', ← ih, image_comp_eq]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
f : α → α
n : ℕ
ih : image f^[n] = (image f)^[n]
succ : image (f ∘ f^[n]) = (image f)^[n + 1]
⊢ image f^[n + 1] = (image f)^[n + 1]
have succ₁ : image (f ∘ f^[n]) = image f ∘ (image f)^[n]
Tactic: rw [iterate_succ', iterate_succ', ← ih, image_comp_eq]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
f : α → α
n : ℕ
ih : image f^[n] = (image f)^[n]
succ : image (f ∘ f^[n]) = (image f)^[n + 1]
succ₁ : image (f ∘ f^[n]) = image f ∘ (image f)^[n]
⊢ image f^[n + 1] = (image f)^[n + 1]
have succ₂ : image (f ∘ f^[n]) = image f ∘ image f^[n]
Tactic: rw [iterate_succ', iterate_succ', ← ih, image_comp_eq]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
f : α → α
n : ℕ
ih : image f^[n] = (image f)^[n]
succ : image (f ∘ f^[n]) = (image f)^[n + 1]
succ₁ : image (f ∘ f^[n]) = image f ∘ (image f)^[n]
succ₂ : image (f ∘ f^[n]) = image f ∘ image f^[n]
⊢ image f^[n + 1] = (image f)^[n + 1]
have succ₃ : image f ∘ image f^[n] = image f ∘ image f^[n]
Tactic: rw [iterate_succ', iterate_succ', ← ih, image_comp_eq]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
f : α → α
n : ℕ
⊢ image f^[n] = (image f)^[n]
have zero : image f^[0] = (image f)^[0]
Tactic: induction n with
  | zero => simp
  | succ n ih => rw [iterate_succ', iterate_succ', ← ih, image_comp_eq]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
f : α → α
n : ℕ
zero : image f^[0] = (image f)^[0]
⊢ image f^[n] = (image f)^[n]
have succ : ∀ (n : ℕ) (ih : image f^[n] = (image f)^[n]), image f^[n + 1] = (image f)^[n + 1]
Tactic: induction n with
  | zero => simp
  | succ n ih => rw [iterate_succ', iterate_succ', ← ih, image_comp_eq]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
inst : BooleanAlgebra α
s : Set α
⊢ compl '' compl '' s = s
have rw : compl ∘ compl '' s = s
Tactic: rw [← image_comp, compl_comp_compl, image_id]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
inst : BooleanAlgebra α
s : Set α
rw : compl ∘ compl '' s = s
⊢ compl '' compl '' s = s
have rw₁ : id '' s = s
Tactic: rw [← image_comp, compl_comp_compl, image_id]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
inst : BooleanAlgebra α
s : Set α
rw : compl ∘ compl '' s = s
rw₁ : id '' s = s
⊢ compl '' compl '' s = s
have rw₂ : s = s
Tactic: rw [← image_comp, compl_comp_compl, image_id]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
hfg : LeftInverse g f
s : Set α
x : α
⊢ f x ∈ g ⁻¹' s ↔ x ∈ s
have rw : g (f x) ∈ s ↔ x ∈ s
Tactic: rw [Set.mem_preimage, hfg x]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
hfg : LeftInverse g f
s : Set α
x : α
rw : g (f x) ∈ s ↔ x ∈ s
⊢ f x ∈ g ⁻¹' s ↔ x ∈ s
have rw₁ : x ∈ s ↔ x ∈ s
Tactic: rw [Set.mem_preimage, hfg x]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
⊢ range f ∩ s ⊂ range f ∩ s' ↔ f ⁻¹' s ⊂ f ⁻¹' s'
have simp : (range f ∩ s ⊆ range f ∩ s' ∧ ∃ (x : β), x ∈ range f ∩ s' ∧ ¬x ∈ range f ∩ s) ↔
  f ⁻¹' s ⊆ f ⁻¹' s' ∧ ∃ (x : α), x ∈ f ⁻¹' s' ∧ ¬x ∈ f ⁻¹' s
Tactic: simp only [Set.ssubset_iff_exists]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
⊢ (range f ∩ s ⊆ range f ∩ s' ∧ ∃ (x : β), x ∈ range f ∩ s' ∧ ¬x ∈ range f ∩ s) ↔
    f ⁻¹' s ⊆ f ⁻¹' s' ∧ ∃ (x : α), x ∈ f ⁻¹' s' ∧ ¬x ∈ f ⁻¹' s
have apply : range f ∩ s ⊆ range f ∩ s' ↔ f ⁻¹' s ⊆ f ⁻¹' s'
Tactic: apply and_congr ?_ (by aesop)
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
⊢ range f ∩ s ⊆ range f ∩ s' ↔ f ⁻¹' s ⊆ f ⁻¹' s'
have mp : range f ∩ s ⊆ range f ∩ s' → f ⁻¹' s ⊆ f ⁻¹' s'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
mp : range f ∩ s ⊆ range f ∩ s' → f ⁻¹' s ⊆ f ⁻¹' s'
⊢ range f ∩ s ⊆ range f ∩ s' ↔ f ⁻¹' s ⊆ f ⁻¹' s'
have mpr : f ⁻¹' s ⊆ f ⁻¹' s' → range f ∩ s ⊆ range f ∩ s'
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
r : range f ∩ s ⊆ range f ∩ s'
x : α
hx : x ∈ f ⁻¹' s
⊢ x ∈ f ⁻¹' s'
have mp : ∀ (r : range f ∩ s ⊆ s') (hx : f x ∈ s), f x ∈ s'
Tactic: simp_all only [subset_inter_iff, inter_subset_left, true_and, mem_preimage,
      mem_inter_iff, mem_range, true_and]
Cleared hypotheses: r, hx
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s s' : Set β
r : f ⁻¹' s ⊆ f ⁻¹' s'
x : β
hx : x ∈ range f ∩ s
⊢ x ∈ range f ∩ s'
have mpr : ∀ (hx : (∃ (y : α), f y = x) ∧ x ∈ s), x ∈ s'
Tactic: simp_all only [subset_inter_iff, inter_subset_left, true_and, mem_preimage,
      mem_inter_iff, mem_range, true_and]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
b : β
s : Set α
h₁ : LeftInverse g f
h₂ : RightInverse g f
⊢ b ∈ f '' s ↔ g b ∈ s
have rw : b ∈ g ⁻¹' s ↔ g b ∈ s
Tactic: rw [image_eq_preimage_of_inverse h₁ h₂, mem_preimage]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
b : β
s : Set α
h₁ : LeftInverse g f
h₂ : RightInverse g f
rw : b ∈ g ⁻¹' s ↔ g b ∈ s
⊢ b ∈ f '' s ↔ g b ∈ s
have rw₁ : g b ∈ s ↔ g b ∈ s
Tactic: rw [image_eq_preimage_of_inverse h₁ h₂, mem_preimage]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
H : Surjective f
⊢ f '' s ∪ f '' sᶜ = univ
have rw : f '' (s ∪ sᶜ) = univ
Tactic: rw [← image_union]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t : Set α
⊢ f '' s \ f '' t ⊆ f '' (s \ t)
have rw : f '' s ⊆ f '' (t ∪ s)
Tactic: rw [diff_subset_iff, ← image_union, union_diff_self]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s t : Set α
⊢ f '' s ∆ t = (f '' s) ∆ (f '' t)
have simp_rw : f '' (s \ t ∪ t \ s) = f '' s \ f '' t ∪ f '' t \ f '' s
Tactic: simp_rw [Set.symmDiff_def, image_union, image_diff hf]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s t : Set α
simp_rw : f '' (s \ t ∪ t \ s) = f '' s \ f '' t ∪ f '' t \ f '' s
⊢ f '' s ∆ t = (f '' s) ∆ (f '' t)
have simp_rw₁ : f '' (s \ t) ∪ f '' (t \ s) = f '' s \ f '' t ∪ f '' t \ f '' s
Tactic: simp_rw [Set.symmDiff_def, image_union, image_diff hf]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
hs : s.Nonempty
t : Set β
a : β
⊢ s ⊆ (fun (x : α) ↦ a) ⁻¹' t ↔ a ∈ t
have rw : (fun (x : α) ↦ a) '' s ⊆ t ↔ a ∈ t
Tactic: rw [← image_subset_iff, hs.image_const, singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
hs : s.Nonempty
t : Set β
a : β
rw : (fun (x : α) ↦ a) '' s ⊆ t ↔ a ∈ t
⊢ s ⊆ (fun (x : α) ↦ a) ⁻¹' t ↔ a ∈ t
have rw₁ : {a} ⊆ t ↔ a ∈ t
Tactic: rw [← image_subset_iff, hs.image_const, singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
hs : s.Nonempty
t : Set β
a : β
rw : (fun (x : α) ↦ a) '' s ⊆ t ↔ a ∈ t
rw₁ : {a} ⊆ t ↔ a ∈ t
⊢ s ⊆ (fun (x : α) ↦ a) ⁻¹' t ↔ a ∈ t
have rw₂ : a ∈ t ↔ a ∈ t
Tactic: rw [← image_subset_iff, hs.image_const, singleton_subset_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ (f '' s ∩ t).Nonempty ↔ (s ∩ f ⁻¹' t).Nonempty
have rw : (f '' (s ∩ f ⁻¹' t)).Nonempty ↔ (s ∩ f ⁻¹' t).Nonempty
Tactic: rw [← image_inter_preimage, image_nonempty]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
rw : (f '' (s ∩ f ⁻¹' t)).Nonempty ↔ (s ∩ f ⁻¹' t).Nonempty
⊢ (f '' s ∩ t).Nonempty ↔ (s ∩ f ⁻¹' t).Nonempty
have rw₁ : (s ∩ f ⁻¹' t).Nonempty ↔ (s ∩ f ⁻¹' t).Nonempty
Tactic: rw [← image_inter_preimage, image_nonempty]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ Disjoint (f '' s) t ↔ Disjoint s (f ⁻¹' t)
have simp_rw : f '' s ∩ t = ∅ ↔ s ∩ f ⁻¹' t = ∅
Tactic: simp_rw [disjoint_iff_inter_eq_empty, ← not_nonempty_iff_eq_empty, image_inter_nonempty_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
simp_rw : f '' s ∩ t = ∅ ↔ s ∩ f ⁻¹' t = ∅
⊢ Disjoint (f '' s) t ↔ Disjoint s (f ⁻¹' t)
have simp_rw₁ : ¬(f '' s ∩ t).Nonempty ↔ ¬(s ∩ f ⁻¹' t).Nonempty
Tactic: simp_rw [disjoint_iff_inter_eq_empty, ← not_nonempty_iff_eq_empty, image_inter_nonempty_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ Disjoint t (f '' s) ↔ Disjoint (f ⁻¹' t) s
have rw : Disjoint (f '' s) t ↔ Disjoint (f ⁻¹' t) s
Tactic: rw [disjoint_comm, disjoint_comm (b := s), disjoint_image_left]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
rw : Disjoint (f '' s) t ↔ Disjoint (f ⁻¹' t) s
⊢ Disjoint t (f '' s) ↔ Disjoint (f ⁻¹' t) s
have rw₁ : Disjoint (f '' s) t ↔ Disjoint s (f ⁻¹' t)
Tactic: rw [disjoint_comm, disjoint_comm (b := s), disjoint_image_left]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
rw : Disjoint (f '' s) t ↔ Disjoint (f ⁻¹' t) s
rw₁ : Disjoint (f '' s) t ↔ Disjoint s (f ⁻¹' t)
⊢ Disjoint t (f '' s) ↔ Disjoint (f ⁻¹' t) s
have rw₂ : Disjoint s (f ⁻¹' t) ↔ Disjoint s (f ⁻¹' t)
Tactic: rw [disjoint_comm, disjoint_comm (b := s), disjoint_image_left]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ f '' (s \ f ⁻¹' t) = f '' s \ t
have simp_rw : f '' (s ∩ (f ⁻¹' t)ᶜ) = f '' s ∩ tᶜ
Tactic: simp_rw [diff_eq, ← preimage_compl, image_inter_preimage]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
simp_rw : f '' (s ∩ (f ⁻¹' t)ᶜ) = f '' s ∩ tᶜ
⊢ f '' (s \ f ⁻¹' t) = f '' s \ t
have simp_rw₁ : f '' (s ∩ f ⁻¹' tᶜ) = f '' s ∩ tᶜ
Tactic: simp_rw [diff_eq, ← preimage_compl, image_inter_preimage]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Set α
f : α → β
hf : Injective f
eq : f '' s = f '' t
⊢ s = t
have rw : f ⁻¹' f '' s = t
Tactic: rw [← preimage_image_eq s hf, ← preimage_image_eq t hf, eq]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Set α
f : α → β
hf : Injective f
eq : f '' s = f '' t
rw : f ⁻¹' f '' s = t
⊢ s = t
have rw₁ : f ⁻¹' f '' s = f ⁻¹' f '' t
Tactic: rw [← preimage_image_eq s hf, ← preimage_image_eq t hf, eq]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Set α
f : α → β
hf : Injective f
eq : f '' s = f '' t
rw : f ⁻¹' f '' s = t
rw₁ : f ⁻¹' f '' s = f ⁻¹' f '' t
⊢ s = t
have rw₂ : f ⁻¹' f '' t = f ⁻¹' f '' t
Tactic: rw [← preimage_image_eq s hf, ← preimage_image_eq t hf, eq]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ t ⊆ f '' s ↔ ∃ (u : Set α), u ⊆ s ∧ f '' u = t
have refine : ∀ (h : t ⊆ f '' s), f '' (f ⁻¹' t ∩ s) = t
Tactic: refine ⟨fun h ↦ ⟨f ⁻¹' t ∩ s, inter_subset_right, ?_⟩,
    fun ⟨u, hu, hu'⟩ ↦ hu'.symm ▸ image_mono hu⟩
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
h : t ⊆ f '' s
⊢ f '' (f ⁻¹' t ∩ s) = t
have rwa : t ∩ f '' s = t
Tactic: rwa [image_preimage_inter, inter_eq_left]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a : α | (σ : (a : α) → α) a ≠ a} ⊆ s
⊢ (⇑σ : (a : α) → α) '' s = s
have h : ∀ (i : α), Membership.mem (γ := Set α) ((⇑σ : (a : α) → α) '' s) i ↔ i ∈ s
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a : α | (σ : (a : α) → α) a ≠ a} ⊆ s
i : α
⊢ Membership.mem (γ := Set α) ((⇑σ : (a : α) → α) '' s) i ↔ i ∈ s
have h : ∀ (hi : (σ : (a : α) → α) i = i), Membership.mem (γ := Set α) ((⇑σ : (a : α) → α) '' s) i ↔ i ∈ s
Tactic: obtain hi | hi := eq_or_ne (σ i) i
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a : α | (σ : (a : α) → α) a ≠ a} ⊆ s
i : α
h : ∀ (hi : (σ : (a : α) → α) i = i), Membership.mem (γ := Set α) ((⇑σ : (a : α) → α) '' s) i ↔ i ∈ s
⊢ Membership.mem (γ := Set α) ((⇑σ : (a : α) → α) '' s) i ↔ i ∈ s
have h₁ : ∀ (hi : (σ : (a : α) → α) i ≠ i), Membership.mem (γ := Set α) ((⇑σ : (a : α) → α) '' s) i ↔ i ∈ s
Tactic: obtain hi | hi := eq_or_ne (σ i) i
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a : α | (σ : (a : α) → α) a ≠ a} ⊆ s
i : α
hi : (σ : (a : α) → α) i = i
⊢ Membership.mem (γ := Set α) ((⇑σ : (a : α) → α) '' s) i ↔ i ∈ s
have h : Membership.mem (γ := Set α) ((⇑σ : (a : α) → α) '' s) i → i ∈ s
Tactic: refine ⟨?_, fun h => ⟨i, h, hi⟩⟩
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a : α | (σ : (a : α) → α) a ≠ a} ⊆ s
i : α
hi : (σ : (a : α) → α) i ≠ i
⊢ Membership.mem (γ := Set α) ((⇑σ : (a : α) → α) '' s) i ↔ i ∈ s
have h : ∀ (h : Eq (α := α) ((σ : (a : α) → α) ((Equiv.symm σ : (a : α) → α) i : α) : α) ((Equiv.symm σ : (a : α) → α) i : α)),
  (σ : (a : α) → α) i = i
Tactic: refine iff_of_true ⟨σ.symm i, hs fun h => hi ?_, σ.apply_symm_apply _⟩ (hs hi)
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
s : Set α
a : α
⊢ 𝒫 insert a s = 𝒫 s ∪ insert a '' 𝒫 s
have h : ∀ (t : Set α), t ∈ 𝒫 insert a s ↔ t ∈ 𝒫 s ∪ insert a '' 𝒫 s
Tactic: ext t
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
s : Set α
a : α
t : Set α
⊢ t ∈ 𝒫 insert a s ↔ t ∈ 𝒫 s ∪ insert a '' 𝒫 s
have h : t ∈ 𝒫 insert a s → t ∈ 𝒫 s ∪ insert a '' 𝒫 s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
s : Set α
a : α
t : Set α
h : t ∈ 𝒫 insert a s → t ∈ 𝒫 s ∪ insert a '' 𝒫 s
⊢ t ∈ 𝒫 insert a s ↔ t ∈ 𝒫 s ∪ insert a '' 𝒫 s
have h₁ : t ∈ 𝒫 s ∪ insert a '' 𝒫 s → t ∈ 𝒫 insert a s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
s : Set α
a : α
t : Set α
h : t ∈ 𝒫 insert a s
⊢ t ∈ 𝒫 s ∪ insert a '' 𝒫 s
have pos : ∀ (hs : a ∈ t), t ∈ 𝒫 s ∪ insert a '' 𝒫 s
Tactic: by_cases hs : a ∈ t
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
s : Set α
a : α
t : Set α
h : t ∈ 𝒫 insert a s
pos : ∀ (hs : a ∈ t), t ∈ 𝒫 s ∪ insert a '' 𝒫 s
⊢ t ∈ 𝒫 s ∪ insert a '' 𝒫 s
have neg : ∀ (hs : ¬a ∈ t), t ∈ 𝒫 s ∪ insert a '' 𝒫 s
Tactic: by_cases hs : a ∈ t
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
s : Set α
a : α
t : Set α
h : t ∈ 𝒫 insert a s
hs : a ∈ t
⊢ t ∈ 𝒫 s ∪ insert a '' 𝒫 s
have pos : t ∈ insert a '' 𝒫 s
Tactic: right
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
⊢ f '' sᶜ = range f \ f '' s
have rw : f '' sᶜ = f '' univ \ f '' s
Tactic: rw [← image_univ, ← image_diff hf, compl_eq_univ_diff]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
rw : f '' sᶜ = f '' univ \ f '' s
⊢ f '' sᶜ = range f \ f '' s
have rw₁ : f '' sᶜ = f '' (univ \ s)
Tactic: rw [← image_univ, ← image_diff hf, compl_eq_univ_diff]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
rw : f '' sᶜ = f '' univ \ f '' s
rw₁ : f '' sᶜ = f '' (univ \ s)
⊢ f '' sᶜ = range f \ f '' s
have rw₂ : f '' (univ \ s) = f '' (univ \ s)
Tactic: rw [← image_univ, ← image_diff hf, compl_eq_univ_diff]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s : Set α
⊢ range f \ f '' s = f '' sᶜ
have rw : range f \ f '' s = range f \ f '' s
Tactic: rw [image_compl_eq_range_diff_image hf]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f ⁻¹' s = univ ↔ range f ⊆ s
have rw : univ ⊆ f ⁻¹' s ↔ range f ⊆ s
Tactic: rw [← univ_subset_iff, ← image_subset_iff, image_univ]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
rw : univ ⊆ f ⁻¹' s ↔ range f ⊆ s
⊢ f ⁻¹' s = univ ↔ range f ⊆ s
have rw₁ : f '' univ ⊆ s ↔ range f ⊆ s
Tactic: rw [← univ_subset_iff, ← image_subset_iff, image_univ]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
rw : univ ⊆ f ⁻¹' s ↔ range f ⊆ s
rw₁ : f '' univ ⊆ s ↔ range f ⊆ s
⊢ f ⁻¹' s = univ ↔ range f ⊆ s
have rw₂ : range f ⊆ s ↔ range f ⊆ s
Tactic: rw [← univ_subset_iff, ← image_subset_iff, image_univ]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ f '' s ⊆ range f
have rw : f '' s ⊆ f '' univ
Tactic: rw [← image_univ]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
ι : Sort u_4
f : ι → α
⊢ range f = ∅ ↔ IsEmpty ι
have rw : range f = ∅ ↔ ¬Nonempty ι
Tactic: rw [← not_nonempty_iff, ← range_nonempty_iff_nonempty, not_nonempty_iff_eq_empty]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
ι : Sort u_4
f : ι → α
rw : range f = ∅ ↔ ¬Nonempty ι
⊢ range f = ∅ ↔ IsEmpty ι
have rw₁ : range f = ∅ ↔ ¬(range f).Nonempty
Tactic: rw [← not_nonempty_iff, ← range_nonempty_iff_nonempty, not_nonempty_iff_eq_empty]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
ι : Sort u_4
f : ι → α
rw : range f = ∅ ↔ ¬Nonempty ι
rw₁ : range f = ∅ ↔ ¬(range f).Nonempty
rw₂ : Type u_1
rw₃ : ι → α
⊢ range f = ∅ ↔ IsEmpty ι
have rw₄ : range f = ∅ ↔ range f = ∅
Tactic: rw [← not_nonempty_iff, ← range_nonempty_iff_nonempty, not_nonempty_iff_eq_empty]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
ι : Sort u_4
f : ι → α
inst : Nonempty ι
y : α
⊢ range f = {y} ↔ ∀ (x : ι), f x = y
have simp_rw : (∀ (x : α), (∃ (y : ι), f y = x) ↔ x = y) ↔ ∀ (x : ι), f x = y
Tactic: simp_rw [Set.ext_iff, Set.mem_range, Set.mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
ι : Sort u_4
f : ι → α
inst : Nonempty ι
y : α
h : ∀ (x : α), (∃ (y : ι), f y = x) ↔ x = y
x : ι
⊢ f x = y
have simp_rw : ∃ (y : ι), f y = f x
Tactic: simp_rw [← h, exists_apply_eq_apply]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
ι : Sort u_4
f : ι → α
inst : Nonempty ι
y : α
h : ∀ (x : ι), f x = y
x : α
⊢ (∃ (y : ι), f y = x) ↔ x = y
have simp_rw : (∃ (y_1 : ι), y = x) ↔ x = y
Tactic: simp_rw [h, exists_const, eq_comm]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
ι : Sort u_4
f : ι → α
inst : Nonempty ι
y : α
h : ∀ (x : ι), f x = y
x : α
simp_rw : (∃ (y_1 : ι), y = x) ↔ x = y
⊢ (∃ (y : ι), f y = x) ↔ x = y
have simp_rw₁ : y = x ↔ x = y
Tactic: simp_rw [h, exists_const, eq_comm]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
p : Set β → Prop
⊢ (∃ (s : Set β), s ⊆ range f ∧ p s) ↔ ∃ (s : Set α), p (f '' s)
have rw : (∃ (s : Set β), s ⊆ range f ∧ p s) ↔ ∃ (a : Set β), a ∈ 𝒫 range f ∧ p a
Tactic: rw [← exists_range_iff, range_image]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
p : Set β → Prop
⊢ (∀ (s : Set β), s ⊆ range f → p s) ↔ ∀ (s : Set α), p (f '' s)
have rw : (∀ (s : Set β), s ⊆ range f → p s) ↔ ∀ (a : Set β), a ∈ 𝒫 range f → p a
Tactic: rw [← forall_mem_range, range_image]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
⊢ f ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t
have mp : f ⁻¹' s ⊆ f ⁻¹' t → s ⊆ t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
mp : f ⁻¹' s ⊆ f ⁻¹' t → s ⊆ t
⊢ f ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t
have mpr : s ⊆ t → f ⁻¹' s ⊆ f ⁻¹' t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
h : f ⁻¹' s ⊆ f ⁻¹' t
x : α
hx : x ∈ s
⊢ x ∈ t
have mp : ∀ (y : β) (hx : f y ∈ s), f y ∈ t
Tactic: rcases hs hx with ⟨y, rfl⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
⊢ f ⁻¹' s = f ⁻¹' t ↔ s = t
have mp : f ⁻¹' s = f ⁻¹' t → s = t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
mp : f ⁻¹' s = f ⁻¹' t → s = t
⊢ f ⁻¹' s = f ⁻¹' t ↔ s = t
have mpr : s = t → f ⁻¹' s = f ⁻¹' t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
h : f ⁻¹' s = f ⁻¹' t
⊢ s = t
have mp : s ⊆ t
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
h : f ⁻¹' s = f ⁻¹' t
mp : s ⊆ t
⊢ s = t
have mp₁ : t ⊆ s
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
h : f ⁻¹' s = f ⁻¹' t
⊢ s ⊆ t
have mp : f ⁻¹' s ⊆ f ⁻¹' t
Tactic: rw [← preimage_subset_preimage_iff hs, h]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
h : f ⁻¹' s = f ⁻¹' t
mp : f ⁻¹' s ⊆ f ⁻¹' t
⊢ s ⊆ t
have mp₁ : f ⁻¹' t ⊆ f ⁻¹' t
Tactic: rw [← preimage_subset_preimage_iff hs, h]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
h : f ⁻¹' s = f ⁻¹' t
⊢ t ⊆ s
have mp : f ⁻¹' t ⊆ f ⁻¹' s
Tactic: rw [← preimage_subset_preimage_iff ht, h]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
ht : t ⊆ range f
h : f ⁻¹' s = f ⁻¹' t
mp : f ⁻¹' t ⊆ f ⁻¹' s
⊢ t ⊆ s
have mp₁ : f ⁻¹' t ⊆ f ⁻¹' t
Tactic: rw [← preimage_subset_preimage_iff ht, h]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f ⁻¹' (range f ∩ s) = f ⁻¹' s
have rw : f ⁻¹' (s ∩ range f) = f ⁻¹' s
Tactic: rw [inter_comm, preimage_inter_range]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
rw : f ⁻¹' (s ∩ range f) = f ⁻¹' s
⊢ f ⁻¹' (range f ∩ s) = f ⁻¹' s
have rw₁ : f ⁻¹' s = f ⁻¹' s
Tactic: rw [inter_comm, preimage_inter_range]