awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.Function (hypothesis)
Goal:
α : Type u_1
β : Type u_2
n : Nonempty α
f : α → β
hf : Injective f
s : Set α
h : ¬Classical.choice n ∈ s
x : β
hx : ¬x ∈ range f
⊢ x ∈ invFun f ⁻¹' s ↔ x ∈ f '' s
have this : ¬x ∈ f '' s
Tactic: have : x ∉ f '' s := fun h' => hx (image_subset_range _ _ h')
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
hfs : SurjOn f s t
⊢ ∃ (u : Set α), u ⊆ s ∧ InjOn f u ∧ f '' u = t
have choose : ∀ (x : ⦃a : β⦄ → a ∈ t → α) (hmem : ∀ ⦃a : β⦄ (a_1 : a ∈ t), x a_1 ∈ s) (heq : ∀ ⦃a : β⦄ (a_1 : a ∈ t), f (x a_1) = a),
  ∃ (u : Set α), u ⊆ s ∧ InjOn f u ∧ f '' u = t
Tactic: choose x hmem heq using hfs
Cleared hypotheses: hfs
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
s t : Set α
h : Semiconj f fa fb
ha : SurjOn fa s t
x : α
hxt : x ∈ t
⊢ f x ∈ fb '' f '' s
have rcases : ∀ (x : α) (hxs : x ∈ s) (hxt : fa x ∈ t), f (fa x) ∈ fb '' f '' s
Tactic: rcases ha hxt with ⟨x, hxs, rfl⟩
Cleared hypotheses: x, hxt
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
s t : Set α
h : Semiconj f fa fb
ha : SurjOn fa s t
x : α
hxs : x ∈ s
hxt : fa x ∈ t
⊢ f (fa x) ∈ fb '' f '' s
have rw : fb (f x) ∈ fb '' f '' s
Tactic: rw [h x]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Surjective fa
⊢ SurjOn fb (range f) (range f)
have rw : SurjOn fb (f '' univ) (f '' univ)
Tactic: rw [← image_univ]
-- Lean 4 proof step from Mathlib.Data.Set.Function (hypothesis)
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
s : Set α
h : Semiconj f fa fb
ha : InjOn fa s
hf : InjOn f (fa '' s)
x : α
hx : x ∈ s
y : α
hy : y ∈ s
H : fb (f x) = fb (f y)
⊢ f x = f y
have H₁ : f (fa x) = f (fa y)
Tactic: simp only [← h.eq] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Injective fa
hf : InjOn f (range fa)
⊢ InjOn fb (range f)
have rw : ∀ (hf : InjOn f (fa '' univ)), InjOn fb (f '' univ)
Tactic: rw [← image_univ] at *
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
ha : Bijective fa
hf : Injective f
⊢ BijOn fb (range f) (range f)
have rw : BijOn fb (f '' univ) (f '' univ)
Tactic: rw [← image_univ]
-- Lean 4 proof step from Mathlib.Data.Set.Function (hypothesis)
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
s : Set β
hb : InjOn fb s
hf : InjOn f (f ⁻¹' s)
x : α
hx : x ∈ f ⁻¹' s
y : α
hy : y ∈ f ⁻¹' s
H : fa x = fa y
⊢ x = y
have this : f (fa x) = f (fa y)
Tactic: have := congr_arg f H
-- Lean 4 proof step from Mathlib.Data.Set.Function (hypothesis)
Goal:
α : Type u_1
β : Type u_2
fa : α → α
fb : β → β
f : α → β
h : Semiconj f fa fb
s : Set β
hb : InjOn fb s
hf : InjOn f (f ⁻¹' s)
x : α
hx : x ∈ f ⁻¹' s
y : α
hy : y ∈ f ⁻¹' s
H : fa x = fa y
this : f (fa x) = f (fa y)
⊢ x = y
have this₁ : fb (f x) = fb (f y)
Tactic: rw [h.eq, h.eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α (Subtype p)
g : Perm α
s t : Set α
h : MapsTo (⇑g : (a : α) → α) s t
a : α
ha : a ∈ s
⊢ Eq (α := β)
    (Function.comp (α := α) (β := Subtype p) (Subtype.val (p := p)) ((⇑f : (a : α) → Subtype p) : (a : α) → Subtype p)
        ((g : (a : α) → α) a : α) :
      β)
    ((g.extendDomain (p := p) f : (a : β) → β)
        (Function.comp (β := Subtype p) (Subtype.val (p := p)) (⇑f : (a : α) → Subtype p) a) :
      β)
have simp_rw : Eq (α := β) ((↑((f : (a : α) → Subtype p) ((g : (a : α) → α) a)) : β) : β)
  ((g.extendDomain (p := p) f : (a : β) → β) (↑((f : (a : α) → Subtype p) a) : β) : β)
Tactic: simp_rw [Function.comp_apply, extendDomain_apply_image]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α (Subtype p)
g : Perm α
s t : Set α
h : SurjOn (⇑g : (a : α) → α) s t
a : α
ha : a ∈ t
⊢ Membership.mem (γ := Set β)
    (image (α := β) (⇑(g.extendDomain (p := p) f) : (a : β) → β)
      (Function.comp (β := Subtype p) (Subtype.val (p := p)) (⇑f : (a : α) → Subtype p) '' s))
    (Function.comp (β := Subtype p) (Subtype.val (p := p)) (⇑f : (a : α) → Subtype p) a)
have obtain : ∀ (b : α) (hb : b ∈ s) (ha : Membership.mem (α := α) t ((g : (a : α) → α) b : α)),
  Membership.mem (γ := Set β)
    (image (α := β) (⇑(g.extendDomain (p := p) f) : (a : β) → β)
      (Function.comp (β := Subtype p) (Subtype.val (p := p)) (⇑f : (a : α) → Subtype p) '' s))
    (Function.comp (α := α) (β := Subtype p) (Subtype.val (p := p)) ((⇑f : (a : α) → Subtype p) : (a : α) → Subtype p)
      ((g : (a : α) → α) b : α))
Tactic: obtain ⟨b, hb, rfl⟩ := h ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α (Subtype p)
g : Perm α
s t : Set α
h : SurjOn (⇑g : (a : α) → α) s t
b : α
hb : b ∈ s
ha : Membership.mem (α := α) t ((g : (a : α) → α) b : α)
⊢ Eq (α := β)
    ((g.extendDomain (p := p) f : (a : β) → β)
        (Function.comp (β := Subtype p) (Subtype.val (p := p)) (⇑f : (a : α) → Subtype p) b) :
      β)
    (Function.comp (α := α) (β := Subtype p) (Subtype.val (p := p)) ((⇑f : (a : α) → Subtype p) : (a : α) → Subtype p)
        ((g : (a : α) → α) b : α) :
      β)
have simp_rw : Eq (α := β) ((g.extendDomain (p := p) f : (a : β) → β) (↑((f : (a : α) → Subtype p) b) : β) : β)
  ((↑((f : (a : α) → Subtype p) ((g : (a : α) → α) b)) : β) : β)
Tactic: simp_rw [Function.comp_apply, extendDomain_apply_image]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α (Subtype p)
g₁ g₂ : Perm α
s : Set α
h : LeftInvOn (β := α) (⇑g₁ : (a : α) → α) (⇑g₂ : (a : α) → α) s
a : α
ha : a ∈ s
⊢ Eq (α := β)
    ((g₁.extendDomain (p := p) f : (a : β) → β)
        ((g₂.extendDomain (p := p) f : (a : β) → β)
            (Function.comp (β := Subtype p) (Subtype.val (p := p)) (⇑f : (a : α) → Subtype p) a) :
          β) :
      β)
    (Function.comp (β := Subtype p) (Subtype.val (p := p)) (⇑f : (a : α) → Subtype p) a : β)
have simp_rw : Eq (α := β)
  ((g₁.extendDomain (p := p) f : (a : β) → β)
      ((g₂.extendDomain (p := p) f : (a : β) → β) (↑((f : (a : α) → Subtype p) a) : β) : β) :
    β)
  ((↑((f : (a : α) → Subtype p) a) : β) : β)
Tactic: simp_rw [Function.comp_apply, extendDomain_apply_image, h ha]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α (Subtype p)
g₁ g₂ : Perm α
s : Set α
h : LeftInvOn (β := α) (⇑g₁ : (a : α) → α) (⇑g₂ : (a : α) → α) s
a : α
ha : a ∈ s
simp_rw :
  Eq (α := β)
    ((g₁.extendDomain (p := p) f : (a : β) → β)
        ((g₂.extendDomain (p := p) f : (a : β) → β) (↑((f : (a : α) → Subtype p) a) : β) : β) :
      β)
    ((↑((f : (a : α) → Subtype p) a) : β) : β)
⊢ Eq (α := β)
    ((g₁.extendDomain (p := p) f : (a : β) → β)
        ((g₂.extendDomain (p := p) f : (a : β) → β)
            (Function.comp (β := Subtype p) (Subtype.val (p := p)) (⇑f : (a : α) → Subtype p) a) :
          β) :
      β)
    (Function.comp (β := Subtype p) (Subtype.val (p := p)) (⇑f : (a : α) → Subtype p) a : β)
have simp_rw₁ : Eq.{u_2 + 1} (α := β) (↑((f : (a : α) → Subtype p) ((g₁ : (a : α) → α) ((g₂ : (a : α) → α) a : α))) : β)
  (↑((f : (a : α) → Subtype p) a) : β)
Tactic: simp_rw [Function.comp_apply, extendDomain_apply_image, h ha]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α (Subtype p)
g₁ g₂ : Perm α
t : Set α
h : RightInvOn (α := α) (⇑g₁ : (a : α) → α) (⇑g₂ : (a : α) → α) t
a : α
ha : a ∈ t
⊢ Eq (α := β)
    ((g₂.extendDomain (p := p) f : (a : β) → β)
        ((g₁.extendDomain (p := p) f : (a : β) → β)
            (Function.comp (β := Subtype p) (Subtype.val (p := p)) (⇑f : (a : α) → Subtype p) a) :
          β) :
      β)
    (Function.comp (β := Subtype p) (Subtype.val (p := p)) (⇑f : (a : α) → Subtype p) a : β)
have simp_rw : Eq (α := β)
  ((g₂.extendDomain (p := p) f : (a : β) → β)
      ((g₁.extendDomain (p := p) f : (a : β) → β) (↑((f : (a : α) → Subtype p) a) : β) : β) :
    β)
  ((↑((f : (a : α) → Subtype p) a) : β) : β)
Tactic: simp_rw [Function.comp_apply, extendDomain_apply_image, h ha]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
β : Type u_2
p : β → Prop
inst : DecidablePred p
f : Equiv.{u_1 + 1, max 1 (u_2 + 1)} α (Subtype p)
g₁ g₂ : Perm α
t : Set α
h : RightInvOn (α := α) (⇑g₁ : (a : α) → α) (⇑g₂ : (a : α) → α) t
a : α
ha : a ∈ t
simp_rw :
  Eq (α := β)
    ((g₂.extendDomain (p := p) f : (a : β) → β)
        ((g₁.extendDomain (p := p) f : (a : β) → β) (↑((f : (a : α) → Subtype p) a) : β) : β) :
      β)
    ((↑((f : (a : α) → Subtype p) a) : β) : β)
⊢ Eq (α := β)
    ((g₂.extendDomain (p := p) f : (a : β) → β)
        ((g₁.extendDomain (p := p) f : (a : β) → β)
            (Function.comp (β := Subtype p) (Subtype.val (p := p)) (⇑f : (a : α) → Subtype p) a) :
          β) :
      β)
    (Function.comp (β := Subtype p) (Subtype.val (p := p)) (⇑f : (a : α) → Subtype p) a : β)
have simp_rw₁ : Eq.{u_2 + 1} (α := β) (↑((f : (a : α) → Subtype p) ((g₂ : (a : α) → α) ((g₁ : (a : α) → α) a : α))) : β)
  (↑((f : (a : α) → Subtype p) a) : β)
Tactic: simp_rw [Function.comp_apply, extendDomain_apply_image, h ha]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
β₁ : Type u_8
β₂ : Type u_9
t₁ : Set β₁
t₂ : Set β₂
⊢ SurjOn Prod.fst (t₁ ×ˢ t₂) t₁ → t₁ = ∅ ∨ t₂.Nonempty
have by_contra! : ∀ (this : SurjOn Prod.fst (t₁ ×ˢ t₂) t₁ ∧ t₁.Nonempty ∧ t₂ = ∅), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
β₁ : Type u_8
β₂ : Type u_9
t₁ : Set β₁
t₂ : Set β₂
⊢ SurjOn Prod.snd (t₁ ×ˢ t₂) t₂ → t₁.Nonempty ∨ t₂ = ∅
have by_contra! : ∀ (this : SurjOn Prod.snd (t₁ ×ˢ t₂) t₂ ∧ t₁ = ∅ ∧ t₂.Nonempty), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α₁ : Type u_7
α₂ : Type u_8
β₁ : Type u_9
β₂ : Type u_10
s₁ : Set α₁
s₂ : Set α₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
h₁ : InjOn f₁ s₁
h₂ : InjOn f₂ s₂
x : α₁ × α₂
hx : x ∈ s₁ ×ˢ s₂
y : α₁ × α₂
hy : y ∈ s₁ ×ˢ s₂
⊢ Eq (α := β₁ × β₂) ((fun (x : α₁ × α₂) ↦ (f₁ x.1, f₂ x.2)) x) ((fun (x : α₁ × α₂) ↦ (f₁ x.1, f₂ x.2)) y) → x = y
have simp_rw : f₁ x.1 = f₁ y.1 ∧ f₂ x.2 = f₂ y.2 → x.1 = y.1 ∧ x.2 = y.2
Tactic: simp_rw [Prod.ext_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α₁ : Type u_7
α₂ : Type u_8
β₁ : Type u_9
β₂ : Type u_10
s₁ : Set α₁
s₂ : Set α₂
t₁ : Set β₁
t₂ : Set β₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
h₁ : SurjOn f₁ s₁ t₁
h₂ : SurjOn f₂ s₂ t₂
x : β₁ × β₂
hx : x ∈ t₁ ×ˢ t₂
⊢ Membership.mem (γ := Set (β₁ × β₂)) ((fun (x : α₁ × α₂) ↦ (f₁ x.1, f₂ x.2)) '' s₁ ×ˢ s₂) x
have obtain : ∀ (a₁ : α₁) (ha₁ : a₁ ∈ s₁) (hx₁ : f₁ a₁ = x.1),
  Membership.mem (γ := Set (β₁ × β₂)) ((fun (x : α₁ × α₂) ↦ (f₁ x.1, f₂ x.2)) '' s₁ ×ˢ s₂) x
Tactic: obtain ⟨a₁, ha₁, hx₁⟩ := h₁ hx.1
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α₁ : Type u_7
α₂ : Type u_8
β₁ : Type u_9
β₂ : Type u_10
s₁ : Set α₁
s₂ : Set α₂
t₁ : Set β₁
t₂ : Set β₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
h₁ : SurjOn f₁ s₁ t₁
h₂ : SurjOn f₂ s₂ t₂
x : β₁ × β₂
hx : x ∈ t₁ ×ˢ t₂
a₁ : α₁
ha₁ : a₁ ∈ s₁
hx₁ : f₁ a₁ = x.1
⊢ Membership.mem (γ := Set (β₁ × β₂)) ((fun (x : α₁ × α₂) ↦ (f₁ x.1, f₂ x.2)) '' s₁ ×ˢ s₂) x
have obtain : ∀ (a₂ : α₂) (ha₂ : a₂ ∈ s₂) (hx₂ : f₂ a₂ = x.2),
  Membership.mem (γ := Set (β₁ × β₂)) ((fun (x : α₁ × α₂) ↦ (f₁ x.1, f₂ x.2)) '' s₁ ×ˢ s₂) x
Tactic: obtain ⟨a₂, ha₂, hx₂⟩ := h₂ hx.2
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
s : Set α
inst : DecidableEq α
a b : α
ha : a ∈ s
hb : b ∈ s
x : α
⊢ Membership.mem (α := α) s ((swap a b : (a : α) → α) x : α) ↔ x ∈ s
have inl : ∀ (ha : x ∈ s), Membership.mem (α := α) s ((swap x b : (a : α) → α) x : α) ↔ x ∈ s
Tactic: obtain rfl | hxa := eq_or_ne x a
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
s : Set α
inst : DecidableEq α
a b : α
ha : a ∈ s
hb : b ∈ s
x : α
inl : ∀ (ha : x ∈ s), Membership.mem (α := α) s ((swap x b : (a : α) → α) x : α) ↔ x ∈ s
⊢ Membership.mem (α := α) s ((swap a b : (a : α) → α) x : α) ↔ x ∈ s
have inr : ∀ (hxa : x ≠ a), Membership.mem (α := α) s ((swap a b : (a : α) → α) x : α) ↔ x ∈ s
Tactic: obtain rfl | hxa := eq_or_ne x a
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
s : Set α
inst : DecidableEq α
b : α
hb : b ∈ s
x : α
ha : x ∈ s
⊢ Membership.mem (α := α) s ((swap x b : (a : α) → α) x : α) ↔ x ∈ s
have inl : ∀ (hb : x ∈ s), Membership.mem (α := α) s ((swap x x : (a : α) → α) x : α) ↔ x ∈ s
Tactic: obtain rfl | hxb := eq_or_ne x b
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
s : Set α
inst : DecidableEq α
b : α
hb : b ∈ s
x : α
ha : x ∈ s
inl : ∀ (hb : x ∈ s), Membership.mem (α := α) s ((swap x x : (a : α) → α) x : α) ↔ x ∈ s
⊢ Membership.mem (α := α) s ((swap x b : (a : α) → α) x : α) ↔ x ∈ s
have inl₁ : ∀ (hxb : x ≠ b), Membership.mem (α := α) s ((swap x b : (a : α) → α) x : α) ↔ x ∈ s
Tactic: obtain rfl | hxb := eq_or_ne x b
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
s : Set α
inst : DecidableEq α
a b : α
ha : a ∈ s
hb : b ∈ s
x : α
hxa : x ≠ a
⊢ Membership.mem (α := α) s ((swap a b : (a : α) → α) x : α) ↔ x ∈ s
have inr : ∀ (hb : x ∈ s), Membership.mem (α := α) s ((swap a x : (a : α) → α) x : α) ↔ x ∈ s
Tactic: obtain rfl | hxb := eq_or_ne x b
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Data.Set.Function (goal)
Goal:
α : Type u_1
s : Set α
inst : DecidableEq α
a b : α
ha : a ∈ s
hb : b ∈ s
x : α
hxa : x ≠ a
inr : ∀ (hb : x ∈ s), Membership.mem (α := α) s ((swap a x : (a : α) → α) x : α) ↔ x ∈ s
⊢ Membership.mem (α := α) s ((swap a b : (a : α) → α) x : α) ↔ x ∈ s
have inr₁ : ∀ (hxb : x ≠ b), Membership.mem (α := α) s ((swap a b : (a : α) → α) x : α) ↔ x ∈ s
Tactic: obtain rfl | hxb := eq_or_ne x b
-- Lean 4 proof step from Mathlib.Data.Set.Functor (goal)
Goal:
α β γ : Type u
f : α → β → γ
s : Set α
t : Set β
⊢ image2 f s t = f <$> s <*> t
have h : ∀ (x : γ), x ∈ image2 f s t ↔ x ∈ f <$> s <*> t
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Functor (goal)
Goal:
α : Type u
β : Set α
γ : Set (↑β : Type u)
a : α
⊢ Membership.mem (γ := Set α)
      (do
        let a ← γ
        pure (↑a : α))
      a →
    a ∈ β
have this : ∀ (val : α) (ha : val ∈ β) (h : Subtype.mk (p := fun (x : α) ↦ x ∈ β) val ha ∈ γ),
  Membership.mem (γ := Set α)
      ((fun (h : Subtype.mk (p := fun (x : α) ↦ x ∈ β) val ha ∈ γ) ↦
          ((fun (a : (↑β : Type u)) ↦ (pure (↑a : α) : Set α)) (Subtype.mk (p := fun (x : α) ↦ x ∈ β) val ha) : Set α))
        h)
      a →
    a ∈ β
Tactic: ⟨_, ⟨⟨⟨_, ha⟩, rfl⟩, _, ⟨_, rfl⟩, _⟩⟩
-- Lean 4 proof step from Mathlib.Data.Set.Functor (goal)
Goal:
α : Type u
β : Set α
γ : Set (↑β : Type u)
a : α
ha :
  Membership.mem (γ := Set α)
    (do
      let a ← γ
      pure (↑a : α))
    a
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ β) a ⋯ ∈ γ
have rcases : ∀ (w : (↑β : Type u)) (ha : w ∈ γ)
  (right :
    Membership.mem (γ := Set α) ((fun (h : w ∈ γ) ↦ ((fun (a : (↑β : Type u)) ↦ (pure (↑a : α) : Set α)) w : Set α)) ha)
      a),
  Subtype.mk (p := fun (x : α) ↦ x ∈ β) a sorry ∈ γ
Tactic: rcases ha with ⟨_, ⟨_, rfl⟩, _, ⟨ha, rfl⟩, _⟩
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Data.Set.Functor (goal)
Goal:
α : Type u
s : Set α
t : Set (↑s : Type u)
⊢ ⋃ x ∈ t, {(↑x : α)} = Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t
have h : ∀ (x : α), Membership.mem (γ := Set α) (⋃ x ∈ t, {(↑x : α)}) x ↔ x ∈ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Functor (goal)
Goal:
α : Type u
β : Set α
γ : Set (↑β : Type u)
a : α
ha : a ∈ Subtype.val (p := fun (x : α) ↦ x ∈ β) '' γ
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ β) a ⋯ ∈ γ
have rcases : ∀ (w : { x : α // x ∈ β }) (ha : w ∈ γ), Subtype.mk (p := fun (x : α) ↦ x ∈ β) (↑w : α) sorry ∈ γ
Tactic: rcases ha with ⟨_, ha, rfl⟩
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Data.Set.Functor (goal)
Goal:
α : Type u
β : Set α
γ : Set (↑β : Type u)
δ : Type u_1
f : α → δ
⊢ f '' Subtype.val (p := fun (x : α) ↦ x ∈ β) '' γ = β.restrict (π := fun (a : α) ↦ δ) f '' γ
have h : ∀ (x : δ), x ∈ f '' Subtype.val (p := fun (x : α) ↦ x ∈ β) '' γ ↔ x ∈ β.restrict (π := fun (a : α) ↦ δ) f '' γ
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
f : α → β
hf : ∀ (b : β), f ⁻¹' {b} = ∅ ∨ f ⁻¹' {b} = univ
⊢ ∃ (b : β), f = const α b
have inl : ∀ (b : β) (hb : f ⁻¹' {b} = univ), ∃ (b : β), f = const α b
Tactic: rcases em (∃ b, f ⁻¹' {b} = univ) with ⟨b, hb⟩ | hf'
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
f : α → β
hf : ∀ (b : β), f ⁻¹' {b} = ∅ ∨ f ⁻¹' {b} = univ
inl : ∀ (b : β) (hb : f ⁻¹' {b} = univ), ∃ (b : β), f = const α b
⊢ ∃ (b : β), f = const α b
have inr : ∀ (hf' : ¬∃ (b : β), f ⁻¹' {b} = univ), ∃ (b : β), f = const α b
Tactic: rcases em (∃ b, f ⁻¹' {b} = univ) with ⟨b, hb⟩ | hf'
-- Lean 4 proof step from Mathlib.Data.Set.Image (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Nonempty β
f : α → β
hf : ∀ (b : β), f ⁻¹' {b} = ∅ ∨ f ⁻¹' {b} = univ
hf' : ¬∃ (b : β), f ⁻¹' {b} = univ
⊢ ∃ (b : β), f = const α b
have this : ∀ (x : α) (b : β), f x ≠ b
Tactic: have : ∀ x b, f x ≠ b := fun x b ↦
      eq_empty_iff_forall_notMem.1 ((hf b).resolve_right fun h ↦ hf' ⟨b, h⟩) x
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
f : α → α
n : ℕ
ih : preimage f^[n] = (preimage f)^[n]
⊢ preimage f^[n + 1] = (preimage f)^[n + 1]
have succ : preimage (f^[n] ∘ f) = (preimage f)^[n + 1]
Tactic: rw [iterate_succ, iterate_succ', preimage_comp_eq, ih]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
f : α → α
n : ℕ
ih : preimage f^[n] = (preimage f)^[n]
succ : preimage (f^[n] ∘ f) = (preimage f)^[n + 1]
⊢ preimage f^[n + 1] = (preimage f)^[n + 1]
have succ₁ : preimage (f^[n] ∘ f) = preimage f ∘ (preimage f)^[n]
Tactic: rw [iterate_succ, iterate_succ', preimage_comp_eq, ih]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
f : α → α
n : ℕ
ih : preimage f^[n] = (preimage f)^[n]
succ : preimage (f^[n] ∘ f) = (preimage f)^[n + 1]
succ₁ : preimage (f^[n] ∘ f) = preimage f ∘ (preimage f)^[n]
⊢ preimage f^[n + 1] = (preimage f)^[n + 1]
have succ₂ : preimage f ∘ preimage f^[n] = preimage f ∘ (preimage f)^[n]
Tactic: rw [iterate_succ, iterate_succ', preimage_comp_eq, ih]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
f : α → α
n : ℕ
ih : preimage f^[n] = (preimage f)^[n]
succ : preimage (f^[n] ∘ f) = (preimage f)^[n + 1]
succ₁ : preimage (f^[n] ∘ f) = preimage f ∘ (preimage f)^[n]
succ₂ : preimage f ∘ preimage f^[n] = preimage f ∘ (preimage f)^[n]
⊢ preimage f^[n + 1] = (preimage f)^[n + 1]
have succ₃ : preimage f ∘ (preimage f)^[n] = preimage f ∘ (preimage f)^[n]
Tactic: rw [iterate_succ, iterate_succ', preimage_comp_eq, ih]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
f : α → α
n : ℕ
⊢ preimage f^[n] = (preimage f)^[n]
have zero : preimage f^[0] = (preimage f)^[0]
Tactic: induction n with
  | zero => simp
  | succ n ih => rw [iterate_succ, iterate_succ', preimage_comp_eq, ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
f : α → α
n : ℕ
zero : preimage f^[0] = (preimage f)^[0]
⊢ preimage f^[n] = (preimage f)^[n]
have succ : ∀ (n : ℕ) (ih : preimage f^[n] = (preimage f)^[n]), preimage f^[n + 1] = (preimage f)^[n + 1]
Tactic: induction n with
  | zero => simp
  | succ n ih => rw [iterate_succ, iterate_succ', preimage_comp_eq, ih]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
p : α → Prop
⊢ p ⁻¹' {True} = {a : α | p a}
have h : ∀ (x : α), x ∈ p ⁻¹' {True} ↔ Membership.mem (γ := Set α) {a : α | p a} x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
p : α → Prop
⊢ p ⁻¹' {False} = {a : α | ¬p a}
have h : ∀ (x : α), x ∈ p ⁻¹' {False} ↔ Membership.mem (γ := Set α) {a : α | ¬p a} x
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
⊢ Eq (α := Set { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)
    (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' v)ᶜ
have h : ∀ (x : α) (x_in_s : x ∈ s),
  Membership.mem (γ := Set { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x x_in_s) ↔
    Membership.mem (γ := Set { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' v)ᶜ
      (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x x_in_s)
Tactic: ext ⟨x, x_in_s⟩
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
⊢ Membership.mem (γ := Set { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x x_in_s) ↔
    Membership.mem (γ := Set { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' v)ᶜ
      (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x x_in_s)
have h : Membership.mem (γ := Set { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)
    (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x x_in_s) →
  Membership.mem (γ := Set { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' v)ᶜ
    (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x x_in_s)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
s u v : Set α
hsuv : s ⊆ u ∪ v
H : s ∩ (u ∩ v) = ∅
x : α
x_in_s : x ∈ s
h :
  Membership.mem (γ := Set { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x x_in_s) →
    Membership.mem (γ := Set { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' v)ᶜ
      (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x x_in_s)
⊢ Membership.mem (γ := Set { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x x_in_s) ↔
    Membership.mem (γ := Set { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' v)ᶜ
      (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x x_in_s)
have h₁ : Membership.mem (γ := Set { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' v)ᶜ
    (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x x_in_s) →
  Membership.mem (γ := Set { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s) ⁻¹' u)
    (Subtype.mk (p := fun (x : α) ↦ x ∈ s) x x_in_s)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
t : Set α
hs : s ⊆ f '' t
hf : InjOn f (f ⁻¹' s)
a : α
ha : a ∈ f ⁻¹' s
⊢ a ∈ t
have obtain : ∀ (b : α) (hb : b ∈ t) (hba : f b = f a), a ∈ t
Tactic: obtain ⟨b, hb, hba⟩ := hs ha
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
t : Set α
hs : s ⊆ f '' t
hf : InjOn f (f ⁻¹' s)
a : α
ha : a ∈ f ⁻¹' s
b : α
hb : b ∈ t
hba : f b = f a
⊢ a ∈ t
have rwa : b ∈ f ⁻¹' s
Tactic: rwa [hf ha _ hba.symm]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_5
β : Type u_6
f : α → β
s : Set α
⊢ f '' s = ∅ ↔ s = ∅
have simp : (∀ (x : β), ¬x ∈ f '' s) ↔ ∀ (x : α), ¬x ∈ s
Tactic: simp only [eq_empty_iff_forall_notMem]
-- Lean 4 proof step from Mathlib.Data.Set.Image (goal)
Goal:
α : Type u_5
β : Type u_6
f : α → β
s : Set α
⊢ ∅ = f '' s ↔ s = ∅
have rw : f '' s = ∅ ↔ s = ∅
Tactic: rw [eq_comm, image_eq_empty]