ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : LinearOrder ι<VAR>u : ι → Ω → β<VAR>τ : Ω → ι<VAR>i : ι<VAR>ω : Ω<VAR>h : τ ω ≤ i<GOAL>stoppedProcess u τ i ω = u (τ ω) ω
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>s t F : Set G<VAR>hF : IsClosed F<GOAL>F * closure {1} = F
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>s t F : Set G<VAR>hF : IsClosed F<GOAL>F * closure {1} ⊆ F
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → F<VAR>p pf pg : FormalMultilinearSeries 𝕜 E F<VAR>x : E<VAR>r r' : ℝ≥0∞<VAR>n m : ℕ<VAR>hf : HasFiniteFPowerSeriesOnBall f pf x n r<VAR>hg : HasFiniteFPowerSeriesOnBall g pg x m r<GOAL>HasFiniteFPowerSeriesOnBall (f - g) (pf - pg) x (max n m) r
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<VAR>y : R<VAR>hI : I.IsRadical<GOAL>Disjoint ↑(Submonoid.powers y) ↑I ↔ y ∉ I.toAddSubmonoid
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<VAR>y : R<VAR>hI : I.IsRadical<VAR>h : y ∉ I.toAddSubmonoid<GOAL>↑(Submonoid.powers y) ⊓ ↑I ≤ ⊥
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<VAR>y : R<VAR>hI : I.IsRadical<VAR>h : y ∉ I.toAddSubmonoid<VAR>n : ℕ<VAR>hx' : (fun x => y ^ x) n ∈ ↑I<GOAL>(fun x => y ^ x) n ∈ ⊥
<VAR>x y : ℝ<GOAL>↑x.cot = ↑(cos x / sin x)
<VAR>I₁ : Type u_1<VAR>I₂ : Type u_2<VAR>I₁₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>inst✝² : TotalComplexShape c₁ c₂ c₁₂<VAR>inst✝¹ : TotalComplexShape c₂ c₁ c₁₂<VAR>inst✝ : TotalComplexShapeSymmetry c₁ c₂ c₁₂<VAR>p q : ℤ<GOAL>(p * q).negOnePow * 1 = q.negOnePow * ((p + 1) * q).negOnePow
<VAR>I₁ : Type u_1<VAR>I₂ : Type u_2<VAR>I₁₂ : Type u_3<VAR>c₁ : ComplexShape I₁<VAR>c₂ : ComplexShape I₂<VAR>c₁₂ : ComplexShape I₁₂<VAR>inst✝² : TotalComplexShape c₁ c₂ c₁₂<VAR>inst✝¹ : TotalComplexShape c₂ c₁ c₁₂<VAR>inst✝ : TotalComplexShapeSymmetry c₁ c₂ c₁₂<VAR>p q : ℤ<GOAL>(p * q).negOnePow * p.negOnePow = 1 * (p * (q + 1)).negOnePow
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s : Multiset α<VAR>t : Multiset β<VAR>s₁ s₂ : Multiset α<VAR>t₁ t₂ : Multiset β<VAR>a : α<VAR>b : β<VAR>x : α ⊕ β<GOAL>x ∈ s.disjSum t ↔ (∃ a ∈ s, inl a = x) ∨ ∃ b ∈ t, inr b = x
<VAR>z x✝ y✝ : ℝ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>x y : ℝ<VAR>h : x < y<VAR>hy : 0 < y<GOAL>∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
<VAR>z x✝ y✝ : ℝ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>x y : ℝ<VAR>h : x < y<VAR>hy : 0 < y<VAR>hn' : 0 < ↑n<GOAL>∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
<VAR>z x✝ y✝ : ℝ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>x y : ℝ<VAR>h : x < y<VAR>hy : 0 < y<VAR>hn' : 0 < ↑n<VAR>q : ℚ<VAR>hxq : max 0 x ^ (↑n)⁻¹ < ↑q<VAR>hqy : ↑q < y ^ (↑n)⁻¹<GOAL>∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
<VAR>z x✝ y✝ : ℝ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>x y : ℝ<VAR>h : x < y<VAR>hy : 0 < y<VAR>hn' : 0 < ↑n<VAR>q : ℚ<VAR>hxq : max 0 x ^ (↑n)⁻¹ < ↑q<VAR>hqy : ↑q < y ^ (↑n)⁻¹<VAR>this : 0 ≤ max 0 x ^ (↑n)⁻¹<GOAL>∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
<VAR>z x✝ y✝ : ℝ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>x y : ℝ<VAR>h : x < y<VAR>hy : 0 < y<VAR>hn' : 0 < ↑n<VAR>q : ℚ<VAR>hxq : max 0 x ^ (↑n)⁻¹ < ↑q<VAR>hqy : ↑q < y ^ (↑n)⁻¹<VAR>this : 0 ≤ max 0 x ^ (↑n)⁻¹<VAR>hq : 0 < ↑q<GOAL>∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
<VAR>z x✝ y✝ : ℝ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>x y : ℝ<VAR>h : x < y<VAR>hy : 0 < y<VAR>hn' : 0 < ↑n<VAR>q : ℚ<VAR>hqy : ↑q < y ^ (↑n)⁻¹<VAR>this : 0 ≤ max 0 x ^ (↑n)⁻¹<VAR>hq : 0 < ↑q<VAR>hxq : (max 0 x ^ (↑n)⁻¹) ^ ↑n < ↑q ^ ↑n<GOAL>∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
<VAR>z x✝ y✝ : ℝ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>x y : ℝ<VAR>h : x < y<VAR>hy : 0 < y<VAR>hn' : 0 < ↑n<VAR>q : ℚ<VAR>this : 0 ≤ max 0 x ^ (↑n)⁻¹<VAR>hq : 0 < ↑q<VAR>hxq : (max 0 x ^ (↑n)⁻¹) ^ ↑n < ↑q ^ ↑n<VAR>hqy : ↑q ^ ↑n < (y ^ (↑n)⁻¹) ^ ↑n<GOAL>∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
<VAR>z x✝ y✝ : ℝ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>x y : ℝ<VAR>h : x < y<VAR>hy : 0 < y<VAR>hn' : 0 < ↑n<VAR>q : ℚ<VAR>this : 0 ≤ max 0 x ^ (↑n)⁻¹<VAR>hq : 0 < ↑q<VAR>hxq : max 0 x < ↑q ^ n<VAR>hqy : ↑q ^ n < y<GOAL>∃ q, 0 < q ∧ x < ↑q ^ n ∧ ↑q ^ n < y
<VAR>z x✝ y✝ : ℝ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>x y : ℝ<VAR>h : x < y<VAR>hy : 0 < y<VAR>hn' : 0 < ↑n<VAR>q : ℚ<VAR>this : 0 ≤ max 0 x ^ (↑n)⁻¹<VAR>hq : 0 < ↑q<VAR>hxq : max 0 x < ↑q ^ n<VAR>hqy : ↑q ^ n < (y ^ (↑n)⁻¹) ^ n<GOAL>0 ≤ y
<VAR>z x✝ y✝ : ℝ<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>x y : ℝ<VAR>h : x < y<VAR>hy : 0 < y<VAR>hn' : 0 < ↑n<VAR>q : ℚ<VAR>this : 0 ≤ max 0 x ^ (↑n)⁻¹<VAR>hq : 0 < ↑q<VAR>hxq : (max 0 x ^ (↑n)⁻¹) ^ n < ↑q ^ n<VAR>hqy : ↑q ^ n < (y ^ (↑n)⁻¹) ^ n<GOAL>0 ≤ max 0 x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<GOAL>Fintype.card { a // a.IsDiag } = Fintype.card α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<GOAL>Fintype.card { a // a.IsDiag } = (image Sym2.mk univ.diag).card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<GOAL>∀ (x : Sym2 α), x ∈ filter IsDiag (image Sym2.mk (univ ×ˢ univ)) ↔ x.IsDiag
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>x : Sym2 α<GOAL>x ∈ filter IsDiag (image Sym2.mk (univ ×ˢ univ)) ↔ x.IsDiag
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>x : Sym2 α<GOAL>(∃ a ∈ univ, Sym2.mk a = x) ∧ x.IsDiag ↔ x.IsDiag
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>x : Sym2 α<VAR>a : α × α<VAR>ha : Quot.mk (Rel α) a = x<GOAL>(∃ a ∈ univ, Sym2.mk a = x) ∧ x.IsDiag ↔ x.IsDiag
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r✝ r₁ r₂ : α → α → Prop<VAR>s✝ t : Set α<VAR>a b x✝ : α<VAR>f✝ : α → β<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>y : Set β<VAR>x : Set α<VAR>f : r ↪r s<VAR>h : y ⊆ ⇑f '' x<GOAL>x ∩ ⇑f ⁻¹' minimals s y = minimals r (x ∩ ⇑f ⁻¹' y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r✝ r₁ r₂ : α → α → Prop<VAR>s✝ t : Set α<VAR>a b x✝ : α<VAR>f✝ : α → β<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>y : Set β<VAR>x : Set α<VAR>f : r ↪r s<VAR>h : y ⊆ ⇑f '' x<GOAL>∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>x y : R<VAR>h : IsCoprime x y<VAR>z : R<GOAL>IsCoprime x (y + x * z)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>x y : R<VAR>h : IsCoprime x y<VAR>z : R<GOAL>IsCoprime (y + x * z) x
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>I J : Ideal R<VAR>N P : Submodule R M<VAR>s : Set M<VAR>r : R<GOAL>r ∈ (span R s).annihilator ↔ ∀ (n : ↑s), r • ↑n = 0
<VAR>R : Type u<VAR>M : Type v<VAR>M' : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>I J : Ideal R<VAR>N P : Submodule R M<VAR>s : Set M<VAR>r : R<GOAL>(∀ n ∈ span R s, r • n = 0) ↔ ∀ (n : ↑s), r • ↑n = 0
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f✝ f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>f : M → M' × N'<VAR>x : M<GOAL>ContMDiffAt I (I'.prod J') n f x ↔ ContMDiffAt I I' n (Prod.fst ∘ f) x ∧ ContMDiffAt I J' n (Prod.snd ∘ f) x
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f✝ f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x✝ : M<VAR>m n : ℕ∞<VAR>f : M → M' × N'<VAR>x : M<GOAL>ContMDiffWithinAt I (I'.prod J') n f univ x ↔ ContMDiffWithinAt I I' n (Prod.fst ∘ f) univ x ∧ ContMDiffWithinAt I J' n (Prod.snd ∘ f) univ x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{?u.58352, u_1} C<VAR>inst✝² : Category.{?u.58356, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>inst✝ : HasZeroMorphisms D<GOAL>S.g.op ≫ S.f.op = 0
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{?u.58352, u_1} C<VAR>inst✝² : Category.{?u.58356, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>inst✝ : HasZeroMorphisms D<GOAL>Quiver.Hom.op 0 = 0
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : LocallyRingedSpace<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<VAR>U : Opens ↑X.toTopCat<GOAL>op U = (Opens.map f.val.base).op.obj (op ((opensFunctor f).obj U))
<VAR>R : Type u_1<VAR>n : ℕ<VAR>h0 : n ≠ 0<GOAL>∑ m ∈ range (n + 1), (-1) ^ m * ↑(n.choose m) = 0
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>x : E<VAR>s : Set E<VAR>x✝ : ℂ<GOAL>logDeriv cos x✝ = (-tan) x✝
<VAR>J : Type v'<VAR>inst✝⁵ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝³ : Category.{?u.324351, u_1} K<VAR>D : Type u_2<VAR>inst✝² : Category.{?u.324358, u_2} D<VAR>inst✝¹ : HasInitial C<VAR>ι : Type u_3<VAR>X : ι → C<VAR>c : Cofan X<VAR>hc : IsVanKampenColimit c<VAR>i j : ι<VAR>inst✝ : DecidableEq ι<GOAL>IsPullback (if h : j = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)) (if h : j = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X j)) (c.inj i) (c.inj j)
<VAR>J : Type v'<VAR>inst✝⁵ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝³ : Category.{?u.324351, u_1} K<VAR>D : Type u_2<VAR>inst✝² : Category.{?u.324358, u_2} D<VAR>inst✝¹ : HasInitial C<VAR>ι : Type u_3<VAR>X : ι → C<VAR>c : Cofan X<VAR>hc : IsVanKampenColimit c<VAR>i j : ι<VAR>inst✝ : DecidableEq ι<GOAL>(Discrete.natTrans fun k => if h : k.as = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to ((Discrete.functor X).obj k)) ≫ c.ι = (Cofan.mk (X i) fun k => if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i)).ι ≫ (Functor.const (Discrete ι)).map (c.inj i)
<VAR>J : Type v'<VAR>inst✝⁵ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝³ : Category.{?u.324351, u_1} K<VAR>D : Type u_2<VAR>inst✝² : Category.{?u.324358, u_2} D<VAR>inst✝¹ : HasInitial C<VAR>ι : Type u_3<VAR>X : ι → C<VAR>c : Cofan X<VAR>hc : IsVanKampenColimit c<VAR>i j : ι<VAR>inst✝ : DecidableEq ι<GOAL>IsColimit (Cofan.mk (X i) fun k => if h : k = i then eqToHom ⋯ else eqToHom ⋯ ≫ initial.to (X i))
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝⁶ : DivisionRing K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>L : Type u_3<VAR>W : Type u_4<VAR>inst✝³ : DivisionRing L<VAR>inst✝² : AddCommGroup W<VAR>inst✝¹ : Module L W<VAR>σ : K →+* L<VAR>τ : L →+* K<VAR>inst✝ : RingHomInvPair σ τ<VAR>f : V →ₛₗ[σ] W<VAR>hf : Function.Injective ⇑f<VAR>u v : ℙ K V<VAR>h : map f hf u = map f hf v<GOAL>u = v
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝⁶ : DivisionRing K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>L : Type u_3<VAR>W : Type u_4<VAR>inst✝³ : DivisionRing L<VAR>inst✝² : AddCommGroup W<VAR>inst✝¹ : Module L W<VAR>σ : K →+* L<VAR>τ : L →+* K<VAR>inst✝ : RingHomInvPair σ τ<VAR>f : V →ₛₗ[σ] W<VAR>hf : Function.Injective ⇑f<VAR>v : ℙ K V<VAR>u : V<VAR>hu : u ≠ 0<VAR>h : map f hf (mk K u hu) = map f hf v<GOAL>mk K u hu = v
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝⁶ : DivisionRing K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>L : Type u_3<VAR>W : Type u_4<VAR>inst✝³ : DivisionRing L<VAR>inst✝² : AddCommGroup W<VAR>inst✝¹ : Module L W<VAR>σ : K →+* L<VAR>τ : L →+* K<VAR>inst✝ : RingHomInvPair σ τ<VAR>f : V →ₛₗ[σ] W<VAR>hf : Function.Injective ⇑f<VAR>u : V<VAR>hu : u ≠ 0<VAR>v : V<VAR>hv : v ≠ 0<VAR>h : map f hf (mk K u hu) = map f hf (mk K v hv)<GOAL>mk K u hu = mk K v hv
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝⁶ : DivisionRing K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>L : Type u_3<VAR>W : Type u_4<VAR>inst✝³ : DivisionRing L<VAR>inst✝² : AddCommGroup W<VAR>inst✝¹ : Module L W<VAR>σ : K →+* L<VAR>τ : L →+* K<VAR>inst✝ : RingHomInvPair σ τ<VAR>f : V →ₛₗ[σ] W<VAR>hf : Function.Injective ⇑f<VAR>u : V<VAR>hu : u ≠ 0<VAR>v : V<VAR>hv : v ≠ 0<VAR>h : ∃ a, a • f v = f u<GOAL>∃ a, a • v = u
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝⁶ : DivisionRing K<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module K V<VAR>L : Type u_3<VAR>W : Type u_4<VAR>inst✝³ : DivisionRing L<VAR>inst✝² : AddCommGroup W<VAR>inst✝¹ : Module L W<VAR>σ : K →+* L<VAR>τ : L →+* K<VAR>inst✝ : RingHomInvPair σ τ<VAR>f : V →ₛₗ[σ] W<VAR>hf : Function.Injective ⇑f<VAR>u : V<VAR>hu : u ≠ 0<VAR>v : V<VAR>hv : v ≠ 0<VAR>a : L<VAR>ha : a • f v = f u<GOAL>f (τ a • v) = f u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>K : Type u_3<VAR>inst✝ : DivisionSemiring α<VAR>a b c d : α<VAR>hbc : Commute b c<VAR>hbd : Commute b d<VAR>hb : b ≠ 0<VAR>hd : d ≠ 0<GOAL>a / b + c / d = (a * d + b * c) / (b * d)
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x✝ : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>iso : E ≃ₗᵢ[𝕜] F<VAR>f : G → E<VAR>x : G<GOAL>fderiv 𝕜 (⇑iso ∘ f) x = (↑{ toLinearEquiv := iso.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }).comp (fderiv 𝕜 f x)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R : ℝ<VAR>z w : ℂ<VAR>f : ℂ → E<GOAL>Periodic (circleTransformDeriv R z w f) (2 * π)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R : ℝ<VAR>z w : ℂ<VAR>f : ℂ → E<VAR>this : ∀ (c : ℂ) (R : ℝ), Periodic (circleMap c R) (2 * π)<GOAL>Periodic (circleTransformDeriv R z w f) (2 * π)
<VAR>𝕜 : Type u_1<VAR>inst✝²¹ : NontriviallyNormedField 𝕜<VAR>EM : Type u_2<VAR>inst✝²⁰ : NormedAddCommGroup EM<VAR>inst✝¹⁹ : NormedSpace 𝕜 EM<VAR>HM : Type u_3<VAR>inst✝¹⁸ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>E : Type u_4<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_5<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_6<VAR>inst✝¹⁴ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E H'<VAR>M : Type u<VAR>inst✝¹³ : TopologicalSpace M<VAR>inst✝¹² : ChartedSpace HM M<VAR>N G A A' R : Type u<VAR>inst✝¹¹ : TopologicalSpace N<VAR>inst✝¹⁰ : ChartedSpace H N<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : ChartedSpace H G<VAR>inst✝⁷ : TopologicalSpace A<VAR>inst✝⁶ : ChartedSpace H A<VAR>inst✝⁵ : TopologicalSpace A'<VAR>inst✝⁴ : ChartedSpace H' A'<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : ChartedSpace H R<VAR>inst✝¹ : CommRing R<VAR>inst✝ : SmoothRing I R<VAR>x : ↑(TopCat.of M)<GOAL>(forgetStalk IM I M R x).inv ≫ ⇑(evalHom IM I M R x) = smoothSheaf.evalHom IM I R x
<VAR>𝕜 : Type u_1<VAR>inst✝²¹ : NontriviallyNormedField 𝕜<VAR>EM : Type u_2<VAR>inst✝²⁰ : NormedAddCommGroup EM<VAR>inst✝¹⁹ : NormedSpace 𝕜 EM<VAR>HM : Type u_3<VAR>inst✝¹⁸ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>E : Type u_4<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_5<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_6<VAR>inst✝¹⁴ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E H'<VAR>M : Type u<VAR>inst✝¹³ : TopologicalSpace M<VAR>inst✝¹² : ChartedSpace HM M<VAR>N G A A' R : Type u<VAR>inst✝¹¹ : TopologicalSpace N<VAR>inst✝¹⁰ : ChartedSpace H N<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : ChartedSpace H G<VAR>inst✝⁷ : TopologicalSpace A<VAR>inst✝⁶ : ChartedSpace H A<VAR>inst✝⁵ : TopologicalSpace A'<VAR>inst✝⁴ : ChartedSpace H' A'<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : ChartedSpace H R<VAR>inst✝¹ : CommRing R<VAR>inst✝ : SmoothRing I R<VAR>x : ↑(TopCat.of M)<GOAL>∀ (j : (OpenNhds x)ᵒᵖ), colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑(TopCat.of M))ᵒᵖ (Type u)).obj (OpenNhds.inclusion x).op).obj (smoothSheaf IM I M R).presheaf) j ≫ (forgetStalk IM I M R x).inv ≫ ⇑(evalHom IM I M R x) = colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑(TopCat.of M))ᵒᵖ (Type u)).obj (OpenNhds.inclusion x).op).obj (smoothSheaf IM I M R).presheaf) j ≫ smoothSheaf.evalHom IM I R x
<VAR>𝕜 : Type u_1<VAR>inst✝²¹ : NontriviallyNormedField 𝕜<VAR>EM : Type u_2<VAR>inst✝²⁰ : NormedAddCommGroup EM<VAR>inst✝¹⁹ : NormedSpace 𝕜 EM<VAR>HM : Type u_3<VAR>inst✝¹⁸ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>E : Type u_4<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_5<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_6<VAR>inst✝¹⁴ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E H'<VAR>M : Type u<VAR>inst✝¹³ : TopologicalSpace M<VAR>inst✝¹² : ChartedSpace HM M<VAR>N G A A' R : Type u<VAR>inst✝¹¹ : TopologicalSpace N<VAR>inst✝¹⁰ : ChartedSpace H N<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : ChartedSpace H G<VAR>inst✝⁷ : TopologicalSpace A<VAR>inst✝⁶ : ChartedSpace H A<VAR>inst✝⁵ : TopologicalSpace A'<VAR>inst✝⁴ : ChartedSpace H' A'<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : ChartedSpace H R<VAR>inst✝¹ : CommRing R<VAR>inst✝ : SmoothRing I R<VAR>x : ↑(TopCat.of M)<VAR>U : (OpenNhds x)ᵒᵖ<GOAL>(forget CommRingCat).map (colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheafCommRing IM I M R).presheaf) U) ≫ ⇑(evalHom IM I M R x) = colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheaf IM I M R).presheaf) U ≫ smoothSheaf.evalHom IM I R x
<VAR>𝕜 : Type u_1<VAR>inst✝²¹ : NontriviallyNormedField 𝕜<VAR>EM : Type u_2<VAR>inst✝²⁰ : NormedAddCommGroup EM<VAR>inst✝¹⁹ : NormedSpace 𝕜 EM<VAR>HM : Type u_3<VAR>inst✝¹⁸ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>E : Type u_4<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_5<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_6<VAR>inst✝¹⁴ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E H'<VAR>M : Type u<VAR>inst✝¹³ : TopologicalSpace M<VAR>inst✝¹² : ChartedSpace HM M<VAR>N G A A' R : Type u<VAR>inst✝¹¹ : TopologicalSpace N<VAR>inst✝¹⁰ : ChartedSpace H N<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : ChartedSpace H G<VAR>inst✝⁷ : TopologicalSpace A<VAR>inst✝⁶ : ChartedSpace H A<VAR>inst✝⁵ : TopologicalSpace A'<VAR>inst✝⁴ : ChartedSpace H' A'<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : ChartedSpace H R<VAR>inst✝¹ : CommRing R<VAR>inst✝ : SmoothRing I R<VAR>x : ↑(TopCat.of M)<VAR>U : (OpenNhds x)ᵒᵖ<GOAL>colimit.ι ((OpenNhds.inclusion x).op ⋙ (smoothSheaf IM I M R).presheaf) U ≫ smoothSheaf.evalHom IM I R x = (forget CommRingCat).map (evalAt IM I M R x (unop U))
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α✝ : Type u_12<VAR>β : Type u_13<VAR>inst✝⁴ : DecidableEq o<VAR>inst✝³ : Zero α✝<VAR>inst✝² : Zero β<VAR>α : Type u_14<VAR>inst✝¹ : AddMonoid α<VAR>inst✝ : StarAddMonoid α<VAR>M : o → Matrix m n α<GOAL>(blockDiagonal M)ᴴ = blockDiagonal fun k => (M k)ᴴ
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>p : Type u_5<VAR>q : Type u_6<VAR>m' : o → Type u_7<VAR>n' : o → Type u_8<VAR>p' : o → Type u_9<VAR>R : Type u_10<VAR>S : Type u_11<VAR>α✝ : Type u_12<VAR>β : Type u_13<VAR>inst✝⁴ : DecidableEq o<VAR>inst✝³ : Zero α✝<VAR>inst✝² : Zero β<VAR>α : Type u_14<VAR>inst✝¹ : AddMonoid α<VAR>inst✝ : StarAddMonoid α<VAR>M : o → Matrix m n α<GOAL>(blockDiagonal fun k => (M k)ᵀ).map star = blockDiagonal fun k => (M k)ᵀ.map star
<VAR>R : Type u<VAR>inst✝⁶ : CommSemiring R<VAR>M : Type v<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>ι : Type w<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>κ : Type u_1<VAR>inst✝¹ : DecidableEq κ<VAR>inst✝ : Fintype κ<VAR>b✝ : Basis ι R M<VAR>c : Basis κ R M<VAR>s : Finset M<VAR>b : Basis { x // x ∈ s } R M<VAR>f : M →ₗ[R] M<VAR>this : ∃ s, Nonempty (Basis { x // x ∈ s } R M)<GOAL>(trace R M) f = ((toMatrix b b) f).trace
<VAR>R : Type u<VAR>inst✝⁶ : CommSemiring R<VAR>M : Type v<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>ι : Type w<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : Fintype ι<VAR>κ : Type u_1<VAR>inst✝¹ : DecidableEq κ<VAR>inst✝ : Fintype κ<VAR>b✝ : Basis ι R M<VAR>c : Basis κ R M<VAR>s : Finset M<VAR>b : Basis { x // x ∈ s } R M<VAR>f : M →ₗ[R] M<VAR>this : ∃ s, Nonempty (Basis { x // x ∈ s } R M)<GOAL>(traceAux R ⋯.some) f = (traceAux R b) f