ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CanonicallyOrderedCommSemiring R<VAR>f g h : ι → R<VAR>s : Finset ι<VAR>i : ι<VAR>hi : i ∈ s<VAR>h2i : g i + h i ≤ f i<VAR>hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j<VAR>hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j<GOAL>∏ i ∈ s, g i + ∏ i ∈ s, h i ≤ ∏ i ∈ s, f i
<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 → R<VAR>hP : W'.Equation P<GOAL>W'.addXYZ P (W'.neg P) = -W'.dblZ P • ![1, 1, 0]
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f : R<VAR>s t : Localization.Away f<VAR>h_eq : (toBasicOpen R f) s = (toBasicOpen R f) t<GOAL>s = t
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f : R<VAR>t : Localization.Away f<VAR>a b : R<VAR>hb : b ∈ Submonoid.powers f<VAR>h_eq : (toBasicOpen R f) (IsLocalization.mk' (Localization.Away f) a ⟨b, hb⟩) = (toBasicOpen R f) t<GOAL>IsLocalization.mk' (Localization.Away f) a ⟨b, hb⟩ = t
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f a b : R<VAR>hb : b ∈ Submonoid.powers f<VAR>c d : R<VAR>hd : d ∈ Submonoid.powers f<VAR>h_eq : (toBasicOpen R f) (IsLocalization.mk' (Localization.Away f) a ⟨b, hb⟩) = (toBasicOpen R f) (IsLocalization.mk' (Localization.Away f) c ⟨d, hd⟩)<GOAL>IsLocalization.mk' (Localization.Away f) a ⟨b, hb⟩ = IsLocalization.mk' (Localization.Away f) c ⟨d, hd⟩
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f a b : R<VAR>hb : b ∈ Submonoid.powers f<VAR>c d : R<VAR>hd : d ∈ Submonoid.powers f<VAR>h_eq : const R a b (PrimeSpectrum.basicOpen f) ⋯ = const R c d (PrimeSpectrum.basicOpen f) ⋯<GOAL>IsLocalization.mk' (Localization.Away f) a ⟨b, hb⟩ = IsLocalization.mk' (Localization.Away f) c ⟨d, hd⟩
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f a b : R<VAR>hb : b ∈ Submonoid.powers f<VAR>c d : R<VAR>hd : d ∈ Submonoid.powers f<VAR>h_eq : const R a b (PrimeSpectrum.basicOpen f) ⋯ = const R c d (PrimeSpectrum.basicOpen f) ⋯<GOAL>∃ c_1, ↑c_1 * (↑⟨d, hd⟩ * a) = ↑c_1 * (↑⟨b, hb⟩ * c)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f a b : R<VAR>hb : b ∈ Submonoid.powers f<VAR>c d : R<VAR>hd : d ∈ Submonoid.powers f<VAR>h_eq : const R a b (PrimeSpectrum.basicOpen f) ⋯ = const R c d (PrimeSpectrum.basicOpen f) ⋯<VAR>I : Ideal R := { carrier := {r | r * (d * a) = r * (b * c)}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }<GOAL>∃ c_1, ↑c_1 * (↑⟨d, hd⟩ * a) = ↑c_1 * (↑⟨b, hb⟩ * c)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f a b : R<VAR>hb : b ∈ Submonoid.powers f<VAR>c d : R<VAR>hd : d ∈ Submonoid.powers f<VAR>h_eq : const R a b (PrimeSpectrum.basicOpen f) ⋯ = const R c d (PrimeSpectrum.basicOpen f) ⋯<VAR>I : Ideal R := { carrier := {r | r * (d * a) = r * (b * c)}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }<GOAL>f ∈ I.radical
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f a b : R<VAR>hb : b ∈ Submonoid.powers f<VAR>c d : R<VAR>hd : d ∈ Submonoid.powers f<VAR>h_eq : const R a b (PrimeSpectrum.basicOpen f) ⋯ = const R c d (PrimeSpectrum.basicOpen f) ⋯<VAR>I : Ideal R := { carrier := {r | r * (d * a) = r * (b * c)}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }<GOAL>∀ x ∈ PrimeSpectrum.zeroLocus ↑I, f ∈ x.asIdeal
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f a b : R<VAR>hb : b ∈ Submonoid.powers f<VAR>c d : R<VAR>hd : d ∈ Submonoid.powers f<VAR>h_eq : const R a b (PrimeSpectrum.basicOpen f) ⋯ = const R c d (PrimeSpectrum.basicOpen f) ⋯<VAR>I : Ideal R := { carrier := {r | r * (d * a) = r * (b * c)}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }<VAR>p : PrimeSpectrum R<VAR>hfp : p ∈ PrimeSpectrum.zeroLocus ↑I<GOAL>f ∈ p.asIdeal
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f a b : R<VAR>hb : b ∈ Submonoid.powers f<VAR>c d : R<VAR>hd : d ∈ Submonoid.powers f<VAR>h_eq : const R a b (PrimeSpectrum.basicOpen f) ⋯ = const R c d (PrimeSpectrum.basicOpen f) ⋯<VAR>I : Ideal R := { carrier := {r | r * (d * a) = r * (b * c)}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }<VAR>p : PrimeSpectrum R<VAR>hfp : f ∉ p.asIdeal<GOAL>p ∉ PrimeSpectrum.zeroLocus ↑I
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f a b : R<VAR>hb : b ∈ Submonoid.powers f<VAR>c d : R<VAR>hd : d ∈ Submonoid.powers f<VAR>h_eq : const R a b (PrimeSpectrum.basicOpen f) ⋯ = const R c d (PrimeSpectrum.basicOpen f) ⋯<VAR>I : Ideal R := { carrier := {r | r * (d * a) = r * (b * c)}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }<VAR>p : PrimeSpectrum R<VAR>hfp : f ∉ p.asIdeal<GOAL>∃ a ∈ ↑I, a ∉ ↑p.asIdeal
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f a b : R<VAR>hb : b ∈ Submonoid.powers f<VAR>c d : R<VAR>hd : d ∈ Submonoid.powers f<VAR>h_eq : const R a b (PrimeSpectrum.basicOpen f) ⋯ = const R c d (PrimeSpectrum.basicOpen f) ⋯<VAR>I : Ideal R := { carrier := {r | r * (d * a) = r * (b * c)}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }<VAR>p : PrimeSpectrum R<VAR>hfp : f ∉ p.asIdeal<VAR>this : IsLocalization.mk' (Localizations R p) a ⟨b, ⋯⟩ = IsLocalization.mk' (Localizations R p) c ⟨d, ⋯⟩<GOAL>∃ a ∈ ↑I, a ∉ ↑p.asIdeal
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f a b : R<VAR>hb : b ∈ Submonoid.powers f<VAR>c d : R<VAR>hd : d ∈ Submonoid.powers f<VAR>h_eq : const R a b (PrimeSpectrum.basicOpen f) ⋯ = const R c d (PrimeSpectrum.basicOpen f) ⋯<VAR>I : Ideal R := { carrier := {r | r * (d * a) = r * (b * c)}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }<VAR>p : PrimeSpectrum R<VAR>hfp : f ∉ p.asIdeal<VAR>this : ∃ c_1, ↑c_1 * (↑⟨d, ⋯⟩ * a) = ↑c_1 * (↑⟨b, ⋯⟩ * c)<GOAL>∃ a ∈ ↑I, a ∉ ↑p.asIdeal
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>f a b : R<VAR>hb : b ∈ Submonoid.powers f<VAR>c d : R<VAR>hd : d ∈ Submonoid.powers f<VAR>h_eq : const R a b (PrimeSpectrum.basicOpen f) ⋯ = const R c d (PrimeSpectrum.basicOpen f) ⋯<VAR>I : Ideal R := { carrier := {r | r * (d * a) = r * (b * c)}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }<VAR>p : PrimeSpectrum R<VAR>hfp : f ∉ p.asIdeal<VAR>r : ↥p.asIdeal.primeCompl<VAR>hr : ↑r * (↑⟨d, ⋯⟩ * a) = ↑r * (↑⟨b, ⋯⟩ * c)<GOAL>∃ a ∈ ↑I, a ∉ ↑p.asIdeal
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v : Finset α<VAR>hε : 0 < ε<GOAL>⊥.nonUniforms G ε = ∅
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v : Finset α<VAR>hε : 0 < ε<GOAL>∀ (x : Finset α × Finset α), x ∉ ⊥.nonUniforms G ε
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u✝ v✝ : Finset α<VAR>hε : 0 < ε<VAR>u v : Finset α<GOAL>(u, v) ∉ ⊥.nonUniforms G ε
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u✝ v✝ : Finset α<VAR>hε : 0 < ε<VAR>u v : Finset α<GOAL>∀ (x : α), x ∈ A ∧ { toFun := singleton, inj' := ⋯ } x = u → ∀ (x : α), x ∈ A ∧ { toFun := singleton, inj' := ⋯ } x = v → u ≠ v → G.IsUniform ε u v
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : DecidableEq α<VAR>A : Finset α<VAR>P : Finpartition A<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε δ : 𝕜<VAR>u v : Finset α<VAR>hε : 0 < ε<VAR>x : α<VAR>left✝¹ : x ∈ A<VAR>y : α<VAR>left✝ : y ∈ A<VAR>a✝ : ¬{x} = {y}<GOAL>G.IsUniform ε {x} {y}
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>hf : Martingale f ℱ μ<VAR>hg : Martingale g ℱ μ<GOAL>Martingale (f - g) ℱ μ
<VAR>Ω : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Preorder ι<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f g : ι → Ω → E<VAR>ℱ : Filtration ι m0<VAR>hf : Martingale f ℱ μ<VAR>hg : Martingale g ℱ μ<GOAL>Martingale (f + -g) ℱ μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β<VAR>s : (i : ι) → κ i → Set β<GOAL>f ⁻¹' ⋂ i, ⋂ j, s i j = ⋂ i, ⋂ j, f ⁻¹' s i j
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : FirstCountableTopology X<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : T2Space X<VAR>S : Set X<GOAL>IsPreirreducible S ↔ S.Subsingleton
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : FirstCountableTopology X<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : T2Space X<VAR>S : Set X<VAR>h : IsPreirreducible S<VAR>x : X<VAR>hx : x ∈ S<VAR>y : X<VAR>hy : y ∈ S<GOAL>x = y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : FirstCountableTopology X<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : T2Space X<VAR>S : Set X<VAR>h : IsPreirreducible S<VAR>x : X<VAR>hx : x ∈ S<VAR>y : X<VAR>hy : y ∈ S<VAR>e : ¬x = y<GOAL>False
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : FirstCountableTopology X<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : T2Space X<VAR>S : Set X<VAR>h : IsPreirreducible S<VAR>x : X<VAR>hx : x ∈ S<VAR>y : X<VAR>hy : y ∈ S<VAR>e : ¬x = y<VAR>U V : Set X<VAR>hU : IsOpen U<VAR>hV : IsOpen V<VAR>hxU : x ∈ U<VAR>hyV : y ∈ V<VAR>h' : Disjoint U V<GOAL>False
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι✝ : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι✝<VAR>c : R<VAR>t : Finset ι✝<VAR>w✝ : ι✝ → R<VAR>z✝ : ι✝ → E<VAR>ι : Sort u_8<VAR>w : ι → R<VAR>z : ι → E<VAR>s : Set E<VAR>hs : Convex R s<VAR>h₀ : ∀ (i : ι), 0 ≤ w i<VAR>h₁ : ∑ᶠ (i : ι), w i = 1<VAR>hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s<GOAL>∑ᶠ (i : ι), w i • z i ∈ s
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι✝ : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι✝<VAR>c : R<VAR>t : Finset ι✝<VAR>w✝ : ι✝ → R<VAR>z✝ : ι✝ → E<VAR>ι : Sort u_8<VAR>w : ι → R<VAR>z : ι → E<VAR>s : Set E<VAR>hs : Convex R s<VAR>h₀ : ∀ (i : ι), 0 ≤ w i<VAR>h₁ : ∑ᶠ (i : ι), w i = 1<VAR>hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s<VAR>hfin_w : (support (w ∘ PLift.down)).Finite<GOAL>∑ᶠ (i : ι), w i • z i ∈ s
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι✝ : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι✝<VAR>c : R<VAR>t : Finset ι✝<VAR>w✝ : ι✝ → R<VAR>z✝ : ι✝ → E<VAR>ι : Sort u_8<VAR>w : ι → R<VAR>z : ι → E<VAR>s : Set E<VAR>hs : Convex R s<VAR>h₀ : ∀ (i : ι), 0 ≤ w i<VAR>h₁ : ∑ᶠ (i : ι), w i = 1<VAR>hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s<VAR>hfin_w : (support (w ∘ PLift.down)).Finite<VAR>hsub : support ((fun i => w i • z i) ∘ PLift.down) ⊆ ↑hfin_w.toFinset<GOAL>∑ᶠ (i : ι), w i • z i ∈ s
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι✝ : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι✝<VAR>c : R<VAR>t : Finset ι✝<VAR>w✝ : ι✝ → R<VAR>z✝ : ι✝ → E<VAR>ι : Sort u_8<VAR>w : ι → R<VAR>z : ι → E<VAR>s : Set E<VAR>hs : Convex R s<VAR>h₀ : ∀ (i : ι), 0 ≤ w i<VAR>h₁ : ∑ᶠ (i : ι), w i = 1<VAR>hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s<VAR>hfin_w : (support (w ∘ PLift.down)).Finite<VAR>hsub : support ((fun i => w i • z i) ∘ PLift.down) ⊆ ↑hfin_w.toFinset<GOAL>∑ i ∈ hfin_w.toFinset, w i.down • z i.down ∈ s
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι✝ : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i j : ι✝<VAR>c : R<VAR>t : Finset ι✝<VAR>w✝ : ι✝ → R<VAR>z✝ : ι✝ → E<VAR>ι : Sort u_8<VAR>w : ι → R<VAR>z : ι → E<VAR>s : Set E<VAR>hs : Convex R s<VAR>h₀ : ∀ (i : ι), 0 ≤ w i<VAR>h₁ : ∑ᶠ (i : ι), w i = 1<VAR>hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s<VAR>hfin_w : (support (w ∘ PLift.down)).Finite<VAR>hsub : support ((fun i => w i • z i) ∘ PLift.down) ⊆ ↑hfin_w.toFinset<GOAL>∑ i ∈ hfin_w.toFinset, w i.down = 1
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι✝ : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s✝ : Set E<VAR>i✝ j : ι✝<VAR>c : R<VAR>t : Finset ι✝<VAR>w✝ : ι✝ → R<VAR>z✝ : ι✝ → E<VAR>ι : Sort u_8<VAR>w : ι → R<VAR>z : ι → E<VAR>s : Set E<VAR>hs : Convex R s<VAR>h₀ : ∀ (i : ι), 0 ≤ w i<VAR>h₁ : ∑ᶠ (i : ι), w i = 1<VAR>hz : ∀ (i : ι), w i ≠ 0 → z i ∈ s<VAR>hfin_w : (support (w ∘ PLift.down)).Finite<VAR>hsub : support ((fun i => w i • z i) ∘ PLift.down) ⊆ ↑hfin_w.toFinset<VAR>i : PLift ι<VAR>hi : i ∈ hfin_w.toFinset<GOAL>w i.down ≠ 0
<VAR>G : Type u_1<VAR>inst✝¹⁰ : Group G<VAR>inst✝⁹ : MeasurableSpace G<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : BorelSpace G<VAR>μ : Measure G<VAR>Γ : Subgroup G<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ<VAR>inst✝⁵ : Countable ↥Γ<VAR>inst✝⁴ : MeasurableSpace (G ⧸ Γ)<VAR>inst✝³ : BorelSpace (G ⧸ Γ)<VAR>K : Type u_2<VAR>inst✝² : NormedField K<VAR>inst✝¹ : NormedSpace ℝ K<VAR>inst✝ : μ.IsMulRightInvariant<VAR>f : G → K<VAR>f_ℒ_1 : Integrable f μ<VAR>g : G ⧸ Γ → K<VAR>hg : AEStronglyMeasurable g (Measure.map mk (μ.restrict 𝓕))<VAR>g_ℒ_infinity : essSup (fun x => ↑‖g x‖₊) (Measure.map mk (μ.restrict 𝓕)) ≠ ⊤<VAR>F_ae_measurable : AEStronglyMeasurable (automorphize f) (Measure.map mk (μ.restrict 𝓕))<VAR>π : G → G ⧸ Γ := mk<GOAL>∫ (x : G), g ↑x * f x ∂μ = ∫ (x : G ⧸ Γ), g x * automorphize f x ∂Measure.map mk (μ.restrict 𝓕)
<VAR>G : Type u_1<VAR>inst✝¹⁰ : Group G<VAR>inst✝⁹ : MeasurableSpace G<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : BorelSpace G<VAR>μ : Measure G<VAR>Γ : Subgroup G<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ<VAR>inst✝⁵ : Countable ↥Γ<VAR>inst✝⁴ : MeasurableSpace (G ⧸ Γ)<VAR>inst✝³ : BorelSpace (G ⧸ Γ)<VAR>K : Type u_2<VAR>inst✝² : NormedField K<VAR>inst✝¹ : NormedSpace ℝ K<VAR>inst✝ : μ.IsMulRightInvariant<VAR>f : G → K<VAR>f_ℒ_1 : Integrable f μ<VAR>g : G ⧸ Γ → K<VAR>hg : AEStronglyMeasurable g (Measure.map mk (μ.restrict 𝓕))<VAR>g_ℒ_infinity : essSup (fun x => ↑‖g x‖₊) (Measure.map mk (μ.restrict 𝓕)) ≠ ⊤<VAR>F_ae_measurable : AEStronglyMeasurable (automorphize f) (Measure.map mk (μ.restrict 𝓕))<VAR>π : G → G ⧸ Γ := mk<VAR>meas_π : Measurable π<GOAL>∫ (x : G), g ↑x * f x ∂μ = ∫ (x : G ⧸ Γ), g x * automorphize f x ∂Measure.map mk (μ.restrict 𝓕)
<VAR>G : Type u_1<VAR>inst✝¹⁰ : Group G<VAR>inst✝⁹ : MeasurableSpace G<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : BorelSpace G<VAR>μ : Measure G<VAR>Γ : Subgroup G<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ<VAR>inst✝⁵ : Countable ↥Γ<VAR>inst✝⁴ : MeasurableSpace (G ⧸ Γ)<VAR>inst✝³ : BorelSpace (G ⧸ Γ)<VAR>K : Type u_2<VAR>inst✝² : NormedField K<VAR>inst✝¹ : NormedSpace ℝ K<VAR>inst✝ : μ.IsMulRightInvariant<VAR>f : G → K<VAR>f_ℒ_1 : Integrable f μ<VAR>g : G ⧸ Γ → K<VAR>hg : AEStronglyMeasurable g (Measure.map mk (μ.restrict 𝓕))<VAR>g_ℒ_infinity : essSup (fun x => ↑‖g x‖₊) (Measure.map mk (μ.restrict 𝓕)) ≠ ⊤<VAR>F_ae_measurable : AEStronglyMeasurable (automorphize f) (Measure.map mk (μ.restrict 𝓕))<VAR>π : G → G ⧸ Γ := mk<VAR>meas_π : Measurable π<VAR>H₀ : automorphize (g ∘ π * f) = g * automorphize f<GOAL>∫ (x : G), g ↑x * f x ∂μ = ∫ (x : G ⧸ Γ), g x * automorphize f x ∂Measure.map mk (μ.restrict 𝓕)
<VAR>G : Type u_1<VAR>inst✝¹⁰ : Group G<VAR>inst✝⁹ : MeasurableSpace G<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : BorelSpace G<VAR>μ : Measure G<VAR>Γ : Subgroup G<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ<VAR>inst✝⁵ : Countable ↥Γ<VAR>inst✝⁴ : MeasurableSpace (G ⧸ Γ)<VAR>inst✝³ : BorelSpace (G ⧸ Γ)<VAR>K : Type u_2<VAR>inst✝² : NormedField K<VAR>inst✝¹ : NormedSpace ℝ K<VAR>inst✝ : μ.IsMulRightInvariant<VAR>f : G → K<VAR>f_ℒ_1 : Integrable f μ<VAR>g : G ⧸ Γ → K<VAR>hg : AEStronglyMeasurable g (Measure.map mk (μ.restrict 𝓕))<VAR>g_ℒ_infinity : essSup (fun x => ↑‖g x‖₊) (Measure.map mk (μ.restrict 𝓕)) ≠ ⊤<VAR>F_ae_measurable : AEStronglyMeasurable (automorphize f) (Measure.map mk (μ.restrict 𝓕))<VAR>π : G → G ⧸ Γ := mk<VAR>meas_π : Measurable π<VAR>H₀ : automorphize (g ∘ π * f) = g * automorphize f<GOAL>∫ (x : G), g (π x) * f x ∂μ = ∫ (x : G ⧸ Γ), automorphize (g ∘ π * f) x ∂Measure.map mk (μ.restrict 𝓕)
<VAR>G : Type u_1<VAR>inst✝¹⁰ : Group G<VAR>inst✝⁹ : MeasurableSpace G<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : BorelSpace G<VAR>μ : Measure G<VAR>Γ : Subgroup G<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ<VAR>inst✝⁵ : Countable ↥Γ<VAR>inst✝⁴ : MeasurableSpace (G ⧸ Γ)<VAR>inst✝³ : BorelSpace (G ⧸ Γ)<VAR>K : Type u_2<VAR>inst✝² : NormedField K<VAR>inst✝¹ : NormedSpace ℝ K<VAR>inst✝ : μ.IsMulRightInvariant<VAR>f : G → K<VAR>f_ℒ_1 : Integrable f μ<VAR>g : G ⧸ Γ → K<VAR>hg : AEStronglyMeasurable g (Measure.map mk (μ.restrict 𝓕))<VAR>g_ℒ_infinity : essSup (fun x => ↑‖g x‖₊) (Measure.map mk (μ.restrict 𝓕)) ≠ ⊤<VAR>F_ae_measurable : AEStronglyMeasurable (automorphize f) (Measure.map mk (μ.restrict 𝓕))<VAR>π : G → G ⧸ Γ := mk<VAR>meas_π : Measurable π<VAR>H₀ : automorphize (g ∘ π * f) = g * automorphize f<VAR>H₁ : Integrable (g ∘ π * f) μ<GOAL>∫ (x : G), g (π x) * f x ∂μ = ∫ (x : G ⧸ Γ), automorphize (g ∘ π * f) x ∂Measure.map mk (μ.restrict 𝓕)
<VAR>G : Type u_1<VAR>inst✝¹⁰ : Group G<VAR>inst✝⁹ : MeasurableSpace G<VAR>inst✝⁸ : TopologicalSpace G<VAR>inst✝⁷ : TopologicalGroup G<VAR>inst✝⁶ : BorelSpace G<VAR>μ : Measure G<VAR>Γ : Subgroup G<VAR>𝓕 : Set G<VAR>h𝓕 : IsFundamentalDomain (↥Γ.op) 𝓕 μ<VAR>inst✝⁵ : Countable ↥Γ<VAR>inst✝⁴ : MeasurableSpace (G ⧸ Γ)<VAR>inst✝³ : BorelSpace (G ⧸ Γ)<VAR>K : Type u_2<VAR>inst✝² : NormedField K<VAR>inst✝¹ : NormedSpace ℝ K<VAR>inst✝ : μ.IsMulRightInvariant<VAR>f : G → K<VAR>f_ℒ_1 : Integrable f μ<VAR>g : G ⧸ Γ → K<VAR>hg : AEStronglyMeasurable g (Measure.map mk (μ.restrict 𝓕))<VAR>g_ℒ_infinity : essSup (fun x => ↑‖g x‖₊) (Measure.map mk (μ.restrict 𝓕)) ≠ ⊤<VAR>F_ae_measurable : AEStronglyMeasurable (automorphize f) (Measure.map mk (μ.restrict 𝓕))<VAR>π : G → G ⧸ Γ := mk<VAR>meas_π : Measurable π<VAR>H₀ : automorphize (g ∘ π * f) = g * automorphize f<VAR>H₁ : Integrable (g ∘ π * f) μ<VAR>H₂ : AEStronglyMeasurable (automorphize (g ∘ π * f)) (Measure.map mk (μ.restrict 𝓕))<GOAL>∫ (x : G), g (π x) * f x ∂μ = ∫ (x : G ⧸ Γ), automorphize (g ∘ π * f) x ∂Measure.map mk (μ.restrict 𝓕)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>w z : ℂ<GOAL>(Complex.orientation.kahler w) z = (starRingEnd ℂ) w * z
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>w z : ℂ<GOAL>↑⟪w, z⟫_ℝ + (Complex.orientation.areaForm w) z • I = (starRingEnd ℂ) w * z
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>α : Type u_5<VAR>f : X → α → Z<VAR>s : Set α<VAR>t : Set Z<VAR>ht : IsClosed t<VAR>hf : ∀ a ∈ s, Continuous fun x => f x a<GOAL>IsClosed {x | MapsTo (f x) s t}
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>r : R<VAR>f : R[X]<GOAL>((taylor r) f).coeff 0 = eval r f
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝¹ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝ : Monoid N<GOAL>⨆ i, MonoidHom.mrange of = ⊤
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>S : Type v<VAR>inst✝³ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>hfp : NeZero e<VAR>inst✝² : IsDedekindDomain S<VAR>hP0 : P ≠ ⊥<VAR>inst✝¹ : p.IsMaximal<VAR>inst✝ : P.IsPrime<VAR>he : e ≠ 0<VAR>this✝¹ : NeZero e := { out := he }<VAR>this✝ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero f p P<VAR>this : Field (R ⧸ p) := Quotient.field p<GOAL>finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>S : Type v<VAR>inst✝³ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>hfp : NeZero e<VAR>inst✝² : IsDedekindDomain S<VAR>hP0 : P ≠ ⊥<VAR>inst✝¹ : p.IsMaximal<VAR>inst✝ : P.IsPrime<VAR>he : e ≠ 0<VAR>this✝¹ : NeZero e := { out := he }<VAR>this✝ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero f p P<VAR>this : Field (R ⧸ p) := Quotient.field p<VAR>hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)<GOAL>finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>S : Type v<VAR>inst✝³ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>hfp : NeZero e<VAR>inst✝² : IsDedekindDomain S<VAR>hP0 : P ≠ ⊥<VAR>inst✝¹ : p.IsMaximal<VAR>inst✝ : P.IsPrime<VAR>he : e ≠ 0<VAR>this✝¹ : NeZero e := { out := he }<VAR>this✝ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero f p P<VAR>this : Field (R ⧸ p) := Quotient.field p<VAR>hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)<VAR>hP : ¬FiniteDimensional (R ⧸ p) (S ⧸ P)<GOAL>finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>S : Type v<VAR>inst✝³ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>hfp : NeZero e<VAR>inst✝² : IsDedekindDomain S<VAR>hP0 : P ≠ ⊥<VAR>inst✝¹ : p.IsMaximal<VAR>inst✝ : P.IsPrime<VAR>he : e ≠ 0<VAR>this✝¹ : NeZero e := { out := he }<VAR>this✝ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero f p P<VAR>this : Field (R ⧸ p) := Quotient.field p<VAR>hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)<VAR>hP : ¬FiniteDimensional (R ⧸ p) (S ⧸ P)<VAR>hPe : ¬FiniteDimensional (R ⧸ p) (S ⧸ P ^ e)<GOAL>finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)
<VAR>m : Type u_1<VAR>n✝ : Type u_2<VAR>inst✝⁴ : DecidableEq n✝<VAR>inst✝³ : Fintype n✝<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>A B : Matrix (Fin (n + 1)) (Fin (n + 1)) R<VAR>c : Fin n → R<VAR>A_zero : ∀ (i : Fin (n + 1)), A i 0 = B i 0<VAR>A_succ : ∀ (i : Fin (n + 1)) (j : Fin n), A i j.succ = B i j.succ + c j * A i j.castSucc<GOAL>A.det = B.det