ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R✝ R : Presieve X<GOAL>(IsSeparatedFor P R ∧ ∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) ↔ IsSeparatedFor P R ∧ ∀ (x : FamilyOfElements P (generate R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>P Q U : Cᵒᵖ ⥤ Type w<VAR>X Y : C<VAR>S : Sieve X<VAR>R✝ R : Presieve X<GOAL>(∀ (x : FamilyOfElements P R), x.Compatible → ∃ t, x.IsAmalgamation t) ↔ ∀ (x : FamilyOfElements P (generate R).arrows), x.Compatible → ∃ t, x.IsAmalgamation t
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>l : Filter α<VAR>f✝ : α → R<VAR>r : R<VAR>inst✝¹ : LinearOrderedAddCommGroup R<VAR>inst✝ : Archimedean R<VAR>f : α → ℤ<VAR>hr : r < 0<VAR>hf : Tendsto f l atBot<GOAL>Tendsto (fun x => f x • r) l atTop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>t : Set γ<VAR>ht : MeasurableSet t<GOAL>κ ⊗ₖ η.restrict ht = (κ ⊗ₖ η).restrict ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>t : Set γ<VAR>ht : MeasurableSet t<GOAL>κ ⊗ₖ η.restrict ht = κ.restrict ?hs ⊗ₖ η.restrict ?ht
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>t : Set γ<VAR>ht : MeasurableSet t<GOAL>MeasurableSet Set.univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>s : Set (β × γ)<VAR>κ : Kernel α β<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝ : IsSFiniteKernel η<VAR>a : α<VAR>t : Set γ<VAR>ht : MeasurableSet t<GOAL>MeasurableSet t
<VAR>k G✝ : Type u<VAR>inst✝⁴ : CommRing k<VAR>inst✝³ : Group G✝<VAR>A : Rep k G✝<VAR>G : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : CommGroup M<VAR>inst✝ : MulAction G M<VAR>f : G → M<VAR>hf : IsMulOneCocycle f<VAR>g : G<GOAL>g • f g⁻¹ = (f g)⁻¹
<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 : α<VAR>m : ℤ<GOAL>toIcoDiv hp a (m • p + b) = m + toIcoDiv hp a b
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>h : λ ∣ FermatLastTheoremForThreeGen.Solution.z S<GOAL>False
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>h : (↑η - 1) * λ ∣ (↑η - 1) * FermatLastTheoremForThreeGen.Solution.z S<GOAL>False
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<VAR>h : λ ^ 2 ∣ S.a + ↑η ^ 2 * S.b<GOAL>False
<VAR>x : ℤ<VAR>hx : x ≠ 0<VAR>n d : ℤ<GOAL>n /. x / (d /. x) = n /. d
<VAR>𝕜 : Type u_1<VAR>inst✝³ : NNNorm 𝕜<VAR>inst✝² : Nonempty 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : Zero E<VAR>inst✝ : SMulZeroClass 𝕜 E<VAR>c : 𝕜<VAR>s t : Set E<VAR>x : E<VAR>r : ℝ≥0∞<GOAL>egauge 𝕜 0 x = ⊤ ↔ x ≠ 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>Q : QuadraticForm R M<VAR>a b : M<VAR>inst✝¹ : Invertible ((ι Q) a)<VAR>inst✝ : Invertible (Q a)<GOAL>(ι Q) a * (ι Q) b * ⅟((ι Q) a) = (ι Q) ((⅟(Q a) * QuadraticMap.polar (⇑Q) a b) • a - b)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹⁵ : NormedAddCommGroup D<VAR>inst✝¹⁴ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup X<VAR>inst✝⁶ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>R : Type u_3<VAR>inst✝⁵ : NormedRing R<VAR>inst✝⁴ : NormedAlgebra 𝕜 R<VAR>𝕜' : Type u_4<VAR>inst✝³ : NormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : CompleteSpace 𝕜'<VAR>inst✝ : CompleteSpace 𝕜<VAR>f g : E → 𝕜<VAR>n : ℕ∞<VAR>hf : ContDiffWithinAt 𝕜 n f s x<VAR>hg : ContDiffWithinAt 𝕜 n g s x<VAR>hx : g x ≠ 0<GOAL>ContDiffWithinAt 𝕜 n (fun x => f x / g x) s x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>inst✝⁴ : One M<VAR>inst✝³ : One N<VAR>inst✝² : FunLike F M N<VAR>inst✝¹ : Subsingleton M<VAR>inst✝ : OneHomClass F M N<VAR>f g : F<VAR>x : M<GOAL>f x = g x
<VAR>a b m n✝ p d n : ℕ<VAR>h : d ∣ n<GOAL>(n / d).factorization = n.factorization - d.factorization
<VAR>a b m n✝ p n : ℕ<VAR>h : 0 ∣ n<GOAL>(n / 0).factorization = n.factorization - factorization 0
<VAR>a b m n✝ p d n : ℕ<VAR>h : d ∣ n<VAR>hd : d ≠ 0<GOAL>(n / d).factorization = n.factorization - d.factorization
<VAR>a b m n p d : ℕ<VAR>hd : d ≠ 0<VAR>h : d ∣ 0<GOAL>(0 / d).factorization = factorization 0 - d.factorization
<VAR>a b m n✝ p d n : ℕ<VAR>h : d ∣ n<VAR>hd : d ≠ 0<VAR>hn : n ≠ 0<GOAL>(n / d).factorization = n.factorization - d.factorization
<VAR>a b m n✝ p d n : ℕ<VAR>h : d ∣ n<VAR>hd : d ≠ 0<VAR>hn : n ≠ 0<GOAL>(fun x => x + d.factorization) (n / d).factorization = (fun x => x + d.factorization) (n.factorization - d.factorization)
<VAR>a b m n✝ p d n : ℕ<VAR>h : d ∣ n<VAR>hd : d ≠ 0<VAR>hn : n ≠ 0<GOAL>(n / d).factorization + d.factorization = n.factorization - d.factorization + d.factorization
<VAR>α✝ : Sort u_1<VAR>β : Sort u_2<VAR>α : Sort u_3<VAR>r : α → α → Prop<VAR>iseqv✝¹ : Equivalence r<VAR>p : α → α → Prop<VAR>iseqv✝ : Equivalence p<VAR>Eq : ∀ (a b : α), Setoid.r a b ↔ Setoid.r a b<GOAL>{ r := r, iseqv := iseqv✝¹ } = { r := p, iseqv := iseqv✝ }
<VAR>α✝ : Sort u_1<VAR>β : Sort u_2<VAR>α : Sort u_3<VAR>r : α → α → Prop<VAR>iseqv✝¹ : Equivalence r<VAR>p : α → α → Prop<VAR>iseqv✝ : Equivalence p<VAR>Eq : ∀ (a b : α), Setoid.r a b ↔ Setoid.r a b<VAR>this : r = p<GOAL>{ r := r, iseqv := iseqv✝¹ } = { r := p, iseqv := iseqv✝ }
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>inst✝¹ : CountableInterFilter l<VAR>f g : α → β<VAR>p : Set α → Prop<VAR>s : Set α<VAR>inst✝ : HasCountableSeparatingOn α p s<VAR>hs : s ∈ l<VAR>hne : s.Nonempty<VAR>hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l<GOAL>∃ a ∈ s, {a} ∈ l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>inst✝¹ : CountableInterFilter l<VAR>f g : α → β<VAR>p : Set α → Prop<VAR>s : Set α<VAR>inst✝ : HasCountableSeparatingOn α p s<VAR>hs : s ∈ l<VAR>hne : s.Nonempty<VAR>hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l<VAR>t : Set α<VAR>hts : t ⊆ s<VAR>ht : t.Subsingleton<VAR>htl : t ∈ l<GOAL>∃ a ∈ s, {a} ∈ l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>inst✝¹ : CountableInterFilter l<VAR>f g : α → β<VAR>p : Set α → Prop<VAR>s : Set α<VAR>inst✝ : HasCountableSeparatingOn α p s<VAR>hs : s ∈ l<VAR>hne : s.Nonempty<VAR>hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l<VAR>hts : ∅ ⊆ s<VAR>ht : ∅.Subsingleton<VAR>htl : ∅ ∈ l<GOAL>∃ a ∈ s, {a} ∈ l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>inst✝¹ : CountableInterFilter l<VAR>f g : α → β<VAR>p : Set α → Prop<VAR>s : Set α<VAR>inst✝ : HasCountableSeparatingOn α p s<VAR>hs : s ∈ l<VAR>hne : s.Nonempty<VAR>hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l<VAR>x : α<VAR>hts : {x} ⊆ s<VAR>ht : {x}.Subsingleton<VAR>htl : {x} ∈ l<GOAL>∃ a ∈ s, {a} ∈ l
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝² : MonoidalCategory C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>U V W X✝ Y✝ Z✝ X Y Z X' : C<VAR>f : X ⟶ X'<GOAL>(f ⊗ 𝟙 (Y ⊗ Z)) ≫ (α_ X' Y Z).inv = (α_ X Y Z).inv ≫ ((f ⊗ 𝟙 Y) ⊗ 𝟙 Z)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>r : ℝ<VAR>x : E<VAR>hr : 0 < r<GOAL>Absorbent 𝕜 (Metric.ball 0 r)
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>r : ℝ<VAR>x : E<VAR>hr : 0 < r<GOAL>Absorbent 𝕜 ((normSeminorm 𝕜 E).ball 0 r)
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>Base : Set α → Prop<VAR>exch✝ : ExchangeProperty Base<VAR>B B' B₁ B₂ : Set α<VAR>exch : ExchangeProperty Base<VAR>hB₁ : Base B₁<VAR>hB₂ : Base B₂<GOAL>(B₁ \ B₂).encard ≤ (B₂ \ B₁).encard
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>Base : Set α → Prop<VAR>exch✝ : ExchangeProperty Base<VAR>B B' B₁ B₂ : Set α<VAR>exch : ExchangeProperty Base<VAR>hB₁ : Base B₁<VAR>hB₂ : Base B₂<VAR>he : B₂ \ B₁ = ∅<GOAL>(B₁ \ B₂).encard ≤ (B₂ \ B₁).encard
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>Base : Set α → Prop<VAR>exch✝ : ExchangeProperty Base<VAR>B B' B₁ B₂ : Set α<VAR>exch : ExchangeProperty Base<VAR>hB₁ : Base B₁<VAR>hB₂ : Base B₂<VAR>hinf : (B₂ \ B₁).encard = ⊤<GOAL>(B₁ \ B₂).encard ≤ (B₂ \ B₁).encard
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>Base : Set α → Prop<VAR>exch✝ : ExchangeProperty Base<VAR>B B' B₁ B₂ : Set α<VAR>exch : ExchangeProperty Base<VAR>hB₁ : Base B₁<VAR>hB₂ : Base B₂<VAR>e : α<VAR>he : e ∈ B₂ \ B₁<VAR>hcard : ((B₂ \ B₁) \ {e}).encard < (B₂ \ B₁).encard<GOAL>(B₁ \ B₂).encard ≤ (B₂ \ B₁).encard
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>Base : Set α → Prop<VAR>exch✝ : ExchangeProperty Base<VAR>B B' B₁ B₂ : Set α<VAR>exch : ExchangeProperty Base<VAR>hB₁ : Base B₁<VAR>hB₂ : Base B₂<VAR>e : α<VAR>he : e ∈ B₂ \ B₁<VAR>hcard : ((B₂ \ B₁) \ {e}).encard < (B₂ \ B₁).encard<VAR>f : α<VAR>hf : f ∈ B₁ \ B₂<VAR>hB' : Base (insert f (B₂ \ {e}))<GOAL>(B₁ \ B₂).encard ≤ (B₂ \ B₁).encard
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>Base : Set α → Prop<VAR>exch✝ : ExchangeProperty Base<VAR>B B' B₁ B₂ : Set α<VAR>exch : ExchangeProperty Base<VAR>hB₁ : Base B₁<VAR>hB₂ : Base B₂<VAR>e : α<VAR>he : e ∈ B₂ \ B₁<VAR>hcard : ((B₂ \ B₁) \ {e}).encard < (B₂ \ B₁).encard<VAR>f : α<VAR>hf : f ∈ B₁ \ B₂<VAR>hB' : Base (insert f (B₂ \ {e}))<VAR>this : (insert f (B₂ \ {e}) \ B₁).encard < (B₂ \ B₁).encard<GOAL>(B₁ \ B₂).encard ≤ (B₂ \ B₁).encard
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>Base : Set α → Prop<VAR>exch✝ : ExchangeProperty Base<VAR>B B' B₁ B₂ : Set α<VAR>exch : ExchangeProperty Base<VAR>hB₁ : Base B₁<VAR>hB₂ : Base B₂<VAR>e : α<VAR>he : e ∈ B₂ \ B₁<VAR>hcard : ((B₂ \ B₁) \ {e}).encard < (B₂ \ B₁).encard<VAR>f : α<VAR>hf : f ∈ B₁ \ B₂<VAR>hB' : Base (insert f (B₂ \ {e}))<VAR>this : (insert f (B₂ \ {e}) \ B₁).encard < (B₂ \ B₁).encard<VAR>hencard : (B₁ \ insert f (B₂ \ {e})).encard ≤ (insert f (B₂ \ {e}) \ B₁).encard<GOAL>(B₁ \ B₂).encard ≤ (B₂ \ B₁).encard
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>Base : Set α → Prop<VAR>exch✝ : ExchangeProperty Base<VAR>B B' B₁ B₂ : Set α<VAR>exch : ExchangeProperty Base<VAR>hB₁ : Base B₁<VAR>hB₂ : Base B₂<VAR>e : α<VAR>he : e ∈ B₂ \ B₁<VAR>hcard : ((B₂ \ B₁) \ {e}).encard < (B₂ \ B₁).encard<VAR>f : α<VAR>hf : f ∈ B₁ \ B₂<VAR>hB' : Base (insert f (B₂ \ {e}))<VAR>this : (insert f (B₂ \ {e}) \ B₁).encard < (B₂ \ B₁).encard<VAR>hencard : ((B₁ \ B₂) \ {f}).encard ≤ ((B₂ \ B₁) \ {e}).encard<GOAL>(B₁ \ B₂).encard ≤ (B₂ \ B₁).encard
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>Base : Set α → Prop<VAR>exch✝ : ExchangeProperty Base<VAR>B B' B₁ B₂ : Set α<VAR>exch : ExchangeProperty Base<VAR>hB₁ : Base B₁<VAR>hB₂ : Base B₂<VAR>e : α<VAR>he : e ∈ B₂ \ B₁<VAR>hcard : ((B₂ \ B₁) \ {e}).encard < (B₂ \ B₁).encard<VAR>f : α<VAR>hf : f ∈ B₁ \ B₂<VAR>hB' : Base (insert f (B₂ \ {e}))<VAR>this : (insert f (B₂ \ {e}) \ B₁).encard < (B₂ \ B₁).encard<VAR>hencard : ((B₁ \ B₂) \ {f}).encard ≤ ((B₂ \ B₁) \ {e}).encard<GOAL>((B₁ \ B₂) \ {f}).encard + 1 ≤ ((B₂ \ B₁) \ {e}).encard + 1
<VAR>R : Type u_1<VAR>inst✝⁹ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommRing S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommRing P<VAR>A : Type u_4<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : UniqueFactorizationMonoid A<VAR>K : Type u_5<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>x : K<VAR>h : num A x = 0<GOAL>0 * (algebraMap ?m.26953 K) ↑(den ?m.26953 x) = (algebraMap ?m.26953 K) (num ?m.26953 x)
<VAR>R : Type u<VAR>M : Type v<VAR>S✝ : Type u_1<VAR>N : Type u_2<VAR>inst✝⁵ : Ring R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Ring S✝<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>f : M →ₗ[R] N<VAR>hf : Surjective ⇑f<VAR>S : Submodule R N<VAR>hI : (comap f S).IsPrincipal<GOAL>S = span R {f (generator (comap f S))}
<VAR>B : Type u₁<VAR>inst✝¹ : Bicategory B<VAR>C : Type u₂<VAR>inst✝ : Bicategory C<VAR>F G H : OplaxFunctor B C<VAR>η : StrongOplaxNatTrans F G<VAR>θ : StrongOplaxNatTrans G H<VAR>a b c : B<VAR>a' : C<VAR>f : a' ⟶ G.obj a<VAR>g : a ⟶ b<VAR>h : b ⟶ c<GOAL>f ◁ (θ.naturality (g ≫ h)).hom ≫ f ◁ θ.app a ◁ H.mapComp g h = f ◁ G.mapComp g h ▷ θ.app c ≫ f ◁ (α_ (G.map g) (G.map h) (θ.app c)).hom ≫ f ◁ G.map g ◁ (θ.naturality h).hom ≫ f ◁ (α_ (G.map g) (θ.app b) (H.map h)).inv ≫ f ◁ (θ.naturality g).hom ▷ H.map h ≫ f ◁ (α_ (θ.app a) (H.map g) (H.map h)).hom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : CommMonoid α<VAR>inst✝³ : TopologicalSpace α<VAR>f✝ g✝ : β → α<VAR>a a₁ a₂ : α<VAR>inst✝² : T2Space α<VAR>α' : Type u_5<VAR>inst✝¹ : CommMonoid α'<VAR>inst✝ : TopologicalSpace α'<VAR>e : α' → α<VAR>hes : Surjective e<VAR>h1 : e 1 = 1<VAR>f : β → α<VAR>g : γ → α'<VAR>h : ∀ {a : α'}, HasProd f (e a) ↔ HasProd g a<VAR>hg : ¬Multipliable g<GOAL>∏' (b : β), f b = e (∏' (c : γ), g c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁴ : CommMonoid α<VAR>inst✝³ : TopologicalSpace α<VAR>f✝ g✝ : β → α<VAR>a a₁ a₂ : α<VAR>inst✝² : T2Space α<VAR>α' : Type u_5<VAR>inst✝¹ : CommMonoid α'<VAR>inst✝ : TopologicalSpace α'<VAR>e : α' → α<VAR>hes : Surjective e<VAR>h1 : e 1 = 1<VAR>f : β → α<VAR>g : γ → α'<VAR>h : ∀ {a : α'}, HasProd f (e a) ↔ HasProd g a<VAR>hg : ¬Multipliable g<VAR>hf : ¬Multipliable f<GOAL>∏' (b : β), f b = e (∏' (c : γ), g c)
<VAR>X : TopCat<VAR>p₀ : ↑X<VAR>inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)<VAR>C : Type v<VAR>inst✝¹ : Category.{w, v} C<VAR>inst✝ : HasTerminal C<VAR>A a : C<VAR>U : Opens ↑X<GOAL>(map' p₀ (𝟙 a)).app (op U) = (𝟙 (skyscraperPresheaf p₀ a)).app (op U)
<VAR>X : TopCat<VAR>p₀ : ↑X<VAR>inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)<VAR>C : Type v<VAR>inst✝¹ : Category.{w, v} C<VAR>inst✝ : HasTerminal C<VAR>A a : C<VAR>U : Opens ↑X<GOAL>(if h : p₀ ∈ U then eqToHom ⋯ ≫ 𝟙 a ≫ eqToHom ⋯ else (⋯ ▸ terminalIsTerminal).from ((skyscraperPresheaf p₀ a).obj (op U))) = (𝟙 (skyscraperPresheaf p₀ a)).app (op U)
<VAR>𝕜 : Type u_1<VAR>inst✝³² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³¹ : NormedAddCommGroup E<VAR>inst✝³⁰ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝²⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝²⁸ : TopologicalSpace M<VAR>inst✝²⁷ : ChartedSpace H M<VAR>inst✝²⁶ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝²⁵ : NormedAddCommGroup E'<VAR>inst✝²⁴ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²³ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²² : TopologicalSpace M'<VAR>inst✝²¹ : ChartedSpace H' M'<VAR>inst✝²⁰ : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_11<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_16<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_17<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>f✝ f₁ : M → M'<VAR>s✝ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>f : E → E'<VAR>s : Set E<VAR>x : E<GOAL>ContMDiffWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') n f s x ↔ ContDiffWithinAt 𝕜 n f s x
<VAR>𝕜 : Type u_1<VAR>inst✝³² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³¹ : NormedAddCommGroup E<VAR>inst✝³⁰ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝²⁹ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝²⁸ : TopologicalSpace M<VAR>inst✝²⁷ : ChartedSpace H M<VAR>inst✝²⁶ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝²⁵ : NormedAddCommGroup E'<VAR>inst✝²⁴ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²³ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²² : TopologicalSpace M'<VAR>inst✝²¹ : ChartedSpace H' M'<VAR>inst✝²⁰ : SmoothManifoldWithCorners I' M'<VAR>F : Type u_8<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_9<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_10<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_11<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_12<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_13<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_14<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_15<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_16<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_17<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>f✝ f₁ : M → M'<VAR>s✝ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>f : E → E'<VAR>s : Set E<VAR>x : E<GOAL>ContDiffWithinAt 𝕜 n f s x → ContinuousWithinAt f s x
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β✝ : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : DivisionCommMonoid β✝<VAR>A : Set α<VAR>B : Set β✝<VAR>f : α → β✝<VAR>m n : ℕ<VAR>β : Type u_5<VAR>inst✝ : DivisionCommMonoid β<VAR>B₁ B₂ : Set β<VAR>f₁ f₂ : α → β<VAR>h₁ : IsMulFreimanHom n A B₁ f₁<VAR>h₂ : IsMulFreimanHom n A B₂ f₂<VAR>s t : Multiset α<VAR>hsA : ∀ ⦃x : α⦄, x ∈ s → x ∈ A<VAR>htA : ∀ ⦃x : α⦄, x ∈ t → x ∈ A<VAR>hs : card s = n<VAR>ht : card t = n<VAR>h : s.prod = t.prod<GOAL>(map (f₁ / f₂) s).prod = (map (f₁ / f₂) t).prod
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f g : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn g s μ<VAR>hfg_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<GOAL>f =ᶠ[ae (μ.restrict t)] g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f g : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn g s μ<VAR>hfg_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<GOAL>f - g =ᶠ[ae (μ.restrict t)] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f g : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn g s μ<VAR>hfg_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<VAR>hfg' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, (f - g) x ∂μ = 0<GOAL>f - g =ᶠ[ae (μ.restrict t)] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f g : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hg_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn g s μ<VAR>hfg_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hμt : μ t ≠ ⊤<VAR>hfg' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, (f - g) x ∂μ = 0<VAR>hfg_int : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn (f - g) s μ<GOAL>f - g =ᶠ[ae (μ.restrict t)] 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : Group α<VAR>s t : Finset α<VAR>a b : α<GOAL>preimage 1 (fun x => x * b⁻¹) ⋯ = {b}
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>x : α<VAR>t : Set α<GOAL>t ∈ 𝓝 x ↔ ∃ i, (i ∈ 𝓤 α ∧ SymmetricRel i) ∧ ball x i ⊆ t
<GOAL>(fun t => (1 - rexp (-π * t))⁻¹) =O[atTop] fun x => 1
<GOAL>Tendsto (fun x => rexp (-π * x)) atTop (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>hs : autoParam s.Finite _auto✝<VAR>ht : autoParam t.Finite _auto✝<GOAL>s.ncard < t.ncard ↔ (s \ t).ncard < (t \ s).ncard
<VAR>m n a✝ b✝ c✝ d a b c : ℕ<VAR>hc : c ≤ a % c + b % c<VAR>hc0 : 0 < c<GOAL>(a + b) / c = a / c + b / c + 1
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>u v w : V<VAR>p : G.Walk u v<GOAL>p.toSubgraph ≤ ⊤.induce {v_1 | v_1 ∈ p.support}
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>u v w : V<VAR>p : G.Walk u v<GOAL>{v_1 | v_1 ∈ p.support} = p.toSubgraph.verts
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ γ₁ γ₂ : Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n' + a = n<VAR>p q : ℤ<VAR>hpq : p + n' = q<VAR>p' : ℤ<VAR>hp' : p + n = p'<GOAL>p' = q + a
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>K L M : CochainComplex C ℤ<VAR>n : ℤ<VAR>γ γ₁ γ₂ : Cochain K L n<VAR>a n' : ℤ<VAR>hn' : n' + a = n<VAR>p q : ℤ<VAR>hpq : p + n' = q<GOAL>(mk fun p q hpq => γ.v p (p + n) ⋯ ≫ (L.shiftFunctorObjXIso a q (p + n) ⋯).inv).v p q hpq = γ.v p (p + n) ⋯ ≫ (L.shiftFunctorObjXIso a q (p + n) ⋯).inv
<VAR>n m : ℕ<VAR>a b c : Fin n<GOAL>a < b ↔ a ≤ b ∧ a ≠ b
<VAR>n m : ℕ<VAR>a b c : Fin n<GOAL>a < b ↔ a ≤ b ∧ ↑a ≠ ↑b