ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimits C<VAR>X Y Z : TopCat<VAR>ℱ : Presheaf C X<VAR>x : ↑X<VAR>U✝ : Opens ↑X<VAR>hxU✝ : (𝟙 X) x ∈ U✝<GOAL>𝟙 (ℱ.obj ((OpenNhds.inclusion ((𝟙 X) x) ⋙ Opens.map (𝟙 X)).op.obj (op { obj := U✝, property := ⋯ }))) ≫ colimit.ι ((OpenNhds.map (𝟙 X) x).op ⋙ ((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj ℱ) (op { obj := U✝, property := ⋯ }) ≫ colimit.pre (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj ℱ) (OpenNhds.map (𝟙 X) x).op = colimit.ι ((OpenNhds.inclusion ((𝟙 X) x)).op ⋙ (pushforward C (𝟙 X)).obj ℱ) (op { obj := U✝, property := ⋯ }) ≫ (stalkFunctor C x).map (Pushforward.id ℱ).hom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R✝ : Type u_3<VAR>R' : Type u_4<VAR>S✝ : Type u_5<VAR>S' : Type u_6<VAR>T : Type u_7<VAR>T' : Type u_8<VAR>R : Type u_9<VAR>S : Type u_10<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : Ring S<VAR>inst✝² : IsDomain (R × S)<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : Nontrivial S<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R✝ : Type u_3<VAR>R' : Type u_4<VAR>S✝ : Type u_5<VAR>S' : Type u_6<VAR>T : Type u_7<VAR>T' : Type u_8<VAR>R : Type u_9<VAR>S : Type u_10<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : Ring S<VAR>inst✝² : IsDomain (R × S)<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : Nontrivial S<VAR>this : (0, 1) = 0 ∨ (1, 0) = 0<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R✝ : Type u_3<VAR>R' : Type u_4<VAR>S✝ : Type u_5<VAR>S' : Type u_6<VAR>T : Type u_7<VAR>T' : Type u_8<VAR>R : Type u_9<VAR>S : Type u_10<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : Ring S<VAR>inst✝² : IsDomain (R × S)<VAR>inst✝¹ : Nontrivial R<VAR>inst✝ : Nontrivial S<VAR>this : 0 = 0 ∧ 1 = 0 ∨ 1 = 0 ∧ 0 = 0<GOAL>False
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Abelian C<VAR>inst✝¹ : HasProjectiveResolutions C<VAR>inst✝ : EnoughProjectives C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>α : ShortComplex.mk (d f) f ⋯ ⟶ ShortComplex.mk (kernel.ι f) f ⋯ := { τ₁ := π (kernel f), τ₂ := 𝟙 (ShortComplex.mk (d f) f ⋯).X₂, τ₃ := 𝟙 (ShortComplex.mk (d f) f ⋯).X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }<VAR>this✝¹ : Epi α.τ₁<VAR>this✝ : IsIso α.τ₂<VAR>this : Mono α.τ₃<GOAL>(ShortComplex.mk (d f) f ⋯).Exact
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Abelian C<VAR>inst✝¹ : HasProjectiveResolutions C<VAR>inst✝ : EnoughProjectives C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>α : ShortComplex.mk (d f) f ⋯ ⟶ ShortComplex.mk (kernel.ι f) f ⋯ := { τ₁ := π (kernel f), τ₂ := 𝟙 (ShortComplex.mk (d f) f ⋯).X₂, τ₃ := 𝟙 (ShortComplex.mk (d f) f ⋯).X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }<VAR>this✝¹ : Epi α.τ₁<VAR>this✝ : IsIso α.τ₂<VAR>this : Mono α.τ₃<GOAL>(ShortComplex.mk (kernel.ι f) f ⋯).Exact
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Abelian C<VAR>inst✝¹ : HasProjectiveResolutions C<VAR>inst✝ : EnoughProjectives C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>α : ShortComplex.mk (d f) f ⋯ ⟶ ShortComplex.mk (kernel.ι f) f ⋯ := { τ₁ := π (kernel f), τ₂ := 𝟙 (ShortComplex.mk (d f) f ⋯).X₂, τ₃ := 𝟙 (ShortComplex.mk (d f) f ⋯).X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }<VAR>this✝¹ : Epi α.τ₁<VAR>this✝ : IsIso α.τ₂<VAR>this : Mono α.τ₃<GOAL>IsLimit (KernelFork.ofι (ShortComplex.mk (kernel.ι f) f ⋯).f ⋯)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<GOAL>Ioo a b ⊆ Ico a b
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<GOAL>Set.Ioo a b ⊆ Set.Ico a b
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f✝ f : G →* N<VAR>H : Subgroup G<VAR>h : f.ker ≤ H<GOAL>comap f (map f H) = H
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>∡ p₃ p₁ p₂ = ↑(Real.arccos (dist p₁ p₂ / dist p₁ p₃))
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<VAR>hs : (∡ p₃ p₁ p₂).sign = 1<GOAL>∡ p₃ p₁ p₂ = ↑(Real.arccos (dist p₁ p₂ / dist p₁ p₃))
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : Group G<VAR>f g : MonoidAlgebra k G<VAR>x : G<GOAL>(f * g) x = sum f fun a b => (single a b * g) x
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : Group G<VAR>f g : MonoidAlgebra k G<VAR>x : G<GOAL>(sum f fun a b => (single a b * g) x) = sum f fun a b => b * g (a⁻¹ * x)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : AddCommMonoid ι<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>f : HomogeneousLocalization 𝒜 x<GOAL>f.den • f.val = (algebraMap A (at x)) f.num
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : AddCommMonoid ι<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>f : HomogeneousLocalization 𝒜 x<GOAL>IsLocalization.mk' (at x) (f.den * f.num) ⟨f.den, ⋯⟩ = (algebraMap A (at x)) f.num
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>f : ℂ → ℝ → ℂ := fun c x => cexp (-c * ↑x ^ 2)<GOAL>ContinuousAt (fun c => ∫ (x : ℝ), cexp (-c * ↑x ^ 2)) b
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>f : ℂ → ℝ → ℂ := fun c x => cexp (-c * ↑x ^ 2)<VAR>d : ℝ<VAR>hd : 0 < d<VAR>hd' : d < b.re<GOAL>ContinuousAt (fun c => ∫ (x : ℝ), cexp (-c * ↑x ^ 2)) b
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>f : ℂ → ℝ → ℂ := fun c x => cexp (-c * ↑x ^ 2)<VAR>d : ℝ<VAR>hd : 0 < d<VAR>hd' : d < b.re<VAR>f_meas : ∀ (c : ℂ), AEStronglyMeasurable (f c) volume<GOAL>ContinuousAt (fun c => ∫ (x : ℝ), cexp (-c * ↑x ^ 2)) b
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>f : ℂ → ℝ → ℂ := fun c x => cexp (-c * ↑x ^ 2)<VAR>d : ℝ<VAR>hd : 0 < d<VAR>hd' : d < b.re<VAR>f_meas : ∀ (c : ℂ), AEStronglyMeasurable (f c) volume<VAR>f_cts : ∀ (x : ℝ), ContinuousAt (fun c => f c x) b<GOAL>ContinuousAt (fun c => ∫ (x : ℝ), cexp (-c * ↑x ^ 2)) b
<VAR>b : ℂ<VAR>hb : 0 < b.re<VAR>f : ℂ → ℝ → ℂ := fun c x => cexp (-c * ↑x ^ 2)<VAR>d : ℝ<VAR>hd : 0 < d<VAR>hd' : d < b.re<VAR>f_meas : ∀ (c : ℂ), AEStronglyMeasurable (f c) volume<VAR>f_cts : ∀ (x : ℝ), ContinuousAt (fun c => f c x) b<VAR>f_le_bd : ∀ᶠ (c : ℂ) in 𝓝 b, ∀ᵐ (x : ℝ), ‖f c x‖ ≤ rexp (-d * x ^ 2)<GOAL>ContinuousAt (fun c => ∫ (x : ℝ), cexp (-c * ↑x ^ 2)) b
<VAR>Ω : Type u_1<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : TopologicalSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>μs : ℕ → Measure Ω<VAR>inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μs i)<VAR>f : Ω →ᵇ ℝ<VAR>f_nn : 0 ≤ f<VAR>h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ liminf (fun i => (μs i) G) atTop<GOAL>∫ (x : Ω), f x ∂μ ≤ liminf (fun i => ∫ (x : Ω), f x ∂μs i) atTop
<VAR>Ω : Type u_1<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : TopologicalSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>μs : ℕ → Measure Ω<VAR>inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μs i)<VAR>f : Ω →ᵇ ℝ<VAR>f_nn : 0 ≤ f<VAR>h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ liminf (fun i => (μs i) G) atTop<VAR>same : ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μ ≤ liminf (fun i => ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop<GOAL>∫ (x : Ω), f x ∂μ ≤ liminf (fun i => ∫ (x : Ω), f x ∂μs i) atTop
<VAR>Ω : Type u_1<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : TopologicalSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>μs : ℕ → Measure Ω<VAR>inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μs i)<VAR>f : Ω →ᵇ ℝ<VAR>f_nn : 0 ≤ f<VAR>h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ liminf (fun i => (μs i) G) atTop<VAR>same : ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μ ≤ liminf (fun i => ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop<GOAL>(∫⁻ (a : Ω), ENNReal.ofReal (f a) ∂μ).toReal ≤ liminf (fun i => ∫ (x : Ω), f x ∂μs i) atTop
<VAR>Ω : Type u_1<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : TopologicalSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>μs : ℕ → Measure Ω<VAR>inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μs i)<VAR>f : Ω →ᵇ ℝ<VAR>f_nn : 0 ≤ f<VAR>h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ liminf (fun i => (μs i) G) atTop<VAR>same : ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μ ≤ liminf (fun i => ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop<GOAL>liminf (fun i => ∫ (x : Ω), f x ∂μs i) atTop = (liminf (fun i => ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop).toReal
<VAR>Ω : Type u_1<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : TopologicalSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>μs : ℕ → Measure Ω<VAR>inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μs i)<VAR>f : Ω →ᵇ ℝ<VAR>f_nn : 0 ≤ f<VAR>h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ liminf (fun i => (μs i) G) atTop<VAR>same : ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μ ≤ liminf (fun i => ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop<GOAL>∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μ ≠ ⊤
<VAR>Ω : Type u_1<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : TopologicalSpace Ω<VAR>inst✝² : OpensMeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝¹ : IsProbabilityMeasure μ<VAR>μs : ℕ → Measure Ω<VAR>inst✝ : ∀ (i : ℕ), IsProbabilityMeasure (μs i)<VAR>f : Ω →ᵇ ℝ<VAR>f_nn : 0 ≤ f<VAR>h_opens : ∀ (G : Set Ω), IsOpen G → μ G ≤ liminf (fun i => (μs i) G) atTop<VAR>same : ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μ ≤ liminf (fun i => ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop<GOAL>liminf (fun i => ∫⁻ (x : Ω), ENNReal.ofReal (f x) ∂μs i) atTop ≠ ⊤
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝⁴ : Monoid M<VAR>inst✝³ : AddMonoid N<VAR>G : Type u_3<VAR>H : Type u_4<VAR>inst✝² : Group G<VAR>inst✝¹ : AddGroup H<VAR>s : Set G<VAR>inst✝ : Finite ↑s<VAR>this : Fintype ↑s<GOAL>Group.rank ↥(closure s) ≤ Nat.card ↑s
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝⁴ : Monoid M<VAR>inst✝³ : AddMonoid N<VAR>G : Type u_3<VAR>H : Type u_4<VAR>inst✝² : Group G<VAR>inst✝¹ : AddGroup H<VAR>s : Set G<VAR>inst✝ : Finite ↑s<VAR>this : Fintype ↑s<GOAL>Group.rank ↥(closure ↑s.toFinset) ≤ s.toFinset.card
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>inst✝⁴ : MeasurableSpace G<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : CommGroup G<VAR>inst✝¹ : MeasurableMul₂ G<VAR>inst✝ : MeasurableInv G<VAR>f g : α → G<VAR>hf : Measurable f<VAR>h : Measurable (f * g)<GOAL>g = f * g * f⁻¹
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>a b x : α<GOAL>|x| * ↑(sign x) = x
<VAR>x y : PGame<VAR>ox : x.Numeric<VAR>oy : y.Numeric<GOAL>x < y ↔ (∃ i, x ≤ y.moveLeft i) ∨ ∃ j, x.moveRight j ≤ y
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι → Type u_4<VAR>inst✝² : Fact (1 ≤ p)<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : (i : ι) → PseudoEMetricSpace (β i)<VAR>x y : WithLp ⊤ ((i : ι) → β i)<GOAL>edist ((WithLp.equiv ⊤ ((i : ι) → β i)) x) ((WithLp.equiv ⊤ ((i : ι) → β i)) y) ≤ edist x y
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β : ι → Type u_4<VAR>inst✝² : Fact (1 ≤ p)<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : (i : ι) → PseudoEMetricSpace (β i)<VAR>x y : WithLp ⊤ ((i : ι) → β i)<GOAL>edist x y ≤ edist ((WithLp.equiv ⊤ ((i : ι) → β i)) x) ((WithLp.equiv ⊤ ((i : ι) → β i)) y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m✝ : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>m : MeasurableSpace α<VAR>f : α →ₛ ℝ≥0∞<VAR>s : Set α<VAR>μ : Measure α<GOAL>f.lintegral (μ.restrict s) = ∑ y ∈ f.range, y * μ (↑f ⁻¹' {y} ∩ s)
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : Monoid M<VAR>inst✝ : AddMonoid N<VAR>P : Submonoid M<VAR>h : P.FG<VAR>S : Set M<VAR>hS : closure S = P<VAR>hf : S.Finite<GOAL>AddSubmonoid.closure (⇑Additive.toMul ⁻¹' S) = toAddSubmonoid P
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : Monoid M<VAR>inst✝ : AddMonoid N<VAR>P : Submonoid M<VAR>h : (toAddSubmonoid P).FG<VAR>T : Set (Additive M)<VAR>hT : AddSubmonoid.closure T = toAddSubmonoid P<VAR>hf : T.Finite<GOAL>closure (⇑Multiplicative.ofAdd ⁻¹' T) = P
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>u : Fin (rank K) → (𝓞 K)ˣ<VAR>w₁ w₂ : InfinitePlace K<VAR>e₁ : { w // w ≠ w₁ } ≃ Fin (rank K)<VAR>e₂ : { w // w ≠ w₂ } ≃ Fin (rank K)<VAR>f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w₁).symm e₁.symm)<VAR>g : { w // w ≠ w₂ } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w₂)).symm<GOAL>|(Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₁ i))))).det| = |(Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).det|
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>u : Fin (rank K) → (𝓞 K)ˣ<VAR>w₁ w₂ : InfinitePlace K<VAR>e₁ : { w // w ≠ w₁ } ≃ Fin (rank K)<VAR>e₂ : { w // w ≠ w₂ } ≃ Fin (rank K)<VAR>f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w₁).symm e₁.symm)<VAR>g : { w // w ≠ w₂ } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w₂)).symm<VAR>h_col : |((Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).submatrix (⇑(g.trans e₂.symm)) id).det| = |↑↑(Equiv.Perm.sign (g.trans e₂.symm)) * (Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).det|<GOAL>|(Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₁ i))))).det| = |(Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).det|
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>u : Fin (rank K) → (𝓞 K)ˣ<VAR>w₁ w₂ : InfinitePlace K<VAR>e₁ : { w // w ≠ w₁ } ≃ Fin (rank K)<VAR>e₂ : { w // w ≠ w₂ } ≃ Fin (rank K)<VAR>f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w₁).symm e₁.symm)<VAR>g : { w // w ≠ w₂ } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w₂)).symm<VAR>h_col : |((Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).submatrix (⇑(g.trans e₂.symm)) id).det| = |(Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).det|<GOAL>|(Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₁ i))))).det| = |(Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).det|
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>u : Fin (rank K) → (𝓞 K)ˣ<VAR>w₁ w₂ : InfinitePlace K<VAR>e₁ : { w // w ≠ w₁ } ≃ Fin (rank K)<VAR>e₂ : { w // w ≠ w₂ } ≃ Fin (rank K)<VAR>f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w₁).symm e₁.symm)<VAR>g : { w // w ≠ w₂ } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w₂)).symm<VAR>h_col : |((Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).submatrix (⇑(g.trans e₂.symm)) id).det| = |(Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).det|<GOAL>|(Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₁ i))))).det| = |((Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).submatrix (⇑(g.trans e₂.symm)) id).det|
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>u : Fin (rank K) → (𝓞 K)ˣ<VAR>w₁ w₂ : InfinitePlace K<VAR>e₁ : { w // w ≠ w₁ } ≃ Fin (rank K)<VAR>e₂ : { w // w ≠ w₂ } ≃ Fin (rank K)<VAR>f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w₁).symm e₁.symm)<VAR>g : { w // w ≠ w₂ } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w₂)).symm<VAR>h_col : |((Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).submatrix (⇑(g.trans e₂.symm)) id).det| = |(Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).det|<VAR>h : |((Matrix.of fun i w => ↑(f w).mult * Real.log ((f w) ((algebraMap (𝓞 K) K) ↑(u i)))).submatrix id (Fin.succAbove 0)).det| = |(↑↑0 - ↑↑(f.symm w₂)).negOnePow • ((Matrix.of fun i w => ↑(f w).mult * Real.log ((f w) ((algebraMap (𝓞 K) K) ↑(u i)))).submatrix id (f.symm w₂).succAbove).det|<GOAL>|(Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₁ i))))).det| = |((Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).submatrix (⇑(g.trans e₂.symm)) id).det|
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>u : Fin (rank K) → (𝓞 K)ˣ<VAR>w₁ w₂ : InfinitePlace K<VAR>e₁ : { w // w ≠ w₁ } ≃ Fin (rank K)<VAR>e₂ : { w // w ≠ w₂ } ≃ Fin (rank K)<VAR>f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w₁).symm e₁.symm)<VAR>g : { w // w ≠ w₂ } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w₂)).symm<VAR>h_col : |((Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).submatrix (⇑(g.trans e₂.symm)) id).det| = |(Matrix.of fun i w => ↑(↑w).mult * Real.log (↑w ((algebraMap (𝓞 K) K) ↑(u (e₂ i))))).det|<GOAL>∀ (i : Fin (rank K)), ∑ j : Fin (rank K + 1), Matrix.of (fun i w => ↑(f w).mult * Real.log ((f w) ((algebraMap (𝓞 K) K) ↑(u i)))) i j = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : Set α<VAR>s : Finset α<VAR>H : ∀ (x : α), x ∈ s ↔ x ∈ p<VAR>inst✝ : Fintype ↑p<GOAL>card ↑p = s.card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : Set α<VAR>s : Finset α<VAR>H : ∀ (x : α), x ∈ s ↔ x ∈ p<VAR>inst✝ : Fintype ↑p<GOAL>card ↑p = card ↑p
<VAR>b o : Ordinal.{u_1}<GOAL>foldr (fun p r => b ^ p.1 * p.2 + r) 0 (CNF b 0) = 0
<VAR>b o : Ordinal.{u_1}<GOAL>foldr (fun p r => b ^ p.1 * p.2 + r) 0 [] = 0
<VAR>b o✝ o : Ordinal.{u_1}<VAR>ho : o ≠ 0<VAR>IH : foldr (fun p r => b ^ p.1 * p.2 + r) 0 (CNF b (o % b ^ log b o)) = o % b ^ log b o<GOAL>foldr (fun p r => b ^ p.1 * p.2 + r) 0 (CNF b o) = o
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A X Y : M<VAR>hx : IsUnit X.det<VAR>hy : IsUnit Y.det<VAR>h : SemiconjBy A X Y<VAR>n : ℕ<GOAL>SemiconjBy A (X ^ ↑n) (Y ^ ↑n)
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A X Y : M<VAR>hx : IsUnit X.det<VAR>hy : IsUnit Y.det<VAR>h : SemiconjBy A X Y<VAR>n : ℕ<GOAL>SemiconjBy A (X ^ -[n+1]) (Y ^ -[n+1])
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A X Y : M<VAR>hx : IsUnit X.det<VAR>hy : IsUnit Y.det<VAR>h : SemiconjBy A X Y<VAR>n : ℕ<VAR>hx' : IsUnit (X ^ n.succ).det<GOAL>SemiconjBy A (X ^ -[n+1]) (Y ^ -[n+1])
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A X Y : M<VAR>hx : IsUnit X.det<VAR>hy : IsUnit Y.det<VAR>h : SemiconjBy A X Y<VAR>n : ℕ<VAR>hx' : IsUnit (X ^ n.succ).det<VAR>hy' : IsUnit (Y ^ n.succ).det<GOAL>SemiconjBy A (X ^ -[n+1]) (Y ^ -[n+1])
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A X Y : M<VAR>hx : IsUnit X.det<VAR>hy : IsUnit Y.det<VAR>h : SemiconjBy A X Y<VAR>n : ℕ<VAR>hx' : IsUnit (X ^ n.succ).det<VAR>hy' : IsUnit (Y ^ n.succ).det<GOAL>A * ↑hx'.unit⁻¹ • (X ^ n.succ).adjugate = ↑hy'.unit⁻¹ • (Y ^ n.succ).adjugate * A
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A X Y : M<VAR>hx : IsUnit X.det<VAR>hy : IsUnit Y.det<VAR>h : SemiconjBy A X Y<VAR>n : ℕ<VAR>hx' : IsUnit (X ^ n.succ).det<VAR>hy' : IsUnit (Y ^ n.succ).det<GOAL>(fun x => Y ^ n.succ * x) (A * ↑hx'.unit⁻¹ • (X ^ n.succ).adjugate) = (fun x => Y ^ n.succ * x) (↑hy'.unit⁻¹ • (Y ^ n.succ).adjugate * A)
<VAR>n' : Type u_1<VAR>inst✝² : DecidableEq n'<VAR>inst✝¹ : Fintype n'<VAR>R : Type u_2<VAR>inst✝ : CommRing R<VAR>A X Y : M<VAR>hx : IsUnit X.det<VAR>hy : IsUnit Y.det<VAR>h : SemiconjBy A X Y<VAR>n : ℕ<VAR>hx' : IsUnit (X ^ n.succ).det<VAR>hy' : IsUnit (Y ^ n.succ).det<GOAL>Y ^ n.succ * (A * ↑hx'.unit⁻¹ • (X ^ n.succ).adjugate) = Y ^ n.succ * (↑hy'.unit⁻¹ • (Y ^ n.succ).adjugate * A)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : LinearOrder α<VAR>inst✝⁵ : OrderTopology α<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝⁴ : Finite ι<VAR>inst✝³ : (i : ι) → LinearOrder (π i)<VAR>inst✝² : (i : ι) → TopologicalSpace (π i)<VAR>inst✝¹ : ∀ (i : ι), OrderTopology (π i)<VAR>a b x : (i : ι) → π i<VAR>a' b' x' : ι → α<VAR>inst✝ : Nonempty ι<VAR>ha : ∀ (i : ι), a i < x i<VAR>hb : ∀ (i : ι), x i < b i<GOAL>Ico a b ∈ 𝓝 x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁷ : TopologicalSpace α<VAR>inst✝⁶ : LinearOrder α<VAR>inst✝⁵ : OrderTopology α<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝⁴ : Finite ι<VAR>inst✝³ : (i : ι) → LinearOrder (π i)<VAR>inst✝² : (i : ι) → TopologicalSpace (π i)<VAR>inst✝¹ : ∀ (i : ι), OrderTopology (π i)<VAR>a b x : (i : ι) → π i<VAR>a' b' x' : ι → α<VAR>inst✝ : Nonempty ι<VAR>ha : ∀ (i : ι), a i < x i<VAR>hb : ∀ (i : ι), x i < b i<VAR>i : ι<VAR>x✝ : i ∈ univ<GOAL>Ico (a i) (b i) ∈ 𝓝 (x i)
<VAR>G : Type u_1<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : SFinite μ<VAR>s : Set G<VAR>inst✝² : MeasurableInv G<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : ν.IsMulLeftInvariant<VAR>sm : MeasurableSet s<VAR>f : G → ℝ≥0∞<VAR>hf : Measurable f<GOAL>μ s * ∫⁻ (y : G), f y ∂ν = ∫⁻ (x : G), ν ((fun z => z * x) ⁻¹' s) * f x⁻¹ ∂μ
<VAR>G : Type u_1<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : SFinite μ<VAR>s : Set G<VAR>inst✝² : MeasurableInv G<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : ν.IsMulLeftInvariant<VAR>sm : MeasurableSet s<VAR>f : G → ℝ≥0∞<VAR>hf : Measurable f<GOAL>∫⁻ (x : G), ∫⁻ (y : G), s.indicator (fun x => 1) (y * x) * f x⁻¹ ∂ν ∂μ = ∫⁻ (x : G), ν ((fun z => z * x) ⁻¹' s) * f x⁻¹ ∂μ
<VAR>G : Type u_1<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : SFinite μ<VAR>s : Set G<VAR>inst✝² : MeasurableInv G<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : ν.IsMulLeftInvariant<VAR>sm : MeasurableSet s<VAR>f : G → ℝ≥0∞<VAR>hf : Measurable f<GOAL>AEMeasurable (uncurry fun x y => s.indicator (fun x => 1) x * f y) (μ.prod ν)
<VAR>G : Type u_1<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : SFinite μ<VAR>s : Set G<VAR>inst✝² : MeasurableInv G<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : ν.IsMulLeftInvariant<VAR>sm : MeasurableSet s<VAR>f : G → ℝ≥0∞<VAR>hf : Measurable f<VAR>ms : ∀ (x : G), Measurable fun y => ((fun z => z * x) ⁻¹' s).indicator (fun x => 1) y<GOAL>∫⁻ (x : G), ∫⁻ (y : G), s.indicator (fun x => 1) (y * x) * f x⁻¹ ∂ν ∂μ = ∫⁻ (x : G), ν ((fun z => z * x) ⁻¹' s) * f x⁻¹ ∂μ
<VAR>G : Type u_1<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : Group G<VAR>inst✝⁵ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : SFinite μ<VAR>s : Set G<VAR>inst✝² : MeasurableInv G<VAR>inst✝¹ : μ.IsMulLeftInvariant<VAR>inst✝ : ν.IsMulLeftInvariant<VAR>sm : MeasurableSet s<VAR>f : G → ℝ≥0∞<VAR>hf : Measurable f<VAR>ms : ∀ (x : G), Measurable fun y => ((fun z => z * x) ⁻¹' s).indicator (fun x => 1) y<VAR>this : ∀ (x y : G), s.indicator (fun x => 1) (y * x) = ((fun z => z * x) ⁻¹' s).indicator (fun b => 1) y<GOAL>∫⁻ (x : G), ∫⁻ (y : G), s.indicator (fun x => 1) (y * x) * f x⁻¹ ∂ν ∂μ = ∫⁻ (x : G), ν ((fun z => z * x) ⁻¹' s) * f x⁻¹ ∂μ
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n : ℕ<VAR>ifp_succ_n : IntFractPair K<VAR>stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n<VAR>succ_nth_fr_eq_zero : ifp_succ_n.fr = 0<GOAL>∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr⁻¹ = ↑⌊ifp_n.fr⁻¹⌋