awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw₁ : ¬a ∈ s ∧ Disjoint t s ↔ ¬a ∈ s ∧ Disjoint s t
⊢ Disjoint s (insert a t) ↔ ¬a ∈ s ∧ Disjoint s t
have rw₂ : ¬a ∈ s ∧ Disjoint s t ↔ ¬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
x y z w : α
⊢ Eq (α := Set α) {x, y} {z, w} ↔ x = z ∧ y = w ∨ x = w ∧ y = z
have simp : ((x = z ∨ x = w) ∧ (y = z ∨ y = w)) ∧ (z = x ∨ z = y) ∧ (w = x ∨ w = y) ↔ x = z ∧ y = w ∨ x = w ∧ y = z
Tactic: simp [subset_antisymm_iff, insert_subset_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Insert (goal)
Goal:
α : Type u_1
s : Set α
a b : α
hs : s.Nonempty
⊢ s ⊆ {a, b} ↔ s = {a} ∨ s = {b} ∨ s = {a, b}
have rw : ¬s = ∅
Tactic: rw [Set.subset_pair_iff_eq, or_iff_right]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ kernImage f sᶜ = (f '' s)ᶜ
have rw : (f '' sᶜᶜ)ᶜ = (f '' s)ᶜ
Tactic: rw [kernImage_eq_compl, compl_compl]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
rw : (f '' sᶜᶜ)ᶜ = (f '' s)ᶜ
⊢ kernImage f sᶜ = (f '' s)ᶜ
have rw₁ : (f '' s)ᶜ = (f '' s)ᶜ
Tactic: rw [kernImage_eq_compl, compl_compl]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ kernImage f ∅ = (range f)ᶜ
have rw : (f '' ∅ᶜ)ᶜ = (range f)ᶜ
Tactic: rw [kernImage_eq_compl, compl_empty, image_univ]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
rw : (f '' ∅ᶜ)ᶜ = (range f)ᶜ
⊢ kernImage f ∅ = (range f)ᶜ
have rw₁ : (f '' univ)ᶜ = (range f)ᶜ
Tactic: rw [kernImage_eq_compl, compl_empty, image_univ]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
rw : (f '' ∅ᶜ)ᶜ = (range f)ᶜ
rw₁ : (f '' univ)ᶜ = (range f)ᶜ
⊢ kernImage f ∅ = (range f)ᶜ
have rw₂ : (range f)ᶜ = (range f)ᶜ
Tactic: rw [kernImage_eq_compl, compl_empty, image_univ]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ kernImage f (f ⁻¹' s) = s ↔ (range f)ᶜ ⊆ s
have rw : (f '' (f ⁻¹' s)ᶜ)ᶜ = s ↔ (range f)ᶜ ⊆ s
Tactic: rw [kernImage_eq_compl, ← preimage_compl, compl_eq_comm, eq_comm, image_preimage_eq_iff,
      compl_subset_comm]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
rw : (f '' (f ⁻¹' s)ᶜ)ᶜ = s ↔ (range f)ᶜ ⊆ s
⊢ kernImage f (f ⁻¹' s) = s ↔ (range f)ᶜ ⊆ s
have rw₁ : (f '' f ⁻¹' sᶜ)ᶜ = s ↔ (range f)ᶜ ⊆ s
Tactic: rw [kernImage_eq_compl, ← preimage_compl, compl_eq_comm, eq_comm, image_preimage_eq_iff,
      compl_subset_comm]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
rw : (f '' (f ⁻¹' s)ᶜ)ᶜ = s ↔ (range f)ᶜ ⊆ s
rw₁ : (f '' f ⁻¹' sᶜ)ᶜ = s ↔ (range f)ᶜ ⊆ s
⊢ kernImage f (f ⁻¹' s) = s ↔ (range f)ᶜ ⊆ s
have rw₂ : sᶜ = f '' f ⁻¹' sᶜ ↔ (range f)ᶜ ⊆ s
Tactic: rw [kernImage_eq_compl, ← preimage_compl, compl_eq_comm, eq_comm, image_preimage_eq_iff,
      compl_subset_comm]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
rw : (f '' (f ⁻¹' s)ᶜ)ᶜ = s ↔ (range f)ᶜ ⊆ s
rw₁ : (f '' f ⁻¹' sᶜ)ᶜ = s ↔ (range f)ᶜ ⊆ s
rw₂ : sᶜ = f '' f ⁻¹' sᶜ ↔ (range f)ᶜ ⊆ s
⊢ kernImage f (f ⁻¹' s) = s ↔ (range f)ᶜ ⊆ s
have rw₃ : f '' f ⁻¹' sᶜ = sᶜ ↔ (range f)ᶜ ⊆ s
Tactic: rw [kernImage_eq_compl, ← preimage_compl, compl_eq_comm, eq_comm, image_preimage_eq_iff,
      compl_subset_comm]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
rw : (f '' (f ⁻¹' s)ᶜ)ᶜ = s ↔ (range f)ᶜ ⊆ s
rw₁ : (f '' f ⁻¹' sᶜ)ᶜ = s ↔ (range f)ᶜ ⊆ s
rw₂ : sᶜ = f '' f ⁻¹' sᶜ ↔ (range f)ᶜ ⊆ s
rw₃ : f '' f ⁻¹' sᶜ = sᶜ ↔ (range f)ᶜ ⊆ s
⊢ kernImage f (f ⁻¹' s) = s ↔ (range f)ᶜ ⊆ s
have rw₄ : sᶜ ⊆ range f ↔ (range f)ᶜ ⊆ s
Tactic: rw [kernImage_eq_compl, ← preimage_compl, compl_eq_comm, eq_comm, image_preimage_eq_iff,
      compl_subset_comm]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
rw : (f '' (f ⁻¹' s)ᶜ)ᶜ = s ↔ (range f)ᶜ ⊆ s
rw₁ : (f '' f ⁻¹' sᶜ)ᶜ = s ↔ (range f)ᶜ ⊆ s
rw₂ : sᶜ = f '' f ⁻¹' sᶜ ↔ (range f)ᶜ ⊆ s
rw₃ : f '' f ⁻¹' sᶜ = sᶜ ↔ (range f)ᶜ ⊆ s
rw₄ : sᶜ ⊆ range f ↔ (range f)ᶜ ⊆ s
⊢ kernImage f (f ⁻¹' s) = s ↔ (range f)ᶜ ⊆ s
have rw₅ : (range f)ᶜ ⊆ s ↔ (range f)ᶜ ⊆ s
Tactic: rw [kernImage_eq_compl, ← preimage_compl, compl_eq_comm, eq_comm, image_preimage_eq_iff,
      compl_subset_comm]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
⊢ (range f)ᶜ ⊆ kernImage f s
have rw : kernImage f ∅ ⊆ kernImage f s
Tactic: rw [← kernImage_empty]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ kernImage f (s ∪ f ⁻¹' t) = kernImage f s ∪ t
have rw : (f '' (s ∪ f ⁻¹' t)ᶜ)ᶜ = kernImage f s ∪ t
Tactic: rw [kernImage_eq_compl, kernImage_eq_compl, compl_union, ← preimage_compl, image_inter_preimage,
      compl_inter, compl_compl]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
rw : (f '' (s ∪ f ⁻¹' t)ᶜ)ᶜ = kernImage f s ∪ t
⊢ kernImage f (s ∪ f ⁻¹' t) = kernImage f s ∪ t
have rw₁ : (f '' (s ∪ f ⁻¹' t)ᶜ)ᶜ = (f '' sᶜ)ᶜ ∪ t
Tactic: rw [kernImage_eq_compl, kernImage_eq_compl, compl_union, ← preimage_compl, image_inter_preimage,
      compl_inter, compl_compl]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
rw : (f '' (s ∪ f ⁻¹' t)ᶜ)ᶜ = kernImage f s ∪ t
rw₁ : (f '' (s ∪ f ⁻¹' t)ᶜ)ᶜ = (f '' sᶜ)ᶜ ∪ t
⊢ kernImage f (s ∪ f ⁻¹' t) = kernImage f s ∪ t
have rw₂ : (f '' (sᶜ ∩ (f ⁻¹' t)ᶜ))ᶜ = (f '' sᶜ)ᶜ ∪ t
Tactic: rw [kernImage_eq_compl, kernImage_eq_compl, compl_union, ← preimage_compl, image_inter_preimage,
      compl_inter, compl_compl]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
rw : (f '' (s ∪ f ⁻¹' t)ᶜ)ᶜ = kernImage f s ∪ t
rw₁ : (f '' (s ∪ f ⁻¹' t)ᶜ)ᶜ = (f '' sᶜ)ᶜ ∪ t
rw₂ : (f '' (sᶜ ∩ (f ⁻¹' t)ᶜ))ᶜ = (f '' sᶜ)ᶜ ∪ t
⊢ kernImage f (s ∪ f ⁻¹' t) = kernImage f s ∪ t
have rw₃ : (f '' (sᶜ ∩ f ⁻¹' tᶜ))ᶜ = (f '' sᶜ)ᶜ ∪ t
Tactic: rw [kernImage_eq_compl, kernImage_eq_compl, compl_union, ← preimage_compl, image_inter_preimage,
      compl_inter, compl_compl]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
rw : (f '' (s ∪ f ⁻¹' t)ᶜ)ᶜ = kernImage f s ∪ t
rw₁ : (f '' (s ∪ f ⁻¹' t)ᶜ)ᶜ = (f '' sᶜ)ᶜ ∪ t
rw₂ : (f '' (sᶜ ∩ (f ⁻¹' t)ᶜ))ᶜ = (f '' sᶜ)ᶜ ∪ t
rw₃ : (f '' (sᶜ ∩ f ⁻¹' tᶜ))ᶜ = (f '' sᶜ)ᶜ ∪ t
⊢ kernImage f (s ∪ f ⁻¹' t) = kernImage f s ∪ t
have rw₄ : (f '' sᶜ ∩ tᶜ)ᶜ = (f '' sᶜ)ᶜ ∪ t
Tactic: rw [kernImage_eq_compl, kernImage_eq_compl, compl_union, ← preimage_compl, image_inter_preimage,
      compl_inter, compl_compl]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
rw : (f '' (s ∪ f ⁻¹' t)ᶜ)ᶜ = kernImage f s ∪ t
rw₁ : (f '' (s ∪ f ⁻¹' t)ᶜ)ᶜ = (f '' sᶜ)ᶜ ∪ t
rw₂ : (f '' (sᶜ ∩ (f ⁻¹' t)ᶜ))ᶜ = (f '' sᶜ)ᶜ ∪ t
rw₃ : (f '' (sᶜ ∩ f ⁻¹' tᶜ))ᶜ = (f '' sᶜ)ᶜ ∪ t
rw₄ : (f '' sᶜ ∩ tᶜ)ᶜ = (f '' sᶜ)ᶜ ∪ t
⊢ kernImage f (s ∪ f ⁻¹' t) = kernImage f s ∪ t
have rw₅ : (f '' sᶜ)ᶜ ∪ tᶜᶜ = (f '' sᶜ)ᶜ ∪ t
Tactic: rw [kernImage_eq_compl, kernImage_eq_compl, compl_union, ← preimage_compl, image_inter_preimage,
      compl_inter, compl_compl]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
rw : (f '' (s ∪ f ⁻¹' t)ᶜ)ᶜ = kernImage f s ∪ t
rw₁ : (f '' (s ∪ f ⁻¹' t)ᶜ)ᶜ = (f '' sᶜ)ᶜ ∪ t
rw₂ : (f '' (sᶜ ∩ (f ⁻¹' t)ᶜ))ᶜ = (f '' sᶜ)ᶜ ∪ t
rw₃ : (f '' (sᶜ ∩ f ⁻¹' tᶜ))ᶜ = (f '' sᶜ)ᶜ ∪ t
rw₄ : (f '' sᶜ ∩ tᶜ)ᶜ = (f '' sᶜ)ᶜ ∪ t
rw₅ : (f '' sᶜ)ᶜ ∪ tᶜᶜ = (f '' sᶜ)ᶜ ∪ t
⊢ kernImage f (s ∪ f ⁻¹' t) = kernImage f s ∪ t
have rw₆ : (f '' sᶜ)ᶜ ∪ t = (f '' sᶜ)ᶜ ∪ t
Tactic: rw [kernImage_eq_compl, kernImage_eq_compl, compl_union, ← preimage_compl, image_inter_preimage,
      compl_inter, compl_compl]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
⊢ kernImage f (f ⁻¹' t ∪ s) = t ∪ kernImage f s
have rw : kernImage f (s ∪ f ⁻¹' t) = t ∪ kernImage f s
Tactic: rw [union_comm, kernImage_union_preimage, union_comm]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
rw : kernImage f (s ∪ f ⁻¹' t) = t ∪ kernImage f s
⊢ kernImage f (f ⁻¹' t ∪ s) = t ∪ kernImage f s
have rw₁ : kernImage f s ∪ t = t ∪ kernImage f s
Tactic: rw [union_comm, kernImage_union_preimage, union_comm]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
t : Set β
rw : kernImage f (s ∪ f ⁻¹' t) = t ∪ kernImage f s
rw₁ : kernImage f s ∪ t = t ∪ kernImage f s
⊢ kernImage f (f ⁻¹' t ∪ s) = t ∪ kernImage f s
have rw₂ : t ∪ kernImage f s = t ∪ kernImage f s
Tactic: rw [union_comm, kernImage_union_preimage, union_comm]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
hv : (pi (α := α) univ v).Nonempty
i : ι
⊢ (fun (x : (i : ι) → α i) ↦ x i) '' ⋂ (k : ι), (fun (x : (j : ι) → α j) ↦ x k) ⁻¹' v k = v i
have h₁ : (fun (x : (i : ι) → α i) ↦ x i) '' ⋂ (k : ι), (fun (x : (j : ι) → α j) ↦ x k) ⁻¹' v k ⊆ v i
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
hv : (pi (α := α) univ v).Nonempty
i : ι
h₁ : (fun (x : (i : ι) → α i) ↦ x i) '' ⋂ (k : ι), (fun (x : (j : ι) → α j) ↦ x k) ⁻¹' v k ⊆ v i
⊢ (fun (x : (i : ι) → α i) ↦ x i) '' ⋂ (k : ι), (fun (x : (j : ι) → α j) ↦ x k) ⁻¹' v k = v i
have h₂ : v i ⊆ (fun (x : (i : ι) → α i) ↦ x i) '' ⋂ (k : ι), (fun (x : (j : ι) → α j) ↦ x k) ⁻¹' v k
Tactic: apply Subset.antisymm
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
hv : (pi (α := α) univ v).Nonempty
i : ι
y : α i
y_in : y ∈ v i
⊢ Membership.mem (γ := Set (α i))
    ((fun (x : (i : ι) → α i) ↦ x i) '' ⋂ (k : ι), (fun (x : (j : ι) → α j) ↦ x k) ⁻¹' v k) y
have h₂ : ∃ (x : (i : ι) → α i), (∀ (i : ι), x i ∈ v i) ∧ x i = y
Tactic: simp only [mem_image, mem_iInter, mem_preimage]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
hv : (pi (α := α) univ v).Nonempty
i : ι
y : α i
y_in : y ∈ v i
⊢ ∃ (x : (i : ι) → α i), (∀ (i : ι), x i ∈ v i) ∧ x i = y
have h₂ : ∀ (z : (i : ι) → α i) (hz : z ∈ pi (α := α) univ v), ∃ (x : (i : ι) → α i), (∀ (i : ι), x i ∈ v i) ∧ x i = y
Tactic: rcases hv with ⟨z, hz⟩
Cleared hypotheses: hv
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
i : ι
y : α i
y_in : y ∈ v i
z : (i : ι) → α i
hz : z ∈ pi (α := α) univ v
⊢ ∃ (x : (i : ι) → α i), (∀ (i : ι), x i ∈ v i) ∧ x i = y
have h₂ : ∀ (i_1 : ι), update (β := α) z i y i_1 ∈ v i_1
Tactic: refine ⟨Function.update z i y, ?_, update_self i y z⟩
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
i : ι
y : α i
y_in : y ∈ v i
z : (i : ι) → α i
hz : z ∈ pi (α := α) univ v
⊢ ∀ (i_1 : ι), update (β := α) z i y i_1 ∈ v i_1
have h₂ : y ∈ v i ∧ ∀ (x : ι), x ≠ i → z x ∈ v x
Tactic: rw [@forall_update_iff ι α _ z i y fun i t => t ∈ v i]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
hv : (pi (α := α) univ v).Nonempty
i : ι
⊢ (fun (x : (i : ι) → α i) ↦ x i) '' ⋂ (k : ι), (fun (x : (j : ι) → α j) ↦ x k) ⁻¹' v k = v i
have h₁ : (fun (x : (i : ι) → α i) ↦ x i) '' ⋂ (k : ι), (fun (x : (j : ι) → α j) ↦ x k) ⁻¹' v k ⊆ v i
Tactic: classical
    apply Subset.antisymm
    · simp [iInter_subset]
    · intro y y_in
      simp only [mem_image, mem_iInter, mem_preimage]
      rcases hv with ⟨z, hz⟩
      refine ⟨Function.update z i y, ?_, update_self i y z⟩
      rw [@forall_update_iff ι α _ z i y fun i t => t ∈ v i]
      exact ⟨y_in, fun j _ => by simpa using hz j⟩
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
ι : Type u_9
α : ι → Type u_10
v : (i : ι) → Set (α i)
hv : (pi (α := α) univ v).Nonempty
i : ι
h₁ : (fun (x : (i : ι) → α i) ↦ x i) '' ⋂ (k : ι), (fun (x : (j : ι) → α j) ↦ x k) ⁻¹' v k ⊆ v i
⊢ (fun (x : (i : ι) → α i) ↦ x i) '' ⋂ (k : ι), (fun (x : (j : ι) → α j) ↦ x k) ⁻¹' v k = v i
have h₂ : v i ⊆ (fun (x : (i : ι) → α i) ↦ x i) '' ⋂ (k : ι), (fun (x : (j : ι) → α j) ↦ x k) ⁻¹' v k
Tactic: classical
    apply Subset.antisymm
    · simp [iInter_subset]
    · intro y y_in
      simp only [mem_image, mem_iInter, mem_preimage]
      rcases hv with ⟨z, hz⟩
      refine ⟨Function.update z i y, ?_, update_self i y z⟩
      rw [@forall_update_iff ι α _ z i y fun i t => t ∈ v i]
      exact ⟨y_in, fun j _ => by simpa using hz j⟩
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
S : Set (Set α)
f : α → β
⊢ f '' ⋂₀ S ⊆ ⋂ s ∈ S, f '' s
have rw : f '' ⋂ i ∈ S, i ⊆ ⋂ s ∈ S, f '' s
Tactic: rw [sInter_eq_biInter]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
⊢ Injective f ↔ ∀ (i : ι), Injective ((U i).restrictPreimage f)
have refine : ∀ (H : ∀ (i : ι), Injective ((U i).restrictPreimage f)) (x y : α) (e : f x = f y), x = y
Tactic: refine ⟨fun H i => (U i).restrictPreimage_injective H, fun H x y e => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Injective ((U i).restrictPreimage f)
x y : α
e : f x = f y
⊢ f x ∈ iUnion U
have rw : Membership.mem (γ := Set β) univ (f x)
Tactic: rw [hU]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Injective ((U i).restrictPreimage f)
x y : α
e : f x = f y
⊢ x = y
have obtain : ∀ (i : ι) (hi : f x ∈ U i), x = y
Tactic: obtain ⟨i, hi⟩ := Set.mem_iUnion.mp
      (show f x ∈ Set.iUnion U by rw [hU]; trivial)
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
⊢ Surjective f ↔ ∀ (i : ι), Surjective ((U i).restrictPreimage f)
have refine : ∀ (H : ∀ (i : ι), Surjective ((U i).restrictPreimage f)) (x : β), ∃ (a : α), f a = x
Tactic: refine ⟨fun H i => (U i).restrictPreimage_surjective H, fun H x => ?_⟩
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Surjective ((U i).restrictPreimage f)
x : β
⊢ x ∈ iUnion U
have rw : Membership.mem (γ := Set β) univ x
Tactic: rw [hU]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
H : ∀ (i : ι), Surjective ((U i).restrictPreimage f)
x : β
⊢ ∃ (a : α), f a = x
have obtain : ∀ (i : ι) (hi : x ∈ U i), ∃ (a : α), f a = x
Tactic: obtain ⟨i, hi⟩ :=
    Set.mem_iUnion.mp
      (show x ∈ Set.iUnion U by rw [hU]; trivial)
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
U : ι → Set β
hU : iUnion U = univ
⊢ Bijective f ↔ ∀ (i : ι), Bijective ((U i).restrictPreimage f)
have rw : ((∀ (i : ι), Injective ((U i).restrictPreimage f)) ∧ ∀ (i : ι), Surjective ((U i).restrictPreimage f)) ↔
  ∀ (i : ι), Bijective ((U i).restrictPreimage f)
Tactic: rw [Bijective, injective_iff_injective_of_iUnion_eq_univ hU,
    surjective_iff_surjective_of_iUnion_eq_univ hU]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
⊢ f '' ⋂ (i : ι), s i = ⋂ (i : ι), f '' s i
have inhabit : ∀ (inhabited_h : Inhabited ι), f '' ⋂ (i : ι), s i = ⋂ (i : ι), f '' s i
Tactic: inhabit ι
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
⊢ f '' ⋂ (i : ι), s i = ⋂ (i : ι), f '' s i
have refine : ∀ (y : β) (hy : Membership.mem (γ := Set β) (⋂ (i : ι), f '' s i) y), y ∈ f '' ⋂ (i : ι), s i
Tactic: refine Subset.antisymm (image_iInter_subset s f) fun y hy => ?_
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
hy : Membership.mem (γ := Set β) (⋂ (i : ι), f '' s i) y
⊢ y ∈ f '' ⋂ (i : ι), s i
have hy₁ : ∀ (i : ι), ∃ x ∈ s i, f x = y
Tactic: simp only [mem_iInter, mem_image] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
hy : ∀ (i : ι), ∃ x ∈ s i, f x = y
⊢ y ∈ f '' ⋂ (i : ι), s i
have choose : ∀ (x : (i : ι) → α) (hx : ∀ (i : ι), x i ∈ s i) (hy : ∀ (i : ι), f (x i) = y), y ∈ f '' ⋂ (i : ι), s i
Tactic: choose x hx hy using hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
x : (i : ι) → α
hx : ∀ (i : ι), x i ∈ s i
hy : ∀ (i : ι), f (x i) = y
⊢ y ∈ f '' ⋂ (i : ι), s i
have refine : ∀ (i : ι), x default ∈ s i
Tactic: refine ⟨x default, mem_iInter.2 fun i => ?_, hy _⟩
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
x : (i : ι) → α
hx : ∀ (i : ι), x i ∈ s i
hy : ∀ (i : ι), f (x i) = y
i : ι
this : x default = x i
⊢ x default ∈ s i
have rw : x i ∈ s i
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
x : (i : ι) → α
hx : ∀ (i : ι), x i ∈ s i
hy : ∀ (i : ι), f (x i) = y
i : ι
⊢ x default ∈ s i
have suffices : x default = x i
Tactic: suffices x default = x i by
    rw [this]
    apply hx
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
x : (i : ι) → α
hx : ∀ (i : ι), x i ∈ s i
hy : ∀ (i : ι), f (x i) = y
i : ι
⊢ x default = x i
have hx₁ : ∀ (i : ι), Membership.mem (γ := Set α) (⋃ (j : ι), s j) (x i)
Tactic: replace hx : ∀ i, x i ∈ ⋃ j, s j := fun i => (subset_iUnion _ _) (hx i)
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst : Nonempty ι
s : ι → Set α
f : α → β
h : InjOn f (⋃ (i : ι), s i)
inhabited_h : Inhabited ι
y : β
x : (i : ι) → α
hy : ∀ (i : ι), f (x i) = y
i : ι
hx : ∀ (i : ι), Membership.mem (γ := Set α) (⋃ (j : ι), s j) (x i)
⊢ x default = x i
have apply : f (x default) = f (x i)
Tactic: apply h (hx _) (hx _)
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
p : ι → Prop
s : (i : ι) → p i → Set α
hp : ∃ (i : ι), p i
f : α → β
h : InjOn f (⋃ (i : ι), ⋃ (hi : p i), s i hi)
⊢ f '' ⋂ (i : ι), ⋂ (hi : p i), s i hi = ⋂ (i : ι), ⋂ (hi : p i), f '' s i hi
have simp : f '' ⨅ (x : Subtype p), s (↑x : ι) sorry = ⨅ (x : Subtype p), f '' s (↑x : ι) sorry
Tactic: simp only [iInter, iInf_subtype']
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
p : ι → Prop
s : (i : ι) → p i → Set α
hp : ∃ (i : ι), p i
f : α → β
h : InjOn f (⋃ (i : ι), ⋃ (hi : p i), s i hi)
⊢ f '' ⨅ (x : Subtype p), s (↑x : ι) ⋯ = ⨅ (x : Subtype p), f '' s (↑x : ι) ⋯
have this : Nonempty.{max 1 u_5} { i : ι // p i }
Tactic: haveI : Nonempty { i // p i } := nonempty_subtype.2 hp
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
p : ι → Prop
s : (i : ι) → p i → Set α
hp : ∃ (i : ι), p i
f : α → β
h : InjOn f (⋃ (i : ι), ⋃ (hi : p i), s i hi)
this : Nonempty.{max 1 u_5} { i : ι // p i }
⊢ f '' ⨅ (x : Subtype p), s (↑x : ι) ⋯ = ⨅ (x : Subtype p), f '' s (↑x : ι) ⋯
have h₁ : InjOn f (⋃ (i : Subtype p), s (↑i : ι) sorry)
Tactic: apply InjOn.image_iInter_eq
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
hf : Bijective f
s : ι → Set α
⊢ f '' ⋂ (i : ι), s i = ⋂ (i : ι), f '' s i
have inl : IsEmpty ι → f '' ⋂ (i : ι), s i = ⋂ (i : ι), f '' s i
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
hf : Bijective f
s : ι → Set α
inl : IsEmpty ι → f '' ⋂ (i : ι), s i = ⋂ (i : ι), f '' s i
⊢ f '' ⋂ (i : ι), s i = ⋂ (i : ι), f '' s i
have inr : Nonempty ι → f '' ⋂ (i : ι), s i = ⋂ (i : ι), f '' s i
Tactic: cases isEmpty_or_nonempty ι
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
hf : Bijective f
s : ι → Set α
h : IsEmpty ι
⊢ f '' ⋂ (i : ι), s i = ⋂ (i : ι), f '' s i
have inl : f '' univ = univ
Tactic: simp_rw [iInter_of_empty, image_univ_of_surjective hf.surjective]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
hs : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
hx : Membership.mem (γ := Set α) (⋃ (i : ι), s i) x
y : α
hy : Membership.mem (γ := Set α) (⋃ (i : ι), s i) y
hxy : f x = f y
⊢ x = y
have rcases : ∀ (i : ι) (hx : x ∈ s i), x = y
Tactic: rcases mem_iUnion.1 hx with ⟨i, hx⟩
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
hs : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
hx_1 : Membership.mem (γ := Set α) (⋃ (i : ι), s i) x
y : α
hy : Membership.mem (γ := Set α) (⋃ (i : ι), s i) y
hxy : f x = f y
i : ι
hx : x ∈ s i
⊢ x = y
have rcases : ∀ (j : ι) (hy : y ∈ s j), x = y
Tactic: rcases mem_iUnion.1 hy with ⟨j, hy⟩
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
hs : Directed (fun (x1 x2 : Set α) ↦ x1 ⊆ x2) s
f : α → β
hf : ∀ (i : ι), InjOn f (s i)
x : α
hx_1 : Membership.mem (γ := Set α) (⋃ (i : ι), s i) x
y : α
hy_1 : Membership.mem (γ := Set α) (⋃ (i : ι), s i) y
hxy : f x = f y
i : ι
hx : x ∈ s i
j : ι
hy : y ∈ s j
⊢ x = y
have rcases : ∀ (k : ι) (hi : s i ⊆ s k) (hj : s j ⊆ s k), x = y
Tactic: rcases hs i j with ⟨k, hi, hj⟩
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst : Nonempty ι
s : ι → Set α
t : Set β
f : α → β
H : ∀ (i : ι), SurjOn f (s i) t
Hinj : InjOn f (⋃ (i : ι), s i)
y : β
hy : y ∈ t
⊢ y ∈ f '' ⋂ (i : ι), s i
have rw : ∀ (i : ι), y ∈ f '' s i
Tactic: rw [Hinj.image_iInter_eq, mem_iInter]
-- Lean 4 proof step from Mathlib.Data.Set.Lattice.Image (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Sort u_5
f : α → β
s : ι → Set α
⊢ f '' ⋃ (i : ι), s i = ⋃ (i : ι), f '' s i
have h : ∀ (x : β), x ∈ f '' ⋃ (i : ι), s i ↔ Membership.mem (γ := Set β) (⋃ (i : ι), f '' s i) x
Tactic: ext1 x