ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : α<GOAL>↑((Equiv.Set.rangeInl α β).symm x) = Sum.inl x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : α<GOAL>(Equiv.Set.rangeInl α β) ⟨Sum.inl x, ⋯⟩ = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : β<GOAL>↑((Equiv.Set.rangeInr α β).symm x) = Sum.inr x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : β<GOAL>(Equiv.Set.rangeInr α β) ⟨Sum.inr x, ⋯⟩ = x
<VAR>α : Sort u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>f_inv : Nonempty α → β → α<VAR>hf : ∀ (h : Nonempty α), Function.LeftInverse (f_inv h) f<VAR>b : ↑(Set.range f)<GOAL>(Equiv.ofLeftInverse f f_inv hf).symm b = f_inv ⋯ ↑b
<VAR>α : Sort u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>f_inv : Nonempty α → β → α<VAR>hf : ∀ (h : Nonempty α), Function.LeftInverse (f_inv h) f<VAR>a : α<GOAL>↑((Equiv.ofLeftInverse f f_inv hf) a) = f a
<VAR>α : Sort u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>a : α<GOAL>(Equiv.ofInjective f hf) a = ⟨f a, ⋯⟩
<VAR>α : Sort u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>b : ↑(Set.range f)<GOAL>f ((Equiv.ofInjective f hf).symm b) = ↑b
<VAR>α : Sort u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>a : α<GOAL>(Equiv.ofInjective f hf).symm ⟨f a, ⋯⟩ = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>⇑(Equiv.ofInjective f hf).symm = Set.rangeSplitting f
<VAR>α : Sort u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>f ∘ ⇑(Equiv.ofInjective f hf).symm = Subtype.val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>f_inv : Nonempty α → β → α<VAR>hf : ∀ (h : Nonempty α), Function.LeftInverse (f_inv h) f<GOAL>Equiv.ofLeftInverse f f_inv hf = Equiv.ofInjective f ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>f_inv : β → α<VAR>hf : Function.LeftInverse f_inv f<GOAL>Equiv.ofLeftInverse' f f_inv hf = Equiv.ofInjective f ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<VAR>p : Set α → Prop<GOAL>(∀ (a : Set α), p a) ↔ ∀ (a : Set β), p (⇑e ⁻¹' a)
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>p : α → Prop<VAR>DecidablePred p<VAR>s : (i : α) → Set (β i)<GOAL>⇑(Equiv.piEquivPiSubtypeProd p β).symm ⁻¹' Set.univ.pi s = (Set.univ.pi fun i => s ↑i) ×ˢ Set.univ.pi fun i => s ↑i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>x : (y : β) × { x // f x = y }<GOAL>(Equiv.sigmaPreimageEquiv f) x = ↑x.snd
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>x : α<GOAL>↑((Equiv.sigmaPreimageEquiv f).symm x).snd = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>x : α<GOAL>((Equiv.sigmaPreimageEquiv f).symm x).fst = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → γ<VAR>g : β → γ<VAR>e : (c : γ) → ↑(f ⁻¹' {c}) ≃ ↑(g ⁻¹' {c})<GOAL>∀ (a : β), (Equiv.ofPreimageEquiv e).symm a = ↑((Equiv.sigmaCongrRight e).symm ((Equiv.sigmaFiberEquiv g).symm a)).snd
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → γ<VAR>g : β → γ<VAR>e : (c : γ) → ↑(f ⁻¹' {c}) ≃ ↑(g ⁻¹' {c})<GOAL>∀ (a : α), (Equiv.ofPreimageEquiv e) a = ↑((e (f a)) ((Equiv.sigmaFiberEquiv f).symm a).snd)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → γ<VAR>g : β → γ<VAR>e : (c : γ) → ↑(f ⁻¹' {c}) ≃ ↑(g ⁻¹' {c})<VAR>a : α<GOAL>g ((Equiv.ofPreimageEquiv e) a) = f a
<VAR>α : Type u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>p : α → Prop<VAR>e : β ≃ Subtype p<VAR>v : β → γ<VAR>w : α → γ<VAR>j : β<VAR>x : γ<VAR>DecidableEq β<VAR>DecidableEq α<VAR>(j : α) → Decidable (p j)<GOAL>(fun i => if h : p i then Function.update v j x (e.symm ⟨i, h⟩) else w i) = Function.update (fun i => if h : p i then v (e.symm ⟨i, h⟩) else w i) (↑(e j)) x
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b : α<VAR>s : Set α<VAR>hs : a ∈ s ↔ b ∈ s<GOAL>Set.BijOn (⇑(Equiv.swap a b)) s s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>a b : α<VAR>s : Set α<VAR>ha : a ∈ s<VAR>hb : b ∉ s<GOAL>Set.BijOn (⇑(Equiv.swap a b)) s (insert b (s \ {a}))
<VAR>α : Sort u_1<VAR>β : α → Sort u_4<VAR>x : α<VAR>f : (x : α) → β x<GOAL>Function.eval x f = f x
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>y : β<GOAL>(fun x => y) = Function.const α y
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>Nonempty α<GOAL>Function.Injective (Function.const α)
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>Nonempty α<VAR>y₁ y₂ : β<GOAL>Function.const α y₁ = Function.const α y₂ ↔ y₁ = y₂
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : β → β → γ<VAR>g : α → β<VAR>a b : α<GOAL>(f on g) a b = f (g a) (g b)
<VAR>α α' : Sort u<VAR>β : α → Sort v<VAR>β' : α' → Sort v<VAR>f : (a : α) → β a<VAR>f' : (a : α') → β' a<VAR>hα : α = α'<VAR>h : ∀ (a : α) (a' : α'), HEq a a' → HEq (f a) (f' a')<GOAL>HEq f f'
<VAR>α : Sort u_1<VAR>β : α → Sort u_4<VAR>f₁ f₂ : (a : α) → β a<GOAL>f₁ ≠ f₂ ↔ ∃ a, f₁ a ≠ f₂ a
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>Subsingleton α<VAR>g : α → β<VAR>x y : α<GOAL>f x = g y ↔ f = g
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>hf : Function.Bijective f<GOAL>Function.Injective f
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>hf : Function.Bijective f<GOAL>Function.Surjective f
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>I : Function.Injective f<VAR>a b : α<GOAL>f a = f b ↔ a = b
<VAR>α : Type u_4<VAR>β : Type u_5<VAR>BEq α<VAR>LawfulBEq α<VAR>BEq β<VAR>LawfulBEq β<VAR>f : α → β<VAR>I : Function.Injective f<VAR>a b : α<GOAL>(f a == f b) = (a == b)
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>I : Function.Injective f<VAR>a b : α<VAR>c : β<VAR>h : f b = c<GOAL>f a = c ↔ a = b
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>a₁ a₂ : α<GOAL>a₁ ≠ a₂ → f a₁ ≠ f a₂
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>x y : α<GOAL>f x ≠ f y ↔ x ≠ y
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>x y : α<VAR>z : β<VAR>h : f y = z<GOAL>f x ≠ z ↔ x ≠ y
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<GOAL>¬Function.Injective f ↔ ∃ a b, f a = f b ∧ a ≠ b
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<VAR>g : γ → α<VAR>I : Function.Injective (f ∘ g)<GOAL>Function.Injective g
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>g : γ → α<GOAL>Function.Injective (f ∘ g) ↔ Function.Injective g
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<VAR>g : γ → α<VAR>I : Function.Injective (f ∘ g)<VAR>hg : Function.Surjective g<GOAL>Function.Injective f
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<VAR>g : γ → α<VAR>hf : Function.Surjective f<VAR>hg : Function.Surjective g<VAR>I : Function.Injective (f ∘ g)<GOAL>Function.Bijective f ∧ Function.Bijective g
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<VAR>g : γ → α<VAR>hg : Function.Bijective g<GOAL>Function.Injective (f ∘ g) ↔ Function.Injective f
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>g : β → γ<VAR>hg : Function.Injective g<GOAL>Function.Injective fun x => g ∘ x
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>Subsingleton α<VAR>f : α → β<GOAL>Function.Injective f
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>p : α → Prop<VAR>DecidablePred p<VAR>f : { a // p a } → β<VAR>f' : { a // ¬p a } → β<VAR>hf : Function.Injective f<VAR>hf' : Function.Injective f'<VAR>im_disj : ∀ {x x' : α} {hx : p x} {hx' : ¬p x'}, f ⟨x, hx⟩ ≠ f' ⟨x', hx'⟩<GOAL>Function.Injective fun x => if h : p x then f ⟨x, h⟩ else f' ⟨x, h⟩
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<VAR>g : γ → α<VAR>S : Function.Surjective (f ∘ g)<GOAL>Function.Surjective f
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<VAR>g : γ → α<VAR>hg : Function.Surjective g<GOAL>Function.Surjective (f ∘ g) ↔ Function.Surjective f
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<VAR>g : γ → α<VAR>S : Function.Surjective (f ∘ g)<VAR>hf : Function.Injective f<GOAL>Function.Surjective g
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<VAR>g : γ → α<VAR>hf : Function.Injective f<VAR>hg : Function.Injective g<VAR>S : Function.Surjective (f ∘ g)<GOAL>Function.Bijective f ∧ Function.Bijective g
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<VAR>hf : Function.Bijective f<VAR>g : γ → α<GOAL>Function.Surjective (f ∘ g) ↔ Function.Surjective g
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>hf : Function.Surjective f<VAR>p : β → Prop<GOAL>(∀ (y : β), p y) ↔ ∀ (x : α), p (f x)
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>hf : Function.Surjective f<VAR>p : β → β → Prop<GOAL>(∀ (y₁ y₂ : β), p y₁ y₂) ↔ ∀ (x₁ x₂ : α), p (f x₁) (f x₂)
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>hf : Function.Surjective f<VAR>p : β → β → β → Prop<GOAL>(∀ (y₁ y₂ y₃ : β), p y₁ y₂ y₃) ↔ ∀ (x₁ x₂ x₃ : α), p (f x₁) (f x₂) (f x₃)
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>hf : Function.Surjective f<VAR>p : β → Prop<GOAL>(∃ y, p y) ↔ ∃ x, p (f x)
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>hf : Function.Surjective f<VAR>p : β → β → Prop<GOAL>(∃ y₁ y₂, p y₁ y₂) ↔ ∃ x₁ x₂, p (f x₁) (f x₂)
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>hf : Function.Surjective f<VAR>p : β → β → β → Prop<GOAL>(∃ y₁ y₂ y₃, p y₁ y₂ y₃) ↔ ∃ x₁ x₂ x₃, p (f x₁) (f x₂) (f x₃)
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<VAR>hf : Function.Surjective f<GOAL>Function.Injective fun g => g ∘ f
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<VAR>hf : Function.Surjective f<VAR>g₁ g₂ : β → γ<GOAL>g₁ ∘ f = g₂ ∘ f ↔ g₁ = g₂
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>h : ∀ (g₁ g₂ : β → Prop), g₁ ∘ f = g₂ ∘ f → g₁ = g₂<GOAL>Function.Surjective f
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<GOAL>Function.Bijective f ↔ ∀ (b : β), ∃! a, f a = b
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>hf : Function.Bijective f<VAR>b : β<GOAL>∃! a, f a = b
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>hf : Function.Bijective f<VAR>p : β → Prop<GOAL>(∃! y, p y) ↔ ∃! x, p (f x)
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<VAR>g : γ → α<VAR>hg : Function.Bijective g<GOAL>Function.Bijective (f ∘ g) ↔ Function.Bijective f
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<VAR>hf : Function.Bijective f<VAR>g : γ → α<GOAL>Function.Bijective (f ∘ g) ↔ Function.Bijective g
<VAR>α : Type u_4<VAR>f : α → Set α<GOAL>¬Function.Surjective f
<VAR>α : Type u_4<VAR>f : Set α → α<GOAL>¬Function.Injective f
<VAR>α : Type u<VAR>f : α → Type (max u v)<GOAL>¬Function.Surjective f
<VAR>α : Type u_4<VAR>β : Sort u_5<VAR>f : α → β<VAR>g : β → Option α<VAR>H : Function.IsPartialInv f g<VAR>x : α<GOAL>g (f x) = some x
<VAR>α : Type u_4<VAR>β : Sort u_5<VAR>f : α → β<VAR>g : β → Option α<VAR>H : Function.IsPartialInv f g<GOAL>Function.Injective f
<VAR>α : Type u_4<VAR>β : Sort u_5<VAR>f : α → β<VAR>g : β → Option α<VAR>H : Function.IsPartialInv f g<VAR>x y : β<VAR>b : α<VAR>h₁ : b ∈ g x<VAR>h₂ : b ∈ g y<GOAL>x = y
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>g : β → α<VAR>h : Function.LeftInverse f g<GOAL>f ∘ g = id
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>g : β → α<GOAL>Function.LeftInverse f g ↔ f ∘ g = id
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>g : β → α<VAR>h : Function.RightInverse f g<GOAL>g ∘ f = id
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>g : β → α<GOAL>Function.RightInverse f g ↔ g ∘ f = id
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<VAR>g : β → α<VAR>h : β → γ<VAR>i : γ → β<VAR>hf : Function.LeftInverse f g<VAR>hh : Function.LeftInverse h i<GOAL>Function.LeftInverse (h ∘ f) (g ∘ i)
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<VAR>g : β → α<VAR>h : β → γ<VAR>i : γ → β<VAR>hf : Function.RightInverse f g<VAR>hh : Function.RightInverse h i<GOAL>Function.RightInverse (h ∘ f) (g ∘ i)
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>g : β → α<VAR>h : Function.LeftInverse g f<GOAL>Function.RightInverse f g
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>g : β → α<VAR>h : Function.RightInverse g f<GOAL>Function.LeftInverse f g
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>g : β → α<VAR>h : Function.LeftInverse f g<GOAL>Function.Surjective f
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>g : β → α<VAR>h : Function.RightInverse f g<GOAL>Function.Injective f
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>g : β → α<VAR>h : Function.LeftInverse f g<VAR>hf : Function.Injective f<GOAL>Function.RightInverse f g
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>g : β → α<VAR>h : Function.LeftInverse f g<VAR>hg : Function.Surjective g<GOAL>Function.RightInverse f g
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>g : β → α<GOAL>Function.RightInverse f g → Function.Surjective f → Function.LeftInverse f g
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>g : β → α<GOAL>Function.RightInverse f g → Function.Injective g → Function.LeftInverse f g
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>g₁ g₂ : β → α<VAR>h₁ : Function.LeftInverse g₁ f<VAR>h₂ : Function.RightInverse g₂ f<GOAL>g₁ = g₂
<VAR>α : Type u_4<VAR>β : Sort u_5<VAR>f : α → β<VAR>I : Function.Injective f<GOAL>Function.IsPartialInv f (Function.partialInv f)
<VAR>α : Type u_4<VAR>β : Sort u_5<VAR>f : α → β<VAR>I : Function.Injective f<VAR>x : α<GOAL>Function.partialInv f (f x) = some x
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>Nonempty α<VAR>f : α → β<VAR>b : β<VAR>h : ∃ a, f a = b<GOAL>f (Function.invFun f b) = b
<VAR>α : Type u_3<VAR>β : Type u_4<VAR>f : α → β<VAR>a : α<GOAL>f (Function.invFun f (f a)) = f a
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>Nonempty α<VAR>f : α → β<VAR>b : β<VAR>h : ¬∃ a, f a = b<GOAL>Function.invFun f b = Classical.choice inst✝
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>Nonempty α<VAR>f : α → β<VAR>g : β → α<VAR>hf : Function.Injective f<VAR>hg : Function.RightInverse g f<GOAL>Function.invFun f = g
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>Nonempty α<VAR>f : α → β<VAR>hf : Function.Surjective f<GOAL>Function.RightInverse (Function.invFun f) f
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>Nonempty α<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>Function.LeftInverse (Function.invFun f) f
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>Nonempty α<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>Function.Surjective (Function.invFun f)
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>Nonempty α<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>Function.invFun f ∘ f = id
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>Nonempty α<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>Function.HasLeftInverse f
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>Nonempty α<VAR>f : α → β<GOAL>Function.Injective f ↔ Function.HasLeftInverse f
<VAR>α : Sort u<VAR>β : Sort v<VAR>f : α → β<VAR>h : Function.Surjective f<VAR>b : β<GOAL>f (Function.surjInv h b) = b
<VAR>α : Sort u<VAR>β : Sort v<VAR>f : α → β<VAR>hf : Function.Surjective f<GOAL>Function.RightInverse (Function.surjInv hf) f
<VAR>α : Sort u<VAR>β : Sort v<VAR>f : α → β<VAR>hf : Function.Bijective f<GOAL>Function.LeftInverse (Function.surjInv ⋯) f
<VAR>α : Sort u<VAR>β : Sort v<VAR>f : α → β<VAR>hf : Function.Surjective f<GOAL>Function.HasRightInverse f
<VAR>α : Sort u<VAR>β : Sort v<VAR>f : α → β<GOAL>Function.Surjective f ↔ Function.HasRightInverse f
<VAR>α : Sort u<VAR>β : Sort v<VAR>f : α → β<GOAL>Function.Bijective f ↔ ∃ g, Function.LeftInverse g f ∧ Function.RightInverse g f
<VAR>α : Sort u<VAR>β : Sort v<VAR>f : α → β<VAR>h : Function.Surjective f<GOAL>Function.Injective (Function.surjInv h)
<VAR>α : Sort u<VAR>β : Sort v<VAR>na : Nonempty α<VAR>Subsingleton β<VAR>f : α → β<GOAL>Function.Surjective f
<VAR>α : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>g : β → γ<VAR>hg : Function.Surjective g<GOAL>Function.Surjective fun x => g ∘ x
<VAR>α : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>g : β → γ<VAR>hg : Function.Bijective g<GOAL>Function.Bijective fun x => g ∘ x
<VAR>α : Sort u<VAR>β : α → Sort v<VAR>DecidableEq α<VAR>a : α<VAR>v : β a<VAR>f : (a : α) → β a<GOAL>Function.update f a v a = v
<VAR>α : Sort u<VAR>β : α → Sort v<VAR>DecidableEq α<VAR>a a' : α<VAR>h : a ≠ a'<VAR>v : β a'<VAR>f : (a : α) → β a<GOAL>Function.update f a' v a = f a
<VAR>α : Sort u<VAR>DecidableEq α<VAR>β : Sort u_1<VAR>f : α → β<VAR>a' : α<VAR>b : β<VAR>a : α<GOAL>Function.update f a' b a = if a = a' then b else f a
<VAR>α : Sort u<VAR>α' : Sort w<VAR>DecidableEq α<VAR>Subsingleton α<VAR>a : α<VAR>v : α'<VAR>f : α → α'<GOAL>Function.update f a v = Function.const α v
<VAR>α : Sort u<VAR>β : α → Sort v<VAR>h : ∀ (a : α), Nonempty (β a)<VAR>a : α<GOAL>Function.Surjective (Function.eval a)
<VAR>α : Sort u<VAR>β : α → Sort v<VAR>DecidableEq α<VAR>f : (a : α) → β a<VAR>a' : α<GOAL>Function.Injective (Function.update f a')
<VAR>α : Sort u<VAR>β : α → Sort v<VAR>DecidableEq α<VAR>f : (a : α) → β a<VAR>a : α<VAR>b : β a<VAR>p : (a : α) → β a → Prop<GOAL>(∀ (x : α), p x (Function.update f a b x)) ↔ p a b ∧ ∀ (x : α), x ≠ a → p x (f x)
<VAR>α : Sort u<VAR>β : α → Sort v<VAR>DecidableEq α<VAR>f : (a : α) → β a<VAR>a : α<VAR>b : β a<VAR>p : (a : α) → β a → Prop<GOAL>(∃ x, p x (Function.update f a b x)) ↔ p a b ∨ ∃ x, x ≠ a ∧ p x (f x)
<VAR>α : Sort u<VAR>β : α → Sort v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>f g : (a : α) → β a<GOAL>Function.update f a b = g ↔ b = g a ∧ ∀ (x : α), x ≠ a → f x = g x
<VAR>α : Sort u<VAR>β : α → Sort v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>f g : (a : α) → β a<GOAL>g = Function.update f a b ↔ g a = b ∧ ∀ (x : α), x ≠ a → g x = f x
<VAR>α : Sort u<VAR>β : α → Sort v<VAR>DecidableEq α<VAR>f : (a : α) → β a<VAR>a : α<VAR>b : β a<GOAL>Function.update f a b = f ↔ b = f a
<VAR>α : Sort u<VAR>β : α → Sort v<VAR>DecidableEq α<VAR>f : (a : α) → β a<VAR>a : α<VAR>b : β a<GOAL>f = Function.update f a b ↔ f a = b
<VAR>α : Sort u<VAR>β : α → Sort v<VAR>DecidableEq α<VAR>f : (a : α) → β a<VAR>a : α<VAR>b : β a<GOAL>f ≠ Function.update f a b ↔ f a ≠ b
<VAR>α : Sort u<VAR>β : α → Sort v<VAR>DecidableEq α<VAR>f : (a : α) → β a<VAR>a : α<VAR>b : β a<GOAL>Function.update f a b ≠ f ↔ b ≠ f a
<VAR>α : Sort u<VAR>β : α → Sort v<VAR>DecidableEq α<VAR>a : α<VAR>f : (a : α) → β a<GOAL>Function.update f a (f a) = f
<VAR>α : Sort u<VAR>β : α → Sort v<VAR>DecidableEq α<VAR>α' : Sort u_1<VAR>g : (a : α) → β a<VAR>f : α' → α<VAR>i : α<VAR>a : β i<VAR>h : ∀ (x : α'), f x ≠ i<GOAL>(fun j => Function.update g i a (f j)) = fun j => g (f j)
<VAR>α' : Sort w<VAR>DecidableEq α'<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>g : α' → β<VAR>f : α → α'<VAR>i : α'<VAR>a : β<VAR>h : ∀ (x : α), f x ≠ i<GOAL>Function.update g i a ∘ f = g ∘ f
<VAR>α : Sort u<VAR>β : α → Sort v<VAR>α' : Sort w<VAR>DecidableEq α<VAR>DecidableEq α'<VAR>g : (a : α) → β a<VAR>f : α' → α<VAR>hf : Function.Injective f<VAR>i : α'<VAR>a : β (f i)<GOAL>(fun j => Function.update g (f i) a (f j)) = Function.update (fun i => g (f i)) i a
<VAR>α : Sort u<VAR>α' : Sort w<VAR>DecidableEq α<VAR>DecidableEq α'<VAR>β : Sort u_1<VAR>g : α' → β<VAR>f : α → α'<VAR>hf : Function.Injective f<VAR>i : α<VAR>a : β<GOAL>Function.update g (f i) a ∘ f = Function.update (g ∘ f) i a
<VAR>ι : Sort u_1<VAR>DecidableEq ι<VAR>α : ι → Sort u_2<VAR>β : ι → Sort u_3<VAR>f : (i : ι) → α i → β i<VAR>g : (i : ι) → α i<VAR>i : ι<VAR>v : α i<VAR>j : ι<GOAL>f j (Function.update g i v j) = Function.update (fun k => f k (g k)) i (f i v) j
<VAR>ι : Sort u_1<VAR>DecidableEq ι<VAR>α : ι → Sort u_2<VAR>β : ι → Sort u_3<VAR>γ : ι → Sort u_4<VAR>f : (i : ι) → α i → β i → γ i<VAR>g : (i : ι) → α i<VAR>h : (i : ι) → β i<VAR>i : ι<VAR>v : α i<VAR>w : β i<VAR>j : ι<GOAL>f j (Function.update g i v j) (Function.update h i w j) = Function.update (fun k => f k (g k) (h k)) i (f i v w) j
<VAR>α : Sort u<VAR>β : α → Sort v<VAR>DecidableEq α<VAR>P : ⦃a : α⦄ → β a → Prop<VAR>f : (a : α) → β a<VAR>a' : α<VAR>v : β a'<VAR>a : α<GOAL>P (Function.update f a' v a) ↔ a = a' ∧ P v ∨ a ≠ a' ∧ P (f a)
<VAR>α : Sort u<VAR>DecidableEq α<VAR>α' : Sort u_1<VAR>β : Sort u_2<VAR>f : α' → β<VAR>g : α → α'<VAR>i : α<VAR>v : α'<GOAL>f ∘ Function.update g i v = Function.update (f ∘ g) i (f v)
<VAR>α : Sort u_2<VAR>DecidableEq α<VAR>β : α → Sort u_1<VAR>a b : α<VAR>h : a ≠ b<VAR>v : β a<VAR>w : β b<VAR>f : (a : α) → β a<GOAL>Function.update (Function.update f a v) b w = Function.update (Function.update f b w) a v
<VAR>α : Sort u_2<VAR>DecidableEq α<VAR>β : α → Sort u_1<VAR>a : α<VAR>v w : β a<VAR>f : (a : α) → β a<GOAL>Function.update (Function.update f a v) a w = Function.update f a w
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<VAR>g : α → γ<VAR>e' : β → γ<VAR>b : β<VAR>Decidable (∃ a, f a = b)<GOAL>Function.extend f g e' b = if h : ∃ a, f a = b then g (Classical.choose h) else e' b
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>g : α → γ<GOAL>Function.FactorsThrough g f
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<VAR>g : α → γ<VAR>hf : Function.FactorsThrough g f<VAR>e' : β → γ<VAR>a : α<GOAL>Function.extend f g e' (f a) = g a
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>g : α → γ<VAR>e' : β → γ<VAR>a : α<GOAL>Function.extend f g e' (f a) = g a
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<VAR>g : α → γ<VAR>e' : β → γ<VAR>b : β<VAR>hb : ¬∃ a, f a = b<GOAL>Function.extend f g e' b = e' b
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<VAR>g : α → γ<VAR>Nonempty γ<GOAL>Function.FactorsThrough g f ↔ ∃ e, g = e ∘ f
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>δ : Sort u_4<VAR>g : α → γ<VAR>F : γ → δ<VAR>f : α → β<VAR>e' : β → γ<VAR>b : β<GOAL>F (Function.extend f g e' b) = Function.extend f (F ∘ g) (F ∘ e') b
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>e' : β → γ<GOAL>Function.Injective fun g => Function.extend f g e'
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<VAR>g : α → γ<VAR>e' : β → γ<VAR>hf : Function.FactorsThrough g f<GOAL>Function.extend f g e' ∘ f = g
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>g : α → γ<VAR>e' : β → γ<GOAL>Function.extend f g e' ∘ f = g
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>g₀ : β → γ<GOAL>Function.Surjective fun g => g ∘ f
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<VAR>Nonempty γ<VAR>hf : Function.Injective f<GOAL>Function.Surjective fun g => g ∘ f
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>f : α → β<VAR>hf : Function.Bijective f<GOAL>Function.Bijective fun g => g ∘ f
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<GOAL>Function.FactorsThrough f f
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>δ : Sort u_4<VAR>f : α → β<VAR>g : α → γ<VAR>h : Function.FactorsThrough g f<VAR>g' : γ → δ<GOAL>Function.FactorsThrough (g' ∘ g) f
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>δ : Sort u_4<VAR>f : α → β<VAR>g : α → γ<VAR>h : Function.FactorsThrough g f<VAR>g' : δ → α<GOAL>Function.FactorsThrough (g ∘ g') (f ∘ g')
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<GOAL>Function.uncurry f = fun p => f p.fst p.snd
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β → γ<VAR>x : α<VAR>y : β<GOAL>Function.uncurry f (x, y) = f x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α × β → γ<VAR>x : α<VAR>y : β<GOAL>Function.curry f x y = f (x, y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>f : α → β → γ<VAR>g : γ → δ<GOAL>Function.uncurry (Function.bicompr g f) = g ∘ Function.uncurry f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ε : Type u_5<VAR>f : γ → δ → ε<VAR>g : α → γ<VAR>h : β → δ<GOAL>Function.uncurry (Function.bicompl f g h) = Function.uncurry f ∘ Prod.map g h
<VAR>α : Sort u<VAR>f : α → α<VAR>h : Function.Involutive f<GOAL>f ∘ f = id
<VAR>α : Sort u<VAR>f : α → α<VAR>h : Function.Involutive f<GOAL>Function.LeftInverse f f
<VAR>α : Sort u<VAR>f : α → α<VAR>h : Function.Involutive f<GOAL>Function.RightInverse f f
<VAR>α : Sort u<VAR>f : α → α<VAR>h : Function.Involutive f<GOAL>Function.Injective f
<VAR>α : Sort u<VAR>f : α → α<VAR>h : Function.Involutive f<GOAL>Function.Surjective f
<VAR>α : Sort u<VAR>f : α → α<VAR>h : Function.Involutive f<GOAL>Function.Bijective f
<VAR>α : Sort u<VAR>f : α → α<VAR>h : Function.Involutive f<VAR>P : Prop<VAR>Decidable P<VAR>x : α<GOAL>f (if P then x else f x) = if ¬P then x else f x