ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>e : α ≃ β<VAR>x : β<VAR>y : α<GOAL>y = e.symm x ↔ e y = x
<VAR>α : Sort u<VAR>β : Sort v<VAR>e : α ≃ β<GOAL>e.symm.symm = e
<VAR>α : Sort u<VAR>β : Sort v<GOAL>Function.Bijective Equiv.symm
<VAR>α : Sort u<VAR>β : Sort v<VAR>e : α ≃ β<GOAL>e.trans (Equiv.refl β) = e
<VAR>α : Sort u<GOAL>(Equiv.refl α).symm = Equiv.refl α
<VAR>α : Sort u<VAR>β : Sort v<VAR>e : α ≃ β<GOAL>(Equiv.refl α).trans e = e
<VAR>α : Sort u<VAR>β : Sort v<VAR>e : α ≃ β<GOAL>e.symm.trans e = Equiv.refl β
<VAR>α : Sort u<VAR>β : Sort v<VAR>e : α ≃ β<GOAL>e.trans e.symm = Equiv.refl α
<VAR>α : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>δ : Sort u_1<VAR>ab : α ≃ β<VAR>bc : β ≃ γ<VAR>cd : γ ≃ δ<GOAL>(ab.trans bc).trans cd = ab.trans (bc.trans cd)
<VAR>α : Sort u<VAR>β : Sort v<VAR>f : α ≃ β<GOAL>Function.LeftInverse ⇑f.symm ⇑f
<VAR>α : Sort u<VAR>β : Sort v<VAR>f : α ≃ β<GOAL>Function.RightInverse ⇑f.symm ⇑f
<VAR>α : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>e : α ≃ β<VAR>f : β → γ<GOAL>Function.Injective (f ∘ ⇑e) ↔ Function.Injective f
<VAR>α : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>f : α → β<VAR>e : β ≃ γ<GOAL>Function.Injective (⇑e ∘ f) ↔ Function.Injective f
<VAR>α : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>e : α ≃ β<VAR>f : β → γ<GOAL>Function.Surjective (f ∘ ⇑e) ↔ Function.Surjective f
<VAR>α : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>f : α → β<VAR>e : β ≃ γ<GOAL>Function.Surjective (⇑e ∘ f) ↔ Function.Surjective f
<VAR>α : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>e : α ≃ β<VAR>f : β → γ<GOAL>Function.Bijective (f ∘ ⇑e) ↔ Function.Bijective f
<VAR>α : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>f : α → β<VAR>e : β ≃ γ<GOAL>Function.Bijective (⇑e ∘ f) ↔ Function.Bijective f
<VAR>α : Sort u_1<VAR>β : Sort u_2<GOAL>(Equiv.refl α).equivCongr (Equiv.refl β) = Equiv.refl (α ≃ β)
<VAR>α : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>δ : Sort u_1<VAR>ab : α ≃ β<VAR>cd : γ ≃ δ<GOAL>(ab.equivCongr cd).symm = ab.symm.equivCongr cd.symm
<VAR>α : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>δ : Sort u_1<VAR>ε : Sort u_2<VAR>ζ : Sort u_3<VAR>ab : α ≃ β<VAR>de : δ ≃ ε<VAR>bc : β ≃ γ<VAR>ef : ε ≃ ζ<GOAL>(ab.equivCongr de).trans (bc.equivCongr ef) = (ab.trans bc).equivCongr (de.trans ef)
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>bg : β ≃ γ<VAR>e : α ≃ β<GOAL>((Equiv.refl α).equivCongr bg) e = e.trans bg
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>ab e : α ≃ β<GOAL>(ab.equivCongr (Equiv.refl β)) e = ab.symm.trans e
<VAR>α : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>δ : Sort u_1<VAR>ab : α ≃ β<VAR>cd : γ ≃ δ<VAR>e : α ≃ γ<VAR>x : β<GOAL>((ab.equivCongr cd) e) x = cd (e (ab.symm x))
<VAR>α' : Type u_1<VAR>β' : Type u_2<VAR>e : α' ≃ β'<VAR>p : Equiv.Perm α'<GOAL>e.permCongr p = (e.symm.trans p).trans e
<VAR>α' : Type u_1<VAR>β' : Type u_2<VAR>e : α' ≃ β'<GOAL>e.permCongr (Equiv.refl α') = Equiv.refl β'
<VAR>α' : Type u_1<VAR>β' : Type u_2<VAR>e : α' ≃ β'<GOAL>e.permCongr.symm = e.symm.permCongr
<VAR>α' : Type u_1<VAR>β' : Type u_2<VAR>e : α' ≃ β'<VAR>p : Equiv.Perm α'<VAR>x : β'<GOAL>(e.permCongr p) x = e (p (e.symm x))
<VAR>α' : Type u_1<VAR>β' : Type u_2<VAR>e : α' ≃ β'<VAR>p : Equiv.Perm β'<VAR>x : α'<GOAL>(e.permCongr.symm p) x = e.symm (p (e x))
<VAR>α' : Type u_1<VAR>β' : Type u_2<VAR>e : α' ≃ β'<VAR>p p' : Equiv.Perm α'<GOAL>Equiv.trans (e.permCongr p) (e.permCongr p') = e.permCongr (Equiv.trans p p')
<VAR>α : Type v<GOAL>⇑Equiv.ulift = ULift.down
<VAR>α : Sort u<GOAL>⇑Equiv.plift = PLift.down
<VAR>α₁ : Sort u_1<VAR>β₁ : Sort u_2<VAR>α₂ : Sort u_3<VAR>β₂ : Sort u_4<VAR>e₁ : α₁ ≃ α₂<VAR>e₂ : β₁ ≃ β₂<VAR>f : α₁ → β₁<GOAL>∀ (a : α₂), (e₁.arrowCongr e₂) f a = (⇑e₂ ∘ f ∘ ⇑e₁.symm) a
<VAR>α₁ : Sort u_1<VAR>β₁ : Sort u_2<VAR>γ₁ : Sort u_3<VAR>α₂ : Sort u_4<VAR>β₂ : Sort u_5<VAR>γ₂ : Sort u_6<VAR>ea : α₁ ≃ α₂<VAR>eb : β₁ ≃ β₂<VAR>ec : γ₁ ≃ γ₂<VAR>f : α₁ → β₁<VAR>g : β₁ → γ₁<GOAL>(ea.arrowCongr ec) (g ∘ f) = (eb.arrowCongr ec) g ∘ (ea.arrowCongr eb) f
<VAR>α : Sort u_1<VAR>β : Sort u_2<GOAL>(Equiv.refl α).arrowCongr (Equiv.refl β) = Equiv.refl (α → β)
<VAR>α₁ : Sort u_1<VAR>α₂ : Sort u_2<VAR>α₃ : Sort u_3<VAR>β₁ : Sort u_4<VAR>β₂ : Sort u_5<VAR>β₃ : Sort u_6<VAR>e₁ : α₁ ≃ α₂<VAR>e₁' : β₁ ≃ β₂<VAR>e₂ : α₂ ≃ α₃<VAR>e₂' : β₂ ≃ β₃<GOAL>(e₁.trans e₂).arrowCongr (e₁'.trans e₂') = (e₁.arrowCongr e₁').trans (e₂.arrowCongr e₂')
<VAR>α₁ : Sort u_1<VAR>α₂ : Sort u_2<VAR>β₁ : Sort u_3<VAR>β₂ : Sort u_4<VAR>e₁ : α₁ ≃ α₂<VAR>e₂ : β₁ ≃ β₂<GOAL>(e₁.arrowCongr e₂).symm = e₁.symm.arrowCongr e₂.symm
<VAR>α₁ : Type u_1<VAR>β₁ : Type u_2<VAR>α₂ : Type u_3<VAR>β₂ : Type u_4<VAR>hα : α₁ ≃ α₂<VAR>hβ : β₁ ≃ β₂<VAR>f : α₁ → β₁<GOAL>∀ (a : α₂), (hα.arrowCongr' hβ) f a = hβ (f (hα.symm a))
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>(Equiv.refl α).arrowCongr' (Equiv.refl β) = Equiv.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₁ : α₁ ≃ α₂<VAR>e₁' : β₁ ≃ β₂<VAR>e₂ : α₂ ≃ α₃<VAR>e₂' : β₂ ≃ β₃<GOAL>(e₁.trans e₂).arrowCongr' (e₁'.trans e₂') = (e₁.arrowCongr' e₁').trans (e₂.arrowCongr' e₂')
<VAR>α₁ : Type u_1<VAR>α₂ : Type u_2<VAR>β₁ : Type u_3<VAR>β₂ : Type u_4<VAR>e₁ : α₁ ≃ α₂<VAR>e₂ : β₁ ≃ β₂<GOAL>(e₁.arrowCongr' e₂).symm = e₁.symm.arrowCongr' e₂.symm
<VAR>α : Sort u<VAR>β : Sort v<VAR>e : α ≃ β<VAR>f : α → α<GOAL>∀ (a : β), e.conj f a = e (f (e.symm a))
<VAR>α : Sort u<GOAL>(Equiv.refl α).conj = Equiv.refl (α → α)
<VAR>α : Sort u<VAR>β : Sort v<VAR>e : α ≃ β<GOAL>e.conj.symm = e.symm.conj
<VAR>α : Sort u<VAR>β : Sort v<VAR>γ : Sort w<VAR>e₁ : α ≃ β<VAR>e₂ : β ≃ γ<GOAL>(e₁.trans e₂).conj = e₁.conj.trans e₂.conj
<VAR>α : Sort u<VAR>β : Sort v<VAR>e : α ≃ β<VAR>f₁ f₂ : α → α<GOAL>e.conj (f₁ ∘ f₂) = e.conj f₁ ∘ e.conj f₂
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>e : α ≃ β<VAR>f : β → γ<VAR>g : α → γ<GOAL>f = g ∘ ⇑e.symm ↔ f ∘ ⇑e = g
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>e : α ≃ β<VAR>f : β → γ<VAR>g : α → γ<GOAL>g ∘ ⇑e.symm = f ↔ g = f ∘ ⇑e
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>e : α ≃ β<VAR>f : γ → α<VAR>g : γ → β<GOAL>f = ⇑e.symm ∘ g ↔ ⇑e ∘ f = g
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>γ : Sort u_3<VAR>e : α ≃ β<VAR>f : γ → α<VAR>g : γ → β<GOAL>⇑e.symm ∘ g = f ↔ g = ⇑e ∘ f
<VAR>α : Sort u<VAR>Unique α<VAR>β : α → Sort u_1<GOAL>⇑(Equiv.piUnique β) = fun f => f default
<VAR>α : Sort u<VAR>Unique α<VAR>β : α → Sort u_1<GOAL>⇑(Equiv.piUnique β).symm = uniqueElim
<VAR>α : Sort u<VAR>β : Sort u_1<VAR>Unique α<GOAL>⇑(Equiv.funUnique α β).symm = uniqueElim
<VAR>α : Sort u<VAR>β : Sort u_1<VAR>Unique α<GOAL>⇑(Equiv.funUnique α β) = fun f => f default
<VAR>α : Type u_2<VAR>β : α → Type u_1<VAR>a : (i : α) × β i<GOAL>(Equiv.psigmaEquivSigma β).symm a = ⟨a.fst, a.snd⟩
<VAR>α : Type u_2<VAR>β : α → Type u_1<VAR>a : (i : α) ×' β i<GOAL>(Equiv.psigmaEquivSigma β) a = ⟨a.fst, a.snd⟩
<VAR>α : Sort u_2<VAR>β : α → Sort u_1<VAR>a : (i : α) ×' β i<GOAL>(Equiv.psigmaEquivSigmaPLift β) a = ⟨{ down := a.fst }, { down := a.snd }⟩
<VAR>α : Sort u_2<VAR>β : α → Sort u_1<VAR>a : (i : PLift α) × PLift (β i.down)<GOAL>(Equiv.psigmaEquivSigmaPLift β).symm a = ⟨a.fst.down, a.snd.down⟩
<VAR>α : Sort u<VAR>β₁ : α → Sort u_1<VAR>β₂ : α → Sort u_2<VAR>F : (a : α) → β₁ a ≃ β₂ a<VAR>a : (a : α) ×' β₁ a<GOAL>(Equiv.psigmaCongrRight F) a = ⟨a.fst, (F a.fst) a.snd⟩
<VAR>α : Sort u_4<VAR>β₁ : α → Sort u_1<VAR>β₂ : α → Sort u_2<VAR>β₃ : α → Sort u_3<VAR>F : (a : α) → β₁ a ≃ β₂ a<VAR>G : (a : α) → β₂ a ≃ β₃ a<GOAL>(Equiv.psigmaCongrRight F).trans (Equiv.psigmaCongrRight G) = Equiv.psigmaCongrRight fun a => (F a).trans (G a)
<VAR>α : Sort u_3<VAR>β₁ : α → Sort u_1<VAR>β₂ : α → Sort u_2<VAR>F : (a : α) → β₁ a ≃ β₂ a<GOAL>(Equiv.psigmaCongrRight F).symm = Equiv.psigmaCongrRight fun a => (F a).symm
<VAR>α : Sort u_2<VAR>β : α → Sort u_1<GOAL>(Equiv.psigmaCongrRight fun a => Equiv.refl (β a)) = Equiv.refl ((a : α) ×' β a)
<VAR>α : Type u_3<VAR>β₁ : α → Type u_1<VAR>β₂ : α → Type u_2<VAR>F : (a : α) → β₁ a ≃ β₂ a<VAR>a : (a : α) × β₁ a<GOAL>(Equiv.sigmaCongrRight F) a = ⟨a.fst, (F a.fst) a.snd⟩
<VAR>α : Type u_4<VAR>β₁ : α → Type u_1<VAR>β₂ : α → Type u_2<VAR>β₃ : α → Type u_3<VAR>F : (a : α) → β₁ a ≃ β₂ a<VAR>G : (a : α) → β₂ a ≃ β₃ a<GOAL>(Equiv.sigmaCongrRight F).trans (Equiv.sigmaCongrRight G) = Equiv.sigmaCongrRight fun a => (F a).trans (G a)
<VAR>α : Type u_3<VAR>β₁ : α → Type u_1<VAR>β₂ : α → Type u_2<VAR>F : (a : α) → β₁ a ≃ β₂ a<GOAL>(Equiv.sigmaCongrRight F).symm = Equiv.sigmaCongrRight fun a => (F a).symm
<VAR>α : Type u_2<VAR>β : α → Type u_1<GOAL>(Equiv.sigmaCongrRight fun a => Equiv.refl (β a)) = Equiv.refl ((a : α) × β a)
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>F G : (a : α) → Equiv.Perm (β a)<GOAL>Equiv.trans (Equiv.Perm.sigmaCongrRight F) (Equiv.Perm.sigmaCongrRight G) = Equiv.Perm.sigmaCongrRight fun a => Equiv.trans (F a) (G a)
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>F : (a : α) → Equiv.Perm (β a)<GOAL>Equiv.symm (Equiv.Perm.sigmaCongrRight F) = Equiv.Perm.sigmaCongrRight fun a => Equiv.symm (F a)
<VAR>α : Type u_1<VAR>β : α → Type u_2<GOAL>(Equiv.Perm.sigmaCongrRight fun a => Equiv.refl (β a)) = Equiv.refl ((a : α) × β a)
<VAR>α₁ : Type u_1<VAR>α₂ : Type u_2<VAR>β : α₂ → Type u_3<VAR>e : α₁ ≃ α₂<VAR>a : (a : α₁) × β (e a)<GOAL>e.sigmaCongrLeft a = ⟨e a.fst, a.snd⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : (_ : α) × β<GOAL>(Equiv.sigmaEquivProd α β) a = (a.fst, a.snd)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α × β<GOAL>(Equiv.sigmaEquivProd α β).symm a = ⟨a.fst, a.snd⟩
<VAR>α : Sort u<VAR>β : Sort v<VAR>q : β → Prop<VAR>e : α ≃ β<GOAL>(∀ (a : α), q (e a)) ↔ ∀ (b : β), q b
<VAR>α : Sort u<VAR>β : Sort v<VAR>p : α → Prop<VAR>e : α ≃ β<GOAL>(∀ (a : α), p a) ↔ ∀ (b : β), p (e.symm b)
<VAR>α : Sort u<VAR>β : Sort v<VAR>p : α → Prop<VAR>q : β → Prop<VAR>e : α ≃ β<VAR>h : ∀ (a : α), p a ↔ q (e a)<GOAL>(∀ (a : α), p a) ↔ ∀ (b : β), q b
<VAR>α : Sort u<VAR>β : Sort v<VAR>p : α → Prop<VAR>q : β → Prop<VAR>e : α ≃ β<VAR>h : ∀ (b : β), p (e.symm b) ↔ q b<GOAL>(∀ (a : α), p a) ↔ ∀ (b : β), q b
<VAR>α : Sort u<VAR>β : Sort v<VAR>q : β → Prop<VAR>e : α ≃ β<GOAL>(∃ a, q (e a)) ↔ ∃ b, q b
<VAR>α : Sort u<VAR>β : Sort v<VAR>p : α → Prop<VAR>e : α ≃ β<GOAL>(∃ a, p a) ↔ ∃ b, p (e.symm b)
<VAR>α : Sort u<VAR>β : Sort v<VAR>p : α → Prop<VAR>q : β → Prop<VAR>e : α ≃ β<VAR>h : ∀ (a : α), p a ↔ q (e a)<GOAL>(∃ a, p a) ↔ ∃ b, q b
<VAR>α : Sort u<VAR>β : Sort v<VAR>p : α → Prop<VAR>q : β → Prop<VAR>e : α ≃ β<VAR>h : ∀ (b : β), p (e.symm b) ↔ q b<GOAL>(∃ a, p a) ↔ ∃ b, q b
<VAR>α : Sort u<VAR>β : Sort v<VAR>q : β → Prop<VAR>e : α ≃ β<GOAL>(∃! a, q (e a)) ↔ ∃! b, q b
<VAR>α : Sort u<VAR>β : Sort v<VAR>p : α → Prop<VAR>e : α ≃ β<GOAL>(∃! a, p a) ↔ ∃! b, p (e.symm b)
<VAR>α : Sort u<VAR>β : Sort v<VAR>p : α → Prop<VAR>q : β → Prop<VAR>e : α ≃ β<VAR>h : ∀ (a : α), p a ↔ q (e a)<GOAL>(∃! a, p a) ↔ ∃! b, q b
<VAR>α : Sort u<VAR>β : Sort v<VAR>p : α → Prop<VAR>q : β → Prop<VAR>e : α ≃ β<VAR>h : ∀ (b : β), p (e.symm b) ↔ q b<GOAL>(∃! a, p a) ↔ ∃! b, q b
<VAR>α₁ : Sort u_1<VAR>α₂ : Sort u_2<VAR>β₁ : Sort u_3<VAR>β₂ : Sort u_4<VAR>p : α₁ → β₁ → Prop<VAR>q : α₂ → β₂ → Prop<VAR>eα : α₁ ≃ α₂<VAR>eβ : β₁ ≃ β₂<VAR>h : ∀ {x : α₁} {y : β₁}, p x y ↔ q (eα x) (eβ y)<GOAL>(∀ (x : α₁) (y : β₁), p x y) ↔ ∀ (x : α₂) (y : β₂), q x y
<VAR>α₁ : Sort u_1<VAR>α₂ : Sort u_2<VAR>β₁ : Sort u_3<VAR>β₂ : Sort u_4<VAR>p : α₁ → β₁ → Prop<VAR>q : α₂ → β₂ → Prop<VAR>eα : α₁ ≃ α₂<VAR>eβ : β₁ ≃ β₂<VAR>h : ∀ {x : α₂} {y : β₂}, p (eα.symm x) (eβ.symm y) ↔ q x y<GOAL>(∀ (x : α₁) (y : β₁), p x y) ↔ ∀ (x : α₂) (y : β₂), q x y
<VAR>α₁ : Sort u_1<VAR>α₂ : Sort u_2<VAR>β₁ : Sort u_3<VAR>β₂ : Sort u_4<VAR>γ₁ : Sort u_5<VAR>γ₂ : Sort u_6<VAR>p : α₁ → β₁ → γ₁ → Prop<VAR>q : α₂ → β₂ → γ₂ → Prop<VAR>eα : α₁ ≃ α₂<VAR>eβ : β₁ ≃ β₂<VAR>eγ : γ₁ ≃ γ₂<VAR>h : ∀ {x : α₁} {y : β₁} {z : γ₁}, p x y z ↔ q (eα x) (eβ y) (eγ z)<GOAL>(∀ (x : α₁) (y : β₁) (z : γ₁), p x y z) ↔ ∀ (x : α₂) (y : β₂) (z : γ₂), q x y z
<VAR>α₁ : Sort u_1<VAR>α₂ : Sort u_2<VAR>β₁ : Sort u_3<VAR>β₂ : Sort u_4<VAR>γ₁ : Sort u_5<VAR>γ₂ : Sort u_6<VAR>p : α₁ → β₁ → γ₁ → Prop<VAR>q : α₂ → β₂ → γ₂ → Prop<VAR>eα : α₁ ≃ α₂<VAR>eβ : β₁ ≃ β₂<VAR>eγ : γ₁ ≃ γ₂<VAR>h : ∀ {x : α₂} {y : β₂} {z : γ₂}, p (eα.symm x) (eβ.symm y) (eγ.symm z) ↔ q x y z<GOAL>(∀ (x : α₁) (y : β₁) (z : γ₁), p x y z) ↔ ∀ (x : α₂) (y : β₂) (z : γ₂), q x y z
<VAR>α : Sort u<VAR>β : Sort v<VAR>f : α → β<VAR>hf : Function.Bijective f<GOAL>∀ (a : α), (Equiv.ofBijective f hf) a = f a
<VAR>α : Sort u<VAR>β : Sort v<VAR>f : α → β<VAR>hf : Function.Bijective f<VAR>x : β<GOAL>f ((Equiv.ofBijective f hf).symm x) = x
<VAR>α : Sort u<VAR>β : Sort v<VAR>f : α → β<VAR>hf : Function.Bijective f<VAR>x : α<GOAL>(Equiv.ofBijective f hf).symm (f x) = x
<VAR>α : Sort u<VAR>β : Sort v<VAR>ra : α → α → Prop<VAR>rb : β → β → Prop<VAR>e : α ≃ β<VAR>eq : ∀ (a₁ a₂ : α), ra a₁ a₂ ↔ rb (e a₁) (e a₂)<VAR>a : α<GOAL>(Quot.congr e eq) (Quot.mk ra a) = Quot.mk rb (e a)
<VAR>α : Sort u<VAR>β : Sort v<VAR>ra : Setoid α<VAR>rb : Setoid β<VAR>e : α ≃ β<VAR>eq : ∀ (a₁ a₂ : α), Setoid.r a₁ a₂ ↔ Setoid.r (e a₁) (e a₂)<VAR>a : α<GOAL>(Quotient.congr e eq) ⟦a⟧ = ⟦e a⟧
<VAR>α : Type u_1<VAR>Encodable α<GOAL>Encodable.encode [] = 0
<VAR>α : Type u_1<VAR>Encodable α<VAR>a : α<VAR>l : List α<GOAL>Encodable.encode (a :: l) = (Nat.pair (Encodable.encode a) (Encodable.encode l)).succ
<VAR>α : Type u_1<VAR>Encodable α<GOAL>Encodable.decode 0 = some []
<VAR>α : Type u_1<VAR>Encodable α<VAR>v : ℕ<GOAL>Encodable.decode v.succ = Seq.seq ((fun x x_1 => x :: x_1) <$> Encodable.decode (Nat.unpair v).1) fun x => Encodable.decode (Nat.unpair v).2
<VAR>α : Type u_1<VAR>Encodable α<VAR>l : List α<GOAL>l.length ≤ Encodable.encode l
<VAR>α : Type u_1<VAR>Encodable α<GOAL>IsLinearOrder α Encodable.enle
<VAR>α : Type u_2<VAR>Fintype α<VAR>Encodable α<VAR>x : α<GOAL>x ∈ Encodable.sortedUniv α
<VAR>α : Type u_2<VAR>Fintype α<VAR>Encodable α<GOAL>(Encodable.sortedUniv α).length = Fintype.card α
<VAR>α : Type u_2<VAR>Fintype α<VAR>Encodable α<GOAL>(Encodable.sortedUniv α).Nodup
<VAR>α : Type u_2<VAR>Fintype α<VAR>Encodable α<VAR>DecidableEq α<GOAL>(Encodable.sortedUniv α).toFinset = Finset.univ
<VAR>α : Type u_1<VAR>Denumerable α<VAR>n : ℕ<GOAL>∃ a ∈ Encodable.decodeList n, Encodable.encodeList a = n
<VAR>α : Type u_1<VAR>Denumerable α<GOAL>Denumerable.ofNat (List α) 0 = []
<VAR>α : Type u_1<VAR>Denumerable α<VAR>v : ℕ<GOAL>Denumerable.ofNat (List α) v.succ = Denumerable.ofNat α (Nat.unpair v).1 :: Denumerable.ofNat (List α) (Nat.unpair v).2
<VAR>l : List ℕ<VAR>n : ℕ<GOAL>Denumerable.lower (Denumerable.raise l n) n = l
<VAR>l : List ℕ<VAR>n : ℕ<GOAL>List.Sorted (fun x x_1 => x ≤ x_1) (n :: l) → Denumerable.raise (Denumerable.lower l n) n = l
<VAR>l : List ℕ<VAR>n : ℕ<GOAL>List.Chain (fun x x_1 => x ≤ x_1) n (Denumerable.raise l n)
<VAR>l : List ℕ<VAR>n : ℕ<GOAL>List.Sorted (fun x x_1 => x ≤ x_1) (Denumerable.raise l n)
<VAR>l : List ℕ<VAR>n : ℕ<GOAL>Denumerable.lower' (Denumerable.raise' l n) n = l
<VAR>l : List ℕ<VAR>n : ℕ<GOAL>(∀ m ∈ l, n ≤ m) → List.Sorted (fun x x_1 => x < x_1) l → Denumerable.raise' (Denumerable.lower' l n) n = l
<VAR>l : List ℕ<VAR>m n : ℕ<GOAL>m < n → List.Chain (fun x x_1 => x < x_1) m (Denumerable.raise' l n)
<VAR>l : List ℕ<VAR>n : ℕ<GOAL>List.Sorted (fun x x_1 => x < x_1) (Denumerable.raise' l n)
<VAR>α : Fin 2 → Type u<GOAL>⇑(piFinTwoEquiv α) = fun f => (f 0, f 1)
<VAR>α : Fin 2 → Type u<GOAL>⇑(piFinTwoEquiv α).symm = fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
<VAR>α : Fin 2 → Type u<VAR>s : Set (α 0)<VAR>t : Set (α 1)<GOAL>(fun f => (f 0, f 1)) ⁻¹' s ×ˢ t = Set.univ.pi (Fin.cons s (Fin.cons t finZeroElim))
<VAR>α : Type u<VAR>s t : Set α<GOAL>(fun f => (f 0, f 1)) ⁻¹' s ×ˢ t = Set.univ.pi ![s, t]
<VAR>α β : Type u<GOAL>⇑(prodEquivPiFinTwo α β).symm = fun f => (f 0, f 1)
<VAR>α β : Type u<GOAL>⇑(prodEquivPiFinTwo α β) = fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
<VAR>α : Type u_1<GOAL>⇑(finTwoArrowEquiv α) = (piFinTwoEquiv fun x => α).toFun
<VAR>α : Type u_1<GOAL>⇑(finTwoArrowEquiv α).symm = fun x => ![x.1, x.2]
<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>(finSuccEquiv' i) i = none
<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>j : Fin n<GOAL>(finSuccEquiv' i) (i.succAbove j) = some j
<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>m : Fin n<VAR>h : m.castSucc < i<GOAL>(finSuccEquiv' i) m.castSucc = some m
<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>m : Fin n<VAR>h : i ≤ m.castSucc<GOAL>(finSuccEquiv' i) m.succ = some m
<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>(finSuccEquiv' i).symm none = i
<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>j : Fin n<GOAL>(finSuccEquiv' i).symm (some j) = i.succAbove j
<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>m : Fin n<VAR>h : m.castSucc < i<GOAL>(finSuccEquiv' i).symm (some m) = m.castSucc
<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>m : Fin n<VAR>h : i ≤ m.castSucc<GOAL>(finSuccEquiv' i).symm (some m) = m.succ
<VAR>n : ℕ<GOAL>(finSuccEquiv n) 0 = none
<VAR>n : ℕ<VAR>m : Fin n<GOAL>(finSuccEquiv n) m.succ = some m
<VAR>n : ℕ<GOAL>(finSuccEquiv n).symm none = 0
<VAR>n : ℕ<VAR>m : Fin n<GOAL>(finSuccEquiv n).symm (some m) = m.succ
<VAR>n : ℕ<GOAL>finSuccEquiv' 0 = finSuccEquiv n
<VAR>n : ℕ<VAR>i : Fin n<GOAL>(finSuccEquiv' (Fin.last n)) i.castSucc = some i
<VAR>n : ℕ<VAR>i : Fin (n + 1)<VAR>h : i ≠ Fin.last n<GOAL>(finSuccEquiv' (Fin.last n)) i = some (i.castLT ⋯)
<VAR>n : ℕ<VAR>i j : Fin (n + 1)<VAR>hi : i ≠ Fin.last n<VAR>hj : j ≠ i<GOAL>(finSuccEquiv' i) j = some ((i.castLT ⋯).predAbove j)
<VAR>n : ℕ<VAR>p : Fin (n + 1)<VAR>i : Fin n<GOAL>(finSuccAboveEquiv p) i = ⟨p.succAbove i, ⋯⟩
<VAR>n : ℕ<VAR>x : { x // x ≠ Fin.last n }<GOAL>(finSuccAboveEquiv (Fin.last n)).symm x = (↑x).castLT ⋯
<VAR>n : ℕ<VAR>i : Fin n<GOAL>finSuccEquivLast i.castSucc = some i
<VAR>n : ℕ<GOAL>finSuccEquivLast (Fin.last n) = none
<VAR>n : ℕ<VAR>i : Fin n<GOAL>finSuccEquivLast.symm (some i) = i.castSucc
<VAR>n : ℕ<GOAL>finSuccEquivLast.symm none = Fin.last n
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>i : Fin (n + 1)<GOAL>⇑(Equiv.piFinSuccAbove α i).symm = fun f => i.insertNth f.1 f.2
<VAR>n : ℕ<VAR>α : Fin (n + 1) → Type u<VAR>i : Fin (n + 1)<GOAL>⇑(Equiv.piFinSuccAbove α i) = fun f => (f i, i.removeNth f)
<VAR>n : ℕ<VAR>β : Type u<GOAL>⇑(Equiv.piFinSucc n β).symm = fun f => Fin.cons f.1 f.2
<VAR>n : ℕ<VAR>β : Type u<GOAL>⇑(Equiv.piFinSucc n β) = fun f => (f 0, Fin.tail f)
<VAR>n : ℕ<VAR>ι : Type u_1<VAR>e : Fin (n + 1) ↪ ι<GOAL>⇑((Equiv.embeddingFinSucc n ι) e).fst = ⇑e ∘ Fin.succ
<VAR>n : ℕ<VAR>ι : Type u_1<VAR>e : Fin (n + 1) ↪ ι<GOAL>↑((Equiv.embeddingFinSucc n ι) e).snd = e 0
<VAR>n : ℕ<VAR>ι : Type u_1<VAR>f : (e : Fin n ↪ ι) × { i // i ∉ Set.range ⇑e }<GOAL>⇑((Equiv.embeddingFinSucc n ι).symm f) = Fin.cons ↑f.snd ⇑f.fst
<VAR>n : ℕ<VAR>β : Type u<GOAL>⇑(Equiv.piFinCastSucc n β) = fun f => (f (Fin.last n), Fin.init f)
<VAR>n : ℕ<VAR>β : Type u<GOAL>⇑(Equiv.piFinCastSucc n β).symm = fun f => Fin.snoc f.2 f.1
<VAR>m n : ℕ<VAR>i : Fin m<GOAL>finSumFinEquiv (Sum.inl i) = Fin.castAdd n i
<VAR>m n : ℕ<VAR>i : Fin n<GOAL>finSumFinEquiv (Sum.inr i) = Fin.natAdd m i
<VAR>m n : ℕ<VAR>x : Fin m<GOAL>finSumFinEquiv.symm (Fin.castAdd n x) = Sum.inl x
<VAR>m n : ℕ<VAR>x : Fin n<GOAL>finSumFinEquiv.symm (Fin.natAdd m x) = Sum.inr x
<VAR>n : ℕ<GOAL>finSumFinEquiv.symm (Fin.last n) = Sum.inr 0
<VAR>m : ℕ<VAR>k : Fin m<VAR>n : ℕ<GOAL>finAddFlip (Fin.castAdd n k) = Fin.natAdd n k
<VAR>n : ℕ<VAR>k : Fin n<VAR>m : ℕ<GOAL>finAddFlip (Fin.natAdd m k) = Fin.castAdd m k
<VAR>m n k : ℕ<VAR>h : k < m<VAR>hk : k < m + n := ⋯<VAR>hnk : n + k < n + m := ⋯<GOAL>finAddFlip ⟨k, hk⟩ = ⟨n + k, hnk⟩
<GOAL>finRotate 0 = Equiv.refl (Fin 0)
<VAR>n : ℕ<GOAL>finRotate (n + 1) = finAddFlip.trans (finCongr ⋯)
<VAR>n k : ℕ<VAR>h : k < n<GOAL>(finRotate (n + 1)) ⟨k, ⋯⟩ = ⟨k + 1, ⋯⟩
<VAR>n : ℕ<GOAL>(finRotate (n + 1)) ⟨n, ⋯⟩ = ⟨0, ⋯⟩
<VAR>n : ℕ<GOAL>(finRotate (n + 1)) (Fin.last n) = 0
<VAR>n : ℕ<VAR>α : Type u_1<VAR>v : Fin n → α<VAR>a : α<GOAL>Fin.snoc v a = fun i => Fin.cons a v ((finRotate (n + 1)) i)
<GOAL>finRotate 1 = Equiv.refl (Fin 1)
<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>(finRotate (n + 1)) i = i + 1
<VAR>n : ℕ<GOAL>(finRotate n.succ) 0 = 1
<VAR>n : ℕ<VAR>i : Fin n.succ<VAR>h : i ≠ Fin.last n<GOAL>↑((finRotate (n + 1)) i) = ↑i + 1
<VAR>n : ℕ<VAR>i : Fin n.succ<GOAL>↑((finRotate n.succ) i) = if i = Fin.last n then 0 else ↑i + 1
<VAR>m n : ℕ<VAR>x : Fin (m * n)<GOAL>finProdFinEquiv.symm x = (x.divNat, x.modNat)
<VAR>m n : ℕ<VAR>x : Fin m × Fin n<GOAL>↑(finProdFinEquiv x) = ↑x.2 + n * ↑x.1
<VAR>n : ℕ<VAR>NeZero n<VAR>p : ℕ × Fin n<GOAL>n.divModEquiv.symm p = p.1 * n + ↑p.2
<VAR>n : ℕ<VAR>NeZero n<VAR>a : ℕ<GOAL>n.divModEquiv a = (a / n, ↑a)
<VAR>n : ℕ<VAR>NeZero n<VAR>a : ℤ<GOAL>(Int.divModEquiv n) a = (a / ↑n, ↑(a.natMod ↑n))
<VAR>n : ℕ<VAR>NeZero n<VAR>p : ℤ × Fin n<GOAL>(Int.divModEquiv n).symm p = p.1 * ↑n + ↑↑p.2
<VAR>n m : ℕ<VAR>h : n ≤ m<VAR>i : Fin n<GOAL>(Fin.castLEquiv h) i = ⟨Fin.castLE h i, ⋯⟩
<VAR>n m : ℕ<VAR>h : n ≤ m<VAR>i : { i // ↑i < n }<GOAL>(Fin.castLEquiv h).symm i = ⟨↑↑i, ⋯⟩
<VAR>α β : Type u<VAR>f : Type u → Type v<VAR>Functor f<VAR>LawfulFunctor f<VAR>h : α ≃ β<VAR>x : f α<GOAL>(Functor.mapEquiv f h) x = ⇑h <$> x
<VAR>α β : Type u<VAR>f : Type u → Type v<VAR>Functor f<VAR>LawfulFunctor f<VAR>h : α ≃ β<VAR>y : f β<GOAL>(Functor.mapEquiv f h).symm y = ⇑h.symm <$> y
<VAR>α : Type u<VAR>f : Type u → Type v<VAR>Functor f<VAR>LawfulFunctor f<GOAL>Functor.mapEquiv f (Equiv.refl α) = Equiv.refl (f α)
<VAR>α β : Type u<VAR>α' β' : Type v<VAR>F : Type u → Type v → Type w<VAR>Bifunctor F<VAR>LawfulBifunctor F<VAR>h : α ≃ β<VAR>h' : α' ≃ β'<VAR>x : F α α'<GOAL>(Bifunctor.mapEquiv F h h') x = bimap (⇑h) (⇑h') x
<VAR>α β : Type u<VAR>α' β' : Type v<VAR>F : Type u → Type v → Type w<VAR>Bifunctor F<VAR>LawfulBifunctor F<VAR>h : α ≃ β<VAR>h' : α' ≃ β'<VAR>y : F β β'<GOAL>(Bifunctor.mapEquiv F h h').symm y = bimap (⇑h.symm) (⇑h'.symm) y
<VAR>α : Type u<VAR>α' : Type v<VAR>F : Type u → Type v → Type w<VAR>Bifunctor F<VAR>LawfulBifunctor F<GOAL>Bifunctor.mapEquiv F (Equiv.refl α) (Equiv.refl α') = Equiv.refl (F α α')
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>F : Sort u_3<VAR>FunLike F Y X<VAR>EmbeddingLike F Y X<VAR>f : F<VAR>p : X → X → Prop<VAR>h : Pairwise p<GOAL>Pairwise (p on ⇑f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>F : Sort u_3<VAR>EquivLike F Y X<VAR>f : F<VAR>p : X → X → Prop<GOAL>Pairwise (p on ⇑f) ↔ Pairwise p
<VAR>α β : Type u<GOAL>Function.OfArity α β 0 = β
<VAR>α β : Type u<VAR>n : ℕ<GOAL>Function.OfArity α β n.succ = (α → Function.OfArity α β n)
<VAR>α : Type u<VAR>β : Type u<VAR>b : β<GOAL>Function.OfArity.const α b 0 = b
<VAR>α : Type u<VAR>β : Type u<VAR>b : β<VAR>n : ℕ<GOAL>Function.OfArity.const α b n.succ = fun x => Function.OfArity.const α b n
<VAR>α : Type u<VAR>β : Type u<VAR>b : β<VAR>n : ℕ<VAR>x : α<GOAL>Function.OfArity.const α b n.succ x = Function.OfArity.const α b n
<VAR>α β : Type u<VAR>n : ℕ<GOAL>Function.FromTypes (fun x => α) β = Function.OfArity α β n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<GOAL>∀ (a : Option α), e.optionCongr a = Option.map (⇑e) a
<VAR>α : Type u_1<GOAL>(Equiv.refl α).optionCongr = Equiv.refl (Option α)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<GOAL>e.optionCongr.symm = e.symm.optionCongr
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>e₁ : α ≃ β<VAR>e₂ : β ≃ γ<GOAL>e₁.optionCongr.trans e₂.optionCongr = (e₁.trans e₂).optionCongr
<VAR>α β : Type u<VAR>e : α ≃ β<GOAL>e.optionCongr = EquivFunctor.mapEquiv Option e
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : Option α ≃ Option β<VAR>x : α<VAR>h : ∃ x', e (some x) = some x'<GOAL>some (e.removeNone_aux x) = e (some x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : Option α ≃ Option β<VAR>x : α<VAR>h : e (some x) = none<GOAL>some (e.removeNone_aux x) = e none
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : Option α ≃ Option β<VAR>x : α<GOAL>e.symm.removeNone_aux (e.removeNone_aux x) = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : Option α ≃ Option β<GOAL>e.removeNone.symm = e.symm.removeNone
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : Option α ≃ Option β<VAR>x : α<VAR>h : ∃ x', e (some x) = some x'<GOAL>some (e.removeNone x) = e (some x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : Option α ≃ Option β<VAR>x : α<VAR>h : e (some x) = none<GOAL>some (e.removeNone x) = e none
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : Option α ≃ Option β<GOAL>e.symm none = none ↔ e none = none
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : Option α ≃ Option β<VAR>x : α<GOAL>some (e.removeNone x) = e none ↔ e.symm none = some x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>e : α ≃ β<GOAL>e.optionCongr.removeNone = e
<VAR>α : Type u_1<VAR>β : Type u_2<GOAL>Function.Injective Equiv.optionCongr