ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S✝ : Type u_7<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : Semiring R₂<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>inst✝² : RingHomSurjective τ₁₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>S : Submodule R M<VAR>hf : Surjective ⇑f<GOAL>Surjective ⇑(f.domRestrict S) ↔ S ⊔ LinearMap.ker f = ⊤
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S✝ : Type u_7<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : Semiring R₂<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>inst✝² : RingHomSurjective τ₁₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>S : Submodule R M<VAR>hf : LinearMap.range f = ⊤<GOAL>LinearMap.range (f.domRestrict S) = ⊤ ↔ S ⊔ LinearMap.ker f = ⊤
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S✝ : Type u_7<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : Semiring R₂<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : Module R₂ M₂<VAR>τ₁₂ : R →+* R₂<VAR>inst✝² : RingHomSurjective τ₁₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F τ₁₂ M M₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>S : Submodule R M<VAR>hf : LinearMap.range f = ⊤<GOAL>LinearMap.range (f.domRestrict S) = LinearMap.range f ↔ S ⊔ LinearMap.ker f = ⊤
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M : Type u₄<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : LieRing L₂<VAR>inst✝⁴ : LieAlgebra R L₂<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>I : LieIdeal R L<VAR>x : L<VAR>hxI : Submodule.span R {x} ⊔ (lieIdealSubalgebra R L I).toSubmodule = ⊤<VAR>n : ℕ<VAR>hn : (toEnd R L M) x ^ n = 0<VAR>k : ℕ<VAR>hk : lowerCentralSeries R (↥↑I) M k = ⊥<GOAL>LieModule.IsNilpotent R L M
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M : Type u₄<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : LieRing L₂<VAR>inst✝⁴ : LieAlgebra R L₂<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>I : LieIdeal R L<VAR>x : L<VAR>hxI : Submodule.span R {x} ⊔ (lieIdealSubalgebra R L I).toSubmodule = ⊤<VAR>n : ℕ<VAR>hn : (toEnd R L M) x ^ n = 0<VAR>k : ℕ<VAR>hk : lowerCentralSeries R (↥↑I) M k = ⊥<VAR>hk' : I.lcs M k = ⊥<GOAL>LieModule.IsNilpotent R L M
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M : Type u₄<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : LieRing L₂<VAR>inst✝⁴ : LieAlgebra R L₂<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>I : LieIdeal R L<VAR>x : L<VAR>hxI : Submodule.span R {x} ⊔ (lieIdealSubalgebra R L I).toSubmodule = ⊤<VAR>n : ℕ<VAR>hn : (toEnd R L M) x ^ n = 0<VAR>k : ℕ<VAR>hk : lowerCentralSeries R (↥↑I) M k = ⊥<VAR>hk' : I.lcs M k = ⊥<GOAL>∀ (l : ℕ), lowerCentralSeries R L M (l * n) ≤ I.lcs M l
<VAR>m n k : ℤ<GOAL>(m * n).lcm (m * k) = m.natAbs * n.lcm k
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>G : Type u_3<VAR>G₀ : Type u_4<VAR>R : Type u_5<VAR>K : Type u_6<VAR>inst✝ : Group G<VAR>g h : G<GOAL>(orbitRel (ConjAct G) G).Rel g h = IsConj g h
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f g : X → Y<VAR>t : Set (SeparationQuotient X)<GOAL>QuotientMap (Prod.map mk mk)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s : Set X<VAR>f g : X → Y<VAR>t : Set (SeparationQuotient X)<VAR>hsurj : Surjective (Prod.map mk mk)<GOAL>QuotientMap (Prod.map mk mk)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s✝ : Set X<VAR>f g : X → Y<VAR>t : Set (SeparationQuotient X)<VAR>hsurj : Surjective (Prod.map mk mk)<VAR>s : Set (SeparationQuotient X × SeparationQuotient Y)<GOAL>IsOpen s ↔ IsOpen (Prod.map mk mk ⁻¹' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x y z : X<VAR>s✝ : Set X<VAR>f g : X → Y<VAR>t : Set (SeparationQuotient X)<VAR>hsurj : Surjective (Prod.map mk mk)<VAR>s : Set (SeparationQuotient X × SeparationQuotient Y)<VAR>hs : IsOpen (Prod.map mk mk ⁻¹' s)<GOAL>IsOpen s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x✝¹ y✝ z : X<VAR>s✝ : Set X<VAR>f g : X → Y<VAR>t : Set (SeparationQuotient X)<VAR>hsurj : Surjective (Prod.map mk mk)<VAR>s : Set (SeparationQuotient X × SeparationQuotient Y)<VAR>hs : IsOpen (Prod.map mk mk ⁻¹' s)<VAR>x✝ : X × Y<VAR>x : X<VAR>y : Y<VAR>h : Prod.map mk mk (x, y) ∈ s<GOAL>s ∈ 𝓝 (Prod.map mk mk (x, y))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x✝¹ y✝ z : X<VAR>s✝ : Set X<VAR>f g : X → Y<VAR>t : Set (SeparationQuotient X)<VAR>hsurj : Surjective (Prod.map mk mk)<VAR>s : Set (SeparationQuotient X × SeparationQuotient Y)<VAR>hs : IsOpen (Prod.map mk mk ⁻¹' s)<VAR>x✝ : X × Y<VAR>x : X<VAR>y : Y<VAR>h : Prod.map mk mk (x, y) ∈ s<GOAL>Prod.map mk mk ⁻¹' s ∈ 𝓝 (x, y)
<VAR>k : ℕ<GOAL>derivative (bernoulli (k + 1)) = (↑k + 1) * bernoulli k
<VAR>k : ℕ<GOAL>∑ x ∈ range (k + 1 + 1), (monomial (k - x)) (_root_.bernoulli x * ↑((k + 1).choose x) * ↑(k + 1 - x)) = (↑k + 1) * ∑ i ∈ range (k + 1), (monomial (k - i)) (_root_.bernoulli i * ↑(k.choose i))
<VAR>k : ℕ<GOAL>∑ x ∈ range (k + 1), (monomial (k - x)) (_root_.bernoulli x * ↑((k + 1).choose x) * ↑(k + 1 - x)) = ∑ i ∈ range (k + 1), (↑k + 1) * (monomial (k - i)) (_root_.bernoulli i * ↑(k.choose i))
<VAR>k m : ℕ<VAR>x✝ : m ∈ range (k + 1)<GOAL>(monomial (k - m)) (_root_.bernoulli m * ↑((k + 1).choose m) * ↑(k + 1 - m)) = (↑k + 1) * (monomial (k - m)) (_root_.bernoulli m * ↑(k.choose m))
<VAR>k m : ℕ<VAR>x✝ : m ∈ range (k + 1)<GOAL>(monomial (k - m)) (_root_.bernoulli m * ↑((k + 1).choose m) * ↑(k + 1 - m)) = (monomial (k - m)) (_root_.bernoulli m * ↑(k.choose m) * ↑(k + 1))
<VAR>k m : ℕ<VAR>x✝ : m ∈ range (k + 1)<GOAL>(monomial (k - m)) (_root_.bernoulli m * ↑((k + 1).choose m * (k + 1 - m))) = (monomial (k - m)) (_root_.bernoulli m * ↑(k.choose m * (k + 1)))
<VAR>k m : ℕ<VAR>x✝ : m ∈ range (k + 1)<GOAL>(k + 1).choose m * (k + 1 - m) = k.choose m * (k + 1)
<VAR>α : Type u<VAR>α' : Type w<VAR>β : Type v<VAR>β' : Type x<VAR>γ : Type u_1<VAR>δ : Type u_2<VAR>r : α → γ → Prop<VAR>s : β → δ → Prop<VAR>x : α ⊕ β<VAR>y : γ ⊕ δ<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>d : δ<VAR>h : LiftRel r s x y<GOAL>x.isLeft = true ↔ y.isLeft = true
<VAR>R : Type u_1<VAR>inst✝³ : LinearOrderedCommRing R<VAR>M : Type u_2<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>v : M<VAR>r : R<GOAL>SameRay R (-v) (r • v) ↔ r ≤ 0 ∨ v = 0
<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : SuccOrder α<VAR>a b : α<VAR>C : α → Sort u_2<GOAL>¬IsSuccLimit a ↔ ∃ b, ¬IsMax b ∧ succ b = a
<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : SuccOrder α<VAR>a b : α<VAR>C : α → Sort u_2<GOAL>(∃ b, b ⋖ a) ↔ ∃ b, ¬IsMax b ∧ succ b = a
<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : SuccOrder α<VAR>a b✝ : α<VAR>C : α → Sort u_2<VAR>b : α<GOAL>¬IsMax b ∧ succ b = a → b ⋖ a
<VAR>α : Type u_1<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : SuccOrder α<VAR>b✝ : α<VAR>C : α → Sort u_2<VAR>b : α<VAR>h : ¬IsMax b<GOAL>b ⋖ succ b
<VAR>xl xr : Type u_1<VAR>xL : xl → PGame<VAR>xR : xr → PGame<GOAL>(-mk xl xr xL xR).birthday = (mk xl xr xL xR).birthday
<VAR>xl xr : Type u_1<VAR>xL : xl → PGame<VAR>xR : xr → PGame<GOAL>max (lsub fun i => ((-mk xl xr xL xR).moveRight i).birthday) (lsub fun i => ((-mk xl xr xL xR).moveLeft i).birthday) = max (lsub fun i => ((mk xl xr xL xR).moveLeft i).birthday) (lsub fun i => ((mk xl xr xL xR).moveRight i).birthday)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>K : Type u_3<VAR>inst✝¹ : DivisionRing K<VAR>a b : K<VAR>A : Type u_4<VAR>inst✝ : DivisionRing A<VAR>m : ℚ<GOAL>m • 1 = ↑m
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a b c d : α<GOAL>Ico a b ∩ Ico c d = Ico (max a c) (min b d)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>f : α → β<VAR>hf : Injective f<GOAL>(M.map f ⋯).comap f = M
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>α₁ : Type u_6<VAR>α₂ : Type u_7<VAR>β₁ : Type u_8<VAR>β₂ : Type u_9<VAR>s₁ : Set α₁<VAR>s₂ : Set α₂<VAR>t₁ : Set β₁<VAR>t₂ : Set β₂<VAR>f₁ : α₁ → β₁<VAR>f₂ : α₂ → β₂<VAR>g₁ : β₁ → α₁<VAR>g₂ : β₂ → α₂<VAR>h₁ : InjOn f₁ s₁<VAR>h₂ : InjOn f₂ s₂<VAR>x : α₁ × α₂<VAR>hx : x ∈ s₁ ×ˢ s₂<VAR>y : α₁ × α₂<VAR>hy : y ∈ s₁ ×ˢ s₂<GOAL>(fun x => (f₁ x.1, f₂ x.2)) x = (fun x => (f₁ x.1, f₂ x.2)) y → x = y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>α₁ : Type u_6<VAR>α₂ : Type u_7<VAR>β₁ : Type u_8<VAR>β₂ : Type u_9<VAR>s₁ : Set α₁<VAR>s₂ : Set α₂<VAR>t₁ : Set β₁<VAR>t₂ : Set β₂<VAR>f₁ : α₁ → β₁<VAR>f₂ : α₂ → β₂<VAR>g₁ : β₁ → α₁<VAR>g₂ : β₂ → α₂<VAR>h₁ : InjOn f₁ s₁<VAR>h₂ : InjOn f₂ s₂<VAR>x : α₁ × α₂<VAR>hx : x ∈ s₁ ×ˢ s₂<VAR>y : α₁ × α₂<VAR>hy : y ∈ s₁ ×ˢ s₂<GOAL>f₁ x.1 = f₁ y.1 ∧ f₂ x.2 = f₂ y.2 → x.1 = y.1 ∧ x.2 = y.2
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K✝ : ℝ≥0<VAR>f✝ : α → β<VAR>x y : α<VAR>r : ℝ≥0∞<VAR>f : ι → Function.End α<VAR>K : ι → ℝ≥0<VAR>h : ∀ (i : ι), LipschitzWith (K i) (f i)<GOAL>LipschitzWith (List.map K []).prod (List.map f []).prod
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K✝ : ℝ≥0<VAR>f✝ : α → β<VAR>x y : α<VAR>r : ℝ≥0∞<VAR>f : ι → Function.End α<VAR>K : ι → ℝ≥0<VAR>h : ∀ (i : ι), LipschitzWith (K i) (f i)<VAR>i : ι<VAR>l : List ι<GOAL>LipschitzWith (List.map K (i :: l)).prod (List.map f (i :: l)).prod
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : PseudoEMetricSpace α<VAR>inst✝¹ : PseudoEMetricSpace β<VAR>inst✝ : PseudoEMetricSpace γ<VAR>K✝ : ℝ≥0<VAR>f✝ : α → β<VAR>x y : α<VAR>r : ℝ≥0∞<VAR>f : ι → Function.End α<VAR>K : ι → ℝ≥0<VAR>h : ∀ (i : ι), LipschitzWith (K i) (f i)<VAR>i : ι<VAR>l : List ι<GOAL>LipschitzWith (K i * (List.map K l).prod) (f i * (List.map f l).prod)
<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>inst✝² : SmoothManifoldWithCorners I'' M''<VAR>s : Set M<VAR>x z : M<VAR>F' : Type u_11<VAR>inst✝¹ : NormedCommRing F'<VAR>inst✝ : NormedAlgebra 𝕜 F'<VAR>p q : M → F'<VAR>p' q' : TangentSpace I z →L[𝕜] F'<VAR>hp : HasMFDerivWithinAt I 𝓘(𝕜, F') p s z p'<VAR>hq : HasMFDerivWithinAt I 𝓘(𝕜, F') q s z q'<GOAL>HasMFDerivWithinAt I 𝓘(𝕜, F') (p * q) s z (p z • q' + q z • p')
<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>inst✝² : SmoothManifoldWithCorners I'' M''<VAR>s : Set M<VAR>x z : M<VAR>F' : Type u_11<VAR>inst✝¹ : NormedCommRing F'<VAR>inst✝ : NormedAlgebra 𝕜 F'<VAR>p q : M → F'<VAR>p' q' : TangentSpace I z →L[𝕜] F'<VAR>hp : HasMFDerivWithinAt I 𝓘(𝕜, F') p s z p'<VAR>hq : HasMFDerivWithinAt I 𝓘(𝕜, F') q s z q'<GOAL>q z • p' = p'.smulRight (q z)
<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>inst✝² : SmoothManifoldWithCorners I'' M''<VAR>s : Set M<VAR>x z : M<VAR>F' : Type u_11<VAR>inst✝¹ : NormedCommRing F'<VAR>inst✝ : NormedAlgebra 𝕜 F'<VAR>p q : M → F'<VAR>p' q' : TangentSpace I z →L[𝕜] F'<VAR>hp : HasMFDerivWithinAt I 𝓘(𝕜, F') p s z p'<VAR>hq : HasMFDerivWithinAt I 𝓘(𝕜, F') q s z q'<VAR>x✝ : TangentSpace I z<GOAL>(q z • p') x✝ = (p'.smulRight (q z)) x✝
<VAR>X : Type u<VAR>Y : Type v<VAR>ι✝ : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t✝ : Set X<VAR>ι : Type v<VAR>hs : IsCompact s<VAR>t : ι → Set X<VAR>htc : ∀ (i : ι), IsClosed (t i)<VAR>hst : s ∩ ⋂ i, t i = ∅<GOAL>s ∩ ⋂ i, ⋂ i_1 ∈ i, t i_1 = ∅
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => a - x) '' Ioi b = Iio (a - b)
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<VAR>this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)<GOAL>(fun x => a - x) '' Ioi b = Iio (a - b)
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<VAR>this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)<GOAL>(fun x => a - x) '' Ioi b = Iio (a - b)
<VAR>X Y : LocallyRingedSpace<VAR>f g : X ⟶ Y<VAR>U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace<VAR>s : ↑((coequalizer f.val g.val).presheaf.obj (op U))<GOAL>⇑(coequalizer.π f.val g.val).base ⁻¹' (⇑(coequalizer.π f.val g.val).base '' (imageBasicOpen f g U s).carrier) = (imageBasicOpen f g U s).carrier
<VAR>X Y : LocallyRingedSpace<VAR>f g : X ⟶ Y<VAR>U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace<VAR>s : ↑((coequalizer f.val g.val).presheaf.obj (op U))<GOAL>⇑f.val.base ≫ ⇑(coequalizer.π f.val g.val).base = ⇑g.val.base ≫ ⇑(coequalizer.π f.val g.val).base
<VAR>X Y : LocallyRingedSpace<VAR>f g : X ⟶ Y<VAR>U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace<VAR>s : ↑((coequalizer f.val g.val).presheaf.obj (op U))<GOAL>IsColimit (Cofork.ofπ ⇑(coequalizer.π f.val g.val).base ?e)
<VAR>X Y : LocallyRingedSpace<VAR>f g : X ⟶ Y<VAR>U : Opens ↑↑(coequalizer f.val g.val).toPresheafedSpace<VAR>s : ↑((coequalizer f.val g.val).presheaf.obj (op U))<GOAL>⇑f.val.base ⁻¹' (imageBasicOpen f g U s).carrier = ⇑g.val.base ⁻¹' (imageBasicOpen f g U s).carrier
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Fintype R<VAR>R' : Type v<VAR>inst✝ : CommRing R'<VAR>χ : MulChar R R'<VAR>ψ : AddChar R R'<VAR>a : Rˣ<GOAL>χ ↑a * gaussSum χ (ψ.mulShift ↑a) = gaussSum χ ψ
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Fintype R<VAR>R' : Type v<VAR>inst✝ : CommRing R'<VAR>χ : MulChar R R'<VAR>ψ : AddChar R R'<VAR>a : Rˣ<GOAL>∑ i : R, χ ↑a * (χ i * ψ (↑a * i)) = ∑ a : R, χ a * ψ a
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Fintype R<VAR>R' : Type v<VAR>inst✝ : CommRing R'<VAR>χ : MulChar R R'<VAR>ψ : AddChar R R'<VAR>a : Rˣ<GOAL>∑ x : R, χ (↑a * x) * ψ (↑a * x) = ∑ a : R, χ a * ψ a
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x✝ y : R<VAR>inst✝ : MonoidWithZero R<VAR>x : R<VAR>m n : ℕ<VAR>h : (x ^ m) ^ n = 0<GOAL>IsNilpotent x
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x✝ y : R<VAR>inst✝ : MonoidWithZero R<VAR>x : R<VAR>m n : ℕ<VAR>h : (x ^ m) ^ n = 0<GOAL>x ^ (m * n) = 0
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ S₄ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁✝ : S₁.HomologyData<VAR>h₂✝ : S₂.HomologyData<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>γ : RightHomologyMapData φ h₁ h₂<VAR>inst✝¹ : S₁.HasHomology<VAR>inst✝ : S₂.HasHomology<VAR>γ' : HomologyMapData φ S₁.homologyData S₂.homologyData<GOAL>leftHomologyMap' φ S₁.homologyData.left S₂.homologyData.left = ((S₁.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S₁) S₁.homologyData.right S₁.rightHomologyData) ≫ rightHomologyMap' (𝟙 S₁) S₁.rightHomologyData h₁) ≫ γ.φH ≫ rightHomologyMap' (𝟙 S₂) h₂ S₂.rightHomologyData ≫ rightHomologyMap' (𝟙 S₂) S₂.rightHomologyData S₂.homologyData.right ≫ S₂.homologyData.iso.inv
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X✝ Y✝ Z : C<VAR>D : Type u_1<VAR>E : Type u_2<VAR>inst✝¹ : Category.{u_3, u_1} D<VAR>inst✝ : Category.{?u.30898, u_2} E<VAR>X Y : C<VAR>e : X ≅ Y<VAR>F : C ⥤ D<GOAL>F.map e.inv ≫ F.map e.hom = 𝟙 (F.obj Y)
<VAR>x✝¹ y✝¹ z✝¹ w x✝ y✝ z✝ x : ℝ<VAR>hx : 0 < x<VAR>y z : ℝ<GOAL>x ^ (y - z) = x ^ y / x ^ z
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>r t : ℝ<VAR>hr : 0 < r<VAR>ht : 0 < t<VAR>x : E<GOAL>t ≤ (1 + ‖x‖) ^ (-r) ↔ ‖x‖ ≤ t ^ (-r⁻¹) - 1
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>r t : ℝ<VAR>hr : 0 < r<VAR>ht : 0 < t<VAR>x : E<GOAL>t ≤ (1 + ‖x‖) ^ (-r) ↔ 1 + ‖x‖ ≤ t ^ (-r)⁻¹
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>f : Quotient (QuotientGroup.rightRel H) → G<VAR>hf : ∀ (q : Quotient (QuotientGroup.rightRel H)), Quotient.mk'' (f q) = q<VAR>q₁ q₂ : Quotient (QuotientGroup.rightRel H)<VAR>h : (range f).restrict Quotient.mk'' ⟨f q₁, ⋯⟩ = (range f).restrict Quotient.mk'' ⟨f q₂, ⋯⟩<GOAL>⟨f q₁, ⋯⟩ = ⟨f q₂, ⋯⟩
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>K : Type u_5<VAR>inst✝ : LinearOrderedSemifield K<VAR>p✝ q✝ p q : ℚ≥0<VAR>h : p < q<GOAL>↑p < ↑q
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>K : Type u_5<VAR>inst✝ : LinearOrderedSemifield K<VAR>p✝ q✝ p q : ℚ≥0<VAR>h : p < q<GOAL>0 < ↑p.den
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>K : Type u_5<VAR>inst✝ : LinearOrderedSemifield K<VAR>p✝ q✝ p q : ℚ≥0<VAR>h : p < q<GOAL>0 < ↑q.den
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>inst✝³ : CommRing P'<VAR>inst✝² : Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>P'' : Type u_4<VAR>inst✝¹ : CommRing P''<VAR>inst✝ : Algebra R P''<VAR>loc'' : IsLocalization S P''<VAR>I✝ J : FractionalIdeal S P<VAR>g : P →ₐ[R] P'<VAR>I : Ideal R<VAR>x : P'<GOAL>x ∈ map g ↑I ↔ x ∈ ↑I
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>P' : Type u_3<VAR>inst✝³ : CommRing P'<VAR>inst✝² : Algebra R P'<VAR>loc' : IsLocalization S P'<VAR>P'' : Type u_4<VAR>inst✝¹ : CommRing P''<VAR>inst✝ : Algebra R P''<VAR>loc'' : IsLocalization S P''<VAR>I✝ J : FractionalIdeal S P<VAR>g : P →ₐ[R] P'<VAR>I : Ideal R<VAR>x : P'<GOAL>x ∈ map g ↑I ↔ ∃ x' ∈ I, (algebraMap R P') x' = x
<VAR>a b : ℤ<VAR>r : ℕ<VAR>h : IsNat (a % -b) r<GOAL>a % b = ↑r
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra R A<VAR>N✝ : LieSubmodule R L M<VAR>I : LieIdeal R L<VAR>N : LieSubmodule R L M<VAR>s : Set (A ⊗[R] M) := {m | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}<VAR>this : ⇑((TensorProduct.mk R A M) 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} = s<GOAL>baseChange A ⁅I, N⁆ = ⁅baseChange A I, baseChange A N⁆
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra R A<VAR>N✝ : LieSubmodule R L M<VAR>I : LieIdeal R L<VAR>N : LieSubmodule R L M<VAR>s : Set (A ⊗[R] M) := {m | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}<VAR>this : ⇑((TensorProduct.mk R A M) 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} = s<GOAL>Submodule.span A s = Submodule.span A {m | ∃ x ∈ baseChange A I, ∃ n ∈ baseChange A N, ⁅x, n⁆ = m}
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra R A<VAR>N✝ : LieSubmodule R L M<VAR>I : LieIdeal R L<VAR>N : LieSubmodule R L M<VAR>s : Set (A ⊗[R] M) := {m | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}<VAR>this : ⇑((TensorProduct.mk R A M) 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} = s<GOAL>s ⊆ {m | ∃ x ∈ baseChange A I, ∃ n ∈ baseChange A N, ⁅x, n⁆ = m}
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra R A<VAR>N✝ : LieSubmodule R L M<VAR>I : LieIdeal R L<VAR>N : LieSubmodule R L M<VAR>s : Set (A ⊗[R] M) := {m | ∃ x ∈ I, ∃ n ∈ N, 1 ⊗ₜ[R] ⁅x, n⁆ = m}<VAR>this : ⇑((TensorProduct.mk R A M) 1) '' {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m} = s<GOAL>{m | ∃ x ∈ baseChange A I, ∃ n ∈ baseChange A N, ⁅x, n⁆ = m} ⊆ ↑(Submodule.span A s)