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 : Set β
⊢ f ⁻¹' f '' f ⁻¹' s = f ⁻¹' s
have rw : f ⁻¹' (range f ∩ s) = f ⁻¹' s
Tactic: rw [image_preimage_eq_range_inter, preimage_range_inter]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
rw : f ⁻¹' (range f ∩ s) = f ⁻¹' s
⊢ f ⁻¹' f '' f ⁻¹' s = f ⁻¹' s
have rw₁ : f ⁻¹' s = f ⁻¹' s
Tactic: rw [image_preimage_eq_range_inter, preimage_range_inter]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
⊢ Eq (α := Set (α ⊕ β)) (range Sum.inl) {x : α ⊕ β | x.isLeft = true}
have h : ∀ (val : α),
  Membership.mem (γ := Set (α ⊕ β)) (range Sum.inl) (Sum.inl val) ↔
    Membership.mem (γ := Set (α ⊕ β)) {x : α ⊕ β | x.isLeft = true} (Sum.inl val)
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
h :
  ∀ (val : α),
    Membership.mem (γ := Set (α ⊕ β)) (range Sum.inl) (Sum.inl val) ↔
      Membership.mem (γ := Set (α ⊕ β)) {x : α ⊕ β | x.isLeft = true} (Sum.inl val)
⊢ Eq (α := Set (α ⊕ β)) (range Sum.inl) {x : α ⊕ β | x.isLeft = true}
have h₁ : ∀ (val : β),
  Membership.mem (γ := Set (α ⊕ β)) (range Sum.inl) (Sum.inr val) ↔
    Membership.mem (γ := Set (α ⊕ β)) {x : α ⊕ β | x.isLeft = true} (Sum.inr val)
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
⊢ Eq (α := Set (α ⊕ β)) (range Sum.inr) {x : α ⊕ β | x.isRight = true}
have h : ∀ (val : α),
  Membership.mem (γ := Set (α ⊕ β)) (range Sum.inr) (Sum.inl val) ↔
    Membership.mem (γ := Set (α ⊕ β)) {x : α ⊕ β | x.isRight = true} (Sum.inl val)
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
h :
  ∀ (val : α),
    Membership.mem (γ := Set (α ⊕ β)) (range Sum.inr) (Sum.inl val) ↔
      Membership.mem (γ := Set (α ⊕ β)) {x : α ⊕ β | x.isRight = true} (Sum.inl val)
⊢ Eq (α := Set (α ⊕ β)) (range Sum.inr) {x : α ⊕ β | x.isRight = true}
have h₁ : ∀ (val : β),
  Membership.mem (γ := Set (α ⊕ β)) (range Sum.inr) (Sum.inr val) ↔
    Membership.mem (γ := Set (α ⊕ β)) {x : α ⊕ β | x.isRight = true} (Sum.inr val)
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
x : α
⊢ Membership.mem (γ := Set (α ⊕ β)) (range Sum.inl ⊔ range Sum.inr) (Sum.inl x)
have inl : Membership.mem (γ := Set (α ⊕ β)) (range Sum.inl) (Sum.inl x)
Tactic: left
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
y : β
⊢ Membership.mem (γ := Set (α ⊕ β)) (range Sum.inl ⊔ range Sum.inr) (Sum.inr y)
have inr : Membership.mem (γ := Set (α ⊕ β)) (range Sum.inr) (Sum.inr y)
Tactic: right
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set β
⊢ Eq.{u_1 + 1} (α := Set α) (Sum.inl ⁻¹' Sum.inr '' s) ∅
have h : ∀ (x : α), Membership.mem (γ := Set α) (Sum.inl ⁻¹' Sum.inr '' s) x ↔ Membership.mem (γ := Set α) ∅ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
⊢ Eq.{u_2 + 1} (α := Set β) (Sum.inr ⁻¹' Sum.inl '' s) ∅
have h : ∀ (x : β), Membership.mem (γ := Set β) (Sum.inr ⁻¹' Sum.inl '' s) x ↔ Membership.mem (γ := Set β) ∅ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
⊢ Eq.{u_1 + 1} (α := Set α) (preimage (β := α ⊕ β) Sum.inl (range Sum.inr)) ∅
have rw : Eq.{u_1 + 1} (α := Set α) (preimage (β := α ⊕ β) Sum.inl (Sum.inr '' univ)) ∅
Tactic: rw [← image_univ, preimage_inl_image_inr]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
rw : Eq.{u_1 + 1} (α := Set α) (preimage (β := α ⊕ β) Sum.inl (Sum.inr '' univ)) ∅
⊢ Eq.{u_1 + 1} (α := Set α) (preimage (β := α ⊕ β) Sum.inl (range Sum.inr)) ∅
have rw₁ : Eq.{u_1 + 1} (α := Set α) ∅ ∅
Tactic: rw [← image_univ, preimage_inl_image_inr]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
⊢ Eq.{u_2 + 1} (α := Set β) (preimage (β := α ⊕ β) Sum.inr (range Sum.inl)) ∅
have rw : Eq.{u_2 + 1} (α := Set β) (preimage (β := α ⊕ β) Sum.inr (Sum.inl '' univ)) ∅
Tactic: rw [← image_univ, preimage_inr_image_inl]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
rw : Eq.{u_2 + 1} (α := Set β) (preimage (β := α ⊕ β) Sum.inr (Sum.inl '' univ)) ∅
⊢ Eq.{u_2 + 1} (α := Set β) (preimage (β := α ⊕ β) Sum.inr (range Sum.inl)) ∅
have rw₁ : Eq.{u_2 + 1} (α := Set β) ∅ ∅
Tactic: rw [← image_univ, preimage_inr_image_inl]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set γ
f : α → γ
g : β → γ
⊢ Sum.elim f g ⁻¹' s = Sum.inl '' f ⁻¹' s ∪ Sum.inr '' g ⁻¹' s
have h : ∀ (val : α), Sum.inl val ∈ Sum.elim f g ⁻¹' s ↔ Sum.inl val ∈ Sum.inl '' f ⁻¹' s ∪ Sum.inr '' g ⁻¹' s
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set γ
f : α → γ
g : β → γ
h : ∀ (val : α), Sum.inl val ∈ Sum.elim f g ⁻¹' s ↔ Sum.inl val ∈ Sum.inl '' f ⁻¹' s ∪ Sum.inr '' g ⁻¹' s
⊢ Sum.elim f g ⁻¹' s = Sum.inl '' f ⁻¹' s ∪ Sum.inr '' g ⁻¹' s
have h₁ : ∀ (val : β), Sum.inr val ∈ Sum.elim f g ⁻¹' s ↔ Sum.inr val ∈ Sum.inl '' f ⁻¹' s ∪ Sum.inr '' g ⁻¹' s
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set (α ⊕ β)
⊢ Sum.inl '' Sum.inl ⁻¹' s ∪ Sum.inr '' Sum.inr ⁻¹' s = s
have rw : Sum.elim Sum.inl Sum.inr ⁻¹' s = s
Tactic: rw [← preimage_sumElim, Sum.elim_inl_inr, preimage_id]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set (α ⊕ β)
rw : Sum.elim Sum.inl Sum.inr ⁻¹' s = s
⊢ Sum.inl '' Sum.inl ⁻¹' s ∪ Sum.inr '' Sum.inr ⁻¹' s = s
have rw₁ : id ⁻¹' s = s
Tactic: rw [← preimage_sumElim, Sum.elim_inl_inr, preimage_id]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set (α ⊕ β)
rw : Sum.elim Sum.inl Sum.inr ⁻¹' s = s
rw₁ : id ⁻¹' s = s
⊢ Sum.inl '' Sum.inl ⁻¹' s ∪ Sum.inr '' Sum.inr ⁻¹' s = s
have rw₂ : s = s
Tactic: rw [← preimage_sumElim, Sum.elim_inl_inr, preimage_id]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
⊢ range (Subtype.map (p := p) (q := q) f h) = Subtype.val (p := q) ⁻¹' f '' {x : α | p x}
have h₁ : ∀ (x : β) (hx : q x),
  Subtype.mk (p := q) x hx ∈ range (Subtype.map (p := p) (q := q) f h) ↔
    Membership.mem (γ := Set (Subtype q)) (Subtype.val (p := q) ⁻¹' f '' {x : α | p x}) (Subtype.mk (p := q) x hx)
Tactic: ext ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
⊢ Subtype.mk (p := q) x hx ∈ range (Subtype.map (p := p) (q := q) f h) ↔
    Membership.mem (γ := Set (Subtype q)) (Subtype.val (p := q) ⁻¹' f '' {x : α | p x}) (Subtype.mk (p := q) x hx)
have h₁ : (∃ (a : α), ∃ (h_1 : p a), Subtype.mk (p := q) (f a) sorry = Subtype.mk (p := q) x hx) ↔
  ∃ (x_1 : α), Membership.mem (γ := Set α) {x : α | p x} x_1 ∧ f x_1 = x
Tactic: simp_rw [mem_preimage, mem_range, mem_image, Subtype.exists, Subtype.map]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f '' (f ⁻¹' s)ᶜ = range f \ s
have rw : f '' (univ \ f ⁻¹' s) = range f \ s
Tactic: rw [compl_eq_univ_diff, image_diff_preimage, image_univ]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
rw : f '' (univ \ f ⁻¹' s) = range f \ s
⊢ f '' (f ⁻¹' s)ᶜ = range f \ s
have rw₁ : f '' univ \ s = range f \ s
Tactic: rw [compl_eq_univ_diff, image_diff_preimage, image_univ]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
rw : f '' (univ \ f ⁻¹' s) = range f \ s
rw₁ : f '' univ \ s = range f \ s
⊢ f '' (f ⁻¹' s)ᶜ = range f \ s
have rw₂ : range f \ s = range f \ s
Tactic: rw [compl_eq_univ_diff, image_diff_preimage, 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 fun (x : (↑s : Type u_1)) ↦ f (↑x : α)
have h : ∀ (x : β), x ∈ f '' s ↔ Membership.mem (γ := Set β) (range fun (x : (↑s : Type u_1)) ↦ f (↑x : α)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
x : β
⊢ x ∈ f '' s ↔ Membership.mem (γ := Set β) (range fun (x : (↑s : Type u_1)) ↦ f (↑x : α)) x
have h : x ∈ f '' s → Membership.mem (γ := Set β) (range fun (x : (↑s : Type u_1)) ↦ f (↑x : α)) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
x : β
h : x ∈ f '' s → Membership.mem (γ := Set β) (range fun (x : (↑s : Type u_1)) ↦ f (↑x : α)) x
⊢ x ∈ f '' s ↔ Membership.mem (γ := Set β) (range fun (x : (↑s : Type u_1)) ↦ f (↑x : α)) x
have h₁ : Membership.mem (γ := Set β) (range fun (x : (↑s : Type u_1)) ↦ f (↑x : α)) x → x ∈ f '' s
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
s t : Set α
h : s ⊆ t
⊢ range (inclusion (s := s) (t := t) h) = {x : (↑t : Type u_1) | (↑x : α) ∈ s}
have h₁ : ∀ (x : α) (hx : x ∈ t),
  Subtype.mk (p := fun (x : α) ↦ x ∈ t) x hx ∈ range (inclusion (s := s) (t := t) h) ↔
    Membership.mem (γ := Set (↑t : Type u_1)) {x : (↑t : Type u_1) | (↑x : α) ∈ s}
      (Subtype.mk (p := fun (x : α) ↦ x ∈ t) x hx)
Tactic: ext ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
x : (↑(range f) : Type u_2)
⊢ rangeFactorization f (rangeSplitting f x) = x
have a : (↑(rangeFactorization f (rangeSplitting f x)) : β) = (↑x : β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
x : (↑(range f) : Type u_2)
⊢ (↑(rangeFactorization f (rangeSplitting f x)) : β) = (↑x : β)
have a : f (rangeSplitting f x) = (↑x : β)
Tactic: simp only [rangeFactorization_coe]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_5
β : Type u_6
γ : Type u_7
γ' : Type u_8
δ : Type u_9
δ' : Type u_10
h : β → α
f : γ → β
f₁ : γ' → α
f₂ : γ → γ'
g : δ → β
g₁ : δ' → α
g₂ : δ → δ'
hf : h ∘ f = f₁ ∘ f₂
hg : h ∘ g = g₁ ∘ g₂
hfg : range f ∪ range g = univ
s : Set β
⊢ h '' s = f₁ '' f₂ '' f ⁻¹' s ∪ g₁ '' g₂ '' g ⁻¹' s
have rw : h '' s = f₁ ∘ f₂ '' f ⁻¹' s ∪ g₁ '' g₂ '' g ⁻¹' s
Tactic: rw [← image_comp, ← image_comp, ← hf, ← hg, image_comp, image_comp, image_preimage_eq_inter_range,
    image_preimage_eq_inter_range, ← image_union, ← inter_union_distrib_left, hfg, inter_univ]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_5
β : Type u_6
γ : Type u_7
γ' : Type u_8
δ : Type u_9
δ' : Type u_10
h : β → α
f : γ → β
f₁ : γ' → α
f₂ : γ → γ'
g : δ → β
g₁ : δ' → α
g₂ : δ → δ'
hf : h ∘ f = f₁ ∘ f₂
hg : h ∘ g = g₁ ∘ g₂
hfg : range f ∪ range g = univ
s : Set β
rw : h '' s = f₁ ∘ f₂ '' f ⁻¹' s ∪ g₁ '' g₂ '' g ⁻¹' s
⊢ h '' s = f₁ '' f₂ '' f ⁻¹' s ∪ g₁ '' g₂ '' g ⁻¹' s
have rw₁ : h '' s = f₁ ∘ f₂ '' f ⁻¹' s ∪ g₁ ∘ g₂ '' g ⁻¹' s
Tactic: rw [← image_comp, ← image_comp, ← hf, ← hg, image_comp, image_comp, image_preimage_eq_inter_range,
    image_preimage_eq_inter_range, ← image_union, ← inter_union_distrib_left, hfg, inter_univ]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_5
β : Type u_6
γ : Type u_7
γ' : Type u_8
δ : Type u_9
δ' : Type u_10
h : β → α
f : γ → β
f₁ : γ' → α
f₂ : γ → γ'
g : δ → β
g₁ : δ' → α
g₂ : δ → δ'
hf : h ∘ f = f₁ ∘ f₂
hg : h ∘ g = g₁ ∘ g₂
hfg : range f ∪ range g = univ
s : Set β
rw : h '' s = f₁ ∘ f₂ '' f ⁻¹' s ∪ g₁ '' g₂ '' g ⁻¹' s
rw₁ : h '' s = f₁ ∘ f₂ '' f ⁻¹' s ∪ g₁ ∘ g₂ '' g ⁻¹' s
⊢ h '' s = f₁ '' f₂ '' f ⁻¹' s ∪ g₁ '' g₂ '' g ⁻¹' s
have rw₂ : h '' s = h ∘ f '' f ⁻¹' s ∪ g₁ ∘ g₂ '' g ⁻¹' s
Tactic: rw [← image_comp, ← image_comp, ← hf, ← hg, image_comp, image_comp, image_preimage_eq_inter_range,
    image_preimage_eq_inter_range, ← image_union, ← inter_union_distrib_left, hfg, inter_univ]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_5
β : Type u_6
γ : Type u_7
γ' : Type u_8
δ : Type u_9
δ' : Type u_10
h : β → α
f : γ → β
f₁ : γ' → α
f₂ : γ → γ'
g : δ → β
g₁ : δ' → α
g₂ : δ → δ'
hf : h ∘ f = f₁ ∘ f₂
hg : h ∘ g = g₁ ∘ g₂
hfg : range f ∪ range g = univ
s : Set β
rw : h '' s = f₁ ∘ f₂ '' f ⁻¹' s ∪ g₁ '' g₂ '' g ⁻¹' s
rw₁ : h '' s = f₁ ∘ f₂ '' f ⁻¹' s ∪ g₁ ∘ g₂ '' g ⁻¹' s
rw₂ : h '' s = h ∘ f '' f ⁻¹' s ∪ g₁ ∘ g₂ '' g ⁻¹' s
⊢ h '' s = f₁ '' f₂ '' f ⁻¹' s ∪ g₁ '' g₂ '' g ⁻¹' s
have rw₃ : h '' s = h ∘ f '' f ⁻¹' s ∪ h ∘ g '' g ⁻¹' s
Tactic: rw [← image_comp, ← image_comp, ← hf, ← hg, image_comp, image_comp, image_preimage_eq_inter_range,
    image_preimage_eq_inter_range, ← image_union, ← inter_union_distrib_left, hfg, inter_univ]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_5
β : Type u_6
γ : Type u_7
γ' : Type u_8
δ : Type u_9
δ' : Type u_10
h : β → α
f : γ → β
f₁ : γ' → α
f₂ : γ → γ'
g : δ → β
g₁ : δ' → α
g₂ : δ → δ'
hf : h ∘ f = f₁ ∘ f₂
hg : h ∘ g = g₁ ∘ g₂
hfg : range f ∪ range g = univ
s : Set β
rw : h '' s = f₁ ∘ f₂ '' f ⁻¹' s ∪ g₁ '' g₂ '' g ⁻¹' s
rw₁ : h '' s = f₁ ∘ f₂ '' f ⁻¹' s ∪ g₁ ∘ g₂ '' g ⁻¹' s
rw₂ : h '' s = h ∘ f '' f ⁻¹' s ∪ g₁ ∘ g₂ '' g ⁻¹' s
rw₃ : h '' s = h ∘ f '' f ⁻¹' s ∪ h ∘ g '' g ⁻¹' s
⊢ h '' s = f₁ '' f₂ '' f ⁻¹' s ∪ g₁ '' g₂ '' g ⁻¹' s
have rw₄ : h '' s = h '' f '' f ⁻¹' s ∪ h ∘ g '' g ⁻¹' s
Tactic: rw [← image_comp, ← image_comp, ← hf, ← hg, image_comp, image_comp, image_preimage_eq_inter_range,
    image_preimage_eq_inter_range, ← image_union, ← inter_union_distrib_left, hfg, inter_univ]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_5
β : Type u_6
γ : Type u_7
γ' : Type u_8
δ : Type u_9
δ' : Type u_10
h : β → α
f : γ → β
f₁ : γ' → α
f₂ : γ → γ'
g : δ → β
g₁ : δ' → α
g₂ : δ → δ'
hf : h ∘ f = f₁ ∘ f₂
hg : h ∘ g = g₁ ∘ g₂
hfg : range f ∪ range g = univ
s : Set β
rw : h '' s = f₁ ∘ f₂ '' f ⁻¹' s ∪ g₁ '' g₂ '' g ⁻¹' s
rw₁ : h '' s = f₁ ∘ f₂ '' f ⁻¹' s ∪ g₁ ∘ g₂ '' g ⁻¹' s
rw₂ : h '' s = h ∘ f '' f ⁻¹' s ∪ g₁ ∘ g₂ '' g ⁻¹' s
rw₃ : h '' s = h ∘ f '' f ⁻¹' s ∪ h ∘ g '' g ⁻¹' s
rw₄ : h '' s = h '' f '' f ⁻¹' s ∪ h ∘ g '' g ⁻¹' s
⊢ h '' s = f₁ '' f₂ '' f ⁻¹' s ∪ g₁ '' g₂ '' g ⁻¹' s
have rw₅ : h '' s = h '' f '' f ⁻¹' s ∪ h '' g '' g ⁻¹' s
Tactic: rw [← image_comp, ← image_comp, ← hf, ← hg, image_comp, image_comp, image_preimage_eq_inter_range,
    image_preimage_eq_inter_range, ← image_union, ← inter_union_distrib_left, hfg, inter_univ]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_5
β : Type u_6
γ : Type u_7
γ' : Type u_8
δ : Type u_9
δ' : Type u_10
h : β → α
f : γ → β
f₁ : γ' → α
f₂ : γ → γ'
g : δ → β
g₁ : δ' → α
g₂ : δ → δ'
hf : h ∘ f = f₁ ∘ f₂
hg : h ∘ g = g₁ ∘ g₂
hfg : range f ∪ range g = univ
s : Set β
rw : h '' s = f₁ ∘ f₂ '' f ⁻¹' s ∪ g₁ '' g₂ '' g ⁻¹' s
rw₁ : h '' s = f₁ ∘ f₂ '' f ⁻¹' s ∪ g₁ ∘ g₂ '' g ⁻¹' s
rw₂ : h '' s = h ∘ f '' f ⁻¹' s ∪ g₁ ∘ g₂ '' g ⁻¹' s
rw₃ : h '' s = h ∘ f '' f ⁻¹' s ∪ h ∘ g '' g ⁻¹' s
rw₄ : h '' s = h '' f '' f ⁻¹' s ∪ h ∘ g '' g ⁻¹' s
rw₅ : h '' s = h '' f '' f ⁻¹' s ∪ h '' g '' g ⁻¹' s
⊢ h '' s = f₁ '' f₂ '' f ⁻¹' s ∪ g₁ '' g₂ '' g ⁻¹' s
have rw₆ : h '' s = h '' (s ∩ range f) ∪ h '' g '' g ⁻¹' s
Tactic: rw [← image_comp, ← image_comp, ← hf, ← hg, image_comp, image_comp, image_preimage_eq_inter_range,
    image_preimage_eq_inter_range, ← image_union, ← inter_union_distrib_left, hfg, inter_univ]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_5
β : Type u_6
γ : Type u_7
γ' : Type u_8
δ : Type u_9
δ' : Type u_10
h : β → α
f : γ → β
f₁ : γ' → α
f₂ : γ → γ'
g : δ → β
g₁ : δ' → α
g₂ : δ → δ'
hf : h ∘ f = f₁ ∘ f₂
hg : h ∘ g = g₁ ∘ g₂
hfg : range f ∪ range g = univ
s : Set β
rw : h '' s = f₁ ∘ f₂ '' f ⁻¹' s ∪ g₁ '' g₂ '' g ⁻¹' s
rw₁ : h '' s = f₁ ∘ f₂ '' f ⁻¹' s ∪ g₁ ∘ g₂ '' g ⁻¹' s
rw₂ : h '' s = h ∘ f '' f ⁻¹' s ∪ g₁ ∘ g₂ '' g ⁻¹' s
rw₃ : h '' s = h ∘ f '' f ⁻¹' s ∪ h ∘ g '' g ⁻¹' s
rw₄ : h '' s = h '' f '' f ⁻¹' s ∪ h ∘ g '' g ⁻¹' s
rw₅ : h '' s = h '' f '' f ⁻¹' s ∪ h '' g '' g ⁻¹' s
rw₆ : h '' s = h '' (s ∩ range f) ∪ h '' g '' g ⁻¹' s
⊢ h '' s = f₁ '' f₂ '' f ⁻¹' s ∪ g₁ '' g₂ '' g ⁻¹' s
have rw₇ : h '' s = h '' (s ∩ range f) ∪ h '' (s ∩ range g)
Tactic: rw [← image_comp, ← image_comp, ← hf, ← hg, image_comp, image_comp, image_preimage_eq_inter_range,
    image_preimage_eq_inter_range, ← image_union, ← inter_union_distrib_left, hfg, inter_univ]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_5
β : Type u_6
γ : Type u_7
γ' : Type u_8
δ : Type u_9
δ' : Type u_10
h : β → α
f : γ → β
f₁ : γ' → α
f₂ : γ → γ'
g : δ → β
g₁ : δ' → α
g₂ : δ → δ'
hf : h ∘ f = f₁ ∘ f₂
hg : h ∘ g = g₁ ∘ g₂
hfg : range f ∪ range g = univ
s : Set β
rw : h '' s = f₁ ∘ f₂ '' f ⁻¹' s ∪ g₁ '' g₂ '' g ⁻¹' s
rw₁ : h '' s = f₁ ∘ f₂ '' f ⁻¹' s ∪ g₁ ∘ g₂ '' g ⁻¹' s
rw₂ : h '' s = h ∘ f '' f ⁻¹' s ∪ g₁ ∘ g₂ '' g ⁻¹' s
rw₃ : h '' s = h ∘ f '' f ⁻¹' s ∪ h ∘ g '' g ⁻¹' s
rw₄ : h '' s = h '' f '' f ⁻¹' s ∪ h ∘ g '' g ⁻¹' s
rw₅ : h '' s = h '' f '' f ⁻¹' s ∪ h '' g '' g ⁻¹' s
rw₆ : h '' s = h '' (s ∩ range f) ∪ h '' g '' g ⁻¹' s
rw₇ : h '' s = h '' (s ∩ range f) ∪ h '' (s ∩ range g)
⊢ h '' s = f₁ '' f₂ '' f ⁻¹' s ∪ g₁ '' g₂ '' g ⁻¹' s
have rw₈ : h '' s = h '' (s ∩ range f ∪ s ∩ range g)
Tactic: rw [← image_comp, ← image_comp, ← hf, ← hg, image_comp, image_comp, image_preimage_eq_inter_range,
    image_preimage_eq_inter_range, ← image_union, ← inter_union_distrib_left, hfg, inter_univ]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_5
β : Type u_6
γ : Type u_7
γ' : Type u_8
δ : Type u_9
δ' : Type u_10
h : β → α
f : γ → β
f₁ : γ' → α
f₂ : γ → γ'
g : δ → β
g₁ : δ' → α
g₂ : δ → δ'
hf : h ∘ f = f₁ ∘ f₂
hg : h ∘ g = g₁ ∘ g₂
hfg : range f ∪ range g = univ
s : Set β
rw : h '' s = f₁ ∘ f₂ '' f ⁻¹' s ∪ g₁ '' g₂ '' g ⁻¹' s
rw₁ : h '' s = f₁ ∘ f₂ '' f ⁻¹' s ∪ g₁ ∘ g₂ '' g ⁻¹' s
rw₂ : h '' s = h ∘ f '' f ⁻¹' s ∪ g₁ ∘ g₂ '' g ⁻¹' s
rw₃ : h '' s = h ∘ f '' f ⁻¹' s ∪ h ∘ g '' g ⁻¹' s
rw₄ : h '' s = h '' f '' f ⁻¹' s ∪ h ∘ g '' g ⁻¹' s
rw₅ : h '' s = h '' f '' f ⁻¹' s ∪ h '' g '' g ⁻¹' s
rw₆ : h '' s = h '' (s ∩ range f) ∪ h '' g '' g ⁻¹' s
rw₇ : h '' s = h '' (s ∩ range f) ∪ h '' (s ∩ range g)
rw₈ : h '' s = h '' (s ∩ range f ∪ s ∩ range g)
⊢ h '' s = f₁ '' f₂ '' f ⁻¹' s ∪ g₁ '' g₂ '' g ⁻¹' s
have rw₉ : h '' s = h '' (s ∩ (range f ∪ range g))
Tactic: rw [← image_comp, ← image_comp, ← hf, ← hg, image_comp, image_comp, image_preimage_eq_inter_range,
    image_preimage_eq_inter_range, ← image_union, ← inter_union_distrib_left, hfg, inter_univ]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_5
β : Type u_6
γ : Type u_7
γ' : Type u_8
δ : Type u_9
δ' : Type u_10
h : β → α
f : γ → β
f₁ : γ' → α
f₂ : γ → γ'
g : δ → β
g₁ : δ' → α
g₂ : δ → δ'
hf : h ∘ f = f₁ ∘ f₂
hg : h ∘ g = g₁ ∘ g₂
hfg : range f ∪ range g = univ
s : Set β
rw : h '' s = f₁ ∘ f₂ '' f ⁻¹' s ∪ g₁ '' g₂ '' g ⁻¹' s
rw₁ : h '' s = f₁ ∘ f₂ '' f ⁻¹' s ∪ g₁ ∘ g₂ '' g ⁻¹' s
rw₂ : h '' s = h ∘ f '' f ⁻¹' s ∪ g₁ ∘ g₂ '' g ⁻¹' s
rw₃ : h '' s = h ∘ f '' f ⁻¹' s ∪ h ∘ g '' g ⁻¹' s
rw₄ : h '' s = h '' f '' f ⁻¹' s ∪ h ∘ g '' g ⁻¹' s
rw₅ : h '' s = h '' f '' f ⁻¹' s ∪ h '' g '' g ⁻¹' s
rw₆ : h '' s = h '' (s ∩ range f) ∪ h '' g '' g ⁻¹' s
rw₇ : h '' s = h '' (s ∩ range f) ∪ h '' (s ∩ range g)
rw₈ : h '' s = h '' (s ∩ range f ∪ s ∩ range g)
rw₉ : h '' s = h '' (s ∩ (range f ∪ range g))
⊢ h '' s = f₁ '' f₂ '' f ⁻¹' s ∪ g₁ '' g₂ '' g ⁻¹' s
have rw₁₀ : h '' s = h '' (s ∩ univ)
Tactic: rw [← image_comp, ← image_comp, ← hf, ← hg, image_comp, image_comp, image_preimage_eq_inter_range,
    image_preimage_eq_inter_range, ← image_union, ← inter_union_distrib_left, hfg, inter_univ]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_5
β : Type u_6
γ : Type u_7
γ' : Type u_8
δ : Type u_9
δ' : Type u_10
h : β → α
f : γ → β
f₁ : γ' → α
f₂ : γ → γ'
g : δ → β
g₁ : δ' → α
g₂ : δ → δ'
hf : h ∘ f = f₁ ∘ f₂
hg : h ∘ g = g₁ ∘ g₂
hfg : range f ∪ range g = univ
s : Set β
rw : h '' s = f₁ ∘ f₂ '' f ⁻¹' s ∪ g₁ '' g₂ '' g ⁻¹' s
rw₁ : h '' s = f₁ ∘ f₂ '' f ⁻¹' s ∪ g₁ ∘ g₂ '' g ⁻¹' s
rw₂ : h '' s = h ∘ f '' f ⁻¹' s ∪ g₁ ∘ g₂ '' g ⁻¹' s
rw₃ : h '' s = h ∘ f '' f ⁻¹' s ∪ h ∘ g '' g ⁻¹' s
rw₄ : h '' s = h '' f '' f ⁻¹' s ∪ h ∘ g '' g ⁻¹' s
rw₅ : h '' s = h '' f '' f ⁻¹' s ∪ h '' g '' g ⁻¹' s
rw₆ : h '' s = h '' (s ∩ range f) ∪ h '' g '' g ⁻¹' s
rw₇ : h '' s = h '' (s ∩ range f) ∪ h '' (s ∩ range g)
rw₈ : h '' s = h '' (s ∩ range f ∪ s ∩ range g)
rw₉ : h '' s = h '' (s ∩ (range f ∪ range g))
rw₁₀ : h '' s = h '' (s ∩ univ)
⊢ h '' s = f₁ '' f₂ '' f ⁻¹' s ∪ g₁ '' g₂ '' g ⁻¹' s
have rw₁₁ : h '' s = h '' s
Tactic: rw [← image_comp, ← image_comp, ← hf, ← hg, image_comp, image_comp, image_preimage_eq_inter_range,
    image_preimage_eq_inter_range, ← image_union, ← inter_union_distrib_left, hfg, inter_univ]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
hs : (f ⁻¹' s).Subsingleton
fx : β
hx : fx ∈ s
fy : β
hy : fy ∈ s
⊢ fx = fy
have rcases : ∀ (x : α) (hx : f x ∈ s) (y : α) (hy : f y ∈ s), f x = f y
Tactic: rcases hf fx, hf fy with ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩
Cleared hypotheses: fx, hx, fy, hy
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
hs : s.Nontrivial
hf : Surjective f
⊢ (f ⁻¹' s).Nontrivial
have rcases : ∀ (fx : β) (hx : fx ∈ s) (fy : β) (hy : fy ∈ s) (hxy : fx ≠ fy), (f ⁻¹' s).Nontrivial
Tactic: rcases hs with ⟨fx, hx, fy, hy, hxy⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
hf : Surjective f
fx : β
hx : fx ∈ s
fy : β
hy : fy ∈ s
hxy : fx ≠ fy
⊢ (f ⁻¹' s).Nontrivial
have rcases : ∀ (x : α) (hx : f x ∈ s) (y : α) (hy : f y ∈ s) (hxy : f x ≠ f y), (f ⁻¹' s).Nontrivial
Tactic: rcases hf fx, hf fy with ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩
Cleared hypotheses: fx, hx, fy, hy, hxy
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f : α → β
hs : s.Nontrivial
hf : InjOn f s
⊢ (f '' s).Nontrivial
have obtain : ∀ (x : α) (hx : x ∈ s) (y : α) (hy : y ∈ s) (hxy : x ≠ y), (f '' s).Nontrivial
Tactic: obtain ⟨x, hx, y, hy, hxy⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
⊢ ∃ (a : Set α), f '' a = s
have h : f '' f ⁻¹' s = s
Tactic: use f ⁻¹' s
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
⊢ f '' f ⁻¹' s = s
have h : s = s
Tactic: rw [hf.image_preimage]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
⊢ (f ⁻¹' s).Nonempty ↔ s.Nonempty
have rw : (f '' f ⁻¹' s).Nonempty ↔ s.Nonempty
Tactic: rw [← image_nonempty, hf.image_preimage]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
rw : (f '' f ⁻¹' s).Nonempty ↔ s.Nonempty
rw₁ : Type u_2
rw₂ : α → β
⊢ (f ⁻¹' s).Nonempty ↔ s.Nonempty
have rw₃ : s.Nonempty ↔ s.Nonempty
Tactic: rw [← image_nonempty, hf.image_preimage]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s t : Set α
h : f '' s = f '' t
⊢ s = t
have rw : f ⁻¹' f '' s = t
Tactic: rw [← preimage_image_eq s hf, ← preimage_image_eq t hf, h]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s t : Set α
h : 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, h]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
s t : Set α
h : 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, h]