ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>x y z : S<GOAL>(z𝖣x + y) = (z𝖣x) + z𝖣y
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>x y z : S<GOAL>single x z + single y z - single (x + y) z ∈ kerTotal R S
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>x y z : S<GOAL>z • (single x 1 + single y 1 - single (x + y) 1) ∈ kerTotal R S
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>f : α → β<VAR>g : β → γ<VAR>a : Filter α<VAR>b : Filter β<VAR>c : Filter γ<VAR>hfg : Tendsto (g ∘ f) a c<VAR>hg : comap g c ≤ b<GOAL>Tendsto f a b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>f : α → β<VAR>g : β → γ<VAR>a : Filter α<VAR>b : Filter β<VAR>c : Filter γ<VAR>hfg : a ≤ comap (g ∘ f) c<VAR>hg : comap g c ≤ b<GOAL>a ≤ comap f b
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>θ : Real.Angle<GOAL>↑(LinearEquiv.det (o.rotation θ).toLinearEquiv) = ↑1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β<VAR>s : (i : ι) → κ i → Set β<GOAL>f ⁻¹' ⋃ i, ⋃ j, s i j = ⋃ i, ⋃ j, f ⁻¹' s i j
<VAR>α : Type u_1<VAR>inst✝¹ : CompleteLattice α<VAR>β : Type u_2<VAR>inst✝ : CompleteLattice β<VAR>f : α ≃o β<GOAL>f (⨅ a ∈ {H | IsCoatom H}, a) = ⨅ a ∈ {H | IsCoatom H}, a
<VAR>α : Type u_1<VAR>inst✝¹ : CompleteLattice α<VAR>β : Type u_2<VAR>inst✝ : CompleteLattice β<VAR>f : α ≃o β<GOAL>⨅ i ∈ {H | IsCoatom H}, f i = ⨅ a ∈ {H | IsCoatom H}, a
<VAR>α : Type u_1<VAR>inst✝¹ : CompleteLattice α<VAR>β : Type u_2<VAR>inst✝ : CompleteLattice β<VAR>f : α ≃o β<GOAL>α ≃ β
<VAR>α : Type u_1<VAR>inst✝¹ : CompleteLattice α<VAR>β : Type u_2<VAR>inst✝ : CompleteLattice β<VAR>f : α ≃o β<GOAL>∀ (x : α), ⨅ (_ : ?e x ∈ {H | IsCoatom H}), ?e x = ⨅ (_ : x ∈ {H | IsCoatom H}), f x
<VAR>G : Type u_1<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝³ : SFinite ν<VAR>inst✝² : SFinite μ<VAR>s : Set G<VAR>inst✝¹ : MeasurableInv G<VAR>inst✝ : μ.IsMulRightInvariant<GOAL>QuasiMeasurePreserving (fun p => p.1 / p.2) (μ.prod ν) μ
<VAR>G : Type u_1<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝³ : SFinite ν<VAR>inst✝² : SFinite μ<VAR>s : Set G<VAR>inst✝¹ : MeasurableInv G<VAR>inst✝ : μ.IsMulRightInvariant<VAR>y : G<GOAL>QuasiMeasurePreserving (fun x => (x, y).1 / (x, y).2) μ μ
<VAR>R : Type uR<VAR>M : Type uM<VAR>K : Type uK<VAR>V : Type uV<VAR>ι : Type uι<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : DecidableEq ι<VAR>b : Basis ι R M<VAR>inst✝ : _root_.Finite ι<VAR>l : Dual R M<VAR>i : ι<GOAL>(b.dualBasis.repr l) i = l (b i)
<VAR>G : PGame<VAR>inst✝ : G.Impartial<VAR>H : PGame<GOAL>G ≈ H ↔ G + H ≈ 0
<VAR>G : PGame<VAR>inst✝ : G.Impartial<VAR>H : PGame<GOAL>0 = ⟦G + H⟧ ↔ ⟦G + H⟧ = ⟦0⟧
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝² : Fintype m<VAR>inst✝¹ : Fintype n<VAR>inst✝ : NonUnitalSemiring α<VAR>u : m → α<VAR>w : n → α<VAR>v : Matrix m n α<GOAL>(fun j => u ⬝ᵥ fun i => v i j) ⬝ᵥ w = u ⬝ᵥ fun i => v i ⬝ᵥ w
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>s : Set α<VAR>inst✝ : NoMinOrder α<VAR>a b x : α<GOAL>Ico a b ∈ 𝓝 x ↔ x ∈ Ioo a b
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>V1 : Type u_3<VAR>P1 : Type u_4<VAR>V2 : Type u_5<VAR>P2 : Type u_6<VAR>V3 : Type u_7<VAR>P3 : Type u_8<VAR>inst✝⁵ : CommRing k<VAR>inst✝⁴ : AddCommGroup V1<VAR>inst✝³ : AffineSpace V1 P1<VAR>inst✝² : AddCommGroup V2<VAR>inst✝¹ : Module k V1<VAR>inst✝ : Module k V2<VAR>c : P1<VAR>r₁ r₂ : k<VAR>p : P1<GOAL>(homothety c (r₁ * r₂)) p = (homothety c r₁) ((homothety c r₂) p)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>‖y‖ / (o.oangle (x + y) y).cos = ‖x + y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (-o).oangle y x = ↑(π / 2)<GOAL>‖y‖ / ((-o).oangle y (x + y)).cos = ‖x + y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (-o).oangle y x = ↑(π / 2)<GOAL>‖y‖ / ((-o).oangle y (y + x)).cos = ‖y + x‖
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>a b : α<VAR>h : b ≤ a<GOAL>variationOnFromTo f s a b ≤ 0
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>a b : α<VAR>h : b ≤ a<GOAL>-variationOnFromTo f s b a ≤ 0
<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) (0 * φ) = (coeff R n) 0
<VAR>α : Type u<VAR>β : Type v<VAR>K : Type u<VAR>inst✝ : DivisionSemiring K<VAR>I : Ideal K<GOAL>I = ⊥ ∨ I = ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>K : Type u<VAR>inst✝ : DivisionSemiring K<VAR>I : Ideal K<GOAL>¬I = ⊤ → I = ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>K : Type u<VAR>inst✝ : DivisionSemiring K<VAR>I : Ideal K<GOAL>I ≠ ⊤ → I = ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>K : Type u<VAR>inst✝ : DivisionSemiring K<VAR>I : Ideal K<GOAL>1 ∉ I → I = ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>K : Type u<VAR>inst✝ : DivisionSemiring K<VAR>I : Ideal K<VAR>h1 : 1 ∉ I<GOAL>I = ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>K : Type u<VAR>inst✝ : DivisionSemiring K<VAR>I : Ideal K<VAR>h1 : 1 ∉ I<GOAL>I ≤ ⊥
<VAR>α : Type u<VAR>β : Type v<VAR>K : Type u<VAR>inst✝ : DivisionSemiring K<VAR>I : Ideal K<VAR>h1 : 1 ∉ I<VAR>r : K<VAR>hr : r ∈ I<VAR>H : ¬r = 0<GOAL>r ∈ ⊥
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>inst✝ : CommRing R<VAR>c₁ c₂ r x y z : R<VAR>a b c : ℍ[R,c₁,c₂]<GOAL>star a + a = 2 * ↑a.re
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>inst✝⁷ : Category.{u_7, u_1} C<VAR>inst✝⁶ : Category.{u_6, u_2} D<VAR>inst✝⁵ : Category.{?u.58445, u_3} E<VAR>inst✝⁴ : Category.{?u.58449, u_4} E'<VAR>A : Type u_5<VAR>inst✝³ : AddMonoid A<VAR>inst✝² : HasShift D A<VAR>inst✝¹ : HasShift E A<VAR>inst✝ : HasShift E' A<VAR>F G H : SingleFunctors C D A<VAR>e : F ≅ G<VAR>n : A<VAR>X : C<GOAL>(e.inv.hom n).app X ≫ (e.hom.hom n).app X = 𝟙 ((G.functor n).obj X)
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>P : Sylow p G<GOAL>Nat.card ↥↑P = p ^ (Nat.card G).factorization p
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>P : Sylow p G<VAR>n : ℕ<VAR>heq : Nat.card ↥↑P = p ^ n<GOAL>Nat.card ↥↑P = p ^ (Nat.card G).factorization p
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>P : Sylow p G<VAR>n : ℕ<VAR>heq : Nat.card ↥↑P = p ^ n<GOAL>Nat.card ↥↑P ∣ p ^ (Nat.card G).factorization p
<VAR>G : Type u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝¹ : Group G<VAR>inst✝ : Finite G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>P : Sylow p G<VAR>n : ℕ<VAR>heq : Nat.card ↥↑P = p ^ n<GOAL>Nat.card ↥↑P ∣ Nat.card G
<VAR>𝕜✝ : Type u_1<VAR>𝕜' : Type u_2<VAR>E✝ : Type u_3<VAR>E' : Type u_4<VAR>F : Type u_5<VAR>ι✝ : Type u_6<VAR>𝕜 : Type u_7<VAR>ι : Type u_8<VAR>E : ι → Type u_9<VAR>inst✝³ : NormedDivisionRing 𝕜<VAR>inst✝² : (i : ι) → AddCommGroup (E i)<VAR>inst✝¹ : (i : ι) → Module 𝕜 (E i)<VAR>inst✝ : (i : ι) → TopologicalSpace (E i)<VAR>S : Set ((i : ι) → E i)<GOAL>IsVonNBounded 𝕜 S ↔ ∀ (i : ι), IsVonNBounded 𝕜 (eval i '' S)
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hμν : μ ≪ ν<GOAL>-llr μ ν =ᶠ[ae μ] llr ν μ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hμν : μ ≪ ν<VAR>x : α<VAR>hx : (μ.rnDeriv ν)⁻¹ x = ν.rnDeriv μ x<GOAL>(-llr μ ν) x = llr ν μ x
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ<VAR>inst✝¹ : SigmaFinite μ<VAR>inst✝ : SigmaFinite ν<VAR>hμν : μ ≪ ν<VAR>x : α<VAR>hx : (μ.rnDeriv ν)⁻¹ x = ν.rnDeriv μ x<GOAL>log (μ.rnDeriv ν x)⁻¹.toReal = log (ν.rnDeriv μ x).toReal
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NontriviallyNormedField 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝕜'<VAR>x : 𝕜<VAR>n : ℤ<GOAL>logDeriv (fun x => x ^ n) x = ↑n / x
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : SFinite μ<VAR>f : α × β → E<VAR>h1f : AEStronglyMeasurable f (μ.prod ν)<GOAL>Integrable f (μ.prod ν) ↔ (∀ᵐ (y : β) ∂ν, Integrable (fun x => f (x, y)) μ) ∧ Integrable (fun y => ∫ (x : α), ‖f (x, y)‖ ∂μ) ν
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝⁷ : MeasurableSpace α<VAR>inst✝⁶ : MeasurableSpace α'<VAR>inst✝⁵ : MeasurableSpace β<VAR>inst✝⁴ : MeasurableSpace β'<VAR>inst✝³ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : SFinite ν<VAR>inst✝ : SFinite μ<VAR>f : α × β → E<VAR>h1f : AEStronglyMeasurable f (μ.prod ν)<GOAL>Integrable f (μ.prod ν) ↔ Integrable (fun z => f z.swap) (ν.prod μ)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝² : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝¹ : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>inst✝ : ∀ (i : ι), SigmaFinite (μ i)<VAR>i : ι<VAR>s : Set (α i)<VAR>hs : (μ i) s = 0<GOAL>(Measure.pi μ) (eval i ⁻¹' s) = 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝² : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝¹ : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>inst✝ : ∀ (i : ι), SigmaFinite (μ i)<VAR>i : ι<VAR>s : Set (α i)<VAR>hs : (μ i) s = 0<VAR>t : Set (α i)<VAR>hst : s ⊆ t<VAR>left✝ : MeasurableSet t<VAR>hμt : (μ i) t = 0<GOAL>(Measure.pi μ) (eval i ⁻¹' s) = 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝² : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝¹ : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>inst✝ : ∀ (i : ι), SigmaFinite (μ i)<VAR>i : ι<VAR>s : Set (α i)<VAR>hs : (μ i) s = 0<VAR>t : Set (α i)<VAR>hst : s ⊆ t<VAR>left✝ : MeasurableSet t<VAR>hμt : (μ i) t = 0<GOAL>(Measure.pi μ) (eval i ⁻¹' t) = 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝² : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝¹ : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>inst✝ : ∀ (i : ι), SigmaFinite (μ i)<VAR>i : ι<VAR>s : Set (α i)<VAR>hs : (μ i) s = 0<VAR>t : Set (α i)<VAR>hst : s ⊆ t<VAR>left✝ : MeasurableSet t<VAR>hμt : (μ i) t = 0<GOAL>∏ i_1 : ι, (μ i_1) (update (fun j => univ) i t i_1) = 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝² : Fintype ι<VAR>m : (i : ι) → OuterMeasure (α i)<VAR>inst✝¹ : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>inst✝ : ∀ (i : ι), SigmaFinite (μ i)<VAR>i : ι<VAR>s : Set (α i)<VAR>hs : (μ i) s = 0<VAR>t : Set (α i)<VAR>hst : s ⊆ t<VAR>left✝ : MeasurableSet t<VAR>hμt : (μ i) t = 0<GOAL>(μ i) (update (fun j => univ) i t i) = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝ : MetricSpace P<VAR>p : P<GOAL>Cospherical {p}
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝ : MetricSpace P<VAR>p : P<GOAL>∃ radius, ∀ p_1 ∈ {p}, dist p_1 p = radius
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>F : Type u_3<VAR>E : ι → Type u_4<VAR>inst✝⁷ : NormedField 𝕜<VAR>inst✝⁶ : (i : ι) → AddCommGroup (E i)<VAR>inst✝⁵ : (i : ι) → Module 𝕜 (E i)<VAR>inst✝⁴ : (i : ι) → TopologicalSpace (E i)<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜 F<VAR>inst✝¹ : TopologicalSpace F<VAR>inst✝ : ContinuousSMul 𝕜 F<VAR>s : Set ((i : ι) → E i)<VAR>hs : IsVonNBounded 𝕜 s<VAR>f : ContinuousMultilinearMap 𝕜 E F<GOAL>IsVonNBounded 𝕜 (⇑f '' s)
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝¹ : L.Structure M<VAR>N : Type u_2<VAR>inst✝ : L.Structure N<VAR>f : M ↪[L] N<VAR>s : L.Substructure M<VAR>t : Set N<VAR>h1 : t.Countable<VAR>h2 : (closure L).toFun t = Substructure.map f.toHom s<GOAL>s.CG
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝¹ : L.Structure M<VAR>N : Type u_2<VAR>inst✝ : L.Structure N<VAR>f : M ↪[L] N<VAR>s : L.Substructure M<VAR>t : Set N<VAR>h1 : t.Countable<VAR>h2 : (closure L).toFun t = Substructure.map f.toHom s<GOAL>∃ S, S.Countable ∧ (closure L).toFun S = s
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝¹ : L.Structure M<VAR>N : Type u_2<VAR>inst✝ : L.Structure N<VAR>f : M ↪[L] N<VAR>s : L.Substructure M<VAR>t : Set N<VAR>h1 : t.Countable<VAR>h2 : (closure L).toFun t = Substructure.map f.toHom s<GOAL>(closure L).toFun (⇑f ⁻¹' t) = s
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝¹ : L.Structure M<VAR>N : Type u_2<VAR>inst✝ : L.Structure N<VAR>f : M ↪[L] N<VAR>s : L.Substructure M<VAR>t : Set N<VAR>h1 : t.Countable<VAR>h2 : (closure L).toFun t = Substructure.map f.toHom s<VAR>hf : Function.Injective ⇑f.toHom<GOAL>(closure L).toFun (⇑f ⁻¹' t) = s
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝¹ : L.Structure M<VAR>N : Type u_2<VAR>inst✝ : L.Structure N<VAR>f : M ↪[L] N<VAR>s : L.Substructure M<VAR>t : Set N<VAR>h1 : t.Countable<VAR>h2 : (closure L).toFun t = Substructure.map f.toHom s<VAR>hf : Function.Injective ⇑f.toHom<GOAL>Substructure.map f.toHom ((closure L).toFun (⇑f ⁻¹' t)) = Substructure.map f.toHom s
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝¹ : L.Structure M<VAR>N : Type u_2<VAR>inst✝ : L.Structure N<VAR>f : M ↪[L] N<VAR>s : L.Substructure M<VAR>t : Set N<VAR>h1 : t.Countable<VAR>h2 : (closure L).toFun t = Substructure.map f.toHom s<VAR>hf : Function.Injective ⇑f.toHom<GOAL>t ⊆ range ⇑f
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝¹ : L.Structure M<VAR>N : Type u_2<VAR>inst✝ : L.Structure N<VAR>f : M ↪[L] N<VAR>s : L.Substructure M<VAR>t : Set N<VAR>h1 : t.Countable<VAR>h2 : (closure L).toFun t = Substructure.map f.toHom s<VAR>hf : Function.Injective ⇑f.toHom<VAR>x : N<VAR>hx : x ∈ t<GOAL>x ∈ range ⇑f
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝¹ : L.Structure M<VAR>N : Type u_2<VAR>inst✝ : L.Structure N<VAR>f : M ↪[L] N<VAR>s : L.Substructure M<VAR>t : Set N<VAR>h1 : t.Countable<VAR>h2 : (closure L).toFun t = Substructure.map f.toHom s<VAR>hf : Function.Injective ⇑f.toHom<VAR>x : N<VAR>hx : x ∈ t<VAR>h' : x ∈ ↑((closure L).toFun t)<GOAL>x ∈ range ⇑f
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝¹ : L.Structure M<VAR>N : Type u_2<VAR>inst✝ : L.Structure N<VAR>f : M ↪[L] N<VAR>s : L.Substructure M<VAR>t : Set N<VAR>h1 : t.Countable<VAR>h2 : (closure L).toFun t = Substructure.map f.toHom s<VAR>hf : Function.Injective ⇑f.toHom<VAR>x : N<VAR>hx : x ∈ t<VAR>h' : x ∈ ↑(Substructure.map f.toHom s)<GOAL>x ∈ range ⇑f
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y : C<VAR>f : J → (X ⟶ Y)<VAR>inst✝ : Nonempty J<VAR>s : Cotrident f<VAR>W : C<VAR>k l : s.pt ⟶ W<VAR>h : s.π ≫ k = s.π ≫ l<GOAL>s.ι.app zero ≫ k = s.ι.app zero ≫ l
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>α : ι → Type u_6<VAR>inst✝² : (i : ι) → LinearOrder (α i)<VAR>inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1<VAR>inst✝ : Finite ι<VAR>s : Set ((i : ι) → α i)<GOAL>s.IsPWO
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>α : ι → Type u_6<VAR>inst✝² : (i : ι) → LinearOrder (α i)<VAR>inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1<VAR>inst✝ : Finite ι<VAR>s : Set ((i : ι) → α i)<VAR>val✝ : Fintype ι<GOAL>s.IsPWO
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>α : ι → Type u_6<VAR>inst✝² : (i : ι) → LinearOrder (α i)<VAR>inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1<VAR>inst✝ : Finite ι<VAR>s : Set ((i : ι) → α i)<VAR>val✝ : Fintype ι<GOAL>∀ (s : Finset ι) (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ x ∈ s, (f ∘ ⇑g) a x ≤ (f ∘ ⇑g) b x
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>α : ι → Type u_6<VAR>inst✝² : (i : ι) → LinearOrder (α i)<VAR>inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1<VAR>inst✝ : Finite ι<VAR>s : Set ((i : ι) → α i)<VAR>val✝ : Fintype ι<GOAL>∀ (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ x ∈ ∅, (f ∘ ⇑g) a x ≤ (f ∘ ⇑g) b x
<VAR>ι : Type u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>π : ι → Type u_5<VAR>α : ι → Type u_6<VAR>inst✝² : (i : ι) → LinearOrder (α i)<VAR>inst✝¹ : ∀ (i : ι), IsWellOrder (α i) fun x x_1 => x < x_1<VAR>inst✝ : Finite ι<VAR>s : Set ((i : ι) → α i)<VAR>val✝ : Fintype ι<GOAL>∀ (a : ι) (s : Finset ι) (h : a ∉ s), (∀ (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ x ∈ s, (f ∘ ⇑g) a x ≤ (f ∘ ⇑g) b x) → ∀ (f : ℕ → (s : ι) → α s), ∃ g, ∀ ⦃a_2 b : ℕ⦄, a_2 ≤ b → ∀ x ∈ Finset.cons a s h, (f ∘ ⇑g) a_2 x ≤ (f ∘ ⇑g) b x
<VAR>C : Type (u + 1)<VAR>inst✝⁵ : Category.{u_1, u + 1} C<VAR>inst✝⁴ : ConcreteCategory C<VAR>D : Type (u + 1)<VAR>inst✝³ : Category.{u_2, u + 1} D<VAR>inst✝² : ConcreteCategory D<VAR>inst✝¹ : HasForget₂ C D<VAR>inst✝ : (forget C).ReflectsIsomorphisms<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>i : IsIso ((forget₂ C D).map f)<VAR>i' : IsIso ((forget D).map ((forget₂ C D).map f))<GOAL>IsIso f
<VAR>C : Type (u + 1)<VAR>inst✝⁵ : Category.{u_1, u + 1} C<VAR>inst✝⁴ : ConcreteCategory C<VAR>D : Type (u + 1)<VAR>inst✝³ : Category.{u_2, u + 1} D<VAR>inst✝² : ConcreteCategory D<VAR>inst✝¹ : HasForget₂ C D<VAR>inst✝ : (forget C).ReflectsIsomorphisms<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>i : IsIso ((forget₂ C D).map f)<VAR>i' : IsIso ((forget D).map ((forget₂ C D).map f))<VAR>this : IsIso ((forget C).map f)<GOAL>IsIso f
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>s : Set α<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>hs : MeasurableSet s<GOAL>MeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Icc (f p.1) (g p.1)}
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>f g : α → ℝ<VAR>s : Set α<VAR>hf : Measurable f<VAR>hg : Measurable g<VAR>hs : MeasurableSet s<GOAL>MeasurableSet ({a | a.1 ∈ s} ∩ {a | a.2 ∈ {a_1 | f a.1 ≤ a_1} ∩ {a_1 | a_1 ≤ g a.1}})
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>inst✝¹ : HasZeroObject C<VAR>ι : Type u_1<VAR>inst✝ : DecidableEq ι<VAR>c : ComplexShape ι<VAR>j : ι<VAR>A : C<GOAL>(singleObjHomologySelfIso c j A).inv ≫ ((single C c j).obj A).homologyι j = (singleObjOpcyclesSelfIso c j A).hom
<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✝ : AddZeroClass M<VAR>a : α<VAR>f : α →₀ M<GOAL>erase a f + single a (f a) = f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>σ : Type u_4<VAR>inst✝³ : Primcodable α<VAR>inst✝² : Primcodable β<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Primcodable σ<VAR>f : β →. σ<VAR>g : α → β<VAR>hf : Partrec f<VAR>hg : Computable g<VAR>n : ℕ<GOAL>(((↑(decode n)).bind fun a => Part.some (encode (g a))).bind fun n => (↑(decode n)).bind fun a => Part.map encode (f a)) = (↑(decode n)).bind fun a => Part.map encode (f (g a))
<VAR>x y : ℝ<GOAL>cosh x - sinh x = rexp (-x)
<VAR>x y : ℝ<GOAL>↑(cosh x - sinh x) = ↑(rexp (-x))
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁹ : CommRing A<VAR>inst✝¹⁸ : Field K<VAR>inst✝¹⁷ : CommRing B<VAR>inst✝¹⁶ : Field L<VAR>inst✝¹⁵ : Algebra A K<VAR>inst✝¹⁴ : Algebra B L<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : Algebra K L<VAR>inst✝¹¹ : Algebra A L<VAR>inst✝¹⁰ : IsScalarTower A K L<VAR>inst✝⁹ : IsScalarTower A B L<VAR>inst✝⁸ : IsDomain A<VAR>inst✝⁷ : IsFractionRing A K<VAR>inst✝⁶ : IsIntegralClosure B A L<VAR>inst✝⁵ : IsFractionRing B L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsIntegrallyClosed A<VAR>inst✝¹ : IsDedekindDomain B<VAR>inst✝ : NoZeroSMulDivisors A B<GOAL>↑(differentIdeal A B) = (FractionalIdeal.dual A K 1)⁻¹
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u<VAR>B : Type u_3<VAR>inst✝¹⁹ : CommRing A<VAR>inst✝¹⁸ : Field K<VAR>inst✝¹⁷ : CommRing B<VAR>inst✝¹⁶ : Field L<VAR>inst✝¹⁵ : Algebra A K<VAR>inst✝¹⁴ : Algebra B L<VAR>inst✝¹³ : Algebra A B<VAR>inst✝¹² : Algebra K L<VAR>inst✝¹¹ : Algebra A L<VAR>inst✝¹⁰ : IsScalarTower A K L<VAR>inst✝⁹ : IsScalarTower A B L<VAR>inst✝⁸ : IsDomain A<VAR>inst✝⁷ : IsFractionRing A K<VAR>inst✝⁶ : IsIntegralClosure B A L<VAR>inst✝⁵ : IsFractionRing B L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>inst✝³ : Algebra.IsSeparable K L<VAR>inst✝² : IsIntegrallyClosed A<VAR>inst✝¹ : IsDedekindDomain B<VAR>inst✝ : NoZeroSMulDivisors A B<GOAL>(fun I => ↑I) ↑(differentIdeal A B) = (fun I => ↑I) (FractionalIdeal.dual A K 1)⁻¹
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>H✝ : LieSubalgebra R L<VAR>inst✝⁶ : IsNilpotent R ↥H✝<VAR>M : Type u_3<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>H : LieSubalgebra R L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsNoetherian R L<GOAL>rootSpace H 0 = H.toLieSubmodule
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : Monoid R<VAR>inst✝² : AddMonoid M<VAR>inst✝¹ : DistribMulAction R M<VAR>inst✝ : DistribMulAction Rᵐᵒᵖ M<VAR>r₁ r₂ : R<GOAL>0 = r₁ •> 0 + 0 <• r₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f g : C(α, β)<VAR>ι : Type u_5<VAR>S : ι → Set α<VAR>φ : (i : ι) → C(↑(S i), β)<VAR>hφ : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), (φ i) ⟨x, hxi⟩ = (φ j) ⟨x, hxj⟩<VAR>hS : ∀ (x : α), ∃ i, S i ∈ 𝓝 x<VAR>i : ι<VAR>x : ↑(S i)<GOAL>(liftCover S φ hφ hS) ↑x = (φ i) x
<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✝² : IsDedekindDomain A<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>x : A<VAR>n : ℕ<VAR>I : Ideal A<GOAL>Associates.mk I ^ n ≤ Associates.mk (span {x}) ↔ x ∈ I ^ n
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a : α<VAR>l l' : List α<VAR>h : l' ≤ l<GOAL>a :: l' ≤ a :: l
<VAR>α : Type u<VAR>inst✝ : LinearOrder α<VAR>a : α<VAR>l l' : List α<VAR>h : l' < l ∨ l' = l<GOAL>a :: l' < a :: l ∨ a :: l' = a :: l
<VAR>a b c d m n✝ k : ℕ<VAR>p q : ℕ → Prop<VAR>n : ℕ<GOAL>n < n.sqrt.succ ^ 2