ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Field K<VAR>inst✝² : IsDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>x : K<VAR>hx : IsIntegral A x<VAR>I : FractionalIdeal A⁰ K := adjoinIntegral A⁰ x hx<VAR>hI : IsUnit I<VAR>mul_self : I * I = I<GOAL>I = 1
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>S T : Set (Set α)<VAR>h_gen : m0 = generateFrom S<VAR>h_inter : IsPiSystem S<VAR>h_sub : T ⊆ S<VAR>hc : T.Countable<VAR>hU : ⋃₀ T = univ<VAR>htop : ∀ s ∈ T, μ s ≠ ⊤<VAR>h_eq : ∀ s ∈ S, μ s = ν s<GOAL>μ = ν
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>S T : Set (Set α)<VAR>h_gen : m0 = generateFrom S<VAR>h_inter : IsPiSystem S<VAR>h_sub : T ⊆ S<VAR>hc : T.Countable<VAR>hU : ⋃₀ T = univ<VAR>htop : ∀ s ∈ T, μ s ≠ ⊤<VAR>h_eq : ∀ s ∈ S, μ s = ν s<GOAL>∀ t ∈ T, ∀ s ∈ S, μ (s ∩ t) = ν (s ∩ t)
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ : Set α<VAR>S T : Set (Set α)<VAR>h_gen : m0 = generateFrom S<VAR>h_inter : IsPiSystem S<VAR>h_sub : T ⊆ S<VAR>hc : T.Countable<VAR>hU : ⋃₀ T = univ<VAR>htop : ∀ s ∈ T, μ s ≠ ⊤<VAR>h_eq : ∀ s ∈ S, μ s = ν s<VAR>t : Set α<VAR>ht : t ∈ T<VAR>s : Set α<VAR>hs : s ∈ S<GOAL>μ (s ∩ t) = ν (s ∩ t)
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ : Set α<VAR>S T : Set (Set α)<VAR>h_gen : m0 = generateFrom S<VAR>h_inter : IsPiSystem S<VAR>h_sub : T ⊆ S<VAR>hc : T.Countable<VAR>hU : ⋃₀ T = univ<VAR>htop : ∀ s ∈ T, μ s ≠ ⊤<VAR>h_eq : ∀ s ∈ S, μ s = ν s<VAR>t : Set α<VAR>ht : t ∈ T<VAR>s : Set α<VAR>hs : s ∈ S<VAR>H : s ∩ t = ∅<GOAL>μ (s ∩ t) = ν (s ∩ t)
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ : Set α<VAR>S T : Set (Set α)<VAR>h_gen : m0 = generateFrom S<VAR>h_inter : IsPiSystem S<VAR>h_sub : T ⊆ S<VAR>hc : T.Countable<VAR>hU : ⋃₀ T = univ<VAR>htop : ∀ s ∈ T, μ s ≠ ⊤<VAR>h_eq : ∀ s ∈ S, μ s = ν s<VAR>t : Set α<VAR>ht : t ∈ T<VAR>s : Set α<VAR>hs : s ∈ S<VAR>H : (s ∩ t).Nonempty<GOAL>μ (s ∩ t) = ν (s ∩ t)
<VAR>ι✝ : Sort u_1<VAR>f✝ g : ι✝ → ℝ≥0∞<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>ι : Sort u_2<VAR>f : ι → ℝ≥0∞<VAR>x : ℝ≥0∞<VAR>h0 : x ≠ 0<VAR>h : x ≠ ⊤<GOAL>x * iInf f = ⨅ i, x * f i
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>n m : σ →₀ ℕ<VAR>φ : MvPowerSeries σ R<GOAL>MvPolynomial.coeff m ((trunc R n) φ) = if m < n then (coeff R m) φ else 0
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>ι : Sort u_1<VAR>p : ι → Prop<VAR>s : ι → Set (α × α)<VAR>h : (𝓤 α).HasBasis p s<VAR>f : Filter α<GOAL>(∀ (i' : ι), p i' → ∃ i ∈ f, id i ×ˢ id i ⊆ s i') ↔ ∀ (i : ι), p i → ∃ t ∈ f, ∀ x ∈ t, ∀ y ∈ t, (x, y) ∈ s i
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝² : Mul G<VAR>inst✝¹ : Mul H<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>inst✝ : DecidableEq H<VAR>f : G →ₙ* H<VAR>hf : Function.Injective ⇑f<VAR>h : UniqueMul A B a0 b0<VAR>x✝¹ x✝ : H<GOAL>x✝¹ ∈ Finset.image (⇑f) A → x✝ ∈ Finset.image (⇑f) B → x✝¹ * x✝ = f a0 * f b0 → x✝¹ = f a0 ∧ x✝ = f b0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝² : Mul G<VAR>inst✝¹ : Mul H<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>inst✝ : DecidableEq H<VAR>f : G →ₙ* H<VAR>hf : Function.Injective ⇑f<VAR>h : UniqueMul A B a0 b0<VAR>x✝¹ x✝ : H<GOAL>(∃ a ∈ A, f a = x✝¹) → (∃ a ∈ B, f a = x✝) → x✝¹ * x✝ = f a0 * f b0 → x✝¹ = f a0 ∧ x✝ = f b0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝² : Mul G<VAR>inst✝¹ : Mul H<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>inst✝ : DecidableEq H<VAR>f : G →ₙ* H<VAR>hf : Function.Injective ⇑f<VAR>h : UniqueMul A B a0 b0<VAR>a : G<VAR>aA : a ∈ A<VAR>b : G<VAR>bB : b ∈ B<VAR>ab : f a * f b = f a0 * f b0<GOAL>f a = f a0 ∧ f b = f b0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝² : Mul G<VAR>inst✝¹ : Mul H<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>inst✝ : DecidableEq H<VAR>f : G →ₙ* H<VAR>hf : Function.Injective ⇑f<VAR>h : UniqueMul A B a0 b0<VAR>a : G<VAR>aA : a ∈ A<VAR>b : G<VAR>bB : b ∈ B<VAR>ab : a * b = a0 * b0<GOAL>a = a0 ∧ b = b0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : CommRing S<VAR>inst✝¹⁰ : CommRing T<VAR>inst✝⁹ : Algebra R S<VAR>inst✝⁸ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝⁴ : Fintype ι<VAR>F : Type u_6<VAR>inst✝³ : Field F<VAR>inst✝² : Algebra K S<VAR>inst✝¹ : Algebra K F<VAR>inst✝ : FiniteDimensional K L<VAR>x : L<GOAL>(Algebra.trace K L) x = finrank (↥K⟮x⟯) L • (Algebra.trace K ↥K⟮x⟯) (AdjoinSimple.gen K x)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : CommRing S<VAR>inst✝¹⁰ : CommRing T<VAR>inst✝⁹ : Algebra R S<VAR>inst✝⁸ : Algebra R T<VAR>K : Type u_4<VAR>L : Type u_5<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : Field L<VAR>inst✝⁵ : Algebra K L<VAR>ι κ : Type w<VAR>inst✝⁴ : Fintype ι<VAR>F : Type u_6<VAR>inst✝³ : Field F<VAR>inst✝² : Algebra K S<VAR>inst✝¹ : Algebra K F<VAR>inst✝ : FiniteDimensional K L<VAR>x : L<GOAL>(Algebra.trace K L) ((algebraMap (↥K⟮x⟯) L) (AdjoinSimple.gen K x)) = finrank (↥K⟮x⟯) L • (Algebra.trace K ↥K⟮x⟯) (AdjoinSimple.gen K x)
<VAR>α : Type u<VAR>inst✝¹ : EMetricSpace α<VAR>s : Set α<VAR>inst✝ : CompleteSpace α<GOAL>IsClosed (range NonemptyCompacts.toCloseds)
<VAR>α : Type u<VAR>inst✝¹ : EMetricSpace α<VAR>s : Set α<VAR>inst✝ : CompleteSpace α<VAR>this : range NonemptyCompacts.toCloseds = {s | (↑s).Nonempty ∧ IsCompact ↑s}<GOAL>IsClosed (range NonemptyCompacts.toCloseds)
<VAR>α : Type u<VAR>inst✝¹ : EMetricSpace α<VAR>s : Set α<VAR>inst✝ : CompleteSpace α<VAR>this : range NonemptyCompacts.toCloseds = {s | (↑s).Nonempty ∧ IsCompact ↑s}<GOAL>IsClosed {s | (↑s).Nonempty ∧ IsCompact ↑s}
<VAR>α : Type u<VAR>inst✝¹ : EMetricSpace α<VAR>s✝ : Set α<VAR>inst✝ : CompleteSpace α<VAR>this : range NonemptyCompacts.toCloseds = {s | (↑s).Nonempty ∧ IsCompact ↑s}<VAR>s : Closeds α<VAR>hs : s ∈ closure {s | (↑s).Nonempty ∧ IsCompact ↑s}<GOAL>(↑s).Nonempty
<VAR>α : Type u<VAR>inst✝¹ : EMetricSpace α<VAR>s✝ : Set α<VAR>inst✝ : CompleteSpace α<VAR>this : range NonemptyCompacts.toCloseds = {s | (↑s).Nonempty ∧ IsCompact ↑s}<VAR>s : Closeds α<VAR>hs : s ∈ closure {s | (↑s).Nonempty ∧ IsCompact ↑s}<GOAL>IsCompact ↑s
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>inst✝³ : Semiring R<VAR>inst✝² : Semiring S<VAR>inst✝¹ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>I✝ J : Ideal R<VAR>K L : Ideal S<VAR>G : Type u_2<VAR>inst✝ : FunLike G S R<VAR>rcg : RingHomClass G S R<VAR>g : G<VAR>I : Ideal R<VAR>hf : Set.LeftInvOn ⇑g ⇑f ↑I<GOAL>map f I ≤ comap g I
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>inst✝³ : Semiring R<VAR>inst✝² : Semiring S<VAR>inst✝¹ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>I✝ J : Ideal R<VAR>K L : Ideal S<VAR>G : Type u_2<VAR>inst✝ : FunLike G S R<VAR>rcg : RingHomClass G S R<VAR>g : G<VAR>I : Ideal R<VAR>hf : Set.LeftInvOn ⇑g ⇑f ↑I<GOAL>⇑f '' ↑I ⊆ ↑(comap g I)
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>inst✝³ : Semiring R<VAR>inst✝² : Semiring S<VAR>inst✝¹ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>I✝ J : Ideal R<VAR>K L : Ideal S<VAR>G : Type u_2<VAR>inst✝ : FunLike G S R<VAR>rcg : RingHomClass G S R<VAR>g : G<VAR>I : Ideal R<VAR>hf : Set.LeftInvOn ⇑g ⇑f ↑I<VAR>x : R<VAR>hx : x ∈ ↑I<GOAL>f x ∈ ↑(comap g I)
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>inst✝³ : Semiring R<VAR>inst✝² : Semiring S<VAR>inst✝¹ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>I✝ J : Ideal R<VAR>K L : Ideal S<VAR>G : Type u_2<VAR>inst✝ : FunLike G S R<VAR>rcg : RingHomClass G S R<VAR>g : G<VAR>I : Ideal R<VAR>hf : Set.LeftInvOn ⇑g ⇑f ↑I<VAR>x : R<VAR>hx : x ∈ ↑I<GOAL>x ∈ I
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f₁ f₂ : α → E<VAR>g₁ g₂ : α → F<VAR>hc : c₁ = c₂<VAR>hf : f₁ =ᶠ[l] f₂<VAR>hg : g₁ =ᶠ[l] g₂<GOAL>IsBigOWith c₁ l f₁ g₁ ↔ IsBigOWith c₂ l f₂ g₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f₁ f₂ : α → E<VAR>g₁ g₂ : α → F<VAR>hc : c₁ = c₂<VAR>hf : f₁ =ᶠ[l] f₂<VAR>hg : g₁ =ᶠ[l] g₂<GOAL>(∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖) ↔ ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₂ * ‖g₂ x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f₁ f₂ : α → E<VAR>g₁ g₂ : α → F<VAR>hf : f₁ =ᶠ[l] f₂<VAR>hg : g₁ =ᶠ[l] g₂<GOAL>(∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖) ↔ ∀ᶠ (x : α) in l, ‖f₂ x‖ ≤ c₁ * ‖g₂ x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f₁ f₂ : α → E<VAR>g₁ g₂ : α → F<VAR>hf : f₁ =ᶠ[l] f₂<VAR>hg : g₁ =ᶠ[l] g₂<GOAL>∀ᶠ (x : α) in l, ‖f₁ x‖ ≤ c₁ * ‖g₁ x‖ ↔ ‖f₂ x‖ ≤ c₁ * ‖g₂ x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f₁ f₂ : α → E<VAR>g₁ g₂ : α → F<VAR>hf : f₁ =ᶠ[l] f₂<VAR>hg : g₁ =ᶠ[l] g₂<VAR>a✝ : α<VAR>e₁ : f₁ a✝ = f₂ a✝<VAR>e₂ : g₁ a✝ = g₂ a✝<GOAL>‖f₁ a✝‖ ≤ c₁ * ‖g₁ a✝‖ ↔ ‖f₂ a✝‖ ≤ c₁ * ‖g₂ a✝‖
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>σ : Type u_4<VAR>inst✝⁴ : Mul M<VAR>inst✝³ : Mul N<VAR>inst✝² : Mul P<VAR>S : Subsemigroup M<VAR>inst✝¹ : Nonempty M<VAR>inst✝ : Nonempty N<VAR>s : Subsemigroup M<VAR>t : Subsemigroup N<GOAL>s.prod t = ⊤ ↔ s = ⊤ ∧ t = ⊤
<VAR>a✝ b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>a : ℕ<VAR>hb : 0 < b<GOAL>a < b * (a / b + 1)
<VAR>a✝ b c d m n k : ℕ<VAR>p q : ℕ → Prop<VAR>a : ℕ<VAR>hb : 0 < b<GOAL>a / b < a / b + 1
<VAR>R : Type u_1<VAR>inst✝¹ : NonAssocSemiring R<VAR>inst✝ : CharP R 1<VAR>r : R<GOAL>r = 1 * r
<VAR>R : Type u_1<VAR>inst✝¹ : NonAssocSemiring R<VAR>inst✝ : CharP R 1<VAR>r : R<GOAL>1 * r = ↑1 * r
<VAR>R : Type u_1<VAR>inst✝¹ : NonAssocSemiring R<VAR>inst✝ : CharP R 1<VAR>r : R<GOAL>↑1 * r = 0 * r
<VAR>R : Type u_1<VAR>inst✝¹ : NonAssocSemiring R<VAR>inst✝ : CharP R 1<VAR>r : R<GOAL>0 * r = 0
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>D : Type u'<VAR>inst✝¹ : Category.{v', u'} D<VAR>inst✝ : Preadditive D<VAR>x✝ : CochainComplex C ℤ<VAR>i✝ : ℤ<GOAL>((shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app x✝).f i✝ = ((shiftFunctorZero' C 0 ⋯).hom.app x✝).f i✝
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>f✝ : α → β<VAR>s t✝ : Set α<VAR>a : α<VAR>inst✝¹ : IsRefl α r<VAR>inst✝ : IsTrans α r<VAR>t : Set β<VAR>hs : s.PartiallyWellOrderedOn r<VAR>ht : t.PartiallyWellOrderedOn r'<VAR>f : ℕ → α × β<VAR>hf : ∀ (n : ℕ), f n ∈ s ×ˢ t<GOAL>∃ m n, m < n ∧ (fun x y => r x.1 y.1 ∧ r' x.2 y.2) (f m) (f n)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>f✝ : α → β<VAR>s t✝ : Set α<VAR>a : α<VAR>inst✝¹ : IsRefl α r<VAR>inst✝ : IsTrans α r<VAR>t : Set β<VAR>hs : s.PartiallyWellOrderedOn r<VAR>ht : t.PartiallyWellOrderedOn r'<VAR>f : ℕ → α × β<VAR>hf : ∀ (n : ℕ), f n ∈ s ×ˢ t<VAR>g₁ : ℕ ↪o ℕ<VAR>h₁ : ∀ (m n : ℕ), m ≤ n → r ((Prod.fst ∘ f) (g₁ m)) ((Prod.fst ∘ f) (g₁ n))<GOAL>∃ m n, m < n ∧ (fun x y => r x.1 y.1 ∧ r' x.2 y.2) (f m) (f n)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>r : α → α → Prop<VAR>r' : β → β → Prop<VAR>f✝ : α → β<VAR>s t✝ : Set α<VAR>a : α<VAR>inst✝¹ : IsRefl α r<VAR>inst✝ : IsTrans α r<VAR>t : Set β<VAR>hs : s.PartiallyWellOrderedOn r<VAR>ht : t.PartiallyWellOrderedOn r'<VAR>f : ℕ → α × β<VAR>hf : ∀ (n : ℕ), f n ∈ s ×ˢ t<VAR>g₁ : ℕ ↪o ℕ<VAR>h₁ : ∀ (m n : ℕ), m ≤ n → r ((Prod.fst ∘ f) (g₁ m)) ((Prod.fst ∘ f) (g₁ n))<VAR>m n : ℕ<VAR>hlt : m < n<VAR>hle : r' ((Prod.snd ∘ f ∘ ⇑g₁) m) ((Prod.snd ∘ f ∘ ⇑g₁) n)<GOAL>∃ m n, m < n ∧ (fun x y => r x.1 y.1 ∧ r' x.2 y.2) (f m) (f n)
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.60184, u_1} C<VAR>U✝ : TopCat<VAR>X : PresheafedSpace C<VAR>f✝ : U✝ ⟶ ↑X<VAR>h : OpenEmbedding ⇑f✝<VAR>U V : (Opens ↑↑X)ᵒᵖ<VAR>f : U ⟶ V<GOAL>X.presheaf.map f ≫ (fun V => X.presheaf.map (⋯.adjunction.counit.app (unop V)).op) V = (fun V => X.presheaf.map (⋯.adjunction.counit.app (unop V)).op) U ≫ X.presheaf.map (⋯.functor.op.map ((Opens.map f✝).op.map f))
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.60184, u_1} C<VAR>U✝ : TopCat<VAR>X : PresheafedSpace C<VAR>f✝ : U✝ ⟶ ↑X<VAR>h : OpenEmbedding ⇑f✝<VAR>U V : (Opens ↑↑X)ᵒᵖ<VAR>f : U ⟶ V<GOAL>X.presheaf.map (f ≫ (⋯.adjunction.counit.app (unop V)).op) = X.presheaf.map ((⋯.adjunction.counit.app (unop U)).op ≫ ⋯.functor.op.map ((Opens.map f✝).op.map f))
<VAR>α : Type u_1<VAR>inst✝ : Fintype α<VAR>s : Finset α<VAR>k : ℕ<GOAL>↑univ.powerset = ↑univ
<VAR>R : Type u_1<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>n : ℕ<VAR>t : R<VAR>ht : dist t 0 < 1<GOAL>‖t‖ < 1
<VAR>R : Type u_1<VAR>x y : R<VAR>n m p : ℕ<VAR>inst✝ : Semiring R<VAR>hp : n + m ≤ p + 1<VAR>h_comm : Commute x y<VAR>hy : y ^ n = 0<GOAL>x ^ m ∣ (x + y) ^ p
<VAR>R : Type u_1<VAR>x y : R<VAR>n m p : ℕ<VAR>inst✝ : Semiring R<VAR>hp : n + m ≤ p + 1<VAR>h_comm : Commute x y<VAR>hy : y ^ n = 0<GOAL>x ^ m ∣ ∑ m ∈ Finset.antidiagonal p, p.choose m.1 • (x ^ m.1 * y ^ m.2)
<VAR>R : Type u_1<VAR>x y : R<VAR>n m p : ℕ<VAR>inst✝ : Semiring R<VAR>hp : n + m ≤ p + 1<VAR>h_comm : Commute x y<VAR>hy : y ^ n = 0<VAR>x✝ : ℕ × ℕ<VAR>i j : ℕ<VAR>hij : (i, j) ∈ Finset.antidiagonal p<GOAL>x ^ m ∣ p.choose (i, j).1 • (x ^ (i, j).1 * y ^ (i, j).2)
<VAR>R : Type u_1<VAR>x y : R<VAR>n m p : ℕ<VAR>inst✝ : Semiring R<VAR>hp : n + m ≤ p + 1<VAR>h_comm : Commute x y<VAR>hy : y ^ n = 0<VAR>x✝ : ℕ × ℕ<VAR>i j : ℕ<VAR>hij : i + j = p<GOAL>x ^ m ∣ p.choose (i, j).1 • (x ^ (i, j).1 * y ^ (i, j).2)
<VAR>R : Type u_1<VAR>x y : R<VAR>n m p : ℕ<VAR>inst✝ : Semiring R<VAR>hp : n + m ≤ p + 1<VAR>h_comm : Commute x y<VAR>hy : y ^ n = 0<VAR>x✝ : ℕ × ℕ<VAR>i j : ℕ<VAR>hij : i + j = p<GOAL>x ^ m ∣ x ^ (i, j).1 * y ^ (i, j).2
<VAR>R : Type u_1<VAR>x y : R<VAR>n m p : ℕ<VAR>inst✝ : Semiring R<VAR>hp : n + m ≤ p + 1<VAR>h_comm : Commute x y<VAR>hy : y ^ n = 0<VAR>x✝ : ℕ × ℕ<VAR>i j : ℕ<VAR>hij : i + j = p<VAR>hi : m ≤ i<GOAL>x ^ m ∣ x ^ (i, j).1 * y ^ (i, j).2
<VAR>R : Type u_1<VAR>x y : R<VAR>n m p : ℕ<VAR>inst✝ : Semiring R<VAR>hp : n + m ≤ p + 1<VAR>h_comm : Commute x y<VAR>hy : y ^ n = 0<VAR>x✝ : ℕ × ℕ<VAR>i j : ℕ<VAR>hij : i + j = p<VAR>hi : i + 1 ≤ m<GOAL>x ^ m ∣ x ^ (i, j).1 * y ^ (i, j).2
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>inst✝⁶ : Category.{?u.63403, u_1} C<VAR>inst✝⁵ : Category.{?u.63407, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>inst✝⁴ : AddMonoid M<VAR>inst✝³ : HasShift C M<VAR>G : Type u_4<VAR>inst✝² : AddGroup G<VAR>inst✝¹ : HasShift C G<VAR>inst✝ : F.ShiftSequence M<VAR>n m mn : M<VAR>hnm : m + n = mn<VAR>a a' a'' : M<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<VAR>X : C<GOAL>mn + a = a''
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>inst✝⁶ : Category.{u_6, u_1} C<VAR>inst✝⁵ : Category.{u_5, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>inst✝⁴ : AddMonoid M<VAR>inst✝³ : HasShift C M<VAR>G : Type u_4<VAR>inst✝² : AddGroup G<VAR>inst✝¹ : HasShift C G<VAR>inst✝ : F.ShiftSequence M<VAR>n m mn : M<VAR>hnm : m + n = mn<VAR>a a' a'' : M<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<VAR>X : C<GOAL>(F.shiftIso mn a a'' ⋯).inv.app X = (F.shiftIso m a' a'' ha'').inv.app X ≫ (F.shiftIso n a a' ha').inv.app ((shiftFunctor C m).obj X) ≫ (F.shift a).map ((shiftFunctorAdd' C m n mn hnm).inv.app X)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>x : PrimeSpectrum R<GOAL>closure {x} = zeroLocus ↑x.asIdeal
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>X Y Z : C<VAR>inst✝² : HasZeroMorphisms C<VAR>f : X ⟶ Y<VAR>inst✝¹ : HasKernel f<VAR>X' Y' : C<VAR>f' : X' ⟶ Y'<VAR>inst✝ : HasKernel f'<VAR>sq : Arrow.mk f ⟶ Arrow.mk f'<GOAL>(kernelSubobjectIso f).hom ≫ kernel.map f f' sq.left sq.right ⋯ = kernelSubobjectMap sq ≫ (kernelSubobjectIso f').hom
<VAR>n m : SimplexCategory<VAR>f : n ⟶ m<GOAL>Epi f ↔ Function.Surjective ⇑(Hom.toOrderHom f)
<VAR>n m : SimplexCategory<VAR>f : n ⟶ m<GOAL>Epi (skeletalEquivalence.functor.map f) ↔ Function.Surjective ⇑(Hom.toOrderHom f)
<VAR>n m : SimplexCategory<VAR>f : n ⟶ m<GOAL>Epi (skeletalFunctor.map f) ↔ Function.Surjective ⇑(Hom.toOrderHom f)
<VAR>R✝ : Type u_1<VAR>inst✝¹³ : CommSemiring R✝<VAR>A✝ : Type u_2<VAR>B✝ : Type u_3<VAR>inst✝¹² : Semiring A✝<VAR>inst✝¹¹ : Semiring B✝<VAR>inst✝¹⁰ : Algebra R✝ A✝<VAR>inst✝⁹ : Algebra R✝ B✝<VAR>R : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>A : Type u_5<VAR>B : Type u_6<VAR>C : Type u_7<VAR>D : Type u_8<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : Ring C<VAR>inst✝⁴ : Ring D<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra R C<VAR>inst✝ : Algebra R D<VAR>f : A →ₐ[R] B<VAR>g : C →ₐ[R] D<VAR>hf : Function.Surjective ⇑f<VAR>hg : Function.Surjective ⇑g<GOAL>RingHom.ker (map f g) = Ideal.map includeLeft (RingHom.ker f) ⊔ Ideal.map includeRight (RingHom.ker g)
<VAR>R✝ : Type u_1<VAR>inst✝¹³ : CommSemiring R✝<VAR>A✝ : Type u_2<VAR>B✝ : Type u_3<VAR>inst✝¹² : Semiring A✝<VAR>inst✝¹¹ : Semiring B✝<VAR>inst✝¹⁰ : Algebra R✝ A✝<VAR>inst✝⁹ : Algebra R✝ B✝<VAR>R : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>A : Type u_5<VAR>B : Type u_6<VAR>C : Type u_7<VAR>D : Type u_8<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : Ring C<VAR>inst✝⁴ : Ring D<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra R C<VAR>inst✝ : Algebra R D<VAR>f : A →ₐ[R] B<VAR>g : C →ₐ[R] D<VAR>hf : Function.Surjective ⇑f<VAR>hg : Function.Surjective ⇑g<VAR>this : map f g = (map f (AlgHom.id R D)).comp (map (AlgHom.id R A) g)<GOAL>RingHom.ker (map f g) = Ideal.map includeLeft (RingHom.ker f) ⊔ Ideal.map includeRight (RingHom.ker g)
<VAR>R✝ : Type u_1<VAR>inst✝¹³ : CommSemiring R✝<VAR>A✝ : Type u_2<VAR>B✝ : Type u_3<VAR>inst✝¹² : Semiring A✝<VAR>inst✝¹¹ : Semiring B✝<VAR>inst✝¹⁰ : Algebra R✝ A✝<VAR>inst✝⁹ : Algebra R✝ B✝<VAR>R : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>A : Type u_5<VAR>B : Type u_6<VAR>C : Type u_7<VAR>D : Type u_8<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : Ring C<VAR>inst✝⁴ : Ring D<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra R C<VAR>inst✝ : Algebra R D<VAR>f : A →ₐ[R] B<VAR>g : C →ₐ[R] D<VAR>hf : Function.Surjective ⇑f<VAR>hg : Function.Surjective ⇑g<VAR>this : map f g = (map f (AlgHom.id R D)).comp (map (AlgHom.id R A) g)<GOAL>RingHom.ker ((map f (AlgHom.id R D)).comp (map (AlgHom.id R A) g)) = Ideal.map includeLeft (RingHom.ker f) ⊔ Ideal.map includeRight (RingHom.ker g)
<VAR>R✝ : Type u_1<VAR>inst✝¹³ : CommSemiring R✝<VAR>A✝ : Type u_2<VAR>B✝ : Type u_3<VAR>inst✝¹² : Semiring A✝<VAR>inst✝¹¹ : Semiring B✝<VAR>inst✝¹⁰ : Algebra R✝ A✝<VAR>inst✝⁹ : Algebra R✝ B✝<VAR>R : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>A : Type u_5<VAR>B : Type u_6<VAR>C : Type u_7<VAR>D : Type u_8<VAR>inst✝⁷ : Ring A<VAR>inst✝⁶ : Ring B<VAR>inst✝⁵ : Ring C<VAR>inst✝⁴ : Ring D<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra R C<VAR>inst✝ : Algebra R D<VAR>f : A →ₐ[R] B<VAR>g : C →ₐ[R] D<VAR>hf : Function.Surjective ⇑f<VAR>hg : Function.Surjective ⇑g<VAR>this : map f g = (map f (AlgHom.id R D)).comp (map (AlgHom.id R A) g)<GOAL>RingHom.ker ((↑(map f (AlgHom.id R D))).comp ↑(map (AlgHom.id R A) g)) = Ideal.map includeLeft (RingHom.ker ↑f) ⊔ Ideal.map includeRight (RingHom.ker ↑g)