awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Set.Function
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) : β) : β)
simp_rw₁ :
  Eq.{u_2 + 1} (α := β) (↑((f : (a : α) → Subtype p) ((g₂ : (a : α) → α) ((g₁ : (a : α) → α) 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 : β)

Tactic:
simp_rw [Function.comp_apply, extendDomain_apply_image, h ha]

Premises used: Equiv.Perm.extendDomain_apply_image, Function.comp_apply
-- Module: Mathlib.Data.Set.Function
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 t : Set α
h : InvOn (⇑g₁ : (a : α) → α) (⇑g₂ : (a : α) → α) s t
⊢ InvOn (α := β) (β := β) (⇑(g₁.extendDomain (p := p) f) : (a : β) → β) (⇑(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) '' t)

Tactic:
⟨h.1.extendDomain, h.2.extendDomain⟩

Premises used: Set.InvOn, Set.LeftInvOn.extendDomain, And.right, And.left, And.intro, Set.RightInvOn.extendDomain
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_7
β₁ : Type u_8
β₂ : Type u_9
s : Set α
f₁ : α → β₁
f₂ : α → β₂
h₁ : InjOn f₁ s
⊢ InjOn (β := β₁ × β₂) (fun (x : α) ↦ (f₁ x, f₂ x)) s

Tactic:
fun _ hx _ hy h => h₁ hx hy (Prod.ext_iff.1 h).1

Premises used: Prod.ext_iff, And.left, Iff.mp, Set.InjOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_7
β₁ : Type u_8
β₂ : Type u_9
s : Set α
f₁ : α → β₁
f₂ : α → β₂
h₂ : InjOn f₂ s
⊢ InjOn (β := β₁ × β₂) (fun (x : α) ↦ (f₁ x, f₂ x)) s

Tactic:
fun _ hx _ hy h => h₂ hx hy (Prod.ext_iff.1 h).2

Premises used: Prod.ext_iff, And.right, Iff.mp, Set.InjOn
-- Module: Mathlib.Data.Set.Function
Goal:
β₁ : Type u_8
β₂ : Type u_9
t₁ : Set β₁
t₂ : Set β₂
h_1 : t₂.Nonempty
x : β₁
h : x ∈ t₁
⊢ x ∈ Prod.fst '' t₁ ×ˢ t₂

Tactic:
simpa [h]
-- Module: Mathlib.Data.Set.Function
Goal:
β₁ : Type u_8
β₂ : Type u_9
t₁ : Set β₁
t₂ : Set β₂
h_1 : t₁.Nonempty
x : β₂
h : x ∈ t₂
⊢ x ∈ Prod.snd '' t₁ ×ˢ t₂

Tactic:
simpa [h]
-- Module: Mathlib.Data.Set.Function
Goal:
β₁ : Type u_8
β₂ : Type u_9
t₁ : Set β₁
t₂ : Set β₂
by_contra! : ∀ (this : SurjOn Prod.fst (t₁ ×ˢ t₂) t₁ ∧ t₁.Nonempty ∧ t₂ = ∅), False
⊢ SurjOn Prod.fst (t₁ ×ˢ t₂) t₁ → t₁ = ∅ ∨ t₂.Nonempty

Tactic:
by_contra!
-- Module: Mathlib.Data.Set.Function
Goal:
β₁ : Type u_8
β₂ : Type u_9
t₁ : Set β₁
t₂ : Set β₂
this : SurjOn Prod.fst (t₁ ×ˢ t₂) t₁ ∧ t₁.Nonempty ∧ t₂ = ∅
⊢ False

Tactic:
aesop
-- Module: Mathlib.Data.Set.Function
Goal:
β₁ : Type u_8
β₂ : Type u_9
t₁ : Set β₁
t₂ : Set β₂
⊢ t₁ = ∅ ∨ t₂.Nonempty → SurjOn Prod.fst (t₁ ×ˢ t₂) t₁

Tactic:
simp +contextual [or_imp, prod_surjOn_fst]

Premises used: or_imp, Set.prod_surjOn_fst
-- Module: Mathlib.Data.Set.Function
Goal:
β₁ : Type u_8
β₂ : Type u_9
t₁ : Set β₁
t₂ : Set β₂
by_contra! : ∀ (this : SurjOn Prod.snd (t₁ ×ˢ t₂) t₂ ∧ t₁ = ∅ ∧ t₂.Nonempty), False
⊢ SurjOn Prod.snd (t₁ ×ˢ t₂) t₂ → t₁.Nonempty ∨ t₂ = ∅

Tactic:
by_contra!
-- Module: Mathlib.Data.Set.Function
Goal:
β₁ : Type u_8
β₂ : Type u_9
t₁ : Set β₁
t₂ : Set β₂
this : SurjOn Prod.snd (t₁ ×ˢ t₂) t₂ ∧ t₁ = ∅ ∧ t₂.Nonempty
⊢ False

Tactic:
aesop
-- Module: Mathlib.Data.Set.Function
Goal:
β₁ : Type u_8
β₂ : Type u_9
t₁ : Set β₁
t₂ : Set β₂
⊢ t₁.Nonempty ∨ t₂ = ∅ → SurjOn Prod.snd (t₁ ×ˢ t₂) t₂

Tactic:
simp +contextual [or_imp, prod_surjOn_snd]

Premises used: or_imp, Set.prod_surjOn_snd
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_7
β₁ : Type u_8
β₂ : Type u_9
s : Set α
t₁ : Set β₁
t₂ : Set β₂
f₁ : α → β₁
f₂ : α → β₂
h₁ : MapsTo f₁ s t₁
h₂ : MapsTo f₂ s t₂
⊢ MapsTo (fun (x : α) ↦ (f₁ x, f₂ x)) s (t₁ ×ˢ t₂)

Tactic:
fun _ hx => ⟨h₁ hx, h₂ hx⟩

Premises used: Set.Mem, setOf, Set.prod, Set.MapsTo, And.intro
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_7
β₁ : Type u_8
β₂ : Type u_9
s : Set α
f₁ : α → β₁
f₂ : α → β₂
g₁ : β₁ → α
h₁ : LeftInvOn g₁ f₁ s
⊢ LeftInvOn (fun (x : β₁ × β₂) ↦ g₁ x.1) (fun (x : α) ↦ (f₁ x, f₂ x)) s

Tactic:
h₁

Premises used: Set.LeftInvOn
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_7
β₁ : Type u_8
β₂ : Type u_9
s : Set α
f₁ : α → β₁
f₂ : α → β₂
g₂ : β₂ → α
h₂ : LeftInvOn g₂ f₂ s
⊢ LeftInvOn (fun (x : β₁ × β₂) ↦ g₂ x.2) (fun (x : α) ↦ (f₁ x, f₂ x)) s

Tactic:
h₂

Premises used: Set.LeftInvOn
-- Module: Mathlib.Data.Set.Function
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₂
simp_rw : f₁ x.1 = f₁ y.1 ∧ f₂ x.2 = f₂ y.2 → x.1 = y.1 ∧ x.2 = y.2
⊢ Eq (α := β₁ × β₂) ((fun (x : α₁ × α₂) ↦ (f₁ x.1, f₂ x.2)) x) ((fun (x : α₁ × α₂) ↦ (f₁ x.1, f₂ x.2)) y) → x = y

Tactic:
simp_rw [Prod.ext_iff]

Premises used: Prod.ext_iff
-- Module: Mathlib.Data.Set.Function
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₂
⊢ f₁ x.1 = f₁ y.1 ∧ f₂ x.2 = f₂ y.2 → x.1 = y.1 ∧ x.2 = y.2

Tactic:
And.imp (h₁ hx.1 hy.1) (h₂ hx.2 hy.2)

Premises used: And.imp, And.right, And.left
-- Module: Mathlib.Data.Set.Function
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₂
⊢ f₁ x.1 = f₁ y.1 ∧ f₂ x.2 = f₂ y.2 → x.1 = y.1 ∧ x.2 = y.2

Tactic:
exact And.imp (h₁ hx.1 hy.1) (h₂ hx.2 hy.2)

Premises used: And.imp, And.right, And.left
-- Module: Mathlib.Data.Set.Function
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₂
obtain :
  ∀ (a₁ : α₁) (ha₁ : a₁ ∈ s₁) (hx₁ : f₁ a₁ = x.1),
    Membership.mem (γ := Set (β₁ × β₂)) ((fun (x : α₁ × α₂) ↦ (f₁ x.1, f₂ x.2)) '' s₁ ×ˢ s₂) x
⊢ Membership.mem (γ := Set (β₁ × β₂)) ((fun (x : α₁ × α₂) ↦ (f₁ x.1, f₂ x.2)) '' s₁ ×ˢ s₂) x

Tactic:
obtain ⟨a₁, ha₁, hx₁⟩ := h₁ hx.1

Premises used: And.left
-- Module: Mathlib.Data.Set.Function
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
obtain :
  ∀ (a₂ : α₂) (ha₂ : a₂ ∈ s₂) (hx₂ : f₂ a₂ = x.2),
    Membership.mem (γ := Set (β₁ × β₂)) ((fun (x : α₁ × α₂) ↦ (f₁ x.1, f₂ x.2)) '' s₁ ×ˢ s₂) x
⊢ Membership.mem (γ := Set (β₁ × β₂)) ((fun (x : α₁ × α₂) ↦ (f₁ x.1, f₂ x.2)) '' s₁ ×ˢ s₂) x

Tactic:
obtain ⟨a₂, ha₂, hx₂⟩ := h₂ hx.2

Premises used: And.right
-- Module: Mathlib.Data.Set.Function
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
a₂ : α₂
ha₂ : a₂ ∈ s₂
hx₂ : f₂ a₂ = x.2
⊢ Membership.mem (γ := Set (β₁ × β₂)) ((fun (x : α₁ × α₂) ↦ (f₁ x.1, f₂ x.2)) '' s₁ ×ˢ s₂) x

Tactic:
⟨(a₁, a₂), ⟨ha₁, ha₂⟩, Prod.ext hx₁ hx₂⟩

Premises used: Set.Mem, setOf, Prod.mk, Prod.ext, And.intro, Exists.intro, Set.image
-- Module: Mathlib.Data.Set.Function
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
a₂ : α₂
ha₂ : a₂ ∈ s₂
hx₂ : f₂ a₂ = x.2
⊢ Membership.mem (γ := Set (β₁ × β₂)) ((fun (x : α₁ × α₂) ↦ (f₁ x.1, f₂ x.2)) '' s₁ ×ˢ s₂) x

Tactic:
exact ⟨(a₁, a₂), ⟨ha₁, ha₂⟩, Prod.ext hx₁ hx₂⟩
-- Module: Mathlib.Data.Set.Function
Goal:
α₁ : Type u_7
α₂ : Type u_8
β₁ : Type u_9
β₂ : Type u_10
s₁ : Set α₁
s₂ : Set α₂
t₁ : Set β₁
t₂ : Set β₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
h₁ : MapsTo f₁ s₁ t₁
h₂ : MapsTo f₂ s₂ t₂
⊢ MapsTo (fun (x : α₁ × α₂) ↦ (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂) (t₁ ×ˢ t₂)

Tactic:
fun _x hx ↦ ⟨h₁ hx.1, h₂ hx.2⟩

Premises used: Set.Mem, setOf, Set.prod, And.right, And.left, Set.MapsTo, And.intro
-- Module: Mathlib.Data.Set.Function
Goal:
α₁ : Type u_7
α₂ : Type u_8
β₁ : Type u_9
β₂ : Type u_10
s₁ : Set α₁
s₂ : Set α₂
t₁ : Set β₁
t₂ : Set β₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
h₁ : BijOn f₁ s₁ t₁
h₂ : BijOn f₂ s₂ t₂
⊢ BijOn (fun (x : α₁ × α₂) ↦ (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂) (t₁ ×ˢ t₂)

Tactic:
⟨h₁.mapsTo.prodMap h₂.mapsTo, h₁.injOn.prodMap h₂.injOn, h₁.surjOn.prodMap h₂.surjOn⟩

Premises used: Set.BijOn.injOn, Set.BijOn.surjOn, Set.InjOn.prodMap, Set.SurjOn.prodMap, And.intro, Set.MapsTo.prodMap, Set.BijOn, Set.BijOn.mapsTo
-- Module: Mathlib.Data.Set.Function
Goal:
α₁ : Type u_7
α₂ : Type u_8
β₁ : Type u_9
β₂ : Type u_10
s₁ : Set α₁
s₂ : Set α₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
g₁ : β₁ → α₁
g₂ : β₂ → α₂
h₁ : LeftInvOn g₁ f₁ s₁
h₂ : LeftInvOn g₂ f₂ s₂
⊢ LeftInvOn (fun (x : β₁ × β₂) ↦ (g₁ x.1, g₂ x.2)) (fun (x : α₁ × α₂) ↦ (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂)

Tactic:
fun _x hx ↦ Prod.ext (h₁ hx.1) (h₂ hx.2)

Premises used: Set.LeftInvOn, And.right, And.left, Prod.ext
-- Module: Mathlib.Data.Set.Function
Goal:
α₁ : Type u_7
α₂ : Type u_8
β₁ : Type u_9
β₂ : Type u_10
t₁ : Set β₁
t₂ : Set β₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
g₁ : β₁ → α₁
g₂ : β₂ → α₂
h₁ : RightInvOn g₁ f₁ t₁
h₂ : RightInvOn g₂ f₂ t₂
⊢ RightInvOn (fun (x : β₁ × β₂) ↦ (g₁ x.1, g₂ x.2)) (fun (x : α₁ × α₂) ↦ (f₁ x.1, f₂ x.2)) (t₁ ×ˢ t₂)

Tactic:
fun _x hx ↦ Prod.ext (h₁ hx.1) (h₂ hx.2)

Premises used: Set.LeftInvOn, And.right, And.left, Prod.ext
-- Module: Mathlib.Data.Set.Function
Goal:
α₁ : Type u_7
α₂ : Type u_8
β₁ : Type u_9
β₂ : Type u_10
s₁ : Set α₁
s₂ : Set α₂
t₁ : Set β₁
t₂ : Set β₂
f₁ : α₁ → β₁
f₂ : α₂ → β₂
g₁ : β₁ → α₁
g₂ : β₂ → α₂
h₁ : InvOn g₁ f₁ s₁ t₁
h₂ : InvOn g₂ f₂ s₂ t₂
⊢ InvOn (fun (x : β₁ × β₂) ↦ (g₁ x.1, g₂ x.2)) (fun (x : α₁ × α₂) ↦ (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂) (t₁ ×ˢ t₂)

Tactic:
⟨h₁.1.prodMap h₂.1, h₁.2.prodMap h₂.2⟩

Premises used: Set.InvOn, Set.LeftInvOn.prodMap, Set.RightInvOn.prodMap, And.right, And.left, And.intro
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
t : Set β
h₁ : MapsTo (⇑e : (a : α) → β) s t
h₂ : MapsTo (⇑e.symm : (a : β) → α) t s
⊢ BijOn (⇑e : (a : α) → β) s t

Tactic:
⟨h₁, e.injective.injOn, fun b hb ↦ ⟨e.symm b, h₂ hb, apply_symm_apply _ _⟩⟩

Premises used: Equiv.apply_symm_apply, Function.Injective.injOn, And.intro, Set.BijOn, Exists.intro, Equiv.injective, Equiv.symm, DFunLike.coe
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
t : Set β
h : ∀ (a : α), Membership.mem (α := β) t ((e : (a : α) → β) a : β) ↔ a ∈ s
b : β
hb rwa rwa₁ rwa₂ rwa₃ : b ∈ t
⊢ Membership.mem (α := β) t ((e : (a : α) → β) ((e.symm : (a : β) → α) b : α) : β)

Tactic:
rwa [apply_symm_apply]

Premises used: Equiv.apply_symm_apply
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
t : Set β
⊢ InvOn (⇑e : (a : α) → β) (⇑e.symm : (a : β) → α) t s

Tactic:
⟨e.rightInverse_symm.leftInvOn _, e.leftInverse_symm.leftInvOn _⟩

Premises used: Set.InvOn, Equiv.leftInverse_symm, Function.LeftInverse.leftInvOn, And.intro, Equiv.rightInverse_symm
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
⊢ BijOn.{u_1, u_2} (β := β) (⇑e : (a : α) → β) s ((⇑e : (a : α) → β) '' s)

Tactic:
e.injective.injOn.bijOn_image

Premises used: Function.Injective.injOn, Set.InjOn.bijOn_image, Equiv.injective
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
⊢ BijOn.{u_2, u_1} (α := β) (⇑e.symm : (a : β) → α) ((⇑e : (a : α) → β) '' s) s

Tactic:
e.bijOn_image.symm e.invOn

Premises used: Equiv.invOn, Set.BijOn.symm, Equiv.bijOn_image
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
t : Set β
⊢ BijOn (⇑e.symm : (a : β) → α) t s ↔ BijOn (⇑e : (a : α) → β) s t

Tactic:
bijOn_comm e.symm.invOn

Premises used: Set.bijOn_comm, Equiv.invOn, Equiv.symm
-- Module: Mathlib.Data.Set.Function
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
inr : ∀ (hxa : x ≠ a), Membership.mem (α := α) s ((swap a b : (a : α) → α) x : α) ↔ x ∈ s
⊢ Membership.mem (α := α) s ((swap a b : (a : α) → α) x : α) ↔ x ∈ s

Tactic:
obtain rfl | hxa := eq_or_ne x a

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Data.Set.Function
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
inl₁ : ∀ (hxb : x ≠ b), Membership.mem (α := α) s ((swap x b : (a : α) → α) x : α) ↔ x ∈ s
⊢ Membership.mem (α := α) s ((swap x b : (a : α) → α) x : α) ↔ x ∈ s

Tactic:
obtain rfl | hxb := eq_or_ne x b

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Data.Set.Function
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
inr₁ : ∀ (hxb : x ≠ b), Membership.mem (α := α) s ((swap a b : (a : α) → α) x : α) ↔ x ∈ s
⊢ Membership.mem (α := α) s ((swap a b : (a : α) → α) x : α) ↔ x ∈ s

Tactic:
obtain rfl | hxb := eq_or_ne x b

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
s : Set α
inst : DecidableEq α
x : α
ha hb : x ∈ s
⊢ Membership.mem (α := α) s ((swap x x : (a : α) → α) x : α) ↔ x ∈ s

Tactic:
simp [*, swap_apply_of_ne_of_ne]

Premises used: Equiv.swap_apply_of_ne_of_ne
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
s : Set α
inst : DecidableEq α
b : α
hb : b ∈ s
x : α
ha : x ∈ s
hxb : x ≠ b
⊢ Membership.mem (α := α) s ((swap x b : (a : α) → α) x : α) ↔ x ∈ s

Tactic:
simp [*, swap_apply_of_ne_of_ne]

Premises used: Equiv.swap_apply_of_ne_of_ne
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
s : Set α
inst : DecidableEq α
a : α
ha : a ∈ s
x : α
hxa : x ≠ a
hb : x ∈ s
⊢ Membership.mem (α := α) s ((swap a x : (a : α) → α) x : α) ↔ x ∈ s

Tactic:
simp [*, swap_apply_of_ne_of_ne]

Premises used: Equiv.swap_apply_of_ne_of_ne
-- Module: Mathlib.Data.Set.Function
Goal:
α : Type u_1
s : Set α
inst : DecidableEq α
a b : α
ha : a ∈ s
hb : b ∈ s
x : α
hxa : x ≠ a
hxb : x ≠ b
⊢ Membership.mem (α := α) s ((swap a b : (a : α) → α) x : α) ↔ x ∈ s

Tactic:
simp [*, swap_apply_of_ne_of_ne]

Premises used: Equiv.swap_apply_of_ne_of_ne
-- Module: Mathlib.Data.Set.Functor
Goal:
α β : Type u
s : Set α
f : α → β
⊢ f <$> s = f '' s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Functor
Goal:
α β : Type u
s : Set (α → β)
t : Set α
⊢ s <*> t = s.seq t

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Functor
Goal:
α β : Type u
s : Set α
t : Set β
⊢ s <* t = {a : α | a ∈ s ∧ t.Nonempty}

Tactic:
rfl

Premises used: setOf, rfl
-- Module: Mathlib.Data.Set.Functor
Goal:
α β : Type u
s : Set α
t : Set β
⊢ Eq (α := Set β) (s *> t) {a : β | s.Nonempty ∧ a ∈ t}

Tactic:
rfl

Premises used: Set.Mem, setOf, rfl
-- Module: Mathlib.Data.Set.Functor
Goal:
α : Type u
a : α
⊢ Eq (α := Set α) (pure a) {a}

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Functor
Goal:
α : Type u
⊢ Eq.{u + 1} (α := Set α) failure ∅

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Functor
Goal:
α : Type u
s t : Set α
⊢ (s <|> t) = s ∪ t

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Functor
Goal:
α β γ : Type u
f : α → β → γ
s : Set α
t : Set β
h : ∀ (x : γ), x ∈ image2 f s t ↔ x ∈ f <$> s <*> t
⊢ image2 f s t = f <$> s <*> t

Tactic:
ext
-- Module: Mathlib.Data.Set.Functor
Goal:
α β γ : Type u
f : α → β → γ
s : Set α
t : Set β
x : γ
⊢ x ∈ image2 f s t ↔ x ∈ f <$> s <*> t

Tactic:
simp
-- Module: Mathlib.Data.Set.Functor
Goal:
α β : Type u
s : Set α
f : α → Set β
α_1 β_1 : Type u_1
x : Set α_1
x_1 : Set β_1
⊢ x <* x_1 = const β_1 <$> x <*> x_1

Tactic:
simp [Set.seq, Set.image2, Set.nonempty_def]

Premises used: Set.nonempty_def, Set.image2, Set.seq
-- Module: Mathlib.Data.Set.Functor
Goal:
α β : Type u
s_1 : Set α
f : α → Set β
α_1 β_1 : Type u_1
s : Set α_1
t : Set β_1
⊢ Eq (α := Set β_1) (s *> t) (const α_1 id <$> s <*> t)

Tactic:
simp [Set.seq, Set.image2, Set.nonempty_def]

Premises used: Set.nonempty_def, Set.image2, Set.seq
-- Module: Mathlib.Data.Set.Functor
Goal:
α β : Type u
s : Set α
f : α → Set β
⊢ s >>= f = ⋃ i ∈ s, f i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Set.Functor
Goal:
α β : Type u
s : Set α
f : α → Set β
α_1 β_1 γ : Type u_1
x : Set α_1
x_1 : α_1 → Set β_1
x_2 : β_1 → Set γ
⊢ x >>= x_1 >>= x_2 = x >>= fun (x : α_1) ↦ x_1 x >>= x_2

Tactic:
simp only [bind_def, biUnion_iUnion]

Premises used: Set.biUnion_iUnion, Set.bind_def
-- Module: Mathlib.Data.Set.Functor
Goal:
α : Type u
β : Set α
γ : Set (↑β : Type u)
a : α
ha : a ∈ β
ha' : Subtype.mk (p := fun (x : α) ↦ x ∈ β) a ha ∈ γ
⊢ Membership.mem (γ := Set α)
    (do
      let a ← γ
      pure (↑a : α))
    a

Tactic:
⟨_, ⟨⟨_, rfl⟩, _, ⟨ha', rfl⟩, rfl⟩⟩

Premises used: Set.Mem, iSup, setOf, And.intro, Exists.intro, Set.iUnion, rfl
-- Module: Mathlib.Data.Set.Functor
Goal:
α : Type u
β : Set α
γ : Set (↑β : Type u)
a : α
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 ∈ β
⊢ Membership.mem (γ := Set α)
      (do
        let a ← γ
        pure (↑a : α))
      a →
    a ∈ β

Tactic:
⟨_, ⟨⟨⟨_, ha⟩, rfl⟩, _, ⟨_, rfl⟩, _⟩⟩
-- Module: Mathlib.Data.Set.Functor
Goal:
α : Type u
β : Set α
γ : Set (↑β : Type u)
a val : α
ha : val ∈ β
h : Subtype.mk (p := fun (x : α) ↦ x ∈ β) val ha ∈ γ
right :
  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
⊢ val ∈ β

Tactic:
ha
-- Module: Mathlib.Data.Set.Functor
Goal:
α : Type u
β : Set α
γ : Set (↑β : Type u)
a val : α
ha : val ∈ β
h : Subtype.mk (p := fun (x : α) ↦ x ∈ β) val ha ∈ γ
right :
  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:
convert! ha
-- Module: Mathlib.Data.Set.Functor
Goal:
α : Type u
β : Set α
γ : Set (↑β : Type u)
a : α
ha :
  Membership.mem (γ := Set α)
    (do
      let a ← γ
      pure (↑a : α))
    a
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 ⋯ ∈ γ
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ β) a ⋯ ∈ γ

Tactic:
rcases ha with ⟨_, ⟨_, rfl⟩, _, ⟨ha, rfl⟩, _⟩

Premises used: rfl
-- Module: Mathlib.Data.Set.Functor
Goal:
α : Type u
β : Set α
γ : Set (↑β : Type u)
a : α
w : (↑β : Type u)
ha : w ∈ γ
right :
  Membership.mem (γ := Set α) ((fun (h : w ∈ γ) ↦ ((fun (a : (↑β : Type u)) ↦ (pure (↑a : α) : Set α)) w : Set α)) ha) a
⊢ w ∈ γ

Tactic:
ha
-- Module: Mathlib.Data.Set.Functor
Goal:
α : Type u
β : Set α
γ : Set (↑β : Type u)
a : α
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 ⋯ ∈ γ

Tactic:
convert! ha
-- Module: Mathlib.Data.Set.Functor
Goal:
α : Type u
β : Set α
γ : Set (↑β : Type u)
hγ :
  (do
      let a ← γ
      pure (↑a : α)) =
    β
⊢ γ = univ

Tactic:
eq_univ_of_forall fun ⟨_, ha⟩ => mem_of_mem_coe <| hγ.symm ▸ ha

Premises used: Membership.mem, _private.0.Set.eq_univ_of_coe_eq.match_1, Set.eq_univ_of_forall, Set.mem_of_mem_coe
-- Module: Mathlib.Data.Set.Functor
Goal:
α : Type u
β : Set α
γ : Set (↑β : Type u)
δ : Type u_1
f : α → δ
⊢ (f '' do
      let a ← γ
      pure (↑a : α)) =
    β.restrict (π := fun (a : α) ↦ δ) f '' γ

Tactic:
ext fun _ =>
    ⟨fun ⟨_, h, ha⟩ => ⟨_, mem_of_mem_coe h, ha⟩, fun ⟨_, h, ha⟩ => ⟨_, mem_coe_of_mem _ h, ha⟩⟩

Premises used: Pure.pure, Set.ext, _private.0.Set.image_coe_eq_restrict_image.match_2, Membership.mem, Subtype.mk, _private.0.Set.image_coe_eq_restrict_image.match_1, And.intro, Iff.intro, Set.mem_coe_of_mem, Set.coe_subset, Exists.intro, Set.image, Bind.bind, Set.restrict, Set.mem_of_mem_coe, Subtype.val, Subtype.property
-- Module: Mathlib.Data.Set.Functor
Goal:
α : Type u
s : Set α
t : Set (↑s : Type u)
h : ∀ (x : α), Membership.mem (γ := Set α) (⋃ x ∈ t, {(↑x : α)}) x ↔ x ∈ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t
⊢ ⋃ x ∈ t, {(↑x : α)} = Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t

Tactic:
ext
-- Module: Mathlib.Data.Set.Functor
Goal:
α : Type u
s : Set α
t : Set (↑s : Type u)
x : α
⊢ Membership.mem (γ := Set α) (⋃ x ∈ t, {(↑x : α)}) x ↔ x ∈ Subtype.val (p := fun (x : α) ↦ x ∈ s) '' t

Tactic:
simp
-- Module: Mathlib.Data.Set.Functor
Goal:
α : Type u
β : Set α
γ : Set (↑β : Type u)
a : α
ha : a ∈ β
ha' : Subtype.mk (p := fun (x : α) ↦ x ∈ β) a ha ∈ γ
⊢ a ∈ Subtype.val (p := fun (x : α) ↦ x ∈ β) '' γ

Tactic:
⟨_, ha', rfl⟩

Premises used: Set.Mem, setOf, And.intro, Exists.intro, Set.image, rfl
-- Module: Mathlib.Data.Set.Functor
Goal:
α : Type u
β : Set α
γ : Set (↑β : Type u)
⊢ Subtype.val (p := fun (x : α) ↦ x ∈ β) '' γ ⊆ β

Tactic:
Subtype.coe_image_subset _ _

Premises used: Subtype.coe_image_subset
-- Module: Mathlib.Data.Set.Functor
Goal:
α : Type u
β : Set α
γ : Set (↑β : Type u)
a : α
ha : a ∈ Subtype.val (p := fun (x : α) ↦ x ∈ β) '' γ
rcases : ∀ (w : { x : α // x ∈ β }) (ha : w ∈ γ), Subtype.mk (p := fun (x : α) ↦ x ∈ β) (↑w : α) ⋯ ∈ γ
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ β) a ⋯ ∈ γ

Tactic:
rcases ha with ⟨_, ha, rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.Set.Functor
Goal:
α : Type u
β : Set α
γ : Set (↑β : Type u)
w : { x : α // x ∈ β }
ha : w ∈ γ
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ β) (↑w : α) ⋯ ∈ γ

Tactic:
ha

Premises used: Set.Mem
-- Module: Mathlib.Data.Set.Functor
Goal:
α : Type u
β : Set α
γ : Set (↑β : Type u)
w : { x : α // x ∈ β }
ha : w ∈ γ
⊢ Subtype.mk (p := fun (x : α) ↦ x ∈ β) (↑w : α) ⋯ ∈ γ

Tactic:
exact ha
-- Module: Mathlib.Data.Set.Functor
Goal:
α : Type u
β : Set α
γ : Set (↑β : Type u)
hγ : Subtype.val (p := fun (x : α) ↦ x ∈ β) '' γ = β
⊢ γ = univ

Tactic:
eq_univ_of_forall fun ⟨_, ha⟩ => mem_of_mem_image_val <| hγ.symm ▸ ha

Premises used: Membership.mem, _private.0.Set.eq_univ_of_coe_eq.match_1, Set.mem_of_mem_image_val, Set.eq_univ_of_forall
-- Module: Mathlib.Data.Set.Functor
Goal:
α : Type u
β : Set α
γ : Set (↑β : Type u)
δ : Type u_1
f : α → δ
h : ∀ (x : δ), x ∈ f '' Subtype.val (p := fun (x : α) ↦ x ∈ β) '' γ ↔ x ∈ β.restrict (π := fun (a : α) ↦ δ) f '' γ
⊢ f '' Subtype.val (p := fun (x : α) ↦ x ∈ β) '' γ = β.restrict (π := fun (a : α) ↦ δ) f '' γ

Tactic:
ext
-- Module: Mathlib.Data.Set.Functor
Goal:
α : Type u
β : Set α
γ : Set (↑β : Type u)
δ : Type u_1
f : α → δ
x : δ
⊢ x ∈ f '' Subtype.val (p := fun (x : α) ↦ x ∈ β) '' γ ↔ x ∈ β.restrict (π := fun (a : α) ↦ δ) f '' γ

Tactic:
simp
-- Module: Mathlib.Data.Set.Functor
Goal:
⊢ LawfulMonad SetM

Tactic:
Set.instLawfulMonad

Premises used: Set.instLawfulMonad, SetM
-- Module: Mathlib.Data.Set.Functor
Goal:
⊢ LawfulAlternative SetM

Tactic:
Set.instLawfulAlternative

Premises used: Set.instLawfulAlternative, SetM