ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : PartialEquiv α β<GOAL>e.symm.trans e ≈ PartialEquiv.ofSet e.target
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e e' : PartialEquiv α β<VAR>h : e ≈ e'<VAR>s : e.source = Set.univ<VAR>t : e.target = Set.univ<GOAL>e = e'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv γ δ<GOAL>(e.prod e').source = e.source ×ˢ e'.source
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv γ δ<GOAL>(e.prod e').target = e.target ×ˢ e'.target
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv γ δ<GOAL>↑(e.prod e') = fun p => (↑e p.1, ↑e' p.2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv γ δ<GOAL>↑(e.prod e').symm = fun p => (↑e.symm p.1, ↑e'.symm p.2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e : PartialEquiv α β<VAR>e' : PartialEquiv γ δ<GOAL>(e.prod e').symm = e.symm.prod e'.symm
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>(PartialEquiv.refl α).prod (PartialEquiv.refl β) = PartialEquiv.refl (α × β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>η : Type u_5<VAR>ε : Type u_6<VAR>e : PartialEquiv α β<VAR>f : PartialEquiv β γ<VAR>e' : PartialEquiv δ η<VAR>f' : PartialEquiv η ε<GOAL>(e.prod e').trans (f.prod f') = (e.trans f).prod (e'.trans f')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e e' : PartialEquiv α β<VAR>s : Set α<VAR>t : Set β<VAR>(x : α) → Decidable (x ∈ s)<VAR>(y : β) → Decidable (y ∈ t)<VAR>H : e.IsImage s t<VAR>H' : e'.IsImage s t<GOAL>↑(e.piecewise e' s t H H') = s.piecewise ↑e ↑e'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e e' : PartialEquiv α β<VAR>s : Set α<VAR>t : Set β<VAR>(x : α) → Decidable (x ∈ s)<VAR>(y : β) → Decidable (y ∈ t)<VAR>H : e.IsImage s t<VAR>H' : e'.IsImage s t<GOAL>↑(e.piecewise e' s t H H').symm = t.piecewise ↑e.symm ↑e'.symm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e e' : PartialEquiv α β<VAR>s : Set α<VAR>t : Set β<VAR>(x : α) → Decidable (x ∈ s)<VAR>(y : β) → Decidable (y ∈ t)<VAR>H : e.IsImage s t<VAR>H' : e'.IsImage s t<GOAL>(e.piecewise e' s t H H').target = t.ite e.target e'.target
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e e' : PartialEquiv α β<VAR>s : Set α<VAR>t : Set β<VAR>(x : α) → Decidable (x ∈ s)<VAR>(y : β) → Decidable (y ∈ t)<VAR>H : e.IsImage s t<VAR>H' : e'.IsImage s t<GOAL>(e.piecewise e' s t H H').source = s.ite e.source e'.source
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e e' : PartialEquiv α β<VAR>s : Set α<VAR>t : Set β<VAR>(x : α) → Decidable (x ∈ s)<VAR>(y : β) → Decidable (y ∈ t)<VAR>H : e.IsImage s t<VAR>H' : e'.IsImage s t<GOAL>(e.piecewise e' s t H H').symm = e.symm.piecewise e'.symm t s ⋯ ⋯
<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<VAR>(x : α) → Decidable (x ∈ e.source)<VAR>(y : β) → Decidable (y ∈ e.target)<GOAL>(e.disjointUnion e' hs ht).target = e.target ∪ 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<VAR>(x : α) → Decidable (x ∈ e.source)<VAR>(y : β) → Decidable (y ∈ e.target)<GOAL>↑(e.disjointUnion e' hs ht) = e.source.piecewise ↑e ↑e'
<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<VAR>(x : α) → Decidable (x ∈ e.source)<VAR>(y : β) → Decidable (y ∈ e.target)<GOAL>↑(e.disjointUnion e' hs ht).symm = e.target.piecewise ↑e.symm ↑e'.symm
<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<VAR>(x : α) → Decidable (x ∈ e.source)<VAR>(y : β) → Decidable (y ∈ e.target)<GOAL>(e.disjointUnion e' hs ht).source = e.source ∪ e'.source
<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<VAR>(x : α) → Decidable (x ∈ e.source)<VAR>(y : β) → Decidable (y ∈ e.target)<GOAL>e.disjointUnion e' hs ht = e.piecewise e' e.source e.target ⋯ ⋯
<VAR>ι : Type u_5<VAR>αi : ι → Type u_6<VAR>βi : ι → Type u_7<VAR>ei : (i : ι) → PartialEquiv (αi i) (βi i)<GOAL>(PartialEquiv.pi ei).source = Set.univ.pi fun i => (ei i).source
<VAR>ι : Type u_5<VAR>αi : ι → Type u_6<VAR>βi : ι → Type u_7<VAR>ei : (i : ι) → PartialEquiv (αi i) (βi i)<GOAL>↑(PartialEquiv.pi ei) = fun f i => ↑(ei i) (f i)
<VAR>ι : Type u_5<VAR>αi : ι → Type u_6<VAR>βi : ι → Type u_7<VAR>ei : (i : ι) → PartialEquiv (αi i) (βi i)<GOAL>(PartialEquiv.pi ei).target = Set.univ.pi fun i => (ei i).target
<VAR>ι : Type u_5<VAR>αi : ι → Type u_6<VAR>βi : ι → Type u_7<VAR>ei : (i : ι) → PartialEquiv (αi i) (βi i)<GOAL>(PartialEquiv.pi ei).symm = PartialEquiv.pi fun i => (ei i).symm
<VAR>ι : Type u_5<VAR>αi : ι → Type u_6<VAR>βi : ι → Type u_7<VAR>ei : (i : ι) → PartialEquiv (αi i) (βi i)<GOAL>↑(PartialEquiv.pi ei).symm = fun f i => ↑(ei i).symm (f i)
<VAR>ι : Type u_5<VAR>αi : ι → Type u_6<GOAL>(PartialEquiv.pi fun i => PartialEquiv.refl (αi i)) = PartialEquiv.refl ((i : ι) → αi i)
<VAR>ι : Type u_5<VAR>αi : ι → Type u_6<VAR>βi : ι → Type u_7<VAR>γi : ι → Type u_8<VAR>ei : (i : ι) → PartialEquiv (αi i) (βi i)<VAR>ei' : (i : ι) → PartialEquiv (βi i) (γi i)<GOAL>(PartialEquiv.pi ei).trans (PartialEquiv.pi ei') = PartialEquiv.pi fun i => (ei i).trans (ei' i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Nonempty α<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>hf : Set.BijOn f s t<GOAL>(Set.BijOn.toPartialEquiv f s t hf).target = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Nonempty α<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>hf : Set.BijOn f s t<GOAL>↑(Set.BijOn.toPartialEquiv f s t hf).symm = Function.invFunOn f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Nonempty α<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>hf : Set.BijOn f s t<GOAL>(Set.BijOn.toPartialEquiv f s t hf).source = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Nonempty α<VAR>f : α → β<VAR>s : Set α<VAR>t : Set β<VAR>hf : Set.BijOn f s t<GOAL>↑(Set.BijOn.toPartialEquiv f s t hf) = f
<VAR>α : Type u_1<GOAL>(Equiv.refl α).toPartialEquiv = PartialEquiv.refl α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<GOAL>e.symm.toPartialEquiv = e.toPartialEquiv.symm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : α ≃ β<VAR>e' : β ≃ γ<GOAL>(e.trans e').toPartialEquiv = e.toPartialEquiv.trans e'.toPartialEquiv
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : α ≃ β<VAR>f' : PartialEquiv β γ<GOAL>∀ (a : γ), ↑(e.transPartialEquiv f').symm a = e.symm (↑f'.symm a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : α ≃ β<VAR>f' : PartialEquiv β γ<GOAL>(e.transPartialEquiv f').source = ⇑e ⁻¹' f'.source
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : α ≃ β<VAR>f' : PartialEquiv β γ<GOAL>∀ (a : α), ↑(e.transPartialEquiv f') a = ↑f' (e a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : α ≃ β<VAR>f' : PartialEquiv β γ<GOAL>(e.transPartialEquiv f').target = f'.target
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : α ≃ β<VAR>f' : PartialEquiv β γ<GOAL>e.transPartialEquiv f' = e.toPartialEquiv.trans f'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e : α ≃ β<VAR>f' : PartialEquiv β γ<VAR>f'' : PartialEquiv γ δ<GOAL>(e.transPartialEquiv f').trans f'' = e.transPartialEquiv (f'.trans f'')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e : α ≃ β<VAR>e' : β ≃ γ<VAR>f'' : PartialEquiv γ δ<GOAL>(e.trans e').transPartialEquiv f'' = e.transPartialEquiv (e'.transPartialEquiv f'')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : PartialEquiv α β<VAR>f' : β ≃ γ<GOAL>∀ (a : γ), ↑(e.transEquiv f').symm a = ↑e.symm (f'.symm a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : PartialEquiv α β<VAR>f' : β ≃ γ<GOAL>∀ (a : α), ↑(e.transEquiv f') a = f' (↑e a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : PartialEquiv α β<VAR>f' : β ≃ γ<GOAL>(e.transEquiv f').source = e.source
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : PartialEquiv α β<VAR>f' : β ≃ γ<GOAL>(e.transEquiv f').target = ⇑f'.symm ⁻¹' e.target
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e : PartialEquiv α β<VAR>e' : β ≃ γ<GOAL>e.transEquiv e' = e.trans e'.toPartialEquiv
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>ga : α → α<VAR>gb : β → β<GOAL>Function.Semiconj f ga gb ↔ f ∘ ga = gb ∘ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>ga : α → α<VAR>gb : β → β<VAR>h : Function.Semiconj f ga gb<VAR>x : α<GOAL>f (ga x) = gb (f x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>ga ga' : α → α<VAR>gb gb' : β → β<VAR>h : Function.Semiconj f ga gb<VAR>h' : Function.Semiconj f ga' gb'<GOAL>Function.Semiconj f (ga ∘ ga') (gb ∘ gb')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>fab : α → β<VAR>fbc : β → γ<VAR>ga : α → α<VAR>gb : β → β<VAR>gc : γ → γ<VAR>hab : Function.Semiconj fab ga gb<VAR>hbc : Function.Semiconj fbc gb gc<GOAL>Function.Semiconj (fbc ∘ fab) ga gc
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>fab : α → β<VAR>fbc : β → γ<VAR>ga : α → α<VAR>gb : β → β<VAR>gc : γ → γ<VAR>hbc : Function.Semiconj fbc gb gc<VAR>hab : Function.Semiconj fab ga gb<GOAL>Function.Semiconj (fbc ∘ fab) ga gc
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<GOAL>Function.Semiconj f id id
<VAR>α : Type u_1<VAR>ga : α → α<GOAL>Function.Semiconj id ga ga
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>ga ga' : α → α<VAR>gb gb' : β → β<VAR>h : Function.Semiconj f ga gb<VAR>ha : Function.RightInverse ga' ga<VAR>hb : Function.LeftInverse gb' gb<GOAL>Function.Semiconj f ga' gb'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>ga : α → α<VAR>gb : β → β<VAR>f' : β → α<VAR>h : Function.Semiconj f ga gb<VAR>hf₁ : Function.LeftInverse f' f<VAR>hf₂ : Function.RightInverse f' f<GOAL>Function.Semiconj f' gb ga
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>ga : α → α<VAR>gb : β → β<VAR>h : Function.Semiconj f ga gb<GOAL>Function.Semiconj (Option.map f) (Option.map ga) (Option.map gb)
<VAR>α : Type u_1<VAR>f g : α → α<VAR>h : Function.Semiconj f g g<GOAL>Function.Commute f g
<VAR>α : Type u_1<VAR>f g : α → α<VAR>h : Function.Commute f g<GOAL>Function.Semiconj f g g
<VAR>α : Type u_1<VAR>f : α → α<GOAL>Function.Commute f f
<VAR>α : Type u_1<VAR>f g : α → α<VAR>h : Function.Commute f g<GOAL>Function.Commute g f
<VAR>α : Type u_1<VAR>f g g' : α → α<VAR>h : Function.Commute f g<VAR>h' : Function.Commute f g'<GOAL>Function.Commute f (g ∘ g')
<VAR>α : Type u_1<VAR>f f' g : α → α<VAR>h : Function.Commute f g<VAR>h' : Function.Commute f' g<GOAL>Function.Commute (f ∘ f') g
<VAR>α : Type u_1<VAR>f : α → α<GOAL>Function.Commute f id
<VAR>α : Type u_1<VAR>f : α → α<GOAL>Function.Commute id f
<VAR>α : Type u_1<VAR>f g : α → α<VAR>h : Function.Commute f g<GOAL>Function.Commute (Option.map f) (Option.map g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>ga : α → α → α<VAR>gb : β → β → β<VAR>h : Function.Semiconj₂ f ga gb<VAR>x y : α<GOAL>f (ga x y) = gb (f x) (f y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>ga : α → α → α<VAR>gb : β → β → β<VAR>h : Function.Semiconj₂ f ga gb<GOAL>Function.bicompr f ga = Function.bicompl gb f f
<VAR>α : Type u_1<VAR>op : α → α → α<GOAL>Function.Semiconj₂ id op op
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>ga : α → α → α<VAR>gb : β → β → β<VAR>f' : β → γ<VAR>gc : γ → γ → γ<VAR>hf' : Function.Semiconj₂ f' gb gc<VAR>hf : Function.Semiconj₂ f ga gb<GOAL>Function.Semiconj₂ (f' ∘ f) ga gc
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>ga : α → α → α<VAR>gb : β → β → β<VAR>Std.Associative ga<VAR>h : Function.Semiconj₂ f ga gb<VAR>h_surj : Function.Surjective f<GOAL>Std.Associative gb
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>ga : α → α → α<VAR>gb : β → β → β<VAR>Std.Associative gb<VAR>h : Function.Semiconj₂ f ga gb<VAR>h_inj : Function.Injective f<GOAL>Std.Associative ga
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>ga : α → α → α<VAR>gb : β → β → β<VAR>Std.IdempotentOp ga<VAR>h : Function.Semiconj₂ f ga gb<VAR>h_surj : Function.Surjective f<GOAL>Std.IdempotentOp gb
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>ga : α → α → α<VAR>gb : β → β → β<VAR>Std.IdempotentOp gb<VAR>h : Function.Semiconj₂ f ga gb<VAR>h_inj : Function.Injective f<GOAL>Std.IdempotentOp ga
<VAR>α : Type v<VAR>β : Type w<VAR>Small.{u, w} β<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>Small.{u, v} α
<VAR>α : Type v<VAR>β : Type w<VAR>Small.{u, v} α<VAR>f : α → β<VAR>hf : Function.Surjective f<GOAL>Small.{u, w} β
<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type v'<VAR>Small.{u, v} α<VAR>f : α → γ<VAR>g : β → γ<VAR>hg : Function.Injective g<VAR>h : ∀ (b : β), ∃ a, f a = g b<GOAL>Small.{u, w} β
<VAR>α : Type u<VAR>f : α → α<GOAL>f^[0] = id
<VAR>α : Type u<VAR>f : α → α<VAR>x : α<GOAL>f^[0] x = x
<VAR>α : Type u<VAR>f : α → α<VAR>n : ℕ<GOAL>f^[n.succ] = f^[n] ∘ f
<VAR>α : Type u<VAR>f : α → α<VAR>n : ℕ<VAR>x : α<GOAL>f^[n.succ] x = f^[n] (f x)
<VAR>α : Type u<VAR>n : ℕ<GOAL>id^[n] = id
<VAR>α : Type u<VAR>f : α → α<VAR>m n : ℕ<GOAL>f^[m + n] = f^[m] ∘ f^[n]
<VAR>α : Type u<VAR>f : α → α<VAR>m n : ℕ<VAR>x : α<GOAL>f^[m + n] x = f^[m] (f^[n] x)
<VAR>α : Type u<VAR>f : α → α<GOAL>f^[1] = f
<VAR>α : Type u<VAR>f : α → α<VAR>m n : ℕ<GOAL>f^[m * n] = f^[m]^[n]
<VAR>α : Type u<VAR>f : α → α<VAR>x : α<VAR>h : f x = x<VAR>n : ℕ<GOAL>f^[n] x = x
<VAR>α : Type u<VAR>f : α → α<VAR>Hinj : Function.Injective f<VAR>n : ℕ<GOAL>Function.Injective f^[n]
<VAR>α : Type u<VAR>f : α → α<VAR>Hsurj : Function.Surjective f<VAR>n : ℕ<GOAL>Function.Surjective f^[n]
<VAR>α : Type u<VAR>f : α → α<VAR>Hbij : Function.Bijective f<VAR>n : ℕ<GOAL>Function.Bijective f^[n]
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>ga : α → α<VAR>gb : β → β<VAR>h : Function.Semiconj f ga gb<VAR>n : ℕ<GOAL>Function.Semiconj f ga^[n] gb^[n]
<VAR>α : Type u<VAR>f : α → α<VAR>g : ℕ → α → α<VAR>H : ∀ (n : ℕ), Function.Semiconj f (g n) (g (n + 1))<VAR>n k : ℕ<GOAL>Function.Semiconj f^[n] (g k) (g (n + k))
<VAR>α : Type u<VAR>f g : α → α<VAR>h : Function.Commute f g<VAR>n : ℕ<GOAL>Function.Commute f g^[n]
<VAR>α : Type u<VAR>f g : α → α<VAR>h : Function.Commute f g<VAR>n : ℕ<GOAL>Function.Commute f^[n] g
<VAR>α : Type u<VAR>f g : α → α<VAR>h : Function.Commute f g<VAR>m n : ℕ<GOAL>Function.Commute f^[m] g^[n]
<VAR>α : Type u<VAR>f g : α → α<VAR>h : Function.Commute f g<VAR>n : ℕ<VAR>x : α<VAR>hx : f x = g x<GOAL>f^[n] x = g^[n] x
<VAR>α : Type u<VAR>f g : α → α<VAR>h : Function.Commute f g<VAR>n : ℕ<GOAL>(f ∘ g)^[n] = f^[n] ∘ g^[n]
<VAR>α : Type u<VAR>f : α → α<VAR>n : ℕ<GOAL>Function.Commute f^[n] f
<VAR>α : Type u<VAR>f : α → α<VAR>n : ℕ<GOAL>Function.Commute f f^[n]
<VAR>α : Type u<VAR>f : α → α<VAR>m n : ℕ<GOAL>Function.Commute f^[m] f^[n]
<VAR>α : Type u<VAR>f : α → α<VAR>op : α → α → α<VAR>hf : Function.Semiconj₂ f op op<VAR>n : ℕ<GOAL>Function.Semiconj₂ f^[n] op op
<VAR>α : Type u<VAR>f : α → α<VAR>n : ℕ<GOAL>f^[n.succ] = f ∘ f^[n]
<VAR>α : Type u<VAR>f : α → α<VAR>n : ℕ<VAR>x : α<GOAL>f^[n.succ] x = f (f^[n] x)
<VAR>α : Type u<VAR>f : α → α<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>f^[n.pred] ∘ f = f^[n]
<VAR>α : Type u<VAR>f : α → α<VAR>n : ℕ<VAR>hn : 0 < n<GOAL>f ∘ f^[n.pred] = f^[n]
<VAR>α : Type u<VAR>p : α → Sort u_1<VAR>f : α → α<VAR>h : (a : α) → p a → p (f a)<VAR>a : α<VAR>ha : p a<GOAL>Function.Iterate.rec p h ha 0 = ha
<VAR>α : Type u<VAR>f g : α → α<VAR>hg : Function.LeftInverse g f<VAR>n : ℕ<GOAL>Function.LeftInverse g^[n] f^[n]
<VAR>α : Type u<VAR>f g : α → α<VAR>hg : Function.RightInverse g f<VAR>n : ℕ<GOAL>Function.RightInverse g^[n] f^[n]
<VAR>α : Type u<VAR>f : α → α<VAR>m n : ℕ<GOAL>f^[n]^[m] = f^[m]^[n]
<VAR>α : Type u<VAR>m n : ℕ<GOAL>Function.Commute (fun f => f^[m]) fun f => f^[n]
<VAR>α : Type u<VAR>f : α → α<VAR>m n : ℕ<VAR>a : α<VAR>hf : Function.Injective f<GOAL>f^[m + n] a = f^[n] a ↔ f^[m] a = a
<VAR>α : Type u<VAR>f : α → α<VAR>m n : ℕ<VAR>a : α<VAR>hf : Function.Injective f<VAR>ha : f^[m] a = f^[n] a<GOAL>f^[m - n] a = a
<VAR>α : Sort u_1<VAR>f : α → α<GOAL>Function.Involutive f ↔ f^[2] = id
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → α<VAR>a : α<VAR>l : List β<GOAL>List.foldl (fun b x => f b) a l = f^[l.length] a
<VAR>α : Type u<VAR>β : Type v<VAR>f : β → β<VAR>b : β<VAR>l : List α<GOAL>List.foldr (fun x => f) b l = f^[l.length] b
<VAR>α : Type v<GOAL>Small.{w, v} α ↔ ∃ S, Nonempty (α ≃ S)
<VAR>α : Type v<VAR>self : Small.{w, v} α<GOAL>∃ S, Nonempty (α ≃ S)
<VAR>α : Type v<VAR>S : Type w<VAR>e : α ≃ S<GOAL>Small.{w, v} α
<VAR>α : Type v<VAR>Small.{w, v} α<VAR>x y : Shrink.{w, v} α<VAR>w : (equivShrink α).symm x = (equivShrink α).symm y<GOAL>x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>hβ : Small.{w, u_2} β<VAR>e : α ≃ β<GOAL>Small.{w, u_1} α
<VAR>α : Type u<VAR>hα : Small.{v, u} α<GOAL>Small.{max v w, u} α
<VAR>α : Type v<GOAL>Small.{max w v, v} α
<GOAL>Small.{max (u + 1) v, u + 1} (Type u)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<GOAL>Small.{w, u_1} α ↔ Small.{w, u_2} β
<GOAL>¬Small.{u, max (u + 1) (v + 1)} (Type (max u v))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<GOAL>Set.range ⇑e = Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>s : Set α<GOAL>⇑e '' s = ⇑e.symm ⁻¹' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>S : Set α<VAR>f : α ≃ β<VAR>x : β<GOAL>x ∈ ⇑f '' S ↔ f.symm x ∈ S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>S : Set α<VAR>f : α ≃ β<GOAL>⇑f '' S = ⇑f.symm ⁻¹' S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>S : Set α<VAR>f : β ≃ α<GOAL>⇑f ⁻¹' S = ⇑f.symm '' S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>s : Set α<VAR>t : Set β<GOAL>⇑e.symm '' t ⊆ s ↔ t ⊆ ⇑e '' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>s : Set α<VAR>t : Set β<GOAL>s ⊆ ⇑e.symm '' t ↔ ⇑e '' s ⊆ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>s : Set α<GOAL>⇑e.symm '' (⇑e '' s) = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>s : Set α<VAR>t : Set β<GOAL>t = ⇑e '' s ↔ ⇑e.symm '' t = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>s : Set β<GOAL>⇑e '' (⇑e.symm '' s) = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>s : Set β<GOAL>⇑e '' (⇑e ⁻¹' s) = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>s : Set α<GOAL>⇑e ⁻¹' (⇑e '' s) = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α ≃ β<VAR>s : Set α<GOAL>⇑f '' sᶜ = (⇑f '' s)ᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>s : Set β<GOAL>⇑e.symm ⁻¹' (⇑e ⁻¹' s) = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>s : Set α<GOAL>⇑e ⁻¹' (⇑e.symm ⁻¹' s) = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>s t : Set β<GOAL>⇑e ⁻¹' s ⊆ ⇑e ⁻¹' t ↔ s ⊆ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>s t : Set α<GOAL>⇑e '' s ⊆ ⇑e '' t ↔ s ⊆ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>s t : Set α<GOAL>⇑e '' s = ⇑e '' t ↔ s = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>s : Set β<VAR>t : Set α<GOAL>⇑e ⁻¹' s = t ↔ s = ⇑e '' t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>s : Set α<VAR>t : Set β<GOAL>s = ⇑e ⁻¹' t ↔ ⇑e '' s = t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>p : α → Prop<GOAL>{b | p (e.symm b)} = ⇑e '' {a | p a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Set α<VAR>t : Set β<VAR>u : Set γ<GOAL>⇑(Equiv.prodAssoc α β γ) ⁻¹' s ×ˢ t ×ˢ u = (s ×ˢ t) ×ˢ u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Set α<VAR>t : Set β<VAR>u : Set γ<GOAL>⇑(Equiv.prodAssoc α β γ).symm ⁻¹' (s ×ˢ t) ×ˢ u = s ×ˢ t ×ˢ u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Set α<VAR>t : Set β<VAR>u : Set γ<GOAL>⇑(Equiv.prodAssoc α β γ) '' (s ×ˢ t) ×ˢ u = s ×ˢ t ×ˢ u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Set α<VAR>t : Set β<VAR>u : Set γ<GOAL>⇑(Equiv.prodAssoc α β γ).symm '' s ×ˢ t ×ˢ u = (s ×ˢ t) ×ˢ u
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : s = t<VAR>a : { a // (fun x => x ∈ s) a }<GOAL>(Equiv.setCongr h) a = ⟨↑a, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>s : Set α<VAR>x : ↑s<GOAL>↑((e.image s) x) = e ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>s : Set α<VAR>y : ↑(⇑e '' s)<GOAL>↑((e.image s).symm y) = e.symm ↑y
<VAR>α : Type u_1<VAR>s t : Set α<VAR>DecidablePred fun x => x ∈ s<VAR>H : s ∩ t ⊆ ∅<VAR>a : ↑(s ∪ t)<VAR>ha : ↑a ∈ s<GOAL>(Equiv.Set.union H) a = Sum.inl ⟨↑a, ha⟩
<VAR>α : Type u_1<VAR>s t : Set α<VAR>DecidablePred fun x => x ∈ s<VAR>H : s ∩ t ⊆ ∅<VAR>a : ↑(s ∪ t)<VAR>ha : ↑a ∈ t<GOAL>(Equiv.Set.union H) a = Sum.inr ⟨↑a, ha⟩
<VAR>α : Type u_1<VAR>s t : Set α<VAR>DecidablePred fun x => x ∈ s<VAR>H : s ∩ t ⊆ ∅<VAR>a : ↑s<GOAL>(Equiv.Set.union H).symm (Sum.inl a) = ⟨↑a, ⋯⟩
<VAR>α : Type u_1<VAR>s t : Set α<VAR>DecidablePred fun x => x ∈ s<VAR>H : s ∩ t ⊆ ∅<VAR>a : ↑t<GOAL>(Equiv.Set.union H).symm (Sum.inr a) = ⟨↑a, ⋯⟩
<VAR>α : Type u<VAR>s t : Set α<VAR>h : s = t<VAR>b : { b // (fun x => x ∈ t) b }<GOAL>(Equiv.Set.ofEq h).symm b = ⟨↑b, ⋯⟩
<VAR>α : Type u<VAR>s t : Set α<VAR>h : s = t<VAR>a : { a // (fun x => x ∈ s) a }<GOAL>(Equiv.Set.ofEq h) a = ⟨↑a, ⋯⟩
<VAR>α : Type u<VAR>s : Set α<VAR>DecidablePred fun x => x ∈ s<VAR>a : α<VAR>H : a ∉ s<VAR>b : ↑s<GOAL>(Equiv.Set.insert H).symm (Sum.inl b) = ⟨↑b, ⋯⟩
<VAR>α : Type u<VAR>s : Set α<VAR>DecidablePred fun x => x ∈ s<VAR>a : α<VAR>H : a ∉ s<VAR>b : PUnit.{u + 1}<GOAL>(Equiv.Set.insert H).symm (Sum.inr b) = ⟨a, ⋯⟩
<VAR>α : Type u<VAR>s : Set α<VAR>DecidablePred fun x => x ∈ s<VAR>a : α<VAR>H : a ∉ s<GOAL>(Equiv.Set.insert H) ⟨a, ⋯⟩ = Sum.inr PUnit.unit
<VAR>α : Type u<VAR>s : Set α<VAR>DecidablePred fun x => x ∈ s<VAR>a : α<VAR>H : a ∉ s<VAR>b : ↑s<GOAL>(Equiv.Set.insert H) ⟨↑b, ⋯⟩ = Sum.inl b
<VAR>α : Type u<VAR>s : Set α<VAR>DecidablePred fun x => x ∈ s<VAR>x : ↑s<GOAL>(Equiv.Set.sumCompl s) (Sum.inl x) = ↑x
<VAR>α : Type u<VAR>s : Set α<VAR>DecidablePred fun x => x ∈ s<VAR>x : ↑sᶜ<GOAL>(Equiv.Set.sumCompl s) (Sum.inr x) = ↑x
<VAR>α : Type u<VAR>s : Set α<VAR>DecidablePred fun x => x ∈ s<VAR>x : α<VAR>hx : x ∈ s<GOAL>(Equiv.Set.sumCompl s).symm x = Sum.inl ⟨x, hx⟩
<VAR>α : Type u<VAR>s : Set α<VAR>DecidablePred fun x => x ∈ s<VAR>x : α<VAR>hx : x ∉ s<GOAL>(Equiv.Set.sumCompl s).symm x = Sum.inr ⟨x, hx⟩
<VAR>α : Type u_1<VAR>s : Set α<VAR>DecidablePred fun x => x ∈ s<VAR>x : ↑s<GOAL>(Equiv.Set.sumCompl s).symm ↑x = Sum.inl x
<VAR>α : Type u_1<VAR>s : Set α<VAR>DecidablePred fun x => x ∈ s<VAR>x : ↑sᶜ<GOAL>(Equiv.Set.sumCompl s).symm ↑x = Sum.inr x
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>DecidablePred fun x => x ∈ s<VAR>x : ↑s<GOAL>(Equiv.Set.sumDiffSubset h) (Sum.inl x) = Set.inclusion h x
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>DecidablePred fun x => x ∈ s<VAR>x : ↑(t \ s)<GOAL>(Equiv.Set.sumDiffSubset h) (Sum.inr x) = Set.inclusion ⋯ x
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>DecidablePred fun x => x ∈ s<VAR>x : ↑t<VAR>hx : ↑x ∈ s<GOAL>(Equiv.Set.sumDiffSubset h).symm x = Sum.inl ⟨↑x, hx⟩
<VAR>α : Type u_1<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>DecidablePred fun x => x ∈ s<VAR>x : ↑t<VAR>hx : ↑x ∉ s<GOAL>(Equiv.Set.sumDiffSubset h).symm x = Sum.inr ⟨↑x, ⋯⟩
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>s : (a : α) → Set (β a)<VAR>f : (a : α) → ↑(s a)<VAR>a : α<GOAL>↑((Equiv.Set.univPi s).symm f) a = ↑(f a)
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>s : (a : α) → Set (β a)<VAR>f : ↑(Set.univ.pi s)<VAR>a : α<GOAL>↑((Equiv.Set.univPi s) f a) = ↑f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<VAR>H : Function.Injective f<VAR>p : ↑s<GOAL>(Equiv.Set.image f s H) p = ⟨f ↑p, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set α<VAR>H : Function.Injective f<VAR>x : α<VAR>h : f x ∈ f '' s<GOAL>(Equiv.Set.image f s H).symm ⟨f x, h⟩ = ⟨x, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>u s : Set α<GOAL>(fun x => ↑((Equiv.Set.image f s hf).symm x)) ⁻¹' u = Subtype.val ⁻¹' (f '' u)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>t : Set β<GOAL>(Equiv.Set.congr e).symm t = ⇑e.symm '' t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>s : Set α<GOAL>(Equiv.Set.congr e) s = ⇑e '' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set ↑(Set.range f)<VAR>x : ↑s<GOAL>↑((Equiv.Set.rangeSplittingImageEquiv f s).symm x) = Set.rangeSplitting f ↑x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>s : Set ↑(Set.range f)<VAR>x : ↑(Set.rangeSplitting f '' s)<GOAL>↑↑((Equiv.Set.rangeSplittingImageEquiv f s) x) = f ↑x