ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>x : β<VAR>e : { e // e none = x }<VAR>a : α<VAR>h : ↑e (some a) ≠ x<GOAL>((Equiv.optionSubtype x) e) a = ⟨↑e (some a), h⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>x : β<VAR>e : { e // e none = x }<VAR>a : α<GOAL>↑(((Equiv.optionSubtype x) e) a) = ↑e (some a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>x : β<VAR>e : { e // e none = x }<VAR>b : { y // y ≠ x }<GOAL>some (((Equiv.optionSubtype x) e).symm b) = (↑e).symm ↑b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>x : β<VAR>e : α ≃ { y // y ≠ x }<VAR>a : α<GOAL>↑((Equiv.optionSubtype x).symm e) (some a) = ↑(e a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>x : β<VAR>e : α ≃ { y // y ≠ x }<GOAL>↑((Equiv.optionSubtype x).symm e) none = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq β<VAR>x : β<VAR>e : α ≃ { y // y ≠ x }<VAR>b : { y // y ≠ x }<GOAL>(↑((Equiv.optionSubtype x).symm e)).symm ↑b = some (e.symm b)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<GOAL>∀ (a_1 : Option { y // y ≠ a }), (Equiv.optionSubtypeNe a) a_1 = a_1.casesOn' a Subtype.val
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b : α<GOAL>(Equiv.optionSubtypeNe a).symm b = if h : b = a then none else some ⟨b, h⟩
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<GOAL>(Equiv.optionSubtypeNe a).symm a = none
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b : α<VAR>hba : b ≠ a<GOAL>(Equiv.optionSubtypeNe a).symm b = some ⟨b, hba⟩
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<GOAL>(Equiv.optionSubtypeNe a) none = a
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a : α<VAR>b : { b // b ≠ a }<GOAL>(Equiv.optionSubtypeNe a) (some b) = ↑b
<VAR>p : Fin 0 → Type u<VAR>τ : Type u<GOAL>Function.FromTypes p τ = τ
<VAR>τ : Type u<GOAL>Function.FromTypes ![] τ = τ
<VAR>n : ℕ<VAR>p : Fin (n + 1) → Type u<VAR>τ : Type u<GOAL>Function.FromTypes p τ = (Matrix.vecHead p → Function.FromTypes (Matrix.vecTail p) τ)
<VAR>n : ℕ<VAR>α : Type u<VAR>p : Fin n → Type u<VAR>τ : Type u<GOAL>Function.FromTypes (Matrix.vecCons α p) τ = (α → Function.FromTypes p τ)
<VAR>p : Fin 0 → Type u<VAR>τ : Type u<VAR>a : Function.FromTypes p τ<GOAL>(Function.fromTypes_zero_equiv p τ) a = a
<VAR>p : Fin 0 → Type u<VAR>τ : Type u<VAR>a : Function.FromTypes p τ<GOAL>(Function.fromTypes_zero_equiv p τ).symm a = a
<VAR>τ : Type u<VAR>a : Function.FromTypes ![] τ<GOAL>(Function.fromTypes_nil_equiv τ) a = a
<VAR>τ : Type u<VAR>a : Function.FromTypes ![] τ<GOAL>(Function.fromTypes_nil_equiv τ).symm a = a
<VAR>n : ℕ<VAR>p : Fin (n + 1) → Type u<VAR>τ : Type u<VAR>a : Function.FromTypes p τ<GOAL>(Function.fromTypes_succ_equiv p τ) a = a
<VAR>n : ℕ<VAR>p : Fin (n + 1) → Type u<VAR>τ : Type u<VAR>a : Function.FromTypes p τ<GOAL>(Function.fromTypes_succ_equiv p τ).symm a = a
<VAR>n : ℕ<VAR>α : Type u<VAR>p : Fin n → Type u<VAR>τ : Type u<VAR>a : Function.FromTypes (Matrix.vecCons α p) τ<GOAL>(Function.fromTypes_cons_equiv α p τ) a = a
<VAR>n : ℕ<VAR>α : Type u<VAR>p : Fin n → Type u<VAR>τ : Type u<VAR>a : Function.FromTypes (Matrix.vecCons α p) τ<GOAL>(Function.fromTypes_cons_equiv α p τ).symm a = a
<VAR>p : Fin 0 → Type u<VAR>τ : Type u<VAR>t : τ<GOAL>Function.FromTypes.const p t = t
<VAR>n : ℕ<VAR>p : Fin (n + 1) → Type u<VAR>τ : Type u<VAR>t : τ<GOAL>Function.FromTypes.const p t = fun x => Function.FromTypes.const (Matrix.vecTail p) t
<VAR>n : ℕ<VAR>p : Fin (n + 1) → Type u<VAR>τ : Type u<VAR>t : τ<VAR>x : p 0<GOAL>Function.FromTypes.const p t x = Function.FromTypes.const (Matrix.vecTail p) t
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>φ : M → N<VAR>ψ : N → P<VAR>χ : outParam (M → P)<VAR>self : CompTriple φ ψ χ<GOAL>ψ ∘ φ = χ
<VAR>M : Type u_1<VAR>σ : M → M<VAR>self : CompTriple.IsId σ<GOAL>σ = id
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>φ : M → N<VAR>ψ : N → P<GOAL>CompTriple φ ψ (ψ ∘ φ)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>φ : M → N<VAR>ψ : N → M<VAR>h : Function.RightInverse φ ψ<VAR>χ : M → M<VAR>CompTriple.IsId χ<GOAL>CompTriple φ ψ χ
<VAR>α : Type u_1<GOAL>Function.Injective ULift.down
<VAR>α : Type u_1<VAR>a b : ULift.{u_2, u_1} α<GOAL>a.down = b.down ↔ a = b
<VAR>α : Sort u_1<GOAL>Function.Injective PLift.down
<VAR>α : Sort u_1<VAR>a b : PLift α<GOAL>a.down = b.down ↔ a = b
<VAR>α : Sort u₁<VAR>β : Sort u₂<VAR>φ : Sort u₃<VAR>f : α → β → φ<GOAL>flip f = fun b a => f a b
<VAR>α : Sort u₁<VAR>β : Sort u₂<VAR>φ : α → β → Sort u₃<VAR>f : (x : α) → (y : β) → φ x y<GOAL>Function.swap f = fun y x => f x y
<VAR>α : Sort u₁<VAR>β : Sort u₂<VAR>f : α → β<GOAL>id ∘ f = f
<VAR>α : Sort u₁<VAR>β : Sort u₂<VAR>f : α → β<GOAL>f ∘ id = f
<VAR>α : Sort u₁<VAR>β : Sort u₂<VAR>φ : Sort u₃<VAR>δ : Sort u₄<VAR>f : φ → δ<VAR>g : β → φ<VAR>h : α → β<GOAL>(f ∘ g) ∘ h = f ∘ g ∘ h
<VAR>α : Sort u₁<VAR>β : Sort u₂<VAR>γ : Sort u_1<VAR>f : α → β<VAR>c : γ<GOAL>Function.const β c ∘ f = Function.const α c
<VAR>α : Sort u₁<VAR>β : Sort u₂<VAR>φ : Sort u₃<VAR>f : β → φ<VAR>b : β<GOAL>f ∘ Function.const α b = Function.const α (f b)
<VAR>α : Sort u₁<VAR>β : Sort u₂<VAR>φ : Sort u₃<VAR>g : β → φ<VAR>f : α → β<VAR>hg : Function.Injective g<VAR>hf : Function.Injective f<GOAL>Function.Injective (g ∘ f)
<VAR>α : Sort u₁<VAR>β : Sort u₂<VAR>φ : Sort u₃<VAR>g : β → φ<VAR>f : α → β<VAR>hg : Function.Surjective g<VAR>hf : Function.Surjective f<GOAL>Function.Surjective (g ∘ f)
<VAR>α : Sort u₁<VAR>β : Sort u₂<VAR>φ : Sort u₃<VAR>g : β → φ<VAR>f : α → β<GOAL>Function.Bijective g → Function.Bijective f → Function.Bijective (g ∘ f)
<VAR>α : Sort u₁<VAR>β : Sort u₂<VAR>g : β → α<VAR>f : α → β<GOAL>Function.LeftInverse g f → Function.Injective f
<VAR>α : Sort u₁<VAR>β : Sort u₂<VAR>f : α → β<GOAL>Function.HasLeftInverse f → Function.Injective f
<VAR>α : Sort u₁<VAR>β : Sort u₂<VAR>f : α → β<VAR>g : β → α<VAR>injf : Function.Injective f<VAR>lfg : Function.LeftInverse f g<GOAL>Function.RightInverse f g
<VAR>α : Sort u₁<VAR>β : Sort u₂<VAR>f : α → β<VAR>g : β → α<VAR>h : Function.RightInverse g f<GOAL>Function.Surjective f
<VAR>α : Sort u₁<VAR>β : Sort u₂<VAR>f : α → β<GOAL>Function.HasRightInverse f → Function.Surjective f
<VAR>α : Sort u₁<VAR>β : Sort u₂<VAR>f : α → β<VAR>g : β → α<VAR>surjf : Function.Surjective f<VAR>rfg : Function.RightInverse f g<GOAL>Function.LeftInverse f g
<VAR>α : Sort u₁<GOAL>Function.Surjective id
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>φ : Type u₃<VAR>f : α → β → φ<GOAL>Function.curry (Function.uncurry f) = f
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>φ : Type u₃<VAR>f : α × β → φ<GOAL>Function.uncurry (Function.curry f) = f
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>g : β → α<VAR>f : α → β<VAR>h : Function.LeftInverse g f<GOAL>g ∘ f = id
<VAR>α : Type u₁<VAR>β : Type u₂<VAR>g : β → α<VAR>f : α → β<VAR>h : Function.RightInverse g f<GOAL>f ∘ g = id
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>self : PartialEquiv α β<VAR>x : β<GOAL>x ∈ self.target → self.invFun x ∈ self.source
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>self : PartialEquiv α β<VAR>x : β<GOAL>x ∈ self.target → ↑self (self.invFun x) = x
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>self : PartialEquiv α β<VAR>x : α<GOAL>x ∈ self.source → self.invFun (↑self x) = x
<VAR>α : Type u_5<VAR>β : Type u_6<VAR>self : PartialEquiv α β<VAR>x : α<GOAL>x ∈ self.source → ↑self x ∈ self.target
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>g : β → α<VAR>s : Set α<VAR>t : Set β<VAR>ml : ∀ ⦃x : α⦄, x ∈ s → f x ∈ t<VAR>mr : ∀ ⦃x : β⦄, x ∈ t → g x ∈ s<VAR>il : ∀ ⦃x : α⦄, x ∈ s → g (f x) = x<VAR>ir : ∀ ⦃x : β⦄, x ∈ t → f (g x) = x<GOAL>↑{ toFun := f, invFun := g, source := s, target := t, map_source' := ml, map_target' := mr, left_inv' := il, right_inv' := ir }.symm = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<GOAL>e.invFun = ↑e.symm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>x : α<VAR>h : x ∈ e.source<GOAL>↑e x ∈ e.target
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<GOAL>↑e '' e.source ⊆ e.target
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>x : β<VAR>h : x ∈ e.target<GOAL>↑e.symm x ∈ e.source
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>x : α<VAR>h : x ∈ e.source<GOAL>↑e.symm (↑e x) = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>x : β<VAR>h : x ∈ e.target<GOAL>↑e (↑e.symm x) = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>x : α<VAR>y : β<VAR>hx : x ∈ e.source<VAR>hy : y ∈ e.target<GOAL>x = ↑e.symm y ↔ ↑e x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<GOAL>Set.MapsTo (↑e) e.source e.target
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<GOAL>Set.MapsTo (↑e.symm) e.target e.source
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<GOAL>Set.LeftInvOn (↑e.symm) (↑e) e.source
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<GOAL>Set.RightInvOn (↑e.symm) (↑e) e.target
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<GOAL>Set.InvOn (↑e.symm) (↑e) e.source e.target
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<GOAL>Set.InjOn (↑e) e.source
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<GOAL>Set.BijOn (↑e) e.source e.target
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<GOAL>Set.SurjOn (↑e) e.source e.target
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>s : Set α<VAR>t : Set β<VAR>h : ⇑e '' s = t<GOAL>(e.toPartialEquivOfImageEq s t h).target = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>s : Set α<VAR>t : Set β<VAR>h : ⇑e '' s = t<GOAL>↑(e.toPartialEquivOfImageEq s t h).symm = ⇑e.symm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>s : Set α<VAR>t : Set β<VAR>h : ⇑e '' s = t<GOAL>↑(e.toPartialEquivOfImageEq s t h) = ⇑e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>s : Set α<VAR>t : Set β<VAR>h : ⇑e '' s = t<GOAL>(e.toPartialEquivOfImageEq s t h).source = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<GOAL>↑e.toPartialEquiv.symm = ⇑e.symm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<GOAL>e.toPartialEquiv.source = Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<GOAL>e.toPartialEquiv.target = Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<GOAL>↑e.toPartialEquiv = ⇑e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>f : α → β<VAR>hf : ↑e = f<VAR>g : β → α<VAR>hg : ↑e.symm = g<VAR>s : Set α<VAR>hs : e.source = s<VAR>t : Set β<VAR>ht : e.target = t<GOAL>(e.copy f hf g hg s hs t ht).source = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>f : α → β<VAR>hf : ↑e = f<VAR>g : β → α<VAR>hg : ↑e.symm = g<VAR>s : Set α<VAR>hs : e.source = s<VAR>t : Set β<VAR>ht : e.target = t<GOAL>↑(e.copy f hf g hg s hs t ht).symm = g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>f : α → β<VAR>hf : ↑e = f<VAR>g : β → α<VAR>hg : ↑e.symm = g<VAR>s : Set α<VAR>hs : e.source = s<VAR>t : Set β<VAR>ht : e.target = t<GOAL>(e.copy f hf g hg s hs t ht).target = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>f : α → β<VAR>hf : ↑e = f<VAR>g : β → α<VAR>hg : ↑e.symm = g<VAR>s : Set α<VAR>hs : e.source = s<VAR>t : Set β<VAR>ht : e.target = t<GOAL>↑(e.copy f hf g hg s hs t ht) = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>f : α → β<VAR>hf : ↑e = f<VAR>g : β → α<VAR>hg : ↑e.symm = g<VAR>s : Set α<VAR>hs : e.source = s<VAR>t : Set β<VAR>ht : e.target = t<GOAL>e.copy f hf g hg s hs t ht = e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<GOAL>e.symm.source = e.target
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<GOAL>e.symm.target = e.source
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<GOAL>e.symm.symm = e
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Function.Bijective PartialEquiv.symm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<GOAL>↑e '' e.source = e.target
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>p : β → Prop<GOAL>(∀ y ∈ e.target, p y) ↔ ∀ x ∈ e.source, p (↑e x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>p : β → Prop<GOAL>(∃ y ∈ e.target, p y) ↔ ∃ x ∈ e.source, p (↑e x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set α<VAR>t : Set β<VAR>x : α<VAR>h : e.IsImage s t<VAR>hx : x ∈ e.source<GOAL>↑e x ∈ t ↔ x ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set α<VAR>t : Set β<VAR>h : e.IsImage s t<VAR>y : β<GOAL>y ∈ e.target → (↑e.symm y ∈ s ↔ y ∈ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set α<VAR>t : Set β<VAR>h : e.IsImage s t<GOAL>e.symm.IsImage t s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set α<VAR>t : Set β<GOAL>e.symm.IsImage t s ↔ e.IsImage s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set α<VAR>t : Set β<VAR>h : e.IsImage s t<GOAL>Set.MapsTo (↑e) (e.source ∩ s) (e.target ∩ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set α<VAR>t : Set β<VAR>h : e.IsImage s t<GOAL>Set.MapsTo (↑e.symm) (e.target ∩ t) (e.source ∩ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set α<VAR>t : Set β<VAR>h : e.IsImage s t<GOAL>↑h.restr = ↑e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set α<VAR>t : Set β<VAR>h : e.IsImage s t<GOAL>↑h.restr.symm = ↑e.symm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set α<VAR>t : Set β<VAR>h : e.IsImage s t<GOAL>h.restr.target = e.target ∩ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set α<VAR>t : Set β<VAR>h : e.IsImage s t<GOAL>h.restr.source = e.source ∩ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set α<VAR>t : Set β<VAR>h : e.IsImage s t<GOAL>↑e '' (e.source ∩ s) = e.target ∩ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set α<VAR>t : Set β<VAR>h : e.IsImage s t<GOAL>↑e.symm '' (e.target ∩ t) = e.source ∩ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set α<VAR>t : Set β<GOAL>e.IsImage s t ↔ e.source ∩ ↑e ⁻¹' t = e.source ∩ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set α<VAR>t : Set β<GOAL>e.IsImage s t ↔ e.target ∩ ↑e.symm ⁻¹' s = e.target ∩ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set α<VAR>t : Set β<VAR>h : ↑e '' (e.source ∩ s) = e.target ∩ t<GOAL>e.IsImage s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set α<VAR>t : Set β<VAR>h : ↑e.symm '' (e.target ∩ t) = e.source ∩ s<GOAL>e.IsImage s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set α<VAR>t : Set β<VAR>h : e.IsImage s t<GOAL>e.IsImage sᶜ tᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set α<VAR>t : Set β<VAR>s' : Set α<VAR>t' : Set β<VAR>h : e.IsImage s t<VAR>h' : e.IsImage s' t'<GOAL>e.IsImage (s ∩ s') (t ∩ t')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set α<VAR>t : Set β<VAR>s' : Set α<VAR>t' : Set β<VAR>h : e.IsImage s t<VAR>h' : e.IsImage s' t'<GOAL>e.IsImage (s ∪ s') (t ∪ t')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set α<VAR>t : Set β<VAR>s' : Set α<VAR>t' : Set β<VAR>h : e.IsImage s t<VAR>h' : e.IsImage s' t'<GOAL>e.IsImage (s \ s') (t \ t')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set α<VAR>t : Set β<VAR>e' : PartialEquiv α β<VAR>(i : α) → Decidable (i ∈ s)<VAR>(i : β) → Decidable (i ∈ t)<VAR>h : e.IsImage s t<VAR>h' : e'.IsImage s t<GOAL>Set.LeftInvOn (t.piecewise ↑e.symm ↑e'.symm) (s.piecewise ↑e ↑e') (s.ite e.source e'.source)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set α<VAR>t : Set β<VAR>e' : PartialEquiv α β<VAR>h : e.IsImage s t<VAR>h' : e'.IsImage s t<VAR>hs : e.source ∩ s = e'.source ∩ s<VAR>heq : Set.EqOn (↑e) (↑e') (e.source ∩ s)<GOAL>e.target ∩ t = e'.target ∩ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set α<VAR>t : Set β<VAR>e' : PartialEquiv α β<VAR>h : e.IsImage s t<VAR>hs : e.source ∩ s = e'.source ∩ s<VAR>heq : Set.EqOn (↑e) (↑e') (e.source ∩ s)<GOAL>Set.EqOn (↑e.symm) (↑e'.symm) (e.target ∩ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<GOAL>e.IsImage e.source e.target
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e e' : PartialEquiv α β<VAR>hs : Disjoint e.source e'.source<VAR>ht : Disjoint e.target e'.target<GOAL>e.IsImage e'.source e'.target
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set α<GOAL>↑e '' (e.source ∩ s) = e.target ∩ ↑e.symm ⁻¹' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set α<GOAL>↑e '' (e.source ∩ s) = e.target ∩ ↑e.symm ⁻¹' (e.source ∩ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set α<VAR>h : s ⊆ e.source<GOAL>↑e '' s = e.target ∩ ↑e.symm ⁻¹' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set β<VAR>h : s ⊆ e.target<GOAL>↑e.symm '' s = e.source ∩ ↑e ⁻¹' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set β<GOAL>↑e.symm '' (e.target ∩ s) = e.source ∩ ↑e ⁻¹' (e.target ∩ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set β<GOAL>↑e.symm '' (e.target ∩ s) = e.source ∩ ↑e ⁻¹' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set α<GOAL>e.source ∩ ↑e ⁻¹' (↑e.symm ⁻¹' s) = e.source ∩ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set β<GOAL>e.source ∩ ↑e ⁻¹' (e.target ∩ s) = e.source ∩ ↑e ⁻¹' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set β<GOAL>e.target ∩ ↑e.symm ⁻¹' (↑e ⁻¹' s) = e.target ∩ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set α<VAR>h : s ⊆ e.source<GOAL>↑e.symm '' (↑e '' s) = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set β<VAR>h : s ⊆ e.target<GOAL>↑e '' (↑e.symm '' s) = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<GOAL>e.source ⊆ ↑e ⁻¹' e.target
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<GOAL>↑e.symm '' e.target = e.source
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<GOAL>e.target ⊆ ↑e.symm ⁻¹' e.source
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e e' : PartialEquiv α β<VAR>h : ∀ (x : α), ↑e x = ↑e' x<VAR>hsymm : ∀ (x : β), ↑e.symm x = ↑e'.symm x<VAR>hs : e.source = e'.source<GOAL>e = e'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set α<GOAL>↑(e.restr s) = ↑e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set α<GOAL>↑(e.restr s).symm = ↑e.symm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set α<GOAL>(e.restr s).source = e.source ∩ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set α<GOAL>(e.restr s).target = e.target ∩ ↑e.symm ⁻¹' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set α<VAR>h : e.source ⊆ s<GOAL>e.restr s = e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<GOAL>e.restr Set.univ = e
<VAR>α : Type u_1<GOAL>(PartialEquiv.refl α).source = Set.univ
<VAR>α : Type u_1<GOAL>(PartialEquiv.refl α).target = Set.univ
<VAR>α : Type u_1<GOAL>↑(PartialEquiv.refl α) = id
<VAR>α : Type u_1<GOAL>(PartialEquiv.refl α).symm = PartialEquiv.refl α
<VAR>α : Type u_1<VAR>s : Set α<GOAL>((PartialEquiv.refl α).restr s).source = s
<VAR>α : Type u_1<VAR>s : Set α<GOAL>((PartialEquiv.refl α).restr s).target = s
<VAR>α : Type u_1<VAR>s : Set α<GOAL>(PartialEquiv.ofSet s).source = s
<VAR>α : Type u_1<VAR>s : Set α<GOAL>(PartialEquiv.ofSet s).target = s
<VAR>α : Type u_1<VAR>s : Set α<GOAL>↑(PartialEquiv.ofSet s) = id
<VAR>α : Type u_1<VAR>s : Set α<GOAL>(PartialEquiv.ofSet s).symm = PartialEquiv.ofSet s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<VAR>h : e.target = e'.source<GOAL>(e.trans' e' h).target = e'.target
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<VAR>h : e.target = e'.source<GOAL>∀ (a : γ), ↑(e.trans' e' h).symm a = (↑e.symm ∘ ↑e'.symm) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<VAR>h : e.target = e'.source<GOAL>(e.trans' e' h).source = e.source
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<VAR>h : e.target = e'.source<GOAL>∀ (a : α), ↑(e.trans' e' h) a = (↑e' ∘ ↑e) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<GOAL>↑(e.trans e') = ↑e' ∘ ↑e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<GOAL>↑(e.trans e').symm = ↑e.symm ∘ ↑e'.symm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<VAR>x : α<GOAL>↑(e.trans e') x = ↑e' (↑e x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<GOAL>(e.trans e').symm = e'.symm.trans e.symm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<GOAL>(e.trans e').source = e.source ∩ ↑e ⁻¹' e'.source
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<GOAL>(e.trans e').source = e.source ∩ ↑e ⁻¹' (e.target ∩ e'.source)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<GOAL>(e.trans e').source = ↑e.symm '' (e.target ∩ e'.source)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<GOAL>↑e '' (e.trans e').source = e.target ∩ e'.source
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<GOAL>(e.trans e').target = e'.target ∩ ↑e'.symm ⁻¹' e.target
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<GOAL>(e.trans e').target = e'.target ∩ ↑e'.symm ⁻¹' (e'.source ∩ e.target)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<GOAL>(e.trans e').target = ↑e' '' (e'.source ∩ e.target)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<GOAL>↑e'.symm '' (e.trans e').target = e'.source ∩ e.target
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<VAR>e'' : PartialEquiv γ δ<GOAL>(e.trans e').trans e'' = e.trans (e'.trans e'')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<GOAL>e.trans (PartialEquiv.refl β) = e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<GOAL>(PartialEquiv.refl α).trans e = e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set β<GOAL>e.trans (PartialEquiv.ofSet s) = e.restr (↑e ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set β<GOAL>e.trans ((PartialEquiv.refl β).restr s) = e.restr (↑e ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<VAR>s : Set β<GOAL>e.trans ((PartialEquiv.refl β).restr s) = e.restr (e.source ∩ ↑e ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv β γ<VAR>s : Set α<GOAL>(e.restr s).trans e' = (e.trans e').restr s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv α γ<VAR>x : α<VAR>he : x ∈ e.source<VAR>he' : x ∈ e'.source<GOAL>↑e x ∈ (e.symm.trans e').source
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<GOAL>e ≈ e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e e' : PartialEquiv α β<VAR>h : e ≈ e'<GOAL>e.source = e'.source
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e e' : PartialEquiv α β<VAR>h : e ≈ e'<GOAL>Set.EqOn (↑e) (↑e') e.source
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e e' : PartialEquiv α β<VAR>h : e ≈ e'<GOAL>e.target = e'.target
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e e' : PartialEquiv α β<VAR>h : e ≈ e'<GOAL>e.symm ≈ e'.symm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e e' : PartialEquiv α β<VAR>h : e ≈ e'<GOAL>Set.EqOn (↑e.symm) (↑e'.symm) e.target
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e e' : PartialEquiv α β<VAR>f f' : PartialEquiv β γ<VAR>he : e ≈ e'<VAR>hf : f ≈ f'<GOAL>e.trans f ≈ e'.trans f'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e e' : PartialEquiv α β<VAR>he : e ≈ e'<VAR>s : Set α<GOAL>e.restr s ≈ e'.restr s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e e' : PartialEquiv α β<VAR>he : e ≈ e'<VAR>s : Set β<GOAL>e.source ∩ ↑e ⁻¹' s = e'.source ∩ ↑e' ⁻¹' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<GOAL>e.trans e.symm ≈ PartialEquiv.ofSet e.source