ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'<VAR>m : (i : ι) → E i<VAR>x : G<GOAL>‖{ toFun := fun x => (f x) m, map_add' := ⋯, map_smul' := ⋯ } x‖ ≤ ‖f‖ * ‖x‖ * ∏ i : ι, ‖m i‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹³ : Fintype ι<VAR>inst✝¹² : Fintype ι'<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁹ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁸ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁶ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁵ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁴ : SeminormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>inst✝² : SeminormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace 𝕜 G'<VAR>f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'<VAR>inst✝ : DecidableEq ι<VAR>m : (i : ι) → E i<VAR>i : ι<VAR>x y : E i<VAR>x✝ : G<GOAL>((fun m => { toFun := fun x => (f x) m, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous (‖f‖ * ∏ i : ι, ‖m i‖) ⋯) (update m i (x + y))) x✝ = ((fun m => { toFun := fun x => (f x) m, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous (‖f‖ * ∏ i : ι, ‖m i‖) ⋯) (update m i x) + (fun m => { toFun := fun x => (f x) m, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous (‖f‖ * ∏ i : ι, ‖m i‖) ⋯) (update m i y)) x✝
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹³ : Fintype ι<VAR>inst✝¹² : Fintype ι'<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁹ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁸ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁷ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁶ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁵ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁴ : SeminormedAddCommGroup G<VAR>inst✝³ : NormedSpace 𝕜 G<VAR>inst✝² : SeminormedAddCommGroup G'<VAR>inst✝¹ : NormedSpace 𝕜 G'<VAR>f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'<VAR>inst✝ : DecidableEq ι<VAR>m : (i : ι) → E i<VAR>i : ι<VAR>c : 𝕜<VAR>x : E i<VAR>x✝ : G<GOAL>((fun m => { toFun := fun x => (f x) m, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous (‖f‖ * ∏ i : ι, ‖m i‖) ⋯) (update m i (c • x))) x✝ = (c • (fun m => { toFun := fun x => (f x) m, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous (‖f‖ * ∏ i : ι, ‖m i‖) ⋯) (update m i x)) x✝
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'<VAR>m : (i : ι) → E i<GOAL>‖{ toFun := fun m => { toFun := fun x => (f x) m, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous (‖f‖ * ∏ i : ι, ‖m i‖) ⋯, map_add' := ⋯, map_smul' := ⋯ } m‖ ≤ ‖f‖ * ∏ i : ι, ‖m i‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁸ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f : G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'<VAR>m : (i : ι) → E i<GOAL>‖{ toFun := fun x => (f x) m, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous (‖f‖ * ∏ i : ι, ‖m i‖) ⋯‖ ≤ ‖f‖ * ∏ i : ι, ‖m i‖
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : Affine R<VAR>x y : R<VAR>h : W.Equation x y<VAR>hΔ : Δ W ≠ 0<GOAL>Δ (variableChange W { u := 1, r := x, s := 0, t := y }).toAffine ≠ 0
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>inst✝¹ : DecidableEq V<VAR>inst✝ : G.LocallyFinite<VAR>u v : V<VAR>n : ℕ<VAR>p : G.Walk u v<GOAL>p ∈ G.finsetWalkLength n u v ↔ p ∈ {p | p.length = n}
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a✝ b✝ c u a : αˣ<VAR>b : α<GOAL>↑a⁻¹ * (↑a * b) = b
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>p : R[X]<VAR>hp : p ∈ degreeLT R n<GOAL>(degreeLTEquiv R n) ⟨p, hp⟩ = 0 ↔ p = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>p : R⟦X⟧<VAR>n d : ℕ<GOAL>(coeff R (d + n)) (X ^ n * p) = (coeff R d) p
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>p : R⟦X⟧<VAR>n d : ℕ<GOAL>∀ b ∈ antidiagonal (d + n), b ≠ (n, d) → (coeff R b.1) (X ^ n) * (coeff R b.2) p = 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>p : R⟦X⟧<VAR>n d : ℕ<GOAL>(n, d) ∉ antidiagonal (d + n) → (coeff R (n, d).1) (X ^ n) * (coeff R (n, d).2) p = 0
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝ : CommRing R<GOAL>⊥.jacobson ≤ sInf (map C '' {J | J.IsMaximal})
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝ : CommRing R<VAR>J : Ideal R[X]<VAR>j : Ideal R<VAR>hj : j ∈ {J | J.IsMaximal} ∧ map C j = J<GOAL>⊥.jacobson ≤ J
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝ : CommRing R<VAR>J : Ideal R[X]<VAR>j : Ideal R<VAR>hj : j ∈ {J | J.IsMaximal} ∧ map C j = J<VAR>this : j.IsMaximal<GOAL>⊥.jacobson ≤ J
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝ : CommRing R<VAR>J : Ideal R[X]<VAR>j : Ideal R<VAR>hj : j ∈ {J | J.IsMaximal} ∧ map C j = J<VAR>this : j.IsMaximal<GOAL>J.jacobson = J
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝ : CommRing R<VAR>J : Ideal R[X]<VAR>j : Ideal R<VAR>hj : j ∈ {J | J.IsMaximal} ∧ map C j = J<VAR>this : j.IsMaximal<GOAL>⊥.jacobson = ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝ : CommRing R<VAR>J : Ideal R[X]<VAR>j : Ideal R<VAR>hj : j ∈ {J | J.IsMaximal} ∧ map C j = J<VAR>this : j.IsMaximal<VAR>f : (R ⧸ j)[X]<VAR>hf : f ∈ ⊥.jacobson<GOAL>f ∈ ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝ : CommRing R<VAR>J : Ideal R[X]<VAR>j : Ideal R<VAR>hj : j ∈ {J | J.IsMaximal} ∧ map C j = J<VAR>this : j.IsMaximal<VAR>f : (R ⧸ j)[X]<VAR>hf : f ∈ ⊥.jacobson<VAR>r1 : X ≠ 0<GOAL>f ∈ ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝ : CommRing R<VAR>J : Ideal R[X]<VAR>j : Ideal R<VAR>hj : j ∈ {J | J.IsMaximal} ∧ map C j = J<VAR>this : j.IsMaximal<VAR>f : (R ⧸ j)[X]<VAR>hf : f ∈ ⊥.jacobson<VAR>r1 : X ≠ 0<VAR>r2 : f * X + 1 = C ((f * X + 1).coeff 0)<GOAL>f ∈ ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝ : CommRing R<VAR>J : Ideal R[X]<VAR>j : Ideal R<VAR>hj : j ∈ {J | J.IsMaximal} ∧ map C j = J<VAR>this : j.IsMaximal<VAR>f : (R ⧸ j)[X]<VAR>hf : f ∈ ⊥.jacobson<VAR>r1 : X ≠ 0<VAR>r2 : f * X + 1 = C 1<GOAL>f ∈ ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝ : CommRing R<VAR>J : Ideal R[X]<VAR>j : Ideal R<VAR>hj : j ∈ {J | J.IsMaximal} ∧ map C j = J<VAR>this : j.IsMaximal<VAR>f : (R ⧸ j)[X]<VAR>hf : f ∈ ⊥.jacobson<VAR>r1 : X ≠ 0<VAR>r2 : f * X = 0<GOAL>f ∈ ⊥
<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>inst✝ : IsLocalization M S<VAR>x : S<GOAL>x ∈ invSubmonoid M S ↔ ∃ m, mk' S 1 m = x
<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>inst✝ : IsLocalization M S<VAR>x : S<GOAL>x ∈ invSubmonoid M S ↔ ∃ m, ↑((toInvSubmonoid M S) m) = x
<VAR>U : Type u_1<VAR>inst✝ : Quiver U<VAR>u v u' v' : U<VAR>hu : u = u'<VAR>hv : v = v'<VAR>p : Path u v<GOAL>HEq (cast hu hv p) p
<VAR>U : Type u_1<VAR>inst✝ : Quiver U<VAR>u v u' v' : U<VAR>hu : u = u'<VAR>hv : v = v'<VAR>p : Path u v<GOAL>HEq (_root_.cast ⋯ p) p
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝² : Category.{u_2, u_1} D<VAR>P : MorphismProperty C<VAR>inst✝¹ : P.RespectsIso<VAR>F : C ⥤ D<VAR>inst✝ : F.IsEquivalence<GOAL>(P.map F).inverseImage F = P
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : Semiring R<VAR>m n✝ : σ →₀ ℕ<VAR>φ ψ φ₁ φ₂ φ₃ : MvPowerSeries σ R<VAR>n : σ →₀ ℕ<GOAL>(coeff R n) (φ₁ * φ₂ * φ₃) = (coeff R n) (φ₁ * (φ₂ * φ₃))
<GOAL>WithBot.some ∘ WithTop.some ⁻¹' Iio ↑⊤ = univ
<GOAL>WithTop.some ⁻¹' (WithBot.some ⁻¹' Iio ↑⊤) = univ
<VAR>x y : ℝ<VAR>hxy : x < y<GOAL>Icc x y ∈ (vitaliFamily volume 1).setsAt y
<VAR>x y : ℝ<VAR>hxy : x < y<GOAL>Metric.closedBall ((x + y) / 2) ((y - x) / 2) ∈ (vitaliFamily volume 1).setsAt y
<VAR>x y : ℝ<VAR>hxy : x < y<GOAL>dist y ((x + y) / 2) ≤ 1 * ((y - x) / 2)
<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✝ : AddCommMonoid M<VAR>f : α → β<VAR>l : β →₀ M<VAR>hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support<GOAL>comapDomain f l ⋯ = 0 → l = 0
<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✝ : AddCommMonoid M<VAR>f : α → β<VAR>l : β →₀ M<VAR>hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support<GOAL>{ support := l.support.preimage f ⋯, toFun := fun a => l (f a), mem_support_toFun := ⋯ }.support = ∅ → l.support = ∅
<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✝ : AddCommMonoid M<VAR>f : α → β<VAR>l : β →₀ M<VAR>hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support<GOAL>(∀ (a : α), f a ∉ l.support) → ∀ (a : β), a ∉ l.support
<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✝ : AddCommMonoid M<VAR>f : α → β<VAR>l : β →₀ M<VAR>hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support<VAR>h : ∀ (a : α), f a ∉ l.support<VAR>a : β<VAR>ha : a ∈ l.support<GOAL>False
<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✝ : AddCommMonoid M<VAR>f : α → β<VAR>l : β →₀ M<VAR>hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support<VAR>h : ∀ (a : α), f a ∉ l.support<VAR>a : β<VAR>ha : a ∈ l.support<VAR>b : α<VAR>hb : b ∈ f ⁻¹' ↑l.support ∧ f b = a<GOAL>False
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝¹ : Ring R<VAR>p q r : R[X]<VAR>S : Type u_1<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>n : ℤ<GOAL>eval₂ f (↑n) p = f (eval (↑n) p)
<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝¹ : Ring R<VAR>p q r : R[X]<VAR>S : Type u_1<VAR>inst✝ : Ring S<VAR>f : R →+* S<VAR>n : ℤ<GOAL>↑n = f ↑n
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : NonUnitalSemiring α<VAR>s✝ : Multiset α<VAR>a x : α<VAR>s : Multiset α<VAR>ih : (∀ x ∈ s, a ∣ x) → a ∣ s.sum<VAR>h : ∀ x_1 ∈ x ::ₘ s, a ∣ x_1<GOAL>a ∣ (x ::ₘ s).sum
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : NonUnitalSemiring α<VAR>s✝ : Multiset α<VAR>a x : α<VAR>s : Multiset α<VAR>ih : (∀ x ∈ s, a ∣ x) → a ∣ s.sum<VAR>h : ∀ x_1 ∈ x ::ₘ s, a ∣ x_1<GOAL>a ∣ x + s.sum
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>I B X : Set α<VAR>hB : autoParam (B ⊆ M.E) _auto✝<GOAL>M.Base B ↔ M✶.Base (M.E \ B)
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>T : L.Theory<VAR>inst✝ : N ⊨ L.completeTheory M<VAR>φ : L.Sentence<GOAL>N ⊨ φ ↔ M ⊨ φ
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>T : L.Theory<VAR>inst✝ : N ⊨ L.completeTheory M<VAR>φ : L.Sentence<VAR>h : N ⊨ φ<GOAL>M ⊨ φ
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>T : L.Theory<VAR>inst✝ : N ⊨ L.completeTheory M<VAR>φ : L.Sentence<VAR>h : ¬M ⊨ φ<GOAL>¬N ⊨ φ
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>T : L.Theory<VAR>inst✝ : N ⊨ L.completeTheory M<VAR>φ : L.Sentence<VAR>h : M ⊨ Formula.not φ<GOAL>N ⊨ Formula.not φ
<VAR>M : Type u_1<VAR>inst✝² : CommMonoidWithZero M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoidWithZero N<VAR>P : Type u_3<VAR>inst✝ : CommMonoidWithZero P<VAR>p : Type u_4<VAR>f : M → ↥S → p<VAR>H : ∀ {a c : M} {b d : ↥S}, (r S) (a, b) (c, d) → f a b = f c d<GOAL>liftOn 0 f H = f 0 1
<VAR>xl xr : Type u<VAR>xL : xl → PGame<VAR>xR : xr → PGame<VAR>j : (mk xl xr xL xR).RightMoves<GOAL>(xR j).Subsequent (mk xl xr xL xR)
<VAR>t : Type u → Type u<VAR>inst✝⁵ : Traversable t<VAR>inst✝⁴ : LawfulTraversable t<VAR>F G : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : LawfulApplicative F<VAR>inst✝¹ : Applicative G<VAR>inst✝ : LawfulApplicative G<VAR>α β γ : Type u<VAR>g : α → F β<VAR>h : β → G γ<VAR>f : β → γ<VAR>x✝ : t β<VAR>x : t (F (G α))<GOAL>sequence (Comp.mk <$> x) = Comp.mk (sequence <$> sequence x)
<VAR>t : Type u → Type u<VAR>inst✝⁵ : Traversable t<VAR>inst✝⁴ : LawfulTraversable t<VAR>F G : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : LawfulApplicative F<VAR>inst✝¹ : Applicative G<VAR>inst✝ : LawfulApplicative G<VAR>α β γ : Type u<VAR>g : α → F β<VAR>h : β → G γ<VAR>f : β → γ<VAR>x✝ : t β<VAR>x : t (F (G α))<GOAL>traverse Comp.mk x = Comp.mk (traverse id <$> traverse id x)
<VAR>t : Type u → Type u<VAR>inst✝⁵ : Traversable t<VAR>inst✝⁴ : LawfulTraversable t<VAR>F G : Type u → Type u<VAR>inst✝³ : Applicative F<VAR>inst✝² : LawfulApplicative F<VAR>inst✝¹ : Applicative G<VAR>inst✝ : LawfulApplicative G<VAR>α β γ : Type u<VAR>g : α → F β<VAR>h : β → G γ<VAR>f : β → γ<VAR>x✝ : t β<VAR>x : t (F (G α))<GOAL>traverse Comp.mk x = traverse (Comp.mk ∘ map id ∘ id) x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>s : Seq α<VAR>S : Seq (Seq1 α)<GOAL>(cons (a, s) S).join = cons a (s.append S.join)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a : α<VAR>s : Seq α<VAR>S : Seq (Seq1 α)<GOAL>IsBisimulation fun s1 s2 => s1 = s2 ∨ ∃ a s S, s1 = (cons (a, s) S).join ∧ s2 = cons a (s.append S.join)
<VAR>F : Type v'<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : StarRing R<VAR>inst✝¹⁴ : NonUnitalSemiring A<VAR>inst✝¹³ : StarRing A<VAR>inst✝¹² : Module R A<VAR>inst✝¹¹ : IsScalarTower R A A<VAR>inst✝¹⁰ : SMulCommClass R A A<VAR>inst✝⁹ : StarModule R A<VAR>inst✝⁸ : NonUnitalSemiring B<VAR>inst✝⁷ : StarRing B<VAR>inst✝⁶ : Module R B<VAR>inst✝⁵ : IsScalarTower R B B<VAR>inst✝⁴ : SMulCommClass R B B<VAR>inst✝³ : StarModule R B<VAR>inst✝² : FunLike F A B<VAR>inst✝¹ : NonUnitalAlgHomClass F R A B<VAR>inst✝ : NonUnitalStarAlgHomClass F R A B<VAR>s : Set A<VAR>p : (x : A) → x ∈ adjoin R s → Prop<VAR>a : A<VAR>ha : a ∈ adjoin R s<VAR>mem : ∀ (x : A) (hx : x ∈ s), p x ⋯<VAR>add : ∀ (x : A) (hx : x ∈ adjoin R s) (y : A) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x + y) ⋯<VAR>zero : p 0 ⋯<VAR>mul : ∀ (x : A) (hx : x ∈ adjoin R s) (y : A) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯<VAR>smul : ∀ (r : R) (x : A) (hx : x ∈ adjoin R s), p x hx → p (r • x) ⋯<VAR>star : ∀ (x : A) (hx : x ∈ adjoin R s), p x hx → p (Star.star x) ⋯<GOAL>p a ha
<VAR>F : Type v'<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : StarRing R<VAR>inst✝¹⁴ : NonUnitalSemiring A<VAR>inst✝¹³ : StarRing A<VAR>inst✝¹² : Module R A<VAR>inst✝¹¹ : IsScalarTower R A A<VAR>inst✝¹⁰ : SMulCommClass R A A<VAR>inst✝⁹ : StarModule R A<VAR>inst✝⁸ : NonUnitalSemiring B<VAR>inst✝⁷ : StarRing B<VAR>inst✝⁶ : Module R B<VAR>inst✝⁵ : IsScalarTower R B B<VAR>inst✝⁴ : SMulCommClass R B B<VAR>inst✝³ : StarModule R B<VAR>inst✝² : FunLike F A B<VAR>inst✝¹ : NonUnitalAlgHomClass F R A B<VAR>inst✝ : NonUnitalStarAlgHomClass F R A B<VAR>s : Set A<VAR>p : (x : A) → x ∈ adjoin R s → Prop<VAR>a : A<VAR>ha : a ∈ adjoin R s<VAR>mem : ∀ (x : A) (hx : x ∈ s), p x ⋯<VAR>add : ∀ (x : A) (hx : x ∈ adjoin R s) (y : A) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x + y) ⋯<VAR>zero : p 0 ⋯<VAR>mul : ∀ (x : A) (hx : x ∈ adjoin R s) (y : A) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯<VAR>smul : ∀ (r : R) (x : A) (hx : x ∈ adjoin R s), p x hx → p (r • x) ⋯<VAR>star : ∀ (x : A) (hx : x ∈ adjoin R s), p x hx → p (Star.star x) ⋯<VAR>x : A<VAR>hx : x ∈ s ∪ Star.star s<GOAL>p x ⋯
<VAR>F : Type v'<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : StarRing R<VAR>inst✝¹⁴ : NonUnitalSemiring A<VAR>inst✝¹³ : StarRing A<VAR>inst✝¹² : Module R A<VAR>inst✝¹¹ : IsScalarTower R A A<VAR>inst✝¹⁰ : SMulCommClass R A A<VAR>inst✝⁹ : StarModule R A<VAR>inst✝⁸ : NonUnitalSemiring B<VAR>inst✝⁷ : StarRing B<VAR>inst✝⁶ : Module R B<VAR>inst✝⁵ : IsScalarTower R B B<VAR>inst✝⁴ : SMulCommClass R B B<VAR>inst✝³ : StarModule R B<VAR>inst✝² : FunLike F A B<VAR>inst✝¹ : NonUnitalAlgHomClass F R A B<VAR>inst✝ : NonUnitalStarAlgHomClass F R A B<VAR>s : Set A<VAR>p : (x : A) → x ∈ adjoin R s → Prop<VAR>a : A<VAR>ha : a ∈ adjoin R s<VAR>mem : ∀ (x : A) (hx : x ∈ s), p x ⋯<VAR>add : ∀ (x : A) (hx : x ∈ adjoin R s) (y : A) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x + y) ⋯<VAR>zero : p 0 ⋯<VAR>mul : ∀ (x : A) (hx : x ∈ adjoin R s) (y : A) (hy : y ∈ adjoin R s), p x hx → p y hy → p (x * y) ⋯<VAR>smul : ∀ (r : R) (x : A) (hx : x ∈ adjoin R s), p x hx → p (r • x) ⋯<VAR>star : ∀ (x : A) (hx : x ∈ adjoin R s), p x hx → p (Star.star x) ⋯<VAR>x : A<VAR>hx✝ : x ∈ s ∪ Star.star s<VAR>hx : x ∈ s ∨ Star.star x ∈ s<GOAL>p x ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteLattice α<VAR>u : ℕ → α<GOAL>⨅ i, ⨅ (_ : True), sSup (u '' Ici i) = ⨅ n, ⨆ i, ⨆ (_ : i ≥ n), u i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteLattice α<VAR>u : ℕ → α<GOAL>⨅ i, ⨆ a ∈ Ici i, u a = ⨅ n, ⨆ i, ⨆ (_ : i ≥ n), u i
<VAR>f : C(↑I, ℝ)<VAR>ε : ℝ<VAR>h : 0 < ε<VAR>n : ℕ<VAR>x : ↑I<VAR>k : Fin (n + 1)<VAR>m : k ∈ (S f ε h n x)ᶜ<GOAL>1 ≤ δ f ε h ^ (-2) * (↑x - ↑k/ₙ) ^ 2
<VAR>f : C(↑I, ℝ)<VAR>ε : ℝ<VAR>h : 0 < ε<VAR>n : ℕ<VAR>x : ↑I<VAR>k : Fin (n + 1)<VAR>m : δ f ε h ≤ dist k/ₙ x<GOAL>1 ≤ δ f ε h ^ (-2) * (↑x - ↑k/ₙ) ^ 2
<VAR>f : C(↑I, ℝ)<VAR>ε : ℝ<VAR>h : 0 < ε<VAR>n : ℕ<VAR>x : ↑I<VAR>k : Fin (n + 1)<VAR>m : δ f ε h ≤ dist k/ₙ x<GOAL>δ f ε h ≤ |↑x - ↑k/ₙ|
<VAR>α : Type u<VAR>inst✝ : Ring α<VAR>x : α<VAR>n : ℕ<GOAL>op ((1 - x) * ∑ i ∈ range n, x ^ i) = op (1 - x ^ n)
<VAR>K : Type u_1<VAR>v : K<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>n : ℕ<GOAL>(of v).convs (n + 1) = ↑⌊v⌋ + 1 / (of (Int.fract v)⁻¹).convs n
<VAR>α : Type u_1<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>X : Type u_2<VAR>inst✝ : PseudoEMetricSpace X<VAR>δ : ℝ<VAR>δ_pos : 0 < δ<VAR>F : Set X<VAR>x : X<VAR>hxF : x ∈ closure F<GOAL>1 ≤ (thickenedIndicator δ_pos F) x
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>H : G.Subgraph<VAR>h : H.Connected<GOAL>H.verts.Nonempty
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>H : G.Subgraph<VAR>h : H.Preconnected ∧ H.verts.Nonempty<GOAL>H.verts.Nonempty
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝¹² : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝¹¹ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝¹⁰ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>E : Type u_9<VAR>inst✝⁷ : AddCommMonoid E<VAR>inst✝⁶ : Module R E<VAR>F : Type u_10<VAR>inst✝⁵ : AddCommMonoid F<VAR>t : ι → Type u_11<VAR>t' : ι → Type u_12<VAR>inst✝⁴ : (i : ι) → AddCommMonoid (t i)<VAR>inst✝³ : (i : ι) → Module R (t i)<VAR>inst✝² : (i : ι) → AddCommMonoid (t' i)<VAR>inst✝¹ : (i : ι) → Module R (t' i)<VAR>g : (i : ι) → t i →ₗ[R] t' i<VAR>f : (i : ι) → s i →ₗ[R] t i<VAR>inst✝ : DecidableEq ι<VAR>i : ι<VAR>c : R<VAR>u : s i →ₗ[R] t i<VAR>x : (i : ι) → s i<GOAL>((map (update f i (c • u))).compMultilinearMap (tprod R)) x = ((c • map (update f i u)).compMultilinearMap (tprod R)) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>Measurable fun μ => ∫⁻ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<GOAL>Measurable fun μ => ⨆ n, ∑ x ∈ (SimpleFunc.eapprox f n).range, x * μ (↑(SimpleFunc.eapprox f n) ⁻¹' {x})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>n : ℕ<VAR>i : ℝ≥0∞<VAR>x✝ : i ∈ (SimpleFunc.eapprox f n).range<GOAL>Measurable fun μ => i * μ (↑(SimpleFunc.eapprox f n) ⁻¹' {i})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>n : ℕ<VAR>i : ℝ≥0∞<VAR>x✝ : i ∈ (SimpleFunc.eapprox f n).range<GOAL>Measurable fun μ => μ (↑(SimpleFunc.eapprox f n) ⁻¹' {i})
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝⁵ : Category.{v, u'} D<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : HasFiniteProducts D<VAR>F : C ⥤ D<VAR>L : D ⥤ C<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : CartesianClosed D<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>h : L ⊣ F<VAR>A : C<VAR>i : IsIso (expComparison F A)<GOAL>IsIso (frobeniusMorphism F h A)
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝⁵ : Category.{v, u'} D<VAR>inst✝⁴ : HasFiniteProducts C<VAR>inst✝³ : HasFiniteProducts D<VAR>F : C ⥤ D<VAR>L : D ⥤ C<VAR>inst✝² : CartesianClosed C<VAR>inst✝¹ : CartesianClosed D<VAR>inst✝ : PreservesLimitsOfShape (Discrete WalkingPair) F<VAR>h : L ⊣ F<VAR>A : C<VAR>i : IsIso ((conjugateEquiv (h.comp (exp.adjunction A)) ((exp.adjunction (F.obj A)).comp h)) (frobeniusMorphism F h A))<GOAL>IsIso (frobeniusMorphism F h A)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>a : ℤ<GOAL>↑p ^ padicValInt p a ∣ a
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>a : ℤ<GOAL>a = 0 ∨ padicValInt p a ≤ padicValInt p a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>l : Filter α<VAR>p : ℕ → Prop<GOAL>(∃ᶠ (n : ℕ) in atTop, p n) ↔ {n | p n}.Infinite
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s t u : Finset α<VAR>P : Finpartition s<VAR>a : α<VAR>ht : t ∈ P.parts<VAR>hat : a ∈ t<GOAL>P.part a = t
<VAR>E : Type u_1<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℂ E<GOAL>Cardinal.lift.{?u.4805, u_1} (Module.rank ℝ E) = Cardinal.lift.{?u.4805, u_1} (2 * Module.rank ℂ E)