ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>r r₁ r₂ : ℝ≥0<VAR>x y : ℝ<VAR>ι : Sort u_1<VAR>ι' : Sort u_2<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Nonempty ι'<VAR>f : ι → ℝ≥0<VAR>g : ι' → ℝ≥0<VAR>a : ℝ≥0<VAR>h : ∀ (i : ι) (j : ι'), a ≤ f i + g j<GOAL>a ≤ (⨅ i, f i) + ⨅ j, g j
<VAR>r r₁ r₂ : ℝ≥0<VAR>x y : ℝ<VAR>ι : Sort u_1<VAR>ι' : Sort u_2<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : Nonempty ι'<VAR>f : ι → ℝ≥0<VAR>g : ι' → ℝ≥0<VAR>a : ℝ≥0<VAR>h : ∀ (i : ι) (j : ι'), a ≤ f i + g j<GOAL>↑a ≤ (⨅ i, ↑(f i)) + ⨅ i, ↑(g i)
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>h : x ≤ y ∧ Disjoint x z<GOAL>x ≤ y \ z
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>h : x ≤ y ∧ Disjoint x z<GOAL>x \ z ≤ y \ z
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module R E<VAR>inst✝⁷ : Module R F<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : ContinuousAdd E<VAR>inst✝³ : ContinuousAdd F<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : ContinuousSMul R E<VAR>inst✝ : ContinuousSMul R F<VAR>f : E →ₗ.[R] F<GOAL>f.closure.HasCore f.domain
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module R E<VAR>inst✝⁷ : Module R F<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : ContinuousAdd E<VAR>inst✝³ : ContinuousAdd F<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : ContinuousSMul R E<VAR>inst✝ : ContinuousSMul R F<VAR>f : E →ₗ.[R] F<GOAL>(f.closure.domRestrict f.domain).closure = f.closure
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module R E<VAR>inst✝⁷ : Module R F<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : ContinuousAdd E<VAR>inst✝³ : ContinuousAdd F<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : ContinuousSMul R E<VAR>inst✝ : ContinuousSMul R F<VAR>f : E →ₗ.[R] F<VAR>x : ↥(f.closure.domRestrict f.domain).domain<VAR>y : ↥f.domain<VAR>hxy : ↑x = ↑y<GOAL>↑(f.closure.domRestrict f.domain) x = ↑f y
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module R E<VAR>inst✝⁷ : Module R F<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : ContinuousAdd E<VAR>inst✝³ : ContinuousAdd F<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : ContinuousSMul R E<VAR>inst✝ : ContinuousSMul R F<VAR>f : E →ₗ.[R] F<VAR>x : ↥(f.closure.domRestrict f.domain).domain<VAR>y : ↥f.domain<VAR>hxy : ↑x = ↑y<VAR>z : ↥f.closure.domain := ⟨↑y, ⋯⟩<GOAL>↑(f.closure.domRestrict f.domain) x = ↑f y
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module R E<VAR>inst✝⁷ : Module R F<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : ContinuousAdd E<VAR>inst✝³ : ContinuousAdd F<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : ContinuousSMul R E<VAR>inst✝ : ContinuousSMul R F<VAR>f : E →ₗ.[R] F<VAR>x : ↥(f.closure.domRestrict f.domain).domain<VAR>y : ↥f.domain<VAR>hxy : ↑x = ↑y<VAR>z : ↥f.closure.domain := ⟨↑y, ⋯⟩<VAR>hyz : ↑y = ↑z<GOAL>↑(f.closure.domRestrict f.domain) x = ↑f y
<VAR>R : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹¹ : CommRing R<VAR>inst✝¹⁰ : AddCommGroup E<VAR>inst✝⁹ : AddCommGroup F<VAR>inst✝⁸ : Module R E<VAR>inst✝⁷ : Module R F<VAR>inst✝⁶ : TopologicalSpace E<VAR>inst✝⁵ : TopologicalSpace F<VAR>inst✝⁴ : ContinuousAdd E<VAR>inst✝³ : ContinuousAdd F<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : ContinuousSMul R E<VAR>inst✝ : ContinuousSMul R F<VAR>f : E →ₗ.[R] F<VAR>x : ↥(f.closure.domRestrict f.domain).domain<VAR>y : ↥f.domain<VAR>hxy : ↑x = ↑y<VAR>z : ↥f.closure.domain := ⟨↑y, ⋯⟩<VAR>hyz : ↑y = ↑z<GOAL>↑(f.closure.domRestrict f.domain) x = ↑f.closure z
<VAR>xl xr : Type u<VAR>ι : Type u_1<VAR>inst✝ : Small.{u, u_1} ι<VAR>f : ι → PGame<VAR>x : PGame := mk ((i : Shrink.{u, u_1} ι) × (f ((equivShrink ι).symm i)).LeftMoves) PEmpty.{u + 1} (fun x => (f ((equivShrink ι).symm x.fst)).moveLeft x.snd) PEmpty.elim<GOAL>BddAbove (Set.range f)
<VAR>xl xr : Type u<VAR>ι : Type u_1<VAR>inst✝ : Small.{u, u_1} ι<VAR>f : ι → PGame<VAR>x : PGame := mk ((i : Shrink.{u, u_1} ι) × (f ((equivShrink ι).symm i)).LeftMoves) PEmpty.{u + 1} (fun x => (f ((equivShrink ι).symm x.fst)).moveLeft x.snd) PEmpty.elim<VAR>i : ι<GOAL>f i ≤ x
<VAR>xl xr : Type u<VAR>ι : Type u_1<VAR>inst✝ : Small.{u, u_1} ι<VAR>f : ι → PGame<VAR>x : PGame := mk ((i : Shrink.{u, u_1} ι) × (f ((equivShrink ι).symm i)).LeftMoves) PEmpty.{u + 1} (fun x => (f ((equivShrink ι).symm x.fst)).moveLeft x.snd) PEmpty.elim<VAR>i : ι<GOAL>(∀ (i_1 : (f ((equivShrink ι).symm ((equivShrink ι) i))).LeftMoves), (f ((equivShrink ι).symm ((equivShrink ι) i))).moveLeft i_1 ⧏ x) ∧ ∀ (j : x.RightMoves), f ((equivShrink ι).symm ((equivShrink ι) i)) ⧏ x.moveRight j
<VAR>α : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>x y : α<VAR>x✝¹ : x ∣ y ∧ ¬y ∣ x<VAR>d : α<VAR>hd : y = x * d<VAR>hyx : ¬y ∣ x<VAR>x✝ : d ∣ 1<VAR>e : α<VAR>he : 1 = d * e<GOAL>x = y * e
<VAR>α : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>x y : α<VAR>x✝¹ : DvdNotUnit x y<VAR>hx0 : x ≠ 0<VAR>d : α<VAR>hdu : ¬IsUnit d<VAR>hdx : y = x * d<VAR>x✝ : y ∣ x<VAR>e : α<VAR>he : x = y * e<GOAL>x * 1 = x * (d * e)
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : DecidableEq n<VAR>R : Type u_2<VAR>K : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Field K<VAR>inst✝ : Fintype m<VAR>A : Matrix m m K<GOAL>Function.Injective A.mulVec ↔ IsUnit A
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝⁴ : DecidableEq m<VAR>inst✝³ : DecidableEq n<VAR>R : Type u_2<VAR>K : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Field K<VAR>inst✝ : Fintype m<VAR>A : Matrix m m K<GOAL>Function.Injective A.mulVec ↔ Function.Injective fun v => v ᵥ* Aᵀ
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f : Filter α<VAR>s : Set α<VAR>a : α<VAR>inst✝ : LinearOrder α<VAR>x : α<VAR>hx : IsTop x<VAR>this : Nonempty α<GOAL>atTop = pure x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f : Filter α<VAR>s : Set α<VAR>a : α<VAR>inst✝ : LinearOrder α<VAR>x : α<VAR>hx : IsTop x<VAR>this : Nonempty α<GOAL>{x} ∈ atTop
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f : Filter α<VAR>s : Set α<VAR>a : α<VAR>inst✝ : LinearOrder α<VAR>x : α<VAR>hx : IsTop x<VAR>this : Nonempty α<GOAL>{x} = Ici x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t : Set α<VAR>f✝ g : α → E<VAR>inst✝ : IsProbabilityMeasure μ<VAR>f : α → E<GOAL>⨍ (x : α), f x ∂μ = ∫ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : LinearOrder β<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : OrderTopology β<VAR>s : Set α<VAR>a : α<VAR>hsa : a ∈ upperBounds s<VAR>hsf : a ∈ closure s<GOAL>IsLUB s a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : LinearOrder β<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : OrderTopology β<VAR>s : Set α<VAR>a : α<VAR>hsa : a ∈ upperBounds s<VAR>hsf : (𝓟 s ⊓ 𝓝 a).NeBot<GOAL>IsLUB s a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<VAR>x✝ y✝ z x y : E<GOAL>insert x (insert y (openSegment 𝕜 x y)) = [x-[𝕜]y]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<VAR>x✝ y✝ z x y : E<GOAL>[x-[𝕜]y] ⊆ insert x (insert y (openSegment 𝕜 x y))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<VAR>x✝ y✝ z x y : E<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>a • x + b • y ∈ insert x (insert y (openSegment 𝕜 x y))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<VAR>x✝ y✝ z x y : E<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>b = 0 → a • x + b • y = x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<VAR>x✝ y✝ z x y : E<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<VAR>hb' : 0 < b<GOAL>a = 0 → a • x + b • y = y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommMonoid E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<VAR>x✝ y✝ z x y : E<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<VAR>hb' : 0 < b<VAR>ha' : 0 < a<GOAL>a • x + b • y ∈ openSegment 𝕜 x y
<VAR>p q✝ : ℚ≥0<VAR>n₁ n₂ d₁ d₂ d : ℕ<VAR>q : ℚ≥0<GOAL>↑(divNat q.num q.den) = mkRat (↑q).num (↑q).den
<VAR>n : ℕ<VAR>hn : Odd n<GOAL>Nat.card { p // Commute p.1 p.2 } = n * (n + 3)
<VAR>n : ℕ<VAR>hn : Odd n<VAR>hn' : NeZero n<GOAL>Nat.card { p // Commute p.1 p.2 } = n * (n + 3)
<VAR>n : ℕ<VAR>hn : Odd n<VAR>hn' : NeZero n<GOAL>n + (n + (n + n * n)) = n * (n + 3)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u_2}<GOAL>(succ o).cof = 1
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u_2}<GOAL>(succ o).cof ≤ 1
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u_2}<GOAL>1 ≤ (succ o).cof
<VAR>G : Type u_1<VAR>M : Type u_2<VAR>inst✝ : Monoid M<VAR>a✝ b c : M<VAR>m n : ℕ<VAR>a : M<GOAL>a ^ 2 = a * a
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>ι : Type u_1<VAR>s : ι → C<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasFiniteBiproducts C<VAR>o : HomOrthogonal s<VAR>α β : Type<VAR>inst✝¹ : Finite α<VAR>inst✝ : Finite β<VAR>f : α → ι<VAR>g : β → ι<VAR>z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)<VAR>j : β<VAR>k : α<GOAL>biproduct.ι (fun a => s (f a)) k ≫ (fun z => biproduct.matrix fun j k => if h : f j = g k then z (f j) ⟨k, ⋯⟩ ⟨j, ⋯⟩ ≫ eqToHom ⋯ else 0) ((fun z i j k => eqToHom ⋯ ≫ biproduct.components z ↑k ↑j ≫ eqToHom ⋯) z) ≫ biproduct.π (fun b => s (g b)) j = biproduct.ι (fun a => s (f a)) k ≫ z ≫ biproduct.π (fun b => s (g b)) j
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>ι : Type u_1<VAR>s : ι → C<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasFiniteBiproducts C<VAR>o : HomOrthogonal s<VAR>α β : Type<VAR>inst✝¹ : Finite α<VAR>inst✝ : Finite β<VAR>f : α → ι<VAR>g : β → ι<VAR>z : (⨁ fun a => s (f a)) ⟶ ⨁ fun b => s (g b)<VAR>j : β<VAR>k : α<GOAL>(if h : f k = g j then (eqToHom ⋯ ≫ biproduct.components z k j ≫ eqToHom ⋯) ≫ eqToHom ⋯ else 0) = biproduct.ι (fun a => s (f a)) k ≫ z ≫ biproduct.π (fun b => s (g b)) j
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>ι : Type u_1<VAR>s : ι → C<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasFiniteBiproducts C<VAR>o : HomOrthogonal s<VAR>α β : Type<VAR>inst✝¹ : Finite α<VAR>inst✝ : Finite β<VAR>f : α → ι<VAR>g : β → ι<VAR>z : (i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (End (s i))<VAR>j : β<VAR>k : α<VAR>w : j ∈ g ⁻¹' {f k}<GOAL>(fun z i j k => eqToHom ⋯ ≫ biproduct.components z ↑k ↑j ≫ eqToHom ⋯) ((fun z => biproduct.matrix fun j k => if h : f j = g k then z (f j) ⟨k, ⋯⟩ ⟨j, ⋯⟩ ≫ eqToHom ⋯ else 0) z) (f k) ⟨j, w⟩ ⟨k, ⋯⟩ = z (f k) ⟨j, w⟩ ⟨k, ⋯⟩
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>ι : Type u_1<VAR>s : ι → C<VAR>inst✝³ : HasZeroMorphisms C<VAR>inst✝² : HasFiniteBiproducts C<VAR>o : HomOrthogonal s<VAR>α β : Type<VAR>inst✝¹ : Finite α<VAR>inst✝ : Finite β<VAR>f : α → ι<VAR>g : β → ι<VAR>z : (i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (End (s i))<VAR>j : β<VAR>k : α<VAR>w : j ∈ g ⁻¹' {f k}<GOAL>(if h : f k = g j then z (f k) ⟨j, ⋯⟩ ⟨k, ⋯⟩ ≫ eqToHom ⋯ else 0) ≫ eqToHom ⋯ = z (f k) ⟨j, w⟩ ⟨k, ⋯⟩
<VAR>I : Type u<VAR>inst✝⁵ : DecidableEq I<VAR>i✝ : I<VAR>R : Type v<VAR>inst✝⁴ : CommSemiring R<VAR>A : I → Type w<VAR>inst✝³ : (i : I) → Semiring (A i)<VAR>inst✝² : (i : I) → Algebra R (A i)<VAR>B : Type w'<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra R B<VAR>maps : {i : I} → A i →ₐ[R] B<VAR>f : FreeProduct R A →ₐ[R] B<VAR>h : ∀ (i : I), f ∘ₐ ι R A i = maps<VAR>i : I<VAR>a : A i<GOAL>(((f ∘ₐ RingQuot.mkAlgHom R (rel R A)).toLinearMap ∘ₗ TensorAlgebra.ι R) ∘ₗ DirectSum.lof R I A i) a = (((((lift R A) fun {i} => maps) ∘ₐ RingQuot.mkAlgHom R (rel R A)).toLinearMap ∘ₗ TensorAlgebra.ι R) ∘ₗ DirectSum.lof R I A i) a
<VAR>I : Type u<VAR>inst✝⁵ : DecidableEq I<VAR>i✝ : I<VAR>R : Type v<VAR>inst✝⁴ : CommSemiring R<VAR>A : I → Type w<VAR>inst✝³ : (i : I) → Semiring (A i)<VAR>inst✝² : (i : I) → Algebra R (A i)<VAR>B : Type w'<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra R B<VAR>maps : {i : I} → A i →ₐ[R] B<VAR>f : FreeProduct R A →ₐ[R] B<VAR>i : I<VAR>a : A i<VAR>h : ∀ (i : I) (x : A i), (f ∘ₐ ι R A i) x = maps x<GOAL>(((f ∘ₐ RingQuot.mkAlgHom R (rel R A)).toLinearMap ∘ₗ TensorAlgebra.ι R) ∘ₗ DirectSum.lof R I A i) a = (((((lift R A) fun {i} => maps) ∘ₐ RingQuot.mkAlgHom R (rel R A)).toLinearMap ∘ₗ TensorAlgebra.ι R) ∘ₗ DirectSum.lof R I A i) a
<VAR>I : Type u<VAR>inst✝⁵ : DecidableEq I<VAR>i✝ : I<VAR>R : Type v<VAR>inst✝⁴ : CommSemiring R<VAR>A : I → Type w<VAR>inst✝³ : (i : I) → Semiring (A i)<VAR>inst✝² : (i : I) → Algebra R (A i)<VAR>B : Type w'<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra R B<VAR>maps : {i : I} → A i →ₐ[R] B<VAR>f : FreeProduct R A →ₐ[R] B<VAR>i : I<VAR>a : A i<VAR>h : (f ∘ₐ ι R A i) a = maps a<GOAL>(((f ∘ₐ RingQuot.mkAlgHom R (rel R A)).toLinearMap ∘ₗ TensorAlgebra.ι R) ∘ₗ DirectSum.lof R I A i) a = (((((lift R A) fun {i} => maps) ∘ₐ RingQuot.mkAlgHom R (rel R A)).toLinearMap ∘ₗ TensorAlgebra.ι R) ∘ₗ DirectSum.lof R I A i) a
<VAR>A : Type u_1<VAR>inst✝⁷ : NormedRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : CstarRing A<VAR>inst✝⁴ : CompleteSpace A<VAR>inst✝³ : NormedAlgebra ℂ A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : PartialOrder A<VAR>inst✝ : StarOrderedRing A<VAR>a : A<VAR>ha : autoParam (IsSelfAdjoint a) _auto✝<GOAL>-(algebraMap ℝ A) ‖a‖ ≤ a
<VAR>A : Type u_1<VAR>inst✝⁷ : NormedRing A<VAR>inst✝⁶ : StarRing A<VAR>inst✝⁵ : CstarRing A<VAR>inst✝⁴ : CompleteSpace A<VAR>inst✝³ : NormedAlgebra ℂ A<VAR>inst✝² : StarModule ℂ A<VAR>inst✝¹ : PartialOrder A<VAR>inst✝ : StarOrderedRing A<VAR>a : A<VAR>ha : autoParam (IsSelfAdjoint a) _auto✝<VAR>this : -a ≤ (algebraMap ℝ A) ‖a‖<GOAL>-(algebraMap ℝ A) ‖a‖ ≤ a
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroup α<VAR>a✝ b : α<VAR>n : ℤ<VAR>a : α<GOAL>mabs (a ^ n) = mabs a ^ |n|
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroup α<VAR>a✝ b : α<VAR>n : ℤ<VAR>a : α<VAR>n0 : 0 ≤ n<GOAL>mabs (a ^ n) = mabs a ^ |n|
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommGroup α<VAR>a✝ b : α<VAR>n : ℤ<VAR>a : α<VAR>n0 : n ≤ 0<GOAL>mabs (a ^ n) = mabs a ^ |n|
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝓕 : Type u_4<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : ProperSpace E<VAR>inst✝ : ProperSpace F<VAR>f✝ : 𝓕<VAR>f : E → F<VAR>h : ∀ (ε : ℝ), ∃ r, ∀ (x : E), r < ‖x‖ → ε < ‖f x‖<GOAL>Tendsto f (cocompact E) (cocompact F)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝓕 : Type u_4<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : ProperSpace E<VAR>inst✝ : ProperSpace F<VAR>f✝ : 𝓕<VAR>f : E → F<VAR>h : ∀ (ε : ℝ), ∃ r, ∀ (x : E), r < ‖x‖ → ε < ‖f x‖<GOAL>∀ s ∈ cocompact F, f ⁻¹' s ∈ cocompact E
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝓕 : Type u_4<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : ProperSpace E<VAR>inst✝ : ProperSpace F<VAR>f✝ : 𝓕<VAR>f : E → F<VAR>h : ∀ (ε : ℝ), ∃ r, ∀ (x : E), r < ‖x‖ → ε < ‖f x‖<VAR>s : Set F<VAR>hs : s ∈ cocompact F<GOAL>f ⁻¹' s ∈ cocompact E
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝓕 : Type u_4<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : ProperSpace E<VAR>inst✝ : ProperSpace F<VAR>f✝ : 𝓕<VAR>f : E → F<VAR>h : ∀ (ε : ℝ), ∃ r, ∀ (x : E), r < ‖x‖ → ε < ‖f x‖<VAR>s : Set F<VAR>hs : s ∈ cocompact F<VAR>ε : ℝ<VAR>hε : (closedBall 0 ε)ᶜ ⊆ s<GOAL>f ⁻¹' s ∈ cocompact E
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝓕 : Type u_4<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : ProperSpace E<VAR>inst✝ : ProperSpace F<VAR>f✝ : 𝓕<VAR>f : E → F<VAR>h : ∀ (ε : ℝ), ∃ r, ∀ (x : E), r < ‖x‖ → ε < ‖f x‖<VAR>s : Set F<VAR>hs : s ∈ cocompact F<VAR>ε : ℝ<VAR>hε : (closedBall 0 ε)ᶜ ⊆ s<VAR>r : ℝ<VAR>hr : ∀ (x : E), r < ‖x‖ → ε < ‖f x‖<GOAL>f ⁻¹' s ∈ cocompact E
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝓕 : Type u_4<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : ProperSpace E<VAR>inst✝ : ProperSpace F<VAR>f✝ : 𝓕<VAR>f : E → F<VAR>h : ∀ (ε : ℝ), ∃ r, ∀ (x : E), r < ‖x‖ → ε < ‖f x‖<VAR>s : Set F<VAR>hs : s ∈ cocompact F<VAR>ε : ℝ<VAR>hε : (closedBall 0 ε)ᶜ ⊆ s<VAR>r : ℝ<VAR>hr : ∀ (x : E), r < ‖x‖ → ε < ‖f x‖<GOAL>∃ r, (closedBall 0 r)ᶜ ⊆ f ⁻¹' s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝓕 : Type u_4<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : ProperSpace E<VAR>inst✝ : ProperSpace F<VAR>f✝ : 𝓕<VAR>f : E → F<VAR>h : ∀ (ε : ℝ), ∃ r, ∀ (x : E), r < ‖x‖ → ε < ‖f x‖<VAR>s : Set F<VAR>hs : s ∈ cocompact F<VAR>ε : ℝ<VAR>hε : (closedBall 0 ε)ᶜ ⊆ s<VAR>r : ℝ<VAR>hr : ∀ (x : E), r < ‖x‖ → ε < ‖f x‖<GOAL>(closedBall 0 r)ᶜ ⊆ f ⁻¹' s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝓕 : Type u_4<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : ProperSpace E<VAR>inst✝ : ProperSpace F<VAR>f✝ : 𝓕<VAR>f : E → F<VAR>h : ∀ (ε : ℝ), ∃ r, ∀ (x : E), r < ‖x‖ → ε < ‖f x‖<VAR>s : Set F<VAR>hs : s ∈ cocompact F<VAR>ε : ℝ<VAR>hε : (closedBall 0 ε)ᶜ ⊆ s<VAR>r : ℝ<VAR>hr : ∀ (x : E), r < ‖x‖ → ε < ‖f x‖<VAR>x : E<VAR>hx : x ∈ (closedBall 0 r)ᶜ<GOAL>x ∈ f ⁻¹' s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝓕 : Type u_4<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : ProperSpace E<VAR>inst✝ : ProperSpace F<VAR>f✝ : 𝓕<VAR>f : E → F<VAR>h : ∀ (ε : ℝ), ∃ r, ∀ (x : E), r < ‖x‖ → ε < ‖f x‖<VAR>s : Set F<VAR>hs : s ∈ cocompact F<VAR>ε : ℝ<VAR>hε : (closedBall 0 ε)ᶜ ⊆ s<VAR>r : ℝ<VAR>hr : ∀ (x : E), r < ‖x‖ → ε < ‖f x‖<VAR>x : E<VAR>hx : r < ‖x‖<GOAL>x ∈ f ⁻¹' s
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>e : C ≌ D<VAR>G : D ⥤ C<VAR>iso : e.inverse ≅ G<VAR>X : C<GOAL>e.functor.map (e.unitIso.hom.app X ≫ iso.hom.app (e.functor.obj X)) ≫ e.functor.map (iso.inv.app (e.functor.obj X)) ≫ e.counitIso.hom.app (e.functor.obj X) = 𝟙 (e.functor.obj X)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : ι → Submodule R M<VAR>inst✝² : DecidableEq ι<VAR>h✝ : IsInternal N<VAR>κ : ι → Type u_4<VAR>inst✝¹ : (i : ι) → Fintype (κ i)<VAR>inst✝ : (i : ι) → DecidableEq (κ i)<VAR>s : Finset ι<VAR>h : IsInternal fun i => N ↑i<VAR>b : (i : { x // x ∈ s }) → Basis (κ ↑i) R ↥(N ↑i)<VAR>σ : ι → ι<VAR>hσ : ∀ (i : ι), σ i ≠ i<VAR>f : Module.End R M<VAR>hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N (σ i))<VAR>hN : ∀ i ∉ s, N i = ⊥<VAR>i : { x // x ∈ s }<VAR>k : κ ↑i<GOAL>((toMatrix (h.collectedBasis b) (h.collectedBasis b)) f).diag ⟨i, k⟩ = 0 ⟨i, k⟩
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>N : ι → Submodule R M<VAR>inst✝² : DecidableEq ι<VAR>h✝ : IsInternal N<VAR>κ : ι → Type u_4<VAR>inst✝¹ : (i : ι) → Fintype (κ i)<VAR>inst✝ : (i : ι) → DecidableEq (κ i)<VAR>s : Finset ι<VAR>h : IsInternal fun i => N ↑i<VAR>b : (i : { x // x ∈ s }) → Basis (κ ↑i) R ↥(N ↑i)<VAR>σ : ι → ι<VAR>hσ : ∀ (i : ι), σ i ≠ i<VAR>f : Module.End R M<VAR>hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N (σ i))<VAR>hN : ∀ i ∉ s, N i = ⊥<VAR>i : { x // x ∈ s }<VAR>k : κ ↑i<GOAL>((h.collectedBasis b).repr (f ↑((b i) k))) ⟨i, k⟩ = 0
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : Semiring A<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Semiring B<VAR>inst✝¹ : Algebra R B<VAR>S : Subalgebra R A<VAR>ι : Type u_4<VAR>inst✝ : Nonempty ι<VAR>K : ι → Subalgebra R A<VAR>dir : Directed (fun x x_1 => x ≤ x_1) K<VAR>f : (i : ι) → ↥(K i) →ₐ[R] B<VAR>hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)<VAR>T : Subalgebra R A<VAR>hT : T = iSup K<VAR>i : ι<VAR>x : ↥(K i)<VAR>hx : ↑x ∈ T<GOAL>Set.iUnionLift (fun i => ↑(K i)) (fun i x => (f i) x) ⋯ ↑T ⋯ ⟨↑x, hx⟩ = (f i) x
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ : E → F<VAR>f' : F<VAR>s t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F<VAR>h : HasLineDerivAt 𝕜 f f' x v<VAR>h₁ : f₁ =ᶠ[𝓝 x] f<GOAL>HasLineDerivAt 𝕜 f₁ f' x v
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ : E → F<VAR>f' : F<VAR>s t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F<VAR>h : HasLineDerivAt 𝕜 f f' x v<VAR>h₁ : f₁ =ᶠ[𝓝 x] f<GOAL>(fun t => f₁ (x + t • v)) =ᶠ[𝓝 0] fun t => f (x + t • v)
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F✝ : Type u_2<VAR>inst✝³ : NormedAddCommGroup F✝<VAR>inst✝² : NormedSpace 𝕜 F✝<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ : E → F✝<VAR>f' : F✝<VAR>s t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F✝<VAR>h : HasLineDerivAt 𝕜 f f' x v<VAR>F : 𝕜 → E := fun t => x + t • v<VAR>h₁ : f₁ =ᶠ[𝓝 (F 0)] f<GOAL>(fun t => f₁ (x + t • v)) =ᶠ[𝓝 0] fun t => f (x + t • v)
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>p : MvPolynomial (Fin (n + 1)) R<VAR>j : Fin n<VAR>i : ℕ<GOAL>degreeOf j (((finSuccEquiv R n) p).coeff i) ≤ degreeOf j.succ p
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>p : MvPolynomial (Fin (n + 1)) R<VAR>j : Fin n<VAR>i : ℕ<GOAL>∀ b ∈ (((finSuccEquiv R n) p).coeff i).support, b j ≤ p.support.sup fun m => m j.succ
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>p : MvPolynomial (Fin (n + 1)) R<VAR>j : Fin n<VAR>i : ℕ<VAR>m : Fin n →₀ ℕ<VAR>hm : m ∈ (((finSuccEquiv R n) p).coeff i).support<GOAL>m j ≤ p.support.sup fun m => m j.succ
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>s : σ →₀ ℕ<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>p : MvPolynomial (Fin (n + 1)) R<VAR>j : Fin n<VAR>i : ℕ<VAR>m : Fin n →₀ ℕ<VAR>hm : m ∈ (((finSuccEquiv R n) p).coeff i).support<GOAL>(cons i m) j.succ ≤ p.support.sup fun m => m j.succ
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P Q R : C<VAR>f✝ : P ⟶ Q<VAR>g✝ : Q ⟶ R<VAR>A B A' B' : C<VAR>f : A ⟶ B<VAR>g : A' ⟶ B'<VAR>e : Arrow.mk f ≅ Arrow.mk g<VAR>h : StrongEpi f<GOAL>Epi g
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P Q R : C<VAR>f✝ : P ⟶ Q<VAR>g✝ : Q ⟶ R<VAR>A B A' B' : C<VAR>f : A ⟶ B<VAR>g : A' ⟶ B'<VAR>e : Arrow.mk f ≅ Arrow.mk g<VAR>h : StrongEpi f<GOAL>Epi (e.inv.left ≫ f ≫ e.hom.right)