awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
p : α → Prop
β : α → Type u_10
inst : DecidablePred p
f : (i : { x : α // p x }) → β (↑i : α)
g : (i : { x : α // ¬p x }) → β (↑i : α)
fst :
  Prod.fst (β := (i : { x : α // ¬p x }) → β (↑i : α))
      ((fun (f : (i : α) → β i) ↦
          ((fun (x : { x : α // p x }) ↦ f (↑x : α), fun (x : { x : α // ¬p x }) ↦ f (↑x : α)) :
            ((i : { x : α // p x }) → β (↑i : α)) × ((i : { x : α // ¬p x }) → β (↑i : α))))
        ((fun (f : ((i : { x : α // p x }) → β (↑i : α)) × ((i : { x : α // ¬p x }) → β (↑i : α))) (x : α) ↦
            (if h : p x then f.fst (Subtype.mk (p := fun (x : α) ↦ p x) x h)
              else f.snd (Subtype.mk (p := fun (x : α) ↦ ¬p x) x h) :
              β x))
          (f, g))) =
    (f, g).fst
snd :
  Prod.snd (α := (i : { x : α // p x }) → β (↑i : α))
      ((fun (f : (i : α) → β i) ↦
          ((fun (x : { x : α // p x }) ↦ f (↑x : α), fun (x : { x : α // ¬p x }) ↦ f (↑x : α)) :
            ((i : { x : α // p x }) → β (↑i : α)) × ((i : { x : α // ¬p x }) → β (↑i : α))))
        ((fun (f : ((i : { x : α // p x }) → β (↑i : α)) × ((i : { x : α // ¬p x }) → β (↑i : α))) (x : α) ↦
            (if h : p x then f.fst (Subtype.mk (p := fun (x : α) ↦ p x) x h)
              else f.snd (Subtype.mk (p := fun (x : α) ↦ ¬p x) x h) :
              β x))
          (f, g))) =
    (f, g).snd
⊢ (fun (f : (i : α) → β i) ↦
        ((fun (x : { x : α // p x }) ↦ f (↑x : α), fun (x : { x : α // ¬p x }) ↦ f (↑x : α)) :
          ((i : { x : α // p x }) → β (↑i : α)) × ((i : { x : α // ¬p x }) → β (↑i : α))))
      ((fun (f : ((i : { x : α // p x }) → β (↑i : α)) × ((i : { x : α // ¬p x }) → β (↑i : α))) (x : α) ↦
          (if h : p x then f.fst (Subtype.mk (p := fun (x : α) ↦ p x) x h)
            else f.snd (Subtype.mk (p := fun (x : α) ↦ ¬p x) x h) :
            β x))
        (f, g)) =
    (f, g)

Tactic:
ext1
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
p : α → Prop
β : α → Type u_10
inst : DecidablePred p
f : (i : { x : α // p x }) → β (↑i : α)
g : (i : { x : α // ¬p x }) → β (↑i : α)
⊢ Prod.fst (β := (i : { x : α // ¬p x }) → β (↑i : α))
      ((fun (f : (i : α) → β i) ↦
          ((fun (x : { x : α // p x }) ↦ f (↑x : α), fun (x : { x : α // ¬p x }) ↦ f (↑x : α)) :
            ((i : { x : α // p x }) → β (↑i : α)) × ((i : { x : α // ¬p x }) → β (↑i : α))))
        ((fun (f : ((i : { x : α // p x }) → β (↑i : α)) × ((i : { x : α // ¬p x }) → β (↑i : α))) (x : α) ↦
            (if h : p x then f.fst (Subtype.mk (p := fun (x : α) ↦ p x) x h)
              else f.snd (Subtype.mk (p := fun (x : α) ↦ ¬p x) x h) :
              β x))
          (f, g))) =
    (f, g).fst

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
p : α → Prop
β : α → Type u_10
inst : DecidablePred p
f : (i : { x : α // p x }) → β (↑i : α)
g : (i : { x : α // ¬p x }) → β (↑i : α)
⊢ Prod.snd (α := (i : { x : α // p x }) → β (↑i : α))
      ((fun (f : (i : α) → β i) ↦
          ((fun (x : { x : α // p x }) ↦ f (↑x : α), fun (x : { x : α // ¬p x }) ↦ f (↑x : α)) :
            ((i : { x : α // p x }) → β (↑i : α)) × ((i : { x : α // ¬p x }) → β (↑i : α))))
        ((fun (f : ((i : { x : α // p x }) → β (↑i : α)) × ((i : { x : α // ¬p x }) → β (↑i : α))) (x : α) ↦
            (if h : p x then f.fst (Subtype.mk (p := fun (x : α) ↦ p x) x h)
              else f.snd (Subtype.mk (p := fun (x : α) ↦ ¬p x) x h) :
              β x))
          (f, g))) =
    (f, g).snd

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
inst : DecidableEq α
i : α
β : α → Type u_10
f : (j : α) → β j
⊢ (fun (f : β i × ((j : { j : α // j ≠ i }) → β (↑j : α))) (j : α) ↦
        (if h : j = i then Eq.rec (motive := fun (x : α) (x_1 : i = x) ↦ β x) f.fst ⋯
          else f.snd (Subtype.mk (p := fun (j : α) ↦ j ≠ i) j h) :
          β j))
      ((fun (f : (j : α) → β j) ↦
          ((f i, fun (j : { j : α // j ≠ i }) ↦ f (↑j : α)) : β i × ((j : { j : α // j ≠ i }) → β (↑j : α))))
        f) =
    f

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
inst : DecidableEq α
i : α
β : α → Type u_10
f : β i × ((j : { j : α // j ≠ i }) → β (↑j : α))
fst :
  Prod.fst (β := (j : { j : α // j ≠ i }) → β (↑j : α))
      ((fun (f : (j : α) → β j) ↦
          ((f i, fun (j : { j : α // j ≠ i }) ↦ f (↑j : α)) : β i × ((j : { j : α // j ≠ i }) → β (↑j : α))))
        ((fun (f : β i × ((j : { j : α // j ≠ i }) → β (↑j : α))) (j : α) ↦
            (if h : j = i then Eq.rec (motive := fun (x : α) (x_1 : i = x) ↦ β x) f.fst ⋯
              else f.snd (Subtype.mk (p := fun (j : α) ↦ j ≠ i) j h) :
              β j))
          f)) =
    f.fst
snd :
  ∀ (x : { j : α // j ≠ i }),
    Prod.snd (α := β i)
        ((fun (f : (j : α) → β j) ↦
            ((f i, fun (j : { j : α // j ≠ i }) ↦ f (↑j : α)) : β i × ((j : { j : α // j ≠ i }) → β (↑j : α))))
          ((fun (f : β i × ((j : { j : α // j ≠ i }) → β (↑j : α))) (j : α) ↦
              (if h : j = i then Eq.rec (motive := fun (x : α) (x_1 : i = x) ↦ β x) f.fst ⋯
                else f.snd (Subtype.mk (p := fun (j : α) ↦ j ≠ i) j h) :
                β j))
            f))
        x =
      f.snd x
⊢ (fun (f : (j : α) → β j) ↦
        ((f i, fun (j : { j : α // j ≠ i }) ↦ f (↑j : α)) : β i × ((j : { j : α // j ≠ i }) → β (↑j : α))))
      ((fun (f : β i × ((j : { j : α // j ≠ i }) → β (↑j : α))) (j : α) ↦
          (if h : j = i then Eq.rec (motive := fun (x : α) (x_1 : i = x) ↦ β x) f.fst ⋯
            else f.snd (Subtype.mk (p := fun (j : α) ↦ j ≠ i) j h) :
            β j))
        f) =
    f

Tactic:
ext x
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
inst : DecidableEq α
i : α
β : α → Type u_10
f : β i × ((j : { j : α // j ≠ i }) → β (↑j : α))
⊢ Prod.fst (β := (j : { j : α // j ≠ i }) → β (↑j : α))
      ((fun (f : (j : α) → β j) ↦
          ((f i, fun (j : { j : α // j ≠ i }) ↦ f (↑j : α)) : β i × ((j : { j : α // j ≠ i }) → β (↑j : α))))
        ((fun (f : β i × ((j : { j : α // j ≠ i }) → β (↑j : α))) (j : α) ↦
            (if h : j = i then Eq.rec (motive := fun (x : α) (x_1 : i = x) ↦ β x) f.fst ⋯
              else f.snd (Subtype.mk (p := fun (j : α) ↦ j ≠ i) j h) :
              β j))
          f)) =
    f.fst

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α_1 : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β_1 : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type u_9
inst : DecidableEq α
i : α
β : α → Type u_10
f : β i × ((j : { j : α // j ≠ i }) → β (↑j : α))
x : { j : α // j ≠ i }
⊢ Prod.snd (α := β i)
      ((fun (f : (j : α) → β j) ↦
          ((f i, fun (j : { j : α // j ≠ i }) ↦ f (↑j : α)) : β i × ((j : { j : α // j ≠ i }) → β (↑j : α))))
        ((fun (f : β i × ((j : { j : α // j ≠ i }) → β (↑j : α))) (j : α) ↦
            (if h : j = i then Eq.rec (motive := fun (x : α) (x_1 : i = x) ↦ β x) f.fst ⋯
              else f.snd (Subtype.mk (p := fun (j : α) ↦ j ≠ i) j h) :
              β j))
          f))
      x =
    f.snd x

Tactic:
grind
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Type u_9
β : Type u_10
b : β
⊢ Eq (α := β ⊕ α × β) ((optionProdEquiv : (a : Option α × β) → β ⊕ α × β) (none, b) : β ⊕ α × β) (Sum.inl b : β ⊕ α × β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Type u_9
β : Type u_10
a : α
b : β
⊢ Eq (α := β ⊕ α × β) ((optionProdEquiv : (a : Option α × β) → β ⊕ α × β) (some a, b) : β ⊕ α × β)
    (Sum.inr (a, b) : β ⊕ α × β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Type u_9
β : Type u_10
b : β
⊢ Eq (α := Prod.{u_9, u_10} (Option α) β)
    ((Equiv.symm optionProdEquiv : (a : β ⊕ α × β) → Option α × β) (Sum.inl b) : Prod.{u_9, u_10} (Option α) β)
    ((none, b) : Prod.{u_9, u_10} (Option α) β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Prod
Goal:
α : Type u_9
β : Type u_10
p : α × β
⊢ (Equiv.symm optionProdEquiv : (a : β ⊕ α × β) → Option α × β) (Sum.inr p) = Prod.map some id p

Tactic:
rfl

Premises used: Prod.map, rfl
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : EquivLike E α β
e : E
⊢ Eq.{u_2 + 1} (α := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β)) univ

Tactic:
eq_univ_of_forall (EquivLike.toEquiv e).surjective

Premises used: Set.eq_univ_of_forall, Equiv.surjective, EquivLike.toEquiv
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
⊢ Eq.{u_2 + 1} (α := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β)) univ

Tactic:
EquivLike.range_eq_univ e

Premises used: EquivLike.range_eq_univ
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set β
h :
  ∀ (x : α),
    Membership.mem (γ := Set α) ((⇑e.symm : (a : β) → α) '' s) x ↔
      Membership.mem (γ := Set α) ((⇑e : (a : α) → β) ⁻¹' s) x
⊢ Eq.{u_1 + 1} (α := Set α) ((⇑e.symm : (a : β) → α) '' s) ((⇑e : (a : α) → β) ⁻¹' s)

Tactic:
ext
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set β
x : α
⊢ Membership.mem (γ := Set α) ((⇑e.symm : (a : β) → α) '' s) x ↔
    Membership.mem (γ := Set α) ((⇑e : (a : α) → β) ⁻¹' s) x

Tactic:
mem_image_iff_of_inverse e.right_inv e.left_inv

Premises used: Equiv.right_inv, Set.Mem, setOf, Set.preimage, Set.mem_image_iff_of_inverse, Equiv.left_inv
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set β
x : α
⊢ Membership.mem (γ := Set α) ((⇑e.symm : (a : β) → α) '' s) x ↔
    Membership.mem (γ := Set α) ((⇑e : (a : α) → β) ⁻¹' s) x

Tactic:
exact mem_image_iff_of_inverse e.right_inv e.left_inv

Premises used: Equiv.right_inv, Set.mem_image_iff_of_inverse, Equiv.left_inv
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' s) ((⇑e.symm : (a : β) → α) ⁻¹' s)

Tactic:
e.symm.image_symm_eq_preimage _

Premises used: Equiv.symm, Equiv.image_symm_eq_preimage
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
S : Set α
f : α ≃ β
x : β
⊢ Membership.mem (γ := Set β) ((⇑f : (a : α) → β) '' S) x ↔ Membership.mem (α := α) S ((f.symm : (a : β) → α) x : α)

Tactic:
Set.ext_iff.mp (image_eq_preimage_symm ..) x

Premises used: Set.Mem, setOf, Equiv.image_eq_preimage_symm, Set.preimage, Iff.mp, Set.ext_iff
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
e : α ≃ β
s : Set α
t : Set β
rw : t ⊆ (⇑e.symm : (a : β) → α) ⁻¹' s ↔ t ⊆ (⇑e : (a : α) → β) '' s
rw₁ rw₂ : t ⊆ (⇑e.symm : (a : β) → α) ⁻¹' s ↔ t ⊆ (⇑e.symm : (a : β) → α) ⁻¹' s
⊢ (⇑e.symm : (a : β) → α) '' t ⊆ s ↔ t ⊆ (⇑e : (a : α) → β) '' s

Tactic:
rw [image_subset_iff, image_eq_preimage_symm]

Premises used: Equiv.image_eq_preimage_symm, Set.image_subset_iff
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
e : α ≃ β
s : Set α
t : Set β
rw rw₁ : s ⊆ (⇑e.symm : (a : β) → α) '' t ↔ s ⊆ (⇑e.symm : (a : β) → α) '' t
⊢ s ⊆ (⇑e.symm : (a : β) → α) '' t ↔ (⇑e.symm.symm : (a : α) → β) '' s ⊆ t

Tactic:
rw [e.symm.symm_image_subset]

Premises used: Equiv.symm, Equiv.symm_image_subset
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
e : α ≃ β
s : Set α
t : Set β
rw rw₁ : (⇑e : (a : α) → β) '' s ⊆ t ↔ (⇑e : (a : α) → β) '' s ⊆ t
⊢ (⇑e.symm.symm : (a : α) → β) '' s ⊆ t ↔ (⇑e : (a : α) → β) '' s ⊆ t

Tactic:
rw [e.symm_symm]

Premises used: Equiv.symm_symm
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
e : α ≃ β
s : Set α
⊢ image.{u_4, u_3} (α := β) (⇑e.symm : (a : β) → α) ((⇑e : (a : α) → β) '' s) = s

Tactic:
e.leftInverse_symm.image_image s

Premises used: Function.LeftInverse.image_image, Equiv.leftInverse_symm
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
e : α ≃ β
s : Set α
t : Set β
⊢ t = (⇑e : (a : α) → β) '' s ↔ (⇑e.symm : (a : β) → α) '' t = s

Tactic:
(e.symm.injective.image_injective.eq_iff' (e.symm_image_image s)).symm

Premises used: Function.Injective.eq_iff', Equiv.injective, Equiv.symm, Equiv.symm_image_image, Iff.symm, Function.Injective.image_injective
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
e : α ≃ β
s : Set β
⊢ image.{u_3, u_4} (α := α) (⇑e : (a : α) → β) ((⇑e.symm : (a : β) → α) '' s) = s

Tactic:
e.symm.symm_image_image s

Premises used: Equiv.symm, Equiv.symm_image_image
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
e : α ≃ β
s : Set β
⊢ image.{u_3, u_4} (α := α) (⇑e : (a : α) → β) ((⇑e : (a : α) → β) ⁻¹' s) = s

Tactic:
e.surjective.image_preimage s

Premises used: Equiv.surjective, Function.Surjective.image_preimage
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
e : α ≃ β
s : Set α
⊢ preimage.{u_3, u_4} (β := β) (⇑e : (a : α) → β) ((⇑e : (a : α) → β) '' s) = s

Tactic:
e.injective.preimage_image s

Premises used: Function.Injective.preimage_image, Equiv.injective
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
f : α ≃ β
s : Set α
⊢ Eq.{u_4 + 1} (α := Set β) ((⇑f : (a : α) → β) '' sᶜ) ((⇑f : (a : α) → β) '' s)ᶜ

Tactic:
image_compl_eq f.bijective

Premises used: Equiv.bijective, Set.Mem, setOf, Set.image_compl_eq
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
e : α ≃ β
s : Set β
⊢ preimage.{u_4, u_3} (β := α) (⇑e.symm : (a : β) → α) ((⇑e : (a : α) → β) ⁻¹' s) = s

Tactic:
e.rightInverse_symm.preimage_preimage s

Premises used: Function.LeftInverse.preimage_preimage, Equiv.rightInverse_symm
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
e : α ≃ β
s : Set α
⊢ preimage.{u_3, u_4} (β := β) (⇑e : (a : α) → β) ((⇑e.symm : (a : β) → α) ⁻¹' s) = s

Tactic:
e.leftInverse_symm.preimage_preimage s

Premises used: Function.LeftInverse.preimage_preimage, Equiv.leftInverse_symm
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
e : α ≃ β
s t : Set β
⊢ Subset.{u_3} (α := Set α) ((⇑e : (a : α) → β) ⁻¹' s) ((⇑e : (a : α) → β) ⁻¹' t) ↔ s ⊆ t

Tactic:
e.surjective.preimage_subset_preimage_iff

Premises used: Function.Surjective.preimage_subset_preimage_iff, Equiv.surjective
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
e : α ≃ β
s t : Set α
⊢ Subset.{u_4} (α := Set β) ((⇑e : (a : α) → β) '' s) ((⇑e : (a : α) → β) '' t) ↔ s ⊆ t

Tactic:
image_subset_image_iff e.injective

Premises used: Set.image_subset_image_iff, Equiv.injective
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
e : α ≃ β
s t : Set α
⊢ Eq.{u_4 + 1} (α := Set β) ((⇑e : (a : α) → β) '' s) ((⇑e : (a : α) → β) '' t) ↔ s = t

Tactic:
image_eq_image e.injective

Premises used: Set.image_eq_image, Equiv.injective
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
e : α ≃ β
s : Set β
t : Set α
⊢ (⇑e : (a : α) → β) ⁻¹' s = t ↔ s = (⇑e : (a : α) → β) '' t

Tactic:
Set.preimage_eq_iff_eq_image e.bijective

Premises used: Equiv.bijective, Set.preimage_eq_iff_eq_image
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
e : α ≃ β
s : Set α
t : Set β
⊢ s = (⇑e : (a : α) → β) ⁻¹' t ↔ (⇑e : (a : α) → β) '' s = t

Tactic:
Set.eq_preimage_iff_image_eq e.bijective

Premises used: Equiv.bijective, Set.eq_preimage_iff_image_eq
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
e : α ≃ β
p : α → Prop
rw :
  Eq.{u_4 + 1} (α := Set β) {b : β | p ((e.symm : (a : β) → α) b)}
    (preimage.{u_4, u_3} (β := α) (⇑e.symm : (a : β) → α) {a : α | p a})
rw₁ rw₂ : Eq.{u_4 + 1} (α := Set β) {b : β | p ((e.symm : (a : β) → α) b)} {a : β | p ((e.symm : (a : β) → α) a)}
⊢ Eq.{u_4 + 1} (α := Set β) {b : β | p ((e.symm : (a : β) → α) b)}
    (image.{u_3, u_4} (α := α) (⇑e : (a : α) → β) {a : α | p a})

Tactic:
rw [Equiv.image_eq_preimage_symm, preimage_setOf_eq]

Premises used: Set.preimage_setOf_eq, Equiv.image_eq_preimage_symm
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
s : Set α
t : Set β
u : Set γ
h :
  ∀ (x : (α × β) × γ),
    Membership.mem (γ := Set ((α × β) × γ)) ((⇑(prodAssoc α β γ) : (a : (α × β) × γ) → α × β × γ) ⁻¹' s ×ˢ t ×ˢ u) x ↔
      x ∈ (s ×ˢ t) ×ˢ u
⊢ (⇑(prodAssoc α β γ) : (a : (α × β) × γ) → α × β × γ) ⁻¹' s ×ˢ t ×ˢ u = (s ×ˢ t) ×ˢ u

Tactic:
ext
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
s : Set α
t : Set β
u : Set γ
x : (α × β) × γ
⊢ Membership.mem (γ := Set ((α × β) × γ)) ((⇑(prodAssoc α β γ) : (a : (α × β) × γ) → α × β × γ) ⁻¹' s ×ˢ t ×ˢ u) x ↔
    x ∈ (s ×ˢ t) ×ˢ u

Tactic:
simp [and_assoc]

Premises used: and_assoc
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
s : Set α
t : Set β
u : Set γ
h :
  ∀ (x : α × β × γ),
    Membership.mem (γ := Set (α × β × γ)) ((⇑(prodAssoc α β γ).symm : (a : α × β × γ) → (α × β) × γ) ⁻¹' (s ×ˢ t) ×ˢ u)
        x ↔
      x ∈ s ×ˢ t ×ˢ u
⊢ (⇑(prodAssoc α β γ).symm : (a : α × β × γ) → (α × β) × γ) ⁻¹' (s ×ˢ t) ×ˢ u = s ×ˢ t ×ˢ u

Tactic:
ext
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
s : Set α
t : Set β
u : Set γ
x : α × β × γ
⊢ Membership.mem (γ := Set (α × β × γ)) ((⇑(prodAssoc α β γ).symm : (a : α × β × γ) → (α × β) × γ) ⁻¹' (s ×ˢ t) ×ˢ u)
      x ↔
    x ∈ s ×ˢ t ×ˢ u

Tactic:
simp [and_assoc]

Premises used: and_assoc
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
s : Set α
t : Set β
u : Set γ
⊢ (⇑(prodAssoc α β γ) : (a : (α × β) × γ) → α × β × γ) '' (s ×ˢ t) ×ˢ u = s ×ˢ t ×ˢ u

Tactic:
simpa only [Equiv.image_eq_preimage_symm] using prod_assoc_symm_preimage

Premises used: Equiv.image_eq_preimage_symm, Equiv.prod_assoc_symm_preimage
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
γ : Type u_5
s : Set α
t : Set β
u : Set γ
⊢ (⇑(prodAssoc α β γ).symm : (a : α × β × γ) → (α × β) × γ) '' s ×ˢ t ×ˢ u = (s ×ˢ t) ×ˢ u

Tactic:
simpa only [Equiv.image_eq_preimage_symm] using prod_assoc_preimage

Premises used: Equiv.image_eq_preimage_symm, Equiv.prod_assoc_preimage
-- 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
s : Set (α × β)
x : (↑s : Type (max u_3 u_4))
⊢ Membership.mem (γ := Set β) {y : β | ((↑x : α × β).1, y) ∈ s} (↑x : α × β).2

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
e : α ≃ β
s : Set α
x : (↑s : Type u_3)
⊢ Membership.mem.{u_4, u_4} (α := β) (γ := Set β) ((⇑e : (a : α) → β) '' s) ((e : (a : α) → β) (↑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
e : α ≃ β
s : Set α
y : (↑((⇑e : (a : α) → β) '' s) : Type u_4)
rcases :
  ∀ (a : α) (m : a ∈ s),
    Membership.mem (α := α) s
      ((e.symm : (a : β) → α)
          ((↑(Subtype.mk (p := fun (x : β) ↦ Membership.mem (γ := Set β) ((⇑e : (a : α) → β) '' s) x)
                  ((e : (a : α) → β) a) ⋯) :
              β) :
            β) :
        α)
⊢ Membership.mem (α := α) s ((e.symm : (a : β) → α) (↑y : β) : α)

Tactic:
rcases y with ⟨-, ⟨a, ⟨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
e : α ≃ β
s : Set α
a : α
m : a ∈ s
⊢ Membership.mem (α := α) s
    ((e.symm : (a : β) → α)
        ((↑(Subtype.mk (p := fun (x : β) ↦ Membership.mem (γ := Set β) ((⇑e : (a : α) → β) '' s) x)
                ((e : (a : α) → β) a) ⋯) :
            β) :
          β) :
      α)

Tactic:
simpa using m
-- 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
e : α ≃ β
s : Set α
x : (↑s : Type u_3)
⊢ (fun (y : (↑((⇑e : (a : α) → β) '' s) : Type u_4)) ↦
        (Subtype.mk (p := fun (x : α) ↦ x ∈ s) ((e.symm : (a : β) → α) (↑y : β)) ⋯ : { x : α // x ∈ s }))
      ((fun (x : (↑s : Type u_3)) ↦
          (Subtype.mk (p := fun (x : β) ↦ Membership.mem (γ := Set β) ((⇑e : (a : α) → β) '' s) x)
              ((e : (a : α) → β) (↑x : α)) ⋯ :
            { x : β // Membership.mem (γ := Set β) ((⇑e : (a : α) → β) '' s) x }))
        x) =
    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
e : α ≃ β
s : Set α
y : (↑((⇑e : (a : α) → β) '' s) : Type u_4)
⊢ (fun (x : (↑s : Type u_3)) ↦
        (Subtype.mk (p := fun (x : β) ↦ Membership.mem (γ := Set β) ((⇑e : (a : α) → β) '' s) x)
            ((e : (a : α) → β) (↑x : α)) ⋯ :
          { x : β // Membership.mem (γ := Set β) ((⇑e : (a : α) → β) '' s) x }))
      ((fun (y : (↑((⇑e : (a : α) → β) '' s) : Type u_4)) ↦
          (Subtype.mk (p := fun (x : α) ↦ x ∈ s) ((e.symm : (a : β) → α) (↑y : β)) ⋯ : { x : α // x ∈ s }))
        y) =
    y

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
e : α ≃ β
s : Set α
hs : Monotone.{u_3, u_4} (α := α) (β := β) (⇑e : (a : α) → β)
⊢ Monotone.{u_3, u_4} (α := (↑s : Type u_3)) (β := (↑((⇑e : (a : α) → β) '' s) : Type u_4))
    (⇑(e.image s) : (a : (↑s : Type u_3)) → (↑((⇑e : (a : α) → β) '' s) : Type u_4))

Tactic:
hs.comp (Subtype.mono_coe _)

Premises used: Monotone, Monotone.comp, Subtype.mono_coe
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
e : α ≃ β
s : Set α
hs : Antitone.{u_3, u_4} (α := α) (β := β) (⇑e : (a : α) → β)
⊢ Antitone.{u_3, u_4} (α := (↑s : Type u_3)) (β := (↑((⇑e : (a : α) → β) '' s) : Type u_4))
    (⇑(e.image s) : (a : (↑s : Type u_3)) → (↑((⇑e : (a : α) → β) '' s) : Type u_4))

Tactic:
hs.comp_monotone (Subtype.mono_coe _)

Premises used: Antitone.comp_monotone, Subtype.mono_coe, Antitone
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
e : α ≃ β
s : Set α
hs : StrictMono.{u_3, u_4} (α := α) (β := β) (⇑e : (a : α) → β)
⊢ StrictMono.{u_3, u_4} (α := (↑s : Type u_3)) (β := (↑((⇑e : (a : α) → β) '' s) : Type u_4))
    (⇑(e.image s) : (a : (↑s : Type u_3)) → (↑((⇑e : (a : α) → β) '' s) : Type u_4))

Tactic:
hs.comp (Subtype.strictMono_coe _)

Premises used: StrictMono, StrictMono.comp, Subtype.strictMono_coe
-- Module: Mathlib.Logic.Equiv.Set
Goal:
α : Type u_3
β : Type u_4
inst : Preorder α
inst_1 : Preorder β
e : α ≃ β
s : Set α
hs : StrictAnti.{u_3, u_4} (α := α) (β := β) (⇑e : (a : α) → β)
⊢ StrictAnti.{u_3, u_4} (α := (↑s : Type u_3)) (β := (↑((⇑e : (a : α) → β) '' s) : Type u_4))
    (⇑(e.image s) : (a : (↑s : Type u_3)) → (↑((⇑e : (a : α) → β) '' s) : Type u_4))

Tactic:
hs.comp_strictMono (Subtype.strictMono_coe _)

Premises used: StrictAnti.comp_strictMono, StrictAnti, Subtype.strictMono_coe