ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup E'<VAR>inst✝⁹ : NormedAddCommGroup E''<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x✝ x' : G<VAR>y y' : E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜 E'<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝² : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : AddGroup G<VAR>hfg : ConvolutionExists f g L μ<VAR>hfg' : ConvolutionExists f g' L μ<VAR>x : G<GOAL>(f ⋆[L, μ] (g + g')) x = (f ⋆[L, μ] g + f ⋆[L, μ] g') x
<VAR>α : Type u_1<VAR>N : α → Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : (a : α) → DecidableEq (N a)<VAR>inst✝ : (a : α) → AddGroup (N a)<VAR>f f₁ f₂ g g₁ g₂ : Π₀ (a : α), N a<GOAL>(-f).neLocus g = f.neLocus (-g)
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Field Fq<VAR>n : ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>b : Fq[X]<VAR>hb : b ≠ 0<VAR>A : Fin n → Fq[X]<GOAL>∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Field Fq<VAR>n : ℕ<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>b : Fq[X]<VAR>hb : b ≠ 0<VAR>A : Fin n → Fq[X]<VAR>hbε : 0 < cardPowDegree b • ε<GOAL>∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Field Fq<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>b : Fq[X]<VAR>hb : b ≠ 0<VAR>hbε : 0 < cardPowDegree b • ε<VAR>n : ℕ<VAR>ih : ∀ (A : Fin n → Fq[X]), ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε<VAR>A : Fin (n + 1) → Fq[X]<GOAL>∃ t, ∀ (i₀ i₁ : Fin (n + 1)), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Field Fq<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>b : Fq[X]<VAR>hb : b ≠ 0<VAR>hbε : 0 < cardPowDegree b • ε<VAR>n : ℕ<VAR>ih : ∀ (A : Fin n → Fq[X]), ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε<VAR>A : Fin (n + 1) → Fq[X]<VAR>anti_archim' : ∀ {i j k : Fin (n + 1)} {ε : ℝ}, ↑(cardPowDegree (A i % b - A j % b)) < ε → ↑(cardPowDegree (A j % b - A k % b)) < ε → ↑(cardPowDegree (A i % b - A k % b)) < ε<GOAL>∃ t, ∀ (i₀ i₁ : Fin (n + 1)), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Field Fq<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>b : Fq[X]<VAR>hb : b ≠ 0<VAR>hbε : 0 < cardPowDegree b • ε<VAR>n : ℕ<VAR>ih : ∀ (A : Fin n → Fq[X]), ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε<VAR>A : Fin (n + 1) → Fq[X]<VAR>anti_archim' : ∀ {i j k : Fin (n + 1)} {ε : ℝ}, ↑(cardPowDegree (A i % b - A j % b)) < ε → ↑(cardPowDegree (A j % b - A k % b)) < ε → ↑(cardPowDegree (A i % b - A k % b)) < ε<VAR>t' : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)<VAR>ht' : ∀ (i₀ i₁ : Fin n), t' i₀ = t' i₁ ↔ ↑(cardPowDegree (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < cardPowDegree b • ε<VAR>j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)<VAR>hj : ∀ (i : Fin n), t' i = j → ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε<VAR>exists_nonempty_j : ¬∃ j, (∃ i, t' i = j) ∧ ∀ (i : Fin n), t' i = j → ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε<VAR>i : Fin n<VAR>hi : ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε<GOAL>t' i = j
<VAR>Fq : Type u_1<VAR>inst✝¹ : Fintype Fq<VAR>inst✝ : Field Fq<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>b : Fq[X]<VAR>hb : b ≠ 0<VAR>hbε : 0 < cardPowDegree b • ε<VAR>n : ℕ<VAR>ih : ∀ (A : Fin n → Fq[X]), ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(cardPowDegree (A i₁ % b - A i₀ % b)) < cardPowDegree b • ε<VAR>A : Fin (n + 1) → Fq[X]<VAR>anti_archim' : ∀ {i j k : Fin (n + 1)} {ε : ℝ}, ↑(cardPowDegree (A i % b - A j % b)) < ε → ↑(cardPowDegree (A j % b - A k % b)) < ε → ↑(cardPowDegree (A i % b - A k % b)) < ε<VAR>t' : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)<VAR>ht' : ∀ (i₀ i₁ : Fin n), t' i₀ = t' i₁ ↔ ↑(cardPowDegree (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < cardPowDegree b • ε<VAR>j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)<VAR>hj : ∀ (i : Fin n), t' i = j → ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε<VAR>exists_nonempty_j : ¬∃ j, (∃ i, t' i = j) ∧ ∀ (i : Fin n), t' i = j → ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε<VAR>i : Fin n<VAR>hi : ↑(cardPowDegree (A 0 % b - A i.succ % b)) < cardPowDegree b • ε<VAR>this : False<GOAL>t' i = j
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>f : R[X]<VAR>inst✝ : Algebra R S<VAR>h : IsAdjoinRoot S f<GOAL>(aeval h.root) f = 0
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>X✝ Y✝ Z : C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : Mono f<VAR>h : mk f = ⊤<GOAL>IsIso f
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>X✝ Y✝ Z : C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : Mono f<VAR>h : mk f = ⊤<GOAL>IsIso (ofMkLEMk f (𝟙 Y) ⋯)
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>R : Type v<VAR>inst✝ : CommRing R<VAR>M N P : Matrix m m R<GOAL>(M * (N * P)).det = (N * (M * P)).det
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝² : Field 𝕜<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra 𝕜 A<VAR>a : A<VAR>p : 𝕜[X]<VAR>k : 𝕜<VAR>hk : k ∈ σ a<VAR>q : 𝕜[X] := C (eval k p) - p<GOAL>(fun x => eval x p) k ∈ σ ((aeval a) p)
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝² : Field 𝕜<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra 𝕜 A<VAR>a : A<VAR>p : 𝕜[X]<VAR>k : 𝕜<VAR>hk : k ∈ σ a<VAR>q : 𝕜[X] := C (eval k p) - p<VAR>hroot : q.IsRoot k<GOAL>(fun x => eval x p) k ∈ σ ((aeval a) p)
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝² : Field 𝕜<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra 𝕜 A<VAR>a : A<VAR>p : 𝕜[X]<VAR>k : 𝕜<VAR>hk : k ∈ σ a<VAR>q : 𝕜[X] := C (eval k p) - p<VAR>hroot : (C k - X) * -(q / (X - C k)) = q<GOAL>(fun x => eval x p) k ∈ σ ((aeval a) p)
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝² : Field 𝕜<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra 𝕜 A<VAR>a : A<VAR>p : 𝕜[X]<VAR>k : 𝕜<VAR>hk : k ∈ σ a<VAR>q : 𝕜[X] := C (eval k p) - p<VAR>hroot : (C k - X) * -(q / (X - C k)) = q<VAR>aeval_q_eq : ↑ₐ (eval k p) - (aeval a) p = (aeval a) q<GOAL>(fun x => eval x p) k ∈ σ ((aeval a) p)
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝² : Field 𝕜<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra 𝕜 A<VAR>a : A<VAR>p : 𝕜[X]<VAR>k : 𝕜<VAR>hk : k ∈ σ a<VAR>q : 𝕜[X] := C (eval k p) - p<VAR>hroot : (C k - X) * -(q / (X - C k)) = q<VAR>aeval_q_eq : ↑ₐ (eval k p) - (aeval a) p = (aeval a) q<GOAL>¬IsUnit ((aeval a) (C k - X) * (aeval a) (-(q / (X - C k))))
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝² : Field 𝕜<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra 𝕜 A<VAR>a : A<VAR>p : 𝕜[X]<VAR>k : 𝕜<VAR>hk : k ∈ σ a<VAR>q : 𝕜[X] := C (eval k p) - p<VAR>hroot : (C k - X) * -(q / (X - C k)) = q<VAR>aeval_q_eq : ↑ₐ (eval k p) - (aeval a) p = (aeval a) q<VAR>hcomm : Commute ((aeval a) (C k - X)) ((aeval a) (-(q / (X - C k))))<GOAL>¬IsUnit ((aeval a) (C k - X) * (aeval a) (-(q / (X - C k))))
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝² : Field 𝕜<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra 𝕜 A<VAR>a : A<VAR>p : 𝕜[X]<VAR>k : 𝕜<VAR>hk : k ∈ σ a<VAR>q : 𝕜[X] := C (eval k p) - p<VAR>hroot : (C k - X) * -(q / (X - C k)) = q<VAR>aeval_q_eq : ↑ₐ (eval k p) - (aeval a) p = (aeval a) q<VAR>hcomm : Commute ((aeval a) (C k - X)) ((aeval a) (-(q / (X - C k))))<GOAL>¬IsUnit ((aeval a) (C k - X))
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>hn : Odd n<GOAL>a ^ n ≤ 0 ↔ a ≤ 0
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>hn : Odd n<GOAL>n ≠ 0
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>hn : Odd 0<GOAL>False
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R N<VAR>B : BilinMap R M N<VAR>N' : Type u_8<VAR>inst✝¹ : AddCommGroup N'<VAR>inst✝ : Module R N'<VAR>f : N →ₗ[R] N'<VAR>Q : QuadraticMap R M N<VAR>x✝¹ x✝ : M<GOAL>((f.compQuadraticMap' Q).polarBilin x✝¹) x✝ = ((compr₂ Q.polarBilin f) x✝¹) x✝
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : Ring B'<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : Algebra A B'<VAR>x : B<VAR>hx : IsIntegral A x<GOAL>(if hx : IsIntegral A x then ⋯.min (fun x_1 => x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx else 0).Monic
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : Ring B<VAR>inst✝² : Ring B'<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : Algebra A B'<VAR>x : B<VAR>hx : IsIntegral A x<GOAL>(⋯.min (fun x_1 => x_1.Monic ∧ eval₂ (algebraMap A B) x x_1 = 0) hx).Monic
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : Invertible 2<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x✝ y✝ z x y : P<GOAL>midpoint R x y = x ↔ x = y
<VAR>p q : ℚ<VAR>s t : Set ℚ<VAR>a✝ : FirstCountableTopology ℚ∞<GOAL>False
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>f : F ⟶ G<VAR>g : G ⟶ K<GOAL>ofHom (f ≫ g) = (ofHom f).comp (ofHom g) ⋯
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>inst✝⁵ : DecidableEq n<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : DecidableEq m<VAR>inst✝² : Fintype m<VAR>R : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Subsingleton n<VAR>A : Matrix n n R<VAR>k : n<VAR>this : Unique n<GOAL>A.det = A k k
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v w : V<VAR>e : Sym2 V<VAR>G₁ G₂ : SimpleGraph V<VAR>x✝ : Sym2 V<VAR>x y : V<GOAL>Quot.mk (Sym2.Rel V) (x, y) ∈ (G₁ ⊓ G₂).edgeSet ↔ Quot.mk (Sym2.Rel V) (x, y) ∈ G₁.edgeSet ∩ G₂.edgeSet
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : TopologicalSpace L<VAR>inst✝² : TopologicalSpace X<VAR>ι : Type u_3<VAR>α : Type u_4<VAR>s : Finset ι<VAR>f : ι → α → L<VAR>l : Filter α<VAR>g : ι → L<VAR>inst✝¹ : SemilatticeSup L<VAR>inst✝ : ContinuousSup L<VAR>hne : s.Nonempty<VAR>hs : ∀ i ∈ s, Tendsto (f i) l (𝓝 (g i))<GOAL>Tendsto (fun a => s.sup' hne fun x => f x a) l (𝓝 (s.sup' hne g))
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>b : Set (Set α)<VAR>hb : IsTopologicalBasis b<VAR>s : Set α<GOAL>Dense s ↔ ∀ o ∈ b, o.Nonempty → (o ∩ s).Nonempty
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>b : Set (Set α)<VAR>hb : IsTopologicalBasis b<VAR>s : Set α<GOAL>(∀ (x : α), ∀ o ∈ b, x ∈ o → (o ∩ s).Nonempty) ↔ ∀ o ∈ b, o.Nonempty → (o ∩ s).Nonempty
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>E : Type uE<VAR>F : Type uF<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : Semiring A<VAR>inst✝¹⁰ : Algebra R A<VAR>inst✝⁹ : Semiring B<VAR>inst✝⁸ : Algebra R B<VAR>inst✝⁷ : Semiring C<VAR>inst✝⁶ : Algebra R C<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra S A<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra S C<VAR>inst✝¹ : IsScalarTower R S A<VAR>inst✝ : IsScalarTower R S C<VAR>f g : A ⊗[R] B →ₐ[S] C<VAR>ha : f.comp includeLeft = g.comp includeLeft<VAR>hb : (AlgHom.restrictScalars R f).comp includeRight = (AlgHom.restrictScalars R g).comp includeRight<GOAL>f = g
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>E : Type uE<VAR>F : Type uF<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : Semiring A<VAR>inst✝¹⁰ : Algebra R A<VAR>inst✝⁹ : Semiring B<VAR>inst✝⁸ : Algebra R B<VAR>inst✝⁷ : Semiring C<VAR>inst✝⁶ : Algebra R C<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra S A<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra S C<VAR>inst✝¹ : IsScalarTower R S A<VAR>inst✝ : IsScalarTower R S C<VAR>f g : A ⊗[R] B →ₐ[S] C<VAR>ha : f.comp includeLeft = g.comp includeLeft<VAR>hb : (AlgHom.restrictScalars R f).comp includeRight = (AlgHom.restrictScalars R g).comp includeRight<GOAL>f.toLinearMap = g.toLinearMap
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>E : Type uE<VAR>F : Type uF<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : Semiring A<VAR>inst✝¹⁰ : Algebra R A<VAR>inst✝⁹ : Semiring B<VAR>inst✝⁸ : Algebra R B<VAR>inst✝⁷ : Semiring C<VAR>inst✝⁶ : Algebra R C<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra S A<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra S C<VAR>inst✝¹ : IsScalarTower R S A<VAR>inst✝ : IsScalarTower R S C<VAR>f g : A ⊗[R] B →ₐ[S] C<VAR>ha : f.comp includeLeft = g.comp includeLeft<VAR>hb : (AlgHom.restrictScalars R f).comp includeRight = (AlgHom.restrictScalars R g).comp includeRight<VAR>a : A<VAR>b : B<GOAL>((AlgebraTensorModule.curry f.toLinearMap) a) b = ((AlgebraTensorModule.curry g.toLinearMap) a) b
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>E : Type uE<VAR>F : Type uF<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : Semiring A<VAR>inst✝¹⁰ : Algebra R A<VAR>inst✝⁹ : Semiring B<VAR>inst✝⁸ : Algebra R B<VAR>inst✝⁷ : Semiring C<VAR>inst✝⁶ : Algebra R C<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra S A<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra S C<VAR>inst✝¹ : IsScalarTower R S A<VAR>inst✝ : IsScalarTower R S C<VAR>f g : A ⊗[R] B →ₐ[S] C<VAR>ha : f.comp includeLeft = g.comp includeLeft<VAR>hb : (AlgHom.restrictScalars R f).comp includeRight = (AlgHom.restrictScalars R g).comp includeRight<VAR>a : A<VAR>b : B<VAR>this : (f.comp includeLeft) a * ((AlgHom.restrictScalars R f).comp includeRight) b = (g.comp includeLeft) a * ((AlgHom.restrictScalars R g).comp includeRight) b<GOAL>((AlgebraTensorModule.curry f.toLinearMap) a) b = ((AlgebraTensorModule.curry g.toLinearMap) a) b
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>C : Type uC<VAR>D : Type uD<VAR>E : Type uE<VAR>F : Type uF<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : Semiring A<VAR>inst✝¹⁰ : Algebra R A<VAR>inst✝⁹ : Semiring B<VAR>inst✝⁸ : Algebra R B<VAR>inst✝⁷ : Semiring C<VAR>inst✝⁶ : Algebra R C<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra S A<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra S C<VAR>inst✝¹ : IsScalarTower R S A<VAR>inst✝ : IsScalarTower R S C<VAR>f g : A ⊗[R] B →ₐ[S] C<VAR>ha : f.comp includeLeft = g.comp includeLeft<VAR>hb : (AlgHom.restrictScalars R f).comp includeRight = (AlgHom.restrictScalars R g).comp includeRight<VAR>a : A<VAR>b : B<VAR>this : f (a ⊗ₜ[R] 1) * f (1 ⊗ₜ[R] b) = g (a ⊗ₜ[R] 1) * g (1 ⊗ₜ[R] b)<GOAL>f (a ⊗ₜ[R] b) = g (a ⊗ₜ[R] b)
<VAR>m✝ n : ℤ<VAR>x✝ : Odd n<VAR>m : ℤ<VAR>hm : n = 2 * m + 1<GOAL>n % 2 = 1
<VAR>m n : ℤ<VAR>h : n % 2 = 1<GOAL>n = 2 * (n / 2) + 1
<VAR>T : Type uT<VAR>N : Type uN<VAR>r : ContextFreeRule T N<VAR>v w : List (Symbol T N)<VAR>hvw : r.Rewrites v w<VAR>p : List (Symbol T N)<GOAL>r.Rewrites (v ++ p) (w ++ p)
<VAR>T : Type uT<VAR>N : Type uN<VAR>r : ContextFreeRule T N<VAR>v w : List (Symbol T N)<VAR>hvw : ∃ p q, v = p ++ [Symbol.nonterminal r.input] ++ q ∧ w = p ++ r.output ++ q<VAR>p : List (Symbol T N)<GOAL>∃ p_1 q, v ++ p = p_1 ++ [Symbol.nonterminal r.input] ++ q ∧ w ++ p = p_1 ++ r.output ++ q
<VAR>T : Type uT<VAR>N : Type uN<VAR>r : ContextFreeRule T N<VAR>v w p x y : List (Symbol T N)<VAR>hxy : v = x ++ [Symbol.nonterminal r.input] ++ y ∧ w = x ++ r.output ++ y<GOAL>∃ p_1 q, v ++ p = p_1 ++ [Symbol.nonterminal r.input] ++ q ∧ w ++ p = p_1 ++ r.output ++ q
<VAR>T : Type uT<VAR>N : Type uN<VAR>r : ContextFreeRule T N<VAR>v w p x y : List (Symbol T N)<VAR>hxy : v = x ++ [Symbol.nonterminal r.input] ++ y ∧ w = x ++ r.output ++ y<GOAL>v ++ p = x ++ [Symbol.nonterminal r.input] ++ (y ++ p) ∧ w ++ p = x ++ r.output ++ (y ++ p)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>p : ℝ≥0∞<VAR>μ : Measure α<VAR>G : Type u_7<VAR>inst✝ : NormedLatticeAddCommGroup G<VAR>f : ↥(simpleFunc G p μ)<GOAL>0 ≤ᶠ[ae μ] ↑↑↑f ↔ 0 ≤ f
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ✝ φ : R⟦X⟧<VAR>n : ℕ<VAR>h : ∀ i < n, (coeff R i) φ = 0<GOAL>↑n ≤ φ.order
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ✝ φ : R⟦X⟧<VAR>n : ℕ<VAR>h : ∀ i < n, (coeff R i) φ = 0<VAR>H : ¬↑n ≤ φ.order<GOAL>False
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ✝ φ : R⟦X⟧<VAR>n : ℕ<VAR>h : ∀ i < n, (coeff R i) φ = 0<VAR>H : φ.order < ↑n<GOAL>False
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ✝ φ : R⟦X⟧<VAR>n : ℕ<VAR>h : ∀ i < n, (coeff R i) φ = 0<VAR>H : φ.order < ↑n<VAR>this : φ.order.Dom<GOAL>False
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ✝ φ : R⟦X⟧<VAR>n : ℕ<VAR>h : ∀ i < n, (coeff R i) φ = 0<VAR>this : φ.order.Dom<VAR>H : φ.order.get this < n<GOAL>False
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Category.{v₂, u₂} D<VAR>L₁ L₂ : C ⥤ D<VAR>R₁ R₂ : D ⥤ C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>α : L₂ ⟶ L₁<VAR>d : D<GOAL>L₂.map (𝟙 (R₁.obj d) ≫ (adj₂.unit.app (R₁.obj d) ≫ R₂.map (𝟙 (L₂.obj (R₁.obj d)) ≫ α.app (R₁.obj d) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫ R₂.map (adj₁.counit.app d)) ≫ 𝟙 (R₂.obj d)) ≫ adj₂.counit.app d = α.app (R₁.obj d) ≫ adj₁.counit.app d
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Category.{v₂, u₂} D<VAR>L₁ L₂ : C ⥤ D<VAR>R₁ R₂ : D ⥤ C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>α : L₂ ⟶ L₁<VAR>d : D<GOAL>L₂.map (adj₂.unit.app (R₁.obj d) ≫ R₂.map (𝟙 (L₂.obj (R₁.obj d)) ≫ α.app (R₁.obj d) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫ R₂.map (adj₁.counit.app d)) ≫ adj₂.counit.app d = α.app (R₁.obj d) ≫ adj₁.counit.app d
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Category.{v₂, u₂} D<VAR>L₁ L₂ : C ⥤ D<VAR>R₁ R₂ : D ⥤ C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>α : L₂ ⟶ L₁<VAR>d : D<VAR>this : L₂.map (((mateEquiv adj₁ adj₂) (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv)).app d) ≫ adj₂.counit.app ((𝟭 D).obj d) = (L₂.leftUnitor.hom ≫ α ≫ L₁.rightUnitor.inv).app (R₁.obj d) ≫ (𝟭 D).map (adj₁.counit.app d)<GOAL>L₂.map (adj₂.unit.app (R₁.obj d) ≫ R₂.map (𝟙 (L₂.obj (R₁.obj d)) ≫ α.app (R₁.obj d) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫ R₂.map (adj₁.counit.app d)) ≫ adj₂.counit.app d = α.app (R₁.obj d) ≫ adj₁.counit.app d
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Category.{v₂, u₂} D<VAR>L₁ L₂ : C ⥤ D<VAR>R₁ R₂ : D ⥤ C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>α : L₂ ⟶ L₁<VAR>d : D<VAR>this : L₂.map (adj₂.unit.app (R₁.obj d) ≫ R₂.map (𝟙 (L₂.obj (R₁.obj d)) ≫ α.app (R₁.obj d) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫ R₂.map (adj₁.counit.app d)) ≫ adj₂.counit.app d = (𝟙 (L₂.obj (R₁.obj d)) ≫ α.app (R₁.obj d) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫ adj₁.counit.app d<GOAL>(𝟙 (L₂.obj (R₁.obj d)) ≫ α.app (R₁.obj d) ≫ 𝟙 (L₁.obj (R₁.obj d))) ≫ adj₁.counit.app d = α.app (R₁.obj d) ≫ adj₁.counit.app d
<VAR>α β : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>f : ι → Cardinal.{w}<VAR>f' : ι' → Cardinal.{w'}<VAR>hf : BddAbove (range f)<VAR>hf' : BddAbove (range f')<VAR>g : ι → ι'<VAR>h : ∀ (i : ι), lift.{w', w} (f i) ≤ lift.{w, w'} (f' (g i))<GOAL>lift.{w', w} (iSup f) ≤ lift.{w, w'} (iSup f')
<VAR>α β : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>f : ι → Cardinal.{w}<VAR>f' : ι' → Cardinal.{w'}<VAR>hf : BddAbove (range f)<VAR>hf' : BddAbove (range f')<VAR>g : ι → ι'<VAR>h : ∀ (i : ι), lift.{w', w} (f i) ≤ lift.{w, w'} (f' (g i))<GOAL>⨆ i, lift.{w', w} (f i) ≤ ⨆ i, lift.{w, w'} (f' i)
<VAR>n✝ m n : ℕ<VAR>j k : Fin n<GOAL>↑↑j < ↑↑k ↔ j < k
<VAR>ι : Type u_1<VAR>F : Filter ι<VAR>f : ι → ℝ<VAR>h : Bornology.IsBounded (range f)<GOAL>IsBounded (fun x x_1 => x ≥ x_1) (map f F)
<VAR>ι : Type u_1<VAR>F : Filter ι<VAR>f : ι → ℝ<VAR>h : Bornology.IsBounded (range f)<VAR>c : ℝ<VAR>hc : c ∈ lowerBounds (range f)<GOAL>IsBounded (fun x x_1 => x ≥ x_1) (map f F)
<VAR>p : ℝ≥0∞<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>α : ι → Type u_3<VAR>β✝ : ι → Type u_4<VAR>inst✝² : Fact (1 ≤ p)<VAR>inst✝¹ : Fintype ι<VAR>β : ι → Type u_5<VAR>inst✝ : (i : ι) → SeminormedAddCommGroup (β i)<VAR>x y : PiLp 2 β<GOAL>edist x y = (∑ i : ι, edist (x i) (y i) ^ 2) ^ (1 / 2)
<VAR>α : Type u<VAR>β : Type v<VAR>f : Perm α<VAR>s : Set α<VAR>inst✝ : Finite ↑s<VAR>h : Set.MapsTo (⇑f) s s<GOAL>Set.MapsTo (⇑f⁻¹) s s
<VAR>α : Type u<VAR>β : Type v<VAR>f : Perm α<VAR>s : Set α<VAR>inst✝ : Finite ↑s<VAR>h : Set.MapsTo (⇑f) s s<VAR>val✝ : Fintype ↑s<GOAL>Set.MapsTo (⇑f⁻¹) s s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<GOAL>(2 * X ^ 6 + C W.b₂ * X ^ 5 + 5 * C W.b₄ * X ^ 4 + 10 * C W.b₆ * X ^ 3 + 10 * C W.b₈ * X ^ 2 + C (W.b₂ * W.b₈ - W.b₄ * W.b₆) * X + C (W.b₄ * W.b₈ - W.b₆ ^ 2)).natDegree ≤ 6
<VAR>α β : Type u<VAR>a : Cardinal.{u}<VAR>h : lift.{v, u} (succ a) > succ (lift.{v, u} a)<GOAL>False
<VAR>α β : Type u<VAR>a : Cardinal.{u}<VAR>h✝ : lift.{v, u} (succ a) > succ (lift.{v, u} a)<VAR>b : Cardinal.{u}<VAR>e : lift.{v, u} b = succ (lift.{v, u} a)<VAR>h : b < succ a<GOAL>False
<VAR>α β : Type u<VAR>a : Cardinal.{u}<VAR>h✝ : lift.{v, u} (succ a) > succ (lift.{v, u} a)<VAR>b : Cardinal.{u}<VAR>e : lift.{v, u} b = succ (lift.{v, u} a)<VAR>h : succ (lift.{v, u} a) ≤ lift.{v, u} a<GOAL>False
<VAR>R : Type u<VAR>a✝ b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>a : R[ℕ]<VAR>n : ℕ<GOAL>{ toFinsupp := a ^ n } = npowRec n { toFinsupp := a }
<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>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>t : Set M'<VAR>g : M' → M''<VAR>x : M<VAR>hg : ContMDiffWithinAt I' I'' n g t (f x)<VAR>hf : ContMDiffWithinAt I I' n f s x<VAR>st : MapsTo f s t<GOAL>ContMDiffWithinAt I I'' n (g ∘ f) s x