ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>a b : α<VAR>inst✝ : CommSemiring α<VAR>h : a ∈ nonunits α<VAR>this : Ideal.span {a} ≠ ⊤<VAR>I : Ideal α<VAR>Imax : I.IsMaximal<VAR>H : Ideal.span {a} ≤ I<GOAL>a ∈ {a}
<VAR>z✝ : ℂ<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>z : ℂ<VAR>hz : 0 ≤ z<GOAL>z = ↑‖z‖
<VAR>z✝ : ℂ<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>z : ℝ<VAR>hz : 0 ≤ ↑z<GOAL>↑z = ↑‖↑z‖
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hq : q ≠ 0<VAR>hr : r ≠ 0<GOAL>padicValRat p (q * r) = padicValRat p q + padicValRat p r
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hq : q ≠ 0<VAR>hr : r ≠ 0<VAR>this : q * r = q.num * r.num /. (↑q.den * ↑r.den)<GOAL>padicValRat p (q * r) = padicValRat p q + padicValRat p r
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hq : q ≠ 0<VAR>hr : r ≠ 0<VAR>this : q * r = q.num * r.num /. (↑q.den * ↑r.den)<VAR>hq' : q.num /. ↑q.den ≠ 0<GOAL>padicValRat p (q * r) = padicValRat p q + padicValRat p r
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hq : q ≠ 0<VAR>hr : r ≠ 0<VAR>this : q * r = q.num * r.num /. (↑q.den * ↑r.den)<VAR>hq' : q.num /. ↑q.den ≠ 0<VAR>hr' : r.num /. ↑r.den ≠ 0<GOAL>padicValRat p (q * r) = padicValRat p q + padicValRat p r
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hq : q ≠ 0<VAR>hr : r ≠ 0<VAR>this : q * r = q.num * r.num /. (↑q.den * ↑r.den)<VAR>hq' : q.num /. ↑q.den ≠ 0<VAR>hr' : r.num /. ↑r.den ≠ 0<VAR>hp' : _root_.Prime ↑p<GOAL>padicValRat p (q * r) = padicValRat p q + padicValRat p r
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hq : q ≠ 0<VAR>hr : r ≠ 0<VAR>this : q * r = q.num * r.num /. (↑q.den * ↑r.den)<VAR>hq' : q.num /. ↑q.den ≠ 0<VAR>hr' : r.num /. ↑r.den ≠ 0<VAR>hp' : _root_.Prime ↑p<GOAL>↑((multiplicity (↑p) (q.num * r.num)).get ⋯) - ↑((multiplicity (↑p) (↑q.den * ↑r.den)).get ⋯) = padicValRat p q + padicValRat p r
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hq : q ≠ 0<VAR>hr : r ≠ 0<VAR>this : q * r = q.num * r.num /. (↑q.den * ↑r.den)<VAR>hq' : q.num /. ↑q.den ≠ 0<VAR>hr' : r.num /. ↑r.den ≠ 0<VAR>hp' : _root_.Prime ↑p<GOAL>↑((multiplicity (↑p) (q.num * r.num)).get ⋯) - ↑((multiplicity (↑p) (↑q.den * ↑r.den)).get ⋯) = ↑((multiplicity (↑p) q.num).get ⋯) - ↑((multiplicity ↑p ↑q.den).get ⋯) + (↑((multiplicity (↑p) r.num).get ⋯) - ↑((multiplicity ↑p ↑r.den).get ⋯))
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>q r : ℚ<VAR>hq : q ≠ 0<VAR>hr : r ≠ 0<VAR>this : q * r = q.num * r.num /. (↑q.den * ↑r.den)<VAR>hq' : q.num /. ↑q.den ≠ 0<VAR>hr' : r.num /. ↑r.den ≠ 0<VAR>hp' : _root_.Prime ↑p<GOAL>↑((multiplicity (↑p) q.num).get ⋯) + ↑((multiplicity (↑p) r.num).get ⋯) - (↑((multiplicity ↑p ↑q.den).get ⋯) + ↑((multiplicity ↑p ↑r.den).get ⋯)) = ↑((multiplicity (↑p) q.num).get ⋯) - ↑((multiplicity ↑p ↑q.den).get ⋯) + (↑((multiplicity (↑p) r.num).get ⋯) - ↑((multiplicity ↑p ↑r.den).get ⋯))
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : BooleanAlgebra α<VAR>s✝ s : Finset ι<VAR>f : ι → α<VAR>a : α<GOAL>(s.sup fun b => a \ f b) = a \ s.inf f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s✝ s' : Set α<VAR>x : α<VAR>p✝ : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>h : 𝔖.Nonempty<VAR>h' : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖<VAR>p : ι → Prop<VAR>s : ι → Set (β × β)<VAR>hb : (𝓤 β).HasBasis p s<GOAL>(𝓤 (α →ᵤ[𝔖] β)).HasBasis (fun Si => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si => UniformOnFun.gen 𝔖 Si.1 (s Si.2)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s✝ s' : Set α<VAR>x : α<VAR>p✝ : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>h : 𝔖.Nonempty<VAR>h' : DirectedOn (fun x x_1 => x ⊆ x_1) 𝔖<VAR>p : ι → Prop<VAR>s : ι → Set (β × β)<VAR>hb : (𝓤 β).HasBasis p s<GOAL>(⨅ i ∈ 𝔖, 𝓤 (α →ᵤ[𝔖] β)).HasBasis (fun Si => Si.1 ∈ 𝔖 ∧ p Si.2) fun Si => UniformOnFun.gen 𝔖 Si.1 (s Si.2)
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : Monoid M<VAR>a : M<VAR>s : Set M<VAR>p : (m : M) → m ∈ closure s → Prop<VAR>one : p 1 ⋯<VAR>mul_right : ∀ (x : M) (hx : x ∈ closure s) (y : M) (hy : y ∈ s), p x hx → p (x * y) ⋯<VAR>x : M<VAR>h : x ∈ closure s<VAR>m : Mᵐᵒᵖ<VAR>hm : m ∈ closure (MulOpposite.unop ⁻¹' s)<GOAL>MulOpposite.unop m ∈ closure s
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : Monoid M<VAR>a : M<VAR>s : Set M<VAR>p : (m : M) → m ∈ closure s → Prop<VAR>one : p 1 ⋯<VAR>mul_right : ∀ (x : M) (hx : x ∈ closure s) (y : M) (hy : y ∈ s), p x hx → p (x * y) ⋯<VAR>x : M<VAR>h : x ∈ closure s<GOAL>{ unop' := x } ∈ closure (MulOpposite.unop ⁻¹' s)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>D' : Type u_3<VAR>inst✝² : Category.{u_4, u_1} C<VAR>inst✝¹ : Category.{?u.6221, u_2} D<VAR>inst✝ : Category.{?u.6225, u_3} D'<VAR>W : MorphismProperty C<VAR>X : C<VAR>P : StructuredArrow (W.Q.obj X) W.Q → Prop<VAR>hP₀ : P (StructuredArrow.mk (𝟙 (W.Q.obj X)))<VAR>hP₁ : ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ W.Q.map f))<VAR>hP₂ : ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))<VAR>g : StructuredArrow (W.Q.obj X) W.Q<VAR>X₀ : Paths (LocQuiver W) := { obj := X }<GOAL>P g
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>D' : Type u_3<VAR>inst✝² : Category.{u_4, u_1} C<VAR>inst✝¹ : Category.{?u.6221, u_2} D<VAR>inst✝ : Category.{?u.6225, u_3} D'<VAR>W : MorphismProperty C<VAR>X : C<VAR>P : StructuredArrow (W.Q.obj X) W.Q → Prop<VAR>hP₀ : P (StructuredArrow.mk (𝟙 (W.Q.obj X)))<VAR>hP₁ : ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ W.Q.map f))<VAR>hP₂ : ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))<VAR>g : StructuredArrow (W.Q.obj X) W.Q<VAR>X₀ : Paths (LocQuiver W) := { obj := X }<GOAL>∀ ⦃Y₀ : Paths (LocQuiver W)⦄ (f : X₀ ⟶ Y₀), P (StructuredArrow.mk ((Quotient.functor (relations W)).map f))
<VAR>l r : List Char<GOAL>{ s := { data := l.reverseAux r }, i := { byteIdx := utf8Len l } } = { s := { data := l.reverse ++ r }, i := { byteIdx := utf8Len l.reverse } }
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v r : ι → F<VAR>i : ι<VAR>x : F<VAR>hi : i ∈ s<GOAL>Lagrange.basis s v i = C (nodalWeight s v i) * (nodal s v / (X - C (v i)))
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝² : NonUnitalNonAssocSemiring α<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>d : n → α<VAR>M : Matrix m n α<VAR>i : m<VAR>j : n<GOAL>(M * diagonal d) i j = M i j * d j
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝² : NonUnitalNonAssocSemiring α<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>d : n → α<VAR>M : Matrix m n α<VAR>i : m<VAR>j : n<GOAL>(M * (diagonal d)ᵀ) i j = M i j * d j
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>inst✝ : CommRing R<VAR>r x y z : R<VAR>a b c : ℍ[R]<GOAL>a.re * b.imK + a.imI * b.imJ - a.imJ * b.imI + a.imK * b.re = a.re * b.imK + a.imI * b.imJ - a.imJ * b.imI + a.imK * b.re
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝ : CommSemiring α<VAR>a✝ b✝ c a b : α<GOAL>(a + b) * (a + b) = a * a + 2 * a * b + b * b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : NormedAddCommGroup F<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>s : Set Ω<VAR>t : Set β<VAR>f : β × Ω → F<VAR>hX : Measurable X<VAR>hY : Measurable Y<VAR>hs : MeasurableSet s<GOAL>(fun a => (((condDistrib Y X μ) (X a)) s).toReal) =ᶠ[ae μ] μ[(Y ⁻¹' s).indicator fun ω => 1|MeasurableSpace.comap X mβ]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : NormedAddCommGroup F<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>s : Set Ω<VAR>t : Set β<VAR>f : β × Ω → F<VAR>hX : Measurable X<VAR>hY : Measurable Y<VAR>hs : MeasurableSet s<GOAL>Integrable ((Y ⁻¹' s).indicator fun ω => 1) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : NormedAddCommGroup F<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>s : Set Ω<VAR>t : Set β<VAR>f : β × Ω → F<VAR>hX : Measurable X<VAR>hY : Measurable Y<VAR>hs : MeasurableSet s<GOAL>∀ (s_1 : Set α), MeasurableSet s_1 → μ s_1 < ⊤ → IntegrableOn (fun a => (((condDistrib Y X μ) (X a)) s).toReal) s_1 μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : NormedAddCommGroup F<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>s : Set Ω<VAR>t : Set β<VAR>f : β × Ω → F<VAR>hX : Measurable X<VAR>hY : Measurable Y<VAR>hs : MeasurableSet s<GOAL>∀ (s_1 : Set α), MeasurableSet s_1 → μ s_1 < ⊤ → ∫ (x : α) in s_1, (((condDistrib Y X μ) (X x)) s).toReal ∂μ = ∫ (x : α) in s_1, (Y ⁻¹' s).indicator (fun ω => 1) x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : MeasurableSpace Ω<VAR>inst✝³ : StandardBorelSpace Ω<VAR>inst✝² : Nonempty Ω<VAR>inst✝¹ : NormedAddCommGroup F<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>X : α → β<VAR>Y : α → Ω<VAR>mβ : MeasurableSpace β<VAR>s : Set Ω<VAR>t : Set β<VAR>f : β × Ω → F<VAR>hX : Measurable X<VAR>hY : Measurable Y<VAR>hs : MeasurableSet s<GOAL>AEStronglyMeasurable' (MeasurableSpace.comap X mβ) (fun a => (((condDistrib Y X μ) (X a)) s).toReal) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<VAR>r : ℕ<VAR>hf : StrictMono f<GOAL>{ ofColex := image f s } ≤ { ofColex := image f t } ↔ { ofColex := s } ≤ { ofColex := t }
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : TopologicalSpace X<VAR>f : E → X<VAR>s : Set X<VAR>hf : IsCoveringMap f<VAR>e₁ e₂ : E<VAR>he : f e₁ = f e₂<VAR>hne : e₁ ≠ e₂<VAR>left✝ : DiscreteTopology ↑(f ⁻¹' {f e₁})<VAR>t : Trivialization (↑(f ⁻¹' {f e₁})) f<VAR>he₁ : f e₁ ∈ t.baseSet<VAR>he₂ : f e₂ ∈ t.baseSet<GOAL>∃ s₁ s₂, IsOpen s₁ ∧ IsOpen s₂ ∧ e₁ ∈ s₁ ∧ e₂ ∈ s₂ ∧ Disjoint s₁ s₂
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : TopologicalSpace X<VAR>f : E → X<VAR>s : Set X<VAR>hf : IsCoveringMap f<VAR>e₁ e₂ : E<VAR>he : f e₁ = f e₂<VAR>hne : e₁ ≠ e₂<VAR>left✝ : DiscreteTopology ↑(f ⁻¹' {f e₁})<VAR>t : Trivialization (↑(f ⁻¹' {f e₁})) f<VAR>he₁ : e₁ ∈ t.source<VAR>he₂ : e₂ ∈ t.source<GOAL>∃ s₁ s₂, IsOpen s₁ ∧ IsOpen s₂ ∧ e₁ ∈ s₁ ∧ e₂ ∈ s₂ ∧ Disjoint s₁ s₂
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : TopologicalSpace X<VAR>f : E → X<VAR>s : Set X<VAR>hf : IsCoveringMap f<VAR>e₁ e₂ : E<VAR>he : f e₁ = f e₂<VAR>hne : e₁ ≠ e₂<VAR>left✝ : DiscreteTopology ↑(f ⁻¹' {f e₁})<VAR>t : Trivialization (↑(f ⁻¹' {f e₁})) f<VAR>he₁ : e₁ ∈ t.source<VAR>he₂ : e₂ ∈ t.source<GOAL>IsOpen (t.source ∩ Prod.snd ∘ ↑t ⁻¹' {(↑t e₁).2})
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : TopologicalSpace X<VAR>f : E → X<VAR>s : Set X<VAR>hf : IsCoveringMap f<VAR>e₁ e₂ : E<VAR>he : f e₁ = f e₂<VAR>hne : e₁ ≠ e₂<VAR>left✝ : DiscreteTopology ↑(f ⁻¹' {f e₁})<VAR>t : Trivialization (↑(f ⁻¹' {f e₁})) f<VAR>he₁ : e₁ ∈ t.source<VAR>he₂ : e₂ ∈ t.source<GOAL>IsOpen (t.source ∩ Prod.snd ∘ ↑t ⁻¹' {(↑t e₂).2})
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : TopologicalSpace X<VAR>f : E → X<VAR>s : Set X<VAR>hf : IsCoveringMap f<VAR>e₁ e₂ : E<VAR>he : f e₁ = f e₂<VAR>hne : e₁ ≠ e₂<VAR>left✝ : DiscreteTopology ↑(f ⁻¹' {f e₁})<VAR>t : Trivialization (↑(f ⁻¹' {f e₁})) f<VAR>he₁ : e₁ ∈ t.source<VAR>he₂ : e₂ ∈ t.source<VAR>x : E<VAR>h₁ : x ∈ t.source ∩ Prod.snd ∘ ↑t ⁻¹' {(↑t e₁).2}<VAR>h₂ : x ∈ t.source ∩ Prod.snd ∘ ↑t ⁻¹' {(↑t e₂).2}<GOAL>↑t.toPartialHomeomorph e₁ = ↑t.toPartialHomeomorph e₂
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : TopologicalSpace X<VAR>f : E → X<VAR>s : Set X<VAR>hf : IsCoveringMap f<VAR>e₁ e₂ : E<VAR>he : f e₁ = f e₂<VAR>hne : e₁ ≠ e₂<VAR>left✝ : DiscreteTopology ↑(f ⁻¹' {f e₁})<VAR>t : Trivialization (↑(f ⁻¹' {f e₁})) f<VAR>he₁ : e₁ ∈ t.source<VAR>he₂ : e₂ ∈ t.source<VAR>x : E<VAR>h₁ : x ∈ t.source ∩ Prod.snd ∘ ↑t ⁻¹' {(↑t e₁).2}<VAR>h₂ : x ∈ t.source ∩ Prod.snd ∘ ↑t ⁻¹' {(↑t e₂).2}<GOAL>(↑t.toPartialHomeomorph e₁).1 = (↑t.toPartialHomeomorph e₂).1
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : (𝓞 K)ˣ<GOAL>∑ w : { w // w ≠ w₀ }, (logEmbedding K) x w = -↑w₀.mult * Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : (𝓞 K)ˣ<VAR>h : Real.log (∏ w : InfinitePlace K, w ((algebraMap (𝓞 K) K) ↑x) ^ w.mult) = Real.log ↑|(Algebra.norm ℚ) ((algebraMap (𝓞 K) K) ↑x)|<GOAL>∑ w : { w // w ≠ w₀ }, (logEmbedding K) x w = -↑w₀.mult * Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : (𝓞 K)ˣ<VAR>h : ∑ i : InfinitePlace K, Real.log (i ((algebraMap (𝓞 K) K) ↑x) ^ i.mult) = 0<GOAL>∑ w : { w // w ≠ w₀ }, (logEmbedding K) x w = -↑w₀.mult * Real.log (w₀ ((algebraMap (𝓞 K) K) ↑x))
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : (𝓞 K)ˣ<VAR>h : Real.log (∏ w : InfinitePlace K, w ((algebraMap (𝓞 K) K) ↑x) ^ w.mult) = 0<GOAL>∀ x_1 ∈ univ, x_1 ((algebraMap (𝓞 K) K) ↑x) ^ x_1.mult ≠ 0
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.207600, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝ : HasHomotopyCofiber φ<VAR>K : CochainComplex C ℤ<VAR>α : Cocycle K F 1<VAR>β : Cochain K G 0<VAR>eq : δ 0 1 β + (↑α).comp (Cochain.ofHom φ) ⋯ = 0<GOAL>Cochain.ofHom (lift φ α β eq) = liftCochain φ (↑α) β ⋯
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s✝ : Multiset α<VAR>a : α<VAR>s t : Multiset α<VAR>x✝ : s ≤ t ∧ a ∈ t<VAR>l : s ≤ t<VAR>m : a ∈ t<VAR>h : a ∉ s<GOAL>ndinsert a s ≤ t
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s✝ : Multiset α<VAR>a : α<VAR>s t : Multiset α<VAR>x✝ : s ≤ t ∧ a ∈ t<VAR>l : s ≤ t<VAR>m : a ∈ t<VAR>h : a ∉ s<GOAL>s ≤ t
<VAR>x✝ y✝ x y : ℝ<VAR>a : ℕ<GOAL>⌊√↑a⌋₊ = a.sqrt
<VAR>x✝ y✝ x y : ℝ<VAR>a : ℕ<GOAL>↑a.sqrt ≤ √↑a ∧ √↑a < ↑a.sqrt + 1
<VAR>ι : Type u_1<VAR>c : ComplexShape ι<VAR>j : ι<VAR>hj : ¬c.Rel (c.prev j) j<VAR>k : ι<VAR>hk' : c.Rel k j<GOAL>c.Rel (c.prev j) j
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>m : M<GOAL>‖S.normedMk m‖ = sInf ((fun m_1 => ‖m + m_1‖) '' ↑S.normedMk.ker)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>X : C<VAR>f : J → C<VAR>Y : C<VAR>j✝ : J<GOAL>((leftDistributor X f ⊗ asIso (𝟙 Y)) ≪≫ rightDistributor (fun j => X ⊗ f j) Y).hom ≫ biproduct.π (fun j => (X ⊗ f j) ⊗ Y) j✝ = (α_ X (⨁ f) Y ≪≫ (asIso (𝟙 X) ⊗ rightDistributor f Y) ≪≫ (leftDistributor X fun j => f j ⊗ Y) ≪≫ biproduct.mapIso fun j => (α_ X (f j) Y).symm).hom ≫ biproduct.π (fun j => (X ⊗ f j) ⊗ Y) j✝
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>X : C<VAR>f : J → C<VAR>Y : C<VAR>j✝ : J<GOAL>∑ x : J, (X ◁ biproduct.π f x ⊗ 𝟙 Y) ≫ (biproduct.ι (fun j => X ⊗ f j) x ⊗ 𝟙 Y) ≫ biproduct.π (fun j => X ⊗ f j) j✝ ▷ Y = ∑ x : J, (α_ X (⨁ f) Y).hom ≫ (𝟙 X ⊗ biproduct.π f x ▷ Y ≫ biproduct.ι (fun j => f j ⊗ Y) x) ≫ X ◁ biproduct.π (fun j => f j ⊗ Y) j✝ ≫ (α_ X (f j✝) Y).inv
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>X : C<VAR>f : J → C<VAR>Y : C<VAR>j✝ : J<GOAL>∑ x : J, ((𝟙 X ⊗ biproduct.π f x) ⊗ 𝟙 Y) ≫ (biproduct.ι (fun j => X ⊗ f j) x ⊗ 𝟙 Y) ≫ (biproduct.π (fun j => X ⊗ f j) j✝ ⊗ 𝟙 Y) = ∑ x : J, (α_ X (⨁ f) Y).hom ≫ (𝟙 X ⊗ (biproduct.π f x ⊗ 𝟙 Y) ≫ biproduct.ι (fun j => f j ⊗ Y) x) ≫ (𝟙 X ⊗ biproduct.π (fun j => f j ⊗ Y) j✝) ≫ (α_ X (f j✝) Y).inv
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>X : C<VAR>f : J → C<VAR>Y : C<VAR>j✝ : J<GOAL>(∑ x : J, if h : x = j✝ then (𝟙 X ⊗ biproduct.π f x) ≫ eqToHom ⋯ ⊗ 𝟙 Y else (𝟙 X ⊗ biproduct.π f x) ≫ 0 ⊗ 𝟙 Y) = ∑ x : J, if h : x = j✝ then (α_ X (⨁ f) Y).hom ≫ (𝟙 X ⊗ (biproduct.π f x ⊗ 𝟙 Y) ≫ eqToHom ⋯) ≫ (α_ X (f j✝) Y).inv else (α_ X (⨁ f) Y).hom ≫ (𝟙 X ⊗ (biproduct.π f x ⊗ 𝟙 Y) ≫ 0) ≫ (α_ X (f j✝) Y).inv
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>hx : 0 < x<VAR>hx' : x ≤ 1<GOAL>0 ≤ logb b x
<VAR>b x y : ℝ<VAR>b_pos : 0 < b<VAR>b_lt_one : b < 1<VAR>hx : 0 < x<VAR>hx' : x ≤ 1<GOAL>x ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : Measure α<VAR>κ✝ η : Kernel α β<VAR>κ : Kernel Unit β<VAR>inst✝ : IsSFiniteKernel κ<VAR>s : Set (Unit × β)<VAR>hs : MeasurableSet s<GOAL>(dirac () ⊗ₘ κ) s = (map (Prod.mk ()) (κ ())) s
<VAR>J : Type v'<VAR>inst✝⁵ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝³ : Category.{?u.306779, u_1} K<VAR>D : Type u_2<VAR>inst✝² : Category.{?u.306786, u_2} D<VAR>n : ℕ<VAR>f : Fin (n + 1) → C<VAR>c₁ : Cofan fun i => f i.succ<VAR>c₂ : BinaryCofan (f 0) c₁.pt<VAR>t₁ : IsVanKampenColimit c₁<VAR>t₂ : IsVanKampenColimit c₂<VAR>inst✝¹ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i<VAR>inst✝ : HasFiniteCoproducts C<VAR>F : Discrete (Fin (n + 1)) ⥤ C<VAR>c : Cocone F<VAR>α : F ⟶ Discrete.functor f<VAR>i : c.pt ⟶ (extendCofan c₁ c₂).pt<VAR>e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (Functor.const (Discrete (Fin (n + 1)))).map i<VAR>hα : NatTrans.Equifibered α<GOAL>Nonempty (IsColimit c) ↔ ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
<VAR>J : Type v'<VAR>inst✝⁵ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝³ : Category.{?u.306779, u_1} K<VAR>D : Type u_2<VAR>inst✝² : Category.{?u.306786, u_2} D<VAR>n : ℕ<VAR>f : Fin (n + 1) → C<VAR>c₁ : Cofan fun i => f i.succ<VAR>c₂ : BinaryCofan (f 0) c₁.pt<VAR>t₁ : IsVanKampenColimit c₁<VAR>t₂ : IsVanKampenColimit c₂<VAR>inst✝¹ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i<VAR>inst✝ : HasFiniteCoproducts C<VAR>F : Discrete (Fin (n + 1)) ⥤ C<VAR>c : Cocone F<VAR>α : F ⟶ Discrete.functor f<VAR>i : c.pt ⟶ (extendCofan c₁ c₂).pt<VAR>e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (Functor.const (Discrete (Fin (n + 1)))).map i<VAR>hα : NatTrans.Equifibered α<GOAL>Nonempty (IsColimit c) → ∀ (j : Discrete (Fin (n + 1))), IsPullback (c.ι.app j) (α.app j) i ((extendCofan c₁ c₂).ι.app j)
<VAR>J : Type v'<VAR>inst✝⁵ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝³ : Category.{?u.306779, u_1} K<VAR>D : Type u_2<VAR>inst✝² : Category.{?u.306786, u_2} D<VAR>n : ℕ<VAR>f : Fin (n + 1) → C<VAR>c₁ : Cofan fun i => f i.succ<VAR>c₂ : BinaryCofan (f 0) c₁.pt<VAR>t₁ : IsVanKampenColimit c₁<VAR>t₂ : IsVanKampenColimit c₂<VAR>inst✝¹ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i<VAR>inst✝ : HasFiniteCoproducts C<VAR>F : Discrete (Fin (n + 1)) ⥤ C<VAR>c : Cocone F<VAR>α : F ⟶ Discrete.functor f<VAR>i : c.pt ⟶ (extendCofan c₁ c₂).pt<VAR>e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (Functor.const (Discrete (Fin (n + 1)))).map i<VAR>hα : NatTrans.Equifibered α<VAR>Hc : IsColimit c<VAR>j : Fin (n + 1)<GOAL>IsPullback (c.ι.app { as := j }) (α.app { as := j }) i ((extendCofan c₁ c₂).ι.app { as := j })
<VAR>J : Type v'<VAR>inst✝⁵ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝³ : Category.{?u.306779, u_1} K<VAR>D : Type u_2<VAR>inst✝² : Category.{?u.306786, u_2} D<VAR>n : ℕ<VAR>f : Fin (n + 1) → C<VAR>c₁ : Cofan fun i => f i.succ<VAR>c₂ : BinaryCofan (f 0) c₁.pt<VAR>t₁ : IsVanKampenColimit c₁<VAR>t₂ : IsVanKampenColimit c₂<VAR>inst✝¹ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i<VAR>inst✝ : HasFiniteCoproducts C<VAR>F : Discrete (Fin (n + 1)) ⥤ C<VAR>c : Cocone F<VAR>α : F ⟶ Discrete.functor f<VAR>i : c.pt ⟶ (extendCofan c₁ c₂).pt<VAR>e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (Functor.const (Discrete (Fin (n + 1)))).map i<VAR>hα : NatTrans.Equifibered α<VAR>Hc : IsColimit c<VAR>j : Fin (n + 1)<VAR>t₂' : ∀ (j : Discrete WalkingPair), IsPullback ((BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b => c.ι.app { as := b.succ })).ι.app j) ((mapPair (α.app { as := 0 }) (Sigma.desc fun b => α.app { as := b.succ } ≫ c₁.inj b)).app j) i (c₂.ι.app j)<GOAL>IsPullback (c.ι.app { as := j }) (α.app { as := j }) i ((extendCofan c₁ c₂).ι.app { as := j })
<VAR>J : Type v'<VAR>inst✝⁵ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝³ : Category.{?u.306779, u_1} K<VAR>D : Type u_2<VAR>inst✝² : Category.{?u.306786, u_2} D<VAR>n : ℕ<VAR>f : Fin (n + 1) → C<VAR>c₁ : Cofan fun i => f i.succ<VAR>c₂ : BinaryCofan (f 0) c₁.pt<VAR>t₁ : IsVanKampenColimit c₁<VAR>t₂ : IsVanKampenColimit c₂<VAR>inst✝¹ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i<VAR>inst✝ : HasFiniteCoproducts C<VAR>F : Discrete (Fin (n + 1)) ⥤ C<VAR>c : Cocone F<VAR>α : F ⟶ Discrete.functor f<VAR>i : c.pt ⟶ (extendCofan c₁ c₂).pt<VAR>e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (Functor.const (Discrete (Fin (n + 1)))).map i<VAR>hα : NatTrans.Equifibered α<VAR>Hc : IsColimit c<VAR>j : Fin (n + 1)<GOAL>mapPair (α.app { as := 0 }) (Sigma.desc fun b => α.app { as := b.succ } ≫ c₁.inj b) ≫ c₂.ι = (BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b => c.ι.app { as := b.succ })).ι ≫ (Functor.const (Discrete WalkingPair)).map i
<VAR>J : Type v'<VAR>inst✝⁵ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝³ : Category.{?u.306779, u_1} K<VAR>D : Type u_2<VAR>inst✝² : Category.{?u.306786, u_2} D<VAR>n : ℕ<VAR>f : Fin (n + 1) → C<VAR>c₁ : Cofan fun i => f i.succ<VAR>c₂ : BinaryCofan (f 0) c₁.pt<VAR>t₁ : IsVanKampenColimit c₁<VAR>t₂ : IsVanKampenColimit c₂<VAR>inst✝¹ : ∀ {Z : C} (i : Z ⟶ c₂.pt), HasPullback c₂.inr i<VAR>inst✝ : HasFiniteCoproducts C<VAR>F : Discrete (Fin (n + 1)) ⥤ C<VAR>c : Cocone F<VAR>α : F ⟶ Discrete.functor f<VAR>i : c.pt ⟶ (extendCofan c₁ c₂).pt<VAR>e : α ≫ (extendCofan c₁ c₂).ι = c.ι ≫ (Functor.const (Discrete (Fin (n + 1)))).map i<VAR>hα : NatTrans.Equifibered α<VAR>Hc : IsColimit c<VAR>j : Fin (n + 1)<GOAL>IsColimit (BinaryCofan.mk (c.ι.app { as := 0 }) (Sigma.desc fun b => c.ι.app { as := b.succ }))
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝³ : Semiring S<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Field K<VAR>p q : R[X]<VAR>r : R<VAR>h : p.natDegree = q.natDegree<VAR>n : ℕ<GOAL>(r ^ (p.natDegree - (p + q).natDegree) • (p + q).scaleRoots r).coeff n = (p.scaleRoots r + q.scaleRoots r).coeff n