ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E✝ : Type u_3<VAR>E : Type u_4<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module ℝ E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>p q : Submodule ℝ E<VAR>hpq : IsCompl p q<VAR>hpc : {0}ᶜ.Nonempty ∧ ∀ x ∈ {0}ᶜ, ∀ y ∈ {0}ᶜ, JoinedIn {0}ᶜ x y<GOAL>(↑q)ᶜ.Nonempty ∧ ∀ x ∈ (↑q)ᶜ, ∀ y ∈ (↑q)ᶜ, JoinedIn (↑q)ᶜ x y
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableEq V<VAR>u v : V<VAR>p : G.Walk u v<VAR>h : p.IsEulerian<GOAL>p.IsTrail
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableEq V<VAR>u v : V<VAR>p : G.Walk u v<VAR>h : p.IsEulerian<GOAL>∀ (a : Sym2 V), List.count a p.edges ≤ 1
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>ι : Type u_6<VAR>u : Finset ι<VAR>A : ι → E → F<VAR>A' : ι → E →L[𝕜] F<VAR>h : ∀ i ∈ u, HasFDerivAtFilter (A i) (A' i) x L<GOAL>HasFDerivAtFilter (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x L
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>ι : Type u_6<VAR>u : Finset ι<VAR>A : ι → E → F<VAR>A' : ι → E →L[𝕜] F<VAR>h : ∀ i ∈ u, (fun x' => A i x' - A i x - (A' i) (x' - x)) =o[L] fun x' => x' - x<GOAL>(fun x' => ∑ i ∈ u, A i x' - ∑ i ∈ u, A i x - (∑ i ∈ u, A' i) (x' - x)) =o[L] fun x' => x' - x
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>ι : Type u_6<VAR>u : Finset ι<VAR>A : ι → E → F<VAR>A' : ι → E →L[𝕜] F<VAR>h : ∀ i ∈ u, (fun x' => A i x' - A i x - (A' i) (x' - x)) =o[L] fun x' => x' - x<VAR>x✝ : E<GOAL>∑ i ∈ u, A i x✝ - ∑ i ∈ u, A i x - (∑ i ∈ u, A' i) (x✝ - x) = ∑ i ∈ u, (A i x✝ - A i x - (A' i) (x✝ - x))
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>x : CliffordAlgebra Q<VAR>h : x ∈ evenOdd Q 1<GOAL>involute x = -x
<VAR>M : Type u<VAR>G : Type v<VAR>X : Type w<VAR>inst✝⁶ : PseudoEMetricSpace X<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MulAction G X<VAR>inst✝³ : IsometricSMul G X<VAR>inst✝² : PseudoEMetricSpace G<VAR>inst✝¹ : IsometricSMul G G<VAR>inst✝ : IsometricSMul Gᵐᵒᵖ G<VAR>a b : G<GOAL>edist a⁻¹ b⁻¹ = edist a b
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>l₁ : List α<GOAL>map Prod.swap (l₁.zip []) = [].zip l₁
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>l₁ : List α<GOAL>map Prod.swap [] = [].zip l₁
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>δ : Type u_3<VAR>ε : Type u_4<VAR>a : α<VAR>l₁ : List α<VAR>b : β<VAR>l₂ : List β<GOAL>map Prod.swap ((a :: l₁).zip (b :: l₂)) = (b :: l₂).zip (a :: l₁)
<VAR>R S : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>r : R<VAR>inst✝ : IsLocalization.Away r S<GOAL>(algebraMap R S).FinitePresentation
<VAR>R S : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing S<VAR>inst✝¹ : Algebra R S<VAR>r : R<VAR>inst✝ : IsLocalization.Away r S<GOAL>Algebra.FinitePresentation R S
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ μ₁ μ₂ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>hs : μ s = 0<VAR>ht : ν t = 0<VAR>hst : univ ⊆ s ∪ t<GOAL>μ ⟂ₘ ν
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ μ₁ μ₂ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>hs : μ s = 0<VAR>ht : ν t = 0<VAR>hst : univ ⊆ s ∪ t<GOAL>ν (toMeasurable μ s)ᶜ = 0
<VAR>α : Type u_1<VAR>m0 : MeasurableSpace α<VAR>μ μ₁ μ₂ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>hs : μ s = 0<VAR>ht : ν t = 0<VAR>hst : univ ⊆ s ∪ t<VAR>x : α<VAR>hx : x ∈ (toMeasurable μ s)ᶜ<VAR>hxs : x ∈ s<GOAL>x ∈ toMeasurable μ s
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>k : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>h : IsNilpotent R L (M ⧸ N)<GOAL>⨅ k, lowerCentralSeries R L M k ≤ N
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<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>k✝ : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>h : IsNilpotent R L (M ⧸ N)<VAR>k : ℕ<VAR>hk : lowerCentralSeries R L M k ≤ N<GOAL>⨅ k, lowerCentralSeries R L M k ≤ N
<VAR>B : Type u₁<VAR>inst✝³ : Bicategory B<VAR>C : Type u₂<VAR>inst✝² : Bicategory C<VAR>D : Type u₃<VAR>inst✝¹ : Bicategory D<VAR>F : PrelaxFunctor B C<VAR>a b : B<VAR>f g : a ⟶ b<VAR>η : f ⟶ g<VAR>inst✝ : IsIso η<GOAL>F.map₂ (inv η) = inv (F.map₂ η)
<VAR>B : Type u₁<VAR>inst✝³ : Bicategory B<VAR>C : Type u₂<VAR>inst✝² : Bicategory C<VAR>D : Type u₃<VAR>inst✝¹ : Bicategory D<VAR>F : PrelaxFunctor B C<VAR>a b : B<VAR>f g : a ⟶ b<VAR>η : f ⟶ g<VAR>inst✝ : IsIso η<GOAL>F.map₂ η ≫ F.map₂ (inv η) = 𝟙 (F.map f)
<VAR>ι : Type w<VAR>R : Type u<VAR>M : Type v₁<VAR>N : Type v₂<VAR>P : Type v₃<VAR>Q : Type v₄<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : AddCommGroup M<VAR>inst✝¹¹ : AddCommGroup N<VAR>inst✝¹⁰ : AddCommGroup P<VAR>inst✝⁹ : AddCommGroup Q<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Module R N<VAR>inst✝⁶ : Module R P<VAR>inst✝⁵ : Module R Q<VAR>inst✝⁴ : Free R M<VAR>inst✝³ : Module.Finite R M<VAR>inst✝² : Free R N<VAR>inst✝¹ : Module.Finite R N<VAR>inst✝ : Nontrivial R<VAR>x : P ⊗[R] (M →ₗ[R] Q)<GOAL>(lTensorHomEquivHomLTensor R M P Q) x = (lTensorHomToHomLTensor R M P Q) x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : CommMonoid γ<VAR>A A₁ A₂ : Set α<VAR>B B₁ B₂ : Set β<VAR>C : Set γ<VAR>f f₁ f₂ : α → β<VAR>g : β → γ<VAR>m n : ℕ<VAR>hf : IsMulFreimanHom 2 A B f<VAR>a b c d : α<VAR>ha : a ∈ A<VAR>hb : b ∈ A<VAR>hc : c ∈ A<VAR>hd : d ∈ A<VAR>h : a * b = c * d<GOAL>f a * f b = f c * f d
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>inst✝ : CommMonoid γ<VAR>A A₁ A₂ : Set α<VAR>B B₁ B₂ : Set β<VAR>C : Set γ<VAR>f f₁ f₂ : α → β<VAR>g : β → γ<VAR>m n : ℕ<VAR>hf : IsMulFreimanHom 2 A B f<VAR>a b c d : α<VAR>ha : a ∈ A<VAR>hb : b ∈ A<VAR>hc : c ∈ A<VAR>hd : d ∈ A<VAR>h : {a, b}.prod = {c, d}.prod<GOAL>{f a, f b}.prod = {f c, f d}.prod
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a : α<VAR>ha : a ≠ 0<VAR>b c : α<GOAL>(fun x => x / a) ⁻¹' [[b, c]] = [[b * a, c * a]]
<VAR>V : Type (u + 1)<VAR>inst✝ : LargeCategory V<VAR>G : MonCat<VAR>M N : Action V G<VAR>f : M ≅ N<VAR>g : ↑G<GOAL>N.ρ g = ((forget V G).mapIso f).conj (M.ρ g)
<VAR>V : Type (u + 1)<VAR>inst✝ : LargeCategory V<VAR>G : MonCat<VAR>M N : Action V G<VAR>f : M ≅ N<VAR>g : ↑G<GOAL>((forget V G).mapIso f).hom ≫ N.ρ g = M.ρ g ≫ ((forget V G).mapIso f).hom
<VAR>𝕜 : Type u_1<VAR>M : Type u_2<VAR>α : Type u_3<VAR>G : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>inst✝⁹ : MeasurableSpace G<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : CompleteSpace E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>μ : Measure G<VAR>f✝ : G → E<VAR>g✝ : G<VAR>inst✝⁴ : Group G<VAR>inst✝³ : MeasurableMul G<VAR>inst✝² : MeasurableInv G<VAR>f : G → F<VAR>inst✝¹ : μ.IsInvInvariant<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>g : G<GOAL>Integrable (fun t => f (g / t)) μ ↔ Integrable f μ
<VAR>𝕜 : Type u_1<VAR>M : Type u_2<VAR>α : Type u_3<VAR>G : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>inst✝⁹ : MeasurableSpace G<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : CompleteSpace E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>μ : Measure G<VAR>f✝ : G → E<VAR>g✝ : G<VAR>inst✝⁴ : Group G<VAR>inst✝³ : MeasurableMul G<VAR>inst✝² : MeasurableInv G<VAR>f : G → F<VAR>inst✝¹ : μ.IsInvInvariant<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>g : G<VAR>h : Integrable (fun t => f (g / t)) μ<GOAL>Integrable f μ
<VAR>𝕜 : Type u_1<VAR>M : Type u_2<VAR>α : Type u_3<VAR>G : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>inst✝⁹ : MeasurableSpace G<VAR>inst✝⁸ : NormedAddCommGroup E<VAR>inst✝⁷ : NormedSpace ℝ E<VAR>inst✝⁶ : CompleteSpace E<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>μ : Measure G<VAR>f✝ : G → E<VAR>g✝ : G<VAR>inst✝⁴ : Group G<VAR>inst✝³ : MeasurableMul G<VAR>inst✝² : MeasurableInv G<VAR>f : G → F<VAR>inst✝¹ : μ.IsInvInvariant<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>g : G<VAR>h : Integrable (fun t => f (g / t)) μ<VAR>x✝ : G<GOAL>x✝ = g / (g⁻¹ * x✝)⁻¹
<VAR>f g : CircleDeg1Lift<VAR>hf : Continuous ⇑f<GOAL>∃ x, f x = x + τ f
<VAR>f g : CircleDeg1Lift<VAR>hf : Continuous ⇑f<VAR>a : ℝ<VAR>ha : f a ≤ a + τ f<GOAL>∃ x, f x = x + τ f
<VAR>f g : CircleDeg1Lift<VAR>hf : Continuous ⇑f<VAR>a : ℝ<VAR>ha : f a ≤ a + τ f<VAR>b : ℝ<VAR>hb : b + τ f ≤ f b<GOAL>∃ x, f x = x + τ f
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹ : EMetricSpace X<VAR>inst✝ : EMetricSpace Y<VAR>s : Set ι<VAR>hs : s.Countable<VAR>t : ι → Set X<VAR>this : Encodable ↑s<GOAL>dimH (⋃ i ∈ s, t i) = ⨆ i ∈ s, dimH (t i)
<VAR>α : Type u<VAR>σ σ' : Type v<VAR>M : NFA α σ<VAR>S : Set σ<VAR>x : List α<VAR>a : α<GOAL>M.evalFrom S (x ++ [a]) = M.stepSet (M.evalFrom S x) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>inst✝ : NoAtoms μ<VAR>a : α<GOAL>μ.restrict {a} = 0
<VAR>x y : ℂ<GOAL>tan (x * I) = tanh x * I
<VAR>α : Type u<VAR>inst✝³ : Group α<VAR>inst✝² : LE α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a✝ b✝ c d a b : α<GOAL>a / b ≤ a ↔ 1 ≤ b
<VAR>f : ℕ → ℝ<VAR>hf : Tendsto f atTop (𝓝 0)<VAR>r✝ : ℝ<VAR>hr : 0 < r✝<VAR>hg : Tendsto (fun x => -f x) atTop (𝓝 (-0))<GOAL>-ofSeq f < ↑r✝
<VAR>f : ℕ → ℝ<VAR>hf : Tendsto f atTop (𝓝 0)<VAR>r✝ : ℝ<VAR>hr : 0 < r✝<VAR>hg : Tendsto (fun x => -f x) atTop (𝓝 0)<GOAL>-ofSeq f < ↑r✝
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>x✝ : M × ↥S<VAR>m : M<VAR>s : ↥S<GOAL>1 • (m, s).2 • (m, s).1 = 1 • (m, s).2 • (m, s).1
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>x✝⁴ x✝³ x✝² : M × ↥S<VAR>m1 : M<VAR>s1 : ↥S<VAR>m2 : M<VAR>s2 : ↥S<VAR>x✝¹ : r S M (m1, s1) (m2, s2)<VAR>m3 : M<VAR>s3 : ↥S<VAR>x✝ : r S M (m2, s2) (m3, s3)<VAR>u1 : ↥S<VAR>hu1 : u1 • (m2, s2).2 • (m1, s1).1 = u1 • (m1, s1).2 • (m2, s2).1<VAR>u2 : ↥S<VAR>hu2 : u2 • (m3, s3).2 • (m2, s2).1 = u2 • (m2, s2).2 • (m3, s3).1<GOAL>r S M (m1, s1) (m3, s3)
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>x✝⁴ x✝³ x✝² : M × ↥S<VAR>m1 : M<VAR>s1 : ↥S<VAR>m2 : M<VAR>s2 : ↥S<VAR>x✝¹ : r S M (m1, s1) (m2, s2)<VAR>m3 : M<VAR>s3 : ↥S<VAR>x✝ : r S M (m2, s2) (m3, s3)<VAR>u1 : ↥S<VAR>hu1 : u1 • (m2, s2).2 • (m1, s1).1 = u1 • (m1, s1).2 • (m2, s2).1<VAR>u2 : ↥S<VAR>hu2 : u2 • (m3, s3).2 • (m2, s2).1 = u2 • (m2, s2).2 • (m3, s3).1<GOAL>(u1 * u2 * s2) • (m3, s3).2 • (m1, s1).1 = (u1 * u2 * s2) • (m1, s1).2 • (m3, s3).1
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>x✝⁴ x✝³ x✝² : M × ↥S<VAR>m1 : M<VAR>s1 : ↥S<VAR>m2 : M<VAR>s2 : ↥S<VAR>x✝¹ : r S M (m1, s1) (m2, s2)<VAR>m3 : M<VAR>s3 : ↥S<VAR>x✝ : r S M (m2, s2) (m3, s3)<VAR>u1 : ↥S<VAR>hu1 : u1 • (m2, s2).2 • (m1, s1).1 = u1 • (m1, s1).2 • (m2, s2).1<VAR>u2 : ↥S<VAR>hu2 : u2 • (m3, s3).2 • (m2, s2).1 = u2 • (m2, s2).2 • (m3, s3).1<VAR>hu1' : (fun x => (u2 * s3) • x) (u1 • (m1, s1).2 • (m2, s2).1) = (fun x => (u2 * s3) • x) (u1 • (m2, s2).2 • (m1, s1).1)<VAR>hu2' : (fun x => (u1 * s1) • x) (u2 • (m2, s2).2 • (m3, s3).1) = (fun x => (u1 * s1) • x) (u2 • (m3, s3).2 • (m2, s2).1)<GOAL>(u1 * u2 * s2) • (m3, s3).2 • (m1, s1).1 = (u1 * u2 * s2) • (m1, s1).2 • (m3, s3).1
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>x✝⁴ x✝³ x✝² : M × ↥S<VAR>m1 : M<VAR>s1 : ↥S<VAR>m2 : M<VAR>s2 : ↥S<VAR>x✝¹ : r S M (m1, s1) (m2, s2)<VAR>m3 : M<VAR>s3 : ↥S<VAR>x✝ : r S M (m2, s2) (m3, s3)<VAR>u1 : ↥S<VAR>hu1 : u1 • (m2, s2).2 • (m1, s1).1 = u1 • (m1, s1).2 • (m2, s2).1<VAR>u2 : ↥S<VAR>hu2 : u2 • (m3, s3).2 • (m2, s2).1 = u2 • (m2, s2).2 • (m3, s3).1<VAR>hu1' : (s1 * (s3 * (u1 * u2))) • m2 = (s2 * (s3 * (u1 * u2))) • m1<VAR>hu2' : (s1 * (s2 * (u1 * u2))) • m3 = (s1 * (s3 * (u1 * u2))) • m2<GOAL>(s2 * (s3 * (u1 * u2))) • m1 = (s1 * (s2 * (u1 * u2))) • m3
<VAR>n : ℕ<VAR>hn : n % 4 = 1<GOAL>χ₄ ↑n = 1
<VAR>n : ℕ<VAR>hn : n % 4 = 1<GOAL>χ₄ ↑1 = 1
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s✝ : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>inst✝ : DecidableEq P<VAR>s : Finset P<VAR>w : P → k<VAR>f : { x // x ∈ s } → P<VAR>hf : Function.Injective f<GOAL>(affineCombination k s.attach f) (w ∘ f) = (affineCombination k (image f univ) id) w
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s✝ : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>inst✝ : DecidableEq P<VAR>s : Finset P<VAR>w : P → k<VAR>f : { x // x ∈ s } → P<VAR>hf : Function.Injective f<GOAL>∑ x ∈ s.attach, w (f x) • (f x -ᵥ Classical.choice ⋯) = ∑ x ∈ image f univ, w x • (x -ᵥ Classical.choice ⋯)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s✝ : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>inst✝ : DecidableEq P<VAR>s : Finset P<VAR>w : P → k<VAR>f : { x // x ∈ s } → P<VAR>hf : Function.Injective f<VAR>g₁ : { x // x ∈ s } → V := fun i => w (f i) • (f i -ᵥ Classical.choice ⋯)<GOAL>∑ x ∈ s.attach, w (f x) • (f x -ᵥ Classical.choice ⋯) = ∑ x ∈ image f univ, w x • (x -ᵥ Classical.choice ⋯)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s✝ : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>inst✝ : DecidableEq P<VAR>s : Finset P<VAR>w : P → k<VAR>f : { x // x ∈ s } → P<VAR>hf : Function.Injective f<VAR>g₁ : { x // x ∈ s } → V := fun i => w (f i) • (f i -ᵥ Classical.choice ⋯)<VAR>g₂ : P → V := fun i => w i • (i -ᵥ Classical.choice ⋯)<GOAL>∑ x ∈ s.attach, w (f x) • (f x -ᵥ Classical.choice ⋯) = ∑ x ∈ image f univ, w x • (x -ᵥ Classical.choice ⋯)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s✝ : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>inst✝ : DecidableEq P<VAR>s : Finset P<VAR>w : P → k<VAR>f : { x // x ∈ s } → P<VAR>hf : Function.Injective f<VAR>g₁ : { x // x ∈ s } → V := fun i => w (f i) • (f i -ᵥ Classical.choice ⋯)<VAR>g₂ : P → V := fun i => w i • (i -ᵥ Classical.choice ⋯)<VAR>hgf : g₁ = g₂ ∘ f<GOAL>univ.sum g₁ = (image f univ).sum g₂
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s✝ : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>inst✝ : DecidableEq P<VAR>s : Finset P<VAR>w : P → k<VAR>f : { x // x ∈ s } → P<VAR>hf : Function.Injective f<VAR>g₁ : { x // x ∈ s } → V := fun i => w (f i) • (f i -ᵥ Classical.choice ⋯)<VAR>g₂ : P → V := fun i => w i • (i -ᵥ Classical.choice ⋯)<VAR>hgf : g₁ = g₂ ∘ f<GOAL>univ.sum (g₂ ∘ f) = ∑ x : { x // x ∈ s }, w (f x) • (f x -ᵥ Classical.choice ⋯)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s✝ : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>inst✝ : DecidableEq P<VAR>s : Finset P<VAR>w : P → k<VAR>f : { x // x ∈ s } → P<VAR>hf : Function.Injective f<VAR>g₁ : { x // x ∈ s } → V := fun i => w (f i) • (f i -ᵥ Classical.choice ⋯)<VAR>g₂ : P → V := fun i => w i • (i -ᵥ Classical.choice ⋯)<VAR>hgf : g₁ = g₂ ∘ f<GOAL>∀ x ∈ univ, ∀ y ∈ univ, f x = f y → x = y
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>r : Cofix F α → Cofix F α → Prop<VAR>h : ∀ (x y : Cofix F α), r x y → LiftR' (α.RelLast' r) x.dest y.dest<VAR>x✝ y✝ : Cofix F α<VAR>a✝ : r x✝ y✝<GOAL>LiftR (fun {i} => α.RelLast r) x✝.dest y✝.dest
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>r : Cofix F α → Cofix F α → Prop<VAR>h : ∀ (x y : Cofix F α), r x y → LiftR' (α.RelLast' r) x.dest y.dest<VAR>x✝ y✝ : Cofix F α<VAR>a✝ : r x✝ y✝<GOAL>LiftR' (α.RelLast' r) x✝.dest y✝.dest
<VAR>C : Type u<VAR>inst✝ : Groupoid C<VAR>S : Subgroupoid C<VAR>c : C<VAR>hc : c ∈ S.objs<VAR>d : C<VAR>hd : d ∈ S.objs<VAR>f : ↑⟨c, hc⟩ ⟶ ↑⟨d, hd⟩<VAR>hf : f ∈ S.arrows ↑⟨c, hc⟩ ↑⟨d, hd⟩<VAR>g : ↑⟨c, hc⟩ ⟶ ↑⟨d, hd⟩<VAR>hg : g ∈ S.arrows ↑⟨c, hc⟩ ↑⟨d, hd⟩<VAR>hfg : (fun f => S.hom.map f) ⟨f, hf⟩ = (fun f => S.hom.map f) ⟨g, hg⟩<GOAL>⟨f, hf⟩ = ⟨g, hg⟩
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝³ : CommRing A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra A B<VAR>x : B<VAR>inst✝ : Nontrivial B<VAR>hx : IsIntegral A x<GOAL>0 < (minpoly A x).natDegree
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝³ : CommRing A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra A B<VAR>x : B<VAR>inst✝ : Nontrivial B<VAR>hx : IsIntegral A x<GOAL>(minpoly A x).natDegree ≠ 0
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝³ : CommRing A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra A B<VAR>x : B<VAR>inst✝ : Nontrivial B<VAR>hx : IsIntegral A x<VAR>ndeg_eq_zero : (minpoly A x).natDegree = 0<GOAL>False
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝³ : CommRing A<VAR>inst✝² : Ring B<VAR>inst✝¹ : Algebra A B<VAR>x : B<VAR>inst✝ : Nontrivial B<VAR>hx : IsIntegral A x<VAR>ndeg_eq_zero : (minpoly A x).natDegree = 0<VAR>eq_one : minpoly A x = 1<GOAL>False
<VAR>x✝ : Game<VAR>x : PGame<VAR>y✝ : Game<VAR>y : PGame<GOAL>¬Quot.mk Setoid.r x ≤ Quot.mk Setoid.r y ↔ Quot.mk Setoid.r y ⧏ Quot.mk Setoid.r x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List α<VAR>x : α<GOAL>x ∈ range l.get ↔ x ∈ {x | x ∈ l}
<VAR>C : Type u_2<VAR>inst✝⁵ : Category.{u_1, u_2} C<VAR>inst✝⁴ : HasZeroMorphisms C<VAR>S₁ S₂ S₃ S₄ : ShortComplex C<VAR>inst✝³ : S₁.HasHomology<VAR>inst✝² : S₂.HasHomology<VAR>inst✝¹ : S₃.HasHomology<VAR>inst✝ : S₄.HasHomology<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>γ : RightHomologyMapData φ h₁ h₂<GOAL>QuasiIso φ ↔ IsIso (rightHomologyMap' φ h₁ h₂)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y✝ Z✝ X Y Z : C<VAR>f : Y ≅ X<VAR>g g' : Y ⟶ Z<GOAL>f.inv ≫ g = f.inv ≫ g' ↔ g = g'
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommRing P<VAR>inst✝ : IsLocalization M S<VAR>p : S[X]<GOAL>∃ b, ∀ (i : ℕ), (algebraMap R S) ((integerNormalization M p).coeff i) = ↑b • p.coeff i
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommRing P<VAR>inst✝ : IsLocalization M S<VAR>p : S[X]<GOAL>∀ (i : ℕ), (algebraMap R S) ((integerNormalization M p).coeff i) = ↑(Classical.choose ⋯) • p.coeff i
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommRing P<VAR>inst✝ : IsLocalization M S<VAR>p : S[X]<VAR>i : ℕ<GOAL>(algebraMap R S) ((integerNormalization M p).coeff i) = ↑(Classical.choose ⋯) • p.coeff i
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommRing P<VAR>inst✝ : IsLocalization M S<VAR>p : S[X]<VAR>i : ℕ<GOAL>(algebraMap R S) (if hi : i ∈ p.support then Classical.choose ⋯ else 0) = ↑(Classical.choose ⋯) • p.coeff i
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>ε : ℚ<VAR>hε : 0 < ε<GOAL>∃ i, ∀ j ≥ i, padicNorm p (↑(nthHomSeq f_compat 1 - 1) j) < ε
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>ε : ℚ<VAR>hε : 0 < ε<GOAL>∀ j ≥ 1, padicNorm p (↑(nthHomSeq f_compat 1 - 1) j) < ε
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>ε : ℚ<VAR>hε : 0 < ε<VAR>j : ℕ<VAR>hj : j ≥ 1<GOAL>padicNorm p (↑(nthHomSeq f_compat 1 - 1) j) < ε
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>ε : ℚ<VAR>hε : 0 < ε<VAR>j : ℕ<VAR>hj : j ≥ 1<VAR>this : Fact (1 < p ^ j)<GOAL>padicNorm p (↑(nthHomSeq f_compat 1 - 1) j) < ε
<VAR>p : ℕ<VAR>hp_prime : Fact (Nat.Prime p)<VAR>R : Type u_1<VAR>inst✝ : NonAssocSemiring R<VAR>f : (k : ℕ) → R →+* ZMod (p ^ k)<VAR>f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1<VAR>ε : ℚ<VAR>hε : 0 < ε<VAR>j : ℕ<VAR>hj : j ≥ 1<VAR>this : Fact (1 < p ^ j)<GOAL>ZMod.cast 1 = 1
<VAR>n : ℕ<VAR>P : MvPFunctor.{u} (n + 1)<VAR>α : TypeVec.{u} n<VAR>R : P.M α → P.M α → Prop<VAR>h : ∀ (x y : P.M α), R x y → ∃ a f f₁ f₂, dest P x = ⟨a, splitFun f f₁⟩ ∧ dest P y = ⟨a, splitFun f f₂⟩ ∧ ∀ (i : (P.B a).last), R (f₁ i) (f₂ i)<VAR>a₁ : P.mp.A<VAR>f₁ : P.mp.B a₁ ⟹ α<VAR>a₂ : P.mp.A<VAR>f₂ : P.mp.B a₂ ⟹ α<VAR>r : R ⟨a₁, f₁⟩ ⟨a₂, f₂⟩<GOAL>⟨a₁, f₁⟩ = ⟨a₂, f₂⟩