awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t : Set β
hf : Surjective f
⊢ f ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t
have hs : s ⊆ range f
Tactic: apply Set.preimage_subset_preimage_iff
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t : Set β
hf : Surjective f
⊢ s ⊆ range f
have hs : s ⊆ univ
Tactic: rw [hf.range_eq]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
h : LeftInverse g f
s : Set α
⊢ g '' f '' s = s
have rw : g ∘ f '' s = s
Tactic: rw [← image_comp, h.comp_eq_id, image_id]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
h : LeftInverse g f
s : Set α
rw : g ∘ f '' s = s
⊢ g '' f '' s = s
have rw₁ : id '' s = s
Tactic: rw [← image_comp, h.comp_eq_id, image_id]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
h : LeftInverse g f
s : Set α
rw : g ∘ f '' s = s
rw₁ : id '' s = s
⊢ g '' f '' s = s
have rw₂ : s = s
Tactic: rw [← image_comp, h.comp_eq_id, image_id]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
h : LeftInverse g f
s : Set α
⊢ f ⁻¹' g ⁻¹' s = s
have rw : g ∘ f ⁻¹' s = s
Tactic: rw [← preimage_comp, h.comp_eq_id, preimage_id]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
h : LeftInverse g f
s : Set α
rw : g ∘ f ⁻¹' s = s
⊢ f ⁻¹' g ⁻¹' s = s
have rw₁ : id ⁻¹' s = s
Tactic: rw [← preimage_comp, h.comp_eq_id, preimage_id]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
h : LeftInverse g f
s : Set α
rw : g ∘ f ⁻¹' s = s
rw₁ : id ⁻¹' s = s
⊢ f ⁻¹' g ⁻¹' s = s
have rw₂ : s = s
Tactic: rw [← preimage_comp, h.comp_eq_id, preimage_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 α
⊢ f '' s = range f ∩ g ⁻¹' s
have rw : f '' s = f '' f ⁻¹' g ⁻¹' s
Tactic: rw [← image_preimage_eq_range_inter, hfg.preimage_preimage]
-- 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 α
rw : f '' s = f '' f ⁻¹' g ⁻¹' s
⊢ f '' s = range f ∩ g ⁻¹' s
have rw₁ : f '' s = f '' s
Tactic: rw [← image_preimage_eq_range_inter, hfg.preimage_preimage]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
s t : Set α
h : t ⊆ s
⊢ image (α := (↑s : Type u_1)) (val (p := fun (x : α) ↦ x ∈ s)) {x : (↑s : Type u_1) | (↑x : α) ∈ t} = t
have h₁ : ∀ (x : α),
  Membership.mem (γ := Set α)
      (image (α := (↑s : Type u_1)) (val (p := fun (x : α) ↦ x ∈ s)) {x : (↑s : Type u_1) | (↑x : α) ∈ t}) x ↔
    x ∈ t
Tactic: ext x
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
s : Set α
⊢ range (ι := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)) = s
have rw : image (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)) univ = s
Tactic: rw [← image_univ]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
s : Set α
⊢ Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' s) univ
have rw : Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' s)
  (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' range (ι := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)))
Tactic: rw [← preimage_range, range_coe]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
s : Set α
rw :
  Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' s)
    (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' range (ι := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)))
⊢ Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' s) univ
have rw₁ : { x : α // x ∈ s } → α
Tactic: rw [← preimage_range, range_coe]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
s : Set α
rw :
  Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' s)
    (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' range (ι := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)))
rw₁ : { x : α // x ∈ s } → α
rw₂ : Type u_1
⊢ Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' s) univ
have rw₃ : Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' s) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' s)
Tactic: rw [← preimage_range, range_coe]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
s : Set α
t : Set (↑s : Type u_1)
x : α
h : x ∈ val (p := fun (x : α) ↦ x ∈ s) '' t
y : { x : α // x ∈ s }
left : y ∈ t
yvaleq : (↑y : α) = x
⊢ x ∈ s
have rw : (↑y : α) ∈ s
Tactic: rw [← yvaleq]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
s t u : Set α
⊢ Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u) ↔
    s ∩ t = s ∩ u
have rw : Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u) ↔
  image (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) = s ∩ u
Tactic: rw [← image_preimage_coe, ← image_preimage_coe, coe_injective.image_injective.eq_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
s t u : Set α
rw :
  Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u) ↔
    image (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) = s ∩ u
⊢ Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u) ↔
    s ∩ t = s ∩ u
have rw₁ : Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u) ↔
  image (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) =
    image (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)
Tactic: rw [← image_preimage_coe, ← image_preimage_coe, coe_injective.image_injective.eq_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
s t u : Set α
rw :
  Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u) ↔
    image (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) = s ∩ u
rw₁ :
  Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u) ↔
    image (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) =
      image (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)
⊢ Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u) ↔
    s ∩ t = s ∩ u
have rw₂ : Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u) ↔
  Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)
Tactic: rw [← image_preimage_coe, ← image_preimage_coe, coe_injective.image_injective.eq_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
s t : Set α
⊢ Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' (s ∩ t)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t)
have rw : s ∩ (s ∩ t) = s ∩ t
Tactic: rw [preimage_coe_eq_preimage_coe_iff, ← inter_assoc, inter_self]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
s t : Set α
rw : s ∩ (s ∩ t) = s ∩ t
⊢ Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' (s ∩ t)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t)
have rw₁ : s ∩ s ∩ t = s ∩ t
Tactic: rw [preimage_coe_eq_preimage_coe_iff, ← inter_assoc, inter_self]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
s t : Set α
rw : s ∩ (s ∩ t) = s ∩ t
rw₁ : s ∩ s ∩ t = s ∩ t
⊢ Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' (s ∩ t)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t)
have rw₂ : s ∩ t = s ∩ t
Tactic: rw [preimage_coe_eq_preimage_coe_iff, ← inter_assoc, inter_self]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
s t : Set α
⊢ Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' (t ∩ s)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t)
have rw : Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' (s ∩ t)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t)
Tactic: rw [inter_comm, preimage_coe_self_inter]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
s t : Set α
rw :
  Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' (s ∩ t)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t)
⊢ Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' (t ∩ s)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t)
have rw₁ : Eq (α := Set { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t)
Tactic: rw [inter_comm, preimage_coe_self_inter]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
s t u : Set α
⊢ Subset (α := Set (↑s : Type u_1)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u) ↔
    s ∩ t ⊆ s ∩ u
have mp : Subset (α := Set (↑s : Type u_1)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u) →
  s ∩ t ⊆ s ∩ u
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
s t u : Set α
mp :
  Subset (α := Set (↑s : Type u_1)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u) →
    s ∩ t ⊆ s ∩ u
⊢ Subset (α := Set (↑s : Type u_1)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u) ↔
    s ∩ t ⊆ s ∩ u
have mpr : s ∩ t ⊆ s ∩ u →
  Subset (α := Set (↑s : Type u_1)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
s t u : Set α
⊢ Subset (α := Set (↑s : Type u_1)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u) →
    s ∩ t ⊆ s ∩ u
have mp : Subset (α := Set (↑s : Type u_1)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u) →
  image (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) ⊆
    image (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)
Tactic: rw [← image_preimage_coe, ← image_preimage_coe]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
t : Set α
p : Set α → Prop
⊢ (∃ (s : Set (↑t : Type u_1)), p (val (p := fun (x : α) ↦ x ∈ t) '' s)) ↔ ∃ (s : Set α), s ⊆ t ∧ p s
have rw : (∃ (s : Set α), s ⊆ range (ι := (↑t : Type u_1)) (val (p := fun (x : α) ↦ x ∈ t)) ∧ p s) ↔ ∃ (s : Set α), s ⊆ t ∧ p s
Tactic: rw [← exists_subset_range_and_iff, range_coe]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
t : Set α
p : Set α → Prop
rw :
  (∃ (s : Set α), s ⊆ range (ι := (↑t : Type u_1)) (val (p := fun (x : α) ↦ x ∈ t)) ∧ p s) ↔ ∃ (s : Set α), s ⊆ t ∧ p s
⊢ (∃ (s : Set (↑t : Type u_1)), p (val (p := fun (x : α) ↦ x ∈ t) '' s)) ↔ ∃ (s : Set α), s ⊆ t ∧ p s
have rw₁ : (∃ (s : Set α), s ⊆ t ∧ p s) ↔ ∃ (s : Set α), s ⊆ t ∧ p s
Tactic: rw [← exists_subset_range_and_iff, range_coe]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
t : Set α
p : Set α → Prop
⊢ (∀ (s : Set (↑t : Type u_1)), p (val (p := fun (x : α) ↦ x ∈ t) '' s)) ↔ ∀ (s : Set α), s ⊆ t → p s
have rw : (∀ (s : Set α), s ⊆ range (ι := (↑t : Type u_1)) (val (p := fun (x : α) ↦ x ∈ t)) → p s) ↔ ∀ (s : Set α), s ⊆ t → p s
Tactic: rw [← forall_subset_range_iff, range_coe]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
t : Set α
p : Set α → Prop
rw :
  (∀ (s : Set α), s ⊆ range (ι := (↑t : Type u_1)) (val (p := fun (x : α) ↦ x ∈ t)) → p s) ↔ ∀ (s : Set α), s ⊆ t → p s
⊢ (∀ (s : Set (↑t : Type u_1)), p (val (p := fun (x : α) ↦ x ∈ t) '' s)) ↔ ∀ (s : Set α), s ⊆ t → p s
have rw₁ : (∀ (s : Set α), s ⊆ t → p s) ↔ ∀ (s : Set α), s ⊆ t → p s
Tactic: rw [← forall_subset_range_iff, range_coe]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
s t : Set α
⊢ Set.Nonempty (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) ↔ (s ∩ t).Nonempty
have rw : Set.Nonempty (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) ↔
  (image (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t)).Nonempty
Tactic: rw [← image_preimage_coe, image_nonempty]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
s t : Set α
rw :
  Set.Nonempty (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) ↔
    (image (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s)) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t)).Nonempty
⊢ Set.Nonempty (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) ↔ (s ∩ t).Nonempty
have rw₁ : Set.Nonempty (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t) ↔
  Set.Nonempty (α := { x : α // x ∈ s }) (val (p := fun (x : α) ↦ x ∈ s) ⁻¹' t)
Tactic: rw [← image_preimage_coe, image_nonempty]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : Option α → β
⊢ Injective f ↔ Injective (f ∘ some) ∧ ¬f none ∈ range (f ∘ some)
have simp : Injective f ↔ Injective (f ∘ some) ∧ ∀ (x : α), ¬f (some x) = f none
Tactic: simp only [mem_range, not_exists, (· ∘ ·)]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : Option α → β
⊢ Injective f ↔ Injective (f ∘ some) ∧ ∀ (x : α), ¬f (some x) = f none
have hf : (Injective (f ∘ some) ∧ ∀ (x : α), ¬f (some x) = f none) → Injective f
Tactic: refine
    ⟨fun hf => ⟨hf.comp (Option.some_injective _), fun x => hf.ne <| Option.some_ne_none _⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
b : β
f : α → β
⊢ (range fun (o : Option α) ↦ o.elim b f) = insert b (range f)
have rw : insert (Option.elim none b f) (range.{u_2, u_1 + 1} (ι := α) ((fun (o : Option α) ↦ o.elim b f) ∘ some)) =
  insert b (range f)
Tactic: rw [range_eq]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
b : β
⊢ (fun (o : Option α) ↦ o.elim b f) '' range some = range f
have rw : (range fun (x : α) ↦ (some x).elim b f) = range f
Tactic: rw [← range_comp']
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u
β : Type v
f : α → β
⊢ Surjective (image f) ↔ Surjective f
have refine : ∀ (h : Surjective (image f)) (y : β), ∃ (a : α), f a = y
Tactic: refine ⟨fun h y => ?_, Surjective.image_surjective⟩
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u
β : Type v
f : α → β
h : Surjective (image f)
y : β
⊢ ∃ (a : α), f a = y
have rcases : ∀ (s : Set α) (hs : f '' s = {y}), ∃ (a : α), f a = y
Tactic: rcases h {y} with ⟨s, hs⟩
-- Lean 4 proof step from Mathlib.Data.Set.Image (hypothesis)
Goal:
α : Type u
β : Type v
f : α → β
h : Surjective (image f)
y : β
s : Set α
hs : f '' s = {y}
⊢ ∃ (a : α), f a = y
have this : Membership.mem (γ := Set β) {y} y
Tactic: have := mem_singleton y
-- Lean 4 proof step from Mathlib.Data.Set.Image (hypothesis)
Goal:
α : Type u
β : Type v
f : α → β
h : Surjective (image f)
y : β
s : Set α
hs : f '' s = {y}
this : Membership.mem (γ := Set β) {y} y
⊢ ∃ (a : α), f a = y
have this₁ : y ∈ f '' s
Tactic: rw [← hs] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u
β : Type v
f : α → β
h : Surjective (image f)
y : β
s : Set α
hs : f '' s = {y}
this : y ∈ f '' s
⊢ ∃ (a : α), f a = y
have rcases : ∀ (x : α), x ∈ s → ∀ (hx : f x = y), ∃ (a : α), f a = y
Tactic: rcases this with ⟨x, _, hx⟩
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u
β : Type v
f : α → β
⊢ Injective (image f) ↔ Injective f
have refine : ∀ (h : Injective (image f)) (x x' : α) (hx : f x = f x'), x = x'
Tactic: refine ⟨fun h x x' hx => ?_, Injective.image_injective⟩
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u
β : Type v
f : α → β
h : Injective (image f)
x x' : α
hx : f x = f x'
⊢ x = x'
have rw : Eq (α := Set α) {x} {x'}
Tactic: rw [← singleton_eq_singleton_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u
β : Type v
f : α → β
h : Injective (image f)
x x' : α
hx : f x = f x'
⊢ Eq (α := Set α) {x} {x'}
have a : f '' {x} = f '' {x'}
Tactic: apply h
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u
β : Type v
f : α → β
h : Injective (image f)
x x' : α
hx : f x = f x'
⊢ f '' {x} = f '' {x'}
have a : {f x} = f '' {x'}
Tactic: rw [image_singleton, image_singleton, hx]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u
β : Type v
f : α → β
h : Injective (image f)
x x' : α
hx : f x = f x'
a : {f x} = f '' {x'}
⊢ f '' {x} = f '' {x'}
have a₁ : Eq (α := Set β) {f x} {f x'}
Tactic: rw [image_singleton, image_singleton, hx]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u
β : Type v
f : α → β
h : Injective (image f)
x x' : α
hx : f x = f x'
a : {f x} = f '' {x'}
a₁ : Eq (α := Set β) {f x} {f x'}
⊢ f '' {x} = f '' {x'}
have a₂ : Eq (α := Set β) {f x'} {f x'}
Tactic: rw [image_singleton, image_singleton, hx]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u
β : Type v
f : α → β
hf : Bijective f
s : Set β
t : Set α
⊢ f ⁻¹' s = t ↔ s = f '' t
have rw : f '' f ⁻¹' s = f '' t ↔ s = f '' t
Tactic: rw [← image_eq_image hf.1, hf.2.image_preimage]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u
β : Type v
f : α → β
hf : Bijective f
s : Set β
t : Set α
rw : f '' f ⁻¹' s = f '' t ↔ s = f '' t
⊢ f ⁻¹' s = t ↔ s = f '' t
have rw₁ : s = f '' t ↔ s = f '' t
Tactic: rw [← image_eq_image hf.1, hf.2.image_preimage]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u
β : Type v
f : α → β
hf : Bijective f
s : Set α
t : Set β
⊢ s = f ⁻¹' t ↔ f '' s = t
have rw : f '' s = f '' f ⁻¹' t ↔ f '' s = t
Tactic: rw [← image_eq_image hf.1, hf.2.image_preimage]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u
β : Type v
f : α → β
hf : Bijective f
s : Set α
t : Set β
rw : f '' s = f '' f ⁻¹' t ↔ f '' s = t
⊢ s = f ⁻¹' t ↔ f '' s = t
have rw₁ : f '' s = t ↔ f '' s = t
Tactic: rw [← image_eq_image hf.1, hf.2.image_preimage]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t : Set β
h : Codisjoint s t
⊢ Codisjoint (f ⁻¹' s) (f ⁻¹' t)
have simp : ∀ (h : s ∪ t = ⊤), f ⁻¹' (s ∪ t) = ⊤
Tactic: simp only [codisjoint_iff_le_sup, Set.sup_eq_union, top_le_iff, ← Set.preimage_union] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s t : Set β
h : s ∪ t = ⊤
⊢ f ⁻¹' (s ∪ t) = ⊤
have rw : f ⁻¹' ⊤ = ⊤
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s t : Set β
h : Disjoint (f ⁻¹' s) (f ⁻¹' t)
⊢ Disjoint s t
have rw : s ∩ t = ∅
Tactic: rw [disjoint_iff_inter_eq_empty, ← image_preimage_eq (_ ∩ _) hf, preimage_inter, h.inter_eq,
    image_empty]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s t : Set β
h : Disjoint (f ⁻¹' s) (f ⁻¹' t)
rw : s ∩ t = ∅
⊢ Disjoint s t
have rw₁ : f '' f ⁻¹' (s ∩ t) = ∅
Tactic: rw [disjoint_iff_inter_eq_empty, ← image_preimage_eq (_ ∩ _) hf, preimage_inter, h.inter_eq,
    image_empty]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s t : Set β
h : Disjoint (f ⁻¹' s) (f ⁻¹' t)
rw : s ∩ t = ∅
rw₁ : f '' f ⁻¹' (s ∩ t) = ∅
⊢ Disjoint s t
have rw₂ : f '' (f ⁻¹' s ∩ f ⁻¹' t) = ∅
Tactic: rw [disjoint_iff_inter_eq_empty, ← image_preimage_eq (_ ∩ _) hf, preimage_inter, h.inter_eq,
    image_empty]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s t : Set β
h : Disjoint (f ⁻¹' s) (f ⁻¹' t)
rw : s ∩ t = ∅
rw₁ : f '' f ⁻¹' (s ∩ t) = ∅
rw₂ : f '' (f ⁻¹' s ∩ f ⁻¹' t) = ∅
⊢ Disjoint s t
have rw₃ : f '' ∅ = ∅
Tactic: rw [disjoint_iff_inter_eq_empty, ← image_preimage_eq (_ ∩ _) hf, preimage_inter, h.inter_eq,
    image_empty]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s t : Set β
h : Disjoint (f ⁻¹' s) (f ⁻¹' t)
rw : s ∩ t = ∅
rw₁ : f '' f ⁻¹' (s ∩ t) = ∅
rw₂ : f '' (f ⁻¹' s ∩ f ⁻¹' t) = ∅
rw₃ : f '' ∅ = ∅
⊢ Disjoint s t
have rw₄ : Eq.{u_2 + 1} (α := Set β) ∅ ∅
Tactic: rw [disjoint_iff_inter_eq_empty, ← image_preimage_eq (_ ∩ _) hf, preimage_inter, h.inter_eq,
    image_empty]
-- Lean 4 proof step from Mathlib.Data.Set.Image (hypothesis)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
h : f ⁻¹' s = ∅
⊢ Disjoint s (range f)
have h₁ : ∀ (x : α), ¬f x ∈ s
Tactic: simp only [eq_empty_iff_forall_notMem, mem_preimage] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Data.Set.Insert (goal)
Goal:
α : Type u_1
β : Type u_2
s t : Set α
a_1 b x a : α
⊢ Membership.mem (γ := Set α) (insert x ∅) a ↔ Membership.mem (γ := Set α) {x} a
have simp : a = x ↔ Membership.mem (γ := Set α) {x} a
Tactic: simp only [mem_empty_iff_false, mem_insert_iff, or_false]
-- Lean 4 proof step from Mathlib.Data.Set.Insert (goal)
Goal:
α : Type u_1
s : Set α
a : α
⊢ (s ∩ {a}).Nonempty ↔ a ∈ s
have rw : ({a} ∩ s).Nonempty ↔ a ∈ s
Tactic: rw [inter_comm, singleton_inter_nonempty]
-- Lean 4 proof step from Mathlib.Data.Set.Insert (goal)
Goal:
α : Type u_1
s : Set α
a : α
rw : ({a} ∩ s).Nonempty ↔ a ∈ s
⊢ (s ∩ {a}).Nonempty ↔ a ∈ s
have rw₁ : a ∈ s ↔ a ∈ s
Tactic: rw [inter_comm, singleton_inter_nonempty]
-- Lean 4 proof step from Mathlib.Data.Set.Insert (goal)
Goal:
α : Type u_1
s : Set α
a : α
⊢ s ∩ {a} = ∅ ↔ ¬a ∈ s
have rw : {a} ∩ s = ∅ ↔ ¬a ∈ s
Tactic: rw [inter_comm, singleton_inter_eq_empty]
-- Lean 4 proof step from Mathlib.Data.Set.Insert (goal)
Goal:
α : Type u_1
s : Set α
a : α
rw : {a} ∩ s = ∅ ↔ ¬a ∈ s
⊢ s ∩ {a} = ∅ ↔ ¬a ∈ s
have rw₁ : ¬a ∈ s ↔ ¬a ∈ s
Tactic: rw [inter_comm, singleton_inter_eq_empty]
-- Lean 4 proof step from Mathlib.Data.Set.Insert (goal)
Goal:
α : Type u_1
l : List α
H : l.Nodup
a : α
⊢ Eq (α := Set α) {x : α | x ∈ l} {a} ↔ l = [a]
have mp : Eq (α := Set α) {x : α | x ∈ l} {a} → l = [a]
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Insert (goal)
Goal:
α : Type u_1
l : List α
H : l.Nodup
a : α
mp : Eq (α := Set α) {x : α | x ∈ l} {a} → l = [a]
⊢ Eq (α := Set α) {x : α | x ∈ l} {a} ↔ l = [a]
have mpr : l = [a] → Eq (α := Set α) {x : α | x ∈ l} {a}
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Insert (goal)
Goal:
α : Type u_1
l : List α
H : l.Nodup
a : α
⊢ Eq (α := Set α) {x : α | x ∈ l} {a} → l = [a]
have mp : (∃ (n : ℕ), n > 0 ∧ l = List.replicate n a) → l = [a]
Tactic: rw [setOf_mem_list_eq_replicate]
-- Lean 4 proof step from Mathlib.Data.Set.Insert (hypothesis)
Goal:
α : Type u_1
a : α
n : ℕ
hn : n > 0
H : (List.replicate n a).Nodup
⊢ List.replicate n a = [a]
have H₁ : n ≤ 1
Tactic: simp only [List.nodup_replicate] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.Set.Insert (goal)
Goal:
α : Type u_1
s : Set α
x : α
⊢ s ⊂ {x} ↔ s = ∅
have rw : s = ∅ → s ≠ {x}
Tactic: rw [ssubset_iff_subset_ne, subset_singleton_iff_eq, or_and_right, and_not_self_iff, or_false,
    and_iff_left_iff_imp]
-- Lean 4 proof step from Mathlib.Data.Set.Insert (goal)
Goal:
α : Type u_1
s t : Set α
a : α
⊢ Disjoint s (insert a t) ↔ ¬a ∈ s ∧ Disjoint s t
have rw : Disjoint (insert a t) s ↔ ¬a ∈ s ∧ Disjoint s t
Tactic: rw [disjoint_comm, disjoint_insert_left, disjoint_comm]
-- Lean 4 proof step from Mathlib.Data.Set.Insert (goal)
Goal:
α : Type u_1
s t : Set α
a : α
rw : Disjoint (insert a t) s ↔ ¬a ∈ s ∧ Disjoint s t
⊢ Disjoint s (insert a t) ↔ ¬a ∈ s ∧ Disjoint s t
have rw₁ : ¬a ∈ s ∧ Disjoint t s ↔ ¬a ∈ s ∧ Disjoint s t
Tactic: rw [disjoint_comm, disjoint_insert_left, disjoint_comm]