awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq α_1
a b : α_1
α : Type w
o : Option α
none :
  Eq.{w + 1} (α := Option α)
    ((fun (s : α ⊕ PUnit) ↦ Sum.elim Option.some (fun (x : PUnit.{v + 1}) ↦ Option.none) s)
      ((fun (o : Option α) ↦ o.elim (inr PUnit.unit) inl) Option.none))
    Option.none
some :
  ∀ (val : α),
    (fun (s : α ⊕ PUnit) ↦ Sum.elim Option.some (fun (x : PUnit.{v + 1}) ↦ Option.none) s)
        ((fun (o : Option α) ↦ o.elim (inr PUnit.unit) inl) (Option.some val)) =
      Option.some val
⊢ (fun (s : α ⊕ PUnit) ↦ Sum.elim Option.some (fun (x : PUnit.{v + 1}) ↦ Option.none) s)
      ((fun (o : Option α) ↦ o.elim (inr PUnit.unit) inl) o) =
    o

Tactic:
cases o
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq α_1
a b : α_1
α : Type w
⊢ Eq.{w + 1} (α := Option α)
    ((fun (s : α ⊕ PUnit) ↦ Sum.elim some (fun (x : PUnit.{v + 1}) ↦ none) s)
      ((fun (o : Option α) ↦ o.elim (inr PUnit.unit) inl) none))
    none

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq α_1
a b : α_1
α : Type w
val : α
⊢ (fun (s : α ⊕ PUnit) ↦ Sum.elim some (fun (x : PUnit.{v + 1}) ↦ none) s)
      ((fun (o : Option α) ↦ o.elim (inr PUnit.unit) inl) (some val)) =
    some val

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq α_1
a b : α_1
α : Type w
s : α ⊕ PUnit
inl :
  ∀ (val : α),
    Eq (α := α ⊕ PUnit)
      ((fun (o : Option α) ↦ o.elim (Sum.inr PUnit.unit) Sum.inl)
        ((fun (s : α ⊕ PUnit) ↦ Sum.elim some (fun (x : PUnit.{v + 1}) ↦ none) s) (Sum.inl val)))
      (Sum.inl val)
inr :
  Eq (α := α ⊕ PUnit)
    ((fun (o : Option α) ↦ o.elim (Sum.inr PUnit.unit) Sum.inl)
      ((fun (s : α ⊕ PUnit) ↦ Sum.elim some (fun (x : PUnit.{v + 1}) ↦ none) s) (Sum.inr PUnit.unit)))
    (Sum.inr PUnit.unit)
⊢ (fun (o : Option α) ↦ o.elim (Sum.inr PUnit.unit) Sum.inl)
      ((fun (s : α ⊕ PUnit) ↦ Sum.elim some (fun (x : PUnit.{v + 1}) ↦ none) s) s) =
    s

Tactic:
rcases s with (_ | ⟨⟨⟩⟩)
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq α_1
a b : α_1
α : Type w
val : α
⊢ Eq (α := α ⊕ PUnit)
    ((fun (o : Option α) ↦ o.elim (inr PUnit.unit) inl)
      ((fun (s : α ⊕ PUnit) ↦ Sum.elim some (fun (x : PUnit.{v + 1}) ↦ none) s) (inl val)))
    (inl val)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α_1 : Type u_1
β : Type u_2
γ : Type u_3
inst : DecidableEq α_1
a b : α_1
α : Type w
⊢ Eq (α := α ⊕ PUnit)
    ((fun (o : Option α) ↦ o.elim (inr PUnit.unit) inl)
      ((fun (s : α ⊕ PUnit) ↦ Sum.elim some (fun (x : PUnit.{v + 1}) ↦ none) s) (inr PUnit.unit)))
    (inr PUnit.unit)

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_4
⊢ Eq (α := α ⊕ PUnit) ((optionEquivSumPUnit α : (a : Option α) → α ⊕ PUnit) none : α ⊕ PUnit)
    (inr PUnit.unit : α ⊕ PUnit)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_4
a : α
⊢ Eq (α := α ⊕ PUnit) ((optionEquivSumPUnit α : (a : Option α) → α ⊕ PUnit) (some a) : α ⊕ PUnit) (inl a : α ⊕ PUnit)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_4
a : α
⊢ ((optionEquivSumPUnit α).symm : (a : α ⊕ PUnit) → Option α) (inl a) = some a

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Logic.Equiv.Option
Goal:
α : Type u_4
a : PUnit
⊢ Eq.{u_4 + 1} (α := Option α) (((optionEquivSumPUnit α).symm : (a : α ⊕ PUnit) → Option α) (inr a) : Option α)
    (none : Option α)

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Logic.Equiv.Pairwise
Goal:
X : Type u_1
Y : Type u_2
F : Sort u_3
inst : FunLike F Y X
inst_1 : EmbeddingLike F Y X
f : F
p : X → X → Prop
h : Pairwise p
⊢ Pairwise.{u_2} (α := Y) (p on (⇑f : (a : Y) → X))

Tactic:
h.comp_of_injective <| EmbeddingLike.injective f

Premises used: Pairwise.comp_of_injective, EmbeddingLike.injective
-- Module: Mathlib.Logic.Equiv.Pairwise
Goal:
X : Type u_1
Y : Type u_2
F : Sort u_3
inst : EquivLike F Y X
f : F
p : X → X → Prop
⊢ Pairwise.{u_2} (α := Y) (p on (⇑f : (a : Y) → X)) ↔ Pairwise p

Tactic:
(EquivLike.bijective f).pairwise_comp_iff

Premises used: EquivLike.bijective, Function.Bijective.pairwise_comp_iff
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
t : Set β
ml : ∀ ⦃x : α⦄, x ∈ s → f x ∈ t
mr : ∀ ⦃x : β⦄, x ∈ t → g x ∈ s
il : ∀ ⦃x : α⦄, x ∈ s → g (f x) = x
ir : ∀ ⦃x : β⦄, x ∈ t → f (g x) = x
⊢ (↑{ toFun := f, invFun := g, source := s, target := t, map_source' := ml, map_target' := mr, left_inv' := il,
          right_inv' := ir : PartialEquiv α β } :
      α → β) =
    f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
f : α → β
g : β → α
s : Set α
t : Set β
ml : ∀ ⦃x : α⦄, x ∈ s → f x ∈ t
mr : ∀ ⦃x : β⦄, x ∈ t → g x ∈ s
il : ∀ ⦃x : α⦄, x ∈ s → g (f x) = x
ir : ∀ ⦃x : β⦄, x ∈ t → f (g x) = x
⊢ (↑{ toFun := f, invFun := g, source := s, target := t, map_source' := ml, map_target' := mr, left_inv' := il,
            right_inv' := ir : PartialEquiv α β }.symm :
      β → α) =
    g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ e.invFun = (↑e.symm : β → α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
x : α
h : x ∈ e.source
⊢ (↑e : α → β) x ∈ e.target

Tactic:
e.map_source' h

Premises used: PartialEquiv.map_source'
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ (↑e : α → β) '' e.source ⊆ e.target

Tactic:
fun _ ⟨_, hx, hex⟩ ↦ mem_of_eq_of_mem (id hex.symm) (e.map_source' hx)

Premises used: PartialEquiv.map_source', PartialEquiv.target, _private.0.PartialEquiv.map_source''.match_1, Membership.mem, id, Set.Subset, Set.mem_of_eq_of_mem, Eq.symm
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
x : β
h : x ∈ e.target
⊢ (↑e.symm : β → α) x ∈ e.source

Tactic:
e.map_target' h

Premises used: Set.Mem, PartialEquiv.map_target'
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
x : α
h : x ∈ e.source
⊢ (↑e.symm : β → α) ((↑e : α → β) x) = x

Tactic:
e.left_inv' h

Premises used: PartialEquiv.left_inv'
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
x : β
h : x ∈ e.target
⊢ (↑e : α → β) ((↑e.symm : β → α) x) = x

Tactic:
e.right_inv' h

Premises used: PartialEquiv.right_inv'
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ e.target ⊆ range (↑e : α → β)

Tactic:
fun x hx ↦ ⟨e.symm x, right_inv e hx⟩

Premises used: Set.Mem, setOf, PartialEquiv.symm, PartialEquiv.right_inv, Set.Subset, Exists.intro, Set.range, PartialEquiv.toFun
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
x : α
y : β
hx : x ∈ e.source
hy : y ∈ e.target
h : x = (↑e.symm : β → α) y
rw : (↑e : α → β) x = (↑e : α → β) ((↑e.symm : β → α) y)
rw₁ rw₂ : (↑e : α → β) ((↑e.symm : β → α) y) = (↑e : α → β) ((↑e.symm : β → α) y)
⊢ (↑e : α → β) x = y

Tactic:
rw [← e.right_inv hy, h]

Premises used: PartialEquiv.right_inv
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
x : α
y : β
hx : x ∈ e.source
hy : y ∈ e.target
h : (↑e : α → β) x = y
rw : (↑e.symm : β → α) ((↑e : α → β) x) = (↑e.symm : β → α) y
rw₁ rw₂ : (↑e.symm : β → α) y = (↑e.symm : β → α) y
⊢ x = (↑e.symm : β → α) y

Tactic:
rw [← e.left_inv hx, h]

Premises used: PartialEquiv.left_inv
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ MapsTo (↑e : α → β) e.source e.target

Tactic:
fun _ => e.map_source

Premises used: PartialEquiv.map_source, Set.MapsTo
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ MapsTo (↑e.symm : β → α) e.target e.source

Tactic:
e.symm.mapsTo

Premises used: PartialEquiv.symm, PartialEquiv.mapsTo
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ LeftInvOn (↑e.symm : β → α) (↑e : α → β) e.source

Tactic:
fun _ => e.left_inv

Premises used: Set.LeftInvOn, PartialEquiv.left_inv
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ RightInvOn (↑e.symm : β → α) (↑e : α → β) e.target

Tactic:
fun _ => e.right_inv

Premises used: Set.LeftInvOn, PartialEquiv.right_inv
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ InvOn (↑e.symm : β → α) (↑e : α → β) e.source e.target

Tactic:
⟨e.leftInvOn, e.rightInvOn⟩

Premises used: Set.InvOn, And.intro, PartialEquiv.leftInvOn, PartialEquiv.rightInvOn
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ InjOn (↑e : α → β) e.source

Tactic:
e.leftInvOn.injOn

Premises used: PartialEquiv.leftInvOn, Set.LeftInvOn.injOn
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ BijOn (↑e : α → β) e.source e.target

Tactic:
e.invOn.bijOn e.mapsTo e.symm_mapsTo

Premises used: PartialEquiv.symm_mapsTo, PartialEquiv.mapsTo, PartialEquiv.invOn, Set.InvOn.bijOn
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ SurjOn (↑e : α → β) e.source e.target

Tactic:
e.bijOn.surjOn

Premises used: PartialEquiv.bijOn, Set.BijOn.surjOn
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e_1 : PartialEquiv α β
e' : PartialEquiv β γ
e : α ≃ β
s : Set α
t : Set β
h : (⇑e : (a : α) → β) '' s = t
x : β
hx : x ∈ t
⊢ Membership.mem (γ := Set β) ((⇑e : (a : α) → β) '' s) x

Tactic:
subst t
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e_1 : PartialEquiv α β
e' : PartialEquiv β γ
e : α ≃ β
s : Set α
x : β
hx : Membership.mem (γ := Set β) ((⇑e : (a : α) → β) '' s) x
rcases : ∀ (x : α) (hx : x ∈ s), Membership.mem (α := α) s ((e.symm : (a : β) → α) ((e : (a : α) → β) x : β) : α)
⊢ Membership.mem (α := α) s ((e.symm : (a : β) → α) x : α)

Tactic:
rcases hx with ⟨x, hx, rfl⟩

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e_1 : PartialEquiv α β
e' : PartialEquiv β γ
e : α ≃ β
s : Set α
x : α
hx rwa rwa₁ rwa₂ rwa₃ : x ∈ s
⊢ Membership.mem (α := α) s ((e.symm : (a : β) → α) ((e : (a : α) → β) x : β) : α)

Tactic:
rwa [e.symm_apply_apply]

Premises used: Equiv.symm_apply_apply
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e_1 : PartialEquiv α β
e' : PartialEquiv β γ
e : α ≃ β
rw : Eq.{u_2 + 1} (α := Set β) (range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β)) univ
rw₁ rw₂ : Eq.{u_2 + 1} (α := Set β) univ univ
⊢ Eq.{u_2 + 1} (α := Set β) (image.{u_1, u_2} (α := α) (⇑e : (a : α) → β) univ) univ

Tactic:
rw [image_univ, e.surjective.range_eq]

Premises used: Set.image_univ, Function.Surjective.range_eq, Equiv.surjective
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
f : α → β
hf : (↑e : α → β) = f
g : β → α
hg : (↑e.symm : β → α) = g
s : Set α
hs : e.source = s
t : Set β
ht : e.target = t
substs : e.copy (↑e : α → β) ⋯ (↑e.symm : β → α) ⋯ e.source ⋯ e.target ⋯ = e
⊢ e.copy f hf g hg s hs t ht = e

Tactic:
substs f g s t
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
mk :
  ∀ (toFun : α → β) (invFun : β → α) (source : Set α) (target : Set β)
    (map_source' : ∀ ⦃x : α⦄, x ∈ source → toFun x ∈ target) (map_target' : ∀ ⦃x : β⦄, x ∈ target → invFun x ∈ source)
    (left_inv' : ∀ ⦃x : α⦄, x ∈ source → invFun (toFun x) = x)
    (right_inv' : ∀ ⦃x : β⦄, x ∈ target → toFun (invFun x) = x),
    { toFun := toFun, invFun := invFun, source := source, target := target, map_source' := map_source',
            map_target' := map_target', left_inv' := left_inv', right_inv' := right_inv' : PartialEquiv α β }.copy
        (↑{ toFun := toFun, invFun := invFun, source := source, target := target, map_source' := map_source',
              map_target' := map_target', left_inv' := left_inv', right_inv' := right_inv' : PartialEquiv α β } :
          α → β)
        ⋯
        (↑{ toFun := toFun, invFun := invFun, source := source, target := target, map_source' := map_source',
                map_target' := map_target', left_inv' := left_inv', right_inv' := right_inv' : PartialEquiv α β }.symm :
          β → α)
        ⋯
        { toFun := toFun, invFun := invFun, source := source, target := target, map_source' := map_source',
            map_target' := map_target', left_inv' := left_inv', right_inv' := right_inv' : PartialEquiv α β }.source
        ⋯
        { toFun := toFun, invFun := invFun, source := source, target := target, map_source' := map_source',
            map_target' := map_target', left_inv' := left_inv', right_inv' := right_inv' : PartialEquiv α β }.target
        ⋯ =
      { toFun := toFun, invFun := invFun, source := source, target := target, map_source' := map_source',
        map_target' := map_target', left_inv' := left_inv', right_inv' := right_inv' }
⊢ e.copy (↑e : α → β) ⋯ (↑e.symm : β → α) ⋯ e.source ⋯ e.target ⋯ = e

Tactic:
cases e
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
toFun : α → β
invFun : β → α
source : Set α
target : Set β
map_source' : ∀ ⦃x : α⦄, x ∈ source → toFun x ∈ target
map_target' : ∀ ⦃x : β⦄, x ∈ target → invFun x ∈ source
left_inv' : ∀ ⦃x : α⦄, x ∈ source → invFun (toFun x) = x
right_inv' : ∀ ⦃x : β⦄, x ∈ target → toFun (invFun x) = x
⊢ { toFun := toFun, invFun := invFun, source := source, target := target, map_source' := map_source',
          map_target' := map_target', left_inv' := left_inv', right_inv' := right_inv' : PartialEquiv α β }.copy
      (↑{ toFun := toFun, invFun := invFun, source := source, target := target, map_source' := map_source',
            map_target' := map_target', left_inv' := left_inv', right_inv' := right_inv' : PartialEquiv α β } :
        α → β)
      ⋯
      (↑{ toFun := toFun, invFun := invFun, source := source, target := target, map_source' := map_source',
              map_target' := map_target', left_inv' := left_inv', right_inv' := right_inv' : PartialEquiv α β }.symm :
        β → α)
      ⋯
      { toFun := toFun, invFun := invFun, source := source, target := target, map_source' := map_source',
          map_target' := map_target', left_inv' := left_inv', right_inv' := right_inv' : PartialEquiv α β }.source
      ⋯
      { toFun := toFun, invFun := invFun, source := source, target := target, map_source' := map_source',
          map_target' := map_target', left_inv' := left_inv', right_inv' := right_inv' : PartialEquiv α β }.target
      ⋯ =
    { toFun := toFun, invFun := invFun, source := source, target := target, map_source' := map_source',
      map_target' := map_target', left_inv' := left_inv', right_inv' := right_inv' }

Tactic:
rfl
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ e.symm.source = e.target

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ e.symm.target = e.source

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ e.symm.symm = e

Tactic:
rfl

Premises used: PartialEquiv.symm, rfl
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
⊢ Bijective (α := PartialEquiv α β) PartialEquiv.symm

Tactic:
Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Premises used: Iff.mpr, PartialEquiv.symm_symm, Function.bijective_iff_has_inverse, And.intro, Exists.intro
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ (↑e : α → β) '' e.source = e.target

Tactic:
e.bijOn.image_eq

Premises used: PartialEquiv.bijOn, Set.BijOn.image_eq
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
p : β → Prop
rw : (∀ (y : β), y ∈ (↑e : α → β) '' e.source → p y) ↔ ∀ (x : α), x ∈ e.source → p ((↑e : α → β) x)
rw₁ rw₂ : (∀ ⦃x : α⦄, x ∈ e.source → p ((↑e : α → β) x)) ↔ ∀ (x : α), x ∈ e.source → p ((↑e : α → β) x)
⊢ (∀ (y : β), y ∈ e.target → p y) ↔ ∀ (x : α), x ∈ e.source → p ((↑e : α → β) x)

Tactic:
rw [← image_source_eq_target, forall_mem_image]

Premises used: PartialEquiv.image_source_eq_target, Set.forall_mem_image
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
p : β → Prop
rw : (∃ (y : β), y ∈ (↑e : α → β) '' e.source ∧ p y) ↔ ∃ (x : α), x ∈ e.source ∧ p ((↑e : α → β) x)
rw₁ rw₂ : (∃ (x : α), x ∈ e.source ∧ p ((↑e : α → β) x)) ↔ ∃ (x : α), x ∈ e.source ∧ p ((↑e : α → β) x)
⊢ (∃ (y : β), y ∈ e.target ∧ p y) ↔ ∃ (x : α), x ∈ e.source ∧ p ((↑e : α → β) x)

Tactic:
rw [← image_source_eq_target, exists_mem_image]

Premises used: PartialEquiv.image_source_eq_target, Set.exists_mem_image
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
x : α
h : e.IsImage s t
hx : x ∈ e.source
⊢ (↑e : α → β) x ∈ t ↔ x ∈ s

Tactic:
h hx
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
h : e.IsImage s t
x : α
hx : x ∈ e.source
rw : x ∈ s ↔ (↑e : α → β) x ∈ t
rw₁ rw₂ : x ∈ s ↔ x ∈ s
⊢ (↑e.symm : β → α) ((↑e : α → β) x) ∈ s ↔ (↑e : α → β) x ∈ t

Tactic:
rw [e.left_inv hx, h hx]

Premises used: PartialEquiv.left_inv
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
h : e.IsImage s t
⊢ e.symm.IsImage t s

Tactic:
h.symm_apply_mem_iff

Premises used: Set.Mem, PartialEquiv.IsImage, PartialEquiv.IsImage.symm_apply_mem_iff
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
⊢ e.symm.IsImage t s ↔ e.IsImage s t

Tactic:
⟨fun h => h.symm, fun h => h.symm⟩

Premises used: Iff.intro, PartialEquiv.IsImage.symm
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
h : e.IsImage s t
⊢ MapsTo (↑e : α → β) (e.source ∩ s) (e.target ∩ t)

Tactic:
fun _ hx => ⟨e.mapsTo hx.1, (h hx.1).2 hx.2⟩

Premises used: Iff.mpr, Set.Mem, setOf, Set.inter, And.right, And.left, Set.MapsTo, And.intro, PartialEquiv.mapsTo
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
h : e.IsImage s t
⊢ MapsTo (↑e.symm : β → α) (e.target ∩ t) (e.source ∩ s)

Tactic:
h.symm.mapsTo

Premises used: PartialEquiv.IsImage.mapsTo, PartialEquiv.IsImage.symm
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
h : e.IsImage s t
⊢ (↑e : α → β) '' (e.source ∩ s) = e.target ∩ t

Tactic:
h.restr.image_source_eq_target

Premises used: setOf, PartialEquiv.image_source_eq_target, Set.inter, PartialEquiv.IsImage.restr
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
h : e.IsImage s t
⊢ (↑e.symm : β → α) '' (e.target ∩ t) = e.source ∩ s

Tactic:
h.symm.image_eq

Premises used: PartialEquiv.IsImage.image_eq, PartialEquiv.IsImage.symm
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
⊢ e.IsImage s t ↔ e.source ∩ (↑e : α → β) ⁻¹' t = e.source ∩ s

Tactic:
simp only [IsImage, Set.ext_iff, mem_inter_iff, mem_preimage, and_congr_right_iff]

Premises used: Set.mem_inter_iff, and_congr_right_iff, PartialEquiv.IsImage, Set.ext_iff, Set.mem_preimage
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
⊢ e.IsImage s t ↔ e.target ∩ (↑e.symm : β → α) ⁻¹' s = e.target ∩ t

Tactic:
symm_iff.symm.trans iff_preimage_eq

Premises used: PartialEquiv.IsImage.iff_preimage_eq, PartialEquiv.IsImage.symm_iff, Iff.trans, Iff.symm
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
h : (↑e : α → β) '' (e.source ∩ s) = e.target ∩ t
⊢ e.IsImage s t

Tactic:
of_symm_preimage_eq <| Eq.trans (of_symm_preimage_eq rfl).image_eq.symm h

Premises used: PartialEquiv.IsImage.image_eq, Eq.symm, PartialEquiv.IsImage.of_symm_preimage_eq, rfl, Eq.trans
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
h : (↑e.symm : β → α) '' (e.target ∩ t) = e.source ∩ s
⊢ e.IsImage s t

Tactic:
of_preimage_eq <| Eq.trans (iff_preimage_eq.2 rfl).symm_image_eq.symm h

Premises used: Iff.mpr, PartialEquiv.IsImage.iff_preimage_eq, PartialEquiv.IsImage.of_preimage_eq, PartialEquiv.IsImage.symm_image_eq, Eq.symm, rfl, Eq.trans
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
h : e.IsImage s t
⊢ e.IsImage sᶜ tᶜ

Tactic:
fun _ hx => not_congr (h hx)

Premises used: Set.Mem, setOf, PartialEquiv.IsImage, Not, not_congr
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
s' : Set α
t' : Set β
h : e.IsImage s t
h' : e.IsImage s' t'
⊢ e.IsImage (s ∩ s') (t ∩ t')

Tactic:
fun _ hx => and_congr (h hx) (h' hx)

Premises used: Set.Mem, setOf, Set.inter, PartialEquiv.IsImage, and_congr
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
s' : Set α
t' : Set β
h : e.IsImage s t
h' : e.IsImage s' t'
⊢ e.IsImage (s ∪ s') (t ∪ t')

Tactic:
fun _ hx => or_congr (h hx) (h' hx)

Premises used: or_congr, Set.union, Set.Mem, setOf, PartialEquiv.IsImage
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
s' : Set α
t' : Set β
h : e.IsImage s t
h' : e.IsImage s' t'
⊢ e.IsImage (s \ s') (t \ t')

Tactic:
h.inter h'.compl

Premises used: Set.Mem, Set.diff, setOf, PartialEquiv.IsImage.compl, Not, PartialEquiv.IsImage.inter
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
inst : (i : α) → Decidable (i ∈ s)
inst_1 : (i : β) → Decidable (i ∈ t)
h : e.IsImage s t
h' : e'.IsImage s t
x : α
he : x ∈ e.source
hs : x ∈ s
inl : t.piecewise (β := fun (a : β) ↦ α) (↑e.symm : β → α) (↑e'.symm : β → α) ((↑e : α → β) x) = x
inl₁ : (↑e.symm : β → α) ((↑e : α → β) x) = x
inl₂ inl₃ : x = x
⊢ t.piecewise (β := fun (a : β) ↦ α) (↑e.symm : β → α) (↑e'.symm : β → α)
      (s.piecewise (β := fun (a : α) ↦ β) (↑e : α → β) (↑e' : α → β) x) =
    x

Tactic:
rw [piecewise_eq_of_mem _ _ _ hs, piecewise_eq_of_mem _ _ _ ((h he).2 hs), e.left_inv he]

Premises used: Iff.mpr, Set.piecewise_eq_of_mem, PartialEquiv.left_inv
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
inst : (i : α) → Decidable (i ∈ s)
inst_1 : (i : β) → Decidable (i ∈ t)
h : e.IsImage s t
h' : e'.IsImage s t
x : α
he : x ∈ e'.source
hs : ¬x ∈ s
inr : t.piecewise (β := fun (a : β) ↦ α) (↑e.symm : β → α) (↑e'.symm : β → α) ((↑e' : α → β) x) = x
inr₁ : (↑e'.symm : β → α) ((↑e' : α → β) x) = x
inr₂ inr₃ : x = x
⊢ t.piecewise (β := fun (a : β) ↦ α) (↑e.symm : β → α) (↑e'.symm : β → α)
      (s.piecewise (β := fun (a : α) ↦ β) (↑e : α → β) (↑e' : α → β) x) =
    x

Tactic:
rw [piecewise_eq_of_notMem _ _ _ hs, piecewise_eq_of_notMem _ _ _ ((h'.compl he).2 hs),
      e'.left_inv he]

Premises used: Iff.mpr, Set.piecewise_eq_of_notMem, PartialEquiv.IsImage.compl, PartialEquiv.left_inv