ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝⁴ : Monoid K<VAR>inst✝³ : (i : ι) → Group (G i)<VAR>inst✝² : Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Transversal φ<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (G i)<VAR>i : ι<VAR>w₁ : Word G<VAR>h₁ : H<VAR>hw₁ : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w₁.toList → g ∈ d.set i<VAR>w₂ : Word G<VAR>h₂ : H<VAR>hw₂ : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w₂.toList → g ∈ d.set i<VAR>h : w₁ = ((CoprodI.of ((φ i) h₁))⁻¹ * CoprodI.of ((φ i) h₂)) • w₂<GOAL>{ toWord := w₁, head := h₁, normalized := hw₁ } = { toWord := w₂, head := h₂, normalized := hw₂ }
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝⁴ : Monoid K<VAR>inst✝³ : (i : ι) → Group (G i)<VAR>inst✝² : Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Transversal φ<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (G i)<VAR>i : ι<VAR>h₁ : H<VAR>w₂ : Word G<VAR>h₂ : H<VAR>hw₂ : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w₂.toList → g ∈ d.set i<VAR>hw₁ : ∀ (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ (((CoprodI.of ((φ i) h₁))⁻¹ * CoprodI.of ((φ i) h₂)) • w₂).toList → g ∈ d.set i_1<GOAL>{ toWord := ((CoprodI.of ((φ i) h₁))⁻¹ * CoprodI.of ((φ i) h₂)) • w₂, head := h₁, normalized := hw₁ } = { toWord := w₂, head := h₂, normalized := hw₂ }
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝⁴ : Monoid K<VAR>inst✝³ : (i : ι) → Group (G i)<VAR>inst✝² : Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Transversal φ<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (G i)<VAR>i : ι<VAR>h₁ : H<VAR>w₂ : Word G<VAR>h₂ : H<VAR>hw₂ : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w₂.toList → g ∈ d.set i<VAR>hw₁✝ : ∀ (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ (((CoprodI.of ((φ i) h₁))⁻¹ * CoprodI.of ((φ i) h₂)) • w₂).toList → g ∈ d.set i_1<VAR>hw₁ : ∀ (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ (CoprodI.of ((φ i) (h₁⁻¹ * h₂)) • w₂).toList → g ∈ d.set i_1<GOAL>{ toWord := ((CoprodI.of ((φ i) h₁))⁻¹ * CoprodI.of ((φ i) h₂)) • w₂, head := h₁, normalized := hw₁✝ } = { toWord := w₂, head := h₂, normalized := hw₂ }
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝⁴ : Monoid K<VAR>inst✝³ : (i : ι) → Group (G i)<VAR>inst✝² : Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Transversal φ<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (G i)<VAR>i : ι<VAR>h₁ : H<VAR>w₂ : Word G<VAR>h₂ : H<VAR>hw₂ : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w₂.toList → g ∈ d.set i<VAR>hw₁✝ : ∀ (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ (((CoprodI.of ((φ i) h₁))⁻¹ * CoprodI.of ((φ i) h₂)) • w₂).toList → g ∈ d.set i_1<VAR>hw₁ : ∀ (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ (CoprodI.of ((φ i) (h₁⁻¹ * h₂)) • w₂).toList → g ∈ d.set i_1<VAR>this : h₁⁻¹ * h₂ = 1<GOAL>{ toWord := ((CoprodI.of ((φ i) h₁))⁻¹ * CoprodI.of ((φ i) h₂)) • w₂, head := h₁, normalized := hw₁✝ } = { toWord := w₂, head := h₂, normalized := hw₂ }
<VAR>ι : Type u_1<VAR>G : ι → Type u_2<VAR>H : Type u_3<VAR>K : Type u_4<VAR>inst✝⁴ : Monoid K<VAR>inst✝³ : (i : ι) → Group (G i)<VAR>inst✝² : Group H<VAR>φ : (i : ι) → H →* G i<VAR>d : Transversal φ<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → DecidableEq (G i)<VAR>i : ι<VAR>h₁ : H<VAR>w₂ : Word G<VAR>h₂ : H<VAR>hw₂ : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w₂.toList → g ∈ d.set i<VAR>hw₁✝ : ∀ (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ (((CoprodI.of ((φ i) h₁))⁻¹ * CoprodI.of ((φ i) h₂)) • w₂).toList → g ∈ d.set i_1<VAR>hw₁ : ∀ (i_1 : ι) (g : G i_1), ⟨i_1, g⟩ ∈ (CoprodI.of ((φ i) (h₁⁻¹ * h₂)) • w₂).toList → g ∈ d.set i_1<VAR>this : h₁ = h₂<GOAL>{ toWord := ((CoprodI.of ((φ i) h₁))⁻¹ * CoprodI.of ((φ i) h₂)) • w₂, head := h₁, normalized := hw₁✝ } = { toWord := w₂, head := h₂, normalized := hw₂ }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>𝓕 : Filter ι<VAR>a : α<GOAL>bliminf s cofinite p = {x | {n | p n ∧ x ∉ s n}.Finite}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>𝓕 : Filter ι<VAR>a : α<GOAL>(bliminf s cofinite p)ᶜ = {x | {n | p n ∧ x ∉ s n}.Finite}ᶜ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>𝓕 : Filter ι<VAR>a : α<GOAL>{x | {n | p n ∧ x ∈ (s n)ᶜ}.Infinite} = {x | {n | p n ∧ x ∉ s n}.Finite}ᶜ
<VAR>E : Type u_1<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace ℝ E<VAR>inst✝¹² : MeasurableSpace E<VAR>inst✝¹¹ : BorelSpace E<VAR>inst✝¹⁰ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝⁹ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : CompleteSpace F<VAR>s : Set E<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>inst✝¹ : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>b : Basis ι ℝ G<VAR>v : ι → G<GOAL>b.addHaar (parallelepiped v) = ENNReal.ofReal |b.det v|
<VAR>E : Type u_1<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace ℝ E<VAR>inst✝¹² : MeasurableSpace E<VAR>inst✝¹¹ : BorelSpace E<VAR>inst✝¹⁰ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝⁹ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : CompleteSpace F<VAR>s : Set E<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>inst✝¹ : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>b : Basis ι ℝ G<VAR>v : ι → G<VAR>this : FiniteDimensional ℝ G<GOAL>b.addHaar (parallelepiped v) = ENNReal.ofReal |b.det v|
<VAR>E : Type u_1<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace ℝ E<VAR>inst✝¹² : MeasurableSpace E<VAR>inst✝¹¹ : BorelSpace E<VAR>inst✝¹⁰ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝⁹ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : CompleteSpace F<VAR>s : Set E<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>inst✝¹ : MeasurableSpace G<VAR>inst✝ : BorelSpace G<VAR>b : Basis ι ℝ G<VAR>v : ι → G<VAR>this : FiniteDimensional ℝ G<VAR>A : parallelepiped v = ⇑((b.constr ℕ) v) '' parallelepiped ⇑b<GOAL>b.addHaar (parallelepiped v) = ENNReal.ofReal |b.det v|
<VAR>R : Type u_1<VAR>inst✝ : DivisionSemiring R<VAR>f : ArithmeticFunction R<VAR>n : ℕ<GOAL>(f.pdiv ↑ζ) n = f n
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>J : GrothendieckTopology C<VAR>R : Sheaf J RingCat<VAR>inst✝ : J.HasSheafCompose (forget₂ RingCat AddCommGrp)<VAR>M N : SheafOfModules R<VAR>s : M.sections<VAR>p : M ⟶ N<GOAL>N.unitHomEquiv (M.unitHomEquiv.symm s ≫ p) = N.unitHomEquiv (N.unitHomEquiv.symm (sectionsMap p s))
<VAR>α : Type u<VAR>a : α<VAR>n k : ℕ<GOAL>((replicate n a).rotate k).length = n
<VAR>α : Type u_2<VAR>n : ℕ<VAR>β : Type u_1<VAR>xs : Vector α n<VAR>ys : Vector β n<VAR>σ : Type<VAR>f : α → σ → σ × β<VAR>s₀ : σ<VAR>S : Set σ<VAR>h₀ : s₀ ∈ S<VAR>closure : ∀ (a : α), ∀ s ∈ S, (f a s).1 ∈ S<VAR>out : ∀ (a : α) (s s' : σ), s ∈ S → s' ∈ S → (f a s).2 = (f a s').2<GOAL>(mapAccumr f xs s₀).2 = map (fun x => (f x s₀).2) xs
<VAR>α : Type u_2<VAR>n : ℕ<VAR>β : Type u_1<VAR>xs : Vector α n<VAR>ys : Vector β n<VAR>σ : Type<VAR>f : α → σ → σ × β<VAR>s₀ : σ<VAR>S : Set σ<VAR>h₀ : s₀ ∈ S<VAR>closure : ∀ (a : α), ∀ s ∈ S, (f a s).1 ∈ S<VAR>out : ∀ (a : α) (s s' : σ), s ∈ S → s' ∈ S → (f a s).2 = (f a s').2<GOAL>(mapAccumr f xs s₀).2 = (mapAccumr (fun x x_1 => ((), (f x s₀).2)) xs ()).2
<VAR>α : Type u_2<VAR>n : ℕ<VAR>β : Type u_1<VAR>xs : Vector α n<VAR>ys : Vector β n<VAR>σ : Type<VAR>f : α → σ → σ × β<VAR>s₀ : σ<VAR>S : Set σ<VAR>h₀ : s₀ ∈ S<VAR>closure : ∀ (a : α), ∀ s ∈ S, (f a s).1 ∈ S<VAR>out : ∀ (a : α) (s s' : σ), s ∈ S → s' ∈ S → (f a s).2 = (f a s').2<GOAL>∃ R, R s₀ () ∧ ∀ {s : σ} {q : Unit} (a : α), R s q → R (f a s).1 ((), (f a s₀).2).1 ∧ (f a s).2 = ((), (f a s₀).2).2
<VAR>α : Type u_2<VAR>n : ℕ<VAR>β : Type u_1<VAR>xs : Vector α n<VAR>ys : Vector β n<VAR>σ : Type<VAR>f : α → σ → σ × β<VAR>s₀ : σ<VAR>S : Set σ<VAR>h₀ : s₀ ∈ S<VAR>closure : ∀ (a : α), ∀ s ∈ S, (f a s).1 ∈ S<VAR>out : ∀ (a : α) (s s' : σ), s ∈ S → s' ∈ S → (f a s).2 = (f a s').2<GOAL>∀ {s : σ} {q : Unit} (a : α), s ∈ S → (f a s).1 ∈ S ∧ (f a s).2 = ((), (f a s₀).2).2
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>p q : A → Prop<VAR>inst✝²² : Semifield R<VAR>inst✝²¹ : StarRing R<VAR>inst✝²⁰ : MetricSpace R<VAR>inst✝¹⁹ : TopologicalSemiring R<VAR>inst✝¹⁸ : ContinuousStar R<VAR>inst✝¹⁷ : Field S<VAR>inst✝¹⁶ : StarRing S<VAR>inst✝¹⁵ : MetricSpace S<VAR>inst✝¹⁴ : TopologicalRing S<VAR>inst✝¹³ : ContinuousStar S<VAR>inst✝¹² : TopologicalSpace A<VAR>inst✝¹¹ : NonUnitalRing A<VAR>inst✝¹⁰ : StarRing A<VAR>inst✝⁹ : Module S A<VAR>inst✝⁸ : IsScalarTower S A A<VAR>inst✝⁷ : SMulCommClass S A A<VAR>inst✝⁶ : NonUnitalContinuousFunctionalCalculus S q<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Module R A<VAR>inst✝³ : IsScalarTower R S A<VAR>inst✝² : StarModule R S<VAR>inst✝¹ : ContinuousSMul R S<VAR>inst✝ : CompleteSpace R<VAR>a : A<VAR>φ : C(↑(σₙ S a), S)₀ →⋆ₙₐ[S] A<VAR>hφ : ClosedEmbedding ⇑φ<VAR>f : C(S, R)<VAR>h : QuasispectrumRestricts a ⇑f<VAR>halg : UniformEmbedding ⇑(algebraMap R S)<VAR>h_cpct : CompactSpace ↑(σₙ S a)<GOAL>ClosedEmbedding ⇑(nonUnitalStarAlgHom φ h)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>p q : A → Prop<VAR>inst✝²² : Semifield R<VAR>inst✝²¹ : StarRing R<VAR>inst✝²⁰ : MetricSpace R<VAR>inst✝¹⁹ : TopologicalSemiring R<VAR>inst✝¹⁸ : ContinuousStar R<VAR>inst✝¹⁷ : Field S<VAR>inst✝¹⁶ : StarRing S<VAR>inst✝¹⁵ : MetricSpace S<VAR>inst✝¹⁴ : TopologicalRing S<VAR>inst✝¹³ : ContinuousStar S<VAR>inst✝¹² : TopologicalSpace A<VAR>inst✝¹¹ : NonUnitalRing A<VAR>inst✝¹⁰ : StarRing A<VAR>inst✝⁹ : Module S A<VAR>inst✝⁸ : IsScalarTower S A A<VAR>inst✝⁷ : SMulCommClass S A A<VAR>inst✝⁶ : NonUnitalContinuousFunctionalCalculus S q<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Module R A<VAR>inst✝³ : IsScalarTower R S A<VAR>inst✝² : StarModule R S<VAR>inst✝¹ : ContinuousSMul R S<VAR>inst✝ : CompleteSpace R<VAR>a : A<VAR>φ : C(↑(σₙ S a), S)₀ →⋆ₙₐ[S] A<VAR>hφ : ClosedEmbedding ⇑φ<VAR>f : C(S, R)<VAR>h : QuasispectrumRestricts a ⇑f<VAR>halg : UniformEmbedding ⇑(algebraMap R S)<VAR>h_cpct : CompactSpace ↑(σₙ S a)<VAR>this : CompactSpace ↑(σₙ R a)<GOAL>ClosedEmbedding ⇑(nonUnitalStarAlgHom φ h)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>p q : A → Prop<VAR>inst✝²² : Semifield R<VAR>inst✝²¹ : StarRing R<VAR>inst✝²⁰ : MetricSpace R<VAR>inst✝¹⁹ : TopologicalSemiring R<VAR>inst✝¹⁸ : ContinuousStar R<VAR>inst✝¹⁷ : Field S<VAR>inst✝¹⁶ : StarRing S<VAR>inst✝¹⁵ : MetricSpace S<VAR>inst✝¹⁴ : TopologicalRing S<VAR>inst✝¹³ : ContinuousStar S<VAR>inst✝¹² : TopologicalSpace A<VAR>inst✝¹¹ : NonUnitalRing A<VAR>inst✝¹⁰ : StarRing A<VAR>inst✝⁹ : Module S A<VAR>inst✝⁸ : IsScalarTower S A A<VAR>inst✝⁷ : SMulCommClass S A A<VAR>inst✝⁶ : NonUnitalContinuousFunctionalCalculus S q<VAR>inst✝⁵ : Algebra R S<VAR>inst✝⁴ : Module R A<VAR>inst✝³ : IsScalarTower R S A<VAR>inst✝² : StarModule R S<VAR>inst✝¹ : ContinuousSMul R S<VAR>inst✝ : CompleteSpace R<VAR>a : A<VAR>φ : C(↑(σₙ S a), S)₀ →⋆ₙₐ[S] A<VAR>hφ : ClosedEmbedding ⇑φ<VAR>f : C(S, R)<VAR>h : QuasispectrumRestricts a ⇑f<VAR>halg : UniformEmbedding ⇑(algebraMap R S)<VAR>h_cpct : CompactSpace ↑(σₙ S a)<VAR>this✝ : CompactSpace ↑(σₙ R a)<VAR>this : h.homeomorph.symm 0 = 0<GOAL>ClosedEmbedding ⇑(nonUnitalStarAlgHom φ h)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : α → Prop<GOAL>(∃ x ∈ ∅, p x) ↔ False
<VAR>K : Type v<VAR>V : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End K V<VAR>p : K[X]<VAR>μ : K<VAR>x : V<VAR>h : f.HasEigenvector μ x<GOAL>((aeval f) p) x = eval μ p • x
<VAR>K : Type v<VAR>V : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End K V<VAR>p : K[X]<VAR>μ : K<VAR>x : V<VAR>h : f.HasEigenvector μ x<GOAL>∀ (a : K), ((aeval f) (C a)) x = eval μ (C a) • x
<VAR>K : Type v<VAR>V : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End K V<VAR>p : K[X]<VAR>μ : K<VAR>x : V<VAR>h : f.HasEigenvector μ x<GOAL>∀ (p q : K[X]), ((aeval f) p) x = eval μ p • x → ((aeval f) q) x = eval μ q • x → ((aeval f) (p + q)) x = eval μ (p + q) • x
<VAR>K : Type v<VAR>V : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End K V<VAR>p : K[X]<VAR>μ : K<VAR>x : V<VAR>h : f.HasEigenvector μ x<GOAL>∀ (n : ℕ) (a : K), ((aeval f) (C a * X ^ n)) x = eval μ (C a * X ^ n) • x → ((aeval f) (C a * X ^ (n + 1))) x = eval μ (C a * X ^ (n + 1)) • x
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>f g : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>hg : g.IsMultiplicative<VAR>m n : ℕ<VAR>cop : m.Coprime n<GOAL>(f.pmul g) (m * n) = (f.pmul g) m * (f.pmul g) n
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>f g : ArithmeticFunction R<VAR>hf : f.IsMultiplicative<VAR>hg : g.IsMultiplicative<VAR>m n : ℕ<VAR>cop : m.Coprime n<GOAL>f m * f n * (g m * g n) = f m * g m * (f n * g n)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α<VAR>x y : α<VAR>inst✝³ : DecidableRel f✝.SameCycle<VAR>inst✝² : DecidableRel g.SameCycle<VAR>f : Perm α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>h : f.SameCycle x y<VAR>hx : x ∈ f.support<GOAL>∃ i < (f.cycleOf x).support.card, (f ^ i) x = y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f✝ g : Perm α<VAR>x y : α<VAR>inst✝³ : DecidableRel f✝.SameCycle<VAR>inst✝² : DecidableRel g.SameCycle<VAR>f : Perm α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>h : f.SameCycle x y<VAR>hx : f x ≠ x<GOAL>∃ i < (f.cycleOf x).support.card, (f ^ i) x = y
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>inst✝⁴ : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : MonoidalCategory D<VAR>E : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>inst✝ : MonoidalCategory E<VAR>F : OplaxMonoidalFunctor C D<VAR>G : OplaxMonoidalFunctor D E<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>X' : C<GOAL>(fun X Y => G.map (F.δ X Y) ≫ G.δ (F.obj X) (F.obj Y)) X X' ≫ __src✝.map f ▷ __src✝.obj X' = __src✝.map (f ▷ X') ≫ (fun X Y => G.map (F.δ X Y) ≫ G.δ (F.obj X) (F.obj Y)) Y X'
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>inst✝⁴ : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : MonoidalCategory D<VAR>E : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>inst✝ : MonoidalCategory E<VAR>F : OplaxMonoidalFunctor C D<VAR>G : OplaxMonoidalFunctor D E<VAR>X Y f : C<VAR>X' : X ⟶ Y<GOAL>(fun X Y => G.map (F.δ X Y) ≫ G.δ (F.obj X) (F.obj Y)) f X ≫ __src✝.obj f ◁ __src✝.map X' = __src✝.map (f ◁ X') ≫ (fun X Y => G.map (F.δ X Y) ≫ G.δ (F.obj X) (F.obj Y)) f Y
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>inst✝⁴ : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : MonoidalCategory D<VAR>E : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>inst✝ : MonoidalCategory E<VAR>F : OplaxMonoidalFunctor C D<VAR>G : OplaxMonoidalFunctor D E<VAR>X Y Z : C<GOAL>(G.map (F.δ (X ⊗ Y) Z) ≫ G.δ (F.obj (X ⊗ Y)) (F.obj Z)) ≫ (G.map (F.δ X Y) ≫ G.δ (F.obj X) (F.obj Y)) ▷ G.obj (F.obj Z) ≫ (α_ (G.obj (F.obj X)) (G.obj (F.obj Y)) (G.obj (F.obj Z))).hom = G.map (F.map (α_ X Y Z).hom) ≫ (G.map (F.δ X (Y ⊗ Z)) ≫ G.δ (F.obj X) (F.obj (Y ⊗ Z))) ≫ G.obj (F.obj X) ◁ (G.map (F.δ Y Z) ≫ G.δ (F.obj Y) (F.obj Z))
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>inst✝⁴ : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : MonoidalCategory D<VAR>E : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>inst✝ : MonoidalCategory E<VAR>F : OplaxMonoidalFunctor C D<VAR>G : OplaxMonoidalFunctor D E<VAR>X Y Z : C<GOAL>G.map (F.δ (X ⊗ Y) Z) ≫ G.map (F.δ X Y ▷ F.obj Z) ≫ G.δ (F.obj X ⊗ F.obj Y) (F.obj Z) ≫ G.δ (F.obj X) (F.obj Y) ▷ G.obj (F.obj Z) ≫ (α_ (G.obj (F.obj X)) (G.obj (F.obj Y)) (G.obj (F.obj Z))).hom = G.map (F.map (α_ X Y Z).hom) ≫ G.map (F.δ X (Y ⊗ Z)) ≫ G.map (F.obj X ◁ F.δ Y Z) ≫ G.δ (F.obj X) (F.obj Y ⊗ F.obj Z) ≫ G.obj (F.obj X) ◁ G.δ (F.obj Y) (F.obj Z)
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>inst✝⁴ : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : MonoidalCategory D<VAR>E : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>inst✝ : MonoidalCategory E<VAR>F : OplaxMonoidalFunctor C D<VAR>G : OplaxMonoidalFunctor D E<VAR>X Y Z : C<GOAL>G.map (F.δ (X ⊗ Y) Z) ≫ G.map (F.δ X Y ▷ F.obj Z) ≫ G.δ (F.obj X ⊗ F.obj Y) (F.obj Z) ≫ G.δ (F.obj X) (F.obj Y) ▷ G.obj (F.obj Z) ≫ (α_ (G.obj (F.obj X)) (G.obj (F.obj Y)) (G.obj (F.obj Z))).hom = (G.map (F.δ (X ⊗ Y) Z ≫ F.δ X Y ▷ F.obj Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom) ≫ G.δ (F.obj X) (F.obj Y ⊗ F.obj Z)) ≫ G.obj (F.obj X) ◁ G.δ (F.obj Y) (F.obj Z)
<VAR>C : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} C<VAR>inst✝⁴ : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>inst✝² : MonoidalCategory D<VAR>E : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>inst✝ : MonoidalCategory E<VAR>F : OplaxMonoidalFunctor C D<VAR>G : OplaxMonoidalFunctor D E<VAR>X Y Z : C<GOAL>G.map (F.δ (X ⊗ Y) Z) ≫ G.map (F.δ X Y ▷ F.obj Z) ≫ G.map (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom ≫ G.δ (F.obj X) (F.obj Y ⊗ F.obj Z) ≫ G.obj (F.obj X) ◁ G.δ (F.obj Y) (F.obj Z) = (G.map (F.δ (X ⊗ Y) Z ≫ F.δ X Y ▷ F.obj Z ≫ (α_ (F.obj X) (F.obj Y) (F.obj Z)).hom) ≫ G.δ (F.obj X) (F.obj Y ⊗ F.obj Z)) ≫ G.obj (F.obj X) ◁ G.δ (F.obj Y) (F.obj Z)
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝¹ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝ : Monoid N<VAR>i j : ι<VAR>w : NeWord M i j<GOAL>w.toList.getLast? = some ⟨j, w.last⟩
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝¹ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝ : Monoid N<VAR>i j : ι<VAR>w : NeWord M i j<GOAL>⟨j, w.last⟩ ∈ w.toList.getLast?
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>inst✝³ : Monoid M<VAR>inst✝² : LinearOrder M<VAR>inst✝¹ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b c : M<VAR>h : a ^ 2 < b * c<GOAL>a < max b c
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>s✝ t : Set α<VAR>a✝ b : α<VAR>inst✝ : IsDirected α fun x x_1 => x ≤ x_1<VAR>s : Set α<VAR>a : α<GOAL>BddAbove (insert a s) ↔ BddAbove s
<VAR>E : Type<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f g : E → ℂ<VAR>z : ℂ<VAR>x : E<VAR>s : Set E<GOAL>AnalyticOn ℂ cexp univ
<VAR>E : Type<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f g : E → ℂ<VAR>z : ℂ<VAR>x : E<VAR>s : Set E<GOAL>Differentiable ℂ cexp
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>K : Type u_4<VAR>K₂ : Type u_5<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>V : Type u_9<VAR>V₂ : Type u_10<VAR>inst✝¹⁰ : Semiring R<VAR>inst✝⁹ : Semiring R₂<VAR>inst✝⁸ : Semiring R₃<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : AddCommMonoid M₂<VAR>inst✝⁵ : AddCommMonoid M₃<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R₂ M₂<VAR>inst✝² : Module R₃ M₃<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝¹ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>inst✝ : RingHomSurjective τ₁₂<VAR>f : M →ₛₗ[τ₁₂] M₂<GOAL>range f.rangeRestrict = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>k : ℕ<VAR>hk : range (k + 1) \ {0} = image Nat.succ (range k)<GOAL>range (k + 1 + 1) \ {0} = image Nat.succ (range (k + 1))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>k : ℕ<VAR>hk : range (k + 1) \ {0} = image Nat.succ (range k)<GOAL>range (k + 1 + 1) \ {0} = image Nat.succ (insert k (range k))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>k : ℕ<VAR>hk : range (k + 1) \ {0} = image Nat.succ (range k)<GOAL>k + 1 ∉ {0}
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>T T' T'' : D<VAR>Y Y' Y'' : C<VAR>S✝ S' : C ⥤ D<VAR>A : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} A<VAR>B : Type u₄<VAR>inst✝ : Category.{v₄, u₄} B<VAR>F : B ⥤ C<VAR>G : C ⥤ D<VAR>S : C<VAR>X✝ Y✝ : CostructuredArrow F S<VAR>f : X✝ ⟶ Y✝<GOAL>(F ⋙ G).map f.left ≫ ((fun X => mk (G.map X.hom)) Y✝).hom = ((fun X => mk (G.map X.hom)) X✝).hom
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>n : ℕ<VAR>a : K<GOAL>root (X ^ n - C a) ^ n = (of (X ^ n - C a)) a
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>S : Type u_4<VAR>inst✝³ : Group G<VAR>inst✝² : AddGroup A<VAR>s : Set G<VAR>inst✝¹ : Group α<VAR>inst✝ : MulDistribMulAction α G<VAR>H : Subgroup G<VAR>h : G<VAR>hh : h ∈ H<VAR>this : {x | x ∈ H} = ↑H<GOAL>↑H * {h} = ↑H
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>m✝ : OuterMeasure α<VAR>ι : Type u_2<VAR>m : ι → OuterMeasure α<VAR>s : Set α<GOAL>(sum fun i => (m i).trim) s ≤ (sum m).trim s
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>m✝ : OuterMeasure α<VAR>ι : Type u_2<VAR>m : ι → OuterMeasure α<VAR>s : Set α<GOAL>∀ (i : Set α), s ⊆ i → MeasurableSet i → ∑' (i : ι), ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (m i) t ≤ ∑' (i_3 : ι), (m i_3) i
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>inst✝² : FiniteDimensional ℝ F<VAR>inst✝¹ : MeasurableSpace F<VAR>inst✝ : BorelSpace F<VAR>m n : ℕ<VAR>_i : Fact (finrank ℝ F = n)<VAR>o : Orientation ℝ F (Fin n)<VAR>b : OrthonormalBasis ι ℝ F<GOAL>o.volumeForm.measure (parallelepiped ⇑b) = 1
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>inst✝² : FiniteDimensional ℝ F<VAR>inst✝¹ : MeasurableSpace F<VAR>inst✝ : BorelSpace F<VAR>m n : ℕ<VAR>_i : Fact (finrank ℝ F = n)<VAR>o : Orientation ℝ F (Fin n)<VAR>b : OrthonormalBasis ι ℝ F<VAR>e : ι ≃ Fin n<GOAL>o.volumeForm.measure (parallelepiped ⇑b) = 1
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : Fintype ι<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : InnerProductSpace ℝ F<VAR>inst✝² : FiniteDimensional ℝ F<VAR>inst✝¹ : MeasurableSpace F<VAR>inst✝ : BorelSpace F<VAR>m n : ℕ<VAR>_i : Fact (finrank ℝ F = n)<VAR>o : Orientation ℝ F (Fin n)<VAR>b : OrthonormalBasis ι ℝ F<VAR>e : ι ≃ Fin n<VAR>A : ⇑b = ⇑(b.reindex e) ∘ ⇑e<GOAL>o.volumeForm.measure (parallelepiped ⇑b) = 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝ : Monoid G<GOAL>¬IsTorsion G ↔ ∃ g, ¬IsOfFinOrder g
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>Q : QuadraticMap R M N<VAR>x : M<GOAL>Q.IsOrtho x 0
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>H H' : G.Subgraph<VAR>hle : H ≤ H'<VAR>hv : H.verts = H'.verts<VAR>h : H.Connected<GOAL>H'.Connected
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>H H' : G.Subgraph<VAR>hle : H ≤ H'<VAR>hv : H.verts = H'.verts<VAR>h : H.Connected<GOAL>(H'.copy H.verts hv H'.Adj ⋯).Connected
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>H H' : G.Subgraph<VAR>hle : H ≤ H'<VAR>hv : H.verts = H'.verts<VAR>h : H.Connected<GOAL>H.coe ≤ (H'.copy H.verts hv H'.Adj ⋯).coe
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>H H' : G.Subgraph<VAR>hle : H ≤ H'<VAR>hv✝ : H.verts = H'.verts<VAR>h : H.Connected<VAR>v : V<VAR>hv : v ∈ H.verts<VAR>w : V<VAR>hw : w ∈ H.verts<VAR>hvw : H.coe.Adj ⟨v, hv⟩ ⟨w, hw⟩<GOAL>(H'.copy H.verts hv✝ H'.Adj ⋯).coe.Adj ⟨v, hv⟩ ⟨w, hw⟩
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>n✝ : ℕ<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>x : 𝕜<VAR>n : ℕ∞<VAR>h : ∀ (m : ℕ), ↑m ≤ n → DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s<GOAL>ContDiffOn 𝕜 n f s