awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
h' : e'.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e : α → β) (↑e' : α → β) (e.source ∩ s)
rw : (↑e : α → β) '' (e.source ∩ s) = e'.target ∩ t
rw₁ : (↑e : α → β) '' (e.source ∩ s) = (↑e' : α → β) '' (e'.source ∩ s)
rw₂ : (↑e : α → β) '' (e.source ∩ s) = (↑e' : α → β) '' (e.source ∩ s)
rw₃ rw₄ : (↑e' : α → β) '' (e.source ∩ s) = (↑e' : α → β) '' (e.source ∩ s)
⊢ e.target ∩ t = e'.target ∩ t

Tactic:
rw [← h.image_eq, ← h'.image_eq, ← hs, heq.image_eq]

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

Tactic:
rw [← h.image_eq]

Premises used: PartialEquiv.IsImage.image_eq
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e : α → β) (↑e' : α → β) (e.source ∩ s)
x : α
hx : x ∈ e.source ∩ s
⊢ x ∈ e.source ∩ s

Tactic:
have hx' := hx
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e : α → β) (↑e' : α → β) (e.source ∩ s)
x : α
hx hx' : x ∈ e.source ∩ s
⊢ x ∈ e'.source ∩ s

Tactic:
rw [hs] at hx'
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
h : e.IsImage s t
hs : e.source ∩ s = e'.source ∩ s
heq : EqOn (↑e : α → β) (↑e' : α → β) (e.source ∩ s)
x : α
hx : x ∈ e.source ∩ s
hx' : x ∈ e'.source ∩ s
rw : x = (↑e'.symm : β → α) ((↑e : α → β) x)
rw₁ : x = (↑e'.symm : β → α) ((↑e' : α → β) x)
rw₂ rw₃ : x = x
⊢ (↑e.symm : β → α) ((↑e : α → β) x) = (↑e'.symm : β → α) ((↑e : α → β) x)

Tactic:
rw [e.left_inv hx.1, heq hx, e'.left_inv hx'.1]

Premises used: And.left, PartialEquiv.left_inv
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
x : α
hx : x ∈ e.source
⊢ (↑e : α → β) x ∈ e.target ↔ x ∈ e.source

Tactic:
simp [hx]
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
hs : Disjoint e.source e'.source
ht : Disjoint e.target e'.target
rw : (↑e : α → β) '' ∅ = e.target ∩ e'.target
rw₁ : (↑e : α → β) '' ∅ = ∅
rw₂ rw₃ : Eq.{u_2 + 1} (α := Set β) ∅ ∅
⊢ (↑e : α → β) '' (e.source ∩ e'.source) = e.target ∩ e'.target

Tactic:
rw [hs.inter_eq, ht.inter_eq, image_empty]

Premises used: Disjoint.inter_eq, Set.image_empty
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
rw : (↑e : α → β) '' (s ∩ e.source) = e.target ∩ (↑e.symm : β → α) ⁻¹' s
rw₁ : (↑e.symm : β → α) ⁻¹' s ∩ (↑e : α → β) '' e.source = e.target ∩ (↑e.symm : β → α) ⁻¹' s
rw₂ : (↑e.symm : β → α) ⁻¹' s ∩ e.target = e.target ∩ (↑e.symm : β → α) ⁻¹' s
rw₃ rw₄ : e.target ∩ (↑e.symm : β → α) ⁻¹' s = e.target ∩ (↑e.symm : β → α) ⁻¹' s
⊢ (↑e : α → β) '' (e.source ∩ s) = e.target ∩ (↑e.symm : β → α) ⁻¹' s

Tactic:
rw [inter_comm, e.leftInvOn.image_inter', image_source_eq_target, inter_comm]

Premises used: Set.LeftInvOn.image_inter', PartialEquiv.image_source_eq_target, Set.inter_comm, PartialEquiv.leftInvOn
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
rw : (↑e : α → β) '' (s ∩ e.source) = e.target ∩ (↑e.symm : β → α) ⁻¹' (s ∩ e.source)
rw₁ : (↑e.symm : β → α) ⁻¹' (s ∩ e.source) ∩ (↑e : α → β) '' e.source = e.target ∩ (↑e.symm : β → α) ⁻¹' (s ∩ e.source)
rw₂ : (↑e.symm : β → α) ⁻¹' (s ∩ e.source) ∩ e.target = e.target ∩ (↑e.symm : β → α) ⁻¹' (s ∩ e.source)
rw₃ rw₄ : e.target ∩ (↑e.symm : β → α) ⁻¹' (s ∩ e.source) = e.target ∩ (↑e.symm : β → α) ⁻¹' (s ∩ e.source)
⊢ (↑e : α → β) '' (e.source ∩ s) = e.target ∩ (↑e.symm : β → α) ⁻¹' (e.source ∩ s)

Tactic:
rw [inter_comm, e.leftInvOn.image_inter, image_source_eq_target, inter_comm]

Premises used: Set.LeftInvOn.image_inter, PartialEquiv.image_source_eq_target, Set.inter_comm, PartialEquiv.leftInvOn
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
h : s ⊆ e.source
rw : (↑e : α → β) '' s = (↑e : α → β) '' (e.source ∩ s)
rw₁ rw₂ : (↑e : α → β) '' s = (↑e : α → β) '' s
⊢ (↑e : α → β) '' s = e.target ∩ (↑e.symm : β → α) ⁻¹' s

Tactic:
rw [← e.image_source_inter_eq', inter_eq_self_of_subset_right h]

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

Tactic:
e.symm.image_eq_target_inter_inv_preimage h

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

Tactic:
e.symm.image_source_inter_eq _

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

Tactic:
e.symm.image_source_inter_eq' _

Premises used: PartialEquiv.symm, PartialEquiv.image_source_inter_eq'
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
x : α
hx : x ∈ e.source
⊢ x ∈ (↑e : α → β) ⁻¹' (↑e.symm : β → α) ⁻¹' s ↔ x ∈ s

Tactic:
simp only [mem_preimage, e.left_inv hx]

Premises used: PartialEquiv.left_inv, Set.mem_preimage
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set β
⊢ e.source ∩ (↑e : α → β) ⁻¹' (e.target ∩ s) = e.source ∩ (↑e : α → β) ⁻¹' s

Tactic:
ext fun _ => ⟨fun hx => ⟨hx.1, hx.2.2⟩, fun hx => ⟨hx.1, e.map_source hx.1, hx.2⟩⟩

Premises used: Set.ext, PartialEquiv.map_source, And.right, And.left, And.intro, Iff.intro
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set β
⊢ e.target ∩ (↑e.symm : β → α) ⁻¹' (↑e : α → β) ⁻¹' s = e.target ∩ s

Tactic:
e.symm.source_inter_preimage_inv_preimage _

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

Tactic:
(e.leftInvOn.mono h).image_image

Premises used: Set.LeftInvOn.mono, PartialEquiv.leftInvOn, Set.LeftInvOn.image_image
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set β
h : s ⊆ e.target
⊢ (↑e : α → β) '' (↑e.symm : β → α) '' s = s

Tactic:
e.symm.symm_image_image_of_subset_source h

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

Tactic:
e.mapsTo

Premises used: Set.Mem, setOf, Set.Subset, Set.preimage, Set.MapsTo, PartialEquiv.mapsTo
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ (↑e.symm : β → α) '' e.target = e.source

Tactic:
e.symm.image_source_eq_target

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

Tactic:
e.symm_mapsTo

Premises used: Set.Mem, setOf, Set.Subset, PartialEquiv.symm_mapsTo, Set.preimage, Set.MapsTo
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), (↑e : α → β) x = (↑e' : α → β) x
hsymm : ∀ (x : β), (↑e.symm : β → α) x = (↑e'.symm : β → α) x
hs : e.source = e'.source
h₁ : ∀ (x : α), (↑e : α → β) x = (↑e' : α → β) x
⊢ (↑e : α → β) = (↑e' : α → β)

Tactic:
ext x
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), (↑e : α → β) x = (↑e' : α → β) x
hsymm : ∀ (x : β), (↑e.symm : β → α) x = (↑e'.symm : β → α) x
hs : e.source = e'.source
x : α
⊢ (↑e : α → β) x = (↑e' : α → β) x

Tactic:
h x
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), (↑e : α → β) x = (↑e' : α → β) x
hsymm : ∀ (x : β), (↑e.symm : β → α) x = (↑e'.symm : β → α) x
hs : e.source = e'.source
x : α
⊢ (↑e : α → β) x = (↑e' : α → β) x

Tactic:
exact h x
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), (↑e : α → β) x = (↑e' : α → β) x
hsymm : ∀ (x : β), (↑e.symm : β → α) x = (↑e'.symm : β → α) x
hs : e.source = e'.source
⊢ (↑e : α → β) = (↑e' : α → β)

Tactic:
have A : (e : α → β) = e' := by
    ext x
    exact h x
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), (↑e : α → β) x = (↑e' : α → β) x
hsymm : ∀ (x : β), (↑e.symm : β → α) x = (↑e'.symm : β → α) x
hs : e.source = e'.source
A : (↑e : α → β) = (↑e' : α → β)
h₁ : ∀ (x : β), (↑e.symm : β → α) x = (↑e'.symm : β → α) x
⊢ (↑e.symm : β → α) = (↑e'.symm : β → α)

Tactic:
ext x
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), (↑e : α → β) x = (↑e' : α → β) x
hsymm : ∀ (x : β), (↑e.symm : β → α) x = (↑e'.symm : β → α) x
hs : e.source = e'.source
A : (↑e : α → β) = (↑e' : α → β)
x : β
⊢ (↑e.symm : β → α) x = (↑e'.symm : β → α) x

Tactic:
hsymm x
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), (↑e : α → β) x = (↑e' : α → β) x
hsymm : ∀ (x : β), (↑e.symm : β → α) x = (↑e'.symm : β → α) x
hs : e.source = e'.source
A : (↑e : α → β) = (↑e' : α → β)
x : β
⊢ (↑e.symm : β → α) x = (↑e'.symm : β → α) x

Tactic:
exact hsymm x
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), (↑e : α → β) x = (↑e' : α → β) x
hsymm : ∀ (x : β), (↑e.symm : β → α) x = (↑e'.symm : β → α) x
hs : e.source = e'.source
A : (↑e : α → β) = (↑e' : α → β)
⊢ (↑e.symm : β → α) = (↑e'.symm : β → α)

Tactic:
have B : (e.symm : β → α) = e'.symm := by
    ext x
    exact hsymm x
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), (↑e : α → β) x = (↑e' : α → β) x
hsymm : ∀ (x : β), (↑e.symm : β → α) x = (↑e'.symm : β → α) x
hs : e.source = e'.source
A : (↑e : α → β) = (↑e' : α → β)
B : (↑e.symm : β → α) = (↑e'.symm : β → α)
⊢ (↑e : α → β) '' e.source = e.target

Tactic:
have I : e '' e.source = e.target := e.image_source_eq_target
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), (↑e : α → β) x = (↑e' : α → β) x
hsymm : ∀ (x : β), (↑e.symm : β → α) x = (↑e'.symm : β → α) x
hs : e.source = e'.source
A : (↑e : α → β) = (↑e' : α → β)
B : (↑e.symm : β → α) = (↑e'.symm : β → α)
I : (↑e : α → β) '' e.source = e.target
⊢ (↑e' : α → β) '' e'.source = e'.target

Tactic:
have I' : e' '' e'.source = e'.target := e'.image_source_eq_target
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), (↑e : α → β) x = (↑e' : α → β) x
hsymm : ∀ (x : β), (↑e.symm : β → α) x = (↑e'.symm : β → α) x
hs : e.source = e'.source
A : (↑e : α → β) = (↑e' : α → β)
B : (↑e.symm : β → α) = (↑e'.symm : β → α)
I : (↑e : α → β) '' e.source = e.target
I' : (↑e' : α → β) '' e'.source = e'.target
⊢ e'.target = e.target

Tactic:
rw [A, hs, I'] at I
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), (↑e : α → β) x = (↑e' : α → β) x
hsymm : ∀ (x : β), (↑e.symm : β → α) x = (↑e'.symm : β → α) x
hs : e.source = e'.source
A : (↑e : α → β) = (↑e' : α → β)
B : (↑e.symm : β → α) = (↑e'.symm : β → α)
I : (↑e : α → β) '' e.source = e.target
I' : (↑e' : α → β) '' e'.source = e'.target
I₁ : e'.target = e.target
⊢ (↑e' : α → β) '' e'.source = e'.target

Tactic:
rw [A, hs, I'] at I
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : ∀ (x : α), (↑e : α → β) x = (↑e' : α → β) x
hsymm : ∀ (x : β), (↑e.symm : β → α) x = (↑e'.symm : β → α) x
hs : e.source = e'.source
A : (↑e : α → β) = (↑e' : α → β)
B : (↑e.symm : β → α) = (↑e'.symm : β → α)
I : e'.target = e.target
I' : (↑e' : α → β) '' e'.source = e'.target
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)
    (h :
      ∀ (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 α β } :
              α → β)
            x =
          (↑e' : α → β) x)
    (hsymm :
      ∀ (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 α β }.symm :
              β → α)
            x =
          (↑e'.symm : β → α) x)
    (hs :
      { 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 =
        e'.source)
    (A :
      (↑{ 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 α β } :
          α → β) =
        (↑e' : α → β))
    (B :
      (↑{ 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 :
          β → α) =
        (↑e'.symm : β → α))
    (I :
      e'.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' : 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' : PartialEquiv α β } =
      e'
⊢ e = e'

Tactic:
cases e
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
⊢ (↑(e.restr s) : α → β) = (↑e : α → β)

Tactic:
rfl

Premises used: setOf, Set.inter, rfl
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
⊢ (↑(e.restr s).symm : β → α) = (↑e.symm : β → α)

Tactic:
rfl

Premises used: PartialEquiv.restr, setOf, Set.inter, PartialEquiv.IsImage.restr, rfl
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
⊢ (e.restr s).source = e.source ∩ s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
⊢ (e.restr s).source ⊆ e.source

Tactic:
inter_subset_left

Premises used: Set.inter_subset_left
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
⊢ (e.restr s).target = e.target ∩ (↑e.symm : β → α) ⁻¹' s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
h : e.source ⊆ s
⊢ (e.restr s).source = e.source

Tactic:
simp [inter_eq_self_of_subset_left h]

Premises used: Set.inter_eq_self_of_subset_left
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ e.restr univ = e

Tactic:
restr_eq_of_source_subset (subset_univ _)

Premises used: PartialEquiv.restr_eq_of_source_subset, Set.subset_univ
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
⊢ (PartialEquiv.refl α).source = univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
⊢ (PartialEquiv.refl α).target = univ

Tactic:
rfl

Premises used: Set.univ, setOf, rfl
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
⊢ (↑(PartialEquiv.refl α) : α → α) = id

Tactic:
rfl

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

Tactic:
rfl

Premises used: Equiv.toPartialEquivOfImageEq, Set.univ, setOf, PartialEquiv.symm, Equiv.toPartialEquiv, PartialEquiv.refl, rfl
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
s : Set α
⊢ ((PartialEquiv.refl α).restr s).source = s

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
s : Set α
⊢ ((PartialEquiv.refl α).restr s).target = s

Tactic:
simp
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
s : Set α
⊢ (ofSet s).source = s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
s : Set α
⊢ (ofSet s).target = s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
s : Set α
⊢ (↑(ofSet s) : α → α) = id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
s : Set α
⊢ (ofSet s).symm = ofSet s

Tactic:
rfl

Premises used: PartialEquiv.ofSet, PartialEquiv.symm, rfl
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv β γ
a : α
b : β
a' : α
ha' : Membership.mem (γ := Set α) {a} a'
rw : const β a (const α b a) = a
rw₁ rw₂ : a = a
⊢ const β a (const α b a') = a'

Tactic:
rw [eq_of_mem_singleton ha', const_apply]

Premises used: Function.const_apply, Set.eq_of_mem_singleton
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv β γ
a : α
b b' : β
hb' : Membership.mem (γ := Set β) {b} b'
rw : const α b (const β a b) = b
rw₁ rw₂ : b = b
⊢ const α b (const β a b') = b'

Tactic:
rw [eq_of_mem_singleton hb', const_apply]

Premises used: Function.const_apply, Set.eq_of_mem_singleton
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e'_1 e' : PartialEquiv β γ
h : e.target = e'.source
x : α
hx : x ∈ e.source
⊢ ((↑e' : β → γ) ∘ (↑e : α → β)) x ∈ e'.target

Tactic:
simp [← h, hx]
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e'_1 e' : PartialEquiv β γ
h : e.target = e'.source
y : γ
hy : y ∈ e'.target
⊢ ((↑e.symm : β → α) ∘ (↑e'.symm : γ → β)) y ∈ e.source

Tactic:
simp [h, hy]
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e'_1 e' : PartialEquiv β γ
h : e.target = e'.source
x : α
hx : x ∈ e.source
⊢ ((↑e.symm : β → α) ∘ (↑e'.symm : γ → β)) (((↑e' : β → γ) ∘ (↑e : α → β)) x) = x

Tactic:
simp [hx, ← h]
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e'_1 e' : PartialEquiv β γ
h : e.target = e'.source
y : γ
hy : y ∈ e'.target
⊢ ((↑e' : β → γ) ∘ (↑e : α → β)) (((↑e.symm : β → α) ∘ (↑e'.symm : γ → β)) y) = y

Tactic:
simp [hy, h]
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e : PartialEquiv α β
e' : PartialEquiv β γ
⊢ (↑(e.trans e') : α → γ) = (↑e' : β → γ) ∘ (↑e : α → β)

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e : PartialEquiv α β
e' : PartialEquiv β γ
x : α
⊢ (↑(e.trans e') : α → γ) x = (↑e' : β → γ) ((↑e : α → β) x)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e : PartialEquiv α β
e' : PartialEquiv β γ
⊢ (e.trans e').symm = e'.symm.trans e.symm

Tactic:
rfl

Premises used: PartialEquiv.trans, PartialEquiv.symm, PartialEquiv.trans', rfl
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e : PartialEquiv α β
e' : PartialEquiv β γ
⊢ (e.trans e').source = e.source ∩ (↑e : α → β) ⁻¹' e'.source

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e : PartialEquiv α β
e' : PartialEquiv β γ
h h₁ h₂ h₃ : ∀ (my_y : α), my_y ∈ (e.trans e').source ↔ my_y ∈ e.source ∩ (↑e : α → β) ⁻¹' (e.target ∩ e'.source)
⊢ (e.trans e').source = e.source ∩ (↑e : α → β) ⁻¹' (e.target ∩ e'.source)

Tactic:
mfld_set_tac
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e : PartialEquiv α β
e' : PartialEquiv β γ
rw : e.source ∩ (↑e : α → β) ⁻¹' (e.target ∩ e'.source) = (↑e.symm : β → α) '' (e.target ∩ e'.source)
rw₁ rw₂ : e.source ∩ (↑e : α → β) ⁻¹' (e.target ∩ e'.source) = e.source ∩ (↑e : α → β) ⁻¹' (e.target ∩ e'.source)
⊢ (e.trans e').source = (↑e.symm : β → α) '' (e.target ∩ e'.source)

Tactic:
rw [e.trans_source', e.symm_image_target_inter_eq]

Premises used: PartialEquiv.symm_image_target_inter_eq, PartialEquiv.trans_source'
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e : PartialEquiv α β
e' : PartialEquiv β γ
⊢ (↑e : α → β) '' (e.trans e').source = e.target ∩ e'.source

Tactic:
(e.symm.restr e'.source).symm.image_source_eq_target

Premises used: PartialEquiv.restr, setOf, PartialEquiv.image_source_eq_target, PartialEquiv.symm, Set.inter, PartialEquiv.source
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e : PartialEquiv α β
e' : PartialEquiv β γ
⊢ (e.trans e').target = e'.target ∩ (↑e'.symm : γ → β) ⁻¹' e.target

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e : PartialEquiv α β
e' : PartialEquiv β γ
⊢ (e.trans e').target = e'.target ∩ (↑e'.symm : γ → β) ⁻¹' (e'.source ∩ e.target)

Tactic:
trans_source' e'.symm e.symm

Premises used: PartialEquiv.symm, PartialEquiv.trans_source'
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e : PartialEquiv α β
e' : PartialEquiv β γ
⊢ (e.trans e').target = (↑e' : β → γ) '' (e'.source ∩ e.target)

Tactic:
trans_source'' e'.symm e.symm

Premises used: PartialEquiv.trans_source'', PartialEquiv.symm
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e : PartialEquiv α β
e' : PartialEquiv β γ
⊢ (↑e'.symm : γ → β) '' (e.trans e').target = e'.source ∩ e.target

Tactic:
image_trans_source e'.symm e.symm

Premises used: PartialEquiv.image_trans_source, PartialEquiv.symm
-- Module: Mathlib.Logic.Equiv.PartialEquiv
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv β γ
e'' : PartialEquiv γ δ
⊢ ((e.trans e').trans e'').source = (e.trans (e'.trans e'')).source

Tactic:
simp [trans_source, @preimage_comp α β γ, inter_assoc]

Premises used: PartialEquiv.trans_source, Set.preimage_comp, Set.inter_assoc