ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>u✝ : Lean.Level<VAR>arg : Q(Type u✝)<VAR>sα✝ : Q(CommSemiring «$arg»)<VAR>u : Lean.Level<VAR>α : Q(Type u)<VAR>sα : Q(CommSemiring «$α»)<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>a a' a₁ a₂ a₃ b b' b₁✝ b₂✝ b₃ c₁ c₂ b₁ : R<VAR>b₂ : ℕ<GOAL>a * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * (a * b₃)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : Module.Free R M<VAR>inst✝² : Module.Finite R M<VAR>inst✝¹ : IsReduced R<VAR>inst✝ : IsNilpotent R L M<VAR>x y : L<GOAL>((traceForm R L M) x) y = (0 x) y
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : Module.Free R M<VAR>inst✝² : Module.Finite R M<VAR>inst✝¹ : IsReduced R<VAR>inst✝ : IsNilpotent R L M<VAR>x y : L<GOAL>_root_.IsNilpotent ((trace R M) (φ x ∘ₗ φ y))
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : Module.Free R M<VAR>inst✝² : Module.Finite R M<VAR>inst✝¹ : IsReduced R<VAR>inst✝ : IsNilpotent R L M<VAR>x y : L<GOAL>_root_.IsNilpotent (φ x ∘ₗ φ y)
<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>R✝ : Type u_7<VAR>R₂ : Type u_8<VAR>M✝ : Type u_9<VAR>M₂ : Type u_10<VAR>M : Type u_11<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : T2Space M<VAR>R : Type u_12<VAR>inst✝⁴ : DivisionRing R<VAR>inst✝³ : Module R M<VAR>inst✝² : ContinuousConstSMul R M<VAR>inst✝¹ : AddGroup α<VAR>inst✝ : AddAction α β<VAR>f : β → M<VAR>g : Quotient (orbitRel α β) → R<VAR>x : Quotient (orbitRel α β)<GOAL>automorphize (g ∘ Quotient.mk' • f) x = (g • automorphize f) x
<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>R✝ : Type u_7<VAR>R₂ : Type u_8<VAR>M✝ : Type u_9<VAR>M₂ : Type u_10<VAR>M : Type u_11<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : T2Space M<VAR>R : Type u_12<VAR>inst✝⁴ : DivisionRing R<VAR>inst✝³ : Module R M<VAR>inst✝² : ContinuousConstSMul R M<VAR>inst✝¹ : AddGroup α<VAR>inst✝ : AddAction α β<VAR>f : β → M<VAR>g : Quotient (orbitRel α β) → R<VAR>x : Quotient (orbitRel α β)<GOAL>∀ (a : β), automorphize (g ∘ Quotient.mk' • f) (Quotient.mk'' a) = (g • automorphize f) (Quotient.mk'' a)
<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>R✝ : Type u_7<VAR>R₂ : Type u_8<VAR>M✝ : Type u_9<VAR>M₂ : Type u_10<VAR>M : Type u_11<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : T2Space M<VAR>R : Type u_12<VAR>inst✝⁴ : DivisionRing R<VAR>inst✝³ : Module R M<VAR>inst✝² : ContinuousConstSMul R M<VAR>inst✝¹ : AddGroup α<VAR>inst✝ : AddAction α β<VAR>f : β → M<VAR>g : Quotient (orbitRel α β) → R<VAR>x : Quotient (orbitRel α β)<VAR>b : β<GOAL>automorphize (g ∘ Quotient.mk' • f) (Quotient.mk'' b) = (g • automorphize f) (Quotient.mk'' b)
<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>R✝ : Type u_7<VAR>R₂ : Type u_8<VAR>M✝ : Type u_9<VAR>M₂ : Type u_10<VAR>M : Type u_11<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : T2Space M<VAR>R : Type u_12<VAR>inst✝⁴ : DivisionRing R<VAR>inst✝³ : Module R M<VAR>inst✝² : ContinuousConstSMul R M<VAR>inst✝¹ : AddGroup α<VAR>inst✝ : AddAction α β<VAR>f : β → M<VAR>g : Quotient (orbitRel α β) → R<VAR>x : Quotient (orbitRel α β)<VAR>b : β<GOAL>Quotient.lift (fun b => ∑' (a : α), g (Quotient.mk' (a +ᵥ b)) • f (a +ᵥ b)) ⋯ (Quotient.mk'' b) = g (Quotient.mk'' b) • Quotient.lift (fun b => ∑' (a : α), f (a +ᵥ b)) ⋯ (Quotient.mk'' b)
<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>R✝ : Type u_7<VAR>R₂ : Type u_8<VAR>M✝ : Type u_9<VAR>M₂ : Type u_10<VAR>M : Type u_11<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : T2Space M<VAR>R : Type u_12<VAR>inst✝⁴ : DivisionRing R<VAR>inst✝³ : Module R M<VAR>inst✝² : ContinuousConstSMul R M<VAR>inst✝¹ : AddGroup α<VAR>inst✝ : AddAction α β<VAR>f : β → M<VAR>g : Quotient (orbitRel α β) → R<VAR>x : Quotient (orbitRel α β)<VAR>b : β<VAR>π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)<GOAL>Quotient.lift (fun b => ∑' (a : α), g (Quotient.mk' (a +ᵥ b)) • f (a +ᵥ b)) ⋯ (Quotient.mk'' b) = g (Quotient.mk'' b) • Quotient.lift (fun b => ∑' (a : α), f (a +ᵥ b)) ⋯ (Quotient.mk'' b)
<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>R✝ : Type u_7<VAR>R₂ : Type u_8<VAR>M✝ : Type u_9<VAR>M₂ : Type u_10<VAR>M : Type u_11<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : T2Space M<VAR>R : Type u_12<VAR>inst✝⁴ : DivisionRing R<VAR>inst✝³ : Module R M<VAR>inst✝² : ContinuousConstSMul R M<VAR>inst✝¹ : AddGroup α<VAR>inst✝ : AddAction α β<VAR>f : β → M<VAR>g : Quotient (orbitRel α β) → R<VAR>x : Quotient (orbitRel α β)<VAR>b : β<VAR>π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)<VAR>H₁ : ∀ (a : α), π (a +ᵥ b) = π b<GOAL>Quotient.lift (fun b => ∑' (a : α), g (Quotient.mk' (a +ᵥ b)) • f (a +ᵥ b)) ⋯ (Quotient.mk'' b) = g (Quotient.mk'' b) • Quotient.lift (fun b => ∑' (a : α), f (a +ᵥ b)) ⋯ (Quotient.mk'' b)
<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>R✝ : Type u_7<VAR>R₂ : Type u_8<VAR>M✝ : Type u_9<VAR>M₂ : Type u_10<VAR>M : Type u_11<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : T2Space M<VAR>R : Type u_12<VAR>inst✝⁴ : DivisionRing R<VAR>inst✝³ : Module R M<VAR>inst✝² : ContinuousConstSMul R M<VAR>inst✝¹ : AddGroup α<VAR>inst✝ : AddAction α β<VAR>f : β → M<VAR>g : Quotient (orbitRel α β) → R<VAR>x : Quotient (orbitRel α β)<VAR>b : β<VAR>π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)<VAR>H₁ : ∀ (a : α), π (a +ᵥ b) = π b<GOAL>∑' (a : α), g (π b) • f (a +ᵥ b) = g (π b) • ∑' (a : α), f (a +ᵥ b)
<VAR>n : ℕ<GOAL>∀ {p : ℕ}, p ∈ n.primeFactorsList → Prime p
<VAR>α : Type u<VAR>l✝ l'✝ l l' : List α<GOAL>l.cyclicPermutations ~r l'.cyclicPermutations ↔ l ~r l'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : VectorMeasure α ℝ≥0∞<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>↑μ.ennrealToMeasure.toENNRealVectorMeasure s = ↑μ s
<VAR>𝕜 : Type u_1<VAR>V : Type u_2<VAR>V₁ : Type u_3<VAR>V₁' : Type u_4<VAR>V₂ : Type u_5<VAR>V₃ : Type u_6<VAR>V₄ : Type u_7<VAR>P₁ : Type u_8<VAR>P₁' : Type u_9<VAR>P : Type u_10<VAR>P₂ : Type u_11<VAR>P₃ : Type u_12<VAR>P₄ : Type u_13<VAR>inst✝²⁵ : NormedField 𝕜<VAR>inst✝²⁴ : SeminormedAddCommGroup V<VAR>inst✝²³ : NormedSpace 𝕜 V<VAR>inst✝²² : PseudoMetricSpace P<VAR>inst✝²¹ : NormedAddTorsor V P<VAR>inst✝²⁰ : SeminormedAddCommGroup V₁<VAR>inst✝¹⁹ : NormedSpace 𝕜 V₁<VAR>inst✝¹⁸ : PseudoMetricSpace P₁<VAR>inst✝¹⁷ : NormedAddTorsor V₁ P₁<VAR>inst✝¹⁶ : SeminormedAddCommGroup V₁'<VAR>inst✝¹⁵ : NormedSpace 𝕜 V₁'<VAR>inst✝¹⁴ : MetricSpace P₁'<VAR>inst✝¹³ : NormedAddTorsor V₁' P₁'<VAR>inst✝¹² : SeminormedAddCommGroup V₂<VAR>inst✝¹¹ : NormedSpace 𝕜 V₂<VAR>inst✝¹⁰ : PseudoMetricSpace P₂<VAR>inst✝⁹ : NormedAddTorsor V₂ P₂<VAR>inst✝⁸ : SeminormedAddCommGroup V₃<VAR>inst✝⁷ : NormedSpace 𝕜 V₃<VAR>inst✝⁶ : PseudoMetricSpace P₃<VAR>inst✝⁵ : NormedAddTorsor V₃ P₃<VAR>inst✝⁴ : SeminormedAddCommGroup V₄<VAR>inst✝³ : NormedSpace 𝕜 V₄<VAR>inst✝² : PseudoMetricSpace P₄<VAR>inst✝¹ : NormedAddTorsor V₄ P₄<VAR>e : P ≃ᵃⁱ[𝕜] P₂<VAR>α : Type u_14<VAR>inst✝ : TopologicalSpace α<VAR>x y : P<GOAL>dist ((pointReflection 𝕜 x) y) y = ‖2 • (x -ᵥ y)‖
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁✝ : S₁.HomologyData<VAR>h₂✝ : S₂.HomologyData<VAR>h₁ h₁' : S.LeftHomologyData<VAR>h₂ h₂' : S.RightHomologyData<GOAL>leftRightHomologyComparison' h₁ h₂ = leftHomologyMap' (𝟙 S) h₁ h₁' ≫ leftRightHomologyComparison' h₁' h₂' ≫ rightHomologyMap' (𝟙 S) h₂' h₂
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<GOAL>spectralRadius 𝕜 a ≤ liminf (fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) atTop
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>ε : ℝ≥0∞<VAR>hε : ε < 1<GOAL>ε * spectralRadius 𝕜 a ≤ liminf (fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) atTop
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>ε : ℝ≥0∞<VAR>hε : ε < 1<VAR>h : ¬ε = 0<GOAL>ε * spectralRadius 𝕜 a ≤ liminf (fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) atTop
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>ε : ℝ≥0∞<VAR>hε : ε < 1<VAR>h : ¬ε = 0<VAR>hε' : ε⁻¹ ≠ ⊤<GOAL>ε * spectralRadius 𝕜 a ≤ liminf (fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) atTop
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>ε : ℝ≥0∞<VAR>hε : ε < 1<VAR>h : ¬ε = 0<VAR>hε' : ε⁻¹ ≠ ⊤<GOAL>spectralRadius 𝕜 a ≤ ⨆ i, (⨅ i_1, ↑‖a ^ (i_1 + i)‖₊ ^ (1 / ↑(i_1 + i))) * ε⁻¹
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>ε : ℝ≥0∞<VAR>hε : ε < 1<VAR>h : ¬ε = 0<VAR>hε' : ε⁻¹ ≠ ⊤<GOAL>spectralRadius 𝕜 a ≤ ⨆ i, ⨅ i_1, ↑‖a ^ (i_1 + i)‖₊ ^ (1 / ↑(i_1 + i)) * ε⁻¹
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>ε : ℝ≥0∞<VAR>hε : 1 < ε⁻¹<VAR>h : ¬ε = 0<VAR>hε' : ε⁻¹ ≠ ⊤<GOAL>spectralRadius 𝕜 a ≤ ⨆ i, ⨅ i_1, ↑‖a ^ (i_1 + i)‖₊ ^ (1 / ↑(i_1 + i)) * ε⁻¹
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>ε : ℝ≥0∞<VAR>hε : 1 < ε⁻¹<VAR>h : ¬ε = 0<VAR>hε' : ε⁻¹ ≠ ⊤<VAR>N : ℕ<VAR>hN : ∀ b ≥ N, ↑‖1‖₊ ^ (1 / ↑b) ≤ ε⁻¹<GOAL>spectralRadius 𝕜 a ≤ ⨆ i, ⨅ i_1, ↑‖a ^ (i_1 + i)‖₊ ^ (1 / ↑(i_1 + i)) * ε⁻¹
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>ε : ℝ≥0∞<VAR>hε : 1 < ε⁻¹<VAR>h : ¬ε = 0<VAR>hε' : ε⁻¹ ≠ ⊤<VAR>N : ℕ<VAR>hN : ∀ b ≥ N, ↑‖1‖₊ ^ (1 / ↑b) ≤ ε⁻¹<GOAL>spectralRadius 𝕜 a ≤ ⨅ i, ↑‖a ^ (i + (N + 1))‖₊ ^ (1 / ↑(i + (N + 1))) * ε⁻¹
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>ε : ℝ≥0∞<VAR>hε : 1 < ε⁻¹<VAR>h : ¬ε = 0<VAR>hε' : ε⁻¹ ≠ ⊤<VAR>N : ℕ<VAR>hN : ∀ b ≥ N, ↑‖1‖₊ ^ (1 / ↑b) ≤ ε⁻¹<VAR>n : ℕ<GOAL>spectralRadius 𝕜 a ≤ ↑‖a ^ (n + (N + 1))‖₊ ^ (1 / ↑(n + (N + 1))) * ε⁻¹
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>ε : ℝ≥0∞<VAR>hε : 1 < ε⁻¹<VAR>h : ¬ε = 0<VAR>hε' : ε⁻¹ ≠ ⊤<VAR>N : ℕ<VAR>hN : ∀ b ≥ N, ↑‖1‖₊ ^ (1 / ↑b) ≤ ε⁻¹<VAR>n : ℕ<GOAL>spectralRadius 𝕜 a ≤ ↑‖a ^ (n + N + 1)‖₊ ^ (1 / ↑(n + N + 1)) * ε⁻¹
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>ε : ℝ≥0∞<VAR>hε : 1 < ε⁻¹<VAR>h : ¬ε = 0<VAR>hε' : ε⁻¹ ≠ ⊤<VAR>N : ℕ<VAR>hN : ∀ b ≥ N, ↑‖1‖₊ ^ (1 / ↑b) ≤ ε⁻¹<VAR>n : ℕ<GOAL>↑‖a ^ (n + N + 1)‖₊ ^ (1 / (↑(n + N) + 1)) * ↑‖1‖₊ ^ (1 / (↑(n + N) + 1)) ≤ ↑‖a ^ (n + N + 1)‖₊ ^ (1 / ↑(n + N + 1)) * ε⁻¹
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>ε : ℝ≥0∞<VAR>hε : 1 < ε⁻¹<VAR>h : ¬ε = 0<VAR>hε' : ε⁻¹ ≠ ⊤<VAR>N : ℕ<VAR>hN : ∀ b ≥ N, ↑‖1‖₊ ^ (1 / ↑b) ≤ ε⁻¹<VAR>n : ℕ<GOAL>↑‖a ^ (n + N + 1)‖₊ ^ (1 / ↑(n + N + 1)) * ↑‖1‖₊ ^ (1 / ↑(n + N + 1)) ≤ ↑‖a ^ (n + N + 1)‖₊ ^ (1 / ↑(n + N + 1)) * ε⁻¹
<VAR>k G : Type u<VAR>inst✝² : CommRing k<VAR>inst✝¹ : Group G<VAR>A : Rep k G<VAR>inst✝ : A.IsTrivial<VAR>f : ↥(oneCocycles A)<VAR>g h : G<GOAL>↑f (g * h) = ↑f g + ↑f h
<VAR>a✝ b✝ c : ℕ<VAR>α : Type u_1<VAR>inst✝ : DivisionRing α<VAR>a : α<VAR>b : ℤ<VAR>nb ne : ℕ<VAR>pb : IsInt b (Int.negOfNat nb)<VAR>pe' : IsInt (a ^ nb)⁻¹ (Int.negOfNat ne)<GOAL>IsInt (a ^ b) (Int.negOfNat ne)
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCancelCommMonoid G<VAR>x : k[G]<GOAL>x /ᵒᶠ 0 = x
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : AddCancelCommMonoid G<VAR>x : k[G]<VAR>x✝ : G<GOAL>(x /ᵒᶠ 0) x✝ = x x✝
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R✝ I J X Y R : Set α<VAR>hI : (M ↾ R).Indep I<GOAL>M.Indep I
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e✝ : I → R<VAR>he✝¹ : OrthogonalIdempotents e✝<VAR>inst✝ : Fintype I<VAR>he✝ : CompleteOrthogonalIdempotents e✝<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>n : ℕ<VAR>e : Fin n → S<VAR>he : CompleteOrthogonalIdempotents e<VAR>he' : ∀ (i : Fin n), e i ∈ f.range<GOAL>∃ e', CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e✝ : I → R<VAR>he✝¹ : OrthogonalIdempotents e✝<VAR>inst✝ : Fintype I<VAR>he✝ : CompleteOrthogonalIdempotents e✝<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>n : ℕ<VAR>e : Fin n → S<VAR>he : CompleteOrthogonalIdempotents e<VAR>he' : ∀ (i : Fin n), e i ∈ f.range<VAR>h✝ : Subsingleton R<GOAL>∃ e', CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e✝ : I → R<VAR>he✝¹ : OrthogonalIdempotents e✝<VAR>inst✝ : Fintype I<VAR>he✝ : CompleteOrthogonalIdempotents e✝<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>n : ℕ<VAR>e : Fin n → S<VAR>he : CompleteOrthogonalIdempotents e<VAR>he' : ∀ (i : Fin n), e i ∈ f.range<VAR>h✝ : Nontrivial R<GOAL>∃ e', CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e✝ : I → R<VAR>he✝¹ : OrthogonalIdempotents e✝<VAR>inst✝ : Fintype I<VAR>he✝ : CompleteOrthogonalIdempotents e✝<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>n : ℕ<VAR>e : Fin n → S<VAR>he : CompleteOrthogonalIdempotents e<VAR>he' : ∀ (i : Fin n), e i ∈ f.range<VAR>h✝¹ : Nontrivial R<VAR>h✝ : Subsingleton S<GOAL>∃ e', CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e✝ : I → R<VAR>he✝¹ : OrthogonalIdempotents e✝<VAR>inst✝ : Fintype I<VAR>he✝ : CompleteOrthogonalIdempotents e✝<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>n : ℕ<VAR>e : Fin n → S<VAR>he : CompleteOrthogonalIdempotents e<VAR>he' : ∀ (i : Fin n), e i ∈ f.range<VAR>h✝¹ : Nontrivial R<VAR>h✝ : Nontrivial S<GOAL>∃ e', CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e✝ : I → R<VAR>he✝¹ : OrthogonalIdempotents e✝<VAR>inst✝ : Fintype I<VAR>he✝ : CompleteOrthogonalIdempotents e✝<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>h✝¹ : Nontrivial R<VAR>h✝ : Nontrivial S<VAR>n : ℕ<VAR>e : Fin (n + 1) → S<VAR>he : CompleteOrthogonalIdempotents e<VAR>he' : ∀ (i : Fin (n + 1)), e i ∈ f.range<GOAL>∃ e', CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e✝ : I → R<VAR>he✝¹ : OrthogonalIdempotents e✝<VAR>inst✝ : Fintype I<VAR>he✝ : CompleteOrthogonalIdempotents e✝<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>h✝¹ : Nontrivial R<VAR>h✝ : Nontrivial S<VAR>n : ℕ<VAR>e : Fin (n + 1) → S<VAR>he : CompleteOrthogonalIdempotents e<VAR>he' : ∀ (i : Fin (n + 1)), e i ∈ f.range<VAR>e' : Fin (n + 1) → R<VAR>h₁ : OrthogonalIdempotents e'<VAR>h₂ : ⇑f ∘ e' = e<GOAL>∃ e', CompleteOrthogonalIdempotents e' ∧ ⇑f ∘ e' = e
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e✝ : I → R<VAR>he✝¹ : OrthogonalIdempotents e✝<VAR>inst✝ : Fintype I<VAR>he✝ : CompleteOrthogonalIdempotents e✝<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>h✝¹ : Nontrivial R<VAR>h✝ : Nontrivial S<VAR>n : ℕ<VAR>e : Fin (n + 1) → S<VAR>he : CompleteOrthogonalIdempotents e<VAR>he' : ∀ (i : Fin (n + 1)), e i ∈ f.range<VAR>e' : Fin (n + 1) → R<VAR>h₁ : OrthogonalIdempotents e'<VAR>h₂ : ⇑f ∘ e' = e<VAR>i : Fin (n + 1)<GOAL>(⇑f ∘ (fun x => x.elim (1 - ∑ i : Fin n, (e' ∘ ⇑(Fin.succEmb n)) i) (e' ∘ ⇑(Fin.succEmb n))) ∘ ⇑(finSuccEquiv n)) i = e i
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e✝ : I → R<VAR>he✝¹ : OrthogonalIdempotents e✝<VAR>inst✝ : Fintype I<VAR>he✝ : CompleteOrthogonalIdempotents e✝<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>h✝¹ : Nontrivial R<VAR>h✝ : Nontrivial S<VAR>n : ℕ<VAR>e : Fin (n + 1) → S<VAR>he : CompleteOrthogonalIdempotents e<VAR>he' : ∀ (i : Fin (n + 1)), e i ∈ f.range<VAR>e' : Fin (n + 1) → R<VAR>h₁ : OrthogonalIdempotents e'<VAR>h₂ : ⇑f ∘ e' = e<VAR>i : Fin (n + 1)<VAR>this : ∀ (i : Fin (n + 1)), f (e' i) = e i<GOAL>(⇑f ∘ (fun x => x.elim (1 - ∑ i : Fin n, (e' ∘ ⇑(Fin.succEmb n)) i) (e' ∘ ⇑(Fin.succEmb n))) ∘ ⇑(finSuccEquiv n)) i = e i
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e✝ : I → R<VAR>he✝¹ : OrthogonalIdempotents e✝<VAR>inst✝ : Fintype I<VAR>he✝ : CompleteOrthogonalIdempotents e✝<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>h✝¹ : Nontrivial R<VAR>h✝ : Nontrivial S<VAR>n : ℕ<VAR>e : Fin (n + 1) → S<VAR>he : CompleteOrthogonalIdempotents e<VAR>he' : ∀ (i : Fin (n + 1)), e i ∈ f.range<VAR>e' : Fin (n + 1) → R<VAR>h₁ : OrthogonalIdempotents e'<VAR>h₂ : ⇑f ∘ e' = e<VAR>this : ∀ (i : Fin (n + 1)), f (e' i) = e i<GOAL>(⇑f ∘ (fun x => x.elim (1 - ∑ i : Fin n, (e' ∘ ⇑(Fin.succEmb n)) i) (e' ∘ ⇑(Fin.succEmb n))) ∘ ⇑(finSuccEquiv n)) ((finSuccEquiv n).symm none) = e ((finSuccEquiv n).symm none)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e✝ : I → R<VAR>he✝¹ : OrthogonalIdempotents e✝<VAR>inst✝ : Fintype I<VAR>he✝ : CompleteOrthogonalIdempotents e✝<VAR>h : ∀ x ∈ RingHom.ker f, IsNilpotent x<VAR>h✝¹ : Nontrivial R<VAR>h✝ : Nontrivial S<VAR>n : ℕ<VAR>e : Fin (n + 1) → S<VAR>he : CompleteOrthogonalIdempotents e<VAR>he' : ∀ (i : Fin (n + 1)), e i ∈ f.range<VAR>e' : Fin (n + 1) → R<VAR>h₁ : OrthogonalIdempotents e'<VAR>h₂ : ⇑f ∘ e' = e<VAR>this : ∀ (i : Fin (n + 1)), f (e' i) = e i<VAR>i : Fin n<GOAL>(⇑f ∘ (fun x => x.elim (1 - ∑ i : Fin n, (e' ∘ ⇑(Fin.succEmb n)) i) (e' ∘ ⇑(Fin.succEmb n))) ∘ ⇑(finSuccEquiv n)) ((finSuccEquiv n).symm (some i)) = e ((finSuccEquiv n).symm (some i))
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>S : L.Substructure M<VAR>s : Set M<VAR>inst✝ : Countable ((l : ℕ) × L.Functions l)<VAR>h : s.Countable<VAR>this : Countable ↑s<GOAL>Countable ↥((closure L).toFun s)
<VAR>L : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>S : L.Substructure M<VAR>s : Set M<VAR>inst✝ : Countable ((l : ℕ) × L.Functions l)<VAR>h : s.Countable<VAR>this : Countable ↑s<GOAL>lift.{?u.25480, w} #↥((closure L).toFun s) ≤ ℵ₀
<VAR>a b c : ℕ<VAR>P : ℕ → Prop<VAR>h : ∀ (n : ℕ), P (n + 1) → P n<VAR>base : ∃ n, ∀ m > n, P m<VAR>step : ∀ (n : ℕ), (∀ m > n, P m) → P n<VAR>n : ℕ<GOAL>P n
<VAR>a b c : ℕ<VAR>P : ℕ → Prop<VAR>h : ∀ (n : ℕ), P (n + 1) → P n<VAR>base : ∃ n, ∀ m > n, P m<VAR>step : ∀ (n : ℕ), (∀ m > n, P m) → P n<VAR>n : ℕ<GOAL>∀ (n : ℕ), (fun n => ∀ m ≥ n, P m) (n + 1) → (fun n => ∀ m ≥ n, P m) n
<VAR>a b c : ℕ<VAR>P : ℕ → Prop<VAR>h : ∀ (n : ℕ), P (n + 1) → P n<VAR>base : ∃ n, ∀ m > n, P m<VAR>step : ∀ (n : ℕ), (∀ m > n, P m) → P n<VAR>n : ℕ<GOAL>¬BddAbove {x | (fun n => ∀ m ≥ n, P m) x}
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>hs : Bornology.IsBounded s<VAR>hy : y ∈ s<GOAL>dist x y ≤ infDist x s + diam s
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>s t u : Set α<VAR>x y : α<VAR>Φ : α → β<VAR>hs : Bornology.IsBounded s<VAR>hy : y ∈ s<GOAL>(edist x y).toReal ≤ (infEdist x s).toReal + (EMetric.diam s).toReal
<VAR>x : ℝ<GOAL>HasDerivAt (fun x => ↑(𝐞 x)) (2 * ↑π * I * ↑(𝐞 x)) x
<VAR>x : ℝ<VAR>h1 : ∀ (y : ℝ), ↑(𝐞 y) = (fourier 1) ↑y<GOAL>HasDerivAt (fun x => ↑(𝐞 x)) (2 * ↑π * I * ↑(𝐞 x)) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ η : Kernel α β<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>inst✝² : DecidablePred fun x => x ∈ s<VAR>E : Type u_4<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>a : α<VAR>g : β → E<GOAL>∫ (b : β), g b ∂(piecewise hs κ η) a = if a ∈ s then ∫ (b : β), g b ∂κ a else ∫ (b : β), g b ∂η a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ η : Kernel α β<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>inst✝² : DecidablePred fun x => x ∈ s<VAR>E : Type u_4<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>a : α<VAR>g : β → E<GOAL>(∫ (b : β), g b ∂if a ∈ s then κ a else η a) = if a ∈ s then ∫ (b : β), g b ∂κ a else ∫ (b : β), g b ∂η a
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : CommRing S<VAR>W : WeierstrassCurve R<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : Algebra S A<VAR>inst✝⁴ : IsScalarTower R S A<VAR>B : Type v<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra S B<VAR>inst✝ : IsScalarTower R S B<VAR>f : A →ₐ[S] B<VAR>n : ℕ<GOAL>(W.baseChange B).preΨ' n = Polynomial.map (↑f) ((W.baseChange A).preΨ' n)
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<GOAL>2 ≤ S'.multiplicity
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>s : Set α<GOAL>∫⁻ (x : α) in s, max (f x) (g x) ∂μ = ∫⁻ (x : α) in s ∩ {x | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in s ∩ {x | g x < f x}, f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>s : Set α<GOAL>MeasurableSet {x | g x < f x}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>s : Set α<GOAL>MeasurableSet {x | f x ≤ g x}
<VAR>x✝ y✝ z x : ℝ<VAR>hx : 0 < x<VAR>y : ℝ<GOAL>0 < x ^ y
<VAR>x✝ y✝ z x : ℝ<VAR>hx : 0 < x<VAR>y : ℝ<GOAL>0 < rexp (log x * y)
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → F<VAR>hP : W.Nonsingular P<VAR>hPz : P z = 0<GOAL>W.neg P = -(P y / P x) • ![1, 1, 0]
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P : Fin 3 → F<VAR>hP : W.Nonsingular P<VAR>hPz : P z = 0<VAR>hX : ∀ {n : ℕ}, IsUnit (P x ^ n)<GOAL>W.neg P = -(P y / P x) • ![1, 1, 0]