awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β : Type u_2
α : Type u
s t : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
⊢ ∀ (x : α), x ∈ t \ s → (fun (x : α) ↦ ¬x ∈ s) x

Tactic:
exacts [fun x hx => hx.2, fun x hx => not_not_intro hx.1]

Premises used: not_not_intro
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β : Type u_2
α : Type u
s t : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
rw : t \ s ∪ s ∩ t = t
⊢ (↑s : Type u) ⊕ (↑(t \ s ∪ s ∩ t) : Type u) ≃ (↑s : Type u) ⊕ (↑t : Type u)

Tactic:
rw [(_ : t \ s ∪ s ∩ t = t)]
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β : Type u_2
α : Type u
s t : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
rw : s ∩ t ∪ t \ s = t
rw₁ : t ∩ s ∪ t \ s = t
rw₂ rw₃ : t = t
⊢ t \ s ∪ s ∩ t = t

Tactic:
rw [union_comm, inter_comm, inter_union_diff]

Premises used: Set.union_comm, Set.inter_comm, Set.inter_union_diff
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β : Type u_2
α : Type u
s t : Set α
inst : DecidablePred fun (x : α) ↦ x ∈ s
rw : (↑s : Type u) ⊕ (↑t : Type u) ≃ (↑s : Type u) ⊕ (↑t : Type u)
rw₁ : t \ s ∪ s ∩ t = t
rw₂ : (↑s : Type u) ⊕ (↑t : Type u) ≃ (↑s : Type u) ⊕ (↑t : Type u)
rw₃ rw₄ : t \ s ∪ s ∩ t = t
⊢ (↑s : Type u) ⊕ (↑(t \ s ∪ s ∩ t) : Type u) ≃ (↑s : Type u) ⊕ (↑t : Type u)

Tactic:
{ rw [(_ : t \ s ∪ s ∩ t = t)]
        rw [union_comm, inter_comm, inter_union_diff] }

Premises used: Set.union_comm, Set.inter_comm, Set.inter_union_diff
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β_2 : Type u_2
α : Type u
β : Type v
s : Set α
t : Set β
inst : DecidablePred fun (x : α) ↦ x ∈ s
inst_1 : DecidablePred fun (x : β) ↦ x ∈ t
e₀ : Equiv.{u + 1, v + 1} (↑s : Type u) (↑t : Type v)
e₁ : Equiv.{u + 1, v + 1} (↑sᶜ : Type u) (↑tᶜ : Type v)
x : (↑s : Type u)
⊢ Eq.{v + 1} (α := β)
    ((Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
            (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv) (Set.sumCompl s).symm (e₀.sumCongr e₁))
            (Set.sumCompl t) :
          (a : α) → β)
        (↑x : α) :
      β)
    ((↑((e₀ : (a : (↑s : Type u)) → (↑t : Type v)) x) : β) : β)

Tactic:
simp only [Sum.map_inl, trans_apply, sumCongr_apply, Set.sumCompl_apply_inl,
        Set.sumCompl_symm_apply, Trans.trans]

Premises used: Sum.map_inl, Trans.trans, Equiv.trans_apply, Equiv.Set.sumCompl_symm_apply, Equiv.sumCongr_apply, Equiv.Set.sumCompl_apply_inl
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β_2 : Type u_2
α : Type u
β : Type v
s : Set α
t : Set β
inst : DecidablePred fun (x : α) ↦ x ∈ s
inst_1 : DecidablePred fun (x : β) ↦ x ∈ t
e₀ : Equiv.{u + 1, v + 1} (↑s : Type u) (↑t : Type v)
e :
  { e : α ≃ β //
    ∀ (x : (↑s : Type u)),
      Eq.{v + 1} (α := β) ((e : (a : α) → β) (↑x : α) : β) ((↑((e₀ : (a : (↑s : Type u)) → (↑t : Type v)) x) : β) : β) }
a :
  ∀ (x : α),
    Eq.{v + 1} (α := β)
      (((↑((fun (e₁ : Equiv.{u + 1, v + 1} (↑sᶜ : Type u) (↑tᶜ : Type v)) ↦
                    (Subtype.mk (p := fun (e : α ≃ β) ↦
                        ∀ (x : (↑s : Type u)),
                          Eq.{v + 1} (α := β) ((e : (a : α) → β) (↑x : α) : β)
                            ((↑((e₀ : (a : (↑s : Type u)) → (↑t : Type v)) x) : β) : β))
                        (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
                          (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv) (Set.sumCompl s).symm (e₀.sumCongr e₁))
                          (Set.sumCompl t))
                        ⋯ :
                      { e : α ≃ β //
                        ∀ (x : (↑s : Type u)),
                          Eq.{v + 1} (α := β) ((e : (a : α) → β) (↑x : α) : β)
                            ((↑((e₀ : (a : (↑s : Type u)) → (↑t : Type v)) x) : β) : β) }))
                  ((fun
                        (e :
                          { e : α ≃ β //
                            ∀ (x : (↑s : Type u)),
                              Eq.{v + 1} (α := β) ((e : (a : α) → β) (↑x : α) : β)
                                ((↑((e₀ : (a : (↑s : Type u)) → (↑t : Type v)) x) : β) : β) }) ↦
                      ((↑e : α ≃ β).subtypeEquiv (p := Membership.mem sᶜ) (q := Membership.mem tᶜ) ⋯ :
                        Equiv.{u + 1, v + 1} { a : α // a ∈ sᶜ } { b : β // b ∈ tᶜ }))
                    e)) :
              α ≃ β) :
            (a : α) → β)
          x :
        β)
      (((↑e : α ≃ β) : (a : α) → β) x : β)
⊢ (fun (e₁ : Equiv.{u + 1, v + 1} (↑sᶜ : Type u) (↑tᶜ : Type v)) ↦
        (Subtype.mk (p := fun (e : α ≃ β) ↦
            ∀ (x : (↑s : Type u)),
              Eq.{v + 1} (α := β) ((e : (a : α) → β) (↑x : α) : β)
                ((↑((e₀ : (a : (↑s : Type u)) → (↑t : Type v)) x) : β) : β))
            (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
              (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv) (Set.sumCompl s).symm (e₀.sumCongr e₁))
              (Set.sumCompl t))
            ⋯ :
          { e : α ≃ β //
            ∀ (x : (↑s : Type u)),
              Eq.{v + 1} (α := β) ((e : (a : α) → β) (↑x : α) : β)
                ((↑((e₀ : (a : (↑s : Type u)) → (↑t : Type v)) x) : β) : β) }))
      ((fun
            (e :
              { e : α ≃ β //
                ∀ (x : (↑s : Type u)),
                  Eq.{v + 1} (α := β) ((e : (a : α) → β) (↑x : α) : β)
                    ((↑((e₀ : (a : (↑s : Type u)) → (↑t : Type v)) x) : β) : β) }) ↦
          ((↑e : α ≃ β).subtypeEquiv (p := Membership.mem sᶜ) (q := Membership.mem tᶜ) ⋯ :
            Equiv.{u + 1, v + 1} { a : α // a ∈ sᶜ } { b : β // b ∈ tᶜ }))
        e) =
    e

Tactic:
ext x
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β_2 : Type u_2
α : Type u
β : Type v
s : Set α
t : Set β
inst : DecidablePred fun (x : α) ↦ x ∈ s
inst_1 : DecidablePred fun (x : β) ↦ x ∈ t
e₀ : Equiv.{u + 1, v + 1} (↑s : Type u) (↑t : Type v)
e :
  { e : α ≃ β //
    ∀ (x : (↑s : Type u)),
      Eq.{v + 1} (α := β) ((e : (a : α) → β) (↑x : α) : β) ((↑((e₀ : (a : (↑s : Type u)) → (↑t : Type v)) x) : β) : β) }
x : α
hx : x ∈ s
⊢ Eq.{v + 1} (α := β)
    (((↑((fun (e₁ : Equiv.{u + 1, v + 1} (↑sᶜ : Type u) (↑tᶜ : Type v)) ↦
                  (Subtype.mk (p := fun (e : α ≃ β) ↦
                      ∀ (x : (↑s : Type u)),
                        Eq.{v + 1} (α := β) ((e : (a : α) → β) (↑x : α) : β)
                          ((↑((e₀ : (a : (↑s : Type u)) → (↑t : Type v)) x) : β) : β))
                      (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
                        (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv) (Set.sumCompl s).symm (e₀.sumCongr e₁))
                        (Set.sumCompl t))
                      ⋯ :
                    { e : α ≃ β //
                      ∀ (x : (↑s : Type u)),
                        Eq.{v + 1} (α := β) ((e : (a : α) → β) (↑x : α) : β)
                          ((↑((e₀ : (a : (↑s : Type u)) → (↑t : Type v)) x) : β) : β) }))
                ((fun
                      (e :
                        { e : α ≃ β //
                          ∀ (x : (↑s : Type u)),
                            Eq.{v + 1} (α := β) ((e : (a : α) → β) (↑x : α) : β)
                              ((↑((e₀ : (a : (↑s : Type u)) → (↑t : Type v)) x) : β) : β) }) ↦
                    ((↑e : α ≃ β).subtypeEquiv (p := Membership.mem sᶜ) (q := Membership.mem tᶜ) ⋯ :
                      Equiv.{u + 1, v + 1} { a : α // a ∈ sᶜ } { b : β // b ∈ tᶜ }))
                  e)) :
            α ≃ β) :
          (a : α) → β)
        x :
      β)
    (((↑e : α ≃ β) : (a : α) → β) x : β)

Tactic:
simp only [Set.sumCompl_symm_apply_of_mem hx, ← e.prop ⟨x, hx⟩, Sum.map_inl, sumCongr_apply,
        trans_apply, Set.sumCompl_apply_inl, Trans.trans]

Premises used: Sum.map_inl, Trans.trans, Equiv.trans_apply, Equiv.Set.sumCompl_symm_apply_of_mem, Equiv.sumCongr_apply, Subtype.mk, Subtype.prop, Equiv.Set.sumCompl_apply_inl
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β_2 : Type u_2
α : Type u
β : Type v
s : Set α
t : Set β
inst : DecidablePred fun (x : α) ↦ x ∈ s
inst_1 : DecidablePred fun (x : β) ↦ x ∈ t
e₀ : Equiv.{u + 1, v + 1} (↑s : Type u) (↑t : Type v)
e :
  { e : α ≃ β //
    ∀ (x : (↑s : Type u)),
      Eq.{v + 1} (α := β) ((e : (a : α) → β) (↑x : α) : β) ((↑((e₀ : (a : (↑s : Type u)) → (↑t : Type v)) x) : β) : β) }
x : α
hx : ¬x ∈ s
⊢ Eq.{v + 1} (α := β)
    (((↑((fun (e₁ : Equiv.{u + 1, v + 1} (↑sᶜ : Type u) (↑tᶜ : Type v)) ↦
                  (Subtype.mk (p := fun (e : α ≃ β) ↦
                      ∀ (x : (↑s : Type u)),
                        Eq.{v + 1} (α := β) ((e : (a : α) → β) (↑x : α) : β)
                          ((↑((e₀ : (a : (↑s : Type u)) → (↑t : Type v)) x) : β) : β))
                      (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
                        (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv) (Set.sumCompl s).symm (e₀.sumCongr e₁))
                        (Set.sumCompl t))
                      ⋯ :
                    { e : α ≃ β //
                      ∀ (x : (↑s : Type u)),
                        Eq.{v + 1} (α := β) ((e : (a : α) → β) (↑x : α) : β)
                          ((↑((e₀ : (a : (↑s : Type u)) → (↑t : Type v)) x) : β) : β) }))
                ((fun
                      (e :
                        { e : α ≃ β //
                          ∀ (x : (↑s : Type u)),
                            Eq.{v + 1} (α := β) ((e : (a : α) → β) (↑x : α) : β)
                              ((↑((e₀ : (a : (↑s : Type u)) → (↑t : Type v)) x) : β) : β) }) ↦
                    ((↑e : α ≃ β).subtypeEquiv (p := Membership.mem sᶜ) (q := Membership.mem tᶜ) ⋯ :
                      Equiv.{u + 1, v + 1} { a : α // a ∈ sᶜ } { b : β // b ∈ tᶜ }))
                  e)) :
            α ≃ β) :
          (a : α) → β)
        x :
      β)
    (((↑e : α ≃ β) : (a : α) → β) x : β)

Tactic:
simp only [Set.sumCompl_symm_apply_of_notMem hx, Sum.map_inr, subtypeEquiv_apply,
        Set.sumCompl_apply_inr, trans_apply, sumCongr_apply, Trans.trans]

Premises used: Trans.trans, Equiv.trans_apply, Equiv.subtypeEquiv_apply, Equiv.sumCongr_apply, Equiv.Set.sumCompl_apply_inr, Sum.map_inr, Equiv.Set.sumCompl_symm_apply_of_notMem
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β_2 : Type u_2
α : Type u
β : Type v
s : Set α
t : Set β
inst : DecidablePred fun (x : α) ↦ x ∈ s
inst_1 : DecidablePred fun (x : β) ↦ x ∈ t
e₀ : Equiv.{u + 1, v + 1} (↑s : Type u) (↑t : Type v)
e : Equiv.{u + 1, v + 1} (↑sᶜ : Type u) (↑tᶜ : Type v)
x : { a : α // a ∈ sᶜ }
⊢ Eq.{v + 1} (α := { b : β // b ∈ tᶜ })
    ((((fun
                  (e :
                    { e : α ≃ β //
                      ∀ (x : (↑s : Type u)),
                        Eq.{v + 1} (α := β) ((e : (a : α) → β) (↑x : α) : β)
                          ((↑((e₀ : (a : (↑s : Type u)) → (↑t : Type v)) x) : β) : β) }) ↦
                ((↑e : α ≃ β).subtypeEquiv (p := Membership.mem sᶜ) (q := Membership.mem tᶜ) ⋯ :
                  Equiv.{u + 1, v + 1} { a : α // a ∈ sᶜ } { b : β // b ∈ tᶜ }))
              ((fun (e₁ : Equiv.{u + 1, v + 1} (↑sᶜ : Type u) (↑tᶜ : Type v)) ↦
                  (Subtype.mk (p := fun (e : α ≃ β) ↦
                      ∀ (x : (↑s : Type u)),
                        Eq.{v + 1} (α := β) ((e : (a : α) → β) (↑x : α) : β)
                          ((↑((e₀ : (a : (↑s : Type u)) → (↑t : Type v)) x) : β) : β))
                      (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv)
                        (Trans.trans (r := Equiv) (s := Equiv) (t := Equiv) (Set.sumCompl s).symm (e₀.sumCongr e₁))
                        (Set.sumCompl t))
                      ⋯ :
                    { e : α ≃ β //
                      ∀ (x : (↑s : Type u)),
                        Eq.{v + 1} (α := β) ((e : (a : α) → β) (↑x : α) : β)
                          ((↑((e₀ : (a : (↑s : Type u)) → (↑t : Type v)) x) : β) : β) }))
                e) :
            Equiv.{u + 1, v + 1} { a : α // a ∈ sᶜ } { b : β // b ∈ tᶜ }) :
          (a : { a : α // a ∈ sᶜ }) → { b : β // b ∈ tᶜ })
        x :
      { b : β // b ∈ tᶜ })
    ((e : (a : { a : α // a ∈ sᶜ }) → { b : β // b ∈ tᶜ }) x : { b : β // b ∈ tᶜ })

Tactic:
simp only [Sum.map_inr, subtypeEquiv_apply, Set.sumCompl_apply_inr, Function.comp_apply,
        sumCongr_apply, Equiv.coe_trans, Subtype.coe_eta, Trans.trans,
        Set.sumCompl_symm_apply_compl]

Premises used: Trans.trans, Equiv.subtypeEquiv_apply, Equiv.sumCongr_apply, Subtype.coe_eta, Equiv.Set.sumCompl_apply_inr, Function.comp_apply, Sum.map_inr, Equiv.coe_trans, Equiv.Set.sumCompl_symm_apply_compl
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
f : α → β
s : Set α
H : Injective f
x : α
h : f x ∈ f '' s
⊢ ((Set.image f s H).symm : (a : (↑(f '' s) : Type u_4)) → (↑s : Type u_3))
      (Subtype.mk (p := fun (x : β) ↦ x ∈ f '' s) (f x) h) =
    Subtype.mk (p := fun (x : α) ↦ x ∈ s) x ⋯

Tactic:
(Equiv.symm_apply_eq _).2 rfl

Premises used: Iff.mpr, Equiv.symm_apply_eq, rfl
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
f : α → β
hf : Injective f
u s : Set α
h :
  ∀ (a : α) (has : a ∈ s),
    Membership.mem (γ := Set (↑(f '' s) : Type u_4))
        ((fun (x : (↑(f '' s) : Type u_4)) ↦
            (↑(((Set.image f s hf).symm : (a : (↑(f '' s) : Type u_4)) → (↑s : Type u_3)) x) : α)) ⁻¹'
          u)
        (Subtype.mk (p := fun (x : β) ↦ x ∈ f '' s) (f a) ⋯) ↔
      Membership.mem (γ := Set (↑(f '' s) : Type u_4)) (Subtype.val (p := fun (x : β) ↦ x ∈ f '' s) ⁻¹' f '' u)
        (Subtype.mk (p := fun (x : β) ↦ x ∈ f '' s) (f a) ⋯)
⊢ Eq (α := Set (↑(f '' s) : Type u_4))
    ((fun (x : (↑(f '' s) : Type u_4)) ↦
        (↑(((Set.image f s hf).symm : (a : (↑(f '' s) : Type u_4)) → (↑s : Type u_3)) x) : α)) ⁻¹'
      u)
    (Subtype.val (p := fun (x : β) ↦ x ∈ f '' s) ⁻¹' f '' u)

Tactic:
ext ⟨b, a, has, rfl⟩

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
f : α → β
hf : Injective f
u s : Set α
a : α
has : a ∈ s
⊢ Membership.mem (γ := Set (↑(f '' s) : Type u_4))
      ((fun (x : (↑(f '' s) : Type u_4)) ↦
          (↑(((Set.image f s hf).symm : (a : (↑(f '' s) : Type u_4)) → (↑s : Type u_3)) x) : α)) ⁻¹'
        u)
      (Subtype.mk (p := fun (x : β) ↦ x ∈ f '' s) (f a) ⋯) ↔
    Membership.mem (γ := Set (↑(f '' s) : Type u_4)) (Subtype.val (p := fun (x : β) ↦ x ∈ f '' s) ⁻¹' f '' u)
      (Subtype.mk (p := fun (x : β) ↦ x ∈ f '' s) (f a) ⋯)

Tactic:
simp [hf.eq_iff]

Premises used: Function.Injective.eq_iff
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β : Type u_2
α : Type u_3
S : Set α
x : Set (↑S : Type u_3)
a : (↑S : Type u_3)
left : a ∈ x
⊢ (↑a : α) ∈ S

Tactic:
a.2

Premises used: Subtype.property
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β : Type u_2
α : Type u_3
S : Set α
x : Set (↑S : Type u_3)
a : (↑S : Type u_3)
left : a ∈ x
⊢ (↑a : α) ∈ S

Tactic:
exact a.2

Premises used: Subtype.property
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β : Type u_2
α : Type u_3
S : Set α
x : (↑(𝒫 S) : Type u_3)
a :
  ∀ (y : α),
    Membership.mem (γ := Set α)
        (↑((fun (x : Set (↑S : Type u_3)) ↦
                Subtype.mk (p := fun (x : Set α) ↦ x ∈ 𝒫 S) (Subtype.val (p := fun (x : α) ↦ x ∈ S) '' x) ⋯)
              ((fun (x : (↑(𝒫 S) : Type u_3)) ↦
                  (Subtype.val (p := fun (x : α) ↦ x ∈ S) ⁻¹' (↑x : Set α) : Set (↑S : Type u_3)))
                x)) :
          Set α)
        y ↔
      y ∈ (↑x : Set α)
⊢ (fun (x : Set (↑S : Type u_3)) ↦
        Subtype.mk (p := fun (x : Set α) ↦ x ∈ 𝒫 S) (Subtype.val (p := fun (x : α) ↦ x ∈ S) '' x) ⋯)
      ((fun (x : (↑(𝒫 S) : Type u_3)) ↦ (Subtype.val (p := fun (x : α) ↦ x ∈ S) ⁻¹' (↑x : Set α) : Set (↑S : Type u_3)))
        x) =
    x

Tactic:
ext y
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β : Type u_2
α : Type u_3
S : Set α
x : (↑(𝒫 S) : Type u_3)
y : α
⊢ Membership.mem (γ := Set α)
      (↑((fun (x : Set (↑S : Type u_3)) ↦
              Subtype.mk (p := fun (x : Set α) ↦ x ∈ 𝒫 S) (Subtype.val (p := fun (x : α) ↦ x ∈ S) '' x) ⋯)
            ((fun (x : (↑(𝒫 S) : Type u_3)) ↦
                (Subtype.val (p := fun (x : α) ↦ x ∈ S) ⁻¹' (↑x : Set α) : Set (↑S : Type u_3)))
              x)) :
        Set α)
      y ↔
    y ∈ (↑x : Set α)

Tactic:
⟨fun ⟨⟨_, _⟩, h, rfl⟩ => h, fun h => ⟨⟨_, x.2 h⟩, h, rfl⟩⟩

Premises used: Membership.mem, Subtype.mk, And.intro, Iff.intro, Exists.intro, _private.0.Equiv.Set.powerset.match_1, Subtype.val, rfl, Subtype.property
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β : Type u_2
α : Type u_3
S : Set α
x : (↑(𝒫 S) : Type u_3)
y : α
⊢ Membership.mem (γ := Set α)
      (↑((fun (x : Set (↑S : Type u_3)) ↦
              Subtype.mk (p := fun (x : Set α) ↦ x ∈ 𝒫 S) (Subtype.val (p := fun (x : α) ↦ x ∈ S) '' x) ⋯)
            ((fun (x : (↑(𝒫 S) : Type u_3)) ↦
                (Subtype.val (p := fun (x : α) ↦ x ∈ S) ⁻¹' (↑x : Set α) : Set (↑S : Type u_3)))
              x)) :
        Set α)
      y ↔
    y ∈ (↑x : Set α)

Tactic:
exact ⟨fun ⟨⟨_, _⟩, h, rfl⟩ => h, fun h => ⟨⟨_, x.2 h⟩, h, rfl⟩⟩
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β : Type u_2
α : Type u_3
S : Set α
x : Set (↑S : Type u_3)
h :
  ∀ (x_1 : (↑S : Type u_3)),
    Membership.mem (γ := Set (↑S : Type u_3))
        ((fun (x : (↑(𝒫 S) : Type u_3)) ↦
            (Subtype.val (p := fun (x : α) ↦ x ∈ S) ⁻¹' (↑x : Set α) : Set (↑S : Type u_3)))
          ((fun (x : Set (↑S : Type u_3)) ↦
              Subtype.mk (p := fun (x : Set α) ↦ x ∈ 𝒫 S) (Subtype.val (p := fun (x : α) ↦ x ∈ S) '' x) ⋯)
            x))
        x_1 ↔
      x_1 ∈ x
⊢ (fun (x : (↑(𝒫 S) : Type u_3)) ↦ (Subtype.val (p := fun (x : α) ↦ x ∈ S) ⁻¹' (↑x : Set α) : Set (↑S : Type u_3)))
      ((fun (x : Set (↑S : Type u_3)) ↦
          Subtype.mk (p := fun (x : Set α) ↦ x ∈ 𝒫 S) (Subtype.val (p := fun (x : α) ↦ x ∈ S) '' x) ⋯)
        x) =
    x

Tactic:
ext
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β : Type u_2
α : Type u_3
S : Set α
x : Set (↑S : Type u_3)
x_1 : (↑S : Type u_3)
⊢ Membership.mem (γ := Set (↑S : Type u_3))
      ((fun (x : (↑(𝒫 S) : Type u_3)) ↦ (Subtype.val (p := fun (x : α) ↦ x ∈ S) ⁻¹' (↑x : Set α) : Set (↑S : Type u_3)))
        ((fun (x : Set (↑S : Type u_3)) ↦
            Subtype.mk (p := fun (x : Set α) ↦ x ∈ 𝒫 S) (Subtype.val (p := fun (x : α) ↦ x ∈ S) '' x) ⋯)
          x))
      x_1 ↔
    x_1 ∈ x

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β_2 : Type u_2
α : Type u_3
β : Type u_4
f : α → β
s : Set (↑(range f) : Type u_4)
x : (↑(rangeSplitting f '' s) : Type u_3)
⊢ f (↑x : α) ∈ range f

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β_2 : Type u_2
α : Type u_3
β : Type u_4
f : α → β
s : Set (↑(range f) : Type u_4)
x : (↑(rangeSplitting f '' s) : Type u_3)
rcases :
  ∀ (y : (↑(range f) : Type u_4)) (m : y ∈ s),
    Subtype.mk (p := fun (x : β) ↦ x ∈ range f)
        (f (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ rangeSplitting f '' s) (rangeSplitting f y) ⋯) : α)) ⋯ ∈
      s
⊢ Subtype.mk (p := fun (x : β) ↦ x ∈ range f) (f (↑x : α)) ⋯ ∈ s

Tactic:
rcases x with ⟨x, ⟨y, ⟨m, rfl⟩⟩⟩

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β_2 : Type u_2
α : Type u_3
β : Type u_4
f : α → β
s : Set (↑(range f) : Type u_4)
y : (↑(range f) : Type u_4)
m : y ∈ s
⊢ Subtype.mk (p := fun (x : β) ↦ x ∈ range f)
      (f (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ rangeSplitting f '' s) (rangeSplitting f y) ⋯) : α)) ⋯ ∈
    s

Tactic:
simpa [apply_rangeSplitting f] using m

Premises used: Set.apply_rangeSplitting
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β_2 : Type u_2
α : Type u_3
β : Type u_4
f : α → β
s : Set (↑(range f) : Type u_4)
x : (↑(rangeSplitting f '' s) : Type u_3)
rcases :
  ∀ (y : (↑(range f) : Type u_4)) (m : y ∈ s),
    Eq (α := (↑(rangeSplitting f '' s) : Type u_3))
      ((fun (x : (↑s : Type u_4)) ↦
          (Subtype.mk (p := fun (x : α) ↦ x ∈ rangeSplitting f '' s) (rangeSplitting f (↑x : (↑(range f) : Type u_4)))
              ⋯ :
            { x : α // x ∈ rangeSplitting f '' s }))
        ((fun (x : (↑(rangeSplitting f '' s) : Type u_3)) ↦
            Subtype.mk (p := fun (x : (↑(range f) : Type u_4)) ↦ x ∈ s)
              (Subtype.mk (p := fun (x : β) ↦ x ∈ range f) (f (↑x : α)) ⋯) ⋯)
          (Subtype.mk (p := fun (x : α) ↦ x ∈ rangeSplitting f '' s) (rangeSplitting f y) ⋯)))
      (Subtype.mk (p := fun (x : α) ↦ x ∈ rangeSplitting f '' s) (rangeSplitting f y) ⋯)
⊢ (fun (x : (↑s : Type u_4)) ↦
        (Subtype.mk (p := fun (x : α) ↦ x ∈ rangeSplitting f '' s) (rangeSplitting f (↑x : (↑(range f) : Type u_4))) ⋯ :
          { x : α // x ∈ rangeSplitting f '' s }))
      ((fun (x : (↑(rangeSplitting f '' s) : Type u_3)) ↦
          Subtype.mk (p := fun (x : (↑(range f) : Type u_4)) ↦ x ∈ s)
            (Subtype.mk (p := fun (x : β) ↦ x ∈ range f) (f (↑x : α)) ⋯) ⋯)
        x) =
    x

Tactic:
rcases x with ⟨x, ⟨y, ⟨m, rfl⟩⟩⟩

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β_2 : Type u_2
α : Type u_3
β : Type u_4
f : α → β
s : Set (↑(range f) : Type u_4)
y : (↑(range f) : Type u_4)
m : y ∈ s
⊢ Eq (α := (↑(rangeSplitting f '' s) : Type u_3))
    ((fun (x : (↑s : Type u_4)) ↦
        (Subtype.mk (p := fun (x : α) ↦ x ∈ rangeSplitting f '' s) (rangeSplitting f (↑x : (↑(range f) : Type u_4))) ⋯ :
          { x : α // x ∈ rangeSplitting f '' s }))
      ((fun (x : (↑(rangeSplitting f '' s) : Type u_3)) ↦
          Subtype.mk (p := fun (x : (↑(range f) : Type u_4)) ↦ x ∈ s)
            (Subtype.mk (p := fun (x : β) ↦ x ∈ range f) (f (↑x : α)) ⋯) ⋯)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ rangeSplitting f '' s) (rangeSplitting f y) ⋯)))
    (Subtype.mk (p := fun (x : α) ↦ x ∈ rangeSplitting f '' s) (rangeSplitting f y) ⋯)

Tactic:
simp [apply_rangeSplitting f]

Premises used: Set.apply_rangeSplitting
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β_2 : Type u_2
α : Type u_3
β : Type u_4
f : α → β
s : Set (↑(range f) : Type u_4)
x : (↑s : Type u_4)
⊢ (fun (x : (↑(rangeSplitting f '' s) : Type u_3)) ↦
        Subtype.mk (p := fun (x : (↑(range f) : Type u_4)) ↦ x ∈ s)
          (Subtype.mk (p := fun (x : β) ↦ x ∈ range f) (f (↑x : α)) ⋯) ⋯)
      ((fun (x : (↑s : Type u_4)) ↦
          (Subtype.mk (p := fun (x : α) ↦ x ∈ rangeSplitting f '' s) (rangeSplitting f (↑x : (↑(range f) : Type u_4)))
              ⋯ :
            { x : α // x ∈ rangeSplitting f '' s }))
        x) =
    x

Tactic:
simp [apply_rangeSplitting f]

Premises used: Set.apply_rangeSplitting
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β_2 : Type u_2
α : Type u_3
β : Type u_4
val : β
h : Membership.mem (γ := Set (α ⊕ β)) (range Sum.inl) (Sum.inr val)
rcases : ∀ (x : α) (h' : Sum.inl x = Sum.inr val), False
⊢ False

Tactic:
rcases h with ⟨x, h'⟩
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β_2 : Type u_2
α : Type u_3
β : Type u_4
val : β
x : α
h' : Sum.inl x = Sum.inr val
⊢ False

Tactic:
cases h'
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
x : α
⊢ (rangeInl α β : (a : (↑(range Sum.inl) : Type (max u_3 u_4))) → α)
      (Subtype.mk (p := fun (x : α ⊕ β) ↦ Membership.mem (γ := Set (α ⊕ β)) (range Sum.inl) x) (Sum.inl x) ⋯) =
    x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α_1 : Sort u
β_1 : Sort v
γ : Sort w
α_2 : Type u_1
β_2 : Type u_2
α : Type u_3
β : Type u_4
val : α
h : Membership.mem (γ := Set (α ⊕ β)) (range Sum.inr) (Sum.inl val)
rcases : ∀ (x : β) (h' : Sum.inr x = Sum.inl val), False
⊢ False

Tactic:
rcases h with ⟨x, h'⟩