ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u_3<VAR>inst✝¹ : Category.{u_1, u_3} C<VAR>r : HomRel C<VAR>D : Type u_4<VAR>inst✝ : Category.{u_2, u_4} D<VAR>F✝ : C ⥤ D<VAR>H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F✝.map f₁ = F✝.map f₂<VAR>F G : Quotient r ⥤ D<VAR>τ₁ τ₂ : F ⟶ G<VAR>h : whiskerLeft (functor r) τ₁ = whiskerLeft (functor r) τ₂<VAR>X : C<GOAL>τ₁.app { as := X } = τ₂.app { as := X }
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l : List α<GOAL>l.sublists.length = 2 ^ l.length
<VAR>K : Type u_1<VAR>R : 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✝⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : IsNoetherian R M<VAR>inst✝ : IsArtinian R M<VAR>h : ∀ N < ⊤, IsCompl (weightSpace (↥↑N) 0) (posFittingComp R L ↥↑N)<VAR>M₀ : LieSubmodule R L M := weightSpace M 0<VAR>M₁ : LieSubmodule R L M := posFittingComp R L M<GOAL>IsCompl M₀ M₁
<VAR>K : Type u_1<VAR>R : 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✝⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : IsNoetherian R M<VAR>inst✝ : IsArtinian R M<VAR>h✝ : ∀ N < ⊤, IsCompl (weightSpace (↥↑N) 0) (posFittingComp R L ↥↑N)<VAR>M₀ : LieSubmodule R L M := weightSpace M 0<VAR>M₁ : LieSubmodule R L M := posFittingComp R L M<VAR>h : ∀ (a : L), weightSpaceOf M 0 a = ⊤<GOAL>IsCompl M₀ M₁
<VAR>K : Type u_1<VAR>R : 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✝⁶ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : LieRingModule L M<VAR>inst✝² : LieModule R L M<VAR>inst✝¹ : IsNoetherian R M<VAR>inst✝ : IsArtinian R M<VAR>h : ∀ N < ⊤, IsCompl (weightSpace (↥↑N) 0) (posFittingComp R L ↥↑N)<VAR>M₀ : LieSubmodule R L M := weightSpace M 0<VAR>M₁ : LieSubmodule R L M := posFittingComp R L M<VAR>x : L<VAR>hx : weightSpaceOf M 0 x ≠ ⊤<GOAL>IsCompl M₀ M₁
<VAR>u : ℕ → ℝ<VAR>h : Subadditive u<VAR>hbdd : BddBelow (range fun n => u n / ↑n)<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>sInf ((fun n => u n / ↑n) '' Ici 1) ≤ u n / ↑n
<VAR>σ₁ σ₂ : Type u_1<VAR>f₁ : σ₁ → Option σ₁<VAR>f₂ : σ₂ → Option σ₂<VAR>tr : σ₁ → σ₂<VAR>H : Respects f₁ f₂ fun a b => tr a = b<VAR>a₁ : σ₁<VAR>b₂ : σ₂<VAR>h : b₂ ∈ tr <$> eval f₁ a₁<GOAL>b₂ ∈ eval f₂ (tr a₁)
<VAR>σ₁ σ₂ : Type u_1<VAR>f₁ : σ₁ → Option σ₁<VAR>f₂ : σ₂ → Option σ₂<VAR>tr : σ₁ → σ₂<VAR>H : Respects f₁ f₂ fun a b => tr a = b<VAR>a₁ : σ₁<VAR>b₂ : σ₂<VAR>h : b₂ ∈ tr <$> eval f₁ a₁<VAR>b₁ : σ₁<VAR>ab : b₁ ∈ eval f₁ a₁<VAR>bb : tr b₁ = b₂<GOAL>b₂ ∈ eval f₂ (tr a₁)
<VAR>σ₁ σ₂ : Type u_1<VAR>f₁ : σ₁ → Option σ₁<VAR>f₂ : σ₂ → Option σ₂<VAR>tr : σ₁ → σ₂<VAR>H : Respects f₁ f₂ fun a b => tr a = b<VAR>a₁ : σ₁<VAR>b₂ : σ₂<VAR>h✝ : b₂ ∈ tr <$> eval f₁ a₁<VAR>b₁ : σ₁<VAR>ab : b₁ ∈ eval f₁ a₁<VAR>bb : tr b₁ = b₂<VAR>h : tr b₁ ∈ eval f₂ (tr a₁)<GOAL>b₂ ∈ eval f₂ (tr a₁)
<VAR>m n✝ n a : ℕ<VAR>h : a < n<GOAL>(↑a).val = a
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p : R<VAR>k✝ n k : ℕ<VAR>hk : k ≠ 0<GOAL>IsPrimePow (n ^ k) ↔ IsPrimePow n
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p : R<VAR>k✝ n k : ℕ<VAR>hk : k ≠ 0<GOAL>(∃! p, Nat.Prime p ∧ p ∣ n ^ k) ↔ ∃! p, Nat.Prime p ∧ p ∣ n
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p : R<VAR>k✝ n k : ℕ<VAR>hk : k ≠ 0<GOAL>∀ (a : ℕ), Nat.Prime a ∧ a ∣ n ^ k ↔ Nat.Prime a ∧ a ∣ n
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p : R<VAR>k✝ n k : ℕ<VAR>hk : k ≠ 0<GOAL>∀ (a : ℕ), Nat.Prime a → (a ∣ n ^ k ↔ a ∣ n)
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n✝ p✝ : R<VAR>k✝ n k : ℕ<VAR>hk : k ≠ 0<VAR>p : ℕ<VAR>hp : Nat.Prime p<GOAL>p ∣ n ^ k ↔ p ∣ n
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<GOAL>Inducing (⇑UniformFun.ofFun ∘ DFunLike.coe)
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>f g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<GOAL>∀ (x : α →ᵇ β), 𝓝 x = comap (⇑UniformFun.ofFun ∘ DFunLike.coe) (𝓝 ((⇑UniformFun.ofFun ∘ DFunLike.coe) x))
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>f✝ g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>f : α →ᵇ β<VAR>l : Filter (α →ᵇ β)<GOAL>l ≤ 𝓝 f ↔ l ≤ comap (⇑UniformFun.ofFun ∘ DFunLike.coe) (𝓝 ((⇑UniformFun.ofFun ∘ DFunLike.coe) f))
<VAR>F : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : PseudoMetricSpace β<VAR>inst✝ : PseudoMetricSpace γ<VAR>f✝ g : α →ᵇ β<VAR>x : α<VAR>C : ℝ<VAR>f : α →ᵇ β<VAR>l : Filter (α →ᵇ β)<GOAL>TendstoUniformly (fun i => ⇑(id i)) (⇑f) l ↔ TendstoUniformly (⇑UniformFun.toFun ∘ ⇑UniformFun.ofFun ∘ DFunLike.coe) (UniformFun.toFun ((⇑UniformFun.ofFun ∘ DFunLike.coe) f)) l
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝³ : Fintype ι<VAR>m✝ : (i : ι) → OuterMeasure (α i)<VAR>m : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝¹ : Fintype ι'<VAR>p : ι → Prop<VAR>inst✝ : DecidablePred p<VAR>e : ((i : Subtype p) → α ↑i) × ((i : { i // ¬p i }) → α ↑i) ≃ᵐ ((i : ι) → α i) := (MeasurableEquiv.piEquivPiSubtypeProd α p).symm<GOAL>MeasurePreserving (⇑(MeasurableEquiv.piEquivPiSubtypeProd α p)) (Measure.pi μ) ((Measure.pi fun i => μ ↑i).prod (Measure.pi fun i => μ ↑i))
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝³ : Fintype ι<VAR>m✝ : (i : ι) → OuterMeasure (α i)<VAR>m : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝¹ : Fintype ι'<VAR>p : ι → Prop<VAR>inst✝ : DecidablePred p<VAR>e : ((i : Subtype p) → α ↑i) × ((i : { i // ¬p i }) → α ↑i) ≃ᵐ ((i : ι) → α i) := (MeasurableEquiv.piEquivPiSubtypeProd α p).symm<GOAL>MeasurePreserving (⇑e) ((Measure.pi fun i => μ ↑i).prod (Measure.pi fun i => μ ↑i)) (Measure.pi μ)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝³ : Fintype ι<VAR>m✝ : (i : ι) → OuterMeasure (α i)<VAR>m : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝¹ : Fintype ι'<VAR>p : ι → Prop<VAR>inst✝ : DecidablePred p<VAR>e : ((i : Subtype p) → α ↑i) × ((i : { i // ¬p i }) → α ↑i) ≃ᵐ ((i : ι) → α i) := (MeasurableEquiv.piEquivPiSubtypeProd α p).symm<VAR>s : (i : ι) → Set (α i)<VAR>x✝ : ∀ (i : ι), MeasurableSet (s i)<GOAL>(Measure.map (⇑e) ((Measure.pi fun i => μ ↑i).prod (Measure.pi fun i => μ ↑i))) (univ.pi s) = ∏ i : ι, (μ i) (s i)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝³ : Fintype ι<VAR>m✝ : (i : ι) → OuterMeasure (α i)<VAR>m : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝¹ : Fintype ι'<VAR>p : ι → Prop<VAR>inst✝ : DecidablePred p<VAR>e : ((i : Subtype p) → α ↑i) × ((i : { i // ¬p i }) → α ↑i) ≃ᵐ ((i : ι) → α i) := (MeasurableEquiv.piEquivPiSubtypeProd α p).symm<VAR>s : (i : ι) → Set (α i)<VAR>x✝ : ∀ (i : ι), MeasurableSet (s i)<VAR>this : ⇑e ⁻¹' univ.pi s = (univ.pi fun i => s ↑i) ×ˢ univ.pi fun i => s ↑i<GOAL>(Measure.map (⇑e) ((Measure.pi fun i => μ ↑i).prod (Measure.pi fun i => μ ↑i))) (univ.pi s) = ∏ i : ι, (μ i) (s i)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : ι → Type u_3<VAR>inst✝³ : Fintype ι<VAR>m✝ : (i : ι) → OuterMeasure (α i)<VAR>m : (i : ι) → MeasurableSpace (α i)<VAR>μ : (i : ι) → Measure (α i)<VAR>inst✝² : ∀ (i : ι), SigmaFinite (μ i)<VAR>inst✝¹ : Fintype ι'<VAR>p : ι → Prop<VAR>inst✝ : DecidablePred p<VAR>e : ((i : Subtype p) → α ↑i) × ((i : { i // ¬p i }) → α ↑i) ≃ᵐ ((i : ι) → α i) := (MeasurableEquiv.piEquivPiSubtypeProd α p).symm<VAR>s : (i : ι) → Set (α i)<VAR>x✝ : ∀ (i : ι), MeasurableSet (s i)<VAR>this : ⇑e ⁻¹' univ.pi s = (univ.pi fun i => s ↑i) ×ˢ univ.pi fun i => s ↑i<GOAL>(∏ i : Subtype p, (μ ↑i) (s ↑i)) * ∏ i : { i // ¬p i }, (μ ↑i) (s ↑i) = ∏ i : ι, (μ i) (s i)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝ : CommSemiring R<VAR>φ : MvPolynomial σ R<GOAL>weightedTotalDegree 1 φ = φ.totalDegree
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>x : CoeSort.coe A<VAR>g : G × G<GOAL>(dOne A ∘ₗ dZero A) x g = 0 x g
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>x : CoeSort.coe A<VAR>g : G × G<GOAL>0 = 0 x g
<VAR>x✝ y x : ℝ<GOAL>sin (-(π / 2)) < x ↔ -1 < x
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>i j k : ι<VAR>hi : c.prev j = i<VAR>hk : c.next j = k<VAR>inst✝¹ : K.HasHomology j<VAR>inst✝ : (K.sc' i j k).HasHomology<GOAL>ShortComplex.cyclesMap ((natIsoSc' C c i j k hi hk).inv.app K) ≫ K.iCycles j = (K.sc' i j k).iCycles
<VAR>C : Type u_1<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : HasZeroMorphisms C<VAR>ι : Type u_2<VAR>c : ComplexShape ι<VAR>K : HomologicalComplex C c<VAR>i j k : ι<VAR>hi : c.prev j = i<VAR>hk : c.next j = k<VAR>inst✝¹ : K.HasHomology j<VAR>inst✝ : (K.sc' i j k).HasHomology<GOAL>(K.sc' i j k).iCycles ≫ ((natIsoSc' C c i j k hi hk).inv.app K).τ₂ = (K.sc' i j k).iCycles
<VAR>α : Type u<VAR>ι : Type v<VAR>a : Cardinal.{u}<VAR>inst✝¹ : Countable ι<VAR>f : ι → Set α<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>t : Set α<VAR>ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i<VAR>h'f : ∀ (i : ι), #↑(f i) ≤ a<VAR>g : ULift.{u, v} ι → Set (ULift.{v, u} α) := (fun x => ULift.down ⁻¹' x) ∘ f ∘ ULift.down<VAR>l' : Filter (ULift.{u, v} ι) := Filter.map ULift.up l<VAR>this : l'.NeBot<GOAL>#↑(ULift.down ⁻¹' t) ≤ lift.{v, u} a
<VAR>α : Type u<VAR>ι : Type v<VAR>a : Cardinal.{u}<VAR>inst✝¹ : Countable ι<VAR>f : ι → Set α<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>t : Set α<VAR>ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i<VAR>h'f : ∀ (i : ι), #↑(f i) ≤ a<VAR>g : ULift.{u, v} ι → Set (ULift.{v, u} α) := (fun x => ULift.down ⁻¹' x) ∘ f ∘ ULift.down<VAR>l' : Filter (ULift.{u, v} ι) := Filter.map ULift.up l<VAR>this : l'.NeBot<GOAL>∀ x ∈ ULift.down ⁻¹' t, ∀ᶠ (i : ULift.{u, v} ι) in l', x ∈ g i
<VAR>α : Type u<VAR>ι : Type v<VAR>a : Cardinal.{u}<VAR>inst✝¹ : Countable ι<VAR>f : ι → Set α<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>t : Set α<VAR>ht : ∀ x ∈ t, ∀ᶠ (i : ι) in l, x ∈ f i<VAR>h'f : ∀ (i : ι), #↑(f i) ≤ a<VAR>g : ULift.{u, v} ι → Set (ULift.{v, u} α) := (fun x => ULift.down ⁻¹' x) ∘ f ∘ ULift.down<VAR>l' : Filter (ULift.{u, v} ι) := Filter.map ULift.up l<VAR>this : l'.NeBot<GOAL>∀ (i : ULift.{u, v} ι), #↑(g i) ≤ lift.{v, u} a
<VAR>R : Type u_1<VAR>F : Type u<VAR>inst✝ : Field F<VAR>p q : F[X]<VAR>f g : RatFunc F<GOAL>↑X = (single 1) 1
<VAR>R : Type u_1<VAR>F : Type u<VAR>inst✝ : Field F<VAR>p q : F[X]<VAR>f g : RatFunc F<GOAL>(ofPowerSeries ℤ F) PowerSeries.X = (single 1) 1
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>mixedEmbedding.norm x ≠ 0 ↔ ∀ (w : InfinitePlace K), (normAtPlace w) x ≠ 0
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>¬mixedEmbedding.norm x ≠ 0 ↔ ¬∀ (w : InfinitePlace K), (normAtPlace w) x ≠ 0
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>a : ℝ<VAR>h : a ≠ 0<GOAL>ofReal |a| • Measure.map (fun x => a * x) volume = volume
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>a : ℝ<VAR>h : a ≠ 0<VAR>p q : ℚ<GOAL>volume (Ioo ↑p ↑q) = (ofReal |a| • Measure.map (fun x => a * x) volume) (Ioo ↑p ↑q)
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>a : ℝ<VAR>h✝ : a ≠ 0<VAR>p q : ℚ<VAR>h : a < 0<GOAL>volume (Ioo ↑p ↑q) = (ofReal |a| • Measure.map (fun x => a * x) volume) (Ioo ↑p ↑q)
<VAR>ι : Type u_1<VAR>inst✝ : Fintype ι<VAR>a : ℝ<VAR>h✝ : a ≠ 0<VAR>p q : ℚ<VAR>h : a > 0<GOAL>volume (Ioo ↑p ↑q) = (ofReal |a| • Measure.map (fun x => a * x) volume) (Ioo ↑p ↑q)
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n : ℕ<VAR>M : Fin n.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝¹⁴ : Semiring R<VAR>inst✝¹³ : (i : Fin n.succ) → AddCommMonoid (M i)<VAR>inst✝¹² : (i : ι) → AddCommMonoid (M₁ i)<VAR>inst✝¹¹ : AddCommMonoid M₂<VAR>inst✝¹⁰ : AddCommMonoid M₃<VAR>inst✝⁹ : AddCommMonoid M'<VAR>inst✝⁸ : (i : Fin n.succ) → Module R (M i)<VAR>inst✝⁷ : (i : ι) → Module R (M₁ i)<VAR>inst✝⁶ : Module R M₂<VAR>inst✝⁵ : Module R M₃<VAR>inst✝⁴ : Module R M'<VAR>f✝ f'✝ : MultilinearMap R M₁ M₂<VAR>M₁' : ι → Type u_1<VAR>inst✝³ : (i : ι) → AddCommMonoid (M₁' i)<VAR>inst✝² : (i : ι) → Module R (M₁' i)<VAR>M₁'' : ι → Type u_2<VAR>inst✝¹ : (i : ι) → AddCommMonoid (M₁'' i)<VAR>inst✝ : (i : ι) → Module R (M₁'' i)<VAR>g : MultilinearMap R M₁' M₂<VAR>f : (i : ι) → M₁ i ≃ₗ[R] M₁' i<VAR>f' : (i : ι) → M₁ i →ₗ[R] M₁' i := fun i => ↑(f i)<GOAL>g.compLinearMap f' = 0 ↔ g = 0
<VAR>n : ℕ<VAR>α : Type u_1<VAR>v : Vector α (n + 1)<GOAL>¬v.toList.isEmpty = true
<VAR>ι : Type uι<VAR>inst✝⁷ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝³ : SeminormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>x : ⨂[𝕜] (i : ι), E i<VAR>G : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<GOAL>‖(lift f.toMultilinearMap) x‖ ≤ projectiveSeminorm x * ‖f‖
<VAR>ι : Type uι<VAR>inst✝⁷ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝³ : SeminormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>x : ⨂[𝕜] (i : ι), E i<VAR>G : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<VAR>this : Nonempty { a // a ∈ x.lifts } := nonempty_subtype.mpr (nonempty_lifts x)<GOAL>‖(lift f.toMultilinearMap) x‖ ≤ projectiveSeminorm x * ‖f‖
<VAR>ι : Type uι<VAR>inst✝⁷ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝³ : SeminormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>x : ⨂[𝕜] (i : ι), E i<VAR>G : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<VAR>this : Nonempty { a // a ∈ x.lifts } := nonempty_subtype.mpr (nonempty_lifts x)<GOAL>‖(lift f.toMultilinearMap) x‖ ≤ ⨅ i, (List.sum ∘ List.map fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) ↑i * ‖f‖
<VAR>ι : Type uι<VAR>inst✝⁷ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝³ : SeminormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>x : ⨂[𝕜] (i : ι), E i<VAR>G : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<VAR>this : Nonempty { a // a ∈ x.lifts } := nonempty_subtype.mpr (nonempty_lifts x)<GOAL>∀ (x_1 : ↑x.lifts), ‖(lift f.toMultilinearMap) x‖ ≤ (List.sum ∘ List.map fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) ↑x_1 * ‖f‖
<VAR>ι : Type uι<VAR>inst✝⁷ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝³ : SeminormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>x : ⨂[𝕜] (i : ι), E i<VAR>G : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<VAR>this : Nonempty { a // a ∈ x.lifts } := nonempty_subtype.mpr (nonempty_lifts x)<VAR>p : FreeAddMonoid (𝕜 × ((i : ι) → E i))<VAR>hp : p ∈ x.lifts<GOAL>‖(lift f.toMultilinearMap) x‖ ≤ (List.sum ∘ List.map fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) ↑⟨p, hp⟩ * ‖f‖
<VAR>ι : Type uι<VAR>inst✝⁷ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝³ : SeminormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>x : ⨂[𝕜] (i : ι), E i<VAR>G : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<VAR>this : Nonempty { a // a ∈ x.lifts } := nonempty_subtype.mpr (nonempty_lifts x)<VAR>p : FreeAddMonoid (𝕜 × ((i : ι) → E i))<VAR>hp✝ : p ∈ x.lifts<VAR>hp : (List.map (fun x => x.1 • ⨂ₜ[𝕜] (i : ι), x.2 i) p).sum = x<GOAL>‖(lift f.toMultilinearMap) x‖ ≤ (List.sum ∘ List.map fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) ↑⟨p, hp✝⟩ * ‖f‖
<VAR>ι : Type uι<VAR>inst✝⁷ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝³ : SeminormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>x : ⨂[𝕜] (i : ι), E i<VAR>G : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<VAR>this : Nonempty { a // a ∈ x.lifts } := nonempty_subtype.mpr (nonempty_lifts x)<VAR>p : FreeAddMonoid (𝕜 × ((i : ι) → E i))<VAR>hp✝ : p ∈ x.lifts<VAR>hp : (List.map (fun x => x.1 • ⨂ₜ[𝕜] (i : ι), x.2 i) p).sum = x<GOAL>‖(↑(List.map (⇑(lift f.toMultilinearMap) ∘ fun x => x.1 • ⨂ₜ[𝕜] (i : ι), x.2 i) p)).sum‖ ≤ (List.sum ∘ List.map fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) ↑⟨p, hp✝⟩ * ‖f‖
<VAR>ι : Type uι<VAR>inst✝⁷ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝³ : SeminormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>x : ⨂[𝕜] (i : ι), E i<VAR>G : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<VAR>this : Nonempty { a // a ∈ x.lifts } := nonempty_subtype.mpr (nonempty_lifts x)<VAR>p : FreeAddMonoid (𝕜 × ((i : ι) → E i))<VAR>hp✝ : p ∈ x.lifts<VAR>hp : (List.map (fun x => x.1 • ⨂ₜ[𝕜] (i : ι), x.2 i) p).sum = x<GOAL>(Multiset.map (fun x => ‖x‖) ↑(List.map (⇑(lift f.toMultilinearMap) ∘ fun x => x.1 • ⨂ₜ[𝕜] (i : ι), x.2 i) p)).sum ≤ (List.sum ∘ List.map fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) ↑⟨p, hp✝⟩ * ‖f‖
<VAR>ι : Type uι<VAR>inst✝⁷ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝³ : SeminormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>x : ⨂[𝕜] (i : ι), E i<VAR>G : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<VAR>this : Nonempty { a // a ∈ x.lifts } := nonempty_subtype.mpr (nonempty_lifts x)<VAR>p : FreeAddMonoid (𝕜 × ((i : ι) → E i))<VAR>hp✝ : p ∈ x.lifts<VAR>hp : (List.map (fun x => x.1 • ⨂ₜ[𝕜] (i : ι), x.2 i) p).sum = x<GOAL>(List.map ((fun x => ‖x‖) ∘ ⇑(lift f.toMultilinearMap) ∘ fun x => x.1 • ⨂ₜ[𝕜] (i : ι), x.2 i) p).sum ≤ (List.map (fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) p).sum * ‖f‖
<VAR>ι : Type uι<VAR>inst✝⁷ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝³ : SeminormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>x : ⨂[𝕜] (i : ι), E i<VAR>G : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<VAR>this : Nonempty { a // a ∈ x.lifts } := nonempty_subtype.mpr (nonempty_lifts x)<VAR>p : FreeAddMonoid (𝕜 × ((i : ι) → E i))<VAR>hp✝ : p ∈ x.lifts<VAR>hp : (List.map (fun x => x.1 • ⨂ₜ[𝕜] (i : ι), x.2 i) p).sum = x<GOAL>(List.map ((fun x => ‖x‖) ∘ ⇑(lift f.toMultilinearMap) ∘ fun x => x.1 • ⨂ₜ[𝕜] (i : ι), x.2 i) p).sum ≤ (List.map (fun x => ‖f‖ • x) (List.map (fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) p)).sum
<VAR>ι : Type uι<VAR>inst✝⁷ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝³ : SeminormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>x : ⨂[𝕜] (i : ι), E i<VAR>G : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<VAR>this : Nonempty { a // a ∈ x.lifts } := nonempty_subtype.mpr (nonempty_lifts x)<VAR>p : FreeAddMonoid (𝕜 × ((i : ι) → E i))<VAR>hp✝ : p ∈ x.lifts<VAR>hp : (List.map (fun x => x.1 • ⨂ₜ[𝕜] (i : ι), x.2 i) p).sum = x<GOAL>List.Forall₂ (fun x x_1 => x ≤ x_1) (List.map ((fun x => ‖x‖) ∘ ⇑(lift f.toMultilinearMap) ∘ fun x => x.1 • ⨂ₜ[𝕜] (i : ι), x.2 i) p) (List.map (fun x => ‖f‖ • x) (List.map (fun p => ‖p.1‖ * ∏ i : ι, ‖p.2 i‖) p))
<VAR>ι : Type uι<VAR>inst✝⁷ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝³ : SeminormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>x : ⨂[𝕜] (i : ι), E i<VAR>G : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<VAR>this : Nonempty { a // a ∈ x.lifts } := nonempty_subtype.mpr (nonempty_lifts x)<VAR>p : FreeAddMonoid (𝕜 × ((i : ι) → E i))<VAR>hp✝ : p ∈ x.lifts<VAR>hp : (List.map (fun x => x.1 • ⨂ₜ[𝕜] (i : ι), x.2 i) p).sum = x<GOAL>∀ (a : 𝕜) (b : (i : ι) → E i), (a, b) ∈ p → ‖a • f fun i => b i‖ ≤ ‖f‖ * (‖a‖ * ∏ x : ι, ‖b x‖)
<VAR>ι : Type uι<VAR>inst✝⁷ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝³ : SeminormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>x : ⨂[𝕜] (i : ι), E i<VAR>G : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<VAR>this : Nonempty { a // a ∈ x.lifts } := nonempty_subtype.mpr (nonempty_lifts x)<VAR>p : FreeAddMonoid (𝕜 × ((i : ι) → E i))<VAR>hp✝ : p ∈ x.lifts<VAR>hp : (List.map (fun x => x.1 • ⨂ₜ[𝕜] (i : ι), x.2 i) p).sum = x<VAR>a : 𝕜<VAR>m : (i : ι) → E i<VAR>a✝ : (a, m) ∈ p<GOAL>‖a • f fun i => m i‖ ≤ ‖f‖ * (‖a‖ * ∏ x : ι, ‖m x‖)
<VAR>ι : Type uι<VAR>inst✝⁷ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝⁵ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁴ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝³ : SeminormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>x : ⨂[𝕜] (i : ι), E i<VAR>G : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<VAR>this : Nonempty { a // a ∈ x.lifts } := nonempty_subtype.mpr (nonempty_lifts x)<VAR>p : FreeAddMonoid (𝕜 × ((i : ι) → E i))<VAR>hp✝ : p ∈ x.lifts<VAR>hp : (List.map (fun x => x.1 • ⨂ₜ[𝕜] (i : ι), x.2 i) p).sum = x<VAR>a : 𝕜<VAR>m : (i : ι) → E i<VAR>a✝ : (a, m) ∈ p<GOAL>‖a‖ * ‖f fun i => m i‖ ≤ ‖a‖ * (‖f‖ * ∏ x : ι, ‖m x‖)
<VAR>R : Type u_1<VAR>p k : ℕ<VAR>hp : Nat.Prime p<VAR>hk : k ≠ 0<GOAL>ω (p ^ k) = 1
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : CommSemiring R₁<VAR>inst✝¹ : AddCommMonoid M₁<VAR>inst✝ : Module R₁ M₁<VAR>I₁ I₂ : R₁ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₁ →ₛₗ[I₂] M<VAR>H✝ H : B.IsRefl<VAR>h : ker B = ⊥<GOAL>ker B.flip = ⊥