ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>β : Type u_4<VAR>β' : Type u_5<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>mβ : MeasurableSpace β<VAR>mβ' : MeasurableSpace β'<VAR>f' : Ω → β<VAR>g' : Ω → β'<VAR>hfg : ProbabilityTheory.Kernel.IndepFun f g κ μ<VAR>hf : ∀ᵐ (a : α) ∂μ, f =ᵐ[κ a] f'<VAR>hg : ∀ᵐ (a : α) ∂μ, g =ᵐ[κ a] g'<GOAL>ProbabilityTheory.Kernel.IndepFun f' g' κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>β : Type u_4<VAR>β' : Type u_5<VAR>γ : Type u_6<VAR>γ' : Type u_7<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>mβ : MeasurableSpace β<VAR>mβ' : MeasurableSpace β'<VAR>mγ : MeasurableSpace γ<VAR>mγ' : MeasurableSpace γ'<VAR>φ : β → γ<VAR>ψ : β' → γ'<VAR>hfg : ProbabilityTheory.Kernel.IndepFun f g κ μ<VAR>hφ : Measurable φ<VAR>hψ : Measurable ψ<GOAL>ProbabilityTheory.Kernel.IndepFun (φ ∘ f) (ψ ∘ g) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>β : Type u_4<VAR>β' : Type u_5<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>_mβ : MeasurableSpace β<VAR>_mβ' : MeasurableSpace β'<VAR>Neg β'<VAR>MeasurableNeg β'<VAR>hfg : ProbabilityTheory.Kernel.IndepFun f g κ μ<GOAL>ProbabilityTheory.Kernel.IndepFun f (-g) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>β : Type u_4<VAR>β' : Type u_5<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>_mβ : MeasurableSpace β<VAR>_mβ' : MeasurableSpace β'<VAR>Neg β<VAR>MeasurableNeg β<VAR>hfg : ProbabilityTheory.Kernel.IndepFun f g κ μ<GOAL>ProbabilityTheory.Kernel.IndepFun (-f) g κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>β : ι → Type u_8<VAR>m : (i : ι) → MeasurableSpace (β i)<VAR>f : (i : ι) → Ω → β i<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>Subsingleton ι<GOAL>ProbabilityTheory.Kernel.iIndepFun m f κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>β : ι → Type u_8<VAR>m : (i : ι) → MeasurableSpace (β i)<VAR>f : (i : ι) → Ω → β i<VAR>h : ProbabilityTheory.Kernel.iIndepFun m f κ μ<GOAL>∀ᵐ (a : α) ∂μ, MeasureTheory.IsProbabilityMeasure (κ a)
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>β : ι → Type u_8<VAR>m : (i : ι) → MeasurableSpace (β i)<VAR>f : (i : ι) → Ω → β i<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>S T : Finset ι<VAR>hST : Disjoint S T<VAR>hf_Indep : ProbabilityTheory.Kernel.iIndepFun m f κ μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<GOAL>ProbabilityTheory.Kernel.IndepFun (fun a i => f (↑i) a) (fun a i => f (↑i) a) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>β : ι → Type u_8<VAR>m : (i : ι) → MeasurableSpace (β i)<VAR>f : (i : ι) → Ω → β i<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>hf_Indep : ProbabilityTheory.Kernel.iIndepFun m f κ μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>i j k : ι<VAR>hik : i ≠ k<VAR>hjk : j ≠ k<GOAL>ProbabilityTheory.Kernel.IndepFun (fun a => (f i a, f j a)) (f k) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>β : ι → Type u_8<VAR>m : (i : ι) → MeasurableSpace (β i)<VAR>f : (i : ι) → Ω → β i<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>hf_indep : ProbabilityTheory.Kernel.iIndepFun m f κ μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>i j k l : ι<VAR>hik : i ≠ k<VAR>hil : i ≠ l<VAR>hjk : j ≠ k<VAR>hjl : j ≠ l<GOAL>ProbabilityTheory.Kernel.IndepFun (fun a => (f i a, f j a)) (fun a => (f k a, f l a)) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_8<VAR>m : MeasurableSpace β<VAR>Add β<VAR>MeasurableAdd₂ β<VAR>f : ι → Ω → β<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>hf_indep : ProbabilityTheory.Kernel.iIndepFun (fun x => m) f κ μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>i j k : ι<VAR>hik : i ≠ k<VAR>hjk : j ≠ k<GOAL>ProbabilityTheory.Kernel.IndepFun (f i + f j) (f k) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_8<VAR>m : MeasurableSpace β<VAR>Mul β<VAR>MeasurableMul₂ β<VAR>f : ι → Ω → β<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>hf_indep : ProbabilityTheory.Kernel.iIndepFun (fun x => m) f κ μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>i j k : ι<VAR>hik : i ≠ k<VAR>hjk : j ≠ k<GOAL>ProbabilityTheory.Kernel.IndepFun (f i * f j) (f k) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_8<VAR>m : MeasurableSpace β<VAR>Mul β<VAR>MeasurableMul₂ β<VAR>f : ι → Ω → β<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>hf_indep : ProbabilityTheory.Kernel.iIndepFun (fun x => m) f κ μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>i j k : ι<VAR>hij : i ≠ j<VAR>hik : i ≠ k<GOAL>ProbabilityTheory.Kernel.IndepFun (f i) (f j * f k) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_8<VAR>m : MeasurableSpace β<VAR>Add β<VAR>MeasurableAdd₂ β<VAR>f : ι → Ω → β<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>hf_indep : ProbabilityTheory.Kernel.iIndepFun (fun x => m) f κ μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>i j k : ι<VAR>hij : i ≠ j<VAR>hik : i ≠ k<GOAL>ProbabilityTheory.Kernel.IndepFun (f i) (f j + f k) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_8<VAR>m : MeasurableSpace β<VAR>Mul β<VAR>MeasurableMul₂ β<VAR>f : ι → Ω → β<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>hf_indep : ProbabilityTheory.Kernel.iIndepFun (fun x => m) f κ μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>i j k l : ι<VAR>hik : i ≠ k<VAR>hil : i ≠ l<VAR>hjk : j ≠ k<VAR>hjl : j ≠ l<GOAL>ProbabilityTheory.Kernel.IndepFun (f i * f j) (f k * f l) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_8<VAR>m : MeasurableSpace β<VAR>Add β<VAR>MeasurableAdd₂ β<VAR>f : ι → Ω → β<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>hf_indep : ProbabilityTheory.Kernel.iIndepFun (fun x => m) f κ μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>i j k l : ι<VAR>hik : i ≠ k<VAR>hil : i ≠ l<VAR>hjk : j ≠ k<VAR>hjl : j ≠ l<GOAL>ProbabilityTheory.Kernel.IndepFun (f i + f j) (f k + f l) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_8<VAR>m : MeasurableSpace β<VAR>Div β<VAR>MeasurableDiv₂ β<VAR>f : ι → Ω → β<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>hf_indep : ProbabilityTheory.Kernel.iIndepFun (fun x => m) f κ μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>i j k : ι<VAR>hik : i ≠ k<VAR>hjk : j ≠ k<GOAL>ProbabilityTheory.Kernel.IndepFun (f i / f j) (f k) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_8<VAR>m : MeasurableSpace β<VAR>Sub β<VAR>MeasurableSub₂ β<VAR>f : ι → Ω → β<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>hf_indep : ProbabilityTheory.Kernel.iIndepFun (fun x => m) f κ μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>i j k : ι<VAR>hik : i ≠ k<VAR>hjk : j ≠ k<GOAL>ProbabilityTheory.Kernel.IndepFun (f i - f j) (f k) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_8<VAR>m : MeasurableSpace β<VAR>Div β<VAR>MeasurableDiv₂ β<VAR>f : ι → Ω → β<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>hf_indep : ProbabilityTheory.Kernel.iIndepFun (fun x => m) f κ μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>i j k : ι<VAR>hij : i ≠ j<VAR>hik : i ≠ k<GOAL>ProbabilityTheory.Kernel.IndepFun (f i) (f j / f k) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_8<VAR>m : MeasurableSpace β<VAR>Sub β<VAR>MeasurableSub₂ β<VAR>f : ι → Ω → β<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>hf_indep : ProbabilityTheory.Kernel.iIndepFun (fun x => m) f κ μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>i j k : ι<VAR>hij : i ≠ j<VAR>hik : i ≠ k<GOAL>ProbabilityTheory.Kernel.IndepFun (f i) (f j - f k) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_8<VAR>m : MeasurableSpace β<VAR>Div β<VAR>MeasurableDiv₂ β<VAR>f : ι → Ω → β<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>hf_indep : ProbabilityTheory.Kernel.iIndepFun (fun x => m) f κ μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>i j k l : ι<VAR>hik : i ≠ k<VAR>hil : i ≠ l<VAR>hjk : j ≠ k<VAR>hjl : j ≠ l<GOAL>ProbabilityTheory.Kernel.IndepFun (f i / f j) (f k / f l) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_8<VAR>m : MeasurableSpace β<VAR>Sub β<VAR>MeasurableSub₂ β<VAR>f : ι → Ω → β<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>hf_indep : ProbabilityTheory.Kernel.iIndepFun (fun x => m) f κ μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>i j k l : ι<VAR>hik : i ≠ k<VAR>hil : i ≠ l<VAR>hjk : j ≠ k<VAR>hjl : j ≠ l<GOAL>ProbabilityTheory.Kernel.IndepFun (f i - f j) (f k - f l) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_8<VAR>m : MeasurableSpace β<VAR>CommMonoid β<VAR>MeasurableMul₂ β<VAR>f : ι → Ω → β<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>hf_Indep : ProbabilityTheory.Kernel.iIndepFun (fun x => m) f κ μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>s : Finset ι<VAR>i : ι<VAR>hi : i ∉ s<GOAL>ProbabilityTheory.Kernel.IndepFun (∏ j ∈ s, f j) (f i) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_8<VAR>m : MeasurableSpace β<VAR>AddCommMonoid β<VAR>MeasurableAdd₂ β<VAR>f : ι → Ω → β<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>hf_Indep : ProbabilityTheory.Kernel.iIndepFun (fun x => m) f κ μ<VAR>hf_meas : ∀ (i : ι), Measurable (f i)<VAR>s : Finset ι<VAR>i : ι<VAR>hi : i ∉ s<GOAL>ProbabilityTheory.Kernel.IndepFun (∑ j ∈ s, f j) (f i) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_8<VAR>m : MeasurableSpace β<VAR>AddCommMonoid β<VAR>MeasurableAdd₂ β<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>f : ℕ → Ω → β<VAR>hf_Indep : ProbabilityTheory.Kernel.iIndepFun (fun x => m) f κ μ<VAR>hf_meas : ∀ (i : ℕ), Measurable (f i)<VAR>n : ℕ<GOAL>ProbabilityTheory.Kernel.IndepFun (∑ j ∈ Finset.range n, f j) (f n) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>β : Type u_8<VAR>m : MeasurableSpace β<VAR>CommMonoid β<VAR>MeasurableMul₂ β<VAR>ProbabilityTheory.IsMarkovKernel κ<VAR>f : ℕ → Ω → β<VAR>hf_Indep : ProbabilityTheory.Kernel.iIndepFun (fun x => m) f κ μ<VAR>hf_meas : ∀ (i : ℕ), Measurable (f i)<VAR>n : ℕ<GOAL>ProbabilityTheory.Kernel.IndepFun (∏ j ∈ Finset.range n, f j) (f n) κ μ
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>β : Type u_4<VAR>_mα : MeasurableSpace α<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : ProbabilityTheory.Kernel α Ω<VAR>μ : MeasureTheory.Measure α<VAR>Zero β<VAR>One β<VAR>m : MeasurableSpace β<VAR>s : ι → Set Ω<VAR>hs : ProbabilityTheory.Kernel.iIndepSet s κ μ<GOAL>ProbabilityTheory.Kernel.iIndepFun (fun _n => m) (fun n => (s n).indicator fun _ω => 1) κ μ
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>Ring R<VAR>self : Valuation R Γ₀<VAR>x y : R<GOAL>(↑self.toMonoidWithZeroHom).toFun (x + y) ≤ max ((↑self.toMonoidWithZeroHom).toFun x) ((↑self.toMonoidWithZeroHom).toFun y)
<VAR>F : Type u_7<VAR>R : outParam (Type u_5)<VAR>Γ₀ : outParam (Type u_6)<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>Ring R<VAR>FunLike F R Γ₀<VAR>self : ValuationClass F R Γ₀<VAR>f : F<VAR>x y : R<GOAL>f (x + y) ≤ max (f x) (f y)
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>f : R →*₀ Γ₀<VAR>h : ∀ (x y : R), (↑f).toFun (x + y) ≤ max ((↑f).toFun x) ((↑f).toFun y)<GOAL>⇑{ toMonoidWithZeroHom := f, map_add_le_max' := h } = ⇑f
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>v : Valuation R Γ₀<GOAL>(↑v.toMonoidWithZeroHom).toFun = ⇑v
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>v : Valuation R Γ₀<GOAL>⇑v.toMonoidWithZeroHom = ⇑v
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>v₁ v₂ : Valuation R Γ₀<VAR>h : ∀ (r : R), v₁ r = v₂ r<GOAL>v₁ = v₂
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>v : Valuation R Γ₀<GOAL>⇑↑v = ⇑v
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>v : Valuation R Γ₀<GOAL>v 0 = 0
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>v : Valuation R Γ₀<GOAL>v 1 = 1
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x y : R<GOAL>v (x * y) = v x * v y
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x y : R<GOAL>v (x + y) ≤ max (v x) (v y)
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x y : R<GOAL>v (x + y) ≤ v x ∨ v (x + y) ≤ v y
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x y : R<VAR>g : Γ₀<VAR>hx : v x ≤ g<VAR>hy : v y ≤ g<GOAL>v (x + y) ≤ g
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x y : R<VAR>g : Γ₀<VAR>hx : v x < g<VAR>hy : v y < g<GOAL>v (x + y) < g
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>ι : Type u_7<VAR>s : Finset ι<VAR>f : ι → R<VAR>g : Γ₀<VAR>hf : ∀ i ∈ s, v (f i) ≤ g<GOAL>v (∑ i ∈ s, f i) ≤ g
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>ι : Type u_7<VAR>s : Finset ι<VAR>f : ι → R<VAR>g : Γ₀<VAR>hg : g ≠ 0<VAR>hf : ∀ i ∈ s, v (f i) < g<GOAL>v (∑ i ∈ s, f i) < g
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>ι : Type u_7<VAR>s : Finset ι<VAR>f : ι → R<VAR>g : Γ₀<VAR>hg : 0 < g<VAR>hf : ∀ i ∈ s, v (f i) < g<GOAL>v (∑ i ∈ s, f i) < g
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x : R<VAR>n : ℕ<GOAL>v (x ^ n) = v x ^ n
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>v₁ v₂ : Valuation R Γ₀<GOAL>v₁ = v₂ ↔ ∀ (r : R), v₁ r = v₂ r
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>Γ₀ : Type u_4<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>Nontrivial Γ₀<VAR>v : Valuation K Γ₀<VAR>x : K<GOAL>v x = 0 ↔ x = 0
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>Γ₀ : Type u_4<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>Nontrivial Γ₀<VAR>v : Valuation K Γ₀<VAR>x : K<GOAL>v x ≠ 0 ↔ x ≠ 0
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>u : Rˣ<GOAL>↑((Units.map ↑v) u) = v ↑u
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>S : Type u_7<VAR>Ring S<VAR>f : S →+* R<VAR>v : Valuation R Γ₀<VAR>s : S<GOAL>(Valuation.comap f v) s = v (f s)
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>v : Valuation R Γ₀<GOAL>Valuation.comap (RingHom.id R) v = v
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>S₁ : Type u_7<VAR>S₂ : Type u_8<VAR>Ring S₁<VAR>Ring S₂<VAR>f : S₁ →+* S₂<VAR>g : S₂ →+* R<GOAL>Valuation.comap (g.comp f) v = Valuation.comap f (Valuation.comap g v)
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x : R<GOAL>v (-x) = v x
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x y : R<GOAL>v (x - y) = v (y - x)
<VAR>Γ₀ : Type u_4<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>R : Type u_7<VAR>DivisionRing R<VAR>v : Valuation R Γ₀<VAR>x : R<GOAL>v x⁻¹ = (v x)⁻¹
<VAR>Γ₀ : Type u_4<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>R : Type u_7<VAR>DivisionRing R<VAR>v : Valuation R Γ₀<VAR>x y : R<GOAL>v (x / y) = v x / v y
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x y : R<GOAL>v (x - y) ≤ max (v x) (v y)
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x y : R<VAR>g : Γ₀<VAR>hx : v x ≤ g<VAR>hy : v y ≤ g<GOAL>v (x - y) ≤ g
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x y : R<VAR>h : v x ≠ v y<GOAL>v (x + y) = max (v x) (v y)
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x y : R<VAR>h : v x < v y<GOAL>v (x + y) = v y
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x y : R<VAR>h : v y < v x<GOAL>v (x + y) = v x
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x y : R<VAR>h : v x < v y<GOAL>v (x - y) = v y
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x y : R<VAR>h : v y < v x<GOAL>v (x - y) = v x
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x y : R<VAR>h : v (y - x) < v x<GOAL>v y = v x
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x : R<VAR>h : v x < 1<GOAL>v (1 + x) = 1
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x : R<VAR>h : v x < 1<GOAL>v (1 - x) = 1
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>Γ₀ : Type u_4<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation K Γ₀<VAR>x : K<VAR>h : x ≠ 0<GOAL>1 < v x ↔ v x⁻¹ < 1
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>Γ₀ : Type u_4<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation K Γ₀<VAR>x : K<VAR>h : x ≠ 0<GOAL>1 ≤ v x ↔ v x⁻¹ ≤ 1
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>Γ₀ : Type u_4<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation K Γ₀<VAR>x : K<VAR>h : x ≠ 0<GOAL>v x < 1 ↔ 1 < v x⁻¹
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>Γ₀ : Type u_4<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation K Γ₀<VAR>x : K<VAR>h : x ≠ 0<GOAL>v x ≤ 1 ↔ 1 ≤ v x⁻¹
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>Γ₀ : Type u_4<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation K Γ₀<VAR>x : K<GOAL>v x = 1 ↔ v x⁻¹ = 1
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>Γ₀ : Type u_4<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation K Γ₀<VAR>x : K<GOAL>v x ≤ 1 ∨ v x⁻¹ < 1
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>Γ₀ : Type u_4<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation K Γ₀<VAR>x : K<GOAL>v x ≤ 1 ∨ v x⁻¹ ≤ 1
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>v : Valuation R Γ₀<GOAL>v.IsEquiv v
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Ring R<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>LinearOrderedCommMonoidWithZero Γ'₀<VAR>v₁ : Valuation R Γ₀<VAR>v₂ : Valuation R Γ'₀<VAR>h : v₁.IsEquiv v₂<GOAL>v₂.IsEquiv v₁
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>LinearOrderedCommMonoidWithZero Γ''₀<VAR>Ring R<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>LinearOrderedCommMonoidWithZero Γ'₀<VAR>v₁ : Valuation R Γ₀<VAR>v₂ : Valuation R Γ'₀<VAR>v₃ : Valuation R Γ''₀<VAR>h₁₂ : v₁.IsEquiv v₂<VAR>h₂₃ : v₂.IsEquiv v₃<GOAL>v₁.IsEquiv v₃
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Ring R<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>v v' : Valuation R Γ₀<VAR>h : v = v'<GOAL>v.IsEquiv v'
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Ring R<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>LinearOrderedCommMonoidWithZero Γ'₀<VAR>v v' : Valuation R Γ₀<VAR>f : Γ₀ →*₀ Γ'₀<VAR>hf : Monotone ⇑f<VAR>inf : Function.Injective ⇑f<VAR>h : v.IsEquiv v'<GOAL>(Valuation.map f hf v).IsEquiv (Valuation.map f hf v')
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Ring R<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>LinearOrderedCommMonoidWithZero Γ'₀<VAR>v₁ : Valuation R Γ₀<VAR>v₂ : Valuation R Γ'₀<VAR>S : Type u_7<VAR>Ring S<VAR>f : S →+* R<VAR>h : v₁.IsEquiv v₂<GOAL>(Valuation.comap f v₁).IsEquiv (Valuation.comap f v₂)
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Ring R<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>LinearOrderedCommMonoidWithZero Γ'₀<VAR>v₁ : Valuation R Γ₀<VAR>v₂ : Valuation R Γ'₀<VAR>h : v₁.IsEquiv v₂<VAR>r s : R<GOAL>v₁ r = v₁ s ↔ v₂ r = v₂ s
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Ring R<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>LinearOrderedCommMonoidWithZero Γ'₀<VAR>v₁ : Valuation R Γ₀<VAR>v₂ : Valuation R Γ'₀<VAR>h : v₁.IsEquiv v₂<VAR>r : R<GOAL>v₁ r ≠ 0 ↔ v₂ r ≠ 0
<VAR>R : Type u_3<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>LinearOrderedCommMonoidWithZero Γ₀<VAR>LinearOrderedCommMonoidWithZero Γ'₀<VAR>Ring R<VAR>v : Valuation R Γ₀<VAR>f : Γ₀ →*₀ Γ'₀<VAR>H : StrictMono ⇑f<GOAL>(Valuation.map f ⋯ v).IsEquiv v
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>LinearOrderedCommGroupWithZero Γ'₀<VAR>v : Valuation K Γ₀<VAR>v' : Valuation K Γ'₀<VAR>h : ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1<GOAL>v.IsEquiv v'
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>LinearOrderedCommGroupWithZero Γ'₀<VAR>v : Valuation K Γ₀<VAR>v' : Valuation K Γ'₀<GOAL>v.IsEquiv v' ↔ ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>LinearOrderedCommGroupWithZero Γ'₀<VAR>v : Valuation K Γ₀<VAR>v' : Valuation K Γ'₀<GOAL>v.IsEquiv v' ↔ ∀ {x : K}, v x = 1 ↔ v' x = 1
<VAR>K : Type u_1<VAR>DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>LinearOrderedCommGroupWithZero Γ₀<VAR>LinearOrderedCommGroupWithZero Γ'₀<VAR>v : Valuation K Γ₀<VAR>v' : Valuation K Γ'₀<GOAL>v.IsEquiv v' ↔ ∀ {x : K}, v x < 1 ↔ v' x < 1