ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>a b c d : α<VAR>h : Disjoint (a ⊓ b) (a ⊔ b)<GOAL>Disjoint a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<GOAL>periodicOrbit f x = Cycle.nil ↔ x ∉ periodicPts f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<GOAL>minimalPeriod f x = 0 ↔ x ∉ periodicPts f
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Semiring α<VAR>I : Ideal α<VAR>a✝ b a : α<VAR>h2 : IsUnit a<VAR>x : α<GOAL>span {a * x} = span {x}
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Semiring α<VAR>I : Ideal α<VAR>a✝ b a : α<VAR>h2 : IsUnit a<VAR>x : α<GOAL>∃ a_1, a_1 * x = a * x
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Semiring α<VAR>I : Ideal α<VAR>a✝ b a : α<VAR>h2 : IsUnit a<VAR>x : α<GOAL>∃ a_1, a_1 * (a * x) = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>j : JordanDecomposition α<GOAL>∃ S, MeasurableSet S ∧ VectorMeasure.restrict j.toSignedMeasure S ≤ VectorMeasure.restrict 0 S ∧ VectorMeasure.restrict 0 Sᶜ ≤ VectorMeasure.restrict j.toSignedMeasure Sᶜ ∧ j.posPart S = 0 ∧ j.negPart Sᶜ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>j : JordanDecomposition α<VAR>S : Set α<VAR>hS₁ : MeasurableSet S<VAR>hS₂ : j.posPart S = 0<VAR>hS₃ : j.negPart Sᶜ = 0<GOAL>∃ S, MeasurableSet S ∧ VectorMeasure.restrict j.toSignedMeasure S ≤ VectorMeasure.restrict 0 S ∧ VectorMeasure.restrict 0 Sᶜ ≤ VectorMeasure.restrict j.toSignedMeasure Sᶜ ∧ j.posPart S = 0 ∧ j.negPart Sᶜ = 0
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>x : S<GOAL>Function.Surjective ⇑(toAdjoin R x)
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>x : S<GOAL>adjoin R (Subtype.val ⁻¹' {x}) ≤ (toAdjoin R x).range
<VAR>x✝¹ y✝¹ z✝ w x✝ y✝ z x : ℝ<VAR>hx : 0 ≤ x<VAR>y : ℝ<GOAL>x ^ (-y) = (x ^ y)⁻¹
<VAR>x✝¹ y✝¹ z✝ w x✝ y✝ z x : ℝ<VAR>hx : 0 ≤ x<VAR>y : ℝ<GOAL>(if x = 0 then if -y = 0 then 1 else 0 else rexp (log x * -y)) = (if x = 0 then if y = 0 then 1 else 0 else rexp (log x * y))⁻¹
<VAR>α✝ : Type u_1<VAR>M : Matroid α✝<VAR>E B I X R J : Set α✝<VAR>α : Type u_2<GOAL>loopyOn ∅ = emptyOn α
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s s₁ s₂ : Finset α<VAR>a : α<VAR>f g : α → β<VAR>inst✝¹ : CommGroup β<VAR>inst✝ : DecidableEq α<GOAL>(∏ x ∈ s₂ \ s₁, f x) / ∏ x ∈ s₁ \ s₂, f x = (∏ x ∈ s₂, f x) / ∏ x ∈ s₁, f x
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : SimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>X.map (SimplexCategory.σ i).op ≫ X.map (SimplexCategory.δ i.castSucc).op = 𝟙 (X _[n])
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : Zero M<VAR>a a' : α<VAR>b : M<GOAL>(single a b) a = b
<VAR>R : Type u_1<VAR>ι : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring ι<VAR>inst✝⁸ : Module ι (Additive ℤˣ)<VAR>inst✝⁷ : DecidableEq ι<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : Ring A<VAR>inst✝⁴ : Ring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>𝒜 : ι → Submodule R A<VAR>ℬ : ι → Submodule R B<VAR>inst✝¹ : GradedAlgebra 𝒜<VAR>inst✝ : GradedAlgebra ℬ<GOAL>(auxEquiv R 𝒜 ℬ) 1 = 1
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : ConcreteCategory C<VAR>inst✝ : PreservesColimit (Functor.empty C) (forget C)<VAR>X : C<VAR>h : Nonempty (IsInitial X)<GOAL>IsEmpty ((forget C).obj X)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : ConcreteCategory C<VAR>inst✝ : PreservesColimit (Functor.empty C) (forget C)<VAR>X : C<VAR>h : Nonempty (IsInitial X)<GOAL>Nonempty (IsInitial ((forget C).obj X))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Finset α<VAR>hs : s.Nonempty<VAR>a : α<VAR>t : Set α<VAR>x : α<GOAL>(if x ∈ t then (uniformOfFinset s hs) x else 0) = if x ∈ s ∧ x ∈ t then (↑s.card)⁻¹ else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Finset α<VAR>hs : s.Nonempty<VAR>a : α<VAR>t : Set α<VAR>x : α<VAR>hx : x ∈ Finset.filter (fun x => x ∈ t) s<VAR>this : x ∈ s ∧ x ∈ t := Eq.mp Mathlib.Data.Finset.Basic._auxLemma.138 hx<GOAL>(if x ∈ s ∧ x ∈ t then (↑s.card)⁻¹ else 0) = (↑s.card)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Finset α<VAR>hs : s.Nonempty<VAR>a : α<VAR>t : Set α<GOAL>∑ _x ∈ Finset.filter (fun x => x ∈ t) s, (↑s.card)⁻¹ = ↑(Finset.filter (fun x => x ∈ t) s).card / ↑s.card
<VAR>l r : List Char<VAR>it : Iterator<VAR>h : ValidFor l r it<GOAL>ValidFor (r.reverse ++ l) [] it.toEnd
<VAR>l r : List Char<VAR>it : Iterator<VAR>h : ValidFor l r it<GOAL>ValidFor (r.reverse ++ l) [] { s := { data := l.reverseAux r }, i := { byteIdx := utf8Len l + utf8Len r } }
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝² : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝¹ : Ring R<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x✝ y✝ z x y : R<GOAL>v (x - y) = v (x + -y)
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝² : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝¹ : Ring R<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>v : Valuation R Γ₀<VAR>x✝ y✝ z x y : R<GOAL>max (v x) (v (-y)) = max (v x) (v y)
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>α : Type u_3<VAR>m : MeasurableSpace Ω<VAR>m' : MeasurableSpace Ω'<VAR>μ : Measure Ω<VAR>s t✝ : Set Ω<VAR>i : Ω' → Ω<VAR>hi : MeasurableEmbedding i<VAR>hs : MeasurableSet s<VAR>t : Set Ω'<VAR>ht : MeasurableSet t<VAR>hi' : μ (range i)ᶜ = 0<GOAL>(comap i μ[|s]) t = (comap i μ)[|i ⁻¹' s] t
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>α : Type u_3<VAR>m : MeasurableSpace Ω<VAR>m' : MeasurableSpace Ω'<VAR>μ : Measure Ω<VAR>s t✝ : Set Ω<VAR>i : Ω' → Ω<VAR>hi : MeasurableEmbedding i<VAR>hs : MeasurableSet s<VAR>t : Set Ω'<VAR>ht : MeasurableSet t<VAR>hi' : μ (range i)ᶜ = 0<GOAL>Function.Injective i
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>α : Type u_3<VAR>m : MeasurableSpace Ω<VAR>m' : MeasurableSpace Ω'<VAR>μ : Measure Ω<VAR>s t✝ : Set Ω<VAR>i : Ω' → Ω<VAR>hi : MeasurableEmbedding i<VAR>hs : MeasurableSet s<VAR>t : Set Ω'<VAR>ht : MeasurableSet t<VAR>hi' : μ (range i)ᶜ = 0<GOAL>∀ (s : Set Ω'), MeasurableSet s → MeasurableSet (i '' s)
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>α : Type u_3<VAR>m : MeasurableSpace Ω<VAR>m' : MeasurableSpace Ω'<VAR>μ : Measure Ω<VAR>s t✝ : Set Ω<VAR>i : Ω' → Ω<VAR>hi : MeasurableEmbedding i<VAR>hs : MeasurableSet s<VAR>t : Set Ω'<VAR>ht : MeasurableSet t<VAR>hi' : μ (range i)ᶜ = 0<GOAL>MeasurableSet (i ⁻¹' s ∩ t)
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>α : Type u_3<VAR>m : MeasurableSpace Ω<VAR>m' : MeasurableSpace Ω'<VAR>μ : Measure Ω<VAR>s t✝ : Set Ω<VAR>i : Ω' → Ω<VAR>hi : MeasurableEmbedding i<VAR>hs : MeasurableSet s<VAR>t : Set Ω'<VAR>ht : MeasurableSet t<VAR>hi' : μ (range i)ᶜ = 0<GOAL>MeasurableSet (i ⁻¹' s)
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>α : Type u_3<VAR>m : MeasurableSpace Ω<VAR>m' : MeasurableSpace Ω'<VAR>μ : Measure Ω<VAR>s t✝ : Set Ω<VAR>i : Ω' → Ω<VAR>hi : MeasurableEmbedding i<VAR>hs : MeasurableSet s<VAR>t : Set Ω'<VAR>ht : MeasurableSet t<VAR>hi' : μ (range i)ᶜ = 0<GOAL>MeasurableSet s
<VAR>Ω : Type u_1<VAR>Ω' : Type u_2<VAR>α : Type u_3<VAR>m : MeasurableSpace Ω<VAR>m' : MeasurableSpace Ω'<VAR>μ : Measure Ω<VAR>s t✝ : Set Ω<VAR>i : Ω' → Ω<VAR>hi : MeasurableEmbedding i<VAR>hs : MeasurableSet s<VAR>t : Set Ω'<VAR>ht : MeasurableSet t<VAR>hi' : μ (range i)ᶜ = 0<GOAL>MeasurableSet t
<VAR>m n a b : ℕ<VAR>cop : m.Coprime n<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<VAR>h : a * m + b * n = m * n<GOAL>False
<VAR>m n b : ℕ<VAR>cop : m.Coprime n<VAR>hb : b ≠ 0<VAR>x : ℕ<VAR>ha : n * x ≠ 0<VAR>h : n * x * m + b * n = m * n<GOAL>False
<VAR>m n : ℕ<VAR>cop : m.Coprime n<VAR>x : ℕ<VAR>ha : n * x ≠ 0<VAR>y : ℕ<VAR>hb : m * y ≠ 0<VAR>h : n * x * m + m * y * n = m * n<GOAL>False
<VAR>m n : ℕ<VAR>cop : m.Coprime n<VAR>x : ℕ<VAR>ha : 1 ≤ x ∧ n ≠ 0<VAR>y : ℕ<VAR>hb : 1 ≤ y ∧ m ≠ 0<VAR>h : n * x * m + m * y * n = m * n<GOAL>False
<VAR>m n : ℕ<VAR>cop : m.Coprime n<VAR>x : ℕ<VAR>ha : 1 ≤ x ∧ n ≠ 0<VAR>y : ℕ<VAR>hb : 1 ≤ y ∧ m ≠ 0<VAR>h : n * x * m + m * y * n = m * n<GOAL>(x + y) * (m * n) = m * n
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : TopologicalSemiring R<VAR>inst✝⁶ : ContinuousStar R<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>a : A<VAR>ha : p a<VAR>inst✝ : UniqueContinuousFunctionalCalculus R A<VAR>f : C(↑(spectrum R a), R)<VAR>f' : C(↑(spectrum R a), ↑(spectrum R ((cfcHom ha) f)))<VAR>hff' : ∀ (x : ↑(spectrum R a)), f x = ↑(f' x)<VAR>g : C(↑(spectrum R ((cfcHom ha) f)), R)<VAR>φ : C(↑(spectrum R ((cfcHom ha) f)), R) →⋆ₐ[R] A := (cfcHom ha).comp (ContinuousMap.compStarAlgHom' R R f')<GOAL>(cfcHom ha) (g.comp f') = (cfcHom ⋯) g
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : TopologicalSemiring R<VAR>inst✝⁶ : ContinuousStar R<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>a : A<VAR>ha : p a<VAR>inst✝ : UniqueContinuousFunctionalCalculus R A<VAR>f : C(↑(spectrum R a), R)<VAR>f' : C(↑(spectrum R a), ↑(spectrum R ((cfcHom ha) f)))<VAR>hff' : ∀ (x : ↑(spectrum R a)), f x = ↑(f' x)<VAR>g : C(↑(spectrum R ((cfcHom ha) f)), R)<VAR>φ : C(↑(spectrum R ((cfcHom ha) f)), R) →⋆ₐ[R] A := (cfcHom ha).comp (ContinuousMap.compStarAlgHom' R R f')<GOAL>cfcHom ⋯ = φ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : TopologicalSemiring R<VAR>inst✝⁶ : ContinuousStar R<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>a : A<VAR>ha : p a<VAR>inst✝ : UniqueContinuousFunctionalCalculus R A<VAR>f : C(↑(spectrum R a), R)<VAR>f' : C(↑(spectrum R a), ↑(spectrum R ((cfcHom ha) f)))<VAR>hff' : ∀ (x : ↑(spectrum R a)), f x = ↑(f' x)<VAR>g : C(↑(spectrum R ((cfcHom ha) f)), R)<VAR>φ : C(↑(spectrum R ((cfcHom ha) f)), R) →⋆ₐ[R] A := (cfcHom ha).comp (ContinuousMap.compStarAlgHom' R R f')<GOAL>Continuous ⇑φ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : TopologicalSemiring R<VAR>inst✝⁶ : ContinuousStar R<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>a : A<VAR>ha : p a<VAR>inst✝ : UniqueContinuousFunctionalCalculus R A<VAR>f : C(↑(spectrum R a), R)<VAR>f' : C(↑(spectrum R a), ↑(spectrum R ((cfcHom ha) f)))<VAR>hff' : ∀ (x : ↑(spectrum R a)), f x = ↑(f' x)<VAR>g : C(↑(spectrum R ((cfcHom ha) f)), R)<VAR>φ : C(↑(spectrum R ((cfcHom ha) f)), R) →⋆ₐ[R] A := (cfcHom ha).comp (ContinuousMap.compStarAlgHom' R R f')<GOAL>φ (ContinuousMap.restrict (spectrum R ((cfcHom ha) f)) (ContinuousMap.id R)) = (cfcHom ha) f
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>p : ℕ<VAR>x y : R<VAR>hp : Nat.Prime p<VAR>h : Commute x y<GOAL>(x + y) ^ p = x ^ p + y ^ p + ↑p * ∑ k ∈ Ioo 0 p, x ^ k * y ^ (p - k) * ↑(p.choose k / p)
<VAR>d : ℤ<VAR>a : Solution₁ d<VAR>h : IsFundamental a<VAR>H : ∀ (n : ℤ), 0 ≤ n → (a ^ n).y < (a ^ (n + 1)).y<GOAL>StrictMono fun n => (a ^ n).y
<VAR>d : ℤ<VAR>a : Solution₁ d<VAR>h : IsFundamental a<VAR>H : ∀ (n : ℤ), 0 ≤ n → (a ^ n).y < (a ^ (n + 1)).y<VAR>n : ℤ<GOAL>(a ^ n).y < (a ^ (n + 1)).y
<VAR>d : ℤ<VAR>a : Solution₁ d<VAR>h : IsFundamental a<VAR>H : ∀ (n : ℤ), 0 ≤ n → (a ^ n).y < (a ^ (n + 1)).y<VAR>n : ℤ<VAR>hn : 0 ≤ n<GOAL>(a ^ n).y < (a ^ (n + 1)).y
<VAR>d : ℤ<VAR>a : Solution₁ d<VAR>h : IsFundamental a<VAR>H : ∀ (n : ℤ), 0 ≤ n → (a ^ n).y < (a ^ (n + 1)).y<VAR>n : ℤ<VAR>hn : n < 0<GOAL>(a ^ n).y < (a ^ (n + 1)).y
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>H : Type u_4<VAR>A : Type u_5<VAR>B : Type u_6<VAR>α : Type u_7<VAR>β : Type u_8<VAR>γ : Type u_9<VAR>δ : Type u_10<VAR>inst✝⁷ : SMul α β<VAR>inst✝⁶ : SMul α γ<VAR>inst✝⁵ : SMul β δ<VAR>inst✝⁴ : SMul α δ<VAR>inst✝³ : SMul γ δ<VAR>inst✝² : IsScalarTower α β δ<VAR>inst✝¹ : IsScalarTower α γ δ<VAR>inst✝ : SMulCommClass β γ δ<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>d : δ<GOAL>(a • b) • c • d = (a • c) • b • d
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIocMod hp a (p + b) = toIocMod hp a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t✝ : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>h : IsBasis p s<VAR>t : Set α<GOAL>t ∈ h.filter ↔ ∃ i, p i ∧ s i ⊆ t
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>f : R[X]<VAR>n : ℕ<GOAL>f.degree < ↑n ↔ ∀ (m : ℕ), n ≤ m → f.coeff m = 0
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁸ : SeminormedAddCommGroup V<VAR>inst✝⁷ : PseudoMetricSpace P<VAR>inst✝⁶ : NormedAddTorsor V P<VAR>inst✝⁵ : NormedAddCommGroup W<VAR>inst✝⁴ : MetricSpace Q<VAR>inst✝³ : NormedAddTorsor W Q<VAR>𝕜 : Type u_6<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : NormedSpace 𝕜 V<VAR>inst✝ : NormedSpace 𝕜 W<VAR>p₁ p₂ : Q<VAR>h : p₁ ≠ p₂<VAR>c₁ c₂ : 𝕜<GOAL>dist c₁ c₂ ≤ ↑(nndist p₁ p₂)⁻¹ * dist ((lineMap p₁ p₂) c₁) ((lineMap p₁ p₂) c₂)
<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.280541, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.280548, u_2} D<VAR>X✝ Y✝ : C<VAR>inst✝ : HasInitial C<VAR>X Y : C<VAR>c : BinaryCofan X Y<VAR>h : IsVanKampenColimit c<GOAL>Mono c.inr
<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.280541, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.280548, u_2} D<VAR>X✝ Y✝ : C<VAR>inst✝ : HasInitial C<VAR>X Y : C<VAR>c : BinaryCofan X Y<VAR>h : IsVanKampenColimit c<GOAL>IsPullback (𝟙 ((pair X Y).obj { as := WalkingPair.right })) (𝟙 ((pair X Y).obj { as := WalkingPair.right })) c.inr c.inr
<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.280541, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.280548, u_2} D<VAR>X✝ Y✝ : C<VAR>inst✝ : HasInitial C<VAR>X Y : C<VAR>c : BinaryCofan X Y<VAR>h : IsVanKampenColimit c<GOAL>mapPair (initial.to X) (𝟙 Y) ≫ c.ι = (BinaryCofan.mk (initial.to Y) (𝟙 Y)).ι ≫ (Functor.const (Discrete WalkingPair)).map c.inr
<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.280541, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.280548, u_2} D<VAR>X✝ Y✝ : C<VAR>inst✝ : HasInitial C<VAR>X Y : C<VAR>c : BinaryCofan X Y<VAR>h : IsVanKampenColimit c<GOAL>IsColimit (BinaryCofan.mk (initial.to Y) (𝟙 Y))
<VAR>ι : Type u_1<VAR>inst✝⁴ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>inst✝³ : (i : ι) → AddCommMonoid (A i)<VAR>inst✝² : AddMonoid ι<VAR>inst✝¹ : GSemiring A<VAR>inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)<VAR>a a' : ⨁ (i : ι), A i<GOAL>((mulHom A) a) a' = DFinsupp.sum a fun i ai => DFinsupp.sum a' fun j aj => (of A (i + j)) (GradedMonoid.GMul.mul ai aj)
<VAR>ι : Type u_1<VAR>inst✝⁴ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>inst✝³ : (i : ι) → AddCommMonoid (A i)<VAR>inst✝² : AddMonoid ι<VAR>inst✝¹ : GSemiring A<VAR>inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)<VAR>a a' : ⨁ (i : ι), A i<GOAL>((DFinsupp.sumAddHom fun x => (toAddMonoid fun x_1 => ((compHom (of A (x + x_1))).comp (gMulHom A)).flip).flip) a) a' = DFinsupp.sum a fun i ai => DFinsupp.sum a' fun j aj => (of A (i + j)) (GradedMonoid.GMul.mul ai aj)
<VAR>ι : Type u_1<VAR>inst✝⁴ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>inst✝³ : (i : ι) → AddCommMonoid (A i)<VAR>inst✝² : AddMonoid ι<VAR>inst✝¹ : GSemiring A<VAR>inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)<VAR>a a' : ⨁ (i : ι), A i<GOAL>(DFinsupp.sum a fun x => ⇑(toAddMonoid fun x_1 => ((compHom (of A (x + x_1))).comp (gMulHom A)).flip).flip) a' = DFinsupp.sum a fun i ai => DFinsupp.sum a' fun j aj => (of A (i + j)) (GradedMonoid.GMul.mul ai aj)
<VAR>ι : Type u_1<VAR>inst✝⁴ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>inst✝³ : (i : ι) → AddCommMonoid (A i)<VAR>inst✝² : AddMonoid ι<VAR>inst✝¹ : GSemiring A<VAR>inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)<VAR>a a' : ⨁ (i : ι), A i<GOAL>(DFinsupp.sum a fun a b => ((toAddMonoid fun x => ((compHom (of A (a + x))).comp (gMulHom A)).flip).flip b) a') = DFinsupp.sum a fun i ai => DFinsupp.sum a' fun j aj => (of A (i + j)) (GradedMonoid.GMul.mul ai aj)
<VAR>ι : Type u_1<VAR>inst✝⁴ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>inst✝³ : (i : ι) → AddCommMonoid (A i)<VAR>inst✝² : AddMonoid ι<VAR>inst✝¹ : GSemiring A<VAR>inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)<VAR>a a' : ⨁ (i : ι), A i<GOAL>(fun a b => ((toAddMonoid fun x => ((compHom (of A (a + x))).comp (gMulHom A)).flip).flip b) a') = fun i ai => DFinsupp.sum a' fun j aj => (of A (i + j)) (GradedMonoid.GMul.mul ai aj)
<VAR>ι : Type u_1<VAR>inst✝⁴ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>inst✝³ : (i : ι) → AddCommMonoid (A i)<VAR>inst✝² : AddMonoid ι<VAR>inst✝¹ : GSemiring A<VAR>inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)<VAR>a a' : ⨁ (i : ι), A i<VAR>x : ι<GOAL>(fun b => ((toAddMonoid fun x_1 => ((compHom (of A (x + x_1))).comp (gMulHom A)).flip).flip b) a') = fun ai => DFinsupp.sum a' fun j aj => (of A (x + j)) (GradedMonoid.GMul.mul ai aj)
<VAR>ι : Type u_1<VAR>inst✝⁴ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>inst✝³ : (i : ι) → AddCommMonoid (A i)<VAR>inst✝² : AddMonoid ι<VAR>inst✝¹ : GSemiring A<VAR>inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)<VAR>a a' : ⨁ (i : ι), A i<VAR>x : ι<GOAL>(fun b => ((toAddMonoid fun x_1 => ((compHom (of A (x + x_1))).comp (gMulHom A)).flip) a') b) = fun ai => DFinsupp.sum a' fun j aj => (of A (x + j)) (GradedMonoid.GMul.mul ai aj)
<VAR>ι : Type u_1<VAR>inst✝⁴ : DecidableEq ι<VAR>A : ι → Type u_2<VAR>inst✝³ : (i : ι) → AddCommMonoid (A i)<VAR>inst✝² : AddMonoid ι<VAR>inst✝¹ : GSemiring A<VAR>inst✝ : (i : ι) → (x : A i) → Decidable (x ≠ 0)<VAR>a a' : ⨁ (i : ι), A i<VAR>x : ι<GOAL>(fun b => (DFinsupp.sum a' fun x_1 => ⇑((compHom (of A (x + x_1))).comp (gMulHom A)).flip) b) = fun ai => DFinsupp.sum a' fun j aj => (of A (x + j)) (GradedMonoid.GMul.mul ai aj)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>f : R →+* S<VAR>I J : Ideal S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Algebra (R ⧸ p) (S ⧸ P)<VAR>inst✝ : IsScalarTower R (R ⧸ p) (S ⧸ P)<VAR>h : Function.Injective ⇑(algebraMap (R ⧸ p) (S ⧸ P))<VAR>x : R<GOAL>x ∈ comap (algebraMap R S) P ↔ x ∈ p
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>S : Type u_2<VAR>inst✝³ : CommRing S<VAR>f : R →+* S<VAR>I J : Ideal S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Algebra (R ⧸ p) (S ⧸ P)<VAR>inst✝ : IsScalarTower R (R ⧸ p) (S ⧸ P)<VAR>h : Function.Injective ⇑(algebraMap (R ⧸ p) (S ⧸ P))<VAR>x : R<GOAL>(algebraMap (R ⧸ p) (S ⧸ P)) ((Quotient.mk p) x) = 0 ↔ (Quotient.mk p) x = 0
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>l : Multiset α<VAR>a : α<GOAL>l.Disjoint {a} ↔ a ∉ l
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>v w : V<GOAL>Fintype.card ↑(G.commonNeighbors v w) ≤ G.degree v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>v w : V<GOAL>Fintype.card ↑(G.commonNeighbors v w) ≤ Fintype.card ↑(G.neighborSet v)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ : Multiset α<VAR>a : α<VAR>s : Multiset α<GOAL>count a s = card s ↔ ∀ x ∈ s, a = x
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>p : Submodule K V<VAR>inst✝ : FiniteDimensional K ↥p<VAR>f : V →ₗ[K] V<VAR>h : ∀ x ∈ p, f x ∈ p<VAR>h' : Disjoint p (ker f)<GOAL>comap f p = p ⊔ ker f
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>p : Submodule K V<VAR>inst✝ : FiniteDimensional K ↥p<VAR>f : V →ₗ[K] V<VAR>h : ∀ x ∈ p, f x ∈ p<VAR>h' : Disjoint p (ker f)<VAR>x : V<VAR>hx : x ∈ comap f p<GOAL>x ∈ p ⊔ ker f
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>p : Submodule K V<VAR>inst✝ : FiniteDimensional K ↥p<VAR>f : V →ₗ[K] V<VAR>h : ∀ x ∈ p, f x ∈ p<VAR>h' : Disjoint p (ker f)<VAR>x : V<VAR>hx : x ∈ comap f p<VAR>y : V<VAR>hy : y ∈ p<VAR>hxy : (f.restrict h) ⟨y, hy⟩ = ⟨f x, hx⟩<GOAL>x ∈ p ⊔ ker f
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁵ : DivisionRing K<VAR>inst✝⁴ : AddCommGroup V<VAR>inst✝³ : Module K V<VAR>V₂ : Type v'<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module K V₂<VAR>p : Submodule K V<VAR>inst✝ : FiniteDimensional K ↥p<VAR>f : V →ₗ[K] V<VAR>h : ∀ x ∈ p, f x ∈ p<VAR>h' : Disjoint p (ker f)<VAR>x : V<VAR>hx : x ∈ comap f p<VAR>y : V<VAR>hy : y ∈ p<VAR>hxy : f y = f x<GOAL>x ∈ p ⊔ ker f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring S<VAR>inst✝² : Algebra R S<VAR>m : Type u_3<VAR>inst✝¹ : Fintype m<VAR>inst✝ : DecidableEq m<VAR>b : Basis m R S<VAR>x : S<VAR>i j : m<GOAL>(leftMulMatrix b) x i j = (b.repr (x * b j)) i
<VAR>s : Set Ordinal.{u}<VAR>a : Ordinal.{u}<VAR>hs : IsClosed s<GOAL>a ∈ s ↔ ∃ o, ∃ (_ : o ≠ 0), ∃ f, (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) ∧ o.bsup f = a
<VAR>R : Type u_1<VAR>inst✝³ : Semiring R<VAR>r : R<VAR>p : R[X]<VAR>S : Type u_2<VAR>inst✝² : AddCommMonoid S<VAR>inst✝¹ : Pow S ℕ<VAR>inst✝ : MulActionWithZero R S<VAR>x : S<GOAL>X.smeval x = x ^ 1
<VAR>n k p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℕ<VAR>ha₁ : n < p ^ a<VAR>ha₂ : k < p ^ a<GOAL>↑(n.choose k) ≡ ∏ i ∈ range a, ↑((n / p ^ i % p).choose (k / p ^ i % p)) [ZMOD ↑p]
<VAR>n k p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℕ<VAR>ha₁ : n < p ^ a<VAR>ha₂ : k < p ^ a<GOAL>↑((n / p ^ a).choose (k / p ^ a)) * ↑(∏ i ∈ range a, (n / p ^ i % p).choose (k / p ^ i % p)) ≡ ∏ i ∈ range a, ↑((n / p ^ i % p).choose (k / p ^ i % p)) [ZMOD ↑p]
<VAR>T : Type u<VAR>inst✝ : TopologicalSpace T<GOAL>Pretopology.ofGrothendieck (Opens T) (grothendieckTopology T) = pretopology T
<VAR>T : Type u<VAR>inst✝ : TopologicalSpace T<GOAL>Pretopology.ofGrothendieck (Opens T) (grothendieckTopology T) ≤ pretopology T
<VAR>T : Type u<VAR>inst✝ : TopologicalSpace T<GOAL>pretopology T ≤ Pretopology.ofGrothendieck (Opens T) (grothendieckTopology T)
<VAR>m n✝ n x : ℕ<VAR>h : x.Coprime n<GOAL>↑x * (↑x)⁻¹ = 1
<VAR>m n✝ n x : ℕ<VAR>h : (x % n).gcd n = 1<GOAL>↑x * (↑x)⁻¹ = 1
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>ι : Sort u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : α → M<VAR>s : Finset (PLift α)<VAR>hs : mulSupport (f ∘ PLift.down) ⊆ ↑s<VAR>x : PLift α<VAR>hx : x ∈ ⋯.toFinset<GOAL>x ∈ s
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>ι : Sort u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f : α → M<VAR>s : Finset (PLift α)<VAR>hs : mulSupport (f ∘ PLift.down) ⊆ ↑s<VAR>x : PLift α<VAR>hx : x ∈ mulSupport (f ∘ PLift.down)<GOAL>x ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝ : μ.HaveLebesgueDecomposition ν<VAR>hμν : μ ≪ ν<GOAL>∫⁻ (x : α), μ.rnDeriv ν x ∂ν = μ Set.univ